{-
    gulcii -- graphical untyped lambda calculus interpreter
    Copyright (C) 2011, 2013  Claude Heiland-Allen

    This program is free software; you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
    the Free Software Foundation; either version 2 of the License, or
    (at your option) any later version.

    This program is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
    GNU General Public License for more details.

    You should have received a copy of the GNU General Public License along
    with this program; if not, write to the Free Software Foundation, Inc.,
    51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
-}

module Graph (Term(..), Definitions, References, Reduction(..), graph, reduce, pretty) where

import qualified Data.Map.Strict as M
import Data.Map.Strict (Map)

import qualified Bruijn as B
import Evaluation (Strategy(..))

data Term
  = Free !String
  | Bound !Integer
  | Lambda !Strategy !Term
  | Apply !Term !Term
  | Reference !Integer
  | Trace !String !Term !Term
  deriving (Read, Show, Eq, Ord)

pretty :: Term -> String
pretty = unwords . pretty'

pretty' :: Term -> [String]
pretty' (Free s) = [s]
pretty' (Bound i) = [show i]
pretty' (Reference i) = ['#':show i]
pretty' (Lambda k t) = ["(", "\\", pretty'' k] ++ pretty' t ++ [")"]
pretty' (Apply s t) = ["("] ++ pretty' s ++ pretty' t ++ [")"]
pretty' (Trace k s t) = ["(", "{", k, ":"] ++ pretty' s ++ ["}"] ++ pretty' t ++ [")"]

pretty'' :: Strategy -> String
pretty'' Strict = "!"
pretty'' Lazy = "."
pretty'' Copy = "?"

type Definitions = Map String Term
type References = Map Integer Term

next :: Map Integer a -> Integer
next refs = case M.maxViewWithKey refs of
  Nothing        -> 0
  Just ((k,_),_) -> k + 1

graph :: B.Term -> Term
graph (B.Free v) = Free v
graph (B.Bound i) = Bound i
graph (B.Lambda k t) = Lambda k (graph t)
graph (B.Apply s t) = Apply (graph s) (graph t)
graph (B.Trace k s t) = Trace k (graph s) (graph t)

{-
bind :: String -> Term -> Term -> Term
bind v s t@(Free u) = if u == v then s else t
bind _ _ t@(Bound _) = t
bind v s (Lambda k t) = Lambda k (bind v s t)
bind v s (Apply a b) = Apply (bind v s a) (bind v s b)
bind _ _ t@(Reference _) = t
-}

{-
Reduce a graph one step, returning Nothing if it is irreducible.
-}

data Reduction = Reduced Term References | Rebound String Term References | Traced String Term Term References
  deriving (Read, Show, Eq, Ord)

mapR :: (Term -> Term) -> Reduction -> Reduction
mapR f (Reduced t refs) = Reduced (f t) refs
mapR f (Rebound s t refs) = Rebound s (f t) refs
mapR f (Traced k s t refs) = Traced k s (f t) refs

reduce, reduce' :: Definitions -> References -> Term -> Maybe Reduction
reduce _ refs (Trace k s t) = Just (Traced k s t refs)
reduce defs refs term = reduce' defs refs term

-- free variables are replaced with their definition
reduce' defs refs (Free v) = case M.lookup v defs of
  Nothing -> Nothing
  Just t -> let r = next refs in Just (Rebound v (Reference r) (M.insert r t refs))

-- bound variables are irreducible
reduce' _ _ (Bound _) = Nothing

-- non top-level traces are irreducible?
--reduce' _ _ (Trace _ _ _) = Nothing
reduce' _ refs (Trace k s t) = Just (Traced k s t refs)

-- maybe reduce inside lambda
reduce' defs refs (Lambda k t) = mapR (Lambda k) `fmap` reduce' defs refs t

reduce' defs refs (Apply a b) = case a of
  -- beta reduction
  Lambda Strict a' -> case reduce defs refs b of
    Just r -> Just (mapR (a `Apply`) r)
    Nothing -> Just (uncurry Reduced (beta refs a' b))
  Lambda Copy a' -> Just (Reduced (beta' 0 a' b) refs)
  Lambda Lazy a' -> Just (uncurry Reduced (beta refs a' b))
  Reference r -> case M.lookup r refs of
    Just a' -> Just (Reduced (Apply a' b) refs)
    _ -> Nothing
  Free s -> case M.lookup s defs of
    Just a' -> Just (Rebound s (Apply a' b) refs)
    _ -> Nothing
  t@(Apply _ _) -> case reduce defs refs t of
    Just r -> Just (mapR (`Apply` b) r)
    _ -> Nothing
  _ -> Nothing -- Bound, Trace

-- reduce references
reduce' defs refs s@(Reference r) = case M.lookup r refs of
  Nothing -> Nothing
  Just t -> case reduce' defs refs t of
    Just (Reduced t' refs') -> Just (Reduced s (M.insert r t' refs'))
    Just (Rebound v t' refs') -> Just (Rebound v s (M.insert r t' refs'))
    _ -> Just (Reduced t refs)

-- beta reduction
beta :: References -> Term -> Term -> (Term, References)
beta refs a b = (beta' 0 a t, refs')
  where
    r = next refs
    refs' = M.insert r b refs
    t = Reference r

beta' :: Integer -> Term -> Term -> Term
beta' i s@(Bound j) t = if i == j then t else s
beta' i (Lambda k s) t = Lambda k (beta' (i + 1) s t)
beta' i (Apply a b) t = Apply (beta' i a t) (beta' i b t)
beta' _ s@(Free _) _ = s
beta' _ s@(Reference _) _ = s
beta' i (Trace k a b) t = Trace k (beta' i a t) (beta' i b t)