# HG changeset patch
# User huffman
# Date 1268556718 28800
# Node ID cdaf99fddd174ae34548afc749ebfe43bf0999a5
# Parent  a86ed293b00505d3a0c6a3532ba72d813980c0a6
move functions into holcf_library.ML

diff -r a86ed293b005 -r cdaf99fddd17 src/HOLCF/Tools/Domain/domain_constructors.ML
--- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Sun Mar 14 00:40:04 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Sun Mar 14 00:51:58 2010 -0800
@@ -376,31 +376,6 @@
     : ((typ -> term) * thm list) * theory =
   let
 
-    (* TODO: move these to holcf_library.ML *)
-    fun one_when_const T = Const (@{const_name one_when}, T ->> oneT ->> T);
-    fun mk_one_when t = one_when_const (fastype_of t) ` t;
-    fun mk_sscase (t, u) =
-      let
-        val (T, V) = dest_cfunT (fastype_of t);
-        val (U, V) = dest_cfunT (fastype_of u);
-      in sscase_const (T, U, V) ` t ` u end;
-    fun strictify_const T = Const (@{const_name strictify}, T ->> T);
-    fun mk_strictify t = strictify_const (fastype_of t) ` t;
-    fun mk_sscases [t] = mk_strictify t
-      | mk_sscases ts = foldr1 mk_sscase ts;
-    fun ssplit_const (T, U, V) =
-      Const (@{const_name ssplit}, (T ->> U ->> V) ->> mk_sprodT (T, U) ->> V);
-    fun mk_fup t =
-      let val (T, U) = dest_cfunT (fastype_of t);
-      in fup_const (T, U) ` t end;
-    fun mk_ssplit t =
-      let val (T, (U, V)) = apsnd dest_cfunT (dest_cfunT (fastype_of t));
-      in ssplit_const (T, U, V) ` t end;
-    fun lambda_stuple []      t = mk_one_when t
-      | lambda_stuple [x]     t = mk_strictify (big_lambda x t)
-      | lambda_stuple [x,y]   t = mk_ssplit (big_lambdas [x, y] t)
-      | lambda_stuple (x::xs) t = mk_ssplit (big_lambda x (lambda_stuple xs t));
-
     (* prove rep/abs rules *)
     val rep_strict = iso_locale RS @{thm iso.rep_strict};
     val abs_inverse = iso_locale RS @{thm iso.abs_iso};
@@ -429,6 +404,8 @@
         in
           lambda_args (map fst args ~~ vs) (list_ccomb (f, vs))
         end;
+      fun mk_sscases [t] = mk_strictify t
+        | mk_sscases ts = foldr1 mk_sscase ts;
       val body = mk_sscases (map2 one_con fs spec);
       val rhs = big_lambdas fs (mk_cfcomp (body, rep_const));
       val ((case_consts, case_defs), thy) =
diff -r a86ed293b005 -r cdaf99fddd17 src/HOLCF/Tools/holcf_library.ML
--- a/src/HOLCF/Tools/holcf_library.ML	Sun Mar 14 00:40:04 2010 -0800
+++ b/src/HOLCF/Tools/holcf_library.ML	Sun Mar 14 00:51:58 2010 -0800
@@ -119,6 +119,9 @@
     else raise TYPE ("mk_cfcomp", [U, U'], [f, g])
   end;
 
+fun strictify_const T = Const (@{const_name strictify}, T ->> T);
+fun mk_strictify t = strictify_const (fastype_of t) ` t;
+
 fun mk_strict t =
   let val (T, U) = dest_cfunT (fastype_of t);
   in mk_eq (t ` mk_bottom T, mk_bottom U) end;
@@ -158,13 +161,21 @@
 fun fup_const (T, U) =
   Const(@{const_name fup}, (T ->> U) ->> mk_upT T ->> U);
 
+fun mk_fup t = fup_const (dest_cfunT (fastype_of t)) ` t;
+
 fun from_up T = fup_const (T, T) ` mk_ID T;
 
 
-(*** Strict product type ***)
+(*** Lifted unit type ***)
 
 val oneT = @{typ "one"};
 
+fun one_when_const T = Const (@{const_name one_when}, T ->> oneT ->> T);
+fun mk_one_when t = one_when_const (fastype_of t) ` t;
+
+
+(*** Strict product type ***)
+
 fun mk_sprodT (T, U) = Type(@{type_name sprod}, [T, U]);
 
 fun dest_sprodT (Type(@{type_name sprod}, [T, U])) = (T, U)
@@ -188,6 +199,13 @@
 fun ssnd_const (T, U) =
   Const(@{const_name ssnd}, mk_sprodT (T, U) ->> U);
 
+fun ssplit_const (T, U, V) =
+  Const (@{const_name ssplit}, (T ->> U ->> V) ->> mk_sprodT (T, U) ->> V);
+
+fun mk_ssplit t =
+  let val (T, (U, V)) = apsnd dest_cfunT (dest_cfunT (fastype_of t));
+  in ssplit_const (T, U, V) ` t end;
+
 
 (*** Strict sum type ***)
 
@@ -221,6 +239,11 @@
   Const(@{const_name sscase},
     (T ->> V) ->> (U ->> V) ->> mk_ssumT (T, U) ->> V);
 
+fun mk_sscase (t, u) =
+  let val (T, V) = dest_cfunT (fastype_of t);
+      val (U, V) = dest_cfunT (fastype_of u);
+  in sscase_const (T, U, V) ` t ` u end;
+
 fun from_sinl (T, U) =
   sscase_const (T, U, T) ` mk_ID T ` mk_bottom (U ->> T);