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
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq 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) *)
(************************************************************************)
DECLARE GLOBAL PLUGIN
{
open Pcoq
open Pcoq.Prim
open Pcoq.Constr
open Pvernac.Vernac_
open Util
open Locus
open Genredexpr
let all_with ~head delta =
let all = [FBeta;FMatch;FFix;FCofix;FZeta;delta] in
Redops.make_red_flag (if head then FHead :: all else all)
let int_or_var = Entry.make "int_or_var"
let nat_or_var = Entry.make "nat_or_var"
let pattern_occ = Entry.make "pattern_occ"
let unfold_occ = Entry.make "unfold_occ"
let ref_or_pattern_occ = Entry.make "ref_or_pattern_occ"
let occs_nums = Entry.make "occs_nums"
let occs = Entry.make "occs"
let delta_flag = Entry.make "delta_flag"
let strategy_flag = Entry.make "strategy_flag"
}
GRAMMAR EXTEND Gram
GLOBAL: int_or_var nat_or_var occs occs_nums unfold_occ pattern_occ
delta_flag strategy_flag ref_or_pattern_occ red_expr;
int_or_var:
[ [ n = integer -> { ArgArg n }
| id = identref -> { ArgVar id } ] ]
;
nat_or_var:
[ [ n = natural -> { ArgArg n }
| id = identref -> { ArgVar id } ] ]
;
occs_nums:
[ [ nl = LIST1 nat_or_var -> { OnlyOccurrences nl }
| "-"; nl = LIST1 nat_or_var -> { AllOccurrencesBut nl } ] ]
;
occs:
[ [ "at"; occs = occs_nums -> { occs } | -> { AllOccurrences } ] ]
;
pattern_occ:
[ [ c = constr; nl = occs -> { (nl,c) } ] ]
;
ref_or_pattern_occ:
(* If a string, it is interpreted as a ref
(anyway a Coq string does not reduce) *)
[ [ c = smart_global; nl = occs -> { nl,Inl c }
| c = constr; nl = occs -> { nl,Inr c } ] ]
;
unfold_occ:
[ [ c = smart_global; nl = occs -> { (nl,c) } ] ]
;
red_flag:
[ [ IDENT "beta" -> { [FBeta] }
| IDENT "iota" -> { [FMatch;FFix;FCofix] }
| IDENT "match" -> { [FMatch] }
| IDENT "fix" -> { [FFix] }
| IDENT "cofix" -> { [FCofix] }
| IDENT "zeta" -> { [FZeta] }
| IDENT "delta"; d = delta_flag -> { [d] }
| IDENT "head" -> { [FHead] }
] ]
;
delta_flag:
[ [ "-"; "["; idl = LIST1 smart_global; "]" -> { FDeltaBut idl }
| "["; idl = LIST1 smart_global; "]" -> { FConst idl }
| -> { FDeltaBut [] }
] ]
;
strategy_flag:
[ [ s = LIST1 red_flag -> { Redops.make_red_flag (List.flatten s) }
| h = OPT [ IDENT "head" -> { () } ]; d = delta_flag -> { all_with ~head:(Option.has_some h) d }
] ]
;
red_expr:
[ [ IDENT "red" -> { Red }
| IDENT "hnf" -> { Hnf }
| IDENT "simpl"; h = OPT [ IDENT "head" -> { () } ];
d = delta_flag; po = OPT ref_or_pattern_occ -> { Simpl (all_with ~head:(Option.has_some h) d,po) }
| IDENT "cbv"; s = strategy_flag -> { Cbv s }
| IDENT "cbn"; s = strategy_flag -> { Cbn s }
| IDENT "lazy"; s = strategy_flag -> { Lazy s }
| IDENT "compute"; delta = delta_flag -> { Cbv (all_with ~head:false delta) }
| IDENT "vm_compute"; po = OPT ref_or_pattern_occ -> { CbvVm po }
| IDENT "native_compute"; po = OPT ref_or_pattern_occ -> { CbvNative po }
| IDENT "unfold"; ul = LIST1 unfold_occ SEP "," -> { Unfold ul }
| IDENT "fold"; cl = LIST1 constr -> { Fold cl }
| IDENT "pattern"; pl = LIST1 pattern_occ SEP"," -> { Pattern pl }
| s = IDENT -> { ExtraRedExpr s } ] ]
;
END
|
