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
152
153
154
155
156
157
158
159
160
|
(* $Id$ *)
open Pp
open Util
open Names
open Term
open Proof_trees
open Tacmach
open Macros
open Coqast
open Ast
let tactic_tab =
(Hashtbl.create 17 : (string, tactic_arg list -> tactic) Hashtbl.t)
let tacinterp_add (s,f) =
try
Hashtbl.add tactic_tab s f
with Failure _ ->
errorlabstrm "tacinterp_add"
[< 'sTR"Cannot add the tactic " ; 'sTR s ; 'sTR" twice" >]
let overwriting_tacinterp_add (s,f) =
if Hashtbl.mem tactic_tab s then begin
Hashtbl.remove tactic_tab s;
warning ("Overwriting definition of tactic interpreter command "^s)
end;
Hashtbl.add tactic_tab s f
let tacinterp_init () = Hashtbl.clear tactic_tab
let tacinterp_map s = Hashtbl.find tactic_tab s
let err_msg_tactic_not_found macro_loc macro =
user_err_loc
(macro_loc,"macro_expand",
[< 'sTR"Tactic macro ";'sTR macro; 'sPC; 'sTR"not found" >])
let cvt_bind = function
| Node(_,"BINDING", [Num(_,n); Node(_,"COMMAND",[c])]) -> (NoDep n,c)
| Node(_,"BINDING", [Nvar(_,s); Node(_,"COMMAND",[c])]) ->
let id = id_of_string s in (Dep id,c)
| Node(_,"BINDING", [Node(_,"COMMAND",[c])]) -> (Com,c)
| x -> errorlabstrm "cvt_bind"
[< 'sTR "Not the expected form in binding!"; print_ast x >]
let rec cvt_intro_pattern = function
| Node(_,"IDENTIFIER", [Nvar(_,s)]) -> IdPat (id_of_string s)
| Node(_,"DISJPATTERN", l) -> DisjPat (List.map cvt_intro_pattern l)
| Node(_,"CONJPATTERN", l) -> ConjPat (List.map cvt_intro_pattern l)
| Node(_,"LISTPATTERN", l) -> ListPat (List.map cvt_intro_pattern l)
| x -> errorlabstrm "cvt_intro_pattern"
[< 'sTR "Not the expected form for an introduction pattern!";
print_ast x >]
let cvt_letpattern (o,l) = function
| Node(_,"HYPPATTERN", Nvar(_,s)::nums) ->
(o, (id_of_string s, List.map num_of_ast nums)::l)
| Node(_,"CCLPATTERN", nums) ->
if o<>None then error "\"Goal\" occurs twice"
else (Some (List.map num_of_ast nums), l)
| arg ->
invalid_arg_loc (Ast.loc arg,"cvt_hyppattern")
let cvt_letpatterns astl = List.fold_left cvt_letpattern (None,[]) astl
let cvt_arg = function
| Nvar(_,s) ->
Identifier (id_of_string s)
| Str(_,s) ->
Quoted_string s
| Num(_,n) ->
Integer n
| Node(_,"COMMAND",[c]) ->
Command c
| Node(_,"BINDINGS",astl) ->
Bindings (List.map cvt_bind astl)
| Node(_,"REDEXP",[Node(_,redname,args)]) ->
Redexp (redname,args)
| Node(_,"CLAUSE",cl) ->
Clause (List.map (compose id_of_string nvar_of_ast) cl)
| Node(_,"TACTIC",[ast]) ->
Tacexp ast
| Node(_,"FIXEXP", [Nvar(_,s); Num(_,n);Node(_,"COMMAND",[c])]) ->
Fixexp (id_of_string s,n,c)
| Node(_,"COFIXEXP", [Nvar(_,s); Node(_,"COMMAND",[c])]) ->
Cofixexp (id_of_string s,c)
| Node(_,"INTROPATTERN", [ast]) ->
Intropattern (cvt_intro_pattern ast)
| Node(_,"LETPATTERNS", astl) ->
let (o,l) = (cvt_letpatterns astl) in Letpatterns (o,l)
| x ->
anomaly_loc (Ast.loc x, "Tacinterp.cvt_bind",
[< 'sTR "Unrecognizable ast node : "; print_ast x >])
let rec interp = function
| Node(loc,opn,tl) ->
(match (opn, tl) with
| ("TACTICLIST",_) -> interp_semi_list tclIDTAC tl
| ("DO",[n;tac]) -> tclDO (num_of_ast n) (interp tac)
| ("TRY",[tac]) -> tclTRY (interp tac)
| ("INFO",[tac]) -> tclINFO (interp tac)
| ("REPEAT",[tac]) -> tclREPEAT (interp tac)
| ("ORELSE",[tac1;tac2]) -> tclORELSE (interp tac1) (interp tac2)
| ("FIRST",l) -> tclFIRST (List.map interp l)
| ("TCLSOLVE",l) -> tclSOLVE (List.map interp l)
| ("CALL",macro::args) ->
interp (macro_expand loc (nvar_of_ast macro)
(List.map cvt_arg args))
| _ -> interp_atomic loc opn (List.map cvt_arg tl))
| ast -> user_err_loc(Ast.loc ast,"Tacinterp.interp",
[< 'sTR"A non-ASTnode constructor was found" >])
and interp_atomic loc opn args =
try
tacinterp_map opn args
with Not_found ->
try
vernac_tactic(opn,args)
with e ->
Stdpp.raise_with_loc loc e
and interp_semi_list acc = function
| (Node(_,"TACLIST",seq))::l ->
interp_semi_list (tclTHENS acc (List.map interp seq)) l
| t::l -> interp_semi_list (tclTHEN acc (interp t)) l
| [] -> acc
let is_just_undef_macro ast =
match ast with
| Node(_,"TACTICLIST",[Node(loc,"CALL",macro::_)]) ->
let id = nvar_of_ast macro in
(try let _ = Macros.lookup id in None with Not_found -> Some id)
| _ -> None
let vernac_interp =
let gentac =
hide_tactic "Interpret"
(fun vargs gl -> match vargs with
| [Tacexp com] -> interp com gl
| _ -> assert false)
in
fun com -> gentac [Tacexp com]
let vernac_interp_atomic =
let gentac =
hide_tactic "InterpretAtomic"
(fun argl gl -> match argl with
| (Identifier id)::args ->
interp_atomic dummy_loc (string_of_id id) args gl
| _ -> assert false)
in
fun opn args -> gentac ((Identifier opn)::args)
let bad_tactic_args s =
anomalylabstrm s
[< 'sTR"Tactic "; 'sTR s; 'sTR" called with bad arguments" >]
|
