# HG changeset patch # User haftmann # Date 1457609584 -3600 # Node ID fc5198b44314427f758b9e11328dd1d2a7633ac7 # Parent 7011429f44f98e4048e70ef71d785f3057f37ceb clarified: constructors in the sense of the code generator are not invertible; correct treatment of constructors with same name but different type; moved doubtful comment to corresponding function call diff -r 7011429f44f9 -r fc5198b44314 src/HOL/Tools/Predicate_Compile/mode_inference.ML --- a/src/HOL/Tools/Predicate_Compile/mode_inference.ML Thu Mar 10 12:33:01 2016 +0100 +++ b/src/HOL/Tools/Predicate_Compile/mode_inference.ML Thu Mar 10 12:33:04 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 7011429f44f9 -r fc5198b44314 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Mar 10 12:33:01 2016 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Mar 10 12:33:04 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 7011429f44f9 -r fc5198b44314 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Mar 10 12:33:01 2016 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Mar 10 12:33:04 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 7011429f44f9 -r fc5198b44314 src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Thu Mar 10 12:33:01 2016 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML Thu Mar 10 12:33:04 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' =