|
1 theory Parser |
|
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" |
|
3 begin |
|
4 |
|
5 atom_decl name |
|
6 |
|
7 |
|
8 section{* Interface for nominal_datatype *} |
|
9 |
|
10 text {* |
|
11 |
|
12 Nominal-Datatype-part: |
|
13 |
|
14 1st Arg: string list |
|
15 ^^^^^^^^^^^ |
|
16 strings of the types to be defined |
|
17 |
|
18 2nd Arg: (string list * binding * mixfix * (binding * typ list * mixfix) list) list |
|
19 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ |
|
20 type(s) to be defined constructors list |
|
21 (ty args, name, syn) (name, typs, syn) |
|
22 |
|
23 Binder-Function-part: |
|
24 |
|
25 3rd Arg: (binding * typ option * mixfix) list |
|
26 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ |
|
27 binding function(s) |
|
28 to be defined |
|
29 (name, type, syn) |
|
30 |
|
31 4th Arg: term list |
|
32 ^^^^^^^^^ |
|
33 the equations of the binding functions |
|
34 (Trueprop equations) |
|
35 *} |
|
36 |
|
37 text {*****************************************************} |
|
38 ML {* |
|
39 (* nominal datatype parser *) |
|
40 local |
|
41 structure P = OuterParse |
|
42 in |
|
43 |
|
44 val _ = OuterKeyword.keyword "bind" |
|
45 val anno_typ = Scan.option (P.name --| P.$$$ "::") -- P.typ |
|
46 |
|
47 (* binding specification *) |
|
48 (* should use and_list *) |
|
49 val bind_parser = |
|
50 P.enum "," ((P.$$$ "bind" |-- P.term) -- (P.$$$ "in" |-- P.name)) |
|
51 |
|
52 val constr_parser = |
|
53 P.binding -- Scan.repeat anno_typ |
|
54 |
|
55 (* datatype parser *) |
|
56 val dt_parser = |
|
57 ((P.type_args -- P.binding -- P.opt_infix) >> P.triple1) -- |
|
58 (P.$$$ "=" |-- P.enum1 "|" ((constr_parser -- bind_parser -- P.opt_mixfix) >> P.triple_swap)) |
|
59 |
|
60 (* function equation parser *) |
|
61 val fun_parser = |
|
62 Scan.optional (P.$$$ "binder" |-- P.fixes -- SpecParse.where_alt_specs) ([],[]) |
|
63 |
|
64 (* main parser *) |
|
65 val main_parser = |
|
66 (P.and_list1 dt_parser) -- fun_parser |
|
67 |
|
68 end |
|
69 *} |
|
70 |
|
71 (* adds "_raw" to the end of constants and types *) |
|
72 ML {* |
|
73 fun add_raw s = s ^ "_raw" |
|
74 fun add_raws ss = map add_raw ss |
|
75 fun raw_bind bn = Binding.suffix_name "_raw" bn |
|
76 |
|
77 fun replace_str ss s = |
|
78 case (AList.lookup (op=) ss s) of |
|
79 SOME s' => s' |
|
80 | NONE => s |
|
81 |
|
82 fun replace_typ ty_ss (Type (a, Ts)) = Type (replace_str ty_ss a, map (replace_typ ty_ss) Ts) |
|
83 | replace_typ ty_ss T = T |
|
84 |
|
85 fun raw_dts ty_ss dts = |
|
86 let |
|
87 val ty_ss' = ty_ss ~~ (add_raws ty_ss) |
|
88 |
|
89 fun raw_dts_aux1 (bind, tys, mx) = |
|
90 (raw_bind bind, map (replace_typ ty_ss') tys, mx) |
|
91 |
|
92 fun raw_dts_aux2 (ty_args, bind, mx, constrs) = |
|
93 (ty_args, raw_bind bind, mx, map raw_dts_aux1 constrs) |
|
94 in |
|
95 map raw_dts_aux2 dts |
|
96 end |
|
97 |
|
98 fun replace_aterm trm_ss (Const (a, T)) = Const (replace_str trm_ss a, T) |
|
99 | replace_aterm trm_ss (Free (a, T)) = Free (replace_str trm_ss a, T) |
|
100 | replace_aterm trm_ss trm = trm |
|
101 |
|
102 fun replace_term trm_ss ty_ss trm = |
|
103 trm |> Term.map_aterms (replace_aterm trm_ss) |> map_types (replace_typ ty_ss) |
|
104 *} |
|
105 |
|
106 ML {* |
|
107 fun get_constrs dts = |
|
108 flat (map (fn (_, _, _, constrs) => constrs) dts) |
|
109 |
|
110 fun get_typed_constrs dts = |
|
111 flat (map (fn (_, bn, _, constrs) => |
|
112 (map (fn (bn', _, _) => (Binding.name_of bn, Binding.name_of bn')) constrs)) dts) |
|
113 |
|
114 fun get_constr_strs dts = |
|
115 map (fn (bn, _, _) => Binding.name_of bn) (get_constrs dts) |
|
116 |
|
117 fun get_bn_fun_strs bn_funs = |
|
118 map (fn (bn_fun, _, _) => Binding.name_of bn_fun) bn_funs |
|
119 *} |
|
120 |
|
121 ML {* |
|
122 fun raw_dts_decl dt_names dts lthy = |
|
123 let |
|
124 val thy = ProofContext.theory_of lthy |
|
125 val conf = Datatype.default_config |
|
126 |
|
127 val dt_names' = add_raws dt_names |
|
128 val dt_full_names = map (Sign.full_bname thy) dt_names |
|
129 val dts' = raw_dts dt_full_names dts |
|
130 in |
|
131 lthy |
|
132 |> Local_Theory.theory_result (Datatype.add_datatype conf dt_names' dts') |
|
133 end |
|
134 *} |
|
135 |
|
136 ML {* |
|
137 fun raw_bn_fun_decl dt_names dts bn_funs bn_eqs lthy = |
|
138 let |
|
139 val thy = ProofContext.theory_of lthy |
|
140 |
|
141 val dt_names' = add_raws dt_names |
|
142 val dt_full_names = map (Sign.full_bname thy) dt_names |
|
143 val dt_full_names' = map (Sign.full_bname thy) dt_names' |
|
144 |
|
145 val ctrs_names = map (Sign.full_bname thy) (get_constr_strs dts) |
|
146 val ctrs_names' = map (fn (x, y) => (Sign.full_bname_path thy (add_raw x) (add_raw y))) |
|
147 (get_typed_constrs dts) |
|
148 |
|
149 val bn_fun_strs = get_bn_fun_strs bn_funs |
|
150 val bn_fun_strs' = add_raws bn_fun_strs |
|
151 |
|
152 val bn_funs' = map (fn (bn, opt_ty, mx) => |
|
153 (raw_bind bn, Option.map (replace_typ (dt_full_names ~~ dt_full_names')) opt_ty, mx)) bn_funs |
|
154 |
|
155 val bn_eqs' = map (fn trm => |
|
156 (Attrib.empty_binding, |
|
157 (replace_term ((ctrs_names ~~ ctrs_names') @ (bn_fun_strs ~~ bn_fun_strs')) (dt_full_names ~~ dt_full_names') trm))) bn_eqs |
|
158 in |
|
159 if null bn_eqs |
|
160 then (([], []), lthy) |
|
161 else Primrec.add_primrec bn_funs' bn_eqs' lthy |
|
162 end |
|
163 *} |
|
164 |
|
165 ML {* |
|
166 fun nominal_datatype2 dts bn_funs bn_eqs lthy = |
|
167 let |
|
168 val dts_names = map (fn (_, s, _, _) => Binding.name_of s) dts |
|
169 in |
|
170 lthy |
|
171 |> raw_dts_decl dts_names dts |
|
172 ||>> raw_bn_fun_decl dts_names dts bn_funs bn_eqs |
|
173 end |
|
174 *} |
|
175 |
|
176 ML {* |
|
177 (* makes a full named type out of a binding with tvars applied to it *) |
|
178 fun mk_type thy bind tvrs = |
|
179 Type (Sign.full_name thy bind, map (fn s => TVar ((s, 0), [])) tvrs) |
|
180 |
|
181 fun get_constrs2 thy dts = |
|
182 let |
|
183 val dts' = map (fn (tvrs, tname, _, constrs) => (mk_type thy tname tvrs, constrs)) dts |
|
184 in |
|
185 flat (map (fn (ty, constrs) => map (fn (bn, tys, mx) => (bn, tys ---> ty, mx)) constrs) dts') |
|
186 end |
|
187 *} |
|
188 |
|
189 ML {* |
|
190 fun nominal_datatype2_cmd (dt_strs, (bn_fun_strs, bn_eq_strs)) lthy = |
|
191 let |
|
192 val thy = ProofContext.theory_of lthy |
|
193 |
|
194 fun prep_typ ((tvs, tname, mx), _) = (tname, length tvs, mx); |
|
195 |
|
196 (* adding the types for parsing datatypes *) |
|
197 val lthy_tmp = lthy |
|
198 |> Local_Theory.theory (Sign.add_types (map prep_typ dt_strs)) |
|
199 |
|
200 fun prep_cnstr lthy (((cname, atys), mx), binders) = |
|
201 (cname, map (Syntax.read_typ lthy o snd) atys, mx) |
|
202 |
|
203 fun prep_dt lthy ((tvs, tname, mx), cnstrs) = |
|
204 (tvs, tname, mx, map (prep_cnstr lthy) cnstrs) |
|
205 |
|
206 (* parsing the datatypes *) |
|
207 val dts_prep = map (prep_dt lthy_tmp) dt_strs |
|
208 |
|
209 (* adding constructors for parsing functions *) |
|
210 val lthy_tmp2 = lthy_tmp |
|
211 |> Local_Theory.theory (Sign.add_consts_i (get_constrs2 thy dts_prep)) |
|
212 |
|
213 val (bn_fun_aux, bn_eq_aux) = fst (Specification.read_spec bn_fun_strs bn_eq_strs lthy_tmp2) |
|
214 |
|
215 fun prep_bn_fun ((bn, T), mx) = (bn, SOME T, mx) |
|
216 |
|
217 fun prep_bn_eq (attr, t) = t |
|
218 |
|
219 val bn_fun_prep = map prep_bn_fun bn_fun_aux |
|
220 val bn_eq_prep = map prep_bn_eq bn_eq_aux |
|
221 in |
|
222 nominal_datatype2 dts_prep bn_fun_prep bn_eq_prep lthy |> snd |
|
223 end |
|
224 *} |
|
225 |
|
226 (* Command Keyword *) |
|
227 ML {* |
|
228 let |
|
229 val kind = OuterKeyword.thy_decl |
|
230 in |
|
231 OuterSyntax.local_theory "nominal_datatype" "test" kind |
|
232 (main_parser >> nominal_datatype2_cmd) |
|
233 end |
|
234 *} |
|
235 |
|
236 |
|
237 end |
|
238 |
|
239 |
|
240 |