139 val bn_eqs' = map (fn (attr, trm) => |
139 val bn_eqs' = map (fn (attr, trm) => |
140 (attr, replace_term (cnstrs_env @ bn_fun_env) dts_env trm)) bn_eqs |
140 (attr, replace_term (cnstrs_env @ bn_fun_env) dts_env trm)) bn_eqs |
141 in |
141 in |
142 (bn_funs', bn_eqs') |
142 (bn_funs', bn_eqs') |
143 end |
143 end |
|
144 *} |
|
145 |
|
146 ML {* |
|
147 fun rawify_binds dts_env cnstrs_env bn_fun_env binds = |
|
148 map (map (map (map (fn (opt_trm, i, j) => |
|
149 (Option.map (replace_term (cnstrs_env @ bn_fun_env) dts_env) opt_trm, i, j))))) binds |
144 *} |
150 *} |
145 |
151 |
146 ML {* |
152 ML {* |
147 fun add_primrec_wrapper funs eqs lthy = |
153 fun add_primrec_wrapper funs eqs lthy = |
148 if null funs then (([], []), lthy) |
154 if null funs then (([], []), lthy) |
153 in |
159 in |
154 Primrec.add_primrec funs' eqs' lthy |
160 Primrec.add_primrec funs' eqs' lthy |
155 end |
161 end |
156 *} |
162 *} |
157 |
163 |
158 |
164 ML {* |
159 ML {* |
165 fun add_datatype_wrapper dt_names dts = |
160 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy = |
166 let |
|
167 val conf = Datatype.default_config |
|
168 in |
|
169 Local_Theory.theory_result (Datatype.add_datatype conf dt_names dts) |
|
170 end |
|
171 *} |
|
172 |
|
173 ML {* |
|
174 fun raw_nominal_decls dts bn_funs bn_eqs binds lthy = |
161 let |
175 let |
162 val thy = ProofContext.theory_of lthy |
176 val thy = ProofContext.theory_of lthy |
163 val thy_name = Context.theory_name thy |
177 val thy_name = Context.theory_name thy |
164 |
|
165 val conf = Datatype.default_config |
|
166 |
178 |
167 val dt_names = map (fn (_, s, _, _) => Binding.name_of s) dts |
179 val dt_names = map (fn (_, s, _, _) => Binding.name_of s) dts |
168 val dt_full_names = map (Long_Name.qualify thy_name) dt_names |
180 val dt_full_names = map (Long_Name.qualify thy_name) dt_names |
169 val dt_full_names' = add_raws dt_full_names |
181 val dt_full_names' = add_raws dt_full_names |
170 val dts_env = dt_full_names ~~ dt_full_names' |
182 val dts_env = dt_full_names ~~ dt_full_names' |
177 val cnstrs_env = cnstrs_full_names ~~ cnstrs_full_names' |
189 val cnstrs_env = cnstrs_full_names ~~ cnstrs_full_names' |
178 |
190 |
179 val bn_fun_strs = get_bn_fun_strs bn_funs |
191 val bn_fun_strs = get_bn_fun_strs bn_funs |
180 val bn_fun_strs' = add_raws bn_fun_strs |
192 val bn_fun_strs' = add_raws bn_fun_strs |
181 val bn_fun_env = bn_fun_strs ~~ bn_fun_strs' |
193 val bn_fun_env = bn_fun_strs ~~ bn_fun_strs' |
182 |
194 val bn_fun_full_env = map (pairself (Long_Name.qualify thy_name)) |
|
195 (bn_fun_strs ~~ bn_fun_strs') |
|
196 |
183 val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env |
197 val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env |
184 |
198 |
185 val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs |
199 val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs |
|
200 |
|
201 val raw_binds = rawify_binds dts_env cnstrs_env bn_fun_full_env binds |
186 in |
202 in |
187 lthy |
203 lthy |
188 |> Local_Theory.theory_result (Datatype.add_datatype conf raw_dt_names raw_dts) |
204 |> add_datatype_wrapper raw_dt_names raw_dts |
189 ||>> add_primrec_wrapper raw_bn_funs raw_bn_eqs |
205 ||>> add_primrec_wrapper raw_bn_funs raw_bn_eqs |
|
206 ||>> pair raw_binds |
|
207 end |
|
208 *} |
|
209 |
|
210 ML {* add_primrec_wrapper *} |
|
211 |
|
212 ML {* |
|
213 fun nominal_datatype2 dts bn_funs bn_eqs binds lthy = |
|
214 let |
|
215 val (((raw_dt_names, (raw_bn_funs, raw_bn_eqs)), raw_binds), lthy') = |
|
216 raw_nominal_decls dts bn_funs bn_eqs binds lthy |
|
217 in |
|
218 ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy') |
190 end |
219 end |
191 *} |
220 *} |
192 |
221 |
193 ML {* |
222 ML {* |
194 (* parsing the datatypes and declaring *) |
223 (* parsing the datatypes and declaring *) |
310 |> Local_Theory.theory (Sign.add_types (map prep_typ dt_strs)) |
339 |> Local_Theory.theory (Sign.add_types (map prep_typ dt_strs)) |
311 |> prepare_dts dt_strs |
340 |> prepare_dts dt_strs |
312 ||>> prepare_bn_funs bn_fun_strs bn_eq_strs |
341 ||>> prepare_bn_funs bn_fun_strs bn_eq_strs |
313 ||> prepare_binds dt_strs |
342 ||> prepare_binds dt_strs |
314 |
343 |
315 val _ = tracing (PolyML.makestring binds) |
|
316 in |
344 in |
317 nominal_datatype2 dts bn_fun bn_eq binds lthy |> snd |
345 nominal_datatype2 dts bn_fun bn_eq binds lthy |> snd |
318 end |
346 end |
319 *} |
347 *} |
320 |
348 |