From a5d5a91f5d26911d77cf7b849458c0e956e7e570 Mon Sep 17 00:00:00 2001 From: Lucie Date: Thu, 17 Apr 2025 14:00:25 +0200 Subject: [PATCH 1/3] Add coq.univ.alg-super, @keep-alg-univs! This is https://github.com/LPCIC/coq-elpi/pull/585 rebased on master. Co-Authored-By: Enrico Tassi Co-Authored-By: Enzo Crance Co-Authored-By: Cyril Cohen --- Changelog.md | 8 ++++ builtin-doc/coq-builtin.elpi | 9 +++- elpi/coq-HOAS.elpi | 2 + src/rocq_elpi_HOAS.ml | 86 ++++++++++++++++++++++++++++++----- src/rocq_elpi_HOAS.mli | 5 +- src/rocq_elpi_builtins.ml | 88 +++++++++++++++++++++--------------- tests-stdlib/test_API_env.v | 2 +- tests/test_API_elaborate.v | 1 - tests/test_HOAS.v | 21 +++++++++ 9 files changed, 167 insertions(+), 55 deletions(-) diff --git a/Changelog.md b/Changelog.md index a403dde1a..1ebe585f6 100644 --- a/Changelog.md +++ b/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. diff --git a/builtin-doc/coq-builtin.elpi b/builtin-doc/coq-builtin.elpi index 7f1af9eb9..f24f79794 100644 --- a/builtin-doc/coq-builtin.elpi +++ b/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. diff --git a/elpi/coq-HOAS.elpi b/elpi/coq-HOAS.elpi index fbb938162..9e5494c96 100644 --- a/elpi/coq-HOAS.elpi +++ b/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 diff --git a/src/rocq_elpi_HOAS.ml b/src/rocq_elpi_HOAS.ml index ef5d7dfe7..a17ece7c2 100644 --- a/src/rocq_elpi_HOAS.ml +++ b/src/rocq_elpi_HOAS.ml @@ -364,6 +364,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 +383,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 +424,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 @@ -1074,14 +1129,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 +1360,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 +1511,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 +2024,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 -> diff --git a/src/rocq_elpi_HOAS.mli b/src/rocq_elpi_HOAS.mli index 70f2d7e7b..99a609b23 100644 --- a/src/rocq_elpi_HOAS.mli +++ b/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 diff --git a/src/rocq_elpi_builtins.ml b/src/rocq_elpi_builtins.ml index 49e9fb049..bc7070ea4 100644 --- a/src/rocq_elpi_builtins.ml +++ b/src/rocq_elpi_builtins.ml @@ -15,7 +15,7 @@ module B = struct let ioarg_any = API.BuiltInPredicate.ioarg_any let ioargC = API.BuiltInPredicate.ioargC let ioargC_flex = API.BuiltInPredicate.ioargC_flex - let ioarg_flex = API.BuiltInPredicate.ioarg_flex + (* let ioarg_flex = API.BuiltInPredicate.ioarg_flex *) let ioarg_poly s = { ioarg_any with API.Conversion.ty = API.Conversion.TyName s } end module Pred = API.BuiltInPredicate @@ -403,20 +403,20 @@ let cs_pattern = K("cs-default","",N, B Default_cs, M (fun ~ok ~ko -> function Default_cs -> ok | _ -> ko ())); - K("cs-sort","",A(sort,N),build_of_sort,match_of_sort) + K("cs-sort","",CA(sort,N),build_of_sort,match_of_sort) ] -} |> CConv.(!<) +} let cs_instance = let open Conv in let open API.AlgebraicData in let open Structures.CSTable in declare { ty = TyName "cs-instance"; doc = "Canonical Structure instances: (cs-instance Proj ValPat Inst)"; pp = (fun fmt { solution } -> Format.fprintf fmt "@[%a@]" Pp.pp_with ((Printer.pr_global solution))); constructors = [ - K("cs-instance","",A(gref,A(cs_pattern,A(gref,N))), + K("cs-instance","",A(gref,CA(cs_pattern,A(gref,N))), B (fun p v i -> assert false), M (fun ~ok ~ko { solution; value; projection } -> ok projection value solution)) ] -} |> CConv.(!<) +} type type_class_instance = { @@ -2400,7 +2400,7 @@ denote the same x as before.|}; match p, c with | _, Data (Variable c) -> raise No_clause | Data p, Data (Constant c) -> - if Constant.equal (Projection.constant p) c then ?: None +? None +! Names.Projection.(arg p + npars p) else raise No_clause + if Environ.QConstant.equal coq_context.env (Projection.constant p) c then ?: None +? None +! Names.Projection.(arg p + npars p) else raise No_clause | NoData, NoData -> U.type_error "coq.env.primitive-projection?: got no input data" | Data p, NoData -> ?: None +! (Constant (Projection.constant p)) +! Names.Projection.(arg p + npars p) | NoData, Data (Constant c) -> @@ -2448,40 +2448,46 @@ The different data types stay, since Coq will eventually become able to handle algebraic universes consistently, making this purging phase unnecessary.|}; MLData univ; - MLData sort; + MLDataC sort; 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 -> + CInOut(B.ioargC_flex sort, "S1", + CInOut(B.ioargC_flex sort, "S2", + Full(global, "constrains S1 <= S2"))), + (fun u1 u2 ~depth { options } _ -> grab_global_env "coq.sort.leq" + (fun state -> match u1, u2 with | Data u1, Data u2 -> - if Sorts.equal u1 u2 then state, !: u1 +! u2,[] + if Sorts.equal u1 u2 then Univ.ContextSet.empty, 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 + Univ.ContextSet.empty, 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 -> + CInOut(B.ioargC_flex sort, "S1", + CInOut(B.ioargC_flex sort, "S2", + Full(global, "constrains S1 = S2"))), + (fun u1 u2 ~depth { options } _ -> grab_global_env "coq.sort.eq" + (fun state -> match u1, u2 with | Data u1, Data u2 -> - if Sorts.equal u1 u2 then state, !: u1 +! u2,[] + if Sorts.equal u1 u2 then Univ.ContextSet.empty, state, !: u1 +! u2,[] else - 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"))), + let state, u2 = if true (* options.algunivs != Some true *) + then purge_algebraic_univs_sort state (EConstr.ESorts.make u2) + else state, u2 in + Univ.ContextSet.empty, add_universe_constraint state (constraint_eq u1 u2), !: u1 +! u2, [] + | _ -> err Pp.(str"coq.sort.eq: called with _ as argument")))), DocAbove); MLCode(Pred("coq.sort.sup", - InOut(B.ioarg_flex sort, "S1", - InOut(B.ioarg_flex sort, "S2", - Full(unit_ctx, "constrains S2 = S1 + 1"))), + CInOut(B.ioargC_flex sort, "S1", + CInOut(B.ioargC_flex sort, "S2", + Full(global, "constrains S2 = S1 + 1"))), (fun u1 u2 ~depth _ _ state -> match u1, u2 with | Data u1, Data u2 -> univ_super state u1 u2, !: u1 +! u2, [] @@ -2489,10 +2495,10 @@ phase unnecessary.|}; DocAbove); MLCode(Pred("coq.sort.pts-triple", - InOut(B.ioarg_flex sort, "S1", - InOut(B.ioarg_flex sort, "S2", - Out(sort, "S3", - Full(unit_ctx, "constrains S3 = sort of product with domain in S1 and codomain in S2")))), + CInOut(B.ioargC_flex sort, "S1", + CInOut(B.ioargC_flex sort, "S2", + COut(sort, "S3", + Full(global, "constrains S3 = sort of product with domain in S1 and codomain in S2")))), (fun u1 u2 _ ~depth _ _ state -> match u1, u2 with | Data u1, Data u2 -> let state, u3 = univ_product state u1 u2 in state, !: u1 +! u2 +! u3, [] @@ -2517,6 +2523,14 @@ phase unnecessary.|}; state, !: u, [])), DocAbove); + MLCode(Pred("coq.univ.alg-super", + In(univ,"U", + Out(univ,"V", + Full(unit_ctx, "relates a univ U to its algebraic successor V, that is U+1 and not any V s.t. U < V"))), + (fun u _ ~depth _ _ state -> + state, !: (Univ.Universe.super u), [])), + DocAbove); + MLCode(Pred("coq.univ", InOut(B.ioarg id, "Name", InOut(B.ioarg univ, "U", @@ -2768,8 +2782,8 @@ declared as cumulative.|}; LPDoc "-- Databases (TC, CS, Coercions) ------------------------------------"; - MLData cs_pattern; - MLData cs_instance; + MLDataC cs_pattern; + MLDataC cs_instance; MLCode(Pred("coq.CS.declare-instance", In(gref, "GR", @@ -2782,7 +2796,7 @@ Supported attributes: DocAbove); MLCode(Pred("coq.CS.db", - Out(list cs_instance, "Db", + COut(CConv.(!>>) list cs_instance, "Db", Read(global,"reads all instances")), (fun _ ~depth _ _ _ -> !: (Structures.CSTable.(entries ())))), @@ -2790,8 +2804,8 @@ Supported attributes: MLCode(Pred("coq.CS.db-for", In(B.unspec gref, "Proj", - In(B.unspec cs_pattern, "Value", - Out(list cs_instance, "Db", + CIn(B.unspecC cs_pattern, "Value", + COut(CConv.(!>>) list cs_instance, "Db", Read(global,"reads all instances for a given Projection or canonical Value, or both")))), (fun proj value _ ~depth _ _ state -> let env = get_global_env state in @@ -3399,7 +3413,7 @@ Universe constraints are put in the constraint store.|})))), MLCode(Pred("coq.typecheck-ty", CIn(term, "Ty", - InOut(B.ioarg sort, "U", + CInOut(B.ioargC sort, "U", InOut(B.ioarg B.diagnostic, "Diagnostic", Full (proof_context, {|typchecks a type Ty returning its universe U. If U is provided, then @@ -3522,7 +3536,7 @@ Supported attributes: MLCode(Pred("coq.elaborate-ty-skeleton", CIn(term_skeleton, "T", - Out(sort, "U", + COut(sort, "U", COut(term, "E", InOut(B.ioarg B.diagnostic, "Diagnostic", Full (proof_context,{|elabotares T expecting it to be a type of sort U. diff --git a/tests-stdlib/test_API_env.v b/tests-stdlib/test_API_env.v index d60655fdb..2d4a65bee 100644 --- a/tests-stdlib/test_API_env.v +++ b/tests-stdlib/test_API_env.v @@ -191,7 +191,7 @@ Elpi Query lp:{{ lp:t lp:y true }}) , constructor "K2x" (parameter "y" _ {{nat}} y\ arity {{ lp:t lp:y false }}) ]), - coq.typecheck-indt-decl D ok, + std.assert-ok! (coq.typecheck-indt-decl D) "illtyped", coq.env.add-indt D _. }}. diff --git a/tests/test_API_elaborate.v b/tests/test_API_elaborate.v index ff52c3d4f..d4e2fefb8 100644 --- a/tests/test_API_elaborate.v +++ b/tests/test_API_elaborate.v @@ -131,7 +131,6 @@ wrong constant:, *) - Elpi test.API2 Record ind2 (A : T1) := { fld1 : A; fld2 : fld1 = fld1; diff --git a/tests/test_HOAS.v b/tests/test_HOAS.v index 5165c09ba..04211fd20 100644 --- a/tests/test_HOAS.v +++ b/tests/test_HOAS.v @@ -647,3 +647,24 @@ coq.env.add-indt D _, coq.env.end-module _ }}. +Elpi Command Comm. +Elpi Accumulate lp:{{ + main [indt-decl X] :- coq.say X, + coq.env.add-indt X _. +}}. +Elpi Comm Class c {A : Type} (x : A -> A). +Goal c S. Abort. + +Elpi Query lp:{{ + coq.typecheck-ty (sort (typ X)) A ok, + A = typ TX, + not(coq.univ.alg-super X TX), + coq.say X ":" TX, + @keep-alg-univs! => coq.typecheck-ty (sort (typ Y)) B ok, + B = typ TY, + coq.say Y ":" TY, + coq.univ.alg-super Y TY, + coq.say Y ":" TY + . + +}}. From f08b8eb70c34ee6bf117938a25191ca8db1615ec Mon Sep 17 00:00:00 2001 From: Lucie Date: Fri, 18 Apr 2025 17:22:19 +0200 Subject: [PATCH 2/3] Deduplicate `sort` and others --- src/rocq_elpi_HOAS.ml | 56 +++++++------------------------------------ 1 file changed, 8 insertions(+), 48 deletions(-) diff --git a/src/rocq_elpi_HOAS.ml b/src/rocq_elpi_HOAS.ml index a17ece7c2..921e17f54 100644 --- a/src/rocq_elpi_HOAS.ml +++ b/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 { @@ -477,6 +430,14 @@ let sort : (Sorts.t, _ coq_context, API.Data.constraints) API.ContextualConversi | _ -> 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 @@ -1107,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 From a1d6264802b6b79a4f974cf427187161301a12a9 Mon Sep 17 00:00:00 2001 From: Lucie Date: Fri, 18 Apr 2025 18:39:14 +0200 Subject: [PATCH 3/3] Get rid of `elpi.implication-precedence` warning --- tests/test_HOAS.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/test_HOAS.v b/tests/test_HOAS.v index 04211fd20..83d013d12 100644 --- a/tests/test_HOAS.v +++ b/tests/test_HOAS.v @@ -660,7 +660,7 @@ Elpi Query lp:{{ A = typ TX, not(coq.univ.alg-super X TX), coq.say X ":" TX, - @keep-alg-univs! => coq.typecheck-ty (sort (typ Y)) B ok, + (@keep-alg-univs! => coq.typecheck-ty (sort (typ Y)) B ok), B = typ TY, coq.say Y ":" TY, coq.univ.alg-super Y TY,