Ltac2 preterm antiquotation $preterm:x

Author: SkySkimmer

dev/ci/user-overlays/17359-SkySkimmer-tac2-preterm-antiquot.sh

@@ -0,0 +1 @@
+overlay serapi https://github.com/SkySkimmer/coq-serapi tac2-preterm-antiquot 17359

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

@@ -0,0 +1,5 @@
+- **Added:**
+  Ltac2 preterm antiquotation `$preterm:`
+  (`#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

@@ -745,10 +745,20 @@ the notation section.
 
 .. prodn:: term += $@lident
 
+or equivalently
+
+.. prodn:: term += $constr:@lident
+
 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 += $preterm:@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_dollar_ident_colon_ident =
+  let open Pcoq.Lookahead in
+  to_entry "test_dollar_ident_colon_ident" begin
+    lk_kw "$" >> lk_ident >> lk_kw ":" >> lk_ident >> check_no_space
+  end
+
 let test_ltac1_env =
   let open Pcoq.Lookahead in
   to_entry "test_ltac1_env" begin
@@ -939,8 +945,19 @@ let rules = [
     Production.make
       (Rule.stop ++ Symbol.nterm test_dollar_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_quotation) id in
+      let id = CAst.make ~loc id in
+      let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_var_quotation) (None, id) in
+      CAst.make ~loc (CGenarg arg)
+    end
+  );
+
+  Pcoq.(
+    Production.make
+      (Rule.stop ++ Symbol.nterm test_dollar_ident_colon_ident ++
+       Symbol.token (PKEYWORD "$") ++ Symbol.nterm Prim.identref ++
+       Symbol.token (PKEYWORD ":") ++ Symbol.nterm Prim.identref)
+    begin fun id _ kind _ _ loc ->
+      let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2_var_quotation) (Some kind, id) in
       CAst.make ~loc (CGenarg arg)
     end
   );

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
@@ -1641,8 +1653,12 @@ let intern_constr self ist c =
   let (_, (c, _)) = Genintern.intern Stdarg.wit_constr ist c in
   let v = match DAst.get c with
     | GGenarg (GenArg (Glbwit tag, v)) ->
-      begin match genarg_type_eq tag wit_ltac2_quotation with
-      | Some Refl -> GlbTacexpr (GTacVar v)
+      begin match genarg_type_eq tag wit_ltac2_var_quotation with
+      | Some Refl ->
+        begin match (fst v) with
+        | ConstrVar -> GlbTacexpr (GTacVar (snd v))
+        | _ -> GlbVal c
+        end
       | None -> GlbVal c
       end
     | _ -> GlbVal c
@@ -1904,32 +1920,72 @@ let () =
   in
   GlobEnv.register_constr_interp0 wit_ltac2_constr interp
 
+let interp_constr_var_as_constr ?loc env sigma tycon id =
+  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 c = Value.to_constr c in
+  let t = Retyping.get_type_of env sigma c in
+  let j = { Environ.uj_val = c; uj_type = t } in
+  match tycon with
+  | None ->
+    j, sigma
+  | Some ty ->
+    let sigma =
+      try Evarconv.unify_leq_delay env sigma t ty
+      with Evarconv.UnableToUnify (sigma,e) ->
+        Pretype_errors.error_actual_type ?loc env sigma j ty e
+    in
+    {j with Environ.uj_type = ty}, sigma
+
+let interp_preterm_var_as_constr ?loc 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
+
 let () =
-  let interp ?loc ~poly env sigma tycon id =
-    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 c = Value.to_constr c in
-    let t = Retyping.get_type_of env sigma c in
-    let j = { Environ.uj_val = c; uj_type = t } in
-    match tycon with
-    | None ->
-      j, sigma
-    | Some ty ->
-      let sigma =
-        try Evarconv.unify_leq_delay env sigma t ty
-        with Evarconv.UnableToUnify (sigma,e) ->
-          Pretype_errors.error_actual_type ?loc env sigma j ty e
-      in
-      {j with Environ.uj_type = ty}, sigma
+  let interp ?loc ~poly env sigma tycon (kind,id) =
+    let f = match kind with
+      | ConstrVar -> interp_constr_var_as_constr
+      | PretermVar -> interp_preterm_var_as_constr
+    in
+    f ?loc env sigma tycon id
   in
-  GlobEnv.register_constr_interp0 wit_ltac2_quotation interp
+  GlobEnv.register_constr_interp0 wit_ltac2_var_quotation 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_raw (kind,id) = Genprint.PrinterBasic (fun _env _sigma ->
+      let ppkind =
+      match kind with
+        | None -> mt()
+        | Some kind -> Id.print kind.CAst.v ++ str ":"
+      in
+      str "$" ++ ppkind ++ Id.print id.CAst.v)
+  in
+  let pr_glb (kind,id) = Genprint.PrinterBasic (fun _env _sigma ->
+      let ppkind = match kind with
+        | ConstrVar -> mt()
+        | PretermVar -> str "preterm:"
+      in
+      str "$" ++ ppkind ++ 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
+  Genprint.register_print0 wit_ltac2_var_quotation pr_raw pr_glb pr_top
 
 let () =
   let subs avoid globs (ids, tac) =

plugins/ltac2/tac2env.ml

@@ -308,16 +308,20 @@ let ltac1_prefix =
 
 (** Generic arguments *)
 
+type var_quotation_kind =
+  | ConstrVar
+  | PretermVar
+
 let wit_ltac2in1 = Genarg.make0 "ltac2in1"
 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_var_quotation = Genarg.make0 "ltac2:quotation"
 let wit_ltac2_val = Genarg.make0 "ltac2:value"
 
 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_var_quotation None
 
 let is_constructor_id id =
   let id = Id.to_string id in

plugins/ltac2/tac2env.mli

@@ -165,8 +165,13 @@ val wit_ltac2in1_val : (Id.t CAst.t list * raw_tacexpr, glb_tacexpr, Util.Empty.
 val wit_ltac2_constr : (raw_tacexpr, Id.Set.t * glb_tacexpr, Util.Empty.t) genarg_type
 (** Ltac2 quotations in Gallina terms *)
 
-val wit_ltac2_quotation : (Id.t Loc.located, Id.t, Util.Empty.t) genarg_type
-(** Ltac2 quotations for variables "$x" in Gallina terms *)
+type var_quotation_kind =
+  | ConstrVar
+  | PretermVar
+
+val wit_ltac2_var_quotation : (lident option * lident, var_quotation_kind * Id.t, Util.Empty.t) genarg_type
+(** Ltac2 quotations for variables "$x" or "$kind:foo" in Gallina terms.
+    NB: "$x" means "$constr:x" *)
 
 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

plugins/ltac2/tac2intern.ml

@@ -1904,30 +1904,42 @@ 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 intern_var_quotation ist (kind, { CAst.v = id; loc }) =
   let open Genintern in
-  let intern ist (loc, id) =
-    let env = match Genintern.Store.get ist.extra ltac2_env with
+  let kind = match kind with
+    | None -> ConstrVar
+    | Some kind -> match Id.to_string kind.CAst.v with
+      | "constr" -> ConstrVar
+      | "preterm" -> PretermVar
+      | _ ->
+        CErrors.user_err ?loc:kind.loc
+          Pp.(str "Unknown Ltac2 variable quotation kind" ++ spc() ++ Id.print kind.v)
+  in
+  let typ = match kind with
+    | ConstrVar -> t_constr
+    | PretermVar -> t_preterm
+  in
+  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, (kind, id))
+
+let () = Genintern.register_intern0 wit_ltac2_var_quotation intern_var_quotation
 
-let () = Genintern.register_subst0 wit_ltac2_quotation (fun _ id -> id)
+let () = Genintern.register_subst0 wit_ltac2_var_quotation (fun _ v -> v)

pretyping/pretyping.ml

@@ -1451,6 +1451,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,62 @@
+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 $preterm: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:($preterm: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 *) *)
+
+(* a bit close to stack overflow *)
+(* Time Ltac2 Eval *)
+(*   let c := z2nat_preterm constr:(20000) in *)
+(*   let c := Constr.pretype c in *)
+(*   Message.print (Message.of_constr c). (* 32 secs *) *)

test-suite/output-coqtop/ltac2_var_quot.out

@@ -0,0 +1,53 @@
+
+
+Coq < Coq < Toplevel input, characters 7-9:
+> Check $x.
+>       ^^
+Error: Unbound value x
+
+Coq < Coq < Toplevel input, characters 16-17:
+> Check $preterm:x.
+>                ^
+Error: Unbound value x
+
+Coq < Coq < Toplevel input, characters 7-8:
+> Check $ x.
+>       ^
+Error: Syntax error: [lconstr] expected after 'Check' (in [query_command]).
+
+Coq < Coq < Toplevel input, characters 7-8:
+> Check $ preterm:x.
+>       ^
+Error: Syntax error: [lconstr] expected after 'Check' (in [query_command]).
+
+Coq < Coq < Toplevel input, characters 7-8:
+> Check $ preterm : x.
+>       ^
+Error: Syntax error: [lconstr] expected after 'Check' (in [query_command]).
+
+Coq < Coq < Toplevel input, characters 18-19:
+> Check $preterm : x.
+>                  ^
+Error: The reference x was not found in the current environment.
+
+Coq < Coq < Toplevel input, characters 16-24:
+> Check fun x => $preterm : x.
+>                ^^^^^^^^
+Error: Unbound value preterm
+
+Coq < Coq < Toplevel input, characters 17-18:
+> Check $preterm: x.
+>                 ^
+Error: The reference x was not found in the current environment.
+
+Coq < Coq < Toplevel input, characters 16-24:
+> Check fun x => $preterm: x.
+>                ^^^^^^^^
+Error: Unbound value preterm
+
+Coq < Coq < Toplevel input, characters 7-8:
+> Check $ preterm :x.
+>       ^
+Error: Syntax error: [lconstr] expected after 'Check' (in [query_command]).
+
+Coq < 

test-suite/output-coqtop/ltac2_var_quot.v

@@ -0,0 +1,21 @@
+Require Import Ltac2.Ltac2.
+
+Check $x.
+
+Check $preterm:x.
+
+Check $ x.
+
+Check $ preterm:x.
+
+Check $ preterm : x.
+
+Check $preterm : x.
+
+Check fun x => $preterm : x.
+
+Check $preterm: x.
+
+Check fun x => $preterm: x.
+
+Check $ preterm :x.