{-
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