# HG changeset patch
# User huffman
# Date 1266866261 28800
# Node ID aa7da51ae1ef56ec2b749e3a4ce5c4aca6d91472
# Parent  978a936faace2d3cc5081ce629df40faa53e1f08
add mixfix field to type Domain_Library.cons

diff -r 978a936faace -r aa7da51ae1ef src/HOLCF/Tools/Domain/domain_axioms.ML
--- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Mon Feb 22 09:43:36 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Mon Feb 22 11:17:41 2010 -0800
@@ -88,23 +88,23 @@
         | inj y i j = mk_sinr (inj y (i-1) (j-1));
     in List.foldr /\# (dc_abs`(inj (parms args) m n)) args end;
           
-    val con_defs = mapn (fn n => fn (con,args) =>
+    val con_defs = mapn (fn n => fn (con, _, args) =>
                                     (extern_name con ^"_def", %%:con == con_def (length cons) n (con,args))) 0 cons;
           
     val dis_defs = let
-      fun ddef (con,_) = (dis_name con ^"_def",%%:(dis_name con) == 
+      fun ddef (con,_,_) = (dis_name con ^"_def",%%:(dis_name con) == 
                                               list_ccomb(%%:(dname^"_when"),map 
-                                                                              (fn (con',args) => (List.foldr /\#
+                                                                              (fn (con',_,args) => (List.foldr /\#
       (if con'=con then TT else FF) args)) cons))
     in map ddef cons end;
 
     val mat_defs =
       let
-        fun mdef (con,_) =
+        fun mdef (con, _, _) =
           let
             val k = Bound 0
             val x = Bound 1
-            fun one_con (con', args') =
+            fun one_con (con', _, args') =
                 if con'=con then k else List.foldr /\# mk_fail args'
             val w = list_ccomb(%%:(dname^"_when"), map one_con cons)
             val rhs = /\ "x" (/\ "k" (w ` x))
@@ -113,14 +113,14 @@
 
     val pat_defs =
       let
-        fun pdef (con,args) =
+        fun pdef (con, _, args) =
           let
             val ps = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args;
             val xs = map (bound_arg args) args;
             val r = Bound (length args);
             val rhs = case args of [] => mk_return HOLogic.unit
                                  | _ => mk_ctuple_pat ps ` mk_ctuple xs;
-            fun one_con (con',args') = List.foldr /\# (if con'=con then rhs else mk_fail) args';
+            fun one_con (con', _, args') = List.foldr /\# (if con'=con then rhs else mk_fail) args';
           in (pat_name con ^"_def", list_comb (%%:(pat_name con), ps) == 
                                               list_ccomb(%%:(dname^"_when"), map one_con cons))
           end
@@ -129,9 +129,9 @@
     val sel_defs = let
       fun sdef con n arg = Option.map (fn sel => (sel^"_def",%%:sel == 
                                                             list_ccomb(%%:(dname^"_when"),map 
-                                                                                            (fn (con',args) => if con'<>con then UU else
+                                                                                            (fn (con', _, args) => if con'<>con then UU else
                                                                                                                List.foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg);
-    in map_filter I (maps (fn (con,args) => mapn (sdef con) 1 args) cons) end;
+    in map_filter I (maps (fn (con, _, args) => mapn (sdef con) 1 args) cons) end;
 
 
 (* ----- axiom and definitions concerning induction ------------------------- *)
@@ -175,7 +175,7 @@
 
 fun add_matchers (((dname,_),cons) : eq) thy =
     let
-      val con_names = map fst cons;
+      val con_names = map first cons;
       val mat_names = map mat_name con_names;
       fun qualify n = Sign.full_name thy (Binding.name n);
       val ms = map qualify con_names ~~ map qualify mat_names;
@@ -190,7 +190,7 @@
     val copy_def = ("copy_def" , %%:(comp_dname^"_copy") ==
                                  /\ "f"(mk_ctuple (map copy_app dnames)));
 
-    fun one_con (con,args) =
+    fun one_con (con, _, args) =
       let
         val nonrec_args = filter_out is_rec args;
         val    rec_args = filter is_rec args;
diff -r 978a936faace -r aa7da51ae1ef src/HOLCF/Tools/Domain/domain_extender.ML
--- a/src/HOLCF/Tools/Domain/domain_extender.ML	Mon Feb 22 09:43:36 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_extender.ML	Mon Feb 22 11:17:41 2010 -0800
@@ -161,6 +161,7 @@
       | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
     fun one_con (con,args,mx) =
         (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),
                    Option.map Binding.name_of sel,vn))
@@ -236,6 +237,7 @@
       | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
     fun one_con (con,args,mx) =
         (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),
                    Option.map Binding.name_of sel,vn))
diff -r 978a936faace -r aa7da51ae1ef src/HOLCF/Tools/Domain/domain_library.ML
--- 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;
 
diff -r 978a936faace -r aa7da51ae1ef src/HOLCF/Tools/Domain/domain_theorems.ML
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon Feb 22 09:43:36 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Mon Feb 22 11:17:41 2010 -0800
@@ -148,7 +148,7 @@
   val ax_abs_iso  = ga "abs_iso"  dname;
   val ax_rep_iso  = ga "rep_iso"  dname;
   val ax_when_def = ga "when_def" dname;
-  fun get_def mk_name (con,_) = ga (mk_name con^"_def") dname;
+  fun get_def mk_name (con, _, _) = ga (mk_name con^"_def") dname;
   val axs_con_def = map (get_def extern_name) cons;
   val axs_dis_def = map (get_def dis_name) cons;
   val axs_mat_def = map (get_def mat_name) cons;
@@ -157,7 +157,7 @@
     let
       fun def_of_sel sel = ga (sel^"_def") dname;
       fun def_of_arg arg = Option.map def_of_sel (sel_of arg);
-      fun defs_of_con (_, args) = map_filter def_of_arg args;
+      fun defs_of_con (_, _, args) = map_filter def_of_arg args;
     in
       maps defs_of_con cons
     end;
@@ -222,10 +222,10 @@
     in (n2, mk_sprodT (t1, t2)) end;
 
   fun cons2typ n [] = (n,oneT)
-    | cons2typ n [con] = args2typ n (snd con)
+    | cons2typ n [con] = args2typ n (third con)
     | cons2typ n (con::cons) =
     let
-      val (n1, t1) = args2typ n (snd con);
+      val (n1, t1) = args2typ n (third con);
       val (n2, t2) = cons2typ n1 cons
     in (n2, mk_ssumT (t1, t2)) end;
 in
@@ -234,7 +234,7 @@
 
 local 
   val iso_swap = iso_locale RS iso_iso_swap;
-  fun one_con (con, args) =
+  fun one_con (con, _, args) =
     let
       val vns = map vname args;
       val eqn = %:x_name === con_app2 con %: vns;
@@ -278,7 +278,7 @@
   val _ = trace " Proving when_apps...";
   val when_apps =
     let
-      fun one_when n (con,args) =
+      fun one_when n (con, _, args) =
         let
           val axs = when_appl :: con_appls;
           val goal = bind_fun (lift_defined %: (nonlazy args, 
@@ -293,12 +293,12 @@
 (* ----- theorems concerning the constructors, discriminators and selectors - *)
 
 local
-  fun dis_strict (con, _) =
+  fun dis_strict (con, _, _) =
     let
       val goal = mk_trp (strict (%%:(dis_name con)));
     in pg axs_dis_def goal (K [rtac when_strict 1]) end;
 
-  fun dis_app c (con, args) =
+  fun dis_app c (con, _, args) =
     let
       val lhs = %%:(dis_name c) ` con_app con args;
       val rhs = if con = c then TT else FF;
@@ -307,9 +307,9 @@
     in pg axs_dis_def goal (K tacs) end;
 
   val _ = trace " Proving dis_apps...";
-  val dis_apps = maps (fn (c,_) => map (dis_app c) cons) cons;
+  val dis_apps = maps (fn (c,_,_) => map (dis_app c) cons) cons;
 
-  fun dis_defin (con, args) =
+  fun dis_defin (con, _, args) =
     let
       val goal = defined (%:x_name) ==> defined (%%:(dis_name con) `% x_name);
       val tacs =
@@ -328,7 +328,7 @@
 end;
 
 local
-  fun mat_strict (con, _) =
+  fun mat_strict (con, _, _) =
     let
       val goal = mk_trp (%%:(mat_name con) ` UU ` %:"rhs" === UU);
       val tacs = [asm_simp_tac (HOLCF_ss addsimps [when_strict]) 1];
@@ -337,7 +337,7 @@
   val _ = trace " Proving mat_stricts...";
   val mat_stricts = map mat_strict cons;
 
-  fun one_mat c (con, args) =
+  fun one_mat c (con, _, args) =
     let
       val lhs = %%:(mat_name c) ` con_app con args ` %:"rhs";
       val rhs =
@@ -350,7 +350,7 @@
 
   val _ = trace " Proving mat_apps...";
   val mat_apps =
-    maps (fn (c,_) => map (one_mat c) cons) cons;
+    maps (fn (c,_,_) => map (one_mat c) cons) cons;
 in
   val mat_rews = mat_stricts @ mat_apps;
 end;
@@ -358,10 +358,10 @@
 local
   fun ps args = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args;
 
-  fun pat_lhs (con,args) = mk_branch (list_comb (%%:(pat_name con), ps args));
+  fun pat_lhs (con,_,args) = mk_branch (list_comb (%%:(pat_name con), ps args));
 
-  fun pat_rhs (con,[]) = mk_return ((%:"rhs") ` HOLogic.unit)
-    | pat_rhs (con,args) =
+  fun pat_rhs (con,_,[]) = mk_return ((%:"rhs") ` HOLogic.unit)
+    | pat_rhs (con,_,args) =
         (mk_branch (mk_ctuple_pat (ps args)))
           `(%:"rhs")`(mk_ctuple (map %# args));
 
@@ -372,11 +372,11 @@
       val tacs = [simp_tac (HOLCF_ss addsimps [when_strict]) 1];
     in pg axs goal (K tacs) end;
 
-  fun pat_app c (con, args) =
+  fun pat_app c (con, _, args) =
     let
       val axs = @{thm branch_def} :: axs_pat_def;
       val lhs = (pat_lhs c)`(%:"rhs")`(con_app con args);
-      val rhs = if con = fst c then pat_rhs c else mk_fail;
+      val rhs = if con = first c then pat_rhs c else mk_fail;
       val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs));
       val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
     in pg axs goal (K tacs) end;
@@ -390,7 +390,7 @@
 end;
 
 local
-  fun con_strict (con, args) = 
+  fun con_strict (con, _, args) = 
     let
       val rules = abs_strict :: @{thms con_strict_rules};
       fun one_strict vn =
@@ -401,7 +401,7 @@
         in pg con_appls goal (K tacs) end;
     in map one_strict (nonlazy args) end;
 
-  fun con_defin (con, args) =
+  fun con_defin (con, _, args) =
     let
       fun iff_disj (t, []) = HOLogic.mk_not t
         | iff_disj (t, ts) = t === foldr1 HOLogic.mk_disj ts;
@@ -423,7 +423,7 @@
 local
   val rules =
     [compact_sinl, compact_sinr, compact_spair, compact_up, compact_ONE];
-  fun con_compact (con, args) =
+  fun con_compact (con, _, args) =
     let
       val concl = mk_trp (mk_compact (con_app con args));
       val goal = lift (fn x => mk_compact (%#x)) (args, concl);
@@ -441,7 +441,7 @@
     pg axs_sel_def (mk_trp (strict (%%:sel)))
       (K [simp_tac (HOLCF_ss addsimps when_rews) 1]);
 
-  fun sel_strict (_, args) =
+  fun sel_strict (_, _, args) =
     map_filter (Option.map one_sel o sel_of) args;
 in
   val _ = trace " Proving sel_stricts...";
@@ -472,14 +472,14 @@
       val tacs2 = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
     in pg axs_sel_def goal (fn ctxt => (tacs1 ctxt @ tacs2)) end;
 
-  fun sel_app c n sel (con, args) =
+  fun sel_app c n sel (con, _, args) =
     if con = c
     then sel_app_same c n sel (con, args)
     else sel_app_diff c n sel (con, args);
 
   fun one_sel c n sel = map (sel_app c n sel) cons;
   fun one_sel' c n arg = Option.map (one_sel c n) (sel_of arg);
-  fun one_con (c, args) =
+  fun one_con (c, _, args) =
     flat (map_filter I (mapn (one_sel' c) 0 args));
 in
   val _ = trace " Proving sel_apps...";
@@ -501,7 +501,7 @@
   val sel_defins =
     if length cons = 1
     then map_filter (fn arg => Option.map sel_defin (sel_of arg))
-                 (filter_out is_lazy (snd (hd cons)))
+                 (filter_out is_lazy (third (hd cons)))
     else [];
 end;
 
@@ -522,7 +522,7 @@
         val tacs = [simp_tac (HOL_ss addsimps rules) 1];
       in pg con_appls goal (K tacs) end;
 
-    fun distinct (con1, args1) (con2, args2) =
+    fun distinct (con1, _, args1) (con2, _, args2) =
         let
           val arg1 = (con1, args1);
           val arg2 =
@@ -554,7 +554,7 @@
         val tacs = [simp_tac (HOL_ss addsimps rules) 1];
       in pg con_appls goal (K tacs) end;
 
-    fun distinct (con1, args1) (con2, args2) =
+    fun distinct (con1, _, args1) (con2, _, args2) =
         let
           val arg1 = (con1, args1);
           val arg2 =
@@ -576,7 +576,7 @@
       val sargs = case largs of [_] => [] | _ => nonlazy args;
       val prop = lift_defined %: (sargs, mk_trp (prem === concl));
     in pg con_appls prop end;
-  val cons' = filter (fn (_,args) => args<>[]) cons;
+  val cons' = filter (fn (_, _, args) => args<>[]) cons;
 in
   val _ = trace " Proving inverts...";
   val inverts =
@@ -584,14 +584,14 @@
       val abs_less = ax_abs_iso RS (allI RS injection_less);
       val tacs =
         [asm_full_simp_tac (HOLCF_ss addsimps [abs_less, spair_less]) 1];
-    in map (fn (con, args) => pgterm (op <<) con args (K tacs)) cons' end;
+    in map (fn (con, _, args) => pgterm (op <<) con args (K tacs)) cons' end;
 
   val _ = trace " Proving injects...";
   val injects =
     let
       val abs_eq = ax_abs_iso RS (allI RS injection_eq);
       val tacs = [asm_full_simp_tac (HOLCF_ss addsimps [abs_eq, spair_eq]) 1];
-    in map (fn (con, args) => pgterm (op ===) con args (K tacs)) cons' end;
+    in map (fn (con, _, args) => pgterm (op ===) con args (K tacs)) cons' end;
 end;
 
 (* ----- theorems concerning one induction step ----------------------------- *)
@@ -610,7 +610,7 @@
   end;
 
 local
-  fun copy_app (con, args) =
+  fun copy_app (con, _, args) =
     let
       val lhs = dc_copy`%"f"`(con_app con args);
       fun one_rhs arg =
@@ -635,7 +635,7 @@
 end;
 
 local
-  fun one_strict (con, args) = 
+  fun one_strict (con, _, args) = 
     let
       val goal = mk_trp (dc_copy`UU`(con_app con args) === UU);
       val rews = the_list copy_strict @ copy_apps @ con_rews;
@@ -648,7 +648,7 @@
       | ERROR s => (trace s; NONE)
     end;
 
-  fun has_nonlazy_rec (_, args) = exists is_nonlazy_rec args;
+  fun has_nonlazy_rec (_, _, args) = exists is_nonlazy_rec args;
 in
   val _ = trace " Proving copy_stricts...";
   val copy_stricts = map_filter one_strict (filter has_nonlazy_rec cons);
@@ -749,7 +749,7 @@
     in pg axs_take_def goal (K [simp_tac iterate_Cprod_ss 1]) end;
   val take_0s = mapn take_0 1 dnames;
   val _ = trace " Proving take_apps...";
-  fun one_take_app dn (con, args) =
+  fun one_take_app dn (con, _, args) =
     let
       fun mk_take n = dc_take (List.nth (dnames, n)) $ %:"n";
       fun one_rhs arg =
@@ -773,7 +773,7 @@
 end; (* local *)
 
 local
-  fun one_con p (con,args) =
+  fun one_con p (con, _, args) =
     let
       fun ind_hyp arg = %:(P_name (1 + rec_of arg)) $ bound_arg args arg;
       val t1 = mk_trp (%:p $ con_app2 con (bound_arg args) args);
@@ -794,7 +794,7 @@
   fun ind_prems_tac prems = EVERY
     (maps (fn cons =>
       (resolve_tac prems 1 ::
-        maps (fn (_,args) => 
+        maps (fn (_,_,args) => 
           resolve_tac prems 1 ::
           map (K(atac 1)) (nonlazy args) @
           map (K(atac 1)) (filter is_rec args))
@@ -809,7 +809,7 @@
           ((rec_of arg =  n andalso nfn(lazy_rec orelse is_lazy arg)) orelse 
             rec_of arg <> n andalso rec_to quant nfn rfn (rec_of arg::ns) 
               (lazy_rec orelse is_lazy arg) (n, (List.nth(conss,rec_of arg))))
-          ) o snd) cons;
+          ) o third) cons;
     fun all_rec_to ns  = rec_to forall not all_rec_to  ns;
     fun warn (n,cons) =
       if all_rec_to [] false (n,cons)
@@ -840,7 +840,7 @@
           fun arg_tac arg =
             case_UU_tac context (prems @ con_rews) 1
               (List.nth (dnames, rec_of arg) ^ "_take n$" ^ vname arg);
-          fun con_tacs (con, args) = 
+          fun con_tacs (con, _, args) = 
             asm_simp_tac take_ss 1 ::
             map arg_tac (filter is_nonlazy_rec args) @
             [resolve_tac prems 1] @
@@ -927,7 +927,7 @@
               etac disjE 1,
               asm_simp_tac (HOL_ss addsimps con_rews) 1,
               asm_simp_tac take_ss 1];
-            fun con_tacs ctxt (con, args) =
+            fun con_tacs ctxt (con, _, args) =
               asm_simp_tac take_ss 1 ::
               maps (arg_tacs ctxt) (nonlazy_rec args);
             fun foo_tacs ctxt n (cons, cases) =