diff options
| -rw-r--r-- | dev/doc/changes.txt | 7 | ||||
| -rw-r--r-- | dev/printers.mllib | 1 | ||||
| -rw-r--r-- | pretyping/find_subterm.ml | 166 | ||||
| -rw-r--r-- | pretyping/find_subterm.mli | 66 | ||||
| -rw-r--r-- | pretyping/pretype_errors.ml | 6 | ||||
| -rw-r--r-- | pretyping/pretype_errors.mli | 6 | ||||
| -rw-r--r-- | pretyping/pretyping.mllib | 1 | ||||
| -rw-r--r-- | pretyping/tacred.ml | 19 | ||||
| -rw-r--r-- | pretyping/tacred.mli | 8 | ||||
| -rw-r--r-- | pretyping/termops.ml | 136 | ||||
| -rw-r--r-- | pretyping/termops.mli | 50 | ||||
| -rw-r--r-- | pretyping/unification.ml | 27 | ||||
| -rw-r--r-- | tactics/extratactics.ml4 | 4 | ||||
| -rw-r--r-- | tactics/tactics.ml | 3 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 7 |
15 files changed, 277 insertions, 230 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index d4e42142b..a919b86c2 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -78,6 +78,13 @@ - Tactics API: new_induct -> induction; new_destruct -> destruct; letin_pat_tac do not accept a type anymore +- New file find_subterm.ml for gathering former functions + subst_closed_term_occ_modulo, subst_closed_term_occ_decl (which now + take and outputs also an evar_map), and + subst_closed_term_occ_modulo, subst_closed_term_occ_decl_modulo (now + renamed into replace_term_occ_modulo and + replace_term_occ_decl_modulo). + ========================================= = CHANGES BETWEEN COQ V8.3 AND COQ V8.4 = ========================================= diff --git a/dev/printers.mllib b/dev/printers.mllib index f826984b4..8477df76c 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -129,6 +129,7 @@ Arguments_renaming Typing Patternops ConstrMatching +Find_subterm Tacred Classops Typeclasses_errors diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml new file mode 100644 index 000000000..61bb2ce03 --- /dev/null +++ b/pretyping/find_subterm.ml @@ -0,0 +1,166 @@ +(************************************************************************) +(* 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 Pp +open Util +open Errors +open Names +open Locus +open Context +open Term +open Nameops +open Termops +open Pretype_errors + +(** Processing occurrences *) + +type occurrence_error = + | InvalidOccurrence of int list + | IncorrectInValueOccurrence of Id.t + +let explain_invalid_occurrence l = + let l = List.sort_uniquize Int.compare l in + str ("Invalid occurrence " ^ String.plural (List.length l) "number" ^": ") + ++ prlist_with_sep spc int l ++ str "." + +let explain_incorrect_in_value_occurrence id = + pr_id id ++ str " has no value." + +let explain_occurrence_error = function + | InvalidOccurrence l -> explain_invalid_occurrence l + | IncorrectInValueOccurrence id -> explain_incorrect_in_value_occurrence id + +let error_occurrences_error e = + errorlabstrm "" (explain_occurrence_error e) + +let error_invalid_occurrence occ = + error_occurrences_error (InvalidOccurrence occ) + +let check_used_occurrences nbocc (nowhere_except_in,locs) = + let rest = List.filter (fun o -> o >= nbocc) locs in + match rest with + | [] -> () + | _ -> error_occurrences_error (InvalidOccurrence rest) + +let proceed_with_occurrences f occs x = + match occs with + | NoOccurrences -> x + | _ -> + (* TODO FINISH ADAPTING WITH HUGO *) + let plocs = Locusops.convert_occs occs in + assert (List.for_all (fun x -> x >= 0) (snd plocs)); + let (nbocc,x) = f 1 x in + check_used_occurrences nbocc plocs; + x + +(** Applying a function over a named_declaration with an hypothesis + location request *) + +let map_named_declaration_with_hyploc f hyploc acc (id,bodyopt,typ) = + let f = f (Some (id,hyploc)) in + match bodyopt,hyploc with + | None, InHypValueOnly -> + error_occurrences_error (IncorrectInValueOccurrence id) + | None, _ | Some _, InHypTypeOnly -> + let acc,typ = f acc typ in acc,(id,bodyopt,typ) + | Some body, InHypValueOnly -> + let acc,body = f acc body in acc,(id,Some body,typ) + | Some body, InHyp -> + let acc,body = f acc body in + let acc,typ = f acc typ in + acc,(id,Some body,typ) + +(** Finding a subterm up to some testing function *) + +exception SubtermUnificationError of subterm_unification_error + +exception NotUnifiable of (constr * constr * unification_error) option + +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 +} + +(* Find subterms using a testing function, but only at a list of + locations or excluding a list of locations; in the occurrences list + (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 = + let (nowhere_except_in,locs) = Locusops.convert_occs occs in + let maxocc = List.fold_right max locs 0 in + let pos = ref occ in + let nested = ref false in + 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 -> + let lastpos = Option.get test.last_found in + raise (SubtermUnificationError (!nested,(cl,!pos,t),lastpos,e)) in + let rec substrec k t = + if nowhere_except_in && !pos > maxocc then t else + try + let subst = test.match_fun test.testing_state t in + if Locusops.is_selected !pos occs then + (add_subst t subst; incr pos; + (* Check nested matching subterms *) + nested := true; ignore (subst_below k t); nested := false; + (* Do the effective substitution *) + Vars.lift k (bywhat ())) + else + (incr pos; 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 + (!pos, t') + +let replace_term_occ_modulo occs test bywhat t = + proceed_with_occurrences + (replace_term_occ_gen_modulo occs test bywhat None) occs t + +let replace_term_occ_decl_modulo (plocs,hyploc) test bywhat d = + proceed_with_occurrences + (map_named_declaration_with_hyploc + (replace_term_occ_gen_modulo plocs test bywhat) + hyploc) + plocs d + +(** Finding an exact subterm *) + +let make_eq_univs_test evd c = + { match_fun = (fun evd c' -> + let b, cst = Universes.eq_constr_universes c c' in + if b then + try Evd.add_universe_constraints evd cst + with Evd.UniversesDiffer -> raise (NotUnifiable None) + else raise (NotUnifiable None)); + merge_fun = (fun evd _ -> evd); + testing_state = evd; + last_found = None +} + +let subst_closed_term_occ evd occs c t = + let test = make_eq_univs_test evd c in + let bywhat () = mkRel 1 in + let t' = replace_term_occ_modulo occs test bywhat t in + t', test.testing_state + +let subst_closed_term_occ_decl evd (plocs,hyploc) c d = + let test = make_eq_univs_test evd c in + let bywhat () = mkRel 1 in + proceed_with_occurrences + (map_named_declaration_with_hyploc + (fun _ -> replace_term_occ_gen_modulo plocs test bywhat None) + hyploc) plocs d, + test.testing_state diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli new file mode 100644 index 000000000..44e435e69 --- /dev/null +++ b/pretyping/find_subterm.mli @@ -0,0 +1,66 @@ +(************************************************************************) +(* 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 Names +open Locus +open Context +open Term +open Evd +open Pretype_errors + +(** Finding subterms, possibly up to some unification function, + possibly at some given occurrences *) + +exception NotUnifiable of (constr * constr * unification_error) option + +exception SubtermUnificationError of subterm_unification_error + +(** A testing function is typically a unification function returning a + substitution or failing with a NotUnifiable error, together with a + 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 +} + +(** This is the basic testing function, looking for exact matches of a + closed term *) +val make_eq_univs_test : evar_map -> constr -> evar_map testing_function + +(** [replace_term_occ_modulo occl test mk c] looks in [c] for subterm + modulo a testing function [test] and replaces successfully + 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 + +(** [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) -> + 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 : evar_map -> occurrences -> 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 : evar_map -> + occurrences * hyp_location_flag -> + constr -> named_declaration -> named_declaration * evar_map + +(** Miscellaneous *) +val error_invalid_occurrence : int list -> 'a diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index d8f51054d..934e7bdbb 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -23,6 +23,10 @@ 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 subterm_unification_error = bool * (position * int * constr) * (position * int * constr) * (constr * constr * unification_error) option + type pretype_error = (* Old Case *) | CantFindCaseType of constr @@ -46,7 +50,7 @@ type pretype_error = | UnexpectedType of constr * constr | NotProduct of constr | TypingError of type_error - | CannotUnifyOccurrences of Termops.subterm_unification_error + | CannotUnifyOccurrences of subterm_unification_error exception PretypeError of env * Evd.evar_map * pretype_error diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index f8e39f316..e816463e7 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -24,6 +24,10 @@ 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 subterm_unification_error = bool * (position * int * constr) * (position * int * constr) * (constr * constr * unification_error) option + type pretype_error = (** Old Case *) | CantFindCaseType of constr @@ -47,7 +51,7 @@ type pretype_error = | UnexpectedType of constr * constr | NotProduct of constr | TypingError of type_error - | CannotUnifyOccurrences of Termops.subterm_unification_error + | CannotUnifyOccurrences of subterm_unification_error exception PretypeError of env * Evd.evar_map * pretype_error diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index f1a9d6915..ceb01fd95 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -9,6 +9,7 @@ Nativenorm Retyping Cbv Pretype_errors +Find_subterm Evarutil Evarsolve Recordops diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 75f6f66fe..6e522933f 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -15,6 +15,7 @@ open Vars open Libnames open Globnames open Termops +open Find_subterm open Namegen open Environ open Closure @@ -1075,22 +1076,6 @@ let compute = cbv_betadeltaiota (* Pattern *) -let make_eq_univs_test evd c = - { match_fun = (fun evd c' -> - let b, cst = Universes.eq_constr_universes c c' in - if b then - try Evd.add_universe_constraints evd cst - with Evd.UniversesDiffer -> raise NotUnifiable - else raise NotUnifiable); - merge_fun = (fun evd _ -> evd); - testing_state = evd; - last_found = None -} -let subst_closed_term_univs_occ evd occs c t = - let test = make_eq_univs_test evd c in - let t' = subst_closed_term_occ_modulo occs test None t in - t', test.testing_state - (* gives [na:ta]c' such that c converts to ([na:ta]c' a), abstracting only * the specified occurrences. *) @@ -1101,7 +1086,7 @@ let abstract_scheme env sigma (locc,a) c = if occur_meta a then mkLambda (na,ta,c) else - let c', sigma' = subst_closed_term_univs_occ sigma locc a c in + let c', sigma' = subst_closed_term_occ sigma locc a c in mkLambda (na,ta,c') let pattern_occs loccs_trm env sigma c = diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index 5e4bc5c46..91364c4ae 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -60,14 +60,6 @@ val unfoldn : (** Fold *) val fold_commands : constr list -> reduction_function -val make_eq_univs_test : evar_map -> constr -> evar_map Termops.testing_function - -(** [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_univs_occ : evar_map -> occurrences -> constr -> constr -> - constr * evar_map - (** Pattern *) val pattern_occs : (occurrences * constr) list -> env -> evar_map -> constr -> constr diff --git a/pretyping/termops.ml b/pretyping/termops.ml index c68f2c4d9..67ffcf8aa 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -679,142 +679,6 @@ let replace_term_gen eq_fun c by_c in_t = let replace_term = replace_term_gen eq_constr -(* Substitute only at a list of locations or excluding a list of - locations; in the occurrences list (b,l), b=true means no - occurrence except the ones in l and b=false, means all occurrences - except the ones in l *) - -type occurrence_error = - | InvalidOccurrence of int list - | IncorrectInValueOccurrence of Id.t - -let explain_invalid_occurrence l = - let l = List.sort_uniquize Int.compare l in - str ("Invalid occurrence " ^ String.plural (List.length l) "number" ^": ") - ++ prlist_with_sep spc int l ++ str "." - -let explain_incorrect_in_value_occurrence id = - pr_id id ++ str " has no value." - -let explain_occurrence_error = function - | InvalidOccurrence l -> explain_invalid_occurrence l - | IncorrectInValueOccurrence id -> explain_incorrect_in_value_occurrence id - -let error_occurrences_error e = - errorlabstrm "" (explain_occurrence_error e) - -let error_invalid_occurrence occ = - error_occurrences_error (InvalidOccurrence occ) - -type position =(Id.t * Locus.hyp_location_flag) option - -type subterm_unification_error = bool * (position * int * constr) * (position * int * constr) - -exception SubtermUnificationError of subterm_unification_error - -exception NotUnifiable - -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 -} - -let subst_closed_term_occ_gen_modulo occs test 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 - let nested = ref false in - 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 -> - let lastpos = Option.get test.last_found in - raise (SubtermUnificationError (!nested,(cl,!pos,t),lastpos)) in - let rec substrec k t = - if nowhere_except_in && !pos > maxocc then t else - try - let subst = test.match_fun test.testing_state t in - if Locusops.is_selected !pos occs then - (add_subst t subst; incr pos; - (* Check nested matching subterms *) - nested := true; ignore (subst_below k t); nested := false; - (* Do the effective substitution *) - mkRel k) - else - (incr pos; 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 1 t in - (!pos, t') - -let check_used_occurrences nbocc (nowhere_except_in,locs) = - let rest = List.filter (fun o -> o >= nbocc) locs in - match rest with - | [] -> () - | _ -> error_occurrences_error (InvalidOccurrence rest) - -let proceed_with_occurrences f occs x = - match occs with - | NoOccurrences -> x - | _ -> - (* TODO FINISH ADAPTING WITH HUGO *) - let plocs = Locusops.convert_occs occs in - assert (List.for_all (fun x -> x >= 0) (snd plocs)); - let (nbocc,x) = f 1 x in - check_used_occurrences nbocc plocs; - x - -let make_eq_test c = { - match_fun = (fun () c' -> if eq_constr c c' then () else raise NotUnifiable); - merge_fun = (fun () () -> ()); - testing_state = (); - last_found = None -} - -let subst_closed_term_occ_gen occs pos c t = - subst_closed_term_occ_gen_modulo occs (make_eq_test c) None pos t - -let subst_closed_term_occ occs c t = - proceed_with_occurrences - (fun occ -> subst_closed_term_occ_gen occs occ c) - occs t - -let subst_closed_term_occ_modulo occs test cl t = - proceed_with_occurrences - (subst_closed_term_occ_gen_modulo occs test cl) occs t - -let map_named_declaration_with_hyploc f hyploc acc (id,bodyopt,typ) = - let f = f (Some (id,hyploc)) in - match bodyopt,hyploc with - | None, InHypValueOnly -> - error_occurrences_error (IncorrectInValueOccurrence id) - | None, _ | Some _, InHypTypeOnly -> - let acc,typ = f acc typ in acc,(id,bodyopt,typ) - | Some body, InHypValueOnly -> - let acc,body = f acc body in acc,(id,Some body,typ) - | Some body, InHyp -> - let acc,body = f acc body in - let acc,typ = f acc typ in - acc,(id,Some body,typ) - -let subst_closed_term_occ_decl (plocs,hyploc) c d = - proceed_with_occurrences - (map_named_declaration_with_hyploc - (fun _ occ -> subst_closed_term_occ_gen plocs occ c) hyploc) plocs d - -let subst_closed_term_occ_decl_modulo (plocs,hyploc) test d = - proceed_with_occurrences - (map_named_declaration_with_hyploc - (subst_closed_term_occ_gen_modulo plocs test) - hyploc) - plocs d - let vars_of_env env = let s = Context.fold_named_context (fun (id,_,_) s -> Id.Set.add id s) diff --git a/pretyping/termops.mli b/pretyping/termops.mli index ebcf4285c..e01b3f455 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -147,56 +147,6 @@ val subst_term : constr -> constr -> constr (** [replace_term d e c] replaces [d] by [e] in [c] *) val replace_term : constr -> constr -> constr -> constr -(** [subst_closed_term_occ_gen occl n c d] replaces occurrences of closed [c] at - positions [occl], counting from [n], by [Rel 1] in [d] *) -val subst_closed_term_occ_gen : - occurrences -> int -> constr -> types -> int * types - -(** [subst_closed_term_occ_modulo] looks for subterm modulo a - testing function returning a substitution of type ['a] (or failing - with NotUnifiable); a function for merging substitution (possibly - failing with NotUnifiable) and an initial substitution are - required too; [subst_closed_term_occ_modulo] itself turns a - NotUnifiable exception into a SubtermUnificationError *) - -exception NotUnifiable - -type position =(Id.t * Locus.hyp_location_flag) option - -type subterm_unification_error = bool * (position * int * constr) * (position * int * constr) - -exception SubtermUnificationError of subterm_unification_error - -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 -} - -val make_eq_test : constr -> unit testing_function - -val subst_closed_term_occ_modulo : - occurrences -> 'a testing_function -> (Id.t * hyp_location_flag) option - -> constr -> types - -(** [subst_closed_term_occ occl c d] replaces occurrences of closed [c] at - positions [occl] by [Rel 1] in [d] (see also Note OCC) *) -val subst_closed_term_occ : occurrences -> constr -> constr -> constr - -(** [subst_closed_term_occ_decl occl c decl] replaces occurrences of closed [c] - at positions [occl] by [Rel 1] in [decl] *) - -val subst_closed_term_occ_decl : - occurrences * hyp_location_flag -> constr -> named_declaration -> - named_declaration - -val subst_closed_term_occ_decl_modulo : - occurrences * hyp_location_flag -> 'a testing_function -> - named_declaration -> named_declaration - -val error_invalid_occurrence : int list -> 'a - (** Alternative term equalities *) val base_sort_cmp : Reduction.conv_pb -> sorts -> sorts -> bool val compare_constr_univ : (Reduction.conv_pb -> constr -> constr -> bool) -> diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 9baabae77..dd0f68390 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -26,6 +26,7 @@ open Coercion open Recordops open Locus open Locusops +open Find_subterm let occur_meta_or_undefined_evar evd c = let rec occrec c = match kind_of_term c with @@ -62,7 +63,7 @@ let abstract_scheme env evd c l lname_typ = else *) if occur_meta a then mkLambda_name env (na,ta,t), evd else - let t', evd' = Tacred.subst_closed_term_univs_occ evd locc a t in + let t', evd' = Find_subterm.subst_closed_term_occ evd locc a t in mkLambda_name env (na,ta,t'), evd') (c,evd) (List.rev l) @@ -1222,17 +1223,21 @@ let make_pattern_test inf_flags env sigma0 (sigma,c) = let matching_fun _ t = try let sigma = w_typed_unify env sigma Reduction.CONV flags c t in Some(sigma, t) - with e when Errors.noncritical e -> raise NotUnifiable in + with + | PretypeError (_,_,CannotUnify (c1,c2,Some e)) -> + raise (NotUnifiable (Some (c1,c2,e))) + | e when Errors.noncritical e -> raise (NotUnifiable None) in let merge_fun c1 c2 = match c1, c2 with | Some (evd,c1), Some (_,c2) -> (try let evd = w_typed_unify env evd Reduction.CONV flags c1 c2 in Some (evd, c1) - with e when Errors.noncritical e -> raise NotUnifiable) + with + | PretypeError (_,_,CannotUnify (c1,c2,Some e)) -> raise (NotUnifiable (Some (c1,c2,e))) + | e when Errors.noncritical e -> raise (NotUnifiable None)) | Some _, None -> c1 | None, Some _ -> c2 - | None, None -> None - in + | None, None -> None in { match_fun = matching_fun; merge_fun = merge_fun; testing_state = None; last_found = None }, (fun test -> match test.testing_state with @@ -1247,7 +1252,7 @@ let make_eq_test evd c = let out cstr = Evd.evar_universe_context cstr.testing_state, c in - (Tacred.make_eq_univs_test evd c, out) + (make_eq_univs_test evd c, out) let make_abstraction_core name (test,out) (sigmac,c) ty occs check_occs env concl = let id = @@ -1260,6 +1265,7 @@ let make_abstraction_core name (test,out) (sigmac,c) ty occs check_occs env conc else x in + let mkvarid () = mkVar id in let compute_dependency _ (hyp,_,_ as d) depdecls = match occurrences_of_hyp hyp occs with | None -> @@ -1272,7 +1278,7 @@ let make_abstraction_core name (test,out) (sigmac,c) ty occs check_occs env conc else depdecls | Some ((AllOccurrences, InHyp) as occ) -> - let newdecl = subst_closed_term_occ_decl_modulo occ test d in + 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 @@ -1280,16 +1286,15 @@ let make_abstraction_core name (test,out) (sigmac,c) ty occs check_occs env conc then raise (PretypeError (env,sigmac,NoOccurrenceFound (c,Some hyp))) else depdecls else - (subst1_named_decl (mkVar id) newdecl)::depdecls + newdecl :: depdecls | Some occ -> - let newdecl = subst_closed_term_occ_decl_modulo occ test d in - (subst1_named_decl (mkVar id) newdecl)::depdecls in + replace_term_occ_decl_modulo occ test mkvarid d :: depdecls in try let depdecls = fold_named_context compute_dependency env ~init:[] in let ccl = match occurrences_of_goal occs with | None -> concl | Some occ -> - subst1 (mkVar id) (subst_closed_term_occ_modulo occ test None concl) + 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 diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 6adec45bc..fa2ac3712 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -582,7 +582,7 @@ END (**********************************************************************) let subst_var_with_hole occ tid t = - let occref = if occ > 0 then ref occ else Termops.error_invalid_occurrence [occ] in + let occref = if occ > 0 then ref occ else Find_subterm.error_invalid_occurrence [occ] in let locref = ref 0 in let rec substrec = function | GVar (_,id) as x -> @@ -598,7 +598,7 @@ let subst_var_with_hole occ tid t = | c -> map_glob_constr_left_to_right substrec c in let t' = substrec t in - if !occref > 0 then Termops.error_invalid_occurrence [occ] else t' + if !occref > 0 then Find_subterm.error_invalid_occurrence [occ] else t' let subst_hole_with_term occ tc t = let locref = ref 0 in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 30568edab..d046a0642 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -15,6 +15,7 @@ open Term open Vars open Context open Termops +open Find_subterm open Namegen open Declarations open Inductiveops @@ -1865,7 +1866,7 @@ let generalize_goal_gen 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_univs_occ evd occs c (it_mkProd_or_LetIn cl newdecls) in + let cl',evd' = subst_closed_term_occ evd 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' diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index d251b571c..16d324029 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -645,15 +645,16 @@ 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 nested (cl2,pos2,t2) (cl1,pos1,t1) = +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 str s ++ str ":" ++ spc () ++ str "Matched term " ++ pr_lconstr_env env t2 ++ strbrk " at position " ++ pr_position (cl2,pos2) ++ strbrk " is not compatible with matched term " ++ pr_lconstr_env env t1 ++ strbrk " at position " ++ - pr_position (cl1,pos1) ++ str "." + pr_position (cl1,pos1) ++ ppreason ++ str "." let explain_pretype_error env sigma err = let env = Evarutil.env_nf_betaiotaevar sigma env in @@ -687,7 +688,7 @@ let explain_pretype_error env sigma err = | AbstractionOverMeta (m,n) -> explain_abstraction_over_meta env m n | NonLinearUnification (m,c) -> explain_non_linear_unification env m c | TypingError t -> explain_type_error env sigma t - | CannotUnifyOccurrences (b,c1,c2) -> explain_cannot_unify_occurrences env b c1 c2 + | CannotUnifyOccurrences (b,c1,c2,e) -> explain_cannot_unify_occurrences env sigma b c1 c2 e (* Module errors *) |