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 -> FToI $ 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 -> FToI $ floor val
> [1, 3, 123, 456]

-- check order independence
:p for i. case myTab.i of
  MyRight val -> FToI $ 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
  yieldAccum (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
  yieldAccum (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
  yieldAccum (AddMonoid Float) \ref.
    for i. case threeCaseTab.i of
      TheEmptyCase    -> ref += 1000.0
      ThePairCase x y -> ref +=  100.0 + y + IToF x
      TheIntCase x    -> ref +=   10.0 + IToF (x * 2)
> 2118.1

data MyIntish = MkIntish Int

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


:p
  f : MyPair Int Float -> Int =
    \(MkMyPair x y). x + (FToI $ 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 + (FToI $ 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 -> (FToI $ floor x)
    MyRight (MkMyPair x y) -> x + (FToI $ 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 =
  (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'.(fromOrdinal _ i')
      False -> ys'.(fromOrdinal _ (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 listToTable ((AsList n xs): List a) : (Fin n)=>a = xs

:t listToTable
> ((a:Type) ?-> (pat:(List a)) -> (Fin ((\((AsList n _)). n) pat)) => a)

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

def listToTable2 (l: List a) : (Fin (listLength l))=>a =
  (AsList _ xs) = l
  xs

:t listToTable2
> ((a:Type) ?-> (l:(List a)) -> (Fin ((\((AsList n _)). n) 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 (listLength l))=>Float =
  for i:(Fin $ listLength l). 0.0

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

data Graph a:Type =
  MkGraph n:Type nodes:(n=>a) m:Type edges:(m=>(n & n))

def graphToAdjacencyMatrix ((MkGraph n nodes m edges):Graph a) : n=>n=>Bool =
  init = for i j. False
  yieldState init \mRef.
    for i:m.
      (from, to) = edges.i
      mRef!from!to := True

:t graphToAdjacencyMatrix
> ((a:Type)
>  ?-> (pat:(Graph a))
>  -> ((\((MkGraph n _ _ _)). n) pat) => ((\((MkGraph n _ _ _)). n) pat) => Bool)

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

-- Test how (nested) projections are handled and pretty-printed.

def pairUnpack ((v, _):(Int & Float)) : Int = v
:p pairUnpack
> \pat:(Int32 & Float32). (\(a, _). a) pat

def adtUnpack ((MkMyPair v _):MyPair Int Float) : Int = v
:p adtUnpack
> \pat:(MyPair Int32 Float32). (\((MkMyPair elt _)). elt) pat

def recordUnpack ({a=v, b=_}:{a:Int & b:Float}) : Int = v
:p recordUnpack
> \pat:{a: Int32 & b: Float32}. (\{a = a, b = _}. a) pat

def nestedUnpack (x:MyPair Int (MyPair (MyIntish & Int) Int)) : Int =
  (MkMyPair _ (MkMyPair (MkIntish y, _) _)) = x
  y

:p nestedUnpack
> \x:(MyPair Int32 (MyPair (MyIntish & Int32) Int32)).
>   (\((MkIntish (((MkMyPair ((MkMyPair _ elt)) _)), _))). elt) x

:p nestedUnpack (MkMyPair 3 (MkMyPair (MkIntish 4, 5) 6))
> 4

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). toList [(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])) ])