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
|
(* $Id$ *)
open Pcoq
open Command
GEXTEND Gram
pattern_list:
[ [ -> ([],[])
| (id1,p) = pattern; (id2,pl) = pattern_list -> (id1@id2, p::pl) ] ]
;
lsimple_pattern:
[ [ c = simple_pattern2 -> c ] ]
;
simple_pattern:
[ [ id = ident -> ([Ast.nvar_of_ast id], id)
| "("; p = lsimple_pattern; ")" -> p ] ]
;
simple_pattern_list:
[ [ -> ([],[])
| (id1,p) = simple_pattern; (id2,pl) = simple_pattern_list ->
(id1@id2, p::pl) ] ]
;
(* The XTRA"!" means we want to override the implicit arg mecanism of bdize,
since params are not given in patterns *)
simple_pattern2:
[ [ (id1,p) = simple_pattern; (id2,lp) = pattern_list ->
(id1@id2, <:ast< (APPLIST (XTRA "!" $p) ($LIST $lp)) >>)
| (id1,p) = simple_pattern; "as"; id = ident ->
((Ast.nvar_of_ast id)::id1, <:ast< (XTRA"AS" $id $p) >>)
| (id1,c1) = simple_pattern; ","; (id2,c2) = simple_pattern ->
(id1@id2, <:ast< (APPLIST (XTRA "!" pair) $c1 $c2) >>) ] ]
;
pattern:
[ [ p = simple_pattern -> p ] ]
;
ne_pattern_list:
[ [ (id1,c1) = pattern; (id2,cl) = ne_pattern_list ->
(id1@id2, c1::cl)
| (id1,c1) = pattern -> (id1,[c1]) ] ]
;
equation:
[ [ (ids,lhs) = ne_pattern_list; "=>"; rhs = command ->
let br =
List.fold_right (fun s ast -> Coqast.Slam loc (Some s) ast)
ids
<:ast< (XTRA"EQN" $rhs ($LIST $lhs)) >> in
let lid = List.map (fun s -> Coqast.Id loc s) ids in
<:ast< (XTRA"LAMEQN"($LIST $lid) $br) >> ] ]
;
ne_eqn_list:
[ [ e = equation; "|"; leqn = ne_eqn_list -> e :: leqn
| e = equation -> [e] ] ]
;
command1:
[ [ "<"; l1 = lcommand; ">"; "Cases"; lc = ne_command_list; "of";
OPT "|"; eqs = ne_eqn_list; "end" ->
<:ast< (XTRA"MULTCASE" $l1 (XTRA"TOMATCH" ($LIST $lc))
($LIST $eqs)) >>
| "Cases"; lc = ne_command_list; "of";
OPT "|"; eqs = ne_eqn_list; "end" ->
<:ast< (XTRA"MULTCASE" (XTRA"SYNTH")
(XTRA"TOMATCH"($LIST $lc)) ($LIST $eqs)) >>
| "<"; l1 = lcommand; ">"; "Cases"; lc = ne_command_list; "of";
"end" ->
<:ast< (XTRA"MULTCASE" $l1 (XTRA"TOMATCH" ($LIST $lc))) >>
| "Cases"; lc = ne_command_list; "of"; "end" ->
<:ast< (XTRA"MULTCASE" (XTRA"SYNTH")
(XTRA"TOMATCH"($LIST $lc))) >> ] ]
;
END
|
