content: {-@ LIQUID "--no-termination" @-}
  {-@ LIQUID "--short-names"    @-}
  {-@ LIQUID "--fullcheck"      @-}
  {-@ LIQUID "--maxparams=3"    @-}
  
  -- | An example from "A Relational Framework for Higher-Order Shape Analysis",
  --   by Gowtham Kaki Suresh Jagannathan, ICFP 2014.
  
  module AlphaConvert (subst, alpha) where
  
  import Prelude hiding ((++), elem)
  import Data.Set (Set (..))
  import Language.Haskell.Liquid.Prelude   
  
  alpha  :: [Bndr] -> Expr -> Expr 
  subst  :: Expr -> Bndr -> Expr -> Expr
  maxs   :: [Int] -> Int 
  lemma1 :: Int -> [Int] -> Bool
  fresh  :: [Bndr] -> Bndr
  free   :: Expr -> [Bndr]
  
  ---------------------------------------------------------------------
  -- | Datatype Definition --------------------------------------------
  ---------------------------------------------------------------------
  
  type Bndr 
    = Int
  
  data Expr 
    = Var Bndr  
    | Abs Bndr Expr
    | App Expr Expr
  
  {-@ measure fv       :: Expr -> (Set Bndr)
      fv (Var x)       = (Set_sng x)
      fv (Abs x e)     = (Set_dif (fv e) (Set_sng x))
      fv (App e a)     = (Set_cup (fv e) (fv a)) 
    @-}
  
  {-@ measure isAbs    :: Expr -> Prop
      isAbs (Var v)    = false
      isAbs (Abs v e)  = true
      isAbs (App e a)  = false             
    @-}
  
  {-@ predicate AddV E E2 X E1   = fv E = Set_cup (Set_dif (fv E2) (Set_sng X)) (fv E1) @-}
  {-@ predicate EqV E1 E2        = fv E1 = fv E2                                        @-}
  {-@ predicate Occ X E          = Set_mem X (fv E)                                     @-}
  {-@ predicate Subst E E1 X E2  = if (Occ X E2) then (AddV E E2 X E1) else (EqV E E2)  @-}
  
  ----------------------------------------------------------------------------
  -- | Part 5: Capture Avoiding Substitution ---------------------------------
  ----------------------------------------------------------------------------
  {-@ subst :: e1:Expr -> x:Bndr -> e2:Expr -> {e:Expr | Subst e e1 x e2} @-} 
  ----------------------------------------------------------------------------
  
  subst e1 x e2@(Var y)
    | x == y                = e1
    | otherwise             = e2
  
  subst e1 x (App ea eb)    = App ea' eb'
    where
      ea'                   = subst e1 x ea
      eb'                   = subst e1 x eb
  
  subst e1 x e2@(Abs y e)  
    | x == y                = e2
    | y `elem` xs           = subst e1 x (alpha xs e2) 
    | otherwise             = Abs y      (subst e1 x e)
       where
        xs                  = free e1 
  
  ----------------------------------------------------------------------------
  -- | Part 4: Alpha Conversion ----------------------------------------------
  ----------------------------------------------------------------------------
  {-@ alpha :: ys:[Bndr] -> e:{Expr | isAbs e} -> {v:Expr | EqV v e} @-}
  ----------------------------------------------------------------------------
  alpha ys (Abs x e) = Abs x' (subst (Var x') x e)
    where 
      xs             = free e
      x'             = fresh (x : ys ++ xs)
  
  alpha _  _         = liquidError "never"
  
  
  ----------------------------------------------------------------------------
  -- | Part 3: Fresh Variables -----------------------------------------------
  ----------------------------------------------------------------------------
  {-@ fresh :: xs:[Bndr] -> {v:Bndr | NotElem v xs} @-}
  ----------------------------------------------------------------------------
  fresh bs = liquidAssert (lemma1 n bs) n
    where 
      n    = 1 + maxs bs
  
  {-@ maxs :: xs:_ -> {v:_ | v = maxs xs} @-}
  maxs ([])   = 0
  maxs (x:xs) = if (x > maxs xs) then x else (maxs xs) 
   
   
  {-@ measure maxs :: [Int] -> Int 
      maxs ([])   = 0
      maxs (x:xs) = if (x > maxs xs) then x else (maxs xs) 
    @-}
  
  {-@ lemma1 :: x:Int -> xs:{[Int] | x > maxs xs} -> {v:Bool | Prop v && NotElem x xs} @-}
  lemma1 _ []     = True 
  lemma1 x (_:ys) = lemma1 x ys 
  
  
  ----------------------------------------------------------------------------
  -- | Part 2: Free Variables ------------------------------------------------
  ----------------------------------------------------------------------------
  
  ----------------------------------------------------------------------------
  {-@ free         :: e:Expr -> {v:[Bndr] | elts v = fv e} @-}
  ----------------------------------------------------------------------------
  free (Var x)     = [x]
  free (App e e')  = free e ++ free e'
  free (Abs x e)   = free e \\ x
  
  
  ----------------------------------------------------------------------------
  -- | Part I: Sets with Lists -----------------------------------------------
  ----------------------------------------------------------------------------
  
  {-@ predicate IsCup X Y Z  = elts X = Set_cup (elts Y) (elts Z)    @-}
  {-@ predicate IsDel X Y Z  = elts X = Set_dif (elts Y) (Set_sng Z) @-}
  {-@ predicate Elem  X Ys   = Set_mem X (elts Ys)                   @-}
  {-@ predicate NotElem X Ys = not (Elem X Ys)                       @-}
  
  {-@ (++)      :: xs:[a] -> ys:[a] -> {v:[a] | IsCup v xs ys}  @-}
  []     ++ ys  = ys
  (x:xs) ++ ys  = x : (xs ++ ys)
  
  {-@ (\\)      :: (Eq a) => xs:[a] -> y:a -> {v:[a] | IsDel v xs y} @-}
  xs   \\ y     = [x | x <- xs, x /= y]
  
  {-@ elem      :: (Eq a) => x:a -> ys:[a] -> {v:Bool | Prop v <=> Elem x ys} @-}
  elem x []     = False
  elem x (y:ys) = x == y || elem x ys
   
  {-@ measure elts :: [a] -> (Set a) 
      elts ([])    = {v | Set_emp v}
      elts (x:xs)  = {v | v = Set_cup (Set_sng x) (elts xs) }
    @-}
  