{-
    gulcii -- graphical untyped lambda calculus interpreter
    Copyright (C) 2011, 2013, 2017  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 Reduce (Reduce(..), Reduction, reduce) where

import Prelude hiding (replicate)

import qualified Data.Map.Strict as Map

import Evaluation (Strategy(..))
import Graph

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

data Reduce = Beta | RefInst | Rebound String | Extrude
  deriving (Read, Show, Eq, Ord)

type Reduction = (Reduce, (References, Term))

mapTerm :: (Term -> Term) -> Reduction -> Reduction
mapTerm f = fmap (fmap f)


reduce :: Definitions -> References -> Term -> Maybe Reduction
reduce defs refs term =
  case reduce' False defs refs term of
    Nothing -> reduce' True defs refs term
    r -> r


reduce' :: Bool -> Definitions -> References -> Term -> Maybe Reduction

reduce' _ defs refs (Free var)
  = (,) (Rebound var) `fmap` (,) refs `fmap` Map.lookup var defs

reduce' _ _    _    (Bound0)
  = Nothing

reduce' _ _    refs (Scope (Lambda strat term))
  = Just (Extrude, (refs, Lambda strat (lifting refs 1 term)))

reduce' f defs refs (Scope t@(Reference _))
  = case dereference refs t of
      l@(Lambda _ _) ->
        Just (RefInst, (refs, Scope l))
      _ -> mapTerm Scope `fmap` reduce' f defs refs t

reduce' _ _    refs (Scope (Apply a b))
  = Just (Extrude, (refs, Apply (Scope a) (Scope b)))

reduce' f defs refs (Scope term)
  = mapTerm Scope `fmap` reduce' f defs refs term

reduce' f defs refs (Lambda strat term)
  = mapTerm (Lambda strat) `fmap` reduce' f defs refs term

reduce' f defs refs term@(Reference ref)
  = case Map.lookup ref refs of
      Just refTerm ->
        case reduce' f defs refs refTerm of
          Just (reason, (refs', term')) ->
            Just (reason, (Map.insert ref term' refs', term))
          Nothing ->
            Just (RefInst, (refs, refTerm))
      Nothing -> Nothing -- error "reference not found"

reduce' _ _    refs (Apply (Lambda Copy a) b)
  = Just (Beta, (refs, beta refs a b))

reduce' f defs refs (Apply l@(Lambda Strict a) b)
  = case reduce' f defs refs b of
      Just (reason, (refs', b')) -> Just (reason, (refs', Apply l b'))
      Nothing -> Just (Beta, (refs, beta refs a b))

reduce' _ _    refs (Apply (Lambda Lazy a) b)
  = let r = next refs
        refs' = Map.insert r b refs
    in  Just (Beta, ( refs'
                    , beta refs' a (Reference r) ))

reduce' f defs refs (Apply a b)
  = case (a, dereference refs a) of
      (Reference _, l@(Lambda _ _)) -> Just (RefInst, (refs, Apply l b))
      _ ->
       case reduce' f defs refs a of
          Just (reason, (refs', a')) ->
            Just (reason, (refs', Apply a' b))
          Nothing
            | f -> mapTerm (Apply a) `fmap` reduce' f defs refs b
            | otherwise -> Nothing


beta :: References -> Term -> Term -> Term
beta refs l v = substitute refs l v 0

substitute :: References -> Term -> Term -> Integer -> Term
substitute _    Bound0 s 0 = s
substitute _    Bound0 _ _ = Bound0
substitute _    (Scope t) _ 0 = t
substitute refs (Scope t) s i = Scope (substitute refs t s (i - 1))
substitute refs (Lambda k t) s i = Lambda k (substitute refs t s (i + 1))
substitute refs (Apply a b) s i = Apply (substitute refs a s i) (substitute refs b s i)
substitute _    t@(Free _) _ _ = t
substitute refs (Reference r) s i = substitute refs (refs Map.! r) s i

lifting :: References -> Integer -> Term -> Term
lifting _    0 t = Scope t
lifting _    _ s@(Free _) = s
lifting _    _ Bound0 = Bound0
lifting refs i (Scope t) = Scope (lifting refs (i - 1) t)
lifting refs i (Lambda k t) = Lambda k (lifting refs (i + 1) t)
lifting refs i (Apply a b) = Apply (lifting refs i a) (lifting refs i b)
lifting refs i (Reference r) = lifting refs i (refs Map.! r)


dereference :: References -> Term -> Term
dereference refs (Reference r) = dereference refs (refs Map.! r)
dereference _ t = t


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