Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP

Comparing changes

Choose two branches to see what's changed or to start a new pull request. If you need to, you can also compare across forks.

Open a pull request

Create a new pull request by comparing changes across two branches. If you need to, you can also compare across forks.
base fork: sphynx/tapl
base: 07d851edea
...
head fork: sphynx/tapl
compare: c3e808e64a
  • 5 commits
  • 5 files changed
  • 0 commit comments
  • 1 contributor
View
2  fulluntyped/DeBruijn.hs
@@ -56,7 +56,7 @@ restoreNamesM t =
-- keeping bound variables (less than "cutoff" parameter) the same.
--
shift :: Int -> NamelessTerm -> NamelessTerm
-shift d term = go 0 term where
+shift d = go 0 where
go cutoff t = case t of
Var k -> Var $ if k < cutoff then k else k + d
Abs n t1 -> Abs n $ go (cutoff+1) t1
View
9 fulluntyped/Interpreter.hs
@@ -32,6 +32,15 @@ eval1 t = case t of
_ ->
Nothing
+evalBig :: NamelessTerm -> NamelessTerm
+evalBig t = case t of
+ lam@(Abs {}) -> lam
+ App t1 t2 ->
+ let v2 = evalBig t2
+ Abs _ t12 = evalBig t1
+ in evalBig (substituteTop v2 t12)
+ t' -> t'
+
-- applies one-step evaluation until no more rules can be applied
eval :: NamelessTerm -> NamelessTerm
eval t =
View
0  fulluntyped/LambdaEnconding.hs → fulluntyped/LambdaEncoding.hs
File renamed without changes
View
3  fulluntyped/Makefile
@@ -9,3 +9,6 @@ compile: clean
test: compile
./Interpreter
+
+hlint:
+ hlint .
View
103 fulluntyped/Pretty.hs
@@ -1,13 +1,98 @@
-module Pretty where
+{-
+Pretty printer which omits all redundant brackets. It takes into
+account three facts:
+
+1. Application is left-associative, that is (x y) z = x y z
+
+2. Lambda abstraction body stretches to the right as far as
+possible: \x.y z k = \x.(y z k)
+
+3. Application binds tighter than abstraction. I.e. we need parens
+in the second expression here: (\x.x x) (\x.x x)
+
+-}
+
+module Pretty
+ ( pretty
+ ) where
+
+import Text.PrettyPrint
import Types
+ -- for more convenient testcases
+import Parser hiding (lambda, test)
+
+-- pretty printing depth, a nice idea by Jón Fairbairn mentioned in
+-- Oleg's interpreter, so we can print even divergent terms.
+maxDepth :: Int
+maxDepth = 10
+
pretty :: Term -> String
-pretty (Var x) = x
-pretty (Abs v t1) = "(\\" ++ v ++ "." ++ pretty t1 ++ ")"
-pretty (App t1 t2) = "(" ++ pretty t1 ++ " " ++ pretty t2 ++ ")"
-
-prettyNameless :: NamelessTerm -> String
-prettyNameless (Var k) = show k
-prettyNameless (Abs v t1) = "(\\." ++ prettyNameless t1 ++ ")"
-prettyNameless (App t1 t2) = "(" ++ prettyNameless t1 ++ " " ++ prettyNameless t2 ++ ")"
+pretty = render . go maxDepth where
+ go _ (Var x) = text x
+ go d _ | d <= 0 = ellipsis -- print ellipsis if we have reached
+ -- max depth
+ go d t = case t of
+ Abs v t1 ->
+ lambda <> text v <> dot <> go' t1
+ App t1 t2@(App {}) ->
+ go' t1 <+> parens (go' t2)
+ App t1@(Abs {}) t2@(Abs {}) ->
+ parens (go' t1) <+> parens (go' t2)
+ App t1@(Abs {}) t2 ->
+ parens (go' t1) <+> go' t2
+ App t1 t2 ->
+ go' t1 <+> go' t2
+
+ where
+ go' = go (d-1)
+
+-- helper stuff
+
+lambda :: Doc
+lambda = char '\\'
+
+dot :: Doc
+dot = char '.'
+
+ellipsis :: Doc
+ellipsis = space <> text "..." <> space
+
+
+-- Test suite.
+
+-- returns a list of failures: (actual, expected)
+tests :: [(String, String)]
+tests = map (\(r,a,e) -> (a,e)) .
+ filter (\(r,_,_) -> not r) .
+ map (uncurry check) $
+ [ identical "x"
+ , identical "x y"
+ , identical "x y z"
+ , identical "x (y z) t"
+ , identical "\\x.x"
+ , identical "\\x.\\y.x y"
+ , identical "(\\x.x x) (\\x.x x)"
+ , identical "(\\x.x x) (\\z.z)"
+ , identical "(\\x.x x) t"
+ , identical "\\x.\\y.\\z.x y z"
+ , identical "\\x.x (y z)"
+ , identical "\\x.x (y z) t"
+ , identical "(\\x.x) y"
+ , identical "(\\x.x y) z"
+ , ("(x)", "x")
+ , ("(x y)", "x y")
+ , ("(((x y)))", "x y")
+ , ("(x (y) z)", "x y z")
+ , ("((x y) z)", "x y z")
+ , ("((x y) z) t", "x y z t")
+ , ("(b k) ((x y) z) t", "b k (x y z) t")
+ , ("\\x.(x y z)", "\\x.x y z")
+ , ("\\x.(x y) z", "\\x.x y z")
+ , ("(\\x.x x) (t)", "(\\x.x x) t")
+ ]
+ where
+ identical x = (x, x)
+ check inp exp = let act = pretty (parseExpr inp)
+ in (exp == act, act, exp)

No commit comments for this range

Something went wrong with that request. Please try again.