--- a/src/HOLCF/ROOT.ML Mon Oct 27 10:46:36 1997 +0100
+++ b/src/HOLCF/ROOT.ML Mon Oct 27 11:34:33 1997 +0100
@@ -16,7 +16,6 @@
use_thy "HOLCF";
-
(* sections axioms, ops *)
use "ax_ops/holcflogic.ML";
@@ -24,7 +23,6 @@
use "ax_ops/thy_ops.ML";
use "ax_ops/thy_syntax.ML";
-
(* sections domain, generated *)
use "domain/library.ML";
@@ -34,7 +32,6 @@
use "domain/extender.ML";
use "domain/interface.ML";
-
print_depth 10;
val HOLCF_build_completed = (); (*indicate successful build*)
--- a/src/HOLCF/ax_ops/holcflogic.ML Mon Oct 27 10:46:36 1997 +0100
+++ b/src/HOLCF/ax_ops/holcflogic.ML Mon Oct 27 11:34:33 1997 +0100
@@ -20,6 +20,7 @@
val mkNotEqUU : term -> term; (* Trueprop(x ~= UU) *)
val mkNotEqUU_in : term -> term -> term; (* "v~=UU ==> t" *)
val ==> : typ * typ -> typ; (* Infix operation typ constructor *)
+ val cfun_arrow : string (* internalized "->" *)
val mkOpApp : term -> term -> term; (* Ops application (f ` x) *)
val mkCPair : term -> term -> term; (* cpair constructor *)
end;
@@ -44,12 +45,16 @@
fun mkNotEqUU_in vterm term =
mk_implies(mkNotEqUU vterm,term)
+val HOLCF_sg = sign_of HOLCF.thy;
+fun mk_typ t (S,T) = Sign.intern_typ HOLCF_sg (Type(t,[S,T]));
+fun rep_Type (Type x) = x| rep_Type _ = error "Internal error: rep_Type";
infixr 6 ==>; (* the analogon to --> for operations *)
-fun a ==> b = Type("->",[a,b]);
+val op ==> = mk_typ "->";
+val cfun_arrow = fst (rep_Type (dummyT ==> dummyT));
(* Ops application (f ` x) *)
-fun mkOpApp (f as Const(_,ft as Type("->",[xt,rt]))) x =
+fun mkOpApp (f as Const(_,ft as Type(_(*"->"*),[xt,rt]))) x =
Const("fapp",ft --> xt --> rt) $ f $ x
| mkOpApp f x = (error("Internal error: mkOpApp: wrong args"));
--- a/src/HOLCF/ax_ops/thy_ops.ML Mon Oct 27 10:46:36 1997 +0100
+++ b/src/HOLCF/ax_ops/thy_ops.ML Mon Oct 27 11:34:33 1997 +0100
@@ -106,14 +106,13 @@
(* Changing a->b->c res. a*b->c to a=>b=>c. Called by syn_decls. *)
(*####*)
-fun op_to_fun true sign (Type("->" ,[larg,t]))=
- Type("fun",[larg,op_to_fun true sign t])
- | op_to_fun false sign (Type("->",[args,res])) = let
+fun op_to_fun true sign (ty as Type(name ,[larg,t]))= if name = cfun_arrow
+ then Type("fun",[larg,op_to_fun true sign t]) else ty
+ | op_to_fun false sign (ty as Type(name,[args,res])) = let
fun otf (Type("*",[larg,rargs])) = Type("fun",[larg,otf rargs])
| otf t = Type("fun",[t,res]);
- in otf args end
- | op_to_fun _ sign t = t(*error("Wrong type for cinfix/cmixfix : "^
- (Sign.string_of_typ sign t))*);
+ in if name = cfun_arrow then otf args else ty end
+ | op_to_fun _ sign t = t;
(*####*)
(* oldstyle is called by add_ext_axioms(_i) *)
@@ -140,9 +139,6 @@
(name,op_to_fun curried sign typ,Mixfix.Infixr(i))::
(syn_decls curried sign tl)
| syn_decls curried sign ((name,typ,CMixfix(x))::tl) =
-(*####
- ("@"^name,op_to_fun curried sign typ,Mixfix.Mixfix(x))::
-####**)
(name,op_to_fun curried sign typ,Mixfix.Mixfix(x))::
(syn_decls curried sign tl)
@@ -170,7 +166,8 @@
::xrules_of true tail
(*####*)
| xrules_of true ((name,typ,CMixfix(_))::tail) =
- let fun argnames n (Type("->" ,[_,t]))= chr n :: argnames (n+1) t
+ let fun argnames n (Type(name ,[_,t]))= if name = cfun_arrow then
+ chr n :: argnames (n+1) t else []
| argnames _ _ = [];
val names = argnames (ord"A") typ;
in if names = [] then [] else
@@ -200,7 +197,8 @@
in itr l end;
fun argnames n (Type("*" ,[_,t]))= chr n :: argnames (n+1) t
| argnames n _ = [chr n];
- val vars = map Variable (case typ of (Type("->" ,[t,_])) =>argnames (ord"A") t
+ val vars = map Variable (case typ of (Type(name ,[t,_])) =>
+ if name = cfun_arrow then argnames (ord"A") t else []
| _ => []);
in if vars = [] then [] else
[Syntax.ParsePrintRule
@@ -241,19 +239,19 @@
(* A1->...->An->R goes to [(A1,B1),...,(An,Bn)] where Bi=Ai->...->An->R
Bi is the Type of the function that is applied to an Ai type argument *)
- fun args_of_curried (typ as (Type("->",[S,T]))) =
- (S,typ) :: args_of_curried T
+ fun args_of_curried (typ as (Type(name,[S,T]))) = if name = cfun_arrow then
+ (S,typ) :: args_of_curried T else []
| args_of_curried _ = [];
in
fun args_of_op true typ = Curried_args(rev(args_of_curried typ))
- | args_of_op false (typ as (Type("->",[S,T]))) =
- Tupeled_args(args_of_tupel S)
+ | args_of_op false (typ as (Type(name,[S,T]))) = if name = cfun_arrow then
+ Tupeled_args(args_of_tupel S) else Tupeled_args([])
| args_of_op false _ = Tupeled_args([]);
end;
(* generates for the type t the type of the fapp constant
that will be applied to t *)
-fun mk_fapp_typ (typ as Type("->",argl)) = Type("fun",[typ,Type("fun",argl)])
+fun mk_fapp_typ (typ as Type(_(*"->"*),argl)) = Type("fun",[typ,Type("fun",argl)])
| mk_fapp_typ t = (
error("Internal error:mk_fapp_typ: wrong argument\n"));
--- a/src/HOLCF/domain/axioms.ML Mon Oct 27 10:46:36 1997 +0100
+++ b/src/HOLCF/domain/axioms.ML Mon Oct 27 11:34:33 1997 +0100
@@ -26,11 +26,12 @@
val dc_rep = %%(dname^"_rep");
val x_name'= "x";
val x_name = idx_name eqs x_name' (n+1);
+ val dnam = Sign.base_name dname;
- val ax_abs_iso=(dname^"_abs_iso",mk_trp(dc_rep`(dc_abs`%x_name')=== %x_name'));
- val ax_rep_iso=(dname^"_rep_iso",mk_trp(dc_abs`(dc_rep`%x_name')=== %x_name'));
+ val ax_abs_iso=(dnam^"_abs_iso",mk_trp(dc_rep`(dc_abs`%x_name')=== %x_name'));
+ val ax_rep_iso=(dnam^"_rep_iso",mk_trp(dc_abs`(dc_rep`%x_name')=== %x_name'));
- val ax_when_def = (dname^"_when_def",%%(dname^"_when") ==
+ val ax_when_def = (dnam^"_when_def",%%(dname^"_when") ==
foldr (uncurry /\ ) (when_funs cons, /\x_name'((when_body cons (fn (x,y) =>
Bound(1+length cons+x-y)))`(dc_rep`Bound 0))));
@@ -45,7 +46,7 @@
| inj y i j = %%"sinr"`(inj y (i-1) (j-1));
in foldr /\# (args, outer (inj (parms args) m n)) end;
- val ax_copy_def = (dname^"_copy_def", %%(dname^"_copy") == /\"f" (dc_abs oo
+ val ax_copy_def = (dnam^"_copy_def", %%(dname^"_copy") == /\"f" (dc_abs oo
foldl (op `) (%%(dname^"_when") ,
mapn (con_def Id true (length cons)) 0 cons)));
@@ -72,11 +73,11 @@
(* ----- axiom and definitions concerning induction ------------------------- *)
fun cproj' T = cproj T (length eqs) n;
- val ax_reach = (dname^"_reach", mk_trp(cproj'(%%"fix"`%%(comp_dname^"_copy"))
+ val ax_reach = (dnam^"_reach", mk_trp(cproj'(%%"fix"`%%(comp_dname^"_copy"))
`%x_name === %x_name));
- val ax_take_def = (dname^"_take_def",%%(dname^"_take") == mk_lam("n",cproj'
+ val ax_take_def = (dnam^"_take_def",%%(dname^"_take") == mk_lam("n",cproj'
(%%"iterate" $ Bound 0 $ %%(comp_dname^"_copy") $ %%"UU")));
- val ax_finite_def = (dname^"_finite_def",%%(dname^"_finite") == mk_lam(x_name,
+ val ax_finite_def = (dnam^"_finite_def",%%(dname^"_finite") == mk_lam(x_name,
mk_ex("n",(%%(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
in [ax_abs_iso, ax_rep_iso, ax_when_def, ax_copy_def] @
@@ -87,13 +88,14 @@
in (* local *)
-fun add_axioms (comp_dname, eqs : eq list) thy' = let
+fun add_axioms (comp_dnam, eqs : eq list) thy' = let
+ val comp_dname = Sign.full_name (sign_of thy') comp_dnam;
val dnames = map (fst o fst) eqs;
val x_name = idx_name dnames "x";
fun copy_app dname = %%(dname^"_copy")`Bound 0;
- val ax_copy_def =(comp_dname^"_copy_def" , %%(comp_dname^"_copy") ==
+ val ax_copy_def =(comp_dnam^"_copy_def" , %%(comp_dname^"_copy") ==
/\"f"(foldr' cpair (map copy_app dnames)));
- val ax_bisim_def=(comp_dname^"_bisim_def",%%(comp_dname^"_bisim")==mk_lam("R",
+ val ax_bisim_def=(comp_dnam^"_bisim_def",%%(comp_dname^"_bisim")==mk_lam("R",
let
fun one_con (con,args) = let
val nonrec_args = filter_out is_rec args;
--- a/src/HOLCF/domain/extender.ML Mon Oct 27 10:46:36 1997 +0100
+++ b/src/HOLCF/domain/extender.ML Mon Oct 27 11:34:33 1997 +0100
@@ -16,70 +16,61 @@
(* ----- general testing and preprocessing of constructor list -------------- *)
- fun check_and_sort_domain (eqs'':((string * typ list) *
- (string * ThyOps.cmixfix * (bool*string*typ) list) list) list) thy'' = let
- val dtnvs = map fst eqs'';
- val cons' = flat (map snd eqs'');
+ fun check_and_sort_domain (dtnvs: (string * typ list) list, cons'' :
+ ((string * ThyOps.cmixfix * (bool*string*typ) list) list) list) sg =
+ let
+ val defaultS = Type.defaultS (tsig_of sg);
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
+ val test_dupl_cons = (case duplicates (map first (flat cons'')) of
+ [] => false | dups => error ("Duplicate constructors: "
+ ^ commas_quote dups));
+ val test_dupl_sels = (case duplicates
+ (map second (flat (map third (flat cons'')))) of
[] => false | dups => error("Duplicate selectors: "^commas_quote dups));
val test_dupl_tvars = exists(fn s=>case duplicates(map(fst o rep_TFree)s)of
[] => false | dups => error("Duplicate type arguments: "
- ^commas_quote dups))
- (map snd dtnvs);
- val default = ["_default"];
- (*test for free type variables, Inconsistent sort constraints,
- non-pcpo-types and invalid use of recursive type*)
- in map (fn ((dname,typevars),cons') => let
- val tvars = ref (map rep_TFree typevars) : (string * sort) list ref;
- fun newsort (TFree(v,s)) = TFree(v,case assoc_string (!tvars,v) of
- None => Imposs "extender:newsort"
- | Some s => if s=default then Type.defaultS(tsig_of thy'') else s)
- | newsort (Type(s,typl)) = Type(s,map newsort typl)
- | newsort (TVar _) = Imposs "extender:newsort 2";
- val analyse_cons = forall (fn con' => let
- val types = map third (third con');
- fun rm_sorts (TFree(s,_)) = TFree(s,[])
- | rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts)
- | rm_sorts (TVar(s,_)) = TVar(s,[])
- and remove_sorts l = map rm_sorts l;
- fun analyse(TFree(v,s)) = (case assoc_string(!tvars,v) of
- None => error ("Free type variable " ^ v ^ " on rhs.")
- | Some sort => s = default orelse
- if sort = default
- then (tvars:= (v,s):: !tvars;true)
- else eq_set_string (s,sort) orelse
- error ("Inconsistent sort constraints "^
- "for type variable "^quote v))
- | analyse(Type(s,typl)) = (case assoc_string (dtnvs,s) of
- None => forall analyse typl
- | Some tvs => remove_sorts tvs = remove_sorts typl orelse
- error ("Recursion of type " ^ s ^
- " with different arguments"))
- | analyse(TVar _) = Imposs "extender:analyse";
- in forall analyse types end) cons';
- fun check_pcpo t = (pcpo_type thy'' t orelse
- error("Not a pcpo type: "^string_of_typ thy'' t); t);
- fun check_type (t as Type(s,typl)) = (case assoc_string (dtnvs,s) of
- None => check_pcpo t | Some _ => t)
- | check_type t = check_pcpo t;
- in ((dname,map newsort typevars),
- map (upd_third (map (upd_third (check_type o newsort)))) cons')
- end) eqs''
- end; (* let *)
- fun check_gen_by thy' (typs': string list,cnstrss': string list list) = let
+ ^commas_quote dups)) (map snd dtnvs);
+ (* test for free type variables, illegal sort constraints on rhs,
+ non-pcpo-types and invalid use of recursive type;
+ replace sorts in type variables on rhs *)
+ fun analyse_equation ((dname,typevars),cons') =
+ let
+ val tvars = map rep_TFree typevars;
+ fun rm_sorts (TFree(s,_)) = TFree(s,[])
+ | rm_sorts (Type(s,ts)) = Type(s,remove_sorts ts)
+ | rm_sorts (TVar(s,_)) = TVar(s,[])
+ and remove_sorts l = map rm_sorts l;
+ fun analyse(TFree(v,s)) = (case assoc_string(tvars,v) of
+ None => error ("Free type variable " ^ v ^ " on rhs.")
+ | Some sort => if eq_set_string (s,defaultS) orelse
+ eq_set_string (s,sort ) then TFree(v,sort)
+ else error ("Additional constraint on rhs "^
+ "for type variable "^quote v))
+ | analyse(Type(s,typl)) = (case assoc_string (dtnvs,s) of
+ None => Type(s,map analyse typl)
+ | Some tvs => if remove_sorts tvs = remove_sorts typl
+ then Type(s,map analyse typl)
+ else error ("Recursion of type " ^ s ^
+ " with different arguments"))
+ | analyse(TVar _) = Imposs "extender:analyse";
+ fun check_pcpo t = (pcpo_type sg t orelse
+ error("Not a pcpo type: "^string_of_typ sg t); t);
+ val analyse_con = upd_third (map (upd_third (check_pcpo o analyse)));
+ in ((dname,typevars), map analyse_con cons') end;
+ in ListPair.map analyse_equation (dtnvs,cons'')
+ end; (* let *)
+
+ fun check_gen_by sg' (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 cs => (case duplicates cs of [] => false
| ds => error ("Duplicate constructors: " ^ commas_quote ds))) cnstrss';
- val tycons = map fst (#tycons(Type.rep_tsig (tsig_of thy')));
+ val tycons = map fst (#tycons(Type.rep_tsig (tsig_of sg')));
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
+ fun type_of c = case (Sign.const_type sg' c) of Some t => t
| None => error ("Unknown constructor: "^c);
fun args_result_type (t as (Type(tn,[arg,rest]))) =
if tn = "->" orelse tn = "=>"
@@ -95,15 +86,15 @@
list list end;
fun test_equal_type tn (cn,_,(_,rt)) = fst (rep_Type 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 (pcpo_type thy' typ)
- then error("Not a pcpo type: "^string_of_typ thy' typ)
+ val typs = ListPair.map (fn (tn, cnstrs) => (map (test_equal_type tn) cnstrs;
+ snd(third(hd(cnstrs))))) (typs',cnstrss);
+ val test_typs = ListPair.map (fn (typ,cnstrs) =>
+ if not (pcpo_type sg' typ)
+ then error("Not a pcpo type: "^string_of_typ sg' typ)
else map (fn (cn,_,(_,rt)) => rt=typ orelse error(
"Non-identical result types for constructors "^
first(hd cnstrs)^" and "^ cn )) cnstrs)
- (typs~~cnstrss);
+ (typs,cnstrss);
val proper_args = let
fun occurs tn (Type(tn',ts)) = (tn'=tn) orelse exists (occurs tn) ts
| occurs _ _ = false;
@@ -120,23 +111,34 @@
in
- fun add_domain (comp_dname,eqs'') thy'' = let
- val eqs' = check_and_sort_domain eqs'' thy'';
- val thy' = thy'' |> Domain_Syntax.add_syntax (comp_dname,eqs');
+ fun add_domain (comp_dnam,eqs''') thy''' = let
+ val sg''' = sign_of thy''';
+ val dtnvs = map ((fn (dname,vs) =>
+ (Sign.full_name sg''' dname,map (str2typ sg''') 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 rep_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 thy' = thy'' |> Domain_Syntax.add_syntax (comp_dnam,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,
+ ((ThyOps.const_name con syn),
+ ListPair.map (fn ((lazy,sel,tp),vn) => ((lazy,
find (tp,dts) handle LIST "find" => ~1),
sel,vn))
- (args~~(mk_var_names(map third args)))
+ (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);
+ val thy = thy' |> Domain_Axioms.add_axioms (comp_dnam,eqs);
in (thy,eqs) end;
fun add_gen_by ((tname,finite),(typs',cnstrss')) thy' = let
- val (typs,cnstrs) = check_gen_by thy' (typs',cnstrss');
+ val (typs,cnstrs) = check_gen_by (sign_of thy') (typs',cnstrss');
in
Domain_Axioms.add_induct ((tname,finite),(typs,cnstrs)) thy' end;
--- a/src/HOLCF/domain/interface.ML Mon Oct 27 10:46:36 1997 +0100
+++ b/src/HOLCF/domain/interface.ML Mon Oct 27 11:34:33 1997 +0100
@@ -40,45 +40,36 @@
(if num > 1 then "val rews = " ^rews1 ^";\n" else "")
end;
- fun mk_domain (eqs'') = let
- val dtnvs = map (rep_Type o fst) eqs'';
+ fun mk_domain eqs'' = let
+ val num = length eqs'';
+ val dtnvs = map fst eqs'';
val dnames = map fst dtnvs;
- val num = length dnames;
val comp_dname = implode (separate "_" dnames);
val conss' = ListPair.map
- (fn (dname,cons'') =>
- let fun sel n m = upd_second
+ (fn (dname,cons'') => let fun sel n m = upd_second
(fn None => dname^"_sel_"^(string_of_int n)^
- "_"^(string_of_int m)
+ "_"^(string_of_int m)
| Some s => s)
fun fill_sels n con = upd_third (mapn (sel n) 1) con;
in mapn fill_sels 1 cons'' end)
- (dnames, map #2 eqs'');
+ (dnames, map snd eqs'');
val eqs' = dtnvs~~conss';
(* ----- string for calling add_domain -------------------------------------- *)
val thy_ext_string = let
- fun mk_tnv (n,v) = mk_pair (quote n, mk_list (map mk_typ v))
- and mk_typ (TFree(name,sort))= "TFree" ^
- mk_pair (quote name, mk_list (map quote sort))
- | mk_typ (Type (name,args))= "Type" ^mk_tnv(name,args)
- | mk_typ _ = Imposs "interface:mk_typ";
fun mk_conslist cons' =
- mk_list (map
- (fn (c,syn,ts)=>
- mk_triple(quote c, syn,
- mk_list
- (map (fn (b,s ,tp) =>
- mk_triple(Bool.toString b, quote s,
- mk_typ tp)) ts))) cons');
+ mk_list (map (fn (c,syn,ts)=>
+ mk_triple(quote c, syn, mk_list (map (fn (b,s ,tp) =>
+ mk_triple(Bool.toString b, quote s, tp)) ts))) cons');
in "val (thy, "^comp_dname^"_equations) = thy |> Domain_Extender.add_domain \n"
- ^ mk_pair(quote comp_dname,
- mk_list(map (fn (t,cs)=> mk_pair (mk_tnv t,mk_conslist cs)) eqs'))
+ ^ mk_pair(quote comp_dname, mk_list(map (fn ((n,vs),cs) =>
+ mk_pair (mk_pair (quote n, mk_list vs),
+ mk_conslist cs)) eqs'))
^ ";\nval thy = thy"
end;
-(* ----- string for calling (comp_)theorems and producing the structures ---------- *)
+(* ----- string for calling (comp_)theorems and producing the structures ---- *)
val val_gen_string = let
fun plural s = if num > 1 then s^"s" else "["^s^"]";
@@ -126,29 +117,29 @@
val name' = name >> strip_quotes;
val type_var' = type_var >> strip_quotes;
- val sort = name' >> (fn s => [s])
- || "{" $$-- !! (list name' --$$ "}");
- val tvar = (type_var' --(optional("::" $$-- !! sort)["_default"])) >>TFree;
-(*val tvar = type_var >> (fn tv => TFree(strip_quotes tv,["pcpo"]));*)
- fun type_args l = ("(" $$-- !! (list1 typ --$$ ")")
- || tvar >> (fn x => [x])
- || empty >> K []) l
- and con_typ l = (type_args -- name' >> (fn (x,y) => Type(y,x))) l
- (* here ident may be used instead of name'
- to avoid ambiguity with standard mixfix option *)
- and typ l = (con_typ
- || tvar) l;
+ fun esc_quote s = let fun esc [] = []
+ | esc ("\""::xs) = esc xs
+ | esc ("[" ::xs) = "{"::esc xs
+ | esc ("]" ::xs) = "}"::esc xs
+ | esc (x ::xs) = x ::esc xs
+ in implode (esc (explode s)) end;
+ val tvar = (type_var' ^^ optional ($$ "::" ^^ (sort >> esc_quote)) "") >> quote;
+ fun type_args l = (tvar >> (fn x => [x])
+ || "(" $$-- !! (list1 tvar --$$ ")")
+ || empty >> K []) l
+ fun con_typ l = (type_args -- name' >> (fn (x,y) => (y,x))) l
+ (* here ident may be used instead of name'
+ to avoid ambiguity with standard mixfix option *)
val domain_arg = "(" $$-- (optional ($$ "lazy" >> K true) false)
-- (optional ((name' >> Some) --$$ "::") None)
-- typ --$$ ")" >> (fn ((lazy,sel),tp) => (lazy,sel,tp))
- || name' >> (fn x => (false,None,Type(x,[])))
- || tvar >> (fn x => (false,None,x));
+ || typ >> (fn x => (false,None,x))
val domain_cons = name' -- !! (repeat domain_arg)
-- ThyOps.opt_cmixfix
>> (fn ((con,args),syn) => (con,syn,args));
in
val domain_decl = (enum1 "," (con_typ --$$ "=" -- !!
- (enum1 "|" domain_cons))) >> mk_domain;
+ (enum1 "|" domain_cons))) >> mk_domain;
val gen_by_decl = (optional ($$ "finite" >> K true) false) --
(enum1 "," (name' --$$ "by" -- !!
(enum1 "|" name'))) >> mk_gen_by;
--- a/src/HOLCF/domain/library.ML Mon Oct 27 10:46:36 1997 +0100
+++ b/src/HOLCF/domain/library.ML Mon Oct 27 11:34:33 1997 +0100
@@ -60,9 +60,9 @@
forbidding "o", "x..","f..","P.." as names *)
(* a number string is added if necessary *)
fun mk_var_names types : string list = let
- fun typid (Type (id,_) ) = hd (explode id)
- | typid (TFree (id,_) ) = hd (tl (explode id))
- | typid (TVar ((id,_),_)) = hd (tl (explode id));
+ fun typid (Type (id,_) ) = hd (explode (Sign.base_name id))
+ | typid (TFree (id,_) ) = hd (tl (explode (Sign.base_name id)))
+ | typid (TVar ((id,_),_)) = hd (tl (explode (Sign.base_name id)));
fun nonreserved s = if s mem ["x","f","P"] then s^"'" else s;
fun index_vnames(vn::vns,occupied) =
(case assoc(occupied,vn) of
@@ -76,11 +76,12 @@
fun rep_Type (Type x) = x | rep_Type _ = Imposs "library:rep_Type";
fun rep_TFree (TFree x) = x | rep_TFree _ = Imposs "library:rep_TFree";
-val tsig_of = #tsig o Sign.rep_sg o sign_of;
-fun pcpo_type thy t = Type.of_sort (tsig_of thy)
- (Sign.certify_typ (sign_of thy) t,["pcpo"]);
-fun string_of_typ thy t = let val sg = sign_of thy in
- Sign.string_of_typ sg (Sign.certify_typ sg t) end;
+val tsig_of = #tsig o Sign.rep_sg;
+val HOLCF_sg = sign_of HOLCF.thy;
+val pcpoS = Sign.intern_sort HOLCF_sg ["pcpo"];
+fun pcpo_type sg t = Type.of_sort (tsig_of sg) (Sign.certify_typ sg t, pcpoS);
+fun string_of_typ sg = Sign.string_of_typ sg o Sign.certify_typ sg;
+fun str2typ sg = typ_of o read_ctyp sg;
(* ----- constructor list handling ----- *)
@@ -105,8 +106,8 @@
(* ----- support for type and mixfix expressions ----- *)
-fun mk_tvar s = TFree("'"^s,["pcpo"]);
-fun mk_typ t (S,T) = Type(t,[S,T]);
+fun mk_tvar s = TFree("'"^s,pcpoS);
+fun mk_typ t (S,T) = Sign.intern_typ HOLCF_sg (Type(t,[S,T]));
infixr 5 -->;
infixr 6 ~>; val op ~> = mk_typ "->";
val NoSyn' = ThyOps.Mixfix NoSyn;
--- a/src/HOLCF/domain/syntax.ML Mon Oct 27 10:46:36 1997 +0100
+++ b/src/HOLCF/domain/syntax.ML Mon Oct 27 11:34:33 1997 +0100
@@ -26,11 +26,12 @@
in
val dtype = Type(dname,typevars);
val dtype2 = foldr' (mk_typ "++") (map prod cons');
- val const_rep = (dname^"_rep" , dtype ~> dtype2, NoSyn');
- val const_abs = (dname^"_abs" , dtype2 ~> dtype , NoSyn');
- val const_when = (dname^"_when", foldr (op ~>) ((map when_type cons'),
- dtype ~> freetvar "t"), NoSyn');
- val const_copy = (dname^"_copy", dtypeprod ~> dtype ~> dtype , NoSyn');
+ val dnam = Sign.base_name dname;
+ val const_rep = (dnam^"_rep" , dtype ~> dtype2, NoSyn');
+ val const_abs = (dnam^"_abs" , dtype2 ~> dtype , NoSyn');
+ val const_when = (dnam^"_when", foldr (op ~>) ((map when_type cons'),
+ dtype ~> freetvar "t"), NoSyn');
+ val const_copy = (dnam^"_copy", dtypeprod ~> dtype ~> dtype , NoSyn');
end;
(* ----- constants concerning the constructors, discriminators and selectors ------ *)
@@ -60,8 +61,8 @@
(* ----- constants concerning induction ------------------------------------------- *)
- val const_take = (dname^"_take" , Type("nat",[]) --> dtype ~> dtype, NoSyn');
- val const_finite = (dname^"_finite", dtype-->HOLogic.boolT , NoSyn');
+ val const_take = (dnam^"_take" , Type("nat",[]) --> dtype ~> dtype, NoSyn');
+ val const_finite = (dnam^"_finite", dtype-->HOLogic.boolT , NoSyn');
(* ----- case translation --------------------------------------------------------- *)
@@ -86,7 +87,7 @@
(mapn case1 1 cons')],
mk_appl (Constant "@fapp") [foldl
(fn (w,a ) => mk_appl (Constant "@fapp" ) [w,a ])
- (Constant (dname^"_when"),mapn arg1 1 cons'),
+ (Constant (dnam^"_when"),mapn arg1 1 cons'),
Variable "x"])
end;
end;
@@ -101,23 +102,17 @@
in (* local *)
-fun add_syntax (comp_dname,eqs': ((string * typ list) *
+fun add_syntax (comp_dnam,eqs': ((string * typ list) *
(string * ThyOps.cmixfix * (bool*string*typ) list) list) list) thy'' =
let
- fun thy_type (dname,tvars) = (dname, length tvars, NoSyn);
- fun thy_arity (dname,tvars) = (dname, map (snd o rep_TFree) tvars, ["pcpo"]);
- val thy_types = map (thy_type o fst) eqs';
- val thy_arities = map (thy_arity o fst) eqs';
- val dtypes = map (Type o fst) eqs';
+ val dtypes = map (Type o fst) eqs';
val funprod = foldr' (mk_typ "*") (map (fn tp => tp ~> tp )dtypes);
val relprod = foldr' (mk_typ "*") (map (fn tp => tp--> tp --> HOLogic.boolT)dtypes);
- val const_copy = (comp_dname^"_copy" ,funprod ~> funprod , NoSyn');
- val const_bisim = (comp_dname^"_bisim" ,relprod --> HOLogic.boolT, NoSyn');
+ val const_copy = (comp_dnam^"_copy" ,funprod ~> funprod , NoSyn');
+ val const_bisim = (comp_dnam^"_bisim" ,relprod --> HOLogic.boolT, NoSyn');
val ctt = map (calc_syntax funprod) eqs';
val add_cur_ops_i = ThyOps.add_ops_i {curried=true, strict=false, total=false};
-in thy'' |> Theory.add_types thy_types
- |> Theory.add_arities_i thy_arities
- |> add_cur_ops_i (flat(map fst ctt))
+in thy'' |> add_cur_ops_i (flat(map fst ctt))
|> add_cur_ops_i ((if length eqs'>1 then [const_copy] else[])@[const_bisim])
|> Theory.add_trrules_i (flat(map snd ctt))
end; (* let *)
--- a/src/HOLCF/domain/theorems.ML Mon Oct 27 10:46:36 1997 +0100
+++ b/src/HOLCF/domain/theorems.ML Mon Oct 27 11:34:33 1997 +0100
@@ -62,7 +62,7 @@
fun theorems thy (((dname,_),cons) : eq, eqs :eq list) =
let
-val dummy = writeln ("Proving isomorphism properties of domain "^dname^"...");
+val dummy = writeln ("Proving isomorphism properties of domain "^dname^"...");
val pg = pg' thy;
(*
infixr 0 y;
@@ -328,15 +328,16 @@
end; (* let *)
-fun comp_theorems thy (comp_dname, eqs: eq list, casess, con_rews, copy_rews) =
+fun comp_theorems thy (comp_dnam, eqs: eq list, casess, con_rews, copy_rews) =
let
+val dnames = map (fst o fst) eqs;
+val conss = map snd eqs;
+val comp_dname = Sign.full_name (sign_of thy) comp_dnam;
+
val dummy = writeln("Proving induction properties of domain "^comp_dname^"...");
val pg = pg' thy;
-val dnames = map (fst o fst) eqs;
-val conss = map snd eqs;
-
(* ----- getting the composite axiom and definitions ------------------------ *)
local val ga = get_axiom thy in