Source file redexpr.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
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
open Pp
open CErrors
open Util
open Names
open Constr
open EConstr
open Genredexpr
open Pattern
open Reductionops
open Tacred
open RedFlags
open Libobject
let warn_vm_disabled =
CWarnings.create ~name:"vm-compute-disabled" ~category:CWarnings.CoreCategories.bytecode_compiler
(fun () ->
strbrk "vm_compute disabled at configure time; falling back to cbv.")
let cbv_vm env sigma c =
if (Environ.typing_flags env).enable_VM then
let ctyp = Retyping.get_type_of env sigma c in
Vnorm.cbv_vm env sigma c ctyp
else begin
warn_vm_disabled ();
compute env sigma c
end
let warn_native_compute_disabled =
CWarnings.create_in Nativeconv.w_native_disabled
(fun () ->
strbrk "native_compute disabled at configure time; falling back to vm_compute.")
let cbv_native env sigma c =
if (Environ.typing_flags env).enable_native_compiler then
let ctyp = Retyping.get_type_of env sigma c in
Nativenorm.native_norm env sigma c ctyp
else
(warn_native_compute_disabled ();
cbv_vm env sigma c)
let { Goptions.get = simplIsCbn } =
Goptions.declare_bool_option_and_ref
~key:["SimplIsCbn"]
~value:false
()
let set_strategy_one ref l =
Global.set_strategy (Evaluable.to_kevaluable ref) l;
match ref, l with
| Evaluable.EvalConstRef sp, Conv_oracle.Opaque -> ()
| Evaluable.EvalConstRef sp, _ ->
if Declareops.is_opaque (Global.lookup_constant sp) then
user_err
(str "Cannot make" ++ spc () ++
Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef sp) ++
spc () ++ str "transparent because it was declared opaque.")
| _ -> ()
let cache_strategy (_,str) =
List.iter
(fun (lev,ql) -> List.iter (fun q -> set_strategy_one q lev) ql)
str
let subst_strategy (subs,(local,obj)) =
local,
List.Smart.map
(fun (k,ql as entry) ->
let ql' = List.Smart.map (Tacred.subst_evaluable_reference subs) ql in
if ql==ql' then entry else (k,ql'))
obj
let map_strategy f l =
let l' = List.fold_right
(fun (lev,ql) str ->
let ql' = List.fold_right
(fun q ql ->
match f q with
Some q' -> q' :: ql
| None -> ql) ql [] in
if List.is_empty ql' then str else (lev,ql')::str) l [] in
if List.is_empty l' then None else Some (false,l')
let classify_strategy (local,_) =
if local then Dispose else Substitute
let disch_ref ref =
match ref with
| Evaluable.EvalConstRef c -> Some ref
| Evaluable.EvalProjectionRef p ->
let p = Lib.discharge_proj_repr p in
Some (Evaluable.EvalProjectionRef p)
| Evaluable.EvalVarRef id -> if Lib.is_in_section (GlobRef.VarRef id) then None else Some ref
let discharge_strategy (local,obj) =
if local then None else
map_strategy disch_ref obj
type strategy_obj = bool * (Conv_oracle.level * Evaluable.t list) list
let inStrategy : strategy_obj -> obj =
declare_object
{(default_object "STRATEGY") with
cache_function = cache_strategy;
load_function = (fun _ obj -> cache_strategy obj);
subst_function = subst_strategy;
discharge_function = discharge_strategy;
classify_function = classify_strategy;
}
let set_strategy local str =
Lib.add_leaf (inStrategy (local,str))
type red_expr = (constr, Evaluable.t, constr_pattern, int) red_expr_gen
type red_expr_val =
(constr, Evaluable.t, constr_pattern, int, strength * RedFlags.reds) red_expr_gen0
let make_flag_constant = function
| Evaluable.EvalVarRef id -> [fVAR id]
| Evaluable.EvalConstRef sp ->
begin
match Structures.PrimitiveProjections.find_opt sp with
| None -> [fCONST sp]
| Some p -> [fCONST sp; fPROJ p]
end
| Evaluable.EvalProjectionRef p -> [fPROJ p; fCONST (Projection.Repr.constant p)]
let make_flag env f =
let red = no_red in
let red = if f.rBeta then red_add red fBETA else red in
let red = if f.rMatch then red_add red fMATCH else red in
let red = if f.rFix then red_add red fFIX else red in
let red = if f.rCofix then red_add red fCOFIX else red in
let red = if f.rZeta then red_add red fZETA else red in
let red =
if f.rDelta then
let red = red_add red fDELTA in
let red = red_add_transparent red
(Conv_oracle.get_transp_state (Environ.oracle env)) in
List.fold_right
(fun v red -> red_sub_list red (make_flag_constant v))
f.rConst red
else
let red = red_add red fDELTA in
List.fold_right
(fun v red -> red_add_list red (make_flag_constant v))
f.rConst red
in
f.rStrength, red
let reduction_tab = ref String.Map.empty
let red_expr_tab = Summary.ref String.Map.empty ~name:"Declare Reduction"
let declare_reduction s f =
if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab
then user_err
(str "There is already a reduction expression of name " ++ str s ++ str ".")
else reduction_tab := String.Map.add s f !reduction_tab
let check_custom = function
| ExtraRedExpr s ->
if not (String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab)
then user_err (str "Reference to undefined reduction expression " ++ str s ++ str ".")
|_ -> ()
let decl_red_expr s e =
if String.Map.mem s !reduction_tab || String.Map.mem s !red_expr_tab
then user_err
(str "There is already a reduction expression of name " ++ str s ++ str ".")
else begin
check_custom e;
red_expr_tab := String.Map.add s e !red_expr_tab
end
let out_arg = function
| Locus.ArgVar _ -> anomaly (Pp.str "Unevaluated or_var variable.")
| Locus.ArgArg x -> x
let check_occurrences occs =
match occs with
| Locus.OnlyOccurrences (n::_ as nl) when n < 0 ->
Locus.AllOccurrencesBut (List.map abs nl)
| Locus.OnlyOccurrences nl when List.exists (fun n -> n < 0) nl ->
CErrors.user_err Pp.(str "Illegal negative occurrence number.")
| Locus.OnlyOccurrences _ | Locus.AllOccurrencesBut _ | Locus.NoOccurrences
| Locus.AllOccurrences | Locus.AtLeastOneOccurrence -> occs
let out_occurrences occs =
let occs = Locusops.occurrences_map (List.map out_arg) occs in
check_occurrences occs
let out_with_occurrences (occs,c) =
(out_occurrences occs, c)
let e_red f env evm c = evm, f env evm c
let contextualize f = function
| Some (occs,c) ->
let l = check_occurrences occs in
let b,c = match c with
| Inl r -> true,PRef (global_of_evaluable_reference r)
| Inr c -> false,c in
e_red (contextually b (l,c) (fun _ -> f))
| None -> e_red f
let warn_simpl_unfolding_modifiers =
CWarnings.create ~name:"simpl-unfolding-modifiers" ~category:CWarnings.CoreCategories.tactics
(fun () ->
Pp.strbrk "The legacy simpl ignores constant unfolding modifiers.")
let rec eval_red_expr env = function
| Simpl (f, o) ->
let () =
if not (simplIsCbn () || List.is_empty f.rConst) then
warn_simpl_unfolding_modifiers () in
let f = if simplIsCbn () then make_flag env f else f.rStrength, RedFlags.all in
Simpl (f, o)
| Cbv f -> Cbv (make_flag env f)
| Cbn f -> Cbn (make_flag env f)
| Lazy f -> Lazy (make_flag env f)
| ExtraRedExpr s ->
begin match String.Map.find s !red_expr_tab with
| e -> eval_red_expr env e
| exception Not_found -> ExtraRedExpr s
end
| (Red | Hnf | Unfold _ | Fold _ | Pattern _ | CbvVm _ | CbvNative _) as e -> e
let red_product_exn env sigma c = match red_product env sigma c with
| None -> user_err Pp.(str "No head constant to reduce.")
| Some c -> c
let reduction_of_red_expr_val = function
| Red -> (e_red red_product_exn, DEFAULTcast)
| Hnf -> (e_red hnf_constr,DEFAULTcast)
| Simpl ((w,f),o) ->
let am = match w, simplIsCbn () with
| Norm, true -> Cbn.norm_cbn f
| Norm, false -> simpl
| Head, true -> Cbn.whd_cbn f
| Head, false -> whd_simpl
in
(contextualize am o,DEFAULTcast)
| Cbv (Norm, f) -> (e_red (cbv_norm_flags ~strong:true f),DEFAULTcast)
| Cbv (Head, f) -> (e_red (cbv_norm_flags ~strong:false f),DEFAULTcast)
| Cbn (w,f) ->
let cbn = match w with Norm -> Cbn.norm_cbn | Head -> Cbn.whd_cbn in
(e_red (cbn f), DEFAULTcast)
| Lazy (w,f) ->
let redf = match w with Norm -> clos_norm_flags | Head -> clos_whd_flags in
(e_red (redf f),DEFAULTcast)
| Unfold ubinds -> (e_red (unfoldn (List.map (on_fst check_occurrences) ubinds)),DEFAULTcast)
| Fold cl -> (e_red (fold_commands cl),DEFAULTcast)
| Pattern lp -> (pattern_occs (List.map (on_fst check_occurrences) lp),DEFAULTcast)
| ExtraRedExpr s ->
(try (e_red (String.Map.find s !reduction_tab),DEFAULTcast)
with Not_found ->
user_err
(str "Unknown user-defined reduction \"" ++ str s ++ str "\"."))
| CbvVm o -> (contextualize cbv_vm o, VMcast)
| CbvNative o -> (contextualize cbv_native o, NATIVEcast)
let reduction_of_red_expr env r =
reduction_of_red_expr_val (eval_red_expr env r)
let error_illegal_clause () =
CErrors.user_err Pp.(str "\"at\" clause not supported in presence of an occurrence clause.")
let error_multiple_patterns () =
CErrors.user_err Pp.(str "\"at\" clause in occurences not supported with multiple patterns or references.")
let error_illegal_non_atomic_clause () =
CErrors.user_err Pp.(str "\"at\" clause not supported in presence of a non atomic \"in\" clause.")
let error_at_in_occurrences_not_supported () =
CErrors.user_err Pp.(str "\"at\" clause not supported for this reduction tactic.")
let bind_red_expr_occurrences occs nbcl redexp =
let open Locus in
let has_at_clause = function
| Unfold l -> List.exists (fun (occl,_) -> occl != AllOccurrences) l
| Pattern l -> List.exists (fun (occl,_) -> occl != AllOccurrences) l
| Simpl (_,Some (occl,_)) -> occl != AllOccurrences
| _ -> false in
if occs == AllOccurrences then
if nbcl > 1 && has_at_clause redexp then
error_illegal_non_atomic_clause ()
else
redexp
else
match redexp with
| Unfold (_::_::_) ->
error_multiple_patterns ()
| Unfold [(occl,c)] ->
if occl != AllOccurrences then
error_illegal_clause ()
else
Unfold [(occs,c)]
| Pattern (_::_::_) ->
error_multiple_patterns ()
| Pattern [(occl,c)] ->
if occl != AllOccurrences then
error_illegal_clause ()
else
Pattern [(occs,c)]
| Simpl (f,Some (occl,c)) ->
if occl != AllOccurrences then
error_illegal_clause ()
else
Simpl (f,Some (occs,c))
| CbvVm (Some (occl,c)) ->
if occl != AllOccurrences then
error_illegal_clause ()
else
CbvVm (Some (occs,c))
| CbvNative (Some (occl,c)) ->
if occl != AllOccurrences then
error_illegal_clause ()
else
CbvNative (Some (occs,c))
| Red | Hnf | Cbv _ | Lazy _ | Cbn _
| ExtraRedExpr _ | Fold _ | Simpl (_,None) | CbvVm None | CbvNative None ->
error_at_in_occurrences_not_supported ()
| Unfold [] | Pattern [] ->
assert false
let reduction_of_red_expr_val ?occs r =
let r = match occs with
| None -> r
| Some (occs, nbcl) -> bind_red_expr_occurrences occs nbcl r
in
reduction_of_red_expr_val r
let subst_mps subst c =
EConstr.of_constr (Mod_subst.subst_mps subst (EConstr.Unsafe.to_constr c))
let subst_red_expr subs =
let env = Global.env () in
let sigma = Evd.from_env env in
Redops.map_red_expr_gen
(subst_mps subs)
(Tacred.subst_evaluable_reference subs)
(Patternops.subst_pattern env sigma subs)
let inReduction : bool * string * red_expr -> obj =
declare_object
{(default_object "REDUCTION") with
cache_function = (fun (_,s,e) -> decl_red_expr s e);
load_function = (fun _ (_,s,e) -> decl_red_expr s e);
subst_function =
(fun (subs,(b,s,e)) -> b,s,subst_red_expr subs e);
classify_function =
(fun ((b,_,_)) -> if b then Dispose else Substitute) }
let declare_red_expr locality s expr =
Lib.add_leaf (inReduction (locality,s,expr))
let make0 ?dyn name =
let wit = Genarg.make0 name in
let () = Geninterp.register_val0 wit dyn in
wit
let wit_red_expr = make0 "redexpr"
module Intern = struct
open CAst
open Constrexpr
open Libnames
let evalref_of_globref ?loc r =
let () =
let is_proof_variable = match r with
| GlobRef.VarRef x -> (try ignore (Global.lookup_named x); false with Not_found -> true)
| _ -> false
in
if not is_proof_variable then Dumpglob.add_glob ?loc r
in
Tacred.soft_evaluable_of_global_reference ?loc r
type ('constr,'ref,'pat) intern_env = {
strict_check : bool;
local_ref : qualid -> 'ref option;
global_ref : ?short:lident -> Evaluable.t -> 'ref;
intern_constr : constr_expr -> 'constr;
ltac_sign : Constrintern.ltac_sign;
intern_pattern : constr_expr -> 'pat;
pattern_of_glob : Glob_term.glob_constr -> 'pat;
}
let intern_global_reference ist qid =
match ist.local_ref qid with
| Some v -> v
| None ->
let r =
try Smartlocate.locate_global_with_alias ~head:true qid
with
| Not_found as exn ->
if not ist.strict_check && qualid_is_ident qid then
let id = qualid_basename qid in
GlobRef.VarRef id
else
let _, info = Exninfo.capture exn in
Nametab.error_global_not_found ~info qid
in
let short =
if qualid_is_ident qid && not ist.strict_check then
Some (make ?loc:qid.CAst.loc @@ qualid_basename qid)
else None
in
let r = evalref_of_globref ?loc:qid.loc r in
ist.global_ref ?short r
let intern_evaluable ist = function
| {v=AN qid} -> intern_global_reference ist qid
| {v=ByNotation (ntn,sc);loc} ->
let check = GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) in
let r = Notation.interp_notation_as_global_reference ?loc ~head:true check ntn sc in
let r = evalref_of_globref ?loc r in
ist.global_ref r
let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
let interp_ref r =
try Inl (intern_evaluable ist r)
with e when CErrors.noncritical e ->
let r = match r with
| {CAst.v=AN r} -> r
| {loc} -> (qualid_of_path ?loc (Nametab.path_of_global (Smartlocate.smart_global r))) in
let loc = r.loc in
let c = Constrintern.interp_reference ist.ltac_sign r in
match DAst.get c with
| GRef (r,None) ->
let r = evalref_of_globref ?loc r in
Inl (ist.global_ref r)
| GVar id ->
let r = evalref_of_globref (GlobRef.VarRef id) in
Inl (ist.global_ref r)
| _ ->
Inr (ist.pattern_of_glob c)
in
let p = match p with
| Inl r -> interp_ref r
| Inr { v = CAppExpl((r,None),[]) } ->
interp_ref (make @@ AN r)
| Inr c ->
Inr (ist.intern_pattern c)
in
(l, p)
let intern_constr_with_occurrences ist (l,c) = (l,ist.intern_constr c)
let intern_flag ist red =
{ red with rConst = List.map (intern_evaluable ist) red.rConst }
let intern_unfold ist (l,qid) = (l,intern_evaluable ist qid)
let intern_red_expr ist = function
| Unfold l -> Unfold (List.map (intern_unfold ist) l)
| Fold l -> Fold (List.map ist.intern_constr l)
| Cbv f -> Cbv (intern_flag ist f)
| Cbn f -> Cbn (intern_flag ist f)
| Lazy f -> Lazy (intern_flag ist f)
| Pattern l -> Pattern (List.map (intern_constr_with_occurrences ist) l)
| Simpl (f,o) ->
Simpl (intern_flag ist f,
Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o)
| CbvVm o -> CbvVm (Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o)
| CbvNative o -> CbvNative (Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o)
| (Red | Hnf | ExtraRedExpr _ as r ) -> r
let intern_constr env c =
Constrintern.intern_gen WithoutTypeConstraint ~strict_check:true env (Evd.from_env env) c
let intern_pattern env c =
Constrintern.intern_gen WithoutTypeConstraint ~strict_check:true ~pattern_mode:true
env (Evd.from_env env) c
let from_env env = {
strict_check = true;
local_ref = (fun _ -> None);
global_ref = (fun ?short:_ r -> r);
intern_constr = intern_constr env;
ltac_sign = Constrintern.empty_ltac_sign;
pattern_of_glob = (fun c -> c);
intern_pattern = intern_pattern env;
}
end
module Interp = struct
type ('constr,'evref,'pat) interp_env = {
interp_occurrence_var : lident -> int list;
interp_constr : Environ.env -> Evd.evar_map -> 'constr -> Evd.evar_map * EConstr.constr;
interp_constr_list : Environ.env -> Evd.evar_map -> 'constr -> Evd.evar_map * EConstr.constr list;
interp_evaluable : Environ.env -> Evd.evar_map -> 'evref -> Evaluable.t;
interp_pattern : Environ.env -> Evd.evar_map -> 'pat -> constr_pattern;
interp_evaluable_or_pattern : Environ.env -> Evd.evar_map
-> 'evref -> (Evaluable.t, constr_pattern) Util.union
}
let interp_occurrences ist occs =
let open Locus in
let map = function
| ArgArg x -> [x]
| ArgVar lid -> ist.interp_occurrence_var lid
in
Locusops.occurrences_map (List.concat_map map) occs
let interp_constr_with_occurrences ist env sigma (occs,c) =
let (sigma,c_interp) = ist.interp_constr env sigma c in
sigma , (interp_occurrences ist occs, c_interp)
let interp_evaluable ist env sigma r = ist.interp_evaluable env sigma r
let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, p) =
let p = match p with
| Inr p -> Inr (ist.interp_pattern env sigma p)
| Inl r -> ist.interp_evaluable_or_pattern env sigma r
in
interp_occurrences ist occs, p
let interp_unfold ist env sigma (occs,qid) =
(interp_occurrences ist occs,interp_evaluable ist env sigma qid)
let interp_flag ist env sigma red =
{ red with rConst = List.map (interp_evaluable ist env sigma) red.rConst }
let interp_red_expr ist env sigma = function
| Unfold l -> sigma , Unfold (List.map (interp_unfold ist env sigma) l)
| Fold l ->
let (sigma,l_interp) = List.fold_left_map (ist.interp_constr_list env) sigma l in
sigma , Fold (List.flatten l_interp)
| Cbv f -> sigma , Cbv (interp_flag ist env sigma f)
| Cbn f -> sigma , Cbn (interp_flag ist env sigma f)
| Lazy f -> sigma , Lazy (interp_flag ist env sigma f)
| Pattern l ->
let (sigma,l_interp) =
Evd.MonadR.List.map_right
(fun c sigma -> interp_constr_with_occurrences ist env sigma c) l sigma
in
sigma , Pattern l_interp
| Simpl (f,o) ->
sigma , Simpl (interp_flag ist env sigma f,
Option.map (interp_closed_typed_pattern_with_occurrences ist env sigma) o)
| CbvVm o ->
sigma , CbvVm (Option.map (interp_closed_typed_pattern_with_occurrences ist env sigma) o)
| CbvNative o ->
sigma , CbvNative (Option.map (interp_closed_typed_pattern_with_occurrences ist env sigma) o)
| (Red | Hnf | ExtraRedExpr _ as r) -> sigma , r
let interp_constr env sigma c =
let flags = Pretyping.all_and_fail_flags in
Pretyping.understand_ltac flags env sigma Glob_ops.empty_lvar WithoutTypeConstraint c
let interp_constr_list env sigma c =
let sigma, c = interp_constr env sigma c in
sigma, [c]
let interp_pattern env sigma c =
let flags = { Pretyping.no_classes_no_fail_inference_flags with expand_evars = false } in
let sigma, c = Pretyping.understand_ltac flags env sigma Glob_ops.empty_lvar WithoutTypeConstraint c in
Patternops.legacy_bad_pattern_of_constr env sigma c
let without_ltac = {
interp_occurrence_var = (fun lid ->
user_err ?loc:lid.loc (str "Unbound variable " ++ Id.print lid.v ++ str "."));
interp_constr;
interp_constr_list;
interp_evaluable = (fun _ _ x -> x);
interp_pattern;
interp_evaluable_or_pattern = (fun _ _ r -> Inl r);
}
end
let interp_redexp_no_ltac env sigma r =
let r = Intern.(intern_red_expr (from_env env) r) in
Interp.(interp_red_expr without_ltac) env sigma r