content: module Termination where
  
  import Prelude hiding (gcd, mod, map, repeat, take)
  import Language.Haskell.Liquid.Prelude
  
  fac   :: Int -> Int
  
  -------------------------------------------------------------------------
  -- | Simple Termination
  -------------------------------------------------------------------------
  
  {-@ fac :: Nat -> Nat @-}
  fac 0 = 1
  fac 1 = 1
  fac n = n * fac (n-1)
  
  
  
  
  -------------------------------------------------------------------------
  -- | Semantic Termination
  -------------------------------------------------------------------------
  
  gcd :: Int -> Int -> Int
  gcd a 0 = a
  gcd a b = gcd b (a `mod` b)
  
  
  mod :: Int -> Int -> Int
  mod a b | a - b >  b = mod (a - b) b
          | a - b <  b = a - b
          | a - b == b = 0
  
  -------------------------------------------------------------------------
  -- | Explicit Metrics #1 
  -------------------------------------------------------------------------
  
  tfac       :: Int -> Int -> Int
  tfac acc 0 = acc
  tfac acc n = tfac (n * acc) (n-1)
  
  
  
  
  -------------------------------------------------------------------------
  -- Explicit Metrics #2 
  -------------------------------------------------------------------------
  
  range :: Int -> Int -> [Int]
  range lo hi
    | lo < hi   = lo : range (lo + 1) hi
    | otherwise = []
  
  
  
  -------------------------------------------------------------------------
  -- | Structural Recursion 
  -------------------------------------------------------------------------
  
  data List a = N | C a (List a)
  
  {-@ measure size @-}
  size          :: List a -> Int 
  size (C x xs) = 1 + size xs
  size (N)      = 0
  
  
  map            :: (a -> b) -> List a -> List b
  map _ N        = N
  map f (C x xs) = f x `C` map f xs
  
  
  
  -------------------------------------------------------------------------
  -- | Default Metrics
  -------------------------------------------------------------------------
  
  map'            :: (a -> b) -> List a -> List b
  map' _ N        = N
  map' f (C x xs) = f x `C` map' f xs
  
  
  
  
  
  
  -------------------------------------------------------------------------
  -- | Termination Expressions Metrics
  -------------------------------------------------------------------------
  
  merge          :: (Ord a) => List a -> List a -> List a
  
  merge (C x xs) (C y ys)
    | x < y      = x `C` merge xs (y `C` ys)
    | otherwise  = y `C` merge (x `C` xs) ys
  merge _   ys   = ys
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  --------------------------------------------------------------------------------
  -- | CHEAT AREA ----------------------------------------------------------------
  --------------------------------------------------------------------------------
  
  -- # START ERRORS 8
  -- # END ERRORS   0
  
  {- gcd   :: a:Nat -> b:{v:Nat | v < a} -> Int @-}
  {- mod   :: a:Nat -> b:{v:Nat| 0 < v && v < a} -> {v:Nat | v < b} @-}
  {- tfac  :: Nat -> n:Nat -> Nat / [n] @-}
  {- range :: lo:Nat -> hi:Nat -> [Nat] / [hi-lo] @-}
  {- map   :: (a -> b) -> xs:List a -> (List b) / [size xs] @-}
  {- merge :: xs:_ -> ys:_ -> _ / [size xs + size ys] @-}
  {- data List [size] a = N | C {x :: a, xs :: List a } @-}
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  
  --------------------------------------------------------------------------------
  -- | BOILERPLATE ---------------------------------------------------------------
  --------------------------------------------------------------------------------
                   
  {-@ invariant {v : List a | 0 <= size v} @-}
  
  