commit ceed899f5ffb589f6526d84af5cefbe2496e4bbb
parent 310087cc97335c281ee5454e659d40eb84c8dc33
Author: AlexKnauth <alexander@knauth.org>
Date: Fri, 24 Jun 2016 19:11:34 -0400
add define, *, and a new join
Diffstat:
5 files changed, 74 insertions(+), 5 deletions(-)
diff --git a/turnstile/examples/ext-stlc.rkt b/turnstile/examples/ext-stlc.rkt
@@ -43,6 +43,7 @@
(define-primop zero? : (→ Int Bool))
(define-primop = : (→ Int Int Bool))
(define-primop - : (→ Int Int Int))
+(define-primop * : (→ Int Int Int))
(define-primop add1 : (→ Int Int))
(define-primop sub1 : (→ Int Int))
(define-primop not : (→ Bool Bool))
diff --git a/turnstile/examples/infer.rkt b/turnstile/examples/infer.rkt
@@ -1,5 +1,6 @@
#lang turnstile
(extends "ext-stlc.rkt" #:except #%app λ)
+(reuse inst #:from "sysf.rkt")
(require (only-in "sysf.rkt" ∀ ~∀ ∀? Λ))
(reuse cons [head hd] [tail tl] nil [isnil nil?] List list #:from "stlc+cons.rkt")
(require (only-in "stlc+cons.rkt" ~List))
@@ -29,6 +30,16 @@
(syntax-parse cs
[([a b] ...)
#'(Constraints (Constraint a b) ...)]))
+ (define-syntax ~?∀
+ (pattern-expander
+ (syntax-parser
+ [(?∀ Xs-pat τ-pat)
+ #:with τ (generate-temporary)
+ #'(~and τ
+ (~parse (~∀ Xs-pat τ-pat)
+ (if (∀? #'τ)
+ #'τ
+ ((current-type-eval) #'(∀ () τ)))))])))
(define-syntax ~?Some
(pattern-expander
(syntax-parser
@@ -121,6 +132,15 @@
((current-type-eval) #`(∀ (X ...) (#,id X ...))))
(inst-type/cs #'[X- ...] #'([X- arg] ...) #'body))
+ (define old-join (current-join))
+
+ (define (new-join a b)
+ (syntax-parse (list a b)
+ [[(~?Some [X ...] A (~Cs [τ_1 τ_2] ...))
+ (~?Some [Y ...] B (~Cs [τ_3 τ_4] ...))]
+ (define AB (old-join #'A #'B))
+ (?Some #'[X ... Y ...] AB #'([τ_1 τ_2] ... [τ_3 τ_4] ...))]))
+ (current-join new-join)
)
(define-typed-syntax λ
@@ -142,12 +162,13 @@
[#:with [A ...] (generate-temporaries #'[e_arg ...])]
[#:with B (generate-temporary 'result)]
[⊢ [[e_fn ≫ e_fn-] ⇒ : τ_fn*]]
- [#:with (~?Some [V1 ...] τ_fn (~Cs [τ_3 τ_4] ...)) (syntax-local-introduce #'τ_fn*)]
+ [#:with (~?Some [V1 ...] τ_fn (~Cs [τ_3 τ_4] ...))
+ (syntax-local-introduce #'τ_fn*)]
[#:with τ_fn-expected (tycons #'→ #'[A ... B])]
[⊢ [[e_arg ≫ e_arg-] ⇒ : τ_arg*] ...]
- [#:with [(~?Some [V2 ...] τ_arg (~Cs [τ_5 τ_6] ...)) ...]
+ [#:with [(~?Some [V3 ...] τ_arg (~Cs [τ_5 τ_6] ...)) ...]
(syntax-local-introduce #'[τ_arg* ...])]
- [#:with τ_out (some/inst/generalize #'[A ... B V1 ... V2 ... ...]
+ [#:with τ_out (some/inst/generalize #'[A ... B V1 ... V3 ... ...]
#'B
#'([τ_fn-expected τ_fn]
[τ_3 τ_4] ...
@@ -156,5 +177,14 @@
--------
[⊢ [[_ ≫ (#%app- e_fn- e_arg- ...)] ⇒ : τ_out]]])
+(define-typed-syntax define
+ [(define x:id e:expr) ≫
+ [⊢ [[e ≫ e-] ⇒ : τ_e]]
+ [#:with tmp (generate-temporary #'x)]
+ --------
+ [_ ≻ (begin-
+ (define-syntax- x (make-rename-transformer (⊢ tmp : τ_e)))
+ (define- tmp e-))]])
+
diff --git a/turnstile/examples/mlish.rkt b/turnstile/examples/mlish.rkt
@@ -2,7 +2,7 @@
(require racket/fixnum racket/flonum
(for-syntax macrotypes/type-constraints macrotypes/variance-constraints))
-(extends "ext-stlc.rkt" #:except #%app λ → + - void = zero? sub1 add1 not let let* and #%datum begin
+(extends "ext-stlc.rkt" #:except #%app λ → + - * void = zero? sub1 add1 not let let* and #%datum begin
#:rename [~→ ~ext-stlc:→])
(reuse inst #:from "sysf.rkt")
(require (only-in "ext-stlc.rkt" → →?))
diff --git a/turnstile/examples/stlc+reco+sub.rkt b/turnstile/examples/stlc+reco+sub.rkt
@@ -1,6 +1,6 @@
#lang turnstile
(extends "stlc+sub.rkt" #:except #%app #%datum)
-(extends "stlc+reco+var.rkt" #:except #%datum +)
+(extends "stlc+reco+var.rkt" #:except #%datum + *)
;;use type=? and eval-type from stlc+reco+var.rkt, not stlc+sub.rkt
;; but extend sub? from stlc+sub.rkt
diff --git a/turnstile/examples/tests/tlb-infer-tests.rkt b/turnstile/examples/tests/tlb-infer-tests.rkt
@@ -43,3 +43,41 @@
(check-type (λ (a f g) (g (λ () (f a)) (+ (f 1) (f 2))))
: (∀ (C) (→ Int (→ Int Int) (→ (→ Int) Int C) C)))
+(define fact-builder
+ (λ (fact)
+ (λ (n)
+ (if (= 0 n)
+ 1
+ (* n (fact (sub1 n)))))))
+
+(check-type fact-builder : (→ (→ Int Int) (→ Int Int)))
+
+(define fact~ (fact-builder (fact-builder (fact-builder (fact-builder (fact-builder (inst (λ (n) 1) Int)))))))
+(check-type fact~ : (→ Int Int))
+(check-type (fact~ 0) : Int -> 1)
+(check-type (fact~ 1) : Int -> 1)
+(check-type (fact~ 2) : Int -> 2)
+(check-type (fact~ 3) : Int -> 6)
+(check-type (fact~ 4) : Int -> 24)
+(check-type (fact~ 5) : Int -> 120)
+(check-type (fact~ 6) : Int -> 720)
+;(check-type (fact~ 7) : Int -> 5040) ; fails, produces 2520
+;(check-type (fact~ 8) : Int -> 40320) ; fails, produces 6720
+
+;(define Y
+; (λ (f)
+; ((λ (g) (f (λ (x) ((g g) x))))
+; (λ (g) (f (λ (x) ((g g) x)))))))
+;(check-type Y : (∀ (A B) (→ (→ (→ A B) (→ A B)) (→ A B))))
+;
+;(define fact (Y fact-builder))
+;(check-type fact : (→ Int Int))
+;(check-type (fact 0) : Int -> 1)
+;(check-type (fact 1) : Int -> 1)
+;(check-type (fact 2) : Int -> 2)
+;(check-type (fact 3) : Int -> 6)
+;(check-type (fact 4) : Int -> 24)
+;(check-type (fact 5) : Int -> 120)
+;(check-type (fact 6) : Int -> 720)
+;(check-type (fact 7) : Int -> 5040)
+;(check-type (fact 8) : Int -> 40320)
