# HG changeset patch
# User huffman
# Date 1267335504 28800
# Node ID 561d8e98d9d353dda033a945ed8c21e2cca3c302
# Parent  9fcfd57631811b7ff1f7d38085a55656565fb261
domain_isomorphism function returns iso_info record

diff -r 9fcfd5763181 -r 561d8e98d9d3 src/HOLCF/Tools/Domain/domain_extender.ML
--- a/src/HOLCF/Tools/Domain/domain_extender.ML	Sat Feb 27 20:56:19 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Sat Feb 27 21:38:24 2010 -0800
@@ -217,7 +217,7 @@
         if null args then oneT else foldr1 mk_sprodT (map mk_arg_typ args);
     fun mk_eq_typ (_, cons) = foldr1 mk_ssumT (map mk_con_typ cons);
     
-    val thy'' = thy''' |>
+    val (iso_infos, thy'') = thy''' |>
       Domain_Isomorphism.domain_isomorphism
         (map (fn ((vs, dname, mx, _), eq) =>
                  (map fst vs, dname, mx, mk_eq_typ eq, NONE))
diff -r 9fcfd5763181 -r 561d8e98d9d3 src/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Sat Feb 27 20:56:19 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_isomorphism.ML	Sat Feb 27 21:38:24 2010 -0800
@@ -6,9 +6,18 @@
 
 signature DOMAIN_ISOMORPHISM =
 sig
+  type iso_info =
+    {
+      repT : typ,
+      absT : typ,
+      rep_const : term,
+      abs_const : term,
+      rep_inverse : thm,
+      abs_inverse : thm
+    }
   val domain_isomorphism:
     (string list * binding * mixfix * typ * (binding * binding) option) list
-      -> theory -> theory
+      -> theory -> iso_info list * theory
   val domain_isomorphism_cmd:
     (string list * binding * mixfix * string * (binding * binding) option) list
       -> theory -> theory
@@ -298,6 +307,16 @@
 (******************************************************************************)
 (* prepare datatype specifications *)
 
+type iso_info =
+  {
+    repT : typ,
+    absT : typ,
+    rep_const : term,
+    abs_const : term,
+    rep_inverse : thm,
+    abs_inverse : thm
+  }
+
 fun read_typ thy str sorts =
   let
     val ctxt = ProofContext.init thy
@@ -320,7 +339,7 @@
     (prep_typ: theory -> 'a -> (string * sort) list -> typ * (string * sort) list)
     (doms_raw: (string list * binding * mixfix * 'a * (binding * binding) option) list)
     (thy: theory)
-    : theory =
+    : iso_info list * theory =
   let
     val _ = Theory.requires thy "Representable" "domain isomorphisms";
 
@@ -467,6 +486,22 @@
       |> fold_map mk_iso_thms (dom_binds ~~ REP_eq_thms ~~ rep_abs_defs)
       |>> ListPair.unzip;
 
+    (* collect info about rep/abs *)
+    val iso_info : iso_info list =
+      let
+        fun mk_info (((lhsT, rhsT), (repC, absC)), (rep_iso, abs_iso)) =
+          {
+            repT = rhsT,
+            absT = lhsT,
+            rep_const = repC,
+            abs_const = absC,
+            rep_inverse = rep_iso,
+            abs_inverse = abs_iso
+          };
+      in
+        map mk_info (dom_eqns ~~ rep_abs_consts ~~ iso_thms)
+      end
+
     (* declare map functions *)
     fun declare_map_const (tbind, (lhsT, rhsT)) thy =
       let
@@ -683,11 +718,11 @@
       fold_map prove_reach_thm (reach_thm_projs ~~ map_ID_thms ~~ dom_eqns);
 
   in
-    thy
+    (iso_info, thy)
   end;
 
 val domain_isomorphism = gen_domain_isomorphism cert_typ;
-val domain_isomorphism_cmd = gen_domain_isomorphism read_typ;
+val domain_isomorphism_cmd = snd oo gen_domain_isomorphism read_typ;
 
 (******************************************************************************)
 (******************************** outer syntax ********************************)