# HG changeset patch
# User huffman
# Date 1267573583 28800
# Node ID f433f18d4c418657cbce77b1ea193cfff5c7f9fe
# Parent  abf45a91d24da4a6137492dd9a7959c4c10c13b0
cleaned up, added type annotations

diff -r abf45a91d24d -r f433f18d4c41 src/HOLCF/Tools/Domain/domain_extender.ML
--- a/src/HOLCF/Tools/Domain/domain_extender.ML	Tue Mar 02 15:06:02 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Tue Mar 02 15:46:23 2010 -0800
@@ -129,38 +129,49 @@
                (binding * (bool * binding option * 'a) list * mixfix) list) list)
     (thy : theory) =
   let
-    fun readS (SOME s) = Syntax.read_sort_global thy s
-      | readS NONE = Sign.defaultS thy;
-    fun readTFree (a, s) = TFree (a, readS s);
+    val dtnvs : (binding * typ list * mixfix) list =
+      let
+        fun readS (SOME s) = Syntax.read_sort_global thy s
+          | readS NONE = Sign.defaultS thy;
+        fun readTFree (a, s) = TFree (a, readS s);
+      in
+        map (fn (vs,dname:binding,mx,_) =>
+                (dname, map readTFree vs, mx)) eqs'''
+      end;
 
-    val dtnvs = map (fn (vs,dname:binding,mx,_) => 
-                        (dname, map readTFree vs, mx)) eqs''';
-    val cons''' = map (fn (_,_,_,cons) => cons) eqs''';
-    fun thy_type  (dname,tvars,mx) = (dname, length tvars, mx);
-    fun thy_arity (dname,tvars,mx) =
-        (Sign.full_name thy dname, map (snd o dest_TFree) tvars, pcpoS);
+    (* declare new types *)
     val thy =
-      thy
-      |> Sign.add_types (map thy_type dtnvs)
-      |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
-    val cons'' =
-      map (map (upd_second (map (upd_third (prep_typ thy))))) cons''';
-    val dtnvs' =
+      let
+        fun thy_type  (dname,tvars,mx) = (dname, length tvars, mx);
+        fun thy_arity (dname,tvars,mx) =
+            (Sign.full_name thy dname, map (snd o dest_TFree) tvars, pcpoS);
+      in
+        thy
+          |> Sign.add_types (map thy_type dtnvs)
+          |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs
+      end;
+
+    val cons''' :
+        (binding * (bool * binding option * 'a) list * mixfix) list list =
+        map (fn (_,_,_,cons) => cons) eqs''';
+    val cons'' :
+        (binding * (bool * binding option * typ) list * mixfix) list list =
+        map (map (upd_second (map (upd_third (prep_typ thy))))) cons''';
+    val dtnvs' : (string * typ list) list =
       map (fn (dname,vs,mx) => (Sign.full_name thy dname,vs)) dtnvs;
     val eqs' : ((string * typ list) *
         (binding * (bool * binding option * typ) list * mixfix) list) list =
-      check_and_sort_domain false dtnvs' cons'' thy;
+        check_and_sort_domain false dtnvs' cons'' thy;
     val thy = Domain_Syntax.add_syntax eqs' thy;
-    val dts  = map (Type o fst) eqs';
-    val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
-    fun strip ss = drop (find_index (fn s => s = "'") ss + 1) ss;
-    fun one_con (con,args,mx) =
+    val dts : typ list = map (Type o fst) eqs';
+    val new_dts : (string * string list) list =
+        map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
+    fun one_con (con,args,mx) : cons =
         (Binding.name_of con,  (* FIXME preverse binding (!?) *)
          mx,
          ListPair.map (fn ((lazy,sel,tp),vn) =>
            mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp), vn))
-                      (args, Datatype_Prop.make_tnames (map third args))
-        ) : cons;
+                      (args, Datatype_Prop.make_tnames (map third args)));
     val eqs : eq list =
         map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs';
     val thy = Domain_Axioms.add_axioms eqs' eqs thy;
@@ -186,13 +197,16 @@
                (binding * (bool * binding option * 'a) list * mixfix) list) list)
     (thy : theory) =
   let
-    fun readS (SOME s) = Syntax.read_sort_global thy s
-      | readS NONE = Sign.defaultS thy;
-    fun readTFree (a, s) = TFree (a, readS s);
+    val dtnvs : (binding * typ list * mixfix) list =
+      let
+        fun readS (SOME s) = Syntax.read_sort_global thy s
+          | readS NONE = Sign.defaultS thy;
+        fun readTFree (a, s) = TFree (a, readS s);
+      in
+        map (fn (vs,dname:binding,mx,_) =>
+                (dname, map readTFree vs, mx)) eqs'''
+      end;
 
-    val dtnvs = map (fn (vs,dname:binding,mx,_) => 
-                        (dname, map readTFree vs, mx)) eqs''';
-    val cons''' = map (fn (_,_,_,cons) => cons) eqs''';
     fun thy_type  (dname,tvars,mx) = (dname, length tvars, mx);
     fun thy_arity (dname,tvars,mx) =
       (Sign.full_name thy dname, map (snd o dest_TFree) tvars, @{sort rep});
@@ -203,13 +217,17 @@
       |> Sign.add_types (map thy_type dtnvs)
       |> fold (AxClass.axiomatize_arity o thy_arity) dtnvs;
 
-    val cons'' : (binding * (bool * binding option * typ) list * mixfix) list list =
-      map (map (upd_second (map (upd_third (prep_typ tmp_thy))))) cons''';
+    val cons''' :
+        (binding * (bool * binding option * 'a) list * mixfix) list list =
+        map (fn (_,_,_,cons) => cons) eqs''';
+    val cons'' :
+        (binding * (bool * binding option * typ) list * mixfix) list list =
+        map (map (upd_second (map (upd_third (prep_typ tmp_thy))))) cons''';
     val dtnvs' : (string * typ list) list =
-      map (fn (dname,vs,mx) => (Sign.full_name thy dname,vs)) dtnvs;
+        map (fn (dname,vs,mx) => (Sign.full_name thy dname,vs)) dtnvs;
     val eqs' : ((string * typ list) *
         (binding * (bool * binding option * typ) list * mixfix) list) list =
-      check_and_sort_domain true dtnvs' cons'' tmp_thy;
+        check_and_sort_domain true dtnvs' cons'' tmp_thy;
 
     fun mk_arg_typ (lazy, dest_opt, T) = if lazy then mk_uT T else T;
     fun mk_con_typ (bind, args, mx) =
@@ -222,16 +240,16 @@
                  (map fst vs, dname, mx, mk_eq_typ eq, NONE))
              (eqs''' ~~ eqs'))
 
-    val dts  = map (Type o fst) eqs';
-    val new_dts = map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
-    fun strip ss = drop (find_index (fn s => s = "'") ss + 1) ss;
-    fun one_con (con,args,mx) =
+    val dts : typ list = map (Type o fst) eqs';
+    val new_dts : (string * string list) list =
+        map (fn ((s,Ts),_) => (s, map (fst o dest_TFree) Ts)) eqs';
+    fun one_con (con,args,mx) : cons =
         (Binding.name_of con,   (* FIXME preverse binding (!?) *)
          mx,
          ListPair.map (fn ((lazy,sel,tp),vn) =>
            mk_arg ((lazy, Datatype_Aux.dtyp_of_typ new_dts tp), vn))
                       (args, Datatype_Prop.make_tnames (map third args))
-        ) : cons;
+        );
     val eqs : eq list =
         map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs';
     val ((rewss, take_rews), theorems_thy) =