src/HOL/Tools/hologic.ML
changeset 32287 65d5c5b30747
parent 32264 0be31453f698
child 32339 40612b7ace87
     1.1 --- a/src/HOL/Tools/hologic.ML	Wed Jul 29 16:43:02 2009 +0200
     1.2 +++ b/src/HOL/Tools/hologic.ML	Wed Jul 29 16:48:34 2009 +0200
     1.3 @@ -66,17 +66,15 @@
     1.4    val mk_snd: term -> term
     1.5    val split_const: typ * typ * typ -> term
     1.6    val mk_split: term -> term
     1.7 -  val prodT_factors: typ -> typ list
     1.8 -  val mk_tuple: typ -> term list -> term
     1.9 -  val dest_tuple: term -> term list
    1.10 -  val ap_split: typ -> typ -> term -> term
    1.11 -  val prod_factors: term -> int list list
    1.12 -  val dest_tuple': int list list -> term -> term list
    1.13 -  val prodT_factors': int list list -> typ -> typ list
    1.14 -  val ap_split': int list list -> typ -> typ -> term -> term
    1.15 -  val mk_tuple': int list list -> typ -> term list -> term
    1.16 +  val flatten_tupleT: typ -> typ list
    1.17    val mk_tupleT: int list list -> typ list -> typ
    1.18 -  val strip_split: term -> term * typ list * int list list
    1.19 +  val strip_tupleT: int list list -> typ -> typ list
    1.20 +  val flat_tupleT_paths: typ -> int list list
    1.21 +  val mk_tuple: int list list -> typ -> term list -> term
    1.22 +  val dest_tuple: int list list -> term -> term list
    1.23 +  val flat_tuple_paths: term -> int list list
    1.24 +  val mk_splits: int list list -> typ -> typ -> term -> term
    1.25 +  val strip_splits: term -> term * typ list * int list list
    1.26    val natT: typ
    1.27    val zero: term
    1.28    val is_zero: term -> bool
    1.29 @@ -320,95 +318,17 @@
    1.30    | _ => raise TERM ("mk_split: bad body type", [t]));
    1.31  
    1.32  (*Maps the type T1 * ... * Tn to [T1, ..., Tn], however nested*)
    1.33 -fun prodT_factors (Type ("*", [T1, T2])) = prodT_factors T1 @ prodT_factors T2
    1.34 -  | prodT_factors T = [T];
    1.35 -
    1.36 -(*Makes a nested tuple from a list, following the product type structure*)
    1.37 -fun mk_tuple (Type ("*", [T1, T2])) tms =
    1.38 -        mk_prod (mk_tuple T1 tms,
    1.39 -                 mk_tuple T2 (Library.drop (length (prodT_factors T1), tms)))
    1.40 -  | mk_tuple T (t::_) = t;
    1.41 -
    1.42 -fun dest_tuple (Const ("Pair", _) $ t $ u) = dest_tuple t @ dest_tuple u
    1.43 -  | dest_tuple t = [t];
    1.44 +fun flatten_tupleT (Type ("*", [T1, T2])) = flatten_tupleT T1 @ flatten_tupleT T2
    1.45 +  | flatten_tupleT T = [T];
    1.46  
    1.47 -(*In ap_split S T u, term u expects separate arguments for the factors of S,
    1.48 -  with result type T.  The call creates a new term expecting one argument
    1.49 -  of type S.*)
    1.50 -fun ap_split T T3 u =
    1.51 -  let
    1.52 -    fun ap (T :: Ts) =
    1.53 -          (case T of
    1.54 -             Type ("*", [T1, T2]) =>
    1.55 -               split_const (T1, T2, Ts ---> T3) $ ap (T1 :: T2 :: Ts)
    1.56 -           | _ => Abs ("x", T, ap Ts))
    1.57 -      | ap [] =
    1.58 -          let val k = length (prodT_factors T)
    1.59 -          in list_comb (incr_boundvars k u, map Bound (k - 1 downto 0)) end
    1.60 -  in ap [T] end;
    1.61 +(* tuples with specific arities
    1.62  
    1.63 -
    1.64 -(* operations on tuples with specific arities *)
    1.65 -(*
    1.66    an "arity" of a tuple is a list of lists of integers
    1.67    ("factors"), denoting paths to subterms that are pairs
    1.68  *)
    1.69  
    1.70  fun prod_err s = raise TERM (s ^ ": inconsistent use of products", []);
    1.71  
    1.72 -fun prod_factors t =
    1.73 -  let
    1.74 -    fun factors p (Const ("Pair", _) $ t $ u) =
    1.75 -          p :: factors (1::p) t @ factors (2::p) u
    1.76 -      | factors p _ = []
    1.77 -  in factors [] t end;
    1.78 -
    1.79 -fun dest_tuple' ps =
    1.80 -  let
    1.81 -    fun dest p t = if p mem ps then (case t of
    1.82 -        Const ("Pair", _) $ t $ u =>
    1.83 -          dest (1::p) t @ dest (2::p) u
    1.84 -      | _ => prod_err "dest_tuple'") else [t]
    1.85 -  in dest [] end;
    1.86 -
    1.87 -fun prodT_factors' ps =
    1.88 -  let
    1.89 -    fun factors p T = if p mem ps then (case T of
    1.90 -        Type ("*", [T1, T2]) =>
    1.91 -          factors (1::p) T1 @ factors (2::p) T2
    1.92 -      | _ => prod_err "prodT_factors'") else [T]
    1.93 -  in factors [] end;
    1.94 -
    1.95 -(*In ap_split' ps S T u, term u expects separate arguments for the factors of S,
    1.96 -  with result type T.  The call creates a new term expecting one argument
    1.97 -  of type S.*)
    1.98 -fun ap_split' ps T T3 u =
    1.99 -  let
   1.100 -    fun ap ((p, T) :: pTs) =
   1.101 -          if p mem ps then (case T of
   1.102 -              Type ("*", [T1, T2]) =>
   1.103 -                split_const (T1, T2, map snd pTs ---> T3) $
   1.104 -                  ap ((1::p, T1) :: (2::p, T2) :: pTs)
   1.105 -            | _ => prod_err "ap_split'")
   1.106 -          else Abs ("x", T, ap pTs)
   1.107 -      | ap [] =
   1.108 -          let val k = length ps
   1.109 -          in list_comb (incr_boundvars (k + 1) u, map Bound (k downto 0)) end
   1.110 -  in ap [([], T)] end;
   1.111 -
   1.112 -fun mk_tuple' ps =
   1.113 -  let
   1.114 -    fun mk p T ts =
   1.115 -      if p mem ps then (case T of
   1.116 -          Type ("*", [T1, T2]) =>
   1.117 -            let
   1.118 -              val (t, ts') = mk (1::p) T1 ts;
   1.119 -              val (u, ts'') = mk (2::p) T2 ts'
   1.120 -            in (pair_const T1 T2 $ t $ u, ts'') end
   1.121 -        | _ => prod_err "mk_tuple'")
   1.122 -      else (hd ts, tl ts)
   1.123 -  in fst oo mk [] end;
   1.124 -
   1.125  fun mk_tupleT ps =
   1.126    let
   1.127      fun mk p Ts =
   1.128 @@ -420,7 +340,67 @@
   1.129        else (hd Ts, tl Ts)
   1.130    in fst o mk [] end;
   1.131  
   1.132 -fun strip_split t =
   1.133 +fun strip_tupleT ps =
   1.134 +  let
   1.135 +    fun factors p T = if p mem ps then (case T of
   1.136 +        Type ("*", [T1, T2]) =>
   1.137 +          factors (1::p) T1 @ factors (2::p) T2
   1.138 +      | _ => prod_err "strip_tupleT") else [T]
   1.139 +  in factors [] end;
   1.140 +
   1.141 +val flat_tupleT_paths =
   1.142 +  let
   1.143 +    fun factors p (Type ("*", [T1, T2])) =
   1.144 +          p :: factors (1::p) T1 @ factors (2::p) T2
   1.145 +      | factors p _ = []
   1.146 +  in factors [] end;
   1.147 +
   1.148 +fun mk_tuple ps =
   1.149 +  let
   1.150 +    fun mk p T ts =
   1.151 +      if p mem ps then (case T of
   1.152 +          Type ("*", [T1, T2]) =>
   1.153 +            let
   1.154 +              val (t, ts') = mk (1::p) T1 ts;
   1.155 +              val (u, ts'') = mk (2::p) T2 ts'
   1.156 +            in (pair_const T1 T2 $ t $ u, ts'') end
   1.157 +        | _ => prod_err "mk_tuple")
   1.158 +      else (hd ts, tl ts)
   1.159 +  in fst oo mk [] end;
   1.160 +
   1.161 +fun dest_tuple ps =
   1.162 +  let
   1.163 +    fun dest p t = if p mem ps then (case t of
   1.164 +        Const ("Pair", _) $ t $ u =>
   1.165 +          dest (1::p) t @ dest (2::p) u
   1.166 +      | _ => prod_err "dest_tuple") else [t]
   1.167 +  in dest [] end;
   1.168 +
   1.169 +val flat_tuple_paths =
   1.170 +  let
   1.171 +    fun factors p (Const ("Pair", _) $ t $ u) =
   1.172 +          p :: factors (1::p) t @ factors (2::p) u
   1.173 +      | factors p _ = []
   1.174 +  in factors [] end;
   1.175 +
   1.176 +(*In mk_splits ps S T u, term u expects separate arguments for the factors of S,
   1.177 +  with result type T.  The call creates a new term expecting one argument
   1.178 +  of type S.*)
   1.179 +fun mk_splits ps T T3 u =
   1.180 +  let
   1.181 +    fun ap ((p, T) :: pTs) =
   1.182 +          if p mem ps then (case T of
   1.183 +              Type ("*", [T1, T2]) =>
   1.184 +                split_const (T1, T2, map snd pTs ---> T3) $
   1.185 +                  ap ((1::p, T1) :: (2::p, T2) :: pTs)
   1.186 +            | _ => prod_err "mk_splits")
   1.187 +          else Abs ("x", T, ap pTs)
   1.188 +      | ap [] =
   1.189 +          let val k = length ps
   1.190 +          in list_comb (incr_boundvars (k + 1) u, map Bound (k downto 0)) end
   1.191 +  in ap [([], T)] end;
   1.192 +
   1.193 +val strip_splits =
   1.194    let
   1.195      fun strip [] qs Ts t = (t, Ts, qs)
   1.196        | strip (p :: ps) qs Ts (Const ("split", _) $ t) =
   1.197 @@ -429,7 +409,7 @@
   1.198        | strip (p :: ps) qs Ts t = strip ps qs
   1.199            (hd (binder_types (fastype_of1 (Ts, t))) :: Ts)
   1.200            (incr_boundvars 1 t $ Bound 0)
   1.201 -  in strip [[]] [] [] t end;
   1.202 +  in strip [[]] [] [] end;
   1.203  
   1.204  
   1.205  (* nat *)