From 41968efaea7707a8f00c9486602193513b286dae Mon Sep 17 00:00:00 2001 From: ben Date: Mon, 21 Mar 2016 23:48:57 -0400 Subject: [PATCH 1/4] [bg] starter functions --- tapl/tests/mlish/bg/README.md | 28 ++++ tapl/tests/mlish/bg/ps1.mlish | 248 ++++++++++++++++++++++++++++++++++ 2 files changed, 276 insertions(+) create mode 100644 tapl/tests/mlish/bg/README.md create mode 100644 tapl/tests/mlish/bg/ps1.mlish diff --git a/tapl/tests/mlish/bg/README.md b/tapl/tests/mlish/bg/README.md new file mode 100644 index 0000000..b1f6128 --- /dev/null +++ b/tapl/tests/mlish/bg/README.md @@ -0,0 +1,28 @@ +bg +=== + +mlish tests by Ben + +- `ps1` : + ``` + (define (fn-list [f* : (List (→ A A))] [a : A] → A) + (define (count-letters/one [s : String] [c : Char] → Int) + (define (count-letters [s* : (List String)] [c : Char] → Int) + (define (map [f : (→ A B)] [x* : (List A)] → (List B)) + (define (append [x* : (List A)] [y* : (List A)] → (List A)) + (define (flatten [x** : (List (List A))] → (List A)) + (define (insert [x : A] → (→ (List A) (List (List A)))) + (define (permutations [x* : (List A)] → (List (List A))) + (define (split [ab* : (List (** A B))] → (** (List A) (List B))) + (define (combine [a*b* : (** (List A) (List B))] → (List (** A B))) + (define (fst [xy : (** A B)] → A) + (define (snd [xy : (** A B)] → B) + (define (foldl [f : (→ A B A)] [acc : A] [x* : (List B)] → A) + (define (sum [x* : (List Float)] → Float) + (define (reverse [x* : (List A)] → (List A)) + (define (convolve [x* : (List Float)] [y* : (List Float)] → Float) + (define (mc [n : Int] [f : (→ A A)] [x : A] → A) + (define (square [n : Int] → Int) + (define (successor [mcn : (→ (→ A A) A A)] → (→ (→ A A) A A)) + ``` +- diff --git a/tapl/tests/mlish/bg/ps1.mlish b/tapl/tests/mlish/bg/ps1.mlish new file mode 100644 index 0000000..f56680e --- /dev/null +++ b/tapl/tests/mlish/bg/ps1.mlish @@ -0,0 +1,248 @@ +#lang s-exp "../../../mlish.rkt" +(require "../../rackunit-typechecking.rkt") + +;; ============================================================================= + +(define-type (List X) + Nil + (Cons X (List X))) + +;; ============================================================================= +;; 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 (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 (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 {Int})) + : (List (List Int)) + ⇒ (Cons (Nil {(List Int)}) 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-type (** X Y) + (Pair X Y)) + +(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 {(** Int Int)})) + : (** (List Int) (List Int)) + ⇒ (Pair (Nil {Int}) (Nil {Int}))) + +(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 {Int}) (Nil {Int}))) + : (List (** Int Int)) + ⇒ (Nil {(** Int Int)})) + +(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 (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 (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 (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*)) + +(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;; From 04e1cb701f48484298ed5b1149bb13cd730f9dea Mon Sep 17 00:00:00 2001 From: ben Date: Tue, 22 Mar 2016 21:25:12 -0400 Subject: [PATCH 2/4] [bg] more lists, sorting, CPS --- tapl/tests/mlish/bg/README.md | 66 ++-- tapl/tests/mlish/bg/basics.mlish | 557 +++++++++++++++++++++++++++++++ tapl/tests/mlish/bg/ps1.mlish | 248 -------------- 3 files changed, 600 insertions(+), 271 deletions(-) create mode 100644 tapl/tests/mlish/bg/basics.mlish delete mode 100644 tapl/tests/mlish/bg/ps1.mlish diff --git a/tapl/tests/mlish/bg/README.md b/tapl/tests/mlish/bg/README.md index b1f6128..4a56998 100644 --- a/tapl/tests/mlish/bg/README.md +++ b/tapl/tests/mlish/bg/README.md @@ -3,26 +3,46 @@ bg mlish tests by Ben -- `ps1` : - ``` - (define (fn-list [f* : (List (→ A A))] [a : A] → A) - (define (count-letters/one [s : String] [c : Char] → Int) - (define (count-letters [s* : (List String)] [c : Char] → Int) - (define (map [f : (→ A B)] [x* : (List A)] → (List B)) - (define (append [x* : (List A)] [y* : (List A)] → (List A)) - (define (flatten [x** : (List (List A))] → (List A)) - (define (insert [x : A] → (→ (List A) (List (List A)))) - (define (permutations [x* : (List A)] → (List (List A))) - (define (split [ab* : (List (** A B))] → (** (List A) (List B))) - (define (combine [a*b* : (** (List A) (List B))] → (List (** A B))) - (define (fst [xy : (** A B)] → A) - (define (snd [xy : (** A B)] → B) - (define (foldl [f : (→ A B A)] [acc : A] [x* : (List B)] → A) - (define (sum [x* : (List Float)] → Float) - (define (reverse [x* : (List A)] → (List A)) - (define (convolve [x* : (List Float)] [y* : (List Float)] → Float) - (define (mc [n : Int] [f : (→ A A)] [x : A] → A) - (define (square [n : Int] → Int) - (define (successor [mcn : (→ (→ A A) A A)] → (→ (→ A A) A 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) +(map [f : (→ A B)] [x* : (List A)] → (List B)) +(append [x* : (List A)] [y* : (List A)] → (List A)) +(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))) +(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)) +(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)) +(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)))) +(split [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)) +``` + + diff --git a/tapl/tests/mlish/bg/basics.mlish b/tapl/tests/mlish/bg/basics.mlish new file mode 100644 index 0000000..b0aebb5 --- /dev/null +++ b/tapl/tests/mlish/bg/basics.mlish @@ -0,0 +1,557 @@ +#lang s-exp "../../../mlish.rkt" +(require "../../rackunit-typechecking.rkt") + +;; ============================================================================= + +(define-type (List X) + Nil + (Cons X (List X))) + +;; ============================================================================= +;; 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 (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 (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 {Int})) + : (List (List Int)) + ⇒ (Cons (Nil {(List Int)}) 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-type (** X Y) + (Pair X Y)) + +(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 {(** Int Int)})) + : (** (List Int) (List Int)) + ⇒ (Pair (Nil {Int}) (Nil {Int}))) + +(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 {Int}) (Nil {Int}))) + : (List (** Int Int)) + ⇒ (Nil {(** Int Int)})) + +(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-type Bool + True + False) + +(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*)) + +(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;; + +;; ----------------------------------------------------------------------------- + +(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 {(List (** String Int))})) + +(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 {(List (** String (List Int)))})) + +(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 {(List (** String (List Int)))})) + +(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)))))))))))))))))))))) + +;; ============================================================================= +;; === sorting + +;; ----------------------------------------------------------------------------- +;; --- mergesort + +(define (split [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 (split 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 (split x*) with + [Pair x* y* -> + (merge (Pair (mergesort x*) (mergesort y*)))])])])) + +(check-type + (mergesort (Nil {Int})) + : (List Int) + ⇒ (Nil {Int})) + +(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 {Int})) + : (List Int) + ⇒ (Nil {Int})) + +(check-type + (quicksort (Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil))))) + : (List Int) + ⇒ (Cons 1 (Cons 2 (Cons 3 (Cons 4 Nil))))) + +(check-type + (quicksort (Cons 3 (Cons 7 (Cons 93 (Cons 0 (Cons 2 Nil)))))) + : (List Int) + ⇒ (Cons 0 (Cons 2 (Cons 3 (Cons 7 (Cons 93 Nil)))))) + +;; ============================================================================= +;; === CPS + +;; ----------------------------------------------------------------------------- +;; --- factorial + +(define (fact [n : Int] → Int) + (if (< n 2) + 1 + (* n (fact (- n 1))))) + +(define (range-aux [n : Int] → (List Int)) + (if (= 0 n) + (Cons n Nil) + (Cons n (range-aux (- n 1))))) + +(define (range [n : Int] → (List Int)) + (if (<= n 0) + Nil + (reverse (range-aux (- n 1))))) + +(define (fact-acc [n : Int] → Int) + (foldl (λ ([acc : Int] [n : Int]) (* n acc)) 1 (map (λ ([n : Int]) (+ n 1)) (range n)))) + +(define (fact-cps-aux [n : Int] [k : (→ Int Int)] → Int) + (if (< n 2) + (k 1) + (fact-cps-aux (- n 1) (λ ([m : Int]) (k (* n m)))))) + +(define (fact-cps [n : Int] → Int) + (fact-cps-aux n (λ ([x : Int]) x))) + +(check-type (fact 0) : Int ⇒ 1) +(check-type (fact 1) : Int ⇒ 1) +(check-type (fact 2) : Int ⇒ 2) +(check-type (fact 3) : Int ⇒ 6) +(check-type (fact 4) : Int ⇒ 24) +(check-type (fact 5) : Int ⇒ 120) + +(check-type (fact-acc 0) : Int ⇒ 1) +(check-type (fact-acc 1) : Int ⇒ 1) +(check-type (fact-acc 2) : Int ⇒ 2) +(check-type (fact-acc 3) : Int ⇒ 6) +(check-type (fact-acc 4) : Int ⇒ 24) +(check-type (fact-acc 5) : Int ⇒ 120) + +(check-type (fact-cps 0) : Int ⇒ 1) +(check-type (fact-cps 1) : Int ⇒ 1) +(check-type (fact-cps 2) : Int ⇒ 2) +(check-type (fact-cps 3) : Int ⇒ 6) +(check-type (fact-cps 4) : Int ⇒ 24) +(check-type (fact-cps 5) : Int ⇒ 120) + +;; ----------------------------------------------------------------------------- +;; --- map + +(define (map-cps-aux [f : (→ A B)] [x* : (List A)] [k : (→ (List B) (List B))] → (List B)) + (match x* with + [Nil -> (k Nil)] + [Cons x x* -> + (map-cps-aux f x* (λ ([b* : (List B)]) (k (Cons (f x) b*))))])) + +(define (map-cps [f : (→ A B)] [x* : (List A)] → (List B)) + (map-cps-aux f x* (λ ([x : (List B)]) x))) + +(check-type + (map-cps (λ ([x : Int]) (+ x 2)) (Cons 2 (Cons 4 (Cons 8 Nil)))) + : (List Int) + ⇒ (Cons 4 (Cons 6 (Cons 10 Nil)))) + +(check-type + (map-cps exact->inexact (Cons 2 (Cons 4 (Cons 8 Nil)))) + : (List Float) + ⇒ (Cons 2.0 (Cons 4.0 (Cons 8.0 Nil)))) + diff --git a/tapl/tests/mlish/bg/ps1.mlish b/tapl/tests/mlish/bg/ps1.mlish deleted file mode 100644 index f56680e..0000000 --- a/tapl/tests/mlish/bg/ps1.mlish +++ /dev/null @@ -1,248 +0,0 @@ -#lang s-exp "../../../mlish.rkt" -(require "../../rackunit-typechecking.rkt") - -;; ============================================================================= - -(define-type (List X) - Nil - (Cons X (List X))) - -;; ============================================================================= -;; 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 (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 (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 {Int})) - : (List (List Int)) - ⇒ (Cons (Nil {(List Int)}) 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-type (** X Y) - (Pair X Y)) - -(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 {(** Int Int)})) - : (** (List Int) (List Int)) - ⇒ (Pair (Nil {Int}) (Nil {Int}))) - -(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 {Int}) (Nil {Int}))) - : (List (** Int Int)) - ⇒ (Nil {(** Int Int)})) - -(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 (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 (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 (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*)) - -(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;; From 05df0337906560e203a8cffdc5eefc925d96de79 Mon Sep 17 00:00:00 2001 From: ben Date: Wed, 23 Mar 2016 00:06:33 -0400 Subject: [PATCH 3/4] [bg] huffman trees --- tapl/mlish.rkt | 1 + tapl/tests/mlish/bg/README.md | 32 ++++ tapl/tests/mlish/bg/huffman.mlish | 278 ++++++++++++++++++++++++++++++ 3 files changed, 311 insertions(+) create mode 100644 tapl/tests/mlish/bg/huffman.mlish diff --git a/tapl/mlish.rkt b/tapl/mlish.rkt index 21a7897..5cc5a0b 100644 --- a/tapl/mlish.rkt +++ b/tapl/mlish.rkt @@ -540,6 +540,7 @@ (define-primop string : (→ Char String)) (define-primop sleep : (→ Int Unit)) (define-primop string=? : (→ String String Bool)) +(define-primop string<=? : (→ String String Bool)) (define-typed-syntax string-append [(_ . strs) diff --git a/tapl/tests/mlish/bg/README.md b/tapl/tests/mlish/bg/README.md index 4a56998..33100ed 100644 --- a/tapl/tests/mlish/bg/README.md +++ b/tapl/tests/mlish/bg/README.md @@ -45,4 +45,36 @@ mlish tests by Ben (map-cps [f : (→ A B)] [x* : (List A)] → (List B)) ``` +`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)) +``` + diff --git a/tapl/tests/mlish/bg/huffman.mlish b/tapl/tests/mlish/bg/huffman.mlish new file mode 100644 index 0000000..0e3399a --- /dev/null +++ b/tapl/tests/mlish/bg/huffman.mlish @@ -0,0 +1,278 @@ +#lang s-exp "../../../mlish.rkt" +(require "../../rackunit-typechecking.rkt") + +;; Huffman trees from SICP + +;; ============================================================================= +;; === Sets of Symbols + +(define-type-alias Symbol String) + +;; Set of strings +(define-type Symbol* + [Empty] + [Singleton String] + [Join String Symbol* Symbol*]) + +(define (empty → Symbol*) + Empty) + +(define (singleton [s : String] → Symbol*) + (Singleton s)) + +(define (insert [s* : Symbol*] [s1 : String] → Symbol*) + (match s* with + [Empty -> (singleton s1)] + [Singleton s2 -> + (if (string<=? s1 s2) + (if (string=? s1 s2) + s* + (Join s2 (singleton s1) (empty))) + (Join s1 (singleton s2) (empty)))] + [Join s2 l* r* -> + (if (string<=? s1 s2) + (if (string=? s1 s2) + s* + (Join s2 (insert l* s1) r*)) + (Join s2 l* (insert r* s1)))])) + +(define (union [s1 : Symbol*] [s2 : Symbol*] → Symbol*) + (match s1 with + [Empty -> s2] + [Singleton s -> (insert s2 s)] + [Join s l* r* -> (union l* (union r* (insert s2 s)))])) + +(define (contains [s* : Symbol*] [s : Symbol] → Bool) + (match s* with + [Empty -> #f] + [Singleton s2 -> (string=? s s2)] + [Join s2 l* r* -> + (if (string<=? s s2) + (if (string=? s s2) + #t + (contains l* s)) + (contains r* s))])) + +;; ----------------------------------------------------------------------------- + +(check-type + (insert (empty) "hello") + : Symbol* + ⇒ (singleton "hello")) + +(check-type + (insert (insert (empty) "a") "b") + : Symbol* + ⇒ (Join "b" (singleton "a") (empty))) + +(check-type + (insert (insert (empty) "b") "a") + : Symbol* + ⇒ (Join "b" (singleton "a") (empty))) + +(check-type + (insert (insert (insert (empty) "a") "b") "c") + : Symbol* + ⇒ (Join "b" (singleton "a") (singleton "c"))) + +(check-type + (insert (insert (insert (empty) "c") "b") "a") + : Symbol* + ⇒ (Join "c" (Join "b" (singleton "a") (empty)) (empty))) + +(check-type + (union + (insert (insert (insert (empty) "c") "b") "a") + (insert (insert (insert (empty) "a") "b") "c")) + : Symbol* + ⇒ (Join "b" (singleton "a") (singleton "c"))) + +;; ----------------------------------------------------------------------------- + +(define-type (List A) + [⊥] + [∷ A (List A)]) + +(define-type-alias SymbolList (List Symbol)) + +(define (list [x : A] → (List A)) + (∷ x ⊥)) + +(define (append [x* : (List A)] [y* : (List A)] → (List A)) + (match x* with + [⊥ -> y*] + [∷ x x* -> + (∷ x (append x* y*))])) + +(define (length [x* : (List A)] → Int) + (match x* with + [⊥ -> 0] + [∷ x x* -> (+ 1 (length x*))])) + +;; ----------------------------------------------------------------------------- + +(define-type Bit O I) +(define-type-alias Bit* (List Bit)) + +;; ----------------------------------------------------------------------------- + +(define-type HTree + [Leaf String Int] ;; Symbol, Weight + [Node HTree HTree Symbol* Int] ;; Left, Right, Symbols, Weight +) + +(define (symbols [h : HTree] → Symbol*) + (match h with + [Leaf s w -> (singleton s)] + [Node lh rh s* w -> s*])) + +(define (weight [h : HTree] → Int) + (match h with + [Leaf s w -> w] + [Node l r s w -> w])) + +(define (make-code-tree [left : HTree] [right : HTree] → HTree) + (Node left right + (union (symbols left) (symbols right)) + (+ (weight left) (weight right)))) + +(define (decode-aux [bits : Bit*] [root : HTree] [current-branch : HTree] → SymbolList) + (match bits with + [⊥ -> + ⊥] + [∷ b bit* -> + (match (choose-branch b current-branch) with + [Leaf s w -> + (∷ s (decode-aux bit* root root))] + [Node l r s* w -> + (decode-aux bit* root (Node l r s* w))])])) + +(define (decode [bits : Bit*] [tree : HTree] → SymbolList) + (decode-aux bits tree tree)) + +(define (choose-branch [bit : Bit] [branch : HTree] → HTree) + (match branch with + [Leaf s w -> + ;; Error + (Leaf "ERROR" 0)] + [Node l* r* s* w -> + (match bit with + [O -> l*] + [I -> r*])])) + +(define-type-alias HTreeSet (List HTree)) + +(define (adjoin-set [x : HTree] [set : HTreeSet] → HTreeSet) + (match set with + [⊥ -> (list x)] + [∷ y y* -> + (if (< (weight x) (weight y)) + (∷ x set) + (∷ y (adjoin-set x y*)))])) + +(define (make-leaf-set [pair* : (List (× Symbol Int))] → HTreeSet) + (match pair* with + [⊥ -> ⊥] + [∷ pair pair* -> + (match pair with + [s i -> + (adjoin-set (Leaf s i) (make-leaf-set pair*))])])) + +(check-type + (make-leaf-set (∷ (tup "A" 4) + (∷ (tup "B" 2) + (∷ (tup "C" 1) + (∷ (tup "D" 1) + ⊥))))) + : HTreeSet + ⇒ (∷ (Leaf "D" 1) + (∷ (Leaf "C" 1) + (∷ (Leaf "B" 2) + (∷ (Leaf "A" 4) + ⊥))))) + +(define sample-tree + (make-code-tree + (Leaf "A" 4) + (make-code-tree + (Leaf "B" 2) + (make-code-tree + (Leaf "D" 1) + (Leaf "C" 1))))) + +(define sample-message + (∷ O (∷ I (∷ I (∷ O (∷ O (∷ I (∷ O (∷ I (∷ O (∷ I (∷ I (∷ I (∷ I (∷ O ⊥))))))))))))))) + +(check-type + (decode sample-message sample-tree) + : SymbolList + ⇒ (∷ "A" (∷ "D" (∷ "A" (∷ "B" (∷ "B" (∷ "C" (∷ "B" ⊥)))))))) + +(define (encode [message : SymbolList] [tree : HTree] → Bit*) + (match message with + [⊥ -> ⊥] + [∷ m m* -> + (append (encode-symbol m tree) (encode m* tree))])) + +(define (contains-symbol [s : Symbol] [tree : HTree] → Bool) + (contains (symbols tree) s)) + +;; Undefined if symbol is not in tree. Be careful! +(define (encode-symbol [s : Symbol] [tree : HTree] → Bit*) + (match tree with + [Leaf s w -> ⊥] + [Node l* r* s* w -> + (if (contains-symbol s l*) + (∷ O (encode-symbol s l*)) + (∷ I (encode-symbol s r*)))])) + +(check-type + (encode (decode sample-message sample-tree) sample-tree) + : Bit* + ⇒ sample-message) + +(define-type-alias Frequency Int) +(define (generate-huffman-tree [pair* : (List (× Symbol Frequency))] → HTree) + (successive-merge (make-leaf-set pair*))) + +(define (successive-merge [tree* : HTreeSet] → HTree) + (match tree* with + [⊥ -> (Leaf "ERROR" 0)] + [∷ t t* -> + (match t* with + [⊥ -> t] + [∷ t2 t* -> + (successive-merge (adjoin-set (make-code-tree t t2) t*))])])) + +(define rock-pair* + (∷ (tup "A" 2) + (∷ (tup "BOOM" 2) + (∷ (tup "GET" 2) + (∷ (tup "JOB" 2) + (∷ (tup "NA" 16) + (∷ (tup "SHA" 3) + (∷ (tup "YIP" 9) + (∷ (tup "WAH" 1) + ⊥))))))))) + +(define rock-tree (generate-huffman-tree rock-pair*)) + +(define rock-message + (∷ "GET" (∷ "A" (∷ "JOB" + (∷ "SHA" (∷ "NA" (∷ "NA" (∷ "NA" (∷ "NA" (∷ "NA" (∷ "NA" (∷ "NA" (∷ "NA" + (∷ "GET" (∷ "A" (∷ "JOB" + (∷ "SHA" (∷ "NA" (∷ "NA" (∷ "NA" (∷ "NA" (∷ "NA" (∷ "NA" (∷ "NA" (∷ "NA" + (∷ "WAH" (∷ "YIP" (∷ "YIP" (∷ "YIP" (∷ "YIP" (∷ "YIP" (∷ "YIP" (∷ "YIP" (∷ "YIP" (∷ "YIP" + (∷ "SHA" (∷ "BOOM" ⊥))))))))))))))))))))))))))))))))))))) + +(define rock-bit* (encode rock-message rock-tree)) + +(check-type + (decode rock-bit* rock-tree) + : SymbolList + ⇒ rock-message) + +(check-type + (length rock-bit*) + : Int + ⇒ 84) From 7dca7d4966f6d02c71ae58ec5e613d709c80fbdb Mon Sep 17 00:00:00 2001 From: ben Date: Wed, 23 Mar 2016 01:22:42 -0400 Subject: [PATCH 4/4] [bg] lambda calculus interpreter --- tapl/tests/mlish/bg/README.md | 13 +++++ tapl/tests/mlish/bg/lambda.rkt | 95 ++++++++++++++++++++++++++++++++++ 2 files changed, 108 insertions(+) create mode 100644 tapl/tests/mlish/bg/lambda.rkt diff --git a/tapl/tests/mlish/bg/README.md b/tapl/tests/mlish/bg/README.md index 33100ed..2e9d4ba 100644 --- a/tapl/tests/mlish/bg/README.md +++ b/tapl/tests/mlish/bg/README.md @@ -78,3 +78,16 @@ rock-bit* (encode rock-message rock-tree)) ``` +`lambda` +--- +``` +(fresh [e : Λ] → Int) +(subst [e : Λ] [i : Int] [v : Λ] → Λ) +(simpl-aux [e : Λ] [i : Int] → (× Int Λ)) +(simpl [e : Λ] → Λ) +(eval [e : Λ] → Λ) +I (Lambda 0 (Var 0)) +K (Lambda 0 (Lambda 1 (Var 0))) +S (Lambda 0 (Lambda 1 (Lambda 2 (App (App (Var 0) (Var 2)) (App (Var 1) (Var 2)))))) +false (App S K) +``` diff --git a/tapl/tests/mlish/bg/lambda.rkt b/tapl/tests/mlish/bg/lambda.rkt new file mode 100644 index 0000000..cee711e --- /dev/null +++ b/tapl/tests/mlish/bg/lambda.rkt @@ -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)) +