aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/univ.ml
Commit message (Collapse)AuthorAge
* deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
|
* The only abstraction-breaking function in Univ is now AUContext.instance.Gravatar Pierre-Marie Pédrot2017-07-13
|
* Cleaning up the implementation of module subtyping in the kernel.Gravatar Pierre-Marie Pédrot2017-07-11
| | | | | | | | We export a function in UGraph to check that a polymorphic instance is a subtype of another, instead of rolling up our own in module code. We also add a few tests for module subtyping in presence of polymorphic constants.
* Less footguns in universe handling: remove subst_instance_context.Gravatar Pierre-Marie Pédrot2017-07-11
| | | | | 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.
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
|
* Simplify Univ.mlGravatar Amin Timany2017-06-16
|
* Squashed commit of the following:Gravatar Amin Timany2017-06-16
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* Check subtyping of inductive types in KernelGravatar Amin Timany2017-06-16
|
* Using UInfoInd for universes in inductive typesGravatar Amin Timany2017-06-16
| | | | | | | | | It stores both universe constraints and subtyping information for blocks of inductive declarations. At this stage the there is no inference or checking implemented. The subtyping information simply encodes equality of levels for the condition of subtyping.
* New datastructure for universes of inductive typesGravatar Amin Timany2017-06-16
|
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
| | | | | | | | | | | | | | | | | As per https://github.com/coq/coq/pull/716#issuecomment-305140839 Partially using ```bash git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i ``` and ```bash git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i ``` The rest were manually edited by looking at the results of ```bash git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less ```
* Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
|
* Document changesGravatar Matthieu Sozeau2016-12-02
|
* Slightly more efficient [Univ.super] implemGravatar Matthieu Sozeau2016-11-30
|
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵Gravatar Pierre Letouzey2016-07-03
| | | | | | module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-30
|\
| * A patch renaming equal into eq in the module dealing withGravatar Hugo Herbelin2016-03-22
| | | | | | | | | | hash-consing, so as to avoid having too many kinds of equalities with same name.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| |
* | Universes algorithm : clarified commentsGravatar Jacques-Henri Jourdan2016-01-17
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-29
|\|
| * Univs: entirely disallow instantiation of polymorphic constants withGravatar Matthieu Sozeau2015-11-27
| | | | | | | | | | | | | | | | | | Prop levels. As they are typed assuming all variables are >= Set now, and this was breaking an invariant in typing. Only one instance in the standard library was used in Hurkens, which can be avoided easily. This also avoids displaying unnecessary >= Set constraints everywhere.
| * Fix output of universe arcs. (Fix bug #4422)Gravatar Guillaume Melquiond2015-11-23
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-11-05
|\|
| * Univs: update refman, better printers for universe contexts.Gravatar Matthieu Sozeau2015-11-04
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-29
|\|
| * Adds support for the virtual machine to perform reduction of universe ↵Gravatar Gregory Malecha2015-10-28
| | | | | | | | | | | | | | | | polymorphic definitions. - This implementation passes universes in separate arguments and does not eagerly instanitate polymorphic definitions. - This means that it pays no cost on monomorphic definitions.
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-10-09
|\|
| * Univs: fix bug #3807Gravatar Matthieu Sozeau2015-10-08
| | | | | | | | Add a flag to disallow minimization to set
* | Splitting kernel universe code in two modules.Gravatar Pierre-Marie Pédrot2015-10-06
|/ | | | | 1. The Univ module now only cares about definitions about universes. 2. The UGraph module contains the algorithm responsible for aciclicity.
* Univs: fix bug #4288, Print Sorted generated backward < constraints.Gravatar Matthieu Sozeau2015-10-05
|
* Univs: fix bug #4251, handling of template polymorphic constants.Gravatar Matthieu Sozeau2015-10-02
|
* Univs (kernel) adapt to new invariantsGravatar Matthieu Sozeau2015-10-02
| | | | | | Remove predicative flag and adapt to new invariant where every universe must be declared, ensuring it is >= Set, safe_repr is not necessary anymore.
* Forcing i > Set for global universes (incomplete)Gravatar Matthieu Sozeau2015-10-02
|
* Universes: enforce Set <= i for all Type occurrences.Gravatar Matthieu Sozeau2015-10-02
|
* Reverting 16 last commits, committed mistakenly using the wrong push command.Gravatar Hugo Herbelin2015-08-02
| | | | | | | | | | | | | | | | | | | | | | Sorry so much. Reverted: 707bfd5719b76d131152a258d49740165fbafe03. 164637cc3a4e8895ed4ec420e300bd692d3e7812. b9c96c601a8366b75ee8b76d3184ee57379e2620. 21e41af41b52914469885f40155702f325d5c786. 7532f3243ba585f21a8f594d3dc788e38dfa2cb8. 27fb880ab6924ec20ce44aeaeb8d89592c1b91cd. fe340267b0c2082b3af8bc965f7bc0e86d1c3c2c. d9b13d0a74bc0c6dff4bfc61e61a3d7984a0a962. 6737055d165c91904fc04534bee6b9c05c0235b1. 342fed039e53f00ff8758513149f8d41fa3a2e99. 21525bae8801d98ff2f1b52217d7603505ada2d2. b78d86d50727af61e0c4417cf2ef12cbfc73239d. 979de570714d340aaab7a6e99e08d46aa616e7da. f556da10a117396c2c796f6915321b67849f65cd. d8226295e6237a43de33475f798c3c8ac6ac4866. fdab811e58094accc02875c1f83e6476f4598d26.
* A patch renaming equal into eq in the module dealing withGravatar Hugo Herbelin2015-08-02
| | | | | hash-consing, so as to avoid having too many kinds of equalities with same name.
* Modules: fix bug #4294Gravatar Matthieu Sozeau2015-07-16
| | | | | We were throwing away constraints from 'with Definition' in module type ascriptions.
* Further simplification of the graph traversal in Univ.Gravatar Pierre-Marie Pédrot2015-07-01
| | | | | | | | We passed the arc to be marked as visited to the functions pushing the neighbours on the remaining stack, but this can be actually done before pushing them, as the [process_le] and [process_lt] functions do not rely on the visited flag. This exposes more clearly the invariants of the algorithm.
* Less closures makes the GC happy.Gravatar Pierre-Marie Pédrot2015-06-24
| | | | | We lambda-lift by hand the graph traversal functions in Univ to allocate less closures.
* Less closures makes the GC happy.Gravatar Pierre-Marie Pédrot2015-06-23
|
* Fixing bug #4019, and checker blow-up at once.Gravatar Pierre-Marie Pédrot2015-02-11
|
* Clarifying the implementation of universe hashconsing.Gravatar Pierre-Marie Pédrot2015-02-11
|
* Fixing bug #3931.Gravatar Pierre-Marie Pédrot2015-01-28
|
* Univs: proper printing of global and local universe names (onlyGravatar Matthieu Sozeau2015-01-17
| | | | printing functions touched in the kernel).
* Make native compiler handle universe polymorphic definitions.Gravatar Maxime Dénès2015-01-17
| | | | | One remaining issue: aliased constants raise an anomaly when some unsubstituted universe variables remain. VM may suffer from the same problem.
* Correct restriction of vm_compute when handling universe polymorphicGravatar Matthieu Sozeau2015-01-15
| | | | | | | | | | definitions. Instead of failing with an anomaly when trying to do conversion or computation with the vm's, consider polymorphic constants as being opaque and keep instances around. This way the code is still correct but (obviously) incomplete for polymorphic definitions and we avoid introducing an anomaly. The patch does nothing clever, it only keeps around instances with constants/inductives and compile constant bodies only for non-polymorphic definitions.
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Aligning printing of universe constraints.Gravatar Hugo Herbelin2015-01-07
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 22:10:21 +0000