Adding a module to manipulate Ltac1 values.

12 files changed, 171 insertions, 2 deletions

diff --git a/_CoqProject b/_CoqProject
index e2ef5cebe1..dda5a8001a 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -47,4 +47,5 @@ theories/Fresh.v
 theories/Std.v
 theories/Env.v
 theories/Notations.v
+theories/Ltac1.v
 theories/Ltac2.v
diff --git a/doc/ltac2.md b/doc/ltac2.md
index 3cee0ac494..b217cb08e6 100644
--- a/doc/ltac2.md
+++ b/doc/ltac2.md
@@ -880,6 +880,8 @@ a backtrace.
 
 ## Ltac1 from Ltac2
 
+### Simple API
+
 One can call Ltac1 code from Ltac2 by using the `ltac1` quotation. It parses
 a Ltac1 expression, and semantics of this quotation is the evaluation of the
 corresponding code for its side effects. In particular, in cannot return values,
@@ -888,6 +890,21 @@ and the quotation has type `unit`.
 Beware, Ltac1 **cannot** access variables from the Ltac2 scope. One is limited
 to the use of standalone function calls.
 
+### Low-level API
+
+There exists a lower-level FFI into Ltac1 that is not recommended for daily use,
+which is available in the `Ltac2.Ltac1` module. This API allows to directly
+manipulate dynamically-typed Ltac1 values, either through the function calls,
+or using the `ltac1val` quotation. The latter parses the same as `ltac1`, but
+has type `Ltac2.Ltac1.t` instead of `unit`, and dynamically behaves as an Ltac1
+thunk, i.e. `ltac1val:(foo)` corresponds to the tactic closure that Ltac1
+would generate from `idtac; foo`.
+
+Due to intricate dynamic semantics, understanding when Ltac1 value quotations
+focus is very hard. This is why some functions return a continuation-passing
+style value, as it can dispatch dynamically between focused and unfocused
+behaviour.
+
 ## Ltac2 from Ltac1
 
 Same as above by switching Ltac1 by Ltac2 and using the `ltac2` quotation
diff --git a/src/g_ltac2.mlg b/src/g_ltac2.mlg
index 5aad77596d..0494227f1e 100644
--- a/src/g_ltac2.mlg
+++ b/src/g_ltac2.mlg
@@ -100,6 +100,7 @@ let inj_open_constr loc c = inj_wit Tac2quote.wit_open_constr loc c
 let inj_pattern loc c = inj_wit Tac2quote.wit_pattern loc c
 let inj_reference loc c = inj_wit Tac2quote.wit_reference loc c
 let inj_ltac1 loc e = inj_wit Tac2quote.wit_ltac1 loc e
+let inj_ltac1val loc e = inj_wit Tac2quote.wit_ltac1val loc e
 
 let pattern_of_qualid qid =
   if Tac2env.is_constructor qid then CAst.make ?loc:qid.CAst.loc @@ CPatRef (RelId qid, [])
@@ -224,6 +225,7 @@ GRAMMAR EXTEND Gram
       | IDENT "pattern"; ":"; "("; c = Constr.lconstr_pattern; ")" -> { inj_pattern loc c }
       | IDENT "reference"; ":"; "("; c = globref; ")" -> { inj_reference loc c }
       | IDENT "ltac1"; ":"; "("; qid = ltac1_expr; ")" -> { inj_ltac1 loc qid }
+      | IDENT "ltac1val"; ":"; "("; qid = ltac1_expr; ")" -> { inj_ltac1val loc qid }
     ] ]
   ;
   let_clause:
diff --git a/src/tac2core.ml b/src/tac2core.ml
index 890062a6d1..aad4814744 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -20,8 +20,11 @@ open Proofview.Notations
 module Value = Tac2ffi
 open Value
 
-let std_core n = KerName.make Tac2env.std_prefix (Label.of_id (Id.of_string_soft n))
-let coq_core n = KerName.make Tac2env.coq_prefix (Label.of_id (Id.of_string_soft n))
+let core_prefix path n = KerName.make path (Label.of_id (Id.of_string_soft n))
+
+let std_core n = core_prefix Tac2env.std_prefix n
+let coq_core n = core_prefix Tac2env.coq_prefix n
+let ltac1_core n = core_prefix Tac2env.ltac1_prefix n
 
 module Core =
 struct
@@ -37,6 +40,7 @@ let t_ident = coq_core "ident"
 let t_option = coq_core "option"
 let t_exn = coq_core "exn"
 let t_reference = std_core "reference"
+let t_ltac1 = ltac1_core "t"
 
 let c_nil = coq_core "[]"
 let c_cons = coq_core "::"
@@ -875,6 +879,73 @@ let () = define1 "env_instantiate" reference begin fun r ->
   return (Value.of_constr c)
 end
 
+(** Ltac1 in Ltac2 *)
+
+let ltac1 = Tac2ffi.repr_ext Value.val_ltac1
+let of_ltac1 v = Value.of_ext Value.val_ltac1 v
+
+let () = define1 "ltac1_ref" (list ident) begin fun ids ->
+  let open Ltac_plugin in
+  let r = match ids with
+  | [] -> raise Not_found
+  | _ :: _ as ids ->
+    let (id, path) = List.sep_last ids in
+    let path = DirPath.make (List.rev path) in
+    let fp = Libnames.make_path path id in
+    if Tacenv.exists_tactic fp then
+      List.hd (Tacenv.locate_extended_all_tactic (Libnames.qualid_of_path fp))
+    else raise Not_found
+  in
+  let tac = Tacinterp.Value.of_closure (Tacinterp.default_ist ()) (Tacenv.interp_ltac r) in
+  return (Value.of_ext val_ltac1 tac)
+end
+
+let () = define1 "ltac1_run" ltac1 begin fun v ->
+  let open Ltac_plugin in
+  Tacinterp.tactic_of_value (Tacinterp.default_ist ()) v >>= fun () ->
+  return v_unit
+end
+
+let () = define3 "ltac1_apply" ltac1 (list ltac1) closure begin fun f args k ->
+  let open Ltac_plugin in
+  let open Tacexpr in
+  let open Locus in
+  let k ret =
+    Proofview.tclIGNORE (Tac2ffi.apply k [Value.of_ext val_ltac1 ret])
+  in
+  let fold arg (i, vars, lfun) =
+    let id = Id.of_string ("x" ^ string_of_int i) in
+    let x = Reference (ArgVar CAst.(make id)) in
+    (succ i, x :: vars, Id.Map.add id arg lfun)
+  in
+  let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in
+  let lfun = Id.Map.add (Id.of_string "F") f lfun in
+  let ist = { (Tacinterp.default_ist ()) with Tacinterp.lfun = lfun; } in
+  let tac = TacArg(CAst.make @@ TacCall (CAst.make (ArgVar CAst.(make @@ Id.of_string "F"),args))) in
+  Tacinterp.val_interp ist tac k >>= fun () ->
+  return v_unit
+end
+
+let () = define1 "ltac1_of_constr" constr begin fun c ->
+  let open Ltac_plugin in
+  return (Value.of_ext val_ltac1 (Tacinterp.Value.of_constr c))
+end
+
+let () = define1 "ltac1_to_constr" ltac1 begin fun v ->
+  let open Ltac_plugin in
+  return (Value.of_option Value.of_constr (Tacinterp.Value.to_constr v))
+end
+
+let () = define1 "ltac1_of_list" (list ltac1) begin fun l ->
+  let open Geninterp.Val in
+  return (Value.of_ext val_ltac1 (inject (Base typ_list) l))
+end
+
+let () = define1 "ltac1_to_list" ltac1 begin fun v ->
+  let open Ltac_plugin in
+  return (Value.of_option (Value.of_list of_ltac1) (Tacinterp.Value.to_list v))
+end
+
 (** ML types *)
 
 let constr_flags () =
@@ -1037,6 +1108,34 @@ let () =
   } in
   define_ml_object Tac2quote.wit_ltac1 obj
 
+let () =
+  let open Ltac_plugin in
+  let intern self ist tac =
+    (** Prevent inner calls to Ltac2 values *)
+    let extra = Tac2intern.drop_ltac2_env ist.Genintern.extra in
+    let ist = { ist with Genintern.extra } in
+    let _, tac = Genintern.intern Ltac_plugin.Tacarg.wit_tactic ist tac in
+    GlbVal tac, gtypref t_ltac1
+  in
+  let interp ist tac =
+    let ist = { env_ist = Id.Map.empty } in
+    let lfun = Tac2interp.set_env ist Id.Map.empty in
+    let ist = Ltac_plugin.Tacinterp.default_ist () in
+    let ist = { ist with Geninterp.lfun = lfun } in
+    return (Value.of_ext val_ltac1 (Tacinterp.Value.of_closure ist tac))
+  in
+  let subst s tac = Genintern.substitute Tacarg.wit_tactic s tac in
+  let print env tac =
+    str "ltac1val:(" ++ Ltac_plugin.Pptactic.pr_glob_tactic env tac ++ str ")"
+  in
+  let obj = {
+    ml_intern = intern;
+    ml_subst = subst;
+    ml_interp = interp;
+    ml_print = print;
+  } in
+  define_ml_object Tac2quote.wit_ltac1val obj
+
 (** Ltac2 in terms *)
 
 let () =
diff --git a/src/tac2env.ml b/src/tac2env.ml
index dcf7440498..8198f92ff8 100644
--- a/src/tac2env.ml
+++ b/src/tac2env.ml
@@ -276,6 +276,9 @@ let coq_prefix =
 let std_prefix =
   MPfile (DirPath.make (List.map Id.of_string ["Std"; "Ltac2"]))
 
+let ltac1_prefix =
+  MPfile (DirPath.make (List.map Id.of_string ["Ltac1"; "Ltac2"]))
+
 (** Generic arguments *)
 
 let wit_ltac2 = Genarg.make0 "ltac2:value"
diff --git a/src/tac2env.mli b/src/tac2env.mli
index 7616579d63..c7e87c5432 100644
--- a/src/tac2env.mli
+++ b/src/tac2env.mli
@@ -133,6 +133,9 @@ val coq_prefix : ModPath.t
 val std_prefix : ModPath.t
 (** Path where Ltac-specific datatypes are defined in Ltac2 plugin. *)
 
+val ltac1_prefix : ModPath.t
+(** Path where the Ltac1 legacy FFI is defined. *)
+
 (** {5 Generic arguments} *)
 
 val wit_ltac2 : (raw_tacexpr, glb_tacexpr, Util.Empty.t) genarg_type
diff --git a/src/tac2ffi.ml b/src/tac2ffi.ml
index df1857c3e7..c271967bd6 100644
--- a/src/tac2ffi.ml
+++ b/src/tac2ffi.ml
@@ -96,6 +96,7 @@ let val_projection = Val.create "projection"
 let val_case = Val.create "case"
 let val_univ = Val.create "universe"
 let val_free : Names.Id.Set.t Val.tag = Val.create "free"
+let val_ltac1 : Geninterp.Val.t Val.tag = Val.create "ltac1"
 
 let extract_val (type a) (type b) (tag : a Val.tag) (tag' : b Val.tag) (v : b) : a =
 match Val.eq tag tag' with
diff --git a/src/tac2ffi.mli b/src/tac2ffi.mli
index d801c4f605..bfc93d99e6 100644
--- a/src/tac2ffi.mli
+++ b/src/tac2ffi.mli
@@ -167,6 +167,7 @@ val val_projection : Projection.t Val.tag
 val val_case : Constr.case_info Val.tag
 val val_univ : Univ.Level.t Val.tag
 val val_free : Id.Set.t Val.tag
+val val_ltac1 : Geninterp.Val.t Val.tag
 
 val val_exn : Exninfo.iexn Tac2dyn.Val.tag
 (** Toplevel representation of OCaml exceptions. Invariant: no [LtacError]
diff --git a/src/tac2quote.ml b/src/tac2quote.ml
index 3bddfe7594..5a26e7465c 100644
--- a/src/tac2quote.ml
+++ b/src/tac2quote.ml
@@ -22,6 +22,7 @@ let wit_ident = Arg.create "ident"
 let wit_constr = Arg.create "constr"
 let wit_open_constr = Arg.create "open_constr"
 let wit_ltac1 = Arg.create "ltac1"
+let wit_ltac1val = Arg.create "ltac1val"
 
 (** Syntactic quoting of expressions. *)
 
diff --git a/src/tac2quote.mli b/src/tac2quote.mli
index 09aa92f9ee..1b03dad8ec 100644
--- a/src/tac2quote.mli
+++ b/src/tac2quote.mli
@@ -96,3 +96,7 @@ val wit_constr : (Constrexpr.constr_expr, Glob_term.glob_constr) Arg.tag
 val wit_open_constr : (Constrexpr.constr_expr, Glob_term.glob_constr) Arg.tag
 
 val wit_ltac1 : (Ltac_plugin.Tacexpr.raw_tactic_expr, Ltac_plugin.Tacexpr.glob_tactic_expr) Arg.tag
+(** Ltac1 AST quotation, seen as a 'tactic'. Its type is unit in Ltac2. *)
+
+val wit_ltac1val : (Ltac_plugin.Tacexpr.raw_tactic_expr, Ltac_plugin.Tacexpr.glob_tactic_expr) Arg.tag
+(** Ltac1 AST quotation, seen as a value-returning expression, with type Ltac1.t. *)
diff --git a/theories/Ltac1.v b/theories/Ltac1.v
new file mode 100644
index 0000000000..c4e0b606d0
--- /dev/null
+++ b/theories/Ltac1.v
@@ -0,0 +1,36 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(** This module defines the Ltac2 FFI to Ltac1 code. Due to intricate semantics
+    of the latter, the functions described here are voluntarily under-specified.
+    Not for the casual user, handle with care and expect undefined behaviours
+    otherwise. **)
+
+Require Import Ltac2.Init.
+
+Ltac2 Type t.
+(** Dynamically-typed Ltac1 values. *)
+
+Ltac2 @ external ref : ident list -> t := "ltac2" "ltac1_ref".
+(** Returns the Ltac1 definition with the given absolute name. *)
+
+Ltac2 @ external run : t -> unit := "ltac2" "ltac1_run".
+(** Runs an Ltac1 value, assuming it is a 'tactic', i.e. not returning
+    anything. *)
+
+Ltac2 @ external apply : t -> t list -> (t -> unit) -> unit := "ltac2" "ltac1_apply".
+(** Applies an Ltac1 value to a list of arguments, and provides the result in
+    CPS style. It does **not** run the returned value. *)
+
+(** Conversion functions *)
+
+Ltac2 @ external of_constr : constr -> t := "ltac2" "ltac1_of_constr".
+Ltac2 @ external to_constr : t -> constr option := "ltac2" "ltac1_to_constr".
+
+Ltac2 @ external of_list : t list -> t := "ltac2" "ltac1_of_list".
+Ltac2 @ external to_list : t -> t list option := "ltac2" "ltac1_to_list".
diff --git a/theories/Ltac2.v b/theories/Ltac2.v
index e838fb7b81..ac90f63560 100644
--- a/theories/Ltac2.v
+++ b/theories/Ltac2.v
@@ -20,4 +20,5 @@ Require Ltac2.Fresh.
 Require Ltac2.Pattern.
 Require Ltac2.Std.
 Require Ltac2.Env.
+Require Ltac2.Ltac1.
 Require Export Ltac2.Notations.