# HG changeset patch # User huffman # Date 1130980788 -3600 # Node ID cf7669049df5b5159ece75b136421c97dbc3f1af # Parent 21d71d20f64e3a3b411a87210606cd4a5448cbd7 cleaned up; renamed library function mk_cRep_CFun to list_ccomb; replaced rep_TFree with dest_TFree; added functions spair, mk_stuple diff -r 21d71d20f64e -r cf7669049df5 src/HOLCF/domain/axioms.ML --- a/src/HOLCF/domain/axioms.ML Thu Nov 03 01:54:51 2005 +0100 +++ b/src/HOLCF/domain/axioms.ML Thu Nov 03 02:19:48 2005 +0100 @@ -27,8 +27,8 @@ val x_name = idx_name eqs x_name' (n+1); val dnam = Sign.base_name dname; - val abs_iso_ax = ("abs_iso" ,mk_trp(dc_rep`(dc_abs`%x_name')=== %:x_name')); - val rep_iso_ax = ("rep_iso" ,mk_trp(dc_abs`(dc_rep`%x_name')=== %:x_name')); + val abs_iso_ax = ("abs_iso", mk_trp(dc_rep`(dc_abs`%x_name') === %:x_name')); + val rep_iso_ax = ("rep_iso", mk_trp(dc_abs`(dc_rep`%x_name') === %:x_name')); val when_def = ("when_def",%%:(dname^"_when") == foldr (uncurry /\ ) (/\x_name'((when_body cons (fn (x,y) => @@ -38,15 +38,14 @@ fun idxs z x arg = (if is_lazy arg then fn t => %%:upN`t else I) (if recu andalso is_rec arg then (cproj (Bound z) eqs (rec_of arg))`Bound(z-x) else Bound(z-x)); - fun parms [] = %%:ONE_N - | parms vs = foldr1(fn(x,t)=> %%:spairN`x`t)(mapn (idxs(length vs))1 vs); + 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)); in foldr /\# (outer (inj (parms args) m n)) args end; val copy_def = ("copy_def", %%:(dname^"_copy") == /\"f" (dc_abs oo - Library.foldl (op `) (%%:(dname^"_when") , + list_ccomb (%%:(dname^"_when") , mapn (con_def I true (length cons)) 0 cons))); (* -- definitions concerning the constructors, discriminators and selectors - *) @@ -56,14 +55,14 @@ val dis_defs = let fun ddef (con,_) = (dis_name con ^"_def",%%:(dis_name con) == - mk_cRep_CFun(%%:(dname^"_when"),map + list_ccomb(%%:(dname^"_when"),map (fn (con',args) => (foldr /\# (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 + list_ccomb(%%:(dname^"_when"),map (fn (con',args) => (foldr /\# (if con'=con then %%:returnN`(mk_ctuple (map (bound_arg args) args)) @@ -72,7 +71,7 @@ val sel_defs = let fun sdef con n arg = Option.map (fn sel => (sel^"_def",%%:sel == - mk_cRep_CFun(%%:(dname^"_when"),map + list_ccomb(%%:(dname^"_when"),map (fn (con',args) => if con'<>con then UU else foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg); in List.mapPartial I (List.concat(map (fn (con,args) => mapn (sdef con) 1 args) cons)) end; @@ -125,8 +124,8 @@ fun rel_app i ra = proj (Bound(allargs_cnt+2)) eqs (rec_of ra) $ Bound (2*recs_cnt-i) $ Bound (recs_cnt-i); val capps = foldr mk_conj (mk_conj( - Bound(allargs_cnt+1)===mk_cRep_CFun(%%:con,map (bound_arg allvns) vns1), - Bound(allargs_cnt+0)===mk_cRep_CFun(%%:con,map (bound_arg allvns) vns2))) + Bound(allargs_cnt+1)===list_ccomb(%%:con,map (bound_arg allvns) vns1), + Bound(allargs_cnt+0)===list_ccomb(%%:con,map (bound_arg allvns) vns2))) (mapn rel_app 1 rec_args); in foldr mk_ex (Library.foldr mk_conj (map (defined o Bound) nonlazy_idxs,capps)) allvns end; diff -r 21d71d20f64e -r cf7669049df5 src/HOLCF/domain/extender.ML --- a/src/HOLCF/domain/extender.ML Thu Nov 03 01:54:51 2005 +0100 +++ b/src/HOLCF/domain/extender.ML Thu Nov 03 02:19:48 2005 +0100 @@ -48,7 +48,7 @@ val test_dupl_sels = (case duplicates (List.mapPartial second (List.concat (map third (List.concat 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 + val test_dupl_tvars = exists(fn s=>case duplicates(map(fst o dest_TFree)s)of [] => false | dups => error("Duplicate type arguments: " ^commas_quote dups)) (map snd dtnvs); (* test for free type variables, illegal sort constraints on rhs, @@ -56,7 +56,7 @@ replace sorts in type variables on rhs *) fun analyse_equation ((dname,typevars),cons') = let - val tvars = map rep_TFree typevars; + val tvars = map dest_TFree typevars; fun distinct_name s = "'"^Sign.base_name dname^"_"^s; val distinct_typevars = map (fn (n,sort) => TFree (distinct_name n,sort)) tvars; @@ -73,7 +73,7 @@ else error ("Inconsistent sort constraint" ^ " for type variable " ^ quote v)) | analyse indirect (t as Type(s,typl)) = (case AList.lookup (op =) dtnvs s of - NONE => if exists (fn x => x = s) indirect_ok + NONE => if s mem indirect_ok then Type(s,map (analyse false) typl) else Type(s,map (analyse true) typl) | SOME typevars => if indirect @@ -103,7 +103,7 @@ 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); + fun thy_arity (dname,tvars) = (dname, map (snd o dest_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''; diff -r 21d71d20f64e -r cf7669049df5 src/HOLCF/domain/library.ML --- a/src/HOLCF/domain/library.ML Thu Nov 03 01:54:51 2005 +0100 +++ b/src/HOLCF/domain/library.ML Thu Nov 03 02:19:48 2005 +0100 @@ -71,9 +71,6 @@ | index_vnames([],occupied) = []; in index_vnames(map nonreserved ids, [("O",0),("o",0)]) end; -fun rep_Type (Type x) = x | rep_Type _ = Imposs "library:rep_Type"; -fun rep_TFree (TFree x) = x | rep_TFree _ = Imposs "library:rep_TFree"; - fun pcpo_type sg t = Sign.of_sort 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; @@ -180,8 +177,8 @@ 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); -fun con_app2 con f args = mk_cRep_CFun(%%:con,map f args); +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 %#; fun if_rec arg f y = if is_rec arg then f (rec_of arg) else y; fun app_rec_arg p arg = if_rec arg (fn n => fn x => (p n)`x) I (%# arg); @@ -207,13 +204,14 @@ val UU = %%:UU_N; fun strict f = f`UU === UU; fun defined t = t ~= UU; -fun cpair (S,T) = %%:cpairN`S`T; +fun cpair (t,u) = %%:cpairN`t`u; +fun spair (t,u) = %%:spairN`t`u; fun mk_ctuple [] = HOLogic.unit (* used in match_defs *) -| mk_ctuple (t::[]) = t -| mk_ctuple (t::ts) = cpair (t, mk_ctuple ts); +| mk_ctuple ts = foldr1 cpair ts; +fun mk_stuple [] = %%:ONE_N +| mk_stuple ts = foldr1 spair ts; fun mk_ctupleT [] = HOLogic.unitT (* used in match_defs *) -| mk_ctupleT (T::[]) = T -| mk_ctupleT (T::Ts) = HOLogic.mk_prodT(T, mk_ctupleT Ts); +| mk_ctupleT Ts = foldr1 HOLogic.mk_prodT Ts; fun lift_defined f = lift (fn x => defined (f x)); fun bound_arg vns v = Bound(length vns -find_index_eq v vns -1); @@ -238,7 +236,7 @@ in cont_eta_contract (foldr'' (fn (a,t) => %%:ssplitN`(/\# (a,t))) (args, - fn a=> /\#(a,(mk_cRep_CFun(funarg(l2,n),mapn idxs 1 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) diff -r 21d71d20f64e -r cf7669049df5 src/HOLCF/domain/theorems.ML --- a/src/HOLCF/domain/theorems.ML Thu Nov 03 01:54:51 2005 +0100 +++ b/src/HOLCF/domain/theorems.ML Thu Nov 03 02:19:48 2005 +0100 @@ -107,7 +107,7 @@ fun appl_of_def def = let val (_ $ con $ lam) = concl_of def; val (vars, rhs) = arglist lam; - val lhs = mk_cRep_CFun (con, bound_vars (length vars)); + val lhs = list_ccomb (con, bound_vars (length vars)); val appl = bind_fun vars (lhs == rhs); val cs = ContProc.cont_thms lam; val betas = map (fn c => mk_meta_eq (c RS beta_cfun)) cs; @@ -158,7 +158,7 @@ local fun bind_fun t = Library.foldr mk_All (when_funs cons,t); fun bound_fun i _ = Bound (length cons - i); - val when_app = Library.foldl (op `) (%%:(dname^"_when"), mapn bound_fun 1 cons); + val when_app = list_ccomb (%%:(dname^"_when"), mapn bound_fun 1 cons); in val when_strict = pg [when_appl, mk_meta_eq rep_strict] (bind_fun(mk_trp(strict when_app))) @@ -166,7 +166,7 @@ val when_apps = let fun one_when n (con,args) = pg (when_appl :: con_appls) (bind_fun (lift_defined %: (nonlazy args, mk_trp(when_app`(con_app con args) === - mk_cRep_CFun(bound_fun n 0,map %# args)))))[ + list_ccomb(bound_fun n 0,map %# args)))))[ asm_simp_tac (HOLCF_ss addsimps [ax_abs_iso]) 1]; in mapn one_when 1 cons end; end; @@ -224,7 +224,7 @@ let val rules = [compact_sinl, compact_sinr, compact_spair, compact_up, compact_ONE]; fun one_compact (con,args) = pg con_appls - (lift (fn x => %%:compactN $ %:(vname x)) (args, mk_trp(%%:compactN $ (con_app con args)))) + (lift (fn x => %%:compactN $ %#x) (args, mk_trp(%%:compactN $ (con_app con args)))) [rtac (iso_locale RS iso_compact_abs) 1, REPEAT (resolve_tac rules 1 ORELSE atac 1)]; in map one_compact cons end; @@ -391,11 +391,11 @@ local val iterate_Cprod_ss = simpset_of Fix.thy; val copy_con_rews = copy_rews @ con_rews; - val copy_take_defs =(if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def; + val copy_take_defs = (if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def; val take_stricts=pg copy_take_defs(mk_trp(foldr1 mk_conj(map(fn((dn,args),_)=> strict(dc_take dn $ %:"n")) eqs))) ([ induct_tac "n" 1, - simp_tac iterate_Cprod_ss 1, + simp_tac iterate_Cprod_ss 1, asm_simp_tac (iterate_Cprod_ss addsimps copy_rews)1]); val take_stricts' = rewrite_rule copy_take_defs take_stricts; val take_0s = mapn(fn n=> fn dn => pg axs_take_def(mk_trp((dc_take dn $ %%:"0")