From 9244a2f8031614e3c936275c3a1d36c2ec214a89 Mon Sep 17 00:00:00 2001 From: Enzo Crance Date: Mon, 21 Nov 2022 09:16:35 +0100 Subject: [PATCH 1/3] :sparkles: Add coq.univ.super --- coq-builtin.elpi | 3 +++ src/coq_elpi_builtins.ml | 8 ++++++++ 2 files changed, 11 insertions(+) diff --git a/coq-builtin.elpi b/coq-builtin.elpi index 432921064..19df2ce79 100644 --- a/coq-builtin.elpi +++ b/coq-builtin.elpi @@ -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. diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index 5fb0ce1f3..1df6649b6 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -2369,6 +2369,14 @@ 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", InOut(B.ioarg id, "Name", InOut(B.ioarg univ, "U", From 756d5b9f34729de9e489f922c92609ecb326845b Mon Sep 17 00:00:00 2001 From: Enzo Crance Date: Mon, 21 Nov 2022 16:40:56 +0100 Subject: [PATCH 2/3] :boom: Algebraic universes not purged anymore --- src/coq_elpi_HOAS.ml | 4 ++-- src/coq_elpi_builtins.ml | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml index baa659091..de76883d9 100644 --- a/src/coq_elpi_HOAS.ml +++ b/src/coq_elpi_HOAS.ml @@ -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 diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index 1df6649b6..5329dfd07 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -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); @@ -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); From 8cb61ede0077079129f08801f13023b3d93b5d20 Mon Sep 17 00:00:00 2001 From: Enzo Crance Date: Thu, 8 Dec 2022 11:20:32 +0100 Subject: [PATCH 3/3] :sparkles: Add coq.univ.max --- src/coq_elpi_builtins.ml | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index 5329dfd07..5952b8ceb 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -2377,6 +2377,15 @@ phase unnecessary.|}; 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",