Explicit arity for closures.

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