aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
Commit message (Collapse)AuthorAge
* 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.
* checker: remove unused per-constant reduction flags.Gravatar Gaëtan Gilbert2018-02-02
|
* [checker] Avoid relying on canonical names.Gravatar Maxime Dénès2018-01-25
| | | | Fixes #5747: "make validate" fails with "bad recursive trees"
* [checker] Remove duplicated functionGravatar Maxime Dénès2018-01-25
|
* [checker] Better error message for bad recursive treesGravatar Maxime Dénès2018-01-25
|
* fix space in coqchk errorGravatar Ralf Jung2018-01-24
|
* Fix #6618: coqchk fails with "ill-typed term".Gravatar Pierre-Marie Pédrot2018-01-20
| | | | | | Primitive projections were not correctly unfolded, leading to failure of conversion checks in some cases. The kernel was strangely not affected by this bug, and it was probably a remnant of some vestigial code.
* Actually use the strategy information in the checker.Gravatar Pierre-Marie Pédrot2018-01-14
|
* Store the conversion oracle in constant and inductive definitions.Gravatar Pierre-Marie Pédrot2018-01-14
| | | | | We also have to update the checker to deserialize this additional data, but it is not using it in type-checking yet.
* Add interfaces for checker and remove dead code.Gravatar Maxime Dénès2018-01-10
|
* 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.
* [lib] Rename Profile to CProfileGravatar Emilio Jesus Gallego Arias2017-12-09
| | | | | New module introduced in OCaml 4.05 I think, can create problems when linking with the OCaml toplevel for `Drop`.
* Merge PR #6277: Qualified import in coqchkGravatar Maxime Dénès2017-12-07
|\
* \ Merge PR #6303: Remove redundant Zcase from the checker.Gravatar Maxime Dénès2017-12-07
|\ \
* \ \ Merge PR #6266: Safe unmarshalling in the checkerGravatar Maxime Dénès2017-12-05
|\ \ \
| | * | Remove redundant Zcase from the checker.Gravatar Pierre-Marie Pédrot2017-12-02
| |/ / |/| | | | | | | | | | | | | | This was redundant with ZcaseT, the only difference lying in the use or not of fclosures for substerms. This code was removed from the kernel in commit f2f805ed, we finish the work in the checker now.
generated by cgit v1.2.3 (git 2.39.1) at 2025-02-01 06:25:56 +0000