Moving the Ltac2 FFI to a separate file.

7 files changed, 233 insertions, 182 deletions

diff --git a/_CoqProject b/_CoqProject
index e3ad3987bd..6c9393628d 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -13,6 +13,8 @@ src/tac2interp.ml
 src/tac2interp.mli
 src/tac2entries.ml
 src/tac2entries.mli
+src/tac2ffi.ml
+src/tac2ffi.mli
 src/tac2core.ml
 src/tac2core.mli
 src/tac2stdlib.ml
diff --git a/src/ltac2_plugin.mlpack b/src/ltac2_plugin.mlpack
index dc78207291..1d7b655dce 100644
--- a/src/ltac2_plugin.mlpack
+++ b/src/ltac2_plugin.mlpack
@@ -3,6 +3,7 @@ Tac2print
 Tac2intern
 Tac2interp
 Tac2entries
+Tac2ffi
 Tac2core
 Tac2stdlib
 G_ltac2
diff --git a/src/tac2core.ml b/src/tac2core.ml
index a3678d1ad0..6d9ede4421 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -18,30 +18,9 @@ open Proofview.Notations
 
 (** Standard values *)
 
-let coq_core n = KerName.make2 Tac2env.coq_prefix (Label.of_id (Id.of_string_soft n))
+module Value = Tac2ffi
 
-let val_tag t = match val_tag t with
-| Val.Base t -> t
-| _ -> assert false
-
-let val_constr = val_tag (topwit Stdarg.wit_constr)
-let val_ident = val_tag (topwit Stdarg.wit_ident)
-let val_pattern = Val.create "ltac2:pattern"
-let val_pp = Val.create "ltac2:pp"
-let val_sort = Val.create "ltac2:sort"
-let val_cast = Val.create "ltac2:cast"
-let val_inductive = Val.create "ltac2:inductive"
-let val_constant = Val.create "ltac2:constant"
-let val_constructor = Val.create "ltac2:constructor"
-let val_projection = Val.create "ltac2:projection"
-let val_univ = Val.create "ltac2:universe"
-let val_kont : (Exninfo.iexn -> valexpr Proofview.tactic) Val.typ =
-  Val.create "ltac2:kont"
-
-let extract_val (type a) (tag : a Val.typ) (Val.Dyn (tag', v)) : a =
-match Val.eq tag tag' with
-| None -> assert false
-| Some Refl -> v
+let coq_core n = KerName.make2 Tac2env.coq_prefix (Label.of_id (Id.of_string_soft n))
 
 module Core =
 struct
@@ -67,108 +46,19 @@ end
 open Core
 
 let v_unit = ValInt 0
-let v_nil = ValInt 0
-let v_cons v vl = ValBlk (0, [|v; vl|])
-
-module Value =
-struct
-
-let of_unit () = v_unit
-
-let to_unit = function
-| ValInt 0 -> ()
-| _ -> assert false
-
-let of_int n = ValInt n
-let to_int = function
-| ValInt n -> n
-| _ -> assert false
-
-let of_bool b = if b then ValInt 0 else ValInt 1
-
-let to_bool = function
-| ValInt 0 -> true
-| ValInt 1 -> false
-| _ -> assert false
-
-let of_char n = ValInt (Char.code n)
-let to_char = function
-| ValInt n -> Char.chr n
-| _ -> assert false
-
-let of_string s = ValStr s
-let to_string = function
-| ValStr s -> s
-| _ -> assert false
-
-let rec of_list = function
-| [] -> v_nil
-| x :: l -> v_cons x (of_list l)
-
-let rec to_list = function
-| ValInt 0 -> []
-| ValBlk (0, [|v; vl|]) -> v :: to_list vl
-| _ -> assert false
-
-let of_ext tag c =
-  ValExt (Val.Dyn (tag, c))
-
-let to_ext tag = function
-| ValExt e -> extract_val tag e
-| _ -> assert false
-
-let of_constr c = of_ext val_constr c
-let to_constr c = to_ext val_constr c
-
-let of_ident c = of_ext val_ident c
-let to_ident c = to_ext val_ident c
-
-let of_pattern c = of_ext val_pattern c
-let to_pattern c = to_ext val_pattern c
-
-(** FIXME: handle backtrace in Ltac2 exceptions *)
-let of_exn c = match fst c with
-| LtacError (kn, c) -> ValOpn (kn, c)
-| _ -> of_ext val_exn c
-
-let to_exn c = match c with
-| ValOpn (kn, c) -> (LtacError (kn, c), Exninfo.null)
-| _ -> to_ext val_exn c
-
-let of_option = function
-| None -> ValInt 0
-| Some c -> ValBlk (0, [|c|])
-
-let to_option = function
-| ValInt 0 -> None
-| ValBlk (0, [|c|]) -> Some c
-| _ -> assert false
-
-let of_pp c = of_ext val_pp c
-let to_pp c = to_ext val_pp c
-
-let of_tuple cl = ValBlk (0, cl)
-let to_tuple = function
-| ValBlk (0, cl) -> cl
-| _ -> assert false
-
-let of_array = of_tuple
-let to_array = to_tuple
 
 let of_name c = match c with
-| Anonymous -> of_option None
-| Name id -> of_option (Some (of_ident id))
+| Anonymous -> Value.of_option None
+| Name id -> Value.of_option (Some (Value.of_ident id))
 
 let of_instance sigma u =
   let u = Univ.Instance.to_array (EConstr.EInstance.kind sigma u) in
-  of_array (Array.map (fun v -> of_ext val_univ v) u)
+  Value.of_array (Array.map (fun v -> Value.of_ext Value.val_univ v) u)
 
 let of_rec_declaration (nas, ts, cs) =
-  (of_array (Array.map of_name nas),
-  of_array (Array.map of_constr ts),
-  of_array (Array.map of_constr cs))
-
-end
+  (Value.of_array (Array.map of_name nas),
+  Value.of_array (Array.map Value.of_constr ts),
+  Value.of_array (Array.map Value.of_constr cs))
 
 let val_valexpr = Val.create "ltac2:valexpr"
 
@@ -395,28 +285,28 @@ let prm_constr_kind : ml_tactic = function
       Value.of_array (Array.map Value.of_constr args)
     |])
   | Sort s ->
-    ValBlk (4, [|Value.of_ext val_sort s|])
+    ValBlk (4, [|Value.of_ext Value.val_sort s|])
   | Cast (c, k, t) ->
     ValBlk (5, [|
       Value.of_constr c;
-      Value.of_ext val_cast k;
+      Value.of_ext Value.val_cast k;
       Value.of_constr t;
     |])
   | Prod (na, t, u) ->
     ValBlk (6, [|
-      Value.of_name na;
+      of_name na;
       Value.of_constr t;
       Value.of_constr u;
     |])
   | Lambda (na, t, c) ->
     ValBlk (7, [|
-      Value.of_name na;
+      of_name na;
       Value.of_constr t;
       Value.of_constr c;
     |])
   | LetIn (na, b, t, c) ->
     ValBlk (8, [|
-      Value.of_name na;
+      of_name na;
       Value.of_constr b;
       Value.of_constr t;
       Value.of_constr c;
@@ -428,18 +318,18 @@ let prm_constr_kind : ml_tactic = function
     |])
   | Const (cst, u) ->
     ValBlk (10, [|
-      Value.of_ext val_constant cst;
-      Value.of_instance sigma u;
+      Value.of_ext Value.val_constant cst;
+      of_instance sigma u;
     |])
   | Ind (ind, u) ->
     ValBlk (11, [|
-      Value.of_ext val_inductive ind;
-      Value.of_instance sigma u;
+      Value.of_ext Value.val_inductive ind;
+      of_instance sigma u;
     |])
   | Construct (cstr, u) ->
     ValBlk (12, [|
-      Value.of_ext val_constructor cstr;
-      Value.of_instance sigma u;
+      Value.of_ext Value.val_constructor cstr;
+      of_instance sigma u;
     |])
   | Case (_, c, t, bl) ->
     ValBlk (13, [|
@@ -448,7 +338,7 @@ let prm_constr_kind : ml_tactic = function
       Value.of_array (Array.map (fun c -> Value.of_constr c) bl);
     |])
   | Fix ((recs, i), def) ->
-    let (nas, ts, cs) = Value.of_rec_declaration def in
+    let (nas, ts, cs) = of_rec_declaration def in
     ValBlk (14, [|
       Value.of_array (Array.map Value.of_int recs);
       Value.of_int i;
@@ -457,7 +347,7 @@ let prm_constr_kind : ml_tactic = function
       cs;
     |])
   | CoFix (i, def) ->
-    let (nas, ts, cs) = Value.of_rec_declaration def in
+    let (nas, ts, cs) = of_rec_declaration def in
     ValBlk (15, [|
       Value.of_int i;
       nas;
@@ -466,7 +356,7 @@ let prm_constr_kind : ml_tactic = function
     |])
   | Proj (p, c) ->
     ValBlk (16, [|
-      Value.of_ext val_projection p;
+      Value.of_ext Value.val_projection p;
       Value.of_constr c;
     |])
   end
@@ -584,7 +474,7 @@ let prm_case : ml_tactic = function
   Proofview.tclCASE (thaw f) >>= begin function
   | Proofview.Next (x, k) ->
     let k = {
-      clos_env = Id.Map.singleton k_var (Value.of_ext val_kont k);
+      clos_env = Id.Map.singleton k_var (Value.of_ext Value.val_kont k);
       clos_var = [Name e_var];
       clos_exp = GTacPrm (prm_apply_kont_h, [GTacVar k_var; GTacVar e_var]);
     } in
@@ -595,7 +485,7 @@ let prm_case : ml_tactic = function
 
 (** 'a kont -> exn -> 'a *)
 let prm_apply_kont : ml_tactic = function
-| [k; e] -> (Value.to_ext val_kont k) (Value.to_exn e)
+| [k; e] -> (Value.to_ext Value.val_kont k) (Value.to_exn e)
 | _ -> assert false
 
 (** int -> int -> (unit -> 'a) -> 'a *)
@@ -768,7 +658,7 @@ let interp_constr flags ist (c, _) =
   Proofview.V82.wrap_exceptions begin fun () ->
     let ist = to_lvar ist in
     let (sigma, c) = understand_ltac flags env sigma ist WithoutTypeConstraint c in
-    let c = Val.Dyn (val_constr, c) in
+    let c = Val.Dyn (Value.val_constr, c) in
     Proofview.Unsafe.tclEVARS sigma >>= fun () ->
     Proofview.tclUNIT c
   end
@@ -791,7 +681,7 @@ let () =
   define_ml_object Stdarg.wit_open_constr obj
 
 let () =
-  let interp _ id = return (Val.Dyn (val_ident, id)) in
+  let interp _ id = return (Val.Dyn (Value.val_ident, id)) in
   let obj = {
     ml_type = t_ident;
     ml_interp = interp;
@@ -799,7 +689,7 @@ let () =
   define_ml_object Stdarg.wit_ident obj
 
 let () =
-  let interp _ c = return (Val.Dyn (val_pattern, c)) in
+  let interp _ c = return (Val.Dyn (Value.val_pattern, c)) in
   let obj = {
     ml_type = t_pattern;
     ml_interp = interp;
diff --git a/src/tac2core.mli b/src/tac2core.mli
index 41c79b2c65..07ff6cd539 100644
--- a/src/tac2core.mli
+++ b/src/tac2core.mli
@@ -25,47 +25,3 @@ val t_string : type_constant
 val t_array : type_constant
 
 end
-
-(** {5 Ltac2 FFI} *)
-
-(** These functions allow to convert back and forth between OCaml and Ltac2
-    data representation. The [to_*] functions raise an anomaly whenever the data
-    has not expected shape. *)
-
-module Value :
-sig
-
-val of_unit : unit -> valexpr
-val to_unit : valexpr -> unit
-
-val of_int : int -> valexpr
-val to_int : valexpr -> int
-
-val of_bool : bool -> valexpr
-val to_bool : valexpr -> bool
-
-val of_char : char -> valexpr
-val to_char : valexpr -> char
-
-val of_list : valexpr list -> valexpr
-val to_list : valexpr -> valexpr list
-
-val of_constr : EConstr.t -> valexpr
-val to_constr : valexpr -> EConstr.t
-
-val of_exn : Exninfo.iexn -> valexpr
-val to_exn : valexpr -> Exninfo.iexn
-
-val of_ident : Id.t -> valexpr
-val to_ident : valexpr -> Id.t
-
-val of_array : valexpr array -> valexpr
-val to_array : valexpr -> valexpr array
-
-val of_tuple : valexpr array -> valexpr
-val to_tuple : valexpr -> valexpr array
-
-val of_option : valexpr option -> valexpr
-val to_option : valexpr -> valexpr option
-
-end
diff --git a/src/tac2ffi.ml b/src/tac2ffi.ml
new file mode 100644
index 0000000000..5f1341ea80
--- /dev/null
+++ b/src/tac2ffi.ml
@@ -0,0 +1,122 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Util
+open Genarg
+open Geninterp
+open Tac2expr
+open Tac2interp
+
+(** Dynamic tags *)
+
+let val_tag t = match val_tag t with
+| Val.Base t -> t
+| _ -> assert false
+
+let val_constr = val_tag (topwit Stdarg.wit_constr)
+let val_ident = val_tag (topwit Stdarg.wit_ident)
+let val_pattern = Val.create "ltac2:pattern"
+let val_pp = Val.create "ltac2:pp"
+let val_sort = Val.create "ltac2:sort"
+let val_cast = Val.create "ltac2:cast"
+let val_inductive = Val.create "ltac2:inductive"
+let val_constant = Val.create "ltac2:constant"
+let val_constructor = Val.create "ltac2:constructor"
+let val_projection = Val.create "ltac2:projection"
+let val_univ = Val.create "ltac2:universe"
+let val_kont : (Exninfo.iexn -> valexpr Proofview.tactic) Val.typ =
+  Val.create "ltac2:kont"
+
+let extract_val (type a) (tag : a Val.typ) (Val.Dyn (tag', v)) : a =
+match Val.eq tag tag' with
+| None -> assert false
+| Some Refl -> v
+
+(** Conversion functions *)
+
+let of_unit () = ValInt 0
+
+let to_unit = function
+| ValInt 0 -> ()
+| _ -> assert false
+
+let of_int n = ValInt n
+let to_int = function
+| ValInt n -> n
+| _ -> assert false
+
+let of_bool b = if b then ValInt 0 else ValInt 1
+
+let to_bool = function
+| ValInt 0 -> true
+| ValInt 1 -> false
+| _ -> assert false
+
+let of_char n = ValInt (Char.code n)
+let to_char = function
+| ValInt n -> Char.chr n
+| _ -> assert false
+
+let of_string s = ValStr s
+let to_string = function
+| ValStr s -> s
+| _ -> assert false
+
+let rec of_list = function
+| [] -> ValInt 0
+| x :: l -> ValBlk (0, [| x; of_list l |])
+
+let rec to_list = function
+| ValInt 0 -> []
+| ValBlk (0, [|v; vl|]) -> v :: to_list vl
+| _ -> assert false
+
+let of_ext tag c =
+  ValExt (Val.Dyn (tag, c))
+
+let to_ext tag = function
+| ValExt e -> extract_val tag e
+| _ -> assert false
+
+let of_constr c = of_ext val_constr c
+let to_constr c = to_ext val_constr c
+
+let of_ident c = of_ext val_ident c
+let to_ident c = to_ext val_ident c
+
+let of_pattern c = of_ext val_pattern c
+let to_pattern c = to_ext val_pattern c
+
+(** FIXME: handle backtrace in Ltac2 exceptions *)
+let of_exn c = match fst c with
+| LtacError (kn, c) -> ValOpn (kn, c)
+| _ -> of_ext val_exn c
+
+let to_exn c = match c with
+| ValOpn (kn, c) -> (LtacError (kn, c), Exninfo.null)
+| _ -> to_ext val_exn c
+
+let of_option = function
+| None -> ValInt 0
+| Some c -> ValBlk (0, [|c|])
+
+let to_option = function
+| ValInt 0 -> None
+| ValBlk (0, [|c|]) -> Some c
+| _ -> assert false
+
+let of_pp c = of_ext val_pp c
+let to_pp c = to_ext val_pp c
+
+let of_tuple cl = ValBlk (0, cl)
+let to_tuple = function
+| ValBlk (0, cl) -> cl
+| _ -> assert false
+
+let of_array = of_tuple
+let to_array = to_tuple
diff --git a/src/tac2ffi.mli b/src/tac2ffi.mli
new file mode 100644
index 0000000000..d72d0452a0
--- /dev/null
+++ b/src/tac2ffi.mli
@@ -0,0 +1,78 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Geninterp
+open Names
+open EConstr
+open Tac2expr
+
+(** {5 Ltac2 FFI} *)
+
+(** These functions allow to convert back and forth between OCaml and Ltac2
+    data representation. The [to_*] functions raise an anomaly whenever the data
+    has not expected shape. *)
+
+val of_unit : unit -> valexpr
+val to_unit : valexpr -> unit
+
+val of_int : int -> valexpr
+val to_int : valexpr -> int
+
+val of_bool : bool -> valexpr
+val to_bool : valexpr -> bool
+
+val of_char : char -> valexpr
+val to_char : valexpr -> char
+
+val of_string : string -> valexpr
+val to_string : valexpr -> string
+
+val of_list : valexpr list -> valexpr
+val to_list : valexpr -> valexpr list
+
+val of_constr : EConstr.t -> valexpr
+val to_constr : valexpr -> EConstr.t
+
+val of_exn : Exninfo.iexn -> valexpr
+val to_exn : valexpr -> Exninfo.iexn
+
+val of_ident : Id.t -> valexpr
+val to_ident : valexpr -> Id.t
+
+val of_array : valexpr array -> valexpr
+val to_array : valexpr -> valexpr array
+
+val of_tuple : valexpr array -> valexpr
+val to_tuple : valexpr -> valexpr array
+
+val of_option : valexpr option -> valexpr
+val to_option : valexpr -> valexpr option
+
+val of_pattern : Pattern.constr_pattern -> valexpr
+val to_pattern : valexpr -> Pattern.constr_pattern
+
+val of_pp : Pp.t -> valexpr
+val to_pp : valexpr -> Pp.t
+
+val of_ext : 'a Val.typ -> 'a -> valexpr
+val to_ext : 'a Val.typ -> valexpr -> 'a
+
+(** {5 Dynamic tags} *)
+
+val val_constr : EConstr.t Val.typ
+val val_ident : Id.t Val.typ
+val val_pattern : Pattern.constr_pattern Val.typ
+val val_pp : Pp.t Val.typ
+val val_sort : ESorts.t Val.typ
+val val_cast : Constr.cast_kind Val.typ
+val val_inductive : inductive Val.typ
+val val_constant : Constant.t Val.typ
+val val_constructor : constructor Val.typ
+val val_projection : Projection.t Val.typ
+val val_univ : Univ.universe_level Val.typ
+val val_kont : (Exninfo.iexn -> valexpr Proofview.tactic) Val.typ
diff --git a/src/tac2stdlib.ml b/src/tac2stdlib.ml
index 89a8d98693..25d83c06fb 100644
--- a/src/tac2stdlib.ml
+++ b/src/tac2stdlib.ml
@@ -12,12 +12,14 @@ open Tac2expr
 open Tac2core
 open Proofview.Notations
 
+module Value = Tac2ffi
+
 (** Standard tactics sharing their implementation with Ltac1 *)
 
 let pname s = { mltac_plugin = "ltac2"; mltac_tactic = s }
 
 let return x = Proofview.tclUNIT x
-let v_unit = Tac2core.Value.of_unit ()
+let v_unit = Value.of_unit ()
 
 let lift tac = tac <*> return v_unit