Supporting no purge of algebraic universes

.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";

_CoqProject

@@ -1,4 +1,5 @@
 -arg -w -arg +elpi.deprecated
+-arg -w -arg -ambiguous-extra-dep
 
 -R theories elpi
 -Q examples elpi.examples

apps/NES/_CoqProject

@@ -8,3 +8,5 @@
 
 theories/NES.v
 
+-arg -w -arg -ambiguous-extra-dep
+

apps/coercion/_CoqProject

@@ -12,3 +12,5 @@ src/elpi_coercion_plugin.mlpack
 src/META.coq-elpi-coercion
 
 theories/coercion.v
+
+-arg -w -arg -ambiguous-extra-dep

apps/cs/_CoqProject

@@ -13,3 +13,5 @@ src/elpi_cs_plugin.mlpack
 src/META.coq-elpi-cs
 
 theories/cs.v
+
+-arg -w -arg -ambiguous-extra-dep

apps/derive/_CoqProject

@@ -39,3 +39,5 @@ theories/derive/eqb.v
 theories/derive/eqbcorrect.v
 theories/derive/eqbOK.v
 theories/derive/eqType_ast.v
+
+-arg -w -arg -ambiguous-extra-dep

apps/eltac/_CoqProject

@@ -20,3 +20,5 @@ theories/case.v
 theories/generalize.v
 theories/cycle.v
 theories/tactics.v
+
+-arg -w -arg -ambiguous-extra-dep

apps/locker/_CoqProject

@@ -7,3 +7,5 @@
 -Q elpi elpi.apps.locker
 
 theories/locker.v
+
+-arg -w -arg -ambiguous-extra-dep

apps/tc/_CoqProject

@@ -20,3 +20,5 @@ theories/db.v
 theories/add_commands.v
 theories/tc.v
 theories/wip.v
+
+-arg -w -arg -ambiguous-extra-dep

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 
@@ -952,8 +957,7 @@ typeabbrev univ (ctype "univ").
 kind sort type.
 type prop sort. % impredicative sort of propositions
 type sprop sort. % impredicative sort of propositions with definitional proof irrelevance
-type typ univ ->
-         sort. % predicative sort of data (carries a universe level)
+type typ univ -> sort. % predicative sort of data (carries a universe level)
 
 % [coq.sort.leq S1 S2] constrains S1 <= S2
 external pred coq.sort.leq o:sort, o:sort.
@@ -974,6 +978,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.
 

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

@@ -166,45 +166,6 @@ let isuniv, univout, (univ : Univ.Universe.t API.Conversion.t) =
     | _ -> univ_to_be_patched.API.Conversion.readback ~depth state t
   end
 }
-
-let sort =
-  let open API.AlgebraicData in  declare {
-  ty = API.Conversion.TyName "sort";
-  doc = "Sorts (kinds of types)";
-  pp = (fun fmt -> function
-    | Sorts.Type _ -> Format.fprintf fmt "Type"
-    | Sorts.Set -> Format.fprintf fmt "Set"
-    | Sorts.Prop -> Format.fprintf fmt "Prop"
-    | Sorts.SProp -> Format.fprintf fmt "SProp"
-    | Sorts.QSort _ -> Format.fprintf fmt "Type");
-  constructors = [
-    K("prop","impredicative sort of propositions",N,
-      B Sorts.prop,
-      M (fun ~ok ~ko -> function Sorts.Prop -> ok | _ -> ko ()));
-    K("sprop","impredicative sort of propositions with definitional proof irrelevance",N,
-      B Sorts.sprop,
-      M (fun ~ok ~ko -> function Sorts.SProp -> ok | _ -> ko ()));
-    K("typ","predicative sort of data (carries a universe level)",A(univ,N),
-      B (fun x -> Sorts.sort_of_univ x),
-      M (fun ~ok ~ko -> function
-        | Sorts.Type x -> ok x
-        | Sorts.Set -> ok Univ.Universe.type0
-        | _ -> ko ()));
-    K("uvar","",A(F.uvar,N),
-      BS (fun (k,_) state ->
-        let m = S.get um state in
-        try
-          let u = UM.host k m in
-          state, Sorts.sort_of_univ u
-        with Not_found ->
-          let state, (_,u) = new_univ_level_variable state in
-          let state = S.update um state (UM.add k u) in
-          state, Sorts.sort_of_univ u),
-      M (fun ~ok ~ko _ -> ko ()));
-  ]
-} |> API.ContextualConversion.(!<)
-
-
 let universe_level_variable =
   let { CD.cin = levelin }, universe_level_variable_to_patch = CD.declare {
     CD.name = "univ.variable";
@@ -347,6 +308,7 @@ type options = {
   keepunivs : bool option;
   redflags : RedFlags.reds option;
   no_tc: bool option;
+  algunivs : bool option;
 }
 
 let default_options () = {
@@ -366,6 +328,7 @@ let default_options () = {
   keepunivs = None;
   redflags = None;
   no_tc = None;
+  algunivs = None;
 }
 
 type 'a coq_context = {
@@ -398,6 +361,59 @@ let pr_coq_ctx { env; db2name; db2rel } sigma =
     v 0 (Printer.pr_rel_context_of env sigma) ++ cut ()
   )
 
+let propc   = E.Constants.declare_global_symbol "prop"
+let spropc   = E.Constants.declare_global_symbol "sprop"
+let typc   = E.Constants.declare_global_symbol "typ"
+
+
+let sort : (Sorts.t, _ coq_context, API.Data.constraints) API.ContextualConversion.t =
+  let open API.ContextualConversion in
+  {
+  ty = API.Conversion.TyName "sort";
+  pp_doc = (fun fmt () ->
+    Format.fprintf fmt "%% Sorts (kinds of types)\n";
+    Format.fprintf fmt "kind sort type.\n";
+    Format.fprintf fmt "type prop sort. %% impredicative sort of propositions\n";
+    Format.fprintf fmt "type sprop sort. %% impredicative sort of propositions with definitional proof irrelevance\n";
+    Format.fprintf fmt "type typ univ -> sort. %% predicative sort of data (carries a universe level)\n";
+  );
+  pp = (fun fmt -> function
+    | Sorts.Type _ -> Format.fprintf fmt "Type"
+    | Sorts.Set -> Format.fprintf fmt "Set"
+    | Sorts.Prop -> Format.fprintf fmt "Prop"
+    | Sorts.SProp -> Format.fprintf fmt "SProp"
+    | Sorts.QSort _ -> Format.fprintf fmt "QSort");
+  embed = (fun ~depth { options } _ state s ->
+    match s with
+    | Sorts.Prop -> state, E.mkConst propc, []
+    | Sorts.SProp -> state, E.mkConst spropc, []
+    | Sorts.Set ->
+        let state, u, gls = univ.embed ~depth state Univ.Universe.type0 in
+        state, E.mkApp typc u [], gls
+    | Sorts.Type u ->
+        let state, u, gls = univ.embed ~depth state u in
+        state, E.mkApp typc u [], gls
+    | Sorts.QSort _ -> nYI "sort polymorphism");
+  readback = (fun ~depth { options } _ state t ->
+    match E.look ~depth t with
+    | E.Const c when c == propc -> state, Sorts.prop, []
+    | E.Const c when c == spropc -> state, Sorts.sprop, []
+    | E.App(c,u,[]) when c == typc ->
+        let state, u, gls = univ.readback ~depth state u in
+        state, Sorts.sort_of_univ u ,gls
+    | E.UnifVar(k,_) -> begin
+        let m = S.get um state in
+        try
+          let u = UM.host k m in
+          state, Sorts.sort_of_univ u, []
+        with Not_found ->
+          let state, (_,u) = new_univ_level_variable state in
+          let state = S.update um state (UM.add k u) in
+          state, Sorts.sort_of_univ u, []
+        end
+    | _ ->  raise API.Conversion.(TypeErr(TyName"sort",depth,t)));
+}
+
 let in_coq_fresh ~id_only =
   let mk_fresh dbl =
     Id.of_string_soft
@@ -947,17 +963,20 @@ let purge_algebraic_univs_sort state s =
       let state, _, _, s = force_level_of_universe state u in
       state, s
   | x -> state, x
-
+
+let sort = { sort with API.ContextualConversion.embed = (fun ~depth ctx csts state s ->
+  let state, s =
+    if ctx.options.algunivs = None || ctx.options.algunivs = Some false then
+      purge_algebraic_univs_sort state (EConstr.ESorts.make s)
+    else
+      state, s in
+  sort.API.ContextualConversion.embed ~depth ctx csts 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 state, s = purge_algebraic_univs_sort state (EConstr.ESorts.make s) in
-  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
-  assert(gl=[]);
-  state, E.mkApp sortc s []
+
+let in_elpi_sort ~depth ctx csts state s =
+  let state, s, gl = sort.API.ContextualConversion.embed ~depth ctx csts state s in
+  state, E.mkApp sortc s [], gl
 
 
 (* ********************************* }}} ********************************** *)
@@ -1147,6 +1166,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
@@ -1168,9 +1193,8 @@ let get_options ~depth hyps state =
     no_tc = get_bool_option "coq:no_tc";
     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 =
   let env = get_global_env state in
   let section = section_ids env in
@@ -1312,7 +1336,10 @@ let rec constr2lp coq_ctx ~calldepth ~depth state t =
          let args = CList.firstn argno args in
          let state, args = CList.fold_left_map (aux ~depth env) state args in
          state, E.mkUnifVar elpi_uvk ~args:(List.rev args) state
-    | C.Sort s -> in_elpi_sort ~depth state (EC.ESorts.kind sigma s)
+    | C.Sort s ->
+         let state, s, gl = in_elpi_sort ~depth coq_ctx API.RawData.no_constraints state (EC.ESorts.kind sigma s) in
+         gls := gl @ !gls;
+         state, s
     | C.Cast (t,_,ty0) ->
          let state, t = aux ~depth env state t in
          let state, ty = aux ~depth env state ty0 in
@@ -1823,7 +1850,7 @@ and lp2constr ~calldepth syntactic_constraints coq_ctx ~depth state ?(on_ty=fals
   debug Pp.(fun () -> str"lp2term@" ++ int depth ++ str":" ++ str(pp2string (P.term depth) t));
   match E.look ~depth t with
   | E.App(s,p,[]) when sortc == s ->
-      let state, u, gsl = sort.API.Conversion.readback ~depth state p in
+      let state, u, gsl = sort.API.ContextualConversion.readback ~depth coq_ctx syntactic_constraints state p in
       state, EC.mkSort (EC.ESorts.make u), gsl
  (* constants *)
   | E.App(c,d,[]) when globalc == c ->

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 = {
@@ -147,7 +148,7 @@ val in_elpi_gr : depth:int -> State.t -> Names.GlobRef.t -> term
 val in_elpi_poly_gr : depth:int -> State.t -> Names.GlobRef.t -> term -> term
 val in_elpi_poly_gr_instance : depth:int -> State.t -> Names.GlobRef.t -> UVars.Instance.t -> term
 val in_elpi_flex_sort : term -> term
-val in_elpi_sort : depth:int -> state -> Sorts.t -> state * term
+val in_elpi_sort : depth:int -> 'a coq_context -> constraints -> state -> Sorts.t -> state * term * Conversion.extra_goals
 val in_elpi_prod : Name.t -> term -> term -> term
 val in_elpi_lam : Name.t -> term -> term -> term
 val in_elpi_let : Name.t -> term -> term -> term -> term
@@ -172,7 +173,7 @@ val gref : Names.GlobRef.t Conversion.t
 val inductive : inductive Conversion.t
 val constructor : constructor Conversion.t
 val constant : global_constant Conversion.t
-val sort : Sorts.t Conversion.t
+val sort : (Sorts.t,'a coq_context,constraints) ContextualConversion.t
 val global_constant_of_globref : Names.GlobRef.t -> global_constant
 val abbreviation : Globnames.abbreviation Conversion.t
 val implicit_kind : Glob_term.binding_kind Conversion.t