fix bug with Y-combinator in shared PCF interpreter

parent 104da943
......@@ -2,6 +2,7 @@
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE CPP #-}
module Control.Arrow.Transformer.Fix where
import Prelude hiding ((.))
......@@ -12,6 +13,11 @@ import Control.Category
import Data.Order
#ifdef TRACE
import Debug.Trace
import Text.Printf
#endif
newtype Fix a b x y = Fix { runFix :: x -> y }
deriving (Arrow,ArrowChoice,ArrowApply)
......@@ -20,8 +26,13 @@ liftFix = Fix
deriving instance Category (Fix a b)
#ifdef TRACE
instance (Show x, Show y) => ArrowFix x y (Fix x y) where
fixA f = Fix (\x -> let y = runFix (f (fixA f)) x in trace (printf "%s <- eval(%s)" (show y) (show x)) y)
#else
instance ArrowFix x y (Fix x y) where
fixA f = Fix (runFix (f (fixA f)))
#endif
deriving instance PreOrd y => PreOrd (Fix a b x y)
deriving instance LowerBounded y => LowerBounded (Fix a b x y)
......
......@@ -8,7 +8,6 @@
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUAGE CPP #-}
{-# OPTIONS_GHC -DTRACE #-}
module Control.Arrow.Transformer.FixCache(CacheArrow,runCacheArrow,runCacheArrow',liftCache) where
import Prelude hiding (id,(.),lookup)
......
......@@ -19,7 +19,7 @@ import Control.Monad (join)
import qualified Data.AbstractPowerset as A
import Data.Order
import Data.Sequence hiding (lookup)
import Data.Sequence
newtype PowersetArrow c x y = PowersetArrow { runPowersetArrow :: c x (A.Pow y)}
......
......@@ -14,8 +14,16 @@ build-type: Simple
extra-source-files:
cabal-version: >=1.10
flag trace
Description: Enable tracing
Default: False
library
ghc-options: -Wall
if flag(trace) {
ghc-options: -Wall -DTRACE
} else {
ghc-options: -Wall
}
exposed-modules:
Data.AbstractPowerset,
Data.Boolean,
......
......@@ -19,10 +19,9 @@ import GHC.Generics
import PCF (Expr(..))
import Shared
data Closure = Closure Expr (Env Text Val) deriving (Eq,Show,Generic)
data Val = NumVal Int | ClosureVal Closure deriving (Eq, Show,Generic)
data Closure = Closure Expr (Env Text Val) deriving (Eq,Generic)
data Val = NumVal Int | ClosureVal Closure deriving (Eq,Generic)
type Interp = Environment Text Val (ErrorArrow String (Fix (Env Text Val,Expr) (Error String Val)))
evalConcrete :: [(Text,Val)] -> Expr -> Error String Val
......@@ -49,3 +48,9 @@ instance IsClosure Val (Env Text Val) Interp where
instance Hashable Closure
instance Hashable Val
instance Show Closure where
show (Closure e env) = show (e,env)
instance Show Val where
show (NumVal n) = show n
show (ClosureVal c) = show c
......@@ -50,7 +50,7 @@ eval = fixA $ \ev -> proc e0 -> case e0 of
env' <- extendEnv -< (x,arg,env)
localEnv ev -< (env', body)
Y e' -> do
fun' <- localEnv ev -< (env, e')
fun' <- localEnv ev -< (env, Y e')
applyClosure' ev -< (fun',arg)
_ -> failA -< "found unexpected epxression in closure: " ++ show e
......
-- {-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE OverloadedStrings #-}
module ConcreteSpec where
import SharedSpecs
import Concrete
-- import Data.Error
-- import qualified Data.HashMap.Lazy as M
-- import qualified Data.Text as T
-- import qualified PCF as E
import Data.Error
import PCF (Expr(..))
import Test.Hspec
main :: IO ()
main = hspec spec
spec :: Spec
spec =
spec = do
sharedSpec evalConcrete (NumVal . fromIntegral)
describe "behavior specific to concrete semantics" $
it "should analyse addition correctly" $ do
-- evalConcrete [] (App (App add zero) two) `shouldBe` Success (NumVal 2)
evalConcrete [] (App (App add one) two) `shouldBe` Success (NumVal 3)
where
add = Y $ Lam "add" $ Lam "x" $ Lam "y" $ IfZero "x" "y" (Succ (App (App "add" (Pred "x")) "y"))
zero = Zero
one = Succ zero
two = Succ one
......@@ -5,7 +5,6 @@ import SharedSpecs
import Data.Bounded
import Data.Error
import Data.Order
import qualified Data.Interval as I
import Data.InfiniteNumbers
import IntervalAnalysis
......@@ -63,13 +62,12 @@ spec = do
where
fix = Lam "f" (App (Lam "x" (App "f" (Lam "v" (App (App "x" "x") "v"))))
(Lam "x" (App "f" (Lam "v" (App (App "x" "x") "v")))))
-- fix = Lam "f" (App (Lam "x" (App "f" (Lam "v" (App (App "x" "x") "v"))))
-- (Lam "x" (App "f" (Lam "v" (App (App "x" "x") "v")))))
-- mult = App fix $ Lam "mult" $ Lam "x" $ Lam "y" $
-- IfZero "x" Zero (App (App add "y") (App (App "mult" (Pred "x")) "y"))
add = Y $ Lam "add" $ Lam "x" $ Lam "y" $
IfZero "x" "y" (Succ (App (App "add" (Pred "x")) "y"))
add = Y $ Lam "add" $ Lam "x" $ Lam "y" $ IfZero "x" "y" (Succ (App (App "add" (Pred "x")) "y"))
zero = Zero
one = Succ zero
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment