Fedor Isakov
|
08bed0c578
|
Apply automatic migrations to FitchProof subproject
|
2019-01-13 14:27:32 +01:00 |
|
Fedor Isakov
|
50487cd41c
|
Fix unification predicate implementation to properly process non-term arguments. Cleanup the code.
|
2019-01-13 14:26:35 +01:00 |
|
Fedor Isakov
|
29a44eac5d
|
Introduce automatic migration from eq to uni for basic scenario: logical on the left
|
2019-01-13 14:26:35 +01:00 |
|
Fedor Isakov
|
a46937b128
|
Change semantics of EqualsPredicate: ask returns true iff values are equal or the logicals are the same, tell throws exception if not
|
2019-01-13 14:26:35 +01:00 |
|
grigorii.kirgizov
|
ce34b598c2
|
lc: minor: add simple Typeclass examples (it's only structure/editor/scopes example); add one test case to DemoScopes
|
2019-01-11 19:09:44 +03:00 |
|
grigorii.kirgizov
|
c8233c24d7
|
lc: move to fully nameless representation of type vars; assign names only in recover
It is also a necessary step to bidirectional typechecking and can simplify things in other places
|
2019-01-11 19:09:44 +03:00 |
|
grigorii.kirgizov
|
eb80329a54
|
lc: change recover_varRef rule, propagate to recover_Var rule instead of duplicating it
|
2019-01-11 19:09:44 +03:00 |
|
grigorii.kirgizov
|
fb4fe40973
|
lc: typeclasses: added structure, editor, constraints (mainly concerned with scoping) aspects
|
2019-01-11 19:09:44 +03:00 |
|
grigorii.kirgizov
|
cf855fc19b
|
lc: add test case for correct handling of instantiation scopes in forall. fails now.
|
2019-01-11 19:09:44 +03:00 |
|
grigorii.kirgizov
|
2cc804079a
|
lc: add test case in DemoScopes for isomorphism between similar forall type
It checks that subsumtion relation is actually a richer 'dsk' relation
from Peyton Jones et al. 2007
|
2019-01-11 19:09:44 +03:00 |
|
grigorii.kirgizov
|
61e282da6c
|
lc: minor: remove few commented lines, add few comments; add space between typevars in ForallType editor
|
2019-01-11 19:09:44 +03:00 |
|
Fedor Isakov
|
134fbb5cdb
|
Add missing dependency to lambdacalc test model
|
2019-01-09 14:48:21 +01:00 |
|
Fedor Isakov
|
16153a23d1
|
Correctly display value assigned to a logical.
|
2019-01-09 13:01:57 +01:00 |
|
Fedor Isakov
|
f226bea8c2
|
Minor fixes in the BL typechecking templates. Insert manual new lines in the test structures for better visualization.
|
2019-01-09 13:01:37 +01:00 |
|
Fedor Isakov
|
bcb8efa653
|
Make editor for DataForm more usable, get rid of hacks in the layout. Introduce NewLineAttribute to manually insert new lines. Deprecate ListRole.
|
2019-01-09 13:01:37 +01:00 |
|
grigorii.kirgizov
|
4eab15c0a3
|
lc: add DemoScopes test case, fix one test example; reverse displayed order of user-supplied type annotations
|
2019-01-09 12:49:34 +03:00 |
|
grigorii.kirgizov
|
583358dc25
|
lc: modify name assignment to variables in 'forall'
|
2019-01-09 11:54:27 +03:00 |
|
grigorii.kirgizov
|
9180f16c25
|
lc: minor: uncomment typeOf_AnnVarRef rule (not fully tested yet), add dummy test rule
|
2019-01-09 11:18:20 +03:00 |
|
grigorii.kirgizov
|
8da1f51434
|
lc: move some examples, add error annotations in DemoScopes and test case for annotations
|
2019-01-09 11:18:20 +03:00 |
|
grigorii.kirgizov
|
1de24dd83c
|
lc: minor: editor enhancements
|
2019-01-09 11:17:42 +03:00 |
|
grigorii.kirgizov
|
47130f794d
|
lc: add proper type var scopes for AnnExpr
|
2019-01-09 11:17:42 +03:00 |
|
grigorii.kirgizov
|
b727b375ba
|
lc: disallow nested annotations on variables definitions
|
2019-01-09 11:17:42 +03:00 |
|
grigorii.kirgizov
|
c407e29ec4
|
lc: some refactorings nothing special
|
2019-01-09 11:17:42 +03:00 |
|
grigorii.kirgizov
|
682ed5b90b
|
lc: refine subsumption rel; add examples in DemoScope; editor enhancements (amend commit)
|
2019-01-09 11:17:42 +03:00 |
|
grigorii.kirgizov
|
24ce9e73aa
|
lc: refine subsumption rel; add examples in DemoScope; editor enhancements
|
2019-01-09 11:17:42 +03:00 |
|
grigorii.kirgizov
|
7f02d10b62
|
Add expr annotations; add examples
|
2019-01-09 11:17:42 +03:00 |
|
grigorii.kirgizov
|
440fcf868a
|
Intermediate commit: add VarType DF with editor; partial work on subsumed relation
|
2019-01-09 11:17:42 +03:00 |
|
grigorii.kirgizov
|
2fa00cac72
|
Minor: move annotation rules to its own handler
|
2019-01-09 11:17:42 +03:00 |
|
grigorii.kirgizov
|
06baa99da8
|
Add Var term; use it instead of free var-s in forall for subst.
Still not finished: can't pass Var name (see forall, freeTypeVars_isFree).
Also add subsumption relation for annotations.
|
2019-01-09 11:17:42 +03:00 |
|
grigorii.kirgizov
|
58a518af4f
|
Partially working forall quantified types
Substitution (i.e. forall instantiation) doesn't work in this version.
|
2019-01-09 11:17:42 +03:00 |
|
grigorii.kirgizov
|
084c4581f0
|
Bounded type vars: add free type var collection (in typeOf), gen, inst, list utils
|
2019-01-09 11:17:42 +03:00 |
|
grigorii.kirgizov
|
1be19ffe1e
|
lc: add pair (without accessors) and its typing to lambda calculus (lc)
|
2019-01-09 11:17:42 +03:00 |
|
grigorii.kirgizov
|
4ed48e2560
|
add unquantified type annotations to lambda calculus
|
2019-01-09 11:17:42 +03:00 |
|
Fedor Isakov
|
b7648ef5c3
|
Document judgements and reasonings in Fitch sample languages.
|
2019-01-07 11:03:55 +01:00 |
|
Fedor Isakov
|
54165ad367
|
Add new samples to the tests
|
2019-01-06 16:39:15 +01:00 |
|
Fedor Isakov
|
80e2b67d78
|
A couple of non-trivial examples of proofs.
|
2019-01-06 16:06:17 +01:00 |
|
Fedor Isakov
|
2078606204
|
Fitch sample: fix relation name constraint.
|
2019-01-06 16:05:52 +01:00 |
|
Fedor Isakov
|
cc4b335286
|
Introduce checking for instances of RuntimeErrorType during tests. Refactor test typechecking launcher.
|
2019-01-04 17:47:44 +01:00 |
|
Fedor Isakov
|
361fff7ec5
|
Drop usages of ListLiteral in tests. Testing BL typesystem.
|
2019-01-04 17:47:02 +01:00 |
|
Fedor Isakov
|
f855e5fa72
|
BL typesystem: drop usages of ListLiteral, replace with ListNode. Fix broken type inference of method calls and constructor invocations. A few minor fixes.
|
2019-01-04 17:46:37 +01:00 |
|
Fedor Isakov
|
c5daa24ee8
|
Deprecate ListLiteral and ListExpression concepts (only used in BL typesystem)
|
2019-01-04 17:44:32 +01:00 |
|
Fedor Isakov
|
d74ad951e3
|
Drop a hack in ListNode implementation that would disallow nested lists
|
2019-01-04 17:43:37 +01:00 |
|
Fedor Isakov
|
b5552d5cd3
|
Cleanup module dependencies
|
2019-01-03 17:16:47 +01:00 |
|
Fedor Isakov
|
2fd4545be4
|
BL typechecking: simplifying promote (subclassing relation), implement LUB as raw types intersection, better support for raw classier types
|
2019-01-03 17:16:47 +01:00 |
|
Fedor Isakov
|
32601dc96a
|
Deprecate unused methods in conreactor.
|
2019-01-03 17:16:47 +01:00 |
|
Fedor Isakov
|
63da3a7a6c
|
Minor optimization of terms representation in UI: hide uninitialized values
|
2019-01-03 17:16:47 +01:00 |
|
Fedor Isakov
|
9a99a440ec
|
Testing BL typesystem. Disable Huge test when not in CI.
|
2019-01-03 17:16:47 +01:00 |
|
Fedor Isakov
|
d5ed9d8fa0
|
Eliminate duplicate language aspect objects from lookup
|
2019-01-02 18:16:28 +01:00 |
|
Fedor Isakov
|
c87ca87a49
|
Cleanup in tests
|
2018-12-30 16:41:28 +01:00 |
|
Fedor Isakov
|
b4693aac3c
|
Switch to the new conreactor version.
|
2018-12-28 11:57:27 +01:00 |