--- 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..<j] = i # [Suc i..<j]"
by (simp add: upt_rec)
+lemma upt_conv_Cons_Cons: -- \<open>no precondition\<close>
+ "m # n # ns = [m..<q] \<longleftrightarrow> n # ns = [Suc m..<q]"
+proof (cases "m < q")
+ case False then show ?thesis by simp
+next
+ case True then show ?thesis by (simp add: upt_conv_Cons)
+qed
+
lemma upt_add_eq_append: "i<=j ==> [i..<j+k] = [i..<j]@[j..<j+k]"
\<comment> \<open>LOOPS as a simprule, since \<open>j <= j\<close>.\<close>
by (induct k) auto
--- 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: -- \<open>no precondition\<close> -- \<open>FIXME move\<close>
- "m # n # ns = [m..<q] \<longleftrightarrow> n # ns = [Suc m..<q]"
-proof (cases "m < q")
- case False then show ?thesis by simp
-next
- case True then show ?thesis by (simp add: upt_conv_Cons)
-qed
-
-
subsection \<open>Characters and strings\<close>
subsubsection \<open>Characters as finite algebraic type\<close>
--- 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;
--- 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 _) = []
--- 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)) =
--- 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
--- 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' =