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
|
(* $Id$ *)
open Pp
open Util
open Names
open Himsg
open Proof_type
open Tacinterp
open Coqast
open Ast
exception ProtectedLoop
exception Drop
exception Quit
let disable_drop e =
if e <> Drop then e
else UserError("Vernac.disable_drop",[< 'sTR"Drop is forbidden." >])
type vernac_arg =
| VARG_VARGLIST of vernac_arg list
| VARG_STRING of string
| VARG_NUMBER of int
| VARG_NUMBERLIST of int list
| VARG_IDENTIFIER of identifier
| VARG_QUALID of Nametab.qualid
| VARG_CONSTANT of constant_path
| VCALL of string * vernac_arg list
| VARG_CONSTR of Coqast.t
| VARG_CONSTRLIST of Coqast.t list
| VARG_TACTIC of Coqast.t
| VARG_TACTIC_ARG of tactic_arg
| VARG_BINDER of identifier list * Coqast.t
| VARG_BINDERLIST of (identifier list * Coqast.t) list
| VARG_AST of Coqast.t
| VARG_ASTLIST of Coqast.t list
| VARG_UNIT
| VARG_DYN of Dyn.t
(* Table of vernac entries *)
let vernac_tab =
(Hashtbl.create 51 : (string, vernac_arg list -> unit -> unit) Hashtbl.t)
let vinterp_add s f =
try
Hashtbl.add vernac_tab s f
with Failure _ ->
errorlabstrm "vinterp_add"
[< 'sTR"Cannot add the vernac command " ; 'sTR s ; 'sTR" twice" >]
let overwriting_vinterp_add s f =
begin
try
let _ = Hashtbl.find vernac_tab s in Hashtbl.remove vernac_tab s
with Not_found -> ()
end;
Hashtbl.add vernac_tab s f
let vinterp_map s =
try
Hashtbl.find vernac_tab s
with Not_found ->
errorlabstrm "Vernac Interpreter"
[< 'sTR"Cannot find vernac command " ; 'sTR s >]
let vinterp_init () = Hashtbl.clear vernac_tab
(* Conversion Coqast.t -> vernac_arg *)
let rec cvt_varg ast =
match ast with
| Node(_,"VERNACARGLIST",l) ->
VARG_VARGLIST (List.map cvt_varg l)
| Node(_,"VERNACCALL",(Str (_,na))::l) ->
VCALL (na,List.map cvt_varg l)
| Node(_,"VERNACCALL",(Id (_,na))::l) ->
VCALL (na,List.map cvt_varg l)
| Nvar(_,s) -> VARG_IDENTIFIER (id_of_string s)
| Node(loc,"QUALIDARG",p) -> VARG_QUALID (Astterm.interp_qualid p)
| Node(loc,"QUALIDCONSTARG",p) ->
let q = Astterm.interp_qualid p in
let sp =
try Nametab.locate_constant q
with Not_found -> Nametab.error_global_not_found_loc loc q
in VARG_CONSTANT sp
| Str(_,s) -> VARG_STRING s
| Num(_,n) -> VARG_NUMBER n
| Node(_,"NONE",[]) -> VARG_UNIT
| Node(_,"CONSTR",[c]) -> VARG_CONSTR c
| Node(_,"CONSTRLIST",l) -> VARG_CONSTRLIST l
| Node(_,"TACTIC",[c]) -> VARG_TACTIC c
| Node(_,"BINDER",c::idl) ->
VARG_BINDER(List.map (compose id_of_string nvar_of_ast) idl, c)
| Node(_,"BINDERLIST",l) ->
VARG_BINDERLIST
(List.map (compose (function
| (VARG_BINDER (x_0,x_1)) -> (x_0,x_1)
| _ -> assert false) cvt_varg) l)
| Node(_,"NUMBERLIST",ln) ->
VARG_NUMBERLIST (List.map num_of_ast ln)
| Node(_,"AST",[a]) -> VARG_AST a
| Node(_,"ASTLIST",al) -> VARG_ASTLIST al
| Node(_,"TACTIC_ARG",[targ]) ->
let (evc,env)= Command.get_current_context () in
VARG_TACTIC_ARG (interp_tacarg (evc,env,[],[],None,get_debug ()) targ)
| Node(_,"VERNACDYN",[Dynamic (_,d)]) -> VARG_DYN d
| _ -> anomaly_loc (Ast.loc ast, "Vernacinterp.cvt_varg",
[< 'sTR "Unrecognizable ast node of vernac arg:";
'bRK(1,0); print_ast ast >])
(* Interpretation of a vernac command *)
let call (opn,converted_args) =
let loc = ref "Looking up command" in
try
let callback = vinterp_map opn in
loc:= "Checking arguments";
let hunk = callback converted_args in
loc:= "Executing command";
hunk()
with
| Drop -> raise Drop
| ProtectedLoop -> raise ProtectedLoop
| e ->
if !Options.debug then
mSGNL [< 'sTR"Vernac Interpreter " ; 'sTR !loc >];
raise e
let interp = function
| Node(_,opn,argl) as cmd ->
let converted_args =
try
List.map cvt_varg argl
with e ->
if !Options.debug then
mSGNL [< 'sTR"Vernac Interpreter " ; 'sTR"Converting arguments" >];
raise e
in
call (opn,converted_args)
| cmd ->
errorlabstrm "Vernac Interpreter"
[< 'sTR"Malformed vernac AST : " ; print_ast cmd >]
let bad_vernac_args s =
anomalylabstrm s
[< 'sTR"Vernac "; 'sTR s; 'sTR" called with bad arguments" >]
|
