From: Tomáš Musil Date: Sun, 6 Sep 2015 17:57:48 +0000 (+0200) Subject: fix more bugs X-Git-Url: http://git.tomasm.cz/fp.git/commitdiff_plain/HEAD fix more bugs --- diff --git a/fp.cabal b/fp.cabal index 7a1dd3f..19f889f 100644 --- a/fp.cabal +++ b/fp.cabal @@ -17,12 +17,13 @@ cabal-version: >=1.10 library exposed-modules: Lambda + Lambda.Term Lambda.Parser.Fancy Lambda.Parser.Simple HM - HM.Parser - Lambda.Term HM.Term + HM.Parser + HM.Lambda build-depends: base >=4.7 && <5 , text >=1.2 && <1.3 , attoparsec >=0.12 && <0.13 diff --git a/src/HM.hs b/src/HM.hs index 9591706..3cbf5c9 100644 --- a/src/HM.hs +++ b/src/HM.hs @@ -67,7 +67,7 @@ composeSub s1 s2 = Map.map (substituteT s1) s2 `Map.union` s1 varBind :: TypeVarName -> Type -> TI Substitution varBind v t | t == TypeVar v = return idSub - | v `Set.member` freeVarsT t = fail $ "occur check failed: " ++ v ++ " in " ++ show t + | v `Set.member` freeVarsT t = fail $ "occur check failed: " ++ v ++ " ~ " ++ show t | otherwise = return $ Map.singleton v t instantiate :: TypeScheme -> TI Type diff --git a/src/HM/Lambda.hs b/src/HM/Lambda.hs index 1d76e1f..f5f0026 100644 --- a/src/HM/Lambda.hs +++ b/src/HM/Lambda.hs @@ -6,10 +6,11 @@ import Control.Monad.State import Data.Map as M import qualified HM.Term as HMT +import HM.Term (Literal) type VarName = String -data LTerm = Var VarName | Lam VarName LTerm | Let VarName LTerm LTerm | App LTerm LTerm deriving (Eq, Show) +data LTerm = Var VarName | Lam VarName LTerm | Let VarName LTerm LTerm | App LTerm LTerm | Lit Literal deriving (Eq) pattern RedEx x t s = App (Lam x t) s @@ -19,9 +20,11 @@ convert (HMT.NTTerm (HMT.Var x)) = Var x convert (HMT.NTTerm (HMT.Lam x t)) = Lam x $ convert t convert (HMT.NTTerm (HMT.Let x y z)) = Let x (convert y) (convert z) convert (HMT.NTTerm (HMT.App y z)) = App (convert y) (convert z) +convert (HMT.NTTerm (HMT.Lit l)) = Lit l isFreeIn :: VarName -> LTerm -> Bool isFreeIn x (Var v) = x == v +isFreeIn _ (Lit _) = False isFreeIn x (App t u) = x `isFreeIn` t || x `isFreeIn` u isFreeIn x (Lam v t) = x /= v && x `isFreeIn` t isFreeIn x (Let v t u) = x `isFreeIn` t || x /= v && x `isFreeIn` u @@ -30,100 +33,29 @@ rename :: LTerm -> LTerm rename (Lam x t) = Lam n (substitute x (Var n) t) where n = rnm x rnm v = if (v ++ "r") `isFreeIn` t then rnm (v ++ "r") else v ++ "r" -rename _ = error "TODO vymyslet reprezentaci, kde pujde udelat fce, ktera bere jen Lambdy" +rename (Let x t u) = Let n t (substitute x (Var n) u) + where n = rnm x + rnm v = if (v ++ "r") `isFreeIn` t then rnm (v ++ "r") else v ++ "r" +rename t = t substitute :: VarName -> LTerm -> LTerm -> LTerm substitute a b (Var x) = if x == a then b else Var x +substitute a b (Lit l) = Lit l substitute a b (Lam x t) | x == a = Lam x t | x `isFreeIn` b = substitute a b $ rename (Lam x t) | otherwise = Lam x (substitute a b t) -substitute a b (Let x t u) = error "TODO implement let" +substitute a b (Let x t u) + | x == a = Let x (substitute a b t) u + | x `isFreeIn` b = substitute a b $ rename (Let x t u) + | otherwise = Let x (substitute a b t) (substitute a b u) substitute a b (App t u) = App (substitute a b t) (substitute a b u) reduce :: LTerm -> LTerm reduce (Var x) = Var x +reduce (Lit l) = Lit l reduce (Lam x t) = Lam x (reduce t) +reduce (Let x t u) = reduce $ substitute x t u reduce (App t u) = app (reduce t) u where app (Lam x v) w = reduce $ substitute x w v app a b = App a (reduce b) - -data Strategy = Eager | Lazy - -reduceStep :: LTerm -> LTerm -reduceStep (RedEx x s t) = substitute x t s -reduceStep t = t - -data Z = R LTerm Z | L Z LTerm | ZL VarName Z | E -data D = Up | Down -type TermZipper = (LTerm, Z, D) - -move :: TermZipper -> TermZipper -move (App l r, c, Down) = (l, L c r, Down) -move (Lam x t, c, Down) = (t, ZL x c, Down) -move (Var x, c, Down) = (Var x, c, Up) -move (t, L c r, Up) = (r, R t c, Down) -move (t, R l c, Up) = (App l t, c, Up) -move (t, ZL x c, Up) = (Lam x t, c, Up) -move (t, E, Up) = (t, E, Up) - -unmove :: TermZipper -> TermZipper -unmove (t, L c r, Down) = (App t r, c, Down) -unmove x = x - --- getTerm :: TermZipper -> Term - -travPost :: (Monad m) => (LTerm -> m LTerm) -> LTerm -> m LTerm -travPost fnc term = tr fnc (term, E, Down) - where - tr f (t@RedEx{}, c, Up) = do - nt <- f t - tr f (nt, c, Down) - tr _ (t, E, Up) = return t - tr f (t, c, Up) = tr f $ move (t, c, Up) - tr f (t, c, Down) = tr f $ move (t, c, Down) - -travPre :: (Monad m) => (LTerm -> m LTerm) -> LTerm -> m LTerm -travPre fnc term = tr fnc (term, E, Down) - where - tr f (t@RedEx{}, c, Down) = do - nt <- f t - tr f $ unmove (nt, c, Down) - tr _ (t, E, Up) = return t - tr f (t, c, Up) = tr f $ move (t, c, Up) - tr f (t, c, Down) = tr f $ move (t, c, Down) - --- | --- --- >>> toNormalForm Eager 100 cI --- Just (λx.x) --- --- >>> toNormalForm Eager 100 $ App cI cI --- Just (λx.x) --- --- >>> toNormalForm Eager 100 $ (App (App cK cI) cY) --- Nothing --- --- >>> toNormalForm Lazy 100 $ (App (App cK cI) cY) --- Just (λx.x) --- --- prop> within 10000000 $ (\ t u -> t == u || t == Nothing || u == Nothing) (alphaNorm <$> toNormalForm Lazy 100 x) (alphaNorm <$> toNormalForm Eager 100 x) - --- inf = tRead "(\\d.a ((\\d c.c d c) (\\x y z.x z (y z)) (\\f.(\\x.f (x x)) (\\x.f (x x))) e))" - -toNormalForm :: Strategy -> Int -> LTerm -> Maybe LTerm -toNormalForm Eager n = flip evalStateT 0 . travPost (cnt >=> short n >=> return . reduceStep) -toNormalForm Lazy n = flip evalStateT 0 . travPre (cnt >=> short n >=> return . reduceStep) - -cnt :: (Monad m) => LTerm -> StateT Int m LTerm -cnt t@RedEx{} = do - modify (+ 1) - return t -cnt t = return t - -short :: Int -> LTerm -> StateT Int Maybe LTerm -short maxN t = do - n <- get - if n > maxN - then lift Nothing - else return t diff --git a/src/HM/Parser.hs b/src/HM/Parser.hs index 24ade14..8b5575d 100644 --- a/src/HM/Parser.hs +++ b/src/HM/Parser.hs @@ -91,17 +91,17 @@ parseTypeAndTerm p = do parseTypedTermNoApp :: Parser TypedTerm -parseTypedTermNoApp = parseTypeAndTerm parseTermNoApp <|> - parseBraces parseTypedTerm <|> +parseTypedTermNoApp = parseBraces parseTypedTerm <|> + parseTypeAndTerm parseTermNoApp <|> (NTTerm <$> parseTermNoApp) parseTypedTerm :: Parser TypedTerm parseTypedTerm = parseTypeAndTerm parseTerm <|> - parseBraces parseTypedTerm <|> - (NTTerm <$> parseTerm) + (NTTerm <$> parseTerm) <|> + parseBraces parseTypedTerm parseType :: Parser Type -parseType = parseBraces parseType <|> +parseType = parseType <|> parseTypeFunction <|> parsePrimitive <|> parseTypeVar