module Rewriting where


--------------------
-- Terms and Rules datatypes
--------------------

data Atom = Con String | Var String

data Term = App Atom [Term]

data Rules = Rules [(Term, Term)]

var v = App (Var v) []
con c = App (Con c) []

splice (App f ts) ts' = App f (ts++ts')


--------------------
-- Show instances for datatypes
--------------------

instance Show Atom where
  show (Con c) = c
  show (Var v) = v
  
instance Show Term where
  show (App (Con "plus") [x,y]) = concat ["(",show x," + ",show y,")"]
  show (App (Con "mult") [x,y]) = concat ["(",show x," * ",show y,")"]
  show term@(App f ts) =
    case fullNum term of
      Just k  -> show k
      Nothing -> unwords (show f : map par ts)
                 where par tm@(App f ts) 
                         = let st = show tm in
                           if elem ' ' st then "(" ++ st ++ ")" else st

{- old definition:
  show (App f ts) = unwords (show f : map par ts)
                    where par (App f []) = show f
                          par tm = "(" ++ show tm ++ ")"
-}

instance Show Rules where
  show (Rules eqs) = unlines (map showEqn eqs)

showEqn (l,r) = show l ++ " = " ++ show r

showCalc (h:ts) = unlines (show h : map (("  = " ++) . show) ts)

fullNum (App (Con "zero") [])  = Just 0
fullNum (App (Con "1+") [n]) = case fullNum n of
                                   Nothing -> Nothing
                                   Just k  -> Just (k+1)
fullNum _ = Nothing


--------------------
-- Unification, substitution and matching
-- (NB: no checks for circularity or non-linearity!)
--------------------

unify (App (Var v) []) t = Just [(v,t)]
unify (App (Con c) ts) (App (Con d) ts') 
  = if c==d && length ts' >= length ts
       then foldl (just (++)) (Just []) (zipWith unify ts ts')
       else Nothing
unify _ _ = Nothing

subst s (App (Con c) ts) = App (Con c) (map (subst s) ts)
subst s (App (Var v) ts) = case lookup v s of
                             Nothing -> App (Var v) ts'
                             Just t  -> splice t ts'
                           where ts' = map (subst s) ts

match (Rules rs) t = mfst m rs
                     where m (l,r) = case unify l t of
                                       Nothing -> Nothing
                                       Just s  -> Just (splice (subst s r) (resid l t))

resid (App _ ps) (App _ ts) = drop (length ps) ts


--------------------
-- Reduction and calculation
-- ¥ for parallel strategy, use mpar versus mlft
-- ¥ for inner-more strategies, use reda versus redn
--------------------

redn rules tm@(App f ts) = case match rules tm of
                            Just t  -> Just t
                            Nothing -> case mlft (redn rules) ts of
                                         Nothing -> Nothing
                                         Just ts' -> Just (App f ts')

reda rules tm@(App f ts) = case mpar (reda rules) ts of
                              Just ts' -> Just (App f ts')
                              Nothing  -> match rules tm

calc rules t = miter (redn rules) t

run n rules term = putStr (showCalc (term : (take n (calc rules term))))


--------------------
-- Maybe utilities
--------------------

just f (Just x) (Just y) = Just (f x y)
just f _ _ = Nothing

mlft f [] = Nothing
mlft f (x:xs) = case f x of
                  Just x' -> Just (x':xs)
                  Nothing -> case mlft f xs of
                               Nothing  -> Nothing
                               Just xs' -> Just (x:xs')

mpar f [] = Nothing
mpar f (x:xs) = case f x of
                  Just x' -> case mpar f xs of
                               Nothing  -> Just (x':xs)
                               Just xs' -> Just (x':xs')
                  Nothing -> case mpar f xs of
                               Nothing  -> Nothing
                               Just xs' -> Just (x:xs')

mfst f [] = Nothing
mfst f (x:xs) = case f x of
                  Just x' -> Just x'
                  Nothing -> mfst f xs

miter f x = case f x of
              Nothing -> []
              Just x' -> x' : miter f x'


--------------------
-- Lessons learned, future work:
-- ¥ saturation check (length in unify) is crucial, esp. for appl strats
-- ¥ use of abstract rule clauses in later positions can fail for norm strats
--   (consider "and x y = false" when actual args remain unevaluated)
-- ¥ how much of the excessive Maybe plumbing can be clawed back via Monads?
-- ¥ how tidily can strategy choices be represented as data?
--------------------