rocq-prover · coqbot-app · Apr 7, 2024 · Dec 19, 2023 · Mar 22, 2024 · Mar 22, 2024
@@ -392,6 +392,7 @@ let understand_state = function
   | "program" -> "vtmodifyprogram", ["pm"]
   | "declare_program" -> "vtdeclareprogram", ["pm"]
   | "program_interactive" -> "vtopenproofprogram", ["pm"]
+  | "opaque_access" -> "vtopaqueaccess", ["opaque_access"]
   | s -> fatal ("unsupported state specifier: " ^ s)
 
 let rec pr_named_arguments fmt = function

diff --git a/dev/ci/user-overlays/18422-SkySkimmer-indirect.sh b/dev/ci/user-overlays/18422-SkySkimmer-indirect.sh
@@ -0,0 +1,15 @@
+overlay equations https://github.com/SkySkimmer/Coq-Equations indirect 18422
+
+overlay paramcoq https://github.com/SkySkimmer/paramcoq indirect 18422
+
+overlay simple_io https://github.com/SkySkimmer/coq-simple-io indirect 18422
+
+overlay quickchick https://github.com/SkySkimmer/QuickChick indirect 18422
+
+overlay vscoq https://github.com/SkySkimmer/vscoq indirect 18422
+
+overlay serapi https://github.com/SkySkimmer/coq-serapi indirect 18422
+
+overlay coq_lsp https://github.com/SkySkimmer/coq-lsp indirect 18422
+
+overlay metacoq https://github.com/SkySkimmer/metacoq indirect 18422
@@ -167,14 +167,18 @@ END
  *
  * Simple_print contains simple_body_access, which shows how to look up
  * a global reference.
+ *
+ * It needs the ability to access the body of opaque constants, which is given by STATE opaque_access.
+ * This makes the expected type of the implementation be
+ * [opaque_access:Global.indirect_accessor -> unit] instead of [unit].
  *)
-VERNAC COMMAND EXTEND ExamplePrint CLASSIFIED AS QUERY
+VERNAC COMMAND EXTEND ExamplePrint CLASSIFIED AS QUERY STATE opaque_access
 | [ "MyPrint" reference(r) ] ->
-   {
+   { fun ~opaque_access ->
      let env = Global.env () in
      let sigma = Evd.from_env env in
      try
-       let t = Simple_print.simple_body_access (Nametab.global r) in
+       let t = Simple_print.simple_body_access ~opaque_access (Nametab.global r) in
        Feedback.msg_notice (Printer.pr_econstr_env env sigma t)
      with Failure s ->
        CErrors.user_err (str s)
@@ -193,10 +197,12 @@ END
  *
  * Inside of simple_body_access, note that it uses Global.env (),
  * which refreshes the environment before looking up the term.
+ *
+ * [![opaque_access]] is equivalent to [STATE opaque_access] but is specific to that parsing rule.
  *)
 VERNAC COMMAND EXTEND DefineLookup CLASSIFIED AS SIDEFF
-| #[ poly = Attributes.polymorphic ] [ "DefineLookup" ident(i) ":=" constr(e) ] ->
-   {
+| #[ poly = Attributes.polymorphic ] ![opaque_access] [ "DefineLookup" ident(i) ":=" constr(e) ] ->
+   { fun ~opaque_access ->
      let env = Global.env () in
      let sigma = Evd.from_env env in
      let (sigma, t) = Constrintern.interp_constr_evars env sigma e in
@@ -205,7 +211,7 @@ VERNAC COMMAND EXTEND DefineLookup CLASSIFIED AS SIDEFF
      Feedback.msg_notice (print r);
      let env = Global.env () in
      let sigma = Evd.from_env env in
-     let t = Simple_print.simple_body_access r in
+     let t = Simple_print.simple_body_access ~opaque_access r in
      let print t = strbrk "Found " ++ Printer.pr_econstr_env env sigma t in
      Feedback.msg_notice (print t)
    }

@@ -1,7 +1,7 @@
 (* A more advanced example of how to explore the structure of terms of
   type constr is given in the coq-dpdgraph plugin. *)
 
-let simple_body_access gref =
+let simple_body_access ~opaque_access gref =
   let open Names.GlobRef in
   match gref with
   | VarRef _ ->
@@ -12,7 +12,9 @@ let simple_body_access gref =
     failwith "constructors are not covered in this example"
   | ConstRef cst ->
     let cb = Environ.lookup_constant cst (Global.env()) in
-    match Global.body_of_constant_body Library.indirect_accessor cb with
+    (* most commands should not use body_of_constant_body and opaque accessors,
+       but for printing it's ok *)
+    match Global.body_of_constant_body opaque_access cb with
     | Some(e, _, _) -> EConstr.of_constr e
     | None -> failwith "This term has no value"
 
@@ -1 +1 @@
-val simple_body_access : Names.GlobRef.t -> EConstr.constr
+val simple_body_access : opaque_access:Global.indirect_accessor -> Names.GlobRef.t -> EConstr.constr
@@ -149,7 +149,7 @@ let force_proof access o = match access.access_proof o with
 | None -> CErrors.user_err Pp.(str "Cannot access opaque delayed proof")
 | Some (c, u) -> (c, u)
 
-let body_of_constant_body access env cb =
+let body_of_constant_body access cb =
   let open Declarations in
   match cb.const_body with
   | Undef _ | Primitive _ | Symbol _ ->
@@ -164,8 +164,6 @@ let body_of_constant_body access env cb =
     let c, u = force_proof access o in
     Some (c, u, Declareops.constant_polymorphic_context cb)
 
-let body_of_constant_body access ce = body_of_constant_body access (env ()) ce
-
 let body_of_constant access cst = body_of_constant_body access (lookup_constant cst)
 
 (** Operations on kernel names *)

@@ -290,31 +290,31 @@ and extract_mbody_spec : 'a. _ -> _ -> 'a generic_module_body -> _ =
    important: last to first ensures correct dependencies.
 *)
 
-let rec extract_structure env mp reso ~all = function
+let rec extract_structure access env mp reso ~all = function
   | [] -> []
   | (l,SFBconst cb) :: struc ->
       (try
          let sg = Evd.from_env env in
          let vl,recd,struc = factor_fix env sg l cb struc in
          let vc = Array.map (make_cst reso mp) vl in
-         let ms = extract_structure env mp reso ~all struc in
+         let ms = extract_structure access env mp reso ~all struc in
          let b = Array.exists Visit.needed_cst vc in
          if all || b then
            let d = extract_fixpoint env sg vc recd in
            if (not b) && (logical_decl d) then ms
            else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end
          else ms
        with Impossible ->
-         let ms = extract_structure env mp reso ~all struc in
+         let ms = extract_structure access env mp reso ~all struc in
          let c = make_cst reso mp l in
          let b = Visit.needed_cst c in
          if all || b then
-           let d = extract_constant env c cb in
+           let d = extract_constant access env c cb in
            if (not b) && (logical_decl d) then ms
            else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end
          else ms)
   | (l,SFBmind mib) :: struc ->
-      let ms = extract_structure env mp reso ~all struc in
+      let ms = extract_structure access env mp reso ~all struc in
       let mind = make_mind reso mp l in
       let b = Visit.needed_ind mind in
       if all || b then
@@ -324,44 +324,44 @@ let rec extract_structure env mp reso ~all = function
       else ms
   | (l, SFBrules rrb) :: struc ->
       let b = List.exists (fun (cst, _) -> Visit.needed_cst cst) rrb.rewrules_rules in
-      let ms = extract_structure env mp reso ~all struc in
+      let ms = extract_structure access env mp reso ~all struc in
       if all || b then begin
         List.iter (fun (cst, _) -> Table.add_symbol_rule (ConstRef cst) l) rrb.rewrules_rules;
         ms
       end else ms
   | (l,SFBmodule mb) :: struc ->
-      let ms = extract_structure env mp reso ~all struc in
+      let ms = extract_structure access env mp reso ~all struc in
       let mp = MPdot (mp,l) in
       let all' = all || Visit.needed_mp_all mp in
       if all' || Visit.needed_mp mp then
-        (l,SEmodule (extract_module env mp ~all:all' mb)) :: ms
+        (l,SEmodule (extract_module access env mp ~all:all' mb)) :: ms
       else ms
   | (l,SFBmodtype mtb) :: struc ->
-      let ms = extract_structure env mp reso ~all struc in
+      let ms = extract_structure access env mp reso ~all struc in
       let mp = MPdot (mp,l) in
       if all || Visit.needed_mp mp then
         (l,SEmodtype (extract_mbody_spec env mp mtb)) :: ms
       else ms
 
 (* From [module_expr] and [module_expression] to implementations *)
 
-and extract_mexpr env mp = function
+and extract_mexpr access env mp = function
   | MEwith _ -> assert false (* no 'with' syntax for modules *)
   | me when lang () != Ocaml || Table.is_extrcompute () ->
       (* In Haskell/Scheme, we expand everything.
          For now, we also extract everything, dead code will be removed later
          (see [Modutil.optimize_struct]. *)
       let sign, delta = expand_mexpr env mp me in
-      extract_msignature env mp delta ~all:true sign
+      extract_msignature access env mp delta ~all:true sign
   | MEident mp ->
       if is_modfile mp && not (modular ()) then error_MPfile_as_mod mp false;
       Visit.add_mp_all mp; Miniml.MEident mp
   | MEapply (me, arg) ->
-      Miniml.MEapply (extract_mexpr env mp me,
-                      extract_mexpr env mp (MEident arg))
+      Miniml.MEapply (extract_mexpr access env mp me,
+                      extract_mexpr access env mp (MEident arg))
 
-and extract_mexpression env mp mty = function
-  | MENoFunctor me -> extract_mexpr env mp me
+and extract_mexpression access env mp mty = function
+  | MENoFunctor me -> extract_mexpr access env mp me
   | MEMoreFunctor me ->
       let (mbid, mtb, mty) = match mty with
       | MoreFunctor (mbid, mtb, mty) -> (mbid, mtb, mty)
@@ -372,21 +372,21 @@ and extract_mexpression env mp mty = function
       Miniml.MEfunctor
         (mbid,
          extract_mbody_spec env mp1 mtb,
-         extract_mexpression env' mp mty me)
+         extract_mexpression access env' mp mty me)
 
-and extract_msignature env mp reso ~all = function
+and extract_msignature access env mp reso ~all = function
   | NoFunctor struc ->
       let env' = Modops.add_structure mp struc reso env in
-      Miniml.MEstruct (mp,extract_structure env' mp reso ~all struc)
+      Miniml.MEstruct (mp,extract_structure access env' mp reso ~all struc)
   | MoreFunctor (mbid, mtb, me) ->
       let mp1 = MPbound mbid in
       let env' = Modops.add_module_type mp1 mtb	env in
       Miniml.MEfunctor
         (mbid,
          extract_mbody_spec env mp1 mtb,
-         extract_msignature env' mp reso ~all me)
+         extract_msignature access env' mp reso ~all me)
 
-and extract_module env mp ~all mb =
+and extract_module access env mp ~all mb =
   (* A module has an empty [mod_expr] when :
      - it is a module variable (for instance X inside a Module F [X:SIG])
      - it is a module assumption (Declare Module).
@@ -395,14 +395,14 @@ and extract_module env mp ~all mb =
      moment we don't support this situation. *)
   let impl = match mb.mod_expr with
     | Abstract -> error_no_module_expr mp
-    | Algebraic me -> extract_mexpression env mp mb.mod_type me
+    | Algebraic me -> extract
10000
_mexpression access env mp mb.mod_type me
     | Struct sign ->
       (* This module has a signature, otherwise it would be FullStruct.
          We extract just the elements required by this signature. *)
       let () = add_labels mp mb.mod_type in
       let sign = Modops.annotate_struct_body sign mb.mod_type in
-      extract_msignature env mp mb.mod_delta ~all:false sign
-    | FullStruct -> extract_msignature env mp mb.mod_delta ~all mb.mod_type
+      extract_msignature access env mp mb.mod_delta ~all:false sign
+    | FullStruct -> extract_msignature access env mp mb.mod_delta ~all mb.mod_type
   in
   (* Slight optimization: for modules without explicit signatures
      ([FullStruct] case), we build the type out of the extracted
@@ -416,15 +416,15 @@ and extract_module env mp ~all mb =
   { ml_mod_expr = impl;
     ml_mod_type = typ }
 
-let mono_environment refs mpl =
+let mono_environment ~opaque_access refs mpl =
   Visit.reset ();
   List.iter Visit.add_ref refs;
   List.iter Visit.add_mp_all mpl;
   let env = Global.env () in
   let l = List.rev (environment_until None) in
   List.rev_map
     (fun (mp,struc) ->
-      mp, extract_structure env mp no_delta ~all:(Visit.needed_mp_all mp) struc)
+      mp, extract_structure opaque_access env mp no_delta ~all:(Visit.needed_mp_all mp) struc)
     l
 
 (**************************************)
@@ -625,24 +625,24 @@ let rec locate_ref = function
     extracting to a file with the command:
     \verb!Extraction "file"! [qualid1] ... [qualidn]. *)
 
-let full_extr f (refs,mps) =
+let full_extr opaque_access f (refs,mps) =
   init false false;
   List.iter (fun mp -> if is_modfile mp then error_MPfile_as_mod mp true) mps;
-  let struc = optimize_struct (refs,mps) (mono_environment refs mps) in
+  let struc = optimize_struct (refs,mps) (mono_environment ~opaque_access refs mps) in
   warns ();
   print_structure_to_file (mono_filename f) false struc;
   reset ()
 
-let full_extraction f lr =
-  full_extr f (locate_ref lr)
+let full_extraction ~opaque_access f lr =
+  full_extr opaque_access f (locate_ref lr)
 
 (*s Separate extraction is similar to recursive extraction, with the output
    decomposed in many files, one per Coq .v file *)
 
-let separate_extraction lr =
+let separate_extraction ~opaque_access lr =
   init true false;
   let refs,mps = locate_ref lr in
-  let struc = optimize_struct (refs,mps) (mono_environment refs mps) in
+  let struc = optimize_struct (refs,mps) (mono_environment ~opaque_access refs mps) in
   let () = List.iter (function
     | MPfile _, _ -> ()
     | (MPdot _ | MPbound _), _ ->
@@ -661,12 +661,12 @@ let separate_extraction lr =
 (*s Simple extraction in the Coq toplevel. The vernacular command
     is \verb!Extraction! [qualid]. *)
 
-let simple_extraction r =
+let simple_extraction ~opaque_access r =
   match locate_ref [r] with
-  | ([], [mp]) as p -> full_extr None p
+  | ([], [mp]) as p -> full_extr opaque_access None p
   | [r],[] ->
       init false false;
-      let struc = optimize_struct ([r],[]) (mono_environment [r] []) in
+      let struc = optimize_struct ([r],[]) (mono_environment ~opaque_access [r] []) in
       let d = get_decl_in_structure r struc in
       warns ();
       let flag =
@@ -682,7 +682,7 @@ let simple_extraction r =
 (*s (Recursive) Extraction of a library. The vernacular command is
   \verb!(Recursive) Extraction Library! [M]. *)
 
-let extraction_library is_rec CAst.{loc;v=m} =
+let extraction_library ~opaque_access is_rec CAst.{loc;v=m} =
   init true true;
   let dir_m =
     let q = qualid_of_ident m in
@@ -693,7 +693,7 @@ let extraction_library is_rec CAst.{loc;v=m} =
   let l = List.rev (environment_until (Some dir_m)) in
   let select l (mp,struc) =
     if Visit.needed_mp mp
-    then (mp, extract_structure env mp no_delta ~all:true struc) :: l
+    then (mp, extract_structure opaque_access env mp no_delta ~all:true struc) :: l
     else l
   in
   let struc = List.fold_left select [] l in
@@ -722,15 +722,15 @@ let flatten_structure struc =
   and flatten_elems l = List.flatten (List.map flatten_elem l)
   in flatten_elems (List.flatten (List.map snd struc))
 
-let structure_for_compute env sg c =
+let structure_for_compute ~opaque_access env sg c =
   init false false ~compute:true;
   let ast, mlt = Extraction.extract_constr env sg c in
   let ast = Mlutil.normalize ast in
   let refs = ref GlobRef.Set.empty in
   let add_ref r = refs := GlobRef.Set.add r !refs in
   let () = ast_iter_references add_ref add_ref add_ref ast in
   let refs = GlobRef.Set.elements !refs in
-  let struc = optimize_struct (refs,[]) (mono_environment refs []) in
+  let struc = optimize_struct (refs,[]) (mono_environment ~opaque_access refs []) in
   (flatten_structure struc), ast, mlt
 
 (* For the test-suite :
@@ -759,11 +759,11 @@ let compile f =
 let remove f =
   if Sys.file_exists f then Sys.remove f
 
-let extract_and_compile l =
+let extract_and_compile ~opaque_access l =
   if lang () != Ocaml then
     CErrors.user_err (Pp.str "This command only works with OCaml extraction");
   let f = Filename.temp_file "testextraction" ".ml" in
-  let () = full_extraction (Some f) l in
+  let () = full_extraction ~opaque_access (Some f) l in
   let () = compile f in
   let () = remove f; remove (f^"i") in
   let base = Filename.chop_suffix f ".ml" in

@@ -13,19 +13,19 @@
 open Names
 open Libnames
 
-val simple_extraction : qualid -> unit
-val full_extraction : string option -> qualid list -> unit
-val separate_extraction : qualid list -> unit
-val extraction_library : bool -> lident -> unit
+val simple_extraction : opaque_access:Global.indirect_accessor -> qualid -> unit
+val full_extraction : opaque_access:Global.indirect_accessor -> string option -> qualid list -> unit
+val separate_extraction : opaque_access:Global.indirect_accessor -> qualid list -> unit
+val extraction_library : opaque_access:Global.indirect_accessor -> bool -> lident -> unit
 
 (* For the test-suite : extraction to a temporary file + ocamlc on it *)
 
-val extract_and_compile : qualid list -> unit
+val extract_and_compile : opaque_access:Global.indirect_accessor -> qualid list -> unit
 
 (* For debug / external output via coqtop.byte + Drop : *)
 
 val mono_environment :
- GlobRef.t list -> ModPath.t list -> Miniml.ml_structure
+ opaque_access:Global.indirect_accessor -> GlobRef.t list -> ModPath.t list -> Miniml.ml_structure
 
 (* Used by the Relation Extraction plugin *)
 
@@ -35,7 +35,7 @@ val print_one_decl :
 (* Used by Extraction Compute *)
 
 val structure_for_compute :
-  Environ.env -> Evd.evar_map -> EConstr.t ->
+  opaque_access:Global.indirect_accessor -> Environ.env -> Evd.evar_map -> EConstr.t ->
     Miniml.ml_decl list * Miniml.ml_ast * Miniml.ml_type
 
 (* Show the extraction of the current ongoing proof *)
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		val simple_body_access : Names.GlobRef.t -> EConstr.constr
		val simple_body_access : opaque_access:Global.indirect_accessor -> Names.GlobRef.t -> EConstr.constr