X-Git-Url: http://git.tomasm.cz/fp.git/blobdiff_plain/33464c9ce7b0b1559f8cb23734065b8ecdd382c1..ec954b9fcade4eb933dcec4aa9517118f5088910:/src/HM/Lambda.hs

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