The interp_app function now takes a closure as an argument.

6 files changed, 25 insertions, 9 deletions

diff --git a/src/tac2core.ml b/src/tac2core.ml
index 2c9226adae..5e475e1d4a 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -103,7 +103,7 @@ let err_matchfailure bt =
 
 (** Helper functions *)
 
-let thaw bt f = Tac2interp.interp_app bt f [v_unit]
+let thaw bt f = Tac2interp.interp_app bt (Value.to_closure f) [v_unit]
 let throw bt e = Proofview.tclLIFT (Proofview.NonLogical.raise (e bt))
 
 let set_bt bt e = match e with
@@ -615,7 +615,7 @@ end
 
 (** (unit -> 'a) -> (exn -> 'a) -> 'a *)
 let () = define2 "plus" begin fun bt x k ->
-  Proofview.tclOR (thaw bt x) (fun e -> Tac2interp.interp_app bt k [Value.of_exn e])
+  Proofview.tclOR (thaw bt x) (fun e -> Tac2interp.interp_app bt (Value.to_closure k) [Value.of_exn e])
 end
 
 (** (unit -> 'a) -> 'a *)
@@ -741,6 +741,7 @@ let () = define1 "refine" begin fun bt c ->
 end
 
 let () = define2 "with_holes" begin fun bt x f ->
+  let f = Value.to_closure f in
   Proofview.tclEVARMAP >>= fun sigma0 ->
   thaw bt x >>= fun ans ->
   Proofview.tclEVARMAP >>= fun sigma ->
diff --git a/src/tac2ffi.ml b/src/tac2ffi.ml
index a0c51783ed..c3f535c1bc 100644
--- a/src/tac2ffi.ml
+++ b/src/tac2ffi.ml
@@ -122,6 +122,18 @@ let list r = {
   r_id = false;
 }
 
+let of_closure cls = ValCls cls
+
+let to_closure = function
+| ValCls cls -> cls
+| ValExt _ | ValInt _ | ValBlk _ | ValStr _ | ValOpn _ -> assert false
+
+let closure = {
+  r_of = of_closure;
+  r_to = to_closure;
+  r_id = false;
+}
+
 let of_ext tag c =
   ValExt (tag, c)
 
diff --git a/src/tac2ffi.mli b/src/tac2ffi.mli
index 2282d34b3a..fe813b0e35 100644
--- a/src/tac2ffi.mli
+++ b/src/tac2ffi.mli
@@ -60,6 +60,10 @@ val of_ident : Id.t -> valexpr
 val to_ident : valexpr -> Id.t
 val ident : Id.t repr
 
+val of_closure : closure -> valexpr
+val to_closure : valexpr -> closure
+val closure : closure repr
+
 val of_array : ('a -> valexpr) -> 'a array -> valexpr
 val to_array : (valexpr -> 'a) -> valexpr -> 'a array
 val array : 'a repr -> 'a array repr
diff --git a/src/tac2interp.ml b/src/tac2interp.ml
index e79ce87268..6bee5a0794 100644
--- a/src/tac2interp.ml
+++ b/src/tac2interp.ml
@@ -46,7 +46,7 @@ let rec interp (ist : environment) = function
 | GTacApp (f, args) ->
   interp ist f >>= fun f ->
   Proofview.Monad.List.map (fun e -> interp ist e) args >>= fun args ->
-  interp_app ist.env_bkt f args
+  interp_app ist.env_bkt (Tac2ffi.to_closure f) args
 | GTacLet (false, el, e) ->
   let fold accu (na, e) =
     interp ist e >>= fun e ->
@@ -97,18 +97,17 @@ let rec interp (ist : environment) = function
   tpe.Tac2env.ml_interp ist e
 
 and interp_app bt f args = match f with
-| ValCls { clos_env = ist; clos_var = ids; clos_exp = e; clos_ref = kn } ->
+| { clos_env = ist; clos_var = ids; clos_exp = e; clos_ref = kn } ->
   let rec push ist ids args = match ids, args with
   | [], [] -> interp ist e
-  | [], _ :: _ -> interp ist e >>= fun f -> interp_app bt f args
+  | [], _ :: _ ->
+    interp ist e >>= fun f -> interp_app bt (Tac2ffi.to_closure f) args
   | _ :: _, [] ->
     let cls = { clos_ref = kn; clos_env = ist.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 { env_ist = ist; env_bkt = FrLtac kn :: bt } 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)
diff --git a/src/tac2interp.mli b/src/tac2interp.mli
index ea7db33b60..ca263b2c4b 100644
--- a/src/tac2interp.mli
+++ b/src/tac2interp.mli
@@ -13,7 +13,7 @@ val empty_environment : environment
 
 val interp : environment -> glb_tacexpr -> valexpr Proofview.tactic
 
-val interp_app : backtrace -> valexpr -> valexpr list -> valexpr Proofview.tactic
+val interp_app : backtrace -> closure -> valexpr list -> valexpr Proofview.tactic
 
 (** {5 Cross-boundary encodings} *)
 
diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index 713a5f1b1c..79af41b7d0 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -18,7 +18,7 @@ module Value = Tac2ffi
 
 let return x = Proofview.tclUNIT x
 let v_unit = Value.of_unit ()
-let thaw bt f = Tac2interp.interp_app bt f [v_unit]
+let thaw bt f = Tac2interp.interp_app bt (Value.to_closure f) [v_unit]
 
 let to_pair f g = function
 | ValBlk (0, [| x; y |]) -> (f x, g y)