aboutsummaryrefslogtreecommitdiff
path: root/checker
AgeCommit message (Collapse)Author
2018-07-03checker Indtypes: remove unused argumentsGaëtan Gilbert
2018-07-03checker Modops strengthening: remove unused argument resolverGaëtan Gilbert
2018-07-03Subtyping.check_constant: remove unused module path argument.Gaëtan Gilbert
2018-07-03Inductive.extract_stack,filter_stack_domain: remove unused argumentsGaëtan Gilbert
2018-06-26Remove Sorts.contentsGaëtan Gilbert
2018-06-25Merge PR #7798: Remove hack skipping comparison of algebraic universes in ↵Matthieu Sozeau
subtyping.
2018-06-23Using more general information for primitive records.Pierre-Marie Pédrot
This brings more compatibility with handling of mutual primitive records in the kernel.
2018-06-23Change the proj_ind field from MutInd.t to inductive.Pierre-Marie Pédrot
This is a first step towards the acceptance of mutual record types in the kernel.
2018-06-22Remove hack skipping comparison of algebraic universes in subtyping.Gaëtan Gilbert
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!).
2018-06-21Remove enforce_leq from checkerGaëtan Gilbert
2018-06-19Merge PR #7841: Remove CanaryPierre-Marie Pédrot
2018-06-18Remove Canary.whitequark
This eliminates 3 uses of Obj from TCB.
2018-06-17Remove the proj_body field from the kernel.Pierre-Marie Pédrot
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.
2018-06-17Remove the proj_eta field of the kernel.Pierre-Marie Pédrot
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.
2018-06-17Getting rid of the const_proj field in the kernel.Pierre-Marie Pédrot
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.
2018-06-07Fix the checker by merely adapting the data structure.Pierre-Marie Pédrot
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.
2018-06-04Merge PR #7552: Fix #7539: Checker does not properly handle negative ↵Matthieu Sozeau
coinductive types.
2018-05-31Reduce circular dependency constants <-> projectionsGaëtan Gilbert
Instead of having the projection data in the constant data we have it independently in the environment.
2018-05-25Merge PR #7325: Fix #7323: coqchk puts polymorphic univs of inductive in ↵Pierre-Marie Pédrot
global env
2018-05-24Merge PR #7177: Unifying names of "smart" combinators + adding combinators ↵Pierre-Marie Pédrot
in CArray
2018-05-24Fix #7323: coqchk puts polymorphic univs of inductive in global envGaëtan Gilbert
2018-05-24Merge PR #7328: Fix #7327: coqchk subtyping of polymorphic constantsPierre-Marie Pédrot
2018-05-24Merge PR #7317: Fix #6798: coqchk ignores ugraph when comparing constant ↵Pierre-Marie Pédrot
instances
2018-05-23Moving Rtree.smart_map into Rtree.Smart.map.Hugo Herbelin
2018-05-23Moving Option.smart_map to Option.Smart.map.Hugo Herbelin
2018-05-23Collecting List.smart_* functions into a module List.Smart.Hugo Herbelin
2018-05-23Collecting Array.smart_* functions into a module Array.Smart.Hugo Herbelin
2018-05-18Fix #7539: Checker does not properly handle negative coinductive types.Pierre-Marie Pédrot
The reduction machine of the checker was not taking into account the fact that cofixpoints needed to be unfolded when applied against a projection.
2018-05-13Infrastructure for ocamldebug on the checkerGaëtan Gilbert
2018-04-23Fix #7327: coqchk subtyping of polymorphic constantsGaëtan Gilbert
2018-04-20Fix #6798: coqchk ignores ugraph when comparing constant instancesGaëtan Gilbert
2018-03-28[api] Deprecate a couple of aliases that we missed.Emilio Jesus Gallego Arias
2018-03-09Merge PR #6800: [checker] Printer cleanup.Maxime Dénès
2018-03-08Update checker to reflect rule on constructors of polymorphic inductive typesMatthieu Sozeau
2018-03-07[checker] Printer cleanup.Emilio Jesus Gallego Arias
Makes printing rules more explicit and should close #6799.
2018-03-05Replace invalid tag @raises in ocamldoc comments with @raisemrmr1993
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-02-28Merge PR #6734: dest_{prod,lam}: no Cast case (it's removed by whd)Maxime Dénès
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-21Merge PR #6740: Adding a sanity check on inductive variance subtyping.Maxime Dénès
2018-02-19Merge PR #6728: Extrude monomorphic universe contexts from with Definition ↵Maxime Dénès
constraints.
2018-02-19Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use ↵Maxime Dénès
camlp4
2018-02-17Change references to CAMLP4 to CAMLP5 to be more accurate since we noJim Fehrle
longer use camlp4.
2018-02-16Extrude monomorphic universe contexts from with Definition constraints.Pierre-Marie Pédrot
We defer the computation of the universe quantification to the upper layer, outside of the kernel.
2018-02-15Adding a sanity check on inductive variance subtyping.Pierre-Marie Pédrot
2018-02-12Merge PR #6262: [error] Replace msg_error by a proper exception.Maxime Dénès
2018-02-11dest_{prod,lam}: no Cast case (it's removed by whd)Gaëtan Gilbert
2018-02-10Simplification: cumulativity information is variance information.Gaëtan Gilbert
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 |= *)
2018-02-09[error] Replace msg_error by a proper exception.Emilio Jesus Gallego Arias
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].
2018-02-02checker: cleanup projection unfoldingGaëtan Gilbert
This just shares the unfold_projection between Closure and Reduction.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 18:31:02 +0000