# HG changeset patch # User haftmann # Date 1248960057 -7200 # Node ID 3fabf5b5fc838752eccc5cbc2f922e46b41d6969 # Parent c8c17c2e6cebcadab63d9f11071e3b77e0872858 path-sensitive tuple combinators carry a "p"(ath) prefix; combinators for standard right-fold tuples diff -r c8c17c2e6ceb -r 3fabf5b5fc83 src/HOL/Tools/hologic.ML --- 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) = diff -r c8c17c2e6ceb -r 3fabf5b5fc83 src/HOL/Tools/inductive_codegen.ML --- 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 diff -r c8c17c2e6ceb -r 3fabf5b5fc83 src/HOL/Tools/inductive_set.ML --- 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)) diff -r c8c17c2e6ceb -r 3fabf5b5fc83 src/HOL/Tools/split_rule.ML --- 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; diff -r c8c17c2e6ceb -r 3fabf5b5fc83 src/HOL/ex/predicate_compile.ML --- 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;