copy over the rest of the mlish tests
This commit is contained in:
AlexKnauth
parent
7677a6de28
commit
1d50b065b9
|
|
@ -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)))]
|
||||
))
|
||||
|
||||
|
|
|
|||
|
|
@ -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 ...)])
|
||||
|
|
|
|||
27
macrotypes/examples/tests/mlish/ack.mlish
Normal file
27
macrotypes/examples/tests/mlish/ack.mlish
Normal file
|
|
@ -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)
|
||||
25
macrotypes/examples/tests/mlish/alex.mlish
Normal file
25
macrotypes/examples/tests/mlish/alex.mlish
Normal file
|
|
@ -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\\)")
|
||||
|
||||
26
macrotypes/examples/tests/mlish/ary.mlish
Normal file
26
macrotypes/examples/tests/mlish/ary.mlish
Normal file
|
|
@ -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))
|
||||
103
macrotypes/examples/tests/mlish/bg/README.md
Normal file
103
macrotypes/examples/tests/mlish/bg/README.md
Normal file
|
|
@ -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)
|
||||
```
|
||||
59
macrotypes/examples/tests/mlish/bg/basics-general.mlish
Normal file
59
macrotypes/examples/tests/mlish/bg/basics-general.mlish
Normal file
|
|
@ -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)
|
||||
370
macrotypes/examples/tests/mlish/bg/basics.mlish
Normal file
370
macrotypes/examples/tests/mlish/bg/basics.mlish
Normal file
|
|
@ -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))))
|
||||
|
||||
138
macrotypes/examples/tests/mlish/bg/basics2.mlish
Normal file
138
macrotypes/examples/tests/mlish/bg/basics2.mlish
Normal file
|
|
@ -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))))))))))))))))))))))
|
||||
|
||||
278
macrotypes/examples/tests/mlish/bg/huffman.mlish
Normal file
278
macrotypes/examples/tests/mlish/bg/huffman.mlish
Normal file
|
|
@ -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)
|
||||
95
macrotypes/examples/tests/mlish/bg/lambda.mlish
Normal file
95
macrotypes/examples/tests/mlish/bg/lambda.mlish
Normal file
|
|
@ -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))
|
||||
|
||||
122
macrotypes/examples/tests/mlish/bg/monad.mlish
Normal file
122
macrotypes/examples/tests/mlish/bg/monad.mlish
Normal file
|
|
@ -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))
|
||||
1654
macrotypes/examples/tests/mlish/bg/okasaki.mlish
Normal file
1654
macrotypes/examples/tests/mlish/bg/okasaki.mlish
Normal file
File diff suppressed because it is too large
Load Diff
129
macrotypes/examples/tests/mlish/chameneos.mlish
Normal file
129
macrotypes/examples/tests/mlish/chameneos.mlish
Normal file
|
|
@ -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)))
|
||||
54
macrotypes/examples/tests/mlish/fannkuch.mlish
Normal file
54
macrotypes/examples/tests/mlish/fannkuch.mlish
Normal file
|
|
@ -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)
|
||||
191
macrotypes/examples/tests/mlish/fasta.mlish
Normal file
191
macrotypes/examples/tests/mlish/fasta.mlish
Normal file
|
|
@ -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"))
|
||||
22
macrotypes/examples/tests/mlish/fibo.mlish
Normal file
22
macrotypes/examples/tests/mlish/fibo.mlish
Normal file
|
|
@ -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)
|
||||
87
macrotypes/examples/tests/mlish/find.mlish
Normal file
87
macrotypes/examples/tests/mlish/find.mlish
Normal file
|
|
@ -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)] [<? : (→ Y Y Bool)] [extract-key : (→ X Y)]
|
||||
→ (Option (× X X)))
|
||||
(match lst with
|
||||
[Nil -> None]
|
||||
[Cons x1 rst ->
|
||||
(let ([y1 (extract-key x1)])
|
||||
(Some (find-min/max-accum rst <? extract-key x1 y1 x1 y1)))]))
|
||||
|
||||
(define (find-min/max-accum [lst : (List X)] [<? : (→ Y Y Bool)] [extract-key : (→ X Y)]
|
||||
[x-min : X] [y-min : Y] [x-max : X] [y-max : Y]
|
||||
→ (× X X))
|
||||
(match lst with
|
||||
[Nil -> (tup x-min x-max)]
|
||||
[Cons x2 rst ->
|
||||
(let ([y2 (extract-key x2)])
|
||||
(cond [(<? y2 y-min)
|
||||
(find-min/max-accum rst <? extract-key x2 y2 x-max y-max)]
|
||||
[(<? y-max y2)
|
||||
(find-min/max-accum rst <? extract-key x-min y-min x2 y2)]
|
||||
[else
|
||||
(find-min/max-accum rst <? extract-key x-min y-min x-max y-max)]))]))
|
||||
|
||||
(check-type
|
||||
(find-min/max (Nil {Int})
|
||||
(λ ([x : Int] [y : Int])
|
||||
(< x y))
|
||||
(λ ([x : Int])
|
||||
x))
|
||||
: (Option (× Int Int))
|
||||
-> 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)))
|
||||
|
||||
19
macrotypes/examples/tests/mlish/hash.mlish
Normal file
19
macrotypes/examples/tests/mlish/hash.mlish
Normal file
|
|
@ -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)
|
||||
243
macrotypes/examples/tests/mlish/infer-variances.mlish
Normal file
243
macrotypes/examples/tests/mlish/infer-variances.mlish
Normal file
|
|
@ -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*))
|
||||
|
||||
74
macrotypes/examples/tests/mlish/inst.mlish
Normal file
74
macrotypes/examples/tests/mlish/inst.mlish
Normal file
|
|
@ -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)
|
||||
|
||||
67
macrotypes/examples/tests/mlish/knuc.mlish
Normal file
67
macrotypes/examples/tests/mlish/knuc.mlish
Normal file
|
|
@ -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))
|
||||
70
macrotypes/examples/tests/mlish/listpats.mlish
Normal file
70
macrotypes/examples/tests/mlish/listpats.mlish
Normal file
|
|
@ -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)
|
||||
121
macrotypes/examples/tests/mlish/loop.mlish
Normal file
121
macrotypes/examples/tests/mlish/loop.mlish
Normal file
|
|
@ -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)
|
||||
|
||||
298
macrotypes/examples/tests/mlish/match2.mlish
Normal file
298
macrotypes/examples/tests/mlish/match2.mlish
Normal file
|
|
@ -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)
|
||||
73
macrotypes/examples/tests/mlish/matrix.mlish
Normal file
73
macrotypes/examples/tests/mlish/matrix.mlish
Normal file
|
|
@ -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)))
|
||||
185
macrotypes/examples/tests/mlish/nbody.mlish
Normal file
185
macrotypes/examples/tests/mlish/nbody.mlish
Normal file
|
|
@ -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")
|
||||
117
macrotypes/examples/tests/mlish/polyrecur.mlish
Normal file
117
macrotypes/examples/tests/mlish/polyrecur.mlish
Normal file
|
|
@ -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")
|
||||
186
macrotypes/examples/tests/mlish/queens.mlish
Normal file
186
macrotypes/examples/tests/mlish/queens.mlish
Normal file
|
|
@ -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))))))
|
||||
129
macrotypes/examples/tests/mlish/result.mlish
Normal file
129
macrotypes/examples/tests/mlish/result.mlish
Normal file
|
|
@ -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)))
|
||||
|
||||
|
||||
20
macrotypes/examples/tests/mlish/sweet-map.rkt
Normal file
20
macrotypes/examples/tests/mlish/sweet-map.rkt
Normal file
|
|
@ -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")
|
||||
295
macrotypes/examples/tests/mlish/term.mlish
Normal file
295
macrotypes/examples/tests/mlish/term.mlish
Normal file
|
|
@ -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")))
|
||||
51
macrotypes/examples/tests/mlish/trees-tests.mlish
Normal file
51
macrotypes/examples/tests/mlish/trees-tests.mlish
Normal file
|
|
@ -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)
|
||||
8
macrotypes/examples/tests/mlish/trees.mlish
Normal file
8
macrotypes/examples/tests/mlish/trees.mlish
Normal file
|
|
@ -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)
|
||||
|
|
@ -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")
|
||||
|
||||
45
macrotypes/examples/tests/run-all-mlish-tests.rkt
Normal file
45
macrotypes/examples/tests/run-all-mlish-tests.rkt
Normal file
|
|
@ -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")
|
||||
22
macrotypes/examples/tests/run-mlish-tests1.rkt
Normal file
22
macrotypes/examples/tests/run-mlish-tests1.rkt
Normal file
|
|
@ -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")
|
||||
24
macrotypes/examples/tests/run-mlish-tests2.rkt
Normal file
24
macrotypes/examples/tests/run-mlish-tests2.rkt
Normal file
|
|
@ -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")
|
||||
7
macrotypes/examples/tests/run-mlish-tests3.rkt
Normal file
7
macrotypes/examples/tests/run-mlish-tests3.rkt
Normal file
|
|
@ -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")
|
||||
5
macrotypes/examples/tests/run-mlish-tests4.rkt
Normal file
5
macrotypes/examples/tests/run-mlish-tests4.rkt
Normal file
|
|
@ -0,0 +1,5 @@
|
|||
#lang racket/base
|
||||
|
||||
;; okasaki tests
|
||||
;(require "mlish/polyrecur.mlish")
|
||||
(require "mlish/bg/okasaki.mlish")
|
||||
Loading…
Reference in New Issue
Block a user