module S06 (
  -- * Exercises 2
  -- | See <../pdfs/06.pdf>.

  -- * Exericse 3
  root,

  -- * Exericse 4
  nested,
  
  -- * Exercise 5
  cbn,

  -- * Exercise 6
  equals
  ) where
import BTree (BTree(..))
import qualified BTree
import Term
import Data.List

type Strat = Term -> [Term]

root :: Strat
root (App (Abs x t) u) = [subst x u t]
root _ = []

nested :: Strat -> Strat
nested _ (Var _) = []
nested s (App t u) = map (`App` u) (s t) ++ map (App t) (s u)
nested s (Abs x t) = map (Abs x) (s t)

leftmost :: Strat -> Strat
leftmost s t = case s t of
  [] -> []
  rs -> [head rs]

isWhnf :: Term -> Bool
isWhnf (Var _) = True
isWhnf (Abs _ _) = True
isWhnf (App (Abs _ _) _) = False
isWhnf (App t _) = isWhnf t

-- call by name reduction
cbn :: Strat
cbn t =
  if isWhnf t then []
  else case root t of
    [] -> leftmost (nested cbn) t
    rs -> rs

newtype Set a = Set (BTree a)

isSubset :: Ord a => Set a -> Set a -> Bool
Set t `isSubset` Set u = t `isSubtree` u
  where
    isSubtree Empty _       = True
    isSubtree (Node x l r) t =
      x `memTree` t && l `isSubtree` t && r `isSubtree` t

equals :: Ord a => Set a -> Set a -> Bool
equals s t = s `isSubset` t && t `isSubset` s

memTree x Empty = False
memTree x (Node y l r) =
  case compare x y of
    EQ -> True
    LT -> x `memTree` l
    GT -> x `memTree` r