Commit Graph

555 Commits

Author SHA1 Message Date
AlexKnauth
0942413764 infer variances for recursive and mutually recursive datatypes 2016-05-20 16:22:30 -04:00
AlexKnauth
2cd9cb2cbd refactor to use ctxt-variance in find-variances 2016-05-20 16:21:57 -04:00
AlexKnauth
c45e967896 add mlish/sweet-map.rkt test 2016-05-20 13:20:00 -04:00
AlexKnauth
94ae1ebabe refactor variance code into infer-variances function 2016-05-13 10:15:55 -04:00
Alex Knauth
c872a1404d Merged in allow-generalization-covariant (pull request #23)
Allow generalization for covariant type variables
2016-05-12 15:32:54 -04:00
AlexKnauth
d170ee8834 add more tests
based section 3 and section 4.1 of
http://caml.inria.fr/pub/papers/garrigue-value_restriction-fiwflp04.pdf
2016-05-12 14:49:22 -04:00
AlexKnauth
7a3c096a83 allow some under-constrained function applications
in cases where the unsolved type variables only appear in covariant
positions.
2016-05-12 14:49:21 -04:00
AlexKnauth
4af0f4e2b4 add find-X-variance, covariant-X?, and covariant-Xs?
and also allow type constructors to declare the variance of their arguments.

infer variances for non-recursive `define-type` types
2016-05-12 14:49:21 -04:00
AlexKnauth
4347b2eaff use find-free-Xs, propagate expected type more 2016-05-11 13:50:27 -04:00
AlexKnauth
5854d76c8d modify solve to return all of the arguments 2016-05-11 13:50:27 -04:00
AlexKnauth
1ca2ece9df use add-constraints for type unification
fixes issue #20
2016-05-11 13:50:27 -04:00
AlexKnauth
d2b4df3a94 don't give empty foralls to functions 2016-05-11 13:50:27 -04:00
AlexKnauth
e243ee0656 add ?∀ and ?Λ 2016-05-11 13:50:26 -04:00
AlexKnauth
95d960267a test the example that would have been unsound 2016-05-10 14:35:05 -04:00
AlexKnauth
c9110ccf73 don't make new foralls for under-constrained function applications
Fixes the unsoundness mentioned in
https://bitbucket.org/stchang/macrotypes/issues/16/allow-under-constrained-function#comment-27692493
by disallowing under-constrained function calls entirely.
This re-opens issue #16, which will have to be solved in a sound way later.
2016-05-10 14:05:53 -04:00
AlexKnauth
1e68e32ecc refactor solve to return a substitution 2016-05-05 14:16:25 -04:00
AlexKnauth
9920c5791d modify #%app to deal with under-constrained function applications
fixes #16
2016-05-05 14:16:25 -04:00
Stephen Chang
5b64b3b042 lift out version consts for checking preserved prop 2016-05-05 14:06:10 -04:00
Stephen Chang
9308677b2a run-all-mlish-tests script: use find-system-path 2016-05-03 14:40:22 -04:00
Stephen Chang
33e39c5e96 abstract and cleanup run-all-mlish-tests script 2016-05-03 14:22:58 -04:00
Stephen Chang
64d1bc9a48 add extra nested lambda test cases 2016-05-03 13:54:40 -04:00
AlexKnauth
7acbfefa71 remove unnecessary annotations 2016-05-02 16:47:15 -04:00
AlexKnauth
59b0ad3d3a allow unannotated lambdas
in cases where the expected type has enough information, and propagate
the expected type in those cases.
2016-05-02 15:11:12 -04:00
AlexKnauth
95a7fb87f8 add ~?∀ for matching possibly polymorphic types 2016-05-02 14:29:51 -04:00
AlexKnauth
9b171fd62e use (current-join) in cond, match, and match2
- update match2 error message tests
- fixes #12
2016-05-02 13:56:48 -04:00
AlexKnauth
44c63e4171 mark syntax properties as preserved 2016-04-28 16:46:30 -04:00
AlexKnauth
92d2fe585a handle #f and #<syntax #f> expected types 2016-04-21 11:02:26 -04:00
Stephen Chang
579815512e for/fold produces better err msg 2016-04-20 19:18:33 -04:00
Stephen Chang
ce1bc6b90f fix continuation marks src in type-error 2016-04-20 17:50:05 -04:00
Stephen Chang
1fc2b3f538 change current-join to throw error on fail
- returns join type on success
2016-04-20 15:42:52 -04:00
Stephen Chang
9b9c1dda96 datatype constructors are functions 2016-04-20 14:12:43 -04:00
Stephen Chang
b439327d78 define-type automatically defines accessors and predicates for record variants 2016-04-20 13:51:05 -04:00
Stephen Chang
51f9008b99 fix bug in reuse to avoid conflict with ids that happen to use the same prefix 2016-04-19 16:06:09 -04:00
Stephen Chang
c64251cac0 infer quantified type variables in the order that they occur (L-to-R)
- backwards incompatible change: quantified type variables no longer sorted lex
- fix and add tests, remove some annotations in tests
- small speed improvement due to eliminating some extra expansions
- closes #9, closes #11
2016-04-19 15:10:07 -04:00
Stephen Chang
29be57dffe use stx->list, closes #10 2016-04-19 12:27:09 -04:00
Stephen Chang
0846a86f24 minor cleanup: add compute-tyvars 2016-04-18 18:22:36 -04:00
AlexKnauth
61f4304085 srcloc for typecheck-fail 2016-04-14 15:35:15 -04:00
Stephen Chang
d2749db6d6 fix the order of inferred tyvars in fn defs
- remove some more unneeded type annotations in tests
2016-04-13 19:32:15 -04:00
Stephen Chang
5c28501236 add some type validation in define-type 2016-04-13 18:03:49 -04:00
Stephen Chang
6cb15a06da code cleanup 2016-04-13 15:14:57 -04:00
Stephen Chang
8a36c7962b revise extra-info to handle mutually recursive datatypes
- define extra-info as a separate macro whose input is the types
  in the tycon
  - extra-info in main tycon is just the name of the extra-info macro
  - extra-info macro is expanded only when extra-info is requested
  - naturally handles additional tyvar substs in the types
  - breaks the recursion to avoid inf loops for recursive and mutually recursive
    datatypes
  - enables simplification of direct recursive datatypes
    - no longer need subst-special
    - performance is much improved (okasaki: ~1min, was ~4min)
2016-04-13 14:00:20 -04:00
Stephen Chang
5c3d0edb5e remove unneeded type annotations in okasaki tests 2016-04-11 16:09:40 -04:00
ben
0bd1962650 [bg] add Okasaki data structures
- all queues: batched, bankers, physicists, hood-melvile, bootstrapped, implicit
- deques: bankers, simple catenable
- random access lists: binary, skew, alt binary
- upcoming: heaps, sets, finite maps
- excluded: catenable lists and deques
2016-04-11 15:17:41 -04:00
Stephen Chang
26a2699d48 fix match expected-type propagation to non-datatype clauses
- closes #8
2016-04-11 14:53:45 -04:00
Stephen Chang
2a9005a31d remove spurious type annotations in tests
- not needed bc rackunit-typechecking now adds expected-type
2016-04-11 14:22:35 -04:00
Stephen Chang
fdf902121e fix more stx-parse err msgs; and other err msgs
- all tests now passing
2016-04-11 14:01:24 -04:00
Stephen Chang
ced8a1affc add trees-tests file 2016-04-11 13:56:54 -04:00
Stephen Chang
73e59ddec7 workaround syntax-parse error msg regressions
- just throw explicit type-error exn instead of relying on #:fail-when etc
- run-all-tests passing
2016-04-06 17:15:20 -04:00
Stephen Chang
01a0bb28a7 improve rackunit-typechecking
- speed up by eliminating duplicate expansion in check-type
- use given type annotation as expected-type
  - eliminates unneeded type annotations
2016-04-06 17:10:46 -04:00
Stephen Chang
1167407cfe fix type constructor arity err causing inf loop
- lambda now supports (implicit) polymorphic type annotations
- (unrelated to this commit) many tests seem to be failing due to a
  slight change in err msg
2016-04-05 10:55:02 -04:00