From d7c12ae513a5330f50f7e6f1f40e0649e431157a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 24 Jan 2024 15:58:15 +0100 Subject: [PATCH] Ltac2.Ltac1: add to/of_preterm --- .../06-Ltac2-language/18551-ltac2-ltac1-uconstr.rst | 4 ++++ plugins/ltac2/tac2core.ml | 6 +++--- plugins/ltac2/tac2ffi.ml | 4 ++++ plugins/ltac2/tac2ffi.mli | 4 ++++ plugins/ltac2/tac2print.ml | 2 +- plugins/ltac2_ltac1/tac2core_ltac1.ml | 8 ++++++++ user-contrib/Ltac2/Ltac1.v | 4 ++++ 7 files changed, 28 insertions(+), 4 deletions(-) create mode 100644 doc/changelog/06-Ltac2-language/18551-ltac2-ltac1-uconstr.rst diff --git a/doc/changelog/06-Ltac2-language/18551-ltac2-ltac1-uconstr.rst b/doc/changelog/06-Ltac2-language/18551-ltac2-ltac1-uconstr.rst new file mode 100644 index 000000000000..eb95793e28db --- /dev/null +++ b/doc/changelog/06-Ltac2-language/18551-ltac2-ltac1-uconstr.rst @@ -0,0 +1,4 @@ +- **Added:** + `Ltac2.Ltac1.of_preterm` and `to_preterm` + (`#18551 `_, + by Gaëtan Gilbert). diff --git a/plugins/ltac2/tac2core.ml b/plugins/ltac2/tac2core.ml index 9424fc5045c9..ea2ebf8b2751 100644 --- a/plugins/ltac2/tac2core.ml +++ b/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; diff --git a/plugins/ltac2/tac2ffi.ml b/plugins/ltac2/tac2ffi.ml index fd98c65d9484..93b92e7a9a65 100644 --- a/plugins/ltac2/tac2ffi.ml +++ b/plugins/ltac2/tac2ffi.ml @@ -248,6 +248,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 diff --git a/plugins/ltac2/tac2ffi.mli b/plugins/ltac2/tac2ffi.mli index 594366fee870..8b78ac25e8dc 100644 --- a/plugins/ltac2/tac2ffi.mli +++ b/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 diff --git a/plugins/ltac2/tac2print.ml b/plugins/ltac2/tac2print.ml index 540507a99f2b..3f00db744a56 100644 --- a/plugins/ltac2/tac2print.ml +++ b/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 ")" diff --git a/plugins/ltac2_ltac1/tac2core_ltac1.ml b/plugins/ltac2_ltac1/tac2core_ltac1.ml index b2e53c37d09c..0fc9f6e4856c 100644 --- a/plugins/ltac2_ltac1/tac2core_ltac1.ml +++ b/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 diff --git a/user-contrib/Ltac2/Ltac1.v b/user-contrib/Ltac2/Ltac1.v index cf550b84b299..920c8248c751 100644 --- a/user-contrib/Ltac2/Ltac1.v +++ b/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".