Skip to content

Adapt to rocq-prover/rocq#21195 (Constraints->UnivConstraints, univ_decl->sort_poly_decl) #934

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Dec 3, 2025
+251 −102
Merged

Adapt to rocq-prover/rocq#21195 (Constraints->UnivConstraints, univ_decl->sort_poly_decl) #934

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
124 changes: 94 additions & 30 deletions src/rocq_elpi_HOAS.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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 {
Expand All @@ -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
Expand All @@ -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.(!<)

Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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,
Expand Down Expand Up @@ -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
Expand Down
43 changes: 37 additions & 6 deletions src/rocq_elpi_HOAS.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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"]
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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 *)

Expand Down Expand Up @@ -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
Loading
Loading