|
1 (* Title: Pure/Isar/parse_spec.ML |
|
2 Author: Makarius |
|
3 |
|
4 Parsers for complex specifications. |
|
5 *) |
|
6 |
|
7 signature PARSE_SPEC = |
|
8 sig |
|
9 val attrib: Attrib.src parser |
|
10 val attribs: Attrib.src list parser |
|
11 val opt_attribs: Attrib.src list parser |
|
12 val thm_name: string -> Attrib.binding parser |
|
13 val opt_thm_name: string -> Attrib.binding parser |
|
14 val spec: (Attrib.binding * string) parser |
|
15 val specs: (Attrib.binding * string list) parser |
|
16 val alt_specs: (Attrib.binding * string) list parser |
|
17 val where_alt_specs: (Attrib.binding * string) list parser |
|
18 val xthm: (Facts.ref * Attrib.src list) parser |
|
19 val xthms1: (Facts.ref * Attrib.src list) list parser |
|
20 val name_facts: (Attrib.binding * (Facts.ref * Attrib.src list) list) list parser |
|
21 val constdecl: (binding * string option * mixfix) parser |
|
22 val constdef: ((binding * string option * mixfix) option * (Attrib.binding * string)) parser |
|
23 val locale_mixfix: mixfix parser |
|
24 val locale_fixes: (binding * string option * mixfix) list parser |
|
25 val locale_insts: (string option list * (Attrib.binding * string) list) parser |
|
26 val class_expr: string list parser |
|
27 val locale_expression: bool -> Expression.expression parser |
|
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 end; |
|
34 |
|
35 structure Parse_Spec: PARSE_SPEC = |
|
36 struct |
|
37 |
|
38 (* theorem specifications *) |
|
39 |
|
40 val attrib = |
|
41 Parse.position ((Parse.keyword_ident_or_symbolic || Parse.xname) -- Parse.!!! Args.parse) |
|
42 >> Args.src; |
|
43 |
|
44 val attribs = Parse.$$$ "[" |-- Parse.list attrib --| Parse.$$$ "]"; |
|
45 val opt_attribs = Scan.optional attribs []; |
|
46 |
|
47 fun thm_name s = Parse.binding -- opt_attribs --| Parse.$$$ s; |
|
48 |
|
49 fun opt_thm_name s = |
|
50 Scan.optional ((Parse.binding -- opt_attribs || attribs >> pair Binding.empty) --| Parse.$$$ s) |
|
51 Attrib.empty_binding; |
|
52 |
|
53 val spec = opt_thm_name ":" -- Parse.prop; |
|
54 val specs = opt_thm_name ":" -- Scan.repeat1 Parse.prop; |
|
55 |
|
56 val alt_specs = |
|
57 Parse.enum1 "|" |
|
58 (spec --| Scan.option (Scan.ahead (Parse.name || Parse.$$$ "[") -- Parse.!!! (Parse.$$$ "|"))); |
|
59 |
|
60 val where_alt_specs = Parse.where_ |-- Parse.!!! alt_specs; |
|
61 |
|
62 val xthm = |
|
63 Parse.$$$ "[" |-- attribs --| Parse.$$$ "]" >> pair (Facts.named "") || |
|
64 (Parse.alt_string >> Facts.Fact || |
|
65 Parse.position Parse.xname -- Scan.option Attrib.thm_sel >> Facts.Named) -- opt_attribs; |
|
66 |
|
67 val xthms1 = Scan.repeat1 xthm; |
|
68 |
|
69 val name_facts = Parse.and_list1 (opt_thm_name "=" -- xthms1); |
|
70 |
|
71 |
|
72 (* basic constant specifications *) |
|
73 |
|
74 val constdecl = |
|
75 Parse.binding -- |
|
76 (Parse.where_ >> K (NONE, NoSyn) || |
|
77 Parse.$$$ "::" |-- Parse.!!! ((Parse.typ >> SOME) -- Parse.opt_mixfix' --| Parse.where_) || |
|
78 Scan.ahead (Parse.$$$ "(") |-- Parse.!!! (Parse.mixfix' --| Parse.where_ >> pair NONE)) |
|
79 >> Parse.triple2; |
|
80 |
|
81 val constdef = Scan.option constdecl -- (opt_thm_name ":" -- Parse.prop); |
|
82 |
|
83 |
|
84 (* locale and context elements *) |
|
85 |
|
86 val locale_mixfix = |
|
87 Parse.$$$ "(" -- Parse.$$$ "structure" -- Parse.!!! (Parse.$$$ ")") >> K Structure || |
|
88 Parse.mixfix; |
|
89 |
|
90 val locale_fixes = |
|
91 Parse.and_list1 (Parse.binding -- Scan.option (Parse.$$$ "::" |-- Parse.typ) -- locale_mixfix |
|
92 >> (single o Parse.triple1) || |
|
93 Parse.params >> map Syntax.no_syn) >> flat; |
|
94 |
|
95 val locale_insts = |
|
96 Scan.optional |
|
97 (Parse.$$$ "[" |-- Parse.!!! (Scan.repeat1 (Parse.maybe Parse.term) --| Parse.$$$ "]")) [] -- |
|
98 Scan.optional (Parse.where_ |-- Parse.and_list1 (opt_thm_name ":" -- Parse.prop)) []; |
|
99 |
|
100 local |
|
101 |
|
102 val loc_element = |
|
103 Parse.$$$ "fixes" |-- Parse.!!! locale_fixes >> Element.Fixes || |
|
104 Parse.$$$ "constrains" |-- |
|
105 Parse.!!! (Parse.and_list1 (Parse.name -- (Parse.$$$ "::" |-- Parse.typ))) |
|
106 >> Element.Constrains || |
|
107 Parse.$$$ "assumes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp)) |
|
108 >> Element.Assumes || |
|
109 Parse.$$$ "defines" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Parse.propp)) |
|
110 >> Element.Defines || |
|
111 Parse.$$$ "notes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name "=" -- xthms1)) |
|
112 >> (curry Element.Notes ""); |
|
113 |
|
114 fun plus1_unless test scan = |
|
115 scan ::: Scan.repeat (Parse.$$$ "+" |-- Scan.unless test (Parse.!!! scan)); |
|
116 |
|
117 fun prefix mandatory = |
|
118 Parse.name -- |
|
119 (Parse.$$$ "!" >> K true || Parse.$$$ "?" >> K false || Scan.succeed mandatory) --| |
|
120 Parse.$$$ ":"; |
|
121 |
|
122 val instance = Parse.where_ |-- |
|
123 Parse.and_list1 (Parse.name -- (Parse.$$$ "=" |-- Parse.term)) >> Expression.Named || |
|
124 Scan.repeat1 (Parse.maybe Parse.term) >> Expression.Positional; |
|
125 |
|
126 in |
|
127 |
|
128 val locale_keyword = |
|
129 Parse.$$$ "fixes" || Parse.$$$ "constrains" || Parse.$$$ "assumes" || |
|
130 Parse.$$$ "defines" || Parse.$$$ "notes"; |
|
131 |
|
132 val class_expr = plus1_unless locale_keyword Parse.xname; |
|
133 |
|
134 fun locale_expression mandatory = |
|
135 let |
|
136 val expr2 = Parse.xname; |
|
137 val expr1 = Scan.optional (prefix mandatory) ("", false) -- expr2 -- |
|
138 Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i))); |
|
139 val expr0 = plus1_unless locale_keyword expr1; |
|
140 in expr0 -- Scan.optional (Parse.$$$ "for" |-- Parse.!!! locale_fixes) [] end; |
|
141 |
|
142 val context_element = Parse.group "context element" loc_element; |
|
143 |
|
144 end; |
|
145 |
|
146 |
|
147 (* statements *) |
|
148 |
|
149 val statement = Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp); |
|
150 |
|
151 val obtain_case = |
|
152 Parse.parbinding -- (Scan.optional (Parse.simple_fixes --| Parse.where_) [] -- |
|
153 (Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat)); |
|
154 |
|
155 val general_statement = |
|
156 statement >> (fn x => ([], Element.Shows x)) || |
|
157 Scan.repeat context_element -- |
|
158 (Parse.$$$ "obtains" |-- Parse.!!! (Parse.enum1 "|" obtain_case) >> Element.Obtains || |
|
159 Parse.$$$ "shows" |-- Parse.!!! statement >> Element.Shows); |
|
160 |
|
161 val statement_keyword = Parse.$$$ "obtains" || Parse.$$$ "shows"; |
|
162 |
|
163 end; |
|
164 |
|
165 (*legacy alias*) |
|
166 structure SpecParse = Parse_Spec; |
|
167 |