Merge branch 'master' of git.martlubbers.net:clean-tests into master

[clean-tests.git] / fundeps / test.icl

diff --git a/fundeps/test.icl b/fundeps/test.icl
new file mode 100644 (file)
index 0000000..034a2e8
--- /dev/null
+++ b/fundeps/test.icl
@@ -0,0 +1,154 @@
+module test
+
+import qualified StdEnv
+import StdEnv => qualified isEven, isOdd, class toInt(..), instance toInt Int, class toString(..)
+
+:: Zero = Zero
+:: Succ a = Succ
+:: One :== Succ Zero
+One :: One
+One = undef
+:: Two :== Succ (Succ Zero)
+Two :: Two
+Two = undef
+:: Three :== Succ (Succ (Succ Zero))
+Three :: Three
+Three = undef
+:: True = Tr
+:: False = Fs
+
+class Even a ~c
+where
+       isEven :: a -> c
+       isEven _ = undef
+class Odd a ~c
+where
+       isOdd :: a -> c
+       isOdd _ = undef
+instance Even Zero True
+instance Odd Zero False
+instance Even (Succ a) b | Odd a b
+instance Odd (Succ a) b | Even a b
+
+dec :: (Succ a) -> a
+dec _ = undef
+
+class Add a b ~c
+where
+       (:+:) infixl 6  :: a b -> c
+       (:+:) _ _ = undef
+instance Add Zero b b
+instance Add (Succ a) b (Succ c) | Add a b c
+
+class Mult a b ~c
+where
+       (:*:) infixl 7 :: a b -> c
+       (:*:) _ _ = undef
+instance Mult Zero b Zero
+instance Mult (Succ a) b d | Mult a b c & Add b c d
+
+class Pow a b ~c
+where
+       (:^:) infixr 8 :: a b -> c
+       (:^:) _ _ = undef
+instance Pow a Zero One
+instance Pow a (Succ b) d | Pow a b c & Mult a c d
+
+instance +++ {!a}
+where
+       (+++) l r =
+               {  'StdEnv'._createArray (size l+size r)
+               &  [i]=l.[i], [size l+j]=r.[j]
+               \\ i<-[0..size l-1] & j <- [0..size r-1]
+               }
+
+:: Vec n a = Vec {!a}
+
+empty :: Vec Zero a
+empty = Vec {}
+
+single :: a -> Vec (Succ Zero) a
+single a = Vec {a}
+
+length :: (Vec n a) -> n
+length _ = undef
+
+nrepeat :: n a -> Vec n a | toInt n
+nrepeat _ a = repeat a
+
+repeat :: a -> Vec n a | toInt n
+repeat a = let r = Vec (createArray (toInt (length r)) a) in r
+
+append :: (Vec n a) (Vec m a) -> Vec x a | Add n m x
+append (Vec a) (Vec b) = Vec (a +++ b)
+
+<<<<<<< HEAD
+//Start = nrepeat (Three :*: Three) 'a'
+
+v1 :: Vec (Succ (Succ Zero)) Int
+v1 = append (single 1) (single 32)
+
+v2 :: Vec Three Int
+v2 = repeat 5
+
+=======
+>>>>>>> 7675818dc8fc41eaf864dc89a8c2ce62c7dae93f
+class Le a b ~c
+where
+       le :: a b -> c
+       le _ _ = undef
+instance Le Zero b True
+instance Le (Succ a) Zero False
+instance Le (Succ a) (Succ b) c | Le a b c
+
+//Because toInt from StdEnv is strict in the first argument
+class toInt a :: a -> Int
+instance toInt Int where toInt i = i
+instance toInt Zero where toInt _ = 0
+instance toInt (Succ n) | toInt n where toInt a = inc (toInt (dec a))
+
+(!!) infixl 9 :: (Vec n a) i -> a | Le (Succ i) n True & toInt i
+(!!) (Vec a) i = a.[toInt i]
+
+(=.) infixl 9 :: (Vec n a) (i, a) -> Vec n a | Le (Succ i) n True & toInt i
+(=.) (Vec a) (i, x) = Vec {{e\\e<-:a} & [toInt i]=x}
+
+:: A = A; :: B = B; :: C = C; :: D = D; :: E = E; :: F = F; :: G = G; :: H = H;
+:: I = I; :: J = J; :: K = K; :: L = L; :: M = M; :: N = N; :: O = O; :: P = P;
+:: Q = Q; :: R = R; :: S = S; :: T = T; :: U = U; :: V = V; :: W = W; :: X = X;
+<<<<<<< HEAD
+:: Y = Y; :: Z = Z; :: Spc = Spc
+:: Nl = Nl
+:: SC l r = SC
+
+:: Cons x xs = Cons
+class HConcat a b ~c
+where
+       hconcat :: a b -> c
+       hconcat _ _ = undef
+instance HConcat () a a
+instance HConcat (Cons x xs) ys (Cons x zs) | HConcat xs ys zs
+
+:: FooS :== Cons F (Cons O (Cons O ()))
+FooS :: FooS
+FooS = undef
+:: BarS :== Cons B (Cons A (Cons A ()))
+BarS :: BarS
+BarS = undef
+
+:: NilS :== ()
+NilS :: NilS
+NilS = undef
+=======
+:: Y = Y; :: Z = Z;
+:: Nul = Nul
+:: SC l r = SC
+
+Start = nrepeat (Three :*: Three) 'a'
+
+e1 :: Vec (Succ (Succ Zero)) Int
+e1 = append (single 1) (single 32)
+
+e2 :: Vec Three Int
+e2 = repeat 5
+>>>>>>> 7675818dc8fc41eaf864dc89a8c2ce62c7dae93f