adapted domain and ax_ops package for name spaces
authoroheimb
Mon Oct 27 11:34:33 1997 +0100 (1997-10-27)
changeset 40082444085532c6
parent 4007 1d6aed7ff375
child 4009 6d9bec7b0b9e
adapted domain and ax_ops package for name spaces
src/HOLCF/ROOT.ML
src/HOLCF/ax_ops/holcflogic.ML
src/HOLCF/ax_ops/thy_ops.ML
src/HOLCF/domain/axioms.ML
src/HOLCF/domain/extender.ML
src/HOLCF/domain/interface.ML
src/HOLCF/domain/library.ML
src/HOLCF/domain/syntax.ML
src/HOLCF/domain/theorems.ML
     1.1 --- a/src/HOLCF/ROOT.ML	Mon Oct 27 10:46:36 1997 +0100
     1.2 +++ b/src/HOLCF/ROOT.ML	Mon Oct 27 11:34:33 1997 +0100
     1.3 @@ -16,7 +16,6 @@
     1.4  
     1.5  use_thy "HOLCF";
     1.6  
     1.7 -
     1.8  (* sections axioms, ops *)
     1.9  
    1.10  use "ax_ops/holcflogic.ML";
    1.11 @@ -24,7 +23,6 @@
    1.12  use "ax_ops/thy_ops.ML";
    1.13  use "ax_ops/thy_syntax.ML";
    1.14  
    1.15 -
    1.16  (* sections domain, generated *)
    1.17  
    1.18  use "domain/library.ML";
    1.19 @@ -34,7 +32,6 @@
    1.20  use "domain/extender.ML";
    1.21  use "domain/interface.ML";
    1.22  
    1.23 -
    1.24  print_depth 10;  
    1.25  
    1.26  val HOLCF_build_completed = (); (*indicate successful build*)
     2.1 --- a/src/HOLCF/ax_ops/holcflogic.ML	Mon Oct 27 10:46:36 1997 +0100
     2.2 +++ b/src/HOLCF/ax_ops/holcflogic.ML	Mon Oct 27 11:34:33 1997 +0100
     2.3 @@ -20,6 +20,7 @@
     2.4   val mkNotEqUU : term -> term;            (* Trueprop(x ~= UU) *)
     2.5   val mkNotEqUU_in : term -> term -> term; (* "v~=UU ==> t" *)
     2.6   val ==>     : typ * typ -> typ;          (* Infix operation typ constructor *)
     2.7 + val cfun_arrow : string                  (* internalized "->" *)
     2.8   val mkOpApp : term -> term -> term;      (* Ops application (f ` x) *)
     2.9   val mkCPair : term -> term -> term;      (* cpair constructor *)
    2.10  end;
    2.11 @@ -44,12 +45,16 @@
    2.12  fun mkNotEqUU_in vterm term = 
    2.13     mk_implies(mkNotEqUU vterm,term)
    2.14  
    2.15 +val HOLCF_sg = sign_of HOLCF.thy;
    2.16 +fun mk_typ t (S,T) = Sign.intern_typ HOLCF_sg (Type(t,[S,T]));
    2.17 +fun rep_Type  (Type  x) = x| rep_Type _ = error "Internal error: rep_Type";
    2.18  
    2.19  infixr 6 ==>; (* the analogon to --> for operations *)
    2.20 -fun a ==> b = Type("->",[a,b]);
    2.21 +val op ==> = mk_typ "->";
    2.22 +val cfun_arrow = fst (rep_Type (dummyT ==> dummyT));
    2.23  
    2.24  (* Ops application (f ` x) *)
    2.25 -fun mkOpApp (f as Const(_,ft as Type("->",[xt,rt]))) x =
    2.26 +fun mkOpApp (f as Const(_,ft as Type(_(*"->"*),[xt,rt]))) x =
    2.27       Const("fapp",ft --> xt --> rt) $ f $ x
    2.28    | mkOpApp f x = (error("Internal error: mkOpApp: wrong args"));
    2.29  
     3.1 --- a/src/HOLCF/ax_ops/thy_ops.ML	Mon Oct 27 10:46:36 1997 +0100
     3.2 +++ b/src/HOLCF/ax_ops/thy_ops.ML	Mon Oct 27 11:34:33 1997 +0100
     3.3 @@ -106,14 +106,13 @@
     3.4  
     3.5  (* Changing a->b->c res. a*b->c to a=>b=>c. Called by syn_decls. *) 
     3.6  (*####*)
     3.7 -fun op_to_fun true  sign (Type("->" ,[larg,t]))=
     3.8 -                                         Type("fun",[larg,op_to_fun true sign t])
     3.9 -  | op_to_fun false sign (Type("->",[args,res])) = let
    3.10 +fun op_to_fun true  sign (ty as Type(name ,[larg,t]))= if name = cfun_arrow
    3.11 +                  then Type("fun",[larg,op_to_fun true sign t]) else ty
    3.12 +  | op_to_fun false sign (ty as Type(name,[args,res])) = let
    3.13                  fun otf (Type("*",[larg,rargs])) = Type("fun",[larg,otf rargs])
    3.14                  |   otf t                        = Type("fun",[t,res]);
    3.15 -                in otf args end
    3.16 -  | op_to_fun _     sign t = t(*error("Wrong type for cinfix/cmixfix : "^
    3.17 -                              (Sign.string_of_typ sign t))*);
    3.18 +                in if name = cfun_arrow then otf args else ty end
    3.19 +  | op_to_fun _     sign t = t;
    3.20  (*####*)
    3.21  
    3.22  (* oldstyle is called by add_ext_axioms(_i) *)
    3.23 @@ -140,9 +139,6 @@
    3.24       (name,op_to_fun curried sign typ,Mixfix.Infixr(i))::
    3.25        (syn_decls curried sign tl)
    3.26    | syn_decls curried sign ((name,typ,CMixfix(x))::tl) =
    3.27 -(*####
    3.28 -     ("@"^name,op_to_fun curried sign typ,Mixfix.Mixfix(x))::
    3.29 -####**)
    3.30       (name,op_to_fun curried sign typ,Mixfix.Mixfix(x))::
    3.31  
    3.32        (syn_decls curried sign tl)
    3.33 @@ -170,7 +166,8 @@
    3.34      ::xrules_of true tail
    3.35  (*####*)
    3.36    | xrules_of true ((name,typ,CMixfix(_))::tail) = 
    3.37 -        let fun argnames n (Type("->" ,[_,t]))= chr n :: argnames (n+1) t
    3.38 +        let fun argnames n (Type(name ,[_,t]))= if name = cfun_arrow then
    3.39 +					chr n :: argnames (n+1) t else []
    3.40              |   argnames _ _ = [];
    3.41              val names = argnames (ord"A") typ;
    3.42          in if names = [] then [] else 
    3.43 @@ -200,7 +197,8 @@
    3.44  	      in  itr l end;
    3.45  	    fun argnames n (Type("*" ,[_,t]))= chr n :: argnames (n+1) t
    3.46  	    |   argnames n _ = [chr n];
    3.47 -	    val vars = map Variable (case typ of (Type("->" ,[t,_])) =>argnames (ord"A") t
    3.48 +	    val vars = map Variable (case typ of (Type(name ,[t,_])) =>
    3.49 +			if name = cfun_arrow then argnames (ord"A") t else []
    3.50  						 | _ => []);
    3.51          in if vars = [] then [] else 
    3.52  	    [Syntax.ParsePrintRule 
    3.53 @@ -241,19 +239,19 @@
    3.54   
    3.55   (* A1->...->An->R goes to [(A1,B1),...,(An,Bn)] where Bi=Ai->...->An->R 
    3.56      Bi is the Type of the function that is applied to an Ai type argument *)
    3.57 - fun args_of_curried (typ as (Type("->",[S,T]))) = 
    3.58 -      (S,typ) :: args_of_curried T
    3.59 + fun args_of_curried (typ as (Type(name,[S,T]))) = if name = cfun_arrow then
    3.60 +      (S,typ) :: args_of_curried T else []
    3.61     | args_of_curried _ = [];
    3.62  in
    3.63   fun args_of_op true typ = Curried_args(rev(args_of_curried typ))
    3.64 -   | args_of_op false (typ as (Type("->",[S,T]))) = 
    3.65 -      Tupeled_args(args_of_tupel S)
    3.66 +   | args_of_op false (typ as (Type(name,[S,T]))) = if name = cfun_arrow then
    3.67 +      Tupeled_args(args_of_tupel S) else Tupeled_args([])
    3.68     | args_of_op false _ = Tupeled_args([]);
    3.69  end;
    3.70  
    3.71  (* generates for the type t the type of the fapp constant 
    3.72     that will be applied to t *)
    3.73 -fun mk_fapp_typ (typ as Type("->",argl)) = Type("fun",[typ,Type("fun",argl)]) 
    3.74 +fun mk_fapp_typ (typ as Type(_(*"->"*),argl)) = Type("fun",[typ,Type("fun",argl)]) 
    3.75    | mk_fapp_typ t = (
    3.76                      error("Internal error:mk_fapp_typ: wrong argument\n"));
    3.77                      
     4.1 --- a/src/HOLCF/domain/axioms.ML	Mon Oct 27 10:46:36 1997 +0100
     4.2 +++ b/src/HOLCF/domain/axioms.ML	Mon Oct 27 11:34:33 1997 +0100
     4.3 @@ -26,11 +26,12 @@
     4.4    val dc_rep = %%(dname^"_rep");
     4.5    val x_name'= "x";
     4.6    val x_name = idx_name eqs x_name' (n+1);
     4.7 +  val dnam = Sign.base_name dname;
     4.8  
     4.9 - val ax_abs_iso=(dname^"_abs_iso",mk_trp(dc_rep`(dc_abs`%x_name')=== %x_name'));
    4.10 - val ax_rep_iso=(dname^"_rep_iso",mk_trp(dc_abs`(dc_rep`%x_name')=== %x_name'));
    4.11 + val ax_abs_iso=(dnam^"_abs_iso",mk_trp(dc_rep`(dc_abs`%x_name')=== %x_name'));
    4.12 + val ax_rep_iso=(dnam^"_rep_iso",mk_trp(dc_abs`(dc_rep`%x_name')=== %x_name'));
    4.13  
    4.14 -  val ax_when_def = (dname^"_when_def",%%(dname^"_when") == 
    4.15 +  val ax_when_def = (dnam^"_when_def",%%(dname^"_when") == 
    4.16       foldr (uncurry /\ ) (when_funs cons, /\x_name'((when_body cons (fn (x,y) =>
    4.17  				Bound(1+length cons+x-y)))`(dc_rep`Bound 0))));
    4.18  
    4.19 @@ -45,7 +46,7 @@
    4.20       |   inj y i j = %%"sinr"`(inj y (i-1) (j-1));
    4.21    in foldr /\# (args, outer (inj (parms args) m n)) end;
    4.22  
    4.23 -  val ax_copy_def = (dname^"_copy_def", %%(dname^"_copy") == /\"f" (dc_abs oo 
    4.24 +  val ax_copy_def = (dnam^"_copy_def", %%(dname^"_copy") == /\"f" (dc_abs oo 
    4.25  	foldl (op `) (%%(dname^"_when") , 
    4.26  	              mapn (con_def Id true (length cons)) 0 cons)));
    4.27  
    4.28 @@ -72,11 +73,11 @@
    4.29  (* ----- axiom and definitions concerning induction ------------------------- *)
    4.30  
    4.31    fun cproj' T = cproj T (length eqs) n;
    4.32 -  val ax_reach = (dname^"_reach", mk_trp(cproj'(%%"fix"`%%(comp_dname^"_copy"))
    4.33 +  val ax_reach = (dnam^"_reach", mk_trp(cproj'(%%"fix"`%%(comp_dname^"_copy"))
    4.34  					`%x_name === %x_name));
    4.35 -  val ax_take_def = (dname^"_take_def",%%(dname^"_take") == mk_lam("n",cproj'
    4.36 +  val ax_take_def = (dnam^"_take_def",%%(dname^"_take") == mk_lam("n",cproj'
    4.37  		    (%%"iterate" $ Bound 0 $ %%(comp_dname^"_copy") $ %%"UU")));
    4.38 -  val ax_finite_def = (dname^"_finite_def",%%(dname^"_finite") == mk_lam(x_name,
    4.39 +  val ax_finite_def = (dnam^"_finite_def",%%(dname^"_finite") == mk_lam(x_name,
    4.40  	mk_ex("n",(%%(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
    4.41  
    4.42  in [ax_abs_iso, ax_rep_iso, ax_when_def, ax_copy_def] @
    4.43 @@ -87,13 +88,14 @@
    4.44  
    4.45  in (* local *)
    4.46  
    4.47 -fun add_axioms (comp_dname, eqs : eq list) thy' = let
    4.48 +fun add_axioms (comp_dnam, eqs : eq list) thy' = let
    4.49 +  val comp_dname = Sign.full_name (sign_of thy') comp_dnam;
    4.50    val dnames = map (fst o fst) eqs;
    4.51    val x_name = idx_name dnames "x"; 
    4.52    fun copy_app dname = %%(dname^"_copy")`Bound 0;
    4.53 -  val ax_copy_def =(comp_dname^"_copy_def" , %%(comp_dname^"_copy") ==
    4.54 +  val ax_copy_def =(comp_dnam^"_copy_def" , %%(comp_dname^"_copy") ==
    4.55  				    /\"f"(foldr' cpair (map copy_app dnames)));
    4.56 -  val ax_bisim_def=(comp_dname^"_bisim_def",%%(comp_dname^"_bisim")==mk_lam("R",
    4.57 +  val ax_bisim_def=(comp_dnam^"_bisim_def",%%(comp_dname^"_bisim")==mk_lam("R",
    4.58      let
    4.59        fun one_con (con,args) = let
    4.60  	val nonrec_args = filter_out is_rec args;
     5.1 --- a/src/HOLCF/domain/extender.ML	Mon Oct 27 10:46:36 1997 +0100
     5.2 +++ b/src/HOLCF/domain/extender.ML	Mon Oct 27 11:34:33 1997 +0100
     5.3 @@ -16,70 +16,61 @@
     5.4  
     5.5  (* ----- general testing and preprocessing of constructor list -------------- *)
     5.6  
     5.7 -  fun check_and_sort_domain (eqs'':((string * typ list) *
     5.8 -     (string * ThyOps.cmixfix * (bool*string*typ) list) list) list) thy'' = let
     5.9 -    val dtnvs = map fst eqs'';
    5.10 -    val cons' = flat (map snd eqs'');
    5.11 +  fun check_and_sort_domain (dtnvs: (string * typ list) list, cons'' :
    5.12 +     ((string * ThyOps.cmixfix * (bool*string*typ) list) list) list) sg =
    5.13 +  let
    5.14 +    val defaultS = Type.defaultS (tsig_of sg);
    5.15      val test_dupl_typs = (case duplicates (map fst dtnvs) of 
    5.16  	[] => false | dups => error ("Duplicate types: " ^ commas_quote dups));
    5.17 -    val test_dupl_cons = (case duplicates (map first cons') of 
    5.18 -	[] => false | dups => error ("Duplicate constructors: " ^ commas_quote dups));
    5.19 -    val test_dupl_sels = (case duplicates(map second (flat(map third cons'))) of
    5.20 +    val test_dupl_cons = (case duplicates (map first (flat cons'')) of 
    5.21 +	[] => false | dups => error ("Duplicate constructors: " 
    5.22 +							 ^ commas_quote dups));
    5.23 +    val test_dupl_sels = (case duplicates 
    5.24 +			       (map second (flat (map third (flat cons'')))) of
    5.25          [] => false | dups => error("Duplicate selectors: "^commas_quote dups));
    5.26      val test_dupl_tvars = exists(fn s=>case duplicates(map(fst o rep_TFree)s)of
    5.27  	[] => false | dups => error("Duplicate type arguments: " 
    5.28 -							   ^commas_quote dups))
    5.29 -	(map snd dtnvs);
    5.30 -    val default = ["_default"];
    5.31 -    (*test for free type variables, Inconsistent sort constraints,
    5.32 -	       non-pcpo-types and invalid use of recursive type*)
    5.33 -    in map (fn ((dname,typevars),cons') => let
    5.34 -      val tvars = ref (map rep_TFree typevars) : (string * sort) list ref;
    5.35 -      fun newsort (TFree(v,s)) = TFree(v,case assoc_string (!tvars,v) of
    5.36 -		None   => Imposs "extender:newsort"
    5.37 -	      | Some s => if s=default then Type.defaultS(tsig_of thy'') else s)
    5.38 -      |   newsort (Type(s,typl)) = Type(s,map newsort typl)
    5.39 -      |   newsort (TVar _) = Imposs "extender:newsort 2";
    5.40 -      val analyse_cons = forall (fn con' => let
    5.41 -	  val types = map third (third con');
    5.42 -	  fun rm_sorts (TFree(s,_)) = TFree(s,[])
    5.43 -	  |   rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts)
    5.44 -	  |   rm_sorts (TVar(s,_))  = TVar(s,[])
    5.45 -	  and remove_sorts l = map rm_sorts l;
    5.46 -          fun analyse(TFree(v,s)) = (case assoc_string(!tvars,v) of 
    5.47 -			None =>	error ("Free type variable " ^ v ^ " on rhs.")
    5.48 -		      | Some sort => s = default orelse
    5.49 -				     if sort = default 
    5.50 -					then (tvars:= (v,s):: !tvars;true)
    5.51 -					else eq_set_string (s,sort) orelse
    5.52 -					error ("Inconsistent sort constraints "^
    5.53 -					       "for type variable "^quote v))
    5.54 -	    | analyse(Type(s,typl)) = (case assoc_string (dtnvs,s) of 
    5.55 -			None => forall analyse typl
    5.56 -		      | Some tvs => remove_sorts tvs = remove_sorts typl orelse 
    5.57 -		       		    error ("Recursion of type " ^ s ^ 
    5.58 -					   " with different arguments"))
    5.59 -	    | analyse(TVar _) = Imposs "extender:analyse";
    5.60 -	  in forall analyse types end) cons';
    5.61 -      fun check_pcpo t = (pcpo_type thy'' t orelse 
    5.62 -			  error("Not a pcpo type: "^string_of_typ thy'' t); t);
    5.63 -      fun check_type (t as Type(s,typl)) = (case assoc_string (dtnvs,s) of 
    5.64 -			None => check_pcpo t | Some _ => t)
    5.65 -      |   check_type t = check_pcpo t;
    5.66 -      in ((dname,map newsort typevars),
    5.67 -	  map (upd_third (map (upd_third (check_type o newsort)))) cons')
    5.68 -      end) eqs''
    5.69 -    end; (* let *)
    5.70 -  fun check_gen_by thy' (typs': string list,cnstrss': string list list) = let
    5.71 +		   ^commas_quote dups)) (map snd dtnvs);
    5.72 +    (* test for free type variables, illegal sort constraints on rhs,
    5.73 +	       non-pcpo-types and invalid use of recursive type;
    5.74 +       replace sorts in type variables on rhs *)
    5.75 +    fun analyse_equation ((dname,typevars),cons') = 
    5.76 +      let
    5.77 +	val tvars = map rep_TFree typevars;
    5.78 +	fun rm_sorts (TFree(s,_)) = TFree(s,[])
    5.79 +	|   rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts)
    5.80 +	|   rm_sorts (TVar(s,_))  = TVar(s,[])
    5.81 +	and remove_sorts l = map rm_sorts l;
    5.82 +	fun analyse(TFree(v,s)) = (case assoc_string(tvars,v) of 
    5.83 +		    None      => error ("Free type variable " ^ v ^ " on rhs.")
    5.84 +	          | Some sort => if eq_set_string (s,defaultS) orelse
    5.85 +				    eq_set_string (s,sort    ) then TFree(v,sort)
    5.86 +				 else error ("Additional constraint on rhs "^
    5.87 +					     "for type variable "^quote v))
    5.88 +        |    analyse(Type(s,typl)) = (case assoc_string (dtnvs,s) of 
    5.89 +		    None     =>      Type(s,map analyse typl)
    5.90 +	          | Some tvs => if remove_sorts tvs = remove_sorts typl 
    5.91 +				then Type(s,map analyse typl) 
    5.92 +				else error ("Recursion of type " ^ s ^ 
    5.93 +					    " with different arguments"))
    5.94 +        | analyse(TVar _) = Imposs "extender:analyse";
    5.95 +	fun check_pcpo t = (pcpo_type sg t orelse 
    5.96 +			   error("Not a pcpo type: "^string_of_typ sg t); t);
    5.97 +	val analyse_con = upd_third (map (upd_third (check_pcpo o analyse)));
    5.98 +      in ((dname,typevars), map analyse_con cons') end; 
    5.99 +  in ListPair.map analyse_equation (dtnvs,cons'')
   5.100 +  end; (* let *)
   5.101 +
   5.102 +  fun check_gen_by sg' (typs': string list,cnstrss': string list list) = let
   5.103      val test_dupl_typs = (case duplicates typs' of [] => false
   5.104  	  | dups => error ("Duplicate types: " ^ commas_quote dups));
   5.105      val test_dupl_cnstrs = map (fn cs => (case duplicates cs of [] => false 
   5.106  	| ds => error ("Duplicate constructors: " ^ commas_quote ds))) cnstrss';
   5.107 -    val tycons = map fst (#tycons(Type.rep_tsig (tsig_of thy')));
   5.108 +    val tycons = map fst (#tycons(Type.rep_tsig (tsig_of sg')));
   5.109      val test_types = forall (fn t => t mem tycons orelse 
   5.110  				     error("Unknown type: "^t)) typs';
   5.111      val cnstrss = let
   5.112 -	fun type_of c = case (Sign.const_type(sign_of thy') c) of Some t => t
   5.113 +	fun type_of c = case (Sign.const_type sg' c) of Some t => t
   5.114  				| None => error ("Unknown constructor: "^c);
   5.115  	fun args_result_type (t as (Type(tn,[arg,rest]))) = 
   5.116  		if tn = "->" orelse tn = "=>"
   5.117 @@ -95,15 +86,15 @@
   5.118  	  list list end;
   5.119      fun test_equal_type tn (cn,_,(_,rt)) = fst (rep_Type rt) = tn orelse
   5.120  		      error("Inappropriate result type for constructor "^cn);
   5.121 -    val typs = map (fn (tn, cnstrs) => (map (test_equal_type tn) cnstrs; 
   5.122 -				snd(third(hd(cnstrs)))))  (typs'~~cnstrss);
   5.123 -    val test_typs = map (fn (typ,cnstrs) => 
   5.124 -			if not (pcpo_type thy' typ)
   5.125 -			then error("Not a pcpo type: "^string_of_typ thy' typ)
   5.126 +    val typs = ListPair.map (fn (tn, cnstrs) => (map (test_equal_type tn) cnstrs;
   5.127 +				snd(third(hd(cnstrs)))))  (typs',cnstrss);
   5.128 +    val test_typs = ListPair.map (fn (typ,cnstrs) => 
   5.129 +			if not (pcpo_type sg' typ)
   5.130 +			then error("Not a pcpo type: "^string_of_typ sg' typ)
   5.131  			else map (fn (cn,_,(_,rt)) => rt=typ orelse error(
   5.132  				"Non-identical result types for constructors "^
   5.133  			        first(hd cnstrs)^" and "^ cn ))  cnstrs)
   5.134 -		    (typs~~cnstrss);
   5.135 +		    (typs,cnstrss);
   5.136      val proper_args = let
   5.137  	fun occurs tn (Type(tn',ts)) = (tn'=tn) orelse exists (occurs tn) ts
   5.138  	|   occurs _  _              = false;
   5.139 @@ -120,23 +111,34 @@
   5.140  
   5.141  in
   5.142  
   5.143 -  fun add_domain (comp_dname,eqs'') thy'' = let
   5.144 -    val eqs' = check_and_sort_domain eqs'' thy'';
   5.145 -    val thy' = thy'' |> Domain_Syntax.add_syntax (comp_dname,eqs');
   5.146 +  fun add_domain (comp_dnam,eqs''') thy''' = let
   5.147 +    val sg''' = sign_of thy''';
   5.148 +    val dtnvs = map ((fn (dname,vs) => 
   5.149 +			 (Sign.full_name sg''' dname,map (str2typ sg''') vs))
   5.150 +                   o fst) eqs''';
   5.151 +    val cons''' = map snd eqs''';
   5.152 +    fun thy_type  (dname,tvars)  = (Sign.base_name dname, length tvars, NoSyn);
   5.153 +    fun thy_arity (dname,tvars)  = (dname, map (snd o rep_TFree) tvars, pcpoS);
   5.154 +    val thy'' = thy''' |> Theory.add_types     (map thy_type  dtnvs)
   5.155 +		       |> Theory.add_arities_i (map thy_arity dtnvs);
   5.156 +    val sg'' = sign_of thy'';
   5.157 +    val cons''=map (map (upd_third (map (upd_third (str2typ sg''))))) cons''';
   5.158 +    val eqs' = check_and_sort_domain (dtnvs,cons'') sg'';
   5.159 +    val thy' = thy'' |> Domain_Syntax.add_syntax (comp_dnam,eqs');
   5.160      val dts  = map (Type o fst) eqs';
   5.161      fun cons cons' = (map (fn (con,syn,args) =>
   5.162 -	(ThyOps.const_name con syn,
   5.163 -	 map (fn ((lazy,sel,tp),vn) => ((lazy,
   5.164 +	((ThyOps.const_name con syn),
   5.165 +	 ListPair.map (fn ((lazy,sel,tp),vn) => ((lazy,
   5.166  					 find (tp,dts) handle LIST "find" => ~1),
   5.167  					sel,vn))
   5.168 -	     (args~~(mk_var_names(map third args)))
   5.169 +	     (args,(mk_var_names(map third args)))
   5.170  	 )) cons') : cons list;
   5.171      val eqs = map (fn (dtnvs,cons') => (dtnvs,cons cons')) eqs' : eq list;
   5.172 -    val thy         = thy' |> Domain_Axioms.add_axioms (comp_dname,eqs);
   5.173 +    val thy         = thy' |> Domain_Axioms.add_axioms (comp_dnam,eqs);
   5.174    in (thy,eqs) end;
   5.175  
   5.176    fun add_gen_by ((tname,finite),(typs',cnstrss')) thy' = let
   5.177 -   val (typs,cnstrs) = check_gen_by thy' (typs',cnstrss');
   5.178 +   val (typs,cnstrs) = check_gen_by (sign_of thy') (typs',cnstrss');
   5.179    in
   5.180     Domain_Axioms.add_induct ((tname,finite),(typs,cnstrs)) thy' end;
   5.181  
     6.1 --- a/src/HOLCF/domain/interface.ML	Mon Oct 27 10:46:36 1997 +0100
     6.2 +++ b/src/HOLCF/domain/interface.ML	Mon Oct 27 11:34:33 1997 +0100
     6.3 @@ -40,45 +40,36 @@
     6.4        (if num > 1 then "val rews = " ^rews1 ^";\n" else "")
     6.5      end;
     6.6  
     6.7 -  fun mk_domain (eqs'') = let
     6.8 -    val dtnvs  = map (rep_Type o fst) eqs'';
     6.9 +  fun mk_domain eqs'' = let
    6.10 +    val num    = length eqs'';
    6.11 +    val dtnvs  = map fst eqs'';
    6.12      val dnames = map fst dtnvs;
    6.13 -    val num = length dnames;
    6.14      val comp_dname = implode (separate "_" dnames);
    6.15      val conss' = ListPair.map 
    6.16 -	(fn (dname,cons'') =>
    6.17 -	  let fun sel n m = upd_second 
    6.18 +	(fn (dname,cons'') => let fun sel n m = upd_second 
    6.19  			      (fn None   => dname^"_sel_"^(string_of_int n)^
    6.20 -						 "_"^(string_of_int m)
    6.21 +						      "_"^(string_of_int m)
    6.22  				| Some s => s)
    6.23  	      fun fill_sels n con = upd_third (mapn (sel n) 1) con;
    6.24  	  in mapn fill_sels 1 cons'' end)
    6.25 -	(dnames, map #2 eqs'');
    6.26 +	(dnames, map snd eqs'');
    6.27      val eqs' = dtnvs~~conss';
    6.28  
    6.29  (* ----- string for calling add_domain -------------------------------------- *)
    6.30  
    6.31      val thy_ext_string = let
    6.32 -      fun mk_tnv (n,v) = mk_pair (quote n, mk_list (map mk_typ v))
    6.33 -      and mk_typ (TFree(name,sort))= "TFree" ^ 
    6.34 -			 mk_pair (quote name, mk_list (map quote sort))
    6.35 -      |   mk_typ (Type (name,args))= "Type" ^mk_tnv(name,args)
    6.36 -      |   mk_typ _                 = Imposs "interface:mk_typ";
    6.37        fun mk_conslist cons' = 
    6.38 -	  mk_list (map 
    6.39 -		   (fn (c,syn,ts)=>
    6.40 -		    mk_triple(quote c, syn, 
    6.41 -			      mk_list
    6.42 -			      (map (fn (b,s ,tp) =>
    6.43 -				    mk_triple(Bool.toString b, quote s,
    6.44 -					      mk_typ tp)) ts))) cons');
    6.45 +	  mk_list (map (fn (c,syn,ts)=>
    6.46 +		    mk_triple(quote c, syn, mk_list (map (fn (b,s ,tp) =>
    6.47 +		    mk_triple(Bool.toString b, quote s, tp)) ts))) cons');
    6.48      in "val (thy, "^comp_dname^"_equations) = thy |> Domain_Extender.add_domain \n"
    6.49 -       ^ mk_pair(quote comp_dname,
    6.50 -		 mk_list(map (fn (t,cs)=> mk_pair (mk_tnv t,mk_conslist cs)) eqs'))
    6.51 +       ^ mk_pair(quote comp_dname, mk_list(map (fn ((n,vs),cs) => 
    6.52 +				   mk_pair (mk_pair (quote n, mk_list vs), 
    6.53 +					    mk_conslist cs)) eqs'))
    6.54         ^ ";\nval thy = thy"
    6.55      end;
    6.56  
    6.57 -(* ----- string for calling (comp_)theorems and producing the structures ---------- *)
    6.58 +(* ----- string for calling (comp_)theorems and producing the structures ---- *)
    6.59  
    6.60      val val_gen_string =  let
    6.61        fun plural s = if num > 1 then s^"s" else "["^s^"]";
    6.62 @@ -126,29 +117,29 @@
    6.63  
    6.64    val name' = name >> strip_quotes;
    6.65    val type_var' = type_var >> strip_quotes;
    6.66 -  val sort = name' >> (fn s => [s])
    6.67 -	  || "{" $$-- !! (list name' --$$ "}");
    6.68 -  val tvar = (type_var' --(optional("::" $$-- !! sort)["_default"])) >>TFree;
    6.69 -(*val tvar = type_var >> (fn tv => TFree(strip_quotes tv,["pcpo"]));*)
    6.70 -  fun type_args l = ("(" $$-- !! (list1 typ --$$ ")")
    6.71 -	         || tvar  >> (fn x => [x])
    6.72 -	         || empty >> K []) l
    6.73 -  and con_typ l   = (type_args -- name' >> (fn (x,y) => Type(y,x))) l
    6.74 -			(* here ident may be used instead of name' 
    6.75 -			   to avoid ambiguity with standard mixfix option *)
    6.76 -  and typ l       = (con_typ 
    6.77 -		   || tvar) l;
    6.78 +  fun esc_quote s = let fun esc [] = []
    6.79 +			|   esc ("\""::xs) = esc xs
    6.80 +			|   esc ("[" ::xs) = "{"::esc xs
    6.81 +			|   esc ("]" ::xs) = "}"::esc xs
    6.82 +			|   esc (x   ::xs) = x  ::esc xs
    6.83 +		    in implode (esc (explode s)) end;
    6.84 +  val tvar = (type_var' ^^ optional ($$ "::" ^^ (sort >> esc_quote)) "") >> quote;
    6.85 +  fun type_args l = (tvar >> (fn x => [x])
    6.86 +                 ||  "(" $$-- !! (list1 tvar --$$ ")")
    6.87 +                 ||  empty >> K []) l
    6.88 +  fun con_typ l   = (type_args -- name' >> (fn (x,y) => (y,x))) l
    6.89 +                      (* here ident may be used instead of name' 
    6.90 +                         to avoid ambiguity with standard mixfix option *)
    6.91    val domain_arg  = "(" $$-- (optional ($$ "lazy" >> K true) false)
    6.92  			  -- (optional ((name' >> Some) --$$ "::") None)
    6.93  			  -- typ --$$ ")" >> (fn ((lazy,sel),tp) => (lazy,sel,tp))
    6.94 -		 || name' >> (fn x => (false,None,Type(x,[]))) 
    6.95 -		 || tvar  >> (fn x => (false,None,x));
    6.96 +		 || typ >> (fn x => (false,None,x)) 
    6.97    val domain_cons = name' -- !! (repeat domain_arg) 
    6.98  		    -- ThyOps.opt_cmixfix
    6.99  		    >> (fn ((con,args),syn) => (con,syn,args));
   6.100  in
   6.101    val domain_decl = (enum1 "," (con_typ --$$ "="  -- !! 
   6.102 -			       (enum1 "|" domain_cons))) 	    >> mk_domain;
   6.103 +			       (enum1 "|" domain_cons))) >> mk_domain;
   6.104    val gen_by_decl = (optional ($$ "finite" >> K true) false) -- 
   6.105  		    (enum1 "," (name'   --$$ "by" -- !!
   6.106  			       (enum1 "|" name'))) >> mk_gen_by;
     7.1 --- a/src/HOLCF/domain/library.ML	Mon Oct 27 10:46:36 1997 +0100
     7.2 +++ b/src/HOLCF/domain/library.ML	Mon Oct 27 11:34:33 1997 +0100
     7.3 @@ -60,9 +60,9 @@
     7.4     forbidding "o", "x..","f..","P.." as names *)
     7.5  (* a number string is added if necessary *)
     7.6  fun mk_var_names types : string list = let
     7.7 -    fun typid (Type  (id,_)   ) = hd     (explode id)
     7.8 -      | typid (TFree (id,_)   ) = hd (tl (explode id))
     7.9 -      | typid (TVar ((id,_),_)) = hd (tl (explode id));
    7.10 +    fun typid (Type  (id,_)   ) = hd     (explode (Sign.base_name id))
    7.11 +      | typid (TFree (id,_)   ) = hd (tl (explode (Sign.base_name id)))
    7.12 +      | typid (TVar ((id,_),_)) = hd (tl (explode (Sign.base_name id)));
    7.13      fun nonreserved s = if s mem ["x","f","P"] then s^"'" else s;
    7.14      fun index_vnames(vn::vns,occupied) =
    7.15            (case assoc(occupied,vn) of
    7.16 @@ -76,11 +76,12 @@
    7.17  
    7.18  fun rep_Type  (Type  x) = x | rep_Type  _ = Imposs "library:rep_Type";
    7.19  fun rep_TFree (TFree x) = x | rep_TFree _ = Imposs "library:rep_TFree";
    7.20 -val tsig_of = #tsig o Sign.rep_sg o sign_of;
    7.21 -fun pcpo_type thy t = Type.of_sort (tsig_of thy) 
    7.22 -			(Sign.certify_typ (sign_of thy) t,["pcpo"]);
    7.23 -fun string_of_typ thy t = let val sg = sign_of thy in
    7.24 -			  Sign.string_of_typ sg (Sign.certify_typ sg t) end;
    7.25 +val tsig_of = #tsig o Sign.rep_sg;
    7.26 +val HOLCF_sg = sign_of HOLCF.thy;
    7.27 +val pcpoS = Sign.intern_sort HOLCF_sg ["pcpo"];
    7.28 +fun pcpo_type sg t = Type.of_sort (tsig_of sg) (Sign.certify_typ sg t, pcpoS);
    7.29 +fun string_of_typ sg = Sign.string_of_typ sg o Sign.certify_typ sg;
    7.30 +fun str2typ sg = typ_of o read_ctyp sg;
    7.31  
    7.32  (* ----- constructor list handling ----- *)
    7.33  
    7.34 @@ -105,8 +106,8 @@
    7.35  
    7.36  (* ----- support for type and mixfix expressions ----- *)
    7.37  
    7.38 -fun mk_tvar s = TFree("'"^s,["pcpo"]);
    7.39 -fun mk_typ t (S,T) = Type(t,[S,T]);
    7.40 +fun mk_tvar s = TFree("'"^s,pcpoS);
    7.41 +fun mk_typ t (S,T) = Sign.intern_typ HOLCF_sg (Type(t,[S,T]));
    7.42  infixr 5 -->;
    7.43  infixr 6 ~>; val op ~> = mk_typ "->";
    7.44  val NoSyn' = ThyOps.Mixfix NoSyn;
     8.1 --- a/src/HOLCF/domain/syntax.ML	Mon Oct 27 10:46:36 1997 +0100
     8.2 +++ b/src/HOLCF/domain/syntax.ML	Mon Oct 27 11:34:33 1997 +0100
     8.3 @@ -26,11 +26,12 @@
     8.4  in
     8.5    val dtype  = Type(dname,typevars);
     8.6    val dtype2 = foldr' (mk_typ "++") (map prod cons');
     8.7 -  val const_rep  = (dname^"_rep" ,              dtype  ~> dtype2, NoSyn');
     8.8 -  val const_abs  = (dname^"_abs" ,              dtype2 ~> dtype , NoSyn');
     8.9 -  val const_when = (dname^"_when", foldr (op ~>) ((map when_type cons'),
    8.10 -						 dtype ~> freetvar "t"), NoSyn');
    8.11 -  val const_copy = (dname^"_copy", dtypeprod ~> dtype  ~> dtype , NoSyn');
    8.12 +  val dnam = Sign.base_name dname;
    8.13 +  val const_rep  = (dnam^"_rep" ,              dtype  ~> dtype2, NoSyn');
    8.14 +  val const_abs  = (dnam^"_abs" ,              dtype2 ~> dtype , NoSyn');
    8.15 +  val const_when = (dnam^"_when", foldr (op ~>) ((map when_type cons'),
    8.16 +					       	 dtype ~> freetvar "t"), NoSyn');
    8.17 +  val const_copy = (dnam^"_copy", dtypeprod ~> dtype  ~> dtype , NoSyn');
    8.18  end;
    8.19  
    8.20  (* ----- constants concerning the constructors, discriminators and selectors ------ *)
    8.21 @@ -60,8 +61,8 @@
    8.22  
    8.23  (* ----- constants concerning induction ------------------------------------------- *)
    8.24  
    8.25 -  val const_take   = (dname^"_take"  , Type("nat",[]) --> dtype ~> dtype, NoSyn');
    8.26 -  val const_finite = (dname^"_finite", dtype-->HOLogic.boolT	        , NoSyn');
    8.27 +  val const_take   = (dnam^"_take"  , Type("nat",[]) --> dtype ~> dtype, NoSyn');
    8.28 +  val const_finite = (dnam^"_finite", dtype-->HOLogic.boolT	        , NoSyn');
    8.29  
    8.30  (* ----- case translation --------------------------------------------------------- *)
    8.31  
    8.32 @@ -86,7 +87,7 @@
    8.33  				 (mapn case1 1 cons')],
    8.34         mk_appl (Constant "@fapp") [foldl 
    8.35  				 (fn (w,a ) => mk_appl (Constant "@fapp" ) [w,a ])
    8.36 -				 (Constant (dname^"_when"),mapn arg1 1 cons'),
    8.37 +				 (Constant (dnam^"_when"),mapn arg1 1 cons'),
    8.38  				 Variable "x"])
    8.39    end;
    8.40  end;
    8.41 @@ -101,23 +102,17 @@
    8.42  
    8.43  in (* local *)
    8.44  
    8.45 -fun add_syntax (comp_dname,eqs': ((string * typ list) *
    8.46 +fun add_syntax (comp_dnam,eqs': ((string * typ list) *
    8.47  		(string * ThyOps.cmixfix * (bool*string*typ) list) list) list) thy'' =
    8.48  let
    8.49 -  fun thy_type  (dname,tvars)  = (dname, length tvars, NoSyn);
    8.50 -  fun thy_arity (dname,tvars)  = (dname, map (snd o rep_TFree) tvars, ["pcpo"]);
    8.51 -  val thy_types   = map (thy_type  o fst) eqs';
    8.52 -  val thy_arities = map (thy_arity o fst) eqs';
    8.53 -  val dtypes      = map (Type      o fst) eqs';
    8.54 +  val dtypes  = map (Type      o fst) eqs';
    8.55    val funprod = foldr' (mk_typ "*") (map (fn tp => tp ~> tp                  )dtypes);
    8.56    val relprod = foldr' (mk_typ "*") (map (fn tp => tp--> tp --> HOLogic.boolT)dtypes);
    8.57 -  val const_copy   = (comp_dname^"_copy"  ,funprod ~> funprod       , NoSyn');
    8.58 -  val const_bisim  = (comp_dname^"_bisim" ,relprod --> HOLogic.boolT, NoSyn');
    8.59 +  val const_copy   = (comp_dnam^"_copy"  ,funprod ~> funprod       , NoSyn');
    8.60 +  val const_bisim  = (comp_dnam^"_bisim" ,relprod --> HOLogic.boolT, NoSyn');
    8.61    val ctt           = map (calc_syntax funprod) eqs';
    8.62    val add_cur_ops_i = ThyOps.add_ops_i {curried=true, strict=false, total=false};
    8.63 -in thy'' |> Theory.add_types      thy_types
    8.64 -	 |> Theory.add_arities_i  thy_arities
    8.65 -	 |> add_cur_ops_i (flat(map fst ctt))
    8.66 +in thy'' |> add_cur_ops_i (flat(map fst ctt))
    8.67  	 |> add_cur_ops_i ((if length eqs'>1 then [const_copy] else[])@[const_bisim])
    8.68  	 |> Theory.add_trrules_i (flat(map snd ctt))
    8.69  end; (* let *)
     9.1 --- a/src/HOLCF/domain/theorems.ML	Mon Oct 27 10:46:36 1997 +0100
     9.2 +++ b/src/HOLCF/domain/theorems.ML	Mon Oct 27 11:34:33 1997 +0100
     9.3 @@ -62,7 +62,7 @@
     9.4  fun theorems thy (((dname,_),cons) : eq, eqs :eq list) =
     9.5  let
     9.6  
     9.7 -val dummy = writeln ("Proving isomorphism properties of domain "^dname^"...");
     9.8 +val dummy = writeln ("Proving isomorphism   properties of domain "^dname^"...");
     9.9  val pg = pg' thy;
    9.10  (*
    9.11  infixr 0 y;
    9.12 @@ -328,15 +328,16 @@
    9.13  end; (* let *)
    9.14  
    9.15  
    9.16 -fun comp_theorems thy (comp_dname, eqs: eq list, casess, con_rews, copy_rews) =
    9.17 +fun comp_theorems thy (comp_dnam, eqs: eq list, casess, con_rews, copy_rews) =
    9.18  let
    9.19  
    9.20 +val dnames = map (fst o fst) eqs;
    9.21 +val conss  = map  snd        eqs;
    9.22 +val comp_dname = Sign.full_name (sign_of thy) comp_dnam;
    9.23 +
    9.24  val dummy = writeln("Proving induction properties of domain "^comp_dname^"...");
    9.25  val pg = pg' thy;
    9.26  
    9.27 -val dnames = map (fst o fst) eqs;
    9.28 -val conss  = map  snd        eqs;
    9.29 -
    9.30  (* ----- getting the composite axiom and definitions ------------------------ *)
    9.31  
    9.32  local val ga = get_axiom thy in