Skip to content

Missing API on universes #544

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 3 commits into
base: master
Choose a base branch
from
Open

Missing API on universes #544

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
9244a2f
:sparkles: Add coq.univ.super
ecranceMERCE Nov 21, 2022
756d5b9
:boom: Algebraic universes not purged anymore
ecranceMERCE Nov 21, 2022
8cb61ed
:sparkles: Add coq.univ.max
ecranceMERCE Dec 8, 2022
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
3 changes: 3 additions & 0 deletions coq-builtin.elpi
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -957,6 +957,9 @@ external pred coq.univ.print .
% [coq.univ.new U] A fresh universe.
external pred coq.univ.new o:univ.

% [coq.univ.super U U1] relates a univ U to its successor U1
external pred coq.univ.super i:univ, o:univ.

% [coq.univ Name U] Finds a named unvierse. Can fail.
external pred coq.univ o:id, o:univ.

Expand Down
4 changes: 2 additions & 2 deletions src/coq_elpi_HOAS.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -913,9 +913,9 @@ let purge_algebraic_univs_sort state s =

let in_elpi_flex_sort t = E.mkApp sortc (E.mkApp typc t []) []

let sort = { sort with API.Conversion.embed = (fun ~depth state s ->
(* let sort = { sort with API.Conversion.embed = (fun ~depth state s ->
let state, s = purge_algebraic_univs_sort state (EConstr.ESorts.make s) in
sort.API.Conversion.embed ~depth state s) }
sort.API.Conversion.embed ~depth state s) } *)

let in_elpi_sort ~depth state s =
let state, s, gl = sort.API.Conversion.embed ~depth state s in
Expand Down
21 changes: 19 additions & 2 deletions src/coq_elpi_builtins.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2311,7 +2311,7 @@ phase unnecessary.|};
| Data u1, Data u2 ->
if Sorts.equal u1 u2 then state, !: u1 +! u2,[]
else
let state, u2 = purge_algebraic_univs_sort state (EConstr.ESorts.make u2) in
(* let state, u2 = purge_algebraic_univs_sort state (EConstr.ESorts.make u2) in *)
add_universe_constraint state (constraint_leq u1 u2), !: u1 +! u2,[]
| _ -> err Pp.(str"coq.sort.leq: called with _ as argument"))),
DocAbove);
Expand All @@ -2325,7 +2325,7 @@ phase unnecessary.|};
| Data u1, Data u2 ->
if Sorts.equal u1 u2 then state, !: u1 +! u2,[]
else
let state, u2 = purge_algebraic_univs_sort state (EConstr.ESorts.make u2) in
(* let state, u2 = purge_algebraic_univs_sort state (EConstr.ESorts.make u2) in *)
add_universe_constraint state (constraint_eq u1 u2), !: u1 +! u2, []
| _ -> err Pp.(str"coq.sort.eq: called with _ as argument"))),
DocAbove);
Expand Down Expand Up @@ -2369,6 +2369,23 @@ phase unnecessary.|};
state, !: u, [])),
DocAbove);

MLCode(Pred("coq.univ.super",
In(univ,"U",
Out(univ,"U1",
Full(unit_ctx, "relates a univ U to its successor U1"))),
(fun u _ ~depth _ _ state ->
state, !: (Univ.Universe.super u), [])),
DocAbove);

MLCode(Pred("coq.univ.max",
In(univ,"U1",
In(univ,"U2",
Out(univ,"UMax",
Full(unit_ctx, "relates univs U1 and U2 to their max UMax")))),
(fun u1 u2 _ ~depth _ _ state ->
state, !: (Univ.Universe.sup u1 u2), [])),
DocAbove);

MLCode(Pred("coq.univ",
InOut(B.ioarg id, "Name",
InOut(B.ioarg univ, "U",
Expand Down