# HG changeset patch # User huffman # Date 1267634951 28800 # Node ID e27550a842b99fdf92db086b5c42eabeb4e7f5f0 # Parent b56d5b1b1a558525b3177c61c97be7a8919f5b8b remove dead code diff -r b56d5b1b1a55 -r e27550a842b9 src/HOLCF/Tools/Domain/domain_library.ML --- a/src/HOLCF/Tools/Domain/domain_library.ML Wed Mar 03 08:26:01 2010 -0800 +++ b/src/HOLCF/Tools/Domain/domain_library.ML Wed Mar 03 08:49:11 2010 -0800 @@ -38,14 +38,10 @@ val string_of_typ : theory -> typ -> string; (* Creating HOLCF types *) - val ->> : typ * typ -> typ; val mk_ssumT : typ * typ -> typ; val mk_sprodT : typ * typ -> typ; val mk_uT : typ -> typ; val oneT : typ; - val mk_maybeT : typ -> typ; - val mk_ctupleT : typ list -> typ; - val mk_TFree : string -> typ; val pcpoS : sort; (* Creating HOLCF terms *) @@ -53,21 +49,12 @@ val %%: : string -> term; val ` : term * term -> term; val `% : term * string -> term; - val /\ : string -> term -> term; val UU : term; val ID : term; - val oo : term * term -> term; - val mk_ctuple : term list -> term; - val mk_fix : term -> term; - val mk_iterate : term * term * term -> term; - val mk_fail : term; - val mk_return : term -> term; val list_ccomb : term * term list -> term; val con_app2 : string -> ('a -> term) -> 'a list -> term; val prj : ('a -> 'b -> 'a) -> ('a -> 'b -> 'a) -> 'a -> 'b list -> int -> 'a val proj : term -> 'a list -> int -> term; - val mk_ctuple_pat : term list -> term; - val mk_branch : term -> term; (* Creating propositions *) val mk_conj : term * term -> term; @@ -78,7 +65,6 @@ val mk_ex : string * term -> term; val mk_constrainall : string * typ * term -> term; val === : term * term -> term; - val strict : term -> term; val defined : term -> term; val mk_adm : term -> term; val lift : ('a -> term) -> 'a list * term -> term; @@ -88,7 +74,6 @@ val mk_trp : term -> term; (* HOLogic.mk_Trueprop *) val == : term * term -> term; val ===> : term * term -> term; - val ==> : term * term -> term; val mk_All : string * term -> term; (* Domain specifications *) @@ -106,20 +91,9 @@ val nonlazy : arg list -> string list; val nonlazy_rec : arg list -> string list; val %# : arg -> term; - val /\# : arg * term -> term; val bound_arg : ''a list -> ''a -> term; (* ''a = arg or string *) val idx_name : 'a list -> string -> int -> string; - val app_rec_arg : (int -> term) -> arg -> term; val con_app : string -> arg list -> term; - val dtyp_of_eq : eq -> Datatype.dtyp; - - - (* Name mangling *) - val strip_esc : string -> string; - val extern_name : string -> string; - val dis_name : string -> string; - val mat_name : string -> string; - val pat_name : string -> string; end; structure Domain_Library :> DOMAIN_LIBRARY = @@ -155,26 +129,6 @@ exception Impossible of string; fun Imposs msg = raise Impossible ("Domain:"^msg); -(* ----- name handling ----- *) - -val strip_esc = - let fun strip ("'" :: c :: cs) = c :: strip cs - | strip ["'"] = [] - | strip (c :: cs) = c :: strip cs - | strip [] = []; - in implode o strip o Symbol.explode end; - -fun extern_name con = - case Symbol.explode con of - ("o"::"p"::" "::rest) => implode rest - | _ => con; -fun dis_name con = "is_"^ (extern_name con); -fun dis_name_ con = "is_"^ (strip_esc con); -fun mat_name con = "match_"^ (extern_name con); -fun mat_name_ con = "match_"^ (strip_esc con); -fun pat_name con = (extern_name con) ^ "_pat"; -fun pat_name_ con = (strip_esc con) ^ "_pat"; - fun cpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort cpo}); fun pcpo_type sg t = Sign.of_sort sg (Sign.certify_typ sg t, @{sort pcpo}); fun string_of_typ sg = Syntax.string_of_typ_global sg o Sign.certify_typ sg; @@ -210,36 +164,13 @@ fun nonlazy_rec args = map vname (filter is_nonlazy_rec args); -(* ----- combinators for making dtyps ----- *) - -fun mk_uD T = Datatype_Aux.DtType(@{type_name "u"}, [T]); -fun mk_sprodD (T, U) = Datatype_Aux.DtType(@{type_name sprod}, [T, U]); -fun mk_ssumD (T, U) = Datatype_Aux.DtType(@{type_name ssum}, [T, U]); -fun mk_liftD T = Datatype_Aux.DtType(@{type_name "lift"}, [T]); -val unitD = Datatype_Aux.DtType(@{type_name "unit"}, []); -val boolD = Datatype_Aux.DtType(@{type_name "bool"}, []); -val oneD = mk_liftD unitD; -val trD = mk_liftD boolD; -fun big_sprodD ds = case ds of [] => oneD | _ => foldr1 mk_sprodD ds; -fun big_ssumD ds = case ds of [] => unitD | _ => foldr1 mk_ssumD ds; - -fun dtyp_of_arg ((lazy, D), _) = if lazy then mk_uD D else D; -fun dtyp_of_cons (_, args) = big_sprodD (map dtyp_of_arg args); -fun dtyp_of_eq (_, cons) = big_ssumD (map dtyp_of_cons cons); - - (* ----- support for type and mixfix expressions ----- *) fun mk_uT T = Type(@{type_name "u"}, [T]); -fun mk_cfunT (T, U) = Type(@{type_name cfun}, [T, U]); fun mk_sprodT (T, U) = Type(@{type_name sprod}, [T, U]); fun mk_ssumT (T, U) = Type(@{type_name ssum}, [T, U]); val oneT = @{typ one}; -val op ->> = mk_cfunT; - -fun mk_TFree s = TFree ("'" ^ s, @{sort pcpo}); - (* ----- support for term expressions ----- *) fun %: s = Free(s,dummyT); @@ -260,7 +191,6 @@ fun mk_All (x,P) = %%:"all" $ mk_lam(x,P); (* meta universal quantification *) infixr 0 ===>; fun S ===> T = %%:"==>" $ S $ T; -infixr 0 ==>; fun S ==> T = mk_trp S ===> mk_trp T; infix 0 ==; fun S == T = %%:"==" $ S $ T; infix 1 ===; fun S === T = %%:"op =" $ S $ T; infix 1 ~=; fun S ~= T = HOLogic.mk_not (S === T); @@ -275,42 +205,22 @@ fun mk_ssplit t = %%: @{const_name ssplit}`t; fun mk_sscase (x, y) = %%: @{const_name sscase}`x`y; fun mk_fup (t,u) = %%: @{const_name fup} ` t ` u; -val ONE = @{term ONE}; -fun mk_iterate (n,f,z) = %%: @{const_name iterate} $ n ` f ` z; -fun mk_fix t = %%: @{const_name fix}`t; -fun mk_return t = %%: @{const_name Fixrec.return}`t; -val mk_fail = %%: @{const_name Fixrec.fail}; - -fun mk_branch t = %%: @{const_name Fixrec.branch} $ t; val pcpoS = @{sort pcpo}; val list_ccomb = Library.foldl (op `); (* continuous version of list_comb *) fun con_app2 con f args = list_ccomb(%%:con,map f args); fun con_app con = con_app2 con %#; -fun if_rec arg f y = if is_rec arg then f (rec_of arg) else y; -fun app_rec_arg p arg = if_rec arg (fn n => fn x => (p n)`x) I (%# arg); fun prj _ _ x ( _::[]) _ = x | prj f1 _ x (_::y::ys) 0 = f1 x y | prj f1 f2 x (y:: ys) j = prj f1 f2 (f2 x y) ys (j-1); fun proj x = prj (fn S => K(%%:"fst" $S)) (fn S => K(%%:"snd" $S)) x; fun lift tfn = Library.foldr (fn (x,t)=> (mk_trp(tfn x) ===> t)); -fun /\ v T = %%: @{const_name Abs_CFun} $ mk_lam(v,T); -fun /\# (arg,T) = /\ (vname arg) T; -infixr 9 oo; fun S oo T = %%: @{const_name cfcomp}`S`T; val UU = %%: @{const_name UU}; -fun strict f = f`UU === UU; fun defined t = t ~= UU; fun cpair (t,u) = %%: @{const_name Pair} $ t $ u; fun spair (t,u) = %%: @{const_name spair}`t`u; -fun mk_ctuple [] = HOLogic.unit (* used in match_defs *) - | mk_ctuple ts = foldr1 cpair ts; -fun mk_ctupleT [] = HOLogic.unitT (* used in match_defs *) - | mk_ctupleT Ts = foldr1 HOLogic.mk_prodT Ts; -fun mk_maybeT T = Type ("Fixrec.maybe",[T]); -fun cpair_pat (p1,p2) = %%: @{const_name cpair_pat} $ p1 $ p2; -val mk_ctuple_pat = foldr1 cpair_pat; fun lift_defined f = lift (fn x => defined (f x)); fun bound_arg vns v = Bound (length vns - find_index (fn v' => v' = v) vns - 1);