# HG changeset patch
# User huffman
# Date 1258678225 28800
# Node ID e8535acd302cfcf35e94a317cb4bc311a48cbece
# Parent  d625c373b1605b14eaab1298a53f54b3b3322615
copy_of_dtyp uses map table from theory data

diff -r d625c373b160 -r e8535acd302c src/HOLCF/Tools/Domain/domain_axioms.ML
--- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Thu Nov 19 16:48:40 2009 -0800
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Thu Nov 19 16:50:25 2009 -0800
@@ -6,10 +6,11 @@
 
 signature DOMAIN_AXIOMS =
 sig
-  val copy_of_dtyp : (int -> term) -> Datatype.dtyp -> term
+  val copy_of_dtyp :
+      string Symtab.table -> (int -> term) -> Datatype.dtyp -> term
 
   val calc_axioms :
-      bool ->
+      bool -> string Symtab.table ->
       string -> Domain_Library.eq list -> int -> Domain_Library.eq ->
       string * (string * term) list * (string * term) list
 
@@ -36,16 +37,18 @@
                  (@{type_name "*"}, @{const_name "cprod_map"}),
                  (@{type_name "u"}, @{const_name "u_map"})];
 
-fun copy_of_dtyp r dt = if DatatypeAux.is_rec_type dt then copy r dt else ID
-and copy r (DatatypeAux.DtRec i) = r i
-  | copy r (DatatypeAux.DtTFree a) = ID
-  | copy r (DatatypeAux.DtType (c, ds)) =
-    case Symtab.lookup copy_tab c of
-      SOME f => list_ccomb (%%:f, map (copy_of_dtyp r) ds)
+fun copy_of_dtyp tab r dt =
+    if DatatypeAux.is_rec_type dt then copy tab r dt else ID
+and copy tab r (DatatypeAux.DtRec i) = r i
+  | copy tab r (DatatypeAux.DtTFree a) = ID
+  | copy tab r (DatatypeAux.DtType (c, ds)) =
+    case Symtab.lookup tab c of
+      SOME f => list_ccomb (%%:f, map (copy_of_dtyp tab r) ds)
     | NONE => (warning ("copy_of_dtyp: unknown type constructor " ^ c); ID);
 
 fun calc_axioms
     (definitional : bool)
+    (map_tab : string Symtab.table)
     (comp_dname : string)
     (eqs : eq list)
     (n : int)
@@ -65,13 +68,15 @@
     val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name'));
 
     val when_def = ("when_def",%%:(dname^"_when") == 
-                              List.foldr (uncurry /\ ) (/\x_name'((when_body cons (fn (x,y) =>
-                                                                                      Bound(1+length cons+x-y)))`(dc_rep`Bound 0))) (when_funs cons));
-          
+        List.foldr (uncurry /\ ) (/\x_name'((when_body cons (fn (x,y) =>
+          Bound(1+length cons+x-y)))`(dc_rep`Bound 0))) (when_funs cons));
+
     val copy_def =
-        let fun r i = proj (Bound 0) eqs i;
-        in ("copy_def", %%:(dname^"_copy") ==
-                        /\ "f" (dc_abs oo (copy_of_dtyp r (dtyp_of_eq eqn)) oo dc_rep)) end;
+      let fun r i = proj (Bound 0) eqs i;
+      in
+        ("copy_def", %%:(dname^"_copy") == /\ "f"
+          (dc_abs oo (copy_of_dtyp map_tab r (dtyp_of_eq eqn)) oo dc_rep))
+      end;
 
 (* -- definitions concerning the constructors, discriminators and selectors - *)
 
@@ -231,8 +236,10 @@
           #> add_axioms_infer axs
           #> Sign.parent_path;
 
+    val map_tab = Domain_Isomorphism.get_map_tab thy';
+
     val thy = thy'
-      |> fold add_one (mapn (calc_axioms definitional comp_dname eqs) 0 eqs);
+      |> fold add_one (mapn (calc_axioms definitional map_tab comp_dname eqs) 0 eqs);
 
   in
     thy
diff -r d625c373b160 -r e8535acd302c src/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Thu Nov 19 16:48:40 2009 -0800
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Thu Nov 19 16:50:25 2009 -0800
@@ -12,6 +12,8 @@
     (string list * binding * mixfix * string) list -> theory -> theory
   val add_type_constructor:
     (string * term * string * thm  * thm) -> theory -> theory
+  val get_map_tab:
+    theory -> string Symtab.table
 end;
 
 structure Domain_Isomorphism :> DOMAIN_ISOMORPHISM =
@@ -68,6 +70,8 @@
     #> RepData.map (Thm.add_thm REP_thm)
     #> IsodeflData.map (Thm.add_thm isodefl_thm);
 
+val get_map_tab = MapData.get;
+
 
 (******************************************************************************)
 (******************************* building types *******************************)
diff -r d625c373b160 -r e8535acd302c src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Nov 19 16:48:40 2009 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Nov 19 16:50:25 2009 -0800
@@ -141,6 +141,8 @@
 
 val _ = message ("Proving isomorphism properties of domain "^dname^" ...");
 val pg = pg' thy;
+val map_tab = Domain_Isomorphism.get_map_tab thy;
+
 
 (* ----- getting the axioms and definitions --------------------------------- *)
 
@@ -599,7 +601,8 @@
       val lhs = dc_copy`%"f"`(con_app con args);
       fun one_rhs arg =
           if DatatypeAux.is_rec_type (dtyp_of arg)
-          then Domain_Axioms.copy_of_dtyp (proj (%:"f") eqs) (dtyp_of arg) ` (%# arg)
+          then Domain_Axioms.copy_of_dtyp map_tab
+                 (proj (%:"f") eqs) (dtyp_of arg) ` (%# arg)
           else (%# arg);
       val rhs = con_app2 con one_rhs args;
       val goal = lift_defined %: (nonlazy_rec args, mk_trp (lhs === rhs));
@@ -660,6 +663,7 @@
 fun comp_theorems (comp_dnam, eqs: eq list) thy =
 let
 val global_ctxt = ProofContext.init thy;
+val map_tab = Domain_Isomorphism.get_map_tab thy;
 
 val dnames = map (fst o fst) eqs;
 val conss  = map  snd        eqs;
@@ -727,7 +731,8 @@
           fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n";
           fun one_rhs arg =
               if DatatypeAux.is_rec_type (dtyp_of arg)
-              then Domain_Axioms.copy_of_dtyp mk_take (dtyp_of arg) ` (%# arg)
+              then Domain_Axioms.copy_of_dtyp map_tab
+                     mk_take (dtyp_of arg) ` (%# arg)
               else (%# arg);
           val lhs = (dc_take dn $ (%%:"Suc" $ %:"n"))`(con_app con args);
           val rhs = con_app2 con one_rhs args;