aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/univ.ml
Commit message (Collapse)AuthorAge
* Simplification: cumulativity information is variance information.Gravatar Gaëtan Gilbert2018-02-10
| | | | | | | | | | | | | | | | | | | | | | | | | Since cumulativity of an inductive type is the universe constraints which make a term convertible with its universe-renamed copy, the only constraints we can get are between a universe and its copy. As such we do not need to be able to represent arbitrary constraints between universes and copied universes in a double-sized ucontext, instead we can just keep around an array describing whether a bound universe is covariant, invariant or irrelevant (CIC has no contravariant conversion rule). Printing is fairly obtuse and should be improved: when we print the CumulativityInfo we add marks to the universes of the instance: = for invariant, + for covariant and * for irrelevant. ie Record Foo@{i j k} := { foo : Type@{i} -> Type@{j} }. Print Foo. gives Cumulative Record Foo : Type@{max(i+1, j+1)} := Build_Foo { foo : Type@{i} -> Type@{j} } (* =i +j *k |= *)
* Moving some universe substitution code out of the kernel.Gravatar Pierre-Marie Pédrot2017-12-30
| | | | | | This code was not used at all inside the kernel, it was related to universe unification that happens in the upper layer. It makes more sense to put it somewhere upper.
* Do not hashcons universes beforehand.Gravatar Pierre-Marie Pédrot2017-09-01
| | | | | This should save a lot of useless reallocations and hashset crawling, which end up costing a lot.
* deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
|
* Fixing the checker w.r.t. wrongly used abstract universe contexts.Gravatar Pierre-Marie Pédrot2017-07-19
| | | | | | | | | | | It seems we were not testing the checker on cumulative inductive types, because judging from the code, it would just have exploded in anomalies. Before this patch, the checker was mixing De Bruijn indices with named variables, resulting in ill-formed universe contexts used throughout the checking of cumulative inductive types. This patch also gets rid of a lot of now dead code, and removes abstraction breaking code from the checker.
* Properly handling polymorphic inductive subtyping in the checker.Gravatar Pierre-Marie Pédrot2017-07-11
| | | | | This is the followup of the previous commit, this time implementing the correct algorithm in the checker.
* 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.
* Getting rid of simple calls to AUContext.instance.Gravatar Pierre-Marie Pédrot2017-07-11
| | | | | | 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.
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
|
* Enable the checking of ind subtyping in checkerGravatar Amin Timany2017-06-16
|
* Correct coqchk checking subtyping relation for inductivesGravatar Amin Timany2017-06-16
|
* Correct coqchk reductionGravatar 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
|
* 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
* 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.
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
|
* Univs: fix checker generating undeclared universes.Gravatar Matthieu Sozeau2015-10-02
|
* Univs: update checkerGravatar 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.
* Hconsing continuedGravatar Hugo Herbelin2015-08-02
|
* 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
|
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Fix checker's treatment of template polymorphicGravatar Matthieu Sozeau2015-01-06
| | | | | inductive instantiation, now using substitution of levels. Fixes the test-suite file coqchk/univ.
* Backporting the change in lists of universes to the checker.Gravatar Pierre-Marie Pédrot2014-12-18
|
* checker: Change in library on disk values, now using context_sets instead ofGravatar Matthieu Sozeau2014-12-17
| | | | constraints only.
* Ensuring the good invariants of hashcons table generation in the API.Gravatar Pierre-Marie Pédrot2014-12-17
|
* Remove unused substitution functions in checker.Gravatar Matthieu Sozeau2014-09-05
|
* Fix checker treatment of inductives using subst_instances instead of ↵Gravatar Matthieu Sozeau2014-09-05
| | | | subst_univs_levels.
* Removing dead code in checker/univ.ml.Gravatar Pierre-Marie Pédrot2014-06-10
|
* Removing explanations of universe inconsistencies from the checker. TheyGravatar Pierre-Marie Pédrot2014-06-10
| | | | were never used and were responsible for code duplication.
* Providing the checker with its own version of the Univ file.Gravatar Pierre-Marie Pédrot2014-06-10
I also took the opportunity to remove a lot of code not used by the checker.
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 00:43:09 +0000