# HG changeset patch
# User huffman
# Date 1130983562 -3600
# Node ID ec9e36ece6bb6cb79e6be92e62635dd24047ad4c
# Parent  3f767ed1f7ae71d3f43cc0229e4855008f7310dc
improve support for mutual recursion: now generates correct copy constant and induction theorem for mutually-recursive types; initial support for indirect recursion

diff -r 3f767ed1f7ae -r ec9e36ece6bb src/HOLCF/domain/axioms.ML
--- a/src/HOLCF/domain/axioms.ML	Thu Nov 03 02:37:09 2005 +0100
+++ b/src/HOLCF/domain/axioms.ML	Thu Nov 03 03:06:02 2005 +0100
@@ -84,7 +84,7 @@
 
   val reach_ax = ("reach", mk_trp(cproj (%%:fixN`%%(comp_dname^"_copy")) eqs n
 					`%x_name === %:x_name));
-  val take_def = ("take_def",%%:(dname^"_take") == mk_lam("n",cproj' 
+  val take_def = ("take_def",%%:(dname^"_take") == mk_lam("n",cproj
 	     (%%:iterateN $ Bound 0 ` %%:(comp_dname^"_copy") ` UU) eqs n));
   val finite_def = ("finite_def",%%:(dname^"_finite") == mk_lam(x_name,
 	mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
diff -r 3f767ed1f7ae -r ec9e36ece6bb src/HOLCF/domain/extender.ML
--- a/src/HOLCF/domain/extender.ML	Thu Nov 03 02:37:09 2005 +0100
+++ b/src/HOLCF/domain/extender.ML	Thu Nov 03 03:06:02 2005 +0100
@@ -25,8 +25,11 @@
 
 signature DOMAIN_EXTENDER =
 sig
-  val add_domain: string *
-      ((bstring * string list) * (string * mixfix * (bool * string option * string) list) list) list
+  val add_domain: string * ((bstring * string list) *
+    (string * mixfix * (bool * string option * string) list) list) list
+    -> theory -> theory
+  val add_domain_i: string * ((bstring * string list) *
+    (string * mixfix * (bool * string option * typ) list) list) list
     -> theory -> theory
 end;
 
@@ -36,8 +39,8 @@
 open Domain_Library;
 
 (* ----- general testing and preprocessing of constructor list -------------- *)
-  fun check_and_sort_domain (dtnvs: (string * typ list) list, 
-     cons'' : ((string * mixfix * (bool*string option*typ) list) list) list) sg =
+fun check_and_sort_domain (dtnvs: (string * typ list) list, 
+     cons'' : ((string * mixfix * (bool * string option * typ) list) list) list) sg =
   let
     val defaultS = Sign.defaultS sg;
     val test_dupl_typs = (case duplicates (map fst dtnvs) of 
@@ -57,9 +60,7 @@
     fun analyse_equation ((dname,typevars),cons') = 
       let
 	val tvars = map dest_TFree typevars;
-	fun distinct_name s = "'"^Sign.base_name dname^"_"^s;
-	val distinct_typevars = map (fn (n,sort) => 
-				     TFree (distinct_name n,sort)) tvars;
+	val distinct_typevars = map TFree tvars;
 	fun rm_sorts (TFree(s,_)) = TFree(s,[])
 	|   rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts)
 	|   rm_sorts (TVar(s,_))  = TVar(s,[])
@@ -69,7 +70,7 @@
 		    NONE => error ("Free type variable " ^ quote v ^ " on rhs.")
 	          | SOME sort => if eq_set_string (s,defaultS) orelse
 				    eq_set_string (s,sort    )
-				 then TFree(distinct_name v,sort)
+				 then TFree(v,sort)
 				 else error ("Inconsistent sort constraint" ^
 				             " for type variable " ^ quote v))
         |   analyse indirect (t as Type(s,typl)) = (case AList.lookup (op =) dtnvs s of
@@ -87,8 +88,8 @@
 					     quote (string_of_typ sg t) ^ 
 					    " with different arguments"))
         |   analyse indirect (TVar _) = Imposs "extender:analyse";
-	fun check_pcpo t = (pcpo_type sg t orelse error(
-      "Constructor argument type is not of sort pcpo: "^string_of_typ sg t); t);
+	fun check_pcpo T = if pcpo_type sg T then T
+          else error("Constructor argument type is not of sort pcpo: "^string_of_typ sg T);
 	val analyse_con = upd_third (map (upd_third (check_pcpo o analyse false)));
       in ((dname,distinct_typevars), map analyse_con cons') end; 
   in ListPair.map analyse_equation (dtnvs,cons'')
@@ -96,46 +97,49 @@
 
 (* ----- calls for building new thy and thms -------------------------------- *)
 
-  fun add_domain (comp_dnam,eqs''') thy''' = let
-    val sg''' = sign_of thy''';
+fun gen_add_domain prep_typ (comp_dnam, eqs''') thy''' =
+  let
     val dtnvs = map ((fn (dname,vs) => 
-			 (Sign.full_name sg''' dname,map (str2typ sg''') vs))
+			 (Sign.full_name thy''' dname, map (str2typ thy''') vs))
                    o fst) eqs''';
     val cons''' = map snd eqs''';
     fun thy_type  (dname,tvars)  = (Sign.base_name dname, length tvars, NoSyn);
     fun thy_arity (dname,tvars)  = (dname, map (snd o dest_TFree) tvars, pcpoS);
     val thy'' = thy''' |> Theory.add_types     (map thy_type  dtnvs)
 		       |> Theory.add_arities_i (map thy_arity dtnvs);
-    val sg'' = sign_of thy'';
-    val cons''=map (map (upd_third (map (upd_third (str2typ sg''))))) cons''';
-    val eqs' = check_and_sort_domain (dtnvs,cons'') sg'';
+    val cons'' = map (map (upd_third (map (upd_third (prep_typ thy''))))) cons''';
+    val eqs' = check_and_sort_domain (dtnvs,cons'') thy'';
     val thy' = thy'' |> Domain_Syntax.add_syntax (comp_dnam,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 = Library.drop (find_index_eq "'" ss +1, ss);
     fun typid (Type  (id,_)) =
           let val c = hd (Symbol.explode (Sign.base_name id))
           in if Symbol.is_letter c then c else "t" end
       | typid (TFree (id,_)   ) = hd (strip (tl (Symbol.explode id)))
       | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id));
-    fun cons cons' = (map (fn (con,syn,args) =>
-	((Syntax.const_name con syn),
+    fun one_con (con,mx,args) =
+	((Syntax.const_name con mx),
 	 ListPair.map (fn ((lazy,sel,tp),vn) => ((lazy,
-					find_index_eq tp dts),
+					find_index_eq tp dts,
+					DatatypeAux.dtyp_of_typ new_dts tp),
 					sel,vn))
 	     (args,(mk_var_names(map (typid o third) args)))
-	 )) cons') : cons list;
-    val eqs = map (fn (dtnvs,cons') => (dtnvs,cons cons')) eqs' : eq list;
+	 ) : cons;
+    val eqs = map (fn (dtnvs,cons') => (dtnvs, map one_con cons')) eqs' : eq list;
     val thy        = thy' |> Domain_Axioms.add_axioms (comp_dnam,eqs);
     val (theorems_thy, (rewss, take_rews)) = (foldl_map (fn (thy0,eq) =>
       Domain_Theorems.theorems (eq,eqs) thy0) (thy,eqs))
       |>>> Domain_Theorems.comp_theorems (comp_dnam, eqs);
-in
-  theorems_thy
-  |> Theory.add_path (Sign.base_name comp_dnam)
-  |> (#1 o (PureThy.add_thmss [(("rews", List.concat rewss @ take_rews), [])]))
-  |> Theory.parent_path
-end;
+  in
+    theorems_thy
+    |> Theory.add_path (Sign.base_name comp_dnam)
+    |> (#1 o (PureThy.add_thmss [(("rews", List.concat rewss @ take_rews), [])]))
+    |> Theory.parent_path
+  end;
 
+val add_domain_i = gen_add_domain Sign.certify_typ;
+val add_domain = gen_add_domain str2typ;
 
 
 (** outer syntax **)
@@ -174,6 +178,6 @@
 val _ = OuterSyntax.add_keywords ["lazy"];
 val _ = OuterSyntax.add_parsers [domainP];
 
-end;
+end; (* local structure *)
 
 end;
diff -r 3f767ed1f7ae -r ec9e36ece6bb src/HOLCF/domain/library.ML
--- a/src/HOLCF/domain/library.ML	Thu Nov 03 02:37:09 2005 +0100
+++ b/src/HOLCF/domain/library.ML	Thu Nov 03 03:06:02 2005 +0100
@@ -77,17 +77,17 @@
 
 (* ----- constructor list handling ----- *)
 
-type cons = (string *			(* operator name of constr *)
-	    ((bool*int)*		(*  (lazy,recursive element or ~1) *)
-	      string option*		(*   selector name    *)
-	      string)			(*   argument name    *)
-	    list);			(* argument list      *)
+type cons = (string *				(* operator name of constr *)
+	    ((bool*int*DatatypeAux.dtyp)*	(*  (lazy,recursive element or ~1) *)
+	      string option*			(*   selector name    *)
+	      string)				(*   argument name    *)
+	    list);				(* argument list      *)
 type eq = (string *		(* name      of abstracted type *)
 	   typ list) *		(* arguments of abstracted type *)
 	  cons list;		(* represented type, as a constructor list *)
 
-fun rec_of arg  = snd (first arg);
-fun is_lazy arg = fst (first arg);
+fun rec_of arg  = second (first arg);
+fun is_lazy arg = first (first arg);
 val sel_of    =       second;
 val     vname =       third;
 val upd_vname =   upd_third;
@@ -185,17 +185,8 @@
 fun prj _  _  x (   _::[]) _ = x
 |   prj f1 _  x (_::y::ys) 0 = f1 x y
 |   prj f1 f2 x (y::   ys) j = prj f1 f2 (f2 x y) ys (j-1);
-fun fix_tp (tn, args) = (tn, map (K oneT) args); (* instantiate type to
-						    avoid type varaibles *)
 fun  proj x      = prj (fn S => K(%%:"fst" $S)) (fn S => K(%%:"snd" $S)) x;
 fun cproj x      = prj (fn S => K(%%:cfstN`S)) (fn S => K(%%:csndN`S)) x;
-fun prj' _  _  x (   _::[]) _ = x
-|   prj' f1 _  x (_::   ys) 0 = f1 x (foldr1 HOLogic.mk_prodT ys)
-|   prj' f1 f2 x (y::   ys) j = prj' f1 f2 (f2 x y) ys (j-1);
-fun cproj' T eqs = prj'
-	(fn S => fn t => Const(cfstN, HOLogic.mk_prodT(dummyT,t)->>dummyT)`S)
-	(fn S => fn t => Const(csndN, HOLogic.mk_prodT(t,dummyT)->>dummyT)`S) 
-		       T (map ((fn tp => tp ->> tp) o Type o fix_tp o fst) eqs);
 fun lift tfn = Library.foldr (fn (x,t)=> (mk_trp(tfn x) ===> t));
 
 fun /\ v T = %%:Abs_CFunN $ mk_lam(v,T);