fix bug with tyvar computation

- define separate ->/test constructor that computes tyvars
  and -> does not because it may be nested
  (see "try" fn in alex.mlish)
- add alex.mlish tests
- other mlish tests still broken --- need to use ->/text
This commit is contained in:
Stephen Chang 2016-03-10 16:14:36 -05:00
parent db1da5ae20
commit b8e3ad1602
3 changed files with 18 additions and 5 deletions

View File

@ -333,11 +333,12 @@
(define-syntax ; wrapping →
(syntax-parser
#;[(_ (~and Xs {X:id ...}) . rst)
#:when (brace? #'Xs)
#:when (with-handlers ([exn:fail:syntax:unbound? (λ (e) (displayln (exn:fail:syntax-exprs e)))])
((current-type-eval) #'(ext-stlc:→ . rst)))
#'( (X ...) (ext-stlc:→ . rst))]
[(_ . rst) #'( () (ext-stlc:→ . rst))]))
; special arrow that computes free vars; for use with tests
; (because we can't write explicit forall
(provide →/test)
(define-syntax →/test
(syntax-parser
[(_ . rst)
(let L ([Xs #'()]) ; compute unbound ids; treat as tyvars
(with-handlers ([exn:fail:syntax:unbound?

View File

@ -0,0 +1,11 @@
#lang s-exp "../../mlish.rkt"
(require "../rackunit-typechecking.rkt")
#;(define (should-err [x : X] [f : (→ X Y)] -> Y)
(let ([y (f x)])
x))
(define (try [x : X][f : (→ X Y)] → X)
(let ([y (f x)]) x))
(check-type try : (→/test X (→ X Y) X))

View File

@ -17,3 +17,4 @@
;; from rw ocaml
(require "mlish/term.mlish")
(require "mlish/find.mlish")
(require "mlish/alex.mlish")