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
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
|
(************************************************************************)
(* * The Rocq Prover / The Rocq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
open Pp
open CErrors
open Names
open Locus
open EConstr
open Termops
open Pretype_errors
module NamedDecl = Context.Named.Declaration
(** Processing occurrences *)
let explain_incorrect_in_value_occurrence id =
Id.print id ++ str " has no value."
let proceed_with_occurrences f occs x =
match occs with
| NoOccurrences -> x
| occs ->
let (occs,x) = f (Locusops.initialize_occurrence_counter occs) x in
Locusops.check_used_occurrences occs;
x
(** Applying a function over a named_declaration with an hypothesis
location request *)
let map_named_declaration_with_hyploc f hyploc acc decl =
let open Context.Named.Declaration in
let f acc typ =
let acc, typ = f (Some (NamedDecl.get_id decl, hyploc)) acc typ in
acc, typ
in
match decl,hyploc with
| LocalAssum (id,_), InHypValueOnly ->
user_err (explain_incorrect_in_value_occurrence id.Context.binder_name)
| LocalAssum (id,typ), _ ->
let acc,typ = f acc typ in acc, LocalAssum (id,typ)
| LocalDef (id,body,typ), InHypTypeOnly ->
let acc,typ = f acc typ in acc, LocalDef (id,body,typ)
| LocalDef (id,body,typ), InHypValueOnly ->
let acc,body = f acc body in acc, LocalDef (id,body,typ)
| LocalDef (id,body,typ), InHyp ->
let acc,body = f acc body in
let acc,typ = f acc typ in
acc, LocalDef (id,body,typ)
(** Finding a subterm up to some testing function *)
exception SubtermUnificationError of subterm_unification_error
type ('a, 'b) testing_function = {
match_fun : int -> 'a -> EConstr.constr -> ('b, unit) Result.t;
merge_fun : 'b -> 'a -> ('a, unit) Result.t;
mutable testing_state : 'a;
mutable last_found : position_reporting 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 env sigma like_first test bywhat cl count t =
let count = ref count in
let rec substrec (nested, k) t =
if Locusops.occurrences_done !count then t else
match test.match_fun k test.testing_state t with
| Result.Ok subst ->
let selected, count' = Locusops.update_occurrence_counter !count in
let () = count := count' in
if selected then
let pos = Locusops.current_occurrence !count in
if nested then
(* in case it is nested but not later detected as unconvertible,
as when matching "id _" in "id (id 0)" *)
let lastpos = Option.get test.last_found in
raise (SubtermUnificationError (nested, ((cl, pos), t), lastpos))
else match test.merge_fun subst test.testing_state with
| Result.Ok state ->
let () = test.testing_state <- state in
let () = test.last_found <- Some ((cl, pos), t) in
(* Check nested matching subterms *)
let () =
if Locusops.more_specific_occurrences !count then
ignore (subst_below (true, k) t)
in
Vars.lift k (bywhat ())
| Result.Error () ->
if like_first then subst_below (nested, k) t
else
let lastpos = Option.get test.last_found in
raise (SubtermUnificationError (nested, ((cl, pos), t), lastpos))
else
subst_below (nested, k) t
| Result.Error () ->
subst_below (nested, k) t
and subst_below k t =
map_constr_with_binders_left_to_right env sigma (fun d (nested, k) -> (nested, k + 1)) substrec k t
in
let t' = substrec (false, 0) t in
(!count, t')
let replace_term_occ_modulo env evd 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 env evd like_first test bywhat None) occs' t
let replace_term_occ_decl_modulo env evd 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 env evd like_first test bywhat)
hyploc)
plocs d
(** Finding an exact subterm *)
let make_eq_univs_test env evd c =
{ match_fun = (fun k evd c' ->
match EConstr.eq_constr_universes_proj env evd c c' with
| None -> Result.Error ()
| Some cst ->
try Result.Ok (Evd.add_universe_constraints evd cst)
with Evd.UniversesDiffer | UGraph.UniverseInconsistency _ -> Result.Error ()
);
merge_fun = (fun evd _ -> Result.Ok evd);
testing_state = evd;
last_found = None
}
let subst_closed_term_occ env evd occs c t =
let test = make_eq_univs_test env evd c in
let bywhat () = mkRel 1 in
let t' = replace_term_occ_modulo env evd occs test bywhat t in
t', test.testing_state
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 env evd like_first test bywhat None)
hyploc) plocs d,
test.testing_state
|
