Adapt to rocq-prover/rocq#21195 (Univ.Constraints -> UnivConstraints)

fixup optcomp

Fix overlay for elimination-constraints

Fix  overlay

Fix overlay, test on 9.1

Fix unused opens

Try to fix the weird issue with univ_binder_compat_820

Typo

Another unused open

Another try

Author: TDiazT

src/rocq_elpi_HOAS.ml

@@ -108,9 +108,13 @@ let constraint_eq u1 u2 =
   let open UnivProblem in
   ULe (u1, u2)
 
+[%%if coq = "9.0" || coq = "9.1"]
 let add_constraints state c = S.update (Option.get !pre_engine) state (fun ({ sigma } as x) ->
   { x with sigma = Evd.add_universe_constraints sigma c })
-    
+[%%else]
+let add_constraints state c = S.update (Option.get !pre_engine) state (fun ({ sigma } as x) ->
+  { x with sigma = Evd.add_constraints sigma c })
+[%%endif]
 let add_universe_constraint state c =
   let open UnivProblem in
   try add_constraints state (Set.singleton c)
@@ -204,23 +208,92 @@ let universe_level_variable =
   end
 }
 
-let universe_constraint : Univ.univ_constraint API.Conversion.t =
+[%%if coq = "9.0" || coq = "9.1"]
+type univ_cst = Univ.univ_constraint
+type univ_csts = Univ.Constraints.t
+type univ_ctx_set = Univ.ContextSet.t
+
+let univ_lt = Univ.Lt
+let univ_le = Univ.Le
+let univ_eq = Univ.Eq
+let univ_csts_of_list = Univ.Constraints.of_list
+let univ_csts_to_list = Univ.Constraints.elements
+let evd_merge_ctx_set rigid = Evd.merge_sort_context_set rigid
+let subst_univs_constraints = Univ.subst_univs_level_constraints
+let univs_of_csts = UVars.UContext.constraints
+let mk_universe_decl univdecl_extensible_instance univdecl_extensible_constraints univdecl_constraints univdecl_instance =
+  let open UState in
+  { univdecl_qualities = [];
+    univdecl_extensible_instance;
+    univdecl_extensible_qualities = false;
+    univdecl_extensible_constraints;
+    univdecl_constraints;
+    univdecl_instance}
+let default_univ_decl = UState.default_univ_decl
+let dest_udecl ({ UState.univdecl_instance ; univdecl_constraints } : UState.universe_decl) =
+  univdecl_instance, univdecl_constraints
+
+let universe_constraint : univ_cst API.Conversion.t =
   let open API.Conversion in let open API.AlgebraicData in declare {
   ty = TyName "univ-constraint";
   doc = "Constraint between two universes level variables";
   pp = (fun fmt _ -> Format.fprintf fmt "<todo>");
   constructors = [
     K("lt","",A(universe_level_variable,A(universe_level_variable,N)),
-      B (fun u1 u2 -> (u1,Univ.Lt,u2)),
+      B (fun u1 u2 -> (u1,univ_lt,u2)),
       M (fun ~ok ~ko -> function (l1,Univ.Lt,l2) -> ok l1 l2 | _ -> ko ()));
     K("le","",A(universe_level_variable,A(universe_level_variable,N)),
-      B (fun u1 u2 -> (u1,Univ.Le,u2)),
+      B (fun u1 u2 -> (u1,univ_le,u2)),
       M (fun ~ok ~ko -> function (l1,Univ.Le,l2) -> ok l1 l2 | _ -> ko ()));
     K("eq","",A(universe_level_variable,A(universe_level_variable,N)),
-      B (fun u1 u2 -> (u1,Univ.Eq,u2)),
+      B (fun u1 u2 -> (u1,univ_eq,u2)),
       M (fun ~ok ~ko -> function (l1,Univ.Eq,l2) -> ok l1 l2 | _ -> ko ()))
   ]
 } |> API.ContextualConversion.(!<)
+[%%else]
+type univ_cst = Univ.UnivConstraint.t
+type univ_csts = Univ.UnivConstraints.t
+type univ_ctx_set = PConstraints.ContextSet.t
+let univ_lt = Univ.UnivConstraint.Lt
+let univ_le = Univ.UnivConstraint.Le
+let univ_eq = Univ.UnivConstraint.Eq
+let univ_csts_of_list = Univ.UnivConstraints.of_list
+let univ_csts_to_list = Univ.UnivConstraints.elements
+let evd_merge_ctx_set rigid = Evd.merge_sort_context_set rigid QGraph.Internal
+let subst_univs_constraints x = UVars.subst_univs_constraints (Sorts.QVar.Map.empty,x)
+let univs_of_csts x = PConstraints.univs @@ UVars.UContext.constraints x
+let mk_universe_decl sort_poly_decl_extensible_instance sort_poly_decl_extensible_constraints sort_poly_decl_univ_constraints sort_poly_decl_instance =
+  let open UState in
+  { sort_poly_decl_qualities = [];
+    sort_poly_decl_extensible_instance;
+    sort_poly_decl_elim_constraints = Sorts.ElimConstraints.empty;
+    sort_poly_decl_extensible_qualities = false;
+    sort_poly_decl_extensible_constraints;
+    sort_poly_decl_univ_constraints;
+    sort_poly_decl_instance}
+let default_univ_decl = UState.default_sort_poly_decl
+let dest_udecl ({ UState.sort_poly_decl_instance ; sort_poly_decl_univ_constraints } : UState.sort_poly_decl) =
+  sort_poly_decl_instance, sort_poly_decl_univ_constraints
+
+let universe_constraint : univ_cst API.Conversion.t =
+  let open API.Conversion in let open API.AlgebraicData in declare {
+  ty = TyName "univ-constraint";
+  doc = "Constraint between two universes level variables";
+  pp = (fun fmt _ -> Format.fprintf fmt "<todo>");
+  constructors = [
+    K("lt","",A(universe_level_variable,A(universe_level_variable,N)),
+      B (fun u1 u2 -> (u1,univ_lt,u2)),
+      M (fun ~ok ~ko -> function (l1,Univ.UnivConstraint.Lt,l2) -> ok l1 l2 | _ -> ko ()));
+    K("le","",A(universe_level_variable,A(universe_level_variable,N)),
+      B (fun u1 u2 -> (u1,univ_le,u2)),
+      M (fun ~ok ~ko -> function (l1,Univ.UnivConstraint.Le,l2) -> ok l1 l2 | _ -> ko ()));
+    K("eq","",A(universe_level_variable,A(universe_level_variable,N)),
+      B (fun u1 u2 -> (u1,univ_eq,u2)),
+      M (fun ~ok ~ko -> function (l1,Univ.UnivConstraint.Eq,l2) -> ok l1 l2 | _ -> ko ()))
+  ]
+} |> API.ContextualConversion.(!<)
+[%%endif]
+
 
 let universe_variance : (Univ.Level.t * UVars.Variance.t option) API.Conversion.t =
   let open API.Conversion in let open API.AlgebraicData in declare {
@@ -243,8 +316,8 @@ let universe_variance : (Univ.Level.t * UVars.Variance.t option) API.Conversion.
   ]
 } |> API.ContextualConversion.(!<)
 
-type universe_decl = (Univ.Level.t list * bool) * (Univ.Constraints.t * bool)
-type universe_decl_cumul = ((Univ.Level.t * UVars.Variance.t option) list  * bool) * (Univ.Constraints.t * bool)
+type universe_decl = (Univ.Level.t list * bool) * (univ_csts * bool)
+type universe_decl_cumul = ((Univ.Level.t * UVars.Variance.t option) list  * bool) * (univ_csts * bool)
 
 type any_universe_decl =
   | NonCumul of universe_decl
@@ -257,11 +330,11 @@ let universe_decl : any_universe_decl API.Conversion.t =
   pp = (fun fmt _ -> Format.fprintf fmt "<todo>");
   constructors = [
     K("upoly-decl","",A(list universe_level_variable,A(bool,A(list universe_constraint,A(bool,N)))),
-     B (fun x sx y sy-> NonCumul ((x,sx),(Univ.Constraints.of_list  y,sy))),
-     M (fun ~ok ~ko -> function NonCumul ((x,sx),(y,sy)) -> ok x sx (Univ.Constraints.elements y) sy | Cumul _ -> ko ()));
+     B (fun x sx y sy-> NonCumul ((x,sx),(univ_csts_of_list  y,sy))),
+     M (fun ~ok ~ko -> function NonCumul ((x,sx),(y,sy)) -> ok x sx (univ_csts_to_list y) sy | Cumul _ -> ko ()));
     K("upoly-decl-cumul","",A(list universe_variance,A(bool,A(list universe_constraint,A(bool,N)))),
-     B (fun x sx y sy -> Cumul ((x,sx),(Univ.Constraints.of_list y,sy))),
-     M (fun ~ok ~ko -> function Cumul ((x,sx),(y,sy)) -> ok x sx (Univ.Constraints.elements y) sy | NonCumul _ -> ko ()))
+     B (fun x sx y sy -> Cumul ((x,sx),(univ_csts_of_list y,sy))),
+     M (fun ~ok ~ko -> function Cumul ((x,sx),(y,sy)) -> ok x sx (univ_csts_to_list y) sy | NonCumul _ -> ko ()))
   ]
 } |> API.ContextualConversion.(!<)
 
@@ -889,8 +962,8 @@ module CoqEngine_HOAS : sig
 
   (* when the env changes under the hood, we can adapt sigma or drop it but keep
      its constraints *)
-  val from_env_keep_univ_of_sigma :  uctx:Univ.ContextSet.t -> env0:Environ.env -> env:Environ.env -> Evd.evar_map -> coq_engine
-  val from_env_keep_univ_and_sigma : uctx:Univ.ContextSet.t -> env0:Environ.env -> env:Environ.env -> Evd.evar_map -> coq_engine
+  val from_env_keep_univ_of_sigma :  uctx:univ_ctx_set -> env0:Environ.env -> env:Environ.env -> Evd.evar_map -> coq_engine
+  val from_env_keep_univ_and_sigma : uctx:univ_ctx_set -> env0:Environ.env -> env:Environ.env -> Evd.evar_map -> coq_engine
 
 end = struct
 
@@ -1690,11 +1763,11 @@ let body_of_constant state c inst_opt = S.update_return engine state (fun x ->
      let c, ctx = UnivGen.fresh_global_instance x.global_env (ConstRef c) ?names:inst_opt  in
      let c, inst = Constr.destConst c in
      let bo = Vars.subst_instance_constr inst bo in
-     let sigma = Evd.merge_sort_context_set Evd.univ_rigid x.sigma ctx in
+     let sigma = evd_merge_ctx_set Evd.univ_rigid x.sigma ctx in
      let sigma = match priv with
      | Opaqueproof.PrivateMonomorphic () -> sigma
      | Opaqueproof.PrivatePolymorphic ctx ->
-      let ctx = Util.on_snd (Univ.subst_univs_level_constraints (snd (UVars.make_instance_subst inst))) ctx in
+      let ctx = Util.on_snd (subst_univs_constraints (snd (UVars.make_instance_subst inst))) ctx in
       Evd.merge_context_set Evd.univ_rigid sigma ctx
      in
      { x with sigma }, (Some (EConstr.of_constr bo), Some inst)
@@ -1852,7 +1925,7 @@ let in_coq_poly_gref ~depth ~origin ~failsafe s t i =
         s, u, []
       with Not_found ->
         let u, ctx = UnivGen.fresh_global_instance (get_global_env s) t in
-        let s = update_sigma s (fun sigma -> Evd.merge_sort_context_set UState.univ_flexible_alg sigma ctx) in
+        let s = update_sigma s (fun sigma -> evd_merge_ctx_set UState.univ_flexible_alg sigma ctx) in
         let u =
           match C.kind u with
           | C.Const (_, u) -> u
@@ -2943,9 +3016,9 @@ let universes_of_term state t =
   let sigma = get_sigma state in
   snd (EConstr.universes_of_constr sigma t)
 
-let universes_of_udecl state ({ UState.univdecl_instance ; univdecl_constraints } : UState.universe_decl) =
-  let used1 = univdecl_instance in
-  let used2 = List.map (fun (x,_,y) -> [x;y]) (Univ.Constraints.elements univdecl_constraints) in
+let universes_of_udecl state udecl =
+  let used1, csts = dest_udecl udecl in
+  let used2 = List.map (fun (x,_,y) -> [x;y]) (univ_csts_to_list csts) in
   let used = List.fold_right Univ.Level.Set.add used1 Univ.Level.Set.empty in
   let used = List.fold_right Univ.Level.Set.add (List.flatten used2) used in
   used
@@ -2966,18 +3039,9 @@ let name_universe_level state l =
   )
 
 
-let mk_universe_decl univdecl_extensible_instance univdecl_extensible_constraints univdecl_constraints univdecl_instance =
-  let open UState in
-  { univdecl_qualities = [];
-    univdecl_extensible_instance;
-    univdecl_extensible_qualities = false;
-    univdecl_extensible_constraints;
-    univdecl_constraints;
-    univdecl_instance}
-
 let poly_cumul_udecl_variance_of_options state options =
   match options.universe_decl with
-  | NotUniversePolymorphic -> state, false, false, UState.default_univ_decl, [| |]
+  | NotUniversePolymorphic -> state, false, false, default_univ_decl, [| |]
   | Cumulative ((univ_lvlt_var,univdecl_extensible_instance),(univdecl_constraints,univdecl_extensible_constraints)) ->
     let univdecl_instance, variance = List.split univ_lvlt_var in
     state, true, true,
@@ -3536,7 +3600,7 @@ let upoly_decl_of ~depth state ~loose_udecl mie =
     if not (CArray.is_empty qvars) then nYI "sort poly inductives"
     else
       let state, vars = CArray.fold_left_map (fun s l -> fst (name_universe_level s l), l) state vars in
-      let csts = UVars.UContext.constraints uc in
+      let csts = univs_of_csts uc in
       begin match mie.mind_entry_variance with
       | None ->
           let state, up, gls = universe_decl.API.Conversion.embed ~depth state (NonCumul ((Array.to_list vars,loose_udecl),(csts,loose_udecl))) in

src/rocq_elpi_HOAS.mli

@@ -24,8 +24,19 @@ type uinstanceoption =
   | VarInstance of (FlexibleData.Elpi.t * RawData.term list * inv_rel_key)
     (* a variable was provided, the command will compute the instance to unify with it *)
 
-type universe_decl = (Univ.Level.t list * bool) * (Univ.Constraints.t * bool)
-type universe_decl_cumul = ((Univ.Level.t * UVars.Variance.t option) list  * bool) * (Univ.Constraints.t * bool)
+[%%if coq = "9.0" || coq = "9.1"]
+type univ_cst = Univ.univ_constraint
+type univ_csts = Univ.Constraints.t
+type univ_ctx_set = Univ.ContextSet.t
+[%%else]
+type univ_cst = Univ.UnivConstraint.t
+type univ_csts = Univ.UnivConstraints.t
+type univ_ctx_set = PConstraints.ContextSet.t
+[%%endif]
+
+type universe_decl = (Univ.Level.t list * bool) * (univ_csts * bool)
+type universe_decl_cumul = ((Univ.Level.t * UVars.Variance.t option) list  * bool) * (univ_csts * bool)
+
 type universe_decl_option =
   | NotUniversePolymorphic
   | Cumulative of universe_decl_cumul
@@ -115,10 +126,14 @@ type record_field_spec = { name : Name.t; is_coercion : coercion_status; is_cano
 val lp2inductive_entry :
   depth:int -> empty coq_context -> constraints -> State.t -> term ->
   State.t * (DeclareInd.default_dep_elim list * Entries.mutual_inductive_entry * Univ.ContextSet.t * UnivNames.universe_binders * (bool * record_field_spec list) option * DeclareInd.one_inductive_impls list) * Conversion.extra_goals
-[%%else]
+[%%elif coq = "9.1"]
 val lp2inductive_entry :
   depth:int -> empty coq_context -> constraints -> State.t -> term ->
   State.t * (DeclareInd.default_dep_elim list * Entries.mutual_inductive_entry * Univ.ContextSet.t * UState.named_universes_entry * (bool * record_field_spec list) option * DeclareInd.one_inductive_impls list) * Conversion.extra_goals
+[%%else]
+val lp2inductive_entry :
+  depth:int -> empty coq_context -> constraints -> State.t -> term ->
+  State.t * (DeclareInd.default_dep_elim list * Entries.mutual_inductive_entry * PConstraints.ContextSet.t * UState.named_universes_entry * (bool * record_field_spec list) option * DeclareInd.one_inductive_impls list) * Conversion.extra_goals
 [%%endif]
 
 [%%if coq = "9.0"]
@@ -222,7 +237,12 @@ val in_elpiast_primitive : loc:Ast.Loc.t -> primitive_value -> Ast.Term.t
 
 val uinstance : UVars.Instance.t Conversion.t
 
+[%%if coq = "9.0" || coq = "9.1"]
 val universe_constraint : Univ.univ_constraint Conversion.t
+[%%else]
+val universe_constraint : Univ.UnivConstraint.t Conversion.t
+[%%endif]
+
 val universe_variance : (Univ.Level.t * UVars.Variance.t option) Conversion.t
 type any_universe_decl =
   | NonCumul of universe_decl
@@ -306,11 +326,16 @@ val body_of_constant :
   State.t -> Names.Constant.t -> UVars.Instance.t option ->
   State.t * EConstr.t option * UVars.Instance.t option
 
-val grab_global_env : uctx:Univ.ContextSet.t -> State.t -> State.t
 val grab_global_env_drop_univs_and_sigma : State.t -> State.t
 val grab_global_env_drop_sigma : State.t -> State.t
-val grab_global_env_drop_sigma_keep_univs : uctx:Univ.ContextSet.t -> State.t -> State.t
 
+[%%if coq = "9.0" || coq = "9.1"]
+val grab_global_env : uctx:Univ.ContextSet.t -> State.t -> State.t
+val grab_global_env_drop_sigma_keep_univs : uctx:Univ.ContextSet.t -> State.t -> State.t
+[%%else]
+val grab_global_env : uctx:PConstraints.ContextSet.t -> State.t -> State.t
+val grab_global_env_drop_sigma_keep_univs : uctx:PConstraints.ContextSet.t -> State.t -> State.t
+[%%endif]
 val mk_decl : depth:int -> Name.t -> ty:term -> term
 (* Adds an Arg for the normal form with ctx_len context entry vars in scope *)
 
@@ -347,10 +372,16 @@ val force_level_of_universe : state -> Univ.Universe.t -> state * Univ.Level.t *
 val purge_algebraic_univs_sort : state -> EConstr.ESorts.t -> state * Sorts.t
 val ideclc : constant
 val uideclc : constant
-val poly_cumul_udecl_variance_of_options : state -> options -> state * bool * bool * UState.universe_decl * Entries.variance_entry
 val merge_universe_context : state -> UState.t -> state
 val restricted_sigma_of : Univ.Level.Set.t -> state -> Evd.evar_map
 val universes_of_term : state -> EConstr.t -> Univ.Level.Set.t
+
+[%%if coq = "9.0" || coq = "9.1"]
+val poly_cumul_udecl_variance_of_options : state -> options -> state * bool * bool * UState.universe_decl * Entries.variance_entry
 val universes_of_udecl : state -> UState.universe_decl -> Univ.Level.Set.t
+[%%else]
+val poly_cumul_udecl_variance_of_options : state -> options -> state * bool * bool * UState.sort_poly_decl * Entries.variance_entry
+val universes_of_udecl : state -> UState.sort_poly_decl -> Univ.Level.Set.t
+[%%endif]
 
 val mind_record : Declarations.mind_specif -> Declarations.record_info