content: module Termination where
  
  import Prelude hiding (sum)
  
  type Value = Int
  
  type Vec = Int -> Value
  
  {-@ sum :: Vec -> Nat -> Value @-}
  sum :: Vec -> Int -> Value
  sum a 0 = a 0
  sum a i = a i + sum a (i-1)
  
  {-@ sum' :: Vec -> Value -> n:Nat -> Value / [n] @-}
  sum' :: Vec -> Value -> Int -> Value
  sum' a acc 0 = acc + a 0
  sum' a acc i = sum' a (acc + a i) (i-1)
  
  type Vec2D = Int -> Int -> Value
  
  {-@ sum2D :: Vec2D -> Nat -> Nat -> Value @-}
  sum2D :: Vec2D -> Int -> Int -> Value
  sum2D a n m = go n m
    where
      {-@ go :: ink:Nat -> joe:Nat -> Value / [ink, joe] @-}
      go 0 0        = a 0 0
      go i j
        | j == 0    =  a i 0 + go (i-1) m
        | otherwise =  a i j + go i (j-1)
  
  {-@ sumFromTo :: Vec -> lo:Nat -> hi:{v:Nat|v>=lo} -> Value @-}
  sumFromTo :: Vec -> Int -> Int ->  Value
  sumFromTo a lo hi = go lo hi
    where
      {-@ go :: lo:Nat -> hi:{v:Nat | v >= lo} -> Value / [hi-lo] @-}
      go :: Int -> Int -> Value
      go lo hi 
        | lo == hi  =  a lo
        | otherwise =  a lo + go (lo + 1) hi
  
  {-@ sumFrom2 :: Vec -> lo:Nat -> hi:{v:Nat | lo <= v } -> Value @-}
  sumFrom2 :: Vec -> Int -> Int ->  Value
  sumFrom2 a lo hi = go lo
    where
      {-@ go :: lo:_ -> _ / [hi - lo] @-}
      go :: Int -> Value
      go lo
        | lo == hi  =  a lo
        | otherwise =  a lo + go (lo + 1)
  
  