From 1d50b065b984544bb9809d401524de5cdbcdfb03 Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Fri, 1 Jul 2016 12:05:26 -0400 Subject: [PATCH] copy over the rest of the mlish tests --- macrotypes/examples/mlish-do.rkt | 7 +- macrotypes/examples/mlish.rkt | 64 +- macrotypes/examples/tests/mlish/ack.mlish | 27 + macrotypes/examples/tests/mlish/alex.mlish | 25 + macrotypes/examples/tests/mlish/ary.mlish | 26 + macrotypes/examples/tests/mlish/bg/README.md | 103 + .../tests/mlish/bg/basics-general.mlish | 59 + .../examples/tests/mlish/bg/basics.mlish | 370 ++++ .../examples/tests/mlish/bg/basics2.mlish | 138 ++ .../examples/tests/mlish/bg/huffman.mlish | 278 +++ .../examples/tests/mlish/bg/lambda.mlish | 95 + .../examples/tests/mlish/bg/monad.mlish | 122 ++ .../examples/tests/mlish/bg/okasaki.mlish | 1654 +++++++++++++++++ .../examples/tests/mlish/chameneos.mlish | 129 ++ .../examples/tests/mlish/fannkuch.mlish | 54 + macrotypes/examples/tests/mlish/fasta.mlish | 191 ++ macrotypes/examples/tests/mlish/fibo.mlish | 22 + macrotypes/examples/tests/mlish/find.mlish | 87 + macrotypes/examples/tests/mlish/hash.mlish | 19 + .../tests/mlish/infer-variances.mlish | 243 +++ macrotypes/examples/tests/mlish/inst.mlish | 74 + macrotypes/examples/tests/mlish/knuc.mlish | 67 + .../examples/tests/mlish/listpats.mlish | 70 + macrotypes/examples/tests/mlish/loop.mlish | 121 ++ macrotypes/examples/tests/mlish/match2.mlish | 298 +++ macrotypes/examples/tests/mlish/matrix.mlish | 73 + macrotypes/examples/tests/mlish/nbody.mlish | 185 ++ .../examples/tests/mlish/polyrecur.mlish | 117 ++ macrotypes/examples/tests/mlish/queens.mlish | 186 ++ macrotypes/examples/tests/mlish/result.mlish | 129 ++ macrotypes/examples/tests/mlish/sweet-map.rkt | 20 + macrotypes/examples/tests/mlish/term.mlish | 295 +++ .../examples/tests/mlish/trees-tests.mlish | 51 + macrotypes/examples/tests/mlish/trees.mlish | 8 + .../mlish/value-restriction-example.mlish | 25 + .../examples/tests/run-all-mlish-tests.rkt | 45 + .../examples/tests/run-mlish-tests1.rkt | 22 + .../examples/tests/run-mlish-tests2.rkt | 24 + .../examples/tests/run-mlish-tests3.rkt | 7 + .../examples/tests/run-mlish-tests4.rkt | 5 + 40 files changed, 5500 insertions(+), 35 deletions(-) create mode 100644 macrotypes/examples/tests/mlish/ack.mlish create mode 100644 macrotypes/examples/tests/mlish/alex.mlish create mode 100644 macrotypes/examples/tests/mlish/ary.mlish create mode 100644 macrotypes/examples/tests/mlish/bg/README.md create mode 100644 macrotypes/examples/tests/mlish/bg/basics-general.mlish create mode 100644 macrotypes/examples/tests/mlish/bg/basics.mlish create mode 100644 macrotypes/examples/tests/mlish/bg/basics2.mlish create mode 100644 macrotypes/examples/tests/mlish/bg/huffman.mlish create mode 100644 macrotypes/examples/tests/mlish/bg/lambda.mlish create mode 100644 macrotypes/examples/tests/mlish/bg/monad.mlish create mode 100644 macrotypes/examples/tests/mlish/bg/okasaki.mlish create mode 100644 macrotypes/examples/tests/mlish/chameneos.mlish create mode 100644 macrotypes/examples/tests/mlish/fannkuch.mlish create mode 100644 macrotypes/examples/tests/mlish/fasta.mlish create mode 100644 macrotypes/examples/tests/mlish/fibo.mlish create mode 100644 macrotypes/examples/tests/mlish/find.mlish create mode 100644 macrotypes/examples/tests/mlish/hash.mlish create mode 100644 macrotypes/examples/tests/mlish/infer-variances.mlish create mode 100644 macrotypes/examples/tests/mlish/inst.mlish create mode 100644 macrotypes/examples/tests/mlish/knuc.mlish create mode 100644 macrotypes/examples/tests/mlish/listpats.mlish create mode 100644 macrotypes/examples/tests/mlish/loop.mlish create mode 100644 macrotypes/examples/tests/mlish/match2.mlish create mode 100644 macrotypes/examples/tests/mlish/matrix.mlish create mode 100644 macrotypes/examples/tests/mlish/nbody.mlish create mode 100644 macrotypes/examples/tests/mlish/polyrecur.mlish create mode 100644 macrotypes/examples/tests/mlish/queens.mlish create mode 100644 macrotypes/examples/tests/mlish/result.mlish create mode 100644 macrotypes/examples/tests/mlish/sweet-map.rkt create mode 100644 macrotypes/examples/tests/mlish/term.mlish create mode 100644 macrotypes/examples/tests/mlish/trees-tests.mlish create mode 100644 macrotypes/examples/tests/mlish/trees.mlish create mode 100644 macrotypes/examples/tests/mlish/value-restriction-example.mlish create mode 100644 macrotypes/examples/tests/run-all-mlish-tests.rkt create mode 100644 macrotypes/examples/tests/run-mlish-tests1.rkt create mode 100644 macrotypes/examples/tests/run-mlish-tests2.rkt create mode 100644 macrotypes/examples/tests/run-mlish-tests3.rkt create mode 100644 macrotypes/examples/tests/run-mlish-tests4.rkt diff --git a/macrotypes/examples/mlish-do.rkt b/macrotypes/examples/mlish-do.rkt index 10df324..1c96b15 100644 --- a/macrotypes/examples/mlish-do.rkt +++ b/macrotypes/examples/mlish-do.rkt @@ -12,13 +12,12 @@ [(do bind:id body:expr) #'body] [(do bind:id - [x1:id : t1:expr - <- m1:expr] + [x1:id <- m1:expr] rst ... body:expr) #'(bind m1 - (λ ([x1 : t1]) + (λ (x1) (do bind rst ... body)))] [(do bind:id [m1:expr] @@ -26,7 +25,7 @@ body:expr) #'(bind m1 - (λ ([dummy : Unit]) + (λ (dummy) (do bind rst ... body)))] )) diff --git a/macrotypes/examples/mlish.rkt b/macrotypes/examples/mlish.rkt index eca45bc..aac7a0e 100644 --- a/macrotypes/examples/mlish.rkt +++ b/macrotypes/examples/mlish.rkt @@ -696,8 +696,7 @@ infer/ctx+erase #'(ctx ...) #'((add-expected e_body ty-expected) ...)) #:when (check-exhaust #'(pat- ...) #'τ_e) - #:with τ_out (stx-foldr (current-join) (stx-car #'(ty_body ...)) (stx-cdr #'(ty_body ...))) - (⊢ (match- e- [pat- (let- ([x- x] ...) e_body-)] ...) : τ_out) + (⊢ (match- e- [pat- (let- ([x- x] ...) e_body-)] ...) : (⊔ ty_body ...)) ])])) (define-typed-syntax match #:datum-literals (with) @@ -736,7 +735,6 @@ #:with ([(x- ... rst-) e_body- ty_body] ...) (stx-map (lambda (ctx e) (infer/ctx+erase ctx e)) #'(([x ty] ... [rst (List ty)]) ...) #'((add-expected e_body t_expect) ...)) - #:with τ_out (stx-foldr (current-join) (stx-car #'(ty_body ...)) (stx-cdr #'(ty_body ...))) #:with (len ...) (stx-map (lambda (p) #`#,(stx-length p)) #'((x ...) ...)) #:with (lenop ...) (stx-map (lambda (p) (if (brack? p) #'=- #'>=-)) #'(xs ...)) #:with (pred? ...) (stx-map @@ -752,7 +750,7 @@ (cond- [(pred? z) (let- ([x- (acc1 z)] ... [rst- (acc2 z)]) e_body-)] ...)) - : τ_out)])] + : (⊔ ty_body ...))])] [else ;; e is variant (syntax-parse #'clauses #:datum-literals (->) [([Clause:id x:id ... @@ -794,14 +792,13 @@ #:fail-unless (and (same-types? #'(τ_guard ...)) (Bool? (stx-car #'(τ_guard ...)))) "guard expression(s) must have type bool" - #:with τ_out (stx-foldr (current-join) (stx-car #'(τ_ec ...)) (stx-cdr #'(τ_ec ...))) #:with z (generate-temporary) ; dont duplicate eval of test expr (⊢ (let- ([z e-]) (cond- [(and- (Cons? z) (let- ([x- (acc z)] ...) e_guard-)) (let- ([x- (acc z)] ...) e_c-)] ...)) - : τ_out)])])]) + : (⊔ τ_ec ...))])])]) ; special arrow that computes free vars; for use with tests ; (because we can't write explicit forall @@ -894,20 +891,19 @@ #:with ty-expected (get-expected-type stx) #:with ([body- ty_body] ...) (infers+erase #'((add-expected body ty-expected) ...)) #:with (([b- ty_b] ...) ...) (stx-map infers+erase #'((b ...) ...)) - #:with τ_out (stx-foldr (current-join) (stx-car #'(ty_body ...)) (stx-cdr #'(ty_body ...))) - (⊢ (cond- [test- b- ... body-] ...) : τ_out)]) + (⊢ (cond- [test- b- ... body-] ...) : (⊔ ty_body ...))]) (define-typed-syntax when [(when test body ...) ; #:with test- (⇑ test as Bool) #:with [test- _] (infer+erase #'test) #:with [(body- _) ...] (infers+erase #'(body ...)) - (⊢ (when- test- body- ...) : Unit)]) + (⊢ (when- test- body- ... (void-)) : Unit)]) (define-typed-syntax unless [(unless test body ...) ; #:with test- (⇑ test as Bool) #:with [test- _] (infer+erase #'test) #:with [(body- _) ...] (infers+erase #'(body ...)) - (⊢ (unless- test- body- ...) : Unit)]) + (⊢ (unless- test- body- ... (void-)) : Unit)]) ;; sync channels and threads (define-type-constructor Channel) @@ -918,15 +914,14 @@ (⊢ (make-channel-) : (Channel ty))]) (define-typed-syntax channel-get [(channel-get c) - #:with (c- (ty)) (⇑ c as Channel) + #:with [c- (~Channel ty)] (infer+erase #'c) (⊢ (channel-get- c-) : ty)]) (define-typed-syntax channel-put [(channel-put c v) - #:with (c- (ty)) (⇑ c as Channel) + #:with [c- (~Channel ty)] (infer+erase #'c) #:with [v- ty_v] (infer+erase #'v) #:fail-unless (typechecks? #'ty_v #'ty) - (format "Cannot send ~a value on ~a channel." - (type->str #'ty_v) (type->str #'ty)) + (typecheck-fail-msg/1 #'ty #'ty_v #'v) (⊢ (channel-put- c- v-) : Unit)]) (define-base-type Thread) @@ -989,16 +984,18 @@ (define-typed-syntax vector-set! [(vector-set! e n v) #:with n- (⇑ n as Int) - #:with [e- (ty)] (⇑ e as Vector) + #:with [e- (~Vector ty)] (infer+erase #'e) #:with [v- ty_v] (infer+erase #'v) - #:when (typecheck? #'ty_v #'ty) + #:fail-unless (typecheck? #'ty_v #'ty) + (typecheck-fail-msg/1 #'ty #'ty_v #'v) (⊢ (vector-set!- e- n- v-) : Unit)]) (define-typed-syntax vector-copy! [(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) + #:with [dest- (~Vector ty_dest)] (infer+erase #'dest) + #:with [src- (~Vector ty_src)] (infer+erase #'src) + #:fail-unless (typecheck? #'ty_dest #'ty_src) + (typecheck-fail-msg/1 #'(Vector ty_src) #'(Vector ty_dest) #'dest) (⊢ (vector-copy!- dest- start- src-) : Unit)]) @@ -1173,30 +1170,34 @@ (⊢ (make-hash- (list- (cons- k- v-) ...)) : (Hash ty_key ty_val))]) (define-typed-syntax hash-set! [(hash-set! h k v) - #:with [h- (ty_key ty_val)] (⇑ h as Hash) + #:with [h- (~Hash ty_key ty_val)] (infer+erase #'h) #:with [k- ty_k] (infer+erase #'k) #:with [v- ty_v] (infer+erase #'v) - #:when (typecheck? #'ty_k #'ty_key) - #:when (typecheck? #'ty_v #'ty_val) + #:fail-unless (typecheck? #'ty_k #'ty_key) (typecheck-fail-msg/1 #'ty_key #'ty_k #'k) + #:fail-unless (typecheck? #'ty_v #'ty_val) (typecheck-fail-msg/1 #'ty_val #'ty_v #'v) (⊢ (hash-set!- h- k- v-) : Unit)]) (define-typed-syntax hash-ref [(hash-ref h k) - #:with [h- (ty_key ty_val)] (⇑ h as Hash) + #:with [h- (~Hash ty_key ty_val)] (infer+erase #'h) #:with [k- ty_k] (infer+erase #'k) - #:when (typecheck? #'ty_k #'ty_key) + #:fail-unless (typecheck? #'ty_k #'ty_key) + (typecheck-fail-msg/1 #'ty_key #'ty_k #'k) (⊢ (hash-ref- h- k-) : ty_val)] [(hash-ref h k fail) - #:with [h- (ty_key ty_val)] (⇑ h as Hash) + #:with [h- (~Hash ty_key ty_val)] (infer+erase #'h) #:with [k- ty_k] (infer+erase #'k) - #:when (typecheck? #'ty_k #'ty_key) + #:fail-unless (typecheck? #'ty_k #'ty_key) + (typecheck-fail-msg/1 #'ty_key #'ty_k #'k) #:with [fail- (~?∀ () (~ext-stlc:→ ty_fail))] (infer+erase #'fail) - #:when (typecheck? #'ty_fail #'ty_val) + #:fail-unless (typecheck? #'ty_fail #'ty_val) + (typecheck-fail-msg/1 #'(→ ty_val) #'(→ ty_fail) #'fail) (⊢ (hash-ref- h- k- fail-) : ty_val)]) (define-typed-syntax hash-has-key? [(hash-has-key? h k) - #:with [h- (ty_key _)] (⇑ h as Hash) + #:with [h- (~Hash ty_key _)] (infer+erase #'h) #:with [k- ty_k] (infer+erase #'k) - #:when (typecheck? #'ty_k #'ty_key) + #:fail-unless (typecheck? #'ty_k #'ty_key) + (typecheck-fail-msg/1 #'ty_key #'ty_k #'k) (⊢ (hash-has-key?- h- k-) : Bool)]) (define-typed-syntax hash-count @@ -1218,7 +1219,7 @@ #:with out- (⇑ out as String-Port) #:with start- (⇑ start as Int) #:with end- (⇑ end as Int) - (⊢ (write-string- str- out- start- end-) : Unit)]) + (⊢ (begin- (write-string- str- out- start- end-) (void-)) : Unit)]) (define-typed-syntax string-length [(string-length str) @@ -1263,7 +1264,8 @@ [(set! x:id e) #:with [x- ty_x] (infer+erase #'x) #:with [e- ty_e] (infer+erase #'e) - #:when (typecheck? #'ty_e #'ty_x) + #:fail-unless (typecheck? #'ty_e #'ty_x) + (typecheck-fail-msg/1 #'ty_x #'ty_e #'e) (⊢ (set!- x e-) : Unit)]) (define-typed-syntax provide-type [(provide-type ty ...) #'(provide- ty ...)]) diff --git a/macrotypes/examples/tests/mlish/ack.mlish b/macrotypes/examples/tests/mlish/ack.mlish new file mode 100644 index 0000000..b29225b --- /dev/null +++ b/macrotypes/examples/tests/mlish/ack.mlish @@ -0,0 +1,27 @@ +#lang s-exp "../../mlish.rkt" +(require "../rackunit-typechecking.rkt") + +;; tests cond with else + +(define (ack/else [m : Int] [n : Int] -> Int) + (cond + [(zero? m) (add1 n)] + [(zero? n) (ack/else (sub1 m) 1)] + [else + (ack/else (sub1 m) (ack/else m (sub1 n)))])) + +(check-type (ack/else 0 0) : Int -> 1) +(check-type (ack/else 1 1) : Int -> 3) +(check-type (ack/else 2 2) : Int -> 7) +(check-type (ack/else 3 4) : Int -> 125) + +(define (ack [m : Int] [n : Int] -> Int) + (cond + [(zero? m) (add1 n)] + [(zero? n) (ack (sub1 m) 1)] + [#t (ack (sub1 m) (ack m (sub1 n)))])) + +(check-type (ack 0 0) : Int -> 1) +(check-type (ack 1 1) : Int -> 3) +(check-type (ack 2 2) : Int -> 7) +(check-type (ack 3 4) : Int -> 125) diff --git a/macrotypes/examples/tests/mlish/alex.mlish b/macrotypes/examples/tests/mlish/alex.mlish new file mode 100644 index 0000000..9e80c23 --- /dev/null +++ b/macrotypes/examples/tests/mlish/alex.mlish @@ -0,0 +1,25 @@ +#lang s-exp "../../mlish.rkt" +(require "../rackunit-typechecking.rkt") + +;; the following function def produces error: +;; define: Function should-err's body (let ((y (f x))) x) has type X, which +;; does not match given type Y. +;; TODO: add check-_ rackunit form for functions +#;(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)) + +(define (accept-A×A [pair : (× A A)] → (× A A)) + pair) + +(typecheck-fail (accept-A×A (tup 8 "ate")) + #:with-msg "couldn't unify Int and String\n *expected: \\(× A A\\)\n *given: \\(× Int String\\)") + +(typecheck-fail (ann (accept-A×A (tup 8 "ate")) : (× String String)) + #:with-msg "expected: \\(× String String\\)\n *given: \\(× Int String\\)") + diff --git a/macrotypes/examples/tests/mlish/ary.mlish b/macrotypes/examples/tests/mlish/ary.mlish new file mode 100644 index 0000000..16280c2 --- /dev/null +++ b/macrotypes/examples/tests/mlish/ary.mlish @@ -0,0 +1,26 @@ +#lang s-exp "../../mlish.rkt" +(require "../rackunit-typechecking.rkt") + +;; test vectors and for loops +(define (main [args : (Vector String)] -> (× Int Int)) + (let* ([n (if (zero? (vector-length args)) + 1 + (string->number (vector-ref args 0)))] + [x (make-vector n 0)] + [y (make-vector n 0)] + [last (sub1 n)]) + (begin + (for ([i (in-range n)]) + (vector-set! x i (add1 i))) + (for* ([k (in-range 1000)] + [i (in-range last -1 -1)]) + (vector-set! y i (+ (vector-ref x i) (vector-ref y i)))) + (tup (vector-ref y 0) + (vector-ref y last))))) + +(check-type (main (vector "100")) + : (× Int Int) -> (tup 1000 100000)) +(check-type (main (vector "1000")) + : (× Int Int) -> (tup 1000 1000000)) +(check-type (main (vector "10000")) + : (× Int Int) -> (tup 1000 10000000)) diff --git a/macrotypes/examples/tests/mlish/bg/README.md b/macrotypes/examples/tests/mlish/bg/README.md new file mode 100644 index 0000000..5d29aa9 --- /dev/null +++ b/macrotypes/examples/tests/mlish/bg/README.md @@ -0,0 +1,103 @@ +bg +=== + +mlish tests by Ben + +`basics-general` +--- +``` +(map [f : (→ A B)] [x* : (List A)] → (List B)) +(append [x* : (List A)] [y* : (List A)] → (List A)) +(fst [xy : (** A B)] → A) +(snd [xy : (** A B)] → B) +(member [x* : (List A)] [y : A] → Bool) +(foldl [f : (→ A B A)] [acc : A] [x* : (List B)] → A) +(foldr [f : (→ A B B)] [x* : (List A)] [acc : B] → B) +(filter [f : (→ A Bool)] [x* : (List A)] → (List A)) +(sum [x* : (List Float)] → Float) +(reverse [x* : (List A)] → (List A)) +``` + +`basics` +--- +``` +(fn-list [f* : (List (→ A A))] [a : A] → A) +(count-letters/one [s : String] [c : Char] → Int) +(count-letters [s* : (List String)] [c : Char] → Int) +(flatten [x** : (List (List A))] → (List A)) +(insert [x : A] → (→ (List A) (List (List A)))) +(permutations [x* : (List A)] → (List (List A))) +(split [ab* : (List (** A B))] → (** (List A) (List B))) +(combine [a*b* : (** (List A) (List B))] → (List (** A B))) +(convolve [x* : (List Float)] [y* : (List Float)] → Float) +(mc [n : Int] [f : (→ A A)] [x : A] → A) +(square [n : Int] → Int) +(successor [mcn : (→ (→ A A) A A)] → (→ (→ A A) A A)) +(split2 [x* : (List A)] → (** (List A) (List A))) +(merge [x*+y* : (** (List Int) (List Int))] → (List Int)) +(mergesort {x* : (List Int)} → (List Int)) +(quicksort [x* : (List Int)] → (List Int)) +(fact [n : Int] → Int) +(range-aux [n : Int] → (List Int)) +(range [n : Int] → (List Int)) +(fact-acc [n : Int] → Int) +(fact-cps-aux [n : Int] [k : (→ Int Int)] → Int) +(fact-cps [n : Int] → Int) +(map-cps-aux [f : (→ A B)] [x* : (List A)] [k : (→ (List B) (List B))] → (List B)) +(map-cps [f : (→ A B)] [x* : (List A)] → (List B)) +``` + +`basics2` +--- +``` +(map-index [is* : (List (** Int (List String)))] → (List (** String Int))) +(reduce-index [si* : (List (** String Int))] → (List (** String (List Int)))) +(make-index [is* : (List (** Int (List String)))] → (List (** String (List Int)))) +``` + +`huffman` +--- +``` +(empty → Symbol*) +(singleton [s : String] → Symbol*) +(insert [s* : Symbol*] [s1 : String] → Symbol*) +(union [s1 : Symbol*] [s2 : Symbol*] → Symbol*) +(contains [s* : Symbol*] [s : Symbol] → Bool) +(list [x : A] → (List A)) +(append [x* : (List A)] [y* : (List A)] → (List A)) +(length [x* : (List A)] → Int) +(symbols [h : HTree] → Symbol*) +(weight [h : HTree] → Int) +(make-code-tree [left : HTree] [right : HTree] → HTree) +(decode-aux [bits : Bit*] [root : HTree] [current-branch : HTree] → SymbolList) +(decode [bits : Bit*] [tree : HTree] → SymbolList) +(choose-branch [bit : Bit] [branch : HTree] → HTree) +(adjoin-set [x : HTree] [set : HTreeSet] → HTreeSet) +(make-leaf-set [pair* : (List (× Symbol Int))] → HTreeSet) +sample-tree +sample-message +(encode [message : SymbolList] [tree : HTree] → Bit*) +(contains-symbol [s : Symbol] [tree : HTree] → Bool) +(encode-symbol [s : Symbol] [tree : HTree] → Bit*) +(generate-huffman-tree [pair* : (List (× Symbol Frequency))] → HTree) +(successive-merge [tree* : HTreeSet] → HTree) +rock-pair* +rock-tree (generate-huffman-tree rock-pair*)) +rock-message +rock-bit* (encode rock-message rock-tree)) +``` + + +`lambda` +--- +``` +(fresh [e : Λ] → Int) +(subst [e : Λ] [i : Int] [v : Λ] → Λ) +(simpl-aux [e : Λ] [i : Int] → (× Int Λ)) +(simpl [e : Λ] → Λ) +(eval [e : Λ] → Λ) +I (Lambda 0 (Var 0)) +K (Lambda 0 (Lambda 1 (Var 0))) +S (Lambda 0 (Lambda 1 (Lambda 2 (App (App (Var 0) (Var 2)) (App (Var 1) (Var 2)))))) +false (App S K) +``` diff --git a/macrotypes/examples/tests/mlish/bg/basics-general.mlish b/macrotypes/examples/tests/mlish/bg/basics-general.mlish new file mode 100644 index 0000000..d8261dc --- /dev/null +++ b/macrotypes/examples/tests/mlish/bg/basics-general.mlish @@ -0,0 +1,59 @@ +#lang s-exp "../../../mlish.rkt" + +(define-type (List X) + Nil + (Cons X (List X))) +(define-type (** X Y) + (Pair X Y)) +(define-type Bool + True + False) + +(define (map [f : (→ A B)] [x* : (List A)] → (List B)) + (match x* with + [Nil -> Nil] + [Cons x x* -> (Cons (f x) (map f x*))])) + +(define (append [x* : (List A)] [y* : (List A)] → (List A)) + (match x* with + [Nil -> y*] + [Cons x x* -> (Cons x (append x* y*))])) + +(define (fst [xy : (** A B)] → A) + (match xy with + [Pair x y -> x])) + +(define (snd [xy : (** A B)] → B) + (match xy with + [Pair x y -> y])) + +(define (member [x* : (List A)] [y : A] → Bool) + (match x* with + [Nil -> False] + [Cons x x* -> + (if (equal? x y) True (member x* y))])) + +(define (foldl [f : (→ A B A)] [acc : A] [x* : (List B)] → A) + (match x* with + [Nil -> acc] + [Cons x x* -> (foldl f (f acc x) x*)])) + +(define (foldr [f : (→ A B B)] [x* : (List A)] [acc : B] → B) + (match x* with + [Nil -> acc] + [Cons x x* -> (f x (foldr f x* acc))])) + +(define (filter [f : (→ A Bool)] [x* : (List A)] → (List A)) + (foldr (λ ([x : A] [acc : (List A)]) (match (f x) with [True -> (Cons x acc)] [False -> acc])) + x* + Nil)) + +(define (sum [x* : (List Float)] → Float) + (foldl fl+ (exact->inexact 0) x*)) + +(define (reverse [x* : (List A)] → (List A)) + (foldl (λ ([x* : (List A)] [x : A]) (Cons x x*)) Nil x*)) + +(provide-type List Nil Cons ** Pair Bool True False) + +(provide map append fst snd member foldl foldr filter sum reverse) diff --git a/macrotypes/examples/tests/mlish/bg/basics.mlish b/macrotypes/examples/tests/mlish/bg/basics.mlish new file mode 100644 index 0000000..5c07d0f --- /dev/null +++ b/macrotypes/examples/tests/mlish/bg/basics.mlish @@ -0,0 +1,370 @@ +#lang s-exp "../../../mlish.rkt" +(require "../../rackunit-typechecking.rkt") +(require "basics-general.mlish") +(require-typed map append fst snd member foldl foldr filter sum reverse + #:from "basics-general.mlish") + +;; ============================================================================= +;; http://www.cs.cornell.edu/courses/cs3110/2011fa/hw/ps1/ps1.html + +(define (fn-list [f* : (List (→ A A))] [a : A] → A) + (match f* with + [Nil -> a] + [Cons f f* -> (fn-list f* (f a))])) + +(check-type + (fn-list (Cons (λ ([x : Int]) (+ x 1)) (Cons (λ ([x : Int]) (* x 2)) Nil)) 4) + : Int + ⇒ 10) + +;; ----------------------------------------------------------------------------- + +(define (count-letters/one [s : String] [c : Char] → Int) + (for/sum ([i (in-range (string-length s))]) + (if (equal? (string-ref s i) c) + 1 + 0))) + +(define (count-letters [s* : (List String)] [c : Char] → Int) + (match s* with + [Nil -> 0] + [Cons s s* -> (+ (count-letters/one s c) + (count-letters s* c))])) + +(check-type + (count-letters (Cons "OCaml" (Cons "Is" (Cons "Alot" (Cons "Better" (Cons "Than" (Cons "Java" Nil)))))) (string-ref "a" 0)) + : Int + ⇒ 4) + +;; ----------------------------------------------------------------------------- + +(define (flatten [x** : (List (List A))] → (List A)) + (match x** with + [Nil -> Nil] + [Cons x* x** -> (append x* (flatten x**))])) + +(define (insert [x : A] → (→ (List A) (List (List A)))) + (λ ([x* : (List A)]) + (Cons (Cons x x*) + (match x* with + [Nil -> Nil] + [Cons y y* -> (map (λ ([z* : (List A)]) (Cons y z*)) + ((insert x) y*))])))) + +(define (permutations [x* : (List A)] → (List (List A))) + (match x* with + [Nil -> (Cons Nil Nil)] + [Cons x x* -> (flatten (map (insert x) (permutations x*)))])) + +(check-type + (permutations Nil) + : (List (List Int)) + ⇒ (Cons Nil Nil)) + +(check-type + (permutations (Cons 1 Nil)) + : (List (List Int)) + ⇒ (Cons (Cons 1 Nil) Nil)) + +(check-type + (permutations (Cons 1 (Cons 2 Nil))) + : (List (List Int)) + ⇒ (Cons (Cons 1 (Cons 2 Nil)) (Cons (Cons 2 (Cons 1 Nil)) Nil))) + +(check-type + (permutations (Cons 1 (Cons 2 (Cons 3 Nil)))) + : (List (List Int)) + ⇒ (Cons (Cons 1 (Cons 2 (Cons 3 Nil))) + (Cons (Cons 2 (Cons 1 (Cons 3 Nil))) + (Cons (Cons 2 (Cons 3 (Cons 1 Nil))) + (Cons (Cons 1 (Cons 3 (Cons 2 Nil))) + (Cons (Cons 3 (Cons 1 (Cons 2 Nil))) + (Cons (Cons 3 (Cons 2 (Cons 1 Nil))) + Nil))))))) + +;; ============================================================================= +;; http://www.cs.cornell.edu/courses/cs3110/2011sp/hw/ps1/ps1.htm + +(define (split [ab* : (List (** A B))] → (** (List A) (List B))) + (match ab* with + [Nil -> (Pair Nil Nil)] + [Cons ab ab* -> + (match ab with + [Pair a b -> + (match (split ab*) with + [Pair a* b* -> + (Pair (Cons a a*) + (Cons b b*))])])])) + +(check-type + (split Nil) + : (** (List Int) (List Int)) + ⇒ (Pair Nil Nil)) + +(check-type + (split (Cons (Pair 1 2) (Cons (Pair 3 4) Nil))) + : (** (List Int) (List Int)) + ⇒ (Pair (Cons 1 (Cons 3 Nil)) + (Cons 2 (Cons 4 Nil)))) + +(check-type + (split (Cons (Pair 1 "one") (Cons (Pair 2 "two") (Cons (Pair 3 "three") Nil)))) + : (** (List Int) (List String)) + ⇒ (Pair (Cons 1 (Cons 2 (Cons 3 Nil))) + (Cons "one" (Cons "two" (Cons "three" Nil))))) + +;; ----------------------------------------------------------------------------- + +(define (combine [a*b* : (** (List A) (List B))] → (List (** A B))) + (match a*b* with + [Pair a* b* -> + (match a* with + [Nil -> + (match b* with + [Nil -> + Nil] + [Cons b b* -> + Nil])] ;; Error + [Cons a a* -> + (match b* with + [Nil -> + Nil] ;; Error + [Cons b b* -> + (Cons (Pair a b) (combine (Pair a* b*)))])])])) + +(check-type + (combine (Pair Nil Nil)) + : (List (** Int Int)) + ⇒ Nil) + +(check-type + (combine (Pair (Cons 1 (Cons 2 Nil)) (Cons 3 (Cons 4 Nil)))) + : (List (** Int Int)) + ⇒ (Cons (Pair 1 3) (Cons (Pair 2 4) Nil))) + +(check-type + (combine (split (Cons (Pair 1 "one") (Cons (Pair 2 "two") (Cons (Pair 3 "three") Nil))))) + : (List (** Int String)) + ⇒ (Cons (Pair 1 "one") (Cons (Pair 2 "two") (Cons (Pair 3 "three") Nil)))) + +;; ----------------------------------------------------------------------------- + +(define (convolve [x* : (List Float)] [y* : (List Float)] → Float) + (sum + (map (λ ([xy : (** Float Float)]) (fl* (fst xy) (snd xy))) + (combine (Pair x* (reverse y*)))))) + +(check-type + (convolve (Cons 1.0 (Cons 2.0 (Cons 3.0 Nil))) (Cons 1.0 (Cons 2.0 (Cons 3.0 Nil)))) + : Float + ⇒ (fl+ (fl+ (fl* 1.0 3.0) (fl* 2.0 2.0)) (fl* 3.0 1.0))) + +;; ----------------------------------------------------------------------------- + +(define (mc [n : Int] [f : (→ A A)] [x : A] → A) + (for/fold ([x x]) + ([_i (in-range n)]) + (f x))) + +(check-type + (mc 3000 (λ ([n : Int]) (+ n 1)) 3110) + : Int + ⇒ 6110) + +(define (square [n : Int] → Int) + (* n n)) + +(check-type + (mc 0 square 2) + : Int + ⇒ 2) + +(check-type + (mc 2 square 2) + : Int + ⇒ 16) + +(check-type + (mc 3 square 2) + : Int + ⇒ 256) + +;; ----------------------------------------------------------------------------- + +(define (successor [mcn : (→ (→ A A) A A)] → (→ (→ A A) A A)) + (λ ([f : (→ A A)] [x : A]) + (f (mcn f x)))) + +(check-type + ((successor (λ ([f : (→ Int Int)] [x : Int]) (mc 0 f x))) square 2) + : Int + ⇒ 4) + +(check-type + ((successor (successor (λ ([f : (→ Int Int)] [x : Int]) (mc 0 f x)))) square 2) + : Int + ⇒ 16) + +(check-type + ((successor (successor (successor (λ ([f : (→ Int Int)] [x : Int]) (mc 0 f x))))) square 2) + : Int + ⇒ 256) + +;; # (mc 3 successor) (mc 0) square 2;; + +;; ============================================================================= +;; === sorting + +;; ----------------------------------------------------------------------------- +;; --- mergesort + +(define (split2 [x* : (List A)] → (** (List A) (List A))) + (match x* with + [Nil -> (Pair Nil Nil)] + [Cons h t -> + (match t with + [Nil -> (Pair (Cons h Nil) Nil)] + [Cons h2 x* -> + (match (split2 x*) with + [Pair x* y* -> + (Pair (Cons h x*) (Cons h2 y*))])])])) + +(define (merge [x*+y* : (** (List Int) (List Int))] → (List Int)) + (match x*+y* with + [Pair xx* yy* -> + (match xx* with + [Nil -> yy*] + [Cons x x* -> + (match yy* with + [Nil -> xx*] + [Cons y y* -> + (if (<= x y) + (Cons x (merge (Pair x* yy*))) + (Cons y (merge (Pair xx* y*))))])])])) + +(define (mergesort [x* : (List Int)] → (List Int)) + (match x* with + [Nil -> Nil] + [Cons h t -> + (match t with + [Nil -> (Cons h Nil)] + [Cons h2 t2 -> + (match (split2 x*) with + [Pair x* y* -> + (merge (Pair (mergesort x*) (mergesort y*)))])])])) + +(check-type (mergesort Nil) : (List Int) ⇒ Nil) + +(check-type + (mergesort (Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil))))) + : (List Int) + ⇒ (Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil))))) + +(check-type + (mergesort (Cons 3 (Cons 7 (Cons 93 (Cons 0 (Cons 2 Nil)))))) + : (List Int) + ⇒ (Cons 0 (Cons 2 (Cons 3 (Cons 7 (Cons 93 Nil)))))) + +;; ----------------------------------------------------------------------------- +;; --- quicksort + +(define (quicksort [x* : (List Int)] → (List Int)) + (match x* with + [Nil -> x*] + [Cons h t -> + (match t with + [Nil -> x*] + [Cons h2 t2 -> + (append + (quicksort (filter (λ ([y : Int]) (if (<= y h) True False)) t)) + (append + (Cons h Nil) + (quicksort (filter (λ ([y : Int]) (if (> y h) True False)) t))))])])) + +(check-type (quicksort Nil) : (List Int) ⇒ Nil) + +(check-type + (quicksort (Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil))))) + : (List Int) + ⇒ (Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil))))) + +(check-type + (quicksort (Cons 3 (Cons 7 (Cons 93 (Cons 0 (Cons 2 Nil)))))) + : (List Int) + ⇒ (Cons 0 (Cons 2 (Cons 3 (Cons 7 (Cons 93 Nil)))))) + +;; ============================================================================= +;; === CPS + +;; ----------------------------------------------------------------------------- +;; --- factorial + +(define (fact [n : Int] → Int) + (if (< n 2) + 1 + (* n (fact (- n 1))))) + +(define (range-aux [n : Int] → (List Int)) + (if (= 0 n) + (Cons n Nil) + (Cons n (range-aux (- n 1))))) + +(define (range [n : Int] → (List Int)) + (if (<= n 0) + Nil + (reverse (range-aux (- n 1))))) + +(define (fact-acc [n : Int] → Int) + (foldl (λ ([acc : Int] [n : Int]) (* n acc)) 1 (map (λ ([n : Int]) (+ n 1)) (range n)))) + +(define (fact-cps-aux [n : Int] [k : (→ Int Int)] → Int) + (if (< n 2) + (k 1) + (fact-cps-aux (- n 1) (λ ([m : Int]) (k (* n m)))))) + +(define (fact-cps [n : Int] → Int) + (fact-cps-aux n (λ ([x : Int]) x))) + +(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-acc 0) : Int ⇒ 1) +(check-type (fact-acc 1) : Int ⇒ 1) +(check-type (fact-acc 2) : Int ⇒ 2) +(check-type (fact-acc 3) : Int ⇒ 6) +(check-type (fact-acc 4) : Int ⇒ 24) +(check-type (fact-acc 5) : Int ⇒ 120) + +(check-type (fact-cps 0) : Int ⇒ 1) +(check-type (fact-cps 1) : Int ⇒ 1) +(check-type (fact-cps 2) : Int ⇒ 2) +(check-type (fact-cps 3) : Int ⇒ 6) +(check-type (fact-cps 4) : Int ⇒ 24) +(check-type (fact-cps 5) : Int ⇒ 120) + +;; ----------------------------------------------------------------------------- +;; --- map + +(define (map-cps-aux [f : (→ A B)] [x* : (List A)] [k : (→ (List B) (List B))] → (List B)) + (match x* with + [Nil -> (k Nil)] + [Cons x x* -> + (map-cps-aux f x* (λ ([b* : (List B)]) (k (Cons (f x) b*))))])) + +(define (map-cps [f : (→ A B)] [x* : (List A)] → (List B)) + (map-cps-aux f x* (λ ([x : (List B)]) x))) + +(check-type + (map-cps (λ ([x : Int]) (+ x 2)) (Cons 2 (Cons 4 (Cons 8 Nil)))) + : (List Int) + ⇒ (Cons 4 (Cons 6 (Cons 10 Nil)))) + +(check-type + (map-cps exact->inexact (Cons 2 (Cons 4 (Cons 8 Nil)))) + : (List Float) + ⇒ (Cons 2.0 (Cons 4.0 (Cons 8.0 Nil)))) + diff --git a/macrotypes/examples/tests/mlish/bg/basics2.mlish b/macrotypes/examples/tests/mlish/bg/basics2.mlish new file mode 100644 index 0000000..04fd222 --- /dev/null +++ b/macrotypes/examples/tests/mlish/bg/basics2.mlish @@ -0,0 +1,138 @@ +#lang s-exp "../../../mlish.rkt" +(require "../../rackunit-typechecking.rkt") +(require "basics-general.mlish") +(require-typed append filter foldr foldl reverse snd member + #:from "basics-general.mlish") + + +;; ============================================================================= +;; http://www.cs.cornell.edu/courses/cs3110/2011fa/hw/ps1/ps1.html +;; continued + +;; ----------------------------------------------------------------------------- + +(define (map-index [is* : (List (** Int (List String)))] → (List (** String Int))) + (match is* with + [Nil -> Nil] + [Cons hd tl -> + (match hd with + [Pair i s* -> + (append (foldr (λ ([s : String] [acc : (List (** String Int))]) (Cons (Pair s i) acc)) + s* + Nil) + (map-index tl))])])) + +(check-type + (map-index Nil) + : (List (** String Int)) + ⇒ Nil) + +(check-type + (map-index (Cons (Pair 0 (Cons "a" (Cons "b" (Cons "c" Nil)))) Nil)) + : (List (** String Int)) + ⇒ (Cons (Pair "a" 0) (Cons (Pair "b" 0) (Cons (Pair "c" 0) Nil)))) + +(check-type + (map-index (Cons (Pair 0 (Cons "a" (Cons "b" (Cons "c" Nil)))) + (Cons (Pair 1 (Cons "d" (Cons "e" Nil))) + Nil))) + : (List (** String Int)) + ⇒ (Cons (Pair "a" 0) (Cons (Pair "b" 0) (Cons (Pair "c" 0) (Cons (Pair "d" 1) (Cons (Pair "e" 1) Nil)))))) + +(define (reduce-index [si* : (List (** String Int))] → (List (** String (List Int)))) + (snd (foldr + (λ ([si : (** String Int)] [acc : (** (List String) (List (** String (List Int))))]) + (match si with + [Pair s i -> + (match acc with + [Pair seen out -> + (match (member seen s) with + [True -> + (Pair + seen + (foldr + (λ ([si* : (** String (List Int))] [acc : (List (** String (List Int)))]) + (match si* with + [Pair s2 i* -> + (if (equal? s s2) + (match (member i* i) with + [True -> (Cons si* acc)] + [False -> (Cons (Pair s2 (Cons i i*)) acc)]) + (Cons si* acc))])) + out + Nil))] + [False -> + (Pair + (Cons s seen) + (Cons (Pair s (Cons i Nil)) out))])])])) + si* + (Pair Nil Nil)))) + + +(check-type + (reduce-index Nil) + : (List (** String (List Int))) + ⇒ Nil) + +(check-type + (reduce-index + (map-index (Cons (Pair 0 (Cons "a" (Cons "b" (Cons "c" Nil)))) + (Cons (Pair 1 (Cons "d" (Cons "e" Nil))) + Nil)))) + : (List (** String (List Int))) + ⇒ (Cons (Pair "a" (Cons 0 Nil)) + (Cons (Pair "b" (Cons 0 Nil)) + (Cons (Pair "c" (Cons 0 Nil)) + (Cons (Pair "d" (Cons 1 Nil)) + (Cons (Pair "e" (Cons 1 Nil)) + Nil)))))) + +(check-type + (reduce-index + (map-index (Cons (Pair 0 (Cons "a" (Cons "b" (Cons "c" Nil)))) + (Cons (Pair 1 (Cons "a" (Cons "b" Nil))) + Nil)))) + : (List (** String (List Int))) + ⇒ (Cons (Pair "c" (Cons 0 Nil)) + (Cons (Pair "a" (Cons 0 (Cons 1 Nil))) + (Cons (Pair "b" (Cons 0 (Cons 1 Nil))) + Nil)))) + +;; For every string, get all integers that refer to the string +(define (make-index [is* : (List (** Int (List String)))] + → (List (** String (List Int)))) + (reduce-index (map-index is*))) + +(check-type + (make-index Nil) + : (List (** String (List Int))) + ⇒ Nil) + +(check-type + (make-index (Cons (Pair 1 (Cons "ocaml" (Cons "is" (Cons "fun" (Cons "because" (Cons "fun" (Cons "is" (Cons "a" (Cons "keyword" Nil))))))))) + (Cons (Pair 2 (Cons "page" (Cons "2" (Cons "intentionally" (Cons "left" (Cons "blank" Nil)))))) + (Cons (Pair 3 (Cons "the" (Cons "quick" (Cons "brown" (Cons "fox" (Cons "jumped" (Cons "over" (Cons "the" (Cons "lazy" (Cons "dog" Nil)))))))))) + (Cons (Pair 4 (Cons "is" (Cons "this" (Cons "the" (Cons "end" Nil))))) Nil))))) + : (List (** String (List Int))) + ⇒ (Cons (Pair "ocaml" (Cons 1 Nil)) + (Cons (Pair "because" (Cons 1 Nil)) + (Cons (Pair "fun" (Cons 1 Nil)) + (Cons (Pair "a" (Cons 1 Nil)) + (Cons (Pair "keyword" (Cons 1 Nil)) + (Cons (Pair "page" (Cons 2 Nil)) + (Cons (Pair "2" (Cons 2 Nil)) + (Cons (Pair "intentionally" (Cons 2 Nil)) + (Cons (Pair "left" (Cons 2 Nil)) + (Cons (Pair "blank" (Cons 2 Nil)) + (Cons (Pair "quick" (Cons 3 Nil)) + (Cons (Pair "brown" (Cons 3 Nil)) + (Cons (Pair "fox" (Cons 3 Nil)) + (Cons (Pair "jumped" (Cons 3 Nil)) + (Cons (Pair "over" (Cons 3 Nil)) + (Cons (Pair "lazy" (Cons 3 Nil)) + (Cons (Pair "dog" (Cons 3 Nil)) + (Cons (Pair "is" (Cons 1 (Cons 4 Nil))) + (Cons (Pair "this" (Cons 4 Nil)) + (Cons (Pair "the" (Cons 3 (Cons 4 Nil))) + (Cons (Pair "end" (Cons 4 Nil)) Nil)))))))))))))))))))))) + diff --git a/macrotypes/examples/tests/mlish/bg/huffman.mlish b/macrotypes/examples/tests/mlish/bg/huffman.mlish new file mode 100644 index 0000000..0e3399a --- /dev/null +++ b/macrotypes/examples/tests/mlish/bg/huffman.mlish @@ -0,0 +1,278 @@ +#lang s-exp "../../../mlish.rkt" +(require "../../rackunit-typechecking.rkt") + +;; Huffman trees from SICP + +;; ============================================================================= +;; === Sets of Symbols + +(define-type-alias Symbol String) + +;; Set of strings +(define-type Symbol* + [Empty] + [Singleton String] + [Join String Symbol* Symbol*]) + +(define (empty → Symbol*) + Empty) + +(define (singleton [s : String] → Symbol*) + (Singleton s)) + +(define (insert [s* : Symbol*] [s1 : String] → Symbol*) + (match s* with + [Empty -> (singleton s1)] + [Singleton s2 -> + (if (string<=? s1 s2) + (if (string=? s1 s2) + s* + (Join s2 (singleton s1) (empty))) + (Join s1 (singleton s2) (empty)))] + [Join s2 l* r* -> + (if (string<=? s1 s2) + (if (string=? s1 s2) + s* + (Join s2 (insert l* s1) r*)) + (Join s2 l* (insert r* s1)))])) + +(define (union [s1 : Symbol*] [s2 : Symbol*] → Symbol*) + (match s1 with + [Empty -> s2] + [Singleton s -> (insert s2 s)] + [Join s l* r* -> (union l* (union r* (insert s2 s)))])) + +(define (contains [s* : Symbol*] [s : Symbol] → Bool) + (match s* with + [Empty -> #f] + [Singleton s2 -> (string=? s s2)] + [Join s2 l* r* -> + (if (string<=? s s2) + (if (string=? s s2) + #t + (contains l* s)) + (contains r* s))])) + +;; ----------------------------------------------------------------------------- + +(check-type + (insert (empty) "hello") + : Symbol* + ⇒ (singleton "hello")) + +(check-type + (insert (insert (empty) "a") "b") + : Symbol* + ⇒ (Join "b" (singleton "a") (empty))) + +(check-type + (insert (insert (empty) "b") "a") + : Symbol* + ⇒ (Join "b" (singleton "a") (empty))) + +(check-type + (insert (insert (insert (empty) "a") "b") "c") + : Symbol* + ⇒ (Join "b" (singleton "a") (singleton "c"))) + +(check-type + (insert (insert (insert (empty) "c") "b") "a") + : Symbol* + ⇒ (Join "c" (Join "b" (singleton "a") (empty)) (empty))) + +(check-type + (union + (insert (insert (insert (empty) "c") "b") "a") + (insert (insert (insert (empty) "a") "b") "c")) + : Symbol* + ⇒ (Join "b" (singleton "a") (singleton "c"))) + +;; ----------------------------------------------------------------------------- + +(define-type (List A) + [⊥] + [∷ A (List A)]) + +(define-type-alias SymbolList (List Symbol)) + +(define (list [x : A] → (List A)) + (∷ x ⊥)) + +(define (append [x* : (List A)] [y* : (List A)] → (List A)) + (match x* with + [⊥ -> y*] + [∷ x x* -> + (∷ x (append x* y*))])) + +(define (length [x* : (List A)] → Int) + (match x* with + [⊥ -> 0] + [∷ x x* -> (+ 1 (length x*))])) + +;; ----------------------------------------------------------------------------- + +(define-type Bit O I) +(define-type-alias Bit* (List Bit)) + +;; ----------------------------------------------------------------------------- + +(define-type HTree + [Leaf String Int] ;; Symbol, Weight + [Node HTree HTree Symbol* Int] ;; Left, Right, Symbols, Weight +) + +(define (symbols [h : HTree] → Symbol*) + (match h with + [Leaf s w -> (singleton s)] + [Node lh rh s* w -> s*])) + +(define (weight [h : HTree] → Int) + (match h with + [Leaf s w -> w] + [Node l r s w -> w])) + +(define (make-code-tree [left : HTree] [right : HTree] → HTree) + (Node left right + (union (symbols left) (symbols right)) + (+ (weight left) (weight right)))) + +(define (decode-aux [bits : Bit*] [root : HTree] [current-branch : HTree] → SymbolList) + (match bits with + [⊥ -> + ⊥] + [∷ b bit* -> + (match (choose-branch b current-branch) with + [Leaf s w -> + (∷ s (decode-aux bit* root root))] + [Node l r s* w -> + (decode-aux bit* root (Node l r s* w))])])) + +(define (decode [bits : Bit*] [tree : HTree] → SymbolList) + (decode-aux bits tree tree)) + +(define (choose-branch [bit : Bit] [branch : HTree] → HTree) + (match branch with + [Leaf s w -> + ;; Error + (Leaf "ERROR" 0)] + [Node l* r* s* w -> + (match bit with + [O -> l*] + [I -> r*])])) + +(define-type-alias HTreeSet (List HTree)) + +(define (adjoin-set [x : HTree] [set : HTreeSet] → HTreeSet) + (match set with + [⊥ -> (list x)] + [∷ y y* -> + (if (< (weight x) (weight y)) + (∷ x set) + (∷ y (adjoin-set x y*)))])) + +(define (make-leaf-set [pair* : (List (× Symbol Int))] → HTreeSet) + (match pair* with + [⊥ -> ⊥] + [∷ pair pair* -> + (match pair with + [s i -> + (adjoin-set (Leaf s i) (make-leaf-set pair*))])])) + +(check-type + (make-leaf-set (∷ (tup "A" 4) + (∷ (tup "B" 2) + (∷ (tup "C" 1) + (∷ (tup "D" 1) + ⊥))))) + : HTreeSet + ⇒ (∷ (Leaf "D" 1) + (∷ (Leaf "C" 1) + (∷ (Leaf "B" 2) + (∷ (Leaf "A" 4) + ⊥))))) + +(define sample-tree + (make-code-tree + (Leaf "A" 4) + (make-code-tree + (Leaf "B" 2) + (make-code-tree + (Leaf "D" 1) + (Leaf "C" 1))))) + +(define sample-message + (∷ O (∷ I (∷ I (∷ O (∷ O (∷ I (∷ O (∷ I (∷ O (∷ I (∷ I (∷ I (∷ I (∷ O ⊥))))))))))))))) + +(check-type + (decode sample-message sample-tree) + : SymbolList + ⇒ (∷ "A" (∷ "D" (∷ "A" (∷ "B" (∷ "B" (∷ "C" (∷ "B" ⊥)))))))) + +(define (encode [message : SymbolList] [tree : HTree] → Bit*) + (match message with + [⊥ -> ⊥] + [∷ m m* -> + (append (encode-symbol m tree) (encode m* tree))])) + +(define (contains-symbol [s : Symbol] [tree : HTree] → Bool) + (contains (symbols tree) s)) + +;; Undefined if symbol is not in tree. Be careful! +(define (encode-symbol [s : Symbol] [tree : HTree] → Bit*) + (match tree with + [Leaf s w -> ⊥] + [Node l* r* s* w -> + (if (contains-symbol s l*) + (∷ O (encode-symbol s l*)) + (∷ I (encode-symbol s r*)))])) + +(check-type + (encode (decode sample-message sample-tree) sample-tree) + : Bit* + ⇒ sample-message) + +(define-type-alias Frequency Int) +(define (generate-huffman-tree [pair* : (List (× Symbol Frequency))] → HTree) + (successive-merge (make-leaf-set pair*))) + +(define (successive-merge [tree* : HTreeSet] → HTree) + (match tree* with + [⊥ -> (Leaf "ERROR" 0)] + [∷ t t* -> + (match t* with + [⊥ -> t] + [∷ t2 t* -> + (successive-merge (adjoin-set (make-code-tree t t2) t*))])])) + +(define rock-pair* + (∷ (tup "A" 2) + (∷ (tup "BOOM" 2) + (∷ (tup "GET" 2) + (∷ (tup "JOB" 2) + (∷ (tup "NA" 16) + (∷ (tup "SHA" 3) + (∷ (tup "YIP" 9) + (∷ (tup "WAH" 1) + ⊥))))))))) + +(define rock-tree (generate-huffman-tree rock-pair*)) + +(define rock-message + (∷ "GET" (∷ "A" (∷ "JOB" + (∷ "SHA" (∷ "NA" (∷ "NA" (∷ "NA" (∷ "NA" (∷ "NA" (∷ "NA" (∷ "NA" (∷ "NA" + (∷ "GET" (∷ "A" (∷ "JOB" + (∷ "SHA" (∷ "NA" (∷ "NA" (∷ "NA" (∷ "NA" (∷ "NA" (∷ "NA" (∷ "NA" (∷ "NA" + (∷ "WAH" (∷ "YIP" (∷ "YIP" (∷ "YIP" (∷ "YIP" (∷ "YIP" (∷ "YIP" (∷ "YIP" (∷ "YIP" (∷ "YIP" + (∷ "SHA" (∷ "BOOM" ⊥))))))))))))))))))))))))))))))))))))) + +(define rock-bit* (encode rock-message rock-tree)) + +(check-type + (decode rock-bit* rock-tree) + : SymbolList + ⇒ rock-message) + +(check-type + (length rock-bit*) + : Int + ⇒ 84) diff --git a/macrotypes/examples/tests/mlish/bg/lambda.mlish b/macrotypes/examples/tests/mlish/bg/lambda.mlish new file mode 100644 index 0000000..cee711e --- /dev/null +++ b/macrotypes/examples/tests/mlish/bg/lambda.mlish @@ -0,0 +1,95 @@ +#lang s-exp "../../../mlish.rkt" +(require "../../rackunit-typechecking.rkt") + +;; Lambda Calculus interpreter + + +;; Problems: +;; - Cannot use variable in head position of match (gotta exhaust constructors) + +;; ----------------------------------------------------------------------------- + +(define-type Λ + (Var Int) + (Lambda Int Λ) + (App Λ Λ)) + +(define (fresh [e : Λ] → Int) + (match e with + [Var i -> (+ i 1)] + [Lambda i e -> (+ i (fresh e))] + [App e1 e2 -> (+ 1 (+ (fresh e1) (fresh e2)))])) + +(define (subst [e : Λ] [i : Int] [v : Λ] → Λ) + (match e with + [Var j -> + (if (= i j) + v + e)] + [Lambda j e2 -> + (if (= i j) + e + (Lambda j (subst e2 i v)))] + [App e1 e2 -> + (App (subst e1 i v) (subst e2 i v))])) + +(define (simpl-aux [e : Λ] [i : Int] → (× Int Λ)) + (match e with + [Var j -> (tup i (Var j))] + [Lambda j e -> + (match (simpl-aux (subst e j (Var i)) (+ i 1)) with + [k e2 -> + (tup k (Lambda i e2))])] + [App e1 e2 -> + (match (simpl-aux e1 i) with + [j e1 -> + (match (simpl-aux e2 j) with + [k e2 -> + (tup k (App e1 e2))])])])) + +(define (simpl [e : Λ] → Λ) + (match (simpl-aux e 0) with + [i e2 -> e2])) + +(define (eval [e : Λ] → Λ) + (match e with + [Var i -> (Var i)] + [Lambda i e1 -> e] + [App e1 e2 -> + (match (eval e1) with + [Var i -> (Var -1)] + [App e1 e2 -> (Var -2)] + [Lambda i e -> + (match (tup 0 (eval e2)) with + [zero v2 -> + (eval (subst e i (subst v2 i (Var (+ (fresh e) (fresh v2))))))])])])) + +;; ----------------------------------------------------------------------------- + +(define I (Lambda 0 (Var 0))) +(define K (Lambda 0 (Lambda 1 (Var 0)))) +(define S (Lambda 0 (Lambda 1 (Lambda 2 (App (App (Var 0) (Var 2)) (App (Var 1) (Var 2))))))) +(define false (App S K)) + +;; ----------------------------------------------------------------------------- + +(check-type + (eval I) + : Λ + ⇒ I) + +(check-type + (eval (App I I)) + : Λ + ⇒ I) + +(check-type + (eval (App (App K (Var 2)) (Var 3))) + : Λ + ⇒ (Var 2)) + +(check-type + (eval (App (App false (Var 2)) (Var 3))) + : Λ + ⇒ (Var 3)) + diff --git a/macrotypes/examples/tests/mlish/bg/monad.mlish b/macrotypes/examples/tests/mlish/bg/monad.mlish new file mode 100644 index 0000000..cbea739 --- /dev/null +++ b/macrotypes/examples/tests/mlish/bg/monad.mlish @@ -0,0 +1,122 @@ +#lang s-exp "../../../mlish.rkt" +(require "../../rackunit-typechecking.rkt") + +(define-type (Option A) + [None] + [Some A]) + +;; ----------------------------------------------------------------------------- + +(define-type (List a) + [Nil] + [∷ a (List a)]) + +(define (foldl [f : (→ A B A)] [acc : A] [x* : (List B)] → A) + (match x* with + [Nil -> acc] + [∷ h t -> (foldl f (f acc h) t)])) + +(define (reverse [x* : (List A)] → (List A)) + (foldl (λ ([acc : (List A)] [x : A]) (∷ x acc)) Nil x*)) + +;; ============================================================================= +;; === BatchedQueue + +(define-type (BatchedQueue A) + [BQ (List A) (List A)]) + +(define (bq-check [f : (List A)] [r : (List A)] → (BatchedQueue A)) + (match f with + [Nil -> (BQ (reverse r) Nil)] + [∷ h t -> (BQ f r)])) + +(define (bq-empty → (BatchedQueue A)) + (BQ Nil Nil)) + +(define (bq-isEmpty [bq : (BatchedQueue A)] → Bool) + (match bq with + [BQ f r -> + (match f with + [Nil -> #t] + [∷ h t -> #f])])) + +(define (bq-snoc [bq : (BatchedQueue A)] [x : A] → (BatchedQueue A)) + (match bq with + [BQ f r -> (bq-check f (∷ x r))])) + +(define (bq-head [bq : (BatchedQueue A)] → (Option A)) + (match bq with + [BQ f r -> + (match f with + [Nil -> None] + [∷ h t -> (Some h)])])) + +(define (bq-tail [bq : (BatchedQueue A)] → (Option (BatchedQueue A))) + (match bq with + [BQ f* r* -> + (match f* with + [Nil -> None] + [∷ x f* -> + (Some (bq-check f* r*))])])) + +(define (list->bq [x* : (List A)] → (BatchedQueue A)) + (foldl + (λ ([q : (BatchedQueue A)] [x : A]) (bq-snoc q x)) + (bq-empty) x*)) + +;; ----------------------------------------------------------------------------- + +(define digit* + (∷ 1 (∷ 2 (∷ 3 (∷ 4 (∷ 5 (∷ 6 (∷ 7 (∷ 8 (∷ 9 Nil)))))))))) + +(check-type digit* : (List Int)) + +(define sample-bq + (list->bq digit*)) + +(check-type sample-bq : (BatchedQueue Int)) + +(check-type (Some sample-bq) : (Option (BatchedQueue Int))) + +(define (>> [f : (→ A (Option B))] [x : (Option A)] → (Option B)) + (match x with + [None -> None] + [Some y -> (f y)])) + +(check-type >> : (→/test (→ X (Option Y)) (Option X) (Option Y))) + +(check-type (bq-tail sample-bq) : (Option (BatchedQueue Int))) + +;; can't pass polymorphic fn? need to inst first +(check-type (>> (inst bq-tail Int) (Some sample-bq)) + : (Option (BatchedQueue Int))) + +;(ann (>> bq-tail (Some sample-bq)) : (Option (BatchedQueue Int))) + +(define intbq-tail (inst bq-tail Int)) + +(check-type intbq-tail : + (→/test (BatchedQueue Int) (Option (BatchedQueue Int)))) + +(check-type (>> intbq-tail (Some sample-bq)) + : (Option (BatchedQueue Int))) + +(check-type (inst bq-head Int) : (→/test (BatchedQueue Int) (Option Int))) + +(define bq-tails-result + (>> intbq-tail (>> intbq-tail (>> intbq-tail (Some sample-bq))))) + +(check-type bq-tails-result : (Option (BatchedQueue Int)) + ⇒ (Some (BQ (∷ 4 (∷ 5 (∷ 6 (∷ 7 (∷ 8 (∷ 9 Nil)))))) Nil))) + +(check-type (>> (inst bq-head Int) bq-tails-result) : (Option Int) -> (Some 4)) + +;; check match2 nested datatype bug +(check-type + (match bq-tails-result with + [None -> None] + [Some bq -> (bq-head bq)]) : (Option Int) -> (Some 4)) +(check-type + (match2 bq-tails-result with + [None -> None] + [Some bq -> (bq-head bq)]) : (Option Int) -> (Some 4)) diff --git a/macrotypes/examples/tests/mlish/bg/okasaki.mlish b/macrotypes/examples/tests/mlish/bg/okasaki.mlish new file mode 100644 index 0000000..643406e --- /dev/null +++ b/macrotypes/examples/tests/mlish/bg/okasaki.mlish @@ -0,0 +1,1654 @@ +#lang s-exp "../../../mlish.rkt" +(require "../../rackunit-typechecking.rkt") + +;; TODO +;; - cannot inst polymorphic function `bq-empty` +;; - cannot inst `(BQ (Nil {A}) (Nil {A}))` +;; - cannot use bq-snoc directly in a foldl (need wrapper λ) + +;; ----------------------------------------------------------------------------- + +(define-type (Option A) + [None] + [Some A]) + +;; ----------------------------------------------------------------------------- + +(define (div (n1 : Int) (n2 : Int) → Int) + (if (< n1 n2) + 0 + (+ 1 (div (- n1 n2) n2)))) + +(define (mod (n1 : Int) (n2 : Int) → Int) + (if (< n1 n2) + n1 + (mod (- n1 n2) n2))) + +;; ----------------------------------------------------------------------------- + +(define-type (List a) + [Nil] + [∷ a (List a)]) + +(define (foldl [f : (→ A B A)] [acc : A] [x* : (List B)] → A) + (match x* with + [Nil -> acc] + [∷ h t -> (foldl f (f acc h) t)])) + +(define (reverse [x* : (List A)] → (List A)) + (foldl (λ ([acc : (List A)] [x : A]) (∷ x acc)) Nil x*)) + +(define (append [x* : (List A)] [y* : (List A)] → (List A)) + (match x* with + [Nil -> y*] + [∷ x x* -> + (∷ x (append x* y*))])) + +(define (take [i : Int] [x* : (List A)] → (List A)) + (if (<= i 0) + Nil + (match x* with + [Nil -> Nil] + [∷ h t -> (∷ h (take (- i 1) t))]))) + +(define (drop [i : Int] [x* : (List A)] → (List A)) + (if (<= i 0) + x* + (match x* with + [Nil -> Nil] + [∷ h t -> (drop (- i 1) t)]))) + +;; ============================================================================= +;; === BatchedQueue + +(define-type (BatchedQueue A) + [BQ (List A) (List A)]) + +(define (bq-check [f : (List A)] [r : (List A)] → (BatchedQueue A)) + (match f with + [Nil -> (BQ (reverse r) Nil)] + [∷ h t -> (BQ f r)])) + +(define (bq-empty → (BatchedQueue A)) + (BQ Nil Nil)) + +(define (bq-isEmpty [bq : (BatchedQueue A)] → Bool) + (match bq with + [BQ f r -> + (match f with + [Nil -> #t] + [∷ h t -> #f])])) + +(define (bq-snoc [bq : (BatchedQueue A)] [x : A] → (BatchedQueue A)) + (match bq with + [BQ f r -> (bq-check f (∷ x r))])) + +(define (bq-head [bq : (BatchedQueue A)] → (Option A)) + (match bq with + [BQ f r -> + (match f with + [Nil -> None] + [∷ h t -> (Some h)])])) + +(define (bq-tail [bq : (BatchedQueue A)] → (Option (BatchedQueue A))) + (match bq with + [BQ f* r* -> + (match f* with + [Nil -> None] + [∷ x f* -> + (Some (bq-check f* r*))])])) + +(define (list->bq [x* : (List A)] → (BatchedQueue A)) + (foldl + ;bq-snoc ;; TODO + (λ ([q : (BatchedQueue A)] [x : A]) (bq-snoc q x)) + (bq-empty) x*)) + +;; ----------------------------------------------------------------------------- + +(define digit* + (∷ 1 (∷ 2 (∷ 3 (∷ 4 (∷ 5 (∷ 6 (∷ 7 (∷ 8 (∷ 9 Nil)))))))))) + +(define abc + (∷ "A" (∷ "B" (∷ "C" Nil)))) + +(define def + (∷ "D" (∷ "E" (∷ "F" Nil)))) + +(define sample-bq (list->bq digit*)) + +(check-type + (bq-isEmpty (BQ (Nil {Bool}) (Nil {Bool}))) + ;(bq-isEmpty (bq-empty {Bool})) + ;(bq-isEmpty (BQ (Nil {Bool}) (Nil {Bool}))) ;; TODO + : Bool + ⇒ #t) + +(check-type + (bq-isEmpty sample-bq) + : Bool + ⇒ #f) + +(check-type + (bq-head sample-bq) + : (Option Int) + ⇒ (Some 1)) + +(check-type + (bq-head (bq-snoc sample-bq 10)) + : (Option Int) + ⇒ (Some 1)) + +(define (>> [f : (→ A (Option A))] [x : (Option A)] → (Option A)) + (match x with + [None -> None] + [Some y -> (f y)])) + +(check-type + (match (bq-tail sample-bq) with + [None -> None] + [Some bq -> (bq-head bq)]) + : (Option Int) + ⇒ (Some 2)) + +;; TODO +;(check-type +; (>> bq-head (>> bq-tail (>> bq-tail (>> bq-tail (Some sample-bq))))) +; : (Option Int) +; ⇒ (Some 4)) + +;; ============================================================================= +;; === Bankers Queue + +(define-type (BankersQueue A) + (Bank Int (List A) Int (List A))) + +(define (bank-check [lenf : Int] [f : (List A)] [lenr : Int] [r : (List A)] → (BankersQueue A)) + (if (<= lenr lenf) + (Bank lenf f lenr r) + (Bank (+ lenf lenr) (append f (reverse r)) 0 Nil))) + +(define (bank-empty → (BankersQueue A)) + (Bank 0 Nil 0 Nil)) + +(define (bank-isEmpty [bq : (BankersQueue A)] → Bool) + (match bq with + [Bank lenf f lenr r -> (= 0 lenf)])) + +(define (bank-snoc [bq : (BankersQueue A)] [x : A] → (BankersQueue A)) + (match bq with + [Bank lenf f lenr r -> (bank-check lenf f (+ 1 lenr) (∷ x r))])) + +(define (bank-head [bq : (BankersQueue A)] → (Option A)) + (match bq with + [Bank lenf f lenr r -> + (match f with + [Nil -> None] + [∷ h t -> (Some h)])])) + +(define (bank-tail [bq : (BankersQueue A)] → (Option (BankersQueue A))) + (match bq with + [Bank lenf f lenr r -> + (match f with + [Nil -> None] + [∷ h t -> (Some (bank-check (- lenf 1) t lenr r))])])) + +;; ----------------------------------------------------------------------------- + +(define sample-bank + (foldl (λ ([acc : (BankersQueue Int)] [x : Int]) (bank-snoc acc x)) (bank-empty) digit*)) + +(check-type + (bank-isEmpty (Bank 0 (Nil {Int}) 0 (Nil {Int}))) + : Bool + ⇒ #t) + +(check-type + (bank-isEmpty sample-bank) + : Bool + ⇒ #f) + +(check-type + (bank-head sample-bank) + : (Option Int) + ⇒ (Some 1)) + +(check-type + (bank-head (bank-snoc sample-bank 10)) + : (Option Int) + ⇒ (Some 1)) + +(check-type + (match (bank-tail sample-bank) with + [None -> None] + [Some bank -> (bank-head bank)]) + : (Option Int) + ⇒ (Some 2)) + +;; ============================================================================= +;; === Physicists Queue + +(define-type (PhysicistsQueue A) + (PQ (List A) Int (List A) Int (List A))) + +(define (pq-check [w : (List A)] [lenf : Int] [f : (List A)] [lenr : Int] [r : (List A)] → (PhysicistsQueue A)) + (if (<= lenr lenf) + (pq-checkw w lenf f lenr r) + (pq-checkw f (+ lenf lenr) (append f (reverse r)) 0 Nil))) + +(define (pq-checkw [w : (List A)] [lenf : Int] [f : (List A)] [lenr : Int] [r : (List A)] → (PhysicistsQueue A)) + (match w with + [Nil -> (PQ f lenf f lenr r)] + [∷ h t -> (PQ w lenf f lenr r)])) + +(define (pq-empty → (PhysicistsQueue A)) + (PQ Nil 0 Nil 0 Nil)) + +(define (pq-isEmpty [pq : (PhysicistsQueue A)] → Bool) + (match pq with + [PQ w lenf f lenr r -> + (= lenf 0)])) + +(define (pq-snoc [pq : (PhysicistsQueue A)] [x : A] → (PhysicistsQueue A)) + (match pq with + [PQ w lenf f lenr r -> (pq-check w lenf f (+ 1 lenr) (∷ x r))])) + +(define (pq-head [pq : (PhysicistsQueue A)] → (Option A)) + (match pq with + [PQ w lenf f lenr r -> + (match w with + [Nil -> None] + [∷ w w* -> (Some w)])])) + +(define (pq-tail [pq : (PhysicistsQueue A)] → (Option (PhysicistsQueue A))) + (match pq with + [PQ w lenf f lenr r -> + (match w with + [Nil -> None] + [∷ x w* -> + (match f with + [Nil -> None] ;; Never happens + [∷ f f* -> (Some (pq-check w* (- lenf 1) f* lenr r))])])])) + +;; ----------------------------------------------------------------------------- + +(define sample-pq + (foldl (λ ([acc : (PhysicistsQueue Int)] [x : Int]) (pq-snoc acc x)) (pq-empty) digit*)) + +(check-type + (pq-isEmpty (PQ (Nil {Int}) 0 (Nil {Int}) 0 (Nil {Int}))) + : Bool + ⇒ #t) + +(check-type + (pq-isEmpty sample-pq) + : Bool + ⇒ #f) + +(check-type + (pq-head sample-pq) + : (Option Int) + ⇒ (Some 1)) + +(check-type + (pq-head (pq-snoc sample-pq 10)) + : (Option Int) + ⇒ (Some 1)) + +(check-type + (match (pq-tail sample-pq) with + [None -> None] + [Some pq -> (pq-head pq)]) + : (Option Int) + ⇒ (Some 2)) + +;; ============================================================================= +;; === Hood-Melville Queue + +(define-type (RotationState A) + [Idle] + [Reversing Int (List A) (List A) (List A) (List A)] + [Appending Int (List A) (List A)] + [Done (List A)]) + +(define-type (HoodMelvilleQueue A) + [HM Int (List A) (RotationState A) Int (List A)]) + +(define (hm-exec [rs : (RotationState A)] → (RotationState A)) + (match rs with + [Idle -> rs] + [Done x -> rs] + [Appending ok f* r* -> + (if (= ok 0) + (Done r*) + (match f* with + [Nil -> rs] + [∷ x f* -> + (Appending (- ok 1) f* (∷ x r*))]))] + [Reversing ok f1* f2* r1* r2* -> + (match f1* with + [Nil -> + (match r1* with + [Nil -> rs] + [∷ y r1* -> + (match r1* with + [Nil -> (Appending ok f2* (∷ y r2*))] + [∷ a b -> rs])])] + [∷ x f1* -> + (match r1* with + [Nil -> rs] + [∷ y r1* -> + (Reversing (+ ok 1) f1* (∷ x f2*) r1* (∷ y r2*))])])])) + +(define (hm-invalidate [rs : (RotationState A)] → (RotationState A)) + (match rs with + [Reversing ok f1* f2* r1* r2* -> + (Reversing (- ok 1) f1* f2* r1* r2*)] + [Appending ok f* r* -> + (if (= 0 ok) + (match r* with + [Nil -> rs] + [∷ x r* -> (Done r*)]) + (Appending (- ok 1) f* r*))] + [Done x -> rs] + [Idle -> rs])) + +(define (hm-exec2 [lenf : Int] [f* : (List A)] [state : (RotationState A)] [lenr : Int] [r : (List A)] → (HoodMelvilleQueue A)) + ((λ ([newstate : (RotationState A)]) + (match newstate with + [Done newf -> (HM lenf newf Idle lenr r)] + [Idle -> (HM lenf f* newstate lenr r)] + [Appending a b c -> (HM lenf f* newstate lenr r)] + [Reversing a b c d e -> (HM lenf f* newstate lenr r)])) + (hm-exec (hm-exec state)))) + +(define (hm-check [lenf : Int] [f* : (List A)] [state : (RotationState A)] [lenr : Int] [r* : (List A)] → (HoodMelvilleQueue A)) + (if (<= lenr lenf) + (hm-exec2 lenf f* state lenr r*) + (hm-exec2 (+ lenf lenr) f* (Reversing 0 f* Nil r* Nil) 0 Nil))) + +(define (hm-empty → (HoodMelvilleQueue A)) + (HM 0 Nil Idle 0 Nil)) + +(define (hm-isEmpty [hm : (HoodMelvilleQueue A)] → Bool) + (match hm with + [HM lenf b c d e -> + (= lenf 0)])) + +(define (hm-snoc [hm : (HoodMelvilleQueue A)] [x : A] → (HoodMelvilleQueue A)) + (match hm with + [HM lenf f state lenr r -> (hm-check lenf f state (+ lenr 1) (∷ x r))])) + +(define (hm-head [hm : (HoodMelvilleQueue A)] → (Option A)) + (match hm with + [HM a f b c d -> + (match f with + [Nil -> None] + [∷ x f* -> (Some x)])])) + +(define (hm-tail [hm : (HoodMelvilleQueue A)] → (Option (HoodMelvilleQueue A))) + (match hm with + [HM lenf f state lenr r -> + (match f with + [Nil -> None] + [∷ x f* -> (Some (hm-check (- lenf 1) f* (hm-invalidate state) lenr r))])])) + +;; ----------------------------------------------------------------------------- + +(define sample-hm + (foldl (λ ([acc : (HoodMelvilleQueue Int)] [x : Int]) (hm-snoc acc x)) (hm-empty) digit*)) + +(check-type + (hm-isEmpty (HM 0 (Nil {Int}) Idle 0 (Nil {Int}))) + : Bool + ⇒ #t) + +(check-type + (hm-isEmpty sample-hm) + : Bool + ⇒ #f) + +(check-type + (hm-head sample-hm) + : (Option Int) + ⇒ (Some 1)) + +(check-type + (hm-head (hm-snoc sample-hm 10)) + : (Option Int) + ⇒ (Some 1)) + +(check-type + (match (hm-tail sample-hm) with + [None -> None] + [Some hm -> (hm-head hm)]) + : (Option Int) + ⇒ (Some 2)) + +;; ============================================================================= +;; === Bootstrapped Queue + +(define-type (BootstrappedQueue a) + [E] + [Q Int (List a) (BootstrappedQueue (List a)) Int (List a)]) + +(define (bs-checkQ [lenfm : Int] [f : (List A)] [m : (BootstrappedQueue (List A))] [lenr : Int] [r : (List A)] → (BootstrappedQueue A)) + (if (<= lenr lenfm) + (bs-checkF lenfm f m lenr r) + (bs-checkF (+ lenfm lenr) f (bs-snoc m (reverse r)) 0 Nil))) + +(define (bs-checkF [lenfm : Int] [f : (List A)] [m : (BootstrappedQueue (List A))] [lenr : Int] [r : (List A)] → (BootstrappedQueue A)) + (match f with + [Nil -> + (match m with + [E -> E] + [Q _a _b _c _d _e -> + (match (bs-head m) with + [None -> E] + [Some hd -> + (match (bs-tail m) with + [None -> E] + [Some tl -> + (Q lenfm hd tl lenr r)])])])] + [∷ _f _f* -> + (Q lenfm f m lenr r)])) + +(define (bs-empty → (BootstrappedQueue A)) + (Q 0 Nil E 0 Nil)) + +(define (bs-isEmpty [m : (BootstrappedQueue A)] → Bool) + (match m with + [E -> #t] + [Q a b c d e -> #f])) + +(define (bs-snoc [m : (BootstrappedQueue A)] [x : A] → (BootstrappedQueue A)) + (match m with + [E -> (Q 1 (∷ x Nil) E 0 Nil)] + [Q lenfm f m lenr r -> (bs-checkQ lenfm f m (+ 1 lenr) (∷ x r))])) + +(define (bs-head [m : (BootstrappedQueue A)] → (Option A)) + (match m with + [E -> None] + [Q lenfm f m lenr r -> + (match f with + [Nil -> None] + [∷ x f* -> (Some x)])])) + +(define (bs-tail [m : (BootstrappedQueue A)] → (Option (BootstrappedQueue A))) + (match m with + [E -> None] + [Q lenfm f m lenr r -> + (match f with + [Nil -> None] + [∷ _x f* -> (Some (bs-checkQ (- lenfm 1) f* m lenr r))])])) + +;; ----------------------------------------------------------------------------- + +(define sample-bs + (foldl (λ ([acc : (BootstrappedQueue Int)] [x : Int]) (bs-snoc acc x)) (bs-empty) digit*)) + +(check-type + (bs-isEmpty (E {Int})) + : Bool + ⇒ #t) + +(check-type + (bs-isEmpty sample-bs) + : Bool + ⇒ #f) + +(check-type + (bs-head sample-bs) + : (Option Int) + ⇒ (Some 1)) + +(check-type + (bs-head (bs-snoc sample-bs 10)) + : (Option Int) + ⇒ (Some 1)) + +(check-type + (match (bs-tail sample-bs) with + [None -> None] + [Some bs -> (bs-head bs)]) + : (Option Int) + ⇒ (Some 2)) + +;; ============================================================================= +;; === Implicit Queue + +(define-type (Digit A) + [Zero] + [One A] + [Two A A]) + +(define-type (ImplicitQueue A) + [Shallow (Digit A)] + [Deep (Digit A) (ImplicitQueue (× A A)) (Digit A)]) + +(define (iq-empty → (ImplicitQueue A)) + (Shallow Zero)) + +(define (iq-isEmpty [iq : (ImplicitQueue A)] → Bool) + (match iq with + [Shallow d -> + (match d with + [Zero -> #t] + [One x -> #f] + [Two x y -> #f])] + [Deep a b c -> #f])) + +(define (iq-snoc [iq : (ImplicitQueue A)] [y : A] → (ImplicitQueue A)) + (match iq with + [Shallow d -> + (match d with + [Zero -> (Shallow (One y))] + [One x -> (Deep (Two x y) (Shallow Zero) Zero)] + [Two x y -> ;; Error + (Shallow Zero)])] + [Deep f m d -> + (match d with + [Zero -> (Deep f m (One y))] + [One x -> (Deep f (iq-snoc m (tup x y)) Zero)] + [Two x y -> (Shallow Zero)])])) ;; Error + +(define (iq-head [iq : (ImplicitQueue A)] → (Option A)) + (match iq with + [Shallow d -> + (match d with + [Zero -> None] + [One x -> (Some x)] + [Two x y -> (Some x)])] ;; Error + [Deep d m r -> + (match d with + [Zero -> None] ;; Error + [One x -> (Some x)] + [Two x y -> (Some x)])])) + +(define (iq-tail [iq : (ImplicitQueue A)] → (Option (ImplicitQueue A))) + (match iq with + [Shallow d -> + (match d with + [Zero -> None] + [One x -> (Some (Shallow Zero))] + [Two x y -> None])] ;; Error + [Deep d m r -> + (match d with + [Zero -> None] ;; Error + [One x -> + (match (iq-head m) with + [None -> (Some (Shallow r))] + [Some yz -> + (match yz with + [y z -> + (match (iq-tail m) with + [None -> None] + [Some tl -> + (Some (Deep (Two y z) tl r))])])])] + [Two x y -> (Some (Deep (One y) m r))])])) + +;; ----------------------------------------------------------------------------- + +(define sample-iq + (foldl (λ ([acc : (ImplicitQueue Int)] [x : Int]) (iq-snoc acc x)) (iq-empty) digit*)) + +(check-type + (iq-isEmpty (Shallow (Zero {Int}))) + : Bool + ⇒ #t) + +(check-type + (iq-isEmpty sample-iq) + : Bool + ⇒ #f) + +(check-type + (iq-head sample-iq) + : (Option Int) + ⇒ (Some 1)) + +(check-type + (iq-head (iq-snoc sample-iq 10)) + : (Option Int) + ⇒ (Some 1)) + +(check-type + (match (iq-tail sample-iq) with + [None -> None] + [Some iq -> (iq-head iq)]) + : (Option Int) + ⇒ (Some 2)) + +;; ============================================================================= +;; === Bankers Deque + +(define-type (BankersDeque A) + [BD Int (List A) Int (List A)]) + +(define c 3) + +(define (bd-check [lenf : Int] [f : (List A)] [lenr : Int] [r : (List A)] → (BankersDeque A)) + (if (> lenf (+ c (+ lenr 1))) + (let* ([i (div (+ lenf lenr) 2)] + [j (- (+ lenf lenr) i)] + [r2 (take j r)] + [f2 (append f (reverse (drop j r)))]) + (BD i f2 j r2)) + (if (> lenr (+ 1 (* c lenf))) + (let* ([j (div (+ lenf lenr) 2)] + [i (- (+ lenr lenf) j)] + [r2 (take j r)] + [f2 (append f (reverse (drop j r)))]) + (BD i f2 j r2)) + (BD lenf f lenr r)))) + +(define (bd-empty → (BankersDeque A)) + (BD 0 Nil 0 Nil)) + +(define (bd-isEmpty [bd : (BankersDeque A)] → Bool) + (match bd with + [BD lenf f lenr r -> (= 0 (+ lenf lenr))])) + +(define (bd-cons [x : A] [bd : (BankersDeque A)] → (BankersDeque A)) + (match bd with + [BD lenf f lenr r -> (bd-check (+ lenf 1) (∷ x f) lenr r)])) + +(define (bd-head [bd : (BankersDeque A)] → (Option A)) + (match bd with + [BD lenf f lenr r -> + (match f with + [Nil -> None] + [∷ x f2 -> (Some x)])])) + +(define (bd-tail [bd : (BankersDeque A)] → (Option (BankersDeque A))) + (match bd with + [BD lenf f lenr r -> + (match f with + [Nil -> None] + [∷ x f2 -> (Some (bd-check (- lenf 1) f2 lenr r))])])) + +(define (bd-snoc [bd : (BankersDeque A)] [x : A] → (BankersDeque A)) + (match bd with + [BD lenf f lenr r -> (bd-check lenf f (+ lenr 1) (∷ x r))])) + +(define (bd-last [bd : (BankersDeque A)] → (Option A)) + (match bd with + [BD lenf f lenr r -> + (match r with + [Nil -> None] + [∷ x r2 -> (Some x)])])) + +(define (bd-init [bd : (BankersDeque A)] → (Option (BankersDeque A))) + (match bd with + [BD lenf f lenr r -> + (match r with + [Nil -> None] + [∷ x r -> (Some (bd-check lenf f (- lenr 1) r))])])) + +;; ----------------------------------------------------------------------------- + +(define sample-bd + (foldl (λ ([acc : (BankersDeque Int)] [x : Int]) (bd-snoc acc x)) (bd-empty) digit*)) + +(check-type + (bd-isEmpty (BD 0 (Nil {Int}) 0 (Nil {Int}))) + : Bool + ⇒ #t) + +(check-type + (bd-isEmpty sample-bd) + : Bool + ⇒ #f) + +(check-type + (bd-head sample-bd) + : (Option Int) + ⇒ (Some 1)) + +(check-type + (bd-last sample-bd) + : (Option Int) + ⇒ (Some 9)) + +(check-type + (bd-head (bd-snoc sample-bd 10)) + : (Option Int) + ⇒ (Some 1)) + +(check-type + (bd-head (bd-cons 10 sample-bd)) + : (Option Int) + ⇒ (Some 10)) + +(check-type + (match (bd-tail sample-bd) with + [None -> None] + [Some bd -> (bd-head bd)]) + : (Option Int) + ⇒ (Some 2)) + +(check-type + (match (bd-init sample-bd) with + [None -> None] + [Some bd -> (bd-last bd)]) + : (Option Int) + ⇒ (Some 8)) + +;; ============================================================================= +;; === Simple Catenable Deque + +(define-type (SimpleCatDeque a) + [SShallow (BankersDeque a)] + [SDeep (BankersDeque a) (SimpleCatDeque (BankersDeque a)) (BankersDeque a)]) + +(define (bd-tooSmall [d : (BankersDeque A)] → Bool) + (if (bd-isEmpty d) + #t + (match (bd-tail d) with + [None -> #t] + [Some d -> (bd-isEmpty d)]))) + +(define (bd-dappendL [d1 : (BankersDeque A)] [d2 : (BankersDeque A)] → (BankersDeque A)) + (match (bd-head d1) with + [None -> d2] + [Some h -> (bd-cons h d2)])) + +(define (bd-dappendR [d1 : (BankersDeque A)] [d2 : (BankersDeque A)] → (BankersDeque A)) + (match (bd-head d2) with + [None -> d1] + [Some h -> (bd-snoc d1 h)])) + +(define (scd-empty → (SimpleCatDeque A)) + (SShallow (bd-empty))) + +(define (scd-isEmpty [scd : (SimpleCatDeque A)] → Bool) + (match scd with + [SShallow d -> (bd-isEmpty d)] + [SDeep a b c -> #f])) + +(define (scd-cons [x : A] [scd : (SimpleCatDeque A)] → (SimpleCatDeque A)) + (match scd with + [SShallow d -> (SShallow (bd-cons x d))] + [SDeep f m r -> (SDeep (bd-cons x f) m r)])) + +(define (scd-snoc [scd : (SimpleCatDeque A)] [x : A] → (SimpleCatDeque A)) + (match scd with + [SShallow d -> (SShallow (bd-snoc d x))] + [SDeep f m r -> (SDeep f m (bd-snoc f x))])) + +(define (scd-head [scd : (SimpleCatDeque A)] → (Option A)) + (match scd with + [SShallow d -> (bd-head d)] + [SDeep f m r -> (bd-head f)])) + +(define (scd-last [scd : (SimpleCatDeque A)] → (Option A)) + (match scd with + [SShallow d -> (bd-last d)] + [SDeep f m r -> (bd-last r)])) + +(define (scd-tail [scd : (SimpleCatDeque A)] → (Option (SimpleCatDeque A))) + (match scd with + [SShallow d -> + (match (bd-tail d) with + [None -> None] + [Some t -> (Some (SShallow t))])] + [SDeep f m r -> + (match (bd-tail f) with + [None -> None] + [Some f2 -> + (if (not (bd-tooSmall f2)) + (Some (SDeep f2 m r)) + (if (scd-isEmpty m) + (Some (SShallow (bd-dappendL f2 r))) + (match (scd-head m) with + [None -> None] + [Some hm -> + (match (scd-tail m) with + [None -> None] + [Some tm -> + (Some (SDeep (bd-dappendL f2 hm) tm r))])])))])])) + +(define (scd-init [scd : (SimpleCatDeque A)] → (Option (SimpleCatDeque A))) + (match scd with + [SShallow d -> + (match (bd-init d) with + [None -> None] + [Some t -> (Some (SShallow t))])] + [SDeep f m r -> + (match (bd-init r) with + [None -> None] + [Some r2 -> + (if (not (bd-tooSmall r2)) + (Some (SDeep f m r2)) + (if (scd-isEmpty m) + (Some (SShallow (bd-dappendR r r2))) + (match (scd-last m) with + [None -> None] + [Some lm -> + (match (scd-init m) with + [None -> None] + [Some im -> + (Some (SDeep f im (bd-dappendR lm r2)))])])))])])) + +(define (scd-++ [scd1 : (SimpleCatDeque A)] [scd2 : (SimpleCatDeque A)] → (SimpleCatDeque A)) + (match scd1 with + [SShallow d1 -> + (match scd2 with + [SShallow d2 -> + (if (bd-tooSmall d1) + (SShallow (bd-dappendL d1 d2)) + (if (bd-tooSmall d2) + (SShallow (bd-dappendR d1 d2)) + (SDeep d1 (scd-empty) d2)))] + [SDeep f m r -> + (if (bd-tooSmall d1) + (SDeep (bd-dappendL d1 f) m r) + (SDeep d1 (scd-cons f m) r))])] + [SDeep f1 m1 r1 -> + (match scd2 with + [SShallow d2 -> + (if (bd-tooSmall d2) + (SDeep f1 m1 (bd-dappendR r1 d2)) + (SDeep f1 (scd-snoc m1 r1) d2))] + [SDeep f2 m2 r2 -> + (SDeep f1 (scd-++ (scd-snoc m1 f1) (scd-cons r1 m2)) r2)])])) + +(define (scd->list [scd : (SimpleCatDeque A)] → (List A)) + (match (scd-head scd) with + [None -> Nil] + [Some hd -> + (match (scd-tail scd) with + [None -> (∷ hd Nil)] + [Some tl -> (∷ hd (scd->list tl))])])) + +;; ----------------------------------------------------------------------------- + +(define sample-scd + (foldl (λ ([acc : (SimpleCatDeque Int)] [x : Int]) (scd-snoc acc x)) (scd-empty) digit*)) + +(define (empty-sample → (SimpleCatDeque Int)) + (scd-empty)) + +(check-type + (scd-isEmpty (SShallow (BD 0 (Nil {Int}) 0 (Nil {Int})))) + : Bool + ⇒ #t) + +(check-type + (scd-isEmpty sample-scd) + : Bool + ⇒ #f) + +(check-type + (scd-head sample-scd) + : (Option Int) + ⇒ (Some 1)) + +(check-type + (scd-head (empty-sample)) + : (Option Int) + ⇒ None) + +(check-type + (scd-last sample-scd) + : (Option Int) + ⇒ (Some 9)) + +(check-type + (scd-last (empty-sample)) + : (Option Int) + ⇒ None) + +(check-type + (scd-head (scd-snoc sample-scd 10)) + : (Option Int) + ⇒ (Some 1)) + +(check-type + (scd-head (scd-cons 10 sample-scd)) + : (Option Int) + ⇒ (Some 10)) + +(check-type + (match (scd-tail sample-scd) with + [None -> None] + [Some scd -> (scd-head scd)]) + : (Option Int) + ⇒ (Some 2)) + +(check-type + (scd-tail (empty-sample)) + : (Option (SimpleCatDeque Int)) + ⇒ None) + +(check-type + (match (scd-init sample-scd) with + [None -> None] + [Some scd -> (scd-last scd)]) + : (Option Int) + ⇒ (Some 8)) + +(check-type + (scd-init (empty-sample)) + : (Option (SimpleCatDeque Int)) + ⇒ None) + +(check-type + (match (scd-head (scd-++ (scd-cons 1 (scd-empty)) (empty-sample))) with + [None -> None] + [Some i -> (Some i)]) + : (Option Int) + ⇒ (Some 1)) + +(check-type + (match (scd-head (scd-++ (empty-sample) (scd-cons 2 (scd-empty)))) with + [None -> None] + [Some scd -> (Some scd)]) + : (Option Int) + ⇒ (Some 2)) + +(check-type + (match (scd-tail (scd-++ (scd-cons 1 (scd-empty)) (scd-cons 2 (scd-empty)))) with + [None -> None] + [Some scd -> (scd-head scd)]) + : (Option Int) + ⇒ (Some 2)) + +(define (scd-ref [n : Int] [scd : (SimpleCatDeque A)] → (Option A)) + (if (< n 1) + (scd-head scd) + (match (scd-tail scd) with + [None -> None] + [Some tl -> (scd-ref (- n 1) tl)]))) + +(check-type + (scd-ref 2 + (scd-++ + (scd-++ (scd-cons 1 (scd-empty)) (scd-cons 2 (scd-empty))) + (scd-++ (scd-cons 3 (scd-empty)) (scd-cons 4 (scd-empty))))) + : (Option Int) + ⇒ (Some 3)) + +(check-type + (scd-ref 0 + (scd-++ + (scd-++ (scd-cons 1 (scd-empty)) (scd-cons 2 (scd-empty))) + (scd-++ (scd-cons 3 (scd-empty)) (scd-cons 4 (scd-empty))))) + : (Option Int) + ⇒ (Some 1)) + +(check-type + (scd->list + (scd-++ + (scd-++ (scd-cons 1 (scd-empty)) (scd-cons 2 (scd-empty))) + (scd-++ (scd-cons 3 (scd-empty)) (scd-cons 4 (scd-empty))))) + : (List Int) + ⇒ (∷ 1 (∷ 2 (∷ 3 (∷ 4 Nil))))) + +(check-type + (scd-ref 1 + (scd-++ + (scd-++ + (scd-++ (scd-cons 1 (scd-empty)) (scd-cons 2 (scd-empty))) + (scd-++ (scd-cons 3 (scd-empty)) (scd-cons 4 (scd-empty)))) + (scd-++ + (scd-++ (scd-cons 5 (scd-empty)) (scd-cons 6 (scd-empty))) + (scd-++ (scd-cons 7 (scd-empty)) (scd-cons 8 (scd-empty)))))) + : (Option Int) + ⇒ (Some 2)) + +(check-type + (scd-ref 3 + (scd-++ + (scd-++ + (scd-++ (scd-cons 1 (scd-empty)) (scd-cons 2 (scd-empty))) + (scd-++ (scd-cons 3 (scd-empty)) (scd-cons 4 (scd-empty)))) + (scd-++ + (scd-++ (scd-cons 5 (scd-empty)) (scd-cons 6 (scd-empty))) + (scd-++ (scd-cons 7 (scd-empty)) (scd-cons 8 (scd-empty)))))) + : (Option Int) + ⇒ (Some 4)) + +;; TODO this is a bug, but at least we have the right types in MLish +;(check-type +; (scd->list +; (scd-++ +; (scd-++ +; (scd-++ (scd-cons 1 (scd-empty)) (scd-cons 2 (scd-empty))) +; (scd-++ (scd-cons 3 (scd-empty)) (scd-cons 4 (scd-empty)))) +; (scd-++ +; (scd-++ (scd-cons 5 (scd-empty)) (scd-cons 6 (scd-empty))) +; (scd-++ (scd-cons 7 (scd-empty)) (scd-cons 8 (scd-empty)))))) +; : (List Int) +; ⇒ (∷ 1 (∷ 2 (∷ 3 (∷ 4 (∷ 5 (∷ 6 (∷ 7 (∷ 8 Nil))))))))) + +;; ============================================================================= +;; === Binary Random Access List + +(define-type (Tree A) + (Leaf A) + (Node Int (Tree A) (Tree A))) + +(define-type (BLDigit A) + (BLZero) + (BLOne (Tree A))) + +(define-type (BinaryList A) + (BL (List (BLDigit A)))) + +(define (size (t : (Tree A)) → Int) + (match t with + (Leaf x -> 1) + (Node w t1 t2 -> w))) + +(define (link (t1 : (Tree A)) (t2 : (Tree A)) → (Tree A)) + (Node (+ (size t1) (size t2)) t1 t2)) + +(define (consTree (t : (Tree A)) (x* : (List (BLDigit A))) → (List (BLDigit A))) + (match x* with + (Nil -> (∷ (BLOne t) Nil)) + (∷ h ts -> + (match h with + (BLZero -> (∷ (BLOne t) ts)) + (BLOne t2 -> (∷ BLZero (consTree (link t t2) ts))))))) + + +;; TODO τ_e bad syntax when using `match2` +(define (unconsTree (d* : (List (BLDigit A))) → (Option (× (Tree A) (List (BLDigit A))))) + (match d* with + (Nil -> None) + (∷ d*-hd d*-tl -> + (match d*-hd with + (BLOne t -> + (match d*-tl with + (Nil -> (Some (tup t Nil))) + (∷ a b -> (Some (tup t (∷ BLZero d*-tl)))))) + (BLZero -> + (match (unconsTree d*-tl) with + (None -> None) + (Some udt -> + (match udt with + (a ts -> + (match a with + (Leaf x -> None) + (Node x t1 t2 -> + (Some (tup t1 (∷ (BLOne t2) ts)))))))))))))) + +(define (bl-empty → (BinaryList A)) + (BL Nil)) + +(define (bl-isEmpty (b : (BinaryList A)) → Bool) + (match b with + (BL x* -> + (match x* with + (Nil -> #t) + (∷ a b -> #f))))) + +(define (bl-cons (x : A) (b : (BinaryList A)) → (BinaryList A)) + (match b with + (BL ts -> (BL (consTree (Leaf x) ts))))) + +(define (bl-head (b : (BinaryList A)) → (Option A)) + (match b with + (BL ts -> + (match (unconsTree ts) with + (None -> None) + (Some xy -> + (match xy with + (x y -> + (match x with + (Leaf x -> (Some x)) + (Node a b c -> None))))))))) + +(define (bl-tail (b : (BinaryList A)) → (Option (BinaryList A))) + (match b with + (BL ts -> + (match (unconsTree ts) with + (None -> None) + (Some xy -> + (match xy with + (x ts2 -> (Some (BL ts2))))))))) + +(define (bl-lookup (i : Int) (b : (BinaryList A)) → (Option A)) + (match b with + [BL ts -> + (look i ts)])) + +(define (look [i : Int] [ts : (List (BLDigit A))] → (Option A)) + (match ts with + [Nil -> None] + [∷ h ts -> + (match h with + [BLZero -> + (look i ts)] + [BLOne t -> + (let ((size-t (size t))) + (if (< i size-t) + (lookTree i t) + (look (- i size-t) ts)))])])) + +(define (lookTree (i : Int) (t : (Tree A)) → (Option A)) + (match t with + [Leaf x -> + (if (= 0 i) + (Some x) + None)] + [Node w t1 t2 -> + (let ((w/2 (div w 2))) + (if (< i w/2) + (lookTree i t1) + (lookTree (- i w/2) t2)))])) + +(define (bl-update (i : Int) (y : A) (b : (BinaryList A)) → (Option (BinaryList A))) + (match b with + [BL ts -> + (match (upd i y ts) with + (None -> None) + (Some x -> (Some (BL x))))])) + +(define (upd (i : Int) (y : A) (b : (List (BLDigit A))) → (Option (List (BLDigit A)))) + (match b with + [Nil -> None] + [∷ h ts -> + (match h with + [BLZero -> + (match (upd i y ts) with + (None -> None) + (Some x -> (Some (∷ BLZero x))))] + [BLOne t -> + (let ((size-t (size t))) + (if (< i size-t) + (match (updTree i y t) with + (None -> None) + (Some x -> (Some (∷ (BLOne x) ts)))) + (match (upd (- i size-t) y ts) with + (None -> None) + (Some x -> (Some (∷ (BLOne t) x))))))])])) + +(define (updTree (i : Int) (y : A) (t : (Tree A)) → (Option (Tree A))) + (match t with + (Leaf x -> + (if (= 0 i) + (Some (Leaf y)) + None)) + (Node w t1 t2 -> + (let ((w/2 (div w 2))) + (if (< i w/2) + (match (updTree i y t1) with + (None -> None) + (Some x -> (Some (Node w x t2)))) + (match (updTree (- i w/2) y t2) with + (None -> None) + (Some x -> (Some (Node w t1 x))))))))) + +(define (list->bl-list (x* : (List A)) → (BinaryList A)) + (match x* with + (Nil -> (bl-empty)) + (∷ x x* -> (bl-cons x (list->bl-list x*))))) + +;; ============================================================================= + +(define bl-digit* + (list->bl-list (∷ 1 (∷ 2 (∷ 3 (∷ 4 (∷ 5 (∷ 6 (∷ 7 (∷ 8 (∷ 9 Nil))))))))))) + +(define (bl-nil → (BinaryList Int)) + (list->bl-list Nil)) + +(check-type + (bl-isEmpty (bl-nil)) + : Bool + ⇒ #t) + +(check-type + (bl-isEmpty bl-digit*) + : Bool + ⇒ #f) + +(check-type + (match (bl-head bl-digit*) with + (None -> 0) + (Some x -> x)) + : Int + ⇒ 1) + +(check-type + (match (bl-tail bl-digit*) with + (None -> 0) + (Some x -> + (match (bl-head x) with + (None -> 0) + (Some y -> y)))) + : Int + ⇒ 2) + +(check-type + (match (bl-lookup 7 bl-digit*) with + (None -> 0) + (Some x -> x)) + : Int + ⇒ 8) + +(check-type + (match (bl-lookup 8 bl-digit*) with + (None -> 0) + (Some x -> x)) + : Int + ⇒ 9) + +(check-type + (bl-lookup -111 bl-digit*) + : (Option Int) + ⇒ None) + +(check-type + (match (bl-update 3 99 bl-digit*) with + (None -> None) + (Some x -> (bl-lookup 3 x))) + : (Option Int) + ⇒ (Some 99)) + +(check-type + (match (bl-update 0 222 bl-digit*) with + (None -> None) + (Some x -> (bl-head x))) + : (Option Int) + ⇒ (Some 222)) + +(check-type + (bl-update 83 1 bl-digit*) + : (Option (BinaryList Int)) + ⇒ None) + +;; ============================================================================= +;; === Skew Binary Random Access Lists + +(define-type (ATree A) + (ALeaf A) + (ANode A (ATree A) (ATree A))) + +(define-type (SkewList A) + (SL (List (× Int (ATree A))))) + +(define (sb-empty → (SkewList A)) + (SL Nil)) + +(define (sb-isEmpty (sl : (SkewList A)) → Bool) + (match sl with + (SL xs -> + (match xs with + (Nil -> #t) + (∷ a b -> #f))))) + +(define (sb-cons (x : A) (sl : (SkewList A)) → (SkewList A)) + (match sl with + (SL ts -> + (let ((base-case (SL (∷ (tup 1 (ALeaf x)) ts)))) + (match ts with + (Nil -> base-case) + (∷ w1t1 ts -> + (match ts with + (Nil -> base-case) + (∷ w2t2 ts -> + (match w1t1 with + (w1 t1 -> + (match w2t2 with + (w2 t2 -> + (if (= w1 w2) + (SL (∷ (tup (+ 1 (+ w1 w2)) (ANode x t1 t2)) ts)) + base-case))))))))))))) + +(define (sb-head (sl : (SkewList A)) → (Option A)) + (match sl with + (SL ts -> + (match ts with + (Nil -> None) + (∷ w1t1 ts -> + (match w1t1 with + (w1 t1 -> + (match t1 with + (ALeaf x -> + (if (= w1 1) + (Some x) + None)) ;; Invariant error + (ANode x t1 t2 -> + (Some x)))))))))) + +(define (sb-tail (sl : (SkewList A)) → (Option (SkewList A))) + (match sl with + (SL ts -> + (match ts with + (Nil -> None) + (∷ w1t1 ts -> + (match w1t1 with + (w1 t1 -> + (match t1 with + (ALeaf x -> + (if (= 1 w1) + (Some (SL ts)) + None)) ;; Invariant + (ANode x t1 t2 -> + (let ((w1/2 (div w1 2))) + (Some (SL (∷ (tup w1/2 t1) (∷ (tup w1/2 t2) ts)))))))))))))) + +(define (sb-lookup (i : Int) (sl : (SkewList A)) → (Option A)) + (match sl with + (SL ts -> + (sb-look i ts)))) + +(define (sb-look (i : Int) (ts : (List (× Int (ATree A)))) → (Option A)) + (match ts with + (Nil -> None) ;; Bad subscript + (∷ wt ts -> + (match wt with + (w t -> + (if (< i w) + (sb-lookTree w i t) + (sb-look (- i w) ts))))))) + +(define (sb-lookTree (w : Int) (i : Int) (t : (ATree A)) → (Option A)) + (match t with + (ALeaf x -> + (if (and (= w 1) (= i 0)) + (Some x) + None)) + (ANode x t1 t2 -> + (if (= 0 i) + (Some x) + (let ((w/2 (div w 2))) + (if (<= i w/2) + (sb-lookTree w/2 (- i 1) t1) + (sb-lookTree w/2 (- (- i 1) w/2) t2))))))) + +(define (sb-update (i : Int) (y : A) (sl : (SkewList A)) → (Option (SkewList A))) + (match sl with + (SL ts -> + (match (sb-upd i y ts) with + (None -> None) + (Some ts -> (Some (SL ts))))))) + +(define (sb-upd (i : Int) (y : A) (ts : (List (× Int (ATree A)))) → (Option (List (× Int (ATree A))))) + (match ts with + (Nil -> None) + (∷ wt ts -> + (match wt with + (w t -> + (if (< i w) + (match (sb-updTree w i y t) with + (None -> None) + (Some x -> (Some (∷ (tup w x) ts)))) + (match (sb-upd (- i w) y ts) with + (None -> None) + (Some x -> (Some (∷ (tup w t) x)))))))))) + +(define (sb-updTree (w : Int) (i : Int) (y : A) (t : (ATree A)) → (Option (ATree A))) + (match t with + (ALeaf x -> + (if (and (= 1 w) (= 0 i)) + (Some (ALeaf y)) + None)) ;; Invariant error + (ANode x t1 t2 -> + (if (= 0 i) + (Some (ANode y t1 t2)) + (let ((w/2 (div w 2))) + (if (<= i w/2) + (match (sb-updTree w/2 (- i 1) y t1) with + (None -> None) + (Some z -> (Some (ANode x z t2)))) + (match (sb-updTree w/2 (- (- i 1) w/2) y t2) with + (None -> None) + (Some z -> (Some (ANode x t1 z)))))))))) + +(define (list->sb-list (x* : (List A)) → (SkewList A)) + (match x* with + (Nil -> (sb-empty)) + (∷ h t -> (sb-cons h (list->sb-list t))))) + +;; ============================================================================= + +(define sb-digit* + (list->sb-list (∷ 1 (∷ 2 (∷ 3 (∷ 4 (∷ 5 (∷ 6 (∷ 7 (∷ 8 (∷ 9 Nil))))))))))) + +(define (sb-nil → (SkewList Int)) + (list->sb-list Nil)) + +(check-type + (sb-isEmpty (sb-nil)) + : Bool + ⇒ #t) + +(check-type + (sb-isEmpty sb-digit*) + : Bool + ⇒ #f) + +(check-type + (match (sb-head sb-digit*) with + (None -> 0) + (Some x -> x)) + : Int + ⇒ 1) + +(check-type + (match (sb-tail sb-digit*) with + (None -> 0) + (Some x -> + (match (sb-head x) with + (None -> 0) + (Some y -> y)))) + : Int + ⇒ 2) + +(check-type + (match (sb-lookup 7 sb-digit*) with + (None -> 0) + (Some x -> x)) + : Int + ⇒ 8) + +(check-type + (match (sb-lookup 8 sb-digit*) with + (None -> 0) + (Some x -> x)) + : Int + ⇒ 9) + +(check-type + (sb-lookup -111 sb-digit*) + : (Option Int) + ⇒ None) + +(check-type + (match (sb-update 3 99 sb-digit*) with + (None -> None) + (Some x -> (sb-lookup 3 x))) + : (Option Int) + ⇒ (Some 99)) + +(check-type + (match (sb-update 0 222 sb-digit*) with + (None -> None) + (Some x -> (sb-head x))) + : (Option Int) + ⇒ (Some 222)) + +(check-type + (sb-update 83 1 sb-digit*) + : (Option (SkewList Int)) + ⇒ None) + +;; ============================================================================= +;; === Alt Binary Random Access List + +(define-type (BinaryRAList A) + (ABLNil) + (ABLZero (BinaryRAList (× A A))) + (ABLOne A (BinaryRAList (× A A)))) + +(define (abl-uncons (bl : (BinaryRAList A)) → (Option (× A (BinaryRAList A)))) + (match bl with + (ABLNil -> None) + (ABLOne x ps -> + (Some (match ps with + (ABLNil -> (tup x ABLNil)) + (ABLOne y ps2 -> (tup x (ABLZero ps))) + (ABLZero ps2 -> (tup x (ABLZero ps)))))) + (ABLZero ps -> + (match (abl-uncons ps) with + (None -> None) + (Some xyps2 -> + (match xyps2 with + (xy ps2 -> + (match xy with + (x y -> (Some (tup x (ABLOne y ps2)))))))))))) + +(define (abl-fupdate (f : (→ A A)) (i : Int) (bl : (BinaryRAList A)) → (Option (BinaryRAList A))) + (match bl with + (ABLNil -> None) + (ABLOne x ps -> + (if (= 0 i) + (Some (ABLOne (f x) ps)) + (match (abl-fupdate f (- i 1) (ABLZero ps)) with + (None -> None) + (Some z -> (Some (abl-cons x z)))))) + (ABLZero ps -> + (let ((f2 (if (= 0 (mod i 2)) + (λ ([xy : (× A A)]) + (match xy with (x y -> (tup (f x) y)))) + (λ ([xy : (× A A)]) + (match xy with (x y -> (tup x (f y)))))))) + (match (abl-fupdate f2 (div i 2) ps) with + (None -> None) + (Some z -> (Some (ABLZero z)))))))) + +(define (aabl-empty → (BinaryRAList A)) + ABLNil) + +(define (abl-isEmpty (bl : (BinaryRAList A)) → Bool) + (match bl with + (ABLNil -> #t) + (ABLOne a b -> #f) + (ABLZero a -> #f))) + +(define (abl-cons (x : A) (bl : (BinaryRAList A)) → (BinaryRAList A)) + (match bl with + (ABLNil -> (ABLOne x ABLNil)) + (ABLZero ps -> (ABLOne x ps)) + (ABLOne y ps -> (ABLZero (abl-cons (tup x y) ps))))) + +(define (abl-head (bl : (BinaryRAList A)) → (Option A)) + (match (abl-uncons bl) with + (None -> None) + (Some xy -> + (match xy with + (x y -> (Some x)))))) + +(define (abl-tail (bl : (BinaryRAList A)) → (Option (BinaryRAList A))) + (match (abl-uncons bl) with + (None -> None) + (Some xy -> + (match xy with + (x y -> (Some y)))))) + +(define (abl-lookup (i : Int) (bl : (BinaryRAList A)) → (Option A)) + (if (< i 0) + None + (abl-lookup/natural i bl))) + +(define (abl-lookup/natural (i : Int) (bl : (BinaryRAList A)) → (Option A)) + (match bl with + (ABLNil -> None) + (ABLOne x ps -> + (if (= 0 i) + (Some x) + (abl-lookup/natural (- i 1) (ABLZero ps)))) + (ABLZero ps -> + (match (abl-lookup/natural (div i 2) ps) with + (None -> None) + (Some xy -> + (match xy with + (x y -> + (if (= 0 (mod i 2)) + (Some x) + (Some y))))))))) + +(define (abl-update (i : Int) (y : A) (bl : (BinaryRAList A)) → (Option (BinaryRAList A))) + (abl-fupdate (λ ([x : A]) y) i bl)) + +(define (list->abl-list (xs : (List A)) → (BinaryRAList A)) + (match xs with + (Nil -> (aabl-empty)) + (∷ a b -> (abl-cons a (list->abl-list b))))) + +;; ============================================================================= + +(define abl-digit* + (list->abl-list (∷ 1 (∷ 2 (∷ 3 (∷ 4 (∷ 5 (∷ 6 (∷ 7 (∷ 8 (∷ 9 Nil))))))))))) + +(define (abl-nil → (BinaryRAList Int)) + (list->abl-list Nil)) + +(check-type + (abl-isEmpty (abl-nil)) + : Bool + ⇒ #t) + +(check-type + (abl-isEmpty abl-digit*) + : Bool + ⇒ #f) + +(check-type + (match (abl-head abl-digit*) with + (None -> 0) + (Some x -> x)) + : Int + ⇒ 1) + +(check-type + (match (abl-tail abl-digit*) with + (None -> 0) + (Some x -> + (match (abl-head x) with + (None -> 0) + (Some y -> y)))) + : Int + ⇒ 2) + +(check-type + (match (abl-lookup 7 abl-digit*) with + (None -> 0) + (Some x -> x)) + : Int + ⇒ 8) + +(check-type + (match (abl-lookup 8 abl-digit*) with + (None -> 0) + (Some x -> x)) + : Int + ⇒ 9) + +(check-type + (abl-lookup -111 abl-digit*) + : (Option Int) + ⇒ None) + +(check-type + (match (abl-update 3 99 abl-digit*) with + (None -> None) + (Some x -> (abl-lookup 3 x))) + : (Option Int) + ⇒ (Some 99)) + +(check-type + (match (abl-update 0 222 abl-digit*) with + (None -> None) + (Some x -> (abl-head x))) + : (Option Int) + ⇒ (Some 222)) + +(check-type + (abl-update 83 1 abl-digit*) + : (Option (BinaryRAList Int)) + ⇒ None) + diff --git a/macrotypes/examples/tests/mlish/chameneos.mlish b/macrotypes/examples/tests/mlish/chameneos.mlish new file mode 100644 index 0000000..b36a7e8 --- /dev/null +++ b/macrotypes/examples/tests/mlish/chameneos.mlish @@ -0,0 +1,129 @@ +#lang s-exp "../../mlish.rkt" +(require "../rackunit-typechecking.rkt") + +(define-type Color Red Yellow Blue) + +(define-type (Option X) None (Some X)) + +(define-type-alias Meet + (× (Channel (Option (× Color String))) + (× Color String))) + +(define-type-alias Result (× Int Int)) + +(define-type-alias MeetChan (Channel Meet)) +(define-type-alias ResultChan (Channel Result)) + +(typecheck-fail (channel-put (make-channel {Bool}) 1) + #:with-msg "channel-put: type mismatch: expected Bool, given Int\n *expression: 1") + +(define (change [c1 : Color] [c2 : Color] -> Color) + (match c1 with + [Red -> + (match c2 with + [Blue -> Yellow] + [Yellow -> Blue] + [Red -> c1])] + [Yellow -> + (match c2 with + [Blue -> Red] + [Red -> Blue] + [Yellow -> c1])] + [Blue -> + (match c2 with + [Yellow -> Red] + [Red -> Yellow] + [Blue -> c1])])) + +(check-type (change Red Blue) : Color -> Yellow) +(check-type (change Yellow Red) : Color -> Blue) +(check-type (change Blue Blue) : Color -> Blue) + +(define NONE (None {(× Color String)})) + +(define (get+put [ch-meet : MeetChan] -> Unit) + (match (channel-get ch-meet) with + [ch v -> + (begin (channel-put ch NONE) + (get+put ch-meet))])) + +(define (swap [ch-meet : MeetChan] [n : Int] -> Unit) + (if (zero? n) + (get+put ch-meet) + (match (channel-get ch-meet) with + [ch1 v1 -> + (match (channel-get ch-meet) with + [ch2 v2 -> + (begin (channel-put ch1 (Some v2)) + (channel-put ch2 (Some v1)) + (swap ch-meet (sub1 n)))])]))) + + +(define (place [ch-meet : MeetChan] [n : Int] -> Thread) + (thread (λ () (swap ch-meet n)))) + +(define (rand-name -> String) + (string (integer->char (random 256)))) + +(define (sleeper [ch-meet : MeetChan] [ch-res : ResultChan] + [ch : (Channel (Option (× Color String)))] + [name : String] [c : Color] [met : Int] [same : Int] + -> Unit) + (begin + (channel-put ch-meet (tup ch (tup c name))) + (match (channel-get ch) with + [Some c+s -> + (match c+s with + [other-col other-name -> + (begin + (sleep 0) + (sleeper + ch-meet ch-res ch + name (change c other-col) + (add1 met) (+ same (if (string=? name other-name) 1 0))))])] + [None -> (channel-put ch-res (tup met same))]))) + +(define (creature [c : Color] [ch-meet : MeetChan] [ch-res : ResultChan] + -> Thread) + (thread + (λ () + (let ([ch (make-channel {(Option (× Color String))})] + [name (rand-name)]) + (sleeper ch-meet ch-res ch name c 0 0))))) + +(define (map [f : (→ X Y)] [lst : (List X)] -> (List Y)) + (if (isnil lst) + nil + (cons (f (head lst)) (map f (tail lst))))) + +(define (go [n : Int] [inits : (List Color)] -> (List Result)) + (let* ([ch-res (make-channel {Result})] + [ch-meet (make-channel {Meet})] + [start (place ch-meet n)] + [ths (map (λ ([c : Color]) (creature c ch-meet ch-res)) inits)]) + (map (λ ([c : Color]) (channel-get ch-res)) inits))) + +(define res1 (go 100 (list Blue Red Yellow))) + +(define (check-res1 [r : Result] -> Bool) + (match r with + [met same -> (or (= met 66) (= met 67))])) + +(check-type (length res1) : Int -> 3) + +(check-type (check-res1 (list-ref res1 0)) : Bool -> #t) +(check-type (check-res1 (list-ref res1 1)) : Bool -> #t) +(check-type (check-res1 (list-ref res1 2)) : Bool -> #t) + ;; -> (list (list 67 0) + ;; (list 66 0) + ;; (list 67 0))) + +(check-type (map (λ ([x : Result]) (proj x 0)) + (go 1000 (list Blue Red Yellow Red Yellow Blue))) + : (List Int) -> (list 333 333 333 333 334 334)) + ;; -> (list (list 333 0) + ;; (list 333 0) + ;; (list 333 0) + ;; (list 333 0) + ;; (list 334 0) + ;; (list 334 0))) diff --git a/macrotypes/examples/tests/mlish/fannkuch.mlish b/macrotypes/examples/tests/mlish/fannkuch.mlish new file mode 100644 index 0000000..27ec3ea --- /dev/null +++ b/macrotypes/examples/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/macrotypes/examples/tests/mlish/fasta.mlish b/macrotypes/examples/tests/mlish/fasta.mlish new file mode 100644 index 0000000..fe754be --- /dev/null +++ b/macrotypes/examples/tests/mlish/fasta.mlish @@ -0,0 +1,191 @@ +#lang s-exp "../../mlish.rkt" +(require "../rackunit-typechecking.rkt") + +(define +alu+ + (string-append "GGCCGGGCGCGGTGGCTCACGCCTGTAATCCCAGCACTTTGG" + "GAGGCCGAGGCGGGCGGATCACCTGAGGTCAGGAGTTCGAGA" + "CCAGCCTGGCCAACATGGTGAAACCCCGTCTCTACTAAAAAT" + "ACAAAAATTAGCCGGGCGTGGTGGCGCGCGCCTGTAATCCCA" + "GCTACTCGGGAGGCTGAGGCAGGAGAATCGCTTGAACCCGGG" + "AGGCGGAGGTTGCAGTGAGCCGAGATCGCGCCACTGCACTCC" + "AGCCTGGGCGACAGAGCGAGACTCCGTCTCAAAAA")) + +(check-type +alu+ : String) + +(define IUB + (hash #\a 0.27 #\c 0.12 #\g 0.12 #\t 0.27 #\B 0.02 + #\D 0.02 #\H 0.02 #\K 0.02 #\M 0.02 #\N 0.02 + #\R 0.02 #\S 0.02 #\V 0.02 #\W 0.02 #\Y 0.02)) + +(check-type IUB : (Hash Char Float)) + +(define HOMOSAPIEN + (hash #\a 0.3029549426680 #\c 0.1979883004921 + #\g 0.1975473066391 #\t 0.3015094502008)) + +(check-type HOMOSAPIEN : (Hash Char Float)) + +(define line-length 60) + +(check-type line-length : Int) + +(define (repeat-fasta [header : String] [N : Int] [sequence : String] -> String) + (let* ([out (open-output-string)] + [len (string-length sequence)] + [buf (make-string (+ len line-length))]) + (string-copy! buf 0 sequence) + (string-copy! buf len sequence 0 line-length) + (write-string header out) + (let loop : String ([n N] [start 0]) + (if (> n 0) + (let ([end (+ start (min n line-length))]) + (write-string buf out start end) + (write-string "\n" out) + (loop (- n line-length) (if (> end len) (- end len) end))) + (get-output-string out))))) + +(define IA 3877) +(define IC 29573) +(define IM 139968) +(define IM.0 (fx->fl IM)) + +(define V + (for/vector ([id (in-range IM)]) + (modulo (+ IC (* id IA)) IM))) + +(check-type V : (Vector Int)) + +(define (random-next [cur : Int] -> Int) (vector-ref V cur)) + +(check-type (tup 0 0.0) : (× Int Float)) + +(check-type (in-hash IUB) : (Sequence (× Char Float))) + +(define (make-lookup-table [frequency-table : (Hash Char Float)] -> String) + (let ([v (make-string IM)]) + (for/fold ([cs (tup 0 0.0)]) + ([k+v (in-hash frequency-table)]) + (match cs with + [c c. -> + (match k+v with + [key val -> + (let* ([c1. (fl+ c. (fl* IM.0 val))] + [c1 (inexact->exact (flceiling c1.))] + #;[b (char->integer key)]) + (for ([i (in-range c c1)]) (string-set! v i key)) + (tup c1 c1.))])])) + v)) + +(define (n-randoms [buf : String][out : String-Port][lookup : String] + [to : Int][R : Int] -> Int) + (let loop : Int ([n 0] [R R]) + (if (< n to) + (let ([R (random-next R)]) + (string-set! buf n (string-ref lookup R)) + (loop (add1 n) R)) + (begin (write-string buf out 0 (add1 to)) R)))) + +(define LF #\newline) + +(define (make-line! [buf : String] [lookup : String] + [start : Int] [R : Int] -> Int) + (let ([end (+ start line-length)]) + (string-set! buf end LF) + (let loop : Int ([n start] [R R]) + (if (< n end) + (let ([R (random-next R)]) + (string-set! buf n (string-ref lookup R)) + (loop (add1 n) R)) + R)))) + +(define (random-fasta [header : String] [N : Int] + [table : (Hash Char Float)] [R : Int] + -> (× Int String)) + (let* ([buf (make-string (add1 line-length))] + [out (open-output-string)] + [lookup-str (make-lookup-table table)] + [full-lines+last (quotient+remainder N line-length)] + [C + (let* ([len+1 (add1 line-length)] + [buflen (* len+1 IM)] + [buf2 (make-string buflen)]) + (let loop : String ([R R] [i 0]) + (if (< i buflen) + (loop (make-line! buf2 lookup-str i R) (+ i len+1)) + buf2)))]) + (string-set! buf line-length LF) + (write-string header out) + (tup + (match full-lines+last with + [full-lines last -> + (let loop : Int ([i full-lines] [R R]) + (if (> i IM) + (begin (write-string C out) (loop (- i IM) R)) + (let loop : Int ([i i] [R R]) + (cond + [(> i 0) + (loop + (sub1 i) + (n-randoms buf out lookup-str line-length R))] + [(> last 0) + (string-set! buf last LF) + (n-randoms buf out lookup-str last R)] + [else R]))))]) + (get-output-string out)))) + +(define n 10) + +(check-type (repeat-fasta ">ONE Homo sapiens alu\n" (* n 2) +alu+) : String + -> ">ONE Homo sapiens alu\nGGCCGGGCGCGGTGGCTCAC\n") + +(define res1 + (random-fasta ">TWO IUB ambiguity codes\n" (* n 3) IUB 42)) + +(define res2 + (match res1 with + [R str -> + (random-fasta ">THREE Homo sapiens frequency\n" (* n 5) HOMOSAPIEN R)])) + +(check-type (proj res1 1) : String + -> ">TWO IUB ambiguity codes\nattRtBtaDtatVataKatgaatcccgDtY\n") + +(check-type (proj res2 1) : String + -> (string-append ">THREE Homo sapiens frequency\n" + "atttgcggaaacgacaaatattaacacatcatcagagtaccataaaggga\n")) + +(define (mk-fasta [n : Int] -> String) + (let + ([res1 (repeat-fasta ">ONE Homo sapiens alu\n" (* n 2) +alu+)] + [res2 (random-fasta ">TWO IUB ambiguity codes\n" (* n 3) IUB 42)] + [res3 + (match res2 with + [R str -> + (random-fasta ">THREE Homo sapiens frequency\n" (* n 5) HOMOSAPIEN R)])]) + (string-append res1 (proj res2 1) (proj res3 1)))) + +(provide mk-fasta) + +(check-type (mk-fasta 100) + : String + -> (string-append + ">ONE Homo sapiens alu\n" + "GGCCGGGCGCGGTGGCTCACGCCTGTAATCCCAGCACTTTGGGAGGCCGAGGCGGGCGGA\n" + "TCACCTGAGGTCAGGAGTTCGAGACCAGCCTGGCCAACATGGTGAAACCCCGTCTCTACT\n" + "AAAAATACAAAAATTAGCCGGGCGTGGTGGCGCGCGCCTGTAATCCCAGCTACTCGGGAG\n" + "GCTGAGGCAGGAGAATCGCT\n" + ">TWO IUB ambiguity codes\n" + "attRtBtaDtatVataKatgaatcccgDtYtcccNaNgtRttNtatttatcctSaRataW\n" + "taatNtNctaatctttggMtMttKtYtMHagBttagcMKMttttcWaactgcSttgaaac\n" + "gtcatHagHtgtaHVgtcattatgRcaVcaatctcWgaNtttVaaYcaaaataYtgWgtt\n" + "acttMgtHHgagtattaaaKSgtBgacaaggSaaRttVaVDHttRgctagtaaacgaaac\n" + "ttcRNtgcatttSagBtHttNRaatgtctattcaSaRYcgtatSattttttttgaBgagD\n" + ">THREE Homo sapiens frequency\n" + "gaagacaggtgtaacgtgggaaaatctctagtaaagctttgatcagcggagacgcgatca\n" + "acagatcctttatatcgcgaaacttctctctatcagcgaactaaggagggcgacaatccg\n" + "agctgttccggaccaaaccctgaaagtacgactctgctctaataaagtcaaaacgtagaa\n" + "gactagatacaattatactgacaacaaaaaaaagttgcgtgcacaagagtacgatgtttg\n" + "accgccagttattatgacgagggtgagaacaagtcaggctaaagtagaagagcaccatag\n" + "gtatcagtttaactgagtaaatgcgaatgcgtgactttaaataagcctgcgtgtgtcaaa\n" + "actctacaatatctttgttatattattgaatcattctggatttgaggcagtggagcatac\n" + "tgtataaaataatttttcggtgggtcaaaaataaatttcaattaagacgttaaggataat\n" + "gaaatgactcaatctaaggt\n")) diff --git a/macrotypes/examples/tests/mlish/fibo.mlish b/macrotypes/examples/tests/mlish/fibo.mlish new file mode 100644 index 0000000..7857ce2 --- /dev/null +++ b/macrotypes/examples/tests/mlish/fibo.mlish @@ -0,0 +1,22 @@ +#lang s-exp "../../mlish.rkt" +(require "../rackunit-typechecking.rkt") + +(define (fib [n : Int] -> Int) + (cond + [(< n 2) 1] + [else + (+ (fib (- n 2)) (fib (sub1 n)))])) + +(define (main [args : (Vector String)] -> Int) + (let ([n (if (= (vector-length args) 0) + 1 + (string->number (vector-ref args 0)))]) + (fib n))) + +(check-type (main (vector "0")) : Int -> 1) + +(check-type (main (vector "1")) : Int -> 1) + +(check-type (main (vector "2")) : Int -> 2) + +(check-type (main (vector "22")) : Int -> 28657) diff --git a/macrotypes/examples/tests/mlish/find.mlish b/macrotypes/examples/tests/mlish/find.mlish new file mode 100644 index 0000000..df8b335 --- /dev/null +++ b/macrotypes/examples/tests/mlish/find.mlish @@ -0,0 +1,87 @@ +#lang s-exp "../../mlish.rkt" +(require "../rackunit-typechecking.rkt") + +(define-type (List X) + Nil + (Cons X (List X))) + +(define-type (Option X) + None + (Some X)) + +(define (find [lst : (List X)] [pred : (→ X Bool)] → (Option X)) + (match lst with + [Nil -> None] + [Cons fst rst -> + (cond [(pred fst) (Some fst)] + [else (find rst pred)])])) + +(check-type + (find (Cons 1 (Cons 2 (Cons 3 Nil))) (λ ([x : Int]) (<= 2 x))) + : (Option Int) + -> (Some 2)) + +(check-type + (find (Cons 1 (Cons 0 (Cons -1 Nil))) (λ ([x : Int]) (<= 2 x))) + : (Option Int) + -> None) + +;; args inferred in order, L-to-R, currently no backtracking +(check-type + (find Nil (λ ([x : Int]) (<= 2 x))) + : (Option Int) + -> None) + +;; reversing arg order leads to successful inference +(define (find2 [pred : (→ X Bool)] [lst : (List X)] → (Option X)) + (match lst with + [Nil -> None] + [Cons fst rst -> + (cond [(pred fst) (Some fst)] + [else (find2 pred rst)])])) + +(check-type + (find2 (λ ([x : Int]) (<= 2 x)) Nil) + : (Option Int) + -> None) + +(define (find-min/max [lst : (List X)] [ None] + [Cons x1 rst -> + (let ([y1 (extract-key x1)]) + (Some (find-min/max-accum rst (tup x-min x-max)] + [Cons x2 rst -> + (let ([y2 (extract-key x2)]) + (cond [( None) + +(check-type + (find-min/max (Cons 1 (Cons 2 (Cons 3 Nil))) + (λ ([x : Int] [y : Int]) + (< x y)) + (λ ([x : Int]) + x)) + : (Option (× Int Int)) + -> (Some (tup 1 3))) + diff --git a/macrotypes/examples/tests/mlish/hash.mlish b/macrotypes/examples/tests/mlish/hash.mlish new file mode 100644 index 0000000..87e2d3e --- /dev/null +++ b/macrotypes/examples/tests/mlish/hash.mlish @@ -0,0 +1,19 @@ +#lang s-exp "../../mlish.rkt" +(require "../rackunit-typechecking.rkt") + +(define (main [argv : (Vector String)] -> Int) + (let* ([n (string->number (vector-ref argv 0))] + [hash + (for/hash ([i (in-range n)]) + (let ([j (add1 i)]) + (tup (number->string j 16) j)))]) + (for/sum ([i (in-range 1 (add1 n))] + #:when + (hash-has-key? hash (number->string i))) + 1))) + +(check-type (main (vector "2000")) : Int -> 799) + +(check-type (main (vector "20000")) : Int -> 4999) + +(check-type (main (vector "200000")) : Int -> 30999) diff --git a/macrotypes/examples/tests/mlish/infer-variances.mlish b/macrotypes/examples/tests/mlish/infer-variances.mlish new file mode 100644 index 0000000..55a72f1 --- /dev/null +++ b/macrotypes/examples/tests/mlish/infer-variances.mlish @@ -0,0 +1,243 @@ +#lang s-exp "../../mlish.rkt" +(require "../rackunit-typechecking.rkt") + +(define-type T1 t1) +;; No type arguments to determine variance for. + +(check-type t1 : T1 -> t1) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; Non-Recursive Types + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(define-type (T2 X) t2) +;; X should be inferred to be irrelevant within (T2 X). +;; That means it should be both covariant and contravariant. + +;; This checks that X is covariant within (T2 X). +(define (t2* → (T2 X)) t2) +(define (t2** → (→ (T2 X))) (inst t2* X)) +(check-type (t2**) : (→/test (T2 X))) + +;; This checks that X is contravariant within (T2 X), +;; by checking that X is covariant within (→ (T2 X) Int). +(define (t2->int [t2 : (T2 X)] → Int) 0) +(define (t2->int* → (→ (T2 X) Int)) (inst t2->int X)) +(check-type (t2->int*) : (→/test (T2 X) Int)) + +;; This checks that X is irrelevant, even within a Ref type, +;; by checking that X is covariant within (Ref (T2 X)). +;; This is still sound because a value of type (Ref (T2 X)) will never +;; contain anything of type X anyway. X is irrelevant within it. +(define (ref-t2* → (Ref (T2 X))) (ref (t2 {X}))) +(define (ref-t2** → (→ (Ref (T2 X)))) (inst ref-t2* X)) +(check-type (ref-t2**) : (→/test (Ref (T2 X)))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(define-type (T3 X) t3-none (t3-some X)) +;; X should be inferred to be covariant within (T3 X). + +;; This checks that X is covariant within (T3 X). +(define (t3-none* → (T3 X)) t3-none) +(define (t3-none** → (→ (T3 X))) (inst t3-none* X)) +(check-type (t3-none**) : (→/test (T3 X))) + +;; This checks that X is not contravariant within (T3 X), +;; by checking that X is not covariant within (→ (T3 X) Int). +(define (t3->int [t3 : (T3 X)] → Int) 0) +(define (t3->int* → (→ (T3 X) Int)) (inst t3->int X)) +(typecheck-fail (t3->int*)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(define-type (T4 X) t4-none (t4-some (→ X Int))) +;; X should be inferred to be contravariant within (T4 X). + +;; This checks that X is not covariant within (T4 X). +(define (t4-none* → (T4 X)) t4-none) +(define (t4-none** → (→ (T4 X))) (inst t4-none* X)) +(typecheck-fail (t4-none**)) + +;; This checks that X is contravariant within (T4 X), +;; by checking that X is covariant within (→ (T4 X) Int). +(define (t4->int [t4 : (T4 X)] → Int) 0) +(define (t4->int* → (→ (T4 X) Int)) (inst t4->int X)) +(check-type (t4->int*) : (→/test (T4 X) Int)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(define-type (T5 X) t5-none (t5-some+ X) (t5-some- (→ X Int))) +;; X should be inferred to be invariant within (T5 X). + +;; This checks that X is not covariant within (T5 X). +(define (t5-none* → (T5 X)) t5-none) +(define (t5-none** → (→ (T5 X))) (inst t5-none* X)) +(typecheck-fail (t5-none**)) + +;; This checks that X is not contravariant within (T5 X), +;; by checking that X is not covariant within (→ (T5 X) Int). +(define (t5->int [t5 : (T5 X)] → Int) 0) +(define (t5->int* → (→ (T5 X) Int)) (inst t5->int X)) +(typecheck-fail (t5->int*)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; Recursive Types + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(define-type (T6 X) t6-none (t6-same (T6 X))) +;; X should be inferred to be irrelevant within (T6 X). + +;; This checks that X is covariant within (T6 X). +(define (t6-none* → (T6 X)) t6-none) +(define (t6-none** → (→ (T6 X))) (inst t6-none* X)) +(check-type (t6-none**) : (→/test (T6 X))) + +;; This checks that X is contravariant within (T6 X), +;; by checking that X is covariant within (→ (T6 X) Int). +(define (t6->int [t6 : (T6 X)] → Int) 0) +(define (t6->int* → (→ (T6 X) Int)) (inst t6->int X)) +(check-type (t6->int*) : (→/test (T6 X) Int)) + +;; This checks that X is irrelevant, even within a Ref type, +;; by checking that X is covariant within (Ref (T6 X)). +;; This is still sound because a value of type (Ref (T6 X)) will never +;; contain anything of type X anyway. X is irrelevant within it. +(define (ref-t6* → (Ref (T6 X))) (ref (t6-none {X}))) +(define (ref-t6** → (→ (Ref (T6 X)))) (inst ref-t6* X)) +(check-type (ref-t6**) : (→/test (Ref (T6 X)))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(define-type (T7 X) t7-none (t7-weird (→ (T7 X) Int))) +(define-type (T8 X) t8-none (t8-weird (T8 (→ X Int)))) +(define-type (T9 X) t9-none (t9-weird (→ (T9 (→ X Int)) Int))) +;; X should be inferred to be irrelevant within (T7 X), (T8 X), and +;; (T9 X). None of these types could contain or recieve an actual X. + +(define-type (T10 X) (t10 (T7 X) (T8 X) (T9 X))) +;; So because of that, X should be irrelevant within (T10 X). + +;; This checks that X is covariant within (T10 X). +(define (t10-none* → (T10 X)) (t10 t7-none t8-none t9-none)) +(define (t10-none** → (→ (T10 X))) (inst t10-none* X)) +(check-type (t10-none**) : (→/test (T10 X))) + +;; This checks that X is contravariant within (T10 X), +;; by checking that X is covariant within (→ (T10 X) Int). +(define (t10->int [t10 : (T10 X)] → Int) 0) +(define (t10->int* → (→ (T10 X) Int)) (inst t10->int X)) +(check-type (t10->int*) : (→/test (T10 X) Int)) + +;; This checks that X is irrelevant, even within a Ref type, +;; by checking that X is covariant within (Ref (T10 X)). +;; This is still sound because a value of type (Ref (T10 X)) will never +;; contain anything of type X anyway. X is irrelevant within it. +(define (ref-t10* → (Ref (T10 X))) (ref (t10 (t7-none {X}) (t8-none {X}) (t9-none {X})))) +(define (ref-t10** → (→ (Ref (T10 X)))) (inst ref-t10* X)) +(check-type (ref-t10**) : (→/test (Ref (T10 X)))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(define-type (T11 X) t11-none (t11+ X) (t11-weird (→ (T11 X) Int))) +(define-type (T12 X) t12-none (t12+ X) (t12-weird (T12 (→ X Int)))) +(define-type (T13 X) t13-none (t13+ X) + (t13-weird (→ (T13 (→ X Int)) Int))) +(define-type (T14 X) t14-none (t14- (→ X Int)) + (t14-weird (→ (T14 (→ X Int)) Int))) +;; X should be inferred to be invariant within (T11 X) and (T12 X), +;; but covariant within (T13 X), and contravariant within (T14 X). + +;; This checks that X is covariant within (T13 X), but not any of the +;; others. +(define (t11-none* → (T11 X)) t11-none) +(define (t12-none* → (T12 X)) t12-none) +(define (t13-none* → (T13 X)) t13-none) +(define (t14-none* → (T14 X)) t14-none) +(define (t11-none** → (→ (T11 X))) (inst t11-none* X)) +(define (t12-none** → (→ (T12 X))) (inst t12-none* X)) +(define (t13-none** → (→ (T13 X))) (inst t13-none* X)) +(define (t14-none** → (→ (T14 X))) (inst t14-none* X)) +(typecheck-fail (t11-none**)) +(typecheck-fail (t12-none**)) +(check-type (t13-none**) : (→/test (T13 X))) +(typecheck-fail (t14-none**)) + +;; This checks that X is contravariant within (T14 X), but not any of +;; the others. +(define (t11->int [t11 : (T11 X)] → Int) 0) +(define (t12->int [t12 : (T12 X)] → Int) 0) +(define (t13->int [t13 : (T13 X)] → Int) 0) +(define (t14->int [t14 : (T14 X)] → Int) 0) +(define (t11->int* → (→ (T11 X) Int)) (inst t11->int X)) +(define (t12->int* → (→ (T12 X) Int)) (inst t12->int X)) +(define (t13->int* → (→ (T13 X) Int)) (inst t13->int X)) +(define (t14->int* → (→ (T14 X) Int)) (inst t14->int X)) +(typecheck-fail (t11->int*)) +(typecheck-fail (t12->int*)) +(typecheck-fail (t13->int*)) +(check-type (t14->int*) : (→/test (T14 X) Int)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(define-type (T15 X) t15-none (t15-cons+ X (T15 X))) +(define-type (T16 X) t16-none (t16-cons- (→ X Int) (T16 X))) +;; X should be inferred to be covariant within (T15 X), and +;; contravariant within (T16 X). (T15 X) is just like a (List X) type, +;; and (T16 X) is just like a (List (→ X Int)). + +;; This checks that X is covariant within (T15 X). +(define (t15-none* → (T15 X)) t15-none) +(define (t15-none** → (→ (T15 X))) (inst t15-none* X)) +(check-type (t15-none**) : (→/test (T15 X))) +;; This checks that X is not covariant within (T16 X). +(define (t16-none* → (T16 X)) t16-none) +(define (t16-none** → (→ (T16 X))) (inst t16-none* X)) +(typecheck-fail (t16-none**)) + +;; This checks that X is not contravariant within (T15 X), +;; by checking that X is not covariant within (→ (T15 X) Int). +(define (t15->int [t15 : (T15 X)] → Int) 0) +(define (t15->int* → (→ (T15 X) Int)) (inst t15->int X)) +(typecheck-fail (t15->int*)) +;; This checks that X is contravariant within (T16 X), +;; by checking that X is covariant within (→ (T16 X) Int). +(define (t16->int [t16 : (T16 X)] → Int) 0) +(define (t16->int* → (→ (T16 X) Int)) (inst t16->int X)) +(check-type (t16->int*) : (→/test (T16 X) Int)) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; Mutually Recursive Types + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(define-type (T17 X) (t17-some X) (t18 (T18 X))) +(define-type (T18 X) t18-none (t18-cons (T17 X) (T18 X))) +;; X should be inferred to be covariant in both (T17 X) and (T18 X). +;; This is similar to an arbitrary-arity tree type. + +;; This checks that X is covariant within (T17 X). +(define (t17-none* → (T17 X)) (t18 t18-none)) +(define (t17-none** → (→ (T17 X))) (inst t17-none* X)) +(check-type (t17-none**) : (→/test (T17 X))) +;; This checks that X is covariant within (T18 X). +(define (t18-none* → (T18 X)) t18-none) +(define (t18-none** → (→ (T18 X))) (inst t18-none* X)) +(check-type (t18-none**) : (→/test (T18 X))) + +;; This checks that X is not contravariant within (T17 X), +;; by checking that X is not covariant within (→ (T17 X) Int). +(define (t17->int [t17 : (T17 X)] → Int) 0) +(define (t17->int* → (→ (T17 X) Int)) (inst t17->int X)) +(typecheck-fail (t17->int*)) +;; This checks that X is not contravariant within (T18 X), +;; by checking that X is not covariant within (→ (T18 X) Int). +(define (t18->int [t18 : (T18 X)] → Int) 0) +(define (t18->int* → (→ (T18 X) Int)) (inst t18->int X)) +(typecheck-fail (t18->int*)) + diff --git a/macrotypes/examples/tests/mlish/inst.mlish b/macrotypes/examples/tests/mlish/inst.mlish new file mode 100644 index 0000000..8a9605b --- /dev/null +++ b/macrotypes/examples/tests/mlish/inst.mlish @@ -0,0 +1,74 @@ +#lang s-exp "../../mlish.rkt" +(require "../rackunit-typechecking.rkt") + +;; tests for instantiation of polymorphic functions and constructors + +(define-type (Result A B) + (Ok A) + (Error B)) + +(define (ok [a : A] -> (Result A B)) + (Ok a)) + +(check-type ok : (→/test A (Result A B))) ; test inferred +(check-type (inst ok Int String) : (→/test Int (Result Int String))) + +(define (f -> (Result Int String)) + (ok 1)) + +(check-type f : (→/test (Result Int String))) + +(define (g -> (Result Int String)) + (Ok 1)) + +(check-type g : (→/test (Result Int String))) + +(define (h -> (Result Int Y)) + (Ok 1)) + +(check-type h : (→/test (Result Int Y))) + +(define (i -> (Result Int String)) + (h)) + +(check-type i : (→/test (Result Int String))) + +(define (f/cond [b : Bool] -> (Result Int String)) + (cond [b (ok 1)] + [else (ok 0)])) + +(check-type f/cond : (→/test Bool (Result Int String))) + +(define-type-alias (Read-Result A) (Result (× A (List Char)) String)) + +(define (alias-test -> (Read-Result A)) + (Error "asd")) + +(check-type alias-test : (→/test (Result (× A (List Char)) String))) +(check-type alias-test : (→/test (Read-Result A))) + +(define (alias-test2 [in : A] -> (Read-Result A)) + (ok (tup in nil))) +(define (alias-test3 [in : A] -> (Read-Result A)) + (ok (tup in (list #\a #\b #\c)))) + +(check-type alias-test2 : (→/test A (Result (× A (List Char)) String))) +(check-type alias-test2 : (→/test A (Read-Result A))) +(check-type alias-test3 : (→/test A (Result (× A (List Char)) String))) +(check-type alias-test3 : (→/test A (Read-Result A))) + +(check-type alias-test2 : (→/test B (Result (× B (List Char)) String))) +(check-type alias-test2 : (→/test B (Read-Result B))) +(check-type alias-test3 : (→/test B (Result (× B (List Char)) String))) +(check-type alias-test3 : (→/test B (Read-Result B))) + +(define (expect-listof-int [loi : (List Int)] → Int) + 0) + +(check-type (expect-listof-int nil) : Int -> 0) + +(define (expect-→listof-int [f : (→ (List Int))] → Int) + 0) + +(check-type (expect-→listof-int (λ () nil)) : Int -> 0) + diff --git a/macrotypes/examples/tests/mlish/knuc.mlish b/macrotypes/examples/tests/mlish/knuc.mlish new file mode 100644 index 0000000..a334274 --- /dev/null +++ b/macrotypes/examples/tests/mlish/knuc.mlish @@ -0,0 +1,67 @@ +#lang s-exp "../../mlish.rkt" +(require "../rackunit-typechecking.rkt") + +(require-typed mk-fasta #:from "fasta.mlish") + +(define (all-counts [len : Int] [dna : String] -> (Hash String (Ref Int))) + (let ([table (hash {String (Ref Int)})]) + (for ([s (in-range (- (string-length dna) len) -1 -1)]) + (let ([key (make-string len)]) + (string-copy! key 0 dna s (+ s len)) + (let* ([b (if (hash-has-key? table key) + (hash-ref table key) + (let ([b (ref 0)]) + (hash-set! table key b) + b))]) + (:= b (add1 (deref b)))))) + table)) + + +(define dna + (let* ([in (mk-fasta 100000)] + ;; Skip to ">THREE ..." + [rst + (head (tail + (regexp-match + (regexp ">THREE Homo sapiens frequency\n(.*)$") + in)))]) + (let ([s (open-output-string)]) + ;; Copy everything but newlines to s: + (for ([l (in-lines rst)]) + (write-string l s)) + ;; Extract the string from s: + (string-upcase (get-output-string s))))) + +(check-type dna : String) + +;; 1-nucleotide counts: +(define counts1 (all-counts 1 dna)) + +(check-type counts1 : (Hash String (Ref Int))) + +(check-type (hash-count counts1) : Int -> 4) + +;; 2-nucleotide counts: +(define counts2 (all-counts 2 dna)) + +(check-type counts2 : (Hash String (Ref Int))) + +(check-type (hash-count counts2) : Int -> 16) + +;; 2-nucleotide counts: +(define counts3 (all-counts 3 dna)) + +(check-type counts3 : (Hash String (Ref Int))) + +(check-type (hash-count counts3) : Int -> 64) + +;; Specific sequences: +(check-type + (for/list ([seq (in-list (list "GGT" "GGTA" "GGTATT" + "GGTATTTTAATT" "GGTATTTTAATTTATAGT"))]) + (let ([table (all-counts (string-length seq) dna)]) + (if (hash-has-key? table seq) + (deref (hash-ref table seq)) + 0))) + : (List Int) + -> (list 5861 1776 176 0 0)) diff --git a/macrotypes/examples/tests/mlish/listpats.mlish b/macrotypes/examples/tests/mlish/listpats.mlish new file mode 100644 index 0000000..a68e3b6 --- /dev/null +++ b/macrotypes/examples/tests/mlish/listpats.mlish @@ -0,0 +1,70 @@ +#lang s-exp "../../mlish.rkt" +(require "../rackunit-typechecking.rkt") + +;; pattern matching for built-in lists + +(check-type + (match (list 1 2) with + [[] -> 0] + [[x y] -> (+ x y)]) : Int -> 3) + +(typecheck-fail + (match (list 1 2) with + [[x y] -> (+ x y)]) #:with-msg "missing empty list case") + +(typecheck-fail + (match (list 1 2) with + [[] -> 0]) #:with-msg "missing non\\-empty list case") + +(check-type + (match (list 1 2) with + [[] -> 0] + [[x y] -> (+ x y)]) : Int -> 3) + +(check-type + (match (list 1 2) with + [[x y] -> (+ x y)] + [[] -> 0]) : Int -> 3) + +(check-type + (match (nil {Int}) with + [[x y] -> (+ x y)] + [[] -> 0]) : Int -> 0) + +(check-type + (match (list 1 2 3) with + [[] -> nil] + [x :: rst -> rst]) : (List Int) -> (list 2 3)) + +(check-type + (match (list 1 2 3) with + [[] -> nil] + [x :: y :: rst -> rst]) : (List Int) -> (list 3)) + +(check-type + (match (nil {Int}) with + [[] -> nil] + [x :: y :: rst -> rst]) : (List Int) -> nil) + +(check-type + (match (list 1 2 3) with + [[] -> 0] + [x :: y :: rst -> (+ x y)]) : Int -> 3) + +(check-type + (match (list 1 2 3) with + [[] -> 0] + [[x] -> 2] + [x :: rst -> 3]) : Int -> 3) + +(check-type + (match (list 1) with + [[] -> 0] + [[x] -> 2] + [x :: rst -> 3]) : Int -> 2) + +(check-type + (match (list 1) with + [[] -> 0] + [x :: rst -> 3] + [[x] -> 2]) : Int -> 3) diff --git a/macrotypes/examples/tests/mlish/loop.mlish b/macrotypes/examples/tests/mlish/loop.mlish new file mode 100644 index 0000000..7392832 --- /dev/null +++ b/macrotypes/examples/tests/mlish/loop.mlish @@ -0,0 +1,121 @@ +#lang s-exp "../../mlish.rkt" +(require "../rackunit-typechecking.rkt") + +;; datatype with no self-reference +(define-type (Test X) + (A X) + (B X X)) + +(typecheck-fail + (define-type (Test2 X) + (AA (Test2 X X))) + #:with-msg "Improper use of constructor Test2; expected 1 args, got 2") + +(typecheck-fail + (define-type (Test3 X) + (AA (→))) + #:with-msg "Improper usage of type constructor →") + +(typecheck-fail + (define-type (Test4 X) + (AA (+ 1 2))) + #:with-msg "\\(\\+ 1 2\\) is not a valid type") + +(check-type (A 1) : (Test Int)) +(check-type (B 1 2) : (Test Int)) + +(check-type + (match (A 1) with + [A x -> x] + [B x y -> (+ x y)]) : Int -> 1) + +(check-type + (match (B 1 2) with + [A x -> x] + [B x y -> (+ x y)]) : Int -> 3) + +;; datatype with self-reference +(define-type (Rec X) + N + (C X (Rec X))) + +; check inferred and explicit instantiation versions +(check-type N : (Rec Int) -> N) +(check-type (N {Int}) : (Rec Int) -> (N {Int})) +(check-type (C 1 N) : (Rec Int) -> (C 1 N)) + +(check-type + (match (N {Int}) with + [N -> 0] + [C x xs -> x]) : Int -> 0) + +(check-type + (match (C 1 N) with + [N -> 0] + [C x xs -> x]) : Int -> 1) + +;; mutually referential datatypes +(define-type (Loop1 X) + (L1 (Loop2 X))) +(define-type (Loop2 X) + (L2 (Loop1 X))) + +(define (looping-f [x : (Loop1 Y)] -> (Loop1 Y)) x) + +(define-type (ListA X) + NA + (CA X (ListB X))) +(define-type (ListB X) + NB + (CB X (ListA X))) + +(typecheck-fail + (define-type (ListC X) + NC + (CC X (ListA X X))) + #:with-msg + "Improper usage of type constructor ListA: \\(ListA X X\\), expected = 1 arguments") + +(typecheck-fail (CA 1 NA)) +(check-type (CA 1 NB) : (ListA Int)) +(check-type (CA 1 (CB 2 NA)) : (ListA Int)) +(typecheck-fail (CA 1 (CB 2 NB))) +(typecheck-fail (CB 1 NB)) +(check-type (CB 1 NA) : (ListB Int)) +(check-type (CB 1 (CA 2 NB)) : (ListB Int)) +(typecheck-fail (CB 1 (CA 2 NA))) + +(check-type + (match (CA 1 NB) with + [NA -> 0] + [CA x xs -> x]) : Int -> 1) + +(check-type + (match (CA 1 (CB 2 NA)) with + [NA -> 0] + [CA x xs -> + (match xs with + [NB -> 3] + [CB x xs -> x])]) : Int -> 2) + +;; "real world" mutually referential datatypes +(define-type (BankersDeque A) + [BD Int (List A) Int (List A)]) + +(define-type (ImplicitCatDeque A) + [Shallow (BankersDeque A)] + [Deep (BankersDeque A) + (ImplicitCatDeque (BankersDeque (CmpdElem (BankersDeque A)))) + (BankersDeque A) + (ImplicitCatDeque (BankersDeque (CmpdElem (BankersDeque A)))) + (BankersDeque A)]) + +(define-type (CmpdElem A) + [Simple (BankersDeque A)] + [Cmpd (BankersDeque A) + (ImplicitCatDeque + (BankersDeque (CmpdElem (BankersDeque A)))) (BankersDeque A)]) + +(define (id (icd : (ImplicitCatDeque Int)) → (ImplicitCatDeque Int)) + icd) + diff --git a/macrotypes/examples/tests/mlish/match2.mlish b/macrotypes/examples/tests/mlish/match2.mlish new file mode 100644 index 0000000..96b3835 --- /dev/null +++ b/macrotypes/examples/tests/mlish/match2.mlish @@ -0,0 +1,298 @@ +#lang s-exp "../../mlish.rkt" +(require "../rackunit-typechecking.rkt") + +;; alternate match that supports nested patterns + +(define-type (Test X) + (A X) + (B (× X X)) + (C (× X (× X X)))) + +(typecheck-fail + (match2 (B (tup 2 3)) with + [B x -> x]) + #:with-msg "clauses not exhaustive; missing: A, C") + +(typecheck-fail + (match2 (B (tup 2 3)) with + [A x -> x] + [C (x,y) -> y] + [B x -> x]) #:with-msg "branches have incompatible types: Int and \\(× Int Int\\)") + +(typecheck-fail + (match2 (B (tup 2 3)) with + [A x -> (tup x x)] + [C x -> x] + [B x -> x]) + #:with-msg "branches have incompatible types: \\(× Int Int\\) and \\(× Int \\(× Int Int\\)\\)") + +(check-type + (match2 (B (tup 2 3)) with + [A x -> (tup x x)] + [C (x,y) -> y] + [B x -> x]) : (× Int Int) -> (list 2 3)) + +(typecheck-fail + (match2 (A (tup 2 3)) with + [A x -> x]) #:with-msg "clauses not exhaustive; missing: B, C") + +(check-type + (match2 (A (tup 2 3)) with + [B (x,y) -> y] + [C (x,y) -> x] + [A x -> x]) : (× Int Int) -> (list 2 3)) + +(check-type + (match2 (A (tup 2 3)) with + [B (x,y) -> y] + [A x -> x] + [C (x,y) -> x]) : (× Int Int) -> (list 2 3)) + +(typecheck-fail + (match2 (A (tup 2 3)) with + [B (x,y) -> y] + [A x -> x] + [C x -> x]) #:with-msg "branches have incompatible types") + +(check-type + (match2 (A 1) with + [A x -> x] + [_ -> -1]) : Int -> 1) + +(typecheck-fail + (match2 (B 1) with + [B x -> x]) + #:with-msg "expected: \\(× X X\\)\n *given: Int") + +(check-type + (match2 (B (tup 2 3)) with + [B (tup x y) -> (+ x y)] + [_ -> -1]) : Int -> 5) + +(check-type + (match2 (C (tup 2 (tup 3 4))) with + [C (tup x (tup y z)) -> (+ x (+ y z))] + [_ -> -1]) : Int -> 9) + +(check-type + (match2 (C (tup 2 (tup 3 4))) with + [A x -> x] + [_ -> 100]) : Int -> 100) + + + +;; lists + +(typecheck-fail + (match2 (list 1) with + [list x -> x]) #:with-msg "missing nil clause") + +(typecheck-fail + (match2 (list 1) with + [nil -> 0] + [list x -> x]) + #:with-msg "missing clause for non-empty, arbitrary length list") + +(check-type + (match2 (list 1) with + [nil -> 0] + [x :: xs -> x]) : Int -> 1) + +(check-type + (match2 (list 1) with + [nil -> 0] + [list x -> x] + [x :: xs -> x]) : Int -> 1) + +(check-type + (match2 (list 1) with + [list -> 0] + [list x -> x] + [x :: xs -> x]) : Int -> 1) + +(check-type + (match2 (list 1) with + [list x -> x] + [_ -> 0]) : Int -> 1) + +(check-type + (match2 (list 1) with + [x :: xs -> x] + [nil -> 0]) : Int -> 1) + +(check-type + (match2 (list 1) with + [_ -> -1] + [list x -> x] + [nil -> 0]) : Int -> -1) + +(check-type + (match2 (list 1) with + [_ -> -1] + [list x -> x] + [list -> 0]) : Int -> -1) + +(check-type + (match2 (list 1) with + [_ -> 0]) : Int -> 0) + +(typecheck-fail + (match2 (list 1) with + [nil -> 0]) + #:with-msg "missing clause for non-empty, arbitrary length list") + +(check-type + (match2 (list 1 2) with + [list x y -> (+ x y)] + [_ -> 0]) : Int -> 3) + +(check-type + (match2 (list 1 2) with + [list -> 0] + [list x y -> (+ x y)] + [_ -> -1]) : Int -> 3) + +(check-type + (match2 (list (list 3 4) (list 5 6)) with + [list -> 0] + [list (list w x) (list y z) -> (+ (+ x y) (+ z w))] + [_ -> -1]) : Int -> 18) + +(check-type + (match2 (list (tup 3 4) (tup 5 6)) with + [list -> 0] + [list (tup w x) (tup y z) -> (+ (+ x y) (+ z w))] + [_ -> -1]) : Int -> 18) + +(check-type + (match2 (nil {Int}) with + [nil -> 0] + [list x y -> (+ x y)] + [_ -> -1]) : Int -> 0) + +(check-type + (match2 (list 1 2) with + [nil -> 0] + [list x y -> (+ x y)] + [_ -> -1]) : Int -> 3) + +(check-type + (match2 (list 1 2 3) with + [nil -> 0] + [list x y -> (+ x y)] + [_ -> -1]) : Int -> -1) + +;; 0-arity constructors +(define-type (Test2 X) + AA + (BB X)) + +(check-type + (match2 (BB 1) with + [AA -> 0] + [BB x -> x]) : Int -> 1) + +(check-type + (match2 (BB (AA {Int})) with + [AA -> 0] + [BB AA -> 1] + [_ -> 2]) : Int -> 1) + +;; drop parens around 0-arity constructors +(check-type + (match2 (BB 1) with + [AA -> 0] + [BB x -> x]) : Int -> 1) + +(check-type + (match2 (BB (AA {Int})) with + [AA -> 0] + [BB AA -> 1] + [_ -> 2]) : Int -> 1) + +;; nicer cons pattern syntax (::) +(check-type + (match2 (list 1 2) with + [nil -> -1] + [x :: xs -> x]) + : Int -> 1) + +(check-type + (match2 (list 1 2) with + [nil -> -1] + [x :: y :: xs -> y]) : Int -> 2) + +(check-type + (match2 (list (tup 1 2) (tup 3 4)) with + [nil -> -1] + [(tup x y) :: (tup a b) :: xs -> (+ a b)]) : Int -> 7) + +(check-type + (match2 (list (list 2 3 4) (list 5 6 7) (list 9 10)) with + [nil -> -1] + [x :: (y :: z :: zs) :: xs -> z]) : Int -> 6) + +(check-type + (match2 (list (list 2 3 4) (list 5 6 7) (list 9 10)) with + [nil -> -1] + [x :: (list a b c) :: xs -> c]) : Int -> 7) + +(typecheck-fail + (match2 (list (list #t #f)) with + [nil -> -1] + [(list x y) :: tl -> (+ x y)]) + #:with-msg "expected: Int\n *given: Bool") + +;; comma tup pattern syntax + +(check-type + (match2 (tup 1 2) with + [(x,y) -> (+ x y)]) : Int -> 3) + +(check-type + (match2 (tup 1 2 4) with + [(_,y,z) -> (+ z y)]) : Int -> 6) + +(check-type + (match2 (list (tup 1 2) (tup 3 4) (tup 5 6)) with + [(x,y) :: (a,b) :: rst -> (+ y a)] + [_ -> -1]) : Int -> 5) + +(check-type + (match2 (list (tup (BB 1) (AA {Int})) (tup (BB 2) (AA {Int}))) with + [((BB x),AA) :: ((BB y),AA) :: rst -> (+ y x)] + [_ -> -1]) : Int -> 3) + +(check-type + (match2 (tup (tup (tup 1 2) (tup 3)) (tup 4 (tup 6 7))) with + [(((x,y),z),(a,(b,c))) -> (+ c y)]) : Int -> 9) + +(check-type + (match2 (tup (tup (tup 1 2) (tup 3)) (tup 4 (tup 6 7))) with + [(((x,y),z),(_,(_,c))) -> (+ c y)]) : Int -> 9) + +(check-type + (match2 (tup (tup (tup 1 2) (tup 3)) (tup 4 (tup 6 7))) with + [(((_,y),_),(_,(_,c))) -> (+ c y)]) : Int -> 9) + +(typecheck-fail + (match2 (tup (BB 1) (BB 2)) with + [((BB x),(BB y)) -> (+ x y)]) + #:with-msg "clauses not exhaustive; missing: AA") + +;; TODO: should tail +#;(typecheck-fail + (match2 (tup (BB 1) (BB 2)) with + [((BB x),(BB y)) -> (+ x y)] + [(AA,AA) -> 0]) + #:with-msg "clauses not exhaustive; missing: AA") + +;; falls off; runtime match exception +#;(match2 (tup (BB 2) (AA {Int})) with + [((BB x),(BB y)) -> (+ x y)] + [(AA,AA) -> 0]) + +(check-type + (match2 (tup (BB 1) (BB 2)) with + [((BB x),(BB y)) -> (+ x y)] + [_ -> -1]) : Int -> 3) diff --git a/macrotypes/examples/tests/mlish/matrix.mlish b/macrotypes/examples/tests/mlish/matrix.mlish new file mode 100644 index 0000000..8bd6871 --- /dev/null +++ b/macrotypes/examples/tests/mlish/matrix.mlish @@ -0,0 +1,73 @@ +#lang s-exp "../../mlish.rkt" +(require "../rackunit-typechecking.rkt") + +(define-type-alias Matrix (Vector (Vector Int))) + +(define size 30) + +(define (vector-map [f : (→ X Y)] [v : (Vector X)] -> (Vector Y)) + (for/vector ([x (in-vector v)]) (f x))) + +(define (mkmatrix [rows : Int] [cols : Int] -> Matrix) + (for/vector ([i (in-range rows)] + [count (in-range 1 (* rows cols) cols)]) + (for/vector ([j (in-range cols)] + [x (in-naturals count)]) + x))) + +(check-type (mkmatrix 3 4) : Matrix + -> (vector (vector 1 2 3 4) + (vector 5 6 7 8) + (vector 9 10 11 12))) + +(check-type (mkmatrix 3 3) + : Matrix + -> (vector (vector 1 2 3) + (vector 4 5 6) + (vector 7 8 9))) + +(check-type (mkmatrix 4 3) + : Matrix + -> (vector (vector 1 2 3) + (vector 4 5 6) + (vector 7 8 9) + (vector 10 11 12))) + +(define (num-cols [mx : Matrix] -> Int) + (let ((row (vector-ref mx 0))) + (vector-length row))) + +(define (num-rows [mx : Matrix] -> Int) + (vector-length mx)) + +(define (vec-mult [v1 : (Vector Int)] [v2 : (Vector Int)] -> Int) + (for/sum ([x (in-vector v1)] + [y (in-vector v2)]) + (* x y))) + +(define (mmult [m1 : Matrix] [m2 : Matrix] -> Matrix) + (for/vector ([row (in-vector m1)]) + (for/vector ([col-num (in-range (num-cols m2))]) + (let ([col + (vector-map + (λ ([r : (Vector Int)]) (vector-ref r col-num)) + m2)]) + (vec-mult row col))))) + +(check-type (mmult (mkmatrix 3 3) (mkmatrix 3 3)) + : Matrix + -> (vector (vector 30 36 42) + (vector 66 81 96) + (vector 102 126 150))) + +(check-type (mmult (mkmatrix 2 3) (mkmatrix 3 2)) + : Matrix + -> (vector (vector 22 28) + (vector 49 64))) + +(check-type (mmult (mkmatrix 4 3) (mkmatrix 3 4)) + : Matrix + -> (vector (vector 38 44 50 56) + (vector 83 98 113 128) + (vector 128 152 176 200) + (vector 173 206 239 272))) diff --git a/macrotypes/examples/tests/mlish/nbody.mlish b/macrotypes/examples/tests/mlish/nbody.mlish new file mode 100644 index 0000000..d5dcdc9 --- /dev/null +++ b/macrotypes/examples/tests/mlish/nbody.mlish @@ -0,0 +1,185 @@ +#lang s-exp "../../mlish.rkt" +(require "../rackunit-typechecking.rkt") + +(define +pi+ 3.141592653589793) + +(check-type +pi+ : Float) + +(define +days-per-year+ 365.24) + +(define * fl*) + +(define +solar-mass+ (* 4.0 (* +pi+ +pi+))) + +(check-type +solar-mass+ : Float) + +(define +dt+ 0.01) + +(define-type Body (body Float ; x + Float ; y + Float ; z + Float ; vx + Float ; vy + Float ; vz + Float ; mass + )) + +(define *sun* + (body 0.0 0.0 0.0 0.0 0.0 0.0 +solar-mass+)) + +(define *jupiter* + (body 4.84143144246472090 + -1.16032004402742839 + -1.03622044471123109e-1 + (* 1.66007664274403694e-3 +days-per-year+) + (* 7.69901118419740425e-3 +days-per-year+) + (* -6.90460016972063023e-5 +days-per-year+) + (* 9.54791938424326609e-4 +solar-mass+))) + +(define *saturn* + (body 8.34336671824457987 + 4.12479856412430479 + -4.03523417114321381e-1 + (* -2.76742510726862411e-3 +days-per-year+) + (* 4.99852801234917238e-3 +days-per-year+) + (* 2.30417297573763929e-5 +days-per-year+) + (* 2.85885980666130812e-4 +solar-mass+))) + +(define *uranus* + (body 1.28943695621391310e1 + -1.51111514016986312e1 + -2.23307578892655734e-1 + (* 2.96460137564761618e-03 +days-per-year+) + (* 2.37847173959480950e-03 +days-per-year+) + (* -2.96589568540237556e-05 +days-per-year+) + (* 4.36624404335156298e-05 +solar-mass+))) + +(define *neptune* + (body 1.53796971148509165e+01 + -2.59193146099879641e+01 + 1.79258772950371181e-01 + (* 2.68067772490389322e-03 +days-per-year+) + (* 1.62824170038242295e-03 +days-per-year+) + (* -9.51592254519715870e-05 +days-per-year+) + (* 5.15138902046611451e-05 +solar-mass+))) + +(define *system* (list *sun* *jupiter* *saturn* *uranus* *neptune*)) + +(check-type *system* : (List Body)) + +(define (offset-momentum -> Unit) + (let loop-i : Unit + ([i *system*] [px 0.0] [py 0.0] [pz 0.0]) + (cond + [(isnil i) + (match (head *system*) with ; sun + [body x y z vx vy vz m -> + (let ([new + (body x y z + (fl/ (fl- 0.0 px) +solar-mass+) + (fl/ (fl- 0.0 py) +solar-mass+) + (fl/ (fl- 0.0 pz) +solar-mass+) + m)]) + (set! *system* (cons new (tail *system*))))])] + [else + (match (head i) with + [body x y z vx vy vz m -> + (loop-i (tail i) + (fl+ px (fl* vx m)) + (fl+ py (fl* vy m)) + (fl+ pz (fl* vz m)))])]))) + +(define (energy [o : (List Body)] -> Float) + (let loop-o : Float ([o o] [e 0.0]) + (cond + [(isnil o) e] + [else + (match (head o) with + [body x y z vx vy vz m -> + (let* ([e (fl+ e (fl* 0.5 + (fl* m + (fl+ (fl+ (fl* vx vx) + (fl* vy vy)) + (fl* vz vz)))))]) + (let loop-i : Float ([i (tail o)] [e e]) + (if (isnil i) + (loop-o (tail o) e) + (match (head i) with + [body x2 y2 z2 vx2 vy2 vz2 m2 -> + (let* ([dx (fl- x x2)] + [dy (fl- y y2)] + [dz (fl- z z2)] + [dist (flsqrt (fl+ (fl+ (fl* dx dx) (fl* dy dy)) + (fl* dz dz)))] + [e (fl- e (fl/ (fl* m m2) dist))]) + (loop-i (tail i) e))]))))])]))) + +(define (advance [bs : (List Body)] -> (List Body)) + (if (isnil bs) + bs + (let ([new (advance2 bs)]) + (cons (head new) (advance (tail new)))))) +;; bs is non-null +(define (advance2 [bs : (List Body)] -> (List Body)) + (match (head bs) with + [body o1x o1y o1z vx vy vz om -> + (let loop-i : (List Body) + ([i (tail bs)] [res (nil {Body})] [vx vx] [vy vy] [vz vz]) + (cond + [(isnil i) + (cons + (body + (fl+ o1x (fl* +dt+ vx)) + (fl+ o1y (fl* +dt+ vy)) + (fl+ o1z (fl* +dt+ vz)) + vx vy vz om) + (reverse res))] + [else + (match (head i) with + [body i1x i1y i1z i1vx i1vy i1vz im -> + (let* ([dx (fl- o1x i1x)] + [dy (fl- o1y i1y)] + [dz (fl- o1z i1z)] + [dist2 (fl+ (fl+ (fl* dx dx) (fl* dy dy)) (fl* dz dz))] + [mag (fl/ +dt+ (fl* dist2 (flsqrt dist2)))] + [dxmag (fl* dx mag)] + [dymag (fl* dy mag)] + [dzmag (fl* dz mag)]) + (loop-i + (tail i) + (cons (body i1x i1y i1z + (fl+ i1vx (fl* dxmag om)) + (fl+ i1vy (fl* dymag om)) + (fl+ i1vz (fl* dzmag om)) + im) res) + (fl- vx (fl* dxmag im)) + (fl- vy (fl* dymag im)) + (fl- vz (fl* dzmag im))))])]))])) + +(check-type (real->decimal-string (energy *system*) 9) + : String -> "-0.169289903") + +(offset-momentum) + +(check-type (real->decimal-string (energy *system*) 9) + : String -> "-0.169075164") + +(check-type + (real->decimal-string + (energy (advance *system*)) + 9) + : String -> "-0.169074954") + +(check-type + (real->decimal-string + (energy (advance (advance *system*))) 9) + : String -> "-0.169074743") + +(check-type + (real->decimal-string + (energy + (for/fold ([bs *system*]) + ([i (in-range 10)]) + (advance bs))) + 9) + : String -> "-0.169073022") diff --git a/macrotypes/examples/tests/mlish/polyrecur.mlish b/macrotypes/examples/tests/mlish/polyrecur.mlish new file mode 100644 index 0000000..8854b72 --- /dev/null +++ b/macrotypes/examples/tests/mlish/polyrecur.mlish @@ -0,0 +1,117 @@ +#lang s-exp "../../mlish.rkt" +(require "../rackunit-typechecking.rkt") + +;; tests of polymorphic recursion + +;; polymorphic recursion of functions +(define (polyf [lst : (List X)] -> (List X)) + (let ([x (polyf (list 1 2 3))] + [y (polyf (list #t #f))]) + (polyf lst))) + +;; polymorphic recursive type +;; from okasaki, ch10 +(define-type (Seq X) + Nil + (Cons X (Seq (× X X)))) + +(define (size [s : (Seq X)] -> Int) + (match s with + [Nil -> 0] + [Cons x ps -> (add1 (* 2 (size ps)))])) + +(check-type (size (Nil {Int})) : Int -> 0) +(check-type (size (Cons 1 Nil)) : Int -> 1) +(check-type (size (Cons 1 (Cons (tup 2 3) Nil))) : Int -> 3) +(check-type + (size (Cons 1 (Cons (tup 2 3) (Cons (tup (tup 4 5) (tup 6 7)) Nil)))) + : Int -> 7) + +;; implicit queue +(define-type (Digit X) + (Zero) + (One X) + (Two X X)) + +(define-type (ImplicitQueue X) + [Shallow (d : (Digit X))] + [Deep (f : (Digit X)) + (m : (ImplicitQueue (× X X))) + (r : (Digit X))]) + +(define (empty -> (ImplicitQueue X)) + (Shallow (Zero))) + +(define (iq-isEmpty [iq : (ImplicitQueue A)] → Bool) + (match iq with + [Shallow d -> + (match d with + [Zero -> #t] + [One x -> #f] + [Two x y -> #f])] + [Deep a b c -> #f])) + +(define (iq-snoc [iq : (ImplicitQueue A)] [y : A] → (ImplicitQueue A)) + (match iq with + [Shallow d -> + (match d with + [Zero -> (Shallow (One y))] + [One x -> (Deep (Two x y) (empty) Zero)] + [Two x y -> (empty)])] ;; Error + [Deep f m d -> + (match d with + [Zero -> (Deep f m (One y))] + [One x -> (Deep f (iq-snoc m (tup x y)) Zero)] + [Two x y -> (empty)])])) ; Error + +(check-type (iq-isEmpty (Shallow (Zero {Int}))) : Bool -> #t) + +(check-type (iq-isEmpty (iq-snoc (Shallow (Zero {Int})) 5)) : Bool -> #f) + +;; example from: +;; blogs.janestreet.com/ensuring-that-a-function-is-polymorphic-in-ocaml-3-12 + +(define-type (PerfectTree X) + (Leaf X) + (Node X (PerfectTree (× X X)))) +(define (flatten [t : (PerfectTree X)] -> (List X)) + (match t with + [Leaf x -> (list x)] + [Node x rst -> + (cons x + (for/fold ([acc nil]) ([p (in-list (flatten rst))]) + (match p with + [x y -> (cons x (cons y acc))])))])) + +(check-type (flatten (Leaf 1)) : (List Int) -> (list 1)) +(check-type (flatten (Node 1 (Leaf (tup 2 3)))) : (List Int) -> (list 1 2 3)) +(check-type + (flatten (Node 1 (Node (tup 2 3) (Leaf (tup (tup 4 5) (tup 6 7)))))) + : (List Int) -> (list 1 6 7 4 5 2 3)) + + +;; catch type constructor arity error; should not loop +(define-type (BankersDeque A) + [BD Int (List A) Int (List A)]) + +(typecheck-fail + (define-type (ImplicitCatDeque A) + [Shall (BankersDeque A)] + [Dp (BankersDeque A) + (ImplicitCatDeque (BankersDeque A) (CmpdElem (BankersDeque A))) + (BankersDeque A) + (ImplicitCatDeque (BankersDeque A) (CmpdElem (BankersDeque A))) + (BankersDeque A)]) + #:with-msg "Improper use of constructor ImplicitCatDeque; expected 1 args, got 2") + +#;(define-type (CmpdElem A) + [Simple (BankersDeque A)] + [Cmpd (BankersDeque A) + (ImplicitCatDeque (BankersDeque (CmpdElem (BankersDeque A)))) + (BankersDeque A)]) + + +#;(typecheck-fail + (λ ([icd : (ImplicitCatDeque A)]) icd) + #:with-msg + "type constructor ImplicitCatDeque expects 1 args, given 2") diff --git a/macrotypes/examples/tests/mlish/queens.mlish b/macrotypes/examples/tests/mlish/queens.mlish new file mode 100644 index 0000000..d45b4b4 --- /dev/null +++ b/macrotypes/examples/tests/mlish/queens.mlish @@ -0,0 +1,186 @@ +#lang s-exp "../../mlish.rkt" +(require "../rackunit-typechecking.rkt") + +;; function polymorphic in list element +(define-type (List X) + Nil + (Cons X (List X))) + +(typecheck-fail + (match (Cons 1 Nil) with + [Nil -> 1]) + #:with-msg "clauses not exhaustive; missing\\: Cons") +(typecheck-fail + (match (Cons 1 Nil) with + [Cons x xs -> 1]) + #:with-msg "clauses not exhaustive; missing: Nil") + +;; list fns ---------- + +; map: tests whether match and define properly propagate 'expected-type +(define (map [f : (→ X Y)] [lst : (List X)] → (List Y)) + (match lst with + [Nil -> Nil] + [Cons x xs -> (Cons (f x) (map f xs))])) +(check-type map : (→/test (→ X Y) (List X) (List Y))) +(check-type map : (→/test {Y X} (→ Y X) (List Y) (List X))) +(check-type map : (→/test (→ A B) (List A) (List B))) +(check-not-type map : (→/test (→ A B) (List B) (List A))) +(check-not-type map : (→/test (→ X X) (List X) (List X))) ; only 1 bound tyvar + +; map: alt signature syntax +(define (map2 f lst) + : (→ X Y) (List X) → (List Y) + (match lst with + [Nil -> Nil] + [Cons x xs -> (Cons (f x) (map2 f xs))])) +(check-type map2 : (→/test (→ X Y) (List X) (List Y))) +(check-type map2 : (→/test {Y X} (→ Y X) (List Y) (List X))) +(check-type map2 : (→/test (→ A B) (List A) (List B))) +(check-not-type map2 : (→/test (→ A B) (List B) (List A))) +(check-not-type map2 : (→/test (→ X X) (List X) (List X))) ; only 1 bound tyvar + +; nil without annotation; tests fn-first, left-to-right arg inference +; does work yet, need to add left-to-right inference in #%app +(check-type (map add1 Nil) : (List Int) ⇒ Nil) +(check-type (map add1 (Cons 1 (Cons 2 (Cons 3 Nil)))) + : (List Int) ⇒ (Cons 2 (Cons 3 (Cons 4 Nil)))) +(typecheck-fail (map add1 (Cons "1" Nil)) + #:with-msg "expected: Int\n *given: String") +(check-type (map (λ ([x : Int]) (+ x 2)) (Cons 1 (Cons 2 (Cons 3 Nil)))) + : (List Int) ⇒ (Cons 3 (Cons 4 (Cons 5 Nil)))) +;; ; doesnt work yet: all lambdas need annotations +;; (check-type (map (λ (x) (+ x 2)) (list 1 2 3)) : (List Int) ⇒ (list 3 4 5)) + +(define (filter [p? : (→ X Bool)] [lst : (List X)] → (List X)) + (match lst with + [Nil -> Nil] + [Cons x xs -> (if (p? x) + (Cons x (filter p? xs)) + (filter p? xs))])) +(define (filter/guard [p? : (→ X Bool)] [lst : (List X)] → (List X)) + (match lst with + [Nil -> Nil] + [Cons x xs #:when (p? x) -> (Cons x (filter p? xs))] + [Cons x xs -> (filter p? xs)])) +(check-type (filter zero? Nil) : (List Int) ⇒ Nil) +(check-type (filter zero? (Cons 1 (Cons 2 (Cons 3 Nil)))) + : (List Int) ⇒ Nil) +(check-type (filter zero? (Cons 0 (Cons 1 (Cons 2 Nil)))) + : (List Int) ⇒ (Cons 0 Nil)) +(check-type + (filter + (λ ([x : Int]) (not (zero? x))) + (Cons 0 (Cons 1 (Cons 2 Nil)))) + : (List Int) ⇒ (Cons 1 (Cons 2 Nil))) +(check-type (filter/guard zero? Nil) : (List Int) ⇒ Nil) +(check-type (filter/guard zero? (Cons 1 (Cons 2 (Cons 3 Nil)))) + : (List Int) ⇒ Nil) +(check-type (filter/guard zero? (Cons 0 (Cons 1 (Cons 2 Nil)))) + : (List Int) ⇒ (Cons 0 Nil)) +(check-type + (filter/guard + (λ ([x : Int]) (not (zero? x))) + (Cons 0 (Cons 1 (Cons 2 Nil)))) + : (List Int) ⇒ (Cons 1 (Cons 2 Nil))) +; doesnt work yet: all lambdas need annotations +;(check-type (filter (λ (x) (not (zero? x))) (list 0 1 2)) : (List Int) ⇒ (list 1 2)) + +(define (foldr [f : (→ X Y Y)] [base : Y] [lst : (List X)] → Y) + (match lst with + [Nil -> base] + [Cons x xs -> (f x (foldr f base xs))])) +(define (foldl [f : (→ X Y Y)] [acc : Y] [lst : (List X)] → Y) + (match lst with + [Nil -> acc] + [Cons x xs -> (foldr f (f x acc) xs)])) + +(define (all? [p? : (→ X Bool)] [lst : (List X)] → Bool) + (match lst with + [Nil -> #t] + [Cons x xs #:when (p? x) -> (all? p? xs)] + [Cons x xs -> #f])) + +(define (tails [lst : (List X)] → (List (List X))) + (match lst with + [Nil -> (Cons Nil Nil)] + [Cons x xs -> (Cons lst (tails xs))])) + +(define (build-list [n : Int] [f : (→ Int X)] → (List X)) + (if (zero? (sub1 n)) + (Cons (f 0) Nil) + (Cons (f (sub1 n)) (build-list (sub1 n) f)))) + +(check-type (build-list 1 add1) + : (List Int) ⇒ (Cons 1 Nil)) +(check-type (build-list 3 add1) + : (List Int) ⇒ (Cons 3 (Cons 2 (Cons 1 Nil)))) +(check-type (build-list 5 sub1) + : (List Int) ⇒ (Cons 3 (Cons 2 (Cons 1 (Cons 0 (Cons -1 Nil)))))) + +;; map + filter + fold + build example +(define INPUT (build-list 1000 number->string)) +(check-type (foldl + 0 (filter even? (map string->number INPUT))) : Int -> 249500) + +(define (append [lst1 : (List X)] [lst2 : (List X)] → (List X)) + (match lst1 with + [Nil -> lst2] + [Cons x xs -> (Cons x (append xs lst2))])) + +;; n-queens -------------------- +(define-type Queen (Q Int Int)) + +(define (safe? [q1 : Queen] [q2 : Queen] → Bool) + (match q1 with + [Q x1 y1 -> + (match q2 with + [Q x2 y2 -> + (not (or (= x1 x2) + (= y1 y2) + (= (abs (- x1 x2)) + (abs (- y1 y2)))))])])) + +(define (safe/list? [qs : (List Queen)] → Bool) + (match qs with + [Nil -> #t] + [Cons q1 rst -> + (all? (λ ([q2 : Queen]) (safe? q1 q2)) rst)])) + +(define (valid? [lst : (List Queen)] → Bool) + (all? safe/list? (tails lst))) + +(define (nqueens [n : Int] → (List Queen)) + (let* ([process-row + (λ ([r : Int] + [all-possible-so-far : (List (List Queen))]) + (foldr + (λ ([qs : (List Queen)] + [new-qss : (List (List Queen))]) + (append + (map + (λ ([c : Int]) (Cons (Q r c) qs)) + (build-list n add1)) + new-qss)) + Nil + all-possible-so-far))] + [all-possible + (foldl process-row + (Cons Nil Nil) + (build-list n add1))]) + (let ([solns (filter valid? all-possible)]) + (match solns with + [Nil -> Nil] + [Cons x xs -> x])))) + +(check-type nqueens : (→ Int (List Queen))) +(check-type (nqueens 1) : (List Queen) ⇒ (Cons (Q 1 1) Nil)) +(check-type (nqueens 2) : (List Queen) ⇒ Nil) +(check-type (nqueens 3) : (List Queen) ⇒ Nil) +(check-type (nqueens 4) + : (List Queen) + ⇒ (Cons (Q 3 1) (Cons (Q 2 4) + (Cons (Q 1 2) (Cons (Q 4 3) Nil))))) +(check-type (nqueens 5) + : (List Queen) + ⇒ (Cons (Q 4 2) (Cons (Q 3 4) + (Cons (Q 2 1) (Cons (Q 1 3) (Cons (Q 5 5) Nil)))))) diff --git a/macrotypes/examples/tests/mlish/result.mlish b/macrotypes/examples/tests/mlish/result.mlish new file mode 100644 index 0000000..67153ce --- /dev/null +++ b/macrotypes/examples/tests/mlish/result.mlish @@ -0,0 +1,129 @@ +#lang s-exp "../../mlish.rkt" +(require "../rackunit-typechecking.rkt" "../../mlish-do.rkt") + +(define-type (Result A B) + (Ok A) + (Error B)) + +(define (ok [a : A] → (Result A B)) + (Ok a)) +(define (error [b : B] → (Result A B)) + (Error b)) + +(provide-type Result) +(provide ok) +(provide error) + +(check-type ok : (→/test A (Result A B))) +(check-type error : (→/test B (Result A B))) +(check-type (inst ok Int String) : (→ Int (Result Int String))) +(check-type (inst error String Int) : (→ String (Result Int String))) + +(check-type + (list (Ok 3) (Error "abject failure") (Ok 4)) + : (List (Result Int String)) + -> (list (Ok 3) (Error "abject failure") (Ok 4))) + +(define (result-bind [a : (Result A Er)] [f : (→ A (Result B Er))] + → (Result B Er)) + (match a with + [Ok v -> (f v)] + [Error er -> (Error er)])) + +(provide result-bind) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; read-tree, a function that parses a tree and uses the result monad. + +(require "trees.mlish") + +;; Parsing 42 in base 10: (rev-list->int 10 (list 2 4) 1 0) yields 42. +(define (rev-list->int [base : Int] [rev-list : (List Int)] [place : Int] [accum : Int] → Int) + (cond + [(isnil rev-list) accum] + [else (rev-list->int base + (tail rev-list) + (* base place) + (+ accum (* place (head rev-list))))])) + +(define (digit? [c : Char] → Bool) + (or (equal? c #\0) + (equal? c #\1) + (equal? c #\2) + (equal? c #\3) + (equal? c #\4) + (equal? c #\5) + (equal? c #\6) + (equal? c #\7) + (equal? c #\8) + (equal? c #\9))) + +(define (digit->int [c : Char] → Int) + (string->number (string c))) + +(define-type-alias (Read-Result A) (Result (× A (List Char)) String)) + +(define (read-int [str : (List Char)] [accum : (List Int)] → (Read-Result Int)) + (cond + [(isnil str) + (cond [(isnil accum) (error "expected an int, given nothing")] + [else (ok (tup (rev-list->int 10 accum 1 0) str))])] + [(digit? (head str)) + (read-int (tail str) (cons (digit->int (head str)) accum))] + [else + (ok (tup (rev-list->int 10 accum 1 0) str))])) + +(define (read-tree [str : (List Char)] → (Read-Result (Tree Int))) + (cond + [(isnil str) + (error "expected a tree of integers, given nothing")] + [(equal? (head str) #\( ) + (let ([do-ok (inst ok Unit String)] + [do-error (inst error String Unit)]) + (do result-bind + [tree1+str <- (read-tree (tail str))] + [(cond [(equal? (head (proj tree1+str 1)) #\space) + (do-ok (void))] + [else (do-error "expected a space")])] + [int+str <- (read-int (tail (proj tree1+str 1)) nil)] + [(cond [(equal? (head (proj int+str 1)) #\space) + (do-ok (void))] + [else (do-error "expected a space")])] + [tree2+str <- (read-tree (tail (proj int+str 1)))] + [(cond [(equal? (head (proj tree2+str 1)) #\) ) + (do-ok (void))] + [else (do-error "expected a `)`")])] + (ok + (tup (Node (proj tree1+str 0) + (proj int+str 0) + (proj tree2+str 0)) + (tail (proj tree2+str 1))))))] + [(digit? (head str)) + (do result-bind + [int+str <- (read-int str nil)] + (ok + (tup (Leaf (proj int+str 0)) + (proj int+str 1))))] + [else + (error "expected either a `(` or a digit")])) + +(check-type + (read-tree (string->list "42")) + : (Read-Result (Tree Int)) + -> (ok + (tup (Leaf 42) nil))) + +(check-type + (read-tree (string->list "x")) + : (Read-Result (Tree Int)) + -> (error + "expected either a `(` or a digit")) + +(check-type + (read-tree (string->list "(42 43 (44 45 46))")) + : (Read-Result (Tree Int)) + -> (ok + (tup (Node (Leaf 42) 43 (Node (Leaf 44) 45 (Leaf 46))) nil))) + + diff --git a/macrotypes/examples/tests/mlish/sweet-map.rkt b/macrotypes/examples/tests/mlish/sweet-map.rkt new file mode 100644 index 0000000..7d6321d --- /dev/null +++ b/macrotypes/examples/tests/mlish/sweet-map.rkt @@ -0,0 +1,20 @@ +#lang sweet-exp "../../mlish.rkt" + +define + sum [lst : (List Int)] → Int + match lst with + [] -> 0 + x :: xs -> + {x + sum(xs)} + +define + map [f : (→ X Y)] [lst : (List X)] → (List Y) + match lst with + [] -> nil + x :: xs -> + cons + f x + map f xs + +sum + map string->number (list "1" "2" "3") diff --git a/macrotypes/examples/tests/mlish/term.mlish b/macrotypes/examples/tests/mlish/term.mlish new file mode 100644 index 0000000..7c86e3d --- /dev/null +++ b/macrotypes/examples/tests/mlish/term.mlish @@ -0,0 +1,295 @@ +#lang s-exp "../../mlish.rkt" +(require "../rackunit-typechecking.rkt") + +;; from chap 6 of RW OCaml + +;; checks: +;; - nested recursive types (see expr) +;; - labeled adts +;; - records +;; - ho polymorphic fn argument + +(define-type BasicColor + Black + Red + Green + Yellow + Blue + Magenta + Cyan + White) + +(check-type Cyan : BasicColor) + +(check-type (list Blue Magenta Red) : (List BasicColor)) + +(define (basic-color->int [c : BasicColor] -> Int) + (match c with + [Black -> 0] [Red -> 1] [Green -> 2] [Yellow -> 3] + [Blue -> 4] [Magenta -> 5] [Cyan -> 6] [White -> 7])) + +(define (map [f : (→ X Y)] [lst : (List X)] -> (List Y)) + (if (isnil lst) + nil + (cons (f (head lst)) (map f (tail lst))))) + +(check-type (map basic-color->int (list Blue Red)) + : (List Int) -> (list 4 1)) + +(define (color-by-number [n : Int] [txt : String] -> String) + (format "\e[38;5;~am~a\e[0m" n txt)) + +(define blue + (color-by-number (basic-color->int Blue) "Blue")) + +(check-type blue : String -> "\e[38;5;4mBlue\e[0m") + +(printf "Hello ~a World!\n" blue) + +(define-type Weight Regular Bold) +(define-type Color + (Basic BasicColor Weight) + (RGB Int Int Int) + (Gray Int)) + +(check-type (list (RGB 250 70 70) (Basic Green Regular)) + : (List Color)) + +(define (color->int [c : Color] -> Int) + (match c with + [Basic bc w -> + (let ([base (match w with [Bold -> 8] [Regular -> 0])]) + (+ base (basic-color->int bc)))] + [RGB r g b -> + (+ 16 (+ b (+ (* g 6) (* r 36))))] + [Gray i -> (+ 232 i)])) + +(define (color-print [c : Color] [s : String] -> Unit) + (printf "~a\n" (color-by-number (color->int c) s))) + +(color-print (Basic Red Bold) "A bold red!") +(color-print (Gray 4) "A muted gray...") + +;; refactoring Color and Weight +(define-type NewColor + (NewBasic BasicColor) + (NewBold BasicColor) + (NewRGB Int Int Int) + (NewGray Int)) + +(typecheck-fail + (match (NewGray 1) with + [Basic bc w -> + (let ([base (match w with [Bold -> 8] [Regular -> 0])]) + (+ base (basic-color->int bc)))] + [RGB r g b -> + (+ 16 (+ b (+ (* g 6) (* r 36))))] + [Gray i -> (+ 232 i)]) + #:with-msg + "clauses not exhaustive; missing: NewGray, NewRGB, NewBold, NewBasic") + +(typecheck-fail + (match (NewGray 1) with + [NewBasic bc w -> + (let ([base (match w with [Bold -> 8] [Regular -> 0])]) + (+ base (basic-color->int bc)))] + [NewRGB r g b -> + (+ 16 (+ b (+ (* g 6) (* r 36))))] + [NewGray i -> (+ 232 i)]) + #:with-msg "clauses not exhaustive; missing: NewBold") + +(typecheck-fail + (match (NewGray 1) with + [NewBasic bc w -> + (let ([base (match w with [Bold -> 8] [Regular -> 0])]) + (+ base (basic-color->int bc)))] + [NewBold bc -> 1] + [NewRGB r g b -> + (+ 16 (+ b (+ (* g 6) (* r 36))))] + [NewGray i -> (+ 232 i)])) ; todo: better err msg for arity + +(check-type + (match (NewGray 1) with + [NewBasic bc -> (basic-color->int bc)] + [NewBold bc -> (+ 8 (basic-color->int bc))] + [NewRGB r g b -> + (+ 16 (+ b (+ (* g 6) (* r 36))))] + [NewGray i -> (+ 232 i)]) : Int) + +;; 2016-03-09: match currently does not support else +(define-type Details + (Logon [user : String] [credentials : String]) + (Heartbeat [status : String]) + (LogEntry [important? : Bool] [msg : String])) + +(define-type-alias SessionID String) +(define-type-alias Time String) +(define-type-alias Common (× SessionID Time)) + +(define-type-alias Msg (× Common Details)) + +(define (foldl [f : (→ X Y Y)] [init : Y] [lst : (List X)] -> Y) + (if (isnil lst) + init + (foldl f (f (head lst) init) (tail lst)))) + +(define (msgs-for-user [user : String] [msgs : (List Msg)] -> (List Msg)) + (match + (foldl + (λ ([m : Msg] [res : (× (List Msg) (List SessionID))]) + (match res with + [ms_out ids_out -> + (match m with + [common details -> + (match common with + [id t -> + (match details with + [Logon u c -> (if (string=? u user) + (tup (cons m ms_out) (cons id ids_out)) + res)] + [Heartbeat st -> (if (member id ids_out) + (tup (cons m ms_out) ids_out) + res)] + [LogEntry i? lmgs -> (if (member id ids_out) + (tup (cons m ms_out) ids_out) + res)])])])])) + (tup nil nil) + msgs) with + [msgs ids -> (reverse msgs)])) + +;; this is incomplete (and wrong, eg logentry has wrong arity) code in the book +(define (handle-msg [state : Int] [msg : Msg] -> String) + (match msg with + [common details -> + (match details with + [LogEntry i? lmsg -> lmsg] + [Logon u c -> u] + [Heartbeat s -> s])])) + +;; expr example +(define-type (Expr X) + (Base X) + (Const Bool) + (And (List (Expr X))) + (Or (List (Expr X))) + (Not (Expr X))) + +(define-type MailField To From CC Date Subject) + +(define-type-alias MailPred (×× [field : MailField] + [contains? : String])) + +(define (test [f : MailField] [c? : String] -> (Expr MailPred)) + (Base (rec [field = f] [contains? = c?]))) + +(check-type (rec [field = To] [contains = "doligez"]) + : (×× [field : MailField] [contains : String])) + +(check-type (get (rec [field = To] [contains = "doligez"]) field) + : MailField -> To) + +(check-type + (And (list (Or (list (Base (rec [field = To] [contains? = "doligez"])) + (Base (rec [field = CC] [contains? = "doligez"])))) + (Base (rec [field = Subject] [contains? = "runtime"])))) + : (Expr MailPred)) + +(define (andmap [f : (→ X Bool)] [lst : (List X)] -> Bool) + (if (isnil lst) + #t + (and (f (head lst)) (andmap f (tail lst))))) +(define (ormap [f : (→ X Bool)] [lst : (List X)] -> Bool) + (if (isnil lst) + #f + (or (f (head lst)) (ormap f (tail lst))))) + +(define (filter [p? : (→ X Bool)] [lst : (List X)] -> (List X)) + (if (isnil lst) + nil + (if (p? (head lst)) + (cons (head lst) (filter p? (tail lst))) + (filter p? (tail lst))))) + +(define (eval [e : (Expr X)] [eval-base : (→ X Bool)] -> Bool) + (let ([eval2 (λ ([e : (Expr X)]) (eval e eval-base))]) + (match e with + [Base base -> (eval-base base)] + [Const b -> b] + [And es -> (andmap eval2 es)] + [Or es -> (ormap eval2 es)] + [Not e -> (not (eval2 e))]))) + +(define (andfn [lst : (List (Expr X))] -> (Expr X)) + (if (member (Const #f) lst) + (Const #f) + (let ([lst2 + (filter (λ ([x : (Expr X)]) (not (equal? x (Const #t)))) lst)]) + (if (isnil lst2) + (Const #t) + (if (isnil (tail lst2)) + (head lst2) + (And lst2)))))) + +(define (orfn [lst : (List (Expr X))] -> (Expr X)) + (if (member (Const #t) lst) + (Const #t) + (let ([lst2 + (filter (λ ([x : (Expr X)]) (not (equal? x (Const #f)))) lst)]) + (if (isnil lst2) + (Const #f) + (if (isnil (tail lst2)) + (head lst2) + (And lst2)))))) + +(define (notfn [e : (Expr X)] -> (Expr X)) + (match e with + [Base b -> (Not e)] + [Const b -> (Const (not b))] + [And es -> (Not e)] + [Or es -> (Not e)] + [Not e2 -> (Not e)])) + +(define (simplify [e : (Expr X)] -> (Expr X)) + (match e with + [Base b -> e] + [Const x -> e] + [And es -> (andfn (map (inst simplify X) es))] + [Or es -> (orfn (map (inst simplify X) es))] + [Not e -> (notfn (simplify e))])) + +(check-type + (simplify (Not (And (list (Or (list (Base "it's snowing") + (Const #t))) + (Base "it's raining"))))) + : (Expr String) + -> (Not (Base "it's raining"))) + +(check-type + (simplify (Not (And (list (Or (list (Base "it's snowing") + (Const #t))) + (Not (Not (Base "it's raining"))))))) + : (Expr String) + -> (Not (Not (Not (Base "it's raining"))))) + +(define (notfn2 [e : (Expr X)] -> (Expr X)) + (match e with + [Const b -> (Const (not b))] + [Base b -> (Not e)] + [And es -> (Not e)] + [Or es -> (Not e)] + [Not e -> e])) + +(define (simplify2 [e : (Expr X)] -> (Expr X)) + (match e with + [Base b -> e] + [Const x -> e] + [And es -> (andfn (map (inst simplify2 X) es))] + [Or es -> (orfn (map (inst simplify2 X) es))] + [Not e -> (notfn2 (simplify2 e))])) + +(check-type + (simplify2 (Not (And (list (Or (list (Base "it's snowing") + (Const #t))) + (Not (Not (Base "it's raining"))))))) + : (Expr String) + -> (Not (Base "it's raining"))) diff --git a/macrotypes/examples/tests/mlish/trees-tests.mlish b/macrotypes/examples/tests/mlish/trees-tests.mlish new file mode 100644 index 0000000..b369e49 --- /dev/null +++ b/macrotypes/examples/tests/mlish/trees-tests.mlish @@ -0,0 +1,51 @@ +#lang s-exp "../../mlish.rkt" +(require "../rackunit-typechecking.rkt") +(require "trees.mlish") + +(define (make [item : Int] [depth : Int] -> (Tree Int)) + (if (zero? depth) + (Leaf item) + (let ([item2 (* item 2)] + [depth2 (sub1 depth)]) + (Node (make (sub1 item2) depth2) + item + (make item2 depth2))))) + +(define tree1 (make 4 1)) +(define tree2 (make 3 2)) + +(check-type tree1 + : (Tree Int) -> (Node (Leaf 7) 4 (Leaf 8))) + +(check-type tree2 + : (Tree Int) + -> (Node + (Node (Leaf 9) 5 (Leaf 10)) + 3 + (Node (Leaf 11) 6 (Leaf 12)))) + +(define (sum [t : (Tree Int)] -> Int) + (match t with + [Leaf v -> v] + [Node l v r -> (+ (+ (sum l) v) (sum r))])) + +(check-type (sum tree1) : Int -> 19) +(check-type (sum tree2) : Int -> 56) + +(define (check/acc [t : (Tree Int)] [acc : Int] -> Int) + (match t with + [Leaf v -> + (+ acc v)] + [Node l v r -> + (check/acc l (- acc (check/acc r 0)))])) +(define (check [t : (Tree Int)] -> Int) + (check/acc t 0)) + +(define min-depth 4) + +(define (main [n : Int] -> Int) + (let* ([max-depth (max (+ min-depth 2) n)] + [stretch-depth (add1 max-depth)]) + (check (make 0 stretch-depth)))) + +(check-type (main 17) : Int -> 0) diff --git a/macrotypes/examples/tests/mlish/trees.mlish b/macrotypes/examples/tests/mlish/trees.mlish new file mode 100644 index 0000000..893dee0 --- /dev/null +++ b/macrotypes/examples/tests/mlish/trees.mlish @@ -0,0 +1,8 @@ +#lang s-exp "../../mlish.rkt" +(require "../rackunit-typechecking.rkt") + +(define-type (Tree X) + (Leaf X) + (Node (Tree X) X (Tree X))) + +(provide-type Tree Leaf Node) diff --git a/macrotypes/examples/tests/mlish/value-restriction-example.mlish b/macrotypes/examples/tests/mlish/value-restriction-example.mlish new file mode 100644 index 0000000..dd00d5c --- /dev/null +++ b/macrotypes/examples/tests/mlish/value-restriction-example.mlish @@ -0,0 +1,25 @@ +#lang s-exp "../../mlish.rkt" +(require "../rackunit-typechecking.rkt") + +(define-type (Option X) + None + (Some X)) + +(define (make-f → (→ A A)) + (let ([r (ref (None {A}))]) + (λ (x) + (let ([y (deref r)]) + (begin + (:= r (Some x)) + (match y with + [None -> x] + [Some y -> y])))))) +;; This has to fail, because if could succeed with the type (→ A A), +;; then it could cause unsoundness. +(typecheck-fail (make-f) #:with-msg "Could not infer instantiation of polymorphic function make-f.") +; ;; If f were defined as the result of (make-f), then it would result +; ;; in unsoundess if these two expressions were also accepted: +; (f 13) +; ;; Because this would typecheck as a String even though it returns 13, an Int: +; (f "foo") + diff --git a/macrotypes/examples/tests/run-all-mlish-tests.rkt b/macrotypes/examples/tests/run-all-mlish-tests.rkt new file mode 100644 index 0000000..f97bbb3 --- /dev/null +++ b/macrotypes/examples/tests/run-all-mlish-tests.rkt @@ -0,0 +1,45 @@ +#lang racket/base +(require (for-syntax racket/base syntax/parse racket/syntax syntax/stx)) +(require racket/match racket/system racket/port racket/format) + +(define R (path->string (find-system-path 'exec-file))) + +(define (mk-process-cmd r n) + (string-append "time " r " run-mlish-tests" (number->string n) ".rkt")) + +(define-for-syntax ((mk-num-id str) n-stx) + (format-id n-stx (string-append str "~a") (syntax-e n-stx))) + +;; do-test: abstracts and interleaves the following def, reporting, and cleanup: +;; (match-define (list i1 o1 id1 err1 f1) +;; (process "time racket run-mlish-tests1.rkt")) +;; (displayln "---- tests: General MLish tests: -----------------------------") +;; (write-string (port->string err1)) +;; (write-string (port->string i1)) +;; (close-input-port i1) +;; (close-output-port o1) +;; (close-input-port err1) +(define-syntax (do-tests stx) + (syntax-parse stx + [(_ (~seq n name) ...) + #:with (in ...) (stx-map (mk-num-id "i") #'(n ...)) + #:with (out ...) (stx-map (mk-num-id "o") #'(n ...)) + #:with (err ...) (stx-map (mk-num-id "err") #'(n ...)) + #'(begin + (match-define (list in out _ err _) + (process (mk-process-cmd R n))) ... + (begin + (displayln + (~a (string-append "----- " name " tests:") + #:pad-string "-" + #:min-width 80)) + (write-string (port->string err)) + (write-string (port->string in))) ... + (close-input-port in) ... + (close-output-port out) ... + (close-input-port err) ...)])) + +(do-tests 1 "General MLish" + 2 "Shootout and RW OCaml" + 3 "Ben's" + 4 "Okasaki / polymorphic recursion") diff --git a/macrotypes/examples/tests/run-mlish-tests1.rkt b/macrotypes/examples/tests/run-mlish-tests1.rkt new file mode 100644 index 0000000..17a258b --- /dev/null +++ b/macrotypes/examples/tests/run-mlish-tests1.rkt @@ -0,0 +1,22 @@ +#lang racket/base +(require "mlish-tests.rkt") +(require "mlish/queens.mlish") +(require "mlish/listpats.mlish") +(require "mlish/match2.mlish") +(require "mlish/polyrecur.mlish") +(require "mlish/loop.mlish") +(require "mlish/value-restriction-example.mlish") +(require "mlish/infer-variances.mlish") + +;; (require "mlish/trees.mlish") +;; (require "mlish/chameneos.mlish") +;; (require "mlish/ack.mlish") +;; (require "mlish/ary.mlish") +;; (require "mlish/fannkuch.mlish") +;; (require "mlish/fasta.mlish") +;; (require "mlish/fibo.mlish") +;; (require "mlish/hash.mlish") +;; ;(require "mlish/heapsort.mlish") +;; (require "mlish/knuc.mlish") +;; (require "mlish/matrix.mlish") +;; (require "mlish/nbody.mlish") diff --git a/macrotypes/examples/tests/run-mlish-tests2.rkt b/macrotypes/examples/tests/run-mlish-tests2.rkt new file mode 100644 index 0000000..92e8e14 --- /dev/null +++ b/macrotypes/examples/tests/run-mlish-tests2.rkt @@ -0,0 +1,24 @@ +#lang racket/base + +;(require "mlish/queens.mlish") + +;; shootout tests +(require "mlish/trees-tests.mlish") +(require "mlish/chameneos.mlish") +(require "mlish/ack.mlish") +(require "mlish/ary.mlish") +(require "mlish/fannkuch.mlish") +(require "mlish/fasta.mlish") +(require "mlish/fibo.mlish") +(require "mlish/hash.mlish") +;(require "mlish/heapsort.mlish") +(require "mlish/knuc.mlish") +(require "mlish/matrix.mlish") +(require "mlish/nbody.mlish") + +;; from rw ocaml +(require "mlish/term.mlish") +(require "mlish/find.mlish") +(require "mlish/alex.mlish") +(require "mlish/inst.mlish") +(require "mlish/result.mlish") diff --git a/macrotypes/examples/tests/run-mlish-tests3.rkt b/macrotypes/examples/tests/run-mlish-tests3.rkt new file mode 100644 index 0000000..048d497 --- /dev/null +++ b/macrotypes/examples/tests/run-mlish-tests3.rkt @@ -0,0 +1,7 @@ +#lang racket/base +;; bg +(require "mlish/bg/basics.mlish") +(require "mlish/bg/basics2.mlish") +(require "mlish/bg/huffman.mlish") +(require "mlish/bg/lambda.mlish") +(require "mlish/bg/monad.mlish") diff --git a/macrotypes/examples/tests/run-mlish-tests4.rkt b/macrotypes/examples/tests/run-mlish-tests4.rkt new file mode 100644 index 0000000..4e8cc2d --- /dev/null +++ b/macrotypes/examples/tests/run-mlish-tests4.rkt @@ -0,0 +1,5 @@ +#lang racket/base + +;; okasaki tests +;(require "mlish/polyrecur.mlish") +(require "mlish/bg/okasaki.mlish")