blob: d27929f86de0aea37921d8a6803784a8c4a8bf30 (
plain)
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
|
(*
Declare ML Module "ctast".
Declare ML Module "paths".
Declare ML Module "name_to_ast".
Declare ML Module "xlate".
Declare ML Module "vtp".
Declare ML Module "translate".
Declare ML Module "pbp".
Declare ML Module "blast".
Declare ML Module "dad".
Declare ML Module "showproof_ct".
Declare ML Module "showproof".
Declare ML Module "debug_tac".
Declare ML Module "paths".
Declare ML Module "history".
Declare ML Module "centaur".
(* Require Export Illustrations. *)
(* Require Export AddDad. *)
(*
Grammar vernac vernac : ast :=
goal_cmd [ "Goal" "Cmd" numarg($n) "with" tacarg($tac) "." ] ->
[(GOAL_CMD $n (TACTIC $tac))]
| kill_proof_after [ "Kill" "Proof" "after" numarg($n)"." ] -> [(KILL_NODE $n)]
| kill_proof_at [ "Kill" "Proof" "at" numarg($n)"." ] -> [(KILL_NODE $n)]
| kill_sub_proof [ "Kill" "SubProof" numarg($n) "." ] -> [(KILL_SUB_PROOF $n)]
| print_past_goal [ "Print" "Past" "Goal" numarg($n) "." ] ->
[(PRINT_GOAL_AT $n) ]
| check_in_goal [ "CHECK_IN_GOAL" numarg($n) constrarg($c) "." ] ->
[(CHECK_IN_GOAL "CHECK" $n $c)]
| eval_in_goal [ "EVAL_IN_GOAL" numarg($n) constrarg($c) "." ] ->
[(CHECK_IN_GOAL "EVAL" $n $c)]
| compute_in_goal [ "COMPUTE_IN_GOAL" numarg($n) constrarg($c) "." ] ->
[(CHECK_IN_GOAL "COMPUTE" $n $c)]
| centaur_reset [ "Centaur" "Reset" identarg($id) "." ] -> [(Centaur_Reset $id)]
(*| show_dad_rules [ "Show" "Dad" "Rules" "." ] -> [(Show_dad_rules)]*)
| start_pcoq [ "Start" "Pcoq" "Mode" "." ] -> [ (START_PCOQ) ]
| start_pcoq [ "Start" "Pcoq" "Debug" "Mode" "." ] -> [ (START_PCOQ_DEBUG) ].
Grammar vernac ne_id_list : ast list :=
id_one [ identarg($id)] -> [$id]
| id_more [identarg($id) ne_id_list($others)] -> [$id ($LIST $others)].
Grammar tactic ne_num_list : ast list :=
ne_last [ numarg($n) ] -> [ $n ]
| ne_num_ste [ numarg($n) ne_num_list($ns) ] -> [ $n ($LIST $ns)].
Grammar tactic two_numarg_list : ast list :=
two_single_and_ne [ numarg($n) "to" ne_num_list($ns)] ->
[$n (TACTIC (to)) ($LIST $ns)]
| two_rec [ numarg($n) two_numarg_list($ns)] -> [ $n ($LIST $ns)].
Grammar tactic simple_tactic : ast :=
pbp0 [ "Pbp" ] -> [(PcoqPbp)]
| pbp1 [ "Pbp" ne_num_list($ns) ] ->
[ (PcoqPbp ($LIST $ns)) ]
| pbp2 [ "Pbp" identarg($id) ] -> [ (PcoqPbp $id) ]
| pbp3 [ "Pbp" identarg($id) ne_num_list($ns)] ->
[ (PcoqPbp $id ($LIST $ns)) ]
| blast1 [ "Blast" ne_num_list($ns) ] ->
[ (PcoqBlast ($LIST $ns)) ]
| dad00 [ "Dad" "to" ] -> [(Dad (TACTIC (to)))]
| dad01 [ "Dad" "to" ne_num_list($ns) ] ->
[(Dad (TACTIC (to)) ($LIST $ns))]
| dadnn [ "Dad" two_numarg_list($ns) ] -> [ (Dad ($LIST $ns)) ]
| debug_tac [ "DebugTac" tactic($tac) ] ->
[(CtDebugTac (TACTIC $tac))]
| on_then_empty [ "OnThen" tactic($tac1) tactic($tac2) ] ->
[(OnThen (TACTIC $tac1) (TACTIC $tac2))]
| on_then_ne [ "OnThen" tactic($tac1) tactic($tac2) ne_num_list($l) ] ->
[(OnThen (TACTIC $tac1) (TACTIC $tac2) ($LIST $l))]
| debug_tac2 [ "DebugTac2" tactic($tac) ] ->
[(CtDebugTac2 (TACTIC $tac))].
(* Maybe we should have syntactic rules to make sur that syntax errors are
displayed with a readable syntax. It is not sure, since the error reporting
procedure changed from V6.1 and does not reprint the command anymore. *)
Grammar vernac vernac : ast :=
text_proof_flag_on [ "Text" "Mode" "fr" "." ] ->
[(TEXT_MODE (AST "fr"))]
| text_proof_flag_on [ "Text" "Mode" "en" "." ] ->
[(TEXT_MODE (AST "en"))]
| text_proof_flag_on [ "Text" "Mode" "Off" "." ] ->
[(TEXT_MODE (AST "off"))].
*)
*)
|
