src/HOLCF/domain/extender.ML

 (* extender.ML
-   ID:         $Id$
    Author : David von Oheimb
    Created: 17-May-95
    Updated: 31-May-95 extracted syntax.ML, theorems.ML
    Updated: 07-Jul-95 streamlined format of cons list
    Updated: 21-Jul-95 gen_by-section
    Updated: 28-Aug-95 simultaneous domain equations
    Copyright 1995 TU Muenchen
 *)
 
 
-structure Extender =
+structure Domain_Extender =
 struct
 
 local
 
 open Domain_Library;
 
 (* ----- general testing and preprocessing of constructor list -------------------- *)
 
   fun check_domain(eqs':((string * typ list) *
-                  (string * ThyOps.cmixfix * (bool*string*typ) list) list) list) = let
+		  (string * ThyOps.cmixfix * (bool*string*typ) list) list) list) = let
     val dtnvs = map fst eqs';
     val cons' = flat (map snd eqs');
     val test_dupl_typs = (case duplicates (map fst dtnvs) of 
-        [] => false | dups => error ("Duplicate types: " ^ commas_quote dups));
+	[] => false | dups => error ("Duplicate types: " ^ commas_quote dups));
     val test_dupl_cons = (case duplicates (map first cons') of 
-        [] => false | dups => error ("Duplicate constructors: " ^ commas_quote dups));
+	[] => false | dups => error ("Duplicate constructors: " ^ commas_quote dups));
     val test_dupl_sels = (case duplicates(map second (flat(map third cons'))) of
         [] => false | dups => error ("Duplicate selectors: "^commas_quote dups));
     val test_dupl_tvars = let fun vname (TFree(v,_)) = v
-                              |   vname _            = Imposs "extender:vname";
-                          in exists (fn tvars => case duplicates (map vname tvars) of
-        [] => false | dups => error ("Duplicate type arguments: " ^commas_quote dups))
-        (map snd dtnvs) end;
+			      |   vname _            = Imposs "extender:vname";
+			  in exists (fn tvars => case duplicates (map vname tvars) of
+	[] => false | dups => error ("Duplicate type arguments: " ^commas_quote dups))
+	(map snd dtnvs) end;
     (*test for free type variables and invalid use of recursive type*)
     val analyse_types = forall (fn ((_,typevars),cons') => 
-        forall (fn con' => let
-          val types = map third (third con');
+	forall (fn con' => let
+	  val types = map third (third con');
           fun analyse(t as TFree(v,_)) = t mem typevars orelse
-                                        error ("Free type variable " ^ v ^ " on rhs.")
-            | analyse(Type(s,typl)) = (case assoc (dtnvs,s) of None => analyses typl
-                                      | Some tvs => tvs = typl orelse 
-                       error ("Recursion of type " ^ s ^ " with different arguments"))
-            | analyse(TVar _) = Imposs "extender:analyse"
-          and analyses ts = forall analyse ts;
-          in analyses types end) cons' 
-        ) eqs';
+					error ("Free type variable " ^ v ^ " on rhs.")
+	    | analyse(Type(s,typl)) = (case assoc (dtnvs,s) of None => analyses typl
+				      | Some tvs => tvs = typl orelse 
+		       error ("Recursion of type " ^ s ^ " with different arguments"))
+	    | analyse(TVar _) = Imposs "extender:analyse"
+	  and analyses ts = forall analyse ts;
+	  in analyses types end) cons' 
+	) eqs';
     in true end; (* let *)
 
   fun check_gen_by thy' (typs': string list,cnstrss': string list list) = let
     val test_dupl_typs = (case duplicates typs' of [] => false
-          | dups => error ("Duplicate types: " ^ commas_quote dups));
+	  | dups => error ("Duplicate types: " ^ commas_quote dups));
     val test_dupl_cnstrs = map (fn cnstrs' => (case duplicates cnstrs' of [] => false
-          | dups => error ("Duplicate constructors: " ^ commas_quote dups))) cnstrss';
+	  | dups => error ("Duplicate constructors: " ^ commas_quote dups))) cnstrss';
     val tsig = #tsig(Sign.rep_sg(sign_of thy'));
     val tycons = map fst (#tycons(Type.rep_tsig tsig));
     val test_types = forall(fn t=>t mem tycons orelse error("Unknown type: "^t))typs';
     val cnstrss = let
-        fun type_of c = case (Sign.const_type(sign_of thy') c) of Some t => t
-                                | None => error ("Unknown constructor: "^c);
-        fun args_result_type (t as (Type(tn,[arg,rest]))) = 
-                        if tn = "->" orelse tn = "=>"
-                        then let val (ts,r) = args_result_type rest in (arg::ts,r) end
-                        else ([],t)
-        |   args_result_type t = ([],t);
+	fun type_of c = case (Sign.const_type(sign_of thy') c) of Some t => t
+				| None => error ("Unknown constructor: "^c);
+	fun args_result_type (t as (Type(tn,[arg,rest]))) = 
+			if tn = "->" orelse tn = "=>"
+			then let val (ts,r) = args_result_type rest in (arg::ts,r) end
+			else ([],t)
+	|   args_result_type t = ([],t);
     in map (map (fn cn => let val (args,res) = args_result_type (type_of cn) in
-                         (cn,mk_var_names args,(args,res)) end)) cnstrss' 
-        : (string *                     (* operator name of constr *)
-           string list *                (* argument name list *)
-           (typ list *                  (* argument types *)
-            typ))                       (* result type *)
-          list list end;
+	                 (cn,mk_var_names args,(args,res)) end)) cnstrss' 
+	: (string * 			(* operator name of constr *)
+	   string list *		(* argument name list *)
+	   (typ list *			(* argument types *)
+	    typ))			(* result type *)
+	  list list end;
     fun test_equal_type tn (cn,_,(_,rt)) = fst (type_name_vars rt) = tn orelse
-                               error("Inappropriate result type for constructor "^cn);
-    val typs = map (fn (tn, cnstrs) => 
-                     (map (test_equal_type tn) cnstrs; snd(third(hd(cnstrs)))))
-                   (typs'~~cnstrss);
+			       error("Inappropriate result type for constructor "^cn);
+    val typs = map (fn (tn, cnstrs) => (map (test_equal_type tn) cnstrs; 
+					snd(third(hd(cnstrs)))))  (typs'~~cnstrss);
     val test_typs = map (fn (typ,cnstrs) => 
-                        if not (Type.typ_instance(tsig,typ,TVar(("'a",0),["pcpo"])))
-                        then error("Not a pcpo type: "^fst(type_name_vars typ))
-                        else map (fn (cn,_,(_,rt)) => rt=typ 
-                          orelse error("Non-identical result types for constructors "^
-                          first(hd cnstrs)^" and "^ cn )) cnstrs) (typs~~cnstrss);
+			if not (Type.typ_instance(tsig,typ,TVar(("'a",0),["pcpo"])))
+			then error("Not a pcpo type: "^fst(type_name_vars typ))
+			else map (fn (cn,_,(_,rt)) => rt=typ 
+		 	  orelse error("Non-identical result types for constructors "^
+			  first(hd cnstrs)^" and "^ cn )) cnstrs) (typs~~cnstrss);
     val proper_args = let
-        fun occurs tn (Type(tn',ts)) = (tn'=tn) orelse exists (occurs tn) ts
-        |   occurs _  _              = false;
-        fun proper_arg cn atyp = forall (fn typ => let 
-                                   val tn = fst(type_name_vars typ) 
-                                   in atyp=typ orelse not (occurs tn atyp) orelse 
-                                      error("Illegal use of type "^ tn ^
-                                         " as argument of constructor " ^cn)end )typs;
-        fun proper_curry (cn,_,(args,_)) = forall (proper_arg cn) args;
+	fun occurs tn (Type(tn',ts)) = (tn'=tn) orelse exists (occurs tn) ts
+	|   occurs _  _              = false;
+	fun proper_arg cn atyp = forall (fn typ => let 
+				   val tn = fst(type_name_vars typ) 
+				   in atyp=typ orelse not (occurs tn atyp) orelse 
+				      error("Illegal use of type "^ tn ^
+					 " as argument of constructor " ^cn)end )typs;
+	fun proper_curry (cn,_,(args,_)) = forall (proper_arg cn) args;
     in map (map proper_curry) cnstrss end;
   in (typs, flat cnstrss) end;
 
 (* ----- calls for building new thy and thms -------------------------------------- *)
 
 in
 
   fun add_domain (comp_dname,eqs') thy'' = let
-    val ok_dummy = check_domain eqs';
+    val ok   = check_domain eqs';
     val thy' = thy'' |> Domain_Syntax.add_syntax (comp_dname,eqs');
     val dts  = map (Type o fst) eqs';
     fun cons cons' = (map (fn (con,syn,args) =>
-        (ThyOps.const_name con syn,
-         map (fn ((lazy,sel,tp),vn) => ((lazy,
-                                         find (tp,dts) handle LIST "find" => ~1),
-                                        sel,vn))
-             (args~~(mk_var_names(map third args)))
-         )) cons') : cons list;
+	(ThyOps.const_name con syn,
+	 map (fn ((lazy,sel,tp),vn) => ((lazy,
+					 find (tp,dts) handle LIST "find" => ~1),
+					sel,vn))
+	     (args~~(mk_var_names(map third args)))
+	 )) cons') : cons list;
     val eqs = map (fn (dtnvs,cons') => (dtnvs,cons cons')) eqs' : eq list;
     val thy         = thy' |> Domain_Axioms.add_axioms (comp_dname,eqs);
   in (thy,eqs) end;
 
   fun add_gen_by ((tname,finite),(typs',cnstrss')) thy' = let
    val (typs,cnstrs) = check_gen_by thy' (typs',cnstrss');
   in
-   Domain_Axioms.add_gen_by ((tname,finite),(typs,cnstrs)) thy' end;
+   Domain_Axioms.add_induct ((tname,finite),(typs,cnstrs)) thy' end;
 
 end (* local *)
 end (* struct *)