Merge PR #18551: Ltac2.Ltac1: add to/of_preterm

Reviewed-by: ppedrot
Ack-by: JasonGross
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>

doc/changelog/06-Ltac2-language/18551-ltac2-ltac1-uconstr.rst

@@ -0,0 +1,4 @@
+- **Added:**
+  `Ltac2.Ltac1.of_preterm` and `to_preterm`
+  (`#18551 <https://github.com/coq/coq/pull/18551>`_,
+  by Gaëtan Gilbert).

plugins/ltac2/tac2core.ml

@@ -778,7 +778,7 @@ let () = define "expected_without_type_constraint" (ret (repr_ext val_expected_t
     WithoutTypeConstraint
 
 let () =
-  define "constr_pretype" (repr_ext val_pretype_flags @-> repr_ext val_expected_type @-> repr_ext val_preterm @-> tac constr) @@ fun flags expected_type c ->
+  define "constr_pretype" (repr_ext val_pretype_flags @-> repr_ext val_expected_type @-> preterm @-> tac constr) @@ fun flags expected_type c ->
   let pretype env sigma =
     let sigma, t = Pretyping.understand_uconstr ~flags ~expected_type env sigma c in
     Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT t
@@ -1654,7 +1654,7 @@ let () =
       genargs = Tac2interp.set_env env Id.Map.empty;
     } in
     let c = { closure; term = c } in
-    return (Tac2ffi.of_ext val_preterm c)
+    return (Tac2ffi.of_preterm c)
   in
   let subst subst (ids,c) = ids, Detyping.subst_glob_constr (Global.env()) subst c in
   let print env sigma (ids,c) =
@@ -1747,7 +1747,7 @@ let interp_preterm_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 {closure; term} = Tac2ffi.to_ext Tac2ffi.val_preterm c in
+  let {closure; term} = Tac2ffi.to_preterm c in
   let vars = {
     ltac_constrs = closure.typed;
     ltac_uconstrs = closure.untyped;

plugins/ltac2/tac2ffi.ml

@@ -236,6 +236,10 @@ let of_constr c = of_ext val_constr c
 let to_constr c = to_ext val_constr c
 let constr = repr_ext val_constr
 
+let of_preterm c = of_ext val_preterm c
+let to_preterm c = to_ext val_preterm c
+let preterm = repr_ext val_preterm
+
 let of_cast c = of_ext val_cast c
 let to_cast c = to_ext val_cast c
 let cast = repr_ext val_cast

plugins/ltac2/tac2ffi.mli

@@ -111,6 +111,10 @@ val of_constr : EConstr.t -> valexpr
 val to_constr : valexpr -> EConstr.t
 val constr : EConstr.t repr
 
+val of_preterm : Ltac_pretype.closed_glob_constr -> valexpr
+val to_preterm : valexpr -> Ltac_pretype.closed_glob_constr
+val preterm : Ltac_pretype.closed_glob_constr repr
+
 val of_cast : Constr.cast_kind -> valexpr
 val to_cast : valexpr -> Constr.cast_kind
 val cast : Constr.cast_kind repr

plugins/ltac2/tac2print.ml

@@ -831,7 +831,7 @@ let () = register_init "constr" begin fun env sigma c ->
 end
 
 let () = register_init "preterm" begin fun env sigma c ->
-  let c = to_ext val_preterm c in
+  let c = to_preterm c in
   (* XXX should we get the ltac2 env out of the closure and print it too? Maybe with a debug flag? *)
   let c = try Printer.pr_closed_glob_env env sigma c with _ -> str "..." in
   str "preterm:(" ++ c ++ str ")"

plugins/ltac2_ltac1/tac2core_ltac1.ml

@@ -80,6 +80,14 @@ let () =
   define "ltac1_to_constr" (ltac1 @-> ret (option constr))
     Ltac_plugin.Tacinterp.Value.to_constr
 
+let () =
+  define "ltac1_of_preterm" (preterm @-> ret ltac1)
+    Ltac_plugin.Taccoerce.Value.of_uconstr
+
+let () =
+  define "ltac1_to_preterm" (ltac1 @-> ret (option preterm))
+    Ltac_plugin.Taccoerce.Value.to_uconstr
+
 let () =
   define "ltac1_of_ident" (ident @-> ret ltac1)
     Ltac_plugin.Taccoerce.Value.of_ident

user-contrib/Ltac2/Ltac1.v

@@ -40,6 +40,10 @@ Ltac2 @ external apply : t -> t list -> (t -> unit) -> unit := "coq-core.plugins
 Ltac2 @ external of_constr : constr -> t := "coq-core.plugins.ltac2_ltac1" "ltac1_of_constr".
 Ltac2 @ external to_constr : t -> constr option := "coq-core.plugins.ltac2_ltac1" "ltac1_to_constr".
 
+(** [preterm] is called [uconstr] in Ltac1. *)
+Ltac2 @ external of_preterm : preterm -> t := "coq-core.plugins.ltac2_ltac1" "ltac1_of_preterm".
+Ltac2 @ external to_preterm : t -> preterm option := "coq-core.plugins.ltac2_ltac1" "ltac1_to_preterm".
+
 Ltac2 @ external of_ident : ident -> t := "coq-core.plugins.ltac2_ltac1" "ltac1_of_ident".
 Ltac2 @ external to_ident : t -> ident option := "coq-core.plugins.ltac2_ltac1" "ltac1_to_ident".