content: {-# LANGUAGE DeriveTraversable, FlexibleInstances #-}
  
  module Full where
  
  import Debug.Trace
  
  data Fm' x -- yer maw
    = V x         -- the variable
    | Z           -- zero
    | D (Fm' x)   -- double
    | S (Fm' x)   -- successor
    | F (Fm' x)   -- full
    deriving (Eq, Ord, Functor, Foldable, Traversable)
  
  type Var = Int
  type Fm = Fm' Var
  
  db :: Fm -> Fm
  db  Z    = Z
  db (S f) = S (S (db f))
  db    f  = D f
  
  fu :: Fm -> Fm
  fu  Z    = Z
  fu (S f) = S (db (fu f))
  fu    f  = F f
  
  type Store =
    ( Int -- name supply
    , [(Var, Fm)] -- defs var = nm
    )
  
  nm :: Fm -> Store -> Fm
  nm (V x) ga = va x ga
  nm  Z    ga = Z
  nm (S f) ga = S (nm f ga)
  nm (D f) ga = db (nm f ga)
  nm (F f) ga = fu (nm f ga)
  
  va :: Var -> Store -> Fm
  va x (_ , xns) = case lookup x xns of
    Just n  -> n
    Nothing -> V x
  
  -- you *have* done the occur check, haven't you?
  gro :: Var -> Fm -> Store -> Store
  gro x f (k, xns) = (k, (x, f) : map (sb x f <$>) xns)
  
  sb :: Var -> Fm -> Fm -> Fm
  sb x f (V y) = if x == y then f else V y
  sb x f  Z    = Z
  sb x f (S g) = S (sb x f g)
  sb x f (D g) = db (sb x f g)
  sb x f (F g) = fu (sb x f g)
  
  unify :: Fm -> Fm -> Store -> Maybe Store
  unify f g ga = go (nm f ga) (nm g ga) where
    go f g | trace (show f ++ " =? " ++ show g) False = undefined
    go f g | f == g = pure ga
    go f g | f > g  = go g f
    go (V x) g = case occ x g of
      False -> pure (gro x g ga)
      True  -> zee g ga
    go  Z    g = zee g ga
    go (D f) g = do
      (h, ga) <- evn g ga
      unify f h ga
    go (S f) g = do
      (h, ga) <- suu g ga
      unify f h ga
    go (F f) (F g) = go f g
    go _ _ = Nothing
  
  occ :: Int -> Fm -> Bool
  occ x = any (x ==)
  
  -- Fm is normal
  zee :: Fm -> Store -> Maybe Store
  zee (V x) ga = pure (gro x Z ga)
  zee  Z    ga = Just ga
  zee (S _) ga = Nothing
  zee (D f) ga = zee f ga
  zee (F f) ga = zee f ga
  
  -- Fm is normal
  suu :: Fm -> Store -> Maybe (Fm, Store)
  suu (V x) (k, xns) = pure (V k, gro x (S (V k)) (k+1, xns))
  suu Z ga = Nothing
  suu (S f) ga = pure (f, ga)
  suu (D f) ga = do
    (g, ga) <- suu f ga
    pure (S (db g), ga)
  suu (F f) ga = do
    (g, ga) <- suu f ga
    pure (db (fu g), ga)
  
  -- Fm is normal
  evn :: Fm -> Store -> Maybe (Fm, Store)
  evn (V x) (k, xns) = pure (V k, gro x (D (V k)) (k+1, xns))
  evn Z ga = pure (Z, ga)
  evn (S f) ga = do
    (g, ga) <- ood f ga
    pure (S g, ga)
  evn (D f) ga = pure (f, ga)
  evn (F f) ga = do
    ga <- zee f ga
    pure (Z, ga)
  
  -- Fm is normal
  ood :: Fm -> Store -> Maybe (Fm, Store)
  ood (V x) (k, xns) = pure (V k, gro x (S (D (V k))) (k+1, xns))
  ood Z _ = Nothing
  ood (S f) ga = do
    (g, ga) <- evn f ga
    pure (g, ga)
  ood (D _) _ = Nothing
  ood (F f) ga = do
    (g, ga) <- suu f ga
    pure (fu g, ga)
  
  
  instance Show Fm where
    show f = go (nm f (0, [])) where
      go (V x) = "V" ++ show x
      go Z = "0"
      go (S f) = mo 1 f where
        mo :: Integer -> Fm -> String
        mo k Z = show k
        mo k (S f) = mo (k+1) f
        mo k f = show k ++ "+" ++ go f
      go (D f) = mo 1 f where
        mo :: Integer -> Fm -> String
        mo k (D f) = mo (k+1) f
        mo k f = po k ++ "*" ++ go f
        po i = if length a <= length b then a else b where
          a = show (2 ^ i)
          b = "2^" ++ show i
      go (F f) = "[" ++ go f ++ "]"
  
  instance Num Fm where
    fromInteger 0 = Z
    fromInteger n = S (fromInteger (n - 1))
    Z + f = f
    f + Z = f
    S f + g = S (f + g)
    f + S g = S (f + g)
    D f + D g = db (f + g)
    x + y | x == y = db x
    Z * f = Z
    f * Z = Z
    S f * g = g + (f * g)
    f * S g = f + (f * g)
    D f * g = db (f * g)
    f * D g = db (f * g)
    negate Z = Z
    signum Z = Z
    signum _ = S Z
    abs x = x
  
  {- DIVERGING in VZSDF order, but not VZDSF
  unify (S (F (D (V 0)))) (D (F (V 0))) (1, [])
  unify (S (F (D (V 0)))) (D (F (V 1))) (2, [])
  unify (S (S (S (S (S (D (V 0))))))) (D (D (D (V 1)))) (2, [])
  -}