author | wenzelm |
Sun, 01 Mar 2009 23:36:12 +0100 | |
changeset 30190 | 479806475f3c |
parent 29601 | 93553f7c722f |
child 30481 | de003023c302 |
permissions | -rw-r--r-- |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/Isar/spec_parse.ML |
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 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
7 |
signature SPEC_PARSE = |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
8 |
sig |
29312 | 9 |
type token = OuterParse.token |
10 |
type 'a parser = 'a OuterParse.parser |
|
11 |
val attrib: Attrib.src parser |
|
12 |
val attribs: Attrib.src list parser |
|
13 |
val opt_attribs: Attrib.src list parser |
|
14 |
val thm_name: string -> Attrib.binding parser |
|
15 |
val opt_thm_name: string -> Attrib.binding parser |
|
16 |
val spec: (Attrib.binding * string list) parser |
|
17 |
val named_spec: (Attrib.binding * string list) parser |
|
29581 | 18 |
val spec_name: ((binding * string) * Attrib.src list) parser |
19 |
val spec_opt_name: ((binding * string) * Attrib.src list) parser |
|
29312 | 20 |
val xthm: (Facts.ref * Attrib.src list) parser |
21 |
val xthms1: (Facts.ref * Attrib.src list) list parser |
|
22 |
val name_facts: (Attrib.binding * (Facts.ref * Attrib.src list) list) list parser |
|
23 |
val locale_mixfix: mixfix parser |
|
29581 | 24 |
val locale_fixes: (binding * string option * mixfix) list parser |
29312 | 25 |
val locale_insts: (string option list * (Attrib.binding * string) list) parser |
26 |
val class_expr: string list parser |
|
29601 | 27 |
val locale_expression: Expression.expression parser |
29312 | 28 |
val locale_keyword: string parser |
29 |
val context_element: Element.context parser |
|
30 |
val statement: (Attrib.binding * (string * string list) list) list parser |
|
31 |
val general_statement: (Element.context list * Element.statement) parser |
|
32 |
val statement_keyword: string parser |
|
33 |
val specification: |
|
29581 | 34 |
(binding * ((Attrib.binding * string list) list * (binding * string option) list)) list parser |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
35 |
end; |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
36 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
37 |
structure SpecParse: SPEC_PARSE = |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
38 |
struct |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
39 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
40 |
structure P = OuterParse; |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
41 |
type token = P.token; |
29312 | 42 |
type 'a parser = 'a P.parser; |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
43 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
44 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
45 |
(* theorem specifications *) |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
46 |
|
27816
0dfed2f2822a
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27378
diff
changeset
|
47 |
val attrib = P.position ((P.keyword_ident_or_symbolic || P.xname) -- P.!!! Args.parse) >> Args.src; |
24014 | 48 |
val attribs = P.$$$ "[" |-- P.list attrib --| P.$$$ "]"; |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
49 |
val opt_attribs = Scan.optional attribs []; |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
50 |
|
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27816
diff
changeset
|
51 |
fun thm_name s = P.binding -- opt_attribs --| P.$$$ s; |
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27816
diff
changeset
|
52 |
|
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
53 |
fun opt_thm_name s = |
28965 | 54 |
Scan.optional ((P.binding -- opt_attribs || attribs >> pair Binding.empty) --| P.$$$ s) |
55 |
Attrib.empty_binding; |
|
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
56 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
57 |
val spec = opt_thm_name ":" -- Scan.repeat1 P.prop; |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
58 |
val named_spec = thm_name ":" -- Scan.repeat1 P.prop; |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
59 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
60 |
val spec_name = thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y)); |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
61 |
val spec_opt_name = opt_thm_name ":" -- P.prop >> (fn ((x, y), z) => ((x, z), y)); |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
62 |
|
24013
3063a756611d
xthm: added [[declaration]] syntax (abbreviates dummy_thm [att]);
wenzelm
parents:
23919
diff
changeset
|
63 |
val xthm = |
26361 | 64 |
P.$$$ "[" |-- attribs --| P.$$$ "]" >> pair (Facts.named "") || |
65 |
(P.alt_string >> Facts.Fact || |
|
27816
0dfed2f2822a
unified Args.T with OuterLex.token, renamed some operations;
wenzelm
parents:
27378
diff
changeset
|
66 |
P.position P.xname -- Scan.option Attrib.thm_sel >> Facts.Named) -- opt_attribs; |
24013
3063a756611d
xthm: added [[declaration]] syntax (abbreviates dummy_thm [att]);
wenzelm
parents:
23919
diff
changeset
|
67 |
|
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
68 |
val xthms1 = Scan.repeat1 xthm; |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
69 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
70 |
val name_facts = P.and_list1 (opt_thm_name "=" -- xthms1); |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
71 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
72 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
73 |
(* locale and context elements *) |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
74 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
75 |
val locale_mixfix = P.$$$ "(" -- P.$$$ "structure" -- P.!!! (P.$$$ ")") >> K Structure || P.mixfix; |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
76 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
77 |
val locale_fixes = |
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27816
diff
changeset
|
78 |
P.and_list1 (P.binding -- Scan.option (P.$$$ "::" |-- P.typ) -- locale_mixfix |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
79 |
>> (single o P.triple1) || |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
80 |
P.params >> map Syntax.no_syn) >> flat; |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
81 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
82 |
val locale_insts = |
22658
263d42253f53
Experimental interpretation code for definitions.
ballarin
parents:
22104
diff
changeset
|
83 |
Scan.optional (P.$$$ "[" |-- P.!!! (Scan.repeat1 (P.maybe P.term) --| P.$$$ "]")) [] |
25094
ba43514068fd
Interpretation equations may have name and/or attribute.
ballarin
parents:
24869
diff
changeset
|
84 |
-- Scan.optional (P.$$$ "where" |-- P.and_list1 (opt_thm_name ":" -- P.prop)) []; |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
85 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
86 |
local |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
87 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
88 |
val loc_element = |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
89 |
P.$$$ "fixes" |-- P.!!! locale_fixes >> Element.Fixes || |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
90 |
P.$$$ "constrains" |-- P.!!! (P.and_list1 (P.name -- (P.$$$ "::" |-- P.typ))) |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
91 |
>> Element.Constrains || |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
92 |
P.$$$ "assumes" |-- P.!!! (P.and_list1 (opt_thm_name ":" -- Scan.repeat1 P.propp)) |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
93 |
>> Element.Assumes || |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
94 |
P.$$$ "defines" |-- P.!!! (P.and_list1 (opt_thm_name ":" -- P.propp)) |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
95 |
>> Element.Defines || |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
96 |
P.$$$ "notes" |-- P.!!! (P.and_list1 (opt_thm_name "=" -- xthms1)) |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
97 |
>> (curry Element.Notes ""); |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
98 |
|
24869 | 99 |
fun plus1_unless test scan = |
25999 | 100 |
scan ::: Scan.repeat (P.$$$ "+" |-- Scan.unless test (P.!!! scan)); |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
101 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
102 |
val rename = P.name -- Scan.option P.mixfix; |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
103 |
|
29214 | 104 |
val prefix = P.name -- Scan.optional (P.$$$ "!" >> K true) false --| P.$$$ ":"; |
29033
721529248e31
Enable keyword 'structure' in for clause of locale expression.
ballarin
parents:
28965
diff
changeset
|
105 |
val named = P.name -- (P.$$$ "=" |-- P.term); |
721529248e31
Enable keyword 'structure' in for clause of locale expression.
ballarin
parents:
28965
diff
changeset
|
106 |
val position = P.maybe P.term; |
721529248e31
Enable keyword 'structure' in for clause of locale expression.
ballarin
parents:
28965
diff
changeset
|
107 |
val instance = P.$$$ "where" |-- P.and_list1 named >> Expression.Named || |
721529248e31
Enable keyword 'structure' in for clause of locale expression.
ballarin
parents:
28965
diff
changeset
|
108 |
Scan.repeat1 position >> Expression.Positional; |
721529248e31
Enable keyword 'structure' in for clause of locale expression.
ballarin
parents:
28965
diff
changeset
|
109 |
|
24869 | 110 |
in |
111 |
||
28722 | 112 |
val locale_keyword = P.$$$ "fixes" || P.$$$ "constrains" || P.$$$ "assumes" || |
113 |
P.$$$ "defines" || P.$$$ "notes"; |
|
114 |
||
115 |
val class_expr = plus1_unless locale_keyword P.xname; |
|
24869 | 116 |
|
29033
721529248e31
Enable keyword 'structure' in for clause of locale expression.
ballarin
parents:
28965
diff
changeset
|
117 |
val locale_expression = |
721529248e31
Enable keyword 'structure' in for clause of locale expression.
ballarin
parents:
28965
diff
changeset
|
118 |
let |
721529248e31
Enable keyword 'structure' in for clause of locale expression.
ballarin
parents:
28965
diff
changeset
|
119 |
fun expr2 x = P.xname x; |
29214 | 120 |
fun expr1 x = (Scan.optional prefix ("", false) -- expr2 -- |
29033
721529248e31
Enable keyword 'structure' in for clause of locale expression.
ballarin
parents:
28965
diff
changeset
|
121 |
Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)))) x; |
721529248e31
Enable keyword 'structure' in for clause of locale expression.
ballarin
parents:
28965
diff
changeset
|
122 |
fun expr0 x = (plus1_unless locale_keyword expr1) x; |
721529248e31
Enable keyword 'structure' in for clause of locale expression.
ballarin
parents:
28965
diff
changeset
|
123 |
in expr0 -- Scan.optional (P.$$$ "for" |-- P.!!! locale_fixes) [] end; |
721529248e31
Enable keyword 'structure' in for clause of locale expression.
ballarin
parents:
28965
diff
changeset
|
124 |
|
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
125 |
val context_element = P.group "context element" loc_element; |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
126 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
127 |
end; |
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 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
130 |
(* statements *) |
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 |
val statement = P.and_list1 (opt_thm_name ":" -- Scan.repeat1 P.propp); |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
133 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
134 |
val obtain_case = |
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27816
diff
changeset
|
135 |
P.parbinding -- (Scan.optional (P.simple_fixes --| P.$$$ "where") [] -- |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
136 |
(P.and_list1 (Scan.repeat1 P.prop) >> flat)); |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
137 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
138 |
val general_statement = |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
139 |
statement >> (fn x => ([], Element.Shows x)) || |
28722 | 140 |
Scan.repeat context_element -- |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
141 |
(P.$$$ "obtains" |-- P.!!! (P.enum1 "|" obtain_case) >> Element.Obtains || |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
142 |
P.$$$ "shows" |-- P.!!! statement >> Element.Shows); |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
143 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
144 |
val statement_keyword = P.$$$ "obtains" || P.$$$ "shows"; |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
145 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
146 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
147 |
(* specifications *) |
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
148 |
|
28083
103d9282a946
explicit type Name.binding for higher-specification elements;
wenzelm
parents:
27816
diff
changeset
|
149 |
val specification = P.enum1 "|" (P.parbinding -- (P.and_list1 spec -- P.for_simple_fixes)); |
22104
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
150 |
|
e8a1c88be824
Parsers for complex specifications (material from outer_parse.ML);
wenzelm
parents:
diff
changeset
|
151 |
end; |