Skip to content

Commit

Permalink
✨ Add coq.univ.super
Browse files Browse the repository at this point in the history
  • Loading branch information
@ecranceMERCE
ecranceMERCE committed Nov 18, 2022
1 parent aa3f4b4 commit 687f9d9
Show file tree
Hide file tree
Showing 2 changed files with 17 additions and 84 deletions.
93 changes: 9 additions & 84 deletions coq-builtin.elpi
View file
Original file line number Diff line number Diff line change
Expand Up @@ -379,15 +379,12 @@ macro @ppmost! :- get-option "coq:pp" "most". % printing most of contents
macro @pplevel! N :- get-option "coq:pplevel" N. % printing precedence (for parentheses)

macro @keepunivs! :- get-option "coq:keepunivs" tt. % skeletons elaboration
macro @dropunivs! :- get-option "coq:keepunivs" ff. % add-indt/add-const

macro @using! S :- get-option "coq:using" S. % like the #[using=S] attribute

macro @inline-at! N :- get-option "coq:inline" (coq.inline.at N). % like Inline(N)
macro @inline! N :- get-option "coq:inline" coq.inline.default. % like

macro @redflags! F :- get-option "coq:redflags" F. % for whd & co

% both arguments are strings eg "8.12.0" "use foo instead"
macro @deprecated! Since Msg :-
get-option "coq:deprecated" (pr Since Msg).
Expand Down Expand Up @@ -669,7 +666,7 @@ external pred coq.env.const i:constant, o:option term, o:term.
external pred coq.env.const-body i:constant, o:option term.

% [coq.env.primitive? GR] tests if GR is a primitive constant (like uin63
% addition) or a primitive type (like uint63)
% addition)
external pred coq.env.primitive? i:constant.

% [coq.locate-module ModName ModPath] locates a module. It's a fatal error
Expand All @@ -680,17 +677,9 @@ external pred coq.locate-module i:id, o:modpath.
% error if ModName cannot be located. *E*
external pred coq.locate-module-type i:id, o:modtypath.

% Contents of a module
kind module-item type.
type submodule modpath -> list module-item -> module-item.
type module-type modtypath -> module-item.
type gref gref -> module-item.
type module-functor modpath -> list modtypath -> module-item.
type module-type-functor modtypath -> list modtypath -> module-item.

% [coq.env.module MP Contents] lists the contents of a module (recurses on
% submodules) *E*
external pred coq.env.module i:modpath, o:list module-item.
external pred coq.env.module i:modpath, o:list gref.

% [coq.env.module-type MTP Entries] lists the items made visible by module
% type (does not recurse on submodules) *E*
Expand All @@ -710,10 +699,6 @@ external pred coq.env.dependencies i:gref, i:modpath, o:coq.gref.set.
external pred coq.env.transitive-dependencies i:gref, i:modpath,
o:coq.gref.set.

% [coq.env.term-dependencies T S] Computes all the grefs S occurring in the
% term T
external pred coq.env.term-dependencies i:term, o:coq.gref.set.

% [coq.env.current-path Path] lists the current module path
external pred coq.env.current-path o:list string.

Expand Down Expand Up @@ -757,8 +742,6 @@ external pred coq.env.current-path o:list string.
% - @using! (default: section variables actually used)
% - @univpoly! (default unset)
% - @udecl! (default unset)
% - @dropunivs! (default: false, drops all universe constraints from the
% store after the definition)
%
external pred coq.env.add-const i:id, i:term, i:term, i:opaque?,
o:constant.
Expand All @@ -781,8 +764,6 @@ external pred coq.env.add-section-variable i:id, i:term, o:constant.

% [coq.env.add-indt Decl I] Declares an inductive type.
% Supported attributes:
% - @dropunivs! (default: false, drops all universe constraints from the
% store after the definition)
% - @primitive! (default: false, makes records primitive)
external pred coq.env.add-indt i:indt-decl, o:inductive.

Expand All @@ -794,12 +775,6 @@ type coq.inline.no coq.inline. % Coq's [no inline] (aka !)
type coq.inline.default coq.inline. % The default, can be omitted
type coq.inline.at int -> coq.inline. % Coq's [inline at <num>]

% [coq.env.fresh-global-id ID FID] Generates an id FID which is fresh in
% the current module and looks similar to ID, i.e. it is ID concatenated
% with a number, starting from 1.
% [coq.env.fresh-global-id X X] can be used to check if X is taken
external pred coq.env.fresh-global-id i:id, o:id.

external pred coq.env.begin-module-functor % Starts a functor *E*
i:id, % The name of the functor
i:option modtypath, % Its module type
Expand Down Expand Up @@ -969,6 +944,9 @@ typeabbrev univ.variable (ctype "univ.variable").
% [coq.univ.variable U L] relates a univ.variable L to a univ U
external pred coq.univ.variable o:univ, o:univ.variable.

% [coq.univ.super U U1] relates a univ U to its successor U1
external pred coq.univ.super i:univ, o:univ.

% [coq.univ.variable.constraints L CL] gives the list of constraints on L.
% Can be used to craft a strict upoly-decl
external pred coq.univ.variable.constraints i:univ.variable,
Expand Down Expand Up @@ -1380,62 +1358,15 @@ external pred coq.elaborate-skeleton i:term, o:term, o:term, o:diagnostic.
external pred coq.elaborate-ty-skeleton i:term, o:sort, o:term,
o:diagnostic.

% -- Coq's reduction flags ------------------------------------

% Flags for lazy, cbv, ... reductions
kind coq.redflag type.
type coq.redflags.beta coq.redflag.
type coq.redflags.delta coq.redflag. % if set then coq.redflags.const disables unfolding
type coq.redflags.match coq.redflag.
type coq.redflags.fix coq.redflag.
type coq.redflags.cofix coq.redflag.
type coq.redflags.zeta coq.redflag.
type coq.redflags.const constant ->
coq.redflag. % enable/disable unfolding

% Set of flags for lazy, cbv, ... reductions
typeabbrev coq.redflags (ctype "coq.redflags").

type coq.redflags.all coq.redflags.
type coq.redflags.allnolet coq.redflags.
type coq.redflags.beta coq.redflags.
type coq.redflags.betadeltazeta coq.redflags.
type coq.redflags.betaiota coq.redflags.
type coq.redflags.betaiotazeta coq.redflags.
type coq.redflags.betazeta coq.redflags.
type coq.redflags.delta coq.redflags.
type coq.redflags.zeta coq.redflags.
type coq.redflags.nored coq.redflags.

% [coq.redflags.add Flags Options NewFlags] Updates reduction Flags by
% adding Options
external pred coq.redflags.add i:coq.redflags, i:list coq.redflag,
o:coq.redflags.

% [coq.redflags.sub Flags Options NewFlags] Updates reduction Flags by
% removing Options
external pred coq.redflags.sub i:coq.redflags, i:list coq.redflag,
o:coq.redflags.

% -- Coq's reduction machines ------------------------------------

% [coq.reduction.lazy.whd T Tred] Puts T in weak head normal form.
% Supported attributes:
% - @redflags! (default coq.redflags.all)
external pred coq.reduction.lazy.whd i:term, o:term.
% [coq.reduction.lazy.whd_all T Tred] Puts T in weak head normal form
external pred coq.reduction.lazy.whd_all i:term, o:term.

% [coq.reduction.lazy.norm T Tred] Puts T in normal form.
% Supported attributes:
% - @redflags! (default coq.redflags.all)
% [coq.reduction.lazy.norm T Tred] Puts T in normal form
external pred coq.reduction.lazy.norm i:term, o:term.

% [coq.reduction.lazy.bi-norm T Tred] Puts T in normal form only reducing
% beta and iota redexes
external pred coq.reduction.lazy.bi-norm i:term, o:term.

% [coq.reduction.cbv.norm T Tred] Puts T in weak head normal form.
% Supported attributes:
% - @redflags! (default coq.redflags.all)
% [coq.reduction.cbv.norm T Tred] Puts T in weak head normal form
external pred coq.reduction.cbv.norm i:term, o:term.

% [coq.reduction.vm.norm T Ty Tred] Puts T in normal form. Its type Ty can
Expand Down Expand Up @@ -1465,12 +1396,6 @@ coq.reduction.vm.whd_all T TY R :-
coq.reduction.vm.norm T TY R.



pred coq.reduction.lazy.whd_all i:term, o:term.
coq.reduction.lazy.whd_all X Y :-
@redflags! coq.redflags.all => coq.reduction.lazy.whd X Y.


% -- Coq's conversion strategy tweaks --------------------------

% Strategy for conversion test
Expand Down
8 changes: 8 additions & 0 deletions src/coq_elpi_builtins.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2236,6 +2236,14 @@ phase unnecessary.|};
state, !: u, [])),
DocAbove);

MLCode(Pred("coq.univ.super",
In(univ,"U",
Out(univ,"U1",
Full(unit_ctx, "relates a univ U to its successor U1"))),
(fun u _ ~depth _ _ state ->
state, !: (Univ.Universe.super u), [])),
DocAbove);

MLCode(Pred("coq.univ",
InOut(B.ioarg id, "Name",
InOut(B.ioarg univ, "U",
Expand Down

0 comments on commit 687f9d9

Please sign in to comment.