module Decide_Termination where

import Prelude hiding (sequence)

import Data.Monoid (mempty)
import Data.Traversable (sequence)
import Data.Map (Map, (!), unionWith)
import qualified Data.Map as Map
import Data.Maybe (fromMaybe, mapMaybe)

data Term = App String [Term]
          | Var String
  deriving (Eq, Show, Read)

type Subst = Map String Term

subst :: Subst -> Term -> Term
subst sigma (App c ts) = App c (map (subst sigma) ts)
subst sigma (Var n) = fromMaybe (Var n) (Map.lookup n sigma)

{-- MATCHING

If 
  match t1 t2 = Just sigma
holds, then
  subst sigma t1 = t2

--}

merge_maybe :: Eq a => Maybe a -> Maybe a -> Maybe a
merge_maybe (Just a) (Just b)
  | a == b = Just a
  | otherwise = Nothing
merge_maybe _ _ = Nothing

merge_map :: (Ord k, Eq v) => Map k v -> Map k v -> Maybe (Map k v)
merge_map s t = sequence (unionWith merge_maybe (Map.map Just s) (Map.map Just t))

match :: Term -> Term -> Maybe Subst
match (Var n) t = Just (Map.singleton n t)
match (App f c) (App g d) = if f == g then match_list c d else Nothing
match (App f c) (Var _) = Nothing

match_list :: [Term] -> [Term] -> Maybe Subst
match_list [] [] = Just mempty
match_list (c:cs) (d:ds) =
  do
  s <- match c d
  t <- match_list cs ds
  merge_map s t
match_list _ _ = Nothing

subterms :: Term -> [Term]
subterms (Var n) = []
subterms (App f ps) = App f ps : concatMap subterms ps

{-- SOLUTION --}

{--  

Check if the equation system is 
  a) right-ground, i.e. there are no variables at the right sides , and, if it is right-ground,
  b) terminating.

Implement the method described in TRaAT:

  * start with a term from the right side of an equation
  * perform reduction until you either
    - find a loop (the original term is a subterm), -> return False
    - or there are no possible reductions -> return True

Of course, you need to remember the starting term, and it needs to be done simultaneously, otherwise
the decision method might not terminate.

--}

decide_termination :: [(Term, Term)] -> Bool
decide_termination = ...

{-- EXAMPLES --}

f x y = App "f" [x, y]
g x = App "g" [x]
h x = App "h" [x]
a = App "a" []
b = App "b" []
c = App "c" []

x = Var "x"
y = Var "y"
z = Var "z"

eqs1 = [(f x x, f a b), (a, b)]
eqs2 = [(f x x, f a b), (b, c)]
eqs3 = [(f x y, f a b)]