aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/tac2core.ml14
-rw-r--r--src/tac2env.mli4
-rw-r--r--src/tac2ffi.ml21
-rw-r--r--src/tac2ffi.mli23
-rw-r--r--src/tac2stdlib.ml18
5 files changed, 44 insertions, 36 deletions
diff --git a/src/tac2core.ml b/src/tac2core.ml
index ea65066d74..9e65111c0d 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -151,19 +151,19 @@ let pf_apply f =
(** Primitives *)
let define_primitive name arity f =
- Tac2env.define_primitive (pname name) (MLTactic (arity, f))
+ Tac2env.define_primitive (pname name) (mk_closure arity f)
-let define0 name f = define_primitive name OneAty (fun _ -> f)
+let define0 name f = define_primitive name arity_one (fun _ -> f)
-let define1 name r0 f = define_primitive name OneAty begin fun x ->
+let define1 name r0 f = define_primitive name arity_one begin fun x ->
f (r0.Value.r_to x)
end
-let define2 name r0 r1 f = define_primitive name (AddAty OneAty) begin fun x y ->
+let define2 name r0 r1 f = define_primitive name (arity_suc arity_one) begin fun x y ->
f (r0.Value.r_to x) (r1.Value.r_to y)
end
-let define3 name r0 r1 r2 f = define_primitive name (AddAty (AddAty OneAty)) begin fun x y z ->
+let define3 name r0 r1 r2 f = define_primitive name (arity_suc (arity_suc arity_one)) begin fun x y z ->
f (r0.Value.r_to x) (r1.Value.r_to y) (r2.Value.r_to z)
end
@@ -617,12 +617,10 @@ end
let () = define1 "case" closure begin fun f ->
Proofview.tclCASE (thaw f) >>= begin function
| Proofview.Next (x, k) ->
- let k = Tac2ffi.abstract 1 begin function
- | [e] ->
+ let k = Tac2ffi.mk_closure arity_one begin fun e ->
let (e, info) = Value.to_exn e in
set_bt info >>= fun info ->
k (e, info)
- | _ -> assert false
end in
return (ValBlk (0, [| Value.of_tuple [| x; Value.of_closure k |] |]))
| Proofview.Fail e -> return (ValBlk (1, [| Value.of_exn e |]))
diff --git a/src/tac2env.mli b/src/tac2env.mli
index 85dba90262..b82923765d 100644
--- a/src/tac2env.mli
+++ b/src/tac2env.mli
@@ -101,8 +101,8 @@ val shortest_qualid_of_projection : ltac_projection -> qualid
(** This state is not part of the summary, contrarily to the ones above. It is
intended to be used from ML plugins to register ML-side functions. *)
-val define_primitive : ml_tactic_name -> ml_tactic -> unit
-val interp_primitive : ml_tactic_name -> ml_tactic
+val define_primitive : ml_tactic_name -> closure -> unit
+val interp_primitive : ml_tactic_name -> closure
(** {5 ML primitive types} *)
diff --git a/src/tac2ffi.ml b/src/tac2ffi.ml
index 3e9842b926..ede4836750 100644
--- a/src/tac2ffi.ml
+++ b/src/tac2ffi.ml
@@ -14,9 +14,9 @@ open Tac2dyn
open Tac2expr
open Proofview.Notations
-type ('a, _) arity =
-| OneAty : ('a, 'a -> 'a Proofview.tactic) arity
-| AddAty : ('a, 'b) arity -> ('a, 'a -> 'b) arity
+type ('a, _) arity0 =
+| OneAty : ('a, 'a -> 'a Proofview.tactic) arity0
+| AddAty : ('a, 'b) arity0 -> ('a, 'a -> 'b) arity0
type valexpr =
| ValInt of int
@@ -25,14 +25,21 @@ type valexpr =
(** Structured blocks *)
| ValStr of Bytes.t
(** Strings *)
-| ValCls of ml_tactic
+| ValCls of closure
(** Closures *)
| ValOpn of KerName.t * valexpr array
(** Open constructors *)
| ValExt : 'a Tac2dyn.Val.tag * 'a -> valexpr
(** Arbitrary data *)
-and ml_tactic = MLTactic : (valexpr, 'v) arity * 'v -> ml_tactic
+and closure = MLTactic : (valexpr, 'v) arity0 * 'v -> closure
+
+let arity_one = OneAty
+let arity_suc a = AddAty a
+
+type 'a arity = (valexpr, 'a) arity0
+
+let mk_closure arity f = MLTactic (arity, f)
type 'a repr = {
r_of : 'a -> valexpr;
@@ -273,7 +280,7 @@ let reference = {
r_id = false;
}
-let rec apply : type a. (valexpr, a) arity -> a -> valexpr list -> valexpr Proofview.tactic =
+let rec apply : type a. 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 *)
@@ -292,7 +299,7 @@ let rec apply : type a. (valexpr, a) arity -> a -> valexpr list -> valexpr Proof
let apply (MLTactic (arity, f)) args = apply arity f args
type n_closure =
-| NClosure : (valexpr, 'a) arity * (valexpr list -> 'a) -> n_closure
+| NClosure : '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)))
diff --git a/src/tac2ffi.mli b/src/tac2ffi.mli
index 26e309e5fd..ed63f2d4a6 100644
--- a/src/tac2ffi.mli
+++ b/src/tac2ffi.mli
@@ -13,9 +13,7 @@ open Tac2expr
(** {5 Toplevel values} *)
-type ('a, _) arity =
-| OneAty : ('a, 'a -> 'a Proofview.tactic) arity
-| AddAty : ('a, 'b) arity -> ('a, 'a -> 'b) arity
+type closure
type valexpr =
| ValInt of int
@@ -24,14 +22,19 @@ type valexpr =
(** Structured blocks *)
| ValStr of Bytes.t
(** Strings *)
-| ValCls of ml_tactic
+| ValCls of closure
(** Closures *)
| ValOpn of KerName.t * valexpr array
(** Open constructors *)
| ValExt : 'a Tac2dyn.Val.tag * 'a -> valexpr
(** Arbitrary data *)
-and ml_tactic = MLTactic : (valexpr, 'v) arity * 'v -> ml_tactic
+type 'a arity
+
+val arity_one : (valexpr -> valexpr Proofview.tactic) arity
+val arity_suc : 'a arity -> (valexpr -> 'a) arity
+
+val mk_closure : 'v arity -> 'v -> closure
(** {5 Ltac2 FFI} *)
@@ -82,9 +85,9 @@ val of_ident : Id.t -> valexpr
val to_ident : valexpr -> Id.t
val ident : Id.t repr
-val of_closure : ml_tactic -> valexpr
-val to_closure : valexpr -> ml_tactic
-val closure : ml_tactic repr
+val of_closure : closure -> valexpr
+val to_closure : valexpr -> closure
+val closure : closure repr
val block : valexpr array repr
@@ -143,11 +146,11 @@ val val_exn : Exninfo.iexn Tac2dyn.Val.tag
(** Closures *)
-val apply : ml_tactic -> valexpr list -> valexpr Proofview.tactic
+val apply : closure -> 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
+val abstract : int -> (valexpr list -> valexpr Proofview.tactic) -> closure
(** 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. *)
diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index 6b3b997232..e94027c899 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -191,27 +191,27 @@ let lift tac = tac <*> return v_unit
let define_prim0 name tac =
let tac _ = lift tac in
- Tac2env.define_primitive (pname name) (MLTactic (OneAty, tac))
+ Tac2env.define_primitive (pname name) (mk_closure arity_one tac)
let define_prim1 name tac =
let tac x = lift (tac x) in
- Tac2env.define_primitive (pname name) (MLTactic (OneAty, tac))
+ Tac2env.define_primitive (pname name) (mk_closure arity_one tac)
let define_prim2 name tac =
let tac x y = lift (tac x y) in
- Tac2env.define_primitive (pname name) (MLTactic (AddAty OneAty, tac))
+ Tac2env.define_primitive (pname name) (mk_closure (arity_suc arity_one) tac)
let define_prim3 name tac =
let tac x y z = lift (tac x y z) in
- Tac2env.define_primitive (pname name) (MLTactic (AddAty (AddAty OneAty), tac))
+ Tac2env.define_primitive (pname name) (mk_closure (arity_suc (arity_suc arity_one)) tac)
let define_prim4 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))
+ Tac2env.define_primitive (pname name) (mk_closure (arity_suc (arity_suc (arity_suc arity_one))) tac)
let define_prim5 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))
+ Tac2env.define_primitive (pname name) (mk_closure (arity_suc (arity_suc (arity_suc (arity_suc arity_one)))) tac)
(** Tactics from Tacexpr *)
@@ -388,15 +388,15 @@ let lift tac = tac >>= fun c -> Proofview.tclUNIT (Value.of_constr c)
let define_red1 name tac =
let tac x = lift (tac x) in
- Tac2env.define_primitive (pname name) (MLTactic (OneAty, tac))
+ Tac2env.define_primitive (pname name) (mk_closure arity_one tac)
let define_red2 name tac =
let tac x y = lift (tac x y) in
- Tac2env.define_primitive (pname name) (MLTactic (AddAty OneAty, tac))
+ Tac2env.define_primitive (pname name) (mk_closure (arity_suc arity_one) tac)
let define_red3 name tac =
let tac x y z = lift (tac x y z) in
- Tac2env.define_primitive (pname name) (MLTactic (AddAty (AddAty OneAty), tac))
+ Tac2env.define_primitive (pname name) (mk_closure (arity_suc (arity_suc arity_one)) 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-08 23:16:33 +0000