X-Git-Url: http://git.tomasm.cz/fp.git/blobdiff_plain/0d7d9b4184cd881452d854cc571595f518fb1afe..HEAD:/src/HM/Lambda.hs?ds=inline

diff --git a/src/HM/Lambda.hs b/src/HM/Lambda.hs
index e85041c..f5f0026 100644
--- a/src/HM/Lambda.hs
+++ b/src/HM/Lambda.hs
@@ -1,15 +1,61 @@
+{-# LANGUAGE PatternSynonyms #-}
+
 module HM.Lambda where
 
 import Control.Monad.State
 import Data.Map as M
 
-import HM.Term
+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 | Lit Literal deriving (Eq)
+
+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)
+convert (HMT.NTTerm (HMT.Lit l)) = Lit l 
 
-type Env = M.Map VarName Term
-type LI a = State Env a
+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
 
-stripType :: TypedTerm -> Term
-stripType (NTTerm t) = t
-stripType (TTerm t _) = t
+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 (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)
+  | 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)