wip

Author: CohenCyril

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

@@ -12,6 +12,8 @@ with builtins; with lib; let
     { case = "8.18"; out = { version = "v1.18.1"; };}
     { case = "8.19"; out = { version = "v1.18.2"; };}
   ] {} );
+  dot-merlin-reader = coq.ocamlPackages.dot-merlin-reader;
+  dune = coq.ocamlPackages.dune_3;
 in mkCoqDerivation {
   pname = "elpi";
   repo  = "coq-elpi";
@@ -64,7 +66,7 @@ in mkCoqDerivation {
   buildFlags = [ "OCAMLWARN=" ];
 
   mlPlugin = true;
-  propagatedBuildInputs = [ coq.ocamlPackages.findlib elpi ];
+  propagatedBuildInputs = [ coq.ocamlPackages.findlib 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
 , atdgen
 , stdlib-shims
@@ -47,10 +48,11 @@ buildDunePackage rec {
   buildInputs = [ ncurses ]
   ++ lib.optional (lib.versionAtLeast version "1.16" || version == "dev") atdgen;
 
-  propagatedBuildInputs = [ re stdlib-shims ]
-  ++ [ menhirLib ]
-  ++ [ ppxlib ppx_deriving ]
-  ;
+  propagatedBuildInputs = [ re stdlib-shims ocaml-lsp ]
+  ++ (if versionAtLeast version "1.15" || version == "dev"
+     then [ menhirLib ]
+     else [ camlp5 ] )
+  ++ [ ppxlib ppx_deriving atdgen ];
 
   meta = with lib; {
     description = "Embeddable λProlog Interpreter";

coq-builtin.elpi

@@ -452,6 +452,11 @@ typeabbrev opaque?   bool.  macro @opaque! :- tt. macro @transparent! :- ff.
 
 %%%%%%% Attributes to be passed to APIs as in @local! => coq.something %%%%%%%%
 
+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 @reversible! :- get-option "coq:reversible" tt. % coercions
 macro @no-tc! :- get-option "coq:no_tc" tt. % skip typeclass inference 

elpi/coq-HOAS.elpi

@@ -301,6 +301,11 @@ typeabbrev opaque?   bool.  macro @opaque! :- tt. macro @transparent! :- ff.
 
 %%%%%%% Attributes to be passed to APIs as in @local! => coq.something %%%%%%%%
 
+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 @reversible! :- get-option "coq:reversible" tt. % coercions
 macro @no-tc! :- get-option "coq:no_tc" tt. % skip typeclass inference 

src/coq_elpi_HOAS.ml

@@ -347,6 +347,7 @@ type options = {
   keepunivs : bool option;
   redflags : RedFlags.reds option;
   no_tc: bool option;
+  algunivs : bool option;
 }
 
 let default_options () = {
@@ -366,6 +367,7 @@ let default_options () = {
   keepunivs = None;
   redflags = None;
   no_tc = None;
+  algunivs = None;
 }
 
 type 'a coq_context = {
@@ -1147,6 +1149,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
@@ -1169,8 +1177,6 @@ let get_options ~depth hyps state =
     keepunivs = get_bool_option "coq:keepunivs";
     redflags = get_redflags_option ();
 
-  }
-
 let mk_coq_context ~options state =
   let env = get_global_env state in
   let section = section_ids env in

src/coq_elpi_HOAS.mli

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

src/coq_elpi_builtins.ml

@@ -2280,29 +2280,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",