From e9ed8befebb9ea9106881fa5e9c4c82bfefc24be Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 18 Feb 2026 14:26:59 +0100 Subject: [PATCH 1/7] Ltac2 expose subst_vars (unsafe API) --- plugins/ltac2/tac2core.ml | 4 ++++ theories/Ltac2/Constr.v | 4 ++++ 2 files changed, 8 insertions(+) diff --git a/plugins/ltac2/tac2core.ml b/plugins/ltac2/tac2core.ml index 3e779c0a8801..733599587a65 100644 --- a/plugins/ltac2/tac2core.ml +++ b/plugins/ltac2/tac2core.ml @@ -694,6 +694,10 @@ let () = define "constr_liftn" (int @-> int @-> constr @-> ret constr) EConstr.Vars.liftn +let () = + define "subst_vars" (list ident @-> constr @-> eret constr) @@ fun ids c _env sigma -> + EConstr.Vars.subst_vars sigma ids c + let () = define "constr_substnl" (list constr @-> int @-> constr @-> ret constr) EConstr.Vars.substnl diff --git a/theories/Ltac2/Constr.v b/theories/Ltac2/Constr.v index ce39400e7082..b4a3e79c8c8e 100644 --- a/theories/Ltac2/Constr.v +++ b/theories/Ltac2/Constr.v @@ -186,6 +186,10 @@ Ltac2 @ external liftn : int -> int -> constr -> constr := "rocq-runtime.plugins Note that with respect to substitution calculi's terminology, [n] is the _shift_ and [k] is the _lift_. *) +Ltac2 @external subst_vars : ident list -> constr -> constr + := "rocq-runtime.plugins.ltac2" "subst_vars". +(** [subst_vars [id1;...;idn] t] substitutes [Var idj] by [Rel j] in [t]. *) + Ltac2 @ external substnl : constr list -> int -> constr -> constr := "rocq-runtime.plugins.ltac2" "constr_substnl". (** [substnl [r₁;...;rₙ] k c] substitutes in parallel [Rel(k+1); ...; Rel(k+n)] with [r₁;...;rₙ] in [c]. *) From 02c32b30e4878e7e5ade8f1840fdae7911e8836d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 18 Feb 2026 14:27:17 +0100 Subject: [PATCH 2/7] Ltac2 expose relevance_of_sort --- plugins/ltac2/tac2core.ml | 5 +++++ theories/Ltac2/Constr.v | 4 ++++ 2 files changed, 9 insertions(+) diff --git a/plugins/ltac2/tac2core.ml b/plugins/ltac2/tac2core.ml index 733599587a65..48c5adfeec36 100644 --- a/plugins/ltac2/tac2core.ml +++ b/plugins/ltac2/tac2core.ml @@ -850,6 +850,11 @@ let () = define "constr_relevance_relevant" (ret relevance) Sorts.Relevant let () = define "constr_relevance_irrelevant" (ret relevance) Sorts.Irrelevant +let () = + define "constr_relevance_of_sort" (sort @-> eret relevance) @@ fun s _ sigma -> + let open EConstr in + ERelevance.kind sigma @@ ESorts.relevance_of_sort s + let () = define "constr_has_evar" (constr @-> tac bool) @@ fun c -> Proofview.tclEVARMAP >>= fun sigma -> diff --git a/theories/Ltac2/Constr.v b/theories/Ltac2/Constr.v index b4a3e79c8c8e..cea95bf4ff0c 100644 --- a/theories/Ltac2/Constr.v +++ b/theories/Ltac2/Constr.v @@ -60,6 +60,10 @@ Module Relevance. Ltac2 @external irrelevant : t := "rocq-runtime.plugins.ltac2" "constr_relevance_irrelevant". + (** Produce the relevance of the given sort (SProp -> irrelevant, etc). *) + Ltac2 @external of_sort : sort -> t + := "rocq-runtime.plugins.ltac2" "constr_relevance_of_sort". + End Relevance. Module Unsafe. From 1525e10c59e0a5e44999f7495512f3a575480b4f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 18 Feb 2026 14:27:26 +0100 Subject: [PATCH 3/7] Ltac2 expose sort_of_product --- doc/corelib/index-list.html.template | 1 + plugins/ltac2/tac2core.ml | 6 ++++++ theories/Ltac2/Sort.v | 17 +++++++++++++++++ 3 files changed, 24 insertions(+) create mode 100644 theories/Ltac2/Sort.v diff --git a/doc/corelib/index-list.html.template b/doc/corelib/index-list.html.template index 2e8228ac8a98..3d7b4326cde9 100644 --- a/doc/corelib/index-list.html.template +++ b/doc/corelib/index-list.html.template @@ -157,6 +157,7 @@ through the Require Import command.

theories/Ltac2/Ref.v theories/Ltac2/Reference.v theories/Ltac2/Rewrite.v + theories/Ltac2/Sort.v theories/Ltac2/Std.v theories/Ltac2/String.v theories/Ltac2/TransparentState.v diff --git a/plugins/ltac2/tac2core.ml b/plugins/ltac2/tac2core.ml index 48c5adfeec36..de9bcb5394cb 100644 --- a/plugins/ltac2/tac2core.ml +++ b/plugins/ltac2/tac2core.ml @@ -860,6 +860,12 @@ let () = Proofview.tclEVARMAP >>= fun sigma -> return (Evarutil.has_undefined_evars sigma c) +let () = + define "sort_of_product" (sort @-> sort @-> eret sort) @@ fun s1 s2 env _ -> + (* XXX ESorts.kind instead of Unsafe? only matters for impredicative set AFAICT *) + let f s = EConstr.Unsafe.to_sorts s in + EConstr.ESorts.make @@ Typeops.sort_of_product env (f s1) (f s2) + (** Uint63 *) let () = define "uint63_compare" (uint63 @-> uint63 @-> ret int) Uint63.compare diff --git a/theories/Ltac2/Sort.v b/theories/Ltac2/Sort.v new file mode 100644 index 000000000000..3d4adf132e56 --- /dev/null +++ b/theories/Ltac2/Sort.v @@ -0,0 +1,17 @@ +(************************************************************************) +(* * The Rocq Prover / The Rocq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* B : s'']. *) +Ltac2 @external sort_of_product : t -> t -> t + := "rocq-runtime.plugins.ltac2" "sort_of_product". From 283131837b99abc2e2368de1982950e9f3cc2fa8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 18 Feb 2026 15:37:52 +0100 Subject: [PATCH 4/7] Ltac2 safe "judgement" APIs --- doc/corelib/index-list.html.template | 1 + plugins/ltac2/tac2core.ml | 48 ++++--- plugins/ltac2/tac2core.mli | 11 +- plugins/ltac2/tac2ffi.ml | 48 ++++++- plugins/ltac2/tac2ffi.mli | 32 ++++- plugins/ltac2/tac2judge.ml | 201 +++++++++++++++++++++++++++ plugins/ltac2/tac2judge.mli | 11 ++ plugins/ltac2/tac2quote.ml | 3 + plugins/ltac2/tac2quote.mli | 3 + theories/Ltac2/Control.v | 18 +++ theories/Ltac2/Init.v | 15 +- theories/Ltac2/Judge.v | 106 ++++++++++++++ 12 files changed, 473 insertions(+), 24 deletions(-) create mode 100644 plugins/ltac2/tac2judge.ml create mode 100644 plugins/ltac2/tac2judge.mli create mode 100644 theories/Ltac2/Judge.v diff --git a/doc/corelib/index-list.html.template b/doc/corelib/index-list.html.template index 3d7b4326cde9..2e5e8fff7911 100644 --- a/doc/corelib/index-list.html.template +++ b/doc/corelib/index-list.html.template @@ -140,6 +140,7 @@ through the Require Import command.

theories/Ltac2/Ind.v theories/Ltac2/Init.v theories/Ltac2/Int.v + theories/Ltac2/Judge.v theories/Ltac2/Lazy.v theories/Ltac2/List.v theories/Ltac2/Ltac1.v diff --git a/plugins/ltac2/tac2core.ml b/plugins/ltac2/tac2core.ml index de9bcb5394cb..fc92e08484b1 100644 --- a/plugins/ltac2/tac2core.ml +++ b/plugins/ltac2/tac2core.ml @@ -67,23 +67,6 @@ open Tac2quote.Refs let v_blk = Valexpr.make_block -let of_relevance = function - | Sorts.Relevant -> ValInt 0 - | Sorts.Irrelevant -> ValInt 1 - | Sorts.RelevanceVar q -> ValBlk (0, [|of_qvar q|]) - -let to_relevance = function - | ValInt 0 -> Sorts.Relevant - | ValInt 1 -> Sorts.Irrelevant - | ValBlk (0, [|qvar|]) -> - let qvar = to_qvar qvar in - Sorts.RelevanceVar qvar - | _ -> assert false - -(* XXX ltac2 exposes relevance internals so breaks ERelevance abstraction - ltac2 Constr.Binder.relevance probably needs to be made an abstract type *) -let relevance = make_repr of_relevance to_relevance - let of_rec_declaration (nas, ts, cs) = let binders = Array.map2 (fun na t -> (na, t)) nas ts in (Tac2ffi.of_array of_binder binders, @@ -177,6 +160,21 @@ let pf_apply ?(catch_exceptions=false) f = | _ :: _ :: _ -> throw Tac2ffi.err_notfocussed +let local_of_env env : local_env = { + local_named = Environ.named_context_val env; + local_rel = Environ.rel_context_val env; +} + +let reset_local_env env ctx = + let env = Environ.reset_with_named_context ctx.local_named env in + Environ.set_rel_context_val ctx.local_rel env + +let pf_apply_in ?(catch_exceptions=false) ctx f = + Proofview.tclEVARMAP >>= fun sigma -> + Proofview.tclENV >>= fun genv -> + let env = reset_local_env genv ctx in + wrap_exceptions ~passthrough:(not catch_exceptions) (fun () -> f env sigma) + open Tac2externals let define ?plugin s = define (pname ?plugin s) @@ -1043,6 +1041,20 @@ let () = | Proofview.Fail e -> return (Error e) end +let () = define "global_env" (unit @-> eret local_env) @@ fun () env _ -> + local_of_env env + +let () = define "goal_env" (unit @-> tac local_env) @@ fun () -> + Proofview.Goal.goals >>= function + | [gl] -> + gl >>= fun gl -> + return (local_of_env (Proofview.Goal.env gl)) + | [] | _ :: _ :: _ -> + throw err_notfocussed + +let () = define "current_env" (unit @-> tac local_env) @@ fun () -> + pf_apply @@ fun env _ -> return (local_of_env env) + let () = define "numgoals" (unit @-> tac int) @@ fun () -> Proofview.numgoals @@ -1114,7 +1126,7 @@ let () = let len = List.length gls in let l = Array.of_list l in if not (is_permutation len l) then - throw (err_invalid_arg (Pp.str "reorder_goals")) + throw (err_invalid_arg (Some (Pp.str "reorder_goals"))) else let gls = Array.of_list gls in let gls = List.init len (fun i -> gls.(l.(i) - 1)) in diff --git a/plugins/ltac2/tac2core.mli b/plugins/ltac2/tac2core.mli index 307f8e985e4f..9c6f417357e6 100644 --- a/plugins/ltac2/tac2core.mli +++ b/plugins/ltac2/tac2core.mli @@ -13,7 +13,16 @@ open Names val throw : ?info:Exninfo.info -> exn -> 'a Proofview.tactic (** [catch_exceptions] default false *) -val pf_apply : ?catch_exceptions:bool -> (Environ.env -> Evd.evar_map -> 'a Proofview.tactic) -> 'a Proofview.tactic +val pf_apply : ?catch_exceptions:bool -> + (Environ.env -> Evd.evar_map -> 'a Proofview.tactic) -> + 'a Proofview.tactic + +val pf_apply_in : ?catch_exceptions:bool -> + Tac2ffi.local_env -> + (Environ.env -> Evd.evar_map -> 'a Proofview.tactic) -> + 'a Proofview.tactic + +val reset_local_env : Environ.env -> Tac2ffi.local_env -> Environ.env (** Adds ltac2 backtrace. With [passthrough:false] (default), acts like [Proofview.wrap_exceptions] + Ltac2 backtrace handling. *) diff --git a/plugins/ltac2/tac2ffi.ml b/plugins/ltac2/tac2ffi.ml index b4c3679d0af1..413938523e67 100644 --- a/plugins/ltac2/tac2ffi.ml +++ b/plugins/ltac2/tac2ffi.ml @@ -37,6 +37,20 @@ module ModField = struct | Rewrule end +type local_env = { + local_named : Environ.named_context_val; + local_rel : Environ.rel_context_val; +} + +type 'a judge = { + env : local_env; + term : EConstr.t; + typ : 'a; +} + +type termj = EConstr.types judge +type typej = EConstr.ESorts.t judge + (** Dynamic tags *) let val_exn = Val.create "exn" @@ -70,6 +84,9 @@ let val_reduction = Val.create "reduction" let val_rewstrategy = Val.create "rewstrategy" let val_modpath = Val.create "modpath" let val_module_field = Val.create "module_field" +let val_local_env = Val.create "local_env" +let val_termj = Val.create "termj" +let val_typej = Val.create "typej" let extract_val (type a) (type b) (tag : a Val.tag) (tag' : b Val.tag) (v : b) : a = match Val.eq tag tag' with @@ -481,6 +498,17 @@ let of_module_field c = of_ext val_module_field c let to_module_field c = to_ext val_module_field c let module_field = repr_ext val_module_field +let of_local_env = of_ext val_local_env +let to_local_env = to_ext val_local_env +let local_env = repr_ext val_local_env + +let of_termj = of_ext val_termj +let to_termj = to_ext val_termj +let termj = repr_ext val_termj + +let of_typej = of_ext val_typej +let to_typej = to_ext val_typej +let typej = repr_ext val_typej let of_reference = let open Names.GlobRef in function | VarRef id -> ValBlk (0, [| of_ident id |]) @@ -500,6 +528,23 @@ let reference = { r_to = to_reference; } +let of_relevance = function + | Sorts.Relevant -> ValInt 0 + | Sorts.Irrelevant -> ValInt 1 + | Sorts.RelevanceVar q -> ValBlk (0, [|of_qvar q|]) + +let to_relevance = function + | ValInt 0 -> Sorts.Relevant + | ValInt 1 -> Sorts.Irrelevant + | ValBlk (0, [|qvar|]) -> + let qvar = to_qvar qvar in + Sorts.RelevanceVar qvar + | _ -> assert false + +(* XXX ltac2 exposes relevance internals so breaks ERelevance abstraction + ltac2 Constr.Binder.relevance probably needs to be made an abstract type *) +let relevance = make_repr of_relevance to_relevance + let err_notfocussed = LtacError (rocq_core "Not_focussed", [||]) @@ -515,5 +560,4 @@ let err_matchfailure = let err_division_by_zero = LtacError (rocq_core "Division_by_zero", [||]) -let err_invalid_arg msg = - LtacError (rocq_core "Invalid_argument", [|of_option of_pp (Some msg)|]) +let err_invalid_arg msg = LtacError (rocq_core "Invalid_argument", [|of_option of_pp msg|]) diff --git a/plugins/ltac2/tac2ffi.mli b/plugins/ltac2/tac2ffi.mli index dab0e6f0f1bd..51e930cf0127 100644 --- a/plugins/ltac2/tac2ffi.mli +++ b/plugins/ltac2/tac2ffi.mli @@ -154,6 +154,10 @@ val of_sort : ESorts.t -> valexpr val to_sort : valexpr -> ESorts.t val sort : ESorts.t repr +val of_relevance : Sorts.relevance -> valexpr +val to_relevance : valexpr -> Sorts.relevance +val relevance : Sorts.relevance repr + val of_reduction : Redexpr.red_expr -> valexpr val to_reduction : valexpr -> Redexpr.red_expr val reduction : Redexpr.red_expr repr @@ -237,6 +241,32 @@ val of_module_field : ModField.t -> valexpr val to_module_field : valexpr -> ModField.t val module_field : ModField.t repr +type local_env = { + local_named : Environ.named_context_val; + local_rel : Environ.rel_context_val; +} + +type 'a judge = { + env : local_env; + term : EConstr.t; + typ : 'a; +} + +type termj = EConstr.types judge +type typej = EConstr.ESorts.t judge + +val of_local_env : local_env -> valexpr +val to_local_env : valexpr -> local_env +val local_env : local_env repr + +val of_termj : termj -> valexpr +val to_termj : valexpr -> termj +val termj : termj repr + +val of_typej : typej -> valexpr +val to_typej : valexpr -> typej +val typej : typej repr + val of_ext : 'a Val.tag -> 'a -> valexpr val to_ext : 'a Val.tag -> valexpr -> 'a val repr_ext : 'a Val.tag -> 'a repr @@ -275,4 +305,4 @@ val err_outofbounds : exn val err_notfound : exn val err_matchfailure : exn val err_division_by_zero : exn -val err_invalid_arg : Pp.t -> exn +val err_invalid_arg : Pp.t option -> exn diff --git a/plugins/ltac2/tac2judge.ml b/plugins/ltac2/tac2judge.ml new file mode 100644 index 000000000000..29e7483660a2 --- /dev/null +++ b/plugins/ltac2/tac2judge.ml @@ -0,0 +1,201 @@ +(************************************************************************) +(* * The Rocq Prover / The Rocq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* + pp_local_env env sigma (repr_to local_env v) } +let () = Tac2print.register_val_printer Tac2quote.Refs.t_termj { val_printer = fun env sigma v _ -> + pp_termj env sigma (repr_to termj v) } +let () = Tac2print.register_val_printer Tac2quote.Refs.t_typej { val_printer = fun env sigma v _ -> + pp_typej env sigma (repr_to typej v) } + +(** Externals *) + +let () = define "env_of_termj" (termj @-> ret local_env) @@ fun t -> t.env + +let () = define "env_of_typej" (typej @-> ret local_env) @@ fun t -> t.env + +let () = define "env_hyps" (local_env @-> ret (list ident)) @@ fun env -> + List.map NamedDecl.get_id env.local_named.env_named_ctx + +let () = define "hypj" (ident @-> local_env @-> tac termj) @@ fun id ctx -> + match EConstr.lookup_named_val id ctx.local_named with + | exception Not_found -> + (* FIXME: Do something more sensible *) + Tacticals.tclZEROMSG + Pp.(str "Hypothesis " ++ quote (Id.print id) ++ str " not found") + | d -> + let t = NamedDecl.get_type d in + return { env = ctx; term = mkVar id; typ=t } + +let () = define "hyp_valuej" (local_env @-> ident @-> tac (option termj)) @@ fun ctx id -> + pf_apply_in ctx @@ fun env _ -> + match EConstr.lookup_named id env with + | exception Not_found -> + (* FIXME: Do something more sensible *) + Tacticals.tclZEROMSG + Pp.(str "Hypothesis " ++ quote (Id.print id) ++ str " not found") + | LocalAssum _ -> return None + | LocalDef (_,bdy,typ) -> return (Some { env = ctx; term = bdy; typ }) + +let () = define "infer_termj" (local_env @-> constr @-> tac termj) @@ fun ctx c -> + pf_apply_in ~catch_exceptions:true ctx @@ fun env sigma -> + let sigma, t = Typing.type_of env sigma c in + Proofview.Unsafe.tclEVARS sigma <*> + return { env = ctx; term = c; typ = t } + +let () = define "termj_is_typej" (termj @-> tac typej) @@ fun { env = ctx; term; typ } -> + pf_apply_in ~catch_exceptions:true ctx @@ fun env sigma -> + let sigma, tj = Typing.type_judgment env sigma (Environ.make_judge term typ) in + Proofview.Unsafe.tclEVARS sigma <*> + return { env = ctx; term = tj.utj_val; typ = tj.utj_type } + +let () = define "typej_is_termj" (typej @-> ret termj) @@ fun { env; term; typ } -> + { env; term; typ = mkSort typ } + +let () = define "typej_of_termj" (termj @-> tac typej) @@ fun j -> + pf_apply_in j.env @@ fun env sigma -> + let s = Retyping.get_sort_of env sigma j.typ in + return { env = j.env; term = j.typ; typ = s } + +let () = define "sort_of_typej" (typej @-> ret sort) @@ fun j -> j.typ + +let () = define "typej_of_sort" (local_env @-> sort @-> ret typej) @@ fun ctx s -> + { env = ctx; term = mkSort s; typ = (ESorts.make @@ Sorts.super @@ EConstr.Unsafe.to_sorts s) } + +let push_named_assum_tac ctx id t r = + if Id.Map.mem id ctx.local_named.env_named_map then + Tac2core.throw + (err_invalid_arg + (Some Pp.(str "Ltac2 judgement push_named_assum: " ++ Id.print id ++ str " not free."))) + else + let idr = Context.make_annot id r in + let local_named = EConstr.push_named_context_val (LocalAssum (idr,t)) ctx.local_named in + return { local_named; local_rel = ctx.local_rel } + +let () = + define "unsafe_push_named_assum" (local_env @-> ident @-> constr @-> relevance @-> tac local_env) @@ fun ctx id t r -> + push_named_assum_tac ctx id t (ERelevance.make r) + +let () = define "push_named_assum" (ident @-> typej @-> tac local_env) @@ fun id j -> + Proofview.tclEVARMAP >>= fun sigma -> + if not (CList.is_empty j.env.local_rel.env_rel_ctx) && not (Vars.closed0 sigma j.term) then + (* is_empty test is a fast path, incorrect with unsafe terms but good enough in the safe case *) + Tac2core.throw + (err_invalid_arg + (Some Pp.(str "Ltac2 judgement push_named_assum: non closed type."))) + else + push_named_assum_tac j.env id j.term (ESorts.relevance_of_sort j.typ) + +let push_named_def_tac ctx id c t r = + Proofview.tclEVARMAP >>= fun sigma -> + if Id.Map.mem id ctx.local_named.env_named_map then + Tac2core.throw + (err_invalid_arg + (Some Pp.(str "Ltac2 judgement push_named_def: " ++ Id.print id ++ str " not free."))) + else + let idr = Context.make_annot id r in + let local_named = EConstr.push_named_context_val (LocalDef (idr,c,t)) ctx.local_named in + return { local_named; local_rel = ctx.local_rel } + +let () = define "unsafe_push_named_def" (local_env @-> ident @-> constr @-> constr @-> relevance @-> tac local_env) @@ fun ctx id c t r -> + push_named_def_tac ctx id c t (ERelevance.make r) + +let () = define "push_named_def" (ident @-> termj @-> tac local_env) @@ fun id j -> + pf_apply_in j.env @@ fun env sigma -> + if not (CList.is_empty j.env.local_rel.env_rel_ctx) && + (not (Vars.closed0 sigma j.typ) || not (Vars.closed0 sigma j.term)) then + (* is_empty test is a fast path, incorrect with unsafe terms but good enough in the safe case *) + Tac2core.throw + (err_invalid_arg + (Some Pp.(str "Ltac2 judgement push_named_def: non closed argument."))) + else + push_named_def_tac j.env id j.term j.typ (Retyping.relevance_of_term env sigma j.term) + +let () = define "term_of_termj" (termj @-> ret constr) @@ fun t -> t.term + +let () = define "type_of_typej" (typej @-> ret constr) @@ fun t -> t.term + +let understand_uconstr_ty ~flags ~expected_type env sigma c = + let open Ltac_pretype in + let { closure; term } = c in + let vars = { + ltac_constrs = closure.typed; + ltac_uconstrs = closure.untyped; + ltac_idents = closure.idents; + ltac_genargs = closure.genargs; + } in + Pretyping.understand_ltac_ty flags env sigma vars expected_type term + +let () = define "pretype_judge" (pretype_flags @-> local_env @-> preterm @-> tac termj) @@ fun flags ctx c -> + pf_apply_in ~catch_exceptions:true ctx @@ fun env sigma -> + let sigma, t, typ = + understand_uconstr_ty ~flags ~expected_type:WithoutTypeConstraint env sigma c + in + let res = { env = ctx; term = t; typ } in + Proofview.Unsafe.tclEVARS sigma <*> + return res + +let () = define "pretype_type_judge" (pretype_flags @-> local_env @-> preterm @-> tac typej) @@ fun flags ctx c -> + pf_apply_in ~catch_exceptions:true ctx @@ fun env sigma -> + let sigma, t, ty = + understand_uconstr_ty ~flags ~expected_type:IsType env sigma c + in + let s = destSort sigma ty in + let res = { env = ctx; term = t; typ = s } in + Proofview.Unsafe.tclEVARS sigma <*> + return res + +let () = define "pretype_in_expecting" (pretype_flags @-> preterm @-> typej @-> tac termj) @@ fun flags c { env = ctx; term=ty; typ=s } -> + pf_apply_in ~catch_exceptions:true ctx @@ fun env sigma -> + let sigma, t, ty = + understand_uconstr_ty ~flags ~expected_type:(OfType ty) env sigma c + in + let res = { env = ctx; term = t; typ = ty } in + Proofview.Unsafe.tclEVARS sigma <*> + return res + +let () = define "message_of_env" (local_env @-> tac pp) @@ fun ctx -> + pf_apply_in ctx @@ fun env sigma -> return (Printer.pr_context_of env sigma) + +let () = define "message_of_constr_in_env" (local_env @-> constr @-> tac pp) @@ fun ctx c -> + pf_apply_in ctx @@ fun env sigma -> return (Printer.pr_econstr_env env sigma c) diff --git a/plugins/ltac2/tac2judge.mli b/plugins/ltac2/tac2judge.mli new file mode 100644 index 000000000000..166d0f75097a --- /dev/null +++ b/plugins/ltac2/tac2judge.mli @@ -0,0 +1,11 @@ +(************************************************************************) +(* * The Rocq Prover / The Rocq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* 'a) (handle : exn -> 'a) : 'a := once (fun () => plus run handle). (** [once_plus run handle] is [once] applied to [plus run handle]. *) +(** Environments *) + +(** Return the global environment (containing section variables and no goal hypotheses). *) +Ltac2 @external global_env : unit -> env + := "rocq-runtime.plugins.ltac2" "global_env". + +(** If 1 goal is focused, return the goal environment + (containing goal hypotheses, and any section variables which haven't been cleared). + Otherwise throw [Not_focussed]. *) +Ltac2 @external goal_env : unit -> env + := "rocq-runtime.plugins.ltac2" "goal_env". + +(** If no goals are focused, [global_env]. + If 1 goal is focused, [goal_env]. + Otherwise throw [Not_focussed]. *) +Ltac2 @external current_env : unit -> env + := "rocq-runtime.plugins.ltac2" "current_env". + (** Proof state manipulation *) Ltac2 @ external numgoals : unit -> int := "rocq-runtime.plugins.ltac2" "numgoals". diff --git a/theories/Ltac2/Init.v b/theories/Ltac2/Init.v index 43fa27cf6b73..5964561f01bf 100644 --- a/theories/Ltac2/Init.v +++ b/theories/Ltac2/Init.v @@ -25,6 +25,19 @@ Ltac2 Type uint63. Ltac2 Type float. Ltac2 Type pstring. +(** Type of terms. "Safe" APIs using this type typically assume 1 or 0 + focused goals such that the term are well typed in the current + goal environment (in the global environment when no goals are focused). *) +Ltac2 Type constr. + +(** Type of preterms (term syntax which has not been typechecked, cf + "type inference" glossary item in the refman). *) +Ltac2 Type preterm. + +(** Type of environments. Environments contain named and local variables + (respectively Var and Ral in Constr.Unsafe). *) +Ltac2 Type env. + (** Constr-specific built-in types *) Ltac2 Type meta. Ltac2 Type evar. @@ -36,8 +49,6 @@ Ltac2 Type inductive. Ltac2 Type constructor. Ltac2 Type projection. Ltac2 Type pattern. -Ltac2 Type constr. -Ltac2 Type preterm. Ltac2 Type binder. Ltac2 Type message. diff --git a/theories/Ltac2/Judge.v b/theories/Ltac2/Judge.v new file mode 100644 index 000000000000..5c850dc0e501 --- /dev/null +++ b/theories/Ltac2/Judge.v @@ -0,0 +1,106 @@ +(************************************************************************) +(* * The Rocq Prover / The Rocq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* env + := "rocq-runtime.plugins.ltac2" "env_of_termj". + +(** From argument [Γ ⊢ t : s] return [Γ]. *) +Ltac2 @external env_of_typej : typej -> env + := "rocq-runtime.plugins.ltac2" "env_of_typej". + +(** Returns the idents bound in argument [Γ]. *) +Ltac2 @external env_hyps : env -> ident list + := "rocq-runtime.plugins.ltac2" "env_hyps". + +(** From [id] and [Γ], if [id : t ∈ Γ] or [id := v : t ∈ Γ] return [Γ ⊢ id : t]. + If [id ∉ Γ], backtracking failure. *) +Ltac2 @external hypj : ident -> env -> termj + := "rocq-runtime.plugins.ltac2" "hypj". + +(** From [id] and [Γ], if [id := v : t ∈ Γ] return [Some (Γ ⊢ v : t)]. + If [id : t ∈ Γ] without a body, return [None]. + If [id ∉ Γ], backtracking failure. *) +Ltac2 @external hyp_valuej : ident -> env -> termj option + := "rocq-runtime.plugins.ltac2" "hyp_valuej". + +(** From arguments [Γ] and [c], + check that [c] is well typed in [Γ] inferring type [t] + and return [Γ ⊢ c : t]. *) +Ltac2 @external infer_termj : env -> constr -> termj + := "rocq-runtime.plugins.ltac2" "infer_termj". + +(* XXX version which doesn't define evars? *) +(** If the given judgement is [Γ ⊢ t : s] where [s] is a sort + (or evar which can be defined to a fresh sort), + return type judgement [Γ ⊢ t : s]. + Not to be confused with [typej_of_termj]. *) +Ltac2 @external termj_is_typej : termj -> typej + := "rocq-runtime.plugins.ltac2" "termj_is_typej". + +(** From type judgement [Γ ⊢ t : s] return term judgement [Γ ⊢ t : s]. *) +Ltac2 @external typej_is_termj : typej -> termj + := "rocq-runtime.plugins.ltac2" "typej_is_termj". + +(** From argument [Γ ⊢ c : t], return [Γ ⊢ t : s]. + Must retype [t] to get its sort [s]. *) +Ltac2 @external typej_of_termj : termj -> typej + := "rocq-runtime.plugins.ltac2" "typej_of_termj". + +(** From argument [Γ ⊢ t : s], return [s] *) +Ltac2 @external sort_of_typej : typej -> sort + := "rocq-runtime.plugins.ltac2" "sort_of_typej". + +(** From [Γ] and [s] produce [Γ ⊢ s : s+1]. + Using this may cause inconvenient errors until algebraic universe + support improves in Rocq. *) +Ltac2 @external typej_of_sort : env -> sort -> typej + := "rocq-runtime.plugins.ltac2" "typej_of_sort". + +(** From arguments [id] and [Γ ⊢ t : s], produce [Γ, id : t]. + [id] must be fresh in [Γ]. [t] must not contain local (Rel) variables. *) +Ltac2 @external push_named_assum : ident -> typej -> env + := "rocq-runtime.plugins.ltac2" "push_named_assum". + +(** From arguments [id] and [Γ ⊢ c : t], produce [Γ, id := c : t]. + [id] must be fresh in [Γ]. [c] and [t] must not contain local (Rel) variables. + The relevance is obtained by examining the term + (faster than retyping but not quite constant time). *) +Ltac2 @external push_named_def : ident -> termj -> env + := "rocq-runtime.plugins.ltac2" "push_named_def". + +(** Infer a term judgement from a preterm in a given environment. *) +Ltac2 @external pretype_judge : Constr.Pretype.Flags.t -> env -> preterm -> termj + := "rocq-runtime.plugins.ltac2" "pretype_judge". + +(** Infer a type judgement from a preterm in a given environment. *) +Ltac2 @external pretype_type_judge : Constr.Pretype.Flags.t -> env -> preterm -> typej + := "rocq-runtime.plugins.ltac2" "pretype_type_judge". + +(** Infer a term judgement from a preterm at a given expected type + (the judgement for the expected type contains the environment). *) +Ltac2 @external pretype_in_expecting : Constr.Pretype.Flags.t -> preterm -> typej -> termj + := "rocq-runtime.plugins.ltac2" "pretype_in_expecting". + +(** Print the given environment. Named and local variables are not distinguished. *) +Ltac2 @external message_of_env : env -> message + := "rocq-runtime.plugins.ltac2" "message_of_env". From 7d817a0f9a82a4c5b3e55d49206d225159b00991 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 18 Feb 2026 16:10:44 +0100 Subject: [PATCH 5/7] Ltac2 "unsafe" local env APIs --- plugins/ltac2/tac2core.ml | 10 +++++++ plugins/ltac2/tac2judge.ml | 14 +++++++--- plugins/ltac2/tac2stdlib.ml | 32 +++++++++++++++++++--- plugins/ltac2/tac2tactics.ml | 14 ++++------ plugins/ltac2/tac2tactics.mli | 4 +-- tactics/tactics.ml | 8 ++---- tactics/tactics.mli | 9 ++++--- theories/Ltac2/Constr.v | 28 ++++++++++++++++++++ theories/Ltac2/Judge.v | 50 +++++++++++++++++++++++++++++++++++ theories/Ltac2/Message.v | 6 +++++ theories/Ltac2/Std.v | 9 +++++++ theories/Ltac2/Unification.v | 23 ++++++++++++++++ 12 files changed, 178 insertions(+), 29 deletions(-) diff --git a/plugins/ltac2/tac2core.ml b/plugins/ltac2/tac2core.ml index fc92e08484b1..a6fb5f0c8fb3 100644 --- a/plugins/ltac2/tac2core.ml +++ b/plugins/ltac2/tac2core.ml @@ -853,6 +853,16 @@ let () = let open EConstr in ERelevance.kind sigma @@ ESorts.relevance_of_sort s +let () = + define "relevance_of_term_in_env" (local_env @-> constr @-> tac relevance) @@ fun ctx t -> + pf_apply_in ctx @@ fun env sigma -> + return (EConstr.Unsafe.to_relevance @@ Retyping.relevance_of_term env sigma t) + +let () = + define "relevance_of_type_in_env" (local_env @-> constr @-> tac relevance) @@ fun ctx t -> + pf_apply_in ctx @@ fun env sigma -> + return (EConstr.Unsafe.to_relevance @@ Retyping.relevance_of_type env sigma t) + let () = define "constr_has_evar" (constr @-> tac bool) @@ fun c -> Proofview.tclEVARMAP >>= fun sigma -> diff --git a/plugins/ltac2/tac2judge.ml b/plugins/ltac2/tac2judge.ml index 29e7483660a2..8f8b75ff02ac 100644 --- a/plugins/ltac2/tac2judge.ml +++ b/plugins/ltac2/tac2judge.ml @@ -151,10 +151,6 @@ let () = define "push_named_def" (ident @-> termj @-> tac local_env) @@ fun id j else push_named_def_tac j.env id j.term j.typ (Retyping.relevance_of_term env sigma j.term) -let () = define "term_of_termj" (termj @-> ret constr) @@ fun t -> t.term - -let () = define "type_of_typej" (typej @-> ret constr) @@ fun t -> t.term - let understand_uconstr_ty ~flags ~expected_type env sigma c = let open Ltac_pretype in let { closure; term } = c in @@ -199,3 +195,13 @@ let () = define "message_of_env" (local_env @-> tac pp) @@ fun ctx -> let () = define "message_of_constr_in_env" (local_env @-> constr @-> tac pp) @@ fun ctx c -> pf_apply_in ctx @@ fun env sigma -> return (Printer.pr_econstr_env env sigma c) + +let () = define "term_of_termj" (termj @-> ret constr) @@ fun t -> t.term + +let () = define "type_of_typej" (typej @-> ret constr) @@ fun t -> t.term + +let () = define "unsafe_typej" (local_env @-> constr @-> sort @-> ret typej) @@ fun ctx t s -> + { env = ctx; term=t; typ=s } + +let () = define "unsafe_termj" (constr @-> typej @-> ret termj) @@ fun c j -> + { env = j.env; term=c; typ=j.term } diff --git a/plugins/ltac2/tac2stdlib.ml b/plugins/ltac2/tac2stdlib.ml index c90c57a08a5e..38b75caf81a0 100644 --- a/plugins/ltac2/tac2stdlib.ml +++ b/plugins/ltac2/tac2stdlib.ml @@ -358,8 +358,15 @@ let () = let () = define "reduce_constr" - (reduction @-> constr @-> tac constr) - Tac2tactics.reduce_constr + (reduction @-> constr @-> tac constr) @@ fun r c -> + Tac2core.pf_apply @@ fun env sigma -> + Tac2tactics.reduce_constr env sigma r c + +let () = + define "reduce_constr_in_env" + (local_env @-> reduction @-> constr @-> tac constr) @@ fun ctx r c -> + Tac2core.pf_apply_in ctx @@ fun env sigma -> + Tac2tactics.reduce_constr env sigma r c let () = define "red" (ret reduction) @@ -838,10 +845,27 @@ let () = | Some sigma -> Proofview.Unsafe.tclEVARS sigma <*> return true | None -> return false +let () = define "infer_conv_in_env" (to_conv_pb @--> transparent_state @-> local_env @-> constr @-> constr @-> tac bool) @@ fun pb ts ctx c1 c2 -> + Tac2core.pf_apply_in ctx @@ fun env sigma -> + match Reductionops.infer_conv ~pb ~ts env sigma c1 c2 with + | Some sigma -> Proofview.Unsafe.tclEVARS sigma <*> return true + | None -> return false + let () = define "evarconv_unify" - (transparent_state @-> constr @-> constr @-> tac unit) - Tac2tactics.evarconv_unify + (transparent_state @-> constr @-> constr @-> tac unit) @@ fun state c1 c2 -> + (* XXX pf_apply instead of enter (ie expect focused goal or 0 goals) *) + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + Tactics.evarconv_unify ~state env sigma CONV c1 c2 + end + +let () = + define "evarconv_unify_in_env" + (to_conv_pb @--> transparent_state @-> local_env @-> constr @-> constr @-> tac unit) @@ fun pb state ctx c1 c2 -> + Tac2core.pf_apply_in ctx @@ fun env sigma -> + Tactics.evarconv_unify ~state env sigma pb c1 c2 let () = define "congruence" diff --git a/plugins/ltac2/tac2tactics.ml b/plugins/ltac2/tac2tactics.ml index 23ca11cb2e29..d0fd48d5e9aa 100644 --- a/plugins/ltac2/tac2tactics.ml +++ b/plugins/ltac2/tac2tactics.ml @@ -260,13 +260,11 @@ let reduce_in red cl = let cl = mk_clause cl in Tactics.reduce red cl -let reduce_constr red c = - Tac2core.pf_apply begin fun env sigma -> - let (redfun, _) = Redexpr.reduction_of_red_expr env red in - let (sigma, ans) = redfun env sigma c in - Proofview.Unsafe.tclEVARS sigma >>= fun () -> - Proofview.tclUNIT ans - end +let reduce_constr env sigma red c = + let (redfun, _) = Redexpr.reduction_of_red_expr env red in + let (sigma, ans) = redfun env sigma c in + Proofview.Unsafe.tclEVARS sigma >>= fun () -> + Proofview.tclUNIT ans let simpl flags where = Proofview.Monad.map @@ -394,8 +392,6 @@ let current_transparent_state () = let state = Conv_oracle.get_transp_state (Environ.oracle env) in Proofview.tclUNIT state -let evarconv_unify state x y = Tactics.evarconv_unify ~state x y - (** Inversion *) let inversion knd arg pat ids = diff --git a/plugins/ltac2/tac2tactics.mli b/plugins/ltac2/tac2tactics.mli index 6854b4058394..f827570c73c4 100644 --- a/plugins/ltac2/tac2tactics.mli +++ b/plugins/ltac2/tac2tactics.mli @@ -76,7 +76,7 @@ val letin_pat_tac : evars_flag -> (bool * intro_pattern_naming) option -> val reduce_in : Redexpr.red_expr -> clause -> unit tactic -val reduce_constr : Redexpr.red_expr -> constr -> constr tactic +val reduce_constr : Environ.env -> Evd.evar_map -> Redexpr.red_expr -> constr -> constr tactic val simpl : Tac2types.red_flag -> Tac2types.red_context -> Redexpr.red_expr tactic @@ -120,8 +120,6 @@ val contradiction : constr_with_bindings option -> unit tactic val current_transparent_state : unit -> TransparentState.t tactic -val evarconv_unify : TransparentState.t -> constr -> constr -> unit tactic - (** Internal *) val mk_intro_pattern : intro_pattern -> Tactypes.intro_pattern diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 6b8b7133f1be..612545d68deb 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3185,18 +3185,14 @@ let unify ?(state=TransparentState.full) x y = Proofview.tclZERO ~info (PretypeError (env, sigma, CannotUnify (x, y, None))) end -let evarconv_unify ?(state=TransparentState.full) ?(with_ho=true) x y = - Proofview.Goal.enter begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in +let evarconv_unify ?(state=TransparentState.full) ?(with_ho=true) env sigma pb x y = try let flags = Evarconv.default_flags_of state in - let sigma = Evarconv.unify ~flags ~with_ho env sigma Conversion.CONV x y in + let sigma = Evarconv.unify ~flags ~with_ho env sigma pb x y in Proofview.Unsafe.tclEVARS sigma with e when noncritical e -> let e, info = Exninfo.capture e in Proofview.tclZERO ~info (PretypeError (env, sigma, CannotUnify (x, y, None))) - end (** [tclWRAPFINALLY before tac finally] runs [before] before each entry-point of [tac] and passes the result of [before] to diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 71bbd581564e..e2b914c2f2d2 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -658,11 +658,14 @@ val constr_eq : strict:bool -> constr -> constr -> unit Proofview.tactic (** Legacy unification. Use [evarconv_unify] instead. *) val unify : ?state:TransparentState.t -> constr -> constr -> unit Proofview.tactic -(** [evarconv_unify ?state ?with_ho x y] unifies [x] and [y], instantiating evars and adding universe constraints - as needed. Fails if [x] and [y] are not unifiable. +(** [evarconv_unify ?state ?with_ho env sigma pb x y] unifies [x] and [y], + instantiating evars and adding universe constraints as needed. + Fails if [x] and [y] are not unifiable. + - [pb]: infer [x <= y] or [x == y]. - [state]: transparency state to use (defaults to [TransparentState.full]). - [with_ho]: whether to use higher order unification (defaults to [true]). *) -val evarconv_unify : ?state:TransparentState.t -> ?with_ho:bool -> constr -> constr -> unit Proofview.tactic +val evarconv_unify : ?state:TransparentState.t -> ?with_ho:bool -> + env -> evar_map -> Conversion.conv_pb -> constr -> constr -> unit Proofview.tactic val specialize_eqs : Id.t -> unit Proofview.tactic diff --git a/theories/Ltac2/Constr.v b/theories/Ltac2/Constr.v index cea95bf4ff0c..b734f13c5a9a 100644 --- a/theories/Ltac2/Constr.v +++ b/theories/Ltac2/Constr.v @@ -39,6 +39,18 @@ Ltac2 @ external type : binder -> constr := "rocq-runtime.plugins.ltac2" "constr Ltac2 @ external relevance : binder -> relevance := "rocq-runtime.plugins.ltac2" "constr_binder_relevance". (** Retrieve the relevance of a binder. *) +Module UnsafeEnv. + (** Early declaration, see [Relevance.UnsafeEnv]. *) + Local Ltac2 @external relevance_of_type_in_env : env -> constr -> relevance + := "rocq-runtime.plugins.ltac2" "relevance_of_type_in_env". + + (** From arguments [Γ] [na] [t] produces the binder for [na : t], + retyping [t] in [Γ] to get its relevance. *) + Ltac2 make_in_ctx (ctx : env) (na : ident option) (t : constr) : binder := + let r := relevance_of_type_in_env ctx t in + Constr.Binder.unsafe_make na r t. +End UnsafeEnv. + End Binder. Module Relevance. @@ -64,6 +76,22 @@ Module Relevance. Ltac2 @external of_sort : sort -> t := "rocq-runtime.plugins.ltac2" "constr_relevance_of_sort". + Module UnsafeEnv. + + (** From arguments [Γ] and [c], if [c] is a valid term in [Γ] return its relevance as a term + (faster than retyping but not quite constant time). + Does not check that [c] is a valid term in [Γ]. *) + Ltac2 @external relevance_of_term_in_env : env -> constr -> t + := "rocq-runtime.plugins.ltac2" "relevance_of_term_in_env". + + (** From arguments [Γ] and [c], if [c] is a valid type in [Γ] return its relevance as a type + (by retyping). + Does not check that [c] is a valid type in [Γ]. *) + Ltac2 @external relevance_of_type_in_env : env -> constr -> t + := "rocq-runtime.plugins.ltac2" "relevance_of_type_in_env". + + End UnsafeEnv. + End Relevance. Module Unsafe. diff --git a/theories/Ltac2/Judge.v b/theories/Ltac2/Judge.v index 5c850dc0e501..eba5c41c592c 100644 --- a/theories/Ltac2/Judge.v +++ b/theories/Ltac2/Judge.v @@ -104,3 +104,53 @@ Ltac2 @external pretype_in_expecting : Constr.Pretype.Flags.t -> preterm -> type (** Print the given environment. Named and local variables are not distinguished. *) Ltac2 @external message_of_env : env -> message := "rocq-runtime.plugins.ltac2" "message_of_env". + +Module UnsafeEnv. +(** Functions in this module may be unsafe in two ways: + - The function expectes invariants on the arguments to be true but does not check them. + Typically [termj] does not check that its arguments are related. + - Calling the function is safe, but combining it with safe functions is not. + Typically [term_of_termj] is safe, but calling [Std.eval_cbv] on the result is not safe. + *) + + (** From argument [Γ ⊢ c : t] return [c]. *) + Ltac2 @external term_of_termj : termj -> constr + := "rocq-runtime.plugins.ltac2" "term_of_termj". + + (** From argument [Γ ⊢ t : s] return [t]. *) + Ltac2 @external type_of_typej : typej -> constr + := "rocq-runtime.plugins.ltac2" "type_of_typej". + + (** From arguments [Γ] [t] and [s] return [Γ ⊢ t : s] without checking anything. *) + Ltac2 @external typej : env -> constr -> sort -> typej + := "rocq-runtime.plugins.ltac2" "unsafe_typej". + + (** From arguments [c] and [Γ ⊢ t : s] return [Γ ⊢ c : t] without checking anything. *) + Ltac2 @external termj : constr -> typej -> termj + := "rocq-runtime.plugins.ltac2" "unsafe_termj". + + (** From arguments [Γ] [id] [t] and [r], produces [Γ, id : t] + assuming [t] has relevance [r]. + Throws if [id] is already bound in [Γ]. + Does not check anything else (e.g. that [t] is valid or has relevance [r] in [Γ]). *) + Ltac2 @external push_named_assum : env -> ident -> constr -> Constr.Relevance.t -> env + := "rocq-runtime.plugins.ltac2" "unsafe_push_named_assum". + + (** From arguments [Γ] [id] [c] [t] and [r], produces [Γ, id := c : t] + assuming [t] has relevance [r]. + Throws if [id] is already bound in [Γ]. + Does not check anything else. *) + Ltac2 @external push_named_def : env -> ident -> constr -> constr -> Constr.Relevance.t -> env + := "rocq-runtime.plugins.ltac2" "unsafe_push_named_def". + + (** Produces the [binder] corresponding to a type judgement and a name. + + Safe to call, but [binder] does not retain context information + so using the resulting value with safe APIs + (eg [Std.eval_hnf (Constr.Binder.type (of_typej ...))]) + is not safe. *) + Ltac2 binder_of_typej (na : ident option) (j : typej) : binder := + Constr.Binder.unsafe_make na (Constr.Relevance.of_sort (sort_of_typej j)) (type_of_typej j). + + +End UnsafeEnv. diff --git a/theories/Ltac2/Message.v b/theories/Ltac2/Message.v index aea63cf373e1..c8713a06fcc0 100644 --- a/theories/Ltac2/Message.v +++ b/theories/Ltac2/Message.v @@ -81,6 +81,12 @@ Ltac2 @external hovbox : int -> message -> message := "rocq-runtime.plugins.ltac on the line (see "Printing Width" option). The [int] is added to the indentation when splitting the line. *) +Module UnsafeEnv. + (** Print the given term in the given environment (does not print the environment). *) + Ltac2 @external message_of_constr_in_env : env -> constr -> message + := "rocq-runtime.plugins.ltac2" "message_of_constr_in_env". +End UnsafeEnv. + Module Format. (** Only for internal use. *) diff --git a/theories/Ltac2/Std.v b/theories/Ltac2/Std.v index 38f8f2d790e7..cc0ce9651341 100644 --- a/theories/Ltac2/Std.v +++ b/theories/Ltac2/Std.v @@ -394,3 +394,12 @@ Ltac2 @ external simple_congruence : int option -> constr list option -> unit := Ltac2 @external f_equal : unit -> unit := "rocq-runtime.plugins.ltac2" "f_equal". + +Module UnsafeEnv. + + (** [eval_in_env Γ red c] reduces [c] according to [red] in environment [Γ]. + Does not check that [c] or [red] are valid in [Γ]. *) + Ltac2 @external eval_in_env : env -> Std.Red.t -> constr -> constr + := "rocq-runtime.plugins.ltac2" "reduce_constr_in_env". + +End UnsafeEnv. diff --git a/theories/Ltac2/Unification.v b/theories/Ltac2/Unification.v index 333f5eac724d..6ef3d6a3405c 100644 --- a/theories/Ltac2/Unification.v +++ b/theories/Ltac2/Unification.v @@ -64,3 +64,26 @@ Ltac2 unify_with_current_ts : constr -> constr -> unit := fun c1 c2 => (** [solve_constraints ()] solves any delayed unification constraints. *) Ltac2 @external solve_constraints : unit -> unit := "rocq-runtime.plugins.ltac2" "solve_constraints". + +Module UnsafeEnv. + + (** [conv_in_env] returns true if both terms are convertible in the given environment, + in which case it updates the proof state with the universes constraints + required for the terms to be convertible. + It returns false if the terms are not convertible. + It fails if there is more than one goal under focus. + + [conv_in_env] is parametrised by: + - Unification.conv_flag which controls if conversion is done up to cumulativity or not + - TransparentState.t which controls which constants get unfolded during conversion + *) + Ltac2 @external conv_in_env : Unification.conv_flag -> TransparentState.t -> env -> constr -> constr -> bool + := "rocq-runtime.plugins.ltac2" "infer_conv_in_env". + + (** [unify_in_env pb ts ctx c1 c2] unifies [c1] and [c2] in [ctx] (using Evarconv unification), + which may have the effect of instantiating evars. + If the [c1] and [c2] cannot be unified, an [Internal] exception is raised. *) + Ltac2 @external unify_in_env : Unification.conv_flag -> TransparentState.t -> env -> constr -> constr -> unit + := "rocq-runtime.plugins.ltac2" "evarconv_unify_in_env". + +End UnsafeEnv. From ab1a21da4c3db0d65d5de658e03e0255d30573a1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 18 Feb 2026 16:15:19 +0100 Subject: [PATCH 6/7] add tests for ltac2 local env APIs --- test-suite/ltac2/HOAS.v | 110 +++++++++++++++++++++++++++++++++ test-suite/ltac2/unif_in_env.v | 48 ++++++++++++++ 2 files changed, 158 insertions(+) create mode 100644 test-suite/ltac2/HOAS.v create mode 100644 test-suite/ltac2/unif_in_env.v diff --git a/test-suite/ltac2/HOAS.v b/test-suite/ltac2/HOAS.v new file mode 100644 index 000000000000..878ce6da0aa4 --- /dev/null +++ b/test-suite/ltac2/HOAS.v @@ -0,0 +1,110 @@ +From Ltac2 Require Import Ltac2. +From Ltac2 Require Import Judge Sort. + +Ltac2 mkProdj (id:ident) (dom : typej) (codom : termj -> typej) := + let codom_ctx := push_named_assum id dom in + let codomj := codom (hypj id codom_ctx) in + (* XXX should assert that codomj has compatible context with dom to be safe *) + let codom := Constr.Unsafe.subst_vars [id] (UnsafeEnv.type_of_typej codomj) in + let r := Constr.Relevance.of_sort (sort_of_typej dom) in + let bnd := Constr.Binder.unsafe_make (Some id) r (UnsafeEnv.type_of_typej dom) in + let c := Constr.Unsafe.make (Constr.Unsafe.Prod bnd codom) in + UnsafeEnv.typej (env_of_typej dom) c (Sort.sort_of_product (sort_of_typej dom) (sort_of_typej codomj)). + +#[warnings="-ltac2-notation-for-abbreviation"] +Ltac2 Notation oflags := Constr.Pretype.Flags.open_constr_flags_no_tc. + +(* forall (A:Set) (x:A) (e:x = x), e = eq_refl + (term construction with a relatively high amout of dependency on introduced variables) *) +Ltac2 Eval + let ctx := Control.global_env() in + let c : typej := + mkProdj @A (pretype_type_judge oflags ctx preterm:(Set)) (fun a => + mkProdj @x (termj_is_typej a) (fun x => + let xc := UnsafeEnv.term_of_termj x in + let refl_typ := pretype_type_judge oflags (env_of_termj x) preterm:($xc = $xc) in + mkProdj @e refl_typ (fun e => + (* NB: because we are using named and not rel, refl_typ is still valid in the extended ctx *) + let ec := UnsafeEnv.term_of_termj e in + let refl_typc := UnsafeEnv.type_of_typej refl_typ in + pretype_type_judge oflags (env_of_termj e) preterm:(@eq $refl_typc $ec eq_refl)))) + in + c. + +(** unsafe HOAS (manual ctx manipulation) *) +Ltac2 mkProd (ctx : env) (id:ident) (dom : constr) (codom : env -> constr -> constr) := + let domr := Constr.Relevance.UnsafeEnv.relevance_of_type_in_env ctx dom in + let codom_ctx := UnsafeEnv.push_named_assum ctx id dom domr in + let codom := codom codom_ctx (Constr.Unsafe.make (Constr.Unsafe.Var id)) in + let codom := Constr.Unsafe.subst_vars [id] codom in + Constr.Unsafe.make (Constr.Unsafe.Prod (Constr.Binder.unsafe_make (Some id) domr dom) codom). + +Ltac2 pretype_in_env flags ctx c := + let j := pretype_judge flags ctx c in + UnsafeEnv.term_of_termj j. + +(* XXX "preterm" is at level 8 but we want to accept top level *) +Ltac2 Notation "open_constr_in_env:(" ctx(tactic) "|-" x(preterm) ")" := + pretype_in_env Constr.Pretype.Flags.open_constr_flags_no_tc ctx x. + +(* forall (A:Set) (x:A) (e:x = x), e = eq_refl + (term construction with a relatively high amout of dependency on introduced variables) *) +Ltac2 Eval + let env := Control.global_env() in + let c := + mkProd env @A 'Set (fun env a => + mkProd env @x a (fun env x => + let refl_typ := open_constr_in_env:(env |- ($x = $x)) in + mkProd env @e refl_typ (fun env e => + (* NB: because we are using named and not rel, refl_typ is still valid in the extended env *) + open_constr_in_env:(env |- (@eq $refl_typ $e eq_refl))))) + in + Control.assert_true (Constr.equal c '(forall (A:Set) (x:A) (e:x = x), e = eq_refl)); + let _ := Constr.type c in + (). + +(* forall x:nat, (x = x) = (x = x) + demonstrates how the locally bound variable can be referred to in terms *) +Ltac2 Eval + let env := Control.global_env() in + let c := + mkProd env @x 'nat (fun env x => + (* we can refer to x as any of [x], [&x] and [$x] + (not sure how reliable bare [x] is) *) + let c1 := open_constr_in_env:(env |- (&x = x)) in + let c2 := open_constr_in_env:(env |- (&x = $x)) in + open_constr_in_env:(env |- ($c1 = $c2))) + in + Control.assert_true (Constr.equal c '(forall x:nat, (x = x) = (x = x))). + +(* forall x:nat, 2 + x = S (S x) + with the RHS constructed by reducing the LHS in the extended context *) +Ltac2 Eval + let env := Control.global_env() in + let c := + mkProd env @x 'nat (fun env x => + let y := open_constr_in_env:(env |- (2 + $x)) in + let y_reduced := Std.UnsafeEnv.eval_in_env env (Std.Red.simpl RedFlags.all None) y in + (* 'eq is '(@eq _) which produces a type evar with empty context *) + open_constr_in_env:(env |- ($y = $y_reduced))) + in + Control.assert_true (Constr.equal c '(forall x, 2 + x = S (S x))); + let _ := Constr.type c in + (). + +Ltac2 mkLetIn (ctx : env) (id:ident) (value : constr) (typ : constr) (body : env -> constr -> constr) := + let r := Constr.Relevance.UnsafeEnv.relevance_of_term_in_env ctx value in + let body_ctx := UnsafeEnv.push_named_def ctx id value typ r in + let body := body body_ctx (Constr.Unsafe.make (Constr.Unsafe.Var id)) in + let body := Constr.Unsafe.subst_vars [id] body in + Constr.Unsafe.make (Constr.Unsafe.LetIn (Constr.Binder.unsafe_make (Some id) r typ) value body). + +Ltac2 Eval + let env := Control.global_env() in + let c := + mkLetIn env @x '3 'nat (fun env x => + open_constr_in_env:(env |- (eq_refl : $x = 3))) + in + Control.assert_true (Constr.equal c '(let x := 3 in eq_refl : x = 3)); + let _ := Constr.type c in + (). diff --git a/test-suite/ltac2/unif_in_env.v b/test-suite/ltac2/unif_in_env.v new file mode 100644 index 000000000000..54a7a727341d --- /dev/null +++ b/test-suite/ltac2/unif_in_env.v @@ -0,0 +1,48 @@ +From Ltac2 Require Import Ltac2. +From Ltac2 Require Import Judge Unification. + +Ltac2 pretype_in_env flags ctx c := + let j := pretype_judge flags ctx c in + UnsafeEnv.term_of_termj j. + +(* XXX "preterm" is at level 8 but we want to accept top level *) +Ltac2 Notation "open_constr_in_env:(" ctx(tactic) "|-" x(preterm) ")" := + pretype_in_env Constr.Pretype.Flags.open_constr_flags_no_tc ctx x. + +Ltac2 conv_in ctx c1 c2 := UnsafeEnv.conv_in_env Unification.CONV TransparentState.full ctx c1 c2. + +Ltac2 unify_in ctx c1 c2 := + match Control.case (fun () => UnsafeEnv.unify_in_env Unification.CONV TransparentState.full ctx c1 c2) with + | Val _ => true + | Err _ => false + end. + +Ltac2 mkVar x := Constr.Unsafe.make (Constr.Unsafe.Var x). + +Ltac2 Eval + let ctx := Control.global_env() in + let a := mkVar @A in + let mk t r := + let ctx := UnsafeEnv.push_named_assum ctx @A t Constr.Binder.Relevant in + let ctx := UnsafeEnv.push_named_assum ctx @x a r in + let ctx := UnsafeEnv.push_named_assum ctx @y a r in + ctx + in + let ctx1 := mk 'Prop Constr.Binder.Relevant in + let ctx2 := mk 'SProp Constr.Binder.Irrelevant in + Control.assert_false (conv_in ctx1 (mkVar @x) (mkVar @y)); + Control.assert_true (conv_in ctx2 (mkVar @x) (mkVar @y)); + Control.assert_false (unify_in ctx1 (mkVar @x) (mkVar @y)); + Control.assert_true (unify_in ctx2 (mkVar @x) (mkVar @y)); + (). + +Ltac2 Eval + let ctx := Control.global_env() in + let ctx := push_named_def @x (pretype_judge Constr.Pretype.Flags.open_constr_flags_no_tc ctx preterm:(3)) in + Control.assert_true (conv_in ctx (mkVar @x) '3); + Control.assert_false (conv_in ctx (mkVar @x) '4); + Control.assert_true (unify_in ctx (mkVar @x) '3); + Control.assert_false (unify_in ctx (mkVar @x) '4); + Control.assert_false (conv_in ctx (mkVar @x) '(S _)); + Control.assert_true (unify_in ctx (mkVar @x) '(S _)); + (). From e09aa881a1267a043f265f0d647131c45a019495 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Fri, 20 Feb 2026 15:42:11 +0100 Subject: [PATCH 7/7] changelog --- doc/changelog/06-Ltac2-language/21654-ltac2-ctx-Added.rst | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 doc/changelog/06-Ltac2-language/21654-ltac2-ctx-Added.rst diff --git a/doc/changelog/06-Ltac2-language/21654-ltac2-ctx-Added.rst b/doc/changelog/06-Ltac2-language/21654-ltac2-ctx-Added.rst new file mode 100644 index 000000000000..9956f94d154c --- /dev/null +++ b/doc/changelog/06-Ltac2-language/21654-ltac2-ctx-Added.rst @@ -0,0 +1,5 @@ +- **Added:** + APIs to manipulate local environments (type `Ltac2.Init.env`), + in particular in new file `Ltac2.Judge` terms carrying their context + (`#21654 `_, + by Gaëtan Gilbert).