From 46b671c7473385ec7747a796e85b3cf704d000c6 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 27 Jul 2017 16:10:49 +0200 Subject: Evd/evarsolve: add an abstraction field to evars for unification Named evar_abstract_arguments, this field indicates if the evar arguments corresponding to certain hypothesis can be immitated during inversion or not. If the argument comes from an abstraction (the evar was of arrow type), then imitation is disallowed as it gives unnatural solutions, and lambda abstraction is preferred. --- engine/evarutil.ml | 16 ++++++++++------ engine/evarutil.mli | 7 ++++--- engine/evd.ml | 11 +++++++++++ engine/evd.mli | 12 ++++++++++++ pretyping/evardefine.ml | 3 ++- proofs/goal.ml | 1 + 6 files changed, 40 insertions(+), 10 deletions(-) diff --git a/engine/evarutil.ml b/engine/evarutil.ml index d70c009c6d..840c14b241 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -424,8 +424,8 @@ let new_pure_evar_full evd ?typeclass_candidate evi = let evd = Evd.declare_future_goal evk evd in (evd, evk) -let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?naming ?typeclass_candidate - ?(principal=false) sign evd typ = +let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?(abstract_arguments = Abstraction.identity) + ?candidates ?naming ?typeclass_candidate ?(principal=false) sign evd typ = let default_naming = IntroAnonymous in let naming = Option.default default_naming naming in let name = match naming with @@ -441,6 +441,7 @@ let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ? evar_concl = typ; evar_body = Evar_empty; evar_filter = filter; + evar_abstract_arguments = abstract_arguments; evar_source = src; evar_candidates = candidates } in @@ -452,11 +453,12 @@ let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ? in (evd, newevk) -let new_evar_instance ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal sign evd typ instance = +let new_evar_instance ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_candidate + ?principal sign evd typ instance = let open EConstr in assert (not !Flags.debug || List.distinct (ids_of_named_context (named_context_of_val sign))); - let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal typ in + let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_candidate ?principal typ in evd, mkEvar (newevk,Array.of_list instance) let new_evar_from_context ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal sign evd typ = @@ -469,7 +471,8 @@ let new_evar_from_context ?src ?filter ?candidates ?naming ?typeclass_candidate (* [new_evar] declares a new existential in an env env with type typ *) (* Converting the env into the sign of the evar to define *) -let new_evar ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal ?hypnaming env evd typ = +let new_evar ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_candidate + ?principal ?hypnaming env evd typ = let sign,typ',instance,subst = push_rel_context_to_named_context ?hypnaming env evd typ in let map c = csubst_subst subst c in let candidates = Option.map (fun l -> List.map map l) candidates in @@ -477,7 +480,8 @@ let new_evar ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal ?h match filter with | None -> instance | Some filter -> Filter.filter_list filter instance in - new_evar_instance sign evd typ' ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal instance + new_evar_instance sign evd typ' ?src ?filter ?abstract_arguments ?candidates ?naming + ?typeclass_candidate ?principal instance let new_type_evar ?src ?filter ?naming ?principal ?hypnaming env evd rigid = let (evd', s) = new_sort_variable rigid evd in diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 23b240f1a0..bb0da44103 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -42,7 +42,7 @@ type naming_mode = val new_evar : ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?candidates:constr list -> + ?abstract_arguments:Abstraction.t -> ?candidates:constr list -> ?naming:intro_pattern_naming_expr -> ?typeclass_candidate:bool -> ?principal:bool -> ?hypnaming:naming_mode -> @@ -50,7 +50,7 @@ val new_evar : val new_pure_evar : ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?candidates:constr list -> + ?abstract_arguments:Abstraction.t -> ?candidates:constr list -> ?naming:intro_pattern_naming_expr -> ?typeclass_candidate:bool -> ?principal:bool -> @@ -80,7 +80,8 @@ val new_global : evar_map -> GlobRef.t -> evar_map * constr of [inst] are typed in the occurrence context and their type (seen as a telescope) is [sign] *) val new_evar_instance : - ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> + ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> + ?abstract_arguments:Abstraction.t -> ?candidates:constr list -> ?naming:intro_pattern_naming_expr -> ?typeclass_candidate:bool -> ?principal:bool -> diff --git a/engine/evd.ml b/engine/evd.ml index eee2cb700c..2d28892e6e 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -126,6 +126,15 @@ struct end +module Abstraction = struct + + type t = bool list + + let identity = [] + + let abstract_last l = true :: l +end + (* The kinds of existential variables are now defined in [Evar_kinds] *) (* The type of mappings for existential variables *) @@ -143,6 +152,7 @@ type evar_info = { evar_hyps : named_context_val; evar_body : evar_body; evar_filter : Filter.t; + evar_abstract_arguments : Abstraction.t; evar_source : Evar_kinds.t Loc.located; evar_candidates : constr list option; (* if not None, list of allowed instances *)} @@ -151,6 +161,7 @@ let make_evar hyps ccl = { evar_hyps = hyps; evar_body = Evar_empty; evar_filter = Filter.identity; + evar_abstract_arguments = Abstraction.identity; evar_source = Loc.tag @@ Evar_kinds.InternalHole; evar_candidates = None; } diff --git a/engine/evd.mli b/engine/evd.mli index de73144895..1c852971f5 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -77,6 +77,14 @@ sig end +module Abstraction : sig + type t = bool list + + val identity : t + + val abstract_last : t -> t +end + (** {6 Evar infos} *) type evar_body = @@ -94,6 +102,10 @@ type evar_info = { (** Boolean mask over {!evar_hyps}. Should have the same length. When filtered out, the corresponding variable is not allowed to occur in the solution *) + evar_abstract_arguments : Abstraction.t; + (** Boolean information over {!evar_hyps}, telling if an hypothesis instance + can be immitated or should stay abstract in HO unification problems + and inversion (see [second_order_matching_with_args] for its use). *) evar_source : Evar_kinds.t located; (** Information about the evar. *) evar_candidates : econstr list option; diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index 571be7466c..a62427834d 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -139,7 +139,8 @@ let define_pure_evar_as_lambda env evd evk = let newenv = push_named (LocalAssum (id, dom)) evenv in let filter = Filter.extend 1 (evar_filter evi) in let src = subterm_source evk ~where:Body (evar_source evk evd1) in - let evd2,body = new_evar newenv evd1 ~src (subst1 (mkVar id) rng) ~filter in + let abstract_arguments = Abstraction.abstract_last evi.evar_abstract_arguments in + let evd2,body = new_evar newenv evd1 ~src (subst1 (mkVar id) rng) ~filter ~abstract_arguments in let lam = mkLambda (Name id, dom, subst_var id body) in Evd.define evk lam evd2, lam diff --git a/proofs/goal.ml b/proofs/goal.ml index 7245d4a004..2104eefa66 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -60,6 +60,7 @@ module V82 = struct let evi = { Evd.evar_hyps = hyps; Evd.evar_concl = concl; Evd.evar_filter = Evd.Filter.identity; + Evd.evar_abstract_arguments = Evd.Abstraction.identity; Evd.evar_body = Evd.Evar_empty; Evd.evar_source = (Loc.tag Evar_kinds.GoalEvar); Evd.evar_candidates = None } -- cgit v1.2.3 From c039d78bd098a499a34038e64bd1e5fbe280d7f3 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 28 Jul 2017 15:31:28 +0200 Subject: locus: Add an AtLeastOneOccurrence constructor. The semantics is obviously that it is an error if not at least one occurrence is found (natural semantics for rewriting for example). --- plugins/ltac/tacintern.ml | 2 +- plugins/ltac/tacinterp.ml | 2 +- pretyping/evarconv.ml | 2 +- pretyping/find_subterm.ml | 2 +- pretyping/locus.ml | 1 + pretyping/locusops.ml | 17 ++++++++++++----- pretyping/locusops.mli | 2 ++ pretyping/tacred.ml | 1 + pretyping/unification.ml | 2 +- tactics/autorewrite.ml | 2 +- tactics/equality.ml | 15 ++++++++------- tactics/ppred.ml | 1 + 12 files changed, 31 insertions(+), 18 deletions(-) diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index a1e21aab04..543d4de0fe 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -557,7 +557,7 @@ let rec intern_atomic lf ist x = | _ -> false in let is_onconcl = match cl.concl_occs with - | AllOccurrences | NoOccurrences -> true + | AtLeastOneOccurrence | AllOccurrences | NoOccurrences -> true | _ -> false in TacChange (None, diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 525ff7fd0f..d17a8e3cc8 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1746,7 +1746,7 @@ and interp_atomic ist tac : unit Proofview.tactic = | _ -> false in let is_onconcl = match cl.concl_occs with - | AllOccurrences | NoOccurrences -> true + | AtLeastOneOccurrence | AllOccurrences | NoOccurrences -> true | _ -> false in let c_interp patvars env sigma = diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index aa30ed8d2e..f8e5e0759b 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1148,7 +1148,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = | (id,_,c,cty,evsref,filter,occs)::subst -> let set_var k = match occs with - | Some Locus.AllOccurrences -> mkVar id + | Some (Locus.AtLeastOneOccurrence | Locus.AllOccurrences) -> mkVar id | Some _ -> user_err Pp.(str "Selection of specific occurrences not supported") | None -> let evty = set_holes evdref cty subst in diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml index b16087031b..d150f8e1cb 100644 --- a/pretyping/find_subterm.ml +++ b/pretyping/find_subterm.ml @@ -125,7 +125,7 @@ let replace_term_occ_gen_modulo sigma occs like_first test bywhat cl occ t = end; add_subst t subst; incr pos; (* Check nested matching subterms *) - if occs != Locus.AllOccurrences && occs != Locus.NoOccurrences then + if not (Locusops.is_all_occurrences occs) && occs != Locus.NoOccurrences then begin nested := true; ignore (subst_below k t); nested := false end; (* Do the effective substitution *) Vars.lift k (bywhat ())) diff --git a/pretyping/locus.ml b/pretyping/locus.ml index 37dd120c1a..087a6b9174 100644 --- a/pretyping/locus.ml +++ b/pretyping/locus.ml @@ -20,6 +20,7 @@ type 'a or_var = type 'a occurrences_gen = | AllOccurrences + | AtLeastOneOccurrence | AllOccurrencesBut of 'a list (** non-empty *) | NoOccurrences | OnlyOccurrences of 'a list (** non-empty *) diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml index 6b6a3f8a9f..aaa4ce684d 100644 --- a/pretyping/locusops.ml +++ b/pretyping/locusops.ml @@ -19,15 +19,17 @@ let occurrences_map f = function | AllOccurrencesBut l -> let l' = f l in if l' = [] then AllOccurrences else AllOccurrencesBut l' - | (NoOccurrences|AllOccurrences) as o -> o + | (NoOccurrences|AllOccurrences|AtLeastOneOccurrence) as o -> o let convert_occs = function + | AtLeastOneOccurrence -> (false,[]) | AllOccurrences -> (false,[]) | AllOccurrencesBut l -> (false,l) | NoOccurrences -> (true,[]) | OnlyOccurrences l -> (true,l) let is_selected occ = function + | AtLeastOneOccurrence -> true | AllOccurrences -> true | AllOccurrencesBut l -> not (Int.List.mem occ l) | OnlyOccurrences l -> Int.List.mem occ l @@ -46,6 +48,11 @@ let is_nowhere = function | { onhyps=Some[]; concl_occs=NoOccurrences } -> true | _ -> false +let is_all_occurrences = function + | AtLeastOneOccurrence + | AllOccurrences -> true + | _ -> false + (** Clause conversion functions, parametrized by a hyp enumeration function *) (** From [clause] to [simple_clause] *) @@ -61,12 +68,12 @@ let simple_clause_of enum_hyps cl = List.map Option.make (enum_hyps ()) | Some l -> List.map (fun ((occs,id),w) -> - if occs <> AllOccurrences then error_occurrences (); + if not (is_all_occurrences occs) then error_occurrences (); if w = InHypValueOnly then error_body_selection (); Some id) l in if cl.concl_occs = NoOccurrences then hyps else - if cl.concl_occs <> AllOccurrences then error_occurrences () + if not (is_all_occurrences cl.concl_occs) then error_occurrences () else None :: hyps (** From [clause] to [concrete_clause] *) @@ -111,7 +118,7 @@ let clause_with_generic_occurrences cls = List.for_all (function ((AllOccurrences,_),_) -> true | _ -> false) hyps in let concl = match cls.concl_occs with - | AllOccurrences | NoOccurrences -> true + | AtLeastOneOccurrence | AllOccurrences | NoOccurrences -> true | _ -> false in hyps && concl @@ -122,6 +129,6 @@ let clause_with_generic_context_selection cls = List.for_all (function ((AllOccurrences,_),InHyp) -> true | _ -> false) hyps in let concl = match cls.concl_occs with - | AllOccurrences | NoOccurrences -> true + | AtLeastOneOccurrence | AllOccurrences | NoOccurrences -> true | _ -> false in hyps && concl diff --git a/pretyping/locusops.mli b/pretyping/locusops.mli index a07c018c32..ac15fe1018 100644 --- a/pretyping/locusops.mli +++ b/pretyping/locusops.mli @@ -21,6 +21,8 @@ val convert_occs : occurrences -> bool * int list val is_selected : int -> occurrences -> bool +val is_all_occurrences : 'a occurrences_gen -> bool + (** Usual clauses *) val allHypsAndConcl : 'a clause_expr diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 2308a541fb..5db571433a 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1105,6 +1105,7 @@ let unfoldoccs env sigma (occs,name) c = | AllOccurrences -> unfold env sigma name c | OnlyOccurrences l -> unfo true l | AllOccurrencesBut l -> unfo false l + | AtLeastOneOccurrence -> unfo false [] (* Unfold reduction tactic: *) let unfoldn loccname env sigma c = diff --git a/pretyping/unification.ml b/pretyping/unification.ml index ac0b58b92b..ce97912b84 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1649,7 +1649,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = match occurrences_of_hyp hyp occs with | NoOccurrences, InHyp -> (push_named_context_val d sign,depdecls) - | AllOccurrences, InHyp as occ -> + | (AllOccurrences | AtLeastOneOccurrence), InHyp as occ -> let occ = if likefirst then LikeFirst else AtOccs occ in let newdecl = replace_term_occ_decl_modulo sigma occ test mkvarid d in if Context.Named.Declaration.equal (EConstr.eq_constr sigma) d newdecl diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index f824552705..3b8232d20a 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -145,7 +145,7 @@ let gen_auto_multi_rewrite conds tac_main lbas cl = let try_do_hyps treat_id l = autorewrite_multi_in ~conds (List.map treat_id l) tac_main lbas in - if cl.concl_occs != AllOccurrences && + if not (Locusops.is_all_occurrences cl.concl_occs) && cl.concl_occs != NoOccurrences then Tacticals.New.tclZEROMSG (str"The \"at\" syntax isn't available yet for the autorewrite tactic.") diff --git a/tactics/equality.ml b/tactics/equality.ml index 769e702da1..a8cfc87f9c 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -437,7 +437,7 @@ let rewrite_side_tac tac sidetac = side_tac tac (Option.map fst sidetac) let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac ((c,l) : constr with_bindings) with_evars = - if occs != AllOccurrences then ( + if not (Locusops.is_all_occurrences occs) then ( rewrite_side_tac (Hook.get forward_general_setoid_rewrite_clause cls lft2rgt occs (c,l) ~new_goals:[]) tac) else Proofview.Goal.enter begin fun gl -> @@ -595,15 +595,16 @@ let init_setoid () = if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then () else check_required_library ["Coq";"Setoids";"Setoid"] -let check_setoid cl = +let check_setoid cl = + let concloccs = Locusops.occurrences_map (fun x -> x) cl.concl_occs in Option.fold_left - ( List.fold_left + (List.fold_left (fun b ((occ,_),_) -> - b||(Locusops.occurrences_map (fun x -> x) occ <> AllOccurrences) + b||(not (Locusops.is_all_occurrences (Locusops.occurrences_map (fun x -> x) occ))) ) ) - ((Locusops.occurrences_map (fun x -> x) cl.concl_occs <> AllOccurrences) && - (Locusops.occurrences_map (fun x -> x) cl.concl_occs <> NoOccurrences)) + (not (Locusops.is_all_occurrences concloccs) && + (concloccs <> NoOccurrences)) cl.onhyps let replace_core clause l2r eq = @@ -1724,7 +1725,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) = tclTHENLIST ((if need_rewrite then [revert (List.map snd dephyps); - general_rewrite dir AllOccurrences true dep_proof_ok (mkVar hyp); + general_rewrite dir AtLeastOneOccurrence true dep_proof_ok (mkVar hyp); (tclMAP (fun (dest,id) -> intro_move (Some id) dest) dephyps)] else [Proofview.tclUNIT ()]) @ diff --git a/tactics/ppred.ml b/tactics/ppred.ml index dd1bcd4699..d832dc279c 100644 --- a/tactics/ppred.ml +++ b/tactics/ppred.ml @@ -6,6 +6,7 @@ open Pputils let pr_with_occurrences pr keyword (occs,c) = match occs with + | AtLeastOneOccurrence -> hov 1 (pr c ++ spc () ++ keyword "at" ++ str" +") | AllOccurrences -> pr c | NoOccurrences -> -- cgit v1.2.3 From 746e74ed6e70cf01f0a0e73f772c3565e28fe3f8 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 26 Jul 2018 17:07:08 +0200 Subject: [evarconv] New flag handling for unifier --- pretyping/cases.ml | 12 +- pretyping/coercion.ml | 30 +-- pretyping/coercion.mli | 7 +- pretyping/evarconv.ml | 621 ++++++++++++++++++++++++++++------------------- pretyping/evarconv.mli | 26 +- pretyping/evarsolve.ml | 136 ++++++----- pretyping/evarsolve.mli | 27 ++- pretyping/pretyping.ml | 2 +- pretyping/unification.ml | 16 +- proofs/evar_refiner.ml | 4 +- tactics/class_tactics.ml | 2 +- 11 files changed, 530 insertions(+), 353 deletions(-) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index ed7c3d6770..57725dbdc1 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1707,9 +1707,12 @@ let abstract_tycon ?loc env sigma subst tycon extenv t = try list_assoc_in_triple i subst0 with Not_found -> mkRel i) 1 (rel_context !!env) in let sigma, ev' = Evarutil.new_evar ~src ~typeclass_candidate:false !!env sigma ty in - begin match solve_simple_eqn (evar_conv_x TransparentState.full) !!env sigma (None,ev,substl inst ev') with - | Success evd -> evdref := evd - | UnifFailure _ -> assert false + begin + let flags = (default_flags_of TransparentState.full) in + let conv = conv_fun evar_conv_x flags in + match solve_simple_eqn conv !!env sigma (None,ev,substl inst ev') with + | Success evd -> evdref := evd + | UnifFailure _ -> assert false end; ev' | _ -> @@ -1945,7 +1948,8 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign = let inh_conv_coerce_to_tycon ?loc ~program_mode env sigma j tycon = match tycon with - | Some p -> Coercion.inh_conv_coerce_to ?loc ~program_mode true env sigma j p + | Some p -> Coercion.inh_conv_coerce_to ?loc ~program_mode true env sigma + ~flags:(default_flags_of TransparentState.full) j p | None -> sigma, j (* We put the tycon inside the arity signature, possibly discovering dependencies. *) diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 9e93c470b1..a8bcec10e8 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -466,7 +466,7 @@ let inh_coerce_to_prod ?loc ~program_mode env evd t = !evdref, typ' else (evd, t) -let inh_coerce_to_fail env evd rigidonly v t c1 = +let inh_coerce_to_fail flags env evd rigidonly v t c1 = if rigidonly && not (Heads.is_rigid env (EConstr.Unsafe.to_constr c1) && Heads.is_rigid env (EConstr.Unsafe.to_constr t)) then raise NoCoercion @@ -483,13 +483,16 @@ let inh_coerce_to_fail env evd rigidonly v t c1 = | None -> evd, None, t with Not_found -> raise NoCoercion in - try (the_conv_x_leq env t' c1 evd, v') + try (unify_leq flags env evd t' c1, v') with UnableToUnify _ -> raise NoCoercion -let rec inh_conv_coerce_to_fail ?loc env evd rigidonly v t c1 = - try (the_conv_x_leq env t c1 evd, v) +let default_flags_of env = + default_flags_of TransparentState.full + +let rec inh_conv_coerce_to_fail ?loc env evd ?(flags=default_flags_of env) rigidonly v t c1 = + try (unify_leq flags env evd t c1, v) with UnableToUnify (best_failed_evd,e) -> - try inh_coerce_to_fail env evd rigidonly v t c1 + try inh_coerce_to_fail flags env evd rigidonly v t c1 with NoCoercion -> match EConstr.kind evd (whd_all env evd t), @@ -520,10 +523,10 @@ let rec inh_conv_coerce_to_fail ?loc env evd rigidonly v t c1 = | _ -> raise (NoCoercionNoUnifier (best_failed_evd,e)) (* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *) -let inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc rigidonly env evd cj t = +let inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc rigidonly flags env evd cj t = let (evd', val') = try - inh_conv_coerce_to_fail ?loc env evd rigidonly (Some cj.uj_val) cj.uj_type t + inh_conv_coerce_to_fail ?loc env evd ~flags rigidonly (Some cj.uj_val) cj.uj_type t with NoCoercionNoUnifier (best_failed_evd,e) -> try if program_mode then @@ -545,15 +548,14 @@ let inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc rigidonly env evd cj t let val' = match val' with Some v -> v | None -> assert(false) in (evd',{ uj_val = val'; uj_type = t }) -let inh_conv_coerce_to ?loc ~program_mode resolve_tc = - inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc false - -let inh_conv_coerce_rigid_to ?loc ~program_mode resolve_tc = - inh_conv_coerce_to_gen ~program_mode resolve_tc ?loc true +let inh_conv_coerce_to ?loc ~program_mode resolve_tc env evd ?(flags=default_flags_of env) = + inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc false flags env evd +let inh_conv_coerce_rigid_to ?loc ~program_mode resolve_tc env evd ?(flags=default_flags_of env) = + inh_conv_coerce_to_gen ?loc ~program_mode resolve_tc true flags env evd -let inh_conv_coerces_to ?loc env evd t t' = +let inh_conv_coerces_to ?loc env evd ?(flags=default_flags_of env) t t' = try - fst (inh_conv_coerce_to_fail ?loc env evd true None t t') + fst (inh_conv_coerce_to_fail ?loc env evd ~flags true None t t') with NoCoercion -> evd (* Maybe not enough information to unify *) diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli index a941391125..c954a2a851 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.mli @@ -45,11 +45,14 @@ val inh_coerce_to_prod : ?loc:Loc.t -> program_mode:bool -> a way [t] and [j.uj_type] are convertible; it fails if no coercion is applicable. resolve_tc=false disables resolving type classes (as the last resort before failing) *) + val inh_conv_coerce_to : ?loc:Loc.t -> program_mode:bool -> bool -> - env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment + env -> evar_map -> ?flags:Evarconv.unify_flags -> + unsafe_judgment -> types -> evar_map * unsafe_judgment val inh_conv_coerce_rigid_to : ?loc:Loc.t -> program_mode:bool ->bool -> - env -> evar_map -> unsafe_judgment -> types -> evar_map * unsafe_judgment + env -> evar_map -> ?flags:Evarconv.unify_flags -> + unsafe_judgment -> types -> evar_map * unsafe_judgment (** [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t] is coercible to an object of type [t'] adding evar constraints if needed; diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index f8e5e0759b..de5f00f71a 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -24,14 +24,28 @@ open Evardefine open Evarsolve open Evd open Pretype_errors -open Context.Named.Declaration module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration -type unify_fun = TransparentState.t -> +type unify_flags = Evarsolve.unify_flags + +type unify_fun = unify_flags -> env -> evar_map -> conv_pb -> EConstr.constr -> EConstr.constr -> Evarsolve.unification_result +let default_transparent_state env = TransparentState.full +(* Conv_oracle.get_transp_state (Environ.oracle env) *) + +let default_flags_of ?(subterm_ts=TransparentState.empty) ts = + { modulo_betaiota = true; + open_ts = ts; closed_ts = ts; subterm_ts; + frozen_evars = Evar.Set.empty; with_cs = true; + allow_K_at_toplevel = true } + +let default_flags env = + let ts = default_transparent_state env in + default_flags_of ts + let debug_unification = ref (false) let () = Goptions.(declare_bool_option { optdepr = false; @@ -42,6 +56,16 @@ let () = Goptions.(declare_bool_option { optwrite = (fun a -> debug_unification:=a); }) +let debug_ho_unification = ref (false) +let () = Goptions.(declare_bool_option { + optdepr = false; + optname = + "Print higher-order unification debug information"; + optkey = ["Debug";"HO";"Unification"]; + optread = (fun () -> !debug_ho_unification); + optwrite = (fun a -> debug_ho_unification:=a); +}) + (*******************************************) (* Functions to deal with impossible cases *) (*******************************************) @@ -101,22 +125,28 @@ type flex_kind_of_term = | MaybeFlexible of EConstr.t (* reducible but not necessarily reduced *) | Flexible of EConstr.existential -let flex_kind_of_term ts env evd c sk = +let is_frozen flags (evk, _) = Evar.Set.mem evk flags.frozen_evars + +let flex_kind_of_term flags env evd c sk = match EConstr.kind evd c with | LetIn _ | Rel _ | Const _ | Var _ | Proj _ -> - Option.cata (fun x -> MaybeFlexible x) Rigid (eval_flexible_term ts env evd c) - | Lambda _ when not (Option.is_empty (Stack.decomp sk)) -> MaybeFlexible c - | Evar ev -> Flexible ev + Option.cata (fun x -> MaybeFlexible x) Rigid (eval_flexible_term flags.open_ts env evd c) + | Lambda _ when not (Option.is_empty (Stack.decomp sk)) -> + if flags.modulo_betaiota then MaybeFlexible c + else Rigid + | Evar ev -> + if is_frozen flags ev then Rigid + else Flexible ev | Lambda _ | Prod _ | Sort _ | Ind _ | Construct _ | CoFix _ | Int _ -> Rigid | Meta _ -> Rigid | Fix _ -> Rigid (* happens when the fixpoint is partially applied *) | Cast _ | App _ | Case _ -> assert false -let apprec_nohdbeta ts env evd c = +let apprec_nohdbeta flags env evd c = let (t,sk as appr) = Reductionops.whd_nored_state evd (c, []) in - if Stack.not_purely_applicative sk + if flags.modulo_betaiota && Stack.not_purely_applicative sk then Stack.zip evd (fst (whd_betaiota_deltazeta_for_iota_state - ts env evd Cst_stack.empty appr)) + flags.open_ts env evd Cst_stack.empty appr)) else c let position_problem l2r = function @@ -365,7 +395,15 @@ let compare_cumulative_instances evd variances u u' = Success evd | Inr p -> UnifFailure (evd, UnifUnivInconsistency p) -let rec evar_conv_x ts env evd pbty term1 term2 = +let conv_fun f flags on_types = + let typefn env evd pbty term1 term2 = + f { (default_flags env) with with_cs = flags.with_cs } env evd pbty term1 term2 + in + let termfn env evd pbty term1 term2 = + f flags env evd pbty term1 term2 + in if on_types then typefn else termfn + +let rec evar_conv_x flags env evd pbty term1 term2 = let term1 = whd_head_evar evd term1 in let term2 = whd_head_evar evd term2 in (* Maybe convertible but since reducing can erase evars which [evar_apprec] @@ -374,7 +412,7 @@ let rec evar_conv_x ts env evd pbty term1 term2 = let ground_test = if is_ground_term evd term1 && is_ground_term evd term2 then ( let e = - match infer_conv ~catch_incon:false ~pb:pbty ~ts:(fst ts) env evd term1 term2 with + match infer_conv ~catch_incon:false ~pb:pbty ~ts:flags.closed_ts env evd term1 term2 with | Some evd -> Success evd | None -> UnifFailure (evd, ConversionFailed (env,term1,term2)) | exception Univ.UniverseInconsistency e -> UnifFailure (evd, UnifUnivInconsistency e) @@ -389,30 +427,30 @@ let rec evar_conv_x ts env evd pbty term1 term2 = | None -> (* Until pattern-unification is used consistently, use nohdbeta to not destroy beta-redexes that can be used for 1st-order unification *) - let term1 = apprec_nohdbeta (fst ts) env evd term1 in - let term2 = apprec_nohdbeta (fst ts) env evd term2 in + let term1 = apprec_nohdbeta flags env evd term1 in + let term2 = apprec_nohdbeta flags env evd term2 in let default () = - evar_eqappr_x ts env evd pbty + evar_eqappr_x flags env evd pbty (whd_nored_state evd (term1,Stack.empty), Cst_stack.empty) (whd_nored_state evd (term2,Stack.empty), Cst_stack.empty) in begin match EConstr.kind evd term1, EConstr.kind evd term2 with - | Evar ev, _ when Evd.is_undefined evd (fst ev) -> - (match solve_simple_eqn (evar_conv_x ts) env evd - (position_problem true pbty,ev, term2) with + | Evar ev, _ when Evd.is_undefined evd (fst ev) && not (is_frozen flags ev) -> + (match solve_simple_eqn flags (conv_fun evar_conv_x flags) env evd + (position_problem true pbty,ev,term2) with | UnifFailure (_,OccurCheck _) -> (* Eta-expansion might apply *) default () | x -> x) - | _, Evar ev when Evd.is_undefined evd (fst ev) -> - (match solve_simple_eqn (evar_conv_x ts) env evd - (position_problem false pbty,ev, term1) with + | _, Evar ev when Evd.is_undefined evd (fst ev) && not (is_frozen flags ev) -> + (match solve_simple_eqn flags (conv_fun evar_conv_x flags) env evd + (position_problem false pbty,ev,term1) with | UnifFailure (_, OccurCheck _) -> (* Eta-expansion might apply *) default () | x -> x) | _ -> default () end -and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty +and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty ((term1,sk1 as appr1),csts1) ((term2,sk2 as appr2),csts2) = let quick_fail i = (* not costly, loses info *) UnifFailure (i, NotSameHead) @@ -423,18 +461,18 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | Some l1' -> (* Miller-Pfenning's patterns unification *) let t2 = tM in let t2 = solve_pattern_eqn env evd l1' t2 in - solve_simple_eqn (evar_conv_x ts) env evd + solve_simple_eqn flags (conv_fun evar_conv_x flags) env evd (position_problem on_left pbty,ev,t2) in let consume_stack on_left (termF,skF) (termO,skO) evd = let switch f a b = if on_left then f a b else f b a in let not_only_app = Stack.not_purely_applicative skO in - match switch (ise_stack2 not_only_app env evd (evar_conv_x ts)) skF skO with + match switch (ise_stack2 not_only_app env evd (evar_conv_x flags)) skF skO with |Some (l,r), Success i' when on_left && (not_only_app || List.is_empty l) -> - switch (evar_conv_x ts env i' pbty) (Stack.zip evd (termF,l)) (Stack.zip evd (termO,r)) + switch (evar_conv_x flags env i' pbty) (Stack.zip evd (termF,l)) (Stack.zip evd (termO,r)) |Some (r,l), Success i' when not on_left && (not_only_app || List.is_empty l) -> - switch (evar_conv_x ts env i' pbty) (Stack.zip evd (termF,l)) (Stack.zip evd (termO,r)) - |None, Success i' -> switch (evar_conv_x ts env i' pbty) termF termO + switch (evar_conv_x flags env i' pbty) (Stack.zip evd (termF,l)) (Stack.zip evd (termO,r)) + |None, Success i' -> switch (evar_conv_x flags env i' pbty) termF termO |_, (UnifFailure _ as x) -> x |Some _, _ -> UnifFailure (evd,NotSameArgSize) in let eta env evd onleft sk term sk' term' = @@ -443,12 +481,12 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let c = nf_evar evd c1 in let env' = push_rel (RelDecl.LocalAssum (na,c)) env in let out1 = whd_betaiota_deltazeta_for_iota_state - (fst ts) env' evd Cst_stack.empty (c'1, Stack.empty) in + flags.open_ts env' evd Cst_stack.empty (c'1, Stack.empty) in let out2 = whd_nored_state evd (lift 1 (Stack.zip evd (term', sk')), Stack.append_app [|EConstr.mkRel 1|] Stack.empty), Cst_stack.empty in - if onleft then evar_eqappr_x ts env' evd CONV out1 out2 - else evar_eqappr_x ts env' evd CONV out2 out1 + if onleft then evar_eqappr_x flags env' evd CONV out1 out2 + else evar_eqappr_x flags env' evd CONV out2 out1 in let rigids env evd sk term sk' term' = let check_strict evd u u' = @@ -506,12 +544,16 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty ise_and evd [(fun i -> try compare_heads i with Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p)); - (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk sk')] + (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk sk')] in - let flex_maybeflex on_left ev ((termF,skF as apprF),cstsF) ((termM, skM as apprM),cstsM) vM = + let consume on_left (_, skF as apprF) (_,skM as apprM) i = + if not (Stack.is_empty skF && Stack.is_empty skM) then + consume_stack on_left apprF apprM i + else quick_fail i + in + let miller on_left ev (termF,skF as apprF) (termM, skM as apprM) i = let switch f a b = if on_left then f a b else f b a in let not_only_app = Stack.not_purely_applicative skM in - let f1 i = match Stack.list_of_app_stack skF with | None -> quick_fail evd | Some lF -> @@ -520,17 +562,17 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (fun () -> if not_only_app then (* Postpone the use of an heuristic *) switch (fun x y -> Success (Evarutil.add_unification_pb (pbty,env,x,y) i)) (Stack.zip evd apprF) tM else quick_fail i) - ev lF tM i - and consume (termF,skF as apprF) (termM,skM as apprM) i = - if not (Stack.is_empty skF && Stack.is_empty skM) then - consume_stack on_left apprF apprM i - else quick_fail i - and delta i = - switch (evar_eqappr_x ts env i pbty) (apprF,cstsF) - (whd_betaiota_deltazeta_for_iota_state - (fst ts) env i cstsM (vM,skM)) + ev lF tM i + in + let flex_maybeflex on_left ev ((termF,skF as apprF),cstsF) ((termM, skM as apprM),cstsM) vM = + let switch f a b = if on_left then f a b else f b a in + let delta i = + switch (evar_eqappr_x flags env i pbty) (apprF,cstsF) + (whd_betaiota_deltazeta_for_iota_state flags.open_ts env i cstsM (vM,skM)) in - let default i = ise_try i [f1; consume apprF apprM; delta] + let default i = ise_try i [miller on_left ev apprF apprM; + consume on_left apprF apprM; + delta] in match EConstr.kind evd termM with | Proj (p, c) when not (Stack.is_empty skF) -> @@ -545,13 +587,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty try let termM' = Retyping.expand_projection env evd p c [] in let apprM', cstsM' = - whd_betaiota_deltazeta_for_iota_state - (fst ts) env evd cstsM (termM',skM) + whd_betaiota_deltazeta_for_iota_state flags.open_ts env evd cstsM (termM',skM) in let delta' i = - switch (evar_eqappr_x ts env i pbty) (apprF,cstsF) (apprM',cstsM') + switch (evar_eqappr_x flags env i pbty) (apprF,cstsF) (apprM',cstsM') in - fun i -> ise_try i [f1; consume apprF apprM'; delta'] + fun i -> ise_try i [miller on_left ev apprF apprM'; + consume on_left apprF apprM'; delta'] with Retyping.RetypeError _ -> (* Happens thanks to w_unify building ill-typed terms *) default @@ -565,7 +607,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty match EConstr.kind evd termR with | Lambda _ when (* if ever problem is ill-typed: *) List.is_empty skR -> eta env evd false skR termR skF termF - | Construct u -> eta_constructor ts env evd skR u skF termF + | Construct u -> eta_constructor flags env evd skR u skF termF | _ -> UnifFailure (evd,NotSameHead) in match Stack.list_of_app_stack skF with @@ -573,12 +615,12 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty ise_try evd [consume_stack on_left apprF apprR; eta] | Some lF -> let tR = Stack.zip evd apprR in - miller_pfenning on_left - (fun () -> - ise_try evd - [eta;(* Postpone the use of an heuristic *) - (fun i -> - if not (occur_rigidly ev i tR) then + miller_pfenning on_left + (fun () -> + ise_try evd + [eta;(* Postpone the use of an heuristic *) + (fun i -> + if not (occur_rigidly ev i tR) then let i,tF = if isRel i tR || isVar i tR then (* Optimization so as to generate candidates *) @@ -587,95 +629,99 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty else i,Stack.zip evd apprF in switch (fun x y -> Success (Evarutil.add_unification_pb (pbty,env,x,y) i)) - tF tR - else + tF tR + else UnifFailure (evd,OccurCheck (fst ev,tR)))]) - ev lF tR evd + ev lF tR evd + in + let first_order env i t1 t2 sk1 sk2 = + (* Try first-order unification *) + match ise_stack2 false env i (evar_conv_x flags) sk1 sk2 with + | None, Success i' -> + (* We do have sk1[] = sk2[]: we now unify ?ev1 and ?ev2 *) + (* Note that ?ev1 and ?ev2, may have been instantiated in the meantime *) + let ev1' = whd_evar i' t1 in + if isEvar i' ev1' then + solve_simple_eqn flags (conv_fun evar_conv_x flags) env i' + (position_problem true pbty,destEvar i' ev1',term2) + else + evar_eqappr_x flags env evd pbty + ((ev1', sk1), csts1) ((term2, sk2), csts2) + | Some (r,[]), Success i' -> + (* We have sk1'[] = sk2[] for some sk1' s.t. sk1[]=sk1'[r[]] *) + (* we now unify r[?ev1] and ?ev2 *) + let ev2' = whd_evar i' t2 in + if isEvar i' ev2' then + solve_simple_eqn flags (conv_fun evar_conv_x flags) env i' + (position_problem false pbty,destEvar i' ev2',Stack.zip i' (term1,r)) + else + evar_eqappr_x flags env evd pbty + ((ev2', sk1), csts1) ((term2, sk2), csts2) + | Some ([],r), Success i' -> + (* Symmetrically *) + (* We have sk1[] = sk2'[] for some sk2' s.t. sk2[]=sk2'[r[]] *) + (* we now unify ?ev1 and r[?ev2] *) + let ev1' = whd_evar i' t1 in + if isEvar i' ev1' then + solve_simple_eqn flags (conv_fun evar_conv_x flags) env i' + (position_problem true pbty,destEvar i' ev1',Stack.zip i' (term2,r)) + else evar_eqappr_x flags env evd pbty + ((ev1', sk1), csts1) ((term2, sk2), csts2) + | None, (UnifFailure _ as x) -> + (* sk1 and sk2 have no common outer part *) + if Stack.not_purely_applicative sk2 then + (* Ad hoc compatibility with 8.4 which treated non-app as rigid *) + flex_rigid true (destEvar evd t1) appr1 appr2 + else + if Stack.not_purely_applicative sk1 then + (* Ad hoc compatibility with 8.4 which treated non-app as rigid *) + flex_rigid false (destEvar evd t2) appr2 appr1 + else + (* We could instead try Miller unification, then + postpone to see if other equations help, as in: + [Check fun a b : unit => (eqᵣefl : _ a = _ a b)] *) + x + | Some _, Success _ -> + (* sk1 and sk2 have a common outer part *) + if Stack.not_purely_applicative sk2 then + (* Ad hoc compatibility with 8.4 which treated non-app as rigid *) + flex_rigid true (destEvar evd t1) appr1 appr2 + else + if Stack.not_purely_applicative sk1 then + (* Ad hoc compatibility with 8.4 which treated non-app as rigid *) + flex_rigid false (destEvar evd t2) appr2 appr1 + else + (* We could instead try Miller unification, then + postpone to see if other equations help, as in: + [Check fun a b c : unit => (eqᵣefl : _ a b = _ c a b)] *) + UnifFailure (i,NotSameArgSize) + | _, _ -> anomaly (Pp.str "Unexpected result from ise_stack2.") in let app_empty = match sk1, sk2 with [], [] -> true | _ -> false in (* Evar must be undefined since we have flushed evars *) let () = if !debug_unification then let open Pp in Feedback.msg_notice (v 0 (pr_state env evd appr1 ++ cut () ++ pr_state env evd appr2 ++ cut ())) in - match (flex_kind_of_term (fst ts) env evd term1 sk1, - flex_kind_of_term (fst ts) env evd term2 sk2) with + match (flex_kind_of_term flags env evd term1 sk1, + flex_kind_of_term flags env evd term2 sk2) with | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) -> (* sk1[?ev1] =? sk2[?ev2] *) - let f1 i = - (* Try first-order unification *) - match ise_stack2 false env i (evar_conv_x ts) sk1 sk2 with - | None, Success i' -> - (* We do have sk1[] = sk2[]: we now unify ?ev1 and ?ev2 *) - (* Note that ?ev1 and ?ev2, may have been instantiated in the meantime *) - let ev1' = whd_evar i' (mkEvar ev1) in - if isEvar i' ev1' then - solve_simple_eqn (evar_conv_x ts) env i' - (position_problem true pbty,destEvar i' ev1', term2) - else - evar_eqappr_x ts env evd pbty - ((ev1', sk1), csts1) ((term2, sk2), csts2) - | Some (r,[]), Success i' -> - (* We have sk1'[] = sk2[] for some sk1' s.t. sk1[]=sk1'[r[]] *) - (* we now unify r[?ev1] and ?ev2 *) - let ev2' = whd_evar i' (mkEvar ev2) in - if isEvar i' ev2' then - solve_simple_eqn (evar_conv_x ts) env i' - (position_problem false pbty,destEvar i' ev2',Stack.zip evd (term1,r)) - else - evar_eqappr_x ts env evd pbty - ((ev2', sk1), csts1) ((term2, sk2), csts2) - | Some ([],r), Success i' -> - (* Symmetrically *) - (* We have sk1[] = sk2'[] for some sk2' s.t. sk2[]=sk2'[r[]] *) - (* we now unify ?ev1 and r[?ev2] *) - let ev1' = whd_evar i' (mkEvar ev1) in - if isEvar i' ev1' then - solve_simple_eqn (evar_conv_x ts) env i' - (position_problem true pbty,destEvar i' ev1',Stack.zip evd (term2,r)) - else evar_eqappr_x ts env evd pbty - ((ev1', sk1), csts1) ((term2, sk2), csts2) - | None, (UnifFailure _ as x) -> - (* sk1 and sk2 have no common outer part *) - if Stack.not_purely_applicative sk2 then - (* Ad hoc compatibility with 8.4 which treated non-app as rigid *) - flex_rigid true ev1 appr1 appr2 - else - if Stack.not_purely_applicative sk1 then - (* Ad hoc compatibility with 8.4 which treated non-app as rigid *) - flex_rigid false ev2 appr2 appr1 - else - (* We could instead try Miller unification, then - postpone to see if other equations help, as in: - [Check fun a b : unit => (eqᵣefl : _ a = _ a b)] *) - x - | Some _, Success _ -> - (* sk1 and sk2 have a common outer part *) - if Stack.not_purely_applicative sk2 then - (* Ad hoc compatibility with 8.4 which treated non-app as rigid *) - flex_rigid true ev1 appr1 appr2 - else - if Stack.not_purely_applicative sk1 then - (* Ad hoc compatibility with 8.4 which treated non-app as rigid *) - flex_rigid false ev2 appr2 appr1 - else - (* We could instead try Miller unification, then - postpone to see if other equations help, as in: - [Check fun a b c : unit => (eqᵣefl : _ a b = _ c a b)] *) - UnifFailure (i,NotSameArgSize) - | _, _ -> anomaly (Pp.str "Unexpected result from ise_stack2.") - + let f1 i = first_order env i term1 term2 sk1 sk2 and f2 i = if Evar.equal sp1 sp2 then - match ise_stack2 false env i (evar_conv_x ts) sk1 sk2 with + match ise_stack2 false env i (evar_conv_x flags) sk1 sk2 with |None, Success i' -> - Success (solve_refl (fun env i pbty a1 a2 -> - is_success (evar_conv_x ts env i pbty a1 a2)) + Success (solve_refl flags (fun p env i pbty a1 a2 -> + let flags = if p then default_flags env else flags in + is_success (evar_conv_x flags env i pbty a1 a2)) env i' (position_problem true pbty) sp1 al1 al2) |_, (UnifFailure _ as x) -> x |Some _, _ -> UnifFailure (i,NotSameArgSize) else UnifFailure (i,NotSameHead) - in - ise_try evd [f1; f2] + and f3 i = miller true (sp1,al1) appr1 appr2 i + and f4 i = miller false (sp2,al2) appr2 appr1 i + and f5 i = consume true appr1 appr2 i in + ise_try evd [f1; f2; f3; f4; f5] | Flexible ev1, MaybeFlexible v2 -> flex_maybeflex true ev1 (appr1,csts1) (appr2,csts2) v2 @@ -689,31 +735,31 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let f1 i = (* FO *) ise_and i [(fun i -> ise_try i - [(fun i -> evar_conv_x ts env i CUMUL t1 t2); - (fun i -> evar_conv_x ts env i CUMUL t2 t1)]); - (fun i -> evar_conv_x ts env i CONV b1 b2); + [(fun i -> evar_conv_x flags env i CUMUL t1 t2); + (fun i -> evar_conv_x flags env i CUMUL t2 t1)]); + (fun i -> evar_conv_x flags env i CONV b1 b2); (fun i -> let b = nf_evar i b1 in let t = nf_evar i t1 in let na = Nameops.Name.pick na1 na2 in - evar_conv_x ts (push_rel (RelDecl.LocalDef (na,b,t)) env) i pbty c'1 c'2); - (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)] + evar_conv_x flags (push_rel (RelDecl.LocalDef (na,b,t)) env) i pbty c'1 c'2); + (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk1 sk2)] and f2 i = - let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (v1,sk1) - and out2 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts2 (v2,sk2) - in evar_eqappr_x ts env i pbty out1 out2 + let out1 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i csts1 (v1,sk1) + and out2 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i csts2 (v2,sk2) + in evar_eqappr_x flags env i pbty out1 out2 in ise_try evd [f1; f2] | Proj (p, c), Proj (p', c') when Projection.repr_equal p p' -> let f1 i = ise_and i - [(fun i -> evar_conv_x ts env i CONV c c'); - (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)] + [(fun i -> evar_conv_x flags env i CONV c c'); + (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk1 sk2)] and f2 i = - let out1 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts1 (v1,sk1) - and out2 = whd_betaiota_deltazeta_for_iota_state (fst ts) env i csts2 (v2,sk2) - in evar_eqappr_x ts env i pbty out1 out2 + let out1 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i csts1 (v1,sk1) + and out2 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i csts2 (v2,sk2) + in evar_eqappr_x flags env i pbty out1 out2 in ise_try evd [f1; f2] @@ -725,7 +771,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty in (match res with | Some (f1,args1) -> - evar_eqappr_x ts env evd pbty ((f1,Stack.append_app args1 sk1),csts1) + evar_eqappr_x flags env evd pbty ((f1,Stack.append_app args1 sk1),csts1) (appr2,csts2) | None -> UnifFailure (evd,NotSameHead)) @@ -736,7 +782,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty in (match res with | Some (f2,args2) -> - evar_eqappr_x ts env evd pbty (appr1,csts1) ((f2,Stack.append_app args2 sk2),csts2) + evar_eqappr_x flags env evd pbty (appr1,csts1) ((f2,Stack.append_app args2 sk2),csts2) | None -> UnifFailure (evd,NotSameHead)) | _, _ -> @@ -753,13 +799,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty try Success (Evd.add_universe_constraints i univs) with UniversesDiffer -> UnifFailure (i,NotSameHead) | Univ.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p)); - (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)] + (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk1 sk2)] | None -> UnifFailure (i,NotSameHead) and f2 i = (try - if not (snd ts) then raise Not_found - else conv_record ts env i + if not flags.with_cs then raise Not_found + else conv_record flags env i (try check_conv_record env i appr1 appr2 with Not_found -> check_conv_record env i appr2 appr1) with Not_found -> UnifFailure (i,NoCanonicalStructure)) @@ -777,7 +823,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | Lambda _ -> assert (match args with [] -> true | _ -> false); true | LetIn (_,b,_,c) -> is_unnamed (fst (whd_betaiota_deltazeta_for_iota_state - (fst ts) env i Cst_stack.empty (subst1 b c, args))) + flags.open_ts env i Cst_stack.empty (subst1 b c, args))) | Fix _ -> true (* Partially applied fix can be the result of a whd call *) | Proj (p, _) -> Projection.unfolded p || Stack.not_purely_applicative args | Case _ | App _| Cast _ -> assert false in @@ -785,20 +831,20 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let applicative_stack = fst (Stack.strip_app sk2) in is_unnamed (fst (whd_betaiota_deltazeta_for_iota_state - (fst ts) env i Cst_stack.empty (v2, applicative_stack))) in + flags.open_ts env i Cst_stack.empty (v2, applicative_stack))) in let rhs_is_already_stuck = rhs_is_already_stuck || rhs_is_stuck_and_unnamed () in if (EConstr.isLambda i term1 || rhs_is_already_stuck) && (not (Stack.not_purely_applicative sk1)) then - evar_eqappr_x ~rhs_is_already_stuck ts env i pbty + evar_eqappr_x ~rhs_is_already_stuck flags env i pbty (whd_betaiota_deltazeta_for_iota_state - (fst ts) env i (Cst_stack.add_cst term1 csts1) (v1,sk1)) + flags.open_ts env i (Cst_stack.add_cst term1 csts1) (v1,sk1)) (appr2,csts2) else - evar_eqappr_x ts env i pbty (appr1,csts1) + evar_eqappr_x flags env i pbty (appr1,csts1) (whd_betaiota_deltazeta_for_iota_state - (fst ts) env i (Cst_stack.add_cst term2 csts2) (v2,sk2)) + flags.open_ts env i (Cst_stack.add_cst term2 csts2) (v2,sk2)) in ise_try evd [f1; f2; f3] end @@ -806,13 +852,14 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | Rigid, Rigid when EConstr.isLambda evd term1 && EConstr.isLambda evd term2 -> let (na1,c1,c'1) = EConstr.destLambda evd term1 in let (na2,c2,c'2) = EConstr.destLambda evd term2 in - assert app_empty; ise_and evd - [(fun i -> evar_conv_x ts env i CONV c1 c2); + [(fun i -> evar_conv_x flags env i CONV c1 c2); (fun i -> let c = nf_evar i c1 in let na = Nameops.Name.pick na1 na2 in - evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i CONV c'1 c'2)] + evar_conv_x flags (push_rel (RelDecl.LocalAssum (na,c)) env) i CONV c'1 c'2); + (** When in modulo_betaiota = false case, lambda's are not reduced *) + (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk1 sk2)] | Flexible ev1, Rigid -> flex_rigid true ev1 appr1 appr2 | Rigid, Flexible ev2 -> flex_rigid false ev2 appr2 appr1 @@ -820,13 +867,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | MaybeFlexible v1, Rigid -> let f3 i = (try - if not (snd ts) then raise Not_found - else conv_record ts env i (check_conv_record env i appr1 appr2) + if not flags.with_cs then raise Not_found + else conv_record flags env i (check_conv_record env i appr1 appr2) with Not_found -> UnifFailure (i,NoCanonicalStructure)) and f4 i = - evar_eqappr_x ts env i pbty + evar_eqappr_x flags env i pbty (whd_betaiota_deltazeta_for_iota_state - (fst ts) env i (Cst_stack.add_cst term1 csts1) (v1,sk1)) + flags.open_ts env i (Cst_stack.add_cst term1 csts1) (v1,sk1)) (appr2,csts2) in ise_try evd [f3; f4] @@ -834,13 +881,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | Rigid, MaybeFlexible v2 -> let f3 i = (try - if not (snd ts) then raise Not_found - else conv_record ts env i (check_conv_record env i appr2 appr1) + if not flags.with_cs then raise Not_found + else conv_record flags env i (check_conv_record env i appr2 appr1) with Not_found -> UnifFailure (i,NoCanonicalStructure)) and f4 i = - evar_eqappr_x ts env i pbty (appr1,csts1) + evar_eqappr_x flags env i pbty (appr1,csts1) (whd_betaiota_deltazeta_for_iota_state - (fst ts) env i (Cst_stack.add_cst term2 csts2) (v2,sk2)) + flags.open_ts env i (Cst_stack.add_cst term2 csts2) (v2,sk2)) in ise_try evd [f3; f4] @@ -869,20 +916,20 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | Prod (n1,c1,c'1), Prod (n2,c2,c'2) when app_empty -> ise_and evd - [(fun i -> evar_conv_x ts env i CONV c1 c2); + [(fun i -> evar_conv_x flags env i CONV c1 c2); (fun i -> let c = nf_evar i c1 in let na = Nameops.Name.pick n1 n2 in - evar_conv_x ts (push_rel (RelDecl.LocalAssum (na,c)) env) i pbty c'1 c'2)] + evar_conv_x flags (push_rel (RelDecl.LocalAssum (na,c)) env) i pbty c'1 c'2)] | Rel x1, Rel x2 -> if Int.equal x1 x2 then - exact_ise_stack2 env evd (evar_conv_x ts) sk1 sk2 + exact_ise_stack2 env evd (evar_conv_x flags) sk1 sk2 else UnifFailure (evd,NotSameHead) | Var var1, Var var2 -> if Id.equal var1 var2 then - exact_ise_stack2 env evd (evar_conv_x ts) sk1 sk2 + exact_ise_stack2 env evd (evar_conv_x flags) sk1 sk2 else UnifFailure (evd,NotSameHead) | Const _, Const _ @@ -891,49 +938,63 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty | Int _, Int _ -> rigids env evd sk1 term1 sk2 term2 + | Evar (sp1,al1), Evar (sp2,al2) -> (** Frozen evars *) + if Evar.equal sp1 sp2 then + match ise_stack2 false env evd (evar_conv_x flags) sk1 sk2 with + |None, Success i' -> + (** FIXME: solve_refl can restrict the evar, do we want to allow that? *) + Success (solve_refl flags (fun p env i pbty a1 a2 -> + let flags = if p then default_flags env else flags in + is_success (evar_conv_x flags env i pbty a1 a2)) + env i' (position_problem true pbty) sp1 al1 al2) + |_, (UnifFailure _ as x) -> x + |Some _, _ -> UnifFailure (evd,NotSameArgSize) + else UnifFailure (evd,NotSameHead) + | Construct u, _ -> - eta_constructor ts env evd sk1 u sk2 term2 + eta_constructor flags env evd sk1 u sk2 term2 | _, Construct u -> - eta_constructor ts env evd sk2 u sk1 term1 + eta_constructor flags env evd sk2 u sk1 term1 | Fix ((li1, i1),(_,tys1,bds1 as recdef1)), Fix ((li2, i2),(_,tys2,bds2)) -> (* Partially applied fixs *) if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then ise_and evd [ - (fun i -> ise_array2 i (fun i' -> evar_conv_x ts env i' CONV) tys1 tys2); - (fun i -> ise_array2 i (fun i' -> evar_conv_x ts (push_rec_types recdef1 env) i' CONV) bds1 bds2); - (fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)] + (fun i -> ise_array2 i (fun i' -> evar_conv_x flags env i' CONV) tys1 tys2); + (fun i -> ise_array2 i (fun i' -> evar_conv_x flags (push_rec_types recdef1 env) i' CONV) bds1 bds2); + (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk1 sk2)] else UnifFailure (evd, NotSameHead) | CoFix (i1,(_,tys1,bds1 as recdef1)), CoFix (i2,(_,tys2,bds2)) -> if Int.equal i1 i2 then ise_and evd [(fun i -> ise_array2 i - (fun i -> evar_conv_x ts env i CONV) tys1 tys2); + (fun i -> evar_conv_x flags env i CONV) tys1 tys2); (fun i -> ise_array2 i - (fun i -> evar_conv_x ts (push_rec_types recdef1 env) i CONV) + (fun i -> evar_conv_x flags (push_rec_types recdef1 env) i CONV) bds1 bds2); (fun i -> exact_ise_stack2 env i - (evar_conv_x ts) sk1 sk2)] + (evar_conv_x flags) sk1 sk2)] else UnifFailure (evd,NotSameHead) | (Meta _, _) | (_, Meta _) -> - begin match ise_stack2 true env evd (evar_conv_x ts) sk1 sk2 with + begin match ise_stack2 true env evd (evar_conv_x flags) sk1 sk2 with |_, (UnifFailure _ as x) -> x - |None, Success i' -> evar_conv_x ts env i' CONV term1 term2 - |Some (sk1',sk2'), Success i' -> evar_conv_x ts env i' CONV (Stack.zip i' (term1,sk1')) (Stack.zip i' (term2,sk2')) + |None, Success i' -> evar_conv_x flags env i' CONV term1 term2 + |Some (sk1',sk2'), Success i' -> evar_conv_x flags env i' CONV (Stack.zip i' (term1,sk1')) (Stack.zip i' (term2,sk2')) end - | (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _ | Int _), _ -> + | (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _ | Int _ | Evar _ | Lambda _), _ -> UnifFailure (evd,NotSameHead) - - | (App _ | Cast _ | Case _ | Proj _), _ -> assert false - | (LetIn _| Evar _), _ -> assert false - | (Lambda _), _ -> assert false - + | _, (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _ | Int _ | Evar _ | Lambda _) -> + UnifFailure (evd,NotSameHead) + | Case _, _ -> UnifFailure (evd,NotSameHead) + | Proj _, _ -> UnifFailure (evd,NotSameHead) + | (App _ | Cast _), _ -> assert false + | LetIn _, _ -> assert false end -and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2),c1,(n,t2)) = +and conv_record flags env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2),c1,(n,t2)) = (* Tries to unify the states (proji params1 c1 | sk1) = (proji params2 (c (?xs:bs)) | sk2) @@ -964,7 +1025,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2) (fun (i,ks,m,test) b -> if match n with Some n -> Int.equal m n | None -> false then let ty = Retyping.get_type_of env i t2 in - let test i = evar_conv_x trs env i CUMUL ty (substl ks b) in + let test i = evar_conv_x flags env i CUMUL ty (substl ks b) in (i,t2::ks, m-1, test) else let dloc = Loc.tag Evar_kinds.InternalHole in @@ -976,20 +1037,20 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2) ise_and evd' [(fun i -> exact_ise_stack2 env i - (fun env' i' cpb x1 x -> evar_conv_x trs env' i' cpb x1 (substl ks x)) + (fun env' i' cpb x1 x -> evar_conv_x flags env' i' cpb x1 (substl ks x)) params1 params); (fun i -> exact_ise_stack2 env i - (fun env' i' cpb u1 u -> evar_conv_x trs env' i' cpb u1 (substl ks u)) + (fun env' i' cpb u1 u -> evar_conv_x flags env' i' cpb u1 (substl ks u)) us2 us); - (fun i -> evar_conv_x trs env i CONV c1 app); - (fun i -> exact_ise_stack2 env i (evar_conv_x trs) sk1 sk2); + (fun i -> evar_conv_x flags env i CONV c1 app); + (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk1 sk2); test; - (fun i -> evar_conv_x trs env i CONV h2 + (fun i -> evar_conv_x flags env i CONV h2 (fst (decompose_app_vect i (substl ks h))))] else UnifFailure(evd,(*dummy*)NotSameHead) -and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 = +and eta_constructor flags env evd sk1 ((ind, i), u) sk2 term2 = let open Declarations in let mib = lookup_mind (fst ind) env in match get_projections env ind with @@ -1001,15 +1062,15 @@ and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 = let term = Stack.zip evd (term2,sk2) in List.map (fun p -> EConstr.mkProj (Projection.make p false, term)) (Array.to_list projs) in - exact_ise_stack2 env evd (evar_conv_x (fst ts, false)) l1' + exact_ise_stack2 env evd (evar_conv_x { flags with with_cs = false}) l1' (Stack.append_app_list l2' Stack.empty) - with + with | Invalid_argument _ -> (* Stack.tail: partially applied constructor *) UnifFailure(evd,NotSameHead)) | _ -> UnifFailure (evd,NotSameHead) -let evar_conv_x ts = evar_conv_x (ts, true) +let evar_conv_x flags = evar_conv_x flags (* Profiling *) let evar_conv_x = @@ -1020,25 +1081,26 @@ let evar_conv_x = let evar_conv_hook_get, evar_conv_hook_set = Hook.make ~default:evar_conv_x () -let evar_conv_x ts = Hook.get evar_conv_hook_get ts +let evar_conv_x flags = Hook.get evar_conv_hook_get flags let set_evar_conv f = Hook.set evar_conv_hook_set f (* We assume here |l1| <= |l2| *) -let first_order_unification ts env evd (ev1,l1) (term2,l2) = +let first_order_unification flags env evd (ev1,l1) (term2,l2) = let (deb2,rest2) = Array.chop (Array.length l2-Array.length l1) l2 in ise_and evd (* First compare extra args for better failure message *) - [(fun i -> ise_array2 i (fun i -> evar_conv_x ts env i CONV) rest2 l1); + [(fun i -> ise_array2 i (fun i -> evar_conv_x flags env i CONV) rest2 l1); (fun i -> (* Then instantiate evar unless already done by unifying args *) let t2 = mkApp(term2,deb2) in if is_defined i (fst ev1) then - evar_conv_x ts env i CONV t2 (mkEvar ev1) + evar_conv_x flags env i CONV t2 (mkEvar ev1) else - solve_simple_eqn ~choose:true (evar_conv_x ts) env i (None,ev1,t2))] + solve_simple_eqn ~choose:true ~imitate_defs:false + flags (conv_fun evar_conv_x flags) env i (None,ev1,t2))] let choose_less_dependent_instance evk evd term args = let evi = Evd.find_undefined evd evk in @@ -1202,31 +1264,79 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = in force_instantiation evd !evsref | [] -> - let evd = - try Evarsolve.check_evar_instance evd evk rhs - (evar_conv_x TransparentState.full) - with IllTypedInstance _ -> raise (TypingFailed evd) - in - Evd.define evk rhs evd + if Evd.is_defined evd evk then + (** Can happen due to dependencies: instantiating evars in the arguments of evk might + instantiate evk itself. *) + (if !debug_ho_unification then + begin + let evi = Evd.find evd evk in + let evenv = evar_env evi in + let body = match evar_body evi with Evar_empty -> assert false | Evar_defined c -> c in + Feedback.msg_debug Pp.(str"evar was defined already as: " ++ prc evenv body) + end; + evd) + else + let evd = + try + let evi = Evd.find_undefined evd evk in + let evenv = evar_env evi in + let evdref = ref evd in + let rhs' = nf_evar !evdref rhs' in + if !debug_ho_unification then + Feedback.msg_debug Pp.(str"abstracted type before second solve_evars: " ++ + prc evenv rhs'); + (** solve_evars is not commuting with nf_evar, because restricting + an evar might provide a more specific type. *) + let evd, _ = !solve_evars evenv evd rhs' in + evdref := evd; + if !debug_ho_unification then + Feedback.msg_debug Pp.(str"abstracted type: " ++ prc evenv (nf_evar !evdref rhs')); + Evarsolve.check_evar_instance !evdref evk rhs' + (conv_fun evar_conv_x (default_flags_of TransparentState.full)) + with IllTypedInstance _ -> raise (TypingFailed evd) + in Evd.define evk rhs' evd in - abstract_free_holes evd subst, true + let evd = abstract_free_holes evd subst in + evd, true with TypingFailed evd -> evd, false -let second_order_matching_with_args ts env evd pbty ev l t = -(* - let evd,ev = evar_absorb_arguments env evd ev l in - let argoccs = Array.map_to_list (fun _ -> None) (snd ev) in - let evd, b = second_order_matching ts env evd ev argoccs t in - if b then Success evd - else UnifFailure (evd, ConversionFailed (env,mkApp(mkEvar ev,l),t)) - if b then Success evd else - *) - let pb = (pbty,env,mkApp(mkEvar ev,l),t) in - UnifFailure (evd, CannotSolveConstraint (pb,ProblemBeyondCapabilities)) - -let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = - let t1 = apprec_nohdbeta ts env evd (whd_head_evar evd t1) in - let t2 = apprec_nohdbeta ts env evd (whd_head_evar evd t2) in +let default_evar_selection flags evd (ev,args) = + let evi = Evd.find_undefined evd ev in + let rec aux args abs = + match args, abs with + | _ :: args, a :: abs -> + let spec = if not flags.allow_K_at_toplevel then + AtOccurrences (if a then Locus.AtLeastOneOccurrence else Locus.AllOccurrences) + else Unspecified a in + spec :: aux args abs + | l, [] -> List.map (fun _ -> default_occurrence_selection) l + | [], _ :: _ -> assert false + in aux (Array.to_list args) evi.evar_abstract_arguments + +let second_order_matching_with_args flags env evd with_ho pbty ev l t = + if with_ho then + let evd,ev = evar_absorb_arguments env evd ev (Array.to_list l) in + let argoccs = default_evar_selection flags evd ev in + let test = default_occurrence_test ~frozen_evars:flags.frozen_evars flags.subterm_ts in + let evd, b = + try second_order_matching flags env evd ev (test,argoccs) t + with PretypeError (_, _, NoOccurrenceFound _) -> evd, false + in + if b then Success evd + else + UnifFailure (evd, ConversionFailed (env,mkApp(mkEvar ev,l),t)) + else + let pb = (pbty,env,mkApp(mkEvar ev,l),t) in + UnifFailure (evd, CannotSolveConstraint (pb,ProblemBeyondCapabilities)) + +let is_beyond_capabilities = function + | CannotSolveConstraint (pb,ProblemBeyondCapabilities) -> true + | _ -> false + +(* TODO frozen *) +let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 = + let t1 = apprec_nohdbeta flags env evd (whd_head_evar evd t1) in + let t2 = apprec_nohdbeta flags env evd (whd_head_evar evd t2) in let (term1,l1 as appr1) = try destApp evd t1 with DestKO -> (t1, [||]) in let (term2,l2 as appr2) = try destApp evd t2 with DestKO -> (t2, [||]) in let () = if !debug_unification then @@ -1257,36 +1367,38 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = let reason = ProblemBeyondCapabilities in UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason))) | Evar (evk1,args1), Evar (evk2,args2) when Evar.equal evk1 evk2 -> - let f env evd pbty x y = is_fconv ~reds:ts pbty env evd x y in - Success (solve_refl ~can_drop:true f env evd + let f ontype env evd pbty x y = + let reds = if ontype then full_transparent_state else flags.open_ts in + is_fconv ~reds pbty env evd x y in + Success (solve_refl ~can_drop:true flags f env evd (position_problem true pbty) evk1 args1 args2) | Evar ev1, Evar ev2 when app_empty -> Success (solve_evar_evar ~force:true - (evar_define (evar_conv_x ts) ~choose:true) (evar_conv_x ts) env evd + flags (evar_define flags (conv_fun evar_conv_x flags) ~choose:true) (conv_fun evar_conv_x flags) env evd (position_problem true pbty) ev1 ev2) | Evar ev1,_ when Array.length l1 <= Array.length l2 -> (* On "?n t1 .. tn = u u1 .. u(n+p)", try first-order unification *) (* and otherwise second-order matching *) ise_try evd - [(fun evd -> first_order_unification ts env evd (ev1,l1) appr2); + [(fun evd -> first_order_unification flags env evd (ev1,l1) appr2); (fun evd -> - second_order_matching_with_args ts env evd pbty ev1 l1 t2)] + second_order_matching_with_args flags env evd with_ho pbty ev1 l1 t2)] | _,Evar ev2 when Array.length l2 <= Array.length l1 -> (* On "u u1 .. u(n+p) = ?n t1 .. tn", try first-order unification *) (* and otherwise second-order matching *) ise_try evd - [(fun evd -> first_order_unification ts env evd (ev2,l2) appr1); + [(fun evd -> first_order_unification flags env evd (ev2,l2) appr1); (fun evd -> - second_order_matching_with_args ts env evd pbty ev2 l2 t1)] + second_order_matching_with_args flags env evd with_ho pbty ev2 l2 t1)] | Evar ev1,_ -> (* Try second-order pattern-matching *) - second_order_matching_with_args ts env evd pbty ev1 l1 t2 + second_order_matching_with_args flags env evd with_ho pbty ev1 l1 t2 | _,Evar ev2 -> (* Try second-order pattern-matching *) - second_order_matching_with_args ts env evd pbty ev2 l2 t1 + second_order_matching_with_args flags env evd with_ho pbty ev2 l2 t1 | _ -> (* Some head evar have been instantiated, or unknown kind of problem *) - evar_conv_x ts env evd pbty t1 t2 + evar_conv_x flags env evd pbty t1 t2 let error_cannot_unify env evd pb ?reason t1 t2 = Pretype_errors.error_cannot_unify @@ -1315,7 +1427,7 @@ let max_undefined_with_candidates evd = with MaxUndefined ans -> Some ans -let rec solve_unconstrained_evars_with_candidates ts evd = +let rec solve_unconstrained_evars_with_candidates flags evd = (* max_undefined is supposed to return the most recent, hence possibly most dependent evar *) match max_undefined_with_candidates evd with @@ -1326,11 +1438,11 @@ let rec solve_unconstrained_evars_with_candidates ts evd = | a::l -> (* In case of variables, most recent ones come first *) try - let conv_algo = evar_conv_x ts in + let conv_algo = conv_fun evar_conv_x flags in let evd = check_evar_instance evd evk a conv_algo in let evd = Evd.define evk a evd in match reconsider_unif_constraints conv_algo evd with - | Success evd -> solve_unconstrained_evars_with_candidates ts evd + | Success evd -> solve_unconstrained_evars_with_candidates flags evd | UnifFailure _ -> aux l with | IllTypedInstance _ -> aux l @@ -1338,7 +1450,7 @@ let rec solve_unconstrained_evars_with_candidates ts evd = (* Expected invariant: most dependent solutions come first *) (* so as to favor progress when used with the refine tactics *) let evd = aux l in - solve_unconstrained_evars_with_candidates ts evd + solve_unconstrained_evars_with_candidates flags evd let solve_unconstrained_impossible_cases env evd = Evd.fold_undefined (fun evk ev_info evd' -> @@ -1347,18 +1459,18 @@ let solve_unconstrained_impossible_cases env evd = let j, ctx = coq_unit_judge env in let evd' = Evd.merge_context_set Evd.univ_flexible_alg ?loc evd' ctx in let ty = j_type j in - let conv_algo = evar_conv_x TransparentState.full in + let conv_algo = conv_fun evar_conv_x (default_flags env) in let evd' = check_evar_instance evd' evk ty conv_algo in Evd.define evk ty evd' | _ -> evd') evd evd let solve_unif_constraints_with_heuristics env - ?(ts=Conv_oracle.get_transp_state (Environ.oracle env)) evd = - let evd = solve_unconstrained_evars_with_candidates ts evd in + ?(flags=default_flags env) ?(with_ho=false) evd = + let evd = solve_unconstrained_evars_with_candidates flags evd in let rec aux evd pbs progress stuck = match pbs with | (pbty,env,t1,t2 as pb) :: pbs -> - (match apply_conversion_problem_heuristic ts env evd pbty t1 t2 with + (match apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 with | Success evd' -> let (evd', rest) = extract_all_conv_pbs evd' in begin match rest with @@ -1386,16 +1498,15 @@ let solve_unif_constraints_with_heuristics env exception UnableToUnify of evar_map * unification_error -let default_transparent_state env = TransparentState.full -(* Conv_oracle.get_transp_state (Environ.oracle env) *) - let the_conv_x env ?(ts=default_transparent_state env) t1 t2 evd = - match evar_conv_x ts env evd CONV t1 t2 with + let flags = default_flags_of ts in + match evar_conv_x flags env evd CONV t1 t2 with | Success evd' -> evd' | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e)) let the_conv_x_leq env ?(ts=default_transparent_state env) t1 t2 evd = - match evar_conv_x ts env evd CUMUL t1 t2 with + let flags = default_flags_of ts in + match evar_conv_x flags env evd CUMUL t1 t2 with | Success evd' -> evd' | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e)) @@ -1404,7 +1515,27 @@ let make_opt = function | UnifFailure _ -> None let conv env ?(ts=default_transparent_state env) evd t1 t2 = - make_opt(evar_conv_x ts env evd CONV t1 t2) + let flags = default_flags_of ts in + make_opt(evar_conv_x flags env evd CONV t1 t2) let cumul env ?(ts=default_transparent_state env) evd t1 t2 = - make_opt(evar_conv_x ts env evd CUMUL t1 t2) + let flags = default_flags_of ts in + make_opt(evar_conv_x flags env evd CUMUL t1 t2) + +let unify flags env evd t1 t2 = + match evar_conv_x flags env evd CONV t1 t2 with + | Success evd' -> evd' + | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e)) + +let unify_leq flags env evd t1 t2 = + match evar_conv_x flags env evd CUMUL t1 t2 with + | Success evd' -> evd' + | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e)) + +let unify_with_heuristics flags ~with_ho env evd cv_pb ty1 ty2 = + let res = evar_conv_x flags env evd cv_pb ty1 ty2 in + match res with + | Success evd -> + solve_unif_constraints_with_heuristics ~flags ~with_ho env evd + | UnifFailure (evd, reason) -> + raise (PretypeError (env, evd, CannotUnify (ty1, ty2, Some reason))) diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 4585fac252..efb827d866 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -16,6 +16,16 @@ open Locus (** {4 Unification for type inference. } *) +type unify_flags = Evarsolve.unify_flags + +(** The default subterm transparent state is no unfoldings *) +val default_flags_of : ?subterm_ts:transparent_state -> transparent_state -> unify_flags + +type unify_fun = unify_flags -> + env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result + +val conv_fun : unify_fun -> unify_flags -> Evarsolve.conv_fun + exception UnableToUnify of evar_map * Pretype_errors.unification_error (** {6 Main unification algorithm for type inference. } *) @@ -24,6 +34,14 @@ exception UnableToUnify of evar_map * Pretype_errors.unification_error val the_conv_x : env -> ?ts:TransparentState.t -> constr -> constr -> evar_map -> evar_map val the_conv_x_leq : env -> ?ts:TransparentState.t -> constr -> constr -> evar_map -> evar_map +(** Allows to pass arbitrary flags to the unifier *) +val unify : unify_flags -> env -> evar_map -> constr -> constr -> evar_map +val unify_leq : unify_flags -> env -> evar_map -> constr -> constr -> evar_map + +(** @raises a PretypeError if it cannot unify *) +val unify_with_heuristics : unify_flags -> with_ho:bool -> + env -> evar_map -> conv_pb -> constr -> constr -> evar_map + (** The same function resolving evars by side-effect and catching the exception *) val conv : env -> ?ts:TransparentState.t -> evar_map -> constr -> constr -> evar_map option @@ -34,7 +52,8 @@ val cumul : env -> ?ts:TransparentState.t -> evar_map -> constr -> constr -> eva (** Try heuristics to solve pending unification problems and to solve evars with candidates *) -val solve_unif_constraints_with_heuristics : env -> ?ts:TransparentState.t -> evar_map -> evar_map +val solve_unif_constraints_with_heuristics : + env -> ?flags:unify_flags -> ?with_ho:bool -> evar_map -> evar_map (** Check all pending unification problems are solved and raise an error otherwise *) @@ -61,9 +80,6 @@ val second_order_matching : TransparentState.t -> env -> evar_map -> val set_solve_evars : (env -> evar_map -> constr -> evar_map * constr) -> unit -type unify_fun = TransparentState.t -> - env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result - (** Override default [evar_conv_x] algorithm. *) val set_evar_conv : unify_fun -> unit @@ -72,7 +88,7 @@ val evar_conv_x : unify_fun (**/**) (* For debugging *) -val evar_eqappr_x : ?rhs_is_already_stuck:bool -> TransparentState.t * bool -> +val evar_eqappr_x : ?rhs_is_already_stuck:bool -> unify_flags -> env -> evar_map -> conv_pb -> state * Cst_stack.t -> state * Cst_stack.t -> Evarsolve.unification_result diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 4c4a236620..aad21ad932 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -24,6 +24,15 @@ open Reductionops open Evarutil open Pretype_errors +type unify_flags = { + modulo_betaiota: bool; + open_ts : transparent_state; + closed_ts : transparent_state; + subterm_ts : transparent_state; + frozen_evars : Evar.Set.t; + allow_K_at_toplevel : bool; + with_cs : bool } + let normalize_evar evd ev = match EConstr.kind evd (mkEvar ev) with | Evar (evk,args) -> (evk,args) @@ -141,8 +150,8 @@ type unification_result = let is_success = function Success _ -> true | UnifFailure _ -> false -let test_success conv_algo env evd c c' rhs = - is_success (conv_algo env evd c c' rhs) +let test_success conv_algo b env evd c c' rhs = + is_success (conv_algo b env evd c c' rhs) let add_conv_oriented_pb ?(tail=true) (pbty,env,t1,t2) evd = match pbty with @@ -165,7 +174,7 @@ let recheck_applications conv_algo env evdref t = if i < Array.length argsty then match EConstr.kind !evdref (whd_all env !evdref ty) with | Prod (na, dom, codom) -> - (match conv_algo env !evdref Reduction.CUMUL argsty.(i) dom with + (match conv_algo true env !evdref Reduction.CUMUL argsty.(i) dom with | Success evd -> evdref := evd; aux (succ i) (subst1 args.(i) codom) | UnifFailure (evd, reason) -> @@ -734,6 +743,19 @@ let restrict_upon_filter evd evk p args = let len = Array.length args in Filter.restrict_upon oldfullfilter len (fun i -> p (Array.unsafe_get args i)) +let check_evar_instance evd evk1 body conv_algo = + let evi = Evd.find evd evk1 in + let evenv = evar_env evi in + (* FIXME: The body might be ill-typed when this is called from w_merge *) + (* This happens in practice, cf MathClasses build failure on 2013-3-15 *) + let ty = + try Retyping.get_type_of ~lax:true evenv evd body + with Retyping.RetypeError _ -> user_err (Pp.(str "Ill-typed evar instance")) + in + match conv_algo true evenv evd Reduction.CUMUL ty evi.evar_concl with + | Success evd -> evd + | UnifFailure _ -> raise (IllTypedInstance (evenv,ty,evi.evar_concl)) + (***************) (* Unification *) @@ -869,12 +891,13 @@ let rec find_solution_type evarenv = function * pass [define] to [do_projection_effects] as a parameter. *) -let rec do_projection_effects define_fun env ty evd = function +let rec do_projection_effects conv_algo define_fun env ty evd = function | ProjectVar -> evd | ProjectEvar ((evk,argsv),evi,id,p) -> - let evd = Evd.define evk (mkVar id) evd in + let evd = check_evar_instance evd evk (mkVar id) conv_algo in + let evd = Evd.define evk (EConstr.mkVar id) evd in (* TODO: simplify constraints involving evk *) - let evd = do_projection_effects define_fun env ty evd p in + let evd = do_projection_effects conv_algo define_fun env ty evd p in let ty = whd_all env evd (Lazy.force ty) in if not (isSort evd ty) then (* Don't try to instantiate if a sort because if evar_concl is an @@ -1112,7 +1135,7 @@ let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs = let filter_compatible_candidates conv_algo env evd evi args rhs c = let c' = instantiate_evar_array evi c args in - match conv_algo env evd Reduction.CONV rhs c' with + match conv_algo false env evd Reduction.CONV rhs c' with | Success evd -> Some (c,evd) | UnifFailure _ -> None @@ -1225,19 +1248,6 @@ let project_evar_on_evar force g env evd aliases k2 pbty (evk1,argsv1 as ev1) (e else raise (CannotProject (evd,ev1')) -let check_evar_instance evd evk1 body conv_algo = - let evi = Evd.find evd evk1 in - let evenv = evar_env evi in - (* FIXME: The body might be ill-typed when this is called from w_merge *) - (* This happens in practice, cf MathClasses build failure on 2013-3-15 *) - let ty = - try Retyping.get_type_of ~lax:true evenv evd body - with Retyping.RetypeError _ -> user_err Pp.(str "Ill-typed evar instance") - in - match conv_algo evenv evd Reduction.CUMUL ty evi.evar_concl with - | Success evd -> evd - | UnifFailure _ -> raise (IllTypedInstance (evenv,ty, evi.evar_concl)) - let update_evar_info ev1 ev2 evd = (* We update the source of obligation evars during evar-evar unifications. *) let loc, evs1 = evar_source ev1 evd in @@ -1264,22 +1274,27 @@ let preferred_orientation evd evk1 evk2 = else if is_obligation_evar evd evk2 then false else true -let solve_evar_evar_aux force f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) = +(** Precondition evk1 is not frozen, evk2 might be. *) +let solve_evar_evar_aux force flags f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) = let aliases = make_alias_map env evd in + let frozen_ev2 = Evar.Set.mem evk2 flags.frozen_evars in if preferred_orientation evd evk1 evk2 then try solve_evar_evar_l2r force f g env evd aliases (opp_problem pbty) ev2 ev1 - with CannotProject (evd,ev2) -> + with CannotProject (evd,ev2) when not frozen_ev2 -> try solve_evar_evar_l2r force f g env evd aliases pbty ev1 ev2 with CannotProject (evd,ev1) -> add_conv_oriented_pb ~tail:true (pbty,env,mkEvar ev1,mkEvar ev2) evd else - try solve_evar_evar_l2r force f g env evd aliases pbty ev1 ev2 + try if not frozen_ev2 then + solve_evar_evar_l2r force f g env evd aliases pbty ev1 ev2 + else raise (CannotProject (evd,ev1)) with CannotProject (evd,ev1) -> try solve_evar_evar_l2r force f g env evd aliases (opp_problem pbty) ev2 ev1 with CannotProject (evd,ev2) -> add_conv_oriented_pb ~tail:true (pbty,env,mkEvar ev1,mkEvar ev2) evd -let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) = +(** Precondition: evk1 is not frozen *) +let solve_evar_evar ?(force=false) flags f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) = let pbty = if force then None else pbty in let evi = Evd.find evd evk1 in let downcast evk t evd = downcast evk t evd in @@ -1314,20 +1329,22 @@ let solve_evar_evar ?(force=false) f g env evd pbty (evk1,args1 as ev1) (evk2,ar downcast evk2 t2 (downcast evk1 t1 evd) with Reduction.NotArity -> evd in - solve_evar_evar_aux force f g env evd pbty ev1 ev2 + solve_evar_evar_aux force flags f g env evd pbty ev1 ev2 + +type types_or_terms = bool type conv_fun = - env -> evar_map -> conv_pb -> EConstr.constr -> EConstr.constr -> unification_result + types_or_terms -> env -> evar_map -> conv_pb -> EConstr.constr -> EConstr.constr -> unification_result type conv_fun_bool = - env -> evar_map -> conv_pb -> EConstr.constr -> EConstr.constr -> bool + types_or_terms -> env -> evar_map -> conv_pb -> EConstr.constr -> EConstr.constr -> bool (* Solve pbs ?e[t1..tn] = ?e[u1..un] which arise often in fixpoint * definitions. We try to unify the ti with the ui pairwise. The pairs * that don't unify are discarded (i.e. ?e is redefined so that it does not * depend on these args). *) -let solve_refl ?(can_drop=false) conv_algo env evd pbty evk argsv1 argsv2 = +let solve_refl ?(can_drop=false) flags conv_algo env evd pbty evk argsv1 argsv2 = let evdref = ref evd in let eq_constr c1 c2 = match EConstr.eq_constr_universes env !evdref c1 c2 with | None -> false @@ -1340,7 +1357,7 @@ let solve_refl ?(can_drop=false) conv_algo env evd pbty evk argsv1 argsv2 = let args = Array.map2 (fun a1 a2 -> (a1, a2)) argsv1 argsv2 in let untypedfilter = restrict_upon_filter evd evk - (fun (a1,a2) -> conv_algo env evd Reduction.CONV a1 a2) args in + (fun (a1,a2) -> conv_algo false env evd Reduction.CONV a1 a2) args in let candidates = filter_candidates evd evk untypedfilter NoUpdate in let filter = closure_of_filter evd evk untypedfilter in let evd,ev1 = restrict_applied_evar evd (evk,argsv1) filter candidates in @@ -1428,7 +1445,8 @@ exception NotEnoughInformationEvarEvar of EConstr.constr exception OccurCheckIn of evar_map * EConstr.constr exception MetaOccurInBodyInternal -let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = +let rec invert_definition flags conv_algo choose imitate_defs + env evd pbty (evk,argsv as ev) rhs = let aliases = make_alias_map env evd in let evdref = ref evd in let progress = ref false in @@ -1447,7 +1465,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = if choose then (mkVar id, p) else raise (NotUniqueInType sols) in let ty = lazy (Retyping.get_type_of env !evdref (of_alias t)) in - let evd = do_projection_effects (evar_define conv_algo ~choose) env ty !evdref p in + let evd = do_projection_effects conv_algo (evar_define flags conv_algo ~choose) env ty !evdref p in evdref := evd; c with @@ -1460,7 +1478,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = let ty = find_solution_type (evar_filtered_env evi) sols in let ty' = instantiate_evar_array evi ty argsv in let (evd,evar,(evk',argsv' as ev')) = - materialize_evar (evar_define conv_algo ~choose) env !evdref 0 ev ty' in + materialize_evar (evar_define flags conv_algo ~choose) env !evdref 0 ev ty' in let ts = expansions_of_var evd aliases t in let test c = isEvar evd c || List.exists (is_alias evd c) ts in let filter = restrict_upon_filter evd evk test argsv' in @@ -1484,13 +1502,15 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = | LocalAssum _ -> project_variable (RelAlias (i-k)) | LocalDef (_,b,_) -> try project_variable (RelAlias (i-k)) - with NotInvertibleUsingOurAlgorithm _ -> imitate envk (lift i (EConstr.of_constr b))) + with NotInvertibleUsingOurAlgorithm _ when imitate_defs -> + imitate envk (lift i (EConstr.of_constr b))) | Var id -> (match Environ.lookup_named id env' with | LocalAssum _ -> project_variable (VarAlias id) | LocalDef (_,b,_) -> try project_variable (VarAlias id) - with NotInvertibleUsingOurAlgorithm _ -> imitate envk (EConstr.of_constr b)) + with NotInvertibleUsingOurAlgorithm _ when imitate_defs -> + imitate envk (EConstr.of_constr b)) | LetIn (na,b,u,c) -> imitate envk (subst1 b c) | Evar (evk',args' as ev') -> @@ -1510,7 +1530,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = (* Make the virtual left evar real *) let ty = get_type_of env' evd t in let (evd,evar'',ev'') = - materialize_evar (evar_define conv_algo ~choose) env' evd k ev ty in + materialize_evar (evar_define flags conv_algo ~choose) env' evd k ev ty in (* materialize_evar may instantiate ev' by another evar; adjust it *) let (evk',args' as ev') = normalize_evar evd ev' in let evd = @@ -1555,7 +1575,7 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = | [x] -> x | _ -> let (evd,evar'',ev'') = - materialize_evar (evar_define conv_algo ~choose) env' !evdref k ev ty in + materialize_evar (evar_define flags conv_algo ~choose) env' !evdref k ev ty in evdref := restrict_evar evd (fst ev'') None (UpdateWith candidates); evar'') | None -> @@ -1594,46 +1614,33 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = * [define] tries to find an instance lhs such that * "lhs [hyps:=args]" unifies to rhs. The term "lhs" must be closed in * context "hyps" and not referring to itself. + * ev is assumed not to be frozen. *) -and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs = +and evar_define flags conv_algo ?(choose=false) ?(imitate_defs=true) env evd pbty (evk,argsv as ev) rhs = match EConstr.kind evd rhs with | Evar (evk2,argsv2 as ev2) -> if Evar.equal evk evk2 then - solve_refl ~can_drop:choose + solve_refl ~can_drop:choose flags (test_success conv_algo) env evd pbty evk argsv argsv2 else - solve_evar_evar ~force:choose - (evar_define conv_algo) conv_algo env evd pbty ev ev2 + solve_evar_evar ~force:choose flags + (evar_define flags conv_algo) conv_algo env evd pbty ev ev2 | _ -> try solve_candidates conv_algo env evd ev rhs with NoCandidates -> try - let (evd',body) = invert_definition conv_algo choose env evd pbty ev rhs in + let (evd',body) = invert_definition flags conv_algo choose imitate_defs env evd pbty ev rhs in if occur_meta evd' body then raise MetaOccurInBodyInternal; (* invert_definition may have instantiate some evars of rhs with evk *) (* so we recheck acyclicity *) if occur_evar_upto_types evd' evk body then raise (OccurCheckIn (evd',body)); (* needed only if an inferred type *) let evd', body = refresh_universes pbty env evd' body in -(* Cannot strictly type instantiations since the unification algorithm - * does not unify applications from left to right. - * e.g problem f x == g y yields x==y and f==g (in that order) - * Another problem is that type variables are evars of type Type - let _ = - try - let env = evar_filtered_env evi in - let ty = evi.evar_concl in - Typing.check env evd' body ty - with e -> - msg_info - (str "Ill-typed evar instantiation: " ++ fnl() ++ - pr_evar_map evd' ++ fnl() ++ - str "----> " ++ int ev ++ str " := " ++ - print_constr body); - raise e in*) - let evd' = check_evar_instance evd' evk body conv_algo in - Evd.define evk body evd' + let evd' = Evd.define evk body evd' in + (** Check after definition, as checking could involve the same + evar definition problem again otherwise *) + check_evar_instance evd' evk body conv_algo with | NotEnoughInformationToProgress sols -> postpone_non_unique_projection env evd pbty ev sols rhs @@ -1648,8 +1655,8 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs = let c = whd_all env evd rhs in match EConstr.kind evd c with | Evar (evk',argsv2) when Evar.equal evk evk' -> - solve_refl (fun env sigma pb c c' -> is_fconv pb env sigma c c') - env evd pbty evk argsv argsv2 + solve_refl flags (fun _b env sigma pb c c' -> is_fconv pb env sigma c c') + env evd pbty evk argsv argsv2 | _ -> raise (OccurCheckIn (evd,rhs)) @@ -1689,7 +1696,7 @@ let reconsider_unif_constraints conv_algo evd = (fun p (pbty,env,t1,t2 as x) -> match p with | Success evd -> - (match conv_algo env evd pbty t1 t2 with + (match conv_algo true env evd pbty t1 t2 with | Success _ as x -> x | UnifFailure (i,e) -> UnifFailure (i,CannotSolveConstraint (x,e))) | UnifFailure _ as x -> x) @@ -1702,10 +1709,11 @@ let reconsider_unif_constraints conv_algo evd = * if the problem couldn't be solved. *) (* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *) -let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1),t2) = +let solve_simple_eqn flags conv_algo ?(choose=false) ?(imitate_defs=true) + env evd (pbty,(evk1,args1 as ev1),t2) = try let t2 = whd_betaiota evd t2 in (* includes whd_evar *) - let evd = evar_define conv_algo ~choose env evd pbty ev1 t2 in + let evd = evar_define flags conv_algo ~choose ~imitate_defs env evd pbty ev1 t2 in reconsider_unif_constraints conv_algo evd with | NotInvertibleUsingOurAlgorithm t -> diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 4665ed29a2..94f17de6cc 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -16,6 +16,15 @@ type alias val of_alias : alias -> EConstr.t +type unify_flags = { + modulo_betaiota : bool; + open_ts : Names.transparent_state; + closed_ts : Names.transparent_state; + subterm_ts : Names.transparent_state; + frozen_evars : Evar.Set.t; + allow_K_at_toplevel : bool; + with_cs : bool} + type unification_result = | Success of evar_map | UnifFailure of evar_map * Pretype_errors.unification_error @@ -31,14 +40,16 @@ val expand_vars_in_term : env -> evar_map -> constr -> constr some problems that cannot be solved in a unique way (except if choose is true); fails if the instance is not valid for the given [ev] *) -type conv_fun = - env -> evar_map -> conv_pb -> constr -> constr -> unification_result +type types_or_terms = bool + +type conv_fun = types_or_terms -> + env -> evar_map -> conv_pb -> constr -> constr -> unification_result -type conv_fun_bool = +type conv_fun_bool = types_or_terms -> env -> evar_map -> conv_pb -> constr -> constr -> bool -val evar_define : conv_fun -> ?choose:bool -> env -> evar_map -> - bool option -> existential -> constr -> evar_map +val evar_define : unify_flags -> conv_fun -> ?choose:bool -> ?imitate_defs:bool -> + env -> evar_map -> bool option -> existential -> constr -> evar_map val refresh_universes : ?status:Evd.rigid -> @@ -49,15 +60,15 @@ val refresh_universes : bool option (* direction: true for levels lower than the existing levels *) -> env -> evar_map -> types -> evar_map * types -val solve_refl : ?can_drop:bool -> conv_fun_bool -> env -> evar_map -> +val solve_refl : ?can_drop:bool -> unify_flags -> conv_fun_bool -> env -> evar_map -> bool option -> Evar.t -> constr array -> constr array -> evar_map -val solve_evar_evar : ?force:bool -> +val solve_evar_evar : ?force:bool -> unify_flags -> (env -> evar_map -> bool option -> existential -> constr -> evar_map) -> conv_fun -> env -> evar_map -> bool option -> existential -> existential -> evar_map -val solve_simple_eqn : conv_fun -> ?choose:bool -> env -> evar_map -> +val solve_simple_eqn : unify_flags -> conv_fun -> ?choose:bool -> ?imitate_defs:bool -> env -> evar_map -> bool option * existential * constr -> unification_result val reconsider_unif_constraints : conv_fun -> evar_map -> unification_result diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 46e463512d..e65bdd8220 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -260,7 +260,7 @@ let apply_inference_hook hook env sigma frozen = match frozen with let apply_heuristics env sigma fail_evar = (* Resolve eagerly, potentially making wrong choices *) try solve_unif_constraints_with_heuristics - ~ts:(Typeclasses.classes_transparent_state ()) env sigma + ~flags:(default_flags_of (Typeclasses.classes_transparent_state ())) env sigma with e when CErrors.noncritical e -> let e = CErrors.push e in if fail_evar then iraise e else sigma diff --git a/pretyping/unification.ml b/pretyping/unification.ml index ce97912b84..6bb999c3f5 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -141,7 +141,8 @@ let abstract_list_all env evd typ c l = evd,(p,typp) let set_occurrences_of_last_arg args = - Some AllOccurrences :: List.tl (Array.map_to_list (fun _ -> None) args) + Evarconv.AtOccurrences AllOccurrences :: + List.tl (Array.map_to_list (fun _ -> Evarconv.default_occurrence_selection) args) let abstract_list_all_with_dependencies env evd typ c l = let (evd, ev) = new_evar env evd typ in @@ -149,8 +150,8 @@ let abstract_list_all_with_dependencies env evd typ c l = let n = List.length l in let argoccs = set_occurrences_of_last_arg (Array.sub (snd ev') 0 n) in let evd,b = - Evarconv.second_order_matching TransparentState.empty - env evd ev' argoccs c in + Evarconv.second_order_matching (Evarconv.default_flags_of TransparentState.empty) + env evd ev' (Evarconv.default_occurrence_test ~frozen_evars:Evar.Set.empty TransparentState.empty, argoccs) c in if b then let p = nf_evar evd ev in evd, p @@ -1315,8 +1316,8 @@ let order_metas metas = (* Solve an equation ?n[x1=u1..xn=un] = t where ?n is an evar *) -let solve_simple_evar_eqn ts env evd ev rhs = - match solve_simple_eqn (Evarconv.evar_conv_x ts) env evd (None,ev,rhs) with +let solve_simple_evar_eqn flags env evd ev rhs = + match solve_simple_eqn flags (Evarconv.conv_fun Evarconv.evar_conv_x flags) env evd (None,ev,rhs) with | UnifFailure (evd,reason) -> error_cannot_unify env evd ~reason (mkEvar ev,rhs); | Success evd -> evd @@ -1326,6 +1327,7 @@ let solve_simple_evar_eqn ts env evd ev rhs = is true, unification of types of metas is required *) let w_merge env with_types flags (evd,metas,evars : subst0) = + let eflags = Evarconv.default_flags_of flags.modulo_delta_types in let rec w_merge_rec evd metas evars eqns = (* Process evars *) @@ -1350,14 +1352,14 @@ let w_merge env with_types flags (evd,metas,evars : subst0) = else let evd' = let evd', rhs'' = pose_all_metas_as_evars curenv evd rhs' in - try solve_simple_evar_eqn flags.modulo_delta_types curenv evd' ev rhs'' + try solve_simple_evar_eqn eflags curenv evd' ev rhs'' with Retyping.RetypeError _ -> error_cannot_unify curenv evd' (mkEvar ev,rhs'') in w_merge_rec evd' metas evars' eqns | _ -> let evd', rhs'' = pose_all_metas_as_evars curenv evd rhs' in let evd' = - try solve_simple_evar_eqn flags.modulo_delta_types curenv evd' ev rhs'' + try solve_simple_evar_eqn eflags curenv evd' ev rhs'' with Retyping.RetypeError _ -> error_cannot_unify curenv evd' (mkEvar ev, rhs'') in w_merge_rec evd' metas evars' eqns diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 1b2756f49f..0f97a942ed 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -37,8 +37,8 @@ let define_and_solve_constraints evk c env evd = match List.fold_left (fun p (pbty,env,t1,t2) -> match p with - | Success evd -> Evarconv.evar_conv_x TransparentState.full env evd pbty t1 t2 - | UnifFailure _ as x -> x) (Success evd) + | Success evd -> Evarconv.evar_conv_x (Evarconv.default_flags_of TransparentState.full) env evd pbty t1 t2 + | UnifFailure _ as x -> x) (Success evd) pbs with | Success evd -> evd diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index ba7645446d..429bada7e3 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1103,7 +1103,7 @@ let initial_select_evars filter = let resolve_typeclass_evars debug depth unique env evd filter split fail = let evd = try Evarconv.solve_unif_constraints_with_heuristics - ~ts:(Typeclasses.classes_transparent_state ()) env evd + ~flags:(Evarconv.default_flags_of (Typeclasses.classes_transparent_state ())) env evd with e when CErrors.noncritical e -> evd in resolve_all_evars debug depth unique env -- cgit v1.2.3 From 1c9e1a39652b401805029519055aa62adacde339 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 26 Jul 2018 17:07:49 +0200 Subject: evarconv/evarsolve: HO matching algorithm with occurrence selection Also extend evarconv to handle frozen evars and flags for delta and betaiota reduction. - Make evar_conv unification take a record of flags - Adds an imitate_defs option to evarsolve, deactivated in first-order unification - Add a way to call back conv_algo differently on types - We distinguish comparison of terms and types which might be different w.r.t. delta reductions allowed (everything for types, controlled for terms). We keep the with_cs flag even for types, to avoid incompatibilities (in HoTT's theories/Spaces/No.v, the refine in No_encode_le_lt would diverge due to trying a default canonical structure during type verification). - In evarsolve, do_project_effects checks evar instances now - Solve evar-evar unification using miller patterns if possible. - FO heuristic in evarconv - Do not catch critical exceptions in evarconv - Force HO matching to abstract toplevel evar args, This disallows K on them, more compatible with w_unify_to_subterm. - occur_rigidly improvement, better approx of occur-check. - K_at_toplevel, subterm_ts, betaiota and frozen_evars flags taken into account in apply_on_subterm and evar_conv_x. This allow implementing a unification without reduction, e.g. for the fast path of rewrite subterm selection. - second_order_matching works up-to cumulativity - pretyping/coercion: now take unification flags as argument - pretyping/unification: default_occurrence_test takes a frozen_evars set export elim_flags_evars to compute frozen evars before elim - evarsolve: fix evar_define doing check in the wrong order, as conv_algo can trigger the definition of the evar itself, define it first in the evd. - w_unify: disallow HO in consider_remaining. Only used in rewrite now - use evar_abstraction info - catch second_order_matching NoOccurrence exception in second_order_matching_with_args - unify_with_heuristics in API - second_order_matching: thin evars after abstraction to put in the right env or fail. --- engine/evd.mli | 2 +- pretyping/evarconv.ml | 323 +++++++++++++++++++++++++++++++++++++------------ pretyping/evarconv.mli | 31 ++++- 3 files changed, 276 insertions(+), 80 deletions(-) diff --git a/engine/evd.mli b/engine/evd.mli index 1c852971f5..1f6a0da882 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -104,7 +104,7 @@ type evar_info = { in the solution *) evar_abstract_arguments : Abstraction.t; (** Boolean information over {!evar_hyps}, telling if an hypothesis instance - can be immitated or should stay abstract in HO unification problems + can be imitated or should stay abstract in HO unification problems and inversion (see [second_order_matching_with_args] for its use). *) evar_source : Evar_kinds.t located; (** Information about the evar. *) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index de5f00f71a..99c32e06ee 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -153,6 +153,18 @@ let position_problem l2r = function | CONV -> None | CUMUL -> Some l2r +(* [occur_rigidly ev evd t] tests if the evar ev occurs in a rigid + context in t + + That function should be an over approximation of occur-check, it can + return true even if the occur-check would fail on the normal form, as + otherwise we will postpone unsolvable constraints while maybe a + reduction would have allowed unification (see bug 3539 for example). + + The boolean indicates if the term is a rigid head. For applications, + this means than an occurrence of the evar in arguments should be looked + at to find an occur-check. *) + let occur_rigidly (evk,_ as ev) evd t = let rec aux t = match EConstr.kind evd t with @@ -161,7 +173,8 @@ let occur_rigidly (evk,_ as ev) evd t = | Proj (p, c) -> not (aux c) | Evar (evk',_) -> if Evar.equal evk evk' then raise Occur else false | Cast (p, _, _) -> aux p - | Lambda _ | LetIn _ -> false + | Lambda (na, t, b) -> aux b + | LetIn (na, _, _, b) -> aux b | Const _ -> false | Prod (_, b, t) -> ignore(aux b || aux t); true | Rel _ | Var _ -> false @@ -1110,28 +1123,55 @@ let choose_less_dependent_instance evk evd term args = | [] -> None | (id, _) :: _ -> Some (Evd.define evk (mkVar id) evd) -let apply_on_subterm env evdref f c t = +type occurrence_match_test = + env -> evar_map -> constr -> + env -> evar_map -> int -> constr -> constr -> bool * evar_map + +type prefer_abstraction = bool + +type occurrence_selection = + | AtOccurrences of Locus.occurrences + | Unspecified of prefer_abstraction + +type occurrences_selection = + occurrence_match_test * occurrence_selection list + +let default_occurrence_selection = Unspecified false + +let default_occurrence_test ~frozen_evars ts _ origsigma _ env sigma _ c pat = + let flags = { (default_flags_of ~subterm_ts:ts ts) with frozen_evars } in + match evar_conv_x flags env sigma CONV c pat with + | Success sigma -> true, sigma + | UnifFailure _ -> false, sigma + +let default_occurrences_selection ?(frozen_evars=Evar.Set.empty) ts n = + (default_occurrence_test ~frozen_evars ts, + List.init n (fun _ -> default_occurrence_selection)) + +let apply_on_subterm env evdref fixedref f test c t = + let test = test env !evdref c in + let prc env = print_constr_env env !evdref in let rec applyrec (env,(k,c) as acc) t = - (* By using eq_constr, we make an approximation, for instance, we *) - (* could also be interested in finding a term u convertible to t *) - (* such that c occurs in u *) - let eq_constr c1 c2 = match EConstr.eq_constr_universes env !evdref c1 c2 with - | None -> false - | Some cstr -> - try ignore (Evd.add_universe_constraints !evdref cstr); true - with UniversesDiffer -> false - in - if eq_constr c t then f k - else + if Evar.Set.exists (fun fixed -> occur_evar !evdref fixed t) !fixedref then match EConstr.kind !evdref t with - | Evar (evk,args) -> - let ctx = evar_filtered_context (Evd.find_undefined !evdref evk) in - let g decl a = if is_local_assum decl then applyrec acc a else a in - mkEvar (evk, Array.of_list (List.map2 g ctx (Array.to_list args))) - | _ -> - map_constr_with_binders_left_to_right !evdref - (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c))) - applyrec acc t + | Evar (ev, args) when Evar.Set.mem ev !fixedref -> t + | _ -> map_constr_with_binders_left_to_right !evdref + (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c))) + applyrec acc t + else + (if !debug_ho_unification then + Feedback.msg_debug Pp.(str"Testing " ++ prc env c ++ str" against " ++ prc env t); + let b, evd = + try test env !evdref k c t + with e when CErrors.noncritical e -> assert false in + if b then (evdref := evd; + if !debug_ho_unification then Feedback.msg_debug (Pp.str "succeeded"); + f k t) + else ( + if !debug_ho_unification then Feedback.msg_debug (Pp.str "failed"); + map_constr_with_binders_left_to_right !evdref + (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c))) + applyrec acc t)) in applyrec (env,(0,c)) t @@ -1178,85 +1218,208 @@ let set_solve_evars f = solve_evars := f * proposition from Dan Grayson] *) +let check_selected_occs env sigma c occ occs = + let notfound = + match occs with + | AtOccurrences occs -> + (match occs with + | Locus.AtLeastOneOccurrence -> occ == 1 + | Locus.AllOccurrences -> false + | Locus.AllOccurrencesBut l -> List.last l > occ + | Locus.OnlyOccurrences l -> List.last l > occ + | Locus.NoOccurrences -> false) + | Unspecified abstract -> false + in if notfound then + raise (PretypeError (env,sigma,NoOccurrenceFound (c,None))) + else () + exception TypingFailed of evar_map -let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = +let set_of_evctx l = + List.fold_left (fun s decl -> Id.Set.add (NamedDecl.get_id decl) s) Id.Set.empty l + +(** Weaken the existentials so that they can be typed in sign and raise + an error if the term otherwise mentions variables not bound in sign. *) +let thin_evars env sigma sign c = + let evdref = ref sigma in + let ctx = set_of_evctx sign in + let rec applyrec (env,acc) t = + match kind sigma t with + | Evar (ev, args) -> + let evi = Evd.find_undefined sigma ev in + let filter = Array.map (fun c -> Id.Set.subset (collect_vars sigma c) ctx) args in + let filter = Filter.make (Array.to_list filter) in + let candidates = Option.map (List.map EConstr.of_constr) (evar_candidates evi) in + let evd, ev = restrict_evar !evdref ev filter candidates in + evdref := evd; whd_evar !evdref t + | Var id -> + if not (Id.Set.mem id ctx) then raise (TypingFailed sigma) + else t + | _ -> + map_constr_with_binders_left_to_right !evdref + (fun d (env,acc) -> (push_rel d env, acc+1)) + applyrec (env,acc) t + in + let c' = applyrec (env,0) c in + (!evdref, c') + +let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = try let evi = Evd.find_undefined evd evk in + let evi = nf_evar_info evd evi in + let env_evar_unf = evar_env evi in let env_evar = evar_filtered_env evi in let sign = named_context_val env_evar in let ctxt = evar_filtered_context evi in - let instance = List.map mkVar (List.map NamedDecl.get_id ctxt) in - + if !debug_ho_unification then + (Feedback.msg_debug Pp.(str"env rhs: " ++ print_env env_rhs); + Feedback.msg_debug Pp.(str"env evars: " ++ print_env env_evar)); + let args = Array.map (nf_evar evd) args in + let vars = List.map NamedDecl.get_id ctxt in + let argsubst = List.map2 (fun id c -> (id, c)) vars (Array.to_list args) in + let instance = List.map mkVar vars in + let rhs = nf_evar evd rhs in + if not (noccur_evar env_rhs evd evk rhs) then raise (TypingFailed evd); + (** Ensure that any progress made by Typing.e_solve_evars will not contradict + the solution we are trying to build here by adding the problem as a constraint. *) + let evd = Evarutil.add_unification_pb (CONV,env_rhs,mkEvar (evk,args),rhs) evd in + let evdref = ref evd in + let prc env c = print_constr_env env !evdref c in let rec make_subst = function | decl'::ctxt', c::l, occs::occsl when isVarId evd (NamedDecl.get_id decl') c -> begin match occs with - | Some _ -> - user_err Pp.(str "Cannot force abstraction on identity instance.") - | None -> + | AtOccurrences loc when not (Locusops.is_all_occurrences loc) -> + user_err Pp.(str "Cannot force abstraction on identity instance.") + | _ -> make_subst (ctxt',l,occsl) end | decl'::ctxt', c::l, occs::occsl -> let id = NamedDecl.get_id decl' in let t = NamedDecl.get_type decl' in let evs = ref [] in - let ty = Retyping.get_type_of env_rhs evd c in - let filter' = filter_possible_projections evd c ty ctxt args in + let c = nf_evar evd c in + (* ty is in env_rhs now *) + let ty = replace_vars argsubst t in + let filter' = filter_possible_projections !evdref c (nf_evar evd ty) ctxt args in (id,t,c,ty,evs,Filter.make filter',occs) :: make_subst (ctxt',l,occsl) | _, _, [] -> [] | _ -> anomaly (Pp.str "Signature or instance are shorter than the occurrences list.") in - - let rec set_holes evdref rhs = function - | (id,_,c,cty,evsref,filter,occs)::subst -> - let set_var k = - match occs with - | Some (Locus.AtLeastOneOccurrence | Locus.AllOccurrences) -> mkVar id - | Some _ -> user_err Pp.(str "Selection of specific occurrences not supported") - | None -> - let evty = set_holes evdref cty subst in - let instance = Filter.filter_list filter instance in - let evd = !evdref in - let (evd, ev) = new_evar_instance sign evd evty ~filter instance in - evdref := evd; - evsref := (fst (destEvar !evdref ev),evty)::!evsref; - ev in - set_holes evdref (apply_on_subterm env_rhs evdref set_var c rhs) subst + let fixed = ref Evar.Set.empty in + let rec set_holes env_rhs evdref rhs = function + | (id,idty,c,cty,evsref,filter,occs)::subst -> + let c = nf_evar !evdref c in + if !debug_ho_unification then + Feedback.msg_debug Pp.(str"set holes for: " ++ + prc env_rhs (mkVar id) ++ spc () ++ + prc env_rhs c ++ str" in " ++ + prc env_rhs rhs); + let occ = ref 1 in + let set_var k inst = + let oc = !occ in + if !debug_ho_unification then + (Feedback.msg_debug Pp.(str"Found one occurrence"); + Feedback.msg_debug Pp.(str"cty: " ++ prc env_rhs c)); + incr occ; + match occs with + | AtOccurrences occs -> + if Locusops.is_selected oc occs then mkVar id + else inst + | Unspecified prefer_abstraction -> + let evty = set_holes env_rhs evdref cty subst in + let evty = nf_evar !evdref evty in + if !debug_ho_unification then + Feedback.msg_debug Pp.(str"abstracting one occurrence " ++ prc env_rhs inst ++ + str" of type: " ++ prc env_evar evty ++ + str " for " ++ prc env_rhs c); + let instance = Filter.filter_list filter instance in + (** Allow any type lower than the variable's type as the + abstracted subterm might have a smaller type, which could be + crucial to make the surrounding context typecheck. *) + let evd, evty = + if isArity !evdref evty then + refresh_universes ~status:Evd.univ_flexible (Some true) + env_evar_unf !evdref evty + else !evdref, evty in + let (evd, ev) = new_evar_instance sign evd evty ~filter instance in + let evk = fst (destEvar !evdref ev) in + evdref := evd; + evsref := (evk,evty,inst,prefer_abstraction)::!evsref; + fixed := Evar.Set.add evk !fixed; + ev + in + let rhs' = apply_on_subterm env_rhs evdref fixed set_var test c rhs in + if !debug_ho_unification then + Feedback.msg_debug Pp.(str"abstracted: " ++ prc env_rhs rhs'); + let () = check_selected_occs env_rhs !evdref c !occ occs in + let env_rhs' = push_named (NamedDecl.LocalAssum (id,idty)) env_rhs in + set_holes env_rhs' evdref rhs' subst | [] -> rhs in let subst = make_subst (ctxt,Array.to_list args,argoccs) in - let evd, rhs = - let evdref = ref evd in - let rhs = set_holes evdref rhs subst in - !evdref, rhs - in - + let rhs' = set_holes env_rhs evdref rhs subst in + let evd = !evdref in + let rhs' = nf_evar evd rhs' in + (** Thin evars making the term typable in env_evar *) + let evd, rhs' = thin_evars env_evar evd ctxt rhs' in (* We instantiate the evars of which the value is forced by typing *) - let evd,rhs = - try !solve_evars env_evar evd rhs + if !debug_ho_unification then + (Feedback.msg_debug Pp.(str"solve_evars on: " ++ prc env_evar rhs'); + Feedback.msg_debug Pp.(str"evars: " ++ pr_evar_map (Some 0) evd)); + let evd,rhs' = + try !solve_evars env_evar evd rhs' with e when Pretype_errors.precatchable_exception e -> (* Could not revert all subterms *) - raise (TypingFailed evd) in + raise (TypingFailed !evdref) in + let rhs' = nf_evar evd rhs' in + (* We instantiate the evars of which the value is forced by typing *) + if !debug_ho_unification then + (Feedback.msg_debug Pp.(str"after solve_evars: " ++ prc env_evar rhs'); + Feedback.msg_debug Pp.(str"evars: " ++ pr_evar_map (Some 0) evd)); let rec abstract_free_holes evd = function - | (id,idty,c,_,evsref,_,_)::l -> + | (id,idty,c,cty,evsref,_,_)::l -> + let c = nf_evar evd c in + if !debug_ho_unification then + Feedback.msg_debug Pp.(str"abstracting: " ++ + prc env_rhs (mkVar id) ++ spc () ++ + prc env_rhs c); let rec force_instantiation evd = function - | (evk,evty)::evs -> - let evd = + | (evk,evty,inst,abstract)::evs -> + let evk = Option.default evk (Evarutil.advance evd evk) in + let evd = if is_undefined evd evk then - (* We force abstraction over this unconstrained occurrence *) + (* We try abstraction or concretisation for *) + (* this unconstrained occurrence *) (* and we use typing to propagate this instantiation *) - (* This is an arbitrary choice *) - let evd = Evd.define evk (mkVar id) evd in - match evar_conv_x ts env_evar evd CUMUL idty evty with - | UnifFailure _ -> user_err Pp.(str "Cannot find an instance") - | Success evd -> - match reconsider_unif_constraints (evar_conv_x ts) evd with - | UnifFailure _ -> user_err Pp.(str "Cannot find an instance") - | Success evd -> - evd + (* We avoid making an arbitrary choice by leaving candidates *) + (* if both can work *) + let evi = Evd.find_undefined evd evk in + let vid = mkVar id in + let candidates = [inst; vid] in + try + let evd, ev = Evarutil.restrict_evar evd evk (Evd.evar_filter evi) (Some candidates) in + let evi = Evd.find evd ev in + (match evar_candidates evi with + | Some [t] -> + if not (noccur_evar env_rhs evd ev (EConstr.of_constr t)) then + raise (TypingFailed evd); + let evd = Evd.define ev (EConstr.of_constr t) evd in + check_evar_instance evd ev (EConstr.of_constr t) (conv_fun evar_conv_x flags) + | Some l when abstract && List.exists (fun c -> isVarId evd id (EConstr.of_constr c)) l -> + let evd = Evd.define ev vid evd in + check_evar_instance evd ev vid (conv_fun evar_conv_x flags) + | _ -> evd) + with e -> user_err (Pp.str "Cannot find an instance") else - evd + ((if !debug_ho_unification then + let evi = Evd.find evd evk in + let env = Evd.evar_env evi in + Feedback.msg_debug Pp.(str"evar is defined: " ++ + int (Evar.repr evk) ++ spc () ++ + prc env (match evar_body evi with Evar_defined c -> c + | Evar_empty -> assert false))); + evd) in force_instantiation evd evs | [] -> @@ -1472,22 +1635,28 @@ let solve_unif_constraints_with_heuristics env | (pbty,env,t1,t2 as pb) :: pbs -> (match apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 with | Success evd' -> - let (evd', rest) = extract_all_conv_pbs evd' in - begin match rest with + let evd' = solve_unconstrained_evars_with_candidates flags evd' in + let (evd', rest) = extract_all_conv_pbs evd' in + begin match rest with | [] -> aux evd' pbs true stuck - | _ -> (* Unification got actually stuck, postpone *) - aux evd pbs progress (pb :: stuck) + | l -> + (* Unification got actually stuck, postpone *) + let reason = CannotSolveConstraint (pb,ProblemBeyondCapabilities) in + aux evd pbs progress ((pb, reason):: stuck) end | UnifFailure (evd,reason) -> - error_cannot_unify env evd pb ~reason t1 t2) + if is_beyond_capabilities reason then + aux evd pbs progress ((pb,reason) :: stuck) + else aux evd [] false ((pb,reason) :: stuck)) | _ -> - if progress then aux evd stuck false [] + if progress then aux evd (List.map fst stuck) false [] else match stuck with | [] -> (* We're finished *) evd - | (pbty,env,t1,t2 as pb) :: _ -> - (* There remains stuck problems *) - error_cannot_unify env evd pb t1 t2 + | ((pbty,env,t1,t2 as pb), reason) :: _ -> + (* There remains stuck problems *) + Pretype_errors.error_cannot_unify ?loc:(loc_of_conv_pb evd pb) + env evd ~reason (t1, t2) in let (evd,pbs) = extract_all_conv_pbs evd in let heuristic_solved_evd = aux evd pbs false [] in diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index efb827d866..994576c45b 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -47,6 +47,7 @@ val unify_with_heuristics : unify_flags -> with_ho:bool -> val conv : env -> ?ts:TransparentState.t -> evar_map -> constr -> constr -> evar_map option val cumul : env -> ?ts:TransparentState.t -> evar_map -> constr -> constr -> evar_map option + (** {6 Unification heuristics. } *) (** Try heuristics to solve pending unification problems and to solve @@ -73,8 +74,34 @@ val check_conv_record : env -> evar_map -> (** Try to solve problems of the form ?x[args] = c by second-order matching, using typing to select occurrences *) -val second_order_matching : TransparentState.t -> env -> evar_map -> - EConstr.existential -> occurrences option list -> constr -> evar_map * bool +type occurrence_match_test = + env -> evar_map -> constr -> (* Used to precompute the local tests *) + env -> evar_map -> int -> constr -> constr -> bool * evar_map + +(** When given the choice of abstracting an occurrence or leaving it, + force abstration. *) +type prefer_abstraction = bool + +type occurrence_selection = + | AtOccurrences of occurrences + | Unspecified of prefer_abstraction + +(** By default, unspecified, not preferring abstraction. + This provides the most general solutions. *) +val default_occurrence_selection : occurrence_selection + +type occurrences_selection = + occurrence_match_test * occurrence_selection list + +val default_occurrence_test : frozen_evars:Evar.Set.t -> TransparentState.t -> occurrence_match_test + +(** [default_occurrence_selection n] + Gives the default test and occurrences for [n] arguments *) +val default_occurrences_selection : ?frozen_evars:Evar.Set.t (* By default, none *) -> + TransparentState.t -> int -> occurrences_selection + +val second_order_matching : unify_flags -> env -> evar_map -> + EConstr.existential -> occurrences_selection -> constr -> evar_map * bool (** Declare function to enforce evars resolution by using typing constraints *) -- cgit v1.2.3 From dc8f191f2d81fd5f851b84e7aeda487df584197e Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 28 Jul 2017 01:35:02 +0200 Subject: unification: abstract_list_all_with_dependencies fix For second_order_matching call, prefer abstraction of evar arguments, and use same test as original (just eq_constr) --- pretyping/unification.ml | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 6bb999c3f5..8d8313eeff 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -142,7 +142,14 @@ let abstract_list_all env evd typ c l = let set_occurrences_of_last_arg args = Evarconv.AtOccurrences AllOccurrences :: - List.tl (Array.map_to_list (fun _ -> Evarconv.default_occurrence_selection) args) + List.tl (Array.map_to_list (fun _ -> Evarconv.Unspecified true) args) + +let occurrence_test _ _ _ env sigma _ c1 c2 = + match EConstr.eq_constr_universes env sigma c1 c2 with + | None -> false, sigma + | Some cstr -> + try true, Evd.add_universe_constraints sigma cstr + with UniversesDiffer -> false, sigma let abstract_list_all_with_dependencies env evd typ c l = let (evd, ev) = new_evar env evd typ in @@ -150,8 +157,9 @@ let abstract_list_all_with_dependencies env evd typ c l = let n = List.length l in let argoccs = set_occurrences_of_last_arg (Array.sub (snd ev') 0 n) in let evd,b = - Evarconv.second_order_matching (Evarconv.default_flags_of TransparentState.empty) - env evd ev' (Evarconv.default_occurrence_test ~frozen_evars:Evar.Set.empty TransparentState.empty, argoccs) c in + Evarconv.second_order_matching + (Evarconv.default_flags_of TransparentState.empty) + env evd ev' (occurrence_test, argoccs) c in if b then let p = nf_evar evd ev in evd, p -- cgit v1.2.3 From 781f050bcfabe02e225f3c1d29ee649610d6d680 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 15 Aug 2018 12:42:04 +0200 Subject: Abstraction naming --- engine/evd.ml | 8 ++++++-- engine/evd.mli | 6 +++++- pretyping/evarconv.ml | 21 ++++++++++++--------- pretyping/evarconv.mli | 3 +-- pretyping/unification.ml | 2 +- 5 files changed, 25 insertions(+), 15 deletions(-) diff --git a/engine/evd.ml b/engine/evd.ml index 2d28892e6e..a89a67c287 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -128,11 +128,15 @@ end module Abstraction = struct - type t = bool list + type abstraction = + | Abstract + | Imitate + + type t = abstraction list let identity = [] - let abstract_last l = true :: l + let abstract_last l = Abstract :: l end (* The kinds of existential variables are now defined in [Evar_kinds] *) diff --git a/engine/evd.mli b/engine/evd.mli index 1f6a0da882..fcccb1be5a 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -78,7 +78,11 @@ sig end module Abstraction : sig - type t = bool list + type abstraction = + | Abstract + | Imitate + + type t = abstraction list val identity : t diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 99c32e06ee..95301fb9ca 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1127,16 +1127,14 @@ type occurrence_match_test = env -> evar_map -> constr -> env -> evar_map -> int -> constr -> constr -> bool * evar_map -type prefer_abstraction = bool - type occurrence_selection = | AtOccurrences of Locus.occurrences - | Unspecified of prefer_abstraction + | Unspecified of Abstraction.abstraction type occurrences_selection = occurrence_match_test * occurrence_selection list -let default_occurrence_selection = Unspecified false +let default_occurrence_selection = Unspecified Abstraction.Imitate let default_occurrence_test ~frozen_evars ts _ origsigma _ env sigma _ c pat = let flags = { (default_flags_of ~subterm_ts:ts ts) with frozen_evars } in @@ -1406,7 +1404,8 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = raise (TypingFailed evd); let evd = Evd.define ev (EConstr.of_constr t) evd in check_evar_instance evd ev (EConstr.of_constr t) (conv_fun evar_conv_x flags) - | Some l when abstract && List.exists (fun c -> isVarId evd id (EConstr.of_constr c)) l -> + | Some l when abstract = Abstraction.Abstract && + List.exists (fun c -> isVarId evd id (EConstr.of_constr c)) l -> let evd = Evd.define ev vid evd in check_evar_instance evd ev vid (conv_fun evar_conv_x flags) | _ -> evd) @@ -1468,10 +1467,14 @@ let default_evar_selection flags evd (ev,args) = let rec aux args abs = match args, abs with | _ :: args, a :: abs -> - let spec = if not flags.allow_K_at_toplevel then - AtOccurrences (if a then Locus.AtLeastOneOccurrence else Locus.AllOccurrences) - else Unspecified a in - spec :: aux args abs + let spec = + if not flags.allow_K_at_toplevel then + let occs = + if a == Abstraction.Abstract then Locus.AtLeastOneOccurrence + else Locus.AllOccurrences + in AtOccurrences occs + else Unspecified a + in spec :: aux args abs | l, [] -> List.map (fun _ -> default_occurrence_selection) l | [], _ :: _ -> assert false in aux (Array.to_list args) evi.evar_abstract_arguments diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 994576c45b..c2ad4e6678 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -80,11 +80,10 @@ type occurrence_match_test = (** When given the choice of abstracting an occurrence or leaving it, force abstration. *) -type prefer_abstraction = bool type occurrence_selection = | AtOccurrences of occurrences - | Unspecified of prefer_abstraction + | Unspecified of Abstraction.abstraction (** By default, unspecified, not preferring abstraction. This provides the most general solutions. *) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 8d8313eeff..486aa38558 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -142,7 +142,7 @@ let abstract_list_all env evd typ c l = let set_occurrences_of_last_arg args = Evarconv.AtOccurrences AllOccurrences :: - List.tl (Array.map_to_list (fun _ -> Evarconv.Unspecified true) args) + List.tl (Array.map_to_list (fun _ -> Evarconv.Unspecified Abstraction.Abstract) args) let occurrence_test _ _ _ env sigma _ c1 c2 = match EConstr.eq_constr_universes env sigma c1 c2 with -- cgit v1.2.3 From 5f05bb81c2de54d31887b276d0f127455dd83815 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 15 Aug 2018 13:10:13 +0200 Subject: Correct occur_rigidly --- pretyping/evarconv.ml | 42 ++++++++++++++++++++++++++---------------- 1 file changed, 26 insertions(+), 16 deletions(-) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 95301fb9ca..0e69dd43d5 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -154,31 +154,41 @@ let position_problem l2r = function | CUMUL -> Some l2r (* [occur_rigidly ev evd t] tests if the evar ev occurs in a rigid - context in t + context in t. Precondition: t has a rigid head. - That function should be an over approximation of occur-check, it can - return true even if the occur-check would fail on the normal form, as - otherwise we will postpone unsolvable constraints while maybe a - reduction would have allowed unification (see bug 3539 for example). + That function is an under approximation of occur-check, it can return + false even if the occur-check would succeed on the normal form. This + means we might postpone unsolvable constraints which will ultimately + result in an occur-check after reductions. If it returns true, we + know that the occur-check would also return true on the normal form. - The boolean indicates if the term is a rigid head. For applications, - this means than an occurrence of the evar in arguments should be looked - at to find an occur-check. *) + The boolean indicates if the term is a rigid head. For applications, + this means than an occurrence of the evar in arguments should be looked + at to find an occur-check. *) -let occur_rigidly (evk,_ as ev) evd t = +let occur_rigidly flags env evd (evk,_) t = let rec aux t = match EConstr.kind evd t with - | App (f, c) -> if aux f then Array.exists aux c else false - | Construct _ | Ind _ | Sort _ | Meta _ | Fix _ | CoFix _ | Int _ -> true - | Proj (p, c) -> not (aux c) - | Evar (evk',_) -> if Evar.equal evk evk' then raise Occur else false + | App (f, c) -> if aux f then (Array.iter (fun x -> ignore (aux x)) c; true) else false + | Construct _ | Ind _ | Sort _ -> true + | Proj (p, c) -> + let cst = Projection.constant p in + if not (is_transparent_constant flags.open_ts cst) then + (ignore (aux c); true) + else false + | Evar (evk',l as ev) -> + if Evar.equal evk evk' then raise Occur + else if is_frozen flags ev then + (Array.iter (fun x -> ignore (aux x)) l; true) + else false | Cast (p, _, _) -> aux p | Lambda (na, t, b) -> aux b | LetIn (na, _, _, b) -> aux b - | Const _ -> false + | Const (c,_) -> not (is_transparent_constant flags.open_ts c) | Prod (_, b, t) -> ignore(aux b || aux t); true | Rel _ | Var _ -> false - | Case (_,_,c,_) -> if eq_constr evd (mkEvar ev) c then raise Occur else false + | Case (_,_,c,_) -> if isEvar evd c && occur_evar evd evk c then raise Occur else false + | Meta _ | Fix _ | CoFix _ | Int _ -> false in try ignore(aux t); false with Occur -> true (* [check_conv_record env sigma (t1,stack1) (t2,stack2)] tries to decompose @@ -633,7 +643,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty ise_try evd [eta;(* Postpone the use of an heuristic *) (fun i -> - if not (occur_rigidly ev i tR) then + if not (occur_rigidly flags env i ev tR) then let i,tF = if isRel i tR || isVar i tR then (* Optimization so as to generate candidates *) -- cgit v1.2.3 From af9b88c253b578ad53ee884ff3102d0a74056a1e Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 15 Aug 2018 14:02:03 +0200 Subject: Fix indentation (removing tabs) --- proofs/goal.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/proofs/goal.ml b/proofs/goal.ml index 2104eefa66..e5688fe730 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -58,11 +58,11 @@ module V82 = struct created. *) let prev_future_goals = Evd.save_future_goals evars in let evi = { Evd.evar_hyps = hyps; - Evd.evar_concl = concl; - Evd.evar_filter = Evd.Filter.identity; + Evd.evar_concl = concl; + Evd.evar_filter = Evd.Filter.identity; Evd.evar_abstract_arguments = Evd.Abstraction.identity; - Evd.evar_body = Evd.Evar_empty; - Evd.evar_source = (Loc.tag Evar_kinds.GoalEvar); + Evd.evar_body = Evd.Evar_empty; + Evd.evar_source = (Loc.tag Evar_kinds.GoalEvar); Evd.evar_candidates = None } in let (evars, evk) = Evarutil.new_pure_evar_full evars ~typeclass_candidate:false evi in -- cgit v1.2.3 From 2cf15ef8e3ddebe285ec0e9f5f8715b025ba4eec Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 15 Aug 2018 14:22:15 +0200 Subject: Rename types_or_terms and the unification function types --- pretyping/evarconv.ml | 25 ++++++++++++++++----- pretyping/evarconv.mli | 2 +- pretyping/evarsolve.ml | 60 +++++++++++++++++++++++++++---------------------- pretyping/evarsolve.mli | 29 ++++++++++++++++-------- 4 files changed, 74 insertions(+), 42 deletions(-) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 0e69dd43d5..8f7c88b0db 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -424,7 +424,10 @@ let conv_fun f flags on_types = in let termfn env evd pbty term1 term2 = f flags env evd pbty term1 term2 - in if on_types then typefn else termfn + in + match on_types with + | TypeUnification -> typefn + | TermUnification -> termfn let rec evar_conv_x flags env evd pbty term1 term2 = let term1 = whd_head_evar evd term1 in @@ -735,7 +738,11 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty match ise_stack2 false env i (evar_conv_x flags) sk1 sk2 with |None, Success i' -> Success (solve_refl flags (fun p env i pbty a1 a2 -> - let flags = if p then default_flags env else flags in + let flags = + match p with + | TypeUnification -> default_flags env + | TermUnification -> flags + in is_success (evar_conv_x flags env i pbty a1 a2)) env i' (position_problem true pbty) sp1 al1 al2) |_, (UnifFailure _ as x) -> x @@ -967,7 +974,11 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty |None, Success i' -> (** FIXME: solve_refl can restrict the evar, do we want to allow that? *) Success (solve_refl flags (fun p env i pbty a1 a2 -> - let flags = if p then default_flags env else flags in + let flags = + match p with + | TypeUnification -> default_flags env + | TermUnification -> flags + in is_success (evar_conv_x flags env i pbty a1 a2)) env i' (position_problem true pbty) sp1 al1 al2) |_, (UnifFailure _ as x) -> x @@ -1544,8 +1555,12 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 = UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason))) | Evar (evk1,args1), Evar (evk2,args2) when Evar.equal evk1 evk2 -> let f ontype env evd pbty x y = - let reds = if ontype then full_transparent_state else flags.open_ts in - is_fconv ~reds pbty env evd x y in + let reds = + match ontype with + | TypeUnification -> full_transparent_state + | TermUnification -> flags.open_ts + in is_fconv ~reds pbty env evd x y + in Success (solve_refl ~can_drop:true flags f env evd (position_problem true pbty) evk1 args1 args2) | Evar ev1, Evar ev2 when app_empty -> diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index c2ad4e6678..bd55b952a6 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -24,7 +24,7 @@ val default_flags_of : ?subterm_ts:transparent_state -> transparent_state -> uni type unify_fun = unify_flags -> env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result -val conv_fun : unify_fun -> unify_flags -> Evarsolve.conv_fun +val conv_fun : unify_fun -> unify_flags -> Evarsolve.unifier exception UnableToUnify of evar_map * Pretype_errors.unification_error diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index aad21ad932..2ff52d1657 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -33,6 +33,34 @@ type unify_flags = { allow_K_at_toplevel : bool; with_cs : bool } +type unification_kind = + | TypeUnification + | TermUnification + +(************************) +(* Unification results *) +(************************) + +type unification_result = + | Success of evar_map + | UnifFailure of evar_map * unification_error + +let is_success = function Success _ -> true | UnifFailure _ -> false + +let test_success conv_algo b env evd c c' rhs = + is_success (conv_algo b env evd c c' rhs) + +(** A unification function: parameterized by the kind of unification, + environment, sigma, conversion problem and the two terms to unify. *) +type unifier = unification_kind -> + env -> evar_map -> conv_pb -> constr -> constr -> unification_result + +(** A conversion function: parameterized by the kind of unification, + environment, sigma, conversion problem and the two terms to convert. + Conversion is not allowed to instantiate evars contrary to unification. *) +type conversion_check = unification_kind -> + env -> evar_map -> conv_pb -> constr -> constr -> bool + let normalize_evar evd ev = match EConstr.kind evd (mkEvar ev) with | Evar (evk,args) -> (evk,args) @@ -138,20 +166,6 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) let get_type_of_refresh ?(polyprop=true) ?(lax=false) env sigma c = let ty = Retyping.get_type_of ~polyprop ~lax env sigma c in refresh_universes (Some false) env sigma ty - - -(************************) -(* Unification results *) -(************************) - -type unification_result = - | Success of evar_map - | UnifFailure of evar_map * unification_error - -let is_success = function Success _ -> true | UnifFailure _ -> false - -let test_success conv_algo b env evd c c' rhs = - is_success (conv_algo b env evd c c' rhs) let add_conv_oriented_pb ?(tail=true) (pbty,env,t1,t2) evd = match pbty with @@ -174,7 +188,7 @@ let recheck_applications conv_algo env evdref t = if i < Array.length argsty then match EConstr.kind !evdref (whd_all env !evdref ty) with | Prod (na, dom, codom) -> - (match conv_algo true env !evdref Reduction.CUMUL argsty.(i) dom with + (match conv_algo TypeUnification env !evdref Reduction.CUMUL argsty.(i) dom with | Success evd -> evdref := evd; aux (succ i) (subst1 args.(i) codom) | UnifFailure (evd, reason) -> @@ -752,7 +766,7 @@ let check_evar_instance evd evk1 body conv_algo = try Retyping.get_type_of ~lax:true evenv evd body with Retyping.RetypeError _ -> user_err (Pp.(str "Ill-typed evar instance")) in - match conv_algo true evenv evd Reduction.CUMUL ty evi.evar_concl with + match conv_algo TypeUnification evenv evd Reduction.CUMUL ty evi.evar_concl with | Success evd -> evd | UnifFailure _ -> raise (IllTypedInstance (evenv,ty,evi.evar_concl)) @@ -1135,7 +1149,7 @@ let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs = let filter_compatible_candidates conv_algo env evd evi args rhs c = let c' = instantiate_evar_array evi c args in - match conv_algo false env evd Reduction.CONV rhs c' with + match conv_algo TermUnification env evd Reduction.CONV rhs c' with | Success evd -> Some (c,evd) | UnifFailure _ -> None @@ -1331,14 +1345,6 @@ let solve_evar_evar ?(force=false) flags f g env evd pbty (evk1,args1 as ev1) (e evd in solve_evar_evar_aux force flags f g env evd pbty ev1 ev2 -type types_or_terms = bool - -type conv_fun = - types_or_terms -> env -> evar_map -> conv_pb -> EConstr.constr -> EConstr.constr -> unification_result - -type conv_fun_bool = - types_or_terms -> env -> evar_map -> conv_pb -> EConstr.constr -> EConstr.constr -> bool - (* Solve pbs ?e[t1..tn] = ?e[u1..un] which arise often in fixpoint * definitions. We try to unify the ti with the ui pairwise. The pairs * that don't unify are discarded (i.e. ?e is redefined so that it does not @@ -1357,7 +1363,7 @@ let solve_refl ?(can_drop=false) flags conv_algo env evd pbty evk argsv1 argsv2 let args = Array.map2 (fun a1 a2 -> (a1, a2)) argsv1 argsv2 in let untypedfilter = restrict_upon_filter evd evk - (fun (a1,a2) -> conv_algo false env evd Reduction.CONV a1 a2) args in + (fun (a1,a2) -> conv_algo TermUnification env evd Reduction.CONV a1 a2) args in let candidates = filter_candidates evd evk untypedfilter NoUpdate in let filter = closure_of_filter evd evk untypedfilter in let evd,ev1 = restrict_applied_evar evd (evk,argsv1) filter candidates in @@ -1696,7 +1702,7 @@ let reconsider_unif_constraints conv_algo evd = (fun p (pbty,env,t1,t2 as x) -> match p with | Success evd -> - (match conv_algo true env evd pbty t1 t2 with + (match conv_algo TermUnification env evd pbty t1 t2 with | Success _ as x -> x | UnifFailure (i,e) -> UnifFailure (i,CannotSolveConstraint (x,e))) | UnifFailure _ as x -> x) diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 94f17de6cc..87804f01b6 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -40,15 +40,26 @@ val expand_vars_in_term : env -> evar_map -> constr -> constr some problems that cannot be solved in a unique way (except if choose is true); fails if the instance is not valid for the given [ev] *) -type types_or_terms = bool +(** One might want to use different conversion strategies for types and terms: + e.g. preventing delta reductions when doing term unifications but allowing + arbitrary delta conversion when checking the types of evar instances. *) -type conv_fun = types_or_terms -> +type unification_kind = + | TypeUnification + | TermUnification + +(** A unification function: parameterized by the kind of unification, + environment, sigma, conversion problem and the two terms to unify. *) +type unifier = unification_kind -> env -> evar_map -> conv_pb -> constr -> constr -> unification_result -type conv_fun_bool = types_or_terms -> +(** A conversion function: parameterized by the kind of unification, + environment, sigma, conversion problem and the two terms to convert. + Conversion is not allowed to instantiate evars contrary to unification. *) +type conversion_check = unification_kind -> env -> evar_map -> conv_pb -> constr -> constr -> bool -val evar_define : unify_flags -> conv_fun -> ?choose:bool -> ?imitate_defs:bool -> +val evar_define : unify_flags -> unifier -> ?choose:bool -> ?imitate_defs:bool -> env -> evar_map -> bool option -> existential -> constr -> evar_map val refresh_universes : @@ -60,18 +71,18 @@ val refresh_universes : bool option (* direction: true for levels lower than the existing levels *) -> env -> evar_map -> types -> evar_map * types -val solve_refl : ?can_drop:bool -> unify_flags -> conv_fun_bool -> env -> evar_map -> +val solve_refl : ?can_drop:bool -> unify_flags -> conversion_check -> env -> evar_map -> bool option -> Evar.t -> constr array -> constr array -> evar_map val solve_evar_evar : ?force:bool -> unify_flags -> (env -> evar_map -> bool option -> existential -> constr -> evar_map) -> - conv_fun -> + unifier -> env -> evar_map -> bool option -> existential -> existential -> evar_map -val solve_simple_eqn : unify_flags -> conv_fun -> ?choose:bool -> ?imitate_defs:bool -> env -> evar_map -> +val solve_simple_eqn : unify_flags -> unifier -> ?choose:bool -> ?imitate_defs:bool -> env -> evar_map -> bool option * existential * constr -> unification_result -val reconsider_unif_constraints : conv_fun -> evar_map -> unification_result +val reconsider_unif_constraints : unifier -> evar_map -> unification_result val is_unification_pattern_evar : env -> evar_map -> existential -> constr list -> constr -> alias list option @@ -87,7 +98,7 @@ exception IllTypedInstance of env * types * types (* May raise IllTypedInstance if types are not convertible *) val check_evar_instance : - evar_map -> Evar.t -> constr -> conv_fun -> evar_map + evar_map -> Evar.t -> constr -> unifier -> evar_map val remove_instance_local_defs : evar_map -> Evar.t -> 'a array -> 'a list -- cgit v1.2.3 From c002eae68ac12dc8ed92e906b346f73606e7fd69 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 15 Aug 2018 17:02:07 +0200 Subject: Flags of evar_conv_x/unifiers: rationalize --- pretyping/cases.ml | 3 +- pretyping/evarconv.ml | 56 +++++++++---------- pretyping/evarconv.mli | 4 +- pretyping/evarsolve.ml | 137 +++++++++++++++++++++++++---------------------- pretyping/evarsolve.mli | 41 +++++++------- pretyping/unification.ml | 2 +- 6 files changed, 125 insertions(+), 118 deletions(-) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 57725dbdc1..3b904570d4 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1709,8 +1709,7 @@ let abstract_tycon ?loc env sigma subst tycon extenv t = let sigma, ev' = Evarutil.new_evar ~src ~typeclass_candidate:false !!env sigma ty in begin let flags = (default_flags_of TransparentState.full) in - let conv = conv_fun evar_conv_x flags in - match solve_simple_eqn conv !!env sigma (None,ev,substl inst ev') with + match solve_simple_eqn evar_unify flags !!env sigma (None,ev,substl inst ev') with | Success evd -> evdref := evd | UnifFailure _ -> assert false end; diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 8f7c88b0db..29fdd1a44c 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -462,13 +462,13 @@ let rec evar_conv_x flags env evd pbty term1 term2 = in begin match EConstr.kind evd term1, EConstr.kind evd term2 with | Evar ev, _ when Evd.is_undefined evd (fst ev) && not (is_frozen flags ev) -> - (match solve_simple_eqn flags (conv_fun evar_conv_x flags) env evd + (match solve_simple_eqn (conv_fun evar_conv_x) flags env evd (position_problem true pbty,ev,term2) with | UnifFailure (_,OccurCheck _) -> (* Eta-expansion might apply *) default () | x -> x) | _, Evar ev when Evd.is_undefined evd (fst ev) && not (is_frozen flags ev) -> - (match solve_simple_eqn flags (conv_fun evar_conv_x flags) env evd + (match solve_simple_eqn (conv_fun evar_conv_x) flags env evd (position_problem false pbty,ev,term1) with | UnifFailure (_, OccurCheck _) -> (* Eta-expansion might apply *) default () @@ -487,7 +487,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty | Some l1' -> (* Miller-Pfenning's patterns unification *) let t2 = tM in let t2 = solve_pattern_eqn env evd l1' t2 in - solve_simple_eqn flags (conv_fun evar_conv_x flags) env evd + solve_simple_eqn (conv_fun evar_conv_x) flags env evd (position_problem on_left pbty,ev,t2) in let consume_stack on_left (termF,skF) (termO,skO) evd = @@ -668,7 +668,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty (* Note that ?ev1 and ?ev2, may have been instantiated in the meantime *) let ev1' = whd_evar i' t1 in if isEvar i' ev1' then - solve_simple_eqn flags (conv_fun evar_conv_x flags) env i' + solve_simple_eqn (conv_fun evar_conv_x) flags env i' (position_problem true pbty,destEvar i' ev1',term2) else evar_eqappr_x flags env evd pbty @@ -678,7 +678,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty (* we now unify r[?ev1] and ?ev2 *) let ev2' = whd_evar i' t2 in if isEvar i' ev2' then - solve_simple_eqn flags (conv_fun evar_conv_x flags) env i' + solve_simple_eqn (conv_fun evar_conv_x) flags env i' (position_problem false pbty,destEvar i' ev2',Stack.zip i' (term1,r)) else evar_eqappr_x flags env evd pbty @@ -689,7 +689,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty (* we now unify ?ev1 and r[?ev2] *) let ev1' = whd_evar i' t1 in if isEvar i' ev1' then - solve_simple_eqn flags (conv_fun evar_conv_x flags) env i' + solve_simple_eqn (conv_fun evar_conv_x) flags env i' (position_problem true pbty,destEvar i' ev1',Stack.zip i' (term2,r)) else evar_eqappr_x flags env evd pbty ((ev1', sk1), csts1) ((term2, sk2), csts2) @@ -737,13 +737,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty if Evar.equal sp1 sp2 then match ise_stack2 false env i (evar_conv_x flags) sk1 sk2 with |None, Success i' -> - Success (solve_refl flags (fun p env i pbty a1 a2 -> + Success (solve_refl (fun flags p env i pbty a1 a2 -> let flags = match p with | TypeUnification -> default_flags env | TermUnification -> flags in - is_success (evar_conv_x flags env i pbty a1 a2)) + is_success (evar_conv_x flags env i pbty a1 a2)) flags env i' (position_problem true pbty) sp1 al1 al2) |_, (UnifFailure _ as x) -> x |Some _, _ -> UnifFailure (i,NotSameArgSize) @@ -972,15 +972,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty if Evar.equal sp1 sp2 then match ise_stack2 false env evd (evar_conv_x flags) sk1 sk2 with |None, Success i' -> - (** FIXME: solve_refl can restrict the evar, do we want to allow that? *) - Success (solve_refl flags (fun p env i pbty a1 a2 -> - let flags = - match p with - | TypeUnification -> default_flags env - | TermUnification -> flags - in - is_success (evar_conv_x flags env i pbty a1 a2)) - env i' (position_problem true pbty) sp1 al1 al2) + ise_array2 i' (fun i' -> evar_conv_x flags env i' CONV) al1 al2 |_, (UnifFailure _ as x) -> x |Some _, _ -> UnifFailure (evd,NotSameArgSize) else UnifFailure (evd,NotSameHead) @@ -1106,6 +1098,8 @@ and eta_constructor flags env evd sk1 ((ind, i), u) sk2 term2 = let evar_conv_x flags = evar_conv_x flags +let evar_unify = conv_fun evar_conv_x + (* Profiling *) let evar_conv_x = if Flags.profile then @@ -1134,7 +1128,7 @@ let first_order_unification flags env evd (ev1,l1) (term2,l2) = evar_conv_x flags env i CONV t2 (mkEvar ev1) else solve_simple_eqn ~choose:true ~imitate_defs:false - flags (conv_fun evar_conv_x flags) env i (None,ev1,t2))] + evar_unify flags env i (None,ev1,t2))] let choose_less_dependent_instance evk evd term args = let evi = Evd.find_undefined evd evk in @@ -1424,11 +1418,11 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = if not (noccur_evar env_rhs evd ev (EConstr.of_constr t)) then raise (TypingFailed evd); let evd = Evd.define ev (EConstr.of_constr t) evd in - check_evar_instance evd ev (EConstr.of_constr t) (conv_fun evar_conv_x flags) + check_evar_instance evar_unify flags evd ev (EConstr.of_constr t) | Some l when abstract = Abstraction.Abstract && List.exists (fun c -> isVarId evd id (EConstr.of_constr c)) l -> let evd = Evd.define ev vid evd in - check_evar_instance evd ev vid (conv_fun evar_conv_x flags) + check_evar_instance evar_unify flags evd ev vid | _ -> evd) with e -> user_err (Pp.str "Cannot find an instance") else @@ -1474,8 +1468,8 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = evdref := evd; if !debug_ho_unification then Feedback.msg_debug Pp.(str"abstracted type: " ++ prc evenv (nf_evar !evdref rhs')); - Evarsolve.check_evar_instance !evdref evk rhs' - (conv_fun evar_conv_x (default_flags_of TransparentState.full)) + let flags = default_flags_of TransparentState.full in + Evarsolve.check_evar_instance evar_unify flags !evdref evk rhs' with IllTypedInstance _ -> raise (TypingFailed evd) in Evd.define evk rhs' evd in @@ -1554,19 +1548,20 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 = let reason = ProblemBeyondCapabilities in UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason))) | Evar (evk1,args1), Evar (evk2,args2) when Evar.equal evk1 evk2 -> - let f ontype env evd pbty x y = + let f flags ontype env evd pbty x y = let reds = match ontype with | TypeUnification -> full_transparent_state | TermUnification -> flags.open_ts in is_fconv ~reds pbty env evd x y in - Success (solve_refl ~can_drop:true flags f env evd + Success (solve_refl ~can_drop:true f flags env evd (position_problem true pbty) evk1 args1 args2) | Evar ev1, Evar ev2 when app_empty -> Success (solve_evar_evar ~force:true - flags (evar_define flags (conv_fun evar_conv_x flags) ~choose:true) (conv_fun evar_conv_x flags) env evd - (position_problem true pbty) ev1 ev2) + (evar_define evar_unify flags ~choose:true) + evar_unify flags env evd + (position_problem true pbty) ev1 ev2) | Evar ev1,_ when Array.length l1 <= Array.length l2 -> (* On "?n t1 .. tn = u u1 .. u(n+p)", try first-order unification *) (* and otherwise second-order matching *) @@ -1629,10 +1624,9 @@ let rec solve_unconstrained_evars_with_candidates flags evd = | a::l -> (* In case of variables, most recent ones come first *) try - let conv_algo = conv_fun evar_conv_x flags in - let evd = check_evar_instance evd evk a conv_algo in + let evd = check_evar_instance evar_unify flags evd evk a in let evd = Evd.define evk a evd in - match reconsider_unif_constraints conv_algo evd with + match reconsider_unif_constraints evar_unify flags evd with | Success evd -> solve_unconstrained_evars_with_candidates flags evd | UnifFailure _ -> aux l with @@ -1650,8 +1644,8 @@ let solve_unconstrained_impossible_cases env evd = let j, ctx = coq_unit_judge env in let evd' = Evd.merge_context_set Evd.univ_flexible_alg ?loc evd' ctx in let ty = j_type j in - let conv_algo = conv_fun evar_conv_x (default_flags env) in - let evd' = check_evar_instance evd' evk ty conv_algo in + let flags = default_flags env in + let evd' = check_evar_instance evar_unify flags evd' evk ty in Evd.define evk ty evd' | _ -> evd') evd evd diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index bd55b952a6..430dff2091 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -24,7 +24,7 @@ val default_flags_of : ?subterm_ts:transparent_state -> transparent_state -> uni type unify_fun = unify_flags -> env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result -val conv_fun : unify_fun -> unify_flags -> Evarsolve.unifier +val conv_fun : unify_fun -> Evarsolve.unifier exception UnableToUnify of evar_map * Pretype_errors.unification_error @@ -112,6 +112,8 @@ val set_evar_conv : unify_fun -> unit (** The default unification algorithm with evars and universes. *) val evar_conv_x : unify_fun +val evar_unify : Evarsolve.unifier + (**/**) (* For debugging *) val evar_eqappr_x : ?rhs_is_already_stuck:bool -> unify_flags -> diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 2ff52d1657..2d2db6a02b 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -47,18 +47,24 @@ type unification_result = let is_success = function Success _ -> true | UnifFailure _ -> false -let test_success conv_algo b env evd c c' rhs = - is_success (conv_algo b env evd c c' rhs) - -(** A unification function: parameterized by the kind of unification, - environment, sigma, conversion problem and the two terms to unify. *) -type unifier = unification_kind -> +let test_success unify flags b env evd c c' rhs = + is_success (unify flags b env evd c c' rhs) + +(** A unification function parameterized by: + - unification flags + - the kind of unification + - environment + - sigma + - conversion problem + - the two terms to unify. *) + +type unifier = unify_flags -> unification_kind -> env -> evar_map -> conv_pb -> constr -> constr -> unification_result (** A conversion function: parameterized by the kind of unification, environment, sigma, conversion problem and the two terms to convert. Conversion is not allowed to instantiate evars contrary to unification. *) -type conversion_check = unification_kind -> +type conversion_check = unify_flags -> unification_kind -> env -> evar_map -> conv_pb -> constr -> constr -> bool let normalize_evar evd ev = @@ -177,7 +183,7 @@ let add_conv_oriented_pb ?(tail=true) (pbty,env,t1,t2) evd = exception IllTypedInstance of env * EConstr.types * EConstr.types -let recheck_applications conv_algo env evdref t = +let recheck_applications unify flags env evdref t = let rec aux env t = match EConstr.kind !evdref t with | App (f, args) -> @@ -188,7 +194,7 @@ let recheck_applications conv_algo env evdref t = if i < Array.length argsty then match EConstr.kind !evdref (whd_all env !evdref ty) with | Prod (na, dom, codom) -> - (match conv_algo TypeUnification env !evdref Reduction.CUMUL argsty.(i) dom with + (match unify flags TypeUnification env !evdref Reduction.CUMUL argsty.(i) dom with | Success evd -> evdref := evd; aux (succ i) (subst1 args.(i) codom) | UnifFailure (evd, reason) -> @@ -757,7 +763,7 @@ let restrict_upon_filter evd evk p args = let len = Array.length args in Filter.restrict_upon oldfullfilter len (fun i -> p (Array.unsafe_get args i)) -let check_evar_instance evd evk1 body conv_algo = +let check_evar_instance unify flags evd evk1 body = let evi = Evd.find evd evk1 in let evenv = evar_env evi in (* FIXME: The body might be ill-typed when this is called from w_merge *) @@ -766,7 +772,7 @@ let check_evar_instance evd evk1 body conv_algo = try Retyping.get_type_of ~lax:true evenv evd body with Retyping.RetypeError _ -> user_err (Pp.(str "Ill-typed evar instance")) in - match conv_algo TypeUnification evenv evd Reduction.CUMUL ty evi.evar_concl with + match unify flags TypeUnification evenv evd Reduction.CUMUL ty evi.evar_concl with | Success evd -> evd | UnifFailure _ -> raise (IllTypedInstance (evenv,ty,evi.evar_concl)) @@ -905,13 +911,13 @@ let rec find_solution_type evarenv = function * pass [define] to [do_projection_effects] as a parameter. *) -let rec do_projection_effects conv_algo define_fun env ty evd = function +let rec do_projection_effects unify flags define_fun env ty evd = function | ProjectVar -> evd | ProjectEvar ((evk,argsv),evi,id,p) -> - let evd = check_evar_instance evd evk (mkVar id) conv_algo in + let evd = check_evar_instance unify flags evd evk (mkVar id) in let evd = Evd.define evk (EConstr.mkVar id) evd in (* TODO: simplify constraints involving evk *) - let evd = do_projection_effects conv_algo define_fun env ty evd p in + let evd = do_projection_effects unify flags define_fun env ty evd p in let ty = whd_all env evd (Lazy.force ty) in if not (isSort evd ty) then (* Don't try to instantiate if a sort because if evar_concl is an @@ -1147,9 +1153,9 @@ let postpone_non_unique_projection env evd pbty (evk,argsv as ev) sols rhs = * Note: argument f is the function used to instantiate evars. *) -let filter_compatible_candidates conv_algo env evd evi args rhs c = +let filter_compatible_candidates unify flags env evd evi args rhs c = let c' = instantiate_evar_array evi c args in - match conv_algo TermUnification env evd Reduction.CONV rhs c' with + match unify flags TermUnification env evd Reduction.CONV rhs c' with | Success evd -> Some (c,evd) | UnifFailure _ -> None @@ -1159,7 +1165,7 @@ let filter_compatible_candidates conv_algo env evd evi args rhs c = exception DoesNotPreserveCandidateRestriction -let restrict_candidates conv_algo env evd filter1 (evk1,argsv1) (evk2,argsv2) = +let restrict_candidates unify flags env evd filter1 (evk1,argsv1) (evk2,argsv2) = let evi1 = Evd.find evd evk1 in let evi2 = Evd.find evd evk2 in match evi1.evar_candidates, evi2.evar_candidates with @@ -1170,7 +1176,7 @@ let restrict_candidates conv_algo env evd filter1 (evk1,argsv1) (evk2,argsv2) = let l1' = List.filter (fun c1 -> let c1' = instantiate_evar_array evi1 c1 argsv1 in let filter c2 = - let compatibility = filter_compatible_candidates conv_algo env evd evi2 argsv2 c1' c2 in + let compatibility = filter_compatible_candidates unify flags env evd evi2 argsv2 c1' c2 in match compatibility with | None -> false | Some _ -> true @@ -1237,14 +1243,14 @@ exception EvarSolvedOnTheFly of evar_map * EConstr.constr (* Try to project evk1[argsv1] on evk2[argsv2], if [ev1] is a pattern on the common domain of definition *) -let project_evar_on_evar force g env evd aliases k2 pbty (evk1,argsv1 as ev1) (evk2,argsv2 as ev2) = +let project_evar_on_evar force unify flags env evd aliases k2 pbty (evk1,argsv1 as ev1) (evk2,argsv2 as ev2) = (* Apply filtering on ev1 so that fvs(ev1) are in fvs(ev2). *) let fvs2 = free_vars_and_rels_up_alias_expansion env evd aliases (mkEvar ev2) in let filter1 = restrict_upon_filter evd evk1 (has_constrainable_free_vars env evd aliases force k2 evk2 fvs2) argsv1 in let candidates1 = - try restrict_candidates g env evd filter1 ev1 ev2 + try restrict_candidates unify flags env evd filter1 ev1 ev2 with DoesNotPreserveCandidateRestriction -> let evd,ev1' = do_restrict_hyps evd ev1 filter1 NoUpdate in raise (CannotProject (evd,ev1')) in @@ -1268,16 +1274,16 @@ let update_evar_info ev1 ev2 evd = let evi = Evd.find evd ev2 in Evd.add evd ev2 {evi with evar_source = loc, evs1} -let solve_evar_evar_l2r force f g env evd aliases pbty ev1 (evk2,_ as ev2) = +let solve_evar_evar_l2r force f unify flags env evd aliases pbty ev1 (evk2,_ as ev2) = try - let evd,body = project_evar_on_evar force g env evd aliases 0 pbty ev1 ev2 in + let evd,body = project_evar_on_evar force unify flags env evd aliases 0 pbty ev1 ev2 in let evd' = Evd.define_with_evar evk2 body evd in let evd' = if is_obligation_evar evd evk2 then update_evar_info evk2 (fst (destEvar evd' body)) evd' else evd' in - check_evar_instance evd' evk2 body g + check_evar_instance unify flags evd' evk2 body with EvarSolvedOnTheFly (evd,c) -> f env evd pbty ev2 c @@ -1289,26 +1295,26 @@ let preferred_orientation evd evk1 evk2 = else true (** Precondition evk1 is not frozen, evk2 might be. *) -let solve_evar_evar_aux force flags f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) = +let solve_evar_evar_aux force f unify flags env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) = let aliases = make_alias_map env evd in let frozen_ev2 = Evar.Set.mem evk2 flags.frozen_evars in if preferred_orientation evd evk1 evk2 then - try solve_evar_evar_l2r force f g env evd aliases (opp_problem pbty) ev2 ev1 + try solve_evar_evar_l2r force f unify flags env evd aliases (opp_problem pbty) ev2 ev1 with CannotProject (evd,ev2) when not frozen_ev2 -> - try solve_evar_evar_l2r force f g env evd aliases pbty ev1 ev2 + try solve_evar_evar_l2r force f unify flags env evd aliases pbty ev1 ev2 with CannotProject (evd,ev1) -> add_conv_oriented_pb ~tail:true (pbty,env,mkEvar ev1,mkEvar ev2) evd else try if not frozen_ev2 then - solve_evar_evar_l2r force f g env evd aliases pbty ev1 ev2 + solve_evar_evar_l2r force f unify flags env evd aliases pbty ev1 ev2 else raise (CannotProject (evd,ev1)) with CannotProject (evd,ev1) -> - try solve_evar_evar_l2r force f g env evd aliases (opp_problem pbty) ev2 ev1 + try solve_evar_evar_l2r force f unify flags env evd aliases (opp_problem pbty) ev2 ev1 with CannotProject (evd,ev2) -> add_conv_oriented_pb ~tail:true (pbty,env,mkEvar ev1,mkEvar ev2) evd (** Precondition: evk1 is not frozen *) -let solve_evar_evar ?(force=false) flags f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) = +let solve_evar_evar ?(force=false) f unify flags env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) = let pbty = if force then None else pbty in let evi = Evd.find evd evk1 in let downcast evk t evd = downcast evk t evd in @@ -1343,14 +1349,14 @@ let solve_evar_evar ?(force=false) flags f g env evd pbty (evk1,args1 as ev1) (e downcast evk2 t2 (downcast evk1 t1 evd) with Reduction.NotArity -> evd in - solve_evar_evar_aux force flags f g env evd pbty ev1 ev2 + solve_evar_evar_aux force f unify flags env evd pbty ev1 ev2 (* Solve pbs ?e[t1..tn] = ?e[u1..un] which arise often in fixpoint * definitions. We try to unify the ti with the ui pairwise. The pairs * that don't unify are discarded (i.e. ?e is redefined so that it does not * depend on these args). *) -let solve_refl ?(can_drop=false) flags conv_algo env evd pbty evk argsv1 argsv2 = +let solve_refl ?(can_drop=false) unify flags env evd pbty evk argsv1 argsv2 = let evdref = ref evd in let eq_constr c1 c2 = match EConstr.eq_constr_universes env !evdref c1 c2 with | None -> false @@ -1363,19 +1369,19 @@ let solve_refl ?(can_drop=false) flags conv_algo env evd pbty evk argsv1 argsv2 let args = Array.map2 (fun a1 a2 -> (a1, a2)) argsv1 argsv2 in let untypedfilter = restrict_upon_filter evd evk - (fun (a1,a2) -> conv_algo TermUnification env evd Reduction.CONV a1 a2) args in + (fun (a1,a2) -> unify flags TermUnification env evd Reduction.CONV a1 a2) args in let candidates = filter_candidates evd evk untypedfilter NoUpdate in let filter = closure_of_filter evd evk untypedfilter in - let evd,ev1 = restrict_applied_evar evd (evk,argsv1) filter candidates in - if Evar.equal (fst ev1) evk && can_drop then (* No refinement *) evd else + let evd',ev1 = restrict_applied_evar evd (evk,argsv1) filter candidates in + if Evar.equal (fst ev1) evk && can_drop then (* No refinement *) evd' else (* either progress, or not allowed to drop, e.g. to preserve possibly *) (* informative equations such as ?e[x:=?y]=?e[x:=?y'] where we don't know *) (* if e can depend on x until ?y is not resolved, or, conversely, we *) (* don't know if ?y has to be unified with ?y, until e is resolved *) - let argsv2 = restrict_instance evd evk filter argsv2 in + let argsv2 = restrict_instance evd' evk filter argsv2 in let ev2 = (fst ev1,argsv2) in (* Leave a unification problem *) - add_conv_oriented_pb (pbty,env,mkEvar ev1,mkEvar ev2) evd + add_conv_oriented_pb (pbty,env,mkEvar ev1,mkEvar ev2) evd' (* If the evar can be instantiated by a finite set of candidates known in advance, we check which of them apply *) @@ -1383,14 +1389,14 @@ let solve_refl ?(can_drop=false) flags conv_algo env evd pbty evk argsv1 argsv2 exception NoCandidates exception IncompatibleCandidates -let solve_candidates conv_algo env evd (evk,argsv) rhs = +let solve_candidates unify flags env evd (evk,argsv) rhs = let evi = Evd.find evd evk in match evi.evar_candidates with | None -> raise NoCandidates | Some l -> let l' = List.map_filter - (fun c -> filter_compatible_candidates conv_algo env evd evi argsv rhs c) l in + (fun c -> filter_compatible_candidates unify flags env evd evi argsv rhs c) l in match l' with | [] -> raise IncompatibleCandidates | [c,evd] -> @@ -1398,7 +1404,7 @@ let solve_candidates conv_algo env evd (evk,argsv) rhs = (* time and the evar been solved by the filtering process *) if Evd.is_undefined evd evk then let evd' = Evd.define evk c evd in - check_evar_instance evd' evk c conv_algo + check_evar_instance unify flags evd' evk c else evd | l when List.length l < List.length l' -> let candidates = List.map fst l in @@ -1451,7 +1457,7 @@ exception NotEnoughInformationEvarEvar of EConstr.constr exception OccurCheckIn of evar_map * EConstr.constr exception MetaOccurInBodyInternal -let rec invert_definition flags conv_algo choose imitate_defs +let rec invert_definition unify flags choose imitate_defs env evd pbty (evk,argsv as ev) rhs = let aliases = make_alias_map env evd in let evdref = ref evd in @@ -1471,7 +1477,7 @@ let rec invert_definition flags conv_algo choose imitate_defs if choose then (mkVar id, p) else raise (NotUniqueInType sols) in let ty = lazy (Retyping.get_type_of env !evdref (of_alias t)) in - let evd = do_projection_effects conv_algo (evar_define flags conv_algo ~choose) env ty !evdref p in + let evd = do_projection_effects unify flags (evar_define unify flags ~choose) env ty !evdref p in evdref := evd; c with @@ -1484,7 +1490,7 @@ let rec invert_definition flags conv_algo choose imitate_defs let ty = find_solution_type (evar_filtered_env evi) sols in let ty' = instantiate_evar_array evi ty argsv in let (evd,evar,(evk',argsv' as ev')) = - materialize_evar (evar_define flags conv_algo ~choose) env !evdref 0 ev ty' in + materialize_evar (evar_define unify flags ~choose) env !evdref 0 ev ty' in let ts = expansions_of_var evd aliases t in let test c = isEvar evd c || List.exists (is_alias evd c) ts in let filter = restrict_upon_filter evd evk test argsv' in @@ -1525,7 +1531,7 @@ let rec invert_definition flags conv_algo choose imitate_defs let aliases = lift_aliases k aliases in (try let ev = (evk,Array.map (lift k) argsv) in - let evd,body = project_evar_on_evar false conv_algo env' !evdref aliases k None ev' ev in + let evd,body = project_evar_on_evar false unify flags env' !evdref aliases k None ev' ev in evdref := evd; body with @@ -1536,15 +1542,15 @@ let rec invert_definition flags conv_algo choose imitate_defs (* Make the virtual left evar real *) let ty = get_type_of env' evd t in let (evd,evar'',ev'') = - materialize_evar (evar_define flags conv_algo ~choose) env' evd k ev ty in + materialize_evar (evar_define unify flags ~choose) env' evd k ev ty in (* materialize_evar may instantiate ev' by another evar; adjust it *) let (evk',args' as ev') = normalize_evar evd ev' in let evd = (* Try to project (a restriction of) the left evar ... *) try - let evd,body = project_evar_on_evar false conv_algo env' evd aliases 0 None ev'' ev' in + let evd,body = project_evar_on_evar false unify flags env' evd aliases 0 None ev'' ev' in let evd = Evd.define evk' body evd in - check_evar_instance evd evk' body conv_algo + check_evar_instance unify flags evd evk' body with | EvarSolvedOnTheFly _ -> assert false (* ev has no candidates *) | CannotProject (evd,ev'') -> @@ -1581,7 +1587,7 @@ let rec invert_definition flags conv_algo choose imitate_defs | [x] -> x | _ -> let (evd,evar'',ev'') = - materialize_evar (evar_define flags conv_algo ~choose) env' !evdref k ev ty in + materialize_evar (evar_define unify flags ~choose) env' !evdref k ev ty in evdref := restrict_evar evd (fst ev'') None (UpdateWith candidates); evar'') | None -> @@ -1611,7 +1617,7 @@ let rec invert_definition flags conv_algo choose imitate_defs else let t' = imitate (env,0) rhs in if !progress then - (recheck_applications conv_algo (evar_env evi) evdref t'; t') + (recheck_applications unify flags (evar_env evi) evdref t'; t') else t' in (!evdref,body) @@ -1623,30 +1629,31 @@ let rec invert_definition flags conv_algo choose imitate_defs * ev is assumed not to be frozen. *) -and evar_define flags conv_algo ?(choose=false) ?(imitate_defs=true) env evd pbty (evk,argsv as ev) rhs = +and evar_define unify flags ?(choose=false) ?(imitate_defs=true) env evd pbty (evk,argsv as ev) rhs = match EConstr.kind evd rhs with | Evar (evk2,argsv2 as ev2) -> if Evar.equal evk evk2 then - solve_refl ~can_drop:choose flags - (test_success conv_algo) env evd pbty evk argsv argsv2 + solve_refl ~can_drop:choose + (test_success unify) flags env evd pbty evk argsv argsv2 else - solve_evar_evar ~force:choose flags - (evar_define flags conv_algo) conv_algo env evd pbty ev ev2 + solve_evar_evar ~force:choose + (evar_define unify flags) unify flags env evd pbty ev ev2 | _ -> - try solve_candidates conv_algo env evd ev rhs + try solve_candidates unify flags env evd ev rhs with NoCandidates -> try - let (evd',body) = invert_definition flags conv_algo choose imitate_defs env evd pbty ev rhs in + let (evd',body) = invert_definition unify flags choose imitate_defs env evd pbty ev rhs in if occur_meta evd' body then raise MetaOccurInBodyInternal; (* invert_definition may have instantiate some evars of rhs with evk *) (* so we recheck acyclicity *) if occur_evar_upto_types evd' evk body then raise (OccurCheckIn (evd',body)); (* needed only if an inferred type *) let evd', body = refresh_universes pbty env evd' body in - let evd' = Evd.define evk body evd' in - (** Check after definition, as checking could involve the same - evar definition problem again otherwise *) - check_evar_instance evd' evk body conv_algo + (** Check instance freezing the evar to be defined, as + checking could involve the same evar definition problem again otherwise *) + let flags = { flags with frozen_evars = Evar.Set.add evk flags.frozen_evars } in + let evd' = check_evar_instance unify flags evd' evk body in + Evd.define evk body evd' with | NotEnoughInformationToProgress sols -> postpone_non_unique_projection env evd pbty ev sols rhs @@ -1661,7 +1668,7 @@ and evar_define flags conv_algo ?(choose=false) ?(imitate_defs=true) env evd pbt let c = whd_all env evd rhs in match EConstr.kind evd c with | Evar (evk',argsv2) when Evar.equal evk evk' -> - solve_refl flags (fun _b env sigma pb c c' -> is_fconv pb env sigma c c') + solve_refl (fun flags _b env sigma pb c c' -> is_fconv pb env sigma c c') flags env evd pbty evk argsv argsv2 | _ -> raise (OccurCheckIn (evd,rhs)) @@ -1696,13 +1703,13 @@ let status_changed evd lev (pbty,_,t1,t2) = (try Evar.Set.mem (head_evar evd t1) lev with NoHeadEvar -> false) || (try Evar.Set.mem (head_evar evd t2) lev with NoHeadEvar -> false) -let reconsider_unif_constraints conv_algo evd = +let reconsider_unif_constraints unify flags evd = let (evd,pbs) = extract_changed_conv_pbs evd (status_changed evd) in List.fold_left (fun p (pbty,env,t1,t2 as x) -> match p with | Success evd -> - (match conv_algo TermUnification env evd pbty t1 t2 with + (match unify flags TermUnification env evd pbty t1 t2 with | Success _ as x -> x | UnifFailure (i,e) -> UnifFailure (i,CannotSolveConstraint (x,e))) | UnifFailure _ as x -> x) @@ -1715,12 +1722,12 @@ let reconsider_unif_constraints conv_algo evd = * if the problem couldn't be solved. *) (* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *) -let solve_simple_eqn flags conv_algo ?(choose=false) ?(imitate_defs=true) +let solve_simple_eqn unify flags ?(choose=false) ?(imitate_defs=true) env evd (pbty,(evk1,args1 as ev1),t2) = try let t2 = whd_betaiota evd t2 in (* includes whd_evar *) - let evd = evar_define flags conv_algo ~choose ~imitate_defs env evd pbty ev1 t2 in - reconsider_unif_constraints conv_algo evd + let evd = evar_define unify flags ~choose ~imitate_defs env evd pbty ev1 t2 in + reconsider_unif_constraints unify flags evd with | NotInvertibleUsingOurAlgorithm t -> UnifFailure (evd,NotClean (ev1,env,t)) diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 87804f01b6..810796457f 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -35,11 +35,6 @@ val is_success : unification_result -> bool their representative that is most ancient in the context *) val expand_vars_in_term : env -> evar_map -> constr -> constr -(** [evar_define choose env ev c] try to instantiate [ev] with [c] (typed in [env]), - possibly solving related unification problems, possibly leaving open - some problems that cannot be solved in a unique way (except if choose is - true); fails if the instance is not valid for the given [ev] *) - (** One might want to use different conversion strategies for types and terms: e.g. preventing delta reductions when doing term unifications but allowing arbitrary delta conversion when checking the types of evar instances. *) @@ -48,18 +43,28 @@ type unification_kind = | TypeUnification | TermUnification -(** A unification function: parameterized by the kind of unification, - environment, sigma, conversion problem and the two terms to unify. *) -type unifier = unification_kind -> +(** A unification function parameterized by: + - unification flags + - the kind of unification + - environment + - sigma + - conversion problem + - the two terms to unify. *) +type unifier = unify_flags -> unification_kind -> env -> evar_map -> conv_pb -> constr -> constr -> unification_result (** A conversion function: parameterized by the kind of unification, environment, sigma, conversion problem and the two terms to convert. Conversion is not allowed to instantiate evars contrary to unification. *) -type conversion_check = unification_kind -> - env -> evar_map -> conv_pb -> constr -> constr -> bool +type conversion_check = unify_flags -> unification_kind -> + env -> evar_map -> conv_pb -> constr -> constr -> bool + +(** [evar_define choose env ev c] try to instantiate [ev] with [c] (typed in [env]), + possibly solving related unification problems, possibly leaving open + some problems that cannot be solved in a unique way (except if choose is + true); fails if the instance is not valid for the given [ev] *) -val evar_define : unify_flags -> unifier -> ?choose:bool -> ?imitate_defs:bool -> +val evar_define : unifier -> unify_flags -> ?choose:bool -> ?imitate_defs:bool -> env -> evar_map -> bool option -> existential -> constr -> evar_map val refresh_universes : @@ -71,18 +76,18 @@ val refresh_universes : bool option (* direction: true for levels lower than the existing levels *) -> env -> evar_map -> types -> evar_map * types -val solve_refl : ?can_drop:bool -> unify_flags -> conversion_check -> env -> evar_map -> +val solve_refl : ?can_drop:bool -> conversion_check -> unify_flags -> env -> evar_map -> bool option -> Evar.t -> constr array -> constr array -> evar_map -val solve_evar_evar : ?force:bool -> unify_flags -> +val solve_evar_evar : ?force:bool -> (env -> evar_map -> bool option -> existential -> constr -> evar_map) -> - unifier -> + unifier -> unify_flags -> env -> evar_map -> bool option -> existential -> existential -> evar_map -val solve_simple_eqn : unify_flags -> unifier -> ?choose:bool -> ?imitate_defs:bool -> env -> evar_map -> +val solve_simple_eqn : unifier -> unify_flags -> ?choose:bool -> ?imitate_defs:bool -> env -> evar_map -> bool option * existential * constr -> unification_result -val reconsider_unif_constraints : unifier -> evar_map -> unification_result +val reconsider_unif_constraints : unifier -> unify_flags -> evar_map -> unification_result val is_unification_pattern_evar : env -> evar_map -> existential -> constr list -> constr -> alias list option @@ -97,8 +102,8 @@ val noccur_evar : env -> evar_map -> Evar.t -> constr -> bool exception IllTypedInstance of env * types * types (* May raise IllTypedInstance if types are not convertible *) -val check_evar_instance : - evar_map -> Evar.t -> constr -> unifier -> evar_map +val check_evar_instance : unifier -> unify_flags -> + evar_map -> Evar.t -> constr -> evar_map val remove_instance_local_defs : evar_map -> Evar.t -> 'a array -> 'a list diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 486aa38558..3de8c381d0 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1325,7 +1325,7 @@ let order_metas metas = (* Solve an equation ?n[x1=u1..xn=un] = t where ?n is an evar *) let solve_simple_evar_eqn flags env evd ev rhs = - match solve_simple_eqn flags (Evarconv.conv_fun Evarconv.evar_conv_x flags) env evd (None,ev,rhs) with + match solve_simple_eqn Evarconv.evar_unify flags env evd (None,ev,rhs) with | UnifFailure (evd,reason) -> error_cannot_unify env evd ~reason (mkEvar ev,rhs); | Success evd -> evd -- cgit v1.2.3 From acc4f5922dcc1f92f3dc3db653b7608949b60c2b Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 15 Aug 2018 17:29:53 +0200 Subject: Add an helper [instantiate_evar] function It does checking of evar instance and Evd.define, assuming an occur-check has already been performed. --- pretyping/evarconv.ml | 124 +++++++++++++++++++++++------------------------- pretyping/evarsolve.ml | 13 +++-- pretyping/evarsolve.mli | 12 +++++ 3 files changed, 80 insertions(+), 69 deletions(-) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 29fdd1a44c..fb649598df 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -420,7 +420,10 @@ let compare_cumulative_instances evd variances u u' = let conv_fun f flags on_types = let typefn env evd pbty term1 term2 = - f { (default_flags env) with with_cs = flags.with_cs } env evd pbty term1 term2 + let flags = { (default_flags env) with + with_cs = flags.with_cs; + frozen_evars = flags.frozen_evars } + in f flags env evd pbty term1 term2 in let termfn env evd pbty term1 term2 = f flags env evd pbty term1 term2 @@ -1397,50 +1400,45 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = Feedback.msg_debug Pp.(str"abstracting: " ++ prc env_rhs (mkVar id) ++ spc () ++ prc env_rhs c); - let rec force_instantiation evd = function - | (evk,evty,inst,abstract)::evs -> - let evk = Option.default evk (Evarutil.advance evd evk) in - let evd = - if is_undefined evd evk then - (* We try abstraction or concretisation for *) - (* this unconstrained occurrence *) - (* and we use typing to propagate this instantiation *) - (* We avoid making an arbitrary choice by leaving candidates *) - (* if both can work *) - let evi = Evd.find_undefined evd evk in - let vid = mkVar id in - let candidates = [inst; vid] in - try - let evd, ev = Evarutil.restrict_evar evd evk (Evd.evar_filter evi) (Some candidates) in - let evi = Evd.find evd ev in - (match evar_candidates evi with - | Some [t] -> - if not (noccur_evar env_rhs evd ev (EConstr.of_constr t)) then - raise (TypingFailed evd); - let evd = Evd.define ev (EConstr.of_constr t) evd in - check_evar_instance evar_unify flags evd ev (EConstr.of_constr t) - | Some l when abstract = Abstraction.Abstract && - List.exists (fun c -> isVarId evd id (EConstr.of_constr c)) l -> - let evd = Evd.define ev vid evd in - check_evar_instance evar_unify flags evd ev vid - | _ -> evd) - with e -> user_err (Pp.str "Cannot find an instance") - else - ((if !debug_ho_unification then - let evi = Evd.find evd evk in - let env = Evd.evar_env evi in - Feedback.msg_debug Pp.(str"evar is defined: " ++ - int (Evar.repr evk) ++ spc () ++ - prc env (match evar_body evi with Evar_defined c -> c - | Evar_empty -> assert false))); - evd) - in - force_instantiation evd evs - | [] -> - abstract_free_holes evd l - in - force_instantiation evd !evsref - | [] -> + let rec force_instantiation evd = function + | (evk,evty,inst,abstract)::evs -> + let evk = Option.default evk (Evarutil.advance evd evk) in + let evd = + if is_undefined evd evk then + (* We try abstraction or concretisation for *) + (* this unconstrained occurrence *) + (* and we use typing to propagate this instantiation *) + (* We avoid making an arbitrary choice by leaving candidates *) + (* if both can work *) + let evi = Evd.find_undefined evd evk in + let vid = mkVar id in + let candidates = [inst; vid] in + try + let evd, ev = Evarutil.restrict_evar evd evk (Evd.evar_filter evi) (Some candidates) in + let evi = Evd.find evd ev in + (match evar_candidates evi with + | Some [t] -> + if not (noccur_evar env_rhs evd ev (EConstr.of_constr t)) then + raise (TypingFailed evd); + instantiate_evar evar_unify flags evd ev (EConstr.of_constr t) + | Some l when abstract = Abstraction.Abstract && + List.exists (fun c -> isVarId evd id (EConstr.of_constr c)) l -> + instantiate_evar evar_unify flags evd ev vid + | _ -> evd) + with e -> user_err (Pp.str "Cannot find an instance") + else + ((if !debug_ho_unification then + let evi = Evd.find evd evk in + let env = Evd.evar_env evi in + Feedback.msg_debug Pp.(str"evar is defined: " ++ + int (Evar.repr evk) ++ spc () ++ + prc env (match evar_body evi with Evar_defined c -> c + | Evar_empty -> assert false))); + evd) + in force_instantiation evd evs + | [] -> abstract_free_holes evd l + in force_instantiation evd !evsref + | [] -> if Evd.is_defined evd evk then (** Can happen due to dependencies: instantiating evars in the arguments of evk might instantiate evk itself. *) @@ -1453,25 +1451,23 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = end; evd) else - let evd = - try - let evi = Evd.find_undefined evd evk in - let evenv = evar_env evi in - let evdref = ref evd in - let rhs' = nf_evar !evdref rhs' in + try + let evi = Evd.find_undefined evd evk in + let evenv = evar_env evi in + let evdref = ref evd in + let rhs' = nf_evar !evdref rhs' in if !debug_ho_unification then Feedback.msg_debug Pp.(str"abstracted type before second solve_evars: " ++ prc evenv rhs'); - (** solve_evars is not commuting with nf_evar, because restricting - an evar might provide a more specific type. *) - let evd, _ = !solve_evars evenv evd rhs' in - evdref := evd; - if !debug_ho_unification then - Feedback.msg_debug Pp.(str"abstracted type: " ++ prc evenv (nf_evar !evdref rhs')); - let flags = default_flags_of TransparentState.full in - Evarsolve.check_evar_instance evar_unify flags !evdref evk rhs' + (** solve_evars is not commuting with nf_evar, because restricting + an evar might provide a more specific type. *) + let evd, _ = !solve_evars evenv evd rhs' in + evdref := evd; + if !debug_ho_unification then + Feedback.msg_debug Pp.(str"abstracted type: " ++ prc evenv (nf_evar !evdref rhs')); + let flags = default_flags_of TransparentState.full in + Evarsolve.instantiate_evar evar_unify flags !evdref evk rhs' with IllTypedInstance _ -> raise (TypingFailed evd) - in Evd.define evk rhs' evd in let evd = abstract_free_holes evd subst in evd, true @@ -1484,6 +1480,8 @@ let default_evar_selection flags evd (ev,args) = | _ :: args, a :: abs -> let spec = if not flags.allow_K_at_toplevel then + (* [evar_absorb_arguments] puts an Abstract flag for the + toplevel binders that were absorbed. *) let occs = if a == Abstraction.Abstract then Locus.AtLeastOneOccurrence else Locus.AllOccurrences @@ -1624,8 +1622,7 @@ let rec solve_unconstrained_evars_with_candidates flags evd = | a::l -> (* In case of variables, most recent ones come first *) try - let evd = check_evar_instance evar_unify flags evd evk a in - let evd = Evd.define evk a evd in + let evd = instantiate_evar evar_unify flags evd evk a in match reconsider_unif_constraints evar_unify flags evd with | Success evd -> solve_unconstrained_evars_with_candidates flags evd | UnifFailure _ -> aux l @@ -1645,8 +1642,7 @@ let solve_unconstrained_impossible_cases env evd = let evd' = Evd.merge_context_set Evd.univ_flexible_alg ?loc evd' ctx in let ty = j_type j in let flags = default_flags env in - let evd' = check_evar_instance evar_unify flags evd' evk ty in - Evd.define evk ty evd' + instantiate_evar evar_unify flags evd' evk ty | _ -> evd') evd evd let solve_unif_constraints_with_heuristics env diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 2d2db6a02b..ffb083e768 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1428,6 +1428,13 @@ let occur_evar_upto_types sigma n c = in try occur_rec c; false with Occur -> true +let instantiate_evar unify flags evd evk body = + (** Check instance freezing the evar to be defined, as + checking could involve the same evar definition problem again otherwise *) + let flags = { flags with frozen_evars = Evar.Set.add evk flags.frozen_evars } in + let evd' = check_evar_instance unify flags evd evk body in + Evd.define evk body evd' + (* We try to instantiate the evar assuming the body won't depend * on arguments that are not Rels or Vars, or appearing several times * (i.e. we tackle a generalization of Miller-Pfenning patterns unification) @@ -1649,11 +1656,7 @@ and evar_define unify flags ?(choose=false) ?(imitate_defs=true) env evd pbty (e if occur_evar_upto_types evd' evk body then raise (OccurCheckIn (evd',body)); (* needed only if an inferred type *) let evd', body = refresh_universes pbty env evd' body in - (** Check instance freezing the evar to be defined, as - checking could involve the same evar definition problem again otherwise *) - let flags = { flags with frozen_evars = Evar.Set.add evk flags.frozen_evars } in - let evd' = check_evar_instance unify flags evd' evk body in - Evd.define evk body evd' + instantiate_evar unify flags evd' evk body with | NotEnoughInformationToProgress sols -> postpone_non_unique_projection env evd pbty ev sols rhs diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 810796457f..dfadb4aaea 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -59,6 +59,17 @@ type unifier = unify_flags -> unification_kind -> type conversion_check = unify_flags -> unification_kind -> env -> evar_map -> conv_pb -> constr -> constr -> bool +(** [instantiate_evar unify flags env sigma ev c] defines the evar [ev] with [c], + checking that the type of [c] is unifiable with [ev]'s declared type first. + + Preconditions: + - [ev] does not occur in [c]. + - [c] does not contain any Meta(_) + *) + +val instantiate_evar : unifier -> unify_flags -> evar_map -> + Evar.t -> constr -> evar_map + (** [evar_define choose env ev c] try to instantiate [ev] with [c] (typed in [env]), possibly solving related unification problems, possibly leaving open some problems that cannot be solved in a unique way (except if choose is @@ -67,6 +78,7 @@ type conversion_check = unify_flags -> unification_kind -> val evar_define : unifier -> unify_flags -> ?choose:bool -> ?imitate_defs:bool -> env -> evar_map -> bool option -> existential -> constr -> evar_map + val refresh_universes : ?status:Evd.rigid -> ?onlyalg:bool (* Only algebraic universes *) -> -- cgit v1.2.3 From 8a5cd826ee8d7d51c85c834c28f090466dda33a5 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 15 Aug 2018 20:14:57 +0200 Subject: [occur_rigidly] Try improving occur-check approximation The code is cleaner and more self-explanatory this way. --- pretyping/evarconv.ml | 71 +++++++++++++++++++++++++++++++++++++------------- pretyping/evarconv.mli | 3 +++ 2 files changed, 56 insertions(+), 18 deletions(-) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index fb649598df..96d7cff152 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -154,7 +154,7 @@ let position_problem l2r = function | CUMUL -> Some l2r (* [occur_rigidly ev evd t] tests if the evar ev occurs in a rigid - context in t. Precondition: t has a rigid head. + context in t. Precondition: t has a rigid head and is not reducible. That function is an under approximation of occur-check, it can return false even if the occur-check would succeed on the normal form. This @@ -162,34 +162,69 @@ let position_problem l2r = function result in an occur-check after reductions. If it returns true, we know that the occur-check would also return true on the normal form. - The boolean indicates if the term is a rigid head. For applications, - this means than an occurrence of the evar in arguments should be looked - at to find an occur-check. *) + [t] is assumed to have a rigid head, which can + appear under a elimination context (e.g. application, match or projection). + + In the inner recursive function, the result indicates if the term is + rigid (irreducible), normal (succession of constructors) or + potentially reducible. For applications, this means than an + occurrence of the evar in arguments should be looked at to find an + occur-check if the head is rigid or normal. For inductive + eliminations, only an occurrence in a rigid context of the + discriminee counts as a rigid occurrence overall, not a normal + occurrence which might disappear after reduction. *) + +type result = Rigid of bool | Normal of bool | Reducible + +let rigid_normal_occ = function Rigid b -> b | Normal b -> b | _ -> false let occur_rigidly flags env evd (evk,_) t = let rec aux t = match EConstr.kind evd t with - | App (f, c) -> if aux f then (Array.iter (fun x -> ignore (aux x)) c; true) else false - | Construct _ | Ind _ | Sort _ -> true + | App (f, c) -> + (match aux f with + | Rigid b -> Rigid (b || Array.exists (fun x -> rigid_normal_occ (aux x)) c) + | Normal b -> Normal (b || Array.exists (fun x -> rigid_normal_occ (aux x)) c) + | Reducible -> Reducible) + | Construct _ -> Normal false + | Ind _ | Sort _ -> Rigid false | Proj (p, c) -> let cst = Projection.constant p in - if not (is_transparent_constant flags.open_ts cst) then - (ignore (aux c); true) - else false + let rigid = not (is_transparent_constant flags.open_ts cst) in + if rigid then aux c + else (* if the evar appears rigidly in c then this elimination + cannot reduce and we have a rigid occurrence, otherwise + we don't know. *) + (match aux c with + | Rigid _ as res -> res + | Normal b -> Reducible + | Reducible -> Reducible) | Evar (evk',l as ev) -> - if Evar.equal evk evk' then raise Occur + if Evar.equal evk evk' then Rigid true else if is_frozen flags ev then - (Array.iter (fun x -> ignore (aux x)) l; true) - else false + Rigid (Array.exists (fun x -> rigid_normal_occ (aux x)) l) + else Reducible | Cast (p, _, _) -> aux p | Lambda (na, t, b) -> aux b | LetIn (na, _, _, b) -> aux b - | Const (c,_) -> not (is_transparent_constant flags.open_ts c) - | Prod (_, b, t) -> ignore(aux b || aux t); true - | Rel _ | Var _ -> false - | Case (_,_,c,_) -> if isEvar evd c && occur_evar evd evk c then raise Occur else false - | Meta _ | Fix _ | CoFix _ | Int _ -> false - in try ignore(aux t); false with Occur -> true + | Const (c,_) -> + if is_transparent_constant flags.open_ts c then Reducible + else Rigid false + | Prod (_, b, t) -> + let b' = aux b and t' = aux t in + if rigid_normal_occ b' || rigid_normal_occ t' then Rigid true + else Reducible + | Rel _ | Var _ -> Reducible + | Case (_,_,c,_) -> + (match aux c with + | Rigid b -> Rigid b + | _ -> Reducible) + | Meta _ | Fix _ | CoFix _ | Int _ -> Reducible + in + match aux t with + | Rigid b -> b + | Normal b -> b + | Reducible -> false (* [check_conv_record env sigma (t1,stack1) (t2,stack2)] tries to decompose the problem (t1 stack1) = (t2 stack2) into a problem diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 430dff2091..fa6f3466f6 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -120,6 +120,9 @@ val evar_eqappr_x : ?rhs_is_already_stuck:bool -> unify_flags -> env -> evar_map -> conv_pb -> state * Cst_stack.t -> state * Cst_stack.t -> Evarsolve.unification_result + +val occur_rigidly : Evarsolve.unify_flags -> + 'a -> Evd.evar_map -> Evar.t * 'b -> EConstr.t -> bool (**/**) (** {6 Functions to deal with impossible cases } *) -- cgit v1.2.3 From 66892881c69cfb91fe1cd772cd88ac2c73c99bbe Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 17 Oct 2018 17:10:32 +0200 Subject: Fix warning unused variable --- pretyping/evarconv.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 96d7cff152..7b510cfd5c 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -768,7 +768,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty Feedback.msg_notice (v 0 (pr_state env evd appr1 ++ cut () ++ pr_state env evd appr2 ++ cut ())) in match (flex_kind_of_term flags env evd term1 sk1, flex_kind_of_term flags env evd term2 sk2) with - | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) -> + | Flexible (sp1,al1), Flexible (sp2,al2) -> (* sk1[?ev1] =? sk2[?ev2] *) let f1 i = first_order env i term1 term2 sk1 sk2 and f2 i = -- cgit v1.2.3 From 1c60cbedfd8a5e64bfa95dfb9a9497e278458c30 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 17 Oct 2018 17:10:48 +0200 Subject: print_constr_env moved to Internal module --- pretyping/evarconv.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 7b510cfd5c..28dd63cfcc 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1201,7 +1201,7 @@ let default_occurrences_selection ?(frozen_evars=Evar.Set.empty) ts n = let apply_on_subterm env evdref fixedref f test c t = let test = test env !evdref c in - let prc env = print_constr_env env !evdref in + let prc env = Termops.Internal.print_constr_env env !evdref in let rec applyrec (env,(k,c) as acc) t = if Evar.Set.exists (fun fixed -> occur_evar !evdref fixed t) !fixedref then match EConstr.kind !evdref t with @@ -1323,8 +1323,8 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = let sign = named_context_val env_evar in let ctxt = evar_filtered_context evi in if !debug_ho_unification then - (Feedback.msg_debug Pp.(str"env rhs: " ++ print_env env_rhs); - Feedback.msg_debug Pp.(str"env evars: " ++ print_env env_evar)); + (Feedback.msg_debug Pp.(str"env rhs: " ++ Termops.Internal.print_env env_rhs); + Feedback.msg_debug Pp.(str"env evars: " ++ Termops.Internal.print_env env_evar)); let args = Array.map (nf_evar evd) args in let vars = List.map NamedDecl.get_id ctxt in let argsubst = List.map2 (fun id c -> (id, c)) vars (Array.to_list args) in @@ -1335,7 +1335,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = the solution we are trying to build here by adding the problem as a constraint. *) let evd = Evarutil.add_unification_pb (CONV,env_rhs,mkEvar (evk,args),rhs) evd in let evdref = ref evd in - let prc env c = print_constr_env env !evdref c in + let prc env c = Termops.Internal.print_constr_env env !evdref c in let rec make_subst = function | decl'::ctxt', c::l, occs::occsl when isVarId evd (NamedDecl.get_id decl') c -> begin match occs with -- cgit v1.2.3 From 78b51f541d0107f06c21fc1260aae2ab9f7229c5 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 17 Oct 2018 18:04:35 +0200 Subject: Change interfaces of evarconv as suggested by Enrico. Now the main functions are unify (solves the problems entirely) and unify_delay and unify_leq (which might leave some unsolved constraints). Deprecated the_conv_x and the_conv_x_leq (which were misnommers as they do unification not conversion). --- plugins/funind/functional_principles_proofs.ml | 4 +- plugins/ltac/rewrite.ml | 2 +- plugins/ssrmatching/ssrmatching.ml | 2 +- pretyping/cases.ml | 24 +++++------ pretyping/coercion.ml | 18 ++++----- pretyping/evarconv.ml | 56 ++++++++++++++------------ pretyping/evarconv.mli | 46 ++++++++++++++------- pretyping/pretyping.ml | 20 ++++----- pretyping/typing.ml | 42 +++++++++---------- tactics/class_tactics.ml | 5 ++- tactics/equality.ml | 13 +++--- tactics/tactics.ml | 10 +++-- 12 files changed, 133 insertions(+), 109 deletions(-) diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 8da30bd9c9..6fd2f7c2bc 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -238,7 +238,9 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type = raise NoChange; end in - let eq_constr c1 c2 = Option.has_some (Evarconv.conv env sigma c1 c2) in + let eq_constr c1 c2 = + try ignore(Evarconv.unify_delay env sigma c1 c2); true + with Evarconv.UnableToUnify _ -> false in if not (noccurn sigma 1 end_of_type) then nochange "dependent"; (* if end_of_type depends on this term we don't touch it *) if not (isApp sigma t) then nochange "not an equality"; diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 2055b25ff4..ea54973fdc 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -449,7 +449,7 @@ let evd_convertible env evd x y = unsolvable constraints remain, so we check that this unification does not introduce any new problem. *) let _, pbs = Evd.extract_all_conv_pbs evd in - let evd' = Evarconv.the_conv_x env x y evd in + let evd' = Evarconv.unify_delay env evd x y in let _, pbs' = Evd.extract_all_conv_pbs evd' in if evd' == evd || problem_inclusion pbs' pbs then Some evd' else None diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 552a4048b1..fb99b87108 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -213,7 +213,7 @@ let unif_EQ_args env sigma pa a = loop 0 let unif_HO env ise p c = - try Evarconv.the_conv_x env p c ise + try Evarconv.unify_delay env ise p c with Evarconv.UnableToUnify(ise, err) -> raise Pretype_errors.(PretypeError(env,ise,CannotUnify(p,c,Some err))) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 3b904570d4..3a0e69788a 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -321,9 +321,9 @@ let inh_coerce_to_ind env sigma0 loc ty tyi = constructor and renounce if not able to give more information *) (* devrait être indifférent d'exiger leq ou pas puisque pour un inductif cela doit être égal *) - match cumul env sigma expected_typ ty with - | Some sigma -> sigma - | None -> sigma0 + match Evarconv.unify_leq_delay env sigma expected_typ ty with + | sigma -> sigma + | exception Evarconv.UnableToUnify _ -> sigma0 let binding_vars_of_inductive sigma = function | NotInd _ -> [] @@ -431,9 +431,9 @@ let adjust_tomatch_to_pattern ~program_mode sigma pb ((current,typ),deps,dep) = let sigma, current = if List.is_empty deps && isEvar sigma typ then (* Don't insert coercions if dependent; only solve evars *) - match cumul !!(pb.env) sigma indt typ with - | None -> sigma, current - | Some sigma -> sigma, current + match Evarconv.unify_leq_delay !!(pb.env) sigma indt typ with + | exception Evarconv.UnableToUnify _ -> sigma, current + | sigma -> sigma, current else let sigma, j = Coercion.inh_conv_coerce_to ~program_mode true !!(pb.env) sigma (make_judge current typ) indt in sigma, j.uj_val @@ -1767,9 +1767,9 @@ let build_tycon ?loc env tycon_env s subst tycon extenv sigma t = let sigma, t = abstract_tycon ?loc tycon_env sigma subst tycon extenv t in let sigma, tt = Typing.type_of !!extenv sigma t in (sigma, t, tt) in - match cumul !!env sigma tt (mkSort s) with - | None -> anomaly (Pp.str "Build_tycon: should be a type."); - | Some sigma -> + match unify_leq_delay !!env sigma tt (mkSort s) with + | exception Evarconv.UnableToUnify _ -> anomaly (Pp.str "Build_tycon: should be a type."); + | sigma -> sigma, { uj_val = t; uj_type = tt } (* For a multiple pattern-matching problem Xi on t1..tn with return @@ -2190,15 +2190,15 @@ let constr_of_pat env sigma arsign pat avoid = let sigma, sign, i, avoid = try let env = EConstr.push_rel_context sign env in - let sigma = the_conv_x_leq (EConstr.push_rel_context sign env) - (lift (succ m) ty) (lift 1 apptype) sigma in + let sigma = unify_leq_delay (EConstr.push_rel_context sign env) sigma + (lift (succ m) ty) (lift 1 apptype) in let sigma, eq_t = mk_eq sigma (lift (succ m) ty) (mkRel 1) (* alias *) (lift 1 app) (* aliased term *) in let neq = eq_id avoid id in sigma, LocalDef (Name neq, mkRel 0, eq_t) :: sign, 2, Id.Set.add neq avoid - with Reduction.NotConvertible -> sigma, sign, 1, avoid + with Evarconv.UnableToUnify _ -> sigma, sign, 1, avoid in (* Mark the equality as a hole *) sigma, pat', sign, lift i app, lift i apptype, realargs, n + i, avoid diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index a8bcec10e8..0adf9365cf 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -64,9 +64,9 @@ let apply_coercion_args env sigma check isproj argl funj = | Prod (_,c1,c2) -> let sigma = if check then - begin match cumul env sigma (Retyping.get_type_of env sigma h) c1 with - | None -> raise NoCoercion - | Some sigma -> sigma + begin match Evarconv.unify_leq_delay env sigma (Retyping.get_type_of env sigma h) c1 with + | exception Evarconv.UnableToUnify _ -> raise NoCoercion + | sigma -> sigma end else sigma in @@ -157,7 +157,7 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr) let rec coerce_unify env x y = let x = hnf env !evdref x and y = hnf env !evdref y in try - evdref := the_conv_x_leq env x y !evdref; + evdref := Evarconv.unify_leq_delay env !evdref x y; None with UnableToUnify _ -> coerce' env x y and coerce' env x y : (EConstr.constr -> EConstr.constr) option = @@ -172,7 +172,7 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr) let rec aux tele typ typ' i co = if i < len then let hdx = l.(i) and hdy = l'.(i) in - try evdref := the_conv_x_leq env hdx hdy !evdref; + try evdref := unify_leq_delay env !evdref hdx hdy; let (n, eqT), restT = dest_prod typ in let (n', eqT'), restT' = dest_prod typ' in aux (hdx :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) co @@ -180,8 +180,8 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr) let (n, eqT), restT = dest_prod typ in let (n', eqT'), restT' = dest_prod typ' in let () = - try evdref := the_conv_x_leq env eqT eqT' !evdref - with UnableToUnify _ -> raise NoSubtacCoercion + try evdref := unify_leq_delay env !evdref eqT eqT' + with UnableToUnify _ -> raise NoSubtacCoercion in (* Disallow equalities on arities *) if Reductionops.is_arity env !evdref eqT then raise NoSubtacCoercion; @@ -483,14 +483,14 @@ let inh_coerce_to_fail flags env evd rigidonly v t c1 = | None -> evd, None, t with Not_found -> raise NoCoercion in - try (unify_leq flags env evd t' c1, v') + try (unify_leq_delay ~flags env evd t' c1, v') with UnableToUnify _ -> raise NoCoercion let default_flags_of env = default_flags_of TransparentState.full let rec inh_conv_coerce_to_fail ?loc env evd ?(flags=default_flags_of env) rigidonly v t c1 = - try (unify_leq flags env evd t c1, v) + try (unify_leq_delay ~flags env evd t c1, v) with UnableToUnify (best_failed_evd,e) -> try inh_coerce_to_fail flags env evd rigidonly v t c1 with NoCoercion -> diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 28dd63cfcc..dc613640d7 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1720,44 +1720,48 @@ let solve_unif_constraints_with_heuristics env exception UnableToUnify of evar_map * unification_error -let the_conv_x env ?(ts=default_transparent_state env) t1 t2 evd = - let flags = default_flags_of ts in - match evar_conv_x flags env evd CONV t1 t2 with +let unify_delay ?flags env evd t1 t2 = + let flags = + match flags with + | None -> default_flags_of (default_transparent_state env) + | Some flags -> flags + in + match evar_conv_x flags env evd CONV t1 t2 with | Success evd' -> evd' | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e)) -let the_conv_x_leq env ?(ts=default_transparent_state env) t1 t2 evd = - let flags = default_flags_of ts in +let unify_leq_delay ?flags env evd t1 t2 = + let flags = + match flags with + | None -> default_flags_of (default_transparent_state env) + | Some flags -> flags + in match evar_conv_x flags env evd CUMUL t1 t2 with | Success evd' -> evd' | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e)) -let make_opt = function - | Success evd -> Some evd - | UnifFailure _ -> None - -let conv env ?(ts=default_transparent_state env) evd t1 t2 = - let flags = default_flags_of ts in - make_opt(evar_conv_x flags env evd CONV t1 t2) +let unify ?flags ?(with_ho=true) env evd cv_pb ty1 ty2 = + let flags = + match flags with + | None -> default_flags_of (default_transparent_state env) + | Some flags -> flags + in + let res = evar_conv_x flags env evd cv_pb ty1 ty2 in + match res with + | Success evd -> + solve_unif_constraints_with_heuristics ~flags ~with_ho env evd + | UnifFailure (evd, reason) -> + raise (PretypeError (env, evd, CannotUnify (ty1, ty2, Some reason))) -let cumul env ?(ts=default_transparent_state env) evd t1 t2 = +(* deprecated *) +let the_conv_x env ?(ts=default_transparent_state env) t1 t2 evd = let flags = default_flags_of ts in - make_opt(evar_conv_x flags env evd CUMUL t1 t2) - -let unify flags env evd t1 t2 = - match evar_conv_x flags env evd CONV t1 t2 with + match evar_conv_x flags env evd CONV t1 t2 with | Success evd' -> evd' | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e)) -let unify_leq flags env evd t1 t2 = +let the_conv_x_leq env ?(ts=default_transparent_state env) t1 t2 evd = + let flags = default_flags_of ts in match evar_conv_x flags env evd CUMUL t1 t2 with | Success evd' -> evd' | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e)) - -let unify_with_heuristics flags ~with_ho env evd cv_pb ty1 ty2 = - let res = evar_conv_x flags env evd cv_pb ty1 ty2 in - match res with - | Success evd -> - solve_unif_constraints_with_heuristics ~flags ~with_ho env evd - | UnifFailure (evd, reason) -> - raise (PretypeError (env, evd, CannotUnify (ty1, ty2, Some reason))) diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index fa6f3466f6..0418b352fe 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -30,34 +30,50 @@ exception UnableToUnify of evar_map * Pretype_errors.unification_error (** {6 Main unification algorithm for type inference. } *) -(** returns exception NotUnifiable with best known evar_map if not unifiable *) +(** There are two variants for unification: one that delays constraints outside its capabilities + ([unify_delay]) and another that tries to solve such remaining constraints using + heuristics ([unify]). *) + +(** Theses functions allow to pass arbitrary flags to the unifier and can delay constraints. + In case of success, the two terms are hence unifiable only if the remaining constraints + can be solved or [check_problems_are_solved] is true. + + @raises UnableToUnify in case the two terms do not unify *) + +val unify_delay : ?flags:unify_flags -> env -> evar_map -> constr -> constr -> evar_map +val unify_leq_delay : ?flags:unify_flags -> env -> evar_map -> constr -> constr -> evar_map + +(** returns exception UnableToUnify with best known evar_map if not unifiable *) val the_conv_x : env -> ?ts:TransparentState.t -> constr -> constr -> evar_map -> evar_map +[@@ocaml.deprecated "Use Evarconv.unify_delay instead"] val the_conv_x_leq : env -> ?ts:TransparentState.t -> constr -> constr -> evar_map -> evar_map +[@@ocaml.deprecated "Use Evarconv.unify_leq_delay instead"] -(** Allows to pass arbitrary flags to the unifier *) -val unify : unify_flags -> env -> evar_map -> constr -> constr -> evar_map -val unify_leq : unify_flags -> env -> evar_map -> constr -> constr -> evar_map +(** This function also calls [solve_unif_constraints_with_heuristics] to resolve any remaining + constraints. In case of success the two terms are unified without condition. -(** @raises a PretypeError if it cannot unify *) -val unify_with_heuristics : unify_flags -> with_ho:bool -> - env -> evar_map -> conv_pb -> constr -> constr -> evar_map - -(** The same function resolving evars by side-effect and - catching the exception *) -val conv : env -> ?ts:TransparentState.t -> evar_map -> constr -> constr -> evar_map option -val cumul : env -> ?ts:TransparentState.t -> evar_map -> constr -> constr -> evar_map option + The with_ho option tells if higher-order unification should be tried to resolve the + constraints. + @raises a PretypeError if it cannot unify *) +val unify : ?flags:unify_flags -> ?with_ho:bool -> + env -> evar_map -> conv_pb -> constr -> constr -> evar_map (** {6 Unification heuristics. } *) (** Try heuristics to solve pending unification problems and to solve - evars with candidates *) + evars with candidates. + + The with_ho option tells if higher-order unification should be tried + to resolve the constraints. + + @raises a PretypeError if it fails to resolve some problem *) val solve_unif_constraints_with_heuristics : env -> ?flags:unify_flags -> ?with_ho:bool -> evar_map -> evar_map -(** Check all pending unification problems are solved and raise an - error otherwise *) +(** Check all pending unification problems are solved and raise a + PretypeError otherwise *) val check_problems_are_solved : env -> evar_map -> unit diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index e65bdd8220..770dfe328f 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -556,9 +556,9 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo | GFix (vn,i) -> i | GCoFix i -> i in - begin match conv !!env sigma ftys.(fixi) t with - | None -> sigma - | Some sigma -> sigma + begin match Evarconv.unify_delay !!env sigma ftys.(fixi) t with + | exception Evarconv.UnableToUnify _ -> sigma + | sigma -> sigma end | None -> sigma in @@ -667,11 +667,11 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo match candargs with | [] -> sigma, [], j_val hj | arg :: args -> - begin match conv !!env sigma (j_val hj) arg with - | Some sigma -> - sigma, args, nf_evar sigma (j_val hj) - | None -> + begin match Evarconv.unify_delay !!env sigma (j_val hj) arg with + | exception Evarconv.UnableToUnify _ -> sigma, [], j_val hj + | sigma -> + sigma, args, nf_evar sigma (j_val hj) end in let sigma, ujval = adjust_evar_source sigma na ujval in @@ -1057,9 +1057,9 @@ and pretype_type ~program_mode k0 resolve_tc valcon (env : GlobEnv.t) sigma c = match valcon with | None -> sigma, tj | Some v -> - begin match cumul !!env sigma v tj.utj_val with - | Some sigma -> sigma, tj - | None -> + begin match Evarconv.unify_leq_delay !!env sigma v tj.utj_val with + | sigma -> sigma, tj + | exception Evarconv.UnableToUnify _ -> error_unexpected_type ?loc:(loc_of_glob_constr c) !!env sigma tj.utj_val v end diff --git a/pretyping/typing.ml b/pretyping/typing.ml index e8d935fcbb..0b54160b3f 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -71,10 +71,10 @@ let judge_of_applied_inductive_knowing_parameters env sigma funj ind argjv = | _ -> error_cant_apply_not_functional env sigma funj argjv in - begin match Evarconv.cumul env sigma hj.uj_type c1 with - | Some sigma -> + begin match Evarconv.unify_leq_delay env sigma hj.uj_type c1 with + | sigma -> apply_rec sigma (n+1) (subst1 hj.uj_val c2) restjl - | None -> + | exception Evarconv.UnableToUnify _ -> error_cant_apply_bad_type env sigma (n, c1, hj.uj_type) funj argjv end in @@ -96,10 +96,10 @@ let judge_of_apply env sigma funj argjv = | _ -> error_cant_apply_not_functional env sigma funj argjv in - begin match Evarconv.cumul env sigma hj.uj_type c1 with - | Some sigma -> + begin match Evarconv.unify_leq_delay env sigma hj.uj_type c1 with + | sigma -> apply_rec sigma (n+1) (subst1 hj.uj_val c2) restjl - | None -> + | exception Evarconv.UnableToUnify _ -> error_cant_apply_bad_type env sigma (n, c1, hj.uj_type) funj argjv end in @@ -109,9 +109,9 @@ let check_branch_types env sigma (ind,u) cj (lfj,explft) = if not (Int.equal (Array.length lfj) (Array.length explft)) then error_number_branches env sigma cj (Array.length explft); Array.fold_left2_i (fun i sigma lfj explft -> - match Evarconv.cumul env sigma lfj.uj_type explft with - | Some sigma -> sigma - | None -> + match Evarconv.unify_leq_delay env sigma lfj.uj_type explft with + | sigma -> sigma + | exception Evarconv.UnableToUnify _ -> error_ill_formed_branch env sigma cj.uj_val ((ind,i+1),u) lfj.uj_type explft) sigma lfj explft @@ -127,9 +127,9 @@ let is_correct_arity env sigma c pj ind specif params = let pt' = whd_all env sigma pt in match EConstr.kind sigma pt', ar with | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' -> - begin match Evarconv.cumul env sigma a1 a1' with - | None -> error () - | Some sigma -> + begin match Evarconv.unify_leq_delay env sigma a1 a1' with + | exception Evarconv.UnableToUnify _ -> error () + | sigma -> srec (push_rel (LocalAssum (na1,a1)) env) sigma t ar' end | Sort s, [] -> @@ -187,9 +187,9 @@ let check_type_fixpoint ?loc env sigma lna lar vdefj = let lt = Array.length vdefj in assert (Int.equal (Array.length lar) lt); Array.fold_left2_i (fun i sigma defj ar -> - match Evarconv.cumul env sigma defj.uj_type (lift lt ar) with - | Some sigma -> sigma - | None -> + match Evarconv.unify_leq_delay env sigma defj.uj_type (lift lt ar) with + | sigma -> sigma + | exception Evarconv.UnableToUnify _ -> error_ill_typed_rec_body ?loc env sigma i lna vdefj lar) sigma vdefj lar @@ -211,10 +211,10 @@ let check_allowed_sort env sigma ind c p = let judge_of_cast env sigma cj k tj = let expected_type = tj.utj_val in - match Evarconv.cumul env sigma cj.uj_type expected_type with - | None -> + match Evarconv.unify_leq_delay env sigma cj.uj_type expected_type with + | exception Evarconv.UnableToUnify _ -> error_actual_type_core env sigma cj expected_type; - | Some sigma -> + | sigma -> sigma, { uj_val = mkCast (cj.uj_val, k, expected_type); uj_type = expected_type } @@ -427,10 +427,10 @@ and execute_array env = Array.fold_left_map (execute env) let check env sigma c t = let sigma, j = execute env sigma c in - match Evarconv.cumul env sigma j.uj_type t with - | None -> + match Evarconv.unify_leq_delay env sigma j.uj_type t with + | exception Evarconv.UnableToUnify _ -> error_actual_type_core env sigma j t - | Some sigma -> sigma + | sigma -> sigma (* Type of a constr *) diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 429bada7e3..d770d0614a 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -230,8 +230,9 @@ let unify_resolve_refine poly flags gls ((c, t, ctx),n,clenv) = let sigma', cl = Clenv.make_evar_clause env sigma ?len:n ty in let term = applist (term, List.map (fun x -> x.hole_evar) cl.cl_holes) in let sigma' = - Evarconv.the_conv_x_leq env ~ts:flags.core_unify_flags.modulo_delta - cl.cl_concl concl sigma' + Evarconv.(unify_leq_delay + ~flags:(default_flags_of flags.core_unify_flags.modulo_delta) + env sigma' cl.cl_concl concl) in (sigma', term) end let unify_resolve_refine poly flags gl clenv = diff --git a/tactics/equality.ml b/tactics/equality.ml index a8cfc87f9c..4a1bb37fa4 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -636,7 +636,7 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt = let evd = if unsafe then Some (Tacmach.New.project gl) else - try Some (Evarconv.the_conv_x (Proofview.Goal.env gl) t1 t2 (Tacmach.New.project gl)) + try Some (Evarconv.unify_delay (Proofview.Goal.env gl) (Tacmach.New.project gl) t1 t2) with Evarconv.UnableToUnify _ -> None in match evd with @@ -1194,9 +1194,8 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = (* is the default value typable with the expected type *) let dflt_typ = unsafe_type_of env sigma dflt in try - let sigma = Evarconv.the_conv_x_leq env dflt_typ p_i sigma in - let sigma = - Evarconv.solve_unif_constraints_with_heuristics env sigma in + let sigma = Evarconv.unify_leq_delay env sigma dflt_typ p_i in + let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in sigma, dflt with Evarconv.UnableToUnify _ -> user_err Pp.(str "Cannot solve a unification problem.") @@ -1211,11 +1210,11 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = match evopt with | Some w -> let w_type = unsafe_type_of env sigma w in - begin match Evarconv.cumul env sigma w_type a with - | Some sigma -> + begin match Evarconv.unify_leq_delay env sigma w_type a with + | sigma -> let sigma, exist_term = Evd.fresh_global env sigma sigdata.intro in sigma, applist(exist_term,[a;p_i_minus_1;w;tuple_tail]) - | None -> + | exception Evarconv.UnableToUnify _ -> user_err Pp.(str "Cannot solve a unification problem.") end | None -> diff --git a/tactics/tactics.ml b/tactics/tactics.ml index db59f7cfc2..415225454a 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3840,9 +3840,9 @@ let specialize_eqs id = let evars = ref (Proofview.Goal.sigma gl) in let unif env evars c1 c2 = compare_upto_variables !evars c1 c2 && - (match Evarconv.conv env !evars c1 c2 with - | Some sigma -> evars := sigma; true - | None -> false) + (match Evarconv.unify_delay env !evars c1 c2 with + | sigma -> evars := sigma; true + | exception Evarconv.UnableToUnify _ -> false) in let rec aux in_eqs ctx acc ty = match EConstr.kind !evars ty with @@ -4398,7 +4398,9 @@ let check_expected_type env sigma (elimc,bl) elimt = let sigma,cl = make_evar_clause env sigma ~len:(n - 1) elimt in let sigma = solve_evar_clause env sigma true cl bl in let (_,u,_) = destProd sigma cl.cl_concl in - fun t -> Option.has_some (Evarconv.cumul env sigma t u) + fun t -> match Evarconv.unify_leq_delay env sigma t u with + | _sigma -> true + | exception Evarconv.UnableToUnify _ -> false let check_enough_applied env sigma elim = (* A heuristic to decide whether the induction arg is enough applied *) -- cgit v1.2.3 From a4157eb4cb5ede453e02b415aa0c2b10ce9f961d Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 17 Oct 2018 18:27:34 +0200 Subject: [evarconv] Clean second order matching of evdrefs Remaining cases are due to map_constr_with_binders_left_to_right which does not allow side effects on the evd yet. --- pretyping/evarconv.ml | 116 +++++++++++++++++++++++++------------------------- 1 file changed, 57 insertions(+), 59 deletions(-) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index dc613640d7..65ccfc641f 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1199,9 +1199,10 @@ let default_occurrences_selection ?(frozen_evars=Evar.Set.empty) ts n = (default_occurrence_test ~frozen_evars ts, List.init n (fun _ -> default_occurrence_selection)) -let apply_on_subterm env evdref fixedref f test c t = - let test = test env !evdref c in - let prc env = Termops.Internal.print_constr_env env !evdref in +let apply_on_subterm env evd fixedref f test c t = + let test = test env evd c in + let prc env evd = Termops.Internal.print_constr_env env evd in + let evdref = ref evd in let rec applyrec (env,(k,c) as acc) t = if Evar.Set.exists (fun fixed -> occur_evar !evdref fixed t) !fixedref then match EConstr.kind !evdref t with @@ -1211,20 +1212,21 @@ let apply_on_subterm env evdref fixedref f test c t = applyrec acc t else (if !debug_ho_unification then - Feedback.msg_debug Pp.(str"Testing " ++ prc env c ++ str" against " ++ prc env t); + Feedback.msg_debug Pp.(str"Testing " ++ prc env !evdref c ++ str" against " ++ prc env !evdref t); let b, evd = try test env !evdref k c t with e when CErrors.noncritical e -> assert false in - if b then (evdref := evd; - if !debug_ho_unification then Feedback.msg_debug (Pp.str "succeeded"); - f k t) + if b then (if !debug_ho_unification then Feedback.msg_debug (Pp.str "succeeded"); + let evd', t' = f !evdref k t in + evdref := evd'; t') else ( if !debug_ho_unification then Feedback.msg_debug (Pp.str "failed"); map_constr_with_binders_left_to_right !evdref (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c))) applyrec acc t)) in - applyrec (env,(0,c)) t + let t' = applyrec (env,(0,c)) t in + !evdref, t' let filter_possible_projections evd c ty ctxt args = (* Since args in the types will be replaced by holes, we count the @@ -1334,98 +1336,96 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = (** Ensure that any progress made by Typing.e_solve_evars will not contradict the solution we are trying to build here by adding the problem as a constraint. *) let evd = Evarutil.add_unification_pb (CONV,env_rhs,mkEvar (evk,args),rhs) evd in - let evdref = ref evd in - let prc env c = Termops.Internal.print_constr_env env !evdref c in + let prc env evd c = Termops.Internal.print_constr_env env evd c in let rec make_subst = function - | decl'::ctxt', c::l, occs::occsl when isVarId evd (NamedDecl.get_id decl') c -> + | decl'::ctxt', c::l, occs::occsl when isVarId evd (NamedDecl.get_id decl') c -> begin match occs with - | AtOccurrences loc when not (Locusops.is_all_occurrences loc) -> - user_err Pp.(str "Cannot force abstraction on identity instance.") - | _ -> - make_subst (ctxt',l,occsl) + | AtOccurrences loc when not (Locusops.is_all_occurrences loc) -> + user_err Pp.(str "Cannot force abstraction on identity instance.") + | _ -> + make_subst (ctxt',l,occsl) end - | decl'::ctxt', c::l, occs::occsl -> + | decl'::ctxt', c::l, occs::occsl -> let id = NamedDecl.get_id decl' in let t = NamedDecl.get_type decl' in let evs = ref [] in let c = nf_evar evd c in (* ty is in env_rhs now *) let ty = replace_vars argsubst t in - let filter' = filter_possible_projections !evdref c (nf_evar evd ty) ctxt args in + let filter' = filter_possible_projections evd c (nf_evar evd ty) ctxt args in (id,t,c,ty,evs,Filter.make filter',occs) :: make_subst (ctxt',l,occsl) - | _, _, [] -> [] - | _ -> anomaly (Pp.str "Signature or instance are shorter than the occurrences list.") in + | _, _, [] -> [] + | _ -> anomaly (Pp.str "Signature or instance are shorter than the occurrences list.") + in let fixed = ref Evar.Set.empty in - let rec set_holes env_rhs evdref rhs = function + let rec set_holes env_rhs evd rhs = function | (id,idty,c,cty,evsref,filter,occs)::subst -> - let c = nf_evar !evdref c in + let c = nf_evar evd c in if !debug_ho_unification then Feedback.msg_debug Pp.(str"set holes for: " ++ - prc env_rhs (mkVar id) ++ spc () ++ - prc env_rhs c ++ str" in " ++ - prc env_rhs rhs); + prc env_rhs evd (mkVar id) ++ spc () ++ + prc env_rhs evd c ++ str" in " ++ + prc env_rhs evd rhs); let occ = ref 1 in - let set_var k inst = + let set_var evd k inst = let oc = !occ in if !debug_ho_unification then (Feedback.msg_debug Pp.(str"Found one occurrence"); - Feedback.msg_debug Pp.(str"cty: " ++ prc env_rhs c)); + Feedback.msg_debug Pp.(str"cty: " ++ prc env_rhs evd c)); incr occ; match occs with | AtOccurrences occs -> - if Locusops.is_selected oc occs then mkVar id - else inst + if Locusops.is_selected oc occs then evd, mkVar id + else evd, inst | Unspecified prefer_abstraction -> - let evty = set_holes env_rhs evdref cty subst in - let evty = nf_evar !evdref evty in + let evd, evty = set_holes env_rhs evd cty subst in + let evty = nf_evar evd evty in if !debug_ho_unification then - Feedback.msg_debug Pp.(str"abstracting one occurrence " ++ prc env_rhs inst ++ - str" of type: " ++ prc env_evar evty ++ - str " for " ++ prc env_rhs c); + Feedback.msg_debug Pp.(str"abstracting one occurrence " ++ prc env_rhs evd inst ++ + str" of type: " ++ prc env_evar evd evty ++ + str " for " ++ prc env_rhs evd c); let instance = Filter.filter_list filter instance in (** Allow any type lower than the variable's type as the abstracted subterm might have a smaller type, which could be crucial to make the surrounding context typecheck. *) let evd, evty = - if isArity !evdref evty then + if isArity evd evty then refresh_universes ~status:Evd.univ_flexible (Some true) - env_evar_unf !evdref evty - else !evdref, evty in + env_evar_unf evd evty + else evd, evty in let (evd, ev) = new_evar_instance sign evd evty ~filter instance in - let evk = fst (destEvar !evdref ev) in - evdref := evd; + let evk = fst (destEvar evd ev) in evsref := (evk,evty,inst,prefer_abstraction)::!evsref; fixed := Evar.Set.add evk !fixed; - ev + evd, ev in - let rhs' = apply_on_subterm env_rhs evdref fixed set_var test c rhs in + let evd, rhs' = apply_on_subterm env_rhs evd fixed set_var test c rhs in if !debug_ho_unification then - Feedback.msg_debug Pp.(str"abstracted: " ++ prc env_rhs rhs'); - let () = check_selected_occs env_rhs !evdref c !occ occs in + Feedback.msg_debug Pp.(str"abstracted: " ++ prc env_rhs evd rhs'); + let () = check_selected_occs env_rhs evd c !occ occs in let env_rhs' = push_named (NamedDecl.LocalAssum (id,idty)) env_rhs in - set_holes env_rhs' evdref rhs' subst - | [] -> rhs in + set_holes env_rhs' evd rhs' subst + | [] -> evd, rhs in let subst = make_subst (ctxt,Array.to_list args,argoccs) in - let rhs' = set_holes env_rhs evdref rhs subst in - let evd = !evdref in + let evd, rhs' = set_holes env_rhs evd rhs subst in let rhs' = nf_evar evd rhs' in (** Thin evars making the term typable in env_evar *) let evd, rhs' = thin_evars env_evar evd ctxt rhs' in (* We instantiate the evars of which the value is forced by typing *) if !debug_ho_unification then - (Feedback.msg_debug Pp.(str"solve_evars on: " ++ prc env_evar rhs'); + (Feedback.msg_debug Pp.(str"solve_evars on: " ++ prc env_evar evd rhs'); Feedback.msg_debug Pp.(str"evars: " ++ pr_evar_map (Some 0) evd)); let evd,rhs' = try !solve_evars env_evar evd rhs' with e when Pretype_errors.precatchable_exception e -> (* Could not revert all subterms *) - raise (TypingFailed !evdref) in + raise (TypingFailed evd) in let rhs' = nf_evar evd rhs' in (* We instantiate the evars of which the value is forced by typing *) if !debug_ho_unification then - (Feedback.msg_debug Pp.(str"after solve_evars: " ++ prc env_evar rhs'); + (Feedback.msg_debug Pp.(str"after solve_evars: " ++ prc env_evar evd rhs'); Feedback.msg_debug Pp.(str"evars: " ++ pr_evar_map (Some 0) evd)); let rec abstract_free_holes evd = function @@ -1433,8 +1433,8 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = let c = nf_evar evd c in if !debug_ho_unification then Feedback.msg_debug Pp.(str"abstracting: " ++ - prc env_rhs (mkVar id) ++ spc () ++ - prc env_rhs c); + prc env_rhs evd (mkVar id) ++ spc () ++ + prc env_rhs evd c); let rec force_instantiation evd = function | (evk,evty,inst,abstract)::evs -> let evk = Option.default evk (Evarutil.advance evd evk) in @@ -1467,7 +1467,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = let env = Evd.evar_env evi in Feedback.msg_debug Pp.(str"evar is defined: " ++ int (Evar.repr evk) ++ spc () ++ - prc env (match evar_body evi with Evar_defined c -> c + prc env evd (match evar_body evi with Evar_defined c -> c | Evar_empty -> assert false))); evd) in force_instantiation evd evs @@ -1482,26 +1482,24 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = let evi = Evd.find evd evk in let evenv = evar_env evi in let body = match evar_body evi with Evar_empty -> assert false | Evar_defined c -> c in - Feedback.msg_debug Pp.(str"evar was defined already as: " ++ prc evenv body) + Feedback.msg_debug Pp.(str"evar was defined already as: " ++ prc evenv evd body) end; evd) else try let evi = Evd.find_undefined evd evk in let evenv = evar_env evi in - let evdref = ref evd in - let rhs' = nf_evar !evdref rhs' in + let rhs' = nf_evar evd rhs' in if !debug_ho_unification then Feedback.msg_debug Pp.(str"abstracted type before second solve_evars: " ++ - prc evenv rhs'); + prc evenv evd rhs'); (** solve_evars is not commuting with nf_evar, because restricting an evar might provide a more specific type. *) let evd, _ = !solve_evars evenv evd rhs' in - evdref := evd; if !debug_ho_unification then - Feedback.msg_debug Pp.(str"abstracted type: " ++ prc evenv (nf_evar !evdref rhs')); + Feedback.msg_debug Pp.(str"abstracted type: " ++ prc evenv evd (nf_evar evd rhs')); let flags = default_flags_of TransparentState.full in - Evarsolve.instantiate_evar evar_unify flags !evdref evk rhs' + Evarsolve.instantiate_evar evar_unify flags evd evk rhs' with IllTypedInstance _ -> raise (TypingFailed evd) in let evd = abstract_free_holes evd subst in -- cgit v1.2.3 From 93ef4e058cb9f7bfc6f3abc8bdc5752a2d8df5ca Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 17 Oct 2018 18:57:53 +0200 Subject: [evarconv] Handle frozen evars in solve_unif_constraints_with_heuristics --- pretyping/evarconv.ml | 18 ++++++++++-------- pretyping/evarsolve.ml | 45 +++++++++++++++++++++++++++++---------------- 2 files changed, 39 insertions(+), 24 deletions(-) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 65ccfc641f..748143cad5 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1545,7 +1545,6 @@ let is_beyond_capabilities = function | CannotSolveConstraint (pb,ProblemBeyondCapabilities) -> true | _ -> false -(* TODO frozen *) let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 = let t1 = apprec_nohdbeta flags env evd (whd_head_evar evd t1) in let t2 = apprec_nohdbeta flags env evd (whd_head_evar evd t2) in @@ -1558,7 +1557,8 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 = Termops.Internal.print_constr_env env evd t2 ++ cut ())) in let app_empty = Array.is_empty l1 && Array.is_empty l2 in match EConstr.kind evd term1, EConstr.kind evd term2 with - | Evar (evk1,args1), (Rel _|Var _) when app_empty + | Evar (evk1,args1 as ev1), (Rel _|Var _) when app_empty + && not (is_frozen flags ev1) && List.for_all (fun a -> EConstr.eq_constr evd a term2 || isEvar evd a) (remove_instance_local_defs evd evk1 args1) -> (* The typical kind of constraint coming from pattern-matching return @@ -1568,8 +1568,9 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 = | None -> let reason = ProblemBeyondCapabilities in UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason))) - | (Rel _|Var _), Evar (evk2,args2) when app_empty - && List.for_all (fun a -> EConstr.eq_constr evd a term1 || isEvar evd a) + | (Rel _|Var _), Evar (evk2,args2 as ev2) when app_empty + && not (is_frozen flags ev2) + && List.for_all (fun a -> EConstr.eq_constr evd a term1 || isEvar evd a) (remove_instance_local_defs evd evk2 args2) -> (* The typical kind of constraint coming from pattern-matching return type inference *) @@ -1589,28 +1590,29 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 = Success (solve_refl ~can_drop:true f flags env evd (position_problem true pbty) evk1 args1 args2) | Evar ev1, Evar ev2 when app_empty -> + (* solve_evar_evar handles the cases ev1 and/or ev2 are frozen *) Success (solve_evar_evar ~force:true (evar_define evar_unify flags ~choose:true) evar_unify flags env evd (position_problem true pbty) ev1 ev2) - | Evar ev1,_ when Array.length l1 <= Array.length l2 -> + | Evar ev1,_ when not (is_frozen flags ev1) && Array.length l1 <= Array.length l2 -> (* On "?n t1 .. tn = u u1 .. u(n+p)", try first-order unification *) (* and otherwise second-order matching *) ise_try evd [(fun evd -> first_order_unification flags env evd (ev1,l1) appr2); (fun evd -> second_order_matching_with_args flags env evd with_ho pbty ev1 l1 t2)] - | _,Evar ev2 when Array.length l2 <= Array.length l1 -> + | _,Evar ev2 when not (is_frozen flags ev2) && Array.length l2 <= Array.length l1 -> (* On "u u1 .. u(n+p) = ?n t1 .. tn", try first-order unification *) (* and otherwise second-order matching *) ise_try evd [(fun evd -> first_order_unification flags env evd (ev2,l2) appr1); (fun evd -> second_order_matching_with_args flags env evd with_ho pbty ev2 l2 t1)] - | Evar ev1,_ -> + | Evar ev1,_ when not (is_frozen flags ev1) -> (* Try second-order pattern-matching *) second_order_matching_with_args flags env evd with_ho pbty ev1 l1 t2 - | _,Evar ev2 -> + | _,Evar ev2 when not (is_frozen flags ev2) -> (* Try second-order pattern-matching *) second_order_matching_with_args flags env evd with_ho pbty ev2 l2 t1 | _ -> diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index ffb083e768..cdaf66f119 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1294,24 +1294,30 @@ let preferred_orientation evd evk1 evk2 = else if is_obligation_evar evd evk2 then false else true -(** Precondition evk1 is not frozen, evk2 might be. *) let solve_evar_evar_aux force f unify flags env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) = let aliases = make_alias_map env evd in + let frozen_ev1 = Evar.Set.mem evk1 flags.frozen_evars in let frozen_ev2 = Evar.Set.mem evk2 flags.frozen_evars in if preferred_orientation evd evk1 evk2 then - try solve_evar_evar_l2r force f unify flags env evd aliases (opp_problem pbty) ev2 ev1 - with CannotProject (evd,ev2) when not frozen_ev2 -> - try solve_evar_evar_l2r force f unify flags env evd aliases pbty ev1 ev2 - with CannotProject (evd,ev1) -> - add_conv_oriented_pb ~tail:true (pbty,env,mkEvar ev1,mkEvar ev2) evd - else - try if not frozen_ev2 then + try if not frozen_ev1 then + solve_evar_evar_l2r force f unify flags env evd aliases (opp_problem pbty) ev2 ev1 + else raise (CannotProject (evd,ev2)) + with CannotProject (evd,ev2) -> + try if not frozen_ev2 then solve_evar_evar_l2r force f unify flags env evd aliases pbty ev1 ev2 else raise (CannotProject (evd,ev1)) + with CannotProject (evd,ev1) -> + add_conv_oriented_pb ~tail:true (pbty,env,mkEvar ev1,mkEvar ev2) evd + else + try if not frozen_ev2 then + solve_evar_evar_l2r force f unify flags env evd aliases pbty ev1 ev2 + else raise (CannotProject (evd,ev1)) with CannotProject (evd,ev1) -> - try solve_evar_evar_l2r force f unify flags env evd aliases (opp_problem pbty) ev2 ev1 + try if not frozen_ev1 then + solve_evar_evar_l2r force f unify flags env evd aliases (opp_problem pbty) ev2 ev1 + else raise (CannotProject (evd,ev2)) with CannotProject (evd,ev2) -> - add_conv_oriented_pb ~tail:true (pbty,env,mkEvar ev1,mkEvar ev2) evd + add_conv_oriented_pb ~tail:true (pbty,env,mkEvar ev1,mkEvar ev2) evd (** Precondition: evk1 is not frozen *) let solve_evar_evar ?(force=false) f unify flags env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) = @@ -1361,7 +1367,7 @@ let solve_refl ?(can_drop=false) unify flags env evd pbty evk argsv1 argsv2 = let eq_constr c1 c2 = match EConstr.eq_constr_universes env !evdref c1 c2 with | None -> false | Some cstr -> - try ignore (Evd.add_universe_constraints !evdref cstr); true + try evdref := Evd.add_universe_constraints !evdref cstr; true with UniversesDiffer -> false in if Array.equal eq_constr argsv1 argsv2 then !evdref else @@ -1373,15 +1379,22 @@ let solve_refl ?(can_drop=false) unify flags env evd pbty evk argsv1 argsv2 = let candidates = filter_candidates evd evk untypedfilter NoUpdate in let filter = closure_of_filter evd evk untypedfilter in let evd',ev1 = restrict_applied_evar evd (evk,argsv1) filter candidates in - if Evar.equal (fst ev1) evk && can_drop then (* No refinement *) evd' else + let frozen = Evar.Set.mem evk flags.frozen_evars in + if Evar.equal (fst ev1) evk && (frozen || can_drop) then + (* No refinement needed *) evd' + else (* either progress, or not allowed to drop, e.g. to preserve possibly *) (* informative equations such as ?e[x:=?y]=?e[x:=?y'] where we don't know *) (* if e can depend on x until ?y is not resolved, or, conversely, we *) (* don't know if ?y has to be unified with ?y, until e is resolved *) - let argsv2 = restrict_instance evd' evk filter argsv2 in - let ev2 = (fst ev1,argsv2) in - (* Leave a unification problem *) - add_conv_oriented_pb (pbty,env,mkEvar ev1,mkEvar ev2) evd' + if frozen then + (* We cannot prune a frozen evar *) + add_conv_oriented_pb (pbty,env,mkEvar (evk, argsv1),mkEvar (evk,argsv2)) evd + else + let argsv2 = restrict_instance evd' evk filter argsv2 in + let ev2 = (fst ev1,argsv2) in + (* Leave a unification problem *) + add_conv_oriented_pb (pbty,env,mkEvar ev1,mkEvar ev2) evd' (* If the evar can be instantiated by a finite set of candidates known in advance, we check which of them apply *) -- cgit v1.2.3 From e3178fb2de9a84bbcdc90a60cd8f27cd1323eb36 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 17 Oct 2018 19:24:30 +0200 Subject: Document the unify_flags more throroughly in evarsolve. --- pretyping/evarsolve.mli | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index dfadb4aaea..ce803fe254 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -18,12 +18,22 @@ val of_alias : alias -> EConstr.t type unify_flags = { modulo_betaiota : bool; + (* Enable beta-iota reductions during unification *) open_ts : Names.transparent_state; + (* Enable delta reduction according to open_ts for open terms *) closed_ts : Names.transparent_state; + (* Enable delta reduction according to closed_ts for closed terms (when calling conversion) *) subterm_ts : Names.transparent_state; + (* Enable delta reduction according to subterm_ts for selection of subterms during higher-order + unifications. *) frozen_evars : Evar.Set.t; + (* Frozen evars are treated like rigid variables during unification: they can not be instantiated. *) allow_K_at_toplevel : bool; - with_cs : bool} + (* During higher-order unifications, allow to produce K-redexes: i.e. to produce + an abstraction for an unused argument *) + with_cs : bool + (* Enable canonical structure resolution during unification *) +} type unification_result = | Success of evar_map -- cgit v1.2.3 From e07fcc19cf8459ce2ae87d9ccbbc7806a0be576f Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 18 Oct 2018 13:21:02 +0200 Subject: Add back the deprecated conv/cumul functions. --- pretyping/evarconv.ml | 12 ++++++++++++ pretyping/evarconv.mli | 9 +++++++++ 2 files changed, 21 insertions(+) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 748143cad5..67d650b112 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1765,3 +1765,15 @@ let the_conv_x_leq env ?(ts=default_transparent_state env) t1 t2 evd = match evar_conv_x flags env evd CUMUL t1 t2 with | Success evd' -> evd' | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e)) + +let make_opt = function + | Success evd -> Some evd + | UnifFailure _ -> None + +let conv env ?(ts=default_transparent_state env) evd t1 t2 = + let flags = default_flags_of ts in + make_opt(evar_conv_x flags env evd CONV t1 t2) + +let cumul env ?(ts=default_transparent_state env) evd t1 t2 = + let flags = default_flags_of ts in + make_opt(evar_conv_x flags env evd CUMUL t1 t2) diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 0418b352fe..2c4a2f144e 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -35,6 +35,9 @@ exception UnableToUnify of evar_map * Pretype_errors.unification_error heuristics ([unify]). *) (** Theses functions allow to pass arbitrary flags to the unifier and can delay constraints. + In case the flags are not specified, they default to + [default_flags_of full_transparent_state] currently. + In case of success, the two terms are hence unifiable only if the remaining constraints can be solved or [check_problems_are_solved] is true. @@ -48,6 +51,12 @@ val the_conv_x : env -> ?ts:TransparentState.t -> constr -> constr -> evar_m [@@ocaml.deprecated "Use Evarconv.unify_delay instead"] val the_conv_x_leq : env -> ?ts:TransparentState.t -> constr -> constr -> evar_map -> evar_map [@@ocaml.deprecated "Use Evarconv.unify_leq_delay instead"] +(** The same function resolving evars by side-effect and + catching the exception *) +val conv : env -> ?ts:transparent_state -> evar_map -> constr -> constr -> evar_map option +[@@ocaml.deprecated "Use Evarconv.unify_delay instead"] +val cumul : env -> ?ts:transparent_state -> evar_map -> constr -> constr -> evar_map option +[@@ocaml.deprecated "Use Evarconv.unify_leq_delay instead"] (** This function also calls [solve_unif_constraints_with_heuristics] to resolve any remaining constraints. In case of success the two terms are unified without condition. -- cgit v1.2.3 From 2265d20c48dff6e1ea9a5cb9be9640603f3be3cf Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 18 Oct 2018 14:46:37 +0200 Subject: Add overlays for unicoq and mtac2 --- dev/ci/user-overlays/07819-mattam-ho-matching-occ-sel.sh | 10 ++++++++++ 1 file changed, 10 insertions(+) create mode 100644 dev/ci/user-overlays/07819-mattam-ho-matching-occ-sel.sh diff --git a/dev/ci/user-overlays/07819-mattam-ho-matching-occ-sel.sh b/dev/ci/user-overlays/07819-mattam-ho-matching-occ-sel.sh new file mode 100644 index 0000000000..c399e27736 --- /dev/null +++ b/dev/ci/user-overlays/07819-mattam-ho-matching-occ-sel.sh @@ -0,0 +1,10 @@ +_OVERLAY_BRANCH=ho-matching-occ-sel + +if [ "$CI_PULL_REQUEST" = "7819" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; then + + unicoq_CI_REF="PR7819-overlay" + + mtac2_CI_REF="PR7819-overlay" + mtac2_CI_GITURL=https://github.com/mattam82/Mtac2 + +fi -- cgit v1.2.3 From ad0cf24789b0f7d5b12cef4d09f93c9d9aeb6150 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 18 Oct 2018 16:12:27 +0200 Subject: Fix issue found in GeoCoq --- pretyping/evarconv.ml | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 67d650b112..f1845af7f2 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -788,7 +788,15 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty else UnifFailure (i,NotSameHead) and f3 i = miller true (sp1,al1) appr1 appr2 i and f4 i = miller false (sp2,al2) appr2 appr1 i - and f5 i = consume true appr1 appr2 i in + and f5 i = + (** We ensure failure of consuming the stacks does not + propagate an error about unification of the stacks while + the heads themselves cannot be unified, so we return + NotSameHead. *) + match consume true appr1 appr2 i with + | Success _ as x -> x + | UnifFailure _ -> quick_fail i + in ise_try evd [f1; f2; f3; f4; f5] | Flexible ev1, MaybeFlexible v2 -> -- cgit v1.2.3 From 62cf1ad380772628ed6e547de3fb875275610b4d Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 18 Oct 2018 16:56:17 +0200 Subject: Add overlay for Equations --- dev/ci/user-overlays/07819-mattam-ho-matching-occ-sel.sh | 2 ++ 1 file changed, 2 insertions(+) diff --git a/dev/ci/user-overlays/07819-mattam-ho-matching-occ-sel.sh b/dev/ci/user-overlays/07819-mattam-ho-matching-occ-sel.sh index c399e27736..e344e869d5 100644 --- a/dev/ci/user-overlays/07819-mattam-ho-matching-occ-sel.sh +++ b/dev/ci/user-overlays/07819-mattam-ho-matching-occ-sel.sh @@ -7,4 +7,6 @@ if [ "$CI_PULL_REQUEST" = "7819" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; the mtac2_CI_REF="PR7819-overlay" mtac2_CI_GITURL=https://github.com/mattam82/Mtac2 + Equations_CI_REF="PR7819-overlay" + fi -- cgit v1.2.3 From ce36c131804cd7fb0a460277d88743c7131c5ed3 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 8 Feb 2019 11:28:07 +0100 Subject: Coercion intf fix --- pretyping/coercion.mli | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli index c954a2a851..43d4059785 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.mli @@ -58,7 +58,8 @@ val inh_conv_coerce_rigid_to : ?loc:Loc.t -> program_mode:bool ->bool -> is coercible to an object of type [t'] adding evar constraints if needed; it fails if no coercion exists *) val inh_conv_coerces_to : ?loc:Loc.t -> - env -> evar_map -> types -> types -> evar_map + env -> evar_map -> ?flags:Evarconv.unify_flags -> + types -> types -> evar_map (** [inh_pattern_coerce_to loc env isevars pat ind1 ind2] coerces the Cases pattern [pat] typed in [ind1] into a pattern typed in [ind2]; -- cgit v1.2.3 From b74aaa4ce0191b92837a15773ae23e53abd22bd9 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 8 Feb 2019 11:28:25 +0100 Subject: evarconf transp state and comments fixes --- pretyping/evarconv.ml | 30 +++++++++++++++--------------- pretyping/evarconv.mli | 9 +++++---- 2 files changed, 20 insertions(+), 19 deletions(-) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index f1845af7f2..cfa0875ca5 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -190,7 +190,7 @@ let occur_rigidly flags env evd (evk,_) t = | Ind _ | Sort _ -> Rigid false | Proj (p, c) -> let cst = Projection.constant p in - let rigid = not (is_transparent_constant flags.open_ts cst) in + let rigid = not (TransparentState.is_transparent_constant flags.open_ts cst) in if rigid then aux c else (* if the evar appears rigidly in c then this elimination cannot reduce and we have a rigid occurrence, otherwise @@ -208,7 +208,7 @@ let occur_rigidly flags env evd (evk,_) t = | Lambda (na, t, b) -> aux b | LetIn (na, _, _, b) -> aux b | Const (c,_) -> - if is_transparent_constant flags.open_ts c then Reducible + if TransparentState.is_transparent_constant flags.open_ts c then Reducible else Rigid false | Prod (_, b, t) -> let b' = aux b and t' = aux t in @@ -789,7 +789,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty and f3 i = miller true (sp1,al1) appr1 appr2 i and f4 i = miller false (sp2,al2) appr2 appr1 i and f5 i = - (** We ensure failure of consuming the stacks does not + (* We ensure failure of consuming the stacks does not propagate an error about unification of the stacks while the heads themselves cannot be unified, so we return NotSameHead. *) @@ -934,7 +934,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty let c = nf_evar i c1 in let na = Nameops.Name.pick na1 na2 in evar_conv_x flags (push_rel (RelDecl.LocalAssum (na,c)) env) i CONV c'1 c'2); - (** When in modulo_betaiota = false case, lambda's are not reduced *) + (* When in modulo_betaiota = false case, lambda's are not reduced *) (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk1 sk2)] | Flexible ev1, Rigid -> flex_rigid true ev1 appr1 appr2 @@ -1014,7 +1014,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty | Int _, Int _ -> rigids env evd sk1 term1 sk2 term2 - | Evar (sp1,al1), Evar (sp2,al2) -> (** Frozen evars *) + | Evar (sp1,al1), Evar (sp2,al2) -> (* Frozen evars *) if Evar.equal sp1 sp2 then match ise_stack2 false env evd (evar_conv_x flags) sk1 sk2 with |None, Success i' -> @@ -1341,7 +1341,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = let instance = List.map mkVar vars in let rhs = nf_evar evd rhs in if not (noccur_evar env_rhs evd evk rhs) then raise (TypingFailed evd); - (** Ensure that any progress made by Typing.e_solve_evars will not contradict + (* Ensure that any progress made by Typing.e_solve_evars will not contradict the solution we are trying to build here by adding the problem as a constraint. *) let evd = Evarutil.add_unification_pb (CONV,env_rhs,mkEvar (evk,args),rhs) evd in let prc env evd c = Termops.Internal.print_constr_env env evd c in @@ -1393,9 +1393,9 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = str" of type: " ++ prc env_evar evd evty ++ str " for " ++ prc env_rhs evd c); let instance = Filter.filter_list filter instance in - (** Allow any type lower than the variable's type as the - abstracted subterm might have a smaller type, which could be - crucial to make the surrounding context typecheck. *) + (* Allow any type lower than the variable's type as the + abstracted subterm might have a smaller type, which could be + crucial to make the surrounding context typecheck. *) let evd, evty = if isArity evd evty then refresh_universes ~status:Evd.univ_flexible (Some true) @@ -1419,12 +1419,12 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = let evd, rhs' = set_holes env_rhs evd rhs subst in let rhs' = nf_evar evd rhs' in - (** Thin evars making the term typable in env_evar *) + (* Thin evars making the term typable in env_evar *) let evd, rhs' = thin_evars env_evar evd ctxt rhs' in (* We instantiate the evars of which the value is forced by typing *) if !debug_ho_unification then (Feedback.msg_debug Pp.(str"solve_evars on: " ++ prc env_evar evd rhs'); - Feedback.msg_debug Pp.(str"evars: " ++ pr_evar_map (Some 0) evd)); + Feedback.msg_debug Pp.(str"evars: " ++ pr_evar_map (Some 0) env_evar evd)); let evd,rhs' = try !solve_evars env_evar evd rhs' with e when Pretype_errors.precatchable_exception e -> @@ -1434,7 +1434,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = (* We instantiate the evars of which the value is forced by typing *) if !debug_ho_unification then (Feedback.msg_debug Pp.(str"after solve_evars: " ++ prc env_evar evd rhs'); - Feedback.msg_debug Pp.(str"evars: " ++ pr_evar_map (Some 0) evd)); + Feedback.msg_debug Pp.(str"evars: " ++ pr_evar_map (Some 0) env_evar evd)); let rec abstract_free_holes evd = function | (id,idty,c,cty,evsref,_,_)::l -> @@ -1483,7 +1483,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = in force_instantiation evd !evsref | [] -> if Evd.is_defined evd evk then - (** Can happen due to dependencies: instantiating evars in the arguments of evk might + (* Can happen due to dependencies: instantiating evars in the arguments of evk might instantiate evk itself. *) (if !debug_ho_unification then begin @@ -1501,7 +1501,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = if !debug_ho_unification then Feedback.msg_debug Pp.(str"abstracted type before second solve_evars: " ++ prc evenv evd rhs'); - (** solve_evars is not commuting with nf_evar, because restricting + (* solve_evars is not commuting with nf_evar, because restricting an evar might provide a more specific type. *) let evd, _ = !solve_evars evenv evd rhs' in if !debug_ho_unification then @@ -1591,7 +1591,7 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 = let f flags ontype env evd pbty x y = let reds = match ontype with - | TypeUnification -> full_transparent_state + | TypeUnification -> TransparentState.full | TermUnification -> flags.open_ts in is_fconv ~reds pbty env evd x y in diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 2c4a2f144e..0fe47c2a48 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -19,7 +19,7 @@ open Locus type unify_flags = Evarsolve.unify_flags (** The default subterm transparent state is no unfoldings *) -val default_flags_of : ?subterm_ts:transparent_state -> transparent_state -> unify_flags +val default_flags_of : ?subterm_ts:TransparentState.t -> TransparentState.t -> unify_flags type unify_fun = unify_flags -> env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result @@ -36,7 +36,7 @@ exception UnableToUnify of evar_map * Pretype_errors.unification_error (** Theses functions allow to pass arbitrary flags to the unifier and can delay constraints. In case the flags are not specified, they default to - [default_flags_of full_transparent_state] currently. + [default_flags_of TransparentState.full] currently. In case of success, the two terms are hence unifiable only if the remaining constraints can be solved or [check_problems_are_solved] is true. @@ -53,9 +53,10 @@ val the_conv_x_leq : env -> ?ts:TransparentState.t -> constr -> constr -> evar_m [@@ocaml.deprecated "Use Evarconv.unify_leq_delay instead"] (** The same function resolving evars by side-effect and catching the exception *) -val conv : env -> ?ts:transparent_state -> evar_map -> constr -> constr -> evar_map option + +val conv : env -> ?ts:TransparentState.t -> evar_map -> constr -> constr -> evar_map option [@@ocaml.deprecated "Use Evarconv.unify_delay instead"] -val cumul : env -> ?ts:transparent_state -> evar_map -> constr -> constr -> evar_map option +val cumul : env -> ?ts:TransparentState.t -> evar_map -> constr -> constr -> evar_map option [@@ocaml.deprecated "Use Evarconv.unify_leq_delay instead"] (** This function also calls [solve_unif_constraints_with_heuristics] to resolve any remaining -- cgit v1.2.3 From ab6397730354d6048062568c87a7d971f20934c0 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 8 Feb 2019 11:28:43 +0100 Subject: evarsolve transp_state and comments fixes --- pretyping/evarsolve.ml | 10 +++++----- pretyping/evarsolve.mli | 6 +++--- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index cdaf66f119..e5f2207333 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -26,9 +26,9 @@ open Pretype_errors type unify_flags = { modulo_betaiota: bool; - open_ts : transparent_state; - closed_ts : transparent_state; - subterm_ts : transparent_state; + open_ts : TransparentState.t; + closed_ts : TransparentState.t; + subterm_ts : TransparentState.t; frozen_evars : Evar.Set.t; allow_K_at_toplevel : bool; with_cs : bool } @@ -1442,8 +1442,8 @@ let occur_evar_upto_types sigma n c = try occur_rec c; false with Occur -> true let instantiate_evar unify flags evd evk body = - (** Check instance freezing the evar to be defined, as - checking could involve the same evar definition problem again otherwise *) + (* Check instance freezing the evar to be defined, as + checking could involve the same evar definition problem again otherwise *) let flags = { flags with frozen_evars = Evar.Set.add evk flags.frozen_evars } in let evd' = check_evar_instance unify flags evd evk body in Evd.define evk body evd' diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index ce803fe254..ebf8230bbd 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -19,11 +19,11 @@ val of_alias : alias -> EConstr.t type unify_flags = { modulo_betaiota : bool; (* Enable beta-iota reductions during unification *) - open_ts : Names.transparent_state; + open_ts : TransparentState.t; (* Enable delta reduction according to open_ts for open terms *) - closed_ts : Names.transparent_state; + closed_ts : TransparentState.t; (* Enable delta reduction according to closed_ts for closed terms (when calling conversion) *) - subterm_ts : Names.transparent_state; + subterm_ts : TransparentState.t; (* Enable delta reduction according to subterm_ts for selection of subterms during higher-order unifications. *) frozen_evars : Evar.Set.t; -- cgit v1.2.3 From d9f86f9920efda1057b09d10d64764babe1dec44 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 8 Feb 2019 16:42:50 +0100 Subject: Update overlay file --- dev/ci/user-overlays/07819-mattam-ho-matching-occ-sel.sh | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/dev/ci/user-overlays/07819-mattam-ho-matching-occ-sel.sh b/dev/ci/user-overlays/07819-mattam-ho-matching-occ-sel.sh index e344e869d5..2b4c1489ad 100644 --- a/dev/ci/user-overlays/07819-mattam-ho-matching-occ-sel.sh +++ b/dev/ci/user-overlays/07819-mattam-ho-matching-occ-sel.sh @@ -7,6 +7,7 @@ if [ "$CI_PULL_REQUEST" = "7819" ] || [ "$CI_BRANCH" = "$_OVERLAY_BRANCH" ]; the mtac2_CI_REF="PR7819-overlay" mtac2_CI_GITURL=https://github.com/mattam82/Mtac2 - Equations_CI_REF="PR7819-overlay" + equations_CI_GITURL=https://github.com/mattam82/Coq-Equations + equations_CI_REF="PR7819-overlay" fi -- cgit v1.2.3