src/HOLCF/domain/library.ML
author wenzelm
Thu Jul 14 19:28:24 2005 +0200 (2005-07-14)
changeset 16842 5979c46853d1
parent 16778 2162c0de4673
child 17325 d9d50222808e
permissions -rw-r--r--
tuned;
     1 (*  Title:      HOLCF/domain/library.ML
     2     ID:         $Id$
     3     Author:     David von Oheimb
     4 
     5 Library for domain section.
     6 *)
     7 
     8 
     9 (* ----- general support ---------------------------------------------------- *)
    10 
    11 fun mapn f n []      = []
    12 |   mapn f n (x::xs) = (f n x) :: mapn f (n+1) xs;
    13 
    14 fun foldr'' f (l,f2) = let fun itr []  = raise Fail "foldr''"
    15 			     | itr [a] = f2 a
    16 			     | itr (a::l) = f(a, itr l)
    17 in  itr l  end;
    18 fun foldr' f l = foldr'' f (l,I);
    19 fun map_cumulr f start xs = foldr (fn (x,(ys,res))=>case f(x,res) of (y,res2) =>
    20 						  (y::ys,res2)) ([],start) xs;
    21 
    22 
    23 fun first  (x,_,_) = x; fun second (_,x,_) = x; fun third  (_,_,x) = x;
    24 fun upd_first  f (x,y,z) = (f x,   y,   z);
    25 fun upd_second f (x,y,z) = (  x, f y,   z);
    26 fun upd_third  f (x,y,z) = (  x,   y, f z);
    27 
    28 fun atomize thm = let val r_inst = read_instantiate;
    29     fun at  thm = case concl_of thm of
    30       _$(Const("op &",_)$_$_)       => at(thm RS conjunct1)@at(thm RS conjunct2)
    31     | _$(Const("All" ,_)$Abs(s,_,_))=> at(thm RS (r_inst [("x","?"^s)] spec))
    32     | _				    => [thm];
    33 in map zero_var_indexes (at thm) end;
    34 
    35 (* ----- specific support for domain ---------------------------------------- *)
    36 
    37 structure Domain_Library = struct
    38 
    39 open HOLCFLogic;
    40 
    41 exception Impossible of string;
    42 fun Imposs msg = raise Impossible ("Domain:"^msg);
    43 
    44 (* ----- name handling ----- *)
    45 
    46 val strip_esc = let fun strip ("'" :: c :: cs) = c :: strip cs
    47 		    |   strip ["'"] = []
    48 		    |   strip (c :: cs) = c :: strip cs
    49 		    |   strip [] = [];
    50 in implode o strip o Symbol.explode end;
    51 
    52 fun extern_name con = case Symbol.explode con of 
    53 		   ("o"::"p"::" "::rest) => implode rest
    54 		   | _ => con;
    55 fun dis_name  con = "is_"^ (extern_name con);
    56 fun dis_name_ con = "is_"^ (strip_esc   con);
    57 fun mat_name  con = "match_"^ (extern_name con);
    58 fun mat_name_ con = "match_"^ (strip_esc   con);
    59 
    60 (* make distinct names out of the type list, 
    61    forbidding "o","n..","x..","f..","P.." as names *)
    62 (* a number string is added if necessary *)
    63 fun mk_var_names ids : string list = let
    64     fun nonreserved s = if s mem ["n","x","f","P"] then s^"'" else s;
    65     fun index_vnames(vn::vns,occupied) =
    66           (case assoc(occupied,vn) of
    67              NONE => if vn mem vns
    68                      then (vn^"1") :: index_vnames(vns,(vn,1)  ::occupied)
    69                      else  vn      :: index_vnames(vns,          occupied)
    70            | SOME(i) => (vn^(string_of_int (i+1)))
    71 				   :: index_vnames(vns,(vn,i+1)::occupied))
    72       | index_vnames([],occupied) = [];
    73 in index_vnames(map nonreserved ids, [("O",0),("o",0)]) end;
    74 
    75 fun rep_Type  (Type  x) = x | rep_Type  _ = Imposs "library:rep_Type";
    76 fun rep_TFree (TFree x) = x | rep_TFree _ = Imposs "library:rep_TFree";
    77 
    78 fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, pcpoS);
    79 fun string_of_typ sg = Sign.string_of_typ sg o Sign.certify_typ sg;
    80 fun str2typ sg = typ_of o read_ctyp sg;
    81 
    82 (* ----- constructor list handling ----- *)
    83 
    84 type cons = (string *			(* operator name of constr *)
    85 	    ((bool*int)*		(*  (lazy,recursive element or ~1) *)
    86 	      string option*		(*   selector name    *)
    87 	      string)			(*   argument name    *)
    88 	    list);			(* argument list      *)
    89 type eq = (string *		(* name      of abstracted type *)
    90 	   typ list) *		(* arguments of abstracted type *)
    91 	  cons list;		(* represented type, as a constructor list *)
    92 
    93 fun rec_of arg  = snd (first arg);
    94 fun is_lazy arg = fst (first arg);
    95 val sel_of    =       second;
    96 val     vname =       third;
    97 val upd_vname =   upd_third;
    98 fun is_rec         arg = rec_of arg >=0;
    99 fun is_nonlazy_rec arg = is_rec arg andalso not (is_lazy arg);
   100 fun nonlazy     args   = map vname (filter_out is_lazy    args);
   101 fun nonlazy_rec args   = map vname (List.filter is_nonlazy_rec args);
   102 
   103 (* ----- qualified names of HOLCF constants ----- *)
   104 
   105 val lessN      = "Porder.op <<"
   106 val UU_N       = "Pcpo.UU";
   107 val admN       = "Adm.adm";
   108 val Rep_CFunN  = "Cfun.Rep_CFun";
   109 val Abs_CFunN  = "Cfun.Abs_CFun";
   110 val ID_N       = "Cfun.ID";
   111 val cfcompN    = "Cfun.cfcomp";
   112 val strictifyN = "Cfun.strictify";
   113 val cpairN     = "Cprod.cpair";
   114 val cfstN      = "Cprod.cfst";
   115 val csndN      = "Cprod.csnd";
   116 val csplitN    = "Cprod.csplit";
   117 val spairN     = "Sprod.spair";
   118 val sfstN      = "Sprod.sfst";
   119 val ssndN      = "Sprod.ssnd";
   120 val ssplitN    = "Sprod.ssplit";
   121 val sinlN      = "Ssum.sinl";
   122 val sinrN      = "Ssum.sinr";
   123 val sscaseN    = "Ssum.sscase";
   124 val upN        = "Up.up";
   125 val fupN       = "Up.fup";
   126 val ONE_N      = "One.ONE";
   127 val TT_N       = "Tr.TT";
   128 val FF_N       = "Tr.FF";
   129 val iterateN   = "Fix.iterate";
   130 val fixN       = "Fix.fix";
   131 val returnN    = "Fixrec.return";
   132 val failN      = "Fixrec.fail";
   133 
   134 val pcpoN      = "Pcpo.pcpo"
   135 val pcpoS      = [pcpoN];
   136 
   137 (* ----- support for type and mixfix expressions ----- *)
   138 
   139 infixr 5 -->;
   140 
   141 (* ----- support for term expressions ----- *)
   142 
   143 fun %: s = Free(s,dummyT);
   144 fun %# arg = %:(vname arg);
   145 fun %%: s = Const(s,dummyT);
   146 
   147 local open HOLogic in
   148 val mk_trp = mk_Trueprop;
   149 fun mk_conj (S,T) = conj $ S $ T;
   150 fun mk_disj (S,T) = disj $ S $ T;
   151 fun mk_imp  (S,T) = imp  $ S $ T;
   152 fun mk_lam  (x,T) = Abs(x,dummyT,T);
   153 fun mk_all  (x,P) = HOLogic.mk_all (x,dummyT,P);
   154 fun mk_ex   (x,P) = mk_exists (x,dummyT,P);
   155 local 
   156 		    fun sg [s]     = %:s
   157 		    |   sg (s::ss) = %%:"_classes" $ %:s $ sg ss
   158 	 	    |   sg _       = Imposs "library:sg";
   159 		    fun sf [] = %%:"_emptysort"
   160 		    |   sf s  = %%:"_sort" $ sg s
   161 		    fun tf (Type (s,args)) = Library.foldl (op $) (%:s,map tf args)
   162 		    |   tf (TFree(s,sort)) = %%:"_ofsort" $ %:s $ sf sort
   163 		    |   tf _               = Imposs "library:tf";
   164 in
   165 fun mk_constrain      (typ,T) = %%:"_constrain" $ T $ tf typ;
   166 fun mk_constrainall (x,typ,P) = %%:"All" $ (%%:"_constrainAbs" $ mk_lam(x,P) $ tf typ);
   167 end;
   168 end;
   169 
   170 fun mk_All  (x,P) = %%:"all" $ mk_lam(x,P); (* meta universal quantification *)
   171 
   172 infixr 0 ===>;  fun S ===> T = %%:"==>" $ S $ T;
   173 infixr 0 ==>;   fun S ==> T = mk_trp S ===> mk_trp T;
   174 infix 0 ==;     fun S ==  T = %%:"==" $ S $ T;
   175 infix 1 ===;    fun S === T = %%:"op =" $ S $ T;
   176 infix 1 ~=;     fun S ~=  T = HOLogic.mk_not (S === T);
   177 infix 1 <<;     fun S <<  T = %%:lessN $ S $ T;
   178 infix 1 ~<<;    fun S ~<< T = HOLogic.mk_not (S << T);
   179 
   180 infix 9 `  ; fun f`  x = %%:Rep_CFunN $ f $ x;
   181 infix 9 `% ; fun f`% s = f` %: s;
   182 infix 9 `%%; fun f`%%s = f` %%:s;
   183 fun mk_cRep_CFun (F,As) = Library.foldl (op `) (F,As);
   184 fun con_app2 con f args = mk_cRep_CFun(%%:con,map f args);
   185 fun con_app con = con_app2 con %#;
   186 fun if_rec  arg f y   = if is_rec arg then f (rec_of arg) else y;
   187 fun app_rec_arg p arg = if_rec arg (fn n => fn x => (p n)`x) I (%# arg);
   188 fun prj _  _  x (   _::[]) _ = x
   189 |   prj f1 _  x (_::y::ys) 0 = f1 x y
   190 |   prj f1 f2 x (y::   ys) j = prj f1 f2 (f2 x y) ys (j-1);
   191 fun fix_tp (tn, args) = (tn, map (K oneT) args); (* instantiate type to
   192 						    avoid type varaibles *)
   193 fun  proj x      = prj (fn S => K(%%:"fst" $S)) (fn S => K(%%:"snd" $S)) x;
   194 fun cproj x      = prj (fn S => K(%%:cfstN`S)) (fn S => K(%%:csndN`S)) x;
   195 fun prj' _  _  x (   _::[]) _ = x
   196 |   prj' f1 _  x (_::   ys) 0 = f1 x (foldr' HOLogic.mk_prodT ys)
   197 |   prj' f1 f2 x (y::   ys) j = prj' f1 f2 (f2 x y) ys (j-1);
   198 fun cproj' T eqs = prj'
   199 	(fn S => fn t => Const(cfstN, HOLogic.mk_prodT(dummyT,t)->>dummyT)`S)
   200 	(fn S => fn t => Const(csndN, HOLogic.mk_prodT(t,dummyT)->>dummyT)`S) 
   201 		       T (map ((fn tp => tp ->> tp) o Type o fix_tp o fst) eqs);
   202 fun lift tfn = Library.foldr (fn (x,t)=> (mk_trp(tfn x) ===> t));
   203 
   204 fun /\ v T = %%:Abs_CFunN $ mk_lam(v,T);
   205 fun /\# (arg,T) = /\ (vname arg) T;
   206 infixr 9 oo; fun S oo T = %%:cfcompN`S`T;
   207 val UU = %%:UU_N;
   208 fun strict f = f`UU === UU;
   209 fun defined t = t ~= UU;
   210 fun cpair (S,T) = %%:cpairN`S`T;
   211 fun mk_ctuple [] = HOLogic.unit (* used in match_defs *)
   212 |   mk_ctuple (t::[]) = t
   213 |   mk_ctuple (t::ts) = cpair (t, mk_ctuple ts);
   214 fun mk_ctupleT [] = HOLogic.unitT   (* used in match_defs *)
   215 |   mk_ctupleT (T::[]) = T
   216 |   mk_ctupleT (T::Ts) = HOLogic.mk_prodT(T, mk_ctupleT Ts);
   217 fun lift_defined f = lift (fn x => defined (f x));
   218 fun bound_arg vns v = Bound(length vns -find_index_eq v vns -1);
   219 
   220 fun cont_eta_contract (Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body)) = 
   221       (case cont_eta_contract body  of
   222         body' as (Const("Cfun.Rep_CFun",Ta) $ f $ Bound 0) => 
   223 	  if not (0 mem loose_bnos f) then incr_boundvars ~1 f 
   224 	  else   Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body')
   225       | body' => Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body'))
   226 |   cont_eta_contract(f$t) = cont_eta_contract f $ cont_eta_contract t
   227 |   cont_eta_contract t    = t;
   228 
   229 fun idx_name dnames s n = s^(if length dnames = 1 then "" else string_of_int n);
   230 fun when_funs cons = if length cons = 1 then ["f"] 
   231                      else mapn (fn n => K("f"^(string_of_int n))) 1 cons;
   232 fun when_body cons funarg = let
   233 	fun one_fun n (_,[]  ) = /\ "dummy" (funarg(1,n))
   234 	|   one_fun n (_,args) = let
   235 		val l2 = length args;
   236 		fun idxs m arg = (if is_lazy arg then fn x=> %%:fupN` %%:ID_N`x
   237 					         else I) (Bound(l2-m));
   238 		in cont_eta_contract (foldr'' 
   239 			(fn (a,t) => %%:ssplitN`(/\# (a,t)))
   240 			(args,
   241 			fn a=> /\#(a,(mk_cRep_CFun(funarg(l2,n),mapn idxs 1 args))))
   242 			) end;
   243 in (if length cons = 1 andalso length(snd(hd cons)) <= 1
   244     then fn t => %%:strictifyN`t else I)
   245      (foldr' (fn (x,y)=> %%:sscaseN`x`y) (mapn one_fun 1 cons)) end;
   246 end; (* struct *)