3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 |
6 |
7 |
7 |
8 (* test for how to add datatypes *) |
8 (* tests *) |
|
9 ML {* |
|
10 Datatype.datatype_cmd; |
|
11 Datatype.add_datatype Datatype.default_config; |
|
12 |
|
13 Primrec.add_primrec_cmd; |
|
14 Primrec.add_primrec; |
|
15 Primrec.add_primrec_simple; |
|
16 *} |
|
17 |
|
18 section {* test for setting up a primrec on the ML-level *} |
|
19 |
|
20 datatype simple = Foo |
|
21 |
|
22 local_setup {* |
|
23 Primrec.add_primrec [(@{binding "Bar"}, SOME @{typ "simple \<Rightarrow> nat"}, NoSyn)] |
|
24 [(Attrib.empty_binding, HOLogic.mk_Trueprop @{term "Bar Foo = Suc 0"})] #> snd |
|
25 *} |
|
26 thm Bar.simps |
|
27 |
|
28 lemma "Bar Foo = XXX" |
|
29 apply(simp) |
|
30 oops |
|
31 |
|
32 section {* test for setting up a datatype on the ML-level *} |
9 setup {* |
33 setup {* |
10 Datatype.datatype_cmd |
34 Datatype.add_datatype Datatype.default_config |
11 ["foo"] |
35 ["foo"] |
12 [([], @{binding "foo"}, NoSyn, |
36 [([], @{binding "foo"}, NoSyn, |
13 [(@{binding "zero"}, [], NoSyn),(@{binding "suc"}, ["foo"], NoSyn)]) |
37 [(@{binding "zero"}, [], NoSyn),(@{binding "suc"}, [Type ("Test.foo", [])], NoSyn)]) |
14 ] |
38 ] #> snd |
|
39 *} |
|
40 |
|
41 ML {* |
|
42 PolyML.makestring (#descr (Datatype.the_info @{theory} "Test.foo")) |
15 *} |
43 *} |
16 |
44 |
17 thm foo.recs |
45 thm foo.recs |
18 thm foo.induct |
46 thm foo.induct |
19 |
47 |
20 |
48 (* adds "_raw" to the end of constants and types *) |
21 ML{* |
49 ML {* |
22 fun filtered_input str = |
50 fun raw_str [] s = s |
23 filter OuterLex.is_proper (OuterSyntax.scan Position.none str) |
51 | raw_str (s'::ss) s = (if s = s' then s ^ "_str" else raw_str ss s) |
24 |
52 |
25 fun parse p input = Scan.finite OuterLex.stopper (Scan.error p) input |
53 val raw_strs = map raw_str |
26 *} |
54 |
27 |
55 fun raw_typ ty_strs (Type (a, Ts)) = Type (raw_str ty_strs a, map (raw_typ ty_strs) Ts) |
28 (* type plus possible annotation *) |
56 | raw_typ ty_strs T = T |
|
57 |
|
58 fun raw_term trm_strs ty_strs (Const (a, T)) = Const (raw_str trm_strs a, raw_typ ty_strs T) |
|
59 | raw_term trm_strs ty_strs (Abs (a, T, t)) = Abs (a, T, raw_term trm_strs ty_strs t) |
|
60 | raw_term trm_strs ty_strs (t $ u) = (raw_term trm_strs ty_strs t) $ (raw_term trm_strs ty_strs u) |
|
61 |
|
62 fun raw_binding bn = Binding.suffix_name "_raw" bn |
|
63 *} |
|
64 |
|
65 section{* Interface for nominal_datatype *} |
|
66 |
|
67 text {* |
|
68 |
|
69 Nominal-Datatype-part: |
|
70 |
|
71 1st Arg: string list |
|
72 ^^^^^^^^^^^ |
|
73 strings of the types to be defined |
|
74 |
|
75 2nd Arg: (string list * binding * mixfix * (binding * typ list * mixfix) list) list |
|
76 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ |
|
77 type(s) to be defined constructors list |
|
78 (ty args, name, syn) (name, typs, syn) |
|
79 |
|
80 Binder-Function-part: |
|
81 |
|
82 3rd Arg: (binding * typ option * mixfix) list |
|
83 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ |
|
84 binding function(s) |
|
85 to be defined |
|
86 (name, type, syn) |
|
87 |
|
88 4th Arg: (attrib * term) list |
|
89 ^^^^^^^^^^^^^^^^^^^ |
|
90 the equations of the binding functions |
|
91 (Trueprop equations) |
|
92 |
|
93 *} |
|
94 |
|
95 ML {* Datatype.add_datatype *} |
|
96 |
|
97 ML {* |
|
98 fun raw_definitions dt_names dts bn_funs bn_eqs lthy = |
|
99 let |
|
100 val conf = Datatype.default_config |
|
101 val bn_funs' = map (fn (bn, ty) => (raw_binding bn, ty, NoSyn)) bn_funs |
|
102 val bn_eqs' = map (pair Attrib.empty_binding) bn_eqs |
|
103 in |
|
104 lthy |
|
105 |> (Local_Theory.theory_result (Datatype.add_datatype conf dt_names dts)) |
|
106 ||>> Primrec.add_primrec bn_funs' bn_eqs' |
|
107 end |
|
108 *} |
|
109 |
|
110 ML {* @{binding "zero"} *} |
|
111 |
|
112 local_setup {* |
|
113 raw_definitions |
|
114 ["foo'"] |
|
115 [([], @{binding "foo'"}, NoSyn, |
|
116 [(@{binding "zero'"}, [], NoSyn),(@{binding "suc'"}, [Type ("Test.foo'", [])], NoSyn)])] |
|
117 [(@{binding "Bar'"}, SOME @{typ "simple \<Rightarrow> nat"})] |
|
118 [HOLogic.mk_Trueprop @{term "Bar'_raw Foo = Suc 0"}] |
|
119 #> snd |
|
120 *} |
|
121 |
|
122 typ foo' |
|
123 thm Bar'.simps |
|
124 |
|
125 text {*****************************************************} |
29 ML {* |
126 ML {* |
30 val anno_typ = |
127 (* nominal datatype parser *) |
31 (Scan.option (OuterParse.name --| OuterParse.$$$ "::")) -- OuterParse.typ |
128 local |
32 *} |
129 structure P = OuterParse |
33 |
130 in |
34 ML {* |
131 |
35 parse (Scan.repeat anno_typ) (filtered_input "x::string bool") |
132 val _ = OuterKeyword.keyword "bind" |
36 *} |
133 val anno_typ = Scan.option (P.name --| P.$$$ "::") -- P.typ |
37 |
|
38 ML {* OuterParse.enum "," ; OuterParse.and_list1 *} |
|
39 |
134 |
40 (* binding specification *) |
135 (* binding specification *) |
41 ML {* |
|
42 datatype bind = B of string * string | BS of string * string |
|
43 |
|
44 val _ = OuterKeyword.keyword "bind" |
|
45 val _ = OuterKeyword.keyword "bindset" |
|
46 |
|
47 val bind_parse_aux = |
|
48 (OuterParse.$$$ "bind" >> (K B)) |
|
49 || (OuterParse.$$$ "bindset" >> (K BS)) |
|
50 |
|
51 (* should use and_list *) |
136 (* should use and_list *) |
52 val bind_parser = |
137 val bind_parser = |
53 OuterParse.enum "," |
138 P.enum "," ((P.$$$ "bind" |-- P.term) -- (P.$$$ "in" |-- P.name)) |
54 ((bind_parse_aux -- OuterParse.term) -- |
|
55 (OuterParse.$$$ "in" |-- OuterParse.name) >> (fn ((bind, s1), s2) => bind (s1,s2))) |
|
56 *} |
|
57 |
139 |
58 (* datatype parser *) |
140 (* datatype parser *) |
59 ML {* |
|
60 val dt_parser = |
141 val dt_parser = |
61 OuterParse.type_args -- OuterParse.binding -- OuterParse.opt_infix -- |
142 P.type_args -- P.binding -- P.opt_infix -- |
62 (OuterParse.$$$ "=" |-- OuterParse.enum1 "|" |
143 (P.$$$ "=" |-- P.enum1 "|" (P.binding -- (Scan.repeat anno_typ) -- bind_parser -- P.opt_mixfix)) |
63 (OuterParse.binding -- (Scan.repeat anno_typ) -- bind_parser -- OuterParse.opt_mixfix)) |
|
64 *} |
|
65 |
144 |
66 (* function equation parser *) |
145 (* function equation parser *) |
67 ML {* |
|
68 val fun_parser = |
146 val fun_parser = |
69 Scan.optional |
147 Scan.optional (P.$$$ "binder" |-- P.fixes -- SpecParse.where_alt_specs) ([],[]) |
70 ((OuterParse.$$$ "binder") |-- OuterParse.fixes -- SpecParse.where_alt_specs) ([],[]) |
|
71 *} |
|
72 |
148 |
73 (* main parser *) |
149 (* main parser *) |
74 ML {* |
|
75 val parser = |
150 val parser = |
76 OuterParse.and_list1 dt_parser -- fun_parser |
151 P.and_list1 dt_parser -- fun_parser |
77 *} |
152 |
|
153 end |
|
154 *} |
|
155 |
78 |
156 |
79 (* printing stuff *) |
157 (* printing stuff *) |
80 ML {* |
158 ML {* |
81 fun print_str_option NONE = "NONE" |
159 fun print_str_option NONE = "NONE" |
82 | print_str_option (SOME s) = (s:bstring) |
160 | print_str_option (SOME s) = (s:bstring) |
83 *} |
161 |
84 |
|
85 ML {* |
|
86 fun print_anno_typ lthy (NONE, ty) = Syntax.string_of_typ lthy ty |
162 fun print_anno_typ lthy (NONE, ty) = Syntax.string_of_typ lthy ty |
87 | print_anno_typ lthy (SOME x, ty) = x ^ ":" ^ Syntax.string_of_typ lthy ty |
163 | print_anno_typ lthy (SOME x, ty) = x ^ ":" ^ Syntax.string_of_typ lthy ty |
88 *} |
164 |
89 |
165 fun print_bind (s1, s2) = "bind " ^ s1 ^ " in " ^ s2 |
90 ML {* |
166 |
91 fun print_bind (B (s1, s2)) = "bind " ^ s1 ^ " in " ^ s2 |
|
92 | print_bind (BS (s1, s2)) = "bindset " ^ s1 ^ " in " ^ s2 |
|
93 *} |
|
94 |
|
95 ML {* |
|
96 fun print_constr lthy (((name, anno_tys), bds), syn) = |
167 fun print_constr lthy (((name, anno_tys), bds), syn) = |
97 (Binding.name_of name ^ " of " ^ (commas (map (print_anno_typ lthy) anno_tys)) ^ " " |
168 (Binding.name_of name ^ " of " ^ (commas (map (print_anno_typ lthy) anno_tys)) ^ " " |
98 ^ (commas (map print_bind bds)) ^ " " |
169 ^ (commas (map print_bind bds)) ^ " " |
99 ^ (Pretty.str_of (Syntax.pretty_mixfix syn))) |
170 ^ (Pretty.str_of (Syntax.pretty_mixfix syn))) |
100 *} |
171 |
101 |
172 fun print_single_dt lthy (((s2, s3), syn), constrs) = |
102 (* TODO: replace with the proper thing *) |
|
103 ML {* |
|
104 fun is_atom ty = ty = "Test.name" |
|
105 *} |
|
106 |
|
107 ML {* |
|
108 fun fv_bds s bds set = |
|
109 case bds of |
|
110 [] => set |
|
111 | B (s1, s2) :: tl => |
|
112 if s2 = s then |
|
113 fv_bds s tl (HOLogic.mk_binop @{const_name "Algebras.minus_class.minus"} (set, HOLogic.mk_set @{typ name} [Free (s1, @{typ name})])) |
|
114 else fv_bds s tl set |
|
115 | BS (s1, s2) :: tl => |
|
116 (* TODO: This is just a copy *) |
|
117 if s2 = s then |
|
118 fv_bds s tl (HOLogic.mk_binop @{const_name "Algebras.minus_class.minus"} (set, HOLogic.mk_set @{typ name} [Free (s1, @{typ name})])) |
|
119 else fv_bds s tl set |
|
120 *} |
|
121 |
|
122 (* TODO: After variant_frees, check that the new names correspond to the ones given by user |
|
123 so that 'bind' is matched with variables correctly *) |
|
124 ML {* |
|
125 fun fv_constr lthy prefix dt_names (((name, anno_tys), bds), syn) = |
|
126 let |
|
127 fun prepare_name (NONE, ty) = ("", ty) |
|
128 | prepare_name (SOME n, ty) = (n, ty); |
|
129 val vars = map Free (Variable.variant_frees lthy [] (map prepare_name anno_tys)); |
|
130 val var_strs = map (Syntax.string_of_term lthy) vars; |
|
131 fun fv_var (t as Free (s, (ty as Type (tyS, _)))) = |
|
132 if is_atom tyS then HOLogic.mk_set ty [t] else |
|
133 if (Long_Name.base_name tyS) mem dt_names then |
|
134 fv_bds s bds (Free ("rfv_" ^ (Long_Name.base_name tyS), Type ("fun", [dummyT, @{typ "name set"}])) $ t) else |
|
135 HOLogic.mk_set @{typ name} [] |
|
136 val fv_eq = |
|
137 if null vars then HOLogic.mk_set @{typ name} [] |
|
138 else foldr1 (HOLogic.mk_binop @{const_name union}) (map fv_var vars) |
|
139 val fv_eq_str = Syntax.string_of_term lthy (Syntax.check_term lthy fv_eq) |
|
140 in |
|
141 prefix ^ " (" ^ (Binding.name_of name) ^ " " ^ (implode (separate " " var_strs)) ^ ") = " ^ fv_eq_str |
|
142 end |
|
143 *} |
|
144 |
|
145 ML {* |
|
146 fun single_dt lthy (((s2, s3), syn), constrs) = |
|
147 ["constructor declaration"] |
173 ["constructor declaration"] |
148 @ ["type arguments: "] @ s2 |
174 @ ["type arguments: "] @ s2 |
149 @ ["datatype name: ", Binding.name_of s3] |
175 @ ["datatype name: ", Binding.name_of s3] |
150 @ ["typ mixfix: ", Pretty.string_of (Syntax.pretty_mixfix syn)] |
176 @ ["typ mixfix: ", Pretty.string_of (Syntax.pretty_mixfix syn)] |
151 @ ["constructors: "] @ (map (print_constr lthy) constrs) |
177 @ ["constructors: "] @ (map (print_constr lthy) constrs) |
152 |> separate "\n" |
178 |> separate "\n" |
153 |> implode |
179 |> implode |
154 *} |
180 |
155 |
181 fun print_single_fun_eq lthy (at, s) = |
156 ML {* |
|
157 fun fv_dt lthy dt_names (((s2, s3), syn), constrs) = |
|
158 map (fv_constr lthy ("rfv_" ^ Binding.name_of s3) dt_names) constrs |
|
159 |> separate "\n" |
|
160 |> implode |
|
161 *} |
|
162 |
|
163 ML {* fun single_fun_eq lthy (at, s) = |
|
164 ["function equations: ", (Syntax.string_of_term lthy s)] |
182 ["function equations: ", (Syntax.string_of_term lthy s)] |
165 |> separate "\n" |
183 |> separate "\n" |
166 |> implode |
184 |> implode |
167 *} |
185 |
168 |
186 fun print_single_fun_fix lthy (b, _, _) = |
169 ML {* fun single_fun_fix (b, _, _) = |
|
170 ["functions: ", Binding.name_of b] |
187 ["functions: ", Binding.name_of b] |
171 |> separate "\n" |
188 |> separate "\n" |
172 |> implode |
189 |> implode |
173 *} |
190 |
174 |
|
175 ML {* |
|
176 fun dt_name (((s2, s3), syn), constrs) = Binding.name_of s3 |
191 fun dt_name (((s2, s3), syn), constrs) = Binding.name_of s3 |
177 *} |
192 |
178 |
|
179 ML {* |
|
180 fun print_dts (dts, (funs, feqs)) lthy = |
193 fun print_dts (dts, (funs, feqs)) lthy = |
181 let |
194 let |
182 val _ = warning (implode (separate "\n" (map (single_dt lthy) dts))); |
195 val _ = warning (implode (separate "\n" (map (print_single_dt lthy) dts))); |
183 val _ = warning (implode (separate "\n" (map single_fun_fix funs))); |
196 val _ = warning (implode (separate "\n" (map (print_single_fun_fix lthy) funs))); |
184 val _ = warning (implode (separate "\n" (map (single_fun_eq lthy) feqs))); |
197 val _ = warning (implode (separate "\n" (map (print_single_fun_eq lthy) feqs))); |
185 in |
198 in |
186 () |
199 () |
187 end |
200 end |
188 *} |
|
189 |
|
190 ML {* |
|
191 fun fv_dts (dts, (funs, feqs)) lthy = |
|
192 let |
|
193 val _ = warning (implode (separate "\n" (map (fv_dt lthy (map dt_name dts)) dts))); |
|
194 in |
|
195 lthy |
|
196 end |
|
197 *} |
|
198 |
|
199 ML {* |
|
200 parser; |
|
201 Datatype.datatype_cmd; |
|
202 *} |
201 *} |
203 |
202 |
204 ML {* |
203 ML {* |
205 fun transp_ty_arg (anno, ty) = ty |
204 fun transp_ty_arg (anno, ty) = ty |
206 |
205 |
223 |
222 |
224 ML {* |
223 ML {* |
225 fun fn_defn [] [] lthy = lthy |
224 fun fn_defn [] [] lthy = lthy |
226 | fn_defn funs feqs lthy = |
225 | fn_defn funs feqs lthy = |
227 Function_Fun.add_fun Function_Common.default_config funs feqs false lthy |
226 Function_Fun.add_fun Function_Common.default_config funs feqs false lthy |
228 *} |
227 |
229 |
|
230 ML {* |
|
231 fun fn_defn_cmd [] [] lthy = lthy |
228 fun fn_defn_cmd [] [] lthy = lthy |
232 | fn_defn_cmd funs feqs lthy = |
229 | fn_defn_cmd funs feqs lthy = |
233 Function_Fun.add_fun_cmd Function_Common.default_config funs feqs false lthy |
230 Function_Fun.add_fun_cmd Function_Common.default_config funs feqs false lthy |
234 *} |
231 *} |
235 |
232 |
236 ML {* |
233 ML {* |
237 fun nominal_datatype2_cmd (dts, (funs, feqs)) thy = |
234 fun parse_fun lthy (b, NONE, m) = (b, NONE, m) |
238 let |
235 | parse_fun lthy (b, SOME ty, m) = (b, SOME (Syntax.read_typ lthy ty), m) |
239 val thy' = dt_defn (map transp_dt dts) thy |
236 |
|
237 fun parse_feq lthy (b, t) = (b, Syntax.read_prop lthy t); |
|
238 |
|
239 fun parse_anno_ty lthy (anno, ty) = (anno, Syntax.read_typ lthy ty); |
|
240 |
|
241 fun parse_constr lthy (((constr_name, ty_args), bind), mx) = |
|
242 (((constr_name, map (parse_anno_ty lthy) ty_args), bind), mx); |
|
243 |
|
244 fun parse_dt lthy (((ty_args, ty_name), mx), constrs) = |
|
245 (((ty_args, ty_name), mx), map (parse_constr lthy) constrs); |
|
246 *} |
|
247 |
|
248 ML {* |
|
249 fun nominal_datatype2_cmd (dt_strs, (fun_strs, feq_strs)) thy = |
|
250 let |
|
251 val thy' = dt_defn (map transp_dt dt_strs) thy |
240 val lthy = Theory_Target.init NONE thy' |
252 val lthy = Theory_Target.init NONE thy' |
241 val lthy' = fn_defn_cmd funs feqs lthy |
253 val lthy' = fn_defn_cmd fun_strs feq_strs lthy |
242 fun parse_fun (b, NONE, m) = (b, NONE, m) |
254 val funs = map (parse_fun lthy') fun_strs |
243 | parse_fun (b, SOME ty, m) = (b, SOME (Syntax.read_typ lthy' ty), m); |
255 val feqs = map (parse_feq lthy') feq_strs |
244 val funs = map parse_fun funs |
256 val dts = map (parse_dt lthy') dt_strs |
245 fun parse_feq (b, t) = (b, Syntax.read_prop lthy' t); |
257 val _ = print_dts (dts, (funs, feqs)) lthy' |
246 val feqs = map parse_feq feqs |
258 in |
247 fun parse_anno_ty (anno, ty) = (anno, Syntax.read_typ lthy' ty); |
259 Local_Theory.exit_global lthy' |
248 fun parse_constr (((constr_name, ty_args), bind), mx) = |
|
249 (((constr_name, map parse_anno_ty ty_args), bind), mx); |
|
250 fun parse_dt (((ty_args, ty_name), mx), constrs) = |
|
251 (((ty_args, ty_name), mx), map parse_constr constrs); |
|
252 val dts = map parse_dt dts |
|
253 val _ = print_dts (dts, (funs, feqs)) lthy |
|
254 in |
|
255 fv_dts (dts, (funs, feqs)) lthy |
|
256 |> Local_Theory.exit_global |
|
257 end |
260 end |
258 *} |
261 *} |
259 |
262 |
260 (* Command Keyword *) |
263 (* Command Keyword *) |
261 ML {* |
264 ML {* |