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
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(* $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
| 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)
| Nvar(_,id) -> VARG_IDENTIFIER id
| Node(loc,"QUALIDARG",p) -> VARG_QUALID (Astterm.interp_qualid p)
| Str(_,s) -> VARG_STRING s
| Id(_,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 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
let ist = { evc=evc; env=env; lfun=[]; lmatch=[];
goalopt=None; debug=get_debug ()} in
VARG_TACTIC_ARG (interp_tacarg ist 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")
|
