110 (ty_args, raw_bind bind, mx, map raw_dts_aux1 constrs) |
110 (ty_args, raw_bind bind, mx, map raw_dts_aux1 constrs) |
111 in |
111 in |
112 map raw_dts_aux2 dts |
112 map raw_dts_aux2 dts |
113 end |
113 end |
114 |
114 |
|
115 fun get_constrs dts = |
|
116 flat (map (fn (_, _, _, constrs) => map (fn (bn, tys, mx) => (bn, tys, mx)) constrs) dts) |
|
117 |
115 fun get_constr_strs dts = |
118 fun get_constr_strs dts = |
116 flat (map (fn (_, _, _, constrs) => map (fn (bn, _, _) => Binding.name_of bn) constrs) dts) |
119 map (fn (bn, _, _) => Binding.name_of bn) (get_constrs dts) |
|
120 |
|
121 fun get_constrs2 dts = |
|
122 flat (map (fn (tvrs, tname, _, constrs) => |
|
123 map (fn (bn, tys, mx) => (bn, tys ---> Type ("Test." ^ Binding.name_of tname, map (fn s => TVar ((s,0),[])) tvrs), mx)) constrs) dts) |
117 |
124 |
118 fun get_bn_fun_strs bn_funs = |
125 fun get_bn_fun_strs bn_funs = |
119 map (fn (bn_fun, _, _) => Binding.name_of bn_fun) bn_funs |
126 map (fn (bn_fun, _, _) => Binding.name_of bn_fun) bn_funs |
120 *} |
127 *} |
121 |
128 |
139 val bn_funs' = map (fn (bn, opt_ty, mx) => |
146 val bn_funs' = map (fn (bn, opt_ty, mx) => |
140 (raw_bind bn, Option.map (raw_typ dt_names) opt_ty, mx)) bn_funs |
147 (raw_bind bn, Option.map (raw_typ dt_names) opt_ty, mx)) bn_funs |
141 val bn_eqs' = map (fn trm => |
148 val bn_eqs' = map (fn trm => |
142 (Attrib.empty_binding, raw_term (cnstr_names @ bn_fun_strs) dt_names trm)) bn_eqs |
149 (Attrib.empty_binding, raw_term (cnstr_names @ bn_fun_strs) dt_names trm)) bn_eqs |
143 in |
150 in |
144 (*Primrec.add_primrec bn_funs' bn_eqs' lthy*) |
151 Primrec.add_primrec bn_funs' bn_eqs' lthy |
145 ((), lthy) |
|
146 end |
152 end |
147 *} |
153 *} |
148 |
154 |
149 ML {* |
155 ML {* |
150 fun nominal_datatype2 dts bn_funs bn_eqs lthy = |
156 fun nominal_datatype2 dts bn_funs bn_eqs lthy = |
156 |> raw_dts_decl dts_names dts |
162 |> raw_dts_decl dts_names dts |
157 ||>> raw_bn_fun_decl dts_names ctrs_names bn_funs bn_eqs |
163 ||>> raw_bn_fun_decl dts_names ctrs_names bn_funs bn_eqs |
158 end |
164 end |
159 *} |
165 *} |
160 |
166 |
|
167 |
161 ML {* |
168 ML {* |
162 fun nominal_datatype2_cmd (dt_strs, (bn_fun_strs, bn_eq_strs)) lthy = |
169 fun nominal_datatype2_cmd (dt_strs, (bn_fun_strs, bn_eq_strs)) lthy = |
163 let |
170 let |
164 val lthy_tmp = lthy |
171 val lthy_tmp = lthy |
165 |> (Local_Theory.theory |
172 |> Local_Theory.theory |
166 (Sign.add_types (map (fn ((tvs, tname, mx), _) => |
173 (Sign.add_types (map (fn ((tvs, tname, mx), _) => |
167 (tname, length tvs, mx)) dt_strs))) |
174 (tname, length tvs, mx)) dt_strs)) |
168 |
175 |
169 fun prep_cnstr lthy (((cname, atys), mx), binders) = |
176 fun prep_cnstr lthy (((cname, atys), mx), binders) = |
170 (cname, map (Syntax.read_typ lthy o snd) atys, mx) |
177 (cname, map (Syntax.read_typ lthy o snd) atys, mx) |
171 |
178 |
172 fun prep_dt lthy ((tvs, tname, mx), cnstrs) = |
179 fun prep_dt lthy ((tvs, tname, mx), cnstrs) = |
173 (tvs, tname, mx, map (prep_cnstr lthy) cnstrs) |
180 (tvs, tname, mx, map (prep_cnstr lthy) cnstrs) |
174 |
181 |
175 fun prep_bn_fun lthy (bn, ty_str, mx) = |
|
176 (bn, Option.map (Syntax.read_typ lthy) ty_str, mx) |
|
177 |
|
178 fun prep_bn_eq lthy (attr, trm_str) = Syntax.read_term lthy trm_str |
|
179 |
|
180 val dts_prep = map (prep_dt lthy_tmp) dt_strs |
182 val dts_prep = map (prep_dt lthy_tmp) dt_strs |
181 val bn_fun_prep = map (prep_bn_fun lthy_tmp) bn_fun_strs |
183 |
182 val bn_eq_prep = map (prep_bn_eq lthy_tmp) bn_eq_strs |
184 val lthy_tmp2 = lthy_tmp |
183 in |
185 |> Local_Theory.theory (Sign.add_consts_i (get_constrs2 dts_prep)) |
184 nominal_datatype2 dts_prep bn_fun_prep [] lthy |> snd |
186 |
|
187 fun prep_bn_fun ((bn, T), mx) = (bn, SOME T, mx) |
|
188 |
|
189 fun prep_bn_eq (attr, t) = t |
|
190 |
|
191 val (bn_fun_aux, bn_eq_aux) = fst (Specification.read_spec bn_fun_strs bn_eq_strs lthy_tmp2) |
|
192 |
|
193 val bn_fun_prep = map prep_bn_fun bn_fun_aux |
|
194 val bn_eq_prep = map prep_bn_eq bn_eq_aux |
|
195 |
|
196 val _ = tracing (cat_lines (map (Syntax.string_of_term lthy_tmp2) bn_eq_prep)) |
|
197 in |
|
198 nominal_datatype2 dts_prep bn_fun_prep bn_eq_prep lthy |> snd |
185 end |
199 end |
186 *} |
200 *} |
187 |
201 |
188 (* Command Keyword *) |
202 (* Command Keyword *) |
189 ML {* |
203 ML {* |