Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

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: dab5074552
...
head fork: sphynx/tapl
compare: b25c864d29
Checking mergeability… Don't worry, you can still create the pull request.
  • 4 commits
  • 5 files changed
  • 0 commit comments
  • 1 contributor
View
26 fulluntyped/DeBruijn.hs
@@ -3,8 +3,6 @@ Convert terms to nameless de Bruijn representation when we used indices
instead of variables names.
-}
-{-# OPTIONS_GHC -Wall #-}
-
module DeBruijn (
removeNames,
restoreNames,
@@ -37,16 +35,16 @@ removeNamesM t =
case t of
Var name -> do
idx <- asks $ elemIndex name
- maybe (error $ "Unknown var: " ++ name) (return . Var) idx
- App t1 t2 -> App <$> removeNamesM t1 <*> removeNamesM t2
- Abs name t1 -> Abs name <$> local (name:) (removeNamesM t1)
+ maybe (error $ "Unknown var: " ++ name) (return . NVar) idx
+ App t1 t2 -> NApp <$> removeNamesM t1 <*> removeNamesM t2
+ Abs name t1 -> NAbs name <$> local (name:) (removeNamesM t1)
restoreNamesM :: NamelessTerm -> Env Term
restoreNamesM t =
case t of
- Var idx -> Var <$> asks (!! idx) -- FIXME: use safe (!!) here
- App t1 t2 -> App <$> restoreNamesM t1 <*> restoreNamesM t2
- Abs n t1 -> do
+ NVar idx -> Var <$> asks (!! idx) -- FIXME: use safe (!!) here
+ NApp t1 t2 -> App <$> restoreNamesM t1 <*> restoreNamesM t2
+ NAbs n t1 -> do
name <- asks $ nextName n
subt <- local (name:) (restoreNamesM t1)
return $ Abs name subt
@@ -58,18 +56,18 @@ restoreNamesM t =
shift :: Int -> NamelessTerm -> NamelessTerm
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
- App t1 t2 -> App (go cutoff t1) (go cutoff t2)
+ NVar k -> NVar $ if k < cutoff then k else k + d
+ NAbs n t1 -> NAbs n $ go (cutoff+1) t1
+ NApp t1 t2 -> NApp (go cutoff t1) (go cutoff t2)
--
-- performs substitution [j |-> s] t
--
substitute :: Int -> NamelessTerm -> NamelessTerm -> NamelessTerm
substitute j s t = case t of
- Var k -> if j == k then s else Var k
- Abs n t1 -> Abs n (substitute (j + 1) (shift 1 s) t1)
- App t1 t2 -> App (substitute j s t1) (substitute j s t2)
+ NVar k -> if j == k then s else NVar k
+ NAbs n t1 -> NAbs n (substitute (j + 1) (shift 1 s) t1)
+ NApp t1 t2 -> NApp (substitute j s t1) (substitute j s t2)
--
-- beta-reduction substitution (\.t1) v2
View
107 fulluntyped/Interpreter.hs
@@ -1,5 +1,3 @@
-{-# OPTIONS_GHC -Wall #-}
-
module Interpreter where
import Types
@@ -12,60 +10,87 @@ 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
- App (Abs _ t1) v2
- | isValue v2 -> pure $ substituteTop v2 t1
- App v1 t2
- | isValue v1 -> App <$> pure v1 <*> eval1 t2
- App t1 t2 ->
- App <$> 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@(Abs {}) -> lam
- App t1 t2 ->
- let v2 = evalBig t2
- Abs _ 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 :: Expr a -> Bool
-isValue (Abs {}) = True
+isValue :: NamelessTerm -> Bool
+isValue (NAbs {}) = True
isValue _ = False
main :: IO ()
View
14 fulluntyped/Pretty.hs
@@ -30,17 +30,15 @@ pretty = render . go maxDepth where
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 {}) ->
+ App t1@(Abs {}) t2@(Var {}) -> --- abs var
+ parens (go' t1) <+> go' t2
+ App t1@(Abs {}) t2 -> -- abs _
parens (go' t1) <+> parens (go' t2)
- App t1@(Var {}) t2@(Abs {}) ->
+ App t1 t2@(App {}) -> -- _ app
go' t1 <+> parens (go' t2)
- App t1@(App {}) t2@(Abs {}) ->
+ App t1 t2@(Abs {}) -> --- var abs
go' t1 <+> parens (go' t2)
- App t1@(Abs {}) t2 ->
- parens (go' t1) <+> go' t2
- App t1 t2 ->
+ App t1 t2 -> --- _ _
go' t1 <+> go' t2
_ ->
-- this is here to please "-Wall"
View
42 fulluntyped/Tests.hs
@@ -9,21 +9,30 @@ To run tests try `make test`.
-}
+{-# LANGUAGE FlexibleInstances #-}
+
module Tests where
-import Test.Framework (defaultMain, testGroup)
-import Test.Framework.Providers.HUnit (testCase)
+import Test.Framework
+import Test.Framework.Providers.HUnit
+import Test.Framework.Providers.SmallCheck
import Test.HUnit
+import Test.SmallCheck
+import Test.SmallCheck.Series
+
import Pretty
import Parser
+import Types
+import Interpreter hiding (main)
main :: IO ()
main = defaultMain tests
tests =
- [ testGroup "Pretty printing tests" prettyTests
+ [ testGroup "Pretty printing unit tests" prettyTests,
+ testGroup "Properties" smallCheckTests
]
prettyTests = map (uncurry mkTestCase)
@@ -43,6 +52,8 @@ prettyTests = map (uncurry mkTestCase)
, identical "(\\x.x y) z"
, identical "x (\\y.y)"
, identical "x y (\\y.y)"
+ , identical "x ((\\x.x) (x x))"
+
, ("(x)", "x")
, ("(x y)", "x y")
, ("(((x y)))", "x y")
@@ -59,3 +70,28 @@ prettyTests = map (uncurry mkTestCase)
mkTestCase inp exp =
testCase ("pretty-printing " ++ inp) $
pretty (parseExpr inp) @?= exp
+
+
+newtype VarName = VarName Name
+
+var :: VarName -> Term
+var (VarName v) = Var v
+
+abstr :: VarName -> Term -> Term
+abstr (VarName v) = Abs v
+
+instance Serial VarName where
+ series = const [VarName [c] | c <- "xy"]
+ coseries = undefined
+
+instance Serial (Expr Name) where
+ series = cons1 var
+ \/ cons2 abstr
+ \/ cons2 App
+ coseries = undefined
+
+smallCheckTests = [
+ withDepth 4 $ testProperty "(parse . pretty) should be id"
+ $ (\t -> parseExpr (pretty t) == t )
+
+ ]
View
21 fulluntyped/Types.hs
@@ -2,24 +2,21 @@ module Types where
import Data.Set ((\\), singleton, union, Set)
-type Name = String
-
--- Expr here is parametrized.
--- 1) "a = String" for named terms
--- 2) "a = Int" for nameless, de Bruijn-style terms.
data Expr a =
Var a
- | Abs String (Expr a)
+ | Abs a (Expr a)
| App (Expr a) (Expr a)
- deriving Show
+ deriving (Show, Eq)
-instance Functor Expr where
- fmap f (Var t) = Var (f t)
- fmap f (Abs name t) = Abs name (fmap f t)
- fmap f (App t1 t2) = App (fmap f t1) (fmap f t2)
+data NamelessTerm =
+ NVar Int
+ -- we keep names in String here to restore them back later
+ | NAbs String NamelessTerm
+ | NApp NamelessTerm NamelessTerm
+ deriving (Show, Eq)
+type Name = String
type Term = Expr Name
-type NamelessTerm = Expr Int
type NamingCtx = [Name]

No commit comments for this range

Something went wrong with that request. Please try again.