Adding a module to manipulate Ltac1 values.

8 files changed, 116 insertions, 2 deletions

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. *)