content: module ListLen_LType (llen) where
  
  import Language.Haskell.Liquid.Prelude
  
  {-@  
  data List [llen] a <p :: x0:a -> x1:a -> Bool>  
    = Nil 
    | Cons (h :: a) (t :: List <p> (a <p h>))
  @-}
  
  {-@ measure llen @-}
  llen :: (List a) -> Int
  {-@ llen :: List a -> Nat @-}
  llen Nil         = 0
  llen (Cons x xs) = 1 + (llen xs)
  
  data List a = Nil | Cons a (List a)
  
  make2d :: a -> Int -> Int -> List ([a])
  make2d x n m = cloneL (clone x n) m
  
  {-@ invariant {v:Int | v >= 0} @-}
  
  clone :: a -> Int -> [a]
  clone x n
    | n == 0
    = []
    | otherwise 
    = x : (clone x (n-1))
  
  cloneL :: a -> Int -> List a
  cloneL x n
    | n == 0
    = Nil
    | otherwise 
    = Cons x  (cloneL x (n-1))
  
  -- check [] = [liquidAssertB True]
  -- check (xs:xss) = let n = length xs in map (\xs' -> liquidAssertB (length xs' == n)) xss
  
  chk :: List [a] -> Bool
  chk Nil = liquidAssertB True
  chk (Cons xs xss) =
    case xss of 
     (Cons xs1 xss1) -> let n = length xs in liquidAssertB (length xs1 == n) && chk xss
     Nil -> liquidAssertB True
  
  fooL  = Cons [1, 1, 3] (Cons [2, 2, 5] Nil)
  fooL1 = make2d 0 n m
    where n = choose 0
          m = choose 1
  
  propL = chk fooL1
  prop  = chk fooL
  