Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: fdl_parser.ML Sprache: SML

Original von: Isabelle^©

(*  Title:      HOL/SPARK/Tools/fdl_parser.ML
    Author:     Stefan Berghofer
    Copyright:  secunet Security Networks AG

Parser for fdl files.
*)

signature FDL_PARSER =
sig
  datatype expr =
      Ident of string
    | Number of int
    | Quantifier of string * string list * string * expr
    | Funct of string * expr list
    | Element of expr * expr list
    | Update of expr * expr list * expr
    | Record of string * (string * expr) list
    | Array of string * expr option *
        ((expr * expr option) list list * expr) list;

  datatype fdl_type =
      Basic_Type of string
    | Enum_Type of string list
    | Array_Type of string list * string
    | Record_Type of (string list * string) list
    | Pending_Type;

  datatype fdl_rule =
      Inference_Rule of expr list * expr
    | Substitution_Rule of expr list * expr * expr;

  type rules =
    ((string * int) * fdl_rule) list *
    (string * (expr * (string * string) list) list) list;

  type vcs = (string * (string *
    ((string * expr) list * (string * expr) list)) list) list;

  type 'a tab = 'a Symtab.table * (string * 'a) list;

  val lookup: 'a tab -> string -> 'a option;
  val update: string * 'a -> 'a tab -> 'a tab;
  val items: 'a tab -> (string * 'a) list;

  type decls =
    {types: fdl_type tab,
     vars: string tab,
     consts: string tab,
     funs: (string list * string) tab};

  val parse_vcs: (Fdl_Lexer.chars -> 'a * Fdl_Lexer.chars) -> Position.T ->
    string -> 'a * ((string * string) * vcs);

  val parse_declarations:  Position.T -> string -> (string * string) * decls;

  val parse_rules: Position.T -> string -> rules;
end;

structure Fdl_Parser: FDL_PARSER =
struct

(** error handling **)

fun beginning n cs =
  let val dots = if length cs > n then " ..." else "";
  in
    space_implode " " (take n cs) ^ dots
  end;

fun !!! scan =
  let
    fun get_pos [] = " (end-of-input)"
      | get_pos (tok :: _) = Fdl_Lexer.pos_of tok;

    fun err (syms, msg) = fn () =>
      "Syntax error" ^ get_pos syms ^ " at " ^
        beginning 10 (map Fdl_Lexer.unparse syms) ^
        (case msg of NONE => "" | SOME m => "\n" ^ m () ^ " expected");
  in Scan.!! err scan end;

fun parse_all p =
  Scan.repeat (Scan.unless (Scan.one Fdl_Lexer.is_eof) (!!! p));

(** parsers **)

fun group s p = p || Scan.fail_with (K (fn () => s));

fun $$$ s = group s
  (Scan.one (fn t => Fdl_Lexer.kind_of t = Fdl_Lexer.Keyword andalso
     Fdl_Lexer.content_of t = s) >> K s);

val identifier = group "identifier"
  (Scan.one (fn t => Fdl_Lexer.kind_of t = Fdl_Lexer.Ident) >>
     Fdl_Lexer.content_of);

val long_identifier = group "long identifier"
  (Scan.one (fn t => Fdl_Lexer.kind_of t = Fdl_Lexer.Long_Ident) >>
     Fdl_Lexer.content_of);

fun the_identifier s = group s
  (Scan.one (fn t => Fdl_Lexer.kind_of t = Fdl_Lexer.Ident andalso
     Fdl_Lexer.content_of t = s) >> K s);

fun prfx_identifier g s = group g
  (Scan.one (fn t => Fdl_Lexer.kind_of t = Fdl_Lexer.Ident andalso
     can (unprefix s) (Fdl_Lexer.content_of t)) >>
     (unprefix s o Fdl_Lexer.content_of));

val mk_identifier = prfx_identifier "identifier \"mk__...\"" "mk__";
val hyp_identifier = prfx_identifier "hypothesis identifer" "H";
val concl_identifier = prfx_identifier "conclusion identifier" "C";

val number = group "number"
  (Scan.one (fn t => Fdl_Lexer.kind_of t = Fdl_Lexer.Number) >>
     (the o Int.fromString o Fdl_Lexer.content_of));

val traceability = group "traceability information"
  (Scan.one (fn t => Fdl_Lexer.kind_of t = Fdl_Lexer.Traceability) >>
     Fdl_Lexer.content_of);

fun enum1 sep scan = scan ::: Scan.repeat ($$$ sep |-- !!! scan);
fun enum sep scan = enum1 sep scan || Scan.succeed [];

fun list1 scan = enum1 "," scan;
fun list scan = enum "," scan;

(* expressions, see section 4.4 of SPARK Proof Manual *)

datatype expr =
    Ident of string
  | Number of int
  | Quantifier of string * string list * string * expr
  | Funct of string * expr list
  | Element of expr * expr list
  | Update of expr * expr list * expr
  | Record of string * (string * expr) list
  | Array of string * expr option *
      ((expr * expr option) list list * expr) list;

fun unop (f, x) = Funct (f, [x]);

fun binop p q = p :|-- (fn x => Scan.optional
  (q -- !!! p >> (fn (f, y) => Funct (f, [x, y]))) x);

(* left-associative *)
fun binops opp argp =
  argp -- Scan.repeat (opp -- !!! argp) >> (fn (x, fys) =>
    fold (fn (f, y) => fn x => Funct (f, [x, y])) fys x);

(* right-associative *)
fun binops' f p = enum1 f p >> foldr1 (fn (x, y) => Funct (f, [x, y]));

val multiplying_operator = $$$ "*" || $$$ "/" || $$$ "div" || $$$ "mod";

val adding_operator = $$$ "+" || $$$ "-";

val relational_operator =
     $$$ "=" || $$$ "<>"
  || $$$ "<" || $$$ ">"
  || $$$ "<="|| $$$ ">=";

val quantification_kind = $$$ "for_all" || $$$ "for_some";

val quantification_generator =
  list1 identifier --| $$$ ":" -- identifier;

fun opt_parens p = $$$ "(" |-- p --| $$$ ")" || p;

fun expression xs = group "expression"
  (binop disjunction ($$$ "->" || $$$ "<->")) xs

and disjunction xs = binops' "or" conjunction xs

and conjunction xs = binops' "and" negation xs

and negation xs =
  (   $$$ "not" -- !!! relation >> unop
   || relation) xs

and relation xs = binop sum relational_operator xs

and sum xs = binops adding_operator term xs

and term xs = binops multiplying_operator factor xs

and factor xs =
  (   $$$ "+" |-- !!! primary
   || $$$ "-" -- !!! primary >> unop
   || binop primary ($$$ "**")) xs

and primary xs = group "primary"
  (   number >> Number
   || $$$ "(" |-- !!! (expression --| $$$ ")")
   || quantified_expression
   || function_designator
   || identifier >> Ident) xs

and quantified_expression xs = (quantification_kind --
  !!! ($$$ "(" |-- quantification_generator --|  $$$ "," --
    expression --| $$$ ")") >> (fn (q, ((xs, T), e)) =>
      Quantifier (q, xs, T, e))) xs

and function_designator xs =
  (   mk_identifier --| $$$ "(" :|--
        (fn s => record_args s || array_args s) --| $$$ ")"
   || $$$ "element" |-- !!! ($$$ "(" |-- expression --| $$$ "," --| $$$ "[" --
        list1 expression --| $$$ "]" --| $$$ ")") >> Element
   || $$$ "update" |-- !!! ($$$ "(" |-- expression --| $$$ "," --| $$$ "[" --
        list1 expression --| $$$ "]" --| $$$ "," -- expression --| $$$ ")") >>
          (fn ((A, xs), x) => Update (A, xs, x))
   || identifier --| $$$ "(" -- !!! (list1 expression --| $$$ ")") >> Funct) xs

and record_args s xs =
  (list1 (identifier --| $$$ ":=" -- !!! expression) >> (pair s #> Record)) xs

and array_args s xs =
  (   array_associations >> (fn assocs => Array (s, NONE, assocs))
   || expression -- Scan.optional ($$$ "," |-- !!! array_associations) [] >>
        (fn (default, assocs) => Array (s, SOME default, assocs))) xs

and array_associations xs =
  (list1 (opt_parens (enum1 "&" ($$$ "[" |--
     !!! (list1 (expression -- Scan.option ($$$ ".." |-- !!! expression)) --|
       $$$ "]"))) --| $$$ ":=" -- expression)) xs;

(* verification conditions *)

type vcs = (string * (string *
  ((string * expr) list * (string * expr) list)) list) list;

val vc =
  identifier --| $$$ "." -- !!!
    (   $$$ "***" |-- !!! (the_identifier "true" --| $$$ ".") >>
          (Ident #> pair "1" #> single #> pair [])
     || $$$ "!!!" |-- !!! (the_identifier "false" --| $$$ ".") >>
          (Ident #> pair "1" #> single #> pair [])
     || Scan.repeat1 (hyp_identifier --
          !!! ($$$ ":" |-- expression --| $$$ ".")) --| $$$ "->" --
        Scan.repeat1 (concl_identifier --
          !!! ($$$ ":" |-- expression --| $$$ ".")));

val subprogram_kind = $$$ "function" || $$$ "procedure";

val vcs =
  subprogram_kind -- (long_identifier || identifier) --
  parse_all (traceability -- !!! (Scan.repeat1 vc));

fun parse_vcs header pos s =
  s |>
  Fdl_Lexer.tokenize header Fdl_Lexer.c_comment pos ||>
  filter Fdl_Lexer.is_proper ||>
  Scan.finite Fdl_Lexer.stopper (Scan.error (!!! vcs)) ||>
  fst;

(* fdl declarations, see section 4.3 of SPARK Proof Manual *)

datatype fdl_type =
    Basic_Type of string
  | Enum_Type of string list
  | Array_Type of string list * string
  | Record_Type of (string list * string) list
  | Pending_Type;

(* also store items in a list to preserve order *)
type 'a tab = 'a Symtab.table * (string * 'a) list;

fun lookup ((tab, _) : 'a tab) = Symtab.lookup tab;
fun update decl (tab, items) = (Symtab.update_new decl tab, decl :: items);
fun items ((_, items) : 'a tab) = rev items;

type decls =
  {types: fdl_type tab,
   vars: string tab,
   consts: string tab,
   funs: (string list * string) tab};

val empty_decls : decls =
  {types = (Symtab.empty, []), vars = (Symtab.empty, []),
   consts = (Symtab.empty, []), funs = (Symtab.empty, [])};

fun add_type_decl decl {types, vars, consts, funs} =
  {types = update decl types,
   vars = vars, consts = consts, funs = funs}
  handle Symtab.DUP s => error ("Duplicate type " ^ s);

fun add_var_decl (vs, ty) {types, vars, consts, funs} =
  {types = types,
   vars = fold (update o rpair ty) vs vars,
   consts = consts, funs = funs}
  handle Symtab.DUP s => error ("Duplicate variable " ^ s);

fun add_const_decl decl {types, vars, consts, funs} =
  {types = types, vars = vars,
   consts = update decl consts,
   funs = funs}
  handle Symtab.DUP s => error ("Duplicate constant " ^ s);

fun add_fun_decl decl {types, vars, consts, funs} =
  {types = types, vars = vars, consts = consts,
   funs = update decl funs}
  handle Symtab.DUP s => error ("Duplicate function " ^ s);

fun type_decl x = ($$$ "type" |-- !!! (identifier --| $$$ "=" --
  (   identifier >> Basic_Type
   || $$$ "(" |-- !!! (list1 identifier --| $$$ ")") >> Enum_Type
   || $$$ "array" |-- !!! ($$$ "[" |-- list1 identifier --| $$$ "]" --|
        $$$ "of" -- identifier) >> Array_Type
   || $$$ "record" |-- !!! (enum1 ";"
        (list1 identifier -- !!! ($$$ ":" |-- identifier)) --|
           $$$ "end") >> Record_Type
   || $$$ "pending" >> K Pending_Type)) >> add_type_decl) x;

fun const_decl x = ($$$ "const" |-- !!! (identifier --| $$$ ":" -- identifier --|
  $$$ "=" --| $$$ "pending") >> add_const_decl) x;

fun var_decl x = ($$$ "var" |-- !!! (list1 identifier --| $$$ ":" -- identifier) >>
  add_var_decl) x;

fun fun_decl x = ($$$ "function" |-- !!! (identifier --
  (Scan.optional ($$$ "(" |-- !!! (list1 identifier --| $$$ ")")) [] --|
   $$$ ":" -- identifier)) >> add_fun_decl) x;

fun declarations x =
(the_identifier "title" |-- subprogram_kind -- identifier --| $$$ ";" --
  (Scan.repeat ((type_decl || const_decl || var_decl || fun_decl) --|
     !!! ($$$ ";")) >> (fn ds => fold I ds empty_decls)) --|
  $$$ "end" --| $$$ ";") x;

fun parse_declarations pos s =
  s |>
  Fdl_Lexer.tokenize (Scan.succeed ()) Fdl_Lexer.curly_comment pos |>
  snd |> filter Fdl_Lexer.is_proper |>
  Scan.finite Fdl_Lexer.stopper (Scan.error (!!! declarations)) |>
  fst;

(* rules, see section 5 of SPADE Proof Checker Rules Manual *)

datatype fdl_rule =
    Inference_Rule of expr list * expr
  | Substitution_Rule of expr list * expr * expr;

type rules =
  ((string * int) * fdl_rule) list *
  (string * (expr * (string * string) list) list) list;

val condition_list = $$$ "[" |-- list expression --| $$$ "]";
val if_condition_list = $$$ "if" |-- !!! condition_list;

val rule =
  identifier -- !!! ($$$ "(" |-- number --| $$$ ")" --| $$$ ":" --
  (expression :|-- (fn e =>
        $$$ "may_be_deduced" >> K (Inference_Rule ([], e))
     || $$$ "may_be_deduced_from" |--
          !!! condition_list >> (Inference_Rule o rpair e)
     || $$$ "may_be_replaced_by" |-- !!! (expression --
          Scan.optional if_condition_list []) >> (fn (e', cs) =>
            Substitution_Rule (cs, e, e'))
     || $$$ "&" |-- !!! (expression --| $$$ "are_interchangeable" --
          Scan.optional if_condition_list []) >> (fn (e', cs) =>
            Substitution_Rule (cs, e, e')))) --| $$$ ".") >>
    (fn (id, (n, rl)) => ((id, n), rl));

val rule_family =
  $$$ "rule_family" |-- identifier --| $$$ ":" --
  enum1 "&" (expression -- !!! ($$$ "requires" |-- $$$ "[" |--
    list (identifier -- !!! ($$$ ":" |-- identifier)) --| $$$ "]")) --|
  $$$ ".";

val rules =
  parse_all (rule >> (apfst o cons) || rule_family >> (apsnd o cons)) >>
  (fn rls => fold_rev I rls ([], []));

fun parse_rules pos s =
  s |>
  Fdl_Lexer.tokenize (Scan.succeed ())
    (Fdl_Lexer.c_comment || Fdl_Lexer.percent_comment) pos |>
  snd |> filter Fdl_Lexer.is_proper |>
  Scan.finite Fdl_Lexer.stopper (Scan.error (!!! rules)) |>
  fst;

end;

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.