cleaned up; renamed library function mk_cRep_CFun to list_ccomb; replaced rep_TFree with dest_TFree; added functions spair, mk_stuple
--- 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;
--- 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'';
--- 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)
--- 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")