ltac2 preterm antiquotation

doc/changelog/06-Ltac2-language/17359-tac2-preterm-antiquot.rst

@@ -0,0 +1,5 @@
+- **Added:**
+  Ltac2 preterm antiquotation `$$`
+  (`#17359 <https://github.com/coq/coq/pull/17359>`_,
+  fixes `#13977 <https://github.com/coq/coq/issues/13977>`_,
+  by Gaëtan Gilbert).

doc/sphinx/proof-engine/ltac2.rst

@@ -749,6 +749,12 @@ In a Coq term, writing :g:`$x` is semantically equivalent to
 :g:`ltac2:(Control.refine (fun () => x))`, up to re-typechecking. It allows to
 insert in a concise way an Ltac2 variable of type :n:`constr` into a Coq term.
 
+Similarly variables of type `preterm` have an antiquotation
+
+.. prodn:: term += $$@lident
+
+It is equivalent to pretyping the preterm with the appropriate typing constraint.
+
 Match over terms
 ~~~~~~~~~~~~~~~~
 

plugins/ltac2/g_ltac2.mlg

@@ -65,6 +65,12 @@ let test_dollar_ident =
     lk_kw "$" >> lk_ident >> check_no_space
   end
 
+let test_2dollar_ident =
+  let open Pcoq.Lookahead in
+  to_entry "test_2dollar_ident" begin
+    lk_kw "$$" >> lk_ident >> check_no_space
+  end
+
 let test_ltac1_env =
   let open Pcoq.Lookahead in
   to_entry "test_ltac1_env" begin
@@ -945,6 +951,16 @@ let rules = [
     end
   );
 
+  Pcoq.(
+    Production.make
+      (Rule.stop ++ Symbol.nterm test_2dollar_ident ++ Symbol.token (PKEYWORD "$$") ++ Symbol.nterm Prim.ident)
+    begin fun id _ _ loc ->
+      let id = Loc.tag ~loc id in
+      let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_prequotation) id in
+      CAst.make ~loc (CGenarg arg)
+    end
+  );
+
   Pcoq.(
     Production.make
       (Rule.stop ++ Symbol.nterm test_ampersand_ident ++ Symbol.token (PKEYWORD "&") ++ Symbol.nterm Prim.ident)

plugins/ltac2/tac2core.ml

@@ -43,6 +43,18 @@ let open_constr_no_classes_flags =
   polymorphic = false;
   }
 
+let preterm_flags =
+  let open Pretyping in
+  {
+  use_coercions = true;
+  use_typeclasses = Pretyping.NoUseTC;
+  solve_unification_constraints = true;
+  fail_evar = false;
+  expand_evars = false;
+  program_mode = false;
+  polymorphic = false;
+  }
+
 (** Standard values *)
 
 module Value = Tac2ffi
@@ -1925,12 +1937,42 @@ let () =
   in
   GlobEnv.register_constr_interp0 wit_ltac2_quotation interp
 
+let () =
+  let interp ?loc ~poly env sigma tycon id =
+    let open Ltac_pretype in
+    let ist = Tac2interp.get_env @@ GlobEnv.lfun env in
+    let env = GlobEnv.renamed_env env in
+    let c = Id.Map.find id ist.env_ist in
+    let {closure; term} = Value.to_ext Value.val_preterm c in
+    let vars = {
+      ltac_constrs = closure.typed;
+      ltac_uconstrs = closure.untyped;
+      ltac_idents = closure.idents;
+      ltac_genargs = closure.genargs;
+    }
+    in
+    let flags = preterm_flags in
+    let tycon = let open Pretyping in match tycon with
+      | Some ty -> OfType ty
+      | None -> WithoutTypeConstraint
+    in
+    let sigma, t, ty = Pretyping.understand_ltac_ty flags env sigma vars tycon term in
+    Environ.make_judge t ty, sigma
+  in
+  GlobEnv.register_constr_interp0 wit_ltac2_prequotation interp
+
 let () =
   let pr_raw id = Genprint.PrinterBasic (fun _env _sigma -> assert false) in
   let pr_glb id = Genprint.PrinterBasic (fun _env _sigma -> str "$" ++ Id.print id) in
   let pr_top x = Util.Empty.abort x in
   Genprint.register_print0 wit_ltac2_quotation pr_raw pr_glb pr_top
 
+let () =
+  let pr_raw id = Genprint.PrinterBasic (fun _env _sigma -> assert false) in
+  let pr_glb id = Genprint.PrinterBasic (fun _env _sigma -> str "$$" ++ Id.print id) in
+  let pr_top e = Util.Empty.abort e in
+  Genprint.register_print0 wit_ltac2_prequotation pr_raw pr_glb pr_top
+
 let () =
   let subs avoid globs (ids, tac) =
     (* Let-bind the notation terms inside the tactic *)

plugins/ltac2/tac2env.ml

@@ -313,11 +313,13 @@ let wit_ltac2in1_val = Genarg.make0 "ltac2in1val"
 let wit_ltac2_constr = Genarg.make0 "ltac2:in-constr"
 let wit_ltac2_quotation = Genarg.make0 "ltac2:quotation"
 let wit_ltac2_val = Genarg.make0 "ltac2:value"
+let wit_ltac2_prequotation = Genarg.make0 "ltac2:prequotation"
 
 let () = Geninterp.register_val0 wit_ltac2in1 None
 let () = Geninterp.register_val0 wit_ltac2in1_val None
 let () = Geninterp.register_val0 wit_ltac2_constr None
 let () = Geninterp.register_val0 wit_ltac2_quotation None
+let () = Geninterp.register_val0 wit_ltac2_prequotation None
 
 let is_constructor_id id =
   let id = Id.to_string id in

plugins/ltac2/tac2env.mli

@@ -172,6 +172,9 @@ val wit_ltac2_val : (Util.Empty.t, unit, Util.Empty.t) genarg_type
 (** Embedding Ltac2 closures of type [Ltac1.t -> Ltac1.t] inside Ltac1. There is
     no relevant data because arguments are passed by conventional names. *)
 
+val wit_ltac2_prequotation : (Id.t Loc.located, Id.t, Util.Empty.t) genarg_type
+(** Ltac2 quotations for preterm variables "$$x" in Gallina terms *)
+
 (** {5 Helper functions} *)
 
 val is_constructor_id : Id.t -> bool

plugins/ltac2/tac2intern.ml

@@ -1904,30 +1904,30 @@ let () = Genintern.register_subst0 wit_ltac2in1 (fun s (ids, e) -> ids, subst_ex
 let () = Genintern.register_subst0 wit_ltac2in1_val subst_expr
 let () = Genintern.register_subst0 wit_ltac2_constr (fun s (ids, e) -> ids, subst_expr s e)
 
-let () =
-  let open Genintern in
-  let intern ist (loc, id) =
-    let env = match Genintern.Store.get ist.extra ltac2_env with
+let intern_quotation typ = let open Genintern in
+  fun ist (loc, id) ->
+  let env = match Genintern.Store.get ist.extra ltac2_env with
     | None ->
       (* Only happens when Ltac2 is called from a constr or ltac1 quotation *)
       empty_env ~strict:ist.strict_check ()
     | Some env -> env
-    in
-    (* Special handling of notation variables *)
-    let () =
-      if Id.Map.mem id ist.intern_sign.notation_variable_status then
-        (* Always fail *)
-        unify ?loc env (GTypRef (Other t_preterm, [])) (GTypRef (Other t_constr, []))
-    in
-    let t =
-      try find_var id env
-      with Not_found ->
-        CErrors.user_err ?loc (str "Unbound value " ++ Id.print id)
-    in
-    let t = fresh_mix_type_scheme env t in
-    let () = unify ?loc env t (GTypRef (Other t_constr, [])) in
-    (ist, id)
   in
-  Genintern.register_intern0 wit_ltac2_quotation intern
+  (* Special handling of notation variables *)
+  let () =
+    if Id.Map.mem id ist.intern_sign.notation_variable_status then
+      (* Always fail for constr, never for preterm *)
+      unify ?loc env (GTypRef (Other t_preterm, [])) (GTypRef (Other typ, []))
+  in
+  let t =
+    try find_var id env
+    with Not_found ->
+      CErrors.user_err ?loc (str "Unbound value " ++ Id.print id)
+  in
+  let t = fresh_mix_type_scheme env t in
+  let () = unify ?loc env t (GTypRef (Other typ, [])) in
+  (ist, id)
+
+let () = Genintern.register_intern0 wit_ltac2_quotation (intern_quotation t_constr)
+let () = Genintern.register_intern0 wit_ltac2_prequotation (intern_quotation t_preterm)
 
 let () = Genintern.register_subst0 wit_ltac2_quotation (fun _ id -> id)

pretyping/pretyping.ml

@@ -1452,6 +1452,9 @@ let understand_ltac flags env sigma lvar kind c =
   let (sigma, c, _) = ise_pretype_gen flags env sigma lvar kind c in
   (sigma, c)
 
+let understand_ltac_ty flags env sigma lvar kind c =
+  ise_pretype_gen flags env sigma lvar kind c
+
 (* Fully evaluate an untyped constr *)
 let understand_uconstr ?(flags = all_and_fail_flags)
   ?(expected_type = WithoutTypeConstraint) env sigma c =

pretyping/pretyping.mli

@@ -98,6 +98,10 @@ val understand_ltac : inference_flags ->
   env -> evar_map -> ltac_var_map ->
   typing_constraint -> glob_constr -> evar_map * EConstr.t
 
+val understand_ltac_ty : inference_flags ->
+  env -> evar_map -> ltac_var_map ->
+  typing_constraint -> glob_constr -> evar_map * EConstr.t * EConstr.types
+
 (** Standard call to get a constr from a glob_constr, resolving
     implicit arguments and coercions, and compiling pattern-matching;
     the default inference_flags tells to use type classes and

test-suite/ltac2/preterm_antiquot.v

@@ -0,0 +1,61 @@
+Require Import ZArith.
+Open Scope Z_scope.
+
+Require Import Ltac2.Ltac2.
+
+Ltac2 rec z2nat_preterm x :=
+  let b := eval cbv in (Z.leb $x 0) in
+  lazy_match! b with
+  | true => preterm:(O)
+  | false =>
+      let pred := eval cbv in (Z.pred $x) in
+        let r := z2nat_preterm pred in
+        preterm:(S $$r)
+  end.
+
+
+Ltac2 rec z2nat_constr x :=
+  let b := eval cbv in (Z.leb $x 0) in
+  lazy_match! b with
+  | true => constr:(O)
+  | false => let pred := eval cbv in (Z.pred $x) in
+             let r := z2nat_constr pred in
+             constr:(S $r)
+  end.
+
+Ltac2 mk_app(a: constr)(b: constr) :=
+  Constr.Unsafe.make (Constr.Unsafe.App a [| b |]).
+
+Ltac2 rec z2nat_mk_app x :=
+  let b := eval cbv in (Z.leb $x 0) in
+  lazy_match! b with
+  | true => Env.instantiate reference:(O)
+  | false => let pred := eval cbv in (Z.pred $x) in
+             mk_app (Env.instantiate reference:(S)) (z2nat_mk_app pred)
+  end.
+
+(* Time Ltac2 Eval *)
+(*   let c := z2nat_constr constr:(10000) in *)
+(*   Message.print (Message.of_constr c). (* 9 secs *) *)
+
+(* Time Ltac2 Eval *)
+(*   let c := z2nat_mk_app constr:(10000) in *)
+(*   Message.print (Message.of_constr c). (* <1 secs *) *)
+
+Time Ltac2 Eval
+  let c := z2nat_preterm constr:(10000) in
+  let c := constr:($$c) in
+  Message.print (Message.of_constr c). (* 6 secs *)
+
+(* Time Ltac2 Eval *)
+(*   let c := z2nat_constr constr:(20000) in *)
+(*   Message.print (Message.of_constr c). (* 22 secs *) *)
+
+(* Time Ltac2 Eval *)
+(*   let c := z2nat_mk_app constr:(20000) in *)
+(*   Message.print (Message.of_constr c). (* 1.6 secs *) *)
+
+Time Ltac2 Eval
+  let c := z2nat_preterm constr:(20000) in
+  let c := Constr.pretype c in
+  Message.print (Message.of_constr c). (* 32 secs *)