9 |
9 |
10 text {* |
10 text {* |
11 |
11 |
12 Nominal-Datatype-part: |
12 Nominal-Datatype-part: |
13 |
13 |
14 1st Arg: string list |
14 |
15 ^^^^^^^^^^^ |
15 1nd Arg: (string list * binding * mixfix * (binding * typ list * mixfix) list) list |
16 strings of the types to be defined |
|
17 |
|
18 2nd Arg: (string list * binding * mixfix * (binding * typ list * mixfix) list) list |
|
19 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ |
16 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ |
20 type(s) to be defined constructors list |
17 type(s) to be defined constructors list |
21 (ty args, name, syn) (name, typs, syn) |
18 (ty args, name, syn) (name, typs, syn) |
22 |
19 |
23 Binder-Function-part: |
20 Binder-Function-part: |
24 |
21 |
25 3rd Arg: (binding * typ option * mixfix) list |
22 2rd Arg: (binding * typ option * mixfix) list |
26 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ |
23 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ |
27 binding function(s) |
24 binding function(s) |
28 to be defined |
25 to be defined |
29 (name, type, syn) |
26 (name, type, syn) |
30 |
27 |
31 4th Arg: term list |
28 3th Arg: term list |
32 ^^^^^^^^^ |
29 ^^^^^^^^^ |
33 the equations of the binding functions |
30 the equations of the binding functions |
34 (Trueprop equations) |
31 (Trueprop equations) |
35 *} |
32 *} |
36 |
33 |
37 text {*****************************************************} |
34 text {*****************************************************} |
38 ML {* |
35 ML {* |
39 (* nominal datatype parser *) |
36 (* nominal datatype parser *) |
40 local |
37 local |
41 structure P = OuterParse |
38 structure P = OuterParse |
|
39 |
|
40 fun tuple ((x, y, z), u) = (x, y, z, u) |
42 in |
41 in |
43 |
42 |
44 val _ = OuterKeyword.keyword "bind" |
43 val _ = OuterKeyword.keyword "bind" |
45 val anno_typ = Scan.option (P.name --| P.$$$ "::") -- P.typ |
44 val anno_typ = Scan.option (P.name --| P.$$$ "::") -- P.typ |
46 |
45 |
47 (* binding specification *) |
46 (* binding specification *) |
48 (* should use and_list *) |
47 (* maybe use and_list *) |
49 val bind_parser = |
48 val bind_parser = |
50 P.enum "," ((P.$$$ "bind" |-- P.term) -- (P.$$$ "in" |-- P.name)) |
49 P.enum "," ((P.$$$ "bind" |-- P.term) -- (P.$$$ "in" |-- P.name)) |
51 |
50 |
52 val constr_parser = |
51 val constr_parser = |
53 P.binding -- Scan.repeat anno_typ |
52 P.binding -- Scan.repeat anno_typ |
54 |
53 |
55 (* datatype parser *) |
54 (* datatype parser *) |
56 val dt_parser = |
55 val dt_parser = |
57 ((P.type_args -- P.binding -- P.opt_infix) >> P.triple1) -- |
56 (P.type_args -- P.binding -- P.opt_infix >> P.triple1) -- |
58 (P.$$$ "=" |-- P.enum1 "|" ((constr_parser -- bind_parser -- P.opt_mixfix) >> P.triple_swap)) |
57 (P.$$$ "=" |-- P.enum1 "|" (constr_parser -- bind_parser -- P.opt_mixfix >> P.triple_swap)) >> tuple |
59 |
58 |
60 (* function equation parser *) |
59 (* function equation parser *) |
61 val fun_parser = |
60 val fun_parser = |
62 Scan.optional (P.$$$ "binder" |-- P.fixes -- SpecParse.where_alt_specs) ([],[]) |
61 Scan.optional (P.$$$ "binder" |-- P.fixes -- SpecParse.where_alt_specs) ([],[]) |
63 |
62 |
64 (* main parser *) |
63 (* main parser *) |
65 val main_parser = |
64 val main_parser = |
66 (P.and_list1 dt_parser) -- fun_parser |
65 (P.and_list1 dt_parser) -- fun_parser >> P.triple2 |
67 |
66 |
68 end |
67 end |
69 *} |
68 *} |
70 |
69 |
71 (* adds "_raw" to the end of constants and types *) |
70 (* adds "_raw" to the end of constants and types *) |
139 val thy = ProofContext.theory_of lthy |
138 val thy = ProofContext.theory_of lthy |
140 |
139 |
141 val dt_names' = add_raws dt_names |
140 val dt_names' = add_raws dt_names |
142 val dt_full_names = map (Sign.full_bname thy) dt_names |
141 val dt_full_names = map (Sign.full_bname thy) dt_names |
143 val dt_full_names' = map (Sign.full_bname thy) dt_names' |
142 val dt_full_names' = map (Sign.full_bname thy) dt_names' |
|
143 val dt_env = dt_full_names ~~ dt_full_names' |
144 |
144 |
145 val ctrs_names = map (Sign.full_bname thy) (get_constr_strs dts) |
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))) |
146 val ctrs_names' = map (fn (x, y) => (Sign.full_bname_path thy (add_raw x) (add_raw y))) |
147 (get_typed_constrs dts) |
147 (get_typed_constrs dts) |
|
148 val ctrs_env = ctrs_names ~~ ctrs_names' |
148 |
149 |
149 val bn_fun_strs = get_bn_fun_strs bn_funs |
150 val bn_fun_strs = get_bn_fun_strs bn_funs |
150 val bn_fun_strs' = add_raws bn_fun_strs |
151 val bn_fun_strs' = add_raws bn_fun_strs |
|
152 val bn_fun_env = bn_fun_strs ~~ bn_fun_strs' |
151 |
153 |
152 val bn_funs' = map (fn (bn, opt_ty, mx) => |
154 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 |
155 (raw_bind bn, Option.map (replace_typ (dt_full_names ~~ dt_full_names')) opt_ty, mx)) bn_funs |
154 |
156 |
155 val bn_eqs' = map (fn trm => |
157 val bn_eqs' = map (fn trm => |
156 (Attrib.empty_binding, |
158 (Attrib.empty_binding, replace_term (ctrs_env @ bn_fun_env) dt_env trm)) bn_eqs |
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 in |
159 if null bn_eqs |
160 if null bn_eqs |
160 then (([], []), lthy) |
161 then (([], []), lthy) |
161 else Primrec.add_primrec bn_funs' bn_eqs' lthy |
162 else Primrec.add_primrec bn_funs' bn_eqs' lthy |
162 end |
163 end |
172 ||>> raw_bn_fun_decl dts_names dts bn_funs bn_eqs |
173 ||>> raw_bn_fun_decl dts_names dts bn_funs bn_eqs |
173 end |
174 end |
174 *} |
175 *} |
175 |
176 |
176 ML {* |
177 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 = |
178 fun get_constrs2 thy dts = |
182 let |
179 let |
|
180 (* makes a full named type out of a binding with tvars applied to it *) |
|
181 fun mk_type thy bind tvrs = |
|
182 Type (Sign.full_name thy bind, map (fn s => TVar ((s, 0), [])) tvrs) |
|
183 |
183 val dts' = map (fn (tvrs, tname, _, constrs) => (mk_type thy tname tvrs, constrs)) dts |
184 val dts' = map (fn (tvrs, tname, _, constrs) => (mk_type thy tname tvrs, constrs)) dts |
184 in |
185 in |
185 flat (map (fn (ty, constrs) => map (fn (bn, tys, mx) => (bn, tys ---> ty, mx)) constrs) dts') |
186 flat (map (fn (ty, constrs) => map (fn (bn, tys, mx) => (bn, tys ---> ty, mx)) constrs) dts') |
186 end |
187 end |
187 *} |
188 *} |
188 |
189 |
189 ML {* |
190 ML {* |
190 fun nominal_datatype2_cmd (dt_strs, (bn_fun_strs, bn_eq_strs)) lthy = |
191 fun nominal_datatype2_cmd (dt_strs, bn_fun_strs, bn_eq_strs) lthy = |
191 let |
192 let |
192 val thy = ProofContext.theory_of lthy |
193 val thy = ProofContext.theory_of lthy |
193 |
194 |
194 fun prep_typ ((tvs, tname, mx), _) = (tname, length tvs, mx); |
195 fun prep_typ (tvs, tname, mx, _) = (tname, length tvs, mx); |
195 |
196 |
196 (* adding the types for parsing datatypes *) |
197 (* adding the types for parsing datatypes *) |
197 val lthy_tmp = lthy |
198 val lthy_tmp = lthy |
198 |> Local_Theory.theory (Sign.add_types (map prep_typ dt_strs)) |
199 |> Local_Theory.theory (Sign.add_types (map prep_typ dt_strs)) |
199 |
200 |
200 fun prep_cnstr lthy (((cname, atys), mx), binders) = |
201 fun prep_cnstr lthy (((cname, atys), mx), binders) = |
201 (cname, map (Syntax.read_typ lthy o snd) atys, mx) |
202 (cname, map (Syntax.read_typ lthy o snd) atys, mx) |
202 |
203 |
203 fun prep_dt lthy ((tvs, tname, mx), cnstrs) = |
204 fun prep_dt lthy (tvs, tname, mx, cnstrs) = |
204 (tvs, tname, mx, map (prep_cnstr lthy) cnstrs) |
205 (tvs, tname, mx, map (prep_cnstr lthy) cnstrs) |
205 |
206 |
206 (* parsing the datatypes *) |
207 (* parsing the datatypes *) |
207 val dts_prep = map (prep_dt lthy_tmp) dt_strs |
208 val dts_prep = map (prep_dt lthy_tmp) dt_strs |
208 |
209 |