--- a/Nominal/NewParser.thy Thu Jun 24 21:35:11 2010 +0100
+++ b/Nominal/NewParser.thy Sun Jun 27 21:41:21 2010 +0100
@@ -264,7 +264,7 @@
val (raw_dt_full_names, lthy1) =
add_datatype_wrapper raw_dt_names raw_dts lthy
in
- (dt_full_names', raw_dt_full_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy1)
+ (raw_dt_full_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy1)
end
*}
@@ -313,17 +313,18 @@
let
(* definition of the raw datatypes *)
val _ = warning "Definition of raw datatypes";
- val (dt_names, raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy0) =
+ val (raw_dt_names, raw_dts, raw_bclauses, raw_bn_funs, raw_bn_eqs, lthy0) =
if get_STEPS lthy > 0
then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy
else raise TEST lthy
val dtinfo = Datatype.the_info (ProofContext.theory_of lthy0) (hd raw_dt_names)
val {descr, sorts, ...} = dtinfo
- val all_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr
- val all_full_tnames = map (fn (_, (n, _, _)) => n) descr
- val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) all_full_tnames
-
+ val all_raw_tys = map (fn (_, (n, _, _)) => n) descr
+ val all_raw_constrs =
+ flat (map (map (fn (c, _, _, _) => c)) (all_dtyp_constrs_types descr sorts))
+
+ val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy0)) all_raw_tys
val inject_thms = flat (map #inject dtinfos);
val distinct_thms = flat (map #distinct dtinfos);
val constr_thms = inject_thms @ distinct_thms
@@ -352,7 +353,7 @@
val (raw_bn_funs, raw_bn_eqs, raw_bn_info, raw_bn_induct, lthy3a) =
if get_STEPS lthy3 > 2
- then raw_bn_decls dt_names raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy3
+ then raw_bn_decls all_raw_tys raw_dts raw_bn_funs raw_bn_eqs constr_thms lthy3
else raise TEST lthy3
val (raw_fvs, raw_fv_bns, raw_fv_defs, raw_fv_bns_induct, lthy3b) =
@@ -439,19 +440,22 @@
(* defining the quotient type *)
val _ = warning "Declaring the quotient types"
val qty_descr = map (fn (vs, bind, mx, _) => (vs, bind, mx)) dts
- val qty_binds = map (fn (_, bind, _, _) => bind) dts
- val qty_names = map Name.of_binding qty_binds;
- val qty_full_names = map (Long_Name.qualify thy_name) qty_names
+ val qty_binds = map (fn (_, bind, _, _) => bind) dts (* not used *)
+ val qty_names = map Name.of_binding qty_binds; (* not used *)
+ val qty_full_names = map (Long_Name.qualify thy_name) qty_names (* not used *)
- val qty_args' = map2 (fn ty => fn trm => (ty, trm, false)) alpha_tys alpha_trms
- val qty_args = (qty_descr ~~ qty_args') ~~ alpha_equivp_thms
-
val (qty_infos, lthy7) =
if get_STEPS lthy > 14
- then fold_map Quotient_Type.add_quotient_type qty_args lthy6
+ then qtype_defs qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6
else raise TEST lthy6
val qtys = map #qtyp qty_infos
+
+ val _ = tracing ("all_raw_tys: " ^ commas (map @{make_string} all_raw_tys))
+ val _ = tracing ("constrs: " ^ commas (map @{make_string} all_raw_constrs))
+ val _ = tracing ("qtys: " ^ commas (map @{make_string} qtys))
+
+
val _ =
if get_STEPS lthy > 15
@@ -465,7 +469,8 @@
map (fn (cname, dts) =>
Const (cname, map (Datatype_Aux.typ_of_dtyp descr sorts) dts --->
Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i))) l) descr);
- val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys (const_names ~~ raw_consts) lthy7;
+ val dd = map2 (fn x => fn y => (x, y, NoSyn)) const_names raw_consts
+ val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys dd lthy7;
val _ = warning "Proving respects";
val bn_nos = map (fn (_, i, _) => i) raw_bn_info;
@@ -500,17 +505,20 @@
val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst]
const_rsp_tac) raw_consts lthy11a
val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) (raw_fvs @ raw_fv_bns)
- val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ (raw_fvs @ raw_fv_bns)) lthy12;
+ val dd = map2 (fn x => fn y => (x, y, NoSyn)) qfv_names (raw_fvs @ raw_fv_bns)
+ val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys dd lthy12;
val (qfv_ts_nobn, qfv_ts_bn) = chop (length raw_perm_funs) qfv_ts;
val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs
- val (qbn_ts, qbn_defs, lthy12b) = quotient_lift_consts_export qtys (qbn_names ~~ raw_bn_funs) lthy12a;
+ val dd = map2 (fn x => fn y => (x, y, NoSyn)) qbn_names raw_bn_funs
+ val (qbn_ts, qbn_defs, lthy12b) = quotient_lift_consts_export qtys dd lthy12a;
val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_bn_trms
- val (qalpha_bn_trms, qalphabn_defs, lthy12c) =
- quotient_lift_consts_export qtys (qalpha_bn_names ~~ alpha_bn_trms) lthy12b;
+ val dd = map2 (fn x => fn y => (x, y, NoSyn)) qalpha_bn_names alpha_bn_trms
+ val (qalpha_bn_trms, qalphabn_defs, lthy12c) = quotient_lift_consts_export qtys dd lthy12b;
val _ = warning "Lifting permutations";
val thy = Local_Theory.exit_global lthy12c;
val perm_names = map (fn x => "permute_" ^ x) qty_names
- val thy' = define_lifted_perms qtys qty_full_names (perm_names ~~ raw_perm_funs) raw_perm_simps thy;
+ val dd = map2 (fn x => fn y => (x, y, NoSyn)) perm_names raw_perm_funs
+ val thy' = define_lifted_perms qtys qty_full_names dd raw_perm_simps thy;
val lthy13 = Theory_Target.init NONE thy';
val q_name = space_implode "_" qty_names;
fun suffix_bind s = Binding.qualify true q_name (Binding.name s);