use qualified names for all constants
authorhuffman
Tue Jul 12 18:28:36 2005 +0200 (2005-07-12)
changeset 167782162c0de4673
parent 16777 555c8951f05c
child 16779 ac1dc3d4746a
use qualified names for all constants
src/HOLCF/domain/axioms.ML
src/HOLCF/domain/library.ML
src/HOLCF/domain/theorems.ML
     1.1 --- a/src/HOLCF/domain/axioms.ML	Tue Jul 12 18:26:44 2005 +0200
     1.2 +++ b/src/HOLCF/domain/axioms.ML	Tue Jul 12 18:28:36 2005 +0200
     1.3 @@ -35,14 +35,14 @@
     1.4  				Bound(1+length cons+x-y)))`(dc_rep`Bound 0))) (when_funs cons));
     1.5  
     1.6    fun con_def outer recu m n (_,args) = let
     1.7 -     fun idxs z x arg = (if is_lazy arg then fn t => %%:"up"`t else Id)
     1.8 +     fun idxs z x arg = (if is_lazy arg then fn t => %%:upN`t else Id)
     1.9  			(if recu andalso is_rec arg then (cproj (Bound z) eqs
    1.10  				  (rec_of arg))`Bound(z-x) else Bound(z-x));
    1.11 -     fun parms [] = %%:"ONE"
    1.12 -     |   parms vs = foldr'(fn(x,t)=> %%:"spair"`x`t)(mapn (idxs(length vs))1 vs);
    1.13 +     fun parms [] = %%:ONE_N
    1.14 +     |   parms vs = foldr'(fn(x,t)=> %%:spairN`x`t)(mapn (idxs(length vs))1 vs);
    1.15       fun inj y 1 _ = y
    1.16 -     |   inj y _ 0 = %%:"sinl"`y
    1.17 -     |   inj y i j = %%:"sinr"`(inj y (i-1) (j-1));
    1.18 +     |   inj y _ 0 = %%:sinlN`y
    1.19 +     |   inj y i j = %%:sinrN`(inj y (i-1) (j-1));
    1.20    in foldr /\# (outer (inj (parms args) m n)) args end;
    1.21  
    1.22    val copy_def = ("copy_def", %%:(dname^"_copy") == /\"f" (dc_abs oo 
    1.23 @@ -58,30 +58,32 @@
    1.24  	fun ddef (con,_) = (dis_name con ^"_def",%%:(dis_name con) == 
    1.25  		 mk_cRep_CFun(%%:(dname^"_when"),map 
    1.26  			(fn (con',args) => (foldr /\#
    1.27 -			   (if con'=con then %%:"TT" else %%:"FF") args)) cons))
    1.28 +			   (if con'=con then %%:TT_N else %%:FF_N) args)) cons))
    1.29  	in map ddef cons end;
    1.30  
    1.31    val mat_defs = let
    1.32  	fun mdef (con,_) = (mat_name con ^"_def",%%:(mat_name con) == 
    1.33  		 mk_cRep_CFun(%%:(dname^"_when"),map 
    1.34  			(fn (con',args) => (foldr /\#
    1.35 -			   (if con'=con then (%%:"return")`(mk_ctuple (map (bound_arg args) args)) else %%:"fail") args)) cons))
    1.36 +			   (if con'=con
    1.37 +                               then %%:returnN`(mk_ctuple (map (bound_arg args) args))
    1.38 +                               else %%:failN) args)) cons))
    1.39  	in map mdef cons end;
    1.40  
    1.41    val sel_defs = let
    1.42  	fun sdef con n arg = Option.map (fn sel => (sel^"_def",%%:sel == 
    1.43  		 mk_cRep_CFun(%%:(dname^"_when"),map 
    1.44 -			(fn (con',args) => if con'<>con then %%:"UU" else
    1.45 +			(fn (con',args) => if con'<>con then UU else
    1.46  			 foldr /\# (Bound (length args - n)) args) cons))) (sel_of arg);
    1.47  	in List.mapPartial Id (List.concat(map (fn (con,args) => mapn (sdef con) 1 args) cons)) end;
    1.48  
    1.49  
    1.50  (* ----- axiom and definitions concerning induction ------------------------- *)
    1.51  
    1.52 -  val reach_ax = ("reach", mk_trp(cproj (%%:"fix"`%%(comp_dname^"_copy")) eqs n
    1.53 +  val reach_ax = ("reach", mk_trp(cproj (%%:fixN`%%(comp_dname^"_copy")) eqs n
    1.54  					`%x_name === %:x_name));
    1.55    val take_def = ("take_def",%%:(dname^"_take") == mk_lam("n",cproj' 
    1.56 -	     (%%:"iterate" $ Bound 0 $ %%:(comp_dname^"_copy") $ %%:"UU") eqs n));
    1.57 +	     (%%:iterateN $ Bound 0 $ %%:(comp_dname^"_copy") $ UU) eqs n));
    1.58    val finite_def = ("finite_def",%%:(dname^"_finite") == mk_lam(x_name,
    1.59  	mk_ex("n",(%%:(dname^"_take") $ Bound 0)`Bound 1 === Bound 1)));
    1.60  
     2.1 --- a/src/HOLCF/domain/library.ML	Tue Jul 12 18:26:44 2005 +0200
     2.2 +++ b/src/HOLCF/domain/library.ML	Tue Jul 12 18:28:36 2005 +0200
     2.3 @@ -102,6 +102,40 @@
     2.4  fun nonlazy     args   = map vname (filter_out is_lazy    args);
     2.5  fun nonlazy_rec args   = map vname (List.filter is_nonlazy_rec args);
     2.6  
     2.7 +(* ----- qualified names of HOLCF constants ----- *)
     2.8 +
     2.9 +val lessN      = "Porder.op <<"
    2.10 +val UU_N       = "Pcpo.UU";
    2.11 +val admN       = "Adm.adm";
    2.12 +val Rep_CFunN  = "Cfun.Rep_CFun";
    2.13 +val Abs_CFunN  = "Cfun.Abs_CFun";
    2.14 +val ID_N       = "Cfun.ID";
    2.15 +val cfcompN    = "Cfun.cfcomp";
    2.16 +val strictifyN = "Cfun.strictify";
    2.17 +val cpairN     = "Cprod.cpair";
    2.18 +val cfstN      = "Cprod.cfst";
    2.19 +val csndN      = "Cprod.csnd";
    2.20 +val csplitN    = "Cprod.csplit";
    2.21 +val spairN     = "Sprod.spair";
    2.22 +val sfstN      = "Sprod.sfst";
    2.23 +val ssndN      = "Sprod.ssnd";
    2.24 +val ssplitN    = "Sprod.ssplit";
    2.25 +val sinlN      = "Ssum.sinl";
    2.26 +val sinrN      = "Ssum.sinr";
    2.27 +val sscaseN    = "Ssum.sscase";
    2.28 +val upN        = "Up.up";
    2.29 +val fupN       = "Up.fup";
    2.30 +val ONE_N      = "One.ONE";
    2.31 +val TT_N       = "Tr.TT";
    2.32 +val FF_N       = "Tr.FF";
    2.33 +val iterateN   = "Fix.iterate";
    2.34 +val fixN       = "Fix.fix";
    2.35 +val returnN    = "Fixrec.return";
    2.36 +val failN      = "Fixrec.fail";
    2.37 +
    2.38 +val pcpoN      = "Pcpo.pcpo"
    2.39 +val pcpoS      = [pcpoN];
    2.40 +
    2.41  (* ----- support for type and mixfix expressions ----- *)
    2.42  
    2.43  infixr 5 -->;
    2.44 @@ -119,6 +153,7 @@
    2.45  fun mk_imp  (S,T) = imp  $ S $ T;
    2.46  fun mk_lam  (x,T) = Abs(x,dummyT,T);
    2.47  fun mk_all  (x,P) = HOLogic.mk_all (x,dummyT,P);
    2.48 +fun mk_ex   (x,P) = mk_exists (x,dummyT,P);
    2.49  local 
    2.50  		    fun sg [s]     = %:s
    2.51  		    |   sg (s::ss) = %%:"_classes" $ %:s $ sg ss
    2.52 @@ -132,20 +167,19 @@
    2.53  fun mk_constrain      (typ,T) = %%:"_constrain" $ T $ tf typ;
    2.54  fun mk_constrainall (x,typ,P) = %%:"All" $ (%%:"_constrainAbs" $ mk_lam(x,P) $ tf typ);
    2.55  end;
    2.56 -fun mk_ex   (x,P) = mk_exists (x,dummyT,P);
    2.57  end;
    2.58  
    2.59  fun mk_All  (x,P) = %%:"all" $ mk_lam(x,P); (* meta universal quantification *)
    2.60  
    2.61 -infixr 0 ===>;fun S ===> T = %%:"==>" $ S $ T;
    2.62 -infixr 0 ==>;fun S ==> T = mk_trp S ===> mk_trp T;
    2.63 -infix 0 ==;  fun S ==  T = %%:"==" $ S $ T;
    2.64 -infix 1 ===; fun S === T = %%:"op =" $ S $ T;
    2.65 -infix 1 ~=;  fun S ~=  T = mk_not (S === T);
    2.66 -infix 1 <<;  fun S <<  T = %%:"op <<" $ S $ T;
    2.67 -infix 1 ~<<; fun S ~<< T = mk_not (S << T);
    2.68 +infixr 0 ===>;  fun S ===> T = %%:"==>" $ S $ T;
    2.69 +infixr 0 ==>;   fun S ==> T = mk_trp S ===> mk_trp T;
    2.70 +infix 0 ==;     fun S ==  T = %%:"==" $ S $ T;
    2.71 +infix 1 ===;    fun S === T = %%:"op =" $ S $ T;
    2.72 +infix 1 ~=;     fun S ~=  T = mk_not (S === T);
    2.73 +infix 1 <<;     fun S <<  T = %%:lessN $ S $ T;
    2.74 +infix 1 ~<<;    fun S ~<< T = mk_not (S << T);
    2.75  
    2.76 -infix 9 `  ; fun f`  x = %%:"Rep_CFun" $ f $ x;
    2.77 +infix 9 `  ; fun f`  x = %%:Rep_CFunN $ f $ x;
    2.78  infix 9 `% ; fun f`% s = f` %: s;
    2.79  infix 9 `%%; fun f`%%s = f` %%:s;
    2.80  fun mk_cRep_CFun (F,As) = Library.foldl (op `) (F,As);
    2.81 @@ -159,24 +193,24 @@
    2.82  fun fix_tp (tn, args) = (tn, map (K oneT) args); (* instantiate type to
    2.83  						    avoid type varaibles *)
    2.84  fun  proj x      = prj (fn S => K(%%:"fst" $S)) (fn S => K(%%:"snd" $S)) x;
    2.85 -fun cproj x      = prj (fn S => K(%%:"cfst"`S)) (fn S => K(%%:"csnd"`S)) x;
    2.86 +fun cproj x      = prj (fn S => K(%%:cfstN`S)) (fn S => K(%%:csndN`S)) x;
    2.87  fun prj' _  _  x (   _::[]) _ = x
    2.88  |   prj' f1 _  x (_::   ys) 0 = f1 x (foldr' mk_prodT ys)
    2.89  |   prj' f1 f2 x (y::   ys) j = prj' f1 f2 (f2 x y) ys (j-1);
    2.90  fun cproj' T eqs = prj'
    2.91 -	(fn S => fn t => Const("cfst",mk_prodT(dummyT,t)->>dummyT)`S)
    2.92 -	(fn S => fn t => Const("csnd",mk_prodT(t,dummyT)->>dummyT)`S) 
    2.93 +	(fn S => fn t => Const(cfstN,mk_prodT(dummyT,t)->>dummyT)`S)
    2.94 +	(fn S => fn t => Const(csndN,mk_prodT(t,dummyT)->>dummyT)`S) 
    2.95  		       T (map ((fn tp => tp ->> tp) o Type o fix_tp o fst) eqs);
    2.96  fun lift tfn = Library.foldr (fn (x,t)=> (mk_trp(tfn x) ===> t));
    2.97  
    2.98 -fun /\ v T = %%:"Abs_CFun" $ mk_lam(v,T);
    2.99 +fun /\ v T = %%:Abs_CFunN $ mk_lam(v,T);
   2.100  fun /\# (arg,T) = /\ (vname arg) T;
   2.101 -infixr 9 oo; fun S oo T = %%:"cfcomp"`S`T;
   2.102 -val UU = %%:"UU";
   2.103 +infixr 9 oo; fun S oo T = %%:cfcompN`S`T;
   2.104 +val UU = %%:UU_N;
   2.105  fun strict f = f`UU === UU;
   2.106  fun defined t = t ~= UU;
   2.107 -fun cpair (S,T) = %%:"cpair"`S`T;
   2.108 -fun mk_ctuple [] = %%:"UU" (* used in match_defs *)
   2.109 +fun cpair (S,T) = %%:cpairN`S`T;
   2.110 +fun mk_ctuple [] = HOLogic.unit (* used in match_defs *)
   2.111  |   mk_ctuple (t::[]) = t
   2.112  |   mk_ctuple (t::ts) = cpair (t, mk_ctuple ts);
   2.113  fun mk_ctupleT [] = HOLogic.unitT   (* used in match_defs *)
   2.114 @@ -185,12 +219,12 @@
   2.115  fun lift_defined f = lift (fn x => defined (f x));
   2.116  fun bound_arg vns v = Bound(length vns -find_index_eq v vns -1);
   2.117  
   2.118 -fun cont_eta_contract (Const("Abs_CFun",TT) $ Abs(a,T,body)) = 
   2.119 +fun cont_eta_contract (Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body)) = 
   2.120        (case cont_eta_contract body  of
   2.121 -        body' as (Const("Rep_CFun",Ta) $ f $ Bound 0) => 
   2.122 +        body' as (Const("Cfun.Rep_CFun",Ta) $ f $ Bound 0) => 
   2.123  	  if not (0 mem loose_bnos f) then incr_boundvars ~1 f 
   2.124 -	  else   Const("Abs_CFun",TT) $ Abs(a,T,body')
   2.125 -      | body' => Const("Abs_CFun",TT) $ Abs(a,T,body'))
   2.126 +	  else   Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body')
   2.127 +      | body' => Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body'))
   2.128  |   cont_eta_contract(f$t) = cont_eta_contract f $ cont_eta_contract t
   2.129  |   cont_eta_contract t    = t;
   2.130  
   2.131 @@ -201,14 +235,14 @@
   2.132  	fun one_fun n (_,[]  ) = /\ "dummy" (funarg(1,n))
   2.133  	|   one_fun n (_,args) = let
   2.134  		val l2 = length args;
   2.135 -		fun idxs m arg = (if is_lazy arg then fn x=> %%:"fup"`%%"ID"`x
   2.136 +		fun idxs m arg = (if is_lazy arg then fn x=> %%:fupN` %%:ID_N`x
   2.137  					         else Id) (Bound(l2-m));
   2.138  		in cont_eta_contract (foldr'' 
   2.139 -			(fn (a,t) => %%:"ssplit"`(/\# (a,t)))
   2.140 +			(fn (a,t) => %%:ssplitN`(/\# (a,t)))
   2.141  			(args,
   2.142  			fn a=> /\#(a,(mk_cRep_CFun(funarg(l2,n),mapn idxs 1 args))))
   2.143  			) end;
   2.144  in (if length cons = 1 andalso length(snd(hd cons)) <= 1
   2.145 -    then fn t => %%:"strictify"`t else Id)
   2.146 -     (foldr' (fn (x,y)=> %%:"sscase"`x`y) (mapn one_fun 1 cons)) end;
   2.147 +    then fn t => %%:strictifyN`t else Id)
   2.148 +     (foldr' (fn (x,y)=> %%:sscaseN`x`y) (mapn one_fun 1 cons)) end;
   2.149  end; (* struct *)
     3.1 --- a/src/HOLCF/domain/theorems.ML	Tue Jul 12 18:26:44 2005 +0200
     3.2 +++ b/src/HOLCF/domain/theorems.ML	Tue Jul 12 18:28:36 2005 +0200
     3.3 @@ -114,7 +114,7 @@
     3.4  val con_appls = map appl_of_def axs_con_def;
     3.5  
     3.6  local
     3.7 -  fun arg2typ n arg = let val t = TVar (("'a",n),["Pcpo.pcpo"])
     3.8 +  fun arg2typ n arg = let val t = TVar (("'a",n),pcpoS)
     3.9                        in (n+1, if is_lazy arg then mk_uT t else t) end;
    3.10    fun args2typ n [] = (n,oneT)
    3.11    |   args2typ n [arg] = arg2typ n arg
    3.12 @@ -177,7 +177,7 @@
    3.13    val dis_apps = let fun one_dis c (con,args)= pg axs_dis_def
    3.14                     (lift_defined %: (nonlazy args,
    3.15                          (mk_trp((%%:(dis_name c))`(con_app con args) ===
    3.16 -                              %%:(if con=c then "TT" else "FF"))))) [
    3.17 +                              %%:(if con=c then TT_N else FF_N))))) [
    3.18                                  asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
    3.19          in List.concat(map (fn (c,_) => map (one_dis c) cons) cons) end;
    3.20    val dis_defins = map (fn (con,args) => pg [] (defined(%:x_name) ==> 
    3.21 @@ -195,8 +195,10 @@
    3.22    val mat_apps = let fun one_mat c (con,args)= pg axs_mat_def
    3.23                     (lift_defined %: (nonlazy args,
    3.24                          (mk_trp((%%:(mat_name c))`(con_app con args) ===
    3.25 -                              (if con=c then (%%:"return")`(mk_ctuple (map %# args)) else %%:"fail"))))) [
    3.26 -                                asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
    3.27 +                              (if con=c
    3.28 +                                  then %%:returnN`(mk_ctuple (map %# args))
    3.29 +                                  else %%:failN)))))
    3.30 +                   [asm_simp_tac (HOLCF_ss addsimps when_rews) 1];
    3.31          in List.concat(map (fn (c,_) => map (one_mat c) cons) cons) end;
    3.32  in mat_stricts @ mat_apps end;
    3.33  
    3.34 @@ -542,7 +544,7 @@
    3.35  ) end (* let *) else
    3.36    (mapn (fn n => fn dn => read_instantiate_sg (sign_of thy) 
    3.37                      [("P",dn^"_finite "^x_name n)] excluded_middle) 1 dnames,
    3.38 -   pg'' thy [] (Library.foldr (op ===>) (mapn (fn n => K(mk_trp(%%:"adm" $ %:(P_name n))))
    3.39 +   pg'' thy [] (Library.foldr (op ===>) (mapn (fn n => K(mk_trp(%%:admN $ %:(P_name n))))
    3.40                 1 dnames, ind_term (fn n => fn dn => %:(P_name n) $ %:(x_name n))))
    3.41                     (fn prems => map (fn ax_reach => rtac (ax_reach RS subst) 1) 
    3.42                                      axs_reach @ [