path: root/tests/adt-tests.dx

data IntFloat =
  MkIntFloat(Int, Float)

:p
  case MkIntFloat 1 2.3 of
    MkIntFloat(x, y) -> (x, y)
> (1, 2.3)

data MyPair(a:Type, b:Type) =
   MkMyPair(a, b)

z = MkMyPair (+1) 2.3

:p z
> (MkMyPair 1 2.3)

:t z
> (MyPair Int32 Float32)

:p
  case z of
    MkMyPair(x, y) -> (x, y)
> (1, 2.3)

data Dual(a:Type) =
   MkDual(a, a)

:p
  d = MkDual 1 2
  case d of
    MkDual(x, y) -> (x, y)
> (1, 2)

:p for i:(Fin 3). MkMyPair (ordinal i) (ordinal i + 1)
> [(MkMyPair 0 1), (MkMyPair 1 2), (MkMyPair 2 3)]

zz = MkMyPair(1, MkMyPair(True, 2.3))

MkMyPair(z1, MkMyPair(z2, z3)) = zz

:p (z1, z2, z3)
> (1, True, 2.3)

:p
  tabOfPairs = for i:(Fin 3). MkMyPair (ordinal i) (ordinal i + 1)
  for i.
   case tabOfPairs[i] of
     -- TODO: investigate shadowing bug if we call these a and b
     MkMyPair(x, y) -> (x + y, y)
> [(1, 1), (3, 2), (5, 3)]

data MyEither(a:Type, b:Type) =
  MyLeft (a)
  MyRight(b)

x : MyEither Int Float = MyLeft 1

:p x
> (MyLeft 1)

:p
  (MyLeft x') = x
  x
> Type error:sum type constructor in can't-fail pattern
>
>   (MyLeft x') = x
>    ^^^^^^^^^

:p
  case x of
    MyLeft  val -> val
    MyRight val -> f_to_i $ floor val
> 1

-- %passes imp
myTab = [MyLeft (+1), MyRight 3.5, MyLeft 123, MyLeft 456]

:p myTab
> [(MyLeft 1), (MyRight 3.5), (MyLeft 123), (MyLeft 456)]

:p for i. case myTab[i] of
  MyLeft( val) -> val
  MyRight(val) -> f_to_i $ floor val
> [1, 3, 123, 456]

-- check order independence
:p for i. case myTab[i] of
  MyRight(val) -> f_to_i $ floor val
  MyLeft( val) -> val
> [1, 3, 123, 456]

-- test non-exhaustive patterns
:p for i. case myTab[i] of
  MyLeft  val -> val
> Runtime error

:p for i. case myTab[i] of
  MyLeft  val -> val
  MyRight _   -> error "nope"
> nope
> Runtime error

:p
  yield_accum (AddMonoid Float) \ref.
    for i. case myTab[i] of
      MyLeft tmp -> ()
      MyRight val -> ref += 1.0 + val
> 4.5

:p
  -- check that the order of the case alternatives doesn't matter
  yield_accum (AddMonoid Float) \ref.
    for i. case myTab[i] of
      MyRight val -> ref += 1.0 + val
      MyLeft tmp -> ()
> 4.5

data ThreeCases =
  TheEmptyCase
  TheIntCase(Int)
  ThePairCase(Int, Float)

threeCaseTab : (Fin 4)=>ThreeCases =
  [TheIntCase 3, TheEmptyCase, ThePairCase 2 0.1, TheEmptyCase]

:p threeCaseTab
> [(TheIntCase 3), TheEmptyCase, (ThePairCase 2 0.1), TheEmptyCase]

:p
  yield_accum (AddMonoid Float) \ref.
    for i. case threeCaseTab[i] of
      TheEmptyCase      -> ref += 1000.0
      ThePairCase(x, y) -> ref +=  100.0 + y + i_to_f x
      TheIntCase x      -> ref +=   10.0 + i_to_f (x * 2)
> 2118.1

data MyIntish = MkIntish(Int)

:p case MkIntish 1 of MkIntish x -> x
> 1


:p
  f : (MyPair Int Float) -> Int =
    \p.
       MkMyPair(x, y) = p
       x + (f_to_i $ floor y)
  f (MkMyPair 1 2.3)
> 3

:p
  pairs = [MkMyPair 2 z,  MkMyPair(2, (MkMyPair 4 3.4))]
  for i.
    MkMyPair(x, MkMyPair(y, z)) = pairs[i]
    x + y + (f_to_i $ floor z)
> [5, 9]

:p
  xs = [MyLeft 1.0, MyLeft 2.0, MyRight (MkMyPair 3 4.0)]
  for i. case xs[i] of
    MyLeft x -> (f_to_i $ floor x)
    MyRight (MkMyPair(x, y)) -> x + (f_to_i $ floor y)
> [1, 2, 7]

xsList = AsList(_, [1,2,3])

:p
  AsList(_, xsTab) = xsList
  sum xsTab
> 6

AsList(_, xsTab) = xsList

:p xsTab
> [1, 2, 3]

:p
  xs = AsList(_, [1,2,3])
  ys = AsList(_, [4,5])
  AsList(_, ans) = xs <> ys
  sum ans
> 15

:p
  MkMyPair(x, y) = case 3 < 2 of
    True  -> MkMyPair 1 2
    False -> MkMyPair 3 4
  (x, y)
> (3, 4)

def catLists (xs:List a, ys:List a) -> List a given (a) =
  AsList(nx, xs') = xs
  AsList(ny, ys') = ys
  nz = nx + ny
  zs = for i:(Fin nz).
    i' = ordinal i
    case i' < nx of
      True  -> xs'[from_ordinal i']
      False -> ys'[from_ordinal (unsafe_nat_diff i' nx)]
  AsList _ zs

:p
  AsList(_, xs) = catLists (AsList(_, [1,2,3])) (AsList _ [4,5])
  sum xs
> 15

:p catLists (AsList _ [1,2,3]) (AsList _ [4,5])
> (AsList 5 [1, 2, 3, 4, 5])

:p
  n = 1 + 4
  AsList _ (for i:(Fin n). ordinal i)
> (AsList 5 [0, 1, 2, 3, 4])



def listToTable2 (l: List a) -> (Fin (list_length l))=>a given (a) =
  AsList(_, xs) = l
  xs

:t listToTable2
> ({a:Type}(l:(List a)) ->   ((Fin (ProjectElt 0 (ProjectElt u l))) => a))

:p
  l = AsList _ [1, 2, 3]
  sum $ listToTable2 l
> 6

l2 = AsList _ [1, 2, 3]
:p sum $ listToTable2 l2
> 6

def zerosLikeList (l : List a) -> (Fin (list_length l))=>Float given (a) =
  for i:(Fin $ list_length l). 0.0

:p zerosLikeList l2
> [0., 0., 0.]

data Graph(n|Ix, a:Type) =
  MkGraph(nodes:(n=>a), edges:(List (n, n)))

def graphToAdjacencyMatrix (g:Graph n a) -> n=>n=>Bool given (n|Ix, a) =
  MkGraph(nodes, AsList(_, edges)) = g
  init = for i j. False
  yield_state init \mRef.
    for i.
      (from, to) = edges[i]
      mRef!from!to := True

:t graphToAdjacencyMatrix
> ({n:Type}[d:(Ix n)]{a:Type}(g:(Graph n a)) ->   (n => n => Bool))

:p
  g : Graph (Fin 3) Int = MkGraph [5, 6, 7] $ AsList _ [(0@_, 1@_), (0@_, 2@_), (2@_, 0@_), (1@_, 1@_)]
  graphToAdjacencyMatrix g
> [[False, True, True], [False, True, False], [True, False, False]]

data MySum =
  Foo(Float)
  Bar(String)

-- bug #348
:p
  xs = for i:(Fin 3).
    if ordinal i < 2
      then Foo 2.0
      else Foo 1.0
  (xs, xs)
> ([(Foo 2.), (Foo 2.), (Foo 1.)], [(Foo 2.), (Foo 2.), (Foo 1.)])

data MySum2 =
  Foo2
  Bar2 (Fin 3 => Int)

-- bug #348
:p concat for i:(Fin 4). AsList _ [(Foo2, Foo2)]
> (AsList 4 [(Foo2, Foo2), (Foo2, Foo2), (Foo2, Foo2), (Foo2, Foo2)])

-- reproducer for a shadowing bug (PR #440)
:p concat $ for i:(Fin 2). to_list [(Just [0,0,0], Just [0,0,0]), (Just [0,0,0], Just [0,0,0])]
> (AsList 4 [((Just [0, 0, 0]), (Just [0, 0, 0])), ((Just [0, 0, 0]), (Just [0, 0, 0])), ((Just [0, 0, 0]), (Just [0, 0, 0])), ((Just [0, 0, 0]), (Just [0, 0, 0]))])