--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/SPARK/Tools/fdl_parser.ML Sat Jan 15 12:35:29 2011 +0100
@@ -0,0 +1,384 @@
+(* 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 [] = " (past end-of-file!)"
+ | get_pos (tok :: _) = Fdl_Lexer.pos_of tok;
+
+ fun err (syms, msg) =
+ "Syntax error" ^ get_pos syms ^ " at " ^
+ beginning 10 (map Fdl_Lexer.unparse syms) ^
+ (case msg of NONE => "" | SOME s => "\n" ^ s ^ " 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 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 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 =
+ ( expression -- Scan.optional ($$$ "," |-- !!! array_associations) [] >>
+ (fn (default, assocs) => Array (s, SOME default, assocs))
+ || array_associations >> (fn assocs => Array (s, NONE, assocs))) xs
+
+and array_associations xs =
+ (list1 (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);
+
+val type_decl = $$$ "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;
+
+val const_decl = $$$ "const" |-- !!! (identifier --| $$$ ":" -- identifier --|
+ $$$ "=" --| $$$ "pending") >> add_const_decl;
+
+val var_decl = $$$ "var" |-- !!! (list1 identifier --| $$$ ":" -- identifier) >>
+ add_var_decl;
+
+val fun_decl = $$$ "function" |-- !!! (identifier --
+ (Scan.optional ($$$ "(" |-- !!! (list1 identifier --| $$$ ")")) [] --|
+ $$$ ":" -- identifier)) >> add_fun_decl;
+
+val declarations =
+ $$$ "title" |-- subprogram_kind -- identifier --| $$$ ";" --
+ (Scan.repeat ((type_decl || const_decl || var_decl || fun_decl) --|
+ !!! ($$$ ";")) >> (fn ds => apply ds empty_decls)) --|
+ $$$ "end" --| $$$ ";"
+
+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 => apply (rev 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;