Source file comRewriteRule.ml
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
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
open Util
open Names
let maybe_error_many_udecls = function
| ({CAst.loc;v=id}, Some _) ->
CErrors.user_err ?loc
Pp.(strbrk "When declaring multiple symbols in one command, " ++
strbrk "only the first is allowed a universe binder " ++
strbrk "(which will be shared by the whole block).")
| (_, None) -> ()
let preprocess_symbols l =
let open Vernacexpr in
if Global.sections_are_opened () then
CErrors.user_err Pp.(str "Declaring a symbol is not allowed in sections.");
let udecl = match l with
| (coe, ((id, udecl)::rest, c))::rest' ->
List.iter maybe_error_many_udecls rest;
List.iter (fun (coe, (idl, c)) -> List.iter maybe_error_many_udecls idl) rest';
udecl
| (_, ([], _))::_ | [] -> assert false
in
let no_coercion_msg = Pp.(str "Cannot deal with coercions in symbols") in
List.iter (function AddCoercion, (({CAst.loc; _}, _) :: _, _) -> CErrors.user_err ?loc no_coercion_msg | AddCoercion, _ -> assert false | _ -> ()) l;
udecl, List.concat_map (fun (coe, (idl, c)) -> List.map (fun (id, _) -> id, c) idl) l
let do_symbol ~poly ~unfold_fix udecl (id, typ) =
if Dumpglob.dump () then Dumpglob.dump_definition id false "symb";
let id = id.CAst.v in
let env = Global.env () in
let evd, udecl = Constrintern.interp_univ_decl_opt env udecl in
let evd, (typ, impls) =
Constrintern.(interp_type_evars_impls ~impls:empty_internalization_env)
env evd typ
in
Pretyping.check_evars_are_solved ~program_mode:false env evd;
let evd = Evd.minimize_universes evd in
let _qvars, uvars = EConstr.universes_of_constr evd typ in
let evd = Evd.restrict_universe_context evd uvars in
let typ = EConstr.to_constr evd typ in
let univs = Evd.check_univ_decl ~poly evd udecl in
let entry = Declare.symbol_entry ~univs ~unfold_fix typ in
let kn = Declare.declare_constant ~name:id ~kind:Decls.IsSymbol (Declare.SymbolEntry entry) in
let () = Impargs.maybe_declare_manual_implicits false (GlobRef.ConstRef kn) impls in
let () = Declare.assumption_message id in
()
let do_symbols ~poly ~unfold_fix l =
let env = Global.env () in
if not @@ Environ.rewrite_rules_allowed env then raise Environ.(RewriteRulesNotAllowed Symb);
let udecl, l = preprocess_symbols l in
List.iter (do_symbol ~poly ~unfold_fix udecl) l
open Util
open Constr
open Declarations
type state = (int * int Evar.Map.t) * (int * int Int.Map.t) * (int * int Int.Map.t)
let rec is_rel_inst k = function
| SList.Nil -> true
| SList.Default _ -> false
| SList.Cons (t, l) -> kind t = Rel k && is_rel_inst (succ k) l
let update_invtbl ~loc env evd evk (curvar, tbl) =
curvar, (succ curvar, tbl |> Evar.Map.update evk @@ function
| None -> Some curvar
| Some k as c when k = curvar -> c
| Some k ->
CErrors.user_err ?loc
Pp.(str "Variable "
++ Termops.pr_existential_key env evd evk
++ str" is bound multiple times in the pattern (holes number "
++ int k ++ str" and " ++ int curvar ++ str")."))
let update_invtblu1 ~loc evd lvlold lvl (curvaru, tbl) =
succ curvaru, tbl |> Int.Map.update lvl @@ function
| None -> Some curvaru
| Some k as c when k = curvaru -> c
| Some k ->
CErrors.user_err ?loc
Pp.(str "Universe variable "
++ Termops.pr_evd_level evd lvlold
++ str" is bound multiple times in the pattern (holes number "
++ int k ++ str" and " ++ int curvaru ++ str").")
let update_invtblq1 ~loc evd qold qvar (curvarq, tbl) =
succ curvarq, tbl |> Int.Map.update qvar @@ function
| None -> Some curvarq
| Some k as c when k = curvarq -> c
| Some k ->
CErrors.user_err ?loc
Pp.(str "Sort variable "
++ Sorts.Quality.pr (Termops.pr_evd_qvar evd) qold
++ str" is bound multiple times in the pattern (holes number "
++ int k ++ str" and " ++ int curvarq ++ str").")
let safe_quality_pattern_of_quality ~loc evd qsubst stateq q =
match Sorts.Quality.(subst (subst_fn qsubst) q) with
| QConstant qc -> stateq, PQConstant qc
| QVar qv ->
let qio = Sorts.QVar.var_index qv in
let stateq = Option.fold_right (update_invtblq1 ~loc evd q) qio stateq in
stateq, PQVar qio
let update_invtblu ~loc evd (qsubst, usubst) (state, stateq, stateu : state) u : state * _ =
let (q, u) = u |> UVars.Instance.to_array in
let stateq, maskq = Array.fold_left_map (safe_quality_pattern_of_quality ~loc evd qsubst) stateq q
in
let stateu, masku = Array.fold_left_map (fun stateu lvlold ->
let lvlnew = Univ.Level.var_index @@ Univ.subst_univs_level_level usubst lvlold in
Option.fold_right (update_invtblu1 ~loc evd lvlold) lvlnew stateu, lvlnew
) stateu u
in
(state, stateq, stateu), (maskq, masku)
let universe_level_subst_var_index usubst u =
match Univ.Universe.level u with
| None -> None
| Some lvlold ->
let lvl = Univ.subst_univs_level_level usubst lvlold in
Option.map (fun lvl -> lvlold, lvl) @@ Univ.Level.var_index lvl
let safe_sort_pattern_of_sort ~loc evd (qsubst, usubst) (st, sq, su as state) s =
let open Sorts in
match s with
| Type u ->
begin match universe_level_subst_var_index usubst u with
| None -> state, PSType None
| Some (lvlold, lvl) ->
(st, sq, update_invtblu1 ~loc evd lvlold lvl su), PSType (Some lvl)
end
| SProp -> state, PSSProp
| Prop -> state, PSProp
| Set -> state, PSSet
| QSort (qold, u) ->
let sq, bq =
match Sorts.Quality.(var_index @@ subst_fn qsubst qold) with
| Some q -> update_invtblq1 ~loc evd (QVar qold) q sq, Some q
| None -> sq, None
in
let su, ba =
match universe_level_subst_var_index usubst u with
| Some (lvlold, lvl) -> update_invtblu1 ~loc evd lvlold lvl su, Some lvl
| None -> su, None
in
(st, sq, su), PSQSort (bq, ba)
let warn_irrelevant_pattern =
CWarnings.create ~name:"irrelevant-pattern"
(fun () -> Pp.(str "This subpattern is irrelevant and can never be matched against."))
let warn_eta_in_pattern =
CWarnings.create ~name:"eta-in-pattern" Fun.id
let warn_redex_in_rewrite_rules =
CWarnings.create ~name:"redex-in-rewrite-rules"
(fun redex -> Pp.(str "This pattern contains a" ++ redex ++ str " which may prevent this rule from being triggered."))
let rec check_may_eta ~loc env evd t =
match EConstr.kind evd (Reductionops.whd_all env evd t) with
| Prod _ ->
warn_eta_in_pattern ?loc
Pp.(str "This subpattern has a product type, but pattern-matching is not done modulo eta, so this rule may not trigger at required times.")
| Sort _ -> ()
| Ind (ind, u) ->
let specif = Inductive.lookup_mind_specif env ind in
if not @@ Inductive.is_primitive_record specif then () else
warn_eta_in_pattern ?loc
Pp.(str "This subpattern has a primitive record type, but pattern-matching is not done modulo eta, so this rule may not trigger at required times.")
| App (i, _) -> check_may_eta ~loc env evd i
| _ ->
warn_eta_in_pattern ?loc
Pp.(str "This subpattern has a yet unknown type, which may be a product type, but pattern-matching is not done modulo eta, so this rule may not trigger at required times.")
let test_may_eta ~loc env evd constr =
let t = Retyping.get_type_of env evd constr in
let () = check_may_eta ~loc env evd t in
()
let rec safe_pattern_of_constr_aux ~loc env evd usubst depth state t = Constr.kind t |> function
| App (f, args) ->
let state, (head, elims) = safe_pattern_of_constr_aux ~loc env evd usubst depth state f in
let state, pargs = Array.fold_left_map (safe_arg_pattern_of_constr ~loc env evd usubst depth) state args in
state, (head, elims @ [PEApp pargs])
| Case (ci, u, params, (ret, _), _, c, brs) ->
let mib, mip = Inductive.lookup_mind_specif env ci.ci_ind in
let state, mask = update_invtblu ~loc evd usubst state u in
let state, (head, elims) = safe_pattern_of_constr_aux ~loc env evd usubst depth state c in
let paramdecl = Vars.subst_instance_context u mib.mind_params_ctxt in
let paramsubst = Vars.subst_of_rel_context_instance paramdecl params in
let state, pret =
let (nas, p) = ret in
let realdecls, _ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in
let self =
let args = Context.Rel.instance mkRel 0 mip.mind_arity_ctxt in
let inst = UVars.Instance.(abstract_instance (length u)) in
mkApp (mkIndU (ci.ci_ind, inst), args)
in
let realdecls = Context.Rel.Declaration.LocalAssum (Context.make_annot Anonymous mip.mind_relevance, self) :: realdecls in
let realdecls =
Inductive.instantiate_context u paramsubst nas realdecls
in
let p_env = Environ.push_rel_context realdecls env in
safe_arg_pattern_of_constr ~loc p_env evd usubst (depth + Array.length nas) state p
in
let do_one_branch i state (nas, br) =
let (ctx, cty) = mip.mind_nf_lc.(i) in
let bctx, _ = List.chop mip.mind_consnrealdecls.(i) ctx in
let bctx = Inductive.instantiate_context u paramsubst nas bctx in
let br_env = Environ.push_rel_context bctx env in
safe_arg_pattern_of_constr ~loc br_env evd usubst (depth + Array.length nas) state br
in
let state, pbrs = Array.fold_left_map_i do_one_branch state brs in
state, (head, elims @ [PECase (ci.ci_ind, mask, pret, pbrs)])
| Proj (p, _, c) ->
let state, (head, elims) = safe_pattern_of_constr_aux ~loc env evd usubst depth state c in
state, (head, elims @ [PEProj p])
| _ ->
let state, head = safe_head_pattern_of_constr ~loc env evd usubst depth state t in
state, (head, [])
and safe_pattern_of_constr ~loc env evd usubst depth state t =
begin match EConstr.ERelevance.kind evd @@ Retyping.relevance_of_term env evd (EConstr.of_constr t) with
| Sorts.Irrelevant -> warn_irrelevant_pattern ?loc ()
| Sorts.RelevanceVar _ -> ()
| Sorts.Relevant -> ()
end;
safe_pattern_of_constr_aux ~loc env evd usubst depth state t
and safe_head_pattern_of_constr ~loc env evd usubst depth state t = Constr.kind t |> function
| Const (c, u) when Environ.is_symbol env c ->
let state, mask = update_invtblu ~loc evd usubst state u in
state, PHSymbol (c, mask)
| Rel i ->
assert (i <= depth);
state, PHRel i
| Sort s ->
let state, ps = safe_sort_pattern_of_sort ~loc evd usubst state s in
state, PHSort ps
| Ind (ind, u) ->
let state, mask = update_invtblu ~loc evd usubst state u in
state, PHInd (ind, mask)
| Construct (c, u) ->
let state, mask = update_invtblu ~loc evd usubst state u in
state, PHConstr (c, mask)
| Int i -> state, PHInt i
| Float f -> state, PHFloat f
| String s -> state, PHString s
| Lambda _ ->
let (ntys, b) = Term.decompose_lambda t in
let tys = Array.rev_of_list ntys in
let (state, env), ptys = Array.fold_left_map_i
(fun i (state, env) (na, ty) ->
let state, p = safe_arg_pattern_of_constr ~loc env evd usubst (depth+i) state ty in
(state, Environ.push_rel (LocalAssum (na, ty)) env), p)
(state, env) tys
in
let state, pbod = safe_arg_pattern_of_constr ~loc env evd usubst (depth + Array.length tys) state b in
state, PHLambda (ptys, pbod)
| Prod _ ->
let (ntys, b) = Term.decompose_prod t in
let tys = Array.rev_of_list ntys in
let (state, env), ptys = Array.fold_left_map_i
(fun i (state, env) (na, ty) ->
let state, p = safe_arg_pattern_of_constr ~loc env evd usubst (depth+i) state ty in
(state, Environ.push_rel (LocalAssum (na, ty)) env), p)
(state, env) tys
in
let state, pbod = safe_arg_pattern_of_constr ~loc env evd usubst (depth + Array.length tys) state b in
state, PHProd (ptys, pbod)
| _ ->
CErrors.user_err ?loc Pp.(str "Subterm not recognised as pattern: " ++ Printer.safe_pr_lconstr_env env evd t)
and safe_arg_pattern_of_constr ~loc env evd usubst depth (st, stateq, stateu as state) t = Constr.kind t |> function
| Evar (evk, inst) ->
let EvarInfo evi = Evd.find evd evk in
(match snd (Evd.evar_source evi) with
| Evar_kinds.MatchingVar (Evar_kinds.FirstOrderPatVar id) ->
let holei, st = update_invtbl ~loc env evd evk st in
if not @@ is_rel_inst 1 inst then
CErrors.user_err ?loc
Pp.(str "In " ++ Printer.safe_pr_lconstr_env env evd (of_kind (Evar (evk, inst)))
++ str ", variable "
++ Termops.pr_existential_key env evd evk
++ str" appears with a non-trivial instantiation.");
if Evd.evar_hyps evi |> Environ.named_context_of_val |> Context.Named.length <> SList.length inst then
CErrors.user_err ?loc Pp.(str "Pattern variable cannot access the whole context: " ++ Printer.safe_pr_lconstr_env env evd t);
(st, stateq, stateu), EHole holei
| Evar_kinds.NamedHole _ -> CErrors.user_err ?loc Pp.(str "Named holes are not supported, you must use regular evars: " ++ Printer.safe_pr_lconstr_env env evd t)
| _ ->
if Option.is_empty @@ Evd.evar_ident evk evd then state, EHoleIgnored else
CErrors.user_err ?loc Pp.(str "Named evar in unsupported context: " ++ Printer.safe_pr_lconstr_env env evd t)
)
| _ ->
test_may_eta ~loc env evd (EConstr.of_constr t);
let state, p = safe_pattern_of_constr ~loc env evd usubst depth state t in
state, ERigid p
let rec evar_subst evmap evd k t =
match EConstr.kind evd t with
| Evar (evk, inst) -> begin
match Evar.Map.find_opt evk evmap with
| None -> t
| Some (n, vars) ->
let head = EConstr.mkRel (n + k) in
let Evd.EvarInfo evi = Evd.find evd evk in
let body = EConstr.mkApp (head, vars) in
let inst = inst |> SList.Smart.map (evar_subst evmap evd k) in
Evd.instantiate_evar_array evd evi body inst
end
| _ -> EConstr.map_with_binders evd succ (evar_subst evmap evd) k t
let test_projection_apps env evd ~loc ind args =
let specif = Inductive.lookup_mind_specif env ind in
if not @@ Inductive.is_primitive_record specif then () else
if Array.for_all_i (fun i arg ->
match arg with
| EHole _ | EHoleIgnored -> true
| ERigid (_, []) -> false
| ERigid (_, elims) ->
match List.last elims with
| PEProj p -> Ind.CanOrd.equal (Projection.inductive p) ind && Projection.arg p = i
| _ -> false
) 0 args then
warn_redex_in_rewrite_rules ?loc Pp.(str " subpattern compatible with an eta-long form for " ++ Id.print (snd specif).mind_typename ++ str"," )
let rec test_pattern_redex env evd ~loc = function
| PHLambda _, PEApp _ :: _ -> warn_redex_in_rewrite_rules ?loc (Pp.str " beta redex")
| PHConstr _, (PECase _ | PEProj _) :: _ -> warn_redex_in_rewrite_rules ?loc (Pp.str " iota redex")
| PHConstr _, PEApp _ :: (PECase _ | PEProj _) :: _ -> warn_redex_in_rewrite_rules ?loc (Pp.str " iota redex")
| PHLambda _, _ -> warn_redex_in_rewrite_rules ?loc (Pp.str " lambda pattern")
| PHConstr (c, _) as head, PEApp args :: elims -> test_projection_apps env evd ~loc (fst c) args; Array.iter (test_pattern_redex_aux env evd ~loc) args; test_pattern_redex env evd ~loc (head, elims)
| head, PEApp args :: elims -> Array.iter (test_pattern_redex_aux env evd ~loc) args; test_pattern_redex env evd ~loc (head, elims)
| head, PECase (_, _, ret, brs) :: elims -> test_pattern_redex_aux env evd ~loc ret; Array.iter (test_pattern_redex_aux env evd ~loc) brs; test_pattern_redex env evd ~loc (head, elims)
| head, PEProj _ :: elims -> test_pattern_redex env evd ~loc (head, elims)
| PHProd (tys, bod), [] -> Array.iter (test_pattern_redex_aux env evd ~loc) tys; test_pattern_redex_aux env evd ~loc bod
| (PHRel _ | PHInt _ | PHFloat _ | PHString _ | PHSort _ | PHInd _ | PHConstr _ | PHSymbol _), [] -> ()
and test_pattern_redex_aux env evd ~loc = function
| EHole _ | EHoleIgnored -> ()
| ERigid p -> test_pattern_redex env evd ~loc p
let warn_rewrite_rules_break_SR = "rewrite-rules-break-SR"
let rewrite_rules_break_SR_warning =
CWarnings.create_warning ~name:warn_rewrite_rules_break_SR ~default:CWarnings.Enabled ()
let rewrite_rules_break_SR_msg = CWarnings.create_msg rewrite_rules_break_SR_warning ()
let warn_rewrite_rules_break_SR ~loc reason =
CWarnings.warn rewrite_rules_break_SR_msg ?loc reason
let () = CWarnings.register_printer rewrite_rules_break_SR_msg
(fun reason -> Pp.(str "This rewrite rule breaks subject reduction (" ++ reason ++ str ")."))
let interp_rule (udecl, lhs, rhs: Constrexpr.universe_decl_expr option * _ * _) =
let env = Global.env () in
let evd = Evd.from_env env in
let evd, udecl =
let open CAst in let open UState in
match udecl with
| None -> evd, default_univ_decl
| Some udecl ->
let evd, qualities = List.fold_left_map (fun evd lid ->
Evd.new_quality_variable ?loc:lid.loc ~name:lid.v evd)
evd
udecl.univdecl_qualities
in
let evd, instance = List.fold_left_map (fun evd lid ->
Evd.new_univ_level_variable ?loc:lid.loc univ_rigid ~name:lid.v evd)
evd
udecl.univdecl_instance
in
let cstrs =
udecl.univdecl_constraints |> List.to_seq
|> Seq.map (Constrintern.interp_univ_constraint evd)
|> Univ.Constraints.of_seq
in
let decl = {
univdecl_qualities = qualities;
univdecl_extensible_qualities = udecl.univdecl_extensible_qualities;
univdecl_instance = instance;
univdecl_extensible_instance = udecl.univdecl_extensible_instance;
univdecl_constraints = cstrs;
univdecl_extensible_constraints = udecl.univdecl_extensible_constraints;
} in
evd, decl
in
let nvarqs = List.length udecl.univdecl_qualities in
let nvarus = List.length udecl.univdecl_instance in
let lhs_loc = lhs.CAst.loc in
let rhs_loc = rhs.CAst.loc in
let lhs = Constrintern.(intern_gen WithoutTypeConstraint env evd lhs) in
let flags = { Pretyping.no_classes_no_fail_inference_flags with undeclared_evars_patvars = true; patvars_abstract = true; expand_evars = false; solve_unification_constraints = false } in
let evd, lhs, typ = Pretyping.understand_tcc_ty ~flags env evd lhs in
let evd = Evd.minimize_universes evd in
let _qvars, uvars = EConstr.universes_of_constr evd lhs in
let evd = Evd.restrict_universe_context evd uvars in
let uctx, uctx' = UState.check_univ_decl_rev (Evd.evar_universe_context evd) udecl in
let usubst =
let inst, auctx = UVars.abstract_universes uctx' in
UVars.make_instance_subst inst
in
let ((nvars', invtbl), (nvarqs', invtblq), (nvarus', invtblu)), (head_pat, elims) =
safe_pattern_of_constr ~loc:lhs_loc env evd usubst 0 ((1, Evar.Map.empty), (0, Int.Map.empty), (0, Int.Map.empty)) (EConstr.Unsafe.to_constr lhs)
in
let () = test_pattern_redex env evd ~loc:lhs_loc (head_pat, elims) in
let head_symbol, head_umask = match head_pat with PHSymbol (symb, mask) -> symb, mask | _ ->
CErrors.user_err ?loc:lhs_loc
Pp.(str "Head head-pattern is not a symbol.")
in
if nvarus <> nvarus' then begin
assert (nvarus' < nvarus);
CErrors.user_err ?loc:lhs_loc
Pp.(str "Not all universe level variables appear in the pattern.")
end;
if nvarqs <> nvarqs' then begin
assert (nvarqs' < nvarqs);
CErrors.user_err ?loc:lhs_loc
Pp.(str "Not all sort variables appear in the pattern.")
end;
let update_invtbl evd evk n =
let Evd.EvarInfo evi = Evd.find evd evk in
let vars = Evd.evar_hyps evi |> Environ.named_context_of_val |> Context.Named.instance EConstr.mkVar in
(n, vars)
in
let invtbl = Evar.Map.mapi (update_invtbl evd) invtbl in
let evd = Evd.set_universe_context evd uctx in
let rhs = Constrintern.(intern_gen WithoutTypeConstraint env evd rhs) in
let flags = { Pretyping.no_classes_no_fail_inference_flags with patvars_abstract = true } in
let evd', rhs =
try Pretyping.understand_tcc ~flags env evd ~expected_type:(OfType typ) rhs
with Type_errors.TypeError _ | Pretype_errors.PretypeError _ ->
warn_rewrite_rules_break_SR ~loc:rhs_loc (Pp.str "the replacement term doesn't have the type of the pattern");
Pretyping.understand_tcc ~flags env evd rhs
in
let evd' = Evd.minimize_universes evd' in
let _qvars', uvars' = EConstr.universes_of_constr evd' rhs in
let evd' = Evd.restrict_universe_context evd' (Univ.Level.Set.union uvars uvars') in
let fail pp = warn_rewrite_rules_break_SR ~loc:rhs_loc Pp.(str "universe inconsistency, missing constraints: " ++ pp) in
let () = UState.check_uctx_impl ~fail (Evd.evar_universe_context evd) (Evd.evar_universe_context evd') in
let evd = evd' in
let rhs =
let rhs' = evar_subst invtbl evd 0 rhs in
match EConstr.to_constr_opt evd rhs' with
| Some rhs -> rhs
| None ->
let pr_unresolved_evar e =
Pp.(hov 2 (str"- " ++ Printer.pr_existential_key env evd e ++ str ": " ++
Himsg.explain_pretype_error env evd (Pretype_errors.UnsolvableImplicit (e,None))))
in
CErrors.user_err ?loc:rhs_loc Pp.(hov 0 begin
str "The replacement term contains unresolved implicit arguments:"++ fnl () ++
str " " ++ Printer.pr_econstr_env env evd rhs ++ fnl () ++
str "More precisely: " ++ fnl () ++
v 0 (prlist_with_sep cut pr_unresolved_evar (Evar.Set.elements (Evarutil.undefined_evars_of_term evd rhs')))
end)
in
let rhs = Vars.subst_univs_level_constr usubst rhs in
let test_qvar q =
match Sorts.QVar.var_index q with
| Some -1 ->
CErrors.user_err ?loc:rhs_loc
Pp.(str "Sort variable " ++ Termops.pr_evd_qvar evd q ++ str " appears in the replacement but does not appear in the pattern.")
| Some n when n < 0 || n > nvarqs' -> CErrors.anomaly Pp.(str "Unknown sort variable in rewrite rule.")
| Some _ -> ()
| None ->
if not @@ Sorts.QVar.Set.mem q (evd |> Evd.sort_context_set |> fst |> fst) then
CErrors.user_err ?loc:rhs_loc
Pp.(str "Sort variable " ++ Termops.pr_evd_qvar evd q ++ str " appears in the replacement but does not appear in the pattern.")
in
let test_level ?(alg_ok=false) lvl =
match Univ.Level.var_index lvl with
| Some -1 ->
CErrors.user_err ?loc:rhs_loc
Pp.(str "Universe level variable " ++ Termops.pr_evd_level evd lvl ++ str " appears in the replacement but does not appear in the pattern.")
| Some n when n < 0 || n > nvarus' -> CErrors.anomaly Pp.(str "Unknown universe level variable in rewrite rule")
| Some _ -> ()
| None ->
try UGraph.check_declared_universes (Environ.universes env) (Univ.Level.Set.singleton lvl)
with UGraph.UndeclaredLevel lvl ->
CErrors.user_err ?loc:rhs_loc
Pp.(str "Universe level " ++ Termops.pr_evd_level evd lvl ++ str " appears in the replacement but does not appear in the pattern.")
in
let () =
let qs, us = Vars.sort_and_universes_of_constr rhs in
Sorts.QVar.Set.iter test_qvar qs;
Univ.Level.Set.iter test_level us
in
head_symbol, { nvars = (nvars' - 1, nvarqs', nvarus'); lhs_pat = head_umask, elims; rhs }
let do_rules id rules =
let env = Global.env () in
if not @@ Environ.rewrite_rules_allowed env then raise Environ.(RewriteRulesNotAllowed Rule);
let body = { rewrules_rules = List.map interp_rule rules } in
Global.add_rewrite_rules id body