subs.hs

import Data.Maybe
import Data.List

data Exp = NullOp Integer | UnOp Integer Exp | BinOp Integer Exp Exp | Var Integer deriving Eq
data ExpEq = VE Integer Exp | VV Integer Integer deriving Eq
data SubstitutionSet = SS [Exp] [ExpEq] deriving Eq
data Relation = R Exp Exp deriving Eq

instance Show ExpEq where
    show (VE n exp) = "v" ++ show n ++ " = " ++ show exp
    show (VV n1 n2) = "v" ++ show n1 ++ " = " ++ "v" ++ show n2

instance Show Exp where
    show (NullOp id) = "f" ++ show id
    show (UnOp id exp) = "f" ++ show id ++ show exp
    show (BinOp id expl expr) = "f" ++ show id ++ show expl ++ show expr
    show (Var id) = "v" ++ show id

instance Show SubstitutionSet where
    show (SS free eqs) = "k = " ++ show (length free) ++ ", " ++ show eqs

instance Show Relation where
    show (R lambda rho) = show lambda ++ " -> " ++ show rho

subs :: Exp -> Exp -> [ExpEq] -> Maybe [ExpEq]
subs exp1 exp2 assertions = 
    case exp1 of NullOp idl -> case exp2 of NullOp idr -> if idl == idr
                                                              then Just assertions
                                                              else Nothing
                                            Var n -> Just (assertions ++ [VE n exp1])
                                            _ -> Nothing

                 UnOp idl expl -> case exp2 of UnOp idr expr -> if idl == idr
                                                                    then subs expl expr assertions
                                                                    else Nothing
                                               Var n -> Just (assertions ++ [VE n exp1])
                                               _ -> Nothing
                 BinOp idl exp1l exp1r -> case exp2 of BinOp idr exp2l exp2r -> if idl == idr
                                                                                    then case subs exp1l exp2l assertions of Just newassertions -> subs exp1r exp2r newassertions
                                                                                                                             Nothing -> Nothing
                                                                                    else Nothing
                                                       Var n -> Just (assertions ++ [VE n exp1])
                                                       _ -> Nothing
                 Var nl -> case exp2 of Var nr -> Just (assertions ++ [VV nl nr])
                                        _ -> Just (assertions ++ [VE nl exp2])

solve :: [ExpEq] -> [ExpEq]
solve (eq:eqs) =
    let neweqs = newequations eq (eq:eqs) in
        neweqs ++ solve (eqs ++ neweqs)

    where newequations eq (h:t) = (case eq of VE n exp -> if eq == h
                                                              then newequations eq t
                                                              else (case h of VE n2 exp2 -> if n == n2
                                                                                                then case subs exp exp2 [] of Just assertions -> assertions
                                                                                                                              Nothing -> []
                                                                                                else []
                                                                              VV n2 n3 -> if n == n2 && ((VE n3 exp) `notElem` eq:eqs)
                                                                                              then [VE n3 exp]
                                                                                              else if n == n3 && ((VE n2 exp) `notElem` eq:eqs)
                                                                                                       then [VE n2 exp]
                                                                                                       else [])
                                              VV n1 n2 -> if eq == h
                                                              then newequations eq t
                                                              else (case h of VE n exp -> if n1 == n && ((VE n2 exp) `notElem` eq:eqs)
                                                                                              then [VE n2 exp]
                                                                                              else []
                                                                              _ -> [])) ++ (if t == []
                                                                                                then []
                                                                                                else newequations eq (tail t))
          newequations _ [] = []
solve [] = []


solveall :: [ExpEq] -> [ExpEq]
solveall eqs =
    let solved = union eqs (solve eqs) in
        if length solved > length eqs -- equations were added
            then solveall solved
            else solved

freevar :: [ExpEq] -> Exp -> Bool
freevar (eq:eqs) (Var n) =
    case eq of VE n1 exp -> if (n /= n1) && freevar eqs (Var n)
                               then True
                               else False
               VV n1 n2 -> if (n /= n1) && freevar eqs (Var n)
                               then True
                               else False

freevar [] v = True

freevars eqs (v:vars) =
    (if freevar eqs v
         then [v]
         else []) ++ freevars eqs vars
freevars eqs [] = []


uniqlefts eqs =
    realuniqlefts eqs []
    where realuniqlefts (eq:eqs) rep =
              let n = (\(VE n e) -> n) eq in
                  if n `elem` rep
                      then (realuniqlefts eqs rep)
                      else ([eq] ++ realuniqlefts eqs (n:rep))
          realuniqlefts _ _ = []

solution solved free = 
   let filtered = filter (\eq -> case eq of VV _ _ -> False 
                                            _ -> True) solved in

       substituted (uniqlefts filtered) filtered free

       where substituted list filtered free =
                 case list of [] -> []
                              _ -> [(\(VE n exp) -> (VE n (replace exp filtered free))) (head list)] ++ substituted (tail list) filtered free

             replace (NullOp id) filtered free = 
                 (NullOp id)

             replace (UnOp id exp) filtered free =
                 (UnOp id (replace exp filtered free))

             replace (BinOp id expl expr) filtered free =
                 (BinOp id (replace expl filtered free) (replace expr filtered free))

             replace (Var n) filtered free =
                 if (Var n) `elem` free
                     then (Var n)
                     else replace (findfirst (Var n) filtered) filtered free

             findfirst (Var n) (eq:eqs) =
                 case ((\(VE n1 exp) -> if n1 == n
                                            then Just exp
                                            else Nothing) eq) of Just exp -> exp
                                                                 Nothing -> findfirst (Var n) eqs

createsubstitutionset alpha beta vars =
    (SS free substitutions)
    where eqs = case subs alpha beta [] of Just assertions -> assertions
                                           Nothing -> []
          all = solveall eqs 
          free = freevars all vars 
          substitutions = solution all free 

makesubstitutions (SS _ eqs) term =
    if eqs == []
        then Just term
        else let eq = head eqs in
                 let var = (\(VE v _) -> (Var v)) eq
                     exp = (\(VE _ e) -> e) eq in
                         case (makesubstitution term var exp) of Just newterm -> makesubstitutions (SS [] (tail eqs)) newterm
                                                                 Nothing -> Nothing


-- substitute beta with beta' in term, if possible
makesubstitution :: Exp -> Exp -> Exp -> Maybe Exp
makesubstitution term beta beta' =
    if term == beta
        then Just beta'
        else case term of (UnOp id exp) -> case (makesubstitution exp beta beta') of Just newexp -> Just (UnOp id newexp)
                                                                                     Nothing -> Nothing
                          (BinOp id expl expr) -> let newexpl = makesubstitution expl beta beta'
                                                      newexpr = makesubstitution expr beta beta' in
                                                          case newexpl of Nothing -> case newexpr of Nothing -> Nothing
                                                                                                     Just r -> Just (BinOp id expl r)
                                                                          Just l -> case newexpr of Nothing -> Just (BinOp id l expr)
                                                                                                    Just r -> Just (BinOp id l r) 
                          _ -> Nothing

-- get the list of variables contained in an expression
getvars :: Exp -> [Exp]
getvars (NullOp id) = []
getvars (UnOp id exp) = (getvars exp)
getvars (BinOp id expl expr) = union (getvars expl) (getvars expr)
getvars (Var n) = [(Var n)]

-- get the list of non-trivial subwords contained in an expression
subwords :: Exp -> [Exp]
subwords (NullOp id) = [(NullOp id)]
subwords (UnOp id exp) = [(UnOp id exp)] ++ (subwords exp)
subwords (BinOp id expl expr) = [(BinOp id expl expr)] ++ (subwords expl) ++ (subwords expr)
subwords (Var n) = []

-- reduce a term until it cannot be reduced anymore
findirreducible :: Exp -> [Relation] -> Exp
findirreducible term relations = 
    case reduce term relations of Just reducedterm -> reducedterm
                                  Nothing -> term

    where reduce term (relation:relations) =
              let lambda = (\(R l r) -> l) relation
                  rho = (\(R l r) -> r) relation
                  betas = subwords term in
                      case realreduce term lambda rho betas of Nothing -> reduce term relations
                                                               Just result -> Just result
          reduce term [] = Nothing

          realreduce term lambda rho (beta:betas) = 
              let set = createsubstitutionset lambda beta (union (getvars beta) (getvars lambda)) in
                  case set of (SS _ []) -> realreduce term lambda rho betas -- try the next beta
                              _ -> makesubstitutions set beta -- found reduction
          realreduce _ _ _ [] = Nothing 


left = BinOp 2 (UnOp 1 (BinOp 2 (UnOp 1 (Var 4)) (BinOp 2 (Var 3) (UnOp 1 (BinOp 2 (Var 2) (Var 2)))))) (BinOp 2 (Var 1) (BinOp 2 (Var 3) (UnOp 1 (Var 1))))
right = BinOp 2 (UnOp 1 (BinOp 2 (Var 5) (BinOp 2 (Var 5) (Var 6)))) (BinOp 2 (Var 7) (BinOp 2 (UnOp 1 (Var 6)) (UnOp 1 (BinOp 2 (Var 5) (Var 6)))))

lambda = BinOp 2 (BinOp 2 (Var 1) (Var 2)) (Var 3)
--left = BinOp 2 (BinOp 2 (Var 1) (Var 2)) (Var 3)
--right = BinOp 2 (Var 1) (Var 2)


main = do
    --putStrLn ( show ( createsubstitutionset left right (union (getvars left) (getvars right))))
    --putStrLn (show (subwords left))

    putStrLn (show (subwords lambda))