Skip to content

Commit

Permalink
Fix eval strategies.
Browse files Browse the repository at this point in the history
This resolves #1.

* src/LambdaAST.hs (emptyTermSet): New definition.
(addTerm): New function.
* src/LambdaAST/Path.hs (Branch, Path): Derive Eq.
(<|>, goRight, goLeft): New function.
(left, right, rightNoLambda, self): New function.
(traverse, find, findRedex, findFreeOccurrence): New function.
(outermostFirst, innermostFirst): New definition.
(outermostfirstNoLambda, innermostFirstNoLambda): New definition.
(findFirstInnermostRedex, findFirstOutermostRedex): Remove.
(findInnermostUnboundOccurrence, findOutermostUnboundOccurrence):
Remove.
(Cursor, PathSelector, TraversalOrder): New type.
* src/Main.hs (setPragma): Make choosing strategies coherent.
* src/Reducer.hs (EvaluationOrder): Remove.
(findNextRedex, findNextUnboundOcc): Remove.
(Strategy, normalOrder, applicativeOrder): Use 'TraversalOrder'.
(callByName, callByValue): New definition.
(defaultStrategy): Update.
(betaReduce): Use 'findRedex'.
(lambdaApply): Drop case distinction.
(deltaReduce): Use 'findFreeOccurrence'.
  • Loading branch information
sirius94 committed Dec 3, 2016
1 parent 161b640 commit 0fe0872
Show file tree
Hide file tree
Showing 4 changed files with 139 additions and 125 deletions.
22 changes: 8 additions & 14 deletions src/LambdaAST.hs
Original file line number Diff line number Diff line change
Expand Up @@ -6,21 +6,10 @@ module LambdaAST
isRedex,

TermSet,
emptyTermSet,
addTerm,

LambdaTerm
(
Lambda,
Application,
Variable,
Definition
),
parameter,
term,
function,
argument,
var,
name,
value
LambdaTerm(..)
)
where

Expand All @@ -31,6 +20,11 @@ type IdentifierSet = Set.Set String

type TermSet = [LambdaTerm]

emptyTermSet = []

addTerm :: LambdaTerm -> TermSet -> TermSet
addTerm t ts = t:ts

data LambdaTerm = Lambda { parameter :: String,
term :: LambdaTerm} |
Application { function :: LambdaTerm,
Expand Down
183 changes: 109 additions & 74 deletions src/LambdaAST/Path.hs
Original file line number Diff line number Diff line change
@@ -1,32 +1,36 @@
{-# LANGUAGE LambdaCase #-}
module LambdaAST.Path
(
findNodeByPath,
replaceByPath,

findFirstInnermostRedex,
findFirstOutermostRedex,

findInnermostUnboundOccurrence,
findOutermostUnboundOccurrence,
TraversalOrder,
outermostFirst,
innermostFirst,
outermostFirstNoLambda,
innermostFirstNoLambda,

replaceByPath,
findRedex,
findFreeOccurrence,

Branch (Left, Right),
Path (Path),
Branch (..),
Path (..),
descend,
root
)
where

import Prelude hiding (Left, Right)
import Prelude hiding (Left, Right, traverse)
import Data.Functor
import Data.Maybe

import LambdaAST

data Branch = Left | Right
deriving Show
deriving (Show, Eq)

newtype Path = Path [Branch]
deriving Show
deriving (Show, Eq)

root = Path []

Expand All @@ -37,12 +41,21 @@ instance Monoid Path where
(<:>) :: Branch -> Path -> Path
(<:>) b (Path p) = Path (b:p)

(<|>) :: Maybe a -> Maybe a -> Maybe a
(<|>) a b = if isJust a then a else b

goRightThen :: Path -> Path
goRightThen p = Right <:> p

goLeftThen :: Path -> Path
goLeftThen p = Left <:> p

goRight :: Path -> Path
goRight (Path p) = Path $ p ++ [Right]

goLeft :: Path -> Path
goLeft (Path p) = Path $ p ++ [Left]

descend :: Maybe Path -> Branch -> Maybe Path
descend (Just (Path (Right:ps))) Right = Just $ Path ps
descend (Just (Path (Left:ps))) Left = Just $ Path ps
Expand All @@ -68,71 +81,93 @@ findNode n h = findNodeInSubTree [] n h
findNodeInSubTree p n Definition { value = right } =
findNodeInSubTree (p ++ [Right]) n right

findFirstInnermostRedex :: LambdaTerm -> Maybe Path
findFirstInnermostRedex Lambda { term = right } =
goRightThen <$> findFirstInnermostRedex right
findFirstInnermostRedex a@Application { function = left, argument = right } =
case goLeftThen <$> findFirstInnermostRedex left of
p@Just {} -> p
Nothing ->
case goRightThen <$> findFirstInnermostRedex right of
p@Just {} -> p
Nothing -> if isRedex a then Just root else Nothing
findFirstInnermostRedex Definition { value = right } =
goRightThen <$> findFirstInnermostRedex right
findFirstInnermostRedex _ = Nothing

findFirstOutermostRedex :: LambdaTerm -> Maybe Path
findFirstOutermostRedex Lambda { term = right } =
goRightThen <$> findFirstInnermostRedex right
findFirstOutermostRedex a@Application { function = left, argument = right } =
if isRedex a
then Just root
else
case goLeftThen <$> findFirstOutermostRedex left of
p@Just {} -> p
Nothing -> goRightThen <$> findFirstOutermostRedex right
findFirstOutermostRedex Definition { value = right } =
goRightThen <$> findFirstInnermostRedex right
findFirstOutermostRedex _ = Nothing

findInnermostUnboundOccurrence :: TermSet -> LambdaTerm -> Maybe Path
findInnermostUnboundOccurrence = findInnermostUnboundOccurrence' []
data Cursor = Cursor { path :: Path,
subTerm :: LambdaTerm,
bound :: TermSet } |
CursorEnd
deriving Eq

rootCursor :: LambdaTerm -> Cursor
rootCursor term = Cursor root term emptyTermSet

type PathSelector = (Cursor -> Cursor)

type TraversalOrder = [PathSelector]

right :: PathSelector
right = pathRight . termRight
where
pathRight = \case
c@Cursor { path = path } -> c { path = goRight path }
_ -> CursorEnd
termRight = \case
c@Cursor { subTerm = Lambda p right, bound = bound } ->
c { subTerm = right, bound = addTerm (Variable p) bound }
c@Cursor { subTerm = Application _ right } ->
c { subTerm = right }
c@Cursor { subTerm = Definition name right, bound = bound } ->
c { subTerm = right, bound = addTerm (Variable name) bound }
_ -> CursorEnd

left :: PathSelector
left = pathLeft . termLeft
where
findInnermostUnboundOccurrence' :: TermSet -> TermSet -> LambdaTerm -> Maybe Path
findInnermostUnboundOccurrence' bound searchSet t@(Lambda p right) =
compareIfNothing bound searchSet t $
goRightThen <$> findInnermostUnboundOccurrence' (Variable p:bound) searchSet right
findInnermostUnboundOccurrence' bound searchSet t@(Application left right) =
compareIfNothing bound searchSet t $
case goLeftThen <$> findInnermostUnboundOccurrence' bound searchSet left of
p@Just {} -> p
Nothing -> goRightThen <$> findInnermostUnboundOccurrence' bound searchSet right
findInnermostUnboundOccurrence' bound searchSet t@(Definition boundVar right) =
compareIfNothing bound searchSet t $
goRightThen <$> findInnermostUnboundOccurrence' (Variable boundVar:bound) searchSet right
findInnermostUnboundOccurrence' bound searchSet t =
compareIfNothing bound searchSet t Nothing
compareIfNothing :: TermSet -> TermSet -> LambdaTerm -> Maybe Path -> Maybe Path
compareIfNothing bound searchSet term Nothing =
if not (term `elem` bound) && (term `elem` searchSet) then Just root else Nothing
compareIfNothing _ _ _ p = p

findOutermostUnboundOccurrence :: TermSet -> LambdaTerm -> Maybe Path
findOutermostUnboundOccurrence = findOutermostUnboundOccurrence' []
pathLeft = \case
c@Cursor { path = path } -> c { path = goLeft path }
_ -> CursorEnd
termLeft = \case
c@Cursor { subTerm = Application left _ } -> c { subTerm = left }
_ -> CursorEnd

rightNoLambda :: PathSelector
rightNoLambda = \case
c@Cursor { subTerm = Lambda {} } -> CursorEnd
c -> right c

self :: PathSelector
self = id

outermostFirst :: TraversalOrder
outermostFirst = [self, left, right]

innermostFirst :: TraversalOrder
innermostFirst = [left, right, self]

outermostFirstNoLambda :: TraversalOrder
outermostFirstNoLambda = [self, left, rightNoLambda]

innermostFirstNoLambda :: TraversalOrder
innermostFirstNoLambda = [left, rightNoLambda, self]

traverse :: TraversalOrder -> (Cursor -> Maybe a) -> LambdaTerm -> Maybe a
traverse selectors f t = traverse' selectors f $ rootCursor t
where
traverse' :: TraversalOrder -> (Cursor -> Maybe a) -> Cursor -> Maybe a
traverse' _ _ CursorEnd = Nothing
traverse' (s:[]) f c = let c' = s c in
(f $ c') <|> traverseIfNotEqual f c c'
traverse' (s:ss) f c = let c' = s c in
(f $ c')
<|> traverseIfNotEqual f c c'
<|> traverse' ss f c
traverseIfNotEqual f p c = (if p /= c then traverse' selectors f c else Nothing)

find :: TraversalOrder -> (Cursor -> Bool) -> LambdaTerm -> Maybe Path
find to p =
traverse to (\c -> if p c then Just (path c) else Nothing)

findRedex :: TraversalOrder -> LambdaTerm -> Maybe Path
findRedex to = find to cursorIsRedex
where
cursorIsRedex c@Cursor { subTerm = term } = isRedex term
cursorIsRedex CursorEnd = False

findFreeOccurrence :: TraversalOrder -> TermSet -> LambdaTerm -> Maybe Path
findFreeOccurrence to searchSet = find to occurrence
where
findOutermostUnboundOccurrence' :: TermSet -> TermSet -> LambdaTerm -> Maybe Path
findOutermostUnboundOccurrence' bound searchSet term |
not (term `elem` bound) && (term `elem` searchSet) = Just root
findOutermostUnboundOccurrence' bound searchSet t@(Lambda p right) =
goRightThen <$> findOutermostUnboundOccurrence' (Variable p:bound) searchSet right
findOutermostUnboundOccurrence' bound searchSet t@(Application left right) =
case goLeftThen <$> findOutermostUnboundOccurrence' bound searchSet left of
p@Just {} -> p
Nothing -> goRightThen <$> findOutermostUnboundOccurrence' bound searchSet right
findOutermostUnboundOccurrence' bound searchSet t@(Definition boundVar right) =
goRightThen <$> findOutermostUnboundOccurrence' (Variable boundVar:bound) searchSet right
findOutermostUnboundOccurrence' _ _ _ = Nothing
occurrence c@Cursor { subTerm = term, bound = bound } =
not (term `elem` bound) && term `elem` searchSet
occurrence CursorEnd = False

replaceByPath :: Path -> LambdaTerm -> LambdaTerm -> LambdaTerm
replaceByPath (Path []) t _ = t
Expand Down
15 changes: 7 additions & 8 deletions src/Main.hs
Original file line number Diff line number Diff line change
Expand Up @@ -21,20 +21,19 @@ repl t =
else getLine >>= evalLine t >>= repl

setPragma :: Pragma -> Context -> IO Context
setPragma Pragma { pragmaOption = "passBy", pragmaValue = value }
setPragma Pragma { pragmaOption = "strategy", pragmaValue = value }
c@Context { strategy = s } =
case value of
"name" -> return c { strategy = s { pass = ByName } }
"value" -> return c { strategy = s { pass = ByValue} }
setPragma Pragma { pragmaOption = "evalOrder", pragmaValue = value }
c@Context { strategy = s } =
case value of
"normal" -> return c { strategy = s { evalOrder = normalOrder } }
"applicative" -> return c { strategy = s { evalOrder = applicativeOrder } }
"normalOrder" -> return c { strategy = normalOrder }
"applicativeOrder" -> return c { strategy = applicativeOrder }
"callByName" -> return c { strategy = callByName }
"callByValue" -> return c { strategy = callByValue }
_ -> putStrLn "No such strategy." >> return c
setPragma Pragma { pragmaOption = "render", pragmaValue = value } c =
case value of
"cl" -> return c { renderer = clRendererSpec }
"latex" -> return c { renderer = latexRendererSpec }
_ -> putStrLn "No such renderer." >> return c
setPragma Pragma { pragmaOption = "maxSteps", pragmaValue = value} c =
return c { evalStepLimit = read value :: Int }
setPragma Pragma { pragmaOption = "load", pragmaValue = path } c =
Expand Down
44 changes: 15 additions & 29 deletions src/Reducer.hs
Original file line number Diff line number Diff line change
Expand Up @@ -5,9 +5,10 @@ module Reducer

Strategy (..),

EvaluationOrder (..),
normalOrder,
applicativeOrder,
callByName,
callByValue,

Passing (..),

Expand All @@ -27,59 +28,44 @@ import Reducer.DefinitionTable
import Reducer.Step
import Reducer.Renderer

data EvaluationOrder =
EvaluationOrder { findRedex :: LambdaTerm -> Maybe Path,
findUnboundOcc :: TermSet -> LambdaTerm -> Maybe Path}
data Passing = ByName | ByValue

data Strategy = Strategy { pass :: Passing,
evalOrder :: EvaluationOrder }
type Strategy = TraversalOrder

data Context = Context { strategy :: Strategy,
table :: DefinitionTable,
renderer :: RendererSpec,
evalStepLimit :: Int }

findNextRedex = findRedex . evalOrder
normalOrder = outermostFirst
applicativeOrder = innermostFirst
callByName = outermostFirstNoLambda
callByValue = innermostFirstNoLambda

findNextUnboundOcc = findUnboundOcc . evalOrder

normalOrder = EvaluationOrder {
findRedex = findFirstOutermostRedex,
findUnboundOcc = findOutermostUnboundOccurrence }
applicativeOrder = EvaluationOrder {
findRedex = findFirstInnermostRedex,
findUnboundOcc = findInnermostUnboundOccurrence }

defaultStrategy = Strategy { pass = ByName, evalOrder = normalOrder }
defaultStrategy = normalOrder

defaultContext = Context { strategy = defaultStrategy,
table = noDefs,
renderer = clRendererSpec,
evalStepLimit = 0 }

betaReduce :: Strategy -> LambdaTerm -> ReductionStep
betaReduce s@Strategy {} t =
case findNextRedex s t of
betaReduce s t =
case findRedex s t of
Nothing -> NoReduction t
Just p ->
let Just a = findNodeByPath p t
step = (lambdaApply s p a) in
step = (lambdaApply p a) in
Beta (path step) $ replaceByPath (path step) (newTerm step) t

lambdaApply :: Strategy -> Path -> LambdaTerm -> ReductionStep
lambdaApply Strategy { pass = ByName } p (Application (Lambda parameter term) argument) =
lambdaApply :: Path -> LambdaTerm -> ReductionStep
lambdaApply p (Application (Lambda parameter term) argument) =
Beta p $ replaceWithSubtree parameter argument term
lambdaApply s@Strategy { pass = ByValue } p
(Application (Lambda parameter term) argument) =
case findNextRedex s argument of
Nothing -> Beta p $ replaceWithSubtree parameter argument term
Just _ -> let step = betaReduce s argument in
Beta (p <> path step) (newTerm step)
lambdaApply _ _ _ = undefined
lambdaApply _ _ = undefined

deltaReduce :: Strategy -> DefinitionTable -> LambdaTerm -> ReductionStep
deltaReduce s d t = case findNextUnboundOcc s (keySet d) t of
deltaReduce s d t = case findFreeOccurrence s (keySet d) t of
Nothing -> NoReduction t
Just p ->
let Just key = (findNodeByPath p t)
Expand Down

0 comments on commit 0fe0872

Please sign in to comment.