# HG changeset patch # User huffman # Date 1121185716 -7200 # Node ID 2162c0de467376ec0a4366c9aa59426cc3850d03 # Parent 555c8951f05cd248030e42912ed578de7c4a59a9 use qualified names for all constants diff -r 555c8951f05c -r 2162c0de4673 src/HOLCF/domain/axioms.ML --- a/src/HOLCF/domain/axioms.ML Tue Jul 12 18:26:44 2005 +0200 +++ b/src/HOLCF/domain/axioms.ML Tue Jul 12 18:28:36 2005 +0200 @@ -35,14 +35,14 @@ Bound(1+length cons+x-y)))`(dc_rep`Bound 0))) (when_funs cons)); fun con_def outer recu m n (_,args) = let - fun idxs z x arg = (if is_lazy arg then fn t => %%:"up"`t else Id) + fun idxs z x arg = (if is_lazy arg then fn t => %%:upN`t else Id) (if recu andalso is_rec arg then (cproj (Bound z) eqs (rec_of arg))`Bound(z-x) else Bound(z-x)); - fun parms [] = %%:"ONE" - | parms vs = foldr'(fn(x,t)=> %%:"spair"`x`t)(mapn (idxs(length vs))1 vs); + fun parms [] = %%:ONE_N + | parms vs = foldr'(fn(x,t)=> %%:spairN`x`t)(mapn (idxs(length vs))1 vs); fun inj y 1 _ = y - | inj y _ 0 = %%:"sinl"`y - | inj y i j = %%:"sinr"`(inj y (i-1) (j-1)); + | inj y _ 0 = %%:sinlN`y + | inj y i j = %%:sinrN`(inj y (i-1) (j-1)); in foldr /\# (outer (inj (parms args) m n)) args end; val copy_def = ("copy_def", %%:(dname^"_copy") == /\"f" (dc_abs oo @@ -58,30 +58,32 @@ fun ddef (con,_) = (dis_name con ^"_def",%%:(dis_name con) == mk_cRep_CFun(%%:(dname^"_when"),map (fn (con',args) => (foldr /\# - (if con'=con then %%:"TT" else %%:"FF") args)) cons)) + (if con'=con then %%:TT_N else %%:FF_N) args)) cons)) in map ddef cons end; val mat_defs = let fun mdef (con,_) = (mat_name con ^"_def",%%:(mat_name con) == mk_cRep_CFun(%%:(dname^"_when"),map (fn (con',args) => (foldr /\# - (if con'=con then (%%:"return")`(mk_ctuple (map (bound_arg args) args)) else %%:"fail") args)) cons)) + (if con'=con + then %%:returnN`(mk_ctuple (map (bound_arg args) args)) + else %%:failN) args)) cons)) in map mdef cons end; val sel_defs = let fun sdef con n arg = Option.map (fn sel => (sel^"_def",%%:sel == mk_cRep_CFun(%%:(dname^"_when"),map - (fn (con',args) => if con'<>con then %%:"UU" else + (fn (con',args) => if con'<>con then UU else foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg); in List.mapPartial Id (List.concat(map (fn (con,args) => mapn (sdef con) 1 args) cons)) end; (* ----- axiom and definitions concerning induction ------------------------- *) - val reach_ax = ("reach", mk_trp(cproj (%%:"fix"`%%(comp_dname^"_copy")) eqs n + val reach_ax = ("reach", mk_trp(cproj (%%:fixN`%%(comp_dname^"_copy")) eqs n `%x_name === %:x_name)); val take_def = ("take_def",%%:(dname^"_take") == mk_lam("n",cproj' - (%%:"iterate" $ Bound 0 $ %%:(comp_dname^"_copy") $ %%:"UU") eqs n)); + (%%:iterateN $ Bound 0 $ %%:(comp_dname^"_copy") $ UU) eqs n)); val finite_def = ("finite_def",%%:(dname^"_finite") == mk_lam(x_name, mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1))); diff -r 555c8951f05c -r 2162c0de4673 src/HOLCF/domain/library.ML --- a/src/HOLCF/domain/library.ML Tue Jul 12 18:26:44 2005 +0200 +++ b/src/HOLCF/domain/library.ML Tue Jul 12 18:28:36 2005 +0200 @@ -102,6 +102,40 @@ fun nonlazy args = map vname (filter_out is_lazy args); fun nonlazy_rec args = map vname (List.filter is_nonlazy_rec args); +(* ----- qualified names of HOLCF constants ----- *) + +val lessN = "Porder.op <<" +val UU_N = "Pcpo.UU"; +val admN = "Adm.adm"; +val Rep_CFunN = "Cfun.Rep_CFun"; +val Abs_CFunN = "Cfun.Abs_CFun"; +val ID_N = "Cfun.ID"; +val cfcompN = "Cfun.cfcomp"; +val strictifyN = "Cfun.strictify"; +val cpairN = "Cprod.cpair"; +val cfstN = "Cprod.cfst"; +val csndN = "Cprod.csnd"; +val csplitN = "Cprod.csplit"; +val spairN = "Sprod.spair"; +val sfstN = "Sprod.sfst"; +val ssndN = "Sprod.ssnd"; +val ssplitN = "Sprod.ssplit"; +val sinlN = "Ssum.sinl"; +val sinrN = "Ssum.sinr"; +val sscaseN = "Ssum.sscase"; +val upN = "Up.up"; +val fupN = "Up.fup"; +val ONE_N = "One.ONE"; +val TT_N = "Tr.TT"; +val FF_N = "Tr.FF"; +val iterateN = "Fix.iterate"; +val fixN = "Fix.fix"; +val returnN = "Fixrec.return"; +val failN = "Fixrec.fail"; + +val pcpoN = "Pcpo.pcpo" +val pcpoS = [pcpoN]; + (* ----- support for type and mixfix expressions ----- *) infixr 5 -->; @@ -119,6 +153,7 @@ fun mk_imp (S,T) = imp $ S $ T; fun mk_lam (x,T) = Abs(x,dummyT,T); fun mk_all (x,P) = HOLogic.mk_all (x,dummyT,P); +fun mk_ex (x,P) = mk_exists (x,dummyT,P); local fun sg [s] = %:s | sg (s::ss) = %%:"_classes" $ %:s $ sg ss @@ -132,20 +167,19 @@ fun mk_constrain (typ,T) = %%:"_constrain" $ T $ tf typ; fun mk_constrainall (x,typ,P) = %%:"All" $ (%%:"_constrainAbs" $ mk_lam(x,P) $ tf typ); end; -fun mk_ex (x,P) = mk_exists (x,dummyT,P); end; fun mk_All (x,P) = %%:"all" $ mk_lam(x,P); (* meta universal quantification *) -infixr 0 ===>;fun S ===> T = %%:"==>" $ S $ T; -infixr 0 ==>;fun S ==> T = mk_trp S ===> mk_trp T; -infix 0 ==; fun S == T = %%:"==" $ S $ T; -infix 1 ===; fun S === T = %%:"op =" $ S $ T; -infix 1 ~=; fun S ~= T = mk_not (S === T); -infix 1 <<; fun S << T = %%:"op <<" $ S $ T; -infix 1 ~<<; fun S ~<< T = mk_not (S << T); +infixr 0 ===>; fun S ===> T = %%:"==>" $ S $ T; +infixr 0 ==>; fun S ==> T = mk_trp S ===> mk_trp T; +infix 0 ==; fun S == T = %%:"==" $ S $ T; +infix 1 ===; fun S === T = %%:"op =" $ S $ T; +infix 1 ~=; fun S ~= T = mk_not (S === T); +infix 1 <<; fun S << T = %%:lessN $ S $ T; +infix 1 ~<<; fun S ~<< T = mk_not (S << T); -infix 9 ` ; fun f` x = %%:"Rep_CFun" $ f $ x; +infix 9 ` ; fun f` x = %%:Rep_CFunN $ f $ x; infix 9 `% ; fun f`% s = f` %: s; infix 9 `%%; fun f`%%s = f` %%:s; fun mk_cRep_CFun (F,As) = Library.foldl (op `) (F,As); @@ -159,24 +193,24 @@ fun fix_tp (tn, args) = (tn, map (K oneT) args); (* instantiate type to avoid type varaibles *) fun proj x = prj (fn S => K(%%:"fst" $S)) (fn S => K(%%:"snd" $S)) x; -fun cproj x = prj (fn S => K(%%:"cfst"`S)) (fn S => K(%%:"csnd"`S)) x; +fun cproj x = prj (fn S => K(%%:cfstN`S)) (fn S => K(%%:csndN`S)) x; fun prj' _ _ x ( _::[]) _ = x | prj' f1 _ x (_:: ys) 0 = f1 x (foldr' mk_prodT ys) | prj' f1 f2 x (y:: ys) j = prj' f1 f2 (f2 x y) ys (j-1); fun cproj' T eqs = prj' - (fn S => fn t => Const("cfst",mk_prodT(dummyT,t)->>dummyT)`S) - (fn S => fn t => Const("csnd",mk_prodT(t,dummyT)->>dummyT)`S) + (fn S => fn t => Const(cfstN,mk_prodT(dummyT,t)->>dummyT)`S) + (fn S => fn t => Const(csndN,mk_prodT(t,dummyT)->>dummyT)`S) T (map ((fn tp => tp ->> tp) o Type o fix_tp o fst) eqs); fun lift tfn = Library.foldr (fn (x,t)=> (mk_trp(tfn x) ===> t)); -fun /\ v T = %%:"Abs_CFun" $ mk_lam(v,T); +fun /\ v T = %%:Abs_CFunN $ mk_lam(v,T); fun /\# (arg,T) = /\ (vname arg) T; -infixr 9 oo; fun S oo T = %%:"cfcomp"`S`T; -val UU = %%:"UU"; +infixr 9 oo; fun S oo T = %%:cfcompN`S`T; +val UU = %%:UU_N; fun strict f = f`UU === UU; fun defined t = t ~= UU; -fun cpair (S,T) = %%:"cpair"`S`T; -fun mk_ctuple [] = %%:"UU" (* used in match_defs *) +fun cpair (S,T) = %%:cpairN`S`T; +fun mk_ctuple [] = HOLogic.unit (* used in match_defs *) | mk_ctuple (t::[]) = t | mk_ctuple (t::ts) = cpair (t, mk_ctuple ts); fun mk_ctupleT [] = HOLogic.unitT (* used in match_defs *) @@ -185,12 +219,12 @@ fun lift_defined f = lift (fn x => defined (f x)); fun bound_arg vns v = Bound(length vns -find_index_eq v vns -1); -fun cont_eta_contract (Const("Abs_CFun",TT) $ Abs(a,T,body)) = +fun cont_eta_contract (Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body)) = (case cont_eta_contract body of - body' as (Const("Rep_CFun",Ta) $ f $ Bound 0) => + body' as (Const("Cfun.Rep_CFun",Ta) $ f $ Bound 0) => if not (0 mem loose_bnos f) then incr_boundvars ~1 f - else Const("Abs_CFun",TT) $ Abs(a,T,body') - | body' => Const("Abs_CFun",TT) $ Abs(a,T,body')) + else Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body') + | body' => Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body')) | cont_eta_contract(f$t) = cont_eta_contract f $ cont_eta_contract t | cont_eta_contract t = t; @@ -201,14 +235,14 @@ fun one_fun n (_,[] ) = /\ "dummy" (funarg(1,n)) | one_fun n (_,args) = let val l2 = length args; - fun idxs m arg = (if is_lazy arg then fn x=> %%:"fup"`%%"ID"`x + fun idxs m arg = (if is_lazy arg then fn x=> %%:fupN` %%:ID_N`x else Id) (Bound(l2-m)); in cont_eta_contract (foldr'' - (fn (a,t) => %%:"ssplit"`(/\# (a,t))) + (fn (a,t) => %%:ssplitN`(/\# (a,t))) (args, fn a=> /\#(a,(mk_cRep_CFun(funarg(l2,n),mapn idxs 1 args)))) ) end; in (if length cons = 1 andalso length(snd(hd cons)) <= 1 - then fn t => %%:"strictify"`t else Id) - (foldr' (fn (x,y)=> %%:"sscase"`x`y) (mapn one_fun 1 cons)) end; + then fn t => %%:strictifyN`t else Id) + (foldr' (fn (x,y)=> %%:sscaseN`x`y) (mapn one_fun 1 cons)) end; end; (* struct *) diff -r 555c8951f05c -r 2162c0de4673 src/HOLCF/domain/theorems.ML --- a/src/HOLCF/domain/theorems.ML Tue Jul 12 18:26:44 2005 +0200 +++ b/src/HOLCF/domain/theorems.ML Tue Jul 12 18:28:36 2005 +0200 @@ -114,7 +114,7 @@ val con_appls = map appl_of_def axs_con_def; local - fun arg2typ n arg = let val t = TVar (("'a",n),["Pcpo.pcpo"]) + fun arg2typ n arg = let val t = TVar (("'a",n),pcpoS) in (n+1, if is_lazy arg then mk_uT t else t) end; fun args2typ n [] = (n,oneT) | args2typ n [arg] = arg2typ n arg @@ -177,7 +177,7 @@ val dis_apps = let fun one_dis c (con,args)= pg axs_dis_def (lift_defined %: (nonlazy args, (mk_trp((%%:(dis_name c))`(con_app con args) === - %%:(if con=c then "TT" else "FF"))))) [ + %%:(if con=c then TT_N else FF_N))))) [ asm_simp_tac (HOLCF_ss addsimps when_rews) 1]; in List.concat(map (fn (c,_) => map (one_dis c) cons) cons) end; val dis_defins = map (fn (con,args) => pg [] (defined(%:x_name) ==> @@ -195,8 +195,10 @@ val mat_apps = let fun one_mat c (con,args)= pg axs_mat_def (lift_defined %: (nonlazy args, (mk_trp((%%:(mat_name c))`(con_app con args) === - (if con=c then (%%:"return")`(mk_ctuple (map %# args)) else %%:"fail"))))) [ - asm_simp_tac (HOLCF_ss addsimps when_rews) 1]; + (if con=c + then %%:returnN`(mk_ctuple (map %# args)) + else %%:failN))))) + [asm_simp_tac (HOLCF_ss addsimps when_rews) 1]; in List.concat(map (fn (c,_) => map (one_mat c) cons) cons) end; in mat_stricts @ mat_apps end; @@ -542,7 +544,7 @@ ) end (* let *) else (mapn (fn n => fn dn => read_instantiate_sg (sign_of thy) [("P",dn^"_finite "^x_name n)] excluded_middle) 1 dnames, - pg'' thy [] (Library.foldr (op ===>) (mapn (fn n => K(mk_trp(%%:"adm" $ %:(P_name n)))) + pg'' thy [] (Library.foldr (op ===>) (mapn (fn n => K(mk_trp(%%:admN $ %:(P_name n)))) 1 dnames, ind_term (fn n => fn dn => %:(P_name n) $ %:(x_name n)))) (fn prems => map (fn ax_reach => rtac (ax_reach RS subst) 1) axs_reach @ [