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
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Util
open Pp
open CErrors
open Genarg
open Names
open Proofview.Notations
open Tac2expr
exception LtacError of KerName.t * valexpr array
let () = register_handler begin function
| LtacError (kn, _) ->
let c = Tac2print.pr_constructor kn in
hov 0 (str "Uncaught Ltac2 exception:" ++ spc () ++ hov 0 c)
| _ -> raise Unhandled
end
let val_exn = Geninterp.Val.create "ltac2:exn"
type environment = valexpr Id.Map.t
let empty_environment = Id.Map.empty
let push_name ist id v = match id with
| Anonymous -> ist
| Name id -> Id.Map.add id v ist
let get_var ist id =
try Id.Map.find id ist with Not_found ->
anomaly (str "Unbound variable " ++ Id.print id)
let get_ref ist kn =
try pi2 (Tac2env.interp_global kn) with Not_found ->
anomaly (str "Unbound reference" ++ KerName.print kn)
let return = Proofview.tclUNIT
let rec interp ist = function
| GTacAtm (AtmInt n) -> return (ValInt n)
| GTacAtm (AtmStr s) -> return (ValStr (Bytes.of_string s))
| GTacVar id -> return (get_var ist id)
| GTacRef qid -> return (get_ref ist qid)
| GTacFun (ids, e) ->
let cls = { clos_env = ist; clos_var = ids; clos_exp = e } in
return (ValCls cls)
| GTacApp (f, args) ->
interp ist f >>= fun f ->
Proofview.Monad.List.map (fun e -> interp ist e) args >>= fun args ->
interp_app f args
| GTacLet (false, el, e) ->
let fold accu (na, e) =
interp ist e >>= fun e ->
return (push_name accu na e)
in
Proofview.Monad.List.fold_left fold ist el >>= fun ist ->
interp ist e
| GTacLet (true, el, e) ->
let map (na, e) = match e with
| GTacFun (ids, e) ->
let cls = { clos_env = ist; clos_var = ids; clos_exp = e } in
na, cls
| _ -> anomaly (str "Ill-formed recursive function")
in
let fixs = List.map map el in
let fold accu (na, cls) = match na with
| Anonymous -> accu
| Name id -> Id.Map.add id (ValCls cls) accu
in
let ist = List.fold_left fold ist fixs in
(** Hack to make a cycle imperatively in the environment *)
let iter (_, e) = e.clos_env <- ist in
let () = List.iter iter fixs in
interp ist e
| GTacArr el ->
Proofview.Monad.List.map (fun e -> interp ist e) el >>= fun el ->
return (ValBlk (0, Array.of_list el))
| GTacCst (_, n, []) -> return (ValInt n)
| GTacCst (_, n, el) ->
Proofview.Monad.List.map (fun e -> interp ist e) el >>= fun el ->
return (ValBlk (n, Array.of_list el))
| GTacCse (e, _, cse0, cse1) ->
interp ist e >>= fun e -> interp_case ist e cse0 cse1
| GTacWth { opn_match = e; opn_branch = cse; opn_default = def } ->
interp ist e >>= fun e -> interp_with ist e cse def
| GTacPrj (_, e, p) ->
interp ist e >>= fun e -> interp_proj ist e p
| GTacSet (_, e, p, r) ->
interp ist e >>= fun e ->
interp ist r >>= fun r ->
interp_set ist e p r
| GTacOpn (kn, el) ->
Proofview.Monad.List.map (fun e -> interp ist e) el >>= fun el ->
return (ValOpn (kn, Array.of_list el))
| GTacPrm (ml, el) ->
Proofview.Monad.List.map (fun e -> interp ist e) el >>= fun el ->
Tac2env.interp_primitive ml el
| GTacExt e ->
let GenArg (Glbwit tag, e) = e in
let tpe = Tac2env.interp_ml_object tag in
tpe.Tac2env.ml_interp ist e
and interp_app f args = match f with
| ValCls { clos_env = ist; clos_var = ids; clos_exp = e } ->
let rec push ist ids args = match ids, args with
| [], [] -> interp ist e
| [], _ :: _ -> interp ist e >>= fun f -> interp_app f args
| _ :: _, [] ->
let cls = { clos_env = ist; clos_var = ids; clos_exp = e } in
return (ValCls cls)
| id :: ids, arg :: args -> push (push_name ist id arg) ids args
in
push ist ids args
| ValExt _ | ValInt _ | ValBlk _ | ValStr _ | ValOpn _ ->
anomaly (str "Unexpected value shape")
and interp_case ist e cse0 cse1 = match e with
| ValInt n -> interp ist cse0.(n)
| ValBlk (n, args) ->
let (ids, e) = cse1.(n) in
let ist = CArray.fold_left2 push_name ist ids args in
interp ist e
| ValExt _ | ValStr _ | ValCls _ | ValOpn _ ->
anomaly (str "Unexpected value shape")
and interp_with ist e cse def = match e with
| ValOpn (kn, args) ->
let br = try Some (KNmap.find kn cse) with Not_found -> None in
begin match br with
| None ->
let (self, def) = def in
let ist = push_name ist self e in
interp ist def
| Some (self, ids, p) ->
let ist = push_name ist self e in
let ist = CArray.fold_left2 push_name ist ids args in
interp ist p
end
| ValInt _ | ValBlk _ | ValExt _ | ValStr _ | ValCls _ ->
anomaly (str "Unexpected value shape")
and interp_proj ist e p = match e with
| ValBlk (_, args) ->
return args.(p)
| ValInt _ | ValExt _ | ValStr _ | ValCls _ | ValOpn _ ->
anomaly (str "Unexpected value shape")
and interp_set ist e p r = match e with
| ValBlk (_, args) ->
let () = args.(p) <- r in
return (ValInt 0)
| ValInt _ | ValExt _ | ValStr _ | ValCls _ | ValOpn _ ->
anomaly (str "Unexpected value shape")
|
