- Fix force_options so it doesn't take so long to run
- Fix property get typechecking so it forces getters to be synchronized with
methods.
- Simplify member_env.
Bug:
Change-Id: I3e2a0710c7fde950e7573ba6216820907b9ae374
Reviewed-on: https://dart-review.googlesource.com/9040
Reviewed-by: Dmitry Stefantsov <dmitryas@google.com>
Previously, we inferred the return type of statements in a way that made it
impossible to prove the statement typing consistency. Now, we use just the
stated return type for checking statements.
The proofs of statement typing are complete, except for one result generalizing
the expression typing consistency result to multiple variables changing; this
result is obvious to see directly from the provided lemmas but very tedious to
prove in Coq.
Bug:
Change-Id: I0bbcfb613df7510015f278fa85021ba0b3e57503
Reviewed-on: https://dart-review.googlesource.com/9020
Reviewed-by: Dmitry Stefantsov <dmitryas@google.com>
This revision includes changes from:
- [kernel] Completion of consistency proofs for type system of first subset of kernel.
due to the suckiness of gerrit.
We generalize type equivalence to subtyping. The contravariant property of
function parameter types causes properties for the totality checker. To
cicumvent this, we define a well-ordered relation on pairs of dart types and
prove subtyping respects it. We develop new lemmas and tactics for managing
proofs involving subtyping, includinging factoring out the messy business of
dealing with its convoluted recursion scheme.
Bug:
Change-Id: I18936168006617874a82eefc983f1b2d4d8af5af
Reviewed-on: https://dart-review.googlesource.com/5861
Reviewed-by: Dmitry Stefantsov <dmitryas@google.com>
I also added mutual induction schemes for types and expressions.
Some changes from the "Cleanup" revision are in here as well because Gerrit is terrible.
Bug:
Change-Id: I0859a6c1cba8179e0a64cc0455ab2a83fad8f26b
Reviewed-on: https://dart-review.googlesource.com/5300
Reviewed-by: Dmitry Stefantsov <dmitryas@google.com>
Summary:
Common datastructures used by both the Kernel AST definition and the object
model are factored into a shared module. A monad for partial computation is
defined to allow us to factor out termination proofs and syntactic validity
checks from the type checking and subtyping relations.
Test Plan:
Ran through coqc.
Bug:
Change-Id: I884666d7cc5b757d62541a46b868f8579a06f011
Reviewed-on: https://dart-review.googlesource.com/4700
Reviewed-by: Dmitry Stefantsov <dmitryas@google.com>
Samir Jindel