--- a/src/HOL/hologic.ML Wed Jul 11 11:11:39 2007 +0200
+++ b/src/HOL/hologic.ML Wed Jul 11 11:13:08 2007 +0200
@@ -67,6 +67,15 @@
val mk_split: term -> term
val prodT_factors: typ -> typ list
val mk_tuple: typ -> term list -> term
+ val dest_tuple: term -> term list
+ val ap_split: typ -> typ -> term -> term
+ val prod_factors: term -> int list list
+ val dest_tuple': int list list -> term -> term list
+ val prodT_factors': int list list -> typ -> typ list
+ val ap_split': int list list -> typ -> typ -> term -> term
+ val mk_tuple': int list list -> typ -> term list -> term
+ val mk_tupleT: int list list -> typ list -> typ
+ val strip_split: term -> term * typ list * int list list
val natT: typ
val zero: term
val is_zero: term -> bool
@@ -294,6 +303,109 @@
mk_tuple T2 (Library.drop (length (prodT_factors T1), tms)))
| mk_tuple T (t::_) = t;
+fun dest_tuple (Const ("Pair", _) $ t $ u) = dest_tuple t @ dest_tuple u
+ | dest_tuple t = [t];
+
+(*In ap_split S T u, term u expects separate arguments for the factors of S,
+ with result type T. The call creates a new term expecting one argument
+ of type S.*)
+fun ap_split T T3 u =
+ let
+ fun ap (T :: Ts) =
+ (case T of
+ Type ("*", [T1, T2]) =>
+ split_const (T1, T2, Ts ---> T3) $ ap (T1 :: T2 :: Ts)
+ | _ => Abs ("x", T, ap Ts))
+ | ap [] =
+ let val k = length (prodT_factors T)
+ in list_comb (incr_boundvars k u, map Bound (k - 1 downto 0)) end
+ in ap [T] end;
+
+
+(***********************************************************)
+(* operations on tuples with specific arities *)
+(* *)
+(* an "arity" of a tuple is a list of lists of integers *)
+(* ("factors"), denoting paths to subterms that are pairs *)
+(***********************************************************)
+
+fun prod_err s = raise TERM (s ^ ": inconsistent use of products", []);
+
+fun prod_factors t =
+ let
+ fun factors p (Const ("Pair", _) $ t $ u) =
+ p :: factors (1::p) t @ factors (2::p) u
+ | factors p _ = []
+ in factors [] t end;
+
+fun dest_tuple' ps =
+ let
+ fun dest p t = if p mem ps then (case t of
+ Const ("Pair", _) $ t $ u =>
+ dest (1::p) t @ dest (2::p) u
+ | _ => prod_err "dest_tuple'") else [t]
+ in dest [] end;
+
+fun prodT_factors' ps =
+ let
+ fun factors p T = if p mem ps then (case T of
+ Type ("*", [T1, T2]) =>
+ factors (1::p) T1 @ factors (2::p) T2
+ | _ => prod_err "prodT_factors'") else [T]
+ in factors [] end;
+
+(*In ap_split' ps S T u, term u expects separate arguments for the factors of S,
+ with result type T. The call creates a new term expecting one argument
+ of type S.*)
+fun ap_split' ps T T3 u =
+ let
+ fun ap ((p, T) :: pTs) =
+ if p mem ps then (case T of
+ Type ("*", [T1, T2]) =>
+ split_const (T1, T2, map snd pTs ---> T3) $
+ ap ((1::p, T1) :: (2::p, T2) :: pTs)
+ | _ => prod_err "ap_split'")
+ else Abs ("x", T, ap pTs)
+ | ap [] =
+ let val k = length ps
+ in list_comb (incr_boundvars (k + 1) u, map Bound (k downto 0)) end
+ in ap [([], T)] end;
+
+fun mk_tuple' ps =
+ let
+ fun mk p T ts =
+ if p mem ps then (case T of
+ Type ("*", [T1, T2]) =>
+ let
+ val (t, ts') = mk (1::p) T1 ts;
+ val (u, ts'') = mk (2::p) T2 ts'
+ in (pair_const T1 T2 $ t $ u, ts'') end
+ | _ => prod_err "mk_tuple'")
+ else (hd ts, tl ts)
+ in fst oo mk [] end;
+
+fun mk_tupleT ps =
+ let
+ fun mk p Ts =
+ if p mem ps then
+ let
+ val (T, Ts') = mk (1::p) Ts;
+ val (U, Ts'') = mk (2::p) Ts'
+ in (mk_prodT (T, U), Ts'') end
+ else (hd Ts, tl Ts)
+ in fst o mk [] end;
+
+fun strip_split t =
+ let
+ fun strip [] qs Ts t = (t, Ts, qs)
+ | strip (p :: ps) qs Ts (Const ("split", _) $ t) =
+ strip ((1 :: p) :: (2 :: p) :: ps) (p :: qs) Ts t
+ | strip (p :: ps) qs Ts (Abs (s, T, t)) = strip ps qs (T :: Ts) t
+ | strip (p :: ps) qs Ts t = strip ps qs
+ (hd (binder_types (fastype_of1 (Ts, t))) :: Ts)
+ (incr_boundvars 1 t $ Bound 0)
+ in strip [[]] [] [] t end;
+
(* nat *)