Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

Improved big-step evaluator

  • Loading branch information...
commit b46b0e71872b2e2b5694e3fb8c0387f5807388db 1 parent 2773baa
@sphynx authored
Showing with 64 additions and 37 deletions.
  1. +64 −37 fulluntyped/Interpreter.hs
View
101 fulluntyped/Interpreter.hs
@@ -10,56 +10,83 @@ import Control.Monad
import qualified Data.Set as Set
+type Strategy = NamelessTerm -> NamelessTerm
+
-- REPL
parseRepl :: IO ()
parseRepl = forever (getLine >>= print . parseExpr)
evalRepl :: IO ()
-evalRepl = forever (getLine >>= putStrLn . run)
-
--- one step of evaluation (as per TAPL).
--- Nothing means "no rules can be applied".
-eval1 :: NamelessTerm -> Maybe NamelessTerm
-eval1 t = case t of
- NApp (NAbs _ t1) v2
- | isValue v2 -> pure $ substituteTop v2 t1
- NApp v1 t2
- | isValue v1 -> NApp <$> pure v1 <*> eval1 t2
- NApp t1 t2 ->
- NApp <$> eval1 t1 <*> pure t2
- _ ->
- Nothing
+evalRepl = forever $ do
+ str <- getLine
+ let e = parseExpr str
+ small = evalNamedTermSmall e
+ big = evalNamedTermBig e
+ putStrLn $ "Small-step eval: " ++ small
+ putStrLn $ "Big-step eval: " ++ big
-evalBig :: NamelessTerm -> NamelessTerm
-evalBig t = case t of
- lam@(NAbs {}) -> lam
- NApp t1 t2 ->
- let v2 = evalBig t2
- NAbs _ t12 = evalBig t1
- in evalBig (substituteTop v2 t12)
- t' -> t'
+maxSteps :: Int
+maxSteps = 20
-- applies one-step evaluation until no more rules can be applied
-eval :: NamelessTerm -> NamelessTerm
-eval t =
- case eval1 t of
- Nothing -> t
- Just t' -> eval t'
+-- or max steps number is reached (to cope with divergent terms)
+evalSmall :: NamelessTerm -> NamelessTerm
+evalSmall = go maxSteps where
+
+ go :: Int -> NamelessTerm -> NamelessTerm
+ go steps t
+ | steps <= 0 = t
+ | otherwise =
+ case evalOneStep t of
+ Nothing -> t
+ Just t' -> go (steps - 1) t'
+
+ -- one step of evaluation (as per TAPL).
+ -- Nothing means "no rules can be applied".
+ evalOneStep :: NamelessTerm -> Maybe NamelessTerm
+ evalOneStep term = case term of
+ NApp (NAbs _ t1) v2
+ | isValue v2 -> pure $ substituteTop v2 t1
+ NApp v1 t2
+ | isValue v1 -> NApp <$> pure v1 <*> evalOneStep t2
+ NApp t1 t2 ->
+ NApp <$> evalOneStep t1 <*> pure t2
+ _ ->
+ Nothing
+
+-- big-step semantics
+evalBig :: NamelessTerm -> NamelessTerm
+evalBig = go maxSteps where
+
+ go steps t
+ | steps <= 0 = t
+ | otherwise = case t of
+ lam@(NAbs {}) -> lam
+ app@(NApp t1 t2) ->
+ let v1 = go steps t1
+ v2 = go steps t2
+ in if isValue v2
+ then case v1 of
+ NAbs _ t12 -> go (steps - 1) (substituteTop v2 t12)
+ _ -> app
+ else
+ app
+ t' -> t'
run :: String -> String
-run s =
- let namedTerm = parseExpr s
- ctx = Set.toList $ freeVars namedTerm
- namelessTerm = removeNames ctx namedTerm
- in pretty . restoreNames ctx . eval $ namelessTerm
+run = evalNamedTermSmall . parseExpr
+evalWithStrategy :: Term -> Strategy -> String
+evalWithStrategy t strategy =
+ let ctx = Set.toList $ freeVars t
+ namelessTerm = removeNames ctx t
+ in pretty . restoreNames ctx . strategy $ namelessTerm
--- test true x y -> x
-term1 :: Term
-term1 = parseExpr "test true"
+evalNamedTermSmall :: Term -> String
+evalNamedTermSmall t = evalWithStrategy t evalSmall
-nTerm1 :: NamelessTerm
-nTerm1 = removeNames [] term1
+evalNamedTermBig :: Term -> String
+evalNamedTermBig t = evalWithStrategy t evalBig
-- whether term is a value
isValue :: NamelessTerm -> Bool
Please sign in to comment.
Something went wrong with that request. Please try again.