Merge pull request #804 from lweqx/keep-alg-univs

Add coq.univ.alg-super, @keep-alg-univs!

Author: CohenCyril

Changelog.md

@@ -5,6 +5,14 @@
 - derive: support for `is_true` in `param1_trivial` (based on pre-existing
   special support for `is_eq` and `is_bool`)
 
+### API
+- New `coq.univ.alg-super` that relates a univ `U` to its algebraic successor
+  `V`, that is `U+1` and not any `V` s.t. `U < V`
+
+### HOAS
+- New `@keep-alg-univs!` option for all APIs taking terms. By default algebraic
+  universes are replaced by named universes. See the `coq.univ.alg-super` API.
+
 # [2.5.0] 18/2/2025
 
 Requires Elpi 2.0.7 and Coq 8.20 or Rocq 9.0.

builtin-doc/coq-builtin.elpi

@@ -454,6 +454,8 @@ 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:keepalgunivs" tt.
+
 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 
@@ -978,8 +980,7 @@ kind univ type.
 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.
@@ -1000,6 +1001,10 @@ external pred coq.univ.print .
 % [coq.univ.new U] A fresh universe.
 external pred coq.univ.new o:univ.
 
+% [coq.univ.alg-super U V] relates a univ U to its algebraic successor V,
+% that is U+1 and not any V s.t. U < V
+external pred coq.univ.alg-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,8 @@ 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:keepalgunivs" tt.
+
 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/rocq_elpi_HOAS.ml

@@ -174,53 +174,6 @@ let isuniv, univout, univino, (univ : Univ.Universe.t API.Conversion.t) =
   end
 }
 
-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 =
-  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 ast_sort ~loc = function
-  | Sorts.Prop -> A.mkGlobal ~loc propc
-  | Sorts.SProp -> A.mkGlobal ~loc spropc
-  | Sorts.Set -> A.mkAppGlobal ~loc typc (A.mkOpaque ~loc @@ univino Univ.Universe.type0) []
-  | Sorts.Type u -> A.mkAppGlobal ~loc typc (A.mkOpaque ~loc @@ univino u) []
-  | _ -> assert false
 
 let universe_level_variable =
   let { CD.cin = levelin }, universe_level_variable_to_patch = CD.declare {
@@ -364,6 +317,7 @@ type options = {
   keepunivs : bool option;
   redflags : RedFlags.reds option;
   no_tc: bool option;
+  algunivs : bool option;
 }
 let default_options () = {
   hoas_holes = Some Verbatim;
@@ -382,14 +336,15 @@ let default_options () = {
   keepunivs = None;
   redflags = None;
   no_tc = None;
+  algunivs = None;
 }
 let make_options ~hoas_holes ~local ~warn ~depr ~primitive ~failsafe ~ppwidth
   ~pp ~pplevel ~using ~inline ~uinstance ~universe_decl ~reversible ~keepunivs
-  ~redflags ~no_tc = 
+  ~redflags ~no_tc ~algunivs =
   let user_warns = Some UserWarn.{ depr; warn } in
   { hoas_holes; local; user_warns; primitive; failsafe; ppwidth; pp;
     pplevel; using; inline; uinstance; universe_decl; reversible; keepunivs;
-    redflags; no_tc; }
+    redflags; no_tc; algunivs; }
 let make_warn = UserWarn.make_warn
 
 type 'a coq_context = {
@@ -422,6 +377,67 @@ 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 ast_sort ~loc = function
+  | Sorts.Prop -> A.mkGlobal ~loc propc
+  | Sorts.SProp -> A.mkGlobal ~loc spropc
+  | Sorts.Set -> A.mkAppGlobal ~loc typc (A.mkOpaque ~loc @@ univino Univ.Universe.type0) []
+  | Sorts.Type u -> A.mkAppGlobal ~loc typc (A.mkOpaque ~loc @@ univino u) []
+  | _ -> assert false
+
+
 let in_coq_fresh ~id_only =
   let mk_fresh dbl =
     Id.of_string_soft
@@ -1052,7 +1068,6 @@ let section_ids env =
       ~init:[] named_ctx
 
 let sortc  = E.Constants.declare_global_symbol "sort"
-let typc   = E.Constants.declare_global_symbol "typ"  
 
 let force_level_of_universe state u =
   match Univ.Universe.level u with
@@ -1074,14 +1089,18 @@ let in_elpi_flex_sort t = E.mkApp sortc (E.mkApp typc t []) []
 let in_elpiast_flex_sort ~loc t =
   A.mkAppGlobal ~loc sortc (A.mkAppGlobal ~loc 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 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_sort ~depth state s =
-  let state, s, gl = sort.API.Conversion.embed ~depth state s in
+let in_elpi_sort ~depth ctx csts state s =
+  let state, s, gl = sort.API.ContextualConversion.embed ~depth ctx csts state s in
   assert(gl=[]);
-  state, E.mkApp sortc s []
+  state, E.mkApp sortc s [], gl
 
 let in_elpiast_sort ~loc state s =
   A.mkAppGlobal ~loc sortc (ast_sort ~loc s) []
@@ -1301,10 +1320,10 @@ let get_options ~depth hyps state =
     let no_tc = get_bool_option "coq:no_tc" in
     let keepunivs = get_bool_option "coq:keepunivs" in
     let redflags = get_redflags_option () in
+    let algunivs = get_bool_option "coq:keepalgunivs" in
     make_options ~hoas_holes ~local ~warn ~depr ~primitive ~failsafe ~ppwidth
       ~pp ~pplevel ~using ~inline ~uinstance ~universe_decl ~reversible ~keepunivs
-      ~redflags ~no_tc
-
+      ~redflags ~no_tc ~algunivs
 let mk_coq_context ~options state =
   let env = get_global_env state in
   let section = section_ids env in
@@ -1452,7 +1471,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
@@ -1962,7 +1984,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/rocq_elpi_HOAS.mli

@@ -48,6 +48,7 @@ type options = {
   keepunivs : bool option;
   redflags : RedFlags.reds option;
   no_tc: bool option;
+  algunivs : bool option;
 }
 
 type 'a coq_context = {
@@ -154,7 +155,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
@@ -197,7 +198,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