# HG changeset patch # User wenzelm # Date 1248982035 -7200 # Node ID 47278524df55c0e0e1044b3a256834a8f5a545ac # Parent c14aeb0bcce45fceca7f596a9ced4caa4ab51670# Parent ab9b66c2bbca7f655fc0e40b374346658f939e1a merged diff -r ab9b66c2bbca -r 47278524df55 src/HOL/Tools/TFL/usyntax.ML --- a/src/HOL/Tools/TFL/usyntax.ML Thu Jul 30 18:43:52 2009 +0200 +++ b/src/HOL/Tools/TFL/usyntax.ML Thu Jul 30 21:27:15 2009 +0200 @@ -118,7 +118,7 @@ val alpha = mk_vartype "'a" val beta = mk_vartype "'b" -val strip_prod_type = HOLogic.prodT_factors; +val strip_prod_type = HOLogic.flatten_tupleT; diff -r ab9b66c2bbca -r 47278524df55 src/HOL/Tools/hologic.ML --- a/src/HOL/Tools/hologic.ML Thu Jul 30 18:43:52 2009 +0200 +++ b/src/HOL/Tools/hologic.ML Thu Jul 30 21:27:15 2009 +0200 @@ -66,17 +66,15 @@ val mk_snd: term -> term val split_const: typ * typ * typ -> term 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 flatten_tupleT: typ -> typ list val mk_tupleT: int list list -> typ list -> typ - val strip_split: term -> term * typ list * int list list + val strip_tupleT: 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 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 natT: typ val zero: term val is_zero: term -> bool @@ -320,95 +318,17 @@ | _ => raise TERM ("mk_split: bad body type", [t])); (*Maps the type T1 * ... * Tn to [T1, ..., Tn], however nested*) -fun prodT_factors (Type ("*", [T1, T2])) = prodT_factors T1 @ prodT_factors T2 - | prodT_factors T = [T]; - -(*Makes a nested tuple from a list, following the product type structure*) -fun mk_tuple (Type ("*", [T1, T2])) tms = - mk_prod (mk_tuple T1 tms, - 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]; +fun flatten_tupleT (Type ("*", [T1, T2])) = flatten_tupleT T1 @ flatten_tupleT T2 + | flatten_tupleT 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; +(* tuples with specific arities - -(* 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 = @@ -420,7 +340,67 @@ else (hd Ts, tl Ts) in fst o mk [] end; -fun strip_split t = +fun strip_tupleT 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] + in factors [] end; + +val flat_tupleT_paths = + let + fun factors p (Type ("*", [T1, T2])) = + p :: factors (1::p) T1 @ factors (2::p) T2 + | factors p _ = [] + in factors [] 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 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; + +val flat_tuple_paths = + let + fun factors p (Const ("Pair", _) $ t $ u) = + p :: factors (1::p) t @ factors (2::p) u + | factors p _ = [] + in factors [] end; + +(*In mk_splits 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 = + 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") + 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 = let fun strip [] qs Ts t = (t, Ts, qs) | strip (p :: ps) qs Ts (Const ("split", _) $ t) = @@ -429,7 +409,7 @@ | 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; + in strip [[]] [] [] end; (* nat *) diff -r ab9b66c2bbca -r 47278524df55 src/HOL/Tools/inductive_codegen.ML --- a/src/HOL/Tools/inductive_codegen.ML Thu Jul 30 18:43:52 2009 +0200 +++ b/src/HOL/Tools/inductive_codegen.ML Thu Jul 30 21:27:15 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_split u + let val (r, Ts, fs) = HOLogic.strip_splits u in case strip_comb r of (Const (s, T), ts) => (case (get_clauses thy s, get_assoc_code thy (s, T)) of diff -r ab9b66c2bbca -r 47278524df55 src/HOL/Tools/inductive_set.ML --- a/src/HOL/Tools/inductive_set.ML Thu Jul 30 18:43:52 2009 +0200 +++ b/src/HOL/Tools/inductive_set.ML Thu Jul 30 21:27:15 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_split t + let val (u, Ts, ps) = HOLogic.strip_splits t in case u of (c as Const ("op :", _)) $ q $ S' => - (case try (HOLogic.dest_tuple' ps) q of + (case try (HOLogic.dest_tuple 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.ap_split' (HOLogic.prod_factors p) U HOLogic.boolT t + HOLogic.mk_splits (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.prodT_factors' ps U ---> HOLogic.boolT)) x + val x' = map_type (K (HOLogic.strip_tupleT ps U ---> HOLogic.boolT)) x in (cterm_of thy x, cterm_of thy (HOLogic.Collect_const U $ - HOLogic.ap_split' ps U HOLogic.boolT x')) + HOLogic.mk_splits 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.prodT_factors' fs' U; + val Ts = HOLogic.strip_tupleT 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.ap_split' fs' U + HOLogic.Collect_const U $ HOLogic.mk_splits fs' U HOLogic.boolT (Bound 0))))] arg_cong' RS sym) end) in @@ -270,7 +270,7 @@ fun factors_of t fs = case strip_abs_body t of Const ("op :", _) $ u $ S => if is_Free S orelse is_Var S then - let val ps = HOLogic.prod_factors u + let val ps = HOLogic.flat_tuple_paths u in (SOME ps, (S, ps) :: fs) end else (NONE, fs) | _ => (NONE, fs); @@ -279,7 +279,7 @@ val ((h', ts'), fs') = (case rhs of Abs _ => (case strip_abs_body rhs of Const ("op :", _) $ u $ S => - (strip_comb S, SOME (HOLogic.prod_factors u)) + (strip_comb S, SOME (HOLogic.flat_tuple_paths u)) | _ => error "member symbol on right-hand side expected") | _ => (strip_comb rhs, NONE)) in @@ -366,7 +366,7 @@ 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_tuple ps T (map Bound (length ps downto 0)), x')))) end) fs in thm |> @@ -412,7 +412,7 @@ PredSetConvData.get (Context.Proof ctxt); fun infer (Abs (_, _, t)) = infer t | infer (Const ("op :", _) $ t $ u) = - infer_arities thy set_arities (SOME (HOLogic.prod_factors t), u) + infer_arities thy set_arities (SOME (HOLogic.flat_tuple_paths t), u) | infer (t $ u) = infer t #> infer u | infer _ = I; val new_arities = filter_out @@ -422,14 +422,14 @@ SOME fs => let val T = HOLogic.dest_setT (fastype_of x); - val Ts = HOLogic.prodT_factors' fs T; + val Ts = HOLogic.strip_tupleT fs T; val x' = map_type (K (Ts ---> HOLogic.boolT)) x in (x, (x', (HOLogic.Collect_const T $ - HOLogic.ap_split' fs T HOLogic.boolT x', + HOLogic.mk_splits 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_tuple 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.prodT_factors' fs U; + val Ts = HOLogic.strip_tupleT 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.ap_split' fs U HOLogic.boolT + HOLogic.Collect_const U $ HOLogic.mk_splits 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.ap_split' fs U HOLogic.boolT (list_comb (p, params3)))))) + HOLogic.mk_splits 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_tuple 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)) diff -r ab9b66c2bbca -r 47278524df55 src/HOL/Tools/split_rule.ML --- a/src/HOL/Tools/split_rule.ML Thu Jul 30 18:43:52 2009 +0200 +++ b/src/HOL/Tools/split_rule.ML Thu Jul 30 21:27:15 2009 +0200 @@ -50,13 +50,13 @@ internal_split_const (T1, T2, T3) $ Abs ("v", T1, ap_split T2 T3 - ((ap_split T1 (HOLogic.prodT_factors T2 ---> T3) (incr_boundvars 1 u)) $ + ((ap_split T1 (HOLogic.flatten_tupleT T2 ---> T3) (incr_boundvars 1 u)) $ Bound 0)) | ap_split T T3 u = u; (*Curries any Var of function type in the rule*) fun split_rule_var' (t as Var (v, Type ("fun", [T1, T2]))) rl = - let val T' = HOLogic.prodT_factors T1 ---> T2; + let val T' = HOLogic.flatten_tupleT T1 ---> T2; val newt = ap_split T1 T2 (Var (v, T')); val cterm = Thm.cterm_of (Thm.theory_of_thm rl); in Thm.instantiate ([], [(cterm t, cterm newt)]) rl end @@ -66,7 +66,7 @@ (* complete splitting of partially splitted rules *) fun ap_split' (T::Ts) U u = Abs ("v", T, ap_split' Ts U - (ap_split T (List.concat (map HOLogic.prodT_factors Ts) ---> U) + (ap_split T (maps HOLogic.flatten_tupleT Ts ---> U) (incr_boundvars 1 u) $ Bound 0)) | ap_split' _ _ u = u; @@ -76,12 +76,12 @@ val (Us', U') = strip_type T; val Us = Library.take (length ts, Us'); val U = Library.drop (length ts, Us') ---> U'; - val T' = List.concat (map HOLogic.prodT_factors Us) ---> U; + val T' = maps HOLogic.flatten_tupleT Us ---> U; fun mk_tuple (v as Var ((a, _), T)) (xs, insts) = let - val Ts = HOLogic.prodT_factors T; + 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 T + in (xs @ ys, (cterm v, cterm (HOLogic.mk_tuple (HOLogic.flat_tupleT_paths T) T (map (Var o apfst (rpair 0)) (ys ~~ Ts))))::insts) end | mk_tuple _ x = x; diff -r ab9b66c2bbca -r 47278524df55 src/HOL/ex/predicate_compile.ML --- a/src/HOL/ex/predicate_compile.ML Thu Jul 30 18:43:52 2009 +0200 +++ b/src/HOL/ex/predicate_compile.ML Thu Jul 30 21:27:15 2009 +0200 @@ -1531,7 +1531,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_split split; + val (body, Ts, fp) = HOLogic.strip_splits split; (*FIXME former order of tuple positions must be restored*) val (pred as Const (name, T), all_args) = strip_comb body val (params, args) = chop (nparams_of thy name) all_args