move definition of match combinators to domain_constructors.ML

--- a/src/HOLCF/Tools/Domain/domain_axioms.ML	Sat Feb 27 16:34:13 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_axioms.ML	Sat Feb 27 18:09:11 2010 -0800
@@ -78,19 +78,6 @@
           (dc_abs oo (copy_of_dtyp map_tab r (dtyp_of_eq eqn)) oo dc_rep))
       end;
 
-    val mat_defs =
-      let
-        fun mdef (con, _, _) =
-          let
-            val k = Bound 0
-            val x = Bound 1
-            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))
-          in (mat_name con ^"_def", %%:(mat_name con) == rhs) end
-      in map mdef cons end;
-
     val pat_defs =
       let
         fun pdef (con, _, args) =
@@ -125,7 +112,7 @@
   in (dnam,
       (if definitional then [] else [abs_iso_ax, rep_iso_ax, reach_ax]),
       (if definitional then [when_def] else [when_def, copy_def]) @
-      mat_defs @ pat_defs @
+      pat_defs @
       [take_def, finite_def])
   end; (* let (calc_axioms) *)
 

--- a/src/HOLCF/Tools/Domain/domain_constructors.ML	Sat Feb 27 16:34:13 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_constructors.ML	Sat Feb 27 18:09:11 2010 -0800
@@ -26,7 +26,8 @@
            dist_eqs : thm list,
            cases : thm list,
            sel_rews : thm list,
-           dis_rews : thm list
+           dis_rews : thm list,
+           match_rews : thm list
          } * theory;
 end;
 
@@ -230,6 +231,13 @@
   sscase_const (T, U, U) ` mk_bottom (T ->> U) ` mk_ID U;
 
 
+(*** pattern match monad type ***)
+
+fun mk_matchT T = Type (@{type_name "maybe"}, [T]);
+
+fun mk_fail T = Const (@{const_name "Fixrec.fail"}, mk_matchT T);
+
+
 (*** miscellaneous constructions ***)
 
 val trT = @{typ "tr"};
@@ -892,6 +900,61 @@
   end;
 
 (******************************************************************************)
+(*************** definitions and theorems for match combinators ***************)
+(******************************************************************************)
+
+fun add_match_combinators
+    (bindings : binding list)
+    (spec : (term * (bool * typ) list) list)
+    (lhsT : typ)
+    (casedist : thm)
+    (case_const : typ -> term)
+    (case_rews : thm list)
+    (thy : theory) =
+  let
+
+    (* get a fresh type variable for the result type *)
+    val resultT : typ =
+      let
+        val ts : string list = map (fst o dest_TFree) (snd (dest_Type lhsT));
+        val t : string = Name.variant ts "'t";
+      in TFree (t, @{sort pcpo}) end;
+
+    (* define match combinators *)
+    local
+      val x = Free ("x", lhsT);
+      fun k args = Free ("k", map snd args -->> mk_matchT resultT);
+      val fail = mk_fail resultT;
+      fun mat_fun i (j, (con, args)) =
+        let
+          val Ts = map snd args;
+          val ns = Name.variant_list ["x","k"] (Datatype_Prop.make_tnames Ts);
+          val vs = map Free (ns ~~ Ts);
+        in
+          if i = j then k args else big_lambdas vs fail
+        end;
+      fun mat_eqn (i, (bind, (con, args))) : binding * term * mixfix =
+        let
+          val mat_bind = Binding.prefix_name "match_" bind;
+          val funs = map_index (mat_fun i) spec
+          val body = list_ccomb (case_const (mk_matchT resultT), funs);
+          val rhs = big_lambda x (big_lambda (k args) (body ` x));
+        in
+          (mat_bind, rhs, NoSyn)
+        end;
+    in
+      val ((match_consts, match_defs), thy) =
+          define_consts (map_index mat_eqn (bindings ~~ spec)) thy
+    end;
+
+  in
+    (match_defs, thy)
+(*
+    (match_stricts @ match_apps, thy)
+*)
+  end;
+
+(******************************************************************************)
 (******************************* main function ********************************)
 (******************************************************************************)
 
@@ -959,6 +1022,18 @@
           casedist case_const cases thy
       end
 
+    (* define and prove theorems for match combinators *)
+    val (match_thms : thm list, thy : theory) =
+      let
+        val bindings = map #1 spec;
+        fun prep_arg (lazy, sel, T) = (lazy, T);
+        fun prep_con c (b, args, mx) = (c, map prep_arg args);
+        val mat_spec = map2 prep_con con_consts spec;
+      in
+        add_match_combinators bindings mat_spec lhsT
+          casedist case_const cases thy
+      end
+
     (* restore original signature path *)
     val thy = Sign.parent_path thy;
 
@@ -975,7 +1050,8 @@
         dist_eqs = #dist_eqs con_result,
         cases = cases,
         sel_rews = sel_thms,
-        dis_rews = dis_thms };
+        dis_rews = dis_thms,
+        match_rews = match_thms };
   in
     (result, thy)
   end;

--- a/src/HOLCF/Tools/Domain/domain_syntax.ML	Sat Feb 27 16:34:13 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_syntax.ML	Sat Feb 27 18:09:11 2010 -0800
@@ -64,8 +64,6 @@
           | esc []      = []
       in implode o esc o Symbol.explode end;
 
-      fun mat_name_ con =
-          Binding.name ("match_" ^ strip_esc (Binding.name_of con));
       fun pat_name_ con =
           Binding.name (strip_esc (Binding.name_of con) ^ "_pat");
       (* strictly speaking, these constants have one argument,
@@ -75,12 +73,6 @@
           let val tvar = mk_TFree (s ^ string_of_int n)
           in if tvar mem typevars then freetvar ("t"^s) n else tvar end;
 
-      fun mk_matT (a,bs,c) =
-          a ->> List.foldr (op ->>) (mk_maybeT c) bs ->> mk_maybeT c;
-      fun mat (con,args,mx) =
-          (mat_name_ con,
-           mk_matT(dtype, map third args, freetvar "t" 1),
-           Mixfix(escape ("match_" ^ Binding.name_of con), [], Syntax.max_pri));
       fun mk_patT (a,b)     = a ->> mk_maybeT b;
       fun pat_arg_typ n arg = mk_patT (third arg, freetvar "t" n);
       fun pat (con,args,mx) =
@@ -90,7 +82,6 @@
              mk_patT (dtype, mk_ctupleT (map (freetvar "t") (1 upto length args))),
            Mixfix(escape (Binding.name_of con ^ "_pat"), [], Syntax.max_pri));
     in
-    val consts_mat = map mat cons';
     val consts_pat = map pat cons';
     end;
 
@@ -159,7 +150,7 @@
         if definitional then [] else [const_rep, const_abs, const_copy];
 
   in (optional_consts @ [const_when] @ 
-      consts_mat @ consts_pat @
+      consts_pat @
       [const_take, const_finite],
       (case_trans false :: case_trans true :: (abscon_trans false @ abscon_trans true @ Case_trans)))
   end; (* let *)

--- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Sat Feb 27 16:34:13 2010 -0800
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Sat Feb 27 18:09:11 2010 -0800
@@ -156,7 +156,6 @@
   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;
-  val axs_mat_def = map (get_def mat_name) cons;
   val axs_pat_def = map (get_def pat_name) cons;
   val ax_copy_def = ga "copy_def" dname;
 end; (* local *)
@@ -191,6 +190,7 @@
 val when_rews = #cases result;
 val when_strict = hd when_rews;
 val dis_rews = #dis_rews result;
+val axs_mat_def = #match_rews result;
 
 (* ----- theorems concerning the isomorphism -------------------------------- *)