Nominal/NewParser.thy
changeset 2337 b151399bd2c3
parent 2336 f2d545b77b31
child 2338 e1764a73c292
--- 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);