fundeps/test.icl

   1 module test
   2
   3 import qualified StdEnv
   4 import StdEnv => qualified isEven, isOdd, class toInt(..), instance toInt Int, class toString(..)
   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 <<<<<<< HEAD
  86 //Start = nrepeat (Three :*: Three) 'a'
  87
  88 v1 :: Vec (Succ (Succ Zero)) Int
  89 v1 = append (single 1) (single 32)
  90
  91 v2 :: Vec Three Int
  92 v2 = repeat 5
  93
  94 =======
  95 >>>>>>> 7675818dc8fc41eaf864dc89a8c2ce62c7dae93f
  96 class Le a b ~c
  97 where
  98         le :: a b -> c
  99         le _ _ = undef
 100 instance Le Zero b True
 101 instance Le (Succ a) Zero False
 102 instance Le (Succ a) (Succ b) c | Le a b c
 103
 104 //Because toInt from StdEnv is strict in the first argument
 105 class toInt a :: a -> Int
 106 instance toInt Int where toInt i = i
 107 instance toInt Zero where toInt _ = 0
 108 instance toInt (Succ n) | toInt n where toInt a = inc (toInt (dec a))
 109
 110 (!!) infixl 9 :: (Vec n a) i -> a | Le (Succ i) n True & toInt i
 111 (!!) (Vec a) i = a.[toInt i]
 112
 113 (=.) infixl 9 :: (Vec n a) (i, a) -> Vec n a | Le (Succ i) n True & toInt i
 114 (=.) (Vec a) (i, x) = Vec {{e\\e<-:a} & [toInt i]=x}
 115
 116 :: A = A; :: B = B; :: C = C; :: D = D; :: E = E; :: F = F; :: G = G; :: H = H;
 117 :: I = I; :: J = J; :: K = K; :: L = L; :: M = M; :: N = N; :: O = O; :: P = P;
 118 :: Q = Q; :: R = R; :: S = S; :: T = T; :: U = U; :: V = V; :: W = W; :: X = X;
 119 <<<<<<< HEAD
 120 :: Y = Y; :: Z = Z; :: Spc = Spc
 121 :: Nl = Nl
 122 :: SC l r = SC
 123
 124 :: Cons x xs = Cons
 125 class HConcat a b ~c
 126 where
 127         hconcat :: a b -> c
 128         hconcat _ _ = undef
 129 instance HConcat () a a
 130 instance HConcat (Cons x xs) ys (Cons x zs) | HConcat xs ys zs
 131
 132 :: FooS :== Cons F (Cons O (Cons O ()))
 133 FooS :: FooS
 134 FooS = undef
 135 :: BarS :== Cons B (Cons A (Cons A ()))
 136 BarS :: BarS
 137 BarS = undef
 138
 139 :: NilS :== ()
 140 NilS :: NilS
 141 NilS = undef
 142 =======
 143 :: Y = Y; :: Z = Z;
 144 :: Nul = Nul
 145 :: SC l r = SC
 146
 147 Start = nrepeat (Three :*: Three) 'a'
 148
 149 e1 :: Vec (Succ (Succ Zero)) Int
 150 e1 = append (single 1) (single 32)
 151
 152 e2 :: Vec Three Int
 153 e2 = repeat 5
 154 >>>>>>> 7675818dc8fc41eaf864dc89a8c2ce62c7dae93f