# HG changeset patch # User oheimb # Date 877948473 -3600 # Node ID 2444085532c67763e246deec7b6392ccb48abb6f # Parent 1d6aed7ff375fdf1aaa1f8c4cfc905b4a61c2067 adapted domain and ax_ops package for name spaces diff -r 1d6aed7ff375 -r 2444085532c6 src/HOLCF/ROOT.ML --- 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*) diff -r 1d6aed7ff375 -r 2444085532c6 src/HOLCF/ax_ops/holcflogic.ML --- 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")); diff -r 1d6aed7ff375 -r 2444085532c6 src/HOLCF/ax_ops/thy_ops.ML --- 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")); diff -r 1d6aed7ff375 -r 2444085532c6 src/HOLCF/domain/axioms.ML --- 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; diff -r 1d6aed7ff375 -r 2444085532c6 src/HOLCF/domain/extender.ML --- 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; diff -r 1d6aed7ff375 -r 2444085532c6 src/HOLCF/domain/interface.ML --- 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; diff -r 1d6aed7ff375 -r 2444085532c6 src/HOLCF/domain/library.ML --- 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; diff -r 1d6aed7ff375 -r 2444085532c6 src/HOLCF/domain/syntax.ML --- 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 *) diff -r 1d6aed7ff375 -r 2444085532c6 src/HOLCF/domain/theorems.ML --- 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