src/HOL/Tools/hologic.ML
changeset 32342 3fabf5b5fc83
parent 32339 40612b7ace87
child 32446 cde4f2c8bdd5
     1.1 --- a/src/HOL/Tools/hologic.ML	Thu Jul 30 13:52:18 2009 +0200
     1.2 +++ b/src/HOL/Tools/hologic.ML	Thu Jul 30 15:20:57 2009 +0200
     1.3 @@ -67,14 +67,18 @@
     1.4    val split_const: typ * typ * typ -> term
     1.5    val mk_split: term -> term
     1.6    val flatten_tupleT: typ -> typ list
     1.7 -  val mk_tupleT: int list list -> typ list -> typ
     1.8 -  val strip_tupleT: int list list -> typ -> typ list
     1.9 +  val mk_tupleT: typ list -> typ
    1.10 +  val strip_tupleT: typ -> typ list
    1.11 +  val mk_tuple: term list -> term
    1.12 +  val strip_tuple: term -> term list
    1.13 +  val mk_ptupleT: int list list -> typ list -> typ
    1.14 +  val strip_ptupleT: int list list -> typ -> typ list
    1.15    val flat_tupleT_paths: typ -> int list list
    1.16 -  val mk_tuple: int list list -> typ -> term list -> term
    1.17 -  val dest_tuple: int list list -> term -> term list
    1.18 +  val mk_ptuple: int list list -> typ -> term list -> term
    1.19 +  val strip_ptuple: int list list -> term -> term list
    1.20    val flat_tuple_paths: term -> int list list
    1.21 -  val mk_splits: int list list -> typ -> typ -> term -> term
    1.22 -  val strip_splits: term -> term * typ list * int list list
    1.23 +  val mk_psplits: int list list -> typ -> typ -> term -> term
    1.24 +  val strip_psplits: term -> term * typ list * int list list
    1.25    val natT: typ
    1.26    val zero: term
    1.27    val is_zero: term -> bool
    1.28 @@ -323,15 +327,33 @@
    1.29  fun flatten_tupleT (Type ("*", [T1, T2])) = flatten_tupleT T1 @ flatten_tupleT T2
    1.30    | flatten_tupleT T = [T];
    1.31  
    1.32 +
    1.33 +(* tuples with right-fold structure *)
    1.34 +
    1.35 +fun mk_tupleT [] = unitT
    1.36 +  | mk_tupleT Ts = foldr1 mk_prodT Ts;
    1.37 +
    1.38 +fun strip_tupleT (Type ("Product_Type.unit", [])) = []
    1.39 +  | strip_tupleT (Type ("*", [T1, T2])) = T1 :: strip_tupleT T2
    1.40 +  | strip_tupleT T = [T];
    1.41 +
    1.42 +fun mk_tuple [] = unit
    1.43 +  | mk_tuple ts = foldr1 mk_prod ts;
    1.44 +
    1.45 +fun strip_tuple (Const ("Product_Type.Unity", _)) = []
    1.46 +  | strip_tuple (Const ("Pair", _) $ t1 $ t2) = t1 :: strip_tuple t2
    1.47 +  | strip_tuple t = [t];
    1.48 +
    1.49 +
    1.50  (* tuples with specific arities
    1.51  
    1.52 -  an "arity" of a tuple is a list of lists of integers
    1.53 -  ("factors"), denoting paths to subterms that are pairs
    1.54 +   an "arity" of a tuple is a list of lists of integers,
    1.55 +   denoting paths to subterms that are pairs
    1.56  *)
    1.57  
    1.58 -fun prod_err s = raise TERM (s ^ ": inconsistent use of products", []);
    1.59 +fun ptuple_err s = raise TERM (s ^ ": inconsistent use of nested products", []);
    1.60  
    1.61 -fun mk_tupleT ps =
    1.62 +fun mk_ptupleT ps =
    1.63    let
    1.64      fun mk p Ts =
    1.65        if p mem ps then
    1.66 @@ -342,12 +364,12 @@
    1.67        else (hd Ts, tl Ts)
    1.68    in fst o mk [] end;
    1.69  
    1.70 -fun strip_tupleT ps =
    1.71 +fun strip_ptupleT ps =
    1.72    let
    1.73      fun factors p T = if p mem ps then (case T of
    1.74          Type ("*", [T1, T2]) =>
    1.75            factors (1::p) T1 @ factors (2::p) T2
    1.76 -      | _ => prod_err "strip_tupleT") else [T]
    1.77 +      | _ => ptuple_err "strip_ptupleT") else [T]
    1.78    in factors [] end;
    1.79  
    1.80  val flat_tupleT_paths =
    1.81 @@ -357,7 +379,7 @@
    1.82        | factors p _ = []
    1.83    in factors [] end;
    1.84  
    1.85 -fun mk_tuple ps =
    1.86 +fun mk_ptuple ps =
    1.87    let
    1.88      fun mk p T ts =
    1.89        if p mem ps then (case T of
    1.90 @@ -366,16 +388,16 @@
    1.91                val (t, ts') = mk (1::p) T1 ts;
    1.92                val (u, ts'') = mk (2::p) T2 ts'
    1.93              in (pair_const T1 T2 $ t $ u, ts'') end
    1.94 -        | _ => prod_err "mk_tuple")
    1.95 +        | _ => ptuple_err "mk_ptuple")
    1.96        else (hd ts, tl ts)
    1.97    in fst oo mk [] end;
    1.98  
    1.99 -fun dest_tuple ps =
   1.100 +fun strip_ptuple ps =
   1.101    let
   1.102      fun dest p t = if p mem ps then (case t of
   1.103          Const ("Pair", _) $ t $ u =>
   1.104            dest (1::p) t @ dest (2::p) u
   1.105 -      | _ => prod_err "dest_tuple") else [t]
   1.106 +      | _ => ptuple_err "strip_ptuple") else [t]
   1.107    in dest [] end;
   1.108  
   1.109  val flat_tuple_paths =
   1.110 @@ -385,24 +407,24 @@
   1.111        | factors p _ = []
   1.112    in factors [] end;
   1.113  
   1.114 -(*In mk_splits ps S T u, term u expects separate arguments for the factors of S,
   1.115 +(*In mk_psplits ps S T u, term u expects separate arguments for the factors of S,
   1.116    with result type T.  The call creates a new term expecting one argument
   1.117    of type S.*)
   1.118 -fun mk_splits ps T T3 u =
   1.119 +fun mk_psplits ps T T3 u =
   1.120    let
   1.121      fun ap ((p, T) :: pTs) =
   1.122            if p mem ps then (case T of
   1.123                Type ("*", [T1, T2]) =>
   1.124                  split_const (T1, T2, map snd pTs ---> T3) $
   1.125                    ap ((1::p, T1) :: (2::p, T2) :: pTs)
   1.126 -            | _ => prod_err "mk_splits")
   1.127 +            | _ => ptuple_err "mk_psplits")
   1.128            else Abs ("x", T, ap pTs)
   1.129        | ap [] =
   1.130            let val k = length ps
   1.131            in list_comb (incr_boundvars (k + 1) u, map Bound (k downto 0)) end
   1.132    in ap [([], T)] end;
   1.133  
   1.134 -val strip_splits =
   1.135 +val strip_psplits =
   1.136    let
   1.137      fun strip [] qs Ts t = (t, Ts, qs)
   1.138        | strip (p :: ps) qs Ts (Const ("split", _) $ t) =