remove dead code
authorhuffman
Wed Mar 03 08:49:11 2010 -0800 (2010-03-03)
changeset 35562e27550a842b9
parent 35561 b56d5b1b1a55
child 35563 f5ec817df77f
remove dead code
src/HOLCF/Tools/Domain/domain_library.ML
     1.1 --- a/src/HOLCF/Tools/Domain/domain_library.ML	Wed Mar 03 08:26:01 2010 -0800
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_library.ML	Wed Mar 03 08:49:11 2010 -0800
     1.3 @@ -38,14 +38,10 @@
     1.4    val string_of_typ : theory -> typ -> string;
     1.5  
     1.6    (* Creating HOLCF types *)
     1.7 -  val ->> : typ * typ -> typ;
     1.8    val mk_ssumT : typ * typ -> typ;
     1.9    val mk_sprodT : typ * typ -> typ;
    1.10    val mk_uT : typ -> typ;
    1.11    val oneT : typ;
    1.12 -  val mk_maybeT : typ -> typ;
    1.13 -  val mk_ctupleT : typ list -> typ;
    1.14 -  val mk_TFree : string -> typ;
    1.15    val pcpoS : sort;
    1.16  
    1.17    (* Creating HOLCF terms *)
    1.18 @@ -53,21 +49,12 @@
    1.19    val %%: : string -> term;
    1.20    val ` : term * term -> term;
    1.21    val `% : term * string -> term;
    1.22 -  val /\ : string -> term -> term;
    1.23    val UU : term;
    1.24    val ID : term;
    1.25 -  val oo : term * term -> term;
    1.26 -  val mk_ctuple : term list -> term;
    1.27 -  val mk_fix : term -> term;
    1.28 -  val mk_iterate : term * term * term -> term;
    1.29 -  val mk_fail : term;
    1.30 -  val mk_return : term -> term;
    1.31    val list_ccomb : term * term list -> term;
    1.32    val con_app2 : string -> ('a -> term) -> 'a list -> term;
    1.33    val prj : ('a -> 'b -> 'a) -> ('a -> 'b -> 'a) -> 'a -> 'b list -> int -> 'a
    1.34    val proj : term -> 'a list -> int -> term;
    1.35 -  val mk_ctuple_pat : term list -> term;
    1.36 -  val mk_branch : term -> term;
    1.37  
    1.38    (* Creating propositions *)
    1.39    val mk_conj : term * term -> term;
    1.40 @@ -78,7 +65,6 @@
    1.41    val mk_ex : string * term -> term;
    1.42    val mk_constrainall : string * typ * term -> term;
    1.43    val === : term * term -> term;
    1.44 -  val strict : term -> term;
    1.45    val defined : term -> term;
    1.46    val mk_adm : term -> term;
    1.47    val lift : ('a -> term) -> 'a list * term -> term;
    1.48 @@ -88,7 +74,6 @@
    1.49    val mk_trp : term -> term; (* HOLogic.mk_Trueprop *)
    1.50    val == : term * term -> term;
    1.51    val ===> : term * term -> term;
    1.52 -  val ==> : term * term -> term;
    1.53    val mk_All : string * term -> term;
    1.54  
    1.55        (* Domain specifications *)
    1.56 @@ -106,20 +91,9 @@
    1.57    val nonlazy : arg list -> string list;
    1.58    val nonlazy_rec : arg list -> string list;
    1.59    val %# : arg -> term;
    1.60 -  val /\# : arg * term -> term;
    1.61    val bound_arg : ''a list -> ''a -> term; (* ''a = arg or string *)
    1.62    val idx_name : 'a list -> string -> int -> string;
    1.63 -  val app_rec_arg : (int -> term) -> arg -> term;
    1.64    val con_app : string -> arg list -> term;
    1.65 -  val dtyp_of_eq : eq -> Datatype.dtyp;
    1.66 -
    1.67 -
    1.68 -  (* Name mangling *)
    1.69 -  val strip_esc : string -> string;
    1.70 -  val extern_name : string -> string;
    1.71 -  val dis_name : string -> string;
    1.72 -  val mat_name : string -> string;
    1.73 -  val pat_name : string -> string;
    1.74  end;
    1.75  
    1.76  structure Domain_Library :> DOMAIN_LIBRARY =
    1.77 @@ -155,26 +129,6 @@
    1.78  exception Impossible of string;
    1.79  fun Imposs msg = raise Impossible ("Domain:"^msg);
    1.80  
    1.81 -(* ----- name handling ----- *)
    1.82 -
    1.83 -val strip_esc =
    1.84 -    let fun strip ("'" :: c :: cs) = c :: strip cs
    1.85 -          | strip ["'"] = []
    1.86 -          | strip (c :: cs) = c :: strip cs
    1.87 -          | strip [] = [];
    1.88 -    in implode o strip o Symbol.explode end;
    1.89 -
    1.90 -fun extern_name con =
    1.91 -    case Symbol.explode con of 
    1.92 -      ("o"::"p"::" "::rest) => implode rest
    1.93 -    | _ => con;
    1.94 -fun dis_name  con = "is_"^ (extern_name con);
    1.95 -fun dis_name_ con = "is_"^ (strip_esc   con);
    1.96 -fun mat_name  con = "match_"^ (extern_name con);
    1.97 -fun mat_name_ con = "match_"^ (strip_esc   con);
    1.98 -fun pat_name  con = (extern_name con) ^ "_pat";
    1.99 -fun pat_name_ con = (strip_esc   con) ^ "_pat";
   1.100 -
   1.101  fun cpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort cpo});
   1.102  fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort pcpo});
   1.103  fun string_of_typ sg = Syntax.string_of_typ_global sg o Sign.certify_typ sg;
   1.104 @@ -210,36 +164,13 @@
   1.105  fun nonlazy_rec args   = map vname (filter is_nonlazy_rec args);
   1.106  
   1.107  
   1.108 -(* ----- combinators for making dtyps ----- *)
   1.109 -
   1.110 -fun mk_uD T = Datatype_Aux.DtType(@{type_name "u"}, [T]);
   1.111 -fun mk_sprodD (T, U) = Datatype_Aux.DtType(@{type_name sprod}, [T, U]);
   1.112 -fun mk_ssumD (T, U) = Datatype_Aux.DtType(@{type_name ssum}, [T, U]);
   1.113 -fun mk_liftD T = Datatype_Aux.DtType(@{type_name "lift"}, [T]);
   1.114 -val unitD = Datatype_Aux.DtType(@{type_name "unit"}, []);
   1.115 -val boolD = Datatype_Aux.DtType(@{type_name "bool"}, []);
   1.116 -val oneD = mk_liftD unitD;
   1.117 -val trD = mk_liftD boolD;
   1.118 -fun big_sprodD ds = case ds of [] => oneD | _ => foldr1 mk_sprodD ds;
   1.119 -fun big_ssumD ds = case ds of [] => unitD | _ => foldr1 mk_ssumD ds;
   1.120 -
   1.121 -fun dtyp_of_arg ((lazy, D), _) = if lazy then mk_uD D else D;
   1.122 -fun dtyp_of_cons (_, args) = big_sprodD (map dtyp_of_arg args);
   1.123 -fun dtyp_of_eq (_, cons) = big_ssumD (map dtyp_of_cons cons);
   1.124 -
   1.125 -
   1.126  (* ----- support for type and mixfix expressions ----- *)
   1.127  
   1.128  fun mk_uT T = Type(@{type_name "u"}, [T]);
   1.129 -fun mk_cfunT (T, U) = Type(@{type_name cfun}, [T, U]);
   1.130  fun mk_sprodT (T, U) = Type(@{type_name sprod}, [T, U]);
   1.131  fun mk_ssumT (T, U) = Type(@{type_name ssum}, [T, U]);
   1.132  val oneT = @{typ one};
   1.133  
   1.134 -val op ->> = mk_cfunT;
   1.135 -
   1.136 -fun mk_TFree s = TFree ("'" ^ s, @{sort pcpo});
   1.137 -
   1.138  (* ----- support for term expressions ----- *)
   1.139  
   1.140  fun %: s = Free(s,dummyT);
   1.141 @@ -260,7 +191,6 @@
   1.142  fun mk_All  (x,P) = %%:"all" $ mk_lam(x,P); (* meta universal quantification *)
   1.143  
   1.144  infixr 0 ===>;  fun S ===> T = %%:"==>" $ S $ T;
   1.145 -infixr 0 ==>;   fun S ==> T = mk_trp S ===> mk_trp T;
   1.146  infix 0 ==;     fun S ==  T = %%:"==" $ S $ T;
   1.147  infix 1 ===;    fun S === T = %%:"op =" $ S $ T;
   1.148  infix 1 ~=;     fun S ~=  T = HOLogic.mk_not (S === T);
   1.149 @@ -275,42 +205,22 @@
   1.150  fun mk_ssplit t = %%: @{const_name ssplit}`t;
   1.151  fun mk_sscase (x, y) = %%: @{const_name sscase}`x`y;
   1.152  fun mk_fup (t,u) = %%: @{const_name fup} ` t ` u;
   1.153 -val ONE = @{term ONE};
   1.154 -fun mk_iterate (n,f,z) = %%: @{const_name iterate} $ n ` f ` z;
   1.155 -fun mk_fix t = %%: @{const_name fix}`t;
   1.156 -fun mk_return t = %%: @{const_name Fixrec.return}`t;
   1.157 -val mk_fail = %%: @{const_name Fixrec.fail};
   1.158 -
   1.159 -fun mk_branch t = %%: @{const_name Fixrec.branch} $ t;
   1.160  
   1.161  val pcpoS = @{sort pcpo};
   1.162  
   1.163  val list_ccomb = Library.foldl (op `); (* continuous version of list_comb *)
   1.164  fun con_app2 con f args = list_ccomb(%%:con,map f args);
   1.165  fun con_app con = con_app2 con %#;
   1.166 -fun if_rec  arg f y   = if is_rec arg then f (rec_of arg) else y;
   1.167 -fun app_rec_arg p arg = if_rec arg (fn n => fn x => (p n)`x) I (%# arg);
   1.168  fun prj _  _  x (   _::[]) _ = x
   1.169    | prj f1 _  x (_::y::ys) 0 = f1 x y
   1.170    | prj f1 f2 x (y::   ys) j = prj f1 f2 (f2 x y) ys (j-1);
   1.171  fun  proj x      = prj (fn S => K(%%:"fst" $S)) (fn S => K(%%:"snd" $S)) x;
   1.172  fun lift tfn = Library.foldr (fn (x,t)=> (mk_trp(tfn x) ===> t));
   1.173  
   1.174 -fun /\ v T = %%: @{const_name Abs_CFun} $ mk_lam(v,T);
   1.175 -fun /\# (arg,T) = /\ (vname arg) T;
   1.176 -infixr 9 oo; fun S oo T = %%: @{const_name cfcomp}`S`T;
   1.177  val UU = %%: @{const_name UU};
   1.178 -fun strict f = f`UU === UU;
   1.179  fun defined t = t ~= UU;
   1.180  fun cpair (t,u) = %%: @{const_name Pair} $ t $ u;
   1.181  fun spair (t,u) = %%: @{const_name spair}`t`u;
   1.182 -fun mk_ctuple [] = HOLogic.unit (* used in match_defs *)
   1.183 -  | mk_ctuple ts = foldr1 cpair ts;
   1.184 -fun mk_ctupleT [] = HOLogic.unitT   (* used in match_defs *)
   1.185 -  | mk_ctupleT Ts = foldr1 HOLogic.mk_prodT Ts;
   1.186 -fun mk_maybeT T = Type ("Fixrec.maybe",[T]);
   1.187 -fun cpair_pat (p1,p2) = %%: @{const_name cpair_pat} $ p1 $ p2;
   1.188 -val mk_ctuple_pat = foldr1 cpair_pat;
   1.189  fun lift_defined f = lift (fn x => defined (f x));
   1.190  fun bound_arg vns v = Bound (length vns - find_index (fn v' => v' = v) vns - 1);
   1.191