blob: d22f94e4e530d821566ab5f1096e486c53358bfd (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Locus
open Evd
open Pretype_errors
open Environ
open EConstr
(** 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 : position_reporting option
}
(** This is the basic testing function, looking for exact matches of a
closed term *)
val make_eq_univs_test : env -> 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 : evar_map -> 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 :
evar_map ->
(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 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) or_like_first ->
constr -> named_declaration -> named_declaration * evar_map
(** Miscellaneous *)
val error_invalid_occurrence : int list -> 'a
|
