wip

Author: CohenCyril

.nix/coq-overlays/coq-elpi/default.nix

@@ -9,6 +9,8 @@ with builtins; with lib; let
     { case = "8.15"; out = { version = "1.16.5"; };}
     { case = "8.16"; out = { version = "1.16.5"; };}
   ] {} );
+  dot-merlin-reader = coq.ocamlPackages.dot-merlin-reader;
+  dune = coq.ocamlPackages.dune_3;
 in mkCoqDerivation {
   pname = "elpi";
   repo  = "coq-elpi";
@@ -53,7 +55,7 @@ in mkCoqDerivation {
   releaseRev = v: "v${v}";
 
   mlPlugin = true;
-  propagatedBuildInputs = [ elpi ];
+  propagatedBuildInputs = [ elpi dot-merlin-reader dune ];
 
   meta = {
     description = "Coq plugin embedding ELPI.";

.nix/ocaml-overlays/elpi/default.nix

@@ -1,6 +1,7 @@
 { lib
 , buildDunePackage, camlp5
 , ocaml
+, ocaml-lsp
 , menhir, menhirLib
 , stdlib-shims
 , re, perl, ncurses
@@ -34,7 +35,7 @@ buildDunePackage rec {
   buildInputs = [ perl ncurses ]
   ++ optional (versionAtLeast version "1.15" || version == "dev") menhir;
 
-  propagatedBuildInputs = [ re stdlib-shims ]
+  propagatedBuildInputs = [ re stdlib-shims ocaml-lsp ]
   ++ (if versionAtLeast version "1.15" || version == "dev"
      then [ menhirLib ]
      else [ camlp5 ] )

coq-builtin.elpi

@@ -354,6 +354,11 @@ typeabbrev opaque?   bool.  macro @opaque! :- tt. macro @transparent! :- ff.
 macro @global!   :- get-option "coq:locality" "global".
 macro @local!    :- get-option "coq:locality" "local".
 
+macro @keep-alg-univs! :-
+  get-option "coq:algunivs" "keep-algunivs".
+macro @purge-alg-univs! :-
+  get-option "coq:algunivs" "purge-algunivs".
+
 macro @primitive! :- get-option "coq:primitive" tt. % primitive records
 macro @nonuniform! :- get-option "coq:nonuniform" tt. % coercions
 macro @reversible! :- get-option "coq:reversible" tt. % coercions

elpi/coq-HOAS.elpi

@@ -339,6 +339,11 @@ typeabbrev opaque?   bool.  macro @opaque! :- tt. macro @transparent! :- ff.
 macro @global!   :- get-option "coq:locality" "global".
 macro @local!    :- get-option "coq:locality" "local".
 
+macro @keep-alg-univs! :-
+  get-option "coq:algunivs" "keep-algunivs".
+macro @purge-alg-univs! :-
+  get-option "coq:algunivs" "purge-algunivs".
+
 macro @primitive! :- get-option "coq:primitive" tt. % primitive records
 macro @nonuniform! :- get-option "coq:nonuniform" tt. % coercions
 macro @reversible! :- get-option "coq:reversible" tt. % coercions

src/coq_elpi_HOAS.ml

@@ -344,6 +344,7 @@ type options = {
   reversible : bool option;
   keepunivs : bool option;
   redflags : CClosure.RedFlags.reds option;
+  algunivs : bool option;
 }
 
 let default_options () = {
@@ -363,6 +364,7 @@ let default_options () = {
   reversible = None;
   keepunivs = None;
   redflags = None;
+  algunivs = None;
 }
 
 type 'a coq_context = {
@@ -1105,6 +1107,12 @@ let get_options ~depth hyps state =
       let _, rd, gl = reduction_flags.Elpi.API.Conversion.readback ~depth state t in
       assert (gl = []);
       Some rd in
+  let keeping_algebraic_universes s =
+    if s = Some "default" then None
+    else if s = Some "keep-alguniv" then Some true
+    else if s = Some "purge-alguniv" then Some false
+    else if s = None then None
+    else err Pp.(str"Unknown algebraic universes attribute: " ++ str (Option.get s)) in
   {
     hoas_holes =
       begin match get_bool_option "HOAS:holes" with
@@ -1126,6 +1134,7 @@ let get_options ~depth hyps state =
     reversible = get_bool_option "coq:reversible";
     keepunivs = get_bool_option "coq:keepunivs";
     redflags = get_redflags_option ();
+    algunivs = keeping_algebraic_universes @@ get_string_option "coq:algunivs";
   }
 
 let mk_coq_context ~options state =

src/coq_elpi_HOAS.mli

@@ -47,6 +47,7 @@ type options = {
   reversible : bool option;
   keepunivs : bool option;
   redflags : CClosure.RedFlags.reds option;
+  algunivs : bool option;
 }
 
 type 'a coq_context = {

src/coq_elpi_builtins.ml

@@ -2173,29 +2173,35 @@ phase unnecessary.|};
   MLCode(Pred("coq.sort.leq",
     InOut(B.ioarg_flex sort, "S1",
     InOut(B.ioarg_flex sort, "S2",
-    Full(unit_ctx, "constrains S1 <= S2"))),
-  (fun u1 u2 ~depth _ _ state ->
+    Full(global, "constrains S1 <= S2"))),
+  (fun u1 u2 ~depth { options } _ -> on_global_state "coq.sort.leq"
+  (fun state ->
     match u1, u2 with
     | 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 *)
-          add_universe_constraint state (constraint_leq u1 u2), !: u1 +! u2,[]
-    | _ -> err Pp.(str"coq.sort.leq: called with _ as argument"))),
+          let state, u2 = if true (* options.algunivs != Some true *)
+          then purge_algebraic_univs_sort state (EConstr.ESorts.make u2)
+          else state, u2 in
+        add_universe_constraint state (constraint_leq u1 u2), !: u1 +! u2,[]
+    | _ -> err Pp.(str"coq.sort.leq: called with _ as argument")))),
   DocAbove);
 
   MLCode(Pred("coq.sort.eq",
     InOut(B.ioarg_flex sort, "S1",
     InOut(B.ioarg_flex sort, "S2",
-    Full(unit_ctx, "constrains S1 = S2"))),
-  (fun u1 u2 ~depth _ _ state ->
+    Full(global, "constrains S1 = S2"))),
+  (fun u1 u2 ~depth { options } _ -> on_global_state "coq.sort.eq"
+  (fun state ->
     match u1, u2 with
     | 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 = if true (* options.algunivs != Some true *)
+        then purge_algebraic_univs_sort state (EConstr.ESorts.make u2)
+        else state, u2 in
         add_universe_constraint state (constraint_eq u1 u2), !: u1 +! u2, []
-    | _ -> err Pp.(str"coq.sort.eq: called with _ as argument"))),
+    | _ -> err Pp.(str"coq.sort.eq: called with _ as argument")))),
   DocAbove);
 
   MLCode(Pred("coq.sort.sup",