src/HOLCF/domain/library.ML
changeset 16842 5979c46853d1
parent 16778 2162c0de4673
child 17325 d9d50222808e
     1.1 --- a/src/HOLCF/domain/library.ML	Thu Jul 14 19:28:23 2005 +0200
     1.2 +++ b/src/HOLCF/domain/library.ML	Thu Jul 14 19:28:24 2005 +0200
     1.3 @@ -8,8 +8,6 @@
     1.4  
     1.5  (* ----- general support ---------------------------------------------------- *)
     1.6  
     1.7 -fun Id x = x;
     1.8 -
     1.9  fun mapn f n []      = []
    1.10  |   mapn f n (x::xs) = (f n x) :: mapn f (n+1) xs;
    1.11  
    1.12 @@ -17,7 +15,7 @@
    1.13  			     | itr [a] = f2 a
    1.14  			     | itr (a::l) = f(a, itr l)
    1.15  in  itr l  end;
    1.16 -fun foldr' f l = foldr'' f (l,Id);
    1.17 +fun foldr' f l = foldr'' f (l,I);
    1.18  fun map_cumulr f start xs = foldr (fn (x,(ys,res))=>case f(x,res) of (y,res2) =>
    1.19  						  (y::ys,res2)) ([],start) xs;
    1.20  
    1.21 @@ -175,9 +173,9 @@
    1.22  infixr 0 ==>;   fun S ==> T = mk_trp S ===> mk_trp T;
    1.23  infix 0 ==;     fun S ==  T = %%:"==" $ S $ T;
    1.24  infix 1 ===;    fun S === T = %%:"op =" $ S $ T;
    1.25 -infix 1 ~=;     fun S ~=  T = mk_not (S === T);
    1.26 +infix 1 ~=;     fun S ~=  T = HOLogic.mk_not (S === T);
    1.27  infix 1 <<;     fun S <<  T = %%:lessN $ S $ T;
    1.28 -infix 1 ~<<;    fun S ~<< T = mk_not (S << T);
    1.29 +infix 1 ~<<;    fun S ~<< T = HOLogic.mk_not (S << T);
    1.30  
    1.31  infix 9 `  ; fun f`  x = %%:Rep_CFunN $ f $ x;
    1.32  infix 9 `% ; fun f`% s = f` %: s;
    1.33 @@ -186,7 +184,7 @@
    1.34  fun con_app2 con f args = mk_cRep_CFun(%%:con,map f args);
    1.35  fun con_app con = con_app2 con %#;
    1.36  fun if_rec  arg f y   = if is_rec arg then f (rec_of arg) else y;
    1.37 -fun app_rec_arg p arg = if_rec arg (fn n => fn x => (p n)`x) Id (%# arg);
    1.38 +fun app_rec_arg p arg = if_rec arg (fn n => fn x => (p n)`x) I (%# arg);
    1.39  fun prj _  _  x (   _::[]) _ = x
    1.40  |   prj f1 _  x (_::y::ys) 0 = f1 x y
    1.41  |   prj f1 f2 x (y::   ys) j = prj f1 f2 (f2 x y) ys (j-1);
    1.42 @@ -195,11 +193,11 @@
    1.43  fun  proj x      = prj (fn S => K(%%:"fst" $S)) (fn S => K(%%:"snd" $S)) x;
    1.44  fun cproj x      = prj (fn S => K(%%:cfstN`S)) (fn S => K(%%:csndN`S)) x;
    1.45  fun prj' _  _  x (   _::[]) _ = x
    1.46 -|   prj' f1 _  x (_::   ys) 0 = f1 x (foldr' mk_prodT ys)
    1.47 +|   prj' f1 _  x (_::   ys) 0 = f1 x (foldr' HOLogic.mk_prodT ys)
    1.48  |   prj' f1 f2 x (y::   ys) j = prj' f1 f2 (f2 x y) ys (j-1);
    1.49  fun cproj' T eqs = prj'
    1.50 -	(fn S => fn t => Const(cfstN,mk_prodT(dummyT,t)->>dummyT)`S)
    1.51 -	(fn S => fn t => Const(csndN,mk_prodT(t,dummyT)->>dummyT)`S) 
    1.52 +	(fn S => fn t => Const(cfstN, HOLogic.mk_prodT(dummyT,t)->>dummyT)`S)
    1.53 +	(fn S => fn t => Const(csndN, HOLogic.mk_prodT(t,dummyT)->>dummyT)`S) 
    1.54  		       T (map ((fn tp => tp ->> tp) o Type o fix_tp o fst) eqs);
    1.55  fun lift tfn = Library.foldr (fn (x,t)=> (mk_trp(tfn x) ===> t));
    1.56  
    1.57 @@ -215,7 +213,7 @@
    1.58  |   mk_ctuple (t::ts) = cpair (t, mk_ctuple ts);
    1.59  fun mk_ctupleT [] = HOLogic.unitT   (* used in match_defs *)
    1.60  |   mk_ctupleT (T::[]) = T
    1.61 -|   mk_ctupleT (T::Ts) = mk_prodT(T, mk_ctupleT Ts);
    1.62 +|   mk_ctupleT (T::Ts) = HOLogic.mk_prodT(T, mk_ctupleT Ts);
    1.63  fun lift_defined f = lift (fn x => defined (f x));
    1.64  fun bound_arg vns v = Bound(length vns -find_index_eq v vns -1);
    1.65  
    1.66 @@ -236,13 +234,13 @@
    1.67  	|   one_fun n (_,args) = let
    1.68  		val l2 = length args;
    1.69  		fun idxs m arg = (if is_lazy arg then fn x=> %%:fupN` %%:ID_N`x
    1.70 -					         else Id) (Bound(l2-m));
    1.71 +					         else I) (Bound(l2-m));
    1.72  		in cont_eta_contract (foldr'' 
    1.73  			(fn (a,t) => %%:ssplitN`(/\# (a,t)))
    1.74  			(args,
    1.75  			fn a=> /\#(a,(mk_cRep_CFun(funarg(l2,n),mapn idxs 1 args))))
    1.76  			) end;
    1.77  in (if length cons = 1 andalso length(snd(hd cons)) <= 1
    1.78 -    then fn t => %%:strictifyN`t else Id)
    1.79 +    then fn t => %%:strictifyN`t else I)
    1.80       (foldr' (fn (x,y)=> %%:sscaseN`x`y) (mapn one_fun 1 cons)) end;
    1.81  end; (* struct *)