src/HOLCF/Tools/domain/domain_library.ML
changeset 26012 f6917792f8a4
parent 25723 80c06e4d4db6
child 26939 1035c89b4c02
     1.1 --- a/src/HOLCF/Tools/domain/domain_library.ML	Tue Jan 29 10:20:00 2008 +0100
     1.2 +++ b/src/HOLCF/Tools/domain/domain_library.ML	Tue Jan 29 18:00:12 2008 +0100
     1.3 @@ -97,44 +97,6 @@
     1.4  fun nonlazy     args   = map vname (filter_out is_lazy    args);
     1.5  fun nonlazy_rec args   = map vname (List.filter is_nonlazy_rec args);
     1.6  
     1.7 -(* ----- qualified names of HOLCF constants ----- *)
     1.8 -
     1.9 -val lessN      = @{const_name Porder.sq_le};
    1.10 -val UU_N       = "Pcpo.UU";
    1.11 -val admN       = "Adm.adm";
    1.12 -val compactN   = "Adm.compact";
    1.13 -val Rep_CFunN  = "Cfun.Rep_CFun";
    1.14 -val Abs_CFunN  = "Cfun.Abs_CFun";
    1.15 -val ID_N       = "Cfun.ID";
    1.16 -val cfcompN    = "Cfun.cfcomp";
    1.17 -val strictifyN = "Cfun.strictify";
    1.18 -val cpairN     = "Cprod.cpair";
    1.19 -val cfstN      = "Cprod.cfst";
    1.20 -val csndN      = "Cprod.csnd";
    1.21 -val csplitN    = "Cprod.csplit";
    1.22 -val spairN     = "Sprod.spair";
    1.23 -val sfstN      = "Sprod.sfst";
    1.24 -val ssndN      = "Sprod.ssnd";
    1.25 -val ssplitN    = "Sprod.ssplit";
    1.26 -val sinlN      = "Ssum.sinl";
    1.27 -val sinrN      = "Ssum.sinr";
    1.28 -val sscaseN    = "Ssum.sscase";
    1.29 -val upN        = "Up.up";
    1.30 -val fupN       = "Up.fup";
    1.31 -val ONE_N      = "One.ONE";
    1.32 -val TT_N       = "Tr.TT";
    1.33 -val FF_N       = "Tr.FF";
    1.34 -val iterateN   = "Fix.iterate";
    1.35 -val fixN       = "Fix.fix";
    1.36 -val returnN    = "Fixrec.return";
    1.37 -val failN      = "Fixrec.fail";
    1.38 -val cpair_patN = "Fixrec.cpair_pat";
    1.39 -val branchN    = "Fixrec.branch";
    1.40 -
    1.41 -val pcpoN      = "Pcpo.pcpo"
    1.42 -val pcpoS      = [pcpoN];
    1.43 -
    1.44 -
    1.45  (* ----- support for type and mixfix expressions ----- *)
    1.46  
    1.47  infixr 5 -->;
    1.48 @@ -164,12 +126,40 @@
    1.49  infix 0 ==;     fun S ==  T = %%:"==" $ S $ T;
    1.50  infix 1 ===;    fun S === T = %%:"op =" $ S $ T;
    1.51  infix 1 ~=;     fun S ~=  T = HOLogic.mk_not (S === T);
    1.52 -infix 1 <<;     fun S <<  T = %%:lessN $ S $ T;
    1.53 +infix 1 <<;     fun S <<  T = %%:@{const_name Porder.sq_le} $ S $ T;
    1.54  infix 1 ~<<;    fun S ~<< T = HOLogic.mk_not (S << T);
    1.55  
    1.56 -infix 9 `  ; fun f`  x = %%:Rep_CFunN $ f $ x;
    1.57 +infix 9 `  ; fun f ` x = %%:@{const_name Rep_CFun} $ f $ x;
    1.58  infix 9 `% ; fun f`% s = f` %: s;
    1.59  infix 9 `%%; fun f`%%s = f` %%:s;
    1.60 +
    1.61 +fun mk_adm t = %%:@{const_name adm} $ t;
    1.62 +fun mk_compact t = %%:@{const_name compact} $ t;
    1.63 +val ID = %%:@{const_name ID};
    1.64 +fun mk_strictify t = %%:@{const_name strictify}`t;
    1.65 +fun mk_cfst t = %%:@{const_name cfst}`t;
    1.66 +fun mk_csnd t = %%:@{const_name csnd}`t;
    1.67 +(*val csplitN    = "Cprod.csplit";*)
    1.68 +(*val sfstN      = "Sprod.sfst";*)
    1.69 +(*val ssndN      = "Sprod.ssnd";*)
    1.70 +fun mk_ssplit t = %%:@{const_name ssplit}`t;
    1.71 +fun mk_sinl t = %%:@{const_name sinl}`t;
    1.72 +fun mk_sinr t = %%:@{const_name sinr}`t;
    1.73 +fun mk_sscase (x, y) = %%:@{const_name sscase}`x`y;
    1.74 +fun mk_up t = %%:@{const_name up}`t;
    1.75 +fun mk_fup (t,u) = %%:@{const_name fup} ` t ` u;
    1.76 +val ONE = @{term ONE};
    1.77 +val TT = @{term TT};
    1.78 +val FF = @{term FF};
    1.79 +fun mk_iterate (n,f,z) = %%:@{const_name iterate} $ n ` f ` z;
    1.80 +fun mk_fix t = %%:@{const_name fix}`t;
    1.81 +fun mk_return t = %%:@{const_name Fixrec.return}`t;
    1.82 +val mk_fail = %%:@{const_name Fixrec.fail};
    1.83 +
    1.84 +fun mk_branch t = %%:@{const_name Fixrec.branch} $ t;
    1.85 +
    1.86 +val pcpoS = @{sort pcpo};
    1.87 +
    1.88  val list_ccomb = Library.foldl (op `); (* continuous version of list_comb *)
    1.89  fun con_app2 con f args = list_ccomb(%%:con,map f args);
    1.90  fun con_app con = con_app2 con %#;
    1.91 @@ -179,25 +169,26 @@
    1.92  |   prj f1 _  x (_::y::ys) 0 = f1 x y
    1.93  |   prj f1 f2 x (y::   ys) j = prj f1 f2 (f2 x y) ys (j-1);
    1.94  fun  proj x      = prj (fn S => K(%%:"fst" $S)) (fn S => K(%%:"snd" $S)) x;
    1.95 -fun cproj x      = prj (fn S => K(%%:cfstN`S)) (fn S => K(%%:csndN`S)) x;
    1.96 +fun cproj x      = prj (fn S => K(mk_cfst S)) (fn S => K(mk_csnd S)) x;
    1.97  fun lift tfn = Library.foldr (fn (x,t)=> (mk_trp(tfn x) ===> t));
    1.98  
    1.99 -fun /\ v T = %%:Abs_CFunN $ mk_lam(v,T);
   1.100 +fun /\ v T = %%:@{const_name Abs_CFun} $ mk_lam(v,T);
   1.101  fun /\# (arg,T) = /\ (vname arg) T;
   1.102 -infixr 9 oo; fun S oo T = %%:cfcompN`S`T;
   1.103 -val UU = %%:UU_N;
   1.104 +infixr 9 oo; fun S oo T = %%:@{const_name cfcomp}`S`T;
   1.105 +val UU = %%:@{const_name UU};
   1.106  fun strict f = f`UU === UU;
   1.107  fun defined t = t ~= UU;
   1.108 -fun cpair (t,u) = %%:cpairN`t`u;
   1.109 -fun spair (t,u) = %%:spairN`t`u;
   1.110 +fun cpair (t,u) = %%:@{const_name cpair}`t`u;
   1.111 +fun spair (t,u) = %%:@{const_name spair}`t`u;
   1.112  fun mk_ctuple [] = HOLogic.unit (* used in match_defs *)
   1.113  |   mk_ctuple ts = foldr1 cpair ts;
   1.114 -fun mk_stuple [] = %%:ONE_N
   1.115 +fun mk_stuple [] = ONE
   1.116  |   mk_stuple ts = foldr1 spair ts;
   1.117  fun mk_ctupleT [] = HOLogic.unitT   (* used in match_defs *)
   1.118  |   mk_ctupleT Ts = foldr1 HOLogic.mk_prodT Ts;
   1.119  fun mk_maybeT T = Type ("Fixrec.maybe",[T]);
   1.120 -fun cpair_pat (p1,p2) = %%:cpair_patN $ p1 $ p2;
   1.121 +fun cpair_pat (p1,p2) = %%:@{const_name cpair_pat} $ p1 $ p2;
   1.122 +val mk_ctuple_pat = foldr1 cpair_pat;
   1.123  fun lift_defined f = lift (fn x => defined (f x));
   1.124  fun bound_arg vns v = Bound(length vns -find_index_eq v vns -1);
   1.125  
   1.126 @@ -217,14 +208,14 @@
   1.127  	fun one_fun n (_,[]  ) = /\ "dummy" (funarg(1,n))
   1.128  	|   one_fun n (_,args) = let
   1.129  		val l2 = length args;
   1.130 -		fun idxs m arg = (if is_lazy arg then fn x=> %%:fupN` %%:ID_N`x
   1.131 +		fun idxs m arg = (if is_lazy arg then (fn t => mk_fup (ID, t))
   1.132  					         else I) (Bound(l2-m));
   1.133  		in cont_eta_contract (foldr'' 
   1.134 -			(fn (a,t) => %%:ssplitN`(/\# (a,t)))
   1.135 +			(fn (a,t) => mk_ssplit (/\# (a,t)))
   1.136  			(args,
   1.137  			fn a=> /\#(a,(list_ccomb(funarg(l2,n),mapn idxs 1 args))))
   1.138  			) end;
   1.139  in (if length cons = 1 andalso length(snd(hd cons)) <= 1
   1.140 -    then fn t => %%:strictifyN`t else I)
   1.141 -     (foldr1 (fn (x,y)=> %%:sscaseN`x`y) (mapn one_fun 1 cons)) end;
   1.142 +    then mk_strictify else I)
   1.143 +     (foldr1 mk_sscase (mapn one_fun 1 cons)) end;
   1.144  end; (* struct *)