| Age | Commit message (Collapse) | Author |
|---|
|
This work makes it possible to take advantage of a compact
representation for integers in the entire system, as opposed to only
in some reduction machines. It is useful for heavily computational
applications, where even constructing terms is not possible without such
a representation.
Concretely, it replaces part of the retroknowledge machinery with
a primitive construction for integers in terms, and introduces a kind of
FFI which maps constants to operators (on integers). Properties of these
operators are expressed as explicit axioms, whereas they were hidden in
the retroknowledge-based approach.
This has been presented at the Coq workshop and some Coq Working Groups,
and has been used by various groups for STM trace checking,
computational analysis, etc.
Contributions by Guillaume Bertholon and Pierre Roux <Pierre.Roux@onera.fr>
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
This has different behaviour if called on an applied Rel, not sure if
that ever happens.
|
|
|
|
|
|
The code to generate the legacy bodies is moved to its only user in
extraction.
It almost seems like we could remove it (ie no special extraction code
for primitive projection constants) but then we run into issues with
automatic unboxing eg `Record foo := { a : nat; b : a <= 5 }.` gets
extracted to `type foo = nat` and (if we remove the special code) `let
a = a`.
|
|
|
|
Since it returns an Id.t and not a Pp.t.
|
|
|
|
|
|
|
|
|
|
comments.
|
|
This is a pre-requisite to use automated formatting tools such as
`ocamlformat`, also, there were quite a few places where the comments
had basically no effect, thus it was confusing for the developer.
p.s: Reading some comments was a lot of fun :)
|
|
Rename Univ.Level.{Qualid -> UGlobal}, remove Univ.Level.Id.
Remove the ability to split the argument of `Univ.Level.Level` into a
dirpath*int pair (except by going through string hacks like
detyping/pretyping(/funind) does).
Id.of_string_soft to turn unnamed universes into qualid is pushed up
to detyping. (TODO some followup PR clean up more)
This makes it pointless to have an opaque type for ints in
Univ.Level: it would only be used as argument to
Univ.Level.UGlobal.make, ie
~~~
open Univ.Level
let x = UGlobal.make dp (Id.make n)
(* vs *)
let x = UGlobal.make dp n
~~~
Remaining places which create levels from ints are various hacks (eg
the dummy in inductive.ml, the Type.n universes in ugraph
sort_universes) and univgen.
UnivGen does have an opaque type for ints used as univ ids since they
get manipulated by the stm.
NB: build breaks due to ocamldep issue if UGlobal is named Global instead.
|
|
Remote counters were trying to build universe levels (as opposed to
simple integers), but did not have access to the right dirpath at
construction time. We fix it by constructing the level only at use time,
and we introduce some abstractions for qualified and unqualified level
names.
|
|
|
|
|
|
This makes setting the option outside of the synchronized summary impossible.
|
|
write_function
|
|
|
|
|
|
This introduces the warning “not-a-class” in the “typeclasses” category.
|
|
cleanups
|
|
|
|
(same for solve_remaining_evars)
This is the standard way to use these functions, with 1 exception in
Unification.
|
|
The use of a term is not needed for the fast typing algorithm of the
application case, so this tweak brings the best of both worlds.
|
|
There is little point to this as the type is dependent on an open value and
is never computed further.
|
|
|
|
This is documented in dev/doc/changes.md.
|
|
|
|
|
|
|
|
There are a couple left which seem OK.
|
|
Enabled by previous commit about Heads.
|
|
This avoids using Projection.constant in kind_of_head, which then
allows compute_head to not check whether the constant is a
compatibility definition (as in that case its body is [fun ... => x.(p)]).
Thus Heads stops caring about the compatibility projection system.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
functions
|
|
|
|
This can be useful to avoid [Typing.type_of (App (f,args))] when
working with universe polymorphism.
|
|
This emphasizes that it works only on inductive types.
Also, the name is_template_polymorphic will be reused for a more
general version.
|
|
|
|
Made possible by the previous commit passing ~evars to
check_hyps_inclusion.
|
|
|
