fix more bugs

diff --git a/fp.cabal b/fp.cabal
index 7a1dd3f..19f889f 100644 (file)
--- a/fp.cabal
+++ b/fp.cabal
@@ -17,12 +17,13 @@ cabal-version:       >=1.10
 
 library 
   exposed-modules: Lambda
 
 library 
   exposed-modules: Lambda

+                   Lambda.Term

                    Lambda.Parser.Fancy
                    Lambda.Parser.Simple
                    HM
                    Lambda.Parser.Fancy
                    Lambda.Parser.Simple
                    HM

-                   HM.Parser
-                   Lambda.Term

                    HM.Term
                    HM.Term

+                   HM.Parser
+                   HM.Lambda

   build-depends:       base >=4.7 && <5
                      , text >=1.2 && <1.3
                      , attoparsec >=0.12 && <0.13
   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 (file)
--- 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
 
 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
             | 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 (file)
--- 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 Data.Map as M
 
 import qualified HM.Term as HMT

+import HM.Term (Literal)

 
 type VarName = String
 
 
 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
 
 
 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.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 :: 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
 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 (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 :: 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 (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
 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 (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)
 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 (file)
--- a/src/HM/Parser.hs
+++ b/src/HM/Parser.hs
@@ -91,17 +91,17 @@ parseTypeAndTerm p = do
 
 
 parseTypedTermNoApp :: Parser TypedTerm
 
 
 parseTypedTermNoApp :: Parser TypedTerm

-parseTypedTermNoApp = parseTypeAndTerm parseTermNoApp <|>
-                      parseBraces parseTypedTerm <|>
+parseTypedTermNoApp = parseBraces parseTypedTerm <|>
+                      parseTypeAndTerm parseTermNoApp <|>

                       (NTTerm <$> parseTermNoApp)
 
 parseTypedTerm :: Parser TypedTerm
 parseTypedTerm = parseTypeAndTerm parseTerm <|>
                       (NTTerm <$> parseTermNoApp)
 
 parseTypedTerm :: Parser TypedTerm
 parseTypedTerm = parseTypeAndTerm parseTerm <|>

-                 parseBraces parseTypedTerm <|>
-                 (NTTerm <$> parseTerm)
+                 (NTTerm <$> parseTerm) <|>
+                 parseBraces parseTypedTerm

 
 parseType :: Parser Type
 
 parseType :: Parser Type

-parseType = parseBraces parseType <|>
+parseType = parseType <|>

             parseTypeFunction <|>
             parsePrimitive <|>
             parseTypeVar
             parseTypeFunction <|>
             parsePrimitive <|>
             parseTypeVar