src/HOLCF/Tools/Domain/domain_library.ML
changeset 35288 aa7da51ae1ef
parent 33971 9c7fa7f76950
child 35443 2e0f9516947e
--- a/src/HOLCF/Tools/Domain/domain_library.ML	Mon Feb 22 09:43:36 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_library.ML	Mon Feb 22 11:17:41 2010 -0800
@@ -132,7 +132,7 @@
 
       (* Domain specifications *)
       eqtype arg;
-  type cons = string * arg list;
+  type cons = string * mixfix * arg list;
   type eq = (string * typ list) * cons list;
   val mk_arg : (bool * Datatype.dtyp) * string option * string -> arg;
   val is_lazy : arg -> bool;
@@ -220,6 +220,7 @@
 
 type cons =
      string *         (* operator name of constr *)
+     mixfix *         (* mixfix syntax of constructor *)
      arg list;        (* argument list      *)
 
 type eq =
@@ -258,7 +259,7 @@
 fun big_ssumD ds = case ds of [] => unitD | _ => foldr1 mk_ssumD ds;
 
 fun dtyp_of_arg ((lazy, D), _, _) = if lazy then mk_uD D else D;
-fun dtyp_of_cons (_, args) = big_sprodD (map dtyp_of_arg args);
+fun dtyp_of_cons (_, _, args) = big_sprodD (map dtyp_of_arg args);
 fun dtyp_of_eq (_, cons) = big_ssumD (map dtyp_of_cons cons);
 
 
@@ -377,8 +378,8 @@
                      else mapn (fn n => K("f"^(string_of_int n))) 1 cons;
 fun when_body cons funarg =
     let
-      fun one_fun n (_,[]  ) = /\ "dummy" (funarg(1,n))
-        | one_fun n (_,args) = let
+      fun one_fun n (_,_,[]  ) = /\ "dummy" (funarg(1,n))
+        | one_fun n (_,_,args) = let
             val l2 = length args;
             fun idxs m arg = (if is_lazy arg then (fn t => mk_fup (ID, t))
                               else I) (Bound(l2-m));
@@ -388,7 +389,7 @@
                   (args,
                 fn a=> /\#(a,(list_ccomb(funarg(l2,n),mapn idxs 1 args))))
                ) end;
-    in (if length cons = 1 andalso length(snd(hd cons)) <= 1
+    in (if length cons = 1 andalso length(third(hd cons)) <= 1
         then mk_strictify else I)
          (foldr1 mk_sscase (mapn one_fun 1 cons)) end;