Paul Chiusano
|
8e3370e228
|
got some more tests working - checking of handle blocks was WRONG
|
2018-06-21 16:18:26 -04:00 |
|
Paul Chiusano
|
accdf4b74d
|
added some failing tests
|
2018-06-21 15:45:59 -04:00 |
|
Runar Bjarnason
|
e6d0c6031f
|
Improved checking of letrecs.
|
2018-06-21 13:52:48 -04:00 |
|
Runar Bjarnason
|
d03e48a77b
|
Debugging letrec typechecking
|
2018-06-21 12:49:12 -04:00 |
|
Paul Chiusano
|
19c20553f1
|
some debugging / diagnostics
|
2018-06-20 17:39:43 -04:00 |
|
Paul Chiusano
|
b9456e8dce
|
hopefully more correct version of Handle synthesis
|
2018-06-20 12:23:27 -04:00 |
|
Paul Chiusano
|
ccb9c97f99
|
added failing test
|
2018-06-20 12:22:58 -04:00 |
|
Paul Chiusano
|
c9f6a7373d
|
Added a case in instantiateR to deal with effects
|
2018-06-20 11:40:56 -04:00 |
|
Paul Chiusano
|
f1dd38d72e
|
when checking body of Handle, the body is checked against a type {e} t, where e is the type introduced by the handler
|
2018-06-19 17:17:42 -04:00 |
|
Rúnar Óli Bjarnason
|
3e70472812
|
Unifying abilities with subabilities
|
2018-06-19 16:46:29 -04:00 |
|
Rúnar Óli Bjarnason
|
8d60ce52d3
|
Disabling ability checks in fake pattern effect terms
|
2018-06-19 15:31:08 -04:00 |
|
Rúnar Óli Bjarnason
|
9a8a3384c5
|
Ability checks on function application
|
2018-06-19 12:24:11 -04:00 |
|
Rúnar Óli Bjarnason
|
dea790f54a
|
Checking handler blocks
|
2018-06-19 11:49:07 -04:00 |
|
Arya Irani
|
4c59e4df93
|
add withEffects
|
2018-06-19 11:32:22 -04:00 |
|
Paul Chiusano
|
6c46ecf7db
|
Typechecker compiles with new typechecking monad that can read a set of ambient abilities, not hooked up anywhere yet
|
2018-06-18 17:29:18 -04:00 |
|
Rúnar Óli Bjarnason
|
4d267330eb
|
Failing handler test
|
2018-06-18 16:39:10 -04:00 |
|
Rúnar Óli Bjarnason
|
8eb057c92a
|
Pattern matching on an effect typechecks!
|
2018-06-18 15:53:57 -04:00 |
|
Rúnar Óli Bjarnason
|
279b6a9ed2
|
Typechecking effect patterns
|
2018-06-18 15:13:52 -04:00 |
|
Arya Irani
|
8d8966a732
|
Merge pull request #196 from unisonweb/topic/refactor-bootstrap
factor pure stuff out of parser-typechecker Bootstrap
|
2018-06-18 10:56:08 -04:00 |
|
Arya Irani
|
b79b80cbca
|
Merge pull request #193 from unisonweb/topic/typechecker
merge topic/typechecker into wip/typechecker
|
2018-06-18 10:53:06 -04:00 |
|
Arya Irani
|
d29a3cb897
|
-Wall warnings for parser-typechecker bootstrap target
|
2018-06-17 14:37:05 -04:00 |
|
Arya Irani
|
5af27e2e33
|
factor pure stuff out of parser-typechecker Bootstrap
|
2018-06-17 14:28:21 -04:00 |
|
Runar Bjarnason
|
f7ccfb67ee
|
Synthesizing effect patterns
|
2018-06-15 17:03:13 -04:00 |
|
Paul Chiusano
|
80e71a987a
|
Merge pull request #190 from unisonweb/topic/varlong-arrays
use VarLong for lengths and backref Pos
|
2018-06-15 10:32:30 -05:00 |
|
Runar Bjarnason
|
416c28a1e8
|
Very wip
|
2018-06-15 00:38:29 -04:00 |
|
Runar Bjarnason
|
a7cf7f74f5
|
Typechecking guards
|
2018-06-15 00:00:13 -04:00 |
|
Runar Bjarnason
|
db0bd927b8
|
Tuple patterns
|
2018-06-14 22:23:56 -04:00 |
|
Arya Irani
|
8c5c4847ab
|
use _updated_ body of synthesized UnisonFile when serializing
|
2018-06-14 19:46:41 -04:00 |
|
Runar Bjarnason
|
823cb434ba
|
Tuple literals parse
|
2018-06-14 17:40:27 -04:00 |
|
Runar Bjarnason
|
046074d2ba
|
As-patterns
|
2018-06-14 17:25:17 -04:00 |
|
Runar Bjarnason
|
910a70f3a9
|
More pattern type checking tests
|
2018-06-14 17:05:56 -04:00 |
|
Runar Bjarnason
|
5c1e4d6543
|
Plumbing to get typechecker tests working
|
2018-06-14 15:22:09 -04:00 |
|
Arya Irani
|
bfd05da1ba
|
refactor towards adding typechecking tests having data declarations
|
2018-06-14 13:34:38 -04:00 |
|
Paul Chiusano
|
88d62e43c4
|
patterns now checked against scrutinee inferred type
|
2018-06-13 21:48:39 -04:00 |
|
Paul Chiusano
|
8d1e6c22f7
|
Typechecker working again with more general term type - existential vars are now allowed in type annotations
|
2018-06-13 21:38:25 -04:00 |
|
Paul Chiusano
|
64954ca8aa
|
generalize a number of smart constructors to not assume type variables and term variables are the same type
|
2018-06-13 21:37:24 -04:00 |
|
Paul Chiusano
|
cebe6c637d
|
another helper function - Term.vtmap, for mapping over the type variables of a term's annotations
|
2018-06-13 21:04:52 -04:00 |
|
Paul Chiusano
|
ecd1b72b85
|
generalized some ABT functions in prep for allowing existential and universal type vars to appear in type annotations on terms
|
2018-06-13 20:54:59 -04:00 |
|
Runar Bjarnason
|
cf7aa13102
|
Rewrote checkCase
|
2018-06-13 15:47:29 -04:00 |
|
Arya Irani
|
97562ff0a7
|
we are debugging typechecking of patterns
|
2018-06-13 14:24:49 -04:00 |
|
Arya Irani
|
efe34fd8d7
|
check for free type vars in data decls before typechecking, subst them away in bootstrap
|
2018-06-13 10:41:30 -04:00 |
|
Paul Chiusano
|
3b6630d1ab
|
Removed defunct check logic for Match, just falling back to synthesis for now. Added synthesis case for Term.Constructor.
|
2018-06-12 22:59:06 -04:00 |
|
Arya Irani
|
e2557cfac4
|
remove Builtin.resolveBuiltins in favor of Term.bindBuiltins and Type.bindBuiltins
note: arguably more efficient to only `subst` away the free vars,
and maybe we should use `Map v (Term v)` in various places instead
|
2018-06-12 18:24:51 -04:00 |
|
Arya Irani
|
8dd5350e1f
|
including that one
|
2018-06-12 17:41:14 -04:00 |
|
Arya Irani
|
59255f1393
|
Take builtin substitutions out of Unison.{Parsers, FileParser}
|
2018-06-12 17:38:27 -04:00 |
|
Arya Irani
|
92f43221d3
|
typechecking for pattern-matching (untested)
|
2018-06-12 17:01:00 -04:00 |
|
Paul Chiusano
|
2da9ace1d5
|
WIP on typechecking case expressions
|
2018-06-12 14:24:02 -04:00 |
|
Paul Chiusano
|
a2ddd994b4
|
fix parser bug where = in bindings was not required to be followed by a space
|
2018-06-12 11:33:07 -04:00 |
|
Paul Chiusano
|
4ff9a686e0
|
added todo to reshuffle module structure a bit
|
2018-06-12 11:23:57 -04:00 |
|
Arya Irani
|
5b601a4248
|
update codecs to use VarInt encoding for Text and Array lengths
Note that the max sizes for these on the JVM are <= 31 bits
|
2018-06-11 18:54:39 -04:00 |
|