From db1da5ae20f223d7f02991039d9cfd1f11b38301 Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Thu, 10 Mar 2016 14:30:43 -0500 Subject: [PATCH] implement find example --- tapl/tests/mlish/find.mlish | 33 ++++++++++++++++++++++++++++++ tapl/tests/run-all-mlish-tests.rkt | 1 + 2 files changed, 34 insertions(+) create mode 100644 tapl/tests/mlish/find.mlish diff --git a/tapl/tests/mlish/find.mlish b/tapl/tests/mlish/find.mlish new file mode 100644 index 0000000..f795f62 --- /dev/null +++ b/tapl/tests/mlish/find.mlish @@ -0,0 +1,33 @@ +#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 {Int})) + +(check-type + (find (Nil {Int}) (λ ([x : Int]) (<= 2 x))) + : (Option Int) + -> (None {Int})) + diff --git a/tapl/tests/run-all-mlish-tests.rkt b/tapl/tests/run-all-mlish-tests.rkt index 115c23b..7f29cf1 100644 --- a/tapl/tests/run-all-mlish-tests.rkt +++ b/tapl/tests/run-all-mlish-tests.rkt @@ -16,3 +16,4 @@ ;; from rw ocaml (require "mlish/term.mlish") +(require "mlish/find.mlish")