From: Tomáš Musil <tomik.musil@gmail.com>
Date: Fri, 4 Sep 2015 00:25:06 +0000 (+0200)
Subject: lambda for HM
X-Git-Url: http://git.tomasm.cz/fp.git/commitdiff_plain/94f9e5a83598d189b1dd90d4fec0927622a8b778

lambda for HM
---

diff --git a/src/HM/Lambda.hs b/src/HM/Lambda.hs
index e85041c..1d76e1f 100644
--- a/src/HM/Lambda.hs
+++ b/src/HM/Lambda.hs
@@ -1,15 +1,129 @@
+{-# LANGUAGE PatternSynonyms #-}
+
 module HM.Lambda where
 
 import Control.Monad.State
 import Data.Map as M
 
-import HM.Term
+import qualified HM.Term as HMT
+
+type VarName = String
+
+data LTerm = Var VarName | Lam VarName LTerm | Let VarName LTerm LTerm | App LTerm LTerm deriving (Eq, Show)
+
+pattern RedEx x t s = App (Lam x t) s
+
+convert :: HMT.TypedTerm -> LTerm
+convert (HMT.TTerm t _) = convert (HMT.NTTerm t)
+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)
+
+isFreeIn :: VarName -> LTerm -> Bool
+isFreeIn x (Var v) = x == v
+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
+
+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"
+
+substitute :: VarName -> LTerm -> LTerm -> LTerm
+substitute a b (Var x) = if x == a then b else Var x
+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 (App t u) = App (substitute a b t) (substitute a b u)
+
+reduce :: LTerm -> LTerm
+reduce (Var x) = Var x
+reduce (Lam x t) = Lam x (reduce t)
+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)
 
-type Env = M.Map VarName Term
-type LI a = State Env a
+-- 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))"
 
-stripType :: TypedTerm -> Term
-stripType (NTTerm t) = t
-stripType (TTerm t _) = t
+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