14 Primrec.add_primrec; |
14 Primrec.add_primrec; |
15 Primrec.add_primrec_simple; |
15 Primrec.add_primrec_simple; |
16 *} |
16 *} |
17 |
17 |
18 section {* test for setting up a primrec on the ML-level *} |
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 *} |
|
33 setup {* |
|
34 Datatype.add_datatype Datatype.default_config |
|
35 ["foo"] |
|
36 [([], @{binding "foo"}, NoSyn, |
|
37 [(@{binding "zero"}, [], NoSyn),(@{binding "suc"}, [Type ("Test.foo", [])], NoSyn)]) |
|
38 ] #> snd |
|
39 *} |
|
40 |
|
41 ML {* |
|
42 PolyML.makestring (#descr (Datatype.the_info @{theory} "Test.foo")) |
|
43 *} |
|
44 |
|
45 thm foo.recs |
|
46 thm foo.induct |
|
47 |
|
48 (* adds "_raw" to the end of constants and types *) |
|
49 ML {* |
|
50 fun raw_str [] s = s |
|
51 | raw_str (s'::ss) s = (if s = s' then s ^ "_str" else raw_str ss s) |
|
52 |
|
53 val raw_strs = map raw_str |
|
54 |
|
55 fun raw_typ ty_strs (Type (a, Ts)) = Type (raw_str ty_strs a, map (raw_typ ty_strs) Ts) |
|
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 |
19 |
65 section{* Interface for nominal_datatype *} |
20 section{* Interface for nominal_datatype *} |
66 |
21 |
67 text {* |
22 text {* |
68 |
23 |
78 (ty args, name, syn) (name, typs, syn) |
33 (ty args, name, syn) (name, typs, syn) |
79 |
34 |
80 Binder-Function-part: |
35 Binder-Function-part: |
81 |
36 |
82 3rd Arg: (binding * typ option * mixfix) list |
37 3rd Arg: (binding * typ option * mixfix) list |
83 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ |
38 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ |
84 binding function(s) |
39 binding function(s) |
85 to be defined |
40 to be defined |
86 (name, type, syn) |
41 (name, type, syn) |
87 |
42 |
88 4th Arg: (attrib * term) list |
43 4th Arg: term list |
89 ^^^^^^^^^^^^^^^^^^^ |
44 ^^^^^^^^^ |
90 the equations of the binding functions |
45 the equations of the binding functions |
91 (Trueprop equations) |
46 (Trueprop equations) |
92 |
47 *} |
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 |
48 |
125 text {*****************************************************} |
49 text {*****************************************************} |
126 ML {* |
50 ML {* |
127 (* nominal datatype parser *) |
51 (* nominal datatype parser *) |
128 local |
52 local |
135 (* binding specification *) |
59 (* binding specification *) |
136 (* should use and_list *) |
60 (* should use and_list *) |
137 val bind_parser = |
61 val bind_parser = |
138 P.enum "," ((P.$$$ "bind" |-- P.term) -- (P.$$$ "in" |-- P.name)) |
62 P.enum "," ((P.$$$ "bind" |-- P.term) -- (P.$$$ "in" |-- P.name)) |
139 |
63 |
|
64 val constr_parser = |
|
65 P.binding -- Scan.repeat anno_typ |
|
66 |
140 (* datatype parser *) |
67 (* datatype parser *) |
141 val dt_parser = |
68 val dt_parser = |
142 P.type_args -- P.binding -- P.opt_infix -- |
69 ((P.type_args -- P.binding -- P.opt_infix) >> P.triple1) -- |
143 (P.$$$ "=" |-- P.enum1 "|" (P.binding -- (Scan.repeat anno_typ) -- bind_parser -- P.opt_mixfix)) |
70 (P.$$$ "=" |-- P.enum1 "|" ((constr_parser -- bind_parser -- P.opt_mixfix) >> P.triple_swap)) |
144 |
71 |
145 (* function equation parser *) |
72 (* function equation parser *) |
146 val fun_parser = |
73 val fun_parser = |
147 Scan.optional (P.$$$ "binder" |-- P.fixes -- SpecParse.where_alt_specs) ([],[]) |
74 Scan.optional (P.$$$ "binder" |-- P.fixes -- SpecParse.where_alt_specs) ([],[]) |
148 |
75 |
149 (* main parser *) |
76 (* main parser *) |
150 val parser = |
77 val main_parser = |
151 P.and_list1 dt_parser -- fun_parser |
78 P.and_list1 dt_parser -- fun_parser |
152 |
79 |
153 end |
80 end |
154 *} |
81 *} |
155 |
82 |
|
83 (* adds "_raw" to the end of constants and types *) |
|
84 ML {* |
|
85 fun add_raw s = s ^ "_raw" |
|
86 fun raw_bind bn = Binding.suffix_name "_raw" bn |
|
87 |
|
88 fun raw_str [] s = s |
|
89 | raw_str (s'::ss) s = |
|
90 if (Long_Name.base_name s) = s' |
|
91 then add_raw s |
|
92 else raw_str ss s |
|
93 |
|
94 fun raw_typ ty_strs (Type (a, Ts)) = Type (raw_str ty_strs a, map (raw_typ ty_strs) Ts) |
|
95 | raw_typ ty_strs T = T |
|
96 |
|
97 fun raw_aterm trm_strs (Const (a, T)) = Const (raw_str trm_strs a, T) |
|
98 | raw_aterm trm_strs (Free (a, T)) = Free (raw_str trm_strs a, T) |
|
99 | raw_aterm trm_strs trm = trm |
|
100 |
|
101 fun raw_term trm_strs ty_strs trm = |
|
102 trm |> Term.map_aterms (raw_aterm trm_strs) |> map_types (raw_typ ty_strs) |
|
103 |
|
104 fun raw_dts ty_strs dts = |
|
105 let |
|
106 fun raw_dts_aux1 (bind, tys, mx) = |
|
107 (raw_bind bind, map (raw_typ ty_strs) tys, mx) |
|
108 |
|
109 fun raw_dts_aux2 (ty_args, bind, mx, constrs) = |
|
110 (ty_args, raw_bind bind, mx, map raw_dts_aux1 constrs) |
|
111 in |
|
112 map raw_dts_aux2 dts |
|
113 end |
|
114 |
|
115 fun get_constr_strs dts = |
|
116 flat (map (fn (_, _, _, constrs) => map (fn (bn, _, _) => Binding.name_of bn) constrs) dts) |
|
117 |
|
118 fun get_bn_fun_strs bn_funs = |
|
119 map (fn (bn_fun, _, _) => Binding.name_of bn_fun) bn_funs |
|
120 *} |
|
121 |
|
122 ML {* |
|
123 fun nominal_dt_decl dt_names dts bn_funs bn_eqs lthy = |
|
124 let |
|
125 val conf = Datatype.default_config |
|
126 |
|
127 val dt_names' = map add_raw dt_names |
|
128 val dts' = raw_dts dt_names dts |
|
129 val constr_strs = get_constr_strs dts |
|
130 val bn_fun_strs = get_bn_fun_strs bn_funs |
|
131 |
|
132 val bn_funs' = map (fn (bn, opt_ty, mx) => |
|
133 (raw_bind bn, Option.map (raw_typ dt_names) opt_ty, mx)) bn_funs |
|
134 val bn_eqs' = map (fn trm => |
|
135 (Attrib.empty_binding, raw_term (constr_strs @ bn_fun_strs) dt_names trm)) bn_eqs |
|
136 in |
|
137 lthy |
|
138 |> (Local_Theory.theory_result (Datatype.add_datatype conf dt_names' dts')) |
|
139 ||>> Primrec.add_primrec bn_funs' bn_eqs' |
|
140 end |
|
141 *} |
|
142 |
|
143 local_setup {* |
|
144 let |
|
145 val T0 = Type ("Test.foo", []) |
|
146 val T1 = T0 --> @{typ "nat"} |
|
147 in |
|
148 nominal_dt_decl |
|
149 ["foo"] |
|
150 [([], @{binding "foo"}, NoSyn, |
|
151 [(@{binding "myzero"}, [], NoSyn),(@{binding "mysuc"}, [Type ("Test.foo", [])], NoSyn)])] |
|
152 [(@{binding "Bar"}, SOME T1, NoSyn)] |
|
153 [HOLogic.mk_Trueprop (HOLogic.mk_eq |
|
154 (Free ("Bar", T1) $ Const ("Test.foo_raw.myzero", T0), @{term "0::nat"})), |
|
155 HOLogic.mk_Trueprop (HOLogic.mk_eq |
|
156 (Free ("Bar", T1) $ (Const ("Test.foo_raw.mysuc", T0 --> T0) $ Free ("n", T0)), @{term "0::nat"}))] |
|
157 #> snd |
|
158 end |
|
159 *} |
|
160 |
|
161 typ foo_raw |
|
162 thm foo_raw.induct |
|
163 term myzero_raw |
|
164 term mysuc_raw |
|
165 thm Bar_raw.simps |
156 |
166 |
157 (* printing stuff *) |
167 (* printing stuff *) |
|
168 |
158 ML {* |
169 ML {* |
159 fun print_str_option NONE = "NONE" |
170 fun print_str_option NONE = "NONE" |
160 | print_str_option (SOME s) = (s:bstring) |
171 | print_str_option (SOME s) = (s:bstring) |
161 |
172 |
162 fun print_anno_typ lthy (NONE, ty) = Syntax.string_of_typ lthy ty |
173 fun print_anno_typ lthy (NONE, ty) = Syntax.string_of_typ lthy ty |