diff -r f2d545b77b31 -r b151399bd2c3 Nominal/NewParser.thy --- 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);