# HG changeset patch # User wenzelm # Date 1457646564 -3600 # Node ID adffc55a682d916cf32b7854d7fd928cca3f7b9e # Parent 8c7301325f9f26efaadf5c1ca002166ccfee0105# Parent 4832491d137619828b072f8938597285b2c3fe37 merged diff -r 4832491d1376 -r adffc55a682d src/HOL/List.thy --- a/src/HOL/List.thy Thu Mar 10 22:49:15 2016 +0100 +++ b/src/HOL/List.thy Thu Mar 10 22:49:24 2016 +0100 @@ -3006,6 +3006,14 @@ lemma upt_conv_Cons: "i < j ==> [i..no precondition\ + "m # n # ns = [m.. n # ns = [Suc m.. [i.. \LOOPS as a simprule, since \j <= j\.\ by (induct k) auto diff -r 4832491d1376 -r adffc55a682d src/HOL/String.thy --- a/src/HOL/String.thy Thu Mar 10 22:49:15 2016 +0100 +++ b/src/HOL/String.thy Thu Mar 10 22:49:24 2016 +0100 @@ -6,15 +6,6 @@ imports Enum begin -lemma upt_conv_Cons_Cons: -- \no precondition\ -- \FIXME move\ - "m # n # ns = [m.. n # ns = [Suc m..Characters and strings\ subsubsection \Characters as finite algebraic type\ diff -r 4832491d1376 -r adffc55a682d src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Thu Mar 10 22:49:15 2016 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Thu Mar 10 22:49:24 2016 +0100 @@ -131,9 +131,7 @@ error_at ctxt eqns ("Unexpected corecursive call in " ^ quote (Syntax.string_of_term ctxt t)); fun unsupported_case_around_corec_call ctxt eqns t = error_at ctxt eqns ("Unsupported corecursive call under case expression " ^ - quote (Syntax.string_of_term ctxt t) ^ "\n(Define " ^ - quote (Syntax.string_of_typ ctxt (domain_type (fastype_of t))) ^ - " with discriminators and selectors to circumvent this limitation.)"); + quote (Syntax.string_of_term ctxt t) ^ " for datatype with no discriminators and selectors"); fun use_primcorecursive () = error ("\"auto\" failed (try " ^ quote (#1 @{command_keyword primcorecursive}) ^ " instead of " ^ quote (#1 @{command_keyword primcorec}) ^ ")"); @@ -359,7 +357,7 @@ fun massage_mutual_call bound_Ts (Type (@{type_name fun}, [_, U2])) (Type (@{type_name fun}, [T1, T2])) t = - Abs (Name.uu, T1, massage_mutual_call bound_Ts U2 T2 (incr_boundvars 1 t $ Bound 0)) + Abs (Name.uu, T1, massage_mutual_call (T1 :: bound_Ts) U2 T2 (incr_boundvars 1 t $ Bound 0)) | massage_mutual_call bound_Ts U T t = (if has_call t then massage_call else massage_noncall) bound_Ts U T t; diff -r 4832491d1376 -r adffc55a682d src/HOL/Tools/Predicate_Compile/mode_inference.ML --- a/src/HOL/Tools/Predicate_Compile/mode_inference.ML Thu Mar 10 22:49:15 2016 +0100 +++ b/src/HOL/Tools/Predicate_Compile/mode_inference.ML Thu Mar 10 22:49:24 2016 +0100 @@ -167,7 +167,8 @@ fold find' xs NONE end -fun is_invertible_function ctxt (Const (f, _)) = is_constr ctxt f +fun is_invertible_function ctxt (Const cT) = + is_some (lookup_constr ctxt cT) | is_invertible_function ctxt _ = false fun non_invertible_subterms ctxt (Free _) = [] diff -r 4832491d1376 -r adffc55a682d src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Mar 10 22:49:15 2016 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Mar 10 22:49:24 2016 +0100 @@ -43,9 +43,8 @@ val is_pred_equation : thm -> bool val is_intro : string -> thm -> bool val is_predT : typ -> bool - val get_constrs : theory -> (string * (int * string)) list - val is_constrt : theory -> term -> bool - val is_constr : Proof.context -> string -> bool + val lookup_constr : Proof.context -> (string * typ) -> int option + val is_constrt : Proof.context -> term -> bool val strip_ex : term -> (string * typ) list * term val focus_ex : term -> Name.context -> ((string * typ) list * term) * Name.context val strip_all : term -> (string * typ) list * term @@ -166,8 +165,6 @@ structure Predicate_Compile_Aux : PREDICATE_COMPILE_AUX = struct -val no_constr = [@{const_name STR}]; - (* general functions *) fun comb_option f (SOME x1, SOME x2) = SOME (f (x1, x2)) @@ -478,37 +475,32 @@ fun is_predT (T as Type("fun", [_, _])) = (body_type T = @{typ bool}) | is_predT _ = false -fun get_constrs thy = +fun lookup_constr ctxt = let - val ctxt = Proof_Context.init_global thy - in - Ctr_Sugar.ctr_sugars_of ctxt - |> maps (map_filter (try dest_Const) o #ctrs) - |> map (apsnd (fn T => (BNF_Util.num_binder_types T, fst (dest_Type (body_type T))))) - end + val tab = Ctr_Sugar.ctr_sugars_of ctxt + |> maps (map_filter (try dest_Const) o #ctrs) + |> map (fn (c, T) => ((c, (fst o dest_Type o body_type) T), BNF_Util.num_binder_types T)) + in fn (c, T) => + case body_type T of + Type (Tname, _) => AList.lookup (op =) tab (c, Tname) + | _ => NONE + end; -(*** check if a term contains only constructor functions ***) -(* TODO: another copy in the core! *) -(* FIXME: constructor terms are supposed to be seen in the way the code generator - sees constructors.*) -fun is_constrt thy = +fun is_constrt ctxt = let - val cnstrs = get_constrs thy + val lookup_constr = lookup_constr ctxt fun check t = (case strip_comb t of (Var _, []) => true | (Free _, []) => true - | (Const (s, T), ts) => - (case (AList.lookup (op =) cnstrs s, body_type T) of - (SOME (i, Tname), Type (Tname', _)) => - length ts = i andalso Tname = Tname' andalso forall check ts + | (Const cT, ts) => + (case lookup_constr cT of + SOME i => + length ts = i andalso forall check ts | _ => false) | _ => false) in check end -fun is_constr ctxt c = - not (member (op =) no_constr c) andalso Code.is_constr (Proof_Context.theory_of ctxt) c; - fun strip_all t = (Term.strip_all_vars t, Term.strip_all_body t) fun strip_ex (Const (@{const_name Ex}, _) $ Abs (x, T, t)) = diff -r 4832491d1376 -r adffc55a682d src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Mar 10 22:49:15 2016 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Mar 10 22:49:24 2016 +0100 @@ -94,6 +94,7 @@ fun flatten thy lookup_pred t (names, prems) = let + val ctxt = Proof_Context.init_global thy; fun lift t (names, prems) = (case lookup_pred (Envir.eta_contract t) of SOME pred => [(pred, (names, prems))] @@ -139,7 +140,9 @@ | flatten' (t as Free _) (names, prems) = [(t, (names, prems))] | flatten' (t as Abs _) (names, prems) = [(t, (names, prems))] | flatten' (t as _ $ _) (names, prems) = - if Predicate_Compile_Aux.is_constrt thy t orelse keep_functions thy t then + if is_constrt ctxt t orelse keep_functions thy t then + (* FIXME: constructor terms are supposed to be seen in the way the code generator + sees constructors?*) [(t, (names, prems))] else case (fst (strip_comb t)) of diff -r 4832491d1376 -r adffc55a682d src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Thu Mar 10 22:49:15 2016 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Thu Mar 10 22:49:24 2016 +0100 @@ -41,19 +41,19 @@ end (* patterns only constructed of variables and pairs/tuples are trivial constructor terms*) -fun is_nontrivial_constrt thy t = +fun is_nontrivial_constrt ctxt t = let - val cnstrs = get_constrs thy + val lookup_constr = lookup_constr ctxt fun check t = (case strip_comb t of (Var _, []) => (true, true) | (Free _, []) => (true, true) | (Const (@{const_name Pair}, _), ts) => apply2 (forall I) (split_list (map check ts)) - | (Const (s, T), ts) => - (case (AList.lookup (op =) cnstrs s, body_type T) of - (SOME (i, Tname), Type (Tname', _)) => (false, - length ts = i andalso Tname = Tname' andalso forall (snd o check) ts) + | (Const cT, ts) => + (case lookup_constr cT of + SOME i => (false, + length ts = i andalso forall (snd o check) ts) | _ => (false, false)) | _ => (false, false)) in check t = (false, true) end @@ -167,7 +167,7 @@ val Ts = binder_types (Sign.the_const_type thy pred_name) val pats = restrict_pattern thy Ts args in - if (exists (is_nontrivial_constrt thy) pats) + if (exists (is_nontrivial_constrt ctxt) pats) orelse (has_duplicates (op =) (fold add_vars pats [])) then let val thy' =