diff --git a/tapl/mlish.rkt b/tapl/mlish.rkt index d50b742..18431ad 100644 --- 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 new file mode 100644 index 0000000..27ec3ea --- /dev/null +++ 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 index 22e40c7..e5a44a8 100644 --- 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")