src/HOLCF/domain/extender.ML

Updated: 01-Mar-96 when functional strictified, copy_def based on when_def

(* extender.ML
   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 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
    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));
    val test_dupl_cons = (case duplicates (map first cons') of 
	[] => 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;
    (*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');
          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';
    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));
    val test_dupl_cnstrs = map (fn cnstrs' => (case duplicates cnstrs' of [] => false
	  | 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);
    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;
    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);
    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);
    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;
    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   = 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;
    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_induct ((tname,finite),(typs,cnstrs)) thy' end;

end (* local *)
end (* struct *)