1 files changed, 122 insertions, 0 deletions
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