From 78a5b30be750c517d529f9f2b8a291699d5d92e6 Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 9 May 2013 18:05:50 +0000 Subject: A uniformization step around understand_* and interp_* functions. - Clarification of the existence of three algorithms for solving unconstrained evars: - the type-class mechanism - the heuristics for solving pending conversion problems and multi-candidates - Declare Implicit Tactic (when called from tactics) Main function for solving unconstrained evars (when not using understand): Pretyping.solve_remaining_evars - Clarification of the existence of three corresponding kinds of errors when reporting about unsolved evars: Main function for checking resolution of evars independently of the understand functions: Pretyping.check_evars_are_solved - Introduction of inference flags in pretyping for governing which combination of the algorithms to use when calling some understand function; there is also a flag of expanding or not evars and for requiring or not the resolution of all evars - Less hackish way of managing Pretyping.type_constraint: all three different possibilities are now represented by three different constructors - Main semantical changes done: - solving unconstrained evars and reporting is not any longer mixed: one first tries to find unconstrained evars by any way possible; one eventually reports on the existence of unsolved evars using check_evars_are_solved - checking unsolved evars is now done by looking at the evar map, not by looking at the evars occurring in the terms to pretype; the only observed consequence so far is in Cases.v because of subterms (surprisingly) disappering after compilation of pattern-matching - the API changed, see dev/doc/changes.txt Still to do: - Find more uniform naming schemes: - for distinguishing when sigma is passed as a reference or as a value (are used: suffix _evars, prefix e_) - for distinguishing when evars are allowed to remain uninstantiated or not (are used: suffix _evars, again, suffix _tcc, infix _open_) - be more consistent on the use of names evd/sigma/evars or evdref/evars - By the way, shouldn't "understand" be better renamed into "infer" or "preinfer", or "pretype". Grammatically, "understanding a term" looks strange. - Investigate whether the inference flags in tacinterp.ml are really what we want (e.g. do we really want that heuristic remains activated when typeclasses are explicitly deactivated, idem in Tacinterp.interp_open_constr where flags are strange). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16499 85f007b7-540e-0410-9357-904b9bb8a0f7 --- proofs/evar_refiner.ml | 10 ++++++++-- proofs/goal.ml | 11 ++++++----- proofs/pfedit.ml | 2 +- proofs/pfedit.mli | 2 +- 4 files changed, 16 insertions(+), 9 deletions(-) (limited to 'proofs') diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index fff4f67b12..0e317e68e5 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -41,8 +41,14 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma = error "Instantiate called on already-defined evar"; let env = Evd.evar_filtered_env evi in let sigma',typed_c = - try Pretyping.understand_ltac ~resolve_classes:true true - sigma env ltac_var (Pretyping.OfType (Some evi.evar_concl)) rawc + let flags = { + Pretyping.use_typeclasses = true; + Pretyping.use_unif_heuristics = true; + Pretyping.use_hook = None; + Pretyping.fail_evar = false; + Pretyping.expand_evars = true } in + try Pretyping.understand_ltac flags + sigma env ltac_var (Pretyping.OfType evi.evar_concl) rawc with e when Errors.noncritical e -> let loc = Glob_ops.loc_of_glob_constr rawc in user_err_loc diff --git a/proofs/goal.ml b/proofs/goal.ml index 6b794c1479..67cd414125 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -111,9 +111,7 @@ let return v _ _ _ _ = v In an ideal world, this could/should be the other way round. As of now, though, it seems at least quite useful to build tactics. *) let interp_constr cexpr env rdefs _ _ = - let (defs,c) = Constrintern.interp_open_constr !rdefs env cexpr in - rdefs := defs ; - c + Constrintern.interp_constr_evars rdefs env cexpr (* Type of constr with holes used by refine. *) (* The list of evars doesn't necessarily contain all the evars in the constr, @@ -217,11 +215,14 @@ module Refinable = struct let init_defs = !rdefs in (* if [check_type] is true, then creates a type constraint for the proof-to-be *) - let tycon = Pretyping.OfType (Option.init check_type (Evd.evar_concl info)) in + let tycon = if check_type then Pretyping.OfType (Evd.evar_concl info) else Pretyping.WithoutTypeConstraint in (* call to [understand_tcc_evars] returns a constr with undefined evars these evars will be our new goals *) + let flags = + if resolve_classes then Pretyping.all_no_fail_flags + else Pretyping.no_classes_no_fail_inference_flags in let open_constr = - Pretyping.understand_tcc_evars ~resolve_classes rdefs env tycon rawc + Pretyping.understand_tcc_evars ~flags rdefs env ~expected_type:tycon rawc in ignore(update_handle handle init_defs !rdefs); open_constr diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index c07db32b75..90f20a7385 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -171,7 +171,7 @@ let implicit_tactic = ref None let declare_implicit_tactic tac = implicit_tactic := Some tac -let solve_by_implicit_tactic env sigma (evk,args) = +let solve_by_implicit_tactic env sigma evk = let evi = Evd.find_undefined sigma evk in match (!implicit_tactic, snd (evar_source evk sigma)) with | Some tac, (Evar_kinds.ImplicitArg _ | Evar_kinds.QuestionMark _) diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 4ca23e7116..73850c6f07 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -174,4 +174,4 @@ val build_by_tactic : env -> types -> tactic -> constr val declare_implicit_tactic : tactic -> unit (* Raise Exit if cannot solve *) -val solve_by_implicit_tactic : env -> Evd.evar_map -> existential -> constr +val solve_by_implicit_tactic : env -> Evd.evar_map -> Evd.evar -> constr -- cgit v1.2.3