# HG changeset patch # User huffman # Date 1201626012 -3600 # Node ID f6917792f8a4475481c203e49d79989de21002f8 # Parent d55224947082d60c287ae1bb764370edbe210b8b new term-building combinators diff -r d55224947082 -r f6917792f8a4 src/HOLCF/Tools/domain/domain_axioms.ML --- a/src/HOLCF/Tools/domain/domain_axioms.ML Tue Jan 29 10:20:00 2008 +0100 +++ b/src/HOLCF/Tools/domain/domain_axioms.ML Tue Jan 29 18:00:12 2008 +0100 @@ -44,11 +44,11 @@ (* -- definitions concerning the constructors, discriminators and selectors - *) fun con_def m n (_,args) = let - fun idxs z x arg = (if is_lazy arg then fn t => %%:upN`t else I) (Bound(z-x)); + fun idxs z x arg = (if is_lazy arg then mk_up else I) (Bound(z-x)); fun parms vs = mk_stuple (mapn (idxs(length vs)) 1 vs); fun inj y 1 _ = y - | inj y _ 0 = %%:sinlN`y - | inj y i j = %%:sinrN`(inj y (i-1) (j-1)); + | inj y _ 0 = mk_sinl y + | inj y i j = mk_sinr (inj y (i-1) (j-1)); in foldr /\# (dc_abs`(inj (parms args) m n)) args end; val con_defs = mapn (fn n => fn (con,args) => @@ -58,7 +58,7 @@ fun ddef (con,_) = (dis_name con ^"_def",%%:(dis_name con) == list_ccomb(%%:(dname^"_when"),map (fn (con',args) => (foldr /\# - (if con'=con then %%:TT_N else %%:FF_N) args)) cons)) + (if con'=con then TT else FF) args)) cons)) in map ddef cons end; val mat_defs = let @@ -66,8 +66,8 @@ list_ccomb(%%:(dname^"_when"),map (fn (con',args) => (foldr /\# (if con'=con - then %%:returnN`(mk_ctuple (map (bound_arg args) args)) - else %%:failN) args)) cons)) + then mk_return (mk_ctuple (map (bound_arg args) args)) + else mk_fail) args)) cons)) in map mdef cons end; val pat_defs = @@ -77,9 +77,9 @@ val ps = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args; val xs = map (bound_arg args) args; val r = Bound (length args); - val rhs = case args of [] => %%:returnN ` HOLogic.unit - | _ => foldr1 cpair_pat ps ` mk_ctuple xs; - fun one_con (con',args') = foldr /\# (if con'=con then rhs else %%:failN) args'; + val rhs = case args of [] => mk_return HOLogic.unit + | _ => mk_ctuple_pat ps ` mk_ctuple xs; + fun one_con (con',args') = foldr /\# (if con'=con then rhs else mk_fail) args'; in (pat_name con ^"_def", list_comb (%%:(pat_name con), ps) == list_ccomb(%%:(dname^"_when"), map one_con cons)) end @@ -95,10 +95,10 @@ (* ----- axiom and definitions concerning induction ------------------------- *) - val reach_ax = ("reach", mk_trp(cproj (%%:fixN`%%(comp_dname^"_copy")) eqs n + val reach_ax = ("reach", mk_trp(cproj (mk_fix (%%:(comp_dname^"_copy"))) eqs n `%x_name === %:x_name)); val take_def = ("take_def",%%:(dname^"_take") == mk_lam("n",cproj - (%%:iterateN $ Bound 0 ` %%:(comp_dname^"_copy") ` UU) eqs n)); + (mk_iterate (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))); @@ -125,7 +125,7 @@ val x_name = idx_name dnames "x"; fun copy_app dname = %%:(dname^"_copy")`Bound 0; val copy_def = ("copy_def" , %%:(comp_dname^"_copy") == - /\"f"(foldr1 cpair (map copy_app dnames))); + /\"f"(mk_ctuple (map copy_app dnames))); val bisim_def = ("bisim_def",%%:(comp_dname^"_bisim")==mk_lam("R", let fun one_con (con,args) = let diff -r d55224947082 -r f6917792f8a4 src/HOLCF/Tools/domain/domain_library.ML --- a/src/HOLCF/Tools/domain/domain_library.ML Tue Jan 29 10:20:00 2008 +0100 +++ b/src/HOLCF/Tools/domain/domain_library.ML Tue Jan 29 18:00:12 2008 +0100 @@ -97,44 +97,6 @@ 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 = @{const_name Porder.sq_le}; -val UU_N = "Pcpo.UU"; -val admN = "Adm.adm"; -val compactN = "Adm.compact"; -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 cpair_patN = "Fixrec.cpair_pat"; -val branchN = "Fixrec.branch"; - -val pcpoN = "Pcpo.pcpo" -val pcpoS = [pcpoN]; - - (* ----- support for type and mixfix expressions ----- *) infixr 5 -->; @@ -164,12 +126,40 @@ infix 0 ==; fun S == T = %%:"==" $ S $ T; infix 1 ===; fun S === T = %%:"op =" $ S $ T; infix 1 ~=; fun S ~= T = HOLogic.mk_not (S === T); -infix 1 <<; fun S << T = %%:lessN $ S $ T; +infix 1 <<; fun S << T = %%:@{const_name Porder.sq_le} $ S $ T; infix 1 ~<<; fun S ~<< T = HOLogic.mk_not (S << T); -infix 9 ` ; fun f` x = %%:Rep_CFunN $ f $ x; +infix 9 ` ; fun f ` x = %%:@{const_name Rep_CFun} $ f $ x; infix 9 `% ; fun f`% s = f` %: s; infix 9 `%%; fun f`%%s = f` %%:s; + +fun mk_adm t = %%:@{const_name adm} $ t; +fun mk_compact t = %%:@{const_name compact} $ t; +val ID = %%:@{const_name ID}; +fun mk_strictify t = %%:@{const_name strictify}`t; +fun mk_cfst t = %%:@{const_name cfst}`t; +fun mk_csnd t = %%:@{const_name csnd}`t; +(*val csplitN = "Cprod.csplit";*) +(*val sfstN = "Sprod.sfst";*) +(*val ssndN = "Sprod.ssnd";*) +fun mk_ssplit t = %%:@{const_name ssplit}`t; +fun mk_sinl t = %%:@{const_name sinl}`t; +fun mk_sinr t = %%:@{const_name sinr}`t; +fun mk_sscase (x, y) = %%:@{const_name sscase}`x`y; +fun mk_up t = %%:@{const_name up}`t; +fun mk_fup (t,u) = %%:@{const_name fup} ` t ` u; +val ONE = @{term ONE}; +val TT = @{term TT}; +val FF = @{term FF}; +fun mk_iterate (n,f,z) = %%:@{const_name iterate} $ n ` f ` z; +fun mk_fix t = %%:@{const_name fix}`t; +fun mk_return t = %%:@{const_name Fixrec.return}`t; +val mk_fail = %%:@{const_name Fixrec.fail}; + +fun mk_branch t = %%:@{const_name Fixrec.branch} $ t; + +val pcpoS = @{sort pcpo}; + val list_ccomb = Library.foldl (op `); (* continuous version of list_comb *) fun con_app2 con f args = list_ccomb(%%:con,map f args); fun con_app con = con_app2 con %#; @@ -179,25 +169,26 @@ | prj f1 _ x (_::y::ys) 0 = f1 x y | prj f1 f2 x (y:: ys) j = prj f1 f2 (f2 x y) ys (j-1); fun proj x = prj (fn S => K(%%:"fst" $S)) (fn S => K(%%:"snd" $S)) x; -fun cproj x = prj (fn S => K(%%:cfstN`S)) (fn S => K(%%:csndN`S)) x; +fun cproj x = prj (fn S => K(mk_cfst S)) (fn S => K(mk_csnd S)) x; fun lift tfn = Library.foldr (fn (x,t)=> (mk_trp(tfn x) ===> t)); -fun /\ v T = %%:Abs_CFunN $ mk_lam(v,T); +fun /\ v T = %%:@{const_name Abs_CFun} $ mk_lam(v,T); fun /\# (arg,T) = /\ (vname arg) T; -infixr 9 oo; fun S oo T = %%:cfcompN`S`T; -val UU = %%:UU_N; +infixr 9 oo; fun S oo T = %%:@{const_name cfcomp}`S`T; +val UU = %%:@{const_name UU}; fun strict f = f`UU === UU; fun defined t = t ~= UU; -fun cpair (t,u) = %%:cpairN`t`u; -fun spair (t,u) = %%:spairN`t`u; +fun cpair (t,u) = %%:@{const_name cpair}`t`u; +fun spair (t,u) = %%:@{const_name spair}`t`u; fun mk_ctuple [] = HOLogic.unit (* used in match_defs *) | mk_ctuple ts = foldr1 cpair ts; -fun mk_stuple [] = %%:ONE_N +fun mk_stuple [] = ONE | mk_stuple ts = foldr1 spair ts; fun mk_ctupleT [] = HOLogic.unitT (* used in match_defs *) | mk_ctupleT Ts = foldr1 HOLogic.mk_prodT Ts; fun mk_maybeT T = Type ("Fixrec.maybe",[T]); -fun cpair_pat (p1,p2) = %%:cpair_patN $ p1 $ p2; +fun cpair_pat (p1,p2) = %%:@{const_name cpair_pat} $ p1 $ p2; +val mk_ctuple_pat = foldr1 cpair_pat; fun lift_defined f = lift (fn x => defined (f x)); fun bound_arg vns v = Bound(length vns -find_index_eq v vns -1); @@ -217,14 +208,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=> %%:fupN` %%:ID_N`x + fun idxs m arg = (if is_lazy arg then (fn t => mk_fup (ID, t)) else I) (Bound(l2-m)); in cont_eta_contract (foldr'' - (fn (a,t) => %%:ssplitN`(/\# (a,t))) + (fn (a,t) => mk_ssplit (/\# (a,t))) (args, fn a=> /\#(a,(list_ccomb(funarg(l2,n),mapn idxs 1 args)))) ) end; in (if length cons = 1 andalso length(snd(hd cons)) <= 1 - then fn t => %%:strictifyN`t else I) - (foldr1 (fn (x,y)=> %%:sscaseN`x`y) (mapn one_fun 1 cons)) end; + then mk_strictify else I) + (foldr1 mk_sscase (mapn one_fun 1 cons)) end; end; (* struct *) diff -r d55224947082 -r f6917792f8a4 src/HOLCF/Tools/domain/domain_theorems.ML --- a/src/HOLCF/Tools/domain/domain_theorems.ML Tue Jan 29 10:20:00 2008 +0100 +++ b/src/HOLCF/Tools/domain/domain_theorems.ML Tue Jan 29 18:00:12 2008 +0100 @@ -276,7 +276,7 @@ fun dis_app c (con, args) = let val lhs = %%:(dis_name c) ` con_app con args; - val rhs = %%:(if con = c then TT_N else FF_N); + val rhs = if con = c then TT else FF; val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs)); val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1]; in pg axs_dis_def goal tacs end; @@ -313,8 +313,8 @@ val lhs = %%:(mat_name c) ` con_app con args; val rhs = if con = c - then %%:returnN ` mk_ctuple (map %# args) - else %%:failN; + then mk_return (mk_ctuple (map %# args)) + else mk_fail; val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs)); val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1]; in pg axs_mat_def goal tacs end; @@ -328,11 +328,11 @@ local fun ps args = mapn (fn n => fn _ => %:("pat" ^ string_of_int n)) 1 args; - fun pat_lhs (con,args) = %%:branchN $ list_comb (%%:(pat_name con), ps args); + fun pat_lhs (con,args) = mk_branch (list_comb (%%:(pat_name con), ps args)); - fun pat_rhs (con,[]) = %%:returnN ` ((%:"rhs") ` HOLogic.unit) + fun pat_rhs (con,[]) = mk_return ((%:"rhs") ` HOLogic.unit) | pat_rhs (con,args) = - (%%:branchN $ foldr1 cpair_pat (ps args)) + (mk_branch (mk_ctuple_pat (ps args))) `(%:"rhs")`(mk_ctuple (map %# args)); fun pat_strict c = @@ -346,7 +346,7 @@ let val axs = @{thm branch_def} :: axs_pat_def; val lhs = (pat_lhs c)`(%:"rhs")`(con_app con args); - val rhs = if con = fst c then pat_rhs c else %%:failN; + val rhs = if con = fst c then pat_rhs c else mk_fail; val goal = lift_defined %: (nonlazy args, mk_trp (lhs === rhs)); val tacs = [asm_simp_tac (HOLCF_ss addsimps when_rews) 1]; in pg axs goal tacs end; @@ -389,8 +389,8 @@ [compact_sinl, compact_sinr, compact_spair, compact_up, compact_ONE]; fun con_compact (con, args) = let - val concl = mk_trp (%%:compactN $ con_app con args); - val goal = lift (fn x => %%:compactN $ %#x) (args, concl); + val concl = mk_trp (mk_compact (con_app con args)); + val goal = lift (fn x => mk_compact (%#x)) (args, concl); val tacs = [ rtac (iso_locale RS iso_compact_abs) 1, REPEAT (resolve_tac rules 1 ORELSE atac 1)]; @@ -890,7 +890,7 @@ val goal = let - fun one_adm n _ = mk_trp (%%:admN $ %:(P_name n)); + fun one_adm n _ = mk_trp (mk_adm (%:(P_name n))); fun concf n dn = %:(P_name n) $ %:(x_name n); in Logic.list_implies (mapn one_adm 1 dnames, ind_term concf) end; fun tacf prems =