Merge pull request #942 from mattam82/sort-poly-flags

Adapt to rocq-prover/rocq#21419

Author: ppedrot

src/rocq_elpi_HOAS.ml

@@ -3088,8 +3088,7 @@ let comInductive_interp_mutual_inductive_constr ~cumulative ~poly ~template ~fin
 [%%else]
 let comInductive_interp_mutual_inductive_constr ~cumulative ~poly ~template ~finite ~ctx_params ~env_ar_params =
   let flags = {
-    ComInductive.poly;
-    cumulative;
+    ComInductive.poly = PolyFlags.make ~univ_poly:poly ~cumulative ~collapse_sort_variables:true;
     template = Some false;
     finite;
     mode = None;

src/rocq_elpi_arg_HOAS.ml

@@ -242,6 +242,14 @@ let univpoly_of ~poly ~cumulative =
   | true, false -> Poly
   | false, _ -> Mono
 
+[%%if coq = "9.0" || coq = "9.1"]
+let univpoly_of_flags flags =
+  univpoly_of ~poly:flags.ComInductive.poly ~cumulative:flags.ComInductive.cumulative
+[%%else]
+let univpoly_of_flags flags =
+  univpoly_of ~poly:(PolyFlags.univ_poly flags.ComInductive.poly) ~cumulative:(PolyFlags.cumulative flags.poly)
+[%%endif]
+
 let of_coq_inductive_definition id =
   let open Vernacentries.Preprocessed_Mind_decl in
   let { flags; udecl; typing_flags; private_ind; uniform; inductives } = id in
@@ -254,7 +262,7 @@ let of_coq_inductive_definition id =
         List.map (function (Vernacexpr.(_,NoCoercion,NoInstance),c) -> c
           | _ -> CErrors.user_err Pp.(str "coercion and instance flags not supported"))
           constructors in
-  let { ComInductive.template; cumulative; poly; finite } = flags in
+  let { ComInductive.template; finite } = flags in
   if template <> None then nYI "raw template polymorphic inductives";
   if udecl <> None then nYI "raw universe polymorphic inductives with universe declaration";
   {
@@ -264,7 +272,7 @@ let of_coq_inductive_definition id =
     non_uniform_parameters;
     arity;
     constructors;
-    univpoly = univpoly_of ~poly ~cumulative
+    univpoly = univpoly_of_flags flags
   }
 
 let of_coq_record_definition id =
@@ -279,7 +287,7 @@ let of_coq_record_definition id =
     match sort.CAst.v with
     | Constrexpr.CSort s -> s
     | _ -> CErrors.user_err ?loc:sort.CAst.loc Pp.(str "only explicits sorts are supported")) in
-  let { ComInductive.template; cumulative; poly; finite } = flags in
+  let { ComInductive.template; finite } = flags in
   if template <> None then nYI "raw template polymorphic inductives";
   if udecl <> None then nYI "raw universe polymorphic inductives with universe declaration";
   {
@@ -288,7 +296,7 @@ let of_coq_record_definition id =
     sort;
     constructor = Some idbuild.v;
     fields = cfs;
-    univpoly = univpoly_of ~poly ~cumulative
+    univpoly = univpoly_of_flags flags
   } 
 
 let intern_record_decl glob_sign (it : raw_record_decl) = glob_sign, it
@@ -461,6 +469,16 @@ let raw_decl_name_to_glob name =
 
 let interp_red_expr = Redexpr.interp_redexp_no_ltac
 
+[%%if coq = "9.0" || coq = "9.1"]
+let interp_definition ~program_mode poly = ComDefinition.interp_definition ~program_mode
+let interp_assumption ~program_mode poly = ComAssumption.interp_assumption ~program_mode
+[%%else]
+let interp_definition ~program_mode poly =
+  ComDefinition.interp_definition ~program_mode ~poly:(PolyFlags.of_univ_poly poly)
+let interp_assumption ~program_mode poly =
+  ComAssumption.interp_assumption ~program_mode ~poly:(PolyFlags.of_univ_poly poly)
+[%%endif]
+
 let raw_constant_decl_to_constr ~depth coq_ctx state { name; typ = (bl,typ); body; red; udecl; atts } =
   let env = coq_ctx.env in
   let poly =
@@ -482,7 +500,7 @@ let raw_constant_decl_to_constr ~depth coq_ctx state { name; typ = (bl,typ); bod
   | Some body, _ ->
       let sigma, red = option_map_acc (interp_red_expr env) sigma red in
       let sigma, (body, typ), impargs =
-        ComDefinition.interp_definition ~program_mode:false
+        interp_definition ~program_mode:false poly
           env sigma Constrintern.empty_internalization_env bl red body typ
       in
       let state, gls0 = set_current_sigma ~depth state sigma in
@@ -491,7 +509,7 @@ let raw_constant_decl_to_constr ~depth coq_ctx state { name; typ = (bl,typ); bod
   | None, Some typ ->
       assert(red = None);
       let sigma, typ, impargs =
-        ComAssumption.interp_assumption ~program_mode:false
+        interp_assumption ~program_mode:false poly
           env sigma Constrintern.empty_internalization_env bl typ in
       let state, gls0 = set_current_sigma ~depth state sigma in
       state, udecl, typ, None, gls0

src/rocq_elpi_builtins.ml

@@ -359,13 +359,15 @@ let empty_ctxset = Univ.ContextSet.empty
 let univ_csts_to_list = Univ.Constraints.elements
 let univs_of_csts = UState.constraints
 let ucsts_filter = Univ.Constraints.filter
+let default_polyflags = false
 [%%else]
 let evd_merge_sort_context_set rigid = Evd.merge_sort_context_set rigid QGraph.Internal
 let check_univ_decl =  UState.check_univ_decl
 let empty_ctxset = PConstraints.ContextSet.empty
 let univ_csts_to_list = Univ.UnivConstraints.elements
 let univs_of_csts x = PConstraints.univs @@ UState.constraints x
 let ucsts_filter = Univ.UnivConstraints.filter
+let default_polyflags = PolyFlags.default
 [%%endif]
 
 let handle_uinst_option_for_inductive ~depth options i state =
@@ -987,6 +989,13 @@ let get_entry_context = function
 | UState.Monomorphic_entry x, _ -> x
 | _ -> Univ.ContextSet.empty
 
+[%%if coq = "9.0" || coq = "9.1"]
+let make_polyflags poly cumul = poly
+[%%else]
+let make_polyflags poly cumul =
+  PolyFlags.make ~univ_poly:poly ~cumulative:cumul ~collapse_sort_variables:true
+[%%endif]
+
 let declare_definition _ using ~cinfo ~info ~opaque ~body sigma =
   let using = Option.map Proof_using.using_from_string using in
   let (kn, uctx) = Declare.declare_definition_full ~cinfo ~info ~opaque ~body ?using sigma in
@@ -1002,7 +1011,7 @@ let add_axiom_or_variable api id ty local_bkind options state =
     err Pp.(str api ++ str": unsupported attribute @udecl-cumul! or @univpoly-cumul!");
   if poly && Option.has_some local_bkind then
     err Pp.(str api ++ str": section variables cannot be universe polymorphic");
-  let univs = check_univ_decl (Evd.ustate sigma) udecl ~poly in
+  let univs = check_univ_decl (Evd.ustate sigma) udecl ~poly:(make_polyflags poly cumul) in
   let kind = Decls.Logical in
   let impargs = [] in
   let loc = to_coq_loc @@ State.get Rocq_elpi_builtins_synterp.invocation_site_loc state in
@@ -2266,7 +2275,7 @@ Supported attributes:
        let hook = Declare.Hook.make (fun { Declare.Hook.S.uctx = x } -> uctx := Some (UState.context_set x)) in
        (* End hack *)
 
-       let info = Declare.Info.make ~scope ~kind ~poly ~udecl ~hook () in
+       let info = Declare.Info.make ~scope ~kind ~poly:(make_polyflags poly cumul) ~udecl ~hook () in
 
        let used =
          Univ.Level.Set.union
@@ -4062,7 +4071,7 @@ Supported attributes:
             let pv =
               let vernac_state = Vernacstate.freeze_full_state () in
               try
-                let rc = apply_proof ~name:(Id.of_string "elpi") ~poly:false proof_context.env focused_tac pv in
+                let rc = apply_proof ~name:(Id.of_string "elpi") ~poly:default_polyflags proof_context.env focused_tac pv in
                 let pstate = Vernacstate.Stm.pstate (Vernacstate.freeze_full_state ()) in
                 let vernac_state = Vernacstate.Stm.set_pstate vernac_state pstate in
                 Vernacstate.unfreeze_full_state vernac_state;

src/rocq_elpi_vernacular.ml

@@ -748,7 +748,6 @@ let execution proof p loc0 args loc1 ?loc ~atts () =
   | _ -> Vernactypes.vtdefault (fun () -> Interp.run_program ~loc p ~atts ~syndata args)
 [%%else]
 let classifier proof _loc0 _args _loc1 ~atts =
-  let open Vernac_classifier in
   match proof with
   | Some (Begin None) -> Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]))
   | Some (Begin (Some a)) when has_att a atts -> Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]))