Skip to content

Adapt to rocq-prover/rocq#21195 (add quality constraint kind) #144

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

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Adapt to rocq-prover/rocq#21195 (add quality constraint kind) #144

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
2 changes: 1 addition & 1 deletion src/debug.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -190,7 +190,7 @@ let debug_mutual_inductive_entry =
match entry.mind_entry_universes with
| Monomorphic_ind_entry | Template_ind_entry _ -> mt ()
| Polymorphic_ind_entry ux ->
UVars.pr_universe_context Sorts.QVar.raw_pr UnivNames.pr_level_with_global_universes ux
UVars.UContext.pr Sorts.QVar.raw_pr UnivNames.pr_level_with_global_universes ux
in
let mind_entry_cumul_pp = bool (Option.has_some entry.mind_entry_variance) in
let mind_entry_private_pp =
Expand Down
12 changes: 6 additions & 6 deletions src/declare_translation.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -114,7 +114,7 @@ let declare_inductive ~opaque_access name ?(continuation = default_continuation)
debug_evar_map [`Inductive] "evar_map inductive " env !evd;
let size = Declarations.(Array.length mut_body.mind_packets) in
let mut_ind_R = DeclareInd.declare_mutual_inductive_with_eliminations translation_entry
(Monomorphic_entry Univ.ContextSet.empty, UnivNames.empty_binders) [] in
(Monomorphic_entry PConstraints.ContextSet.empty, UnivNames.empty_binders) [] in
for k = 0 to size-1 do
Relations.declare_inductive_relation arity (mut_ind, k) (mut_ind_R, k)
done;
Expand Down Expand Up @@ -245,7 +245,7 @@ and declare_module ~opaque_access ?(continuation = ignore) ?name arity mp mb =
let env = Global.env () in
let evd = Evd.from_env env in
let evd, ucst =
Evd.(with_sort_context_set univ_rigid evd (UnivGen.fresh_constant_instance env cst))
Evd.(with_sort_context_set univ_rigid QGraph.Rigid evd (UnivGen.fresh_constant_instance env cst))
in
let evdr = ref evd in
ignore(declare_realizer ~opaque_access ~continuation arity evdr env None (mkConstU (fst ucst, EInstance.make (snd ucst))))
Expand All @@ -264,7 +264,7 @@ and declare_module ~opaque_access ?(continuation = ignore) ?name arity mp mb =
let env = Global.env () in
let evd = Evd.from_env env in
let evd, ucst =
Evd.(with_sort_context_set univ_rigid evd (UnivGen.fresh_constant_instance env cst))
Evd.(with_sort_context_set univ_rigid QGraph.Rigid evd (UnivGen.fresh_constant_instance env cst))
in
let c = mkConstU (fst ucst, EInstance.make (snd ucst)) in
let evdr = ref evd in
Expand All @@ -288,7 +288,7 @@ and declare_module ~opaque_access ?(continuation = ignore) ?name arity mp mb =
continuation ()
else begin
let evd, pind =
Evd.(with_sort_context_set univ_rigid !evdr (UnivGen.fresh_inductive_instance env ind))
Evd.(with_sort_context_set univ_rigid QGraph.Rigid !evdr (UnivGen.fresh_inductive_instance env ind))
in
evdr := evd;
debug_string [`Module] (Printf.sprintf "inductive field: '%s'." (Names.Label.to_string lab));
Expand Down Expand Up @@ -357,7 +357,7 @@ let command_constant ~opaque_access ?(continuation = default_continuation) ~full
let scope = Locality.(Global ImportDefaultBehavior) in
let kind = Decls.(IsDefinition Definition) in
let evd, pconst =
Evd.(with_sort_context_set univ_rigid evd (UnivGen.fresh_constant_instance env constant))
Evd.(with_sort_context_set univ_rigid QGraph.Static evd (UnivGen.fresh_constant_instance env constant))
in
let constr = mkConstU (fst pconst, EInstance.make @@ snd pconst) in
declare_abstraction ~opaque_access ~continuation ~opaque ~poly ~scope ~kind
Expand All @@ -367,7 +367,7 @@ let command_inductive ~opaque_access ?(continuation = default_continuation) ~ful
let env = Global.env () in
let evd = Evd.from_env env in
let evd, pind =
Evd.(with_sort_context_set univ_rigid evd (UnivGen.fresh_inductive_instance env inductive))
Evd.(with_sort_context_set univ_rigid QGraph.Static evd (UnivGen.fresh_inductive_instance env inductive))
in
let name = match names with
| None ->
Expand Down
12 changes: 6 additions & 6 deletions src/parametricity.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -463,7 +463,7 @@ and translate_constant order (evd : Evd.evar_map ref) env cst : constr =
Declarations.(match cb.const_body with
| Def _ ->
let (value, _, constraints) = constant_value_and_type env (kn,names) in
let evd' = Evd.add_constraints !evd constraints in
let evd' = Evd.add_poly_constraints QGraph.Internal !evd constraints in
evd := evd';
translate order evd env (of_constr (Option.get value))
| OpaqueDef op ->
Expand Down Expand Up @@ -1130,20 +1130,20 @@ let fix_template_params order evdr env temp b params =
match Univ.Level.var_index u0 with
| None ->
(* not template, this is technically allowed but dubious *)
Univ.Constraints.add (u0, cst, v) accu
Univ.UnivConstraints.add (u0, cst, v) accu
| Some u0 -> match Int.Map.find_opt u0 umap with
| None -> assert false (* unbound template level *)
| Some (ur, repl) ->
let accu = Univ.Constraints.add (ur, cst, v) accu in
let fold accu u = Univ.Constraints.add (u, cst, v) accu in
let accu = Univ.UnivConstraints.add (ur, cst, v) accu in
let fold accu u = Univ.UnivConstraints.add (u, cst, v) accu in
List.fold_left fold accu repl
in
let uctx = UVars.AbstractContext.repr temp.template_context in
let univs = UVars.UContext.instance uctx in
let qvars, univs = UVars.Instance.to_array univs in
let cstrs = UVars.UContext.constraints uctx in
let univs = Array.concat @@ Array.map_to_list map_univs univs in
let cstrs = Univ.Constraints.fold fold_cstrs cstrs Univ.Constraints.empty in
let cstrs = PConstraints.fold ((fun _ csts -> csts), fold_cstrs) cstrs PConstraints.empty in
let unames = { UVars.quals = Array.make (Array.length qvars) Anonymous; UVars.univs = Array.make (Array.length univs) Anonymous } in
let uctx = UVars.UContext.make unames (UVars.Instance.of_array (qvars,univs), cstrs) in
let default_univs =
Expand Down Expand Up @@ -1171,7 +1171,7 @@ let rec translate_mind_body name order evdr env kn b inst =
in
let r = ERelevance.make ind.mind_relevance in
let env = push_rel (toDecl (mkannot (Names.Name typename) r, None, (of_constr full_arity))) env in
let env = Environ.add_constraints cst env in
let env = Environ.add_constraints QGraph.Internal cst env in
env
) env (Array.to_list b.mind_packets)
in
Expand Down