aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
Commit message (Collapse)AuthorAge
* checker Indtypes: remove unused argumentsGravatar Gaëtan Gilbert2018-07-03
|
* checker Modops strengthening: remove unused argument resolverGravatar Gaëtan Gilbert2018-07-03
|
* Subtyping.check_constant: remove unused module path argument.Gravatar Gaëtan Gilbert2018-07-03
|
* Inductive.extract_stack,filter_stack_domain: remove unused argumentsGravatar Gaëtan Gilbert2018-07-03
|
* Remove Sorts.contentsGravatar Gaëtan Gilbert2018-06-26
|
* Merge PR #7798: Remove hack skipping comparison of algebraic universes in ↵Gravatar Matthieu Sozeau2018-06-25
|\ | | | | | | subtyping.
* | Using more general information for primitive records.Gravatar Pierre-Marie Pédrot2018-06-23
| | | | | | | | | | This brings more compatibility with handling of mutual primitive records in the kernel.
* | Change the proj_ind field from MutInd.t to inductive.Gravatar Pierre-Marie Pédrot2018-06-23
| | | | | | | | | | This is a first step towards the acceptance of mutual record types in the kernel.
| * Remove hack skipping comparison of algebraic universes in subtyping.Gravatar Gaëtan Gilbert2018-06-22
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | When inferring [u <= v+k] I replaced the exception and instead add [u <= v]. This is trivially sound and it doesn't seem possible to have the one without the other (except specially for [Set <= v+k] which was already handled). I don't know an example where this used to fail and now succeeds (the point was to remove an anomaly, but the example ~~~ Module Type SG. Definition DG := Type. End SG. Module MG : SG. Definition DG := Type : Type. Fail End MG. ~~~ now fails with universe inconsistency. Fix #7695 (soundness bug!).
| * Remove enforce_leq from checkerGravatar Gaëtan Gilbert2018-06-21
|/
* Merge PR #7841: Remove CanaryGravatar Pierre-Marie Pédrot2018-06-19
|\
| * Remove Canary.Gravatar whitequark2018-06-18
| | | | | | | | This eliminates 3 uses of Obj from TCB.
* | Remove the proj_body field from the kernel.Gravatar Pierre-Marie Pédrot2018-06-17
| | | | | | | | | | | | | | | | | | | | | | | | | | | | This was completely wrong, such a term could not even be type-checked by the kernel as it was internally using a match construct over a negative record. They were luckily only used in upper layers, namley printing and extraction. Recomputing the projection body might be costly in detyping, but this only happens when the compatibility flag is turned on, which is not the default. Such flag is probably bound to disappear anyways. Extraction should be fixed though so as to define directly primitive projections, similarly to what has been done in native compute.
* | Remove the proj_eta field of the kernel.Gravatar Pierre-Marie Pédrot2018-06-17
| | | | | | | | | | | | This field was not used inside the kernel and not used in performance-critical code where caching is essential, so we extrude the code that computes it out of the kernel.
* | Getting rid of the const_proj field in the kernel.Gravatar Pierre-Marie Pédrot2018-06-17
|/ | | | | | This field used to signal that a constant was the compatibility eta-expansion of a primitive projections, but since a previous cleanup in the kernel it had become useless.
* Fix the checker by merely adapting the data structure.Gravatar Pierre-Marie Pédrot2018-06-07
| | | | | | | | | | Unluckily, this is completely wrong as we trust the inlined term to be well-typed in some unavailable environment. To start with, the checker should not even rely on substitutions as it does not trust functors, but it does anyways. I have thus commented this code as a useful backdoor for when Coq is used to implement the next blockchain Ponzi scheme. We really need to sort this out though.
* Merge PR #7552: Fix #7539: Checker does not properly handle negative ↵Gravatar Matthieu Sozeau2018-06-04
|\ | | | | | | coinductive types.
* | Reduce circular dependency constants <-> projectionsGravatar Gaëtan Gilbert2018-05-31
| | | | | | | | | | Instead of having the projection data in the constant data we have it independently in the environment.
* | Merge PR #7325: Fix #7323: coqchk puts polymorphic univs of inductive in ↵Gravatar Pierre-Marie Pédrot2018-05-25
|\ \ | | | | | | | | | global env
* \ \ Merge PR #7177: Unifying names of "smart" combinators + adding combinators ↵Gravatar Pierre-Marie Pédrot2018-05-24
|\ \ \ | | | | | | | | | | | | in CArray
| | * | Fix #7323: coqchk puts polymorphic univs of inductive in global envGravatar Gaëtan Gilbert2018-05-24
| |/ / |/| |
* | | Merge PR #7328: Fix #7327: coqchk subtyping of polymorphic constantsGravatar Pierre-Marie Pédrot2018-05-24
|\ \ \
* \ \ \ Merge PR #7317: Fix #6798: coqchk ignores ugraph when comparing constant ↵Gravatar Pierre-Marie Pédrot2018-05-24
|\ \ \ \ | | | | | | | | | | | | | | | instances
| | | * | Moving Rtree.smart_map into Rtree.Smart.map.Gravatar Hugo Herbelin2018-05-23
| | | | |
| | | * | Moving Option.smart_map to Option.Smart.map.Gravatar Hugo Herbelin2018-05-23
| | | | |
| | | * | Collecting List.smart_* functions into a module List.Smart.Gravatar Hugo Herbelin2018-05-23
| | | | |
| | | * | Collecting Array.smart_* functions into a module Array.Smart.Gravatar Hugo Herbelin2018-05-23
| |_|/ / |/| | |
| | | * Fix #7539: Checker does not properly handle negative coinductive types.Gravatar Pierre-Marie Pédrot2018-05-18
| | | | | | | | | | | | | | | | | | | | The reduction machine of the checker was not taking into account the fact that cofixpoints needed to be unfolded when applied against a projection.
* | | | Infrastructure for ocamldebug on the checkerGravatar Gaëtan Gilbert2018-05-13
| |_|/ |/| |
| | * Fix #7327: coqchk subtyping of polymorphic constantsGravatar Gaëtan Gilbert2018-04-23
| |/
| * Fix #6798: coqchk ignores ugraph when comparing constant instancesGravatar Gaëtan Gilbert2018-04-20
|/
* [api] Deprecate a couple of aliases that we missed.Gravatar Emilio Jesus Gallego Arias2018-03-28
|
* Merge PR #6800: [checker] Printer cleanup.Gravatar Maxime Dénès2018-03-09
|\
* | Update checker to reflect rule on constructors of polymorphic inductive typesGravatar Matthieu Sozeau2018-03-08
| |
| * [checker] Printer cleanup.Gravatar Emilio Jesus Gallego Arias2018-03-07
|/ | | | Makes printing rules more explicit and should close #6799.
* Replace invalid tag @raises in ocamldoc comments with @raiseGravatar mrmr19932018-03-05
|
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
* \ Merge PR #6734: dest_{prod,lam}: no Cast case (it's removed by whd)Gravatar Maxime Dénès2018-02-28
|\ \
| | * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
| |/ |/|
* | Merge PR #6740: Adding a sanity check on inductive variance subtyping.Gravatar Maxime Dénès2018-02-21
|\ \
* \ \ Merge PR #6728: Extrude monomorphic universe contexts from with Definition ↵Gravatar Maxime Dénès2018-02-19
|\ \ \ | | | | | | | | | | | | constraints.
* \ \ \ Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use ↵Gravatar Maxime Dénès2018-02-19
|\ \ \ \ | | | | | | | | | | | | | | | camlp4
| * | | | Change references to CAMLP4 to CAMLP5 to be more accurate since we noGravatar Jim Fehrle2018-02-17
| | | | | | | | | | | | | | | | | | | | longer use camlp4.
| | * | | Extrude monomorphic universe contexts from with Definition constraints.Gravatar Pierre-Marie Pédrot2018-02-16
| |/ / / |/| | | | | | | | | | | | | | | We defer the computation of the universe quantification to the upper layer, outside of the kernel.
| | * | Adding a sanity check on inductive variance subtyping.Gravatar Pierre-Marie Pédrot2018-02-15
| |/ / |/| |
* | | Merge PR #6262: [error] Replace msg_error by a proper exception.Gravatar Maxime Dénès2018-02-12
|\ \ \
| | | * dest_{prod,lam}: no Cast case (it's removed by whd)Gravatar Gaëtan Gilbert2018-02-11
| | |/
* | / 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 |= *)
| * [error] Replace msg_error by a proper exception.Gravatar Emilio Jesus Gallego Arias2018-02-09
|/ | | | | | | | | | The current error mechanism in the core part of Coq is 100% exception based; there was some confusion in the past as to whether raising and exception could be replace with `Feedback.msg_error`. As of today, this is not the case [due to some issues in the layer that generates error feedbacks in the STM] so all cases of `msg_error` must raise an exception of print at a different level [for now].
* checker: cleanup projection unfoldingGravatar Gaëtan Gilbert2018-02-02
| | | | This just shares the unfold_projection between Closure and Reduction.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-03 21:38:14 +0000