fundeps/test.icl

   1 module test
   2
   3 import qualified StdEnv
   4 import StdEnv => qualified isEven, isOdd, class toInt(toInt), instance toInt Int
   5
   6 :: Zero = Zero
   7 :: Succ a = Succ
   8 :: One :== Succ Zero
   9 One :: One
  10 One = undef
  11 :: Two :== Succ (Succ Zero)
  12 Two :: Two
  13 Two = undef
  14 :: Three :== Succ (Succ (Succ Zero))
  15 Three :: Three
  16 Three = undef
  17 :: True = Tr
  18 :: False = Fs
  19
  20 class Even a ~c
  21 where
  22         isEven :: a -> c
  23         isEven _ = undef
  24 class Odd a ~c
  25 where
  26         isOdd :: a -> c
  27         isOdd _ = undef
  28 instance Even Zero True
  29 instance Odd Zero False
  30 instance Even (Succ a) b | Odd a b
  31 instance Odd (Succ a) b | Even a b
  32
  33 dec :: (Succ a) -> a
  34 dec _ = undef
  35
  36 class Add a b ~c
  37 where
  38         (:+:) infixl 6  :: a b -> c
  39         (:+:) _ _ = undef
  40 instance Add Zero b b
  41 instance Add (Succ a) b (Succ c) | Add a b c
  42
  43 class Mult a b ~c
  44 where
  45         (:*:) infixl 7 :: a b -> c
  46         (:*:) _ _ = undef
  47 instance Mult Zero b Zero
  48 instance Mult (Succ a) b d | Mult a b c & Add b c d
  49
  50 class Pow a b ~c
  51 where
  52         (:^:) infixr 8 :: a b -> c
  53         (:^:) _ _ = undef
  54 instance Pow a Zero One
  55 instance Pow a (Succ b) d | Pow a b c & Mult a c d
  56
  57 instance +++ {!a}
  58 where
  59         (+++) l r =
  60                 {  'StdEnv'._createArray (size l+size r)
  61                 &  [i]=l.[i], [size l+j]=r.[j]
  62                 \\ i<-[0..size l-1] & j <- [0..size r-1]
  63                 }
  64
  65 :: Vec n a = Vec {!a}
  66
  67 empty :: Vec Zero a
  68 empty = Vec {}
  69
  70 single :: a -> Vec (Succ Zero) a
  71 single a = Vec {a}
  72
  73 length :: (Vec n a) -> n
  74 length _ = undef
  75
  76 nrepeat :: n a -> Vec n a | toInt n
  77 nrepeat _ a = repeat a
  78
  79 repeat :: a -> Vec n a | toInt n
  80 repeat a = let r = Vec (createArray (toInt (length r)) a) in r
  81
  82 append :: (Vec n a) (Vec m a) -> Vec x a | Add n m x
  83 append (Vec a) (Vec b) = Vec (a +++ b)
  84
  85 class Le a b ~c
  86 where
  87         le :: a b -> c
  88         le _ _ = undef
  89 instance Le Zero b True
  90 instance Le (Succ a) Zero False
  91 instance Le (Succ a) (Succ b) c | Le a b c
  92
  93 //Because toInt from StdEnv is strict in the first argument
  94 class toInt a :: a -> Int
  95 instance toInt Int where toInt i = i
  96 instance toInt Zero where toInt _ = 0
  97 instance toInt (Succ n) | toInt n where toInt a = inc (toInt (dec a))
  98
  99 (!!) infixl 9 :: (Vec n a) i -> a | Le (Succ i) n True & toInt i
 100 (!!) (Vec a) i = a.[toInt i]
 101
 102 (=.) infixl 9 :: (Vec n a) (i, a) -> Vec n a | Le (Succ i) n True & toInt i
 103 (=.) (Vec a) (i, x) = Vec {{e\\e<-:a} & [toInt i]=x}
 104
 105 :: A = A; :: B = B; :: C = C; :: D = D; :: E = E; :: F = F; :: G = G; :: H = H;
 106 :: I = I; :: J = J; :: K = K; :: L = L; :: M = M; :: N = N; :: O = O; :: P = P;
 107 :: Q = Q; :: R = R; :: S = S; :: T = T; :: U = U; :: V = V; :: W = W; :: X = X;
 108 :: Y = Y; :: Z = Z;
 109 :: Nul = Nul
 110 :: SC l r = SC
 111
 112 Start = nrepeat (Three :*: Three) 'a'
 113
 114 e1 :: Vec (Succ (Succ Zero)) Int
 115 e1 = append (single 1) (single 32)
 116
 117 e2 :: Vec Three Int
 118 e2 = repeat 5