| Age | Commit message (Collapse) | Author |
|---|
|
We use an option type instead of returning a pair with a boolean. Indeed, the
boolean being true was always indicating that the returned value was unchanged.
The previous API was somewhat error-prone, and I don't understand why it was
designed this way in the first place.
|
|
|
|
|
|
|
|
|
|
In #6092, `global_reference` was moved to `kernel`. It makes sense to
go further and use the current kernel style for names.
This has a good effect on the dependency graph, as some core modules
don't depend on library anymore.
A question about providing equality for the GloRef module remains, as
there are two different notions of equality for constants. In that
sense, `KerPair` seems suspicious and at some point it should be
looked at.
|
|
We bootstrap the circular evar_map <-> econstr dependency by moving
the internal EConstr.API module to Evd.MiniEConstr. Then we make the
Evd functions use econstr.
|
|
|
|
|
|
|
|
When comparing 2 irrelevant universes [u] and [v] we add a "weak
constraint" [UWeak(u,v)] to the UState. Then at minimization time a
weak constraint between unrelated universes where one is flexible
causes them to be unified.
|
|
|
|
|
|
In Reductionops.infer_conv we did not have enough information to
properly try to unify irrelevant universes. This requires changing the
Reduction.universe_compare type a bit.
|
|
Previously [fun x : Ind@{i} => x : Ind@{j}] with Ind some cumulative
inductive would try to generate a constraint [i = j] and use
cumulativity only if this resulted in an inconsistency. This is
confusingly different from the behaviour with [Type] and means
cumulativity can only be used to lift between universes related by
strict inequalities. (This isn't a kernel restriction so there might
be some workaround to send the kernel the right constraints, but
not in a nice way.)
See modified test for more details of what is now possible.
Technical notes:
When universe constraints were inferred by comparing the shape of
terms without reduction, cumulativity was not used and so too-strict
equality constraints were generated. Then in order to use cumulativity
we had to make this comparison fail to fall back to full conversion.
When unifiying 2 instances of a cumulative inductive type, if there
are any Irrelevant universes we try to unify them if they are
flexible.
|
|
Following up on #6791, we remove support refolding in reduction.
We also update a test case that was not properly understood, see the
discussion in #6895.
|
|
|
|
|
|
|
|
|
|
|
|
The part in Reduction should be semantics preserving, but Reductionops
only tried cumulativity if equality fails. This is probably wrong so I
changed it.
|
|
|
|
|
|
arguments.
|
|
|
|
This is a follow-up on 866b449c497933a3ab1185c194d8d33a86c432f2.
|
|
|
|
New module introduced in OCaml 4.05 I think, can create problems when
linking with the OCaml toplevel for `Drop`.
|
|
This was dead code, probably due to the fact it was once shared with the
kernel stack type.
|
|
It was actually not used. The only place generating one was easily writable
without it.
|
|
Extending terms is notoriously difficult. We try to get more help from
the compiler by making sure such an extension will trigger non
exhaustive pattern matching warnings.
|
|
|
|
|
|
The message is the "Conversion test raised an anomaly" one.
|
|
We do up to `Term` which is the main bulk of the changes.
|
|
This will allow to merge back `Names` with `API.Names`
|
|
The code from Universes what essentially a duplicate of the one from EConstr,
but they were copied for historical reasons. Now, this is not useful anymore,
so that we remove the implementation from Universes and rely on the one from
EConstr.
|
|
|
|
|
|
|
|
This function was lurking around, waiting to bite anybody willing to use it.
We use instead a better API, correct and much less error-prone.
|
|
This function breaks the abstraction barrier of abstract universe contexts,
as it provides a way to observe the bound names of such a context. We remove
all the uses that can be easily get rid of with the current API.
|
|
|
|
|
|
|
|
Except I have disabled the minimization of universes after sections as
it seems to interfere with the STM machinery causing files like
test-suite/vio/print.v to loop when processed asynchronously.
This is very peculiar and needs more investigation as the aforementioned
file does not have any sections or any universe polymorphic definitions!
commit fc785326080b9451eb4700b16ccd3f7df214e0ed
Author: Amin Timany <amintimany@gmail.com>
Date: Mon Apr 24 17:14:21 2017 +0200
Revert STL to monomorphic
commit 62b573fb13d290d8fe4c85822da62d3e5e2a6996
Author: Amin Timany <amintimany@gmail.com>
Date: Mon Apr 24 17:02:42 2017 +0200
Try unifying universes before apply subtyping
commit ff393742c37b9241c83498e84c2274967a1a58dc
Author: Amin Timany <amintimany@gmail.com>
Date: Sun Apr 23 13:49:04 2017 +0200
Compile more of STL with universe polymorphism
commit 5c831b41ebd1fc32e2dd976697c8e474f48580d6
Author: Amin Timany <amintimany@gmail.com>
Date: Tue Apr 18 21:26:45 2017 +0200
Made more progress on compiling the standard library
commit b8550ffcce0861794116eb3b12b84e1158c2b4f8
Author: Amin Timany <amintimany@gmail.com>
Date: Sun Apr 16 22:55:19 2017 +0200
Make more number theoretic modules monomorphic
commit 29d126d4d4910683f7e6aada2a25209151e41b10
Author: Amin Timany <amintimany@gmail.com>
Date: Fri Apr 14 16:11:48 2017 +0200
WIP more of standard library compiles
Also: Matthieu fixed a bug in rewrite system which was faulty when
introducing new morphisms (Add Morphism) command.
commit 23bc33b843f098acaba4c63c71c68f79c4641f8c
Author: Amin Timany <amintimany@gmail.com>
Date: Fri Apr 14 11:39:21 2017 +0200
WIP: more of the standard library compiles
We have implemented convertibility of constructors up-to mutual
subtyping of their corresponding inductive types. This is similar to
the behavior of template polymorphism.
commit d0abc5c50d593404fb41b98d588c3843382afd4f
Author: Amin Timany <amintimany@gmail.com>
Date: Wed Apr 12 19:02:39 2017 +0200
WIP: trying to get the standard library compile with universe polymorphism
We are trying to prune universes after section ends. Sections add a
load of universes that are not appearing in the body, type or the
constraints.
|
|
|
|
|
|
|
