commit ee6c0c11f73628cda3bdf09e9ae5b56e55f5ef74
parent 468cf075d6f62d1e3fdefafde1bdac51585334e7
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Sat, 5 Mar 2016 10:12:32 -0500
mlish: add for/list, when, printf, multi expr bodies
- add fannkuch test
Diffstat:
3 files changed, 133 insertions(+), 8 deletions(-)
diff --git a/tapl/mlish.rkt b/tapl/mlish.rkt
@@ -1,7 +1,7 @@
#lang s-exp "typecheck.rkt"
(require (for-syntax syntax/id-set))
-(extends "ext-stlc.rkt" #:except #%app λ → + - void = zero? sub1 add1 not let and #%datum
+(extends "ext-stlc.rkt" #:except #%app λ → + - void = zero? sub1 add1 not let and #%datum begin
#:rename [~→ ~ext-stlc:→])
(reuse inst ~∀ ∀ ∀? Λ #:from "sysf.rkt")
(require (only-in "stlc+rec-iso.rkt" case fld unfld μ ~× × ×? ∨ var tup proj define-type-alias)
@@ -12,8 +12,8 @@
;(provide hd tl nil?)
(provide → × tup proj define-type-alias)
(provide define-type match)
-(provide (rename-out [ext-stlc:let let] [ext-stlc:and and] [ext-stlc:#%datum #%datum]))
-(reuse cons nil isnil head tail list List #:from "stlc+cons.rkt")
+(provide (rename-out [ext-stlc:and and] [ext-stlc:#%datum #%datum]))
+(reuse cons nil isnil head tail list List ~List List? #:from "stlc+cons.rkt")
;; ML-like language
;; - top level recursive functions
@@ -106,7 +106,7 @@
#'(begin
(define-syntax f (make-rename-transformer (⊢ g : (∀ (X ...) (ext-stlc:→ τ ... τ_out)))))
(define g (Λ (X ...) (ext-stlc:λ ([x : τ] ...) e_ann))))]
- [(_ (f:id [x:id (~datum :) τ] ... (~or (~datum ->) (~datum →)) τ_out) e)
+ [(_ (f:id [x:id (~datum :) τ] ... (~or (~datum ->) (~datum →)) τ_out) e_body ... e)
#:with Ys
(let L ([Xs #'()]) ; compute unbound ids; treat as tyvars
(with-handlers
@@ -128,7 +128,7 @@
;(⊢ g : (∀ Ys (ext-stlc:→ τ ... τ_out)))))
(⊢ g : (∀ Ys (ext-stlc:→ τ+orig ...)))))
(define g
- (Λ Ys (ext-stlc:λ ([x : τ] ...) e_ann))))])
+ (Λ Ys (ext-stlc:λ ([x : τ] ...) (ext-stlc:begin e_body ... e_ann)))))])
;
;; internal form used to expand many types at once under the same context
(define-type-constructor Tmp #:arity >= 0 #:bvs >= 0) ; need a >= 0 arity
@@ -339,6 +339,9 @@
(define-primop min : (→ Int Int Int))
(define-primop void : (→ Unit))
(define-primop = : (→ Int Int Bool))
+(define-primop <= : (→ Int Int Bool))
+(define-primop < : (→ Int Int Bool))
+(define-primop > : (→ Int Int Bool))
(define-primop zero? : (→ Int Bool))
(define-primop sub1 : (→ Int Int))
(define-primop add1 : (→ Int Int))
@@ -396,7 +399,7 @@
(mk-app-err-msg stx #:given #'(τ_arg ...) #:expected #'(τ_in ...))
(⊢ (#%app e_fn- e_arg- ...) : τ_out)])
-;; cond
+;; cond and other conditionals
(define-typed-syntax cond
[(_ [(~and test (~not (~datum else))) body] ...
(~optional [(~and (~datum else) (~parse else_test #'(ext-stlc:#%datum . #t))) else_body]
@@ -411,7 +414,13 @@
#:when (or (not (attribute else_body))
(typecheck? #'last-ty #'τ_out))
(⊢ (cond [test- body-] ... [else_test last-body-]) : τ_out)])
-;; sync channels
+(define-typed-syntax when
+ [(_ test body ...)
+ #:with test- (⇑ test as Bool)
+ #:with [(body- _) ...] (infers+erase #'(body ...))
+ (⊢ (when test- body- ...) : Unit)])
+
+;; sync channels and threads
(define-type-constructor Channel)
(define-typed-syntax make-channel
@@ -459,7 +468,8 @@
#:when (same-types? #'(ty ...))
#:with one-ty (stx-car #'(ty ...))
(⊢ (vector v- ...) : (Vector one-ty))])
-(define-typed-syntax make-vector
+(define-typed-syntax make-vector/tc #:export-as make-vector
+ [(_ n) #'(make-vector/tc n (ext-stlc:#%datum . 0))]
[(_ n e)
#:with n- (⇑ n as Int)
#:with [e- ty] (infer+erase #'e)
@@ -480,6 +490,14 @@
#:with [v- ty_v] (infer+erase #'v)
#:when (typecheck? #'ty_v #'ty)
(⊢ (vector-set! e- n- v-) : Unit)])
+(define-typed-syntax vector-copy!
+ [(_ dest start src)
+ #:with start- (⇑ start as Int)
+ #:with [dest- (ty_dest)] (⇑ dest as Vector)
+ #:with [src- (ty_src)] (⇑ src as Vector)
+ #:when (typecheck? #'ty_dest #'ty_src)
+ (⊢ (vector-copy! dest- start- src-) : Unit)])
+
;; sequences and for loops
@@ -493,6 +511,12 @@
[(_ start end step)
#:with (e- ...) (⇑s (start end step) as Int)
(⊢ (in-range e- ...) : (Sequence Int))])
+
+(define-typed-syntax in-vector
+ [(_ e)
+ #:with [e- (ty)] (⇑ e as Vector)
+ (⊢ (in-vector e-) : (Sequence ty))])
+
(define-typed-syntax for
[(_ ([x:id e]...) body)
#:with ([e- (ty)] ...) (⇑s (e ...) as Sequence)
@@ -504,8 +528,52 @@
#:with [(x- ...) body- ty_body] (infer/ctx+erase #'([x : ty] ...) #'body)
(⊢ (for* ([x- e-] ...) body-) : Unit)])
+(define-typed-syntax for/list
+ [(_ ([x:id e]...) body)
+ #:with ([e- (ty)] ...) (⇑s (e ...) as Sequence)
+ #:with [(x- ...) body- ty_body] (infer/ctx+erase #'([x : ty] ...) #'body)
+ (⊢ (for/list ([x- e-] ...) body-) : (List ty_body))])
+(define-typed-syntax for*/list
+ [(_ ([x:id e]...) body)
+ #:with ([e- (ty)] ...) (⇑s (e ...) as Sequence)
+ #:with [(x- ...) body- ty_body] (infer/ctx+erase #'([x : ty] ...) #'body)
+ (⊢ (for*/list ([x- e-] ...) body-) : (List ty_body))])
+
+; printing and displaying
(define-typed-syntax printf
[(_ str e ...)
#:with s- (⇑ str as String)
#:with ([e- ty] ...) (infers+erase #'(e ...))
(⊢ (printf s- e- ...) : Unit)])
+(define-typed-syntax display
+ [(_ e)
+ #:with [e- _] (infer+erase #'e)
+ (⊢ (display e-) : Unit)])
+(define-typed-syntax displayln
+ [(_ e)
+ #:with [e- _] (infer+erase #'e)
+ (⊢ (displayln e-) : Unit)])
+(define-primop newline : (→ Unit))
+
+(define-typed-syntax list->vector
+ [(_ e)
+ #:with [e- (ty)] (⇑ e as List)
+ (⊢ (list->vector e-) : (Vector ty))])
+
+(define-typed-syntax let
+ [(_ name:id (~datum :) ty:type ~! ([x:id e] ...) b ... body)
+ #:with ([e- ty_e] ...) (infers+erase #'(e ...))
+ #:with [(name- . xs-) (body- ...) (_ ... ty_body)]
+ (infers/ctx+erase #'([name : (→ ty_e ... ty.norm)][x : ty_e] ...)
+ #'(b ... body))
+ (⊢ (letrec ([name- (λ xs- body- ...)])
+ (name- e- ...))
+ : ty_body)]
+ [(_ ([x:id e] ...) body ...)
+ #'(ext-stlc:let ([x e] ...) (begin/tc body ...))])
+
+(define-typed-syntax begin/tc #:export-as begin
+ [(_ body ... b)
+ #:with expected (get-expected-type stx)
+ #:with b_ann (add-expected-type #'b #'expected)
+ #'(ext-stlc:begin body ... b_ann)])
diff --git a/tapl/tests/mlish/fannkuch.mlish b/tapl/tests/mlish/fannkuch.mlish
@@ -0,0 +1,54 @@
+#lang s-exp "../../mlish.rkt"
+(require "../rackunit-typechecking.rkt")
+
+(define (fannkuch [n : Int] -> Int)
+ (let ([pi (list->vector
+ (for/list ([i (in-range n)]) i))]
+ [tmp (make-vector n)]
+ [count (make-vector n)])
+ (let loop : Int ([flips 0] [perms 0] [r n])
+ #;(when (< perms 30)
+ (for ([x (in-vector pi)])
+ (display (add1 x)))
+ (newline))
+ (for ([i (in-range r)])
+ (vector-set! count i (add1 i)))
+ (let ((flips2 (max (count-flips pi tmp) flips)))
+ (let loop2 : Int ([r 1])
+ (if (= r n)
+ flips2
+ (let ((perm0 (vector-ref pi 0)))
+ (for ([i (in-range r)])
+ (vector-set! pi i (vector-ref pi (add1 i))))
+ (vector-set! pi r perm0)
+ (vector-set! count r (sub1 (vector-ref count r)))
+ (cond
+ [(<= (vector-ref count r) 0)
+ (loop2 (add1 r))]
+ [else (loop flips2 (add1 perms) r)]))))))))
+
+(define (count-flips [pi : (Vector Int)] [rho : (Vector Int)] -> Int)
+ (vector-copy! rho 0 pi)
+ (let loop : Int ([i 0])
+ (if (= (vector-ref rho 0) 0)
+ i
+ (begin
+ (vector-reverse-slice! rho 0 (add1 (vector-ref rho 0)))
+ (loop (add1 i))))))
+
+(define (vector-reverse-slice! [v : (Vector X)] [i : Int] [j : Int] -> Unit)
+ (let loop : Unit ([i i] [j (sub1 j)])
+ (when (> j i)
+ (vector-swap! v i j)
+ (loop (add1 i) (sub1 j)))))
+
+(define (vector-swap! [v : (Vector X)] [i : Int] [j : Int] -> Unit)
+ (let ((t (vector-ref v i)))
+ (vector-set! v i (vector-ref v j))
+ (vector-set! v j t)))
+
+(check-type (fannkuch 5) : Int -> 7)
+(check-type (fannkuch 6) : Int -> 10)
+(check-type (fannkuch 7) : Int -> 16)
+(check-type (fannkuch 8) : Int -> 22)
+(check-type (fannkuch 9) : Int -> 30)
diff --git a/tapl/tests/run-all-mlish-tests.rkt b/tapl/tests/run-all-mlish-tests.rkt
@@ -3,3 +3,6 @@
(require "mlish/queens.mlish")
(require "mlish/trees.mlish")
(require "mlish/chameneos.mlish")
+(require "mlish/ack.mlish")
+(require "mlish/ary.mlish")
+(require "mlish/fannkuch.mlish")
