--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/parse_spec.ML Sat May 15 23:32:15 2010 +0200
@@ -0,0 +1,167 @@
+(* Title: Pure/Isar/parse_spec.ML
+ Author: Makarius
+
+Parsers for complex specifications.
+*)
+
+signature PARSE_SPEC =
+sig
+ val attrib: Attrib.src parser
+ val attribs: Attrib.src list parser
+ val opt_attribs: Attrib.src list parser
+ val thm_name: string -> Attrib.binding parser
+ val opt_thm_name: string -> Attrib.binding parser
+ val spec: (Attrib.binding * string) parser
+ val specs: (Attrib.binding * string list) parser
+ val alt_specs: (Attrib.binding * string) list parser
+ val where_alt_specs: (Attrib.binding * string) list parser
+ val xthm: (Facts.ref * Attrib.src list) parser
+ val xthms1: (Facts.ref * Attrib.src list) list parser
+ val name_facts: (Attrib.binding * (Facts.ref * Attrib.src list) list) list parser
+ val constdecl: (binding * string option * mixfix) parser
+ val constdef: ((binding * string option * mixfix) option * (Attrib.binding * string)) parser
+ val locale_mixfix: mixfix parser
+ val locale_fixes: (binding * string option * mixfix) list parser
+ val locale_insts: (string option list * (Attrib.binding * string) list) parser
+ val class_expr: string list parser
+ val locale_expression: bool -> Expression.expression parser
+ val locale_keyword: string parser
+ val context_element: Element.context parser
+ val statement: (Attrib.binding * (string * string list) list) list parser
+ val general_statement: (Element.context list * Element.statement) parser
+ val statement_keyword: string parser
+end;
+
+structure Parse_Spec: PARSE_SPEC =
+struct
+
+(* theorem specifications *)
+
+val attrib =
+ Parse.position ((Parse.keyword_ident_or_symbolic || Parse.xname) -- Parse.!!! Args.parse)
+ >> Args.src;
+
+val attribs = Parse.$$$ "[" |-- Parse.list attrib --| Parse.$$$ "]";
+val opt_attribs = Scan.optional attribs [];
+
+fun thm_name s = Parse.binding -- opt_attribs --| Parse.$$$ s;
+
+fun opt_thm_name s =
+ Scan.optional ((Parse.binding -- opt_attribs || attribs >> pair Binding.empty) --| Parse.$$$ s)
+ Attrib.empty_binding;
+
+val spec = opt_thm_name ":" -- Parse.prop;
+val specs = opt_thm_name ":" -- Scan.repeat1 Parse.prop;
+
+val alt_specs =
+ Parse.enum1 "|"
+ (spec --| Scan.option (Scan.ahead (Parse.name || Parse.$$$ "[") -- Parse.!!! (Parse.$$$ "|")));
+
+val where_alt_specs = Parse.where_ |-- Parse.!!! alt_specs;
+
+val xthm =
+ Parse.$$$ "[" |-- attribs --| Parse.$$$ "]" >> pair (Facts.named "") ||
+ (Parse.alt_string >> Facts.Fact ||
+ Parse.position Parse.xname -- Scan.option Attrib.thm_sel >> Facts.Named) -- opt_attribs;
+
+val xthms1 = Scan.repeat1 xthm;
+
+val name_facts = Parse.and_list1 (opt_thm_name "=" -- xthms1);
+
+
+(* basic constant specifications *)
+
+val constdecl =
+ Parse.binding --
+ (Parse.where_ >> K (NONE, NoSyn) ||
+ Parse.$$$ "::" |-- Parse.!!! ((Parse.typ >> SOME) -- Parse.opt_mixfix' --| Parse.where_) ||
+ Scan.ahead (Parse.$$$ "(") |-- Parse.!!! (Parse.mixfix' --| Parse.where_ >> pair NONE))
+ >> Parse.triple2;
+
+val constdef = Scan.option constdecl -- (opt_thm_name ":" -- Parse.prop);
+
+
+(* locale and context elements *)
+
+val locale_mixfix =
+ Parse.$$$ "(" -- Parse.$$$ "structure" -- Parse.!!! (Parse.$$$ ")") >> K Structure ||
+ Parse.mixfix;
+
+val locale_fixes =
+ Parse.and_list1 (Parse.binding -- Scan.option (Parse.$$$ "::" |-- Parse.typ) -- locale_mixfix
+ >> (single o Parse.triple1) ||
+ Parse.params >> map Syntax.no_syn) >> flat;
+
+val locale_insts =
+ Scan.optional
+ (Parse.$$$ "[" |-- Parse.!!! (Scan.repeat1 (Parse.maybe Parse.term) --| Parse.$$$ "]")) [] --
+ Scan.optional (Parse.where_ |-- Parse.and_list1 (opt_thm_name ":" -- Parse.prop)) [];
+
+local
+
+val loc_element =
+ Parse.$$$ "fixes" |-- Parse.!!! locale_fixes >> Element.Fixes ||
+ Parse.$$$ "constrains" |--
+ Parse.!!! (Parse.and_list1 (Parse.name -- (Parse.$$$ "::" |-- Parse.typ)))
+ >> Element.Constrains ||
+ Parse.$$$ "assumes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp))
+ >> Element.Assumes ||
+ Parse.$$$ "defines" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Parse.propp))
+ >> Element.Defines ||
+ Parse.$$$ "notes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name "=" -- xthms1))
+ >> (curry Element.Notes "");
+
+fun plus1_unless test scan =
+ scan ::: Scan.repeat (Parse.$$$ "+" |-- Scan.unless test (Parse.!!! scan));
+
+fun prefix mandatory =
+ Parse.name --
+ (Parse.$$$ "!" >> K true || Parse.$$$ "?" >> K false || Scan.succeed mandatory) --|
+ Parse.$$$ ":";
+
+val instance = Parse.where_ |--
+ Parse.and_list1 (Parse.name -- (Parse.$$$ "=" |-- Parse.term)) >> Expression.Named ||
+ Scan.repeat1 (Parse.maybe Parse.term) >> Expression.Positional;
+
+in
+
+val locale_keyword =
+ Parse.$$$ "fixes" || Parse.$$$ "constrains" || Parse.$$$ "assumes" ||
+ Parse.$$$ "defines" || Parse.$$$ "notes";
+
+val class_expr = plus1_unless locale_keyword Parse.xname;
+
+fun locale_expression mandatory =
+ let
+ val expr2 = Parse.xname;
+ val expr1 = Scan.optional (prefix mandatory) ("", false) -- expr2 --
+ Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)));
+ val expr0 = plus1_unless locale_keyword expr1;
+ in expr0 -- Scan.optional (Parse.$$$ "for" |-- Parse.!!! locale_fixes) [] end;
+
+val context_element = Parse.group "context element" loc_element;
+
+end;
+
+
+(* statements *)
+
+val statement = Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp);
+
+val obtain_case =
+ Parse.parbinding -- (Scan.optional (Parse.simple_fixes --| Parse.where_) [] --
+ (Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat));
+
+val general_statement =
+ statement >> (fn x => ([], Element.Shows x)) ||
+ Scan.repeat context_element --
+ (Parse.$$$ "obtains" |-- Parse.!!! (Parse.enum1 "|" obtain_case) >> Element.Obtains ||
+ Parse.$$$ "shows" |-- Parse.!!! statement >> Element.Shows);
+
+val statement_keyword = Parse.$$$ "obtains" || Parse.$$$ "shows";
+
+end;
+
+(*legacy alias*)
+structure SpecParse = Parse_Spec;
+