# HG changeset patch
# User berghofe
# Date 1184145188 -7200
# Node ID 28df61d931e25669d720afc1521392a2e3679ed0
# Parent  7c9e6e2fe249fda407bf0129625faabf45bf7b6d
New operations on tuples with specific arities.

diff -r 7c9e6e2fe249 -r 28df61d931e2 src/HOL/hologic.ML
--- 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 *)