aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/tac2core.ml33
-rw-r--r--src/tac2expr.mli6
-rw-r--r--src/tac2ffi.ml33
-rw-r--r--src/tac2ffi.mli10
-rw-r--r--src/tac2interp.ml31
-rw-r--r--src/tac2stdlib.ml67
6 files changed, 97 insertions, 83 deletions
diff --git a/src/tac2core.ml b/src/tac2core.ml
index bb6578090d..ea65066d74 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -101,7 +101,7 @@ let err_matchfailure =
(** Helper functions *)
-let thaw f = f [v_unit]
+let thaw f = Tac2ffi.apply f [v_unit]
let fatal_flag : unit Exninfo.t = Exninfo.make ()
let fatal_info = Exninfo.add Exninfo.null fatal_flag ()
@@ -150,24 +150,21 @@ let pf_apply f =
(** Primitives *)
-let define0 name f = Tac2env.define_primitive (pname name) begin fun arg -> match arg with
-| [_] -> f
-| _ -> assert false
-end
+let define_primitive name arity f =
+ Tac2env.define_primitive (pname name) (MLTactic (arity, f))
+
+let define0 name f = define_primitive name OneAty (fun _ -> f)
-let define1 name r0 f = Tac2env.define_primitive (pname name) begin fun arg -> match arg with
-| [x] -> f (r0.Value.r_to x)
-| _ -> assert false
+let define1 name r0 f = define_primitive name OneAty begin fun x ->
+ f (r0.Value.r_to x)
end
-let define2 name r0 r1 f = Tac2env.define_primitive (pname name) begin fun arg -> match arg with
-| [x; y] -> f (r0.Value.r_to x) (r1.Value.r_to y)
-| _ -> assert false
+let define2 name r0 r1 f = define_primitive name (AddAty OneAty) begin fun x y ->
+ f (r0.Value.r_to x) (r1.Value.r_to y)
end
-let define3 name r0 r1 r2 f = Tac2env.define_primitive (pname name) begin fun arg -> match arg with
-| [x; y; z] -> f (r0.Value.r_to x) (r1.Value.r_to y) (r2.Value.r_to z)
-| _ -> assert false
+let define3 name r0 r1 r2 f = define_primitive name (AddAty (AddAty OneAty)) begin fun x y z ->
+ f (r0.Value.r_to x) (r1.Value.r_to y) (r2.Value.r_to z)
end
(** Printing *)
@@ -588,7 +585,7 @@ end
(** (unit -> 'a) -> (exn -> 'a) -> 'a *)
let () = define2 "plus" closure closure begin fun x k ->
- Proofview.tclOR (thaw x) (fun e -> k [Value.of_exn e])
+ Proofview.tclOR (thaw x) (fun e -> Tac2ffi.apply k [Value.of_exn e])
end
(** (unit -> 'a) -> 'a *)
@@ -620,13 +617,13 @@ end
let () = define1 "case" closure begin fun f ->
Proofview.tclCASE (thaw f) >>= begin function
| Proofview.Next (x, k) ->
- let k = function
+ let k = Tac2ffi.abstract 1 begin function
| [e] ->
let (e, info) = Value.to_exn e in
set_bt info >>= fun info ->
k (e, info)
| _ -> assert false
- in
+ end in
return (ValBlk (0, [| Value.of_tuple [| x; Value.of_closure k |] |]))
| Proofview.Fail e -> return (ValBlk (1, [| Value.of_exn e |]))
end
@@ -705,7 +702,7 @@ let () = define2 "with_holes" closure closure begin fun x f ->
thaw x >>= fun ans ->
Proofview.tclEVARMAP >>= fun sigma ->
Proofview.Unsafe.tclEVARS sigma0 >>= fun () ->
- Tacticals.New.tclWITHHOLES false (f [ans]) sigma
+ Tacticals.New.tclWITHHOLES false (Tac2ffi.apply f [ans]) sigma
end
let () = define1 "progress" closure begin fun f ->
diff --git a/src/tac2expr.mli b/src/tac2expr.mli
index 0b9923f7b9..bbe127e94d 100644
--- a/src/tac2expr.mli
+++ b/src/tac2expr.mli
@@ -188,6 +188,10 @@ type frame =
type backtrace = frame list
+type ('a, _) arity =
+| OneAty : ('a, 'a -> 'a Proofview.tactic) arity
+| AddAty : ('a, 'b) arity -> ('a, 'a -> 'b) arity
+
type valexpr =
| ValInt of int
(** Immediate integers *)
@@ -202,7 +206,7 @@ type valexpr =
| ValExt : 'a Tac2dyn.Val.tag * 'a -> valexpr
(** Arbitrary data *)
-and ml_tactic = valexpr list -> valexpr Proofview.tactic
+and ml_tactic = MLTactic : (valexpr, 'v) arity * 'v -> ml_tactic
type environment = {
env_ist : valexpr Id.Map.t;
diff --git a/src/tac2ffi.ml b/src/tac2ffi.ml
index 16c17cce62..b4191acd60 100644
--- a/src/tac2ffi.ml
+++ b/src/tac2ffi.ml
@@ -12,6 +12,7 @@ open Globnames
open Genarg
open Tac2dyn
open Tac2expr
+open Proofview.Notations
type 'a repr = {
r_of : 'a -> valexpr;
@@ -248,3 +249,35 @@ let reference = {
r_to = to_reference;
r_id = false;
}
+
+let rec apply : type a. (valexpr, a) arity -> a -> valexpr list -> valexpr Proofview.tactic =
+ fun arity f args -> match args, arity with
+ | [], arity -> Proofview.tclUNIT (ValCls (MLTactic (arity, f)))
+ (** A few hardcoded cases for efficiency *)
+ | [a0], OneAty -> f a0
+ | [a0; a1], AddAty OneAty -> f a0 a1
+ | [a0; a1; a2], AddAty (AddAty OneAty) -> f a0 a1 a2
+ | [a0; a1; a2; a3], AddAty (AddAty (AddAty OneAty)) -> f a0 a1 a2 a3
+ (** Generic cases *)
+ | a :: args, OneAty ->
+ f a >>= fun f ->
+ let MLTactic (arity, f) = to_closure f in
+ apply arity f args
+ | a :: args, AddAty arity ->
+ apply arity (f a) args
+
+let apply (MLTactic (arity, f)) args = apply arity f args
+
+type n_closure =
+| NClosure : (valexpr, 'a) arity * (valexpr list -> 'a) -> n_closure
+
+let rec abstract n f =
+ if Int.equal n 1 then NClosure (OneAty, fun accu v -> f (List.rev (v :: accu)))
+ else
+ let NClosure (arity, fe) = abstract (n - 1) f in
+ NClosure (AddAty arity, fun accu v -> fe (v :: accu))
+
+let abstract n f =
+ let () = assert (n > 0) in
+ let NClosure (arity, f) = abstract n f in
+ MLTactic (arity, f [])
diff --git a/src/tac2ffi.mli b/src/tac2ffi.mli
index 05f4d210ab..489531671c 100644
--- a/src/tac2ffi.mli
+++ b/src/tac2ffi.mli
@@ -119,6 +119,16 @@ val val_exn : Exninfo.iexn Tac2dyn.Val.tag
(** Toplevel representation of OCaml exceptions. Invariant: no [LtacError]
should be put into a value with tag [val_exn]. *)
+(** Closures *)
+
+val apply : ml_tactic -> valexpr list -> valexpr Proofview.tactic
+(** Given a closure, apply it to some arguments. Handling of argument mismatches
+ is done automatically, i.e. in case of over or under-application. *)
+
+val abstract : int -> (valexpr list -> valexpr Proofview.tactic) -> ml_tactic
+(** Turn a fixed-arity function into a closure. The inner function is guaranteed
+ to be applied to a list whose size is the integer argument. *)
+
(** Exception *)
exception LtacError of KerName.t * valexpr array
diff --git a/src/tac2interp.ml b/src/tac2interp.ml
index 19efeb7669..815fdffe0f 100644
--- a/src/tac2interp.ml
+++ b/src/tac2interp.ml
@@ -88,7 +88,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 ->
- Tac2ffi.to_closure f args
+ Tac2ffi.apply (Tac2ffi.to_closure f) args
| GTacLet (false, el, e) ->
let fold accu (na, e) =
interp ist e >>= fun e ->
@@ -133,28 +133,23 @@ let rec interp (ist : environment) = function
return (ValOpn (kn, Array.of_list el))
| GTacPrm (ml, el) ->
Proofview.Monad.List.map (fun e -> interp ist e) el >>= fun el ->
- with_frame (FrPrim ml) (Tac2env.interp_primitive ml el)
+ with_frame (FrPrim ml) (Tac2ffi.apply (Tac2env.interp_primitive ml) el)
| GTacExt (tag, e) ->
let tpe = Tac2env.interp_ml_object tag in
with_frame (FrExtn (tag, e)) (tpe.Tac2env.ml_interp ist e)
-and interp_app f = (); fun args -> match f with
-| { clos_env = ist; clos_var = ids; clos_exp = e; clos_ref = kn } ->
- let frame = match kn with
- | None -> FrAnon e
- | Some kn -> FrLtac kn
+and interp_app f =
+ let ans = fun args ->
+ let { clos_env = ist; clos_var = ids; clos_exp = e; clos_ref = kn } = f in
+ let frame = match kn with
+ | None -> FrAnon e
+ | Some kn -> FrLtac kn
+ in
+ let ist = { env_ist = ist } in
+ let ist = List.fold_left2 push_name ist ids args in
+ with_frame frame (interp ist e)
in
- let rec push ist ids args = match ids, args with
- | [], [] -> with_frame frame (interp ist e)
- | [], _ :: _ ->
- with_frame frame (interp ist e) >>= fun f -> Tac2ffi.to_closure f args
- | _ :: _, [] ->
- let cls = { clos_ref = kn; clos_env = ist.env_ist; clos_var = ids; clos_exp = e } in
- let f = interp_app cls in
- return (ValCls f)
- | id :: ids, arg :: args -> push (push_name ist id arg) ids args
- in
- push { env_ist = ist } ids args
+ Tac2ffi.abstract (List.length f.clos_var) ans
and interp_case ist e cse0 cse1 = match e with
| ValInt n -> interp ist cse0.(n)
diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index e253cc382b..6512510f0a 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 f = Value.to_closure f [v_unit]
+let thaw f = Tac2ffi.apply (Value.to_closure f) [v_unit]
let to_pair f g = function
| ValBlk (0, [| x; y |]) -> (f x, g y)
@@ -189,46 +189,28 @@ let pname s = { mltac_plugin = "ltac2"; mltac_tactic = s }
let lift tac = tac <*> return v_unit
let define_prim0 name tac =
- let tac arg = match arg with
- | [_] -> lift tac
- | _ -> assert false
- in
- Tac2env.define_primitive (pname name) tac
+ let tac _ = lift tac in
+ Tac2env.define_primitive (pname name) (MLTactic (OneAty, tac))
let define_prim1 name tac =
- let tac arg = match arg with
- | [x] -> lift (tac x)
- | _ -> assert false
- in
- Tac2env.define_primitive (pname name) tac
+ let tac x = lift (tac x) in
+ Tac2env.define_primitive (pname name) (MLTactic (OneAty, tac))
let define_prim2 name tac =
- let tac arg = match arg with
- | [x; y] -> lift (tac x y)
- | _ -> assert false
- in
- Tac2env.define_primitive (pname name) tac
+ let tac x y = lift (tac x y) in
+ Tac2env.define_primitive (pname name) (MLTactic (AddAty OneAty, tac))
let define_prim3 name tac =
- let tac arg = match arg with
- | [x; y; z] -> lift (tac x y z)
- | _ -> assert false
- in
- Tac2env.define_primitive (pname name) tac
+ let tac x y z = lift (tac x y z) in
+ Tac2env.define_primitive (pname name) (MLTactic (AddAty (AddAty OneAty), tac))
let define_prim4 name tac =
- let tac arg = match arg with
- | [x; y; z; u] -> lift (tac x y z u)
- | _ -> assert false
- in
- Tac2env.define_primitive (pname name) tac
+ let tac x y z u = lift (tac x y z u) in
+ Tac2env.define_primitive (pname name) (MLTactic (AddAty (AddAty (AddAty OneAty)), tac))
let define_prim5 name tac =
- let tac arg = match arg with
- | [x; y; z; u; v] -> lift (tac x y z u v)
- | _ -> assert false
- in
- Tac2env.define_primitive (pname name) tac
+ let tac x y z u v = lift (tac x y z u v) in
+ Tac2env.define_primitive (pname name) (MLTactic (AddAty (AddAty (AddAty (AddAty OneAty))), tac))
(** Tactics from Tacexpr *)
@@ -401,26 +383,19 @@ end
(** Reduction functions *)
+let lift tac = tac >>= fun c -> Proofview.tclUNIT (Value.of_constr c)
+
let define_red1 name tac =
- let tac arg = match arg with
- | [x] -> tac x >>= fun c -> Proofview.tclUNIT (Value.of_constr c)
- | _ -> assert false
- in
- Tac2env.define_primitive (pname name) tac
+ let tac x = lift (tac x) in
+ Tac2env.define_primitive (pname name) (MLTactic (OneAty, tac))
let define_red2 name tac =
- let tac arg = match arg with
- | [x; y] -> tac x y >>= fun c -> Proofview.tclUNIT (Value.of_constr c)
- | _ -> assert false
- in
- Tac2env.define_primitive (pname name) tac
+ let tac x y = lift (tac x y) in
+ Tac2env.define_primitive (pname name) (MLTactic (AddAty OneAty, tac))
let define_red3 name tac =
- let tac arg = match arg with
- | [x; y; z] -> tac x y z >>= fun c -> Proofview.tclUNIT (Value.of_constr c)
- | _ -> assert false
- in
- Tac2env.define_primitive (pname name) tac
+ let tac x y z = lift (tac x y z) in
+ Tac2env.define_primitive (pname name) (MLTactic (AddAty (AddAty OneAty), tac))
let () = define_red1 "eval_red" begin fun c ->
let c = Value.to_constr c in
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 11:37:41 +0000