From dac0b95c77dc316a2ef65bbc3901ed7c9366e982 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 14 Sep 2017 21:36:47 +0200
Subject: Abstracting away the type of arities and ML tactics.

---
 src/tac2core.ml   | 14 ++++++--------
 src/tac2env.mli   |  4 ++--
 src/tac2ffi.ml    | 21 ++++++++++++++-------
 src/tac2ffi.mli   | 23 +++++++++++++----------
 src/tac2stdlib.ml | 18 +++++++++---------
 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
-- 
cgit v1.2.3