Ltac2 local env APIs

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 <https://github.com/rocq-prover/rocq/pull/21654>`_,
+  by Gaëtan Gilbert).

doc/corelib/index-list.html.template

@@ -140,6 +140,7 @@ through the <tt>Require Import</tt> command.</p>
     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
@@ -157,6 +158,7 @@ through the <tt>Require Import</tt> command.</p>
     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

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)
@@ -694,6 +692,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
@@ -846,11 +848,32 @@ 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 "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 ->
   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
@@ -1028,6 +1051,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
@@ -1099,7 +1136,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

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. *)

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|])

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