author | wenzelm |
Sat, 13 Jun 2015 13:09:05 +0200 | |
changeset 60449 | 229bad93377e |
parent 60448 | 78f3c67bc35e |
child 60555 | 51a6997b1384 |
permissions | -rw-r--r-- |
36952
338c3f8229e4
renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
wenzelm
parents:
36950
diff
changeset
|
1 |
(* Title: Pure/Isar/parse_spec.ML |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
3 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
4 |
Parsers for complex specifications. |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
5 |
*) |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
6 |
|
36952
338c3f8229e4
renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
wenzelm
parents:
36950
diff
changeset
|
7 |
signature PARSE_SPEC = |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
8 |
sig |
29312 | 9 |
val thm_name: string -> Attrib.binding parser |
10 |
val opt_thm_name: string -> Attrib.binding parser |
|
30481
de003023c302
removed old named_spec, spec_name, spec_opt_name;
wenzelm
parents:
29601
diff
changeset
|
11 |
val spec: (Attrib.binding * string) parser |
de003023c302
removed old named_spec, spec_name, spec_opt_name;
wenzelm
parents:
29601
diff
changeset
|
12 |
val specs: (Attrib.binding * string list) parser |
de003023c302
removed old named_spec, spec_name, spec_opt_name;
wenzelm
parents:
29601
diff
changeset
|
13 |
val alt_specs: (Attrib.binding * string) list parser |
de003023c302
removed old named_spec, spec_name, spec_opt_name;
wenzelm
parents:
29601
diff
changeset
|
14 |
val where_alt_specs: (Attrib.binding * string) list parser |
58011
bc6bced136e5
tuned signature -- moved type src to Token, without aliases;
wenzelm
parents:
56945
diff
changeset
|
15 |
val name_facts: (Attrib.binding * (Facts.ref * Token.src list) list) list parser |
33287
0f99569d23e1
provide SpecParse.constdecl/constdef, e.g. for quotient_definition;
wenzelm
parents:
30726
diff
changeset
|
16 |
val constdecl: (binding * string option * mixfix) parser |
0f99569d23e1
provide SpecParse.constdecl/constdef, e.g. for quotient_definition;
wenzelm
parents:
30726
diff
changeset
|
17 |
val constdef: ((binding * string option * mixfix) option * (Attrib.binding * string)) parser |
47067
4ef29b0c568f
optional 'includes' element for long theorem statements;
wenzelm
parents:
46922
diff
changeset
|
18 |
val includes: (xstring * Position.T) list parser |
29581 | 19 |
val locale_fixes: (binding * string option * mixfix) list parser |
29312 | 20 |
val locale_insts: (string option list * (Attrib.binding * string) list) parser |
46922
3717f3878714
source positions for locale and class expressions;
wenzelm
parents:
45592
diff
changeset
|
21 |
val class_expression: string list parser |
49754
acafcac41690
more explicit namespace prefix for 'statespace' -- duplicate facts;
wenzelm
parents:
47067
diff
changeset
|
22 |
val locale_prefix: bool -> (string * bool) parser |
acafcac41690
more explicit namespace prefix for 'statespace' -- duplicate facts;
wenzelm
parents:
47067
diff
changeset
|
23 |
val locale_keyword: string parser |
30726 | 24 |
val locale_expression: bool -> Expression.expression parser |
29312 | 25 |
val context_element: Element.context parser |
26 |
val statement: (Attrib.binding * (string * string list) list) list parser |
|
60449 | 27 |
val if_statement: (Attrib.binding * (string * string list) list) list parser |
60448 | 28 |
val obtains: Element.obtains parser |
29312 | 29 |
val general_statement: (Element.context list * Element.statement) parser |
30 |
val statement_keyword: string parser |
|
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
31 |
end; |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
32 |
|
36952
338c3f8229e4
renamed structure SpecParse to Parse_Spec, keeping the old name as alias for some time;
wenzelm
parents:
36950
diff
changeset
|
33 |
structure Parse_Spec: PARSE_SPEC = |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
34 |
struct |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
35 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
36 |
(* theorem specifications *) |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
37 |
|
58028
e4250d370657
tuned signature -- define some elementary operations earlier;
wenzelm
parents:
58011
diff
changeset
|
38 |
fun thm_name s = Parse.binding -- Parse.opt_attribs --| Parse.$$$ s; |
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27816
diff
changeset
|
39 |
|
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
40 |
fun opt_thm_name s = |
58028
e4250d370657
tuned signature -- define some elementary operations earlier;
wenzelm
parents:
58011
diff
changeset
|
41 |
Scan.optional |
e4250d370657
tuned signature -- define some elementary operations earlier;
wenzelm
parents:
58011
diff
changeset
|
42 |
((Parse.binding -- Parse.opt_attribs || Parse.attribs >> pair Binding.empty) --| Parse.$$$ s) |
28965 | 43 |
Attrib.empty_binding; |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
44 |
|
36950 | 45 |
val spec = opt_thm_name ":" -- Parse.prop; |
46 |
val specs = opt_thm_name ":" -- Scan.repeat1 Parse.prop; |
|
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
47 |
|
30481
de003023c302
removed old named_spec, spec_name, spec_opt_name;
wenzelm
parents:
29601
diff
changeset
|
48 |
val alt_specs = |
36950 | 49 |
Parse.enum1 "|" |
50 |
(spec --| Scan.option (Scan.ahead (Parse.name || Parse.$$$ "[") -- Parse.!!! (Parse.$$$ "|"))); |
|
30481
de003023c302
removed old named_spec, spec_name, spec_opt_name;
wenzelm
parents:
29601
diff
changeset
|
51 |
|
36950 | 52 |
val where_alt_specs = Parse.where_ |-- Parse.!!! alt_specs; |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
53 |
|
58028
e4250d370657
tuned signature -- define some elementary operations earlier;
wenzelm
parents:
58011
diff
changeset
|
54 |
val name_facts = Parse.and_list1 (opt_thm_name "=" -- Parse.xthms1); |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
55 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
56 |
|
33287
0f99569d23e1
provide SpecParse.constdecl/constdef, e.g. for quotient_definition;
wenzelm
parents:
30726
diff
changeset
|
57 |
(* basic constant specifications *) |
0f99569d23e1
provide SpecParse.constdecl/constdef, e.g. for quotient_definition;
wenzelm
parents:
30726
diff
changeset
|
58 |
|
0f99569d23e1
provide SpecParse.constdecl/constdef, e.g. for quotient_definition;
wenzelm
parents:
30726
diff
changeset
|
59 |
val constdecl = |
36950 | 60 |
Parse.binding -- |
61 |
(Parse.where_ >> K (NONE, NoSyn) || |
|
62 |
Parse.$$$ "::" |-- Parse.!!! ((Parse.typ >> SOME) -- Parse.opt_mixfix' --| Parse.where_) || |
|
63 |
Scan.ahead (Parse.$$$ "(") |-- Parse.!!! (Parse.mixfix' --| Parse.where_ >> pair NONE)) |
|
64 |
>> Parse.triple2; |
|
33287
0f99569d23e1
provide SpecParse.constdecl/constdef, e.g. for quotient_definition;
wenzelm
parents:
30726
diff
changeset
|
65 |
|
36950 | 66 |
val constdef = Scan.option constdecl -- (opt_thm_name ":" -- Parse.prop); |
33287
0f99569d23e1
provide SpecParse.constdecl/constdef, e.g. for quotient_definition;
wenzelm
parents:
30726
diff
changeset
|
67 |
|
0f99569d23e1
provide SpecParse.constdecl/constdef, e.g. for quotient_definition;
wenzelm
parents:
30726
diff
changeset
|
68 |
|
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
69 |
(* locale and context elements *) |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
70 |
|
47067
4ef29b0c568f
optional 'includes' element for long theorem statements;
wenzelm
parents:
46922
diff
changeset
|
71 |
val includes = Parse.$$$ "includes" |-- Parse.!!! (Scan.repeat1 (Parse.position Parse.xname)); |
4ef29b0c568f
optional 'includes' element for long theorem statements;
wenzelm
parents:
46922
diff
changeset
|
72 |
|
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
73 |
val locale_fixes = |
51654
8450b944e58a
just one syntax category "mixfix" -- check structure annotation semantically;
wenzelm
parents:
49754
diff
changeset
|
74 |
Parse.and_list1 (Parse.binding -- Scan.option (Parse.$$$ "::" |-- Parse.typ) -- Parse.mixfix |
36950 | 75 |
>> (single o Parse.triple1) || |
60448 | 76 |
Parse.params) >> flat; |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
77 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
78 |
val locale_insts = |
36950 | 79 |
Scan.optional |
80 |
(Parse.$$$ "[" |-- Parse.!!! (Scan.repeat1 (Parse.maybe Parse.term) --| Parse.$$$ "]")) [] -- |
|
81 |
Scan.optional (Parse.where_ |-- Parse.and_list1 (opt_thm_name ":" -- Parse.prop)) []; |
|
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
82 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
83 |
local |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
84 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
85 |
val loc_element = |
36950 | 86 |
Parse.$$$ "fixes" |-- Parse.!!! locale_fixes >> Element.Fixes || |
87 |
Parse.$$$ "constrains" |-- |
|
88 |
Parse.!!! (Parse.and_list1 (Parse.name -- (Parse.$$$ "::" |-- Parse.typ))) |
|
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
89 |
>> Element.Constrains || |
36950 | 90 |
Parse.$$$ "assumes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp)) |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
91 |
>> Element.Assumes || |
36950 | 92 |
Parse.$$$ "defines" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Parse.propp)) |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
93 |
>> Element.Defines || |
58028
e4250d370657
tuned signature -- define some elementary operations earlier;
wenzelm
parents:
58011
diff
changeset
|
94 |
Parse.$$$ "notes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name "=" -- Parse.xthms1)) |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
95 |
>> (curry Element.Notes ""); |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
96 |
|
24869 | 97 |
fun plus1_unless test scan = |
36950 | 98 |
scan ::: Scan.repeat (Parse.$$$ "+" |-- Scan.unless test (Parse.!!! scan)); |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
99 |
|
36950 | 100 |
val instance = Parse.where_ |-- |
101 |
Parse.and_list1 (Parse.name -- (Parse.$$$ "=" |-- Parse.term)) >> Expression.Named || |
|
102 |
Scan.repeat1 (Parse.maybe Parse.term) >> Expression.Positional; |
|
29033
721529248e31
Enable keyword 'structure' in for clause of locale expression.
ballarin
parents:
28965
diff
changeset
|
103 |
|
24869 | 104 |
in |
105 |
||
49754
acafcac41690
more explicit namespace prefix for 'statespace' -- duplicate facts;
wenzelm
parents:
47067
diff
changeset
|
106 |
fun locale_prefix mandatory = |
acafcac41690
more explicit namespace prefix for 'statespace' -- duplicate facts;
wenzelm
parents:
47067
diff
changeset
|
107 |
Scan.optional |
acafcac41690
more explicit namespace prefix for 'statespace' -- duplicate facts;
wenzelm
parents:
47067
diff
changeset
|
108 |
(Parse.name -- |
acafcac41690
more explicit namespace prefix for 'statespace' -- duplicate facts;
wenzelm
parents:
47067
diff
changeset
|
109 |
(Parse.$$$ "!" >> K true || Parse.$$$ "?" >> K false || Scan.succeed mandatory) --| |
acafcac41690
more explicit namespace prefix for 'statespace' -- duplicate facts;
wenzelm
parents:
47067
diff
changeset
|
110 |
Parse.$$$ ":") |
acafcac41690
more explicit namespace prefix for 'statespace' -- duplicate facts;
wenzelm
parents:
47067
diff
changeset
|
111 |
("", false); |
acafcac41690
more explicit namespace prefix for 'statespace' -- duplicate facts;
wenzelm
parents:
47067
diff
changeset
|
112 |
|
36950 | 113 |
val locale_keyword = |
114 |
Parse.$$$ "fixes" || Parse.$$$ "constrains" || Parse.$$$ "assumes" || |
|
115 |
Parse.$$$ "defines" || Parse.$$$ "notes"; |
|
28722 | 116 |
|
46922
3717f3878714
source positions for locale and class expressions;
wenzelm
parents:
45592
diff
changeset
|
117 |
val class_expression = plus1_unless locale_keyword Parse.class; |
24869 | 118 |
|
30726 | 119 |
fun locale_expression mandatory = |
29033
721529248e31
Enable keyword 'structure' in for clause of locale expression.
ballarin
parents:
28965
diff
changeset
|
120 |
let |
46922
3717f3878714
source positions for locale and class expressions;
wenzelm
parents:
45592
diff
changeset
|
121 |
val expr2 = Parse.position Parse.xname; |
49754
acafcac41690
more explicit namespace prefix for 'statespace' -- duplicate facts;
wenzelm
parents:
47067
diff
changeset
|
122 |
val expr1 = locale_prefix mandatory -- expr2 -- |
30720 | 123 |
Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i))); |
124 |
val expr0 = plus1_unless locale_keyword expr1; |
|
36950 | 125 |
in expr0 -- Scan.optional (Parse.$$$ "for" |-- Parse.!!! locale_fixes) [] end; |
29033
721529248e31
Enable keyword 'structure' in for clause of locale expression.
ballarin
parents:
28965
diff
changeset
|
126 |
|
44357 | 127 |
val context_element = Parse.group (fn () => "context element") loc_element; |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
128 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
129 |
end; |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
130 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
131 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
132 |
(* statements *) |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
133 |
|
36950 | 134 |
val statement = Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp); |
60449 | 135 |
val if_statement = Scan.optional (Parse.$$$ "if" |-- Parse.!!! statement) []; |
60414 | 136 |
|
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
137 |
val obtain_case = |
59784 | 138 |
Parse.parbinding -- |
60448 | 139 |
(Scan.optional (Parse.and_list1 Parse.fixes --| Parse.where_ >> flat) [] -- |
59784 | 140 |
(Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat)); |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
141 |
|
60448 | 142 |
val obtains = Parse.enum1 "|" obtain_case; |
143 |
||
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
144 |
val general_statement = |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
145 |
statement >> (fn x => ([], Element.Shows x)) || |
28722 | 146 |
Scan.repeat context_element -- |
60448 | 147 |
(Parse.$$$ "obtains" |-- Parse.!!! obtains >> Element.Obtains || |
36950 | 148 |
Parse.$$$ "shows" |-- Parse.!!! statement >> Element.Shows); |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
149 |
|
36950 | 150 |
val statement_keyword = Parse.$$$ "obtains" || Parse.$$$ "shows"; |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
151 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
152 |
end; |