1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Pure/Isar/parse_spec.ML Sat May 15 23:32:15 2010 +0200
1.3 @@ -0,0 +1,167 @@
1.4 +(* Title: Pure/Isar/parse_spec.ML
1.5 + Author: Makarius
1.6 +
1.7 +Parsers for complex specifications.
1.8 +*)
1.9 +
1.10 +signature PARSE_SPEC =
1.11 +sig
1.12 + val attrib: Attrib.src parser
1.13 + val attribs: Attrib.src list parser
1.14 + val opt_attribs: Attrib.src list parser
1.15 + val thm_name: string -> Attrib.binding parser
1.16 + val opt_thm_name: string -> Attrib.binding parser
1.17 + val spec: (Attrib.binding * string) parser
1.18 + val specs: (Attrib.binding * string list) parser
1.19 + val alt_specs: (Attrib.binding * string) list parser
1.20 + val where_alt_specs: (Attrib.binding * string) list parser
1.21 + val xthm: (Facts.ref * Attrib.src list) parser
1.22 + val xthms1: (Facts.ref * Attrib.src list) list parser
1.23 + val name_facts: (Attrib.binding * (Facts.ref * Attrib.src list) list) list parser
1.24 + val constdecl: (binding * string option * mixfix) parser
1.25 + val constdef: ((binding * string option * mixfix) option * (Attrib.binding * string)) parser
1.26 + val locale_mixfix: mixfix parser
1.27 + val locale_fixes: (binding * string option * mixfix) list parser
1.28 + val locale_insts: (string option list * (Attrib.binding * string) list) parser
1.29 + val class_expr: string list parser
1.30 + val locale_expression: bool -> Expression.expression parser
1.31 + val locale_keyword: string parser
1.32 + val context_element: Element.context parser
1.33 + val statement: (Attrib.binding * (string * string list) list) list parser
1.34 + val general_statement: (Element.context list * Element.statement) parser
1.35 + val statement_keyword: string parser
1.36 +end;
1.37 +
1.38 +structure Parse_Spec: PARSE_SPEC =
1.39 +struct
1.40 +
1.41 +(* theorem specifications *)
1.42 +
1.43 +val attrib =
1.44 + Parse.position ((Parse.keyword_ident_or_symbolic || Parse.xname) -- Parse.!!! Args.parse)
1.45 + >> Args.src;
1.46 +
1.47 +val attribs = Parse.$$$ "[" |-- Parse.list attrib --| Parse.$$$ "]";
1.48 +val opt_attribs = Scan.optional attribs [];
1.49 +
1.50 +fun thm_name s = Parse.binding -- opt_attribs --| Parse.$$$ s;
1.51 +
1.52 +fun opt_thm_name s =
1.53 + Scan.optional ((Parse.binding -- opt_attribs || attribs >> pair Binding.empty) --| Parse.$$$ s)
1.54 + Attrib.empty_binding;
1.55 +
1.56 +val spec = opt_thm_name ":" -- Parse.prop;
1.57 +val specs = opt_thm_name ":" -- Scan.repeat1 Parse.prop;
1.58 +
1.59 +val alt_specs =
1.60 + Parse.enum1 "|"
1.61 + (spec --| Scan.option (Scan.ahead (Parse.name || Parse.$$$ "[") -- Parse.!!! (Parse.$$$ "|")));
1.62 +
1.63 +val where_alt_specs = Parse.where_ |-- Parse.!!! alt_specs;
1.64 +
1.65 +val xthm =
1.66 + Parse.$$$ "[" |-- attribs --| Parse.$$$ "]" >> pair (Facts.named "") ||
1.67 + (Parse.alt_string >> Facts.Fact ||
1.68 + Parse.position Parse.xname -- Scan.option Attrib.thm_sel >> Facts.Named) -- opt_attribs;
1.69 +
1.70 +val xthms1 = Scan.repeat1 xthm;
1.71 +
1.72 +val name_facts = Parse.and_list1 (opt_thm_name "=" -- xthms1);
1.73 +
1.74 +
1.75 +(* basic constant specifications *)
1.76 +
1.77 +val constdecl =
1.78 + Parse.binding --
1.79 + (Parse.where_ >> K (NONE, NoSyn) ||
1.80 + Parse.$$$ "::" |-- Parse.!!! ((Parse.typ >> SOME) -- Parse.opt_mixfix' --| Parse.where_) ||
1.81 + Scan.ahead (Parse.$$$ "(") |-- Parse.!!! (Parse.mixfix' --| Parse.where_ >> pair NONE))
1.82 + >> Parse.triple2;
1.83 +
1.84 +val constdef = Scan.option constdecl -- (opt_thm_name ":" -- Parse.prop);
1.85 +
1.86 +
1.87 +(* locale and context elements *)
1.88 +
1.89 +val locale_mixfix =
1.90 + Parse.$$$ "(" -- Parse.$$$ "structure" -- Parse.!!! (Parse.$$$ ")") >> K Structure ||
1.91 + Parse.mixfix;
1.92 +
1.93 +val locale_fixes =
1.94 + Parse.and_list1 (Parse.binding -- Scan.option (Parse.$$$ "::" |-- Parse.typ) -- locale_mixfix
1.95 + >> (single o Parse.triple1) ||
1.96 + Parse.params >> map Syntax.no_syn) >> flat;
1.97 +
1.98 +val locale_insts =
1.99 + Scan.optional
1.100 + (Parse.$$$ "[" |-- Parse.!!! (Scan.repeat1 (Parse.maybe Parse.term) --| Parse.$$$ "]")) [] --
1.101 + Scan.optional (Parse.where_ |-- Parse.and_list1 (opt_thm_name ":" -- Parse.prop)) [];
1.102 +
1.103 +local
1.104 +
1.105 +val loc_element =
1.106 + Parse.$$$ "fixes" |-- Parse.!!! locale_fixes >> Element.Fixes ||
1.107 + Parse.$$$ "constrains" |--
1.108 + Parse.!!! (Parse.and_list1 (Parse.name -- (Parse.$$$ "::" |-- Parse.typ)))
1.109 + >> Element.Constrains ||
1.110 + Parse.$$$ "assumes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp))
1.111 + >> Element.Assumes ||
1.112 + Parse.$$$ "defines" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Parse.propp))
1.113 + >> Element.Defines ||
1.114 + Parse.$$$ "notes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name "=" -- xthms1))
1.115 + >> (curry Element.Notes "");
1.116 +
1.117 +fun plus1_unless test scan =
1.118 + scan ::: Scan.repeat (Parse.$$$ "+" |-- Scan.unless test (Parse.!!! scan));
1.119 +
1.120 +fun prefix mandatory =
1.121 + Parse.name --
1.122 + (Parse.$$$ "!" >> K true || Parse.$$$ "?" >> K false || Scan.succeed mandatory) --|
1.123 + Parse.$$$ ":";
1.124 +
1.125 +val instance = Parse.where_ |--
1.126 + Parse.and_list1 (Parse.name -- (Parse.$$$ "=" |-- Parse.term)) >> Expression.Named ||
1.127 + Scan.repeat1 (Parse.maybe Parse.term) >> Expression.Positional;
1.128 +
1.129 +in
1.130 +
1.131 +val locale_keyword =
1.132 + Parse.$$$ "fixes" || Parse.$$$ "constrains" || Parse.$$$ "assumes" ||
1.133 + Parse.$$$ "defines" || Parse.$$$ "notes";
1.134 +
1.135 +val class_expr = plus1_unless locale_keyword Parse.xname;
1.136 +
1.137 +fun locale_expression mandatory =
1.138 + let
1.139 + val expr2 = Parse.xname;
1.140 + val expr1 = Scan.optional (prefix mandatory) ("", false) -- expr2 --
1.141 + Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)));
1.142 + val expr0 = plus1_unless locale_keyword expr1;
1.143 + in expr0 -- Scan.optional (Parse.$$$ "for" |-- Parse.!!! locale_fixes) [] end;
1.144 +
1.145 +val context_element = Parse.group "context element" loc_element;
1.146 +
1.147 +end;
1.148 +
1.149 +
1.150 +(* statements *)
1.151 +
1.152 +val statement = Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp);
1.153 +
1.154 +val obtain_case =
1.155 + Parse.parbinding -- (Scan.optional (Parse.simple_fixes --| Parse.where_) [] --
1.156 + (Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat));
1.157 +
1.158 +val general_statement =
1.159 + statement >> (fn x => ([], Element.Shows x)) ||
1.160 + Scan.repeat context_element --
1.161 + (Parse.$$$ "obtains" |-- Parse.!!! (Parse.enum1 "|" obtain_case) >> Element.Obtains ||
1.162 + Parse.$$$ "shows" |-- Parse.!!! statement >> Element.Shows);
1.163 +
1.164 +val statement_keyword = Parse.$$$ "obtains" || Parse.$$$ "shows";
1.165 +
1.166 +end;
1.167 +
1.168 +(*legacy alias*)
1.169 +structure SpecParse = Parse_Spec;
1.170 +