Allowing to include Coq terms in Ltac2 using the constr:(...) syntax.

3 files changed, 74 insertions, 1 deletions

diff --git a/g_ltac2.ml4 b/g_ltac2.ml4
index 349220f9de..b613f22a8d 100644
--- a/g_ltac2.ml4
+++ b/g_ltac2.ml4
@@ -21,6 +21,9 @@ let tac2def_typ = Gram.entry_create "tactic:tac2def_typ"
 let tac2def_ext = Gram.entry_create "tactic:tac2def_ext"
 let tac2mode = Gram.entry_create "vernac:ltac2_command"
 
+let inj_wit wit loc x = CTacExt (loc, Genarg.in_gen (Genarg.rawwit wit) x)
+let inj_constr loc c = inj_wit Stdarg.wit_constr loc c
+
 GEXTEND Gram
   GLOBAL: tac2expr tac2type tac2def_val tac2def_typ tac2def_ext;
   tac2pat:
@@ -77,6 +80,7 @@ GEXTEND Gram
     [ [ n = Prim.integer -> CTacAtm (!@loc, AtmInt n)
       | s = Prim.string -> CTacAtm (!@loc, AtmStr s)
       | id = Prim.qualid -> CTacRef id
+      | IDENT "constr"; ":"; "("; c = Constr.lconstr; ")" -> inj_constr !@loc c
     ] ]
   ;
   let_clause:
diff --git a/tac2core.ml b/tac2core.ml
index af4124e647..95632bf7b1 100644
--- a/tac2core.ml
+++ b/tac2core.ml
@@ -8,8 +8,11 @@
 
 open CSig
 open Pp
+open CErrors
 open Names
+open Genarg
 open Geninterp
+open Tac2env
 open Tac2expr
 open Proofview.Notations
 
@@ -26,6 +29,7 @@ let t_string = coq_core "string"
 let t_array = coq_core "array"
 let t_unit = coq_core "unit"
 let t_list = coq_core "list"
+let t_constr = coq_core "constr"
 
 let c_nil = coq_core "[]"
 let c_cons = coq_core "::"
@@ -66,6 +70,8 @@ match Val.eq tag tag' with
 let val_pp = Val.create "ltac2:pp"
 let get_pp v = extract_val val_pp v
 
+let val_valexpr = Val.create "ltac2:valexpr"
+
 (** Helper functions *)
 
 let return x = Proofview.tclUNIT x
@@ -117,3 +123,66 @@ let () = Tac2env.define_primitive (pname "array_make") prm_array_make
 let () = Tac2env.define_primitive (pname "array_length") prm_array_length
 let () = Tac2env.define_primitive (pname "array_get") prm_array_get
 let () = Tac2env.define_primitive (pname "array_set") prm_array_set
+
+(** ML types *)
+
+let val_tag t = match val_tag t with
+| Val.Base t -> t
+| _ -> assert false
+
+let tag_constr = val_tag (topwit Stdarg.wit_constr)
+
+let constr_flags () =
+  let open Pretyping in
+  {
+    use_typeclasses = true;
+    solve_unification_constraints = true;
+    use_hook = Pfedit.solve_by_implicit_tactic ();
+    fail_evar = true;
+    expand_evars = true
+  }
+
+(** In Ltac2, the notion of "current environment" only makes sense when there is
+    at most one goal under focus. Contrarily to Ltac1, instead of dynamically
+    focussing when we need it, we raise a non-backtracking error when it does
+    not make sense. *)
+exception NonFocussedGoal
+
+let () = register_handler begin function
+| NonFocussedGoal -> str "Several goals under focus"
+| _ -> raise Unhandled
+end
+
+let pf_apply f =
+  Proofview.Goal.goals >>= function
+  | [] ->
+    Proofview.tclENV >>= fun env ->
+    Proofview.tclEVARMAP >>= fun sigma ->
+    f env sigma
+  | [gl] ->
+    gl >>= fun gl ->
+    f (Proofview.Goal.env gl) (Tacmach.New.project gl)
+  | _ :: _ :: _ ->
+    Proofview.tclLIFT (Proofview.NonLogical.raise NonFocussedGoal)
+
+(** Embed all Ltac2 data into Values *)
+let to_lvar ist =
+  let open Pretyping in
+  let map e = Val.Dyn (val_valexpr, e) in
+  let lfun = Id.Map.map map ist in
+  { empty_lvar with ltac_genargs = lfun }
+
+let () =
+  let open Pretyping in
+  let interp ist (c, _) = pf_apply begin fun env sigma ->
+    let ist = to_lvar ist in
+    let (sigma, c) = understand_ltac (constr_flags ()) env sigma ist WithoutTypeConstraint c in
+    let c = Val.Dyn (tag_constr, c) in
+    Proofview.Unsafe.tclEVARS sigma >>= fun () ->
+    Proofview.tclUNIT c
+  end in
+  let obj = {
+    ml_type = t_constr;
+    ml_interp = interp;
+  } in
+  define_ml_object Stdarg.wit_constr obj
diff --git a/tac2intern.ml b/tac2intern.ml
index 516690dfd3..a554f959a0 100644
--- a/tac2intern.ml
+++ b/tac2intern.ml
@@ -613,7 +613,7 @@ let rec intern_rec env = function
   let genv = Global.env_of_context Environ.empty_named_context_val in
   let ist = empty_glob_sign genv in
   let ist = { ist with extra = Store.set ist.extra ltac2_env env } in
-  let (_, ext) = generic_intern ist ext in
+  let (_, ext) = Flags.with_option Ltac_plugin.Tacintern.strict_check (fun () -> generic_intern ist ext) () in
   (GTacExt ext, GTypRef (tpe.ml_type, []))
 
 and intern_let_rec env loc el e =