62 map (fn (bn, _, _) => Binding.name_of bn) (flat (get_cnstrs dts)) |
62 map (fn (bn, _, _) => Binding.name_of bn) (flat (get_cnstrs dts)) |
63 |
63 |
64 fun get_bn_fun_strs bn_funs = |
64 fun get_bn_fun_strs bn_funs = |
65 map (fn (bn_fun, _, _) => Binding.name_of bn_fun) bn_funs |
65 map (fn (bn_fun, _, _) => Binding.name_of bn_fun) bn_funs |
66 *} |
66 *} |
|
67 |
67 |
68 |
68 ML {* |
69 ML {* |
69 fun add_primrec_wrapper funs eqs lthy = |
70 fun add_primrec_wrapper funs eqs lthy = |
70 if null funs then (([], []), lthy) |
71 if null funs then (([], []), lthy) |
71 else |
72 else |
72 let |
73 let |
73 val eqs' = map (fn (_, eq) => (Attrib.empty_binding, eq)) eqs |
74 val eqs' = map (fn (_, eq) => (Attrib.empty_binding, eq)) eqs |
74 val funs' = map (fn (bn, ty, mx) => (bn, SOME ty, mx)) funs |
75 val funs' = map (fn (bn, ty, mx) => (bn, SOME ty, mx)) funs |
|
76 val ((funs'', eqs''), lthy') = Primrec.add_primrec funs' eqs' lthy |
|
77 val phi = ProofContext.export_morphism lthy' lthy |
75 in |
78 in |
76 Primrec.add_primrec funs' eqs' lthy |
79 ((map (Morphism.term phi) funs'', map (Morphism.thm phi) eqs''), lthy') |
77 end |
80 end |
78 *} |
81 *} |
79 |
82 |
80 ML {* |
83 ML {* |
81 fun add_datatype_wrapper dt_names dts = |
84 fun add_datatype_wrapper dt_names dts = |
359 |
361 |
360 ML {* |
362 ML {* |
361 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy = |
363 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy = |
362 let |
364 let |
363 (* definition of the raw datatype and raw bn-functions *) |
365 (* definition of the raw datatype and raw bn-functions *) |
364 val ((((raw_dt_names, (raw_bn_funs_loc, raw_bn_eqs_loc)), raw_bclauses), raw_bns), lthy1) = |
366 val ((((raw_dt_names, (raw_bn_funs, raw_bn_eqs)), raw_bclauses), raw_bns), lthy1) = |
365 if STEPS > 1 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy |
367 if STEPS > 1 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy |
366 else raise TEST lthy |
368 else raise TEST lthy |
|
369 |
|
370 val _ = tracing ("raw_bn_eqs\n" ^ cat_lines (map (@{make_string} o prop_of) raw_bn_eqs)) |
|
371 |
|
372 val _ = tracing ("raw_bns\n" ^ @{make_string} raw_bns) |
|
373 val _ = tracing ("raw_bclauses\n" ^ @{make_string} raw_bclauses) |
367 |
374 |
368 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names); |
375 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names); |
369 val {descr, sorts, ...} = dtinfo; |
376 val {descr, sorts, ...} = dtinfo; |
370 val raw_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr; |
377 val raw_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr; |
371 val all_typs = map (fn i => Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i)) (map fst descr) |
378 val all_typs = map (fn i => Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i)) (map fst descr) |
372 val all_full_tnames = map (fn (_, (n, _, _)) => n) descr; |
379 val all_full_tnames = map (fn (_, (n, _, _)) => n) descr; |
373 |
380 |
374 val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy1)) all_full_tnames; |
381 val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy1)) all_full_tnames; |
375 |
382 |
376 (* what is the difference between raw_dt_names and all_full_tnames ? *) |
|
377 (* what is the purpose of dtinfo and dtinfos ? *) |
|
378 val _ = tracing ("raw_dt_names " ^ commas raw_dt_names) |
|
379 val _ = tracing ("all_full_tnames " ^ commas all_full_tnames) |
|
380 |
|
381 val inject_thms = flat (map #inject dtinfos); |
383 val inject_thms = flat (map #inject dtinfos); |
382 val distinct_thms = flat (map #distinct dtinfos); |
384 val distinct_thms = flat (map #distinct dtinfos); |
383 val rel_dtinfos = List.take (dtinfos, (length dts)); |
385 val rel_dtinfos = List.take (dtinfos, (length dts)); |
384 val rel_distinct = map #distinct rel_dtinfos; (* thm list list *) |
386 val rel_distinct = map #distinct rel_dtinfos; (* thm list list *) |
385 val induct_thm = #induct dtinfo; |
387 val induct_thm = #induct dtinfo; |
388 (* definitions of raw permutations *) |
390 (* definitions of raw permutations *) |
389 val ((raw_perm_def, raw_perm_simps, perms), lthy2) = |
391 val ((raw_perm_def, raw_perm_simps, perms), lthy2) = |
390 if STEPS > 2 then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy1 |
392 if STEPS > 2 then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy1 |
391 else raise TEST lthy1 |
393 else raise TEST lthy1 |
392 |
394 |
|
395 (* definition of raw fv_functions *) |
393 val morphism_2_0 = ProofContext.export_morphism lthy2 lthy |
396 val morphism_2_0 = ProofContext.export_morphism lthy2 lthy |
394 fun export_fun f (t, l) = (f t, map (map (apsnd (Option.map f))) l); |
397 fun export_fun f (t, l) = (f t, map (map (apsnd (Option.map f))) l); |
395 val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_0)))) raw_bns; |
398 val raw_bns_exp = map (apsnd (map (export_fun (Morphism.term morphism_2_0)))) raw_bns; |
396 val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp); |
399 val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp); |
397 val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc |
|
398 |
400 |
399 val (_, lthy2a) = Local_Theory.note ((Binding.empty, |
401 val (_, lthy2a) = Local_Theory.note ((Binding.empty, |
400 [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), raw_perm_def) lthy2; |
402 [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), raw_perm_def) lthy2; |
401 val thy = Local_Theory.exit_global lthy2a; |
403 val thy = Local_Theory.exit_global lthy2a; |
402 val thy_name = Context.theory_name thy |
404 val thy_name = Context.theory_name thy |
403 |
405 |
404 val lthy3 = Theory_Target.init NONE thy; |
406 val lthy3 = Theory_Target.init NONE thy; |
405 val raw_bn_funs = map (fn (f, _, _) => f) bn_funs_decls; |
407 val raw_bn_funs = map (fn (f, _, _) => f) bn_funs_decls; |
406 |
408 |
407 (* definition of raw fv_functions *) |
409 (* |
|
410 val _ = tracing ("raw_bns\n" ^ @{make_string} raw_bns) |
|
411 val _ = tracing ("raw_bns\n" ^ @{make_string} raw_bns_exp) |
|
412 val _ = tracing ("bn_funs\n" ^ @{make_string} bn_funs_decls) |
408 val _ = tracing ("raw_bclauses\n" ^ @{make_string} raw_bclauses) |
413 val _ = tracing ("raw_bclauses\n" ^ @{make_string} raw_bclauses) |
409 val _ = tracing ("raw_bclauses\n" ^ @{make_string} bn_funs_decls) |
414 *) |
410 val ((fv, fvbn), fv_def, lthy3a) = |
415 val ((fv, fvbn), fv_def, lthy3a) = |
411 if STEPS > 3 then define_raw_fv descr sorts bn_funs_decls raw_bclauses lthy3 |
416 if STEPS > 3 then define_raw_fv descr sorts bn_funs_decls raw_bclauses lthy3 |
412 else raise TEST lthy3 |
417 else raise TEST lthy3 |
413 |
418 |
414 |
419 |