77 lines
1.4 KiB
Agda
77 lines
1.4 KiB
Agda
module TestCase
|
|
|
|
-- I'm testing cases here, but using examples carefully design to be
|
|
-- simple case trees. Patterns are a var or a constructor applied to vars.
|
|
|
|
-- There are indexes below, but we're got pulling constraints out of them yet.
|
|
|
|
ptype Int
|
|
|
|
data Nat : U where
|
|
Z : Nat
|
|
S : Nat -> Nat
|
|
|
|
data Vect : Nat -> U -> U where
|
|
Nil : {a : U} -> Vect Z a
|
|
Cons : {a : U} {n : Nat} -> a -> Vect n a -> Vect (S n) a
|
|
|
|
plus : Nat -> Nat -> Nat
|
|
plus = \ n m => case n of
|
|
Z => m
|
|
S k => S (plus k m)
|
|
|
|
-- Example from Jesper talk (translated to explicit case tree)
|
|
max : Nat -> Nat -> Nat
|
|
max = \ n m => case n of
|
|
Z => m
|
|
S k => case m of
|
|
Z => S k
|
|
S l => S (max k l)
|
|
|
|
length : {a : U} {n : Nat} -> Vect n a -> Nat
|
|
length = \ v => case v of
|
|
Nil => Z
|
|
Cons x xs => S (length xs)
|
|
|
|
data Unit : U where
|
|
MkUnit : Unit
|
|
|
|
-- This should fail (and does!)
|
|
-- bar : Vect (S Z) Unit
|
|
-- bar = (Cons MkUnit (Cons MkUnit Nil))
|
|
|
|
data Bool : U where
|
|
True : Bool
|
|
False : Bool
|
|
|
|
not : Bool -> Bool
|
|
not = \ v => case v of
|
|
True => False
|
|
False => True
|
|
|
|
|
|
not2 : Bool -> Bool
|
|
not2 = \ v => case v of
|
|
True => False
|
|
x => True
|
|
|
|
and : Bool -> Bool -> Bool
|
|
and = \ x y => case x of
|
|
True => y
|
|
False => False
|
|
|
|
-- FIXME - a case is evaluated here, and I don't know why.
|
|
|
|
nand : Bool -> Bool -> Bool
|
|
nand = \ x y => not (case x of
|
|
True => y
|
|
False => False)
|
|
|
|
-- -- this should be an error.
|
|
-- foo : Bool -> Bool
|
|
|
|
data Void : U where
|
|
|
|
foo : Int
|
|
foo = 42
|