path-sensitive tuple combinators carry a "p"(ath) prefix; combinators for standard right-fold tuples
--- a/src/HOL/Tools/hologic.ML Thu Jul 30 13:52:18 2009 +0200
+++ b/src/HOL/Tools/hologic.ML Thu Jul 30 15:20:57 2009 +0200
@@ -67,14 +67,18 @@
val split_const: typ * typ * typ -> term
val mk_split: term -> term
val flatten_tupleT: typ -> typ list
- val mk_tupleT: int list list -> typ list -> typ
- val strip_tupleT: int list list -> typ -> typ list
+ val mk_tupleT: typ list -> typ
+ val strip_tupleT: typ -> typ list
+ val mk_tuple: term list -> term
+ val strip_tuple: term -> term list
+ val mk_ptupleT: int list list -> typ list -> typ
+ val strip_ptupleT: int list list -> typ -> typ list
val flat_tupleT_paths: typ -> int list list
- val mk_tuple: int list list -> typ -> term list -> term
- val dest_tuple: int list list -> term -> term list
+ val mk_ptuple: int list list -> typ -> term list -> term
+ val strip_ptuple: int list list -> term -> term list
val flat_tuple_paths: term -> int list list
- val mk_splits: int list list -> typ -> typ -> term -> term
- val strip_splits: term -> term * typ list * int list list
+ val mk_psplits: int list list -> typ -> typ -> term -> term
+ val strip_psplits: term -> term * typ list * int list list
val natT: typ
val zero: term
val is_zero: term -> bool
@@ -323,15 +327,33 @@
fun flatten_tupleT (Type ("*", [T1, T2])) = flatten_tupleT T1 @ flatten_tupleT T2
| flatten_tupleT T = [T];
+
+(* tuples with right-fold structure *)
+
+fun mk_tupleT [] = unitT
+ | mk_tupleT Ts = foldr1 mk_prodT Ts;
+
+fun strip_tupleT (Type ("Product_Type.unit", [])) = []
+ | strip_tupleT (Type ("*", [T1, T2])) = T1 :: strip_tupleT T2
+ | strip_tupleT T = [T];
+
+fun mk_tuple [] = unit
+ | mk_tuple ts = foldr1 mk_prod ts;
+
+fun strip_tuple (Const ("Product_Type.Unity", _)) = []
+ | strip_tuple (Const ("Pair", _) $ t1 $ t2) = t1 :: strip_tuple t2
+ | strip_tuple t = [t];
+
+
(* tuples with specific arities
- an "arity" of a tuple is a list of lists of integers
- ("factors"), denoting paths to subterms that are pairs
+ an "arity" of a tuple is a list of lists of integers,
+ denoting paths to subterms that are pairs
*)
-fun prod_err s = raise TERM (s ^ ": inconsistent use of products", []);
+fun ptuple_err s = raise TERM (s ^ ": inconsistent use of nested products", []);
-fun mk_tupleT ps =
+fun mk_ptupleT ps =
let
fun mk p Ts =
if p mem ps then
@@ -342,12 +364,12 @@
else (hd Ts, tl Ts)
in fst o mk [] end;
-fun strip_tupleT ps =
+fun strip_ptupleT 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 "strip_tupleT") else [T]
+ | _ => ptuple_err "strip_ptupleT") else [T]
in factors [] end;
val flat_tupleT_paths =
@@ -357,7 +379,7 @@
| factors p _ = []
in factors [] end;
-fun mk_tuple ps =
+fun mk_ptuple ps =
let
fun mk p T ts =
if p mem ps then (case T of
@@ -366,16 +388,16 @@
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")
+ | _ => ptuple_err "mk_ptuple")
else (hd ts, tl ts)
in fst oo mk [] end;
-fun dest_tuple ps =
+fun strip_ptuple 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]
+ | _ => ptuple_err "strip_ptuple") else [t]
in dest [] end;
val flat_tuple_paths =
@@ -385,24 +407,24 @@
| factors p _ = []
in factors [] end;
-(*In mk_splits ps S T u, term u expects separate arguments for the factors of S,
+(*In mk_psplits 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 mk_splits ps T T3 u =
+fun mk_psplits 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 "mk_splits")
+ | _ => ptuple_err "mk_psplits")
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;
-val strip_splits =
+val strip_psplits =
let
fun strip [] qs Ts t = (t, Ts, qs)
| strip (p :: ps) qs Ts (Const ("split", _) $ t) =
--- a/src/HOL/Tools/inductive_codegen.ML Thu Jul 30 13:52:18 2009 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Thu Jul 30 15:20:57 2009 +0200
@@ -645,7 +645,7 @@
fun inductive_codegen thy defs dep module brack t gr = (case strip_comb t of
(Const ("Collect", _), [u]) =>
- let val (r, Ts, fs) = HOLogic.strip_splits u
+ let val (r, Ts, fs) = HOLogic.strip_psplits u
in case strip_comb r of
(Const (s, T), ts) =>
(case (get_clauses thy s, get_assoc_code thy (s, T)) of
--- a/src/HOL/Tools/inductive_set.ML Thu Jul 30 13:52:18 2009 +0200
+++ b/src/HOL/Tools/inductive_set.ML Thu Jul 30 15:20:57 2009 +0200
@@ -33,10 +33,10 @@
val collect_mem_simproc =
Simplifier.simproc (theory "Set") "Collect_mem" ["Collect t"] (fn thy => fn ss =>
fn S as Const ("Collect", Type ("fun", [_, T])) $ t =>
- let val (u, Ts, ps) = HOLogic.strip_splits t
+ let val (u, Ts, ps) = HOLogic.strip_psplits t
in case u of
(c as Const ("op :", _)) $ q $ S' =>
- (case try (HOLogic.dest_tuple ps) q of
+ (case try (HOLogic.strip_ptuple ps) q of
NONE => NONE
| SOME ts =>
if not (loose_bvar (S', 0)) andalso
@@ -79,7 +79,7 @@
fun mk_collect p T t =
let val U = HOLogic.dest_setT T
in HOLogic.Collect_const U $
- HOLogic.mk_splits (HOLogic.flat_tuple_paths p) U HOLogic.boolT t
+ HOLogic.mk_psplits (HOLogic.flat_tuple_paths p) U HOLogic.boolT t
end;
fun decomp (Const (s, _) $ ((m as Const ("op :",
Type (_, [_, Type (_, [T, _])]))) $ p $ S) $ u) =
@@ -223,11 +223,11 @@
map (fn (x, ps) =>
let
val U = HOLogic.dest_setT (fastype_of x);
- val x' = map_type (K (HOLogic.strip_tupleT ps U ---> HOLogic.boolT)) x
+ val x' = map_type (K (HOLogic.strip_ptupleT ps U ---> HOLogic.boolT)) x
in
(cterm_of thy x,
cterm_of thy (HOLogic.Collect_const U $
- HOLogic.mk_splits ps U HOLogic.boolT x'))
+ HOLogic.mk_psplits ps U HOLogic.boolT x'))
end) fs;
fun mk_to_pred_eq p fs optfs' T thm =
@@ -240,7 +240,7 @@
| SOME fs' =>
let
val (_, U) = split_last (binder_types T);
- val Ts = HOLogic.strip_tupleT fs' U;
+ val Ts = HOLogic.strip_ptupleT fs' U;
(* FIXME: should cterm_instantiate increment indexes? *)
val arg_cong' = Thm.incr_indexes (Thm.maxidx_of thm + 1) arg_cong;
val (arg_cong_f, _) = arg_cong' |> cprop_of |> Drule.strip_imp_concl |>
@@ -248,7 +248,7 @@
in
thm' RS (Drule.cterm_instantiate [(arg_cong_f,
cterm_of thy (Abs ("P", Ts ---> HOLogic.boolT,
- HOLogic.Collect_const U $ HOLogic.mk_splits fs' U
+ HOLogic.Collect_const U $ HOLogic.mk_psplits fs' U
HOLogic.boolT (Bound 0))))] arg_cong' RS sym)
end)
in
@@ -361,12 +361,12 @@
val insts = map (fn (x, ps) =>
let
val Ts = binder_types (fastype_of x);
- val T = HOLogic.mk_tupleT ps Ts;
+ val T = HOLogic.mk_ptupleT ps Ts;
val x' = map_type (K (HOLogic.mk_setT T)) x
in
(cterm_of thy x,
cterm_of thy (list_abs (map (pair "x") Ts, HOLogic.mk_mem
- (HOLogic.mk_tuple ps T (map Bound (length ps downto 0)), x'))))
+ (HOLogic.mk_ptuple ps T (map Bound (length ps downto 0)), x'))))
end) fs
in
thm |>
@@ -422,14 +422,14 @@
SOME fs =>
let
val T = HOLogic.dest_setT (fastype_of x);
- val Ts = HOLogic.strip_tupleT fs T;
+ val Ts = HOLogic.strip_ptupleT fs T;
val x' = map_type (K (Ts ---> HOLogic.boolT)) x
in
(x, (x',
(HOLogic.Collect_const T $
- HOLogic.mk_splits fs T HOLogic.boolT x',
+ HOLogic.mk_psplits fs T HOLogic.boolT x',
list_abs (map (pair "x") Ts, HOLogic.mk_mem
- (HOLogic.mk_tuple fs T (map Bound (length fs downto 0)),
+ (HOLogic.mk_ptuple fs T (map Bound (length fs downto 0)),
x)))))
end
| NONE => (x, (x, (x, x))))) params;
@@ -448,13 +448,13 @@
Pretty.str ("of " ^ s ^ " do not agree with types"),
Pretty.block (Pretty.commas (map (Syntax.pretty_typ ctxt) paramTs)),
Pretty.str "of declared parameters"]));
- val Ts = HOLogic.strip_tupleT fs U;
+ val Ts = HOLogic.strip_ptupleT fs U;
val c' = Free (s ^ "p",
map fastype_of params1 @ Ts ---> HOLogic.boolT)
in
((c', (fs, U, Ts)),
(list_comb (c, params2),
- HOLogic.Collect_const U $ HOLogic.mk_splits fs U HOLogic.boolT
+ HOLogic.Collect_const U $ HOLogic.mk_psplits fs U HOLogic.boolT
(list_comb (c', params1))))
end) |> split_list |>> split_list;
val eqns' = eqns @
@@ -484,7 +484,7 @@
val (defs, ctxt2) = fold_map (LocalTheory.define Thm.internalK)
(map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.empty_binding,
fold_rev lambda params (HOLogic.Collect_const U $
- HOLogic.mk_splits fs U HOLogic.boolT (list_comb (p, params3))))))
+ HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3))))))
(cnames_syn ~~ cs_info ~~ preds)) ctxt1;
(* prove theorems for converting predicate to set notation *)
@@ -495,7 +495,7 @@
(HOLogic.mk_Trueprop (HOLogic.mk_eq
(list_comb (p, params3),
list_abs (map (pair "x") Ts, HOLogic.mk_mem
- (HOLogic.mk_tuple fs U (map Bound (length fs downto 0)),
+ (HOLogic.mk_ptuple fs U (map Bound (length fs downto 0)),
list_comb (c, params))))))
(K (REPEAT (rtac ext 1) THEN simp_tac (HOL_basic_ss addsimps
[def, mem_Collect_eq, split_conv]) 1))
--- a/src/HOL/Tools/split_rule.ML Thu Jul 30 13:52:18 2009 +0200
+++ b/src/HOL/Tools/split_rule.ML Thu Jul 30 15:20:57 2009 +0200
@@ -81,7 +81,7 @@
let
val Ts = HOLogic.flatten_tupleT T;
val ys = Name.variant_list xs (replicate (length Ts) a);
- in (xs @ ys, (cterm v, cterm (HOLogic.mk_tuple (HOLogic.flat_tupleT_paths T) T
+ in (xs @ ys, (cterm v, cterm (HOLogic.mk_ptuple (HOLogic.flat_tupleT_paths T) T
(map (Var o apfst (rpair 0)) (ys ~~ Ts))))::insts)
end
| mk_tuple _ x = x;
--- a/src/HOL/ex/predicate_compile.ML Thu Jul 30 13:52:18 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML Thu Jul 30 15:20:57 2009 +0200
@@ -68,20 +68,6 @@
HOLogic.mk_eq (Free (a, fastype_of b), b) :: mk_eqs a cs
in mk_eqs x xs end;
-fun mk_tupleT [] = HOLogic.unitT
- | mk_tupleT Ts = foldr1 HOLogic.mk_prodT Ts;
-
-fun dest_tupleT (Type (@{type_name Product_Type.unit}, [])) = []
- | dest_tupleT (Type (@{type_name "*"}, [T1, T2])) = T1 :: (dest_tupleT T2)
- | dest_tupleT t = [t]
-
-fun mk_tuple [] = HOLogic.unit
- | mk_tuple ts = foldr1 HOLogic.mk_prod ts;
-
-fun dest_tuple (Const (@{const_name Product_Type.Unity}, _)) = []
- | dest_tuple (Const (@{const_name Pair}, _) $ t1 $ t2) = t1 :: (dest_tuple t2)
- | dest_tuple t = [t]
-
fun mk_pred_enumT T = Type (@{type_name Predicate.pred}, [T])
fun dest_pred_enumT (Type (@{type_name Predicate.pred}, [T])) = T
@@ -557,7 +543,7 @@
| funT_of T (SOME mode) = let
val Ts = binder_types T;
val (Us1, Us2) = get_args mode Ts
- in Us1 ---> (mk_pred_enumT (mk_tupleT Us2)) end;
+ in Us1 ---> (mk_pred_enumT (HOLogic.mk_tupleT Us2)) end;
fun funT'_of (iss, is) T = let
val Ts = binder_types T
@@ -565,7 +551,7 @@
val paramTs' = map2 (fn SOME is => funT'_of ([], is) | NONE => I) iss paramTs
val (inargTs, outargTs) = get_args is argTs
in
- (paramTs' @ inargTs) ---> (mk_pred_enumT (mk_tupleT outargTs))
+ (paramTs' @ inargTs) ---> (mk_pred_enumT (HOLogic.mk_tupleT outargTs))
end;
@@ -593,7 +579,7 @@
val names = fold Term.add_free_names (success_t :: eqs'' @ out_ts) [];
val name = Name.variant names "x";
val name' = Name.variant (name :: names) "y";
- val T = mk_tupleT (map fastype_of out_ts);
+ val T = HOLogic.mk_tupleT (map fastype_of out_ts);
val U = fastype_of success_t;
val U' = dest_pred_enumT U;
val v = Free (name, T);
@@ -601,7 +587,7 @@
in
lambda v (fst (Datatype.make_case
(ProofContext.init thy) false [] v
- [(mk_tuple out_ts,
+ [(HOLogic.mk_tuple out_ts,
if null eqs'' then success_t
else Const (@{const_name HOL.If}, HOLogic.boolT --> U --> U --> U) $
foldr1 HOLogic.mk_conj eqs'' $ success_t $
@@ -609,19 +595,6 @@
(v', mk_empty U')]))
end;
-(*FIXME function can be removed*)
-fun mk_funcomp f t =
- let
- val names = Term.add_free_names t [];
- val Ts = binder_types (fastype_of t);
- val vs = map Free
- (Name.variant_list names (replicate (length Ts) "x") ~~ Ts)
- in
- fold_rev lambda vs (f (list_comb (t, vs)))
- end;
-
-
-
fun compile_param_ext thy modes (NONE, t) = t
| compile_param_ext thy modes (m as SOME (Mode ((iss, is'), is, ms)), t) =
let
@@ -643,11 +616,11 @@
Const (predfun_name_of thy name (iss, is'), funT'_of (iss, is') T)
else error "compile param: Not an inductive predicate with correct mode"
| Free (name, T) => Free (name, funT_of T (SOME is'))
- val outTs = dest_tupleT (dest_pred_enumT (body_type (fastype_of f')))
+ val outTs = HOLogic.strip_tupleT (dest_pred_enumT (body_type (fastype_of f')))
val out_vs = map Free (out_names ~~ outTs)
val params' = map (compile_param thy modes) (ms ~~ params)
val f_app = list_comb (f', params' @ inargs)
- val single_t = (mk_single (mk_tuple (map (fn i => nth out_vs (i - 1)) outp_perm)))
+ val single_t = (mk_single (HOLogic.mk_tuple (map (fn i => nth out_vs (i - 1)) outp_perm)))
val match_t = compile_match thy [] [] out_vs single_t
in list_abs (ivs,
mk_bind (f_app, match_t))
@@ -682,7 +655,7 @@
(curry Library.drop (length ms) (fst (strip_type T)))
val params' = map (compile_param thy modes) (ms ~~ params)
in list_comb (Const (predfun_name_of thy name mode, ((map fastype_of params') @ Ts) --->
- mk_pred_enumT (mk_tupleT Us)), params')
+ mk_pred_enumT (HOLogic.mk_tupleT Us)), params')
end
else error "not a valid inductive expression"
| (Free (name, T), args) =>
@@ -717,7 +690,7 @@
out_ts'' (names', map (rpair []) vs);
in
compile_match thy constr_vs (eqs @ eqs') out_ts'''
- (mk_single (mk_tuple out_ts))
+ (mk_single (HOLogic.mk_tuple out_ts))
end
| compile_prems out_ts vs names ps =
let
@@ -772,12 +745,12 @@
val xs = map2 (fn s => fn T => Free (s, T)) xnames Us1;
val cl_ts =
map (fn cl => compile_clause thy
- all_vs param_vs modes mode cl (mk_tuple xs)) cls;
+ all_vs param_vs modes mode cl (HOLogic.mk_tuple xs)) cls;
val mode_id = predfun_name_of thy s mode
in
HOLogic.mk_Trueprop (HOLogic.mk_eq
(list_comb (Const (mode_id, (Ts1' @ Us1) --->
- mk_pred_enumT (mk_tupleT Us2)),
+ mk_pred_enumT (HOLogic.mk_tupleT Us2)),
map2 (fn s => fn T => Free (s, T)) param_vs Ts1' @ xs),
foldr1 mk_sup cl_ts))
end;
@@ -808,7 +781,7 @@
(map (fn i => "x" ^ string_of_int i) (1 upto (length Ts)));
val args = map Free (argnames ~~ Ts)
val (inargs, outargs) = get_args mode args
- val r = mk_Eval (list_comb (x, inargs), mk_tuple outargs)
+ val r = mk_Eval (list_comb (x, inargs), HOLogic.mk_tuple outargs)
val t = fold_rev lambda args r
in
(t, argnames @ names)
@@ -834,9 +807,9 @@
val param_eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (param_vs ~~ params')
val funargs = params @ inargs
val funpropE = HOLogic.mk_Trueprop (mk_Eval (list_comb (funtrm, funargs),
- if null outargs then Free("y", HOLogic.unitT) else mk_tuple outargs))
+ if null outargs then Free("y", HOLogic.unitT) else HOLogic.mk_tuple outargs))
val funpropI = HOLogic.mk_Trueprop (mk_Eval (list_comb (funtrm, funargs),
- mk_tuple outargs))
+ HOLogic.mk_tuple outargs))
val introtrm = Logic.list_implies (predpropI :: param_eqs, funpropI)
val _ = Output.tracing (Syntax.string_of_term_global thy introtrm)
val simprules = [defthm, @{thm eval_pred},
@@ -879,7 +852,7 @@
| mk_split_lambda' (x::xs) t = HOLogic.mk_split (lambda x (mk_split_lambda' xs t))
in mk_split_lambda' xs t end;
val predterm = mk_Enum (mk_split_lambda xouts (list_comb (Const (name, T), xparams' @ xargs)))
- val funT = (Ts1' @ Us1) ---> (mk_pred_enumT (mk_tupleT Us2))
+ val funT = (Ts1' @ Us1) ---> (mk_pred_enumT (HOLogic.mk_tupleT Us2))
val mode_id = Sign.full_bname thy (Long_Name.base_name mode_id)
val lhs = list_comb (Const (mode_id, funT), xparams @ xins)
val def = Logic.mk_equals (lhs, predterm)
@@ -1141,7 +1114,7 @@
end
else all_tac
in
- split_term_tac (mk_tuple out_ts)
+ split_term_tac (HOLogic.mk_tuple out_ts)
THEN (DETERM (TRY ((Splitter.split_asm_tac [@{thm "split_if_asm"}] 1) THEN (etac @{thm botE} 2))))
end
@@ -1536,7 +1509,7 @@
let
val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t
| _ => error ("Not a set comprehension: " ^ Syntax.string_of_term_global thy t_compr);
- val (body, Ts, fp) = HOLogic.strip_splits split;
+ val (body, Ts, fp) = HOLogic.strip_psplits split;
val (pred as Const (name, T), all_args) = strip_comb body;
val (params, args) = chop (nparams_of thy name) all_args;
val user_mode = map_filter I (map_index
@@ -1556,14 +1529,14 @@
val t_eval = if null outargs then t_pred else let
val outargs_bounds = map (fn Bound i => i) outargs;
val outargsTs = map (nth Ts) outargs_bounds;
- val T_pred = mk_tupleT outargsTs;
- val T_compr = HOLogic.mk_tupleT fp Ts;
+ val T_pred = HOLogic.mk_tupleT outargsTs;
+ val T_compr = HOLogic.mk_ptupleT fp Ts;
val arrange_bounds = map_index I outargs_bounds
|> sort (prod_ord (K EQUAL) int_ord)
|> map fst;
val arrange = funpow (length outargs_bounds - 1) HOLogic.mk_split
(Term.list_abs (map (pair "") outargsTs,
- HOLogic.mk_tuple fp T_compr (map Bound arrange_bounds)))
+ HOLogic.mk_ptuple fp T_compr (map Bound arrange_bounds)))
in mk_pred_map T_pred T_compr arrange t_pred end
in t_eval end;