diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-23 23:35:02 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-25 18:36:19 +0200 |
| commit | bf018569405c0ae1c5d08dfa27600102b9d77977 (patch) | |
| tree | d8b4435ee65ceb8cd03977748711c13e028c131c | |
| parent | b39465da31bfd488dfad4ea4627186f9a1843e56 (diff) | |
This commit introduces changes in induction and destruct.
The main change is that selection of subterm is made similar whether
the given term is fully applied or not.
- The selection of subterm now works as follows depending on whether
the "at" is given, of whether the subterm is fully applied or not,
and whether there are incompatible subterms matching the pattern. In
particular, we have:
"at" given
| subterm fully applied
| | incompatible subterms
| | |
Y Y - it works like in 8.4
Y N - this was broken in 8.4 ("at" was ineffective and it was finding
all subterms syntactically equal to the first one which matches)
N Y Y it now finds all subterms like the first one which matches
while in 8.4 it used to fail (I hope it is not a too risky in-draft
for a semantics we would regret...) (e.g. "destruct (S _)" on
goal "S x = S y + S x" now selects the two occurrences of "S x"
while it was failing before)
N Y N it works like in 8.4
N N - it works like in 8.4, selecting all subterms like the
first one which matches
- Note that the "historical" semantics, when looking for a subterm, to
select all subterms that syntactically match the first subterm to
match the pattern (looking from left to right) is now internally called
"like first".
- Selection of subterms can now find the type by pattern-matching (useful e.g.
for "induction (nat_rect _ _ _ _)")
- A version of Unification.w_unify w/o any conversion is used for
finding the subterm: it could be easily replaced by an other
matching algorithm.
In particular, "destruct H" now works on a goal such as "H:True -> x<=y |- P y".
Secondary change is in the interpretation of terms with existential
variables:
- When several arguments are given, interpretation is delayed at the
time of execution
- Because we aim at eventually accepting "edestruct c" with unresolved
holes in c, we need the sigma obtained from c to be an extension of
the sigma of the tactics, while before, we just type-checked c
independently of the sigma of the tactic
- Finishing the resolution of evars (using type classes, candidates,
pending conversion problems) is made slightly cleaner: it now takes
three states: a term is evaluated in state sigma, leading to state
sigma' >= sigma, with evars finally solved in state sigma'' >=
sigma'; we solve evars in the diff of sigma' and sigma and report
the solution in sigma''
- We however renounce to give now a success semantics to "edestruct c"
when "c" has unresolved holes, waiting instead for a decision on
what to do in the case of a similar eapply (see mail to coqdev).
An auxiliary change is that an "in" clause can be attached to each component
of a "destruct t, u, v", etc.
Incidentally, make_abstraction does not do evar resolution itself any longer.
36 files changed, 1024 insertions, 327 deletions
@@ -206,6 +206,16 @@ Tactics - Tactics from plugins are now active only when the corresponding module is imported (source of incompatibilities, solvable by adding an "Import", like e.g. "Import Omega"). +- Semantics of destruct/induction has been made more regular in some + edge cases, possibly leading to incompatibilies: + - new goals are now opened when the term does not match a subterm of + the goal and has unresolved holes, while in 8.4 these holes were + turned into existential variables + - when no "at" option is given, the historical semantics which + selects all subterms syntactically identical to the first subterm + matching the given pattern is used + - non-dependent destruct/induction on an hypothesis with premisses in + an inductive type with indices is fixed Program diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4 index 1eadf7dfd..816502c1e 100644 --- a/grammar/q_coqast.ml4 +++ b/grammar/q_coqast.ml4 @@ -367,17 +367,18 @@ let rec mlexpr_of_atomic_tactic = function (* Derived basic tactics *) | Tacexpr.TacInductionDestruct (isrec,ev,l) -> <:expr< Tacexpr.TacInductionDestruct $mlexpr_of_bool isrec$ $mlexpr_of_bool ev$ - $mlexpr_of_triple + $mlexpr_of_pair (mlexpr_of_list - (mlexpr_of_pair - (mlexpr_of_pair + (mlexpr_of_triple + (mlexpr_of_pair (mlexpr_of_option mlexpr_of_bool) - mlexpr_of_induction_arg) + mlexpr_of_induction_arg) (mlexpr_of_pair (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern_naming)) - (mlexpr_of_option (mlexpr_of_intro_pattern_disjunctive))))) + (mlexpr_of_option (mlexpr_of_intro_pattern_disjunctive))) + (mlexpr_of_option mlexpr_of_clause))) (mlexpr_of_option mlexpr_of_constr_with_binding) - (mlexpr_of_option mlexpr_of_clause) l$ >> + l$ >> (* Context management *) | Tacexpr.TacClear (b,l) -> diff --git a/intf/locus.mli b/intf/locus.mli index e0ce43331..35b738064 100644 --- a/intf/locus.mli +++ b/intf/locus.mli @@ -86,3 +86,9 @@ type goal_location = hyp_location option the conclusion (conclusion is represented by None) *) type simple_clause = Id.t option list + +(** {6 A notion of occurrences allowing to express "all occurrences + convertible to the first which matches"} *) + +type 'a or_like_first = AtOccs of 'a | LikeFirst + diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 2967c10dd..c8c7e28e9 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -56,15 +56,15 @@ type 'id message_token = | MsgInt of int | MsgIdent of 'id -type 'constr induction_clause = +type ('constr,'id) induction_clause = 'constr with_bindings induction_arg * (intro_pattern_naming_expr located option (* eqn:... *) * 'constr or_and_intro_pattern_expr located or_var option) (* as ... *) + * 'id clause_expr option (* in ... *) type ('constr,'id) induction_clause_list = - 'constr induction_clause list + ('constr,'id) induction_clause list * 'constr with_bindings option (* using ... *) - * 'id clause_expr option (* in ... *) type 'a with_bindings_arg = clear_flag * 'a with_bindings diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 80edccfeb..25dd0db45 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -136,19 +136,19 @@ let induction_arg_of_constr (c,lbind as clbind) = match lbind with | _ -> ElimOnConstr clbind let mkTacCase with_evar = function - | [(clear,ElimOnConstr cl),(None,None)],None,None -> + | [(clear,ElimOnConstr cl),(None,None),None],None -> TacCase (with_evar,(clear,cl)) (* Reinterpret numbers as a notation for terms *) - | [(clear,ElimOnAnonHyp n),(None,None)],None,None -> + | [(clear,ElimOnAnonHyp n),(None,None),None],None -> TacCase (with_evar, (clear,(CPrim (Loc.ghost, Numeral (Bigint.of_int n)), NoBindings))) (* Reinterpret ident as notations for variables in the context *) (* because we don't know if they are quantified or not *) - | [(clear,ElimOnIdent id),(None,None)],None,None -> + | [(clear,ElimOnIdent id),(None,None),None],None -> TacCase (with_evar,(clear,(CRef (Ident id,None),NoBindings))) | ic -> - if List.exists (function ((_, ElimOnAnonHyp _),_) -> true | _ -> false) (pi1 ic) + if List.exists (function ((_, ElimOnAnonHyp _),_,_) -> true | _ -> false) (fst ic) then error "Use of numbers as direct arguments of 'case' is not supported."; TacInductionDestruct (false,with_evar,ic) @@ -520,11 +520,17 @@ GEXTEND Gram [ [ b = orient; p = rewriter -> let (m,c) = p in (b,m,c) ] ] ; induction_clause: - [ [ c = induction_arg; pat = as_or_and_ipat; eq = eqn_ipat -> (c,(eq,pat)) ] ] + [ [ c = induction_arg; pat = as_or_and_ipat; eq = eqn_ipat; cl = opt_clause + -> (c,(eq,pat),cl) ] ] ; induction_clause_list: - [ [ ic = LIST1 induction_clause SEP ","; - el = OPT eliminator; cl = opt_clause -> (ic,el,cl) ] ] + [ [ ic = LIST1 induction_clause SEP ","; el = OPT eliminator; + cl_tolerance = opt_clause -> + (* Condition for accepting "in" at the end by compatibility *) + match ic,el,cl_tolerance with + | [c,pat,None],Some _,Some _ -> ([c,pat,cl_tolerance],el) + | _,_,Some _ -> err () + | _,_,None -> (ic,el) ]] ; move_location: [ [ IDENT "after"; id = id_or_meta -> MoveAfter id @@ -613,6 +619,13 @@ GEXTEND Gram l = LIST0 [","; c = pattern_occ; na = as_name -> (c,na)] -> TacAtom (!@loc, TacGeneralize (((nl,c),na)::l)) | IDENT "generalize"; IDENT "dependent"; c = constr -> TacAtom (!@loc, TacGeneralizeDep c) +(* Towards a "generalize in" which generalize in place: problem: this is somehow inconsistent with "generalize at" (from 8.2) which is not in place. + | IDENT "generalize"; c = constr; "in"; cl = in_clause; + na = as_name; + l = LIST0 [","; c = constr; "in"; cl = in_clause; na = as_name -> + ((cl,c),na)] -> + TacGeneralize (true,((cl,c),na)::l) +*) (* Derived basic tactics *) | IDENT "induction"; ic = induction_clause_list -> diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 71ebf4923..d1747eed6 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -25,9 +25,7 @@ let is_rec_info scheme_info = List.fold_left_i test_branche 1 false (List.rev scheme_info.Tactics.branches) let choose_dest_or_ind scheme_info = - if is_rec_info scheme_info - then Tactics.induction false - else Tactics.destruct false + Tactics.induction_destruct (is_rec_info scheme_info) false let functional_induction with_clean c princl pat = Dumpglob.pause (); @@ -80,7 +78,10 @@ let functional_induction with_clean c princl pat = if princ_infos.Tactics.farg_in_concl then [c] else [] in - List.map (fun c -> None,Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))) (args@c_list) + let encoded_pat_as_patlist = + List.make (List.length args + List.length c_list - 1) None @ [pat] in + List.map2 (fun c pat -> ((None,Tacexpr.ElimOnConstr (fun env sigma -> sigma,(c,NoBindings))),(None,pat),None)) + (args@c_list) encoded_pat_as_patlist in let princ' = Some (princ,bindings) in let princ_vars = @@ -113,10 +114,7 @@ let functional_induction with_clean c princl pat = Tacticals.tclTHEN (Proofview.V82.of_tactic (choose_dest_or_ind princ_infos - args_as_induction_constr - princ' - (None,pat) - None)) + (args_as_induction_constr,princ'))) subst_and_reduce g in diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 93d47d6b1..9022db79f 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -1600,6 +1600,11 @@ let dependent_evar_ident ev evd = | _ -> anomaly (str "Not an evar resulting of a dependent binding") (*******************************************************************) + +type pending = (* before: *) evar_map * (* after: *) evar_map + +type pending_constr = pending * constr + type open_constr = evar_map * constr (*******************************************************************) diff --git a/pretyping/evd.mli b/pretyping/evd.mli index cc64b3594..8acf81175 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -575,10 +575,16 @@ val eq_constr_univs_test : evar_map -> constr -> constr -> bool (** Syntactic equality up to universes, throwing away the (consistent) constraints in case of success. *) -(******************************************************************** - constr with holes *) +(********************************************************************) +(* constr with holes and pending resolution of classes, conversion *) +(* problems, candidates, etc. *) + +type pending = (* before: *) evar_map * (* after: *) evar_map + +type pending_constr = pending * constr + +type open_constr = evar_map * constr (* Special case when before is empty *) -type open_constr = evar_map * constr (** Partially constructed constrs. *) type unsolvability_explanation = SeveralInstancesFound of int diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml index d8698a165..2ffbee4d0 100644 --- a/pretyping/find_subterm.ml +++ b/pretyping/find_subterm.ml @@ -50,8 +50,7 @@ let check_used_occurrences nbocc (nowhere_except_in,locs) = let proceed_with_occurrences f occs x = match occs with | NoOccurrences -> x - | _ -> - (* TODO FINISH ADAPTING WITH HUGO *) + | occs -> let plocs = Locusops.convert_occs occs in assert (List.for_all (fun x -> x >= 0) (snd plocs)); let (nbocc,x) = f 1 x in @@ -85,7 +84,7 @@ type 'a testing_function = { match_fun : 'a -> constr -> 'a; merge_fun : 'a -> 'a -> 'a; mutable testing_state : 'a; - mutable last_found : ((Id.t * hyp_location_flag) option * int * constr) option + mutable last_found : position_reporting option } (* Find subterms using a testing function, but only at a list of @@ -93,7 +92,76 @@ type 'a testing_function = { (b,l), b=true means no occurrence except the ones in l and b=false, means all occurrences except the ones in l *) -let replace_term_occ_gen_modulo occs test bywhat cl occ t = +(* +type 'a loc_state = { + hyp_location : (Id.t * hyp_location_flag) option; + maxocc : bool * int; + locs : occurrences; + current : int; + like_first : bool +} + +let all_found pos = + let nowhere_except_in, maxocc = pos.maxocc in + nowhere_except_in && pos.current > maxocc + +let is_selected pos = Locusops.is_selected pos.current pos.locs + +let incr pos = pos := { !pos with current = (!pos).current + 1 } + +let make_current_pos cl pos = function + | AtOccs occs -> + let nowhere_except_in,locs = Locusops.convert_occs occs in + let maxocc = List.fold_right max locs 0 in + { hyp_location = cl; + maxocc = (nowhere_except_in,maxocc); + locs = occs; + current = pos; + like_first = false } + | LikeFirst -> + { hyp_location = None; + maxocc = (false,max_int); + locs = AllOccurrences; + current = pos; + like_first = true } + +let extract pos = (pos.hyp_location,pos.current) + +let like_first pos = pos.like_first + +let replace_term_occ_gen_modulo occs test bywhat cl pos t = + let nested = ref false in + let currentpos = ref (make_current_pos cl pos occs) in + let add_subst t subst = + try + test.testing_state <- test.merge_fun subst test.testing_state; + test.last_found <- Some (extract !currentpos,t) + with NotUnifiable e when not (like_first !currentpos) -> + let lastpos = Option.get test.last_found in + raise + (SubtermUnificationError (!nested,(extract !currentpos,t),lastpos,e)) in + let rec substrec k t = + if all_found !currentpos then (* shortcut *) t else + try + let subst = test.match_fun test.testing_state t in + if is_selected !currentpos then + (add_subst t subst; incr currentpos; + (* Check nested matching subterms *) + nested := true; ignore (subst_below k t); nested := false; + (* Do the effective substitution *) + Vars.lift k (bywhat ())) + else + (incr currentpos; subst_below k t) + with NotUnifiable _ -> + subst_below k t + and subst_below k t = + map_constr_with_binders_left_to_right (fun d k -> k+1) substrec k t + in + let t' = substrec 0 t in + (!currentpos, t') +*) + +let replace_term_occ_gen_modulo occs like_first test bywhat cl occ t = let (nowhere_except_in,locs) = Locusops.convert_occs occs in let maxocc = List.fold_right max locs 0 in let pos = ref occ in @@ -101,10 +169,10 @@ let replace_term_occ_gen_modulo occs test bywhat cl occ t = let add_subst t subst = try test.testing_state <- test.merge_fun subst test.testing_state; - test.last_found <- Some (cl,!pos,t) - with NotUnifiable e -> + test.last_found <- Some ((cl,!pos),t) + with NotUnifiable e when not like_first -> let lastpos = Option.get test.last_found in - raise (SubtermUnificationError (!nested,(cl,!pos,t),lastpos,e)) in + raise (SubtermUnificationError (!nested,((cl,!pos),t),lastpos,e)) in let rec substrec k t = if nowhere_except_in && !pos > maxocc then t else if not (Vars.closed0 t) then subst_below k t else @@ -127,13 +195,17 @@ let replace_term_occ_gen_modulo occs test bywhat cl occ t = (!pos, t') let replace_term_occ_modulo occs test bywhat t = + let occs',like_first = + match occs with AtOccs occs -> occs,false | LikeFirst -> AllOccurrences,true in proceed_with_occurrences - (replace_term_occ_gen_modulo occs test bywhat None) occs t + (replace_term_occ_gen_modulo occs' like_first test bywhat None) occs' t -let replace_term_occ_decl_modulo (plocs,hyploc) test bywhat d = +let replace_term_occ_decl_modulo occs test bywhat d = + let (plocs,hyploc),like_first = + match occs with AtOccs occs -> occs,false | LikeFirst -> (AllOccurrences,InHyp),true in proceed_with_occurrences (map_named_declaration_with_hyploc - (replace_term_occ_gen_modulo plocs test bywhat) + (replace_term_occ_gen_modulo plocs like_first test bywhat) hyploc) plocs d @@ -157,11 +229,13 @@ let subst_closed_term_occ env evd occs c t = let t' = replace_term_occ_modulo occs test bywhat t in t', test.testing_state -let subst_closed_term_occ_decl env evd (plocs,hyploc) c d = +let subst_closed_term_occ_decl env evd occs c d = let test = make_eq_univs_test env evd c in + let (plocs,hyploc),like_first = + match occs with AtOccs occs -> occs,false | LikeFirst -> (AllOccurrences,InHyp),true in let bywhat () = mkRel 1 in proceed_with_occurrences (map_named_declaration_with_hyploc - (fun _ -> replace_term_occ_gen_modulo plocs test bywhat None) + (fun _ -> replace_term_occ_gen_modulo plocs like_first test bywhat None) hyploc) plocs d, test.testing_state diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli index b24c95807..ea1ce6228 100644 --- a/pretyping/find_subterm.mli +++ b/pretyping/find_subterm.mli @@ -26,11 +26,12 @@ exception SubtermUnificationError of subterm_unification_error function to merge substitutions and an initial substitution; last_found is used for error messages and it has to be initialized with None. *) + type 'a testing_function = { match_fun : 'a -> constr -> 'a; merge_fun : 'a -> 'a -> 'a; mutable testing_state : 'a; - mutable last_found : ((Id.t * hyp_location_flag) option * int * constr) option + mutable last_found : position_reporting option } (** This is the basic testing function, looking for exact matches of a @@ -42,25 +43,26 @@ val make_eq_univs_test : env -> evar_map -> constr -> evar_map testing_function matching subterms at the indicated occurrences [occl] with [mk ()]; it turns a NotUnifiable exception raised by the testing function into a SubtermUnificationError. *) -val replace_term_occ_modulo : - occurrences -> 'a testing_function -> (unit -> constr) -> constr -> constr +val replace_term_occ_modulo : occurrences or_like_first -> + 'a testing_function -> (unit -> constr) -> constr -> constr (** [replace_term_occ_decl_modulo] is similar to [replace_term_occ_modulo] but for a named_declaration. *) val replace_term_occ_decl_modulo : - occurrences * hyp_location_flag -> 'a testing_function -> (unit -> constr) -> + (occurrences * hyp_location_flag) or_like_first -> + 'a testing_function -> (unit -> constr) -> named_declaration -> named_declaration (** [subst_closed_term_occ occl c d] replaces occurrences of closed [c] at positions [occl] by [Rel 1] in [d] (see also Note OCC), unifying universes which results in a set of constraints. *) -val subst_closed_term_occ : env -> evar_map -> occurrences -> constr -> - constr -> constr * evar_map +val subst_closed_term_occ : env -> evar_map -> occurrences or_like_first -> + constr -> constr -> constr * evar_map (** [subst_closed_term_occ_decl evd occl c decl] replaces occurrences of closed [c] at positions [occl] by [Rel 1] in [decl]. *) val subst_closed_term_occ_decl : env -> evar_map -> - occurrences * hyp_location_flag -> + (occurrences * hyp_location_flag) or_like_first -> constr -> named_declaration -> named_declaration * evar_map (** Miscellaneous *) diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml index 5484c8095..21157d9d5 100644 --- a/pretyping/locusops.ml +++ b/pretyping/locusops.ml @@ -87,17 +87,22 @@ let out_arg = function | Misctypes.ArgVar _ -> Errors.anomaly (Pp.str "Unevaluated or_var variable") | Misctypes.ArgArg x -> x -let occurrences_of_hyp id cls = +let occurrences_of_hyp id =function + | LikeFirst -> LikeFirst + | AtOccs cls -> let rec hyp_occ = function [] -> NoOccurrences, InHyp | ((occs,id'),hl)::_ when Names.Id.equal id id' -> occurrences_map (List.map out_arg) occs, hl | _::l -> hyp_occ l in - match cls.onhyps with + AtOccs (match cls.onhyps with None -> AllOccurrences,InHyp - | Some l -> hyp_occ l + | Some l -> hyp_occ l) -let occurrences_of_goal cls = - occurrences_map (List.map out_arg) cls.concl_occs +let occurrences_of_goal = function + | LikeFirst -> LikeFirst + | AtOccs cls -> AtOccs (occurrences_map (List.map out_arg) cls.concl_occs) -let in_every_hyp cls = Option.is_empty cls.onhyps +let in_every_hyp = function + | LikeFirst -> true + | AtOccs cls -> Option.is_empty cls.onhyps diff --git a/pretyping/locusops.mli b/pretyping/locusops.mli index 73d13c0bc..f6d27a185 100644 --- a/pretyping/locusops.mli +++ b/pretyping/locusops.mli @@ -38,7 +38,7 @@ val concrete_clause_of : (unit -> Id.t list) -> clause -> concrete_clause (** Miscellaneous functions *) -val occurrences_of_hyp : Id.t -> Id.t clause_expr -> - occurrences * hyp_location_flag -val occurrences_of_goal : 'a clause_expr -> occurrences -val in_every_hyp : 'a clause_expr -> bool +val occurrences_of_hyp : Id.t -> clause or_like_first -> + (occurrences * hyp_location_flag) or_like_first +val occurrences_of_goal : clause or_like_first -> occurrences or_like_first +val in_every_hyp : clause or_like_first -> bool diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index e16d1206a..99b5a51f9 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -23,9 +23,11 @@ type unification_error = | InstanceNotSameType of existential_key * env * types * types | UnifUnivInconsistency of Univ.univ_inconsistency -type position =(Id.t * Locus.hyp_location_flag) option +type position = (Id.t * Locus.hyp_location_flag) option -type subterm_unification_error = bool * (position * int * constr) * (position * int * constr) * (constr * constr * unification_error) option +type position_reporting = (position * int) * constr + +type subterm_unification_error = bool * position_reporting * position_reporting * (constr * constr * unification_error) option type pretype_error = (* Old Case *) diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index b74ca1936..5882d8b9c 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -24,9 +24,11 @@ type unification_error = | InstanceNotSameType of existential_key * env * types * types | UnifUnivInconsistency of Univ.univ_inconsistency -type position =(Id.t * Locus.hyp_location_flag) option +type position = (Id.t * Locus.hyp_location_flag) option -type subterm_unification_error = bool * (position * int * constr) * (position * int * constr) * (constr * constr * unification_error) option +type position_reporting = (position * int) * constr + +type subterm_unification_error = bool * position_reporting * position_reporting * (constr * constr * unification_error) option type pretype_error = (** Old Case *) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 5383101b4..6dbf7915b 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -142,19 +142,27 @@ type inference_flags = { expand_evars : bool } -let apply_typeclasses env evdref fail_evar = +let fold_pending_holes f (sigma,sigma') = + Evd.fold_undefined + (fun evk _ acc -> if Evd.mem sigma evk then acc else f evk acc) + sigma' + +let is_pending_hole (sigma,sigma') evk = + Evd.is_undefined sigma' evk && not (Evd.mem sigma evk) + +let apply_typeclasses env evdref pending fail_evar = evdref := Typeclasses.resolve_typeclasses ~filter:(if Flags.is_program_mode () - then Typeclasses.no_goals_or_obligations else Typeclasses.no_goals) + then (fun evk evi -> is_pending_hole pending evk && Typeclasses.no_goals_or_obligations evk evi) + else (fun evk evi -> is_pending_hole pending evk && Typeclasses.no_goals evk evi)) ~split:true ~fail:fail_evar env !evdref; if Flags.is_program_mode () then (* Try optionally solving the obligations *) evdref := Typeclasses.resolve_typeclasses - ~filter:Typeclasses.all_evars ~split:true ~fail:false env !evdref + ~filter:(fun evk evi -> is_pending_hole pending evk && Typeclasses.all_evars evk evi) ~split:true ~fail:false env !evdref -let apply_inference_hook hook initial_sigma evdref = - evdref := fold_undefined (fun evk evi sigma -> - if not (Evd.mem initial_sigma evk) && - is_undefined sigma evk (* i.e. not defined by side-effect *) +let apply_inference_hook hook evdref pending = + evdref := fold_pending_holes (fun evk sigma -> + if Evd.is_undefined sigma evk (* in particular not defined by side-effect *) then try let c = hook sigma evk in @@ -162,7 +170,7 @@ let apply_inference_hook hook initial_sigma evdref = with Exit -> sigma else - sigma) !evdref !evdref + sigma) pending !evdref let apply_heuristics env evdref fail_evar = (* Resolve eagerly, potentially making wrong choices *) @@ -171,39 +179,39 @@ let apply_heuristics env evdref fail_evar = with e when Errors.noncritical e -> let e = Errors.push e in if fail_evar then raise e -let check_typeclasses_instances_are_solved env sigma = +let check_typeclasses_instances_are_solved env current_sigma pending = (* Naive way, call resolution again with failure flag *) - apply_typeclasses env (ref sigma) true + apply_typeclasses env (ref current_sigma) pending true -let check_extra_evars_are_solved env initial_sigma sigma = - Evd.fold_undefined - (fun evk evi () -> - if not (Evd.mem initial_sigma evk) then - let (loc,k) = evar_source evk sigma in +let check_extra_evars_are_solved env current_sigma pending = + fold_pending_holes + (fun evk () -> + if not (Evd.is_defined current_sigma evk) then + let (loc,k) = evar_source evk current_sigma in match k with | Evar_kinds.ImplicitArg (gr, (i, id), false) -> () | _ -> - let evi = nf_evar_info sigma (Evd.find_undefined sigma evk) in - error_unsolvable_implicit loc env sigma evi k None) sigma () + let evi = nf_evar_info current_sigma (Evd.find_undefined current_sigma evk) in + error_unsolvable_implicit loc env current_sigma evi k None) pending () -let check_evars_are_solved env initial_sigma sigma = - check_typeclasses_instances_are_solved env sigma; - check_problems_are_solved env sigma; - check_extra_evars_are_solved env initial_sigma sigma +let check_evars_are_solved env current_sigma pending = + check_typeclasses_instances_are_solved env current_sigma pending; + check_problems_are_solved env current_sigma; + check_extra_evars_are_solved env current_sigma pending (* Try typeclasses, hooks, unification heuristics ... *) -let solve_remaining_evars flags env initial_sigma sigma = - let evdref = ref sigma in - if flags.use_typeclasses then apply_typeclasses env evdref false; +let solve_remaining_evars flags env current_sigma pending = + let evdref = ref current_sigma in + if flags.use_typeclasses then apply_typeclasses env evdref pending false; if Option.has_some flags.use_hook then - apply_inference_hook (Option.get flags.use_hook env) initial_sigma evdref; + apply_inference_hook (Option.get flags.use_hook env) evdref pending; if flags.use_unif_heuristics then apply_heuristics env evdref false; - if flags.fail_evar then check_evars_are_solved env initial_sigma !evdref; + if flags.fail_evar then check_evars_are_solved env !evdref pending; !evdref let process_inference_flags flags env initial_sigma (sigma,c) = - let sigma = solve_remaining_evars flags env initial_sigma sigma in + let sigma = solve_remaining_evars flags env sigma (initial_sigma,sigma) in let c = if flags.expand_evars then nf_evar sigma c else c in sigma,c diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 5df4c8372..eb5626474 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -108,14 +108,17 @@ val understand_judgment_tcc : env -> evar_map ref -> (** Trying to solve remaining evars and remaining conversion problems with type classes, heuristics, and possibly an external solver *) +(* For simplicity, it is assumed that current map has no other evars + with candidate and no other conversion problems that the one in + [pending], however, it can contain more evars than the pending ones. *) val solve_remaining_evars : inference_flags -> - env -> (* initial map *) evar_map -> (* map to solve *) evar_map -> evar_map + env -> (* initial map *) evar_map -> (* map to solve *) pending -> evar_map (** Checking evars are all solved and reporting an appropriate error message *) val check_evars_are_solved : - env -> (* initial map: *) evar_map -> (* map to check: *) evar_map -> unit + env -> (* current map: *) evar_map -> (* map to check: *) pending -> unit (**/**) (** Internal of Pretyping... *) diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index b2938cb99..d86da79d6 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1131,7 +1131,7 @@ let abstract_scheme env (locc,a) (c, sigma) = if occur_meta a then mkLambda (na,ta,c), sigma else - let c', sigma' = subst_closed_term_occ env sigma locc a c in + let c', sigma' = subst_closed_term_occ env sigma (AtOccs locc) a c in mkLambda (na,ta,c'), sigma' let pattern_occs loccs_trm env sigma c = diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 527199e3b..2f1c230b7 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -90,7 +90,7 @@ let abstract_scheme env evd c l lname_typ = let abstract_list_all env evd typ c l = let ctxt,_ = splay_prod_n env evd (List.length l) typ in - let l_with_all_occs = List.map (function a -> (AllOccurrences,a)) l in + let l_with_all_occs = List.map (function a -> (LikeFirst,a)) l in let p,evd = abstract_scheme env evd c l_with_all_occs ctxt in let evd,typp = try Typing.e_type_of env evd p @@ -1362,9 +1362,10 @@ let indirectly_dependent c d decls = let indirect_dependency d decls = pi1 (List.hd (List.filter (fun (id,_,_) -> dependent_in_decl (mkVar id) d) decls)) -let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env initial_sigma (sigma,c) = - let sigma = Pretyping.solve_remaining_evars flags env initial_sigma sigma - in Evd.evar_universe_context sigma, nf_evar sigma c +let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sigma (pending,c) = + let sigma = Pretyping.solve_remaining_evars flags env current_sigma pending in + let sigma, subst = nf_univ_variables sigma in + sigma, subst_univs_constr subst (nf_evar sigma c) let default_matching_core_flags sigma = let ts = Names.full_transparent_state in { @@ -1394,7 +1395,7 @@ let default_matching_merge_flags sigma = use_pattern_unification = true; } -let default_matching_flags sigma = +let default_matching_flags (sigma,_) = let flags = default_matching_core_flags sigma in { core_unify_flags = flags; merge_unify_flags = default_matching_merge_flags sigma; @@ -1404,12 +1405,35 @@ let default_matching_flags sigma = } (* This supports search of occurrences of term from a pattern *) +(* from_prefix is useful e.g. for subterms in an inductive type: we can say *) +(* "destruct t" and it finds "t u" *) -let make_pattern_test inf_flags env sigma0 (sigma,c) = - let flags = default_matching_flags sigma0 in +exception PatternNotFound + +let make_pattern_test from_prefix_of_ind env sigma (pending,c) = + let flags = default_matching_flags pending in + let n = List.length (snd (decompose_app c)) in let matching_fun _ t = - try let sigma = w_typed_unify env sigma Reduction.CONV flags c t in - Some(sigma, t) + try + let t' = + if from_prefix_of_ind then + (* We check for fully applied subterms of the form "u u1 .. un" *) + (* of inductive type knowning only a prefix "u u1 .. ui" *) + let t,l = decompose_app t in + let l1,l2 = + try List.chop n l with Failure _ -> raise (NotUnifiable None) in + if not (List.for_all closed0 l2) then raise (NotUnifiable None) + else + applist (t,l1) + else t in + let sigma = w_typed_unify env sigma Reduction.CONV flags c t' in + let _ = + if from_prefix_of_ind then + (* We check that the subterm we found from prefix is applied *) + (* enough to be of inductive type *) + try ignore (Inductiveops.find_mrectype env sigma (Retyping.get_type_of env sigma t)) + with UserError _ -> raise (NotUnifiable None) in + Some(sigma, t) with | PretypeError (_,_,CannotUnify (c1,c2,Some e)) -> raise (NotUnifiable (Some (c1,c2,e))) @@ -1425,22 +1449,25 @@ let make_pattern_test inf_flags env sigma0 (sigma,c) = { match_fun = matching_fun; merge_fun = merge_fun; testing_state = None; last_found = None }, (fun test -> match test.testing_state with - | None -> - finish_evar_resolution ~flags:inf_flags env sigma0 (sigma,c) + | None -> None +(* + let sigma, c = finish_evar_resolution ~flags:inf_flags env sigma (pending,c) in + sigma,c +*) | Some (sigma,_) -> + let c = nf_evar sigma (local_strong whd_meta sigma c) in let univs, subst = nf_univ_variables sigma in - Evd.evar_universe_context univs, - subst_univs_constr subst (nf_evar sigma c)) + Some (sigma,subst_univs_constr subst c)) let make_eq_test env evd c = let out cstr = - Evd.evar_universe_context cstr.testing_state, c + match cstr.last_found with None -> None | _ -> Some (cstr.testing_state, c) in - (make_eq_univs_test env evd c, out) + (make_eq_univs_test env evd c, out) -let make_abstraction_core name (test,out) (sigmac,c) ty occs check_occs env concl = +let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = let id = - let t = match ty with Some t -> t | None -> get_type_of env sigmac c in + let t = match ty with Some t -> t | None -> get_type_of env sigma c in let x = id_of_name_using_hdchar (Global.env()) t name in let ids = ids_of_named_context (named_context env) in if name == Anonymous then next_ident_away_in_goal x ids else @@ -1450,9 +1477,9 @@ let make_abstraction_core name (test,out) (sigmac,c) ty occs check_occs env conc x in let mkvarid () = mkVar id in - let compute_dependency _ (hyp,_,_ as d) depdecls = + let compute_dependency _ (hyp,_,_ as d) (sign,depdecls) = match occurrences_of_hyp hyp occs with - | NoOccurrences, InHyp -> + | AtOccs (NoOccurrences, InHyp) -> if indirectly_dependent c d depdecls then (* Told explicitly not to abstract over [d], but it is dependent *) let id' = indirect_dependency d depdecls in @@ -1460,31 +1487,34 @@ let make_abstraction_core name (test,out) (sigmac,c) ty occs check_occs env conc ++ str " without also abstracting or erasing " ++ Nameops.pr_id hyp ++ str ".") else - depdecls - | (AllOccurrences, InHyp) as occ -> + (push_named_context_val d sign,depdecls) + | (AtOccs (AllOccurrences, InHyp) | LikeFirst) as occ -> let newdecl = replace_term_occ_decl_modulo occ test mkvarid d in if Context.eq_named_declaration d newdecl && not (indirectly_dependent c d depdecls) then if check_occs && not (in_every_hyp occs) - then raise (PretypeError (env,sigmac,NoOccurrenceFound (c,Some hyp))) - else depdecls + then raise (PretypeError (env,sigma,NoOccurrenceFound (c,Some hyp))) + else (push_named_context_val d sign, depdecls) else - newdecl :: depdecls + (push_named_context_val newdecl sign, newdecl :: depdecls) | occ -> - replace_term_occ_decl_modulo occ test mkvarid d :: depdecls in + let newdecl = replace_term_occ_decl_modulo occ test mkvarid d in + (push_named_context_val newdecl sign, newdecl :: depdecls) in try - let depdecls = fold_named_context compute_dependency env ~init:[] in + let sign,depdecls = + fold_named_context compute_dependency env + ~init:(empty_named_context_val,[]) in let ccl = match occurrences_of_goal occs with - | NoOccurrences -> concl + | AtOccs NoOccurrences -> concl | occ -> replace_term_occ_modulo occ test mkvarid concl in let lastlhyp = if List.is_empty depdecls then None else Some (pi1(List.last depdecls)) in - (id,depdecls,lastlhyp,ccl,out test) + (id,sign,depdecls,lastlhyp,ccl,out test) with SubtermUnificationError e -> - raise (PretypeError (env,sigmac,CannotUnifyOccurrences e)) + raise (PretypeError (env,sigma,CannotUnifyOccurrences e)) (** [make_abstraction] is the main entry point to abstract over a term or pattern at some occurrences; it returns: @@ -1497,22 +1527,27 @@ let make_abstraction_core name (test,out) (sigmac,c) ty occs check_occs env conc - the term or pattern to abstract fully instantiated *) +type prefix_of_inductive_support_flag = bool + type abstraction_request = -| AbstractPattern of Name.t * (evar_map * constr) * clause * bool * Pretyping.inference_flags +| AbstractPattern of prefix_of_inductive_support_flag * Name.t * pending_constr * clause or_like_first * bool | AbstractExact of Name.t * constr * types option * clause * bool type abstraction_result = - Names.Id.t * Context.named_declaration list * Names.Id.t option * - constr * (Evd.evar_universe_context * constr) + Names.Id.t * named_context_val * + Context.named_declaration list * Names.Id.t option * + types * (Evd.evar_map * constr) option let make_abstraction env evd ccl abs = match abs with - | AbstractPattern (name,c,occs,check_occs,flags) -> + | AbstractPattern (from_prefix,name,c,occs,check_occs) -> make_abstraction_core name - (make_pattern_test flags env evd c) c None occs check_occs env ccl + (make_pattern_test from_prefix env evd c) + env evd (snd c) None occs check_occs ccl | AbstractExact (name,c,ty,occs,check_occs) -> make_abstraction_core name - (make_eq_test env evd c) (evd,c) ty occs check_occs env ccl + (make_eq_test env evd c) + env evd c ty (AtOccs occs) check_occs ccl let keyed_unify env evd kop = if not !keyed_unification then fun cl -> true diff --git a/pretyping/unification.mli b/pretyping/unification.mli index bedd6bf16..3b4998129 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -45,7 +45,7 @@ val elim_no_delta_flags : unit -> unify_flags val w_unify : env -> evar_map -> conv_pb -> ?flags:unify_flags -> constr -> constr -> evar_map -(** [w_unify_to_subterm env (c,t) m] performs unification of [c] with a +(** [w_unify_to_subterm env m (c,t)] performs unification of [c] with a subterm of [t]. Constraints are added to [m] and the matched subterm of [t] is also returned. *) val w_unify_to_subterm : @@ -63,20 +63,25 @@ val w_coerce_to_type : env -> evar_map -> constr -> types -> types -> (* Looking for subterms in contexts at some occurrences, possibly with pattern*) +exception PatternNotFound + type abstraction_request = -| AbstractPattern of Names.Name.t * (evar_map * constr) * Locus.clause * bool * Pretyping.inference_flags +| AbstractPattern of bool * Names.Name.t * pending_constr * Locus.clause Locus.or_like_first * bool | AbstractExact of Names.Name.t * constr * types option * Locus.clause * bool val finish_evar_resolution : ?flags:Pretyping.inference_flags -> - env -> Evd.evar_map -> open_constr -> Evd.evar_universe_context * constr + env -> Evd.evar_map -> pending_constr -> Evd.evar_map * constr type abstraction_result = - Names.Id.t * Context.named_declaration list * Names.Id.t option * - constr * (Evd.evar_universe_context * constr) + Names.Id.t * named_context_val * + Context.named_declaration list * Names.Id.t option * + types * (Evd.evar_map * constr) option val make_abstraction : env -> Evd.evar_map -> constr -> abstraction_request -> abstraction_result +val pose_all_metas_as_evars : env -> evar_map -> constr -> evar_map * constr + (*i This should be in another module i*) (** [abstract_list_all env evd t c l] diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 9b27f9c7b..e6fda4b59 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -771,14 +771,14 @@ and pr_atom1 = function ++ str "in" ++ pr_hyp_location pr.pr_name (id,[],(hloc,ref None))) *) (* Derived basic tactics *) - | TacInductionDestruct (isrec,ev,(l,el,cl)) -> + | TacInductionDestruct (isrec,ev,(l,el)) -> hov 1 (str (with_evars ev (if isrec then "induction" else "destruct")) ++ spc () ++ - prlist_with_sep pr_comma (fun ((clear_flag,h),ids) -> + prlist_with_sep pr_comma (fun ((clear_flag,h),ids,cl) -> pr_clear_flag clear_flag (pr_induction_arg pr.pr_constr pr.pr_lconstr) h ++ - pr_with_induction_names pr.pr_constr ids) l ++ - pr_opt pr_eliminator el ++ - pr_opt_no_spc (pr_clauses None pr.pr_name) cl) + pr_with_induction_names pr.pr_constr ids ++ + pr_opt_no_spc (pr_clauses None pr.pr_name) cl) l ++ + pr_opt pr_eliminator el) | TacDoubleInduction (h1,h2) -> hov 1 (str "double induction" ++ diff --git a/proofs/clenv.ml b/proofs/clenv.ml index d852a0278..fb5a76bd3 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -118,13 +118,13 @@ let clenv_environments evd bound t = in clrec (evd,[]) bound t -let mk_clenv_from_env environ sigma n (c,cty) = +let mk_clenv_from_env env sigma n (c,cty) = let evd = create_goal_evar_defs sigma in let (evd,args,concl) = clenv_environments evd n cty in { templval = mk_freelisted (applist (c,args)); templtyp = mk_freelisted concl; evd = evd; - env = environ } + env = env } let mk_clenv_from_n gls n (c,cty) = mk_clenv_from_env (pf_env gls) gls.sigma n (c, cty) @@ -532,6 +532,9 @@ let make_clenv_binding_gen hyps_only n env sigma (c,t) = function let make_clenv_binding_env_apply env sigma n = make_clenv_binding_gen true n env sigma + +let make_clenv_binding_env env sigma = + make_clenv_binding_gen false None env sigma let make_clenv_binding_apply env sigma n = make_clenv_binding_gen true n env sigma let make_clenv_binding env sigma = make_clenv_binding_gen false None env sigma diff --git a/proofs/clenv.mli b/proofs/clenv.mli index d7bdaf2f5..5868f1e9b 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -96,6 +96,10 @@ val make_clenv_binding_env_apply : val make_clenv_binding_apply : env -> evar_map -> int option -> constr * constr -> constr bindings -> clausenv + +val make_clenv_binding_env : + env -> evar_map -> constr * constr -> constr bindings -> clausenv + val make_clenv_binding : env -> evar_map -> constr * constr -> constr bindings -> clausenv diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 560e662a1..28eba7f42 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -436,7 +436,7 @@ let start_proof_com kind thms hook = let thms = List.map (fun (sopt,(bl,t,guard)) -> let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in let t', imps' = interp_type_evars_impls ~impls env evdref t in - check_evars_are_solved env Evd.empty !evdref; + check_evars_are_solved env !evdref (Evd.empty,!evdref); let ids = List.map pi1 ctx in (compute_proof_name (pi1 kind) sopt, (nf_evar !evdref (it_mkProd_or_LetIn t' ctx), diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml new file mode 100644 index 000000000..806d37319 --- /dev/null +++ b/tactics/hiddentac.ml @@ -0,0 +1,96 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Tactics +open Util +open Locus +open Misctypes + +(* Basic tactics *) +let h_intro_move = intro_move +let h_intro x = h_intro_move (Some x) MoveLast +let h_intros_until = intros_until +let h_assumption = assumption +let h_exact = exact_check +let h_exact_no_check = exact_no_check +let h_vm_cast_no_check = vm_cast_no_check +let h_apply = apply_with_bindings_gen +let h_apply_in simple ev cb (id,ipat) = apply_in simple ev id cb ipat +let h_elim = elim +let h_elim_type = elim_type +let h_case = general_case_analysis +let h_case_type = case_type +let h_fix = fix +let h_mutual_fix id n l = mutual_fix id n l 0 + +let h_cofix = cofix +let h_mutual_cofix id l = mutual_cofix id l 0 + +let h_cut = cut +let h_generalize_gen cl = + generalize_gen (List.map (on_fst Redexpr.out_with_occurrences) cl) +let h_generalize cl = + h_generalize_gen (List.map (fun c -> ((AllOccurrences,c),Names.Anonymous)) + cl) +let h_generalize_dep = generalize_dep +let h_let_tac b na c cl eqpat = + let id = Option.default (Loc.ghost,IntroAnonymous) eqpat in + let with_eq = if b then None else Some (true,id) in + letin_tac with_eq na c None cl +let h_let_pat_tac b na c cl eqpat = + let id = Option.default (Loc.ghost,IntroAnonymous) eqpat in + let with_eq = if b then None else Some (true,id) in + letin_pat_tac with_eq na c None cl + +(* Derived basic tactics *) +let h_simple_induction_destruct isrec h = + if isrec then (simple_induct h) else (simple_destruct h) +let h_simple_induction = h_simple_induction_destruct true +let h_simple_destruct = h_simple_induction_destruct false + +let h_induction_destruct = induction_destruct +let h_new_induction ev c idl e cl = + h_induction_destruct true ev ([c,idl,cl],e) +let h_new_destruct ev c idl e cl = h_induction_destruct false ev ([c,idl,cl],e) + +let h_specialize = specialize +let h_lapply = cut_and_apply + +(* Context management *) +let h_clear b l = (if b then keep else clear) l +let h_clear_body = clear_body +let h_move = move_hyp +let h_rename = rename_hyp +let h_revert = revert + +(* Constructors *) +let h_left = left_with_bindings +let h_right = right_with_bindings +let h_split = split_with_bindings + +let h_constructor ev n l = constructor_tac ev None n l +let h_one_constructor n = one_constructor n NoBindings +let h_simplest_left = h_left false NoBindings +let h_simplest_right = h_right false NoBindings + +(* Conversion *) +let h_reduce = reduce +let h_change = change + +(* Equivalence relations *) +let h_reflexivity = intros_reflexivity +let h_symmetry = intros_symmetry +let h_transitivity = intros_transitivity + +let h_simplest_apply c = h_apply false false [Loc.ghost,(c,NoBindings)] +let h_simplest_eapply c = h_apply false true [Loc.ghost,(c,NoBindings)] +let h_simplest_elim c = h_elim false (c,NoBindings) None +let h_simplest_case c = h_case false (c,NoBindings) + +let h_intro_patterns = intro_patterns + diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli new file mode 100644 index 000000000..e1e9ebadd --- /dev/null +++ b/tactics/hiddentac.mli @@ -0,0 +1,125 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Loc +open Names +open Pp +open Term +open Proof_type +open Tacmach +open Genarg +open Tacexpr +open Glob_term +open Evd +open Clenv +open Termops +open Misctypes + +(** Tactics for the interpreter. They used to left a trace in the proof tree + when they are called. *) + +(** Basic tactics *) + +val h_intro_move : Id.t option -> Id.t move_location -> tactic +val h_intro : Id.t -> tactic +val h_intros_until : quantified_hypothesis -> tactic + +val h_assumption : tactic +val h_exact : constr -> tactic +val h_exact_no_check : constr -> tactic +val h_vm_cast_no_check : constr -> tactic + +val h_apply : advanced_flag -> evars_flag -> + constr with_bindings located list -> tactic +val h_apply_in : advanced_flag -> evars_flag -> + constr with_bindings located list -> + Id.t * intro_pattern_expr located option -> tactic + +val h_elim : evars_flag -> constr with_bindings -> + constr with_bindings option -> tactic +val h_elim_type : constr -> tactic +val h_case : evars_flag -> constr with_bindings -> tactic +val h_case_type : constr -> tactic + +val h_mutual_fix : Id.t -> int -> + (Id.t * int * constr) list -> tactic +val h_fix : Id.t option -> int -> tactic +val h_mutual_cofix : Id.t -> (Id.t * constr) list -> tactic +val h_cofix : Id.t option -> tactic + +val h_cut : constr -> tactic +val h_generalize : constr list -> tactic +val h_generalize_gen : (constr Locus.with_occurrences * Name.t) list -> tactic +val h_generalize_dep : ?with_let:bool -> constr -> tactic +val h_let_tac : letin_flag -> Name.t -> constr -> Locus.clause -> + intro_pattern_expr located option -> tactic +val h_let_pat_tac : letin_flag -> Name.t -> evar_map * constr -> + Locus.clause -> intro_pattern_expr located option -> + tactic + +(** Derived basic tactics *) + +val h_simple_induction : quantified_hypothesis -> tactic +val h_simple_destruct : quantified_hypothesis -> tactic +val h_simple_induction_destruct : rec_flag -> quantified_hypothesis -> tactic +val h_new_induction : evars_flag -> + (evar_map * constr with_bindings) induction_arg -> + intro_pattern_expr located option * intro_pattern_expr located option -> + constr with_bindings option -> + Locus.clause option -> tactic +val h_new_destruct : evars_flag -> + (evar_map * constr with_bindings) induction_arg -> + intro_pattern_expr located option * intro_pattern_expr located option -> + constr with_bindings option -> + Locus.clause option -> tactic +val h_induction_destruct : rec_flag -> evars_flag -> + ((evar_map * constr with_bindings) induction_arg * + (intro_pattern_expr located option * intro_pattern_expr located option) * + Locus.clause option) list * + constr with_bindings option -> tactic + +val h_specialize : int option -> constr with_bindings -> tactic +val h_lapply : constr -> tactic + +(** Automation tactic : see Auto *) + + +(** Context management *) +val h_clear : bool -> Id.t list -> tactic +val h_clear_body : Id.t list -> tactic +val h_move : bool -> Id.t -> Id.t move_location -> tactic +val h_rename : (Id.t*Id.t) list -> tactic +val h_revert : Id.t list -> tactic + +(** Constructors *) +val h_constructor : evars_flag -> int -> constr bindings -> tactic +val h_left : evars_flag -> constr bindings -> tactic +val h_right : evars_flag -> constr bindings -> tactic +val h_split : evars_flag -> constr bindings list -> tactic + +val h_one_constructor : int -> tactic +val h_simplest_left : tactic +val h_simplest_right : tactic + + +(** Conversion *) +val h_reduce : Redexpr.red_expr -> Locus.clause -> tactic +val h_change : + Pattern.constr_pattern option -> constr -> Locus.clause -> tactic + +(** Equivalence relations *) +val h_reflexivity : tactic +val h_symmetry : Locus.clause -> tactic +val h_transitivity : constr option -> tactic + +val h_simplest_apply : constr -> tactic +val h_simplest_eapply : constr -> tactic +val h_simplest_elim : constr -> tactic +val h_simplest_case : constr -> tactic + +val h_intro_patterns : intro_pattern_expr located list -> tactic diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 3f27d0b91..22951491b 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -497,13 +497,13 @@ let rec intern_atomic lf ist x = List.map (intern_constr ist) lems,l) (* Derived basic tactics *) - | TacInductionDestruct (ev,isrec,(l,el,cls)) -> - TacInductionDestruct (ev,isrec,(List.map (fun (c,(ipato,ipats)) -> + | TacInductionDestruct (ev,isrec,(l,el)) -> + TacInductionDestruct (ev,isrec,(List.map (fun (c,(ipato,ipats),cls) -> (intern_induction_arg ist c, (Option.map (intern_intro_pattern_naming_loc lf ist) ipato, - Option.map (intern_or_and_intro_pattern_loc lf ist) ipats))) l, - Option.map (intern_constr_with_bindings ist) el, - Option.map (clause_app (intern_hyp_location ist)) cls)) + Option.map (intern_or_and_intro_pattern_loc lf ist) ipats), + Option.map (clause_app (intern_hyp_location ist)) cls)) l, + Option.map (intern_constr_with_bindings ist) el)) | TacDoubleInduction (h1,h2) -> let h1 = intern_quantified_hypothesis ist h1 in let h2 = intern_quantified_hypothesis ist h2 in diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index d05f5f8ad..873f872aa 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -916,10 +916,9 @@ let interp_open_constr_with_bindings_loc ist ((c,_),bl as cb) = (loc,f) let interp_induction_arg ist gl arg = - let env = pf_env gl and sigma = project gl in match arg with | keep,ElimOnConstr c -> - keep,ElimOnConstr (interp_constr_with_bindings ist env sigma c) + keep,ElimOnConstr (fun env sigma -> interp_constr_with_bindings ist env sigma c) | keep,ElimOnAnonHyp n as x -> x | keep,ElimOnIdent (loc,id) -> let error () = user_err_loc (loc, "", @@ -930,7 +929,7 @@ let interp_induction_arg ist gl arg = if Tactics.is_quantified_hypothesis id' gl then keep,ElimOnIdent (loc,id') else - (try keep,ElimOnConstr (sigma,(constr_of_id env id',NoBindings)) + (try keep,ElimOnConstr (fun env sigma -> sigma,(constr_of_id env id',NoBindings)) with Not_found -> user_err_loc (loc,"", pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared or a quantified hypothesis.")) @@ -951,15 +950,17 @@ let interp_induction_arg ist gl arg = keep,ElimOnAnonHyp (out_gen (topwit wit_int) v) else match Value.to_constr v with | None -> error () - | Some c -> keep,ElimOnConstr (sigma,(c,NoBindings)) + | Some c -> keep,ElimOnConstr (fun env sigma -> sigma,(c,NoBindings)) with Not_found -> (* We were in non strict (interactive) mode *) if Tactics.is_quantified_hypothesis id gl then keep,ElimOnIdent (loc,id) else let c = (GVar (loc,id),Some (CRef (Ident (loc,id),None))) in - let (sigma,c) = interp_constr ist env sigma c in - keep,ElimOnConstr (sigma,(c,NoBindings)) + let f env sigma = + let (sigma,c) = interp_constr ist env sigma c in + sigma,(c,NoBindings) in + keep,ElimOnConstr f (* Associates variables with values and gives the remaining variables and values *) @@ -1818,9 +1819,10 @@ and interp_atomic ist tac : unit Proofview.tactic = let with_eq = if b then None else Some (true,id) in Tactics.letin_pat_tac with_eq na c cl in + let (sigma',c) = interp_pure_open_constr ist env sigma c in Tacticals.New.tclWITHHOLES false (*in hope of a future "eset/epose"*) (let_pat_tac b (interp_fresh_name ist env sigma na) - (interp_pure_open_constr ist env sigma c) clp) sigma eqpat + ((sigma,sigma'),c) clp) sigma' eqpat end (* Automation tactics *) @@ -1842,7 +1844,7 @@ and interp_atomic ist tac : unit Proofview.tactic = end (* Derived basic tactics *) - | TacInductionDestruct (isrec,ev,(l,el,cls)) -> + | TacInductionDestruct (isrec,ev,(l,el)) -> (* spiwack: some unknown part of destruct needs the goal to be prenormalised. *) Proofview.V82.nf_evar_goals <*> @@ -1850,19 +1852,18 @@ and interp_atomic ist tac : unit Proofview.tactic = let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let sigma,l = - List.fold_map begin fun sigma (c,(ipato,ipats)) -> + List.fold_map begin fun sigma (c,(ipato,ipats),cls) -> (* TODO: move sigma as a side-effect *) let c = Tacmach.New.of_old (fun gl -> interp_induction_arg ist gl c) gl in let ipato = interp_intro_pattern_naming_option ist env sigma ipato in let sigma,ipats = interp_or_and_intro_pattern_option ist env sigma ipats in - sigma,(c,(ipato,ipats)) + let cls = Option.map (interp_clause ist env sigma) cls in + sigma,(c,(ipato,ipats),cls) end sigma l in let sigma,el = Option.fold_map (interp_constr_with_bindings ist env) sigma el in - let interp_clause = interp_clause ist env sigma in - let cls = Option.map interp_clause cls in - Tacticals.New.tclWITHHOLES ev (Tactics.induction_destruct isrec ev) sigma (l,el,cls) + Tactics.induction_destruct isrec ev (l,el) end | TacDoubleInduction (h1,h2) -> let h1 = interp_quantified_hypothesis ist h1 in diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index c66ff7418..1eec2f257 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -175,10 +175,11 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with | TacAuto (d,n,lems,l) -> TacAuto (d,n,List.map (subst_glob_constr subst) lems,l) (* Derived basic tactics *) - | TacInductionDestruct (isrec,ev,(l,el,cls)) -> - let l' = List.map (fun (c,ids) -> subst_induction_arg subst c, ids) l in + | TacInductionDestruct (isrec,ev,(l,el)) -> + let l' = List.map (fun (c,ids,cls) -> + subst_induction_arg subst c, ids, cls) l in let el' = Option.map (subst_glob_with_bindings subst) el in - TacInductionDestruct (isrec,ev,(l',el',cls)) + TacInductionDestruct (isrec,ev,(l',el')) | TacDoubleInduction (h1,h2) as x -> x (* Context management *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index b78bb9299..a75d7c5ac 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -59,8 +59,24 @@ let dloc = Loc.ghost let typ_of = Retyping.get_type_of -(* Option for 8.2 compatibility *) +(* Option for 8.4 compatibility *) open Goptions +let legacy_elim_if_not_fully_applied_argument = ref false + +let use_legacy_elim_if_not_fully_applied_argument () = + !legacy_elim_if_not_fully_applied_argument + || Flags.version_less_or_equal Flags.V8_4 + +let _ = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "partially applied elimination argument legacy"; + optkey = ["Legacy";"Partially";"Applied";"Elimination";"Argument"]; + optread = (fun () -> !legacy_elim_if_not_fully_applied_argument) ; + optwrite = (fun b -> legacy_elim_if_not_fully_applied_argument := b) } + +(* Option for 8.2 compatibility *) let dependent_propositions_elimination = ref true let use_dependent_propositions_elimination () = @@ -828,19 +844,32 @@ let rec intros_move = function (* Apply a tactic on a quantified hypothesis, an hypothesis in context or a term with bindings *) -let onOpenInductionArg tac = function - | clear_flag,ElimOnConstr cbl -> - tac clear_flag cbl +let onOpenInductionArg env sigma tac = function + | clear_flag,ElimOnConstr f -> + let (sigma',cbl) = f env sigma in + let pending = (sigma,sigma') in + Tacticals.New.tclTHEN + (Proofview.Unsafe.tclEVARS sigma') + (tac clear_flag (pending,cbl)) | clear_flag,ElimOnAnonHyp n -> Tacticals.New.tclTHEN (intros_until_n n) (Tacticals.New.onLastHyp - (fun c -> tac clear_flag (Evd.empty,(c,NoBindings)))) + (fun c -> + Proofview.Goal.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let pending = (sigma,sigma) in + tac clear_flag (pending,(c,NoBindings)) + end)) | clear_flag,ElimOnIdent (_,id) -> (* A quantified hypothesis *) Tacticals.New.tclTHEN (try_intros_until_id_check id) - (tac clear_flag (Evd.empty,(mkVar id,NoBindings))) + (Proofview.Goal.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let pending = (sigma,sigma) in + tac clear_flag (pending,(mkVar id,NoBindings)) + end) let onInductionArg tac = function | clear_flag,ElimOnConstr cbl -> @@ -856,7 +885,7 @@ let onInductionArg tac = function (tac clear_flag (mkVar id,NoBindings)) let map_induction_arg f = function - | clear_flag,ElimOnConstr (sigma,(c,bl)) -> clear_flag,ElimOnConstr (f (sigma,c),bl) + | clear_flag,ElimOnConstr g -> clear_flag,ElimOnConstr (f g) | clear_flag,ElimOnAnonHyp n as x -> x | clear_flag,ElimOnIdent id as x -> x @@ -2123,11 +2152,11 @@ let apply_delayed_in simple with_evars clear_flag id lemmas ipat = (* Implementation without generalisation: abbrev will be lost in hyps in *) (* in the extracted proof *) -let tactic_infer_flags = { +let tactic_infer_flags with_evar = { Pretyping.use_typeclasses = true; Pretyping.use_unif_heuristics = true; Pretyping.use_hook = Some solve_by_implicit_tactic; - Pretyping.fail_evar = true; + Pretyping.fail_evar = not with_evar; Pretyping.expand_evars = true } let decode_hyp = function @@ -2140,22 +2169,20 @@ let decode_hyp = function [...x:=c:T;x1:T1(x),...,x2:T2(x),... |- G(x)] if [b] is true *) -let letin_tac_gen with_eq abs ty = - Proofview.Goal.nf_enter begin fun gl -> +let letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty = + Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in - let evd = Proofview.Goal.sigma gl in - let ccl = Proofview.Goal.concl gl in - let (id,depdecls,lastlhyp,ccl,(ctx,c)) = make_abstraction env evd ccl abs in - let t = match ty with Some t -> t | _ -> typ_of env (Proofview.Goal.sigma gl) c in + let sigma = Proofview.Goal.sigma gl in + let t = match ty with Some t -> t | _ -> typ_of env sigma c in let eq_tac gl = match with_eq with | Some (lr,(loc,ido)) -> let heq = match ido with | IntroAnonymous -> new_fresh_id [id] (add_prefix "Heq" id) gl - | IntroFresh heq_base -> new_fresh_id [id] heq_base gl + | IntroFresh heq_base -> new_fresh_id [id] heq_base gl | IntroIdentifier id -> id in let eqdata = build_coq_eq_data () in let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in - let sigma, eq = Evd.fresh_global env (Proofview.Goal.sigma gl) eqdata.eq in + let sigma, eq = Evd.fresh_global env sigma eqdata.eq in let sigma, refl = Evd.fresh_global env sigma eqdata.refl in let eq = applist (eq,args) in let refl = applist (refl, [t;mkVar id]) in @@ -2166,24 +2193,76 @@ let letin_tac_gen with_eq abs ty = (intro_gen (NamingMustBe (loc,heq)) (decode_hyp lastlhyp) true false) (clear_body [heq;id]) | None -> - (Proofview.Goal.sigma gl, mkNamedLetIn id c t ccl, Proofview.tclUNIT ()) in - Tacticals.New.tclTHEN - (Proofview.Unsafe.tclEVARUNIVCONTEXT ctx) - (Proofview.Goal.nf_enter (fun gl -> - let (sigma,newcl,eq_tac) = eq_tac gl in - Tacticals.New.tclTHENLIST - [ Proofview.Unsafe.tclEVARS sigma; - convert_concl_no_check newcl DEFAULTcast; - intro_gen (NamingMustBe (dloc,id)) (decode_hyp lastlhyp) true false; - Tacticals.New.tclMAP convert_hyp_no_check depdecls; - eq_tac ])) + (sigma, mkNamedLetIn id c t ccl, Proofview.tclUNIT ()) in + let (sigma,newcl,eq_tac) = eq_tac gl in + Tacticals.New.tclTHENLIST + [ Proofview.Unsafe.tclEVARS sigma; + convert_concl_no_check newcl DEFAULTcast; + intro_gen (NamingMustBe (dloc,id)) (decode_hyp lastlhyp) true false; + Tacticals.New.tclMAP convert_hyp_no_check depdecls; + eq_tac ] end -let letin_tac with_eq name c ty occs = - letin_tac_gen with_eq (AbstractExact (name,c,ty,occs,true)) ty +let insert_before decls lasthyp env = + match lasthyp with + | None -> push_named_context decls env + | Some id -> + Environ.fold_named_context + (fun _ (id',_,_ as d) env -> + let env = if Id.equal id id' then push_named_context decls env else env in + push_named d env) + ~init:(reset_context env) env + +(* unsafe *) + +let mkletin_goal env sigma with_eq dep (id,lastlhyp,ccl,c) ty = + let body = if dep then Some c else None in + let t = match ty with Some t -> t | _ -> typ_of env sigma c in + match with_eq with + | Some (lr,(loc,ido)) -> + let heq = match ido with + | IntroAnonymous -> fresh_id_in_env [id] (add_prefix "Heq" id) env + | IntroFresh heq_base -> fresh_id_in_env [id] heq_base env + | IntroIdentifier id -> id in + let eqdata = build_coq_eq_data () in + let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in + let sigma, eq = Evd.fresh_global env sigma eqdata.eq in + let sigma, refl = Evd.fresh_global env sigma eqdata.refl in + let eq = applist (eq,args) in + let refl = applist (refl, [t;mkVar id]) in + let newenv = insert_before [id,body,t;heq,None,eq] lastlhyp env in + let (sigma,x) = new_evar newenv sigma ~principal:true ccl in + (sigma,mkNamedLetIn id c t (mkNamedLetIn heq refl eq x)) + | None -> + let newenv = insert_before [id,body,t] lastlhyp env in + let (sigma,x) = new_evar newenv sigma ~principal:true ccl in + (sigma,mkNamedLetIn id c t x) -let letin_pat_tac with_eq name c occs = - letin_tac_gen with_eq (AbstractPattern (name,c,occs,false,tactic_infer_flags)) None +let letin_tac with_eq id c ty occs = + Proofview.Goal.nf_enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let ccl = Proofview.Goal.concl gl in + let abs = AbstractExact (id,c,ty,occs,true) in + let (id,_,depdecls,lastlhyp,ccl,_) = make_abstraction env sigma ccl abs in + (* We keep the original term to match *) + letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) ty + end + +let letin_pat_tac with_eq id c occs = + Proofview.Goal.nf_enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let ccl = Proofview.Goal.concl gl in + let abs = AbstractPattern (false,id,c,AtOccs occs,false) in + let (id,_,depdecls,lastlhyp,ccl,res) = make_abstraction env sigma ccl abs in + let sigma,c = match res with + | None -> finish_evar_resolution ~flags:(tactic_infer_flags false) env sigma c + | Some (sigma,c) -> (sigma,c) in + Tacticals.New.tclTHEN + (Proofview.Unsafe.tclEVARS sigma) + (letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) None) + end (* Tactics "pose proof" (usetac=None) and "assert"/"enough" (otherwise) *) let forward b usetac ipat c = @@ -2268,7 +2347,7 @@ let generalize_goal_gen env ids i ((occs,c,b),na) t (cl,evd) = let decls,cl = decompose_prod_n_assum i cl in let dummy_prod = it_mkProd_or_LetIn mkProp decls in let newdecls,_ = decompose_prod_n_assum i (subst_term_gen eq_constr_nounivs c dummy_prod) in - let cl',evd' = subst_closed_term_occ env evd occs c (it_mkProd_or_LetIn cl newdecls) in + let cl',evd' = subst_closed_term_occ env evd (AtOccs occs) c (it_mkProd_or_LetIn cl newdecls) in let na = generalized_name c t ids cl' na in mkProd_or_LetIn (na,b,t) cl', evd' @@ -3305,7 +3384,7 @@ let compute_elim_sig ?elimc elimt = }; raise Exit); raise Exit(* exit anyway *) - with Exit -> (* Ending by computing indrev: *) + with Exit -> (* Ending by computing indref: *) match !res.indarg with | None -> !res (* No indref *) | Some ( _,Some _,_) -> error_ind_scheme "" @@ -3313,7 +3392,7 @@ let compute_elim_sig ?elimc elimt = let indhd,indargs = decompose_app ind in try {!res with indref = Some (global_of_constr indhd) } with e when Errors.noncritical e -> - error "Cannot find the inductive type of the inductive scheme.";; + error "Cannot find the inductive type of the inductive scheme." let compute_scheme_signature scheme names_info ind_type_guess = let f,l = decompose_app scheme.concl in @@ -3436,6 +3515,26 @@ let find_induction_type isrec elim hyp0 gl = evd, scheme, ElimUsing (elim,indsign) in evd,(Option.get scheme.indref,scheme.nparams, elim) +let find_induction_type_and_adjust_indarg isrec elim (c,lbind) gl = + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let tmptyp = typ_of env sigma c in + let typ, nrealargs = match elim with + | None -> + let mind,typ = reduce_to_quantified_ind env sigma tmptyp in + typ, inductive_nrealargs (fst mind) + | Some (e,ebind as elimc) -> + let elimt = Typing.type_of env sigma e in + let scheme = compute_elim_sig ~elimc elimt in + if scheme.indarg = None then error "Cannot find induction type"; + let indref = Option.get scheme.indref in + let typ = reduce_to_quantified_ref env sigma indref tmptyp in + typ, scheme.nargs in + let ctxt,_ = splay_prod env sigma typ in + let indclause = make_clenv_binding_env env sigma (c,typ) lbind in + let is_partial_and_ground = ctxt <> [] && is_ground_term sigma c in + indclause, nrealargs, is_partial_and_ground + let find_elim_signature isrec elim hyp0 gl = compute_elim_signature (find_elim isrec elim hyp0 gl) hyp0 @@ -3614,8 +3713,7 @@ let induction_tac with_evars elim (varname,lbind) typ gl = Proofview.V82.of_tactic (elimination_clause_scheme with_evars ~with_classes:false rename i (elimc, elimt, lbindelimc) indclause) gl -let induction_from_context isrec with_evars (indref,nparams,elim) (hyp0,lbind) names - inhyps = +let induction_from_context isrec with_evars (indref,nparams,elim) hyp0 names inhyps = Proofview.Goal.nf_enter begin fun gl -> let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in let reduce_to_quantified_ref = @@ -3624,7 +3722,7 @@ let induction_from_context isrec with_evars (indref,nparams,elim) (hyp0,lbind) n let typ0 = reduce_to_quantified_ref indref tmptyp0 in let indvars = find_atomic_param_of_ind nparams ((strip_prod typ0)) in let induct_tac elim = Proofview.V82.tactic (tclTHENLIST [ - induction_tac with_evars elim (hyp0,lbind) typ0; + induction_tac with_evars elim (hyp0,NoBindings) typ0; tclTRY (unfold_body hyp0); thin [hyp0] ]) in @@ -3632,13 +3730,13 @@ let induction_from_context isrec with_evars (indref,nparams,elim) (hyp0,lbind) n (Some (hyp0,inhyps)) elim indvars names induct_tac end -let induction_with_atomization_of_ind_arg isrec with_evars elim names (hyp0,lbind) inhyps = +let induction_with_atomization_of_ind_arg isrec with_evars elim names hyp0 inhyps = Proofview.Goal.nf_enter begin fun gl -> let sigma, elim_info = find_induction_type isrec elim hyp0 gl in Tacticals.New.tclTHENLIST [Proofview.Unsafe.tclEVARS sigma; (atomize_param_of_ind elim_info hyp0); (induction_from_context isrec with_evars elim_info - (hyp0,lbind) names inhyps)] + hyp0 names inhyps)] end (* Induction on a list of induction arguments. Analyse the elim @@ -3689,48 +3787,157 @@ let clear_unselected_context id inhyps cls gl = thin ids gl | None -> tclIDTAC gl -let induction_gen clear_flag isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls = +let use_bindings env sigma (c,lbind) typ = + (* We don't try to normalize the type to an inductive type because *) + (* we want to support cases such that "nat_rect ?A ?o ?s n" of type ?A *) + (* where the type "?A" is known only by matching *) + let rec find_clause typ = + try make_clenv_binding env sigma (c,typ) lbind + with e when catchable_exception e -> + try find_clause (try_red_product env sigma typ) + with Redelimination -> raise e in + let indclause = find_clause typ in + (* We lose the possibility of coercions in with-bindings *) + pose_all_metas_as_evars env indclause.evd (clenv_value indclause) + +let clear_induction_arg_if_hyp is_arg_pure_hyp c env = + if is_arg_pure_hyp then + let id = destVar c in + fold_named_context (fun _ (id',_,_ as d) env -> + if Id.equal id id' then env else push_named d env) + env ~init:(reset_context env) + else + env + +let make_body env sigma is_arg_pure_hyp c lbind t = + let mind,typ = reduce_to_quantified_ind env sigma t in + let indclause = make_clenv_binding env sigma (c,typ) lbind in + let env = clear_induction_arg_if_hyp is_arg_pure_hyp c env in + let evdref = ref indclause.evd in + let rec aux c = match kind_of_term c with + | Meta mv -> + (match Evd.meta_opt_fvalue !evdref mv with + | Some ({rebus=c},_) -> c + | None -> + let {rebus=ty;freemetas=mvs} = Evd.meta_ftype !evdref mv in + let ty = if Evd.Metaset.is_empty mvs then ty else aux ty in + let src = Evd.evar_source_of_meta mv !evdref in + let ev = Evarutil.e_new_evar env evdref ~src ty in + evdref := meta_assign mv (ev,(Conv,TypeNotProcessed)) !evdref; + ev) + | _ -> + Constr.map aux c in + let c = aux (clenv_value indclause) in + (* side-effect *) + (!evdref, c) + +let pose_induction_arg clear_flag isrec with_evars is_arg_pure_hyp elim + id ((pending,(c0,lbind)),(eqname,names)) t inhyps cls = + Proofview.Goal.nf_enter begin fun gl -> + let env = Proofview.Goal.env gl in + let ccl = Proofview.Goal.concl gl in + Proofview.Refine.refine ~unsafe:true begin fun sigma -> + let (sigma',c') = use_bindings env sigma (c0,lbind) t in + let occs = match cls with None -> LikeFirst | Some occs -> AtOccs occs in + let abs = AbstractPattern (true,Name id,(pending,c'),occs,false) in + let (id,sign,_,lastlhyp,ccl,res) = make_abstraction env sigma' ccl abs in + match res with + | None -> + (* pattern not found *) + let (sigma,c0) = finish_evar_resolution ~flags:(tactic_infer_flags with_evars) env sigma (pending,c0) in + let (sigma,c) = make_body env sigma is_arg_pure_hyp c0 lbind t in + let t = Retyping.get_type_of env sigma c in + let with_eq = Option.map (fun eq -> (false,eq)) eqname in + let env = clear_induction_arg_if_hyp is_arg_pure_hyp c0 env in + mkletin_goal env sigma with_eq false (id,lastlhyp,ccl,c) (Some t) + + | Some (sigma',c) -> + (* pattern found *) + let with_eq = Option.map (fun eq -> (false,eq)) eqname in + (* TODO: if ind has predicate parameters, use JMeq instead of eq *) + let env = reset_with_named_context sign env in + (mkletin_goal env sigma' with_eq true (id,lastlhyp,ccl,c) None) + end +end + +let isIndType env sigma t = + try let _ = find_mrectype env sigma t in true with Not_found -> false + +let induction_gen clear_flag isrec with_evars elim + ((_pending,(c,lbind)),(eqname,names) as arg) cls = let inhyps = match cls with | Some {onhyps=Some hyps} -> List.map (fun ((_,id),_) -> id) hyps | _ -> [] in - match kind_of_term c with - | Var id when not (mem_named_context id (Global.named_context())) - && lbind == NoBindings && not with_evars && Option.is_empty eqname - && clear_flag == None && not (has_selected_occurrences cls) -> - Tacticals.New.tclTHEN - (Proofview.V82.tactic (clear_unselected_context id inhyps cls)) - (induction_with_atomization_of_ind_arg - isrec with_evars elim names (id,lbind) inhyps) - | _ -> - Proofview.Goal.enter begin fun gl -> - let env = Proofview.Goal.env gl in - let x = id_of_name_using_hdchar (Global.env()) (typ_of env sigma c) - Anonymous in - let id = new_fresh_id [] x gl in - (* We need the equality name now *) - let with_eq = Option.map (fun eq -> (false,eq)) eqname in - (* TODO: if ind has predicate parameters, use JMeq instead of eq *) - Proofview.Goal.enter begin fun gl -> - Tacticals.New.tclTHEN - (* Warning: letin is buggy when c is not of inductive type *) - (letin_tac_gen with_eq - (AbstractPattern (Name id,(sigma,c),(Option.default allHypsAndConcl cls),false,tactic_infer_flags)) None) - (induction_with_atomization_of_ind_arg - isrec with_evars elim names (id,lbind) inhyps) - end - end + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let t = typ_of env sigma c in + let is_arg_pure_hyp = + isVar c && not (mem_named_context (destVar c) (Global.named_context())) + && lbind == NoBindings && not with_evars && Option.is_empty eqname + && not (has_selected_occurrences cls) in + if is_arg_pure_hyp && isIndType env sigma t then + (* First case: induction on a variable already in an inductive type and + with maximal abstraction over the variable. + This is a situation where the induction argument is a + clearable variable of the goal w/o occurrence selection + and w/o equality kept: no need to generalize *) + let id = destVar c in + Tacticals.New.tclTHEN + (Proofview.V82.tactic (clear_unselected_context id inhyps cls)) + (induction_with_atomization_of_ind_arg + isrec with_evars elim names id inhyps) + else + (* Otherwise, we find for the pattern, possibly adding missing arguments and + declaring the induction argument as a new local variable *) + let id = + (* Type not the right one if partially applied but anyway for internal use*) + let x = id_of_name_using_hdchar (Global.env()) t Anonymous in + new_fresh_id [] x gl in + if isrec then + (* Historically, induction has side conditions last *) + Tacticals.New.tclTHENFIRST + (Tacticals.New.tclTHENLIST [ + pose_induction_arg clear_flag isrec with_evars is_arg_pure_hyp elim id arg t inhyps cls; + if with_evars + (* do not give a success semantics to edestruct on an + open term yet *) + && true + then Proofview.shelve_unifiable + else Proofview.guard_no_unifiable; + Proofview.cycle (-1); + ]) + (induction_with_atomization_of_ind_arg + isrec with_evars elim names id inhyps) + else + (* Historically, destruct has side conditions first *) + Tacticals.New.tclTHENLAST + (Tacticals.New.tclTHENLIST [ + pose_induction_arg clear_flag isrec with_evars is_arg_pure_hyp elim id arg t inhyps cls; + if with_evars + (* do not give a success semantics to edestruct on an + open term yet *) + && true + then Proofview.shelve_unifiable + else Proofview.guard_no_unifiable + ]) + (induction_with_atomization_of_ind_arg + isrec with_evars elim names id inhyps) + end (* Induction on a list of arguments. First make induction arguments atomic (using letins), then do induction. The specificity here is that all arguments and parameters of the scheme are given (mandatory for the moment), so we don't need to deal with parameters of the inductive type as in induction_gen. *) -let induction_gen_l isrec with_evars elim (eqname,names) lc = - if not (Option.is_empty eqname) then - errorlabstrm "" (str "Do not know what to do with " ++ - Miscprint.pr_intro_pattern_naming (snd (Option.get eqname))); +let induction_gen_l isrec with_evars elim names lc = let newlc = ref [] in let letids = ref [] in + let lc = List.map (function + | (c,None) -> c + | (c,Some(loc,eqname)) -> + user_err_loc (loc,"",str "Do not know what to do with " ++ + Miscprint.pr_intro_pattern_naming eqname)) lc in let rec atomize_list l = match l with | [] -> Proofview.tclUNIT () @@ -3771,66 +3978,89 @@ let induction_gen_l isrec with_evars elim (eqname,names) lc = principles). TODO: really unify induction with one and induction with several args *) -let induction_destruct_core isrec with_evars (lc,elim,names,cls) = - assert (List.length lc > 0); (* ensured by syntax, but if called inside caml? *) - Proofview.Goal.enter begin fun gl -> - let ifi = is_functional_induction elim gl in - if Int.equal (List.length lc) 1 && not ifi then - (* standard induction *) - onOpenInductionArg - (fun clear_flag c -> induction_gen clear_flag isrec with_evars elim names c cls) - (List.hd lc) - else begin - (* functional induction *) - (* Several induction hyps: induction scheme is mandatory *) - if Option.is_empty elim - then - errorlabstrm "" (strbrk "Induction scheme must be given when several induction hypotheses are given.\n" ++ - str "Example: induction x1 x2 x3 using my_scheme."); - if not (Option.is_empty cls) then - error "'in' clause not supported here."; - let finish_evar_resolution (sigma, c) = - snd (finish_evar_resolution (Proofview.Goal.env gl) (Proofview.Goal.sigma gl) (sigma, c)) - in - let lc = List.map (map_induction_arg finish_evar_resolution) lc in - begin match lc with - | [_] -> - (* Hook to recover standard induction on non-standard induction schemes *) +let induction_destruct isrec with_evars (lc,elim) = + match lc with + | [] -> assert false (* ensured by syntax, but if called inside caml? *) + | [c,(eqname,names as allnames),cls] -> + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let ifi = is_functional_induction elim gl in + if not ifi then + (* standard induction *) + onOpenInductionArg env sigma + (fun clear_flag c -> induction_gen clear_flag isrec with_evars elim (c,allnames) cls) c + else begin + (* Standard induction on non-standard induction schemes *) (* will be removable when is_functional_induction will be more clever *) + if not (Option.is_empty cls) then error "'in' clause not supported here."; + let finish_evar_resolution f = + let (sigma',(c,lbind)) = f env sigma in + let pending = (sigma,sigma') in + snd (finish_evar_resolution env sigma' (pending,c)),lbind in + let c = map_induction_arg finish_evar_resolution c in onInductionArg (fun _clear_flag (c,lbind) -> if lbind != NoBindings then error "'with' clause not supported here."; - induction_gen_l isrec with_evars elim names [c]) (List.hd lc) - | _ -> + induction_gen_l isrec with_evars elim names [c,eqname]) c + end + end + | _ -> + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + if elim = None then + (* Several arguments, without "using" clause *) + (* TODO: Do as if the arguments after the first one were called with *) + (* "destruct", but selecting occurrences on the initial copy of *) + (* the goal *) + let (a,b,cl) = List.hd lc in + let l = List.tl lc in + (* TODO *) + Tacticals.New.tclTHEN + (onOpenInductionArg env sigma (fun clear_flag a -> + induction_gen clear_flag isrec with_evars None (a,b) cl) a) + (Tacticals.New.tclMAP (fun (a,b,cl) -> + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + onOpenInductionArg env sigma (fun clear_flag a -> + induction_gen clear_flag false with_evars None (a,b) cl) a + end) l) + else + (* Several induction hyps with induction scheme *) + let finish_evar_resolution f = + let (sigma',(c,lbind)) = f env sigma in + let pending = (sigma,sigma') in + if lbind != NoBindings then + error "'with' clause not supported here."; + snd (finish_evar_resolution env sigma' (pending,c)) in + let lc = List.map (on_pi1 (map_induction_arg finish_evar_resolution)) lc in let newlc = - List.map (fun x -> + List.map (fun (x,(eqn,names),cls) -> + if cls <> None then error "'in' clause not yet supported here."; match x with (* FIXME: should we deal with ElimOnIdent? *) - | _clear_flag,ElimOnConstr (x,NoBindings) -> x + | _clear_flag,ElimOnConstr x -> + if eqn <> None then error "'eqn' clause not supported here."; + (x,names) | _ -> error "Don't know where to find some argument.") lc in + (* Check that "as", if any, is given only on the last argument *) + let names,rest = List.sep_last (List.map snd newlc) in + if List.exists (fun n -> not (Option.is_empty n)) rest then + error "'as' clause with multiple arguments and 'using' clause can only occur last."; + let newlc = List.map (fun (x,_) -> (x,None)) newlc in induction_gen_l isrec with_evars elim names newlc end - end - end -let induction_destruct isrec with_evars = function - | [],_,_ -> Proofview.tclUNIT () - | [a,b],el,cl -> induction_destruct_core isrec with_evars ([a],el,b,cl) - | (a,b)::l,None,cl -> - Tacticals.New.tclTHEN - (induction_destruct_core isrec with_evars ([a],None,b,cl)) - (Tacticals.New.tclMAP (fun (a,b) -> induction_destruct_core false with_evars ([a],None,b,cl)) l) - | l,Some el,cl -> - let check_basic_using = function - | a,(None,None) -> a - | _ -> error "Unsupported syntax for \"using\"." - in - let l' = List.map check_basic_using l in - induction_destruct_core isrec with_evars (l', Some el, (None,None), cl) +let induction ev clr c l e = + induction_gen clr true ev e + (((Evd.empty,Evd.empty),(c,NoBindings)),(None,l)) None -let induction ev lc e idl cls = induction_destruct_core true ev (lc,e,idl,cls) -let destruct ev lc e idl cls = induction_destruct_core false ev (lc,e,idl,cls) +let destruct ev clr c l e = + induction_gen clr false ev e + (((Evd.empty,Evd.empty),(c,NoBindings)),(None,l)) None (* The registered tactic, which calls the default elimination * if no elimination constant is provided. *) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index a4fb6dd88..5a78bff33 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -164,6 +164,7 @@ val unfold_constr : global_reference -> tactic val clear : Id.t list -> tactic val clear_body : Id.t list -> unit Proofview.tactic +val unfold_body : Id.t -> tactic val keep : Id.t list -> tactic val apply_clear_request : clear_flag -> bool -> constr -> unit Proofview.tactic @@ -274,11 +275,8 @@ val elim : val simple_induct : quantified_hypothesis -> unit Proofview.tactic -val induction : evars_flag -> - (evar_map * constr with_bindings) induction_arg list -> - constr with_bindings option -> - intro_pattern_naming option * or_and_intro_pattern option -> - clause option -> unit Proofview.tactic +val induction : evars_flag -> clear_flag -> constr -> or_and_intro_pattern option -> + constr with_bindings option -> unit Proofview.tactic (** {6 Case analysis tactics. } *) @@ -286,21 +284,18 @@ val general_case_analysis : evars_flag -> clear_flag -> constr with_bindings -> val simplest_case : constr -> unit Proofview.tactic val simple_destruct : quantified_hypothesis -> unit Proofview.tactic -val destruct : evars_flag -> - (evar_map * constr with_bindings) induction_arg list -> - constr with_bindings option -> - intro_pattern_naming option * or_and_intro_pattern option -> - clause option -> unit Proofview.tactic +val destruct : evars_flag -> clear_flag -> constr -> or_and_intro_pattern option -> + constr with_bindings option -> unit Proofview.tactic (** {6 Generic case analysis / induction tactics. } *) (** Implements user-level "destruct" and "induction" *) val induction_destruct : rec_flag -> evars_flag -> - ((evar_map * constr with_bindings) induction_arg * - (intro_pattern_naming option * or_and_intro_pattern option)) list * - constr with_bindings option * - clause option -> unit Proofview.tactic + (delayed_open_constr_with_bindings induction_arg + * (intro_pattern_naming option * or_and_intro_pattern option) + * clause option) list * + constr with_bindings option -> unit Proofview.tactic (** {6 Eliminations giving the type instead of the proof. } *) @@ -382,7 +377,7 @@ val letin_tac : (bool * intro_pattern_naming) option -> (** Common entry point for user-level "set", "pose" and "remember" *) val letin_pat_tac : (bool * intro_pattern_naming) option -> - Name.t -> evar_map * constr -> clause -> unit Proofview.tactic + Name.t -> pending_constr -> clause -> unit Proofview.tactic (** {6 Generalize tactics. } *) diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index 48927b6cc..314b612e1 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -98,25 +98,105 @@ Abort. Goal exists x, S x = S 0. eexists. -Fail destruct (S _). (* Incompatible occurrences *) +destruct (S _). (* Incompatible occurrences but takes the first one since Oct 2014 *) +change (0 = S 0). Abort. Goal exists x, S 0 = S x. eexists. -Fail destruct (S _). (* Incompatible occurrences *) +destruct (S _). (* Incompatible occurrences but takes the first one since Oct 2014 *) +change (0 = S ?x). Abort. Goal exists n p:nat, (S n,S n) = (S p,S p) /\ p = n. do 2 eexists. -Fail destruct (_, S _). (* Was succeeding at some time in trunk *) -Show Proof. +destruct (_, S _). (* Was unifying at some time in trunk, now takes the first occurrence *) +change ((n, n0) = (S ?p, S ?p) /\ ?p = ?n0). +Abort. (* Avoid unnatural selection of a subterm larger than expected *) Goal let g := fun x:nat => x in g (S 0) = 0. intro. destruct S. -(* Check that it is not the larger subterm "f (S 0)" which is +(* Check that it is not the larger subterm "g (S 0)" which is selected, as it was the case in 8.4 *) unfold g at 1. Abort. + +(* Some tricky examples convenient to support *) + +Goal forall x, nat_rect (fun _ => nat) O (fun x y => S x) x = nat_rect (fun _ => nat) O (fun x y => S x) x. +intros. +destruct (nat_rect _ _ _ _). +Abort. +(* Check compatibility in selecting what is open or "shelved" *) + +Goal (forall x, x=0 -> nat) -> True. +intros. +Fail destruct H. +edestruct H. +- reflexivity. +- exact Logic.I. +- exact Logic.I. +Qed. + +(* Check an example which was working with case/elim in 8.4 but not with + destruct/induction *) + +Goal forall x, (True -> x = 0) -> 0=0. +intros. +destruct H. +- trivial. +- apply (eq_refl x). +Qed. + +(* Check an example which was working with case/elim in 8.4 but not with + destruct/induction (not the different order between induction/destruct) *) + +Goal forall x, (True -> x = 0) -> 0=0. +intros. +induction H. +- apply (eq_refl x). +- trivial. +Qed. + +(* This test assumes that destruct/induction on non-dependent hypotheses behave the same + when using holes or not + +Goal forall x, (True -> x = 0) -> 0=0. +intros. +destruct (H _). +- apply I. +- apply (eq_refl x). +Qed. +*) + +(* Check destruct vs edestruct *) + +Goal forall x, (forall y, y = 0 -> x = 0) -> 0=0. +intros. +Fail destruct H. +edestruct H. +- trivial. +- apply (eq_refl x). +Qed. + +Goal forall x, (forall y, y = 0 -> x = 0) -> 0=0. +intros. +Fail destruct (H _). +edestruct (H _). +- trivial. +- apply (eq_refl x). +Qed. + +Goal forall x, (forall y, y = 0 -> x = 0) -> 0=0. +intros. +Fail destruct (H _ _). +(* Now a test which assumes that destruct/induction on non-dependent hypotheses behave the same + when using holes or not +edestruct (H _ _). +- trivial. +- apply (eq_refl x). +Qed. +*) diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v index 4e20a5077..1c2a6a0f2 100644 --- a/test-suite/success/induct.v +++ b/test-suite/success/induct.v @@ -73,5 +73,3 @@ intros. induction x as [y * IHx]. change (x = x) in IHx. (* We should have IHx:x=x *) Abort. - - diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 59306f9d4..f74a4badf 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -77,23 +77,15 @@ let sumbool = Coqlib.build_coq_sumbool let andb = fun _ -> (Coqlib.build_bool_type()).Coqlib.andb -let induct_on c = - induction false - [None,Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))] - None (None,None) None +let induct_on c = induction false None c None None + +let destruct_on c = destruct false None c None None let destruct_on_using c id = - destruct false - [None,Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))] - None - (None,Some (dl,[[dl,IntroNaming IntroAnonymous]; - [dl,IntroNaming (IntroIdentifier id)]])) - None - -let destruct_on c = - destruct false - [None,Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))] - None (None,None) None + destruct false None c (Some (dl,[[dl,IntroNaming IntroAnonymous]])) None + +let destruct_on_as c l = + destruct false None c (Some (dl,l)) None (* reconstruct the inductive with the correct deBruijn indexes *) let mkFullInd (ind,u) n = @@ -591,12 +583,9 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). Simple.apply_in freshz (andb_prop()); Proofview.Goal.nf_enter begin fun gl -> let fresht = fresh_id (Id.of_string "Z") gl in - (destruct false [None,Tacexpr.ElimOnConstr - (Evd.empty,((mkVar freshz,NoBindings)))] - None - (None, Some (dl,[[ - dl,IntroNaming (IntroIdentifier fresht); - dl,IntroNaming (IntroIdentifier freshz)]])) None) + (destruct_on_as (mkVar freshz) + [[dl,IntroNaming (IntroIdentifier fresht); + dl,IntroNaming (IntroIdentifier freshz)]]) end ]); (* diff --git a/toplevel/command.ml b/toplevel/command.ml index 57f2571c5..f8c9f25b8 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -127,7 +127,7 @@ let interp_definition bl p red_option c ctypopt = red_constant_entry (rel_context_length ctx) ce red_option, !evdref, imps let check_definition (ce, evd, imps) = - check_evars_are_solved (Global.env ()) Evd.empty evd; + check_evars_are_solved (Global.env ()) evd (Evd.empty,evd); ce let get_locality id = function @@ -266,7 +266,7 @@ let do_assumptions (_, poly, _ as kind) nl l = (env,((is_coe,idl),t,(ctx,imps)))) env l in - let evd = solve_remaining_evars all_and_fail_flags env Evd.empty !evdref in + let evd = solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref) in let l = List.map (on_pi2 (nf_evar evd)) l in snd (List.fold_left (fun (subst,status) ((is_coe,idl),t,(ctx,imps)) -> let t = replace_vars subst t in @@ -508,7 +508,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = () in (* Try further to solve evars, and instantiate them *) - let sigma = solve_remaining_evars all_and_fail_flags env_params Evd.empty !evdref in + let sigma = solve_remaining_evars all_and_fail_flags env_params !evdref (Evd.empty,!evdref) in evdref := sigma; (* Compute renewed arities *) let nf,_ = e_nf_evars_and_universes evdref in @@ -841,7 +841,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation = let binders = letbinders @ [arg] in let binders_env = push_rel_context binders_rel env in let rel, _ = interp_constr_evars_impls env evdref r in - let () = check_evars_are_solved env Evd.empty !evdref in + let () = check_evars_are_solved env !evdref (Evd.empty,!evdref) in let relty = Typing.type_of env !evdref rel in let relargty = let error () = @@ -1019,7 +1019,7 @@ let interp_recursive isfix fixl notations = (env,rec_sign,evd), (fixnames,fixdefs,fixtypes), List.combine3 fixctxnames fiximps fixannots let check_recursive isfix env evd (fixnames,fixdefs,_) = - check_evars_are_solved env Evd.empty evd; + check_evars_are_solved env evd (Evd.empty,evd); if List.for_all Option.has_some fixdefs then begin let fixdefs = List.map Option.get fixdefs in check_mutuality env isfix (List.combine fixnames fixdefs) diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 37205e404..b0e0917f6 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -679,7 +679,7 @@ let pr_position (cl,pos) = | Some (id,Locus.InHypValueOnly) -> str " of the body of hypothesis " ++ pr_id id in int pos ++ clpos -let explain_cannot_unify_occurrences env sigma nested (cl2,pos2,t2) (cl1,pos1,t1) e = +let explain_cannot_unify_occurrences env sigma nested ((cl2,pos2),t2) ((cl1,pos1),t1) e = let s = if nested then "Found nested occurrences of the pattern" else "Found incompatible occurrences of the pattern" in let ppreason = match e with None -> mt() | Some (c1,c2,e) -> explain_unification_error env sigma c1 c2 (Some e) in diff --git a/toplevel/record.ml b/toplevel/record.ml index dfeedfbc8..6d3dcdcb4 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -126,7 +126,7 @@ let typecheck_params_and_fields def id t ps nots fs = interp_fields_evars env_ar evars impls_env nots (binders_of_decls fs) in let sigma = - Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar Evd.empty !evars in + Pretyping.solve_remaining_evars Pretyping.all_and_fail_flags env_ar !evars (Evd.empty,!evars) in let evars, nf = Evarutil.nf_evars_and_universes sigma in let arity = nf t' in let evars = |