diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/tac2core.ml | 5 | ||||
| -rw-r--r-- | src/tac2ffi.ml | 12 | ||||
| -rw-r--r-- | src/tac2ffi.mli | 4 | ||||
| -rw-r--r-- | src/tac2interp.ml | 9 | ||||
| -rw-r--r-- | src/tac2interp.mli | 2 | ||||
| -rw-r--r-- | src/tac2stdlib.ml | 2 |
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) |