src/HM/Lambda.hs

   1 {-# LANGUAGE PatternSynonyms #-}
   2
   3 module HM.Lambda where
   4
   5 import Control.Monad.State
   6 import Data.Map as M
   7
   8 import qualified HM.Term as HMT
   9
  10 type VarName = String
  11
  12 data LTerm = Var VarName | Lam VarName LTerm | Let VarName LTerm LTerm | App LTerm LTerm deriving (Eq, Show)
  13
  14 pattern RedEx x t s = App (Lam x t) s
  15
  16 convert :: HMT.TypedTerm -> LTerm
  17 convert (HMT.TTerm t _) = convert (HMT.NTTerm t)
  18 convert (HMT.NTTerm (HMT.Var x)) = Var x
  19 convert (HMT.NTTerm (HMT.Lam x t)) = Lam x $ convert t
  20 convert (HMT.NTTerm (HMT.Let x y z)) = Let x (convert y) (convert z)
  21 convert (HMT.NTTerm (HMT.App y z)) = App (convert y) (convert z)
  22
  23 isFreeIn :: VarName -> LTerm -> Bool
  24 isFreeIn x (Var v) = x == v
  25 isFreeIn x (App t u) = x `isFreeIn` t || x `isFreeIn` u
  26 isFreeIn x (Lam v t) = x /= v && x `isFreeIn` t
  27 isFreeIn x (Let v t u) = x `isFreeIn` t || x /= v && x `isFreeIn` u
  28
  29 rename :: LTerm -> LTerm
  30 rename (Lam x t) = Lam n (substitute x (Var n) t)
  31   where n = rnm x
  32         rnm v = if (v ++ "r") `isFreeIn` t then rnm (v ++ "r") else v ++ "r"
  33 rename _ = error "TODO vymyslet reprezentaci, kde pujde udelat fce, ktera bere jen Lambdy"
  34
  35 substitute :: VarName -> LTerm -> LTerm -> LTerm
  36 substitute a b (Var x) = if x == a then b else Var x
  37 substitute a b (Lam x t)
  38   | x == a = Lam x t
  39   | x `isFreeIn` b = substitute a b $ rename (Lam x t)
  40   | otherwise = Lam x (substitute a b t)
  41 substitute a b (Let x t u) = error "TODO implement let"
  42 substitute a b (App t u) = App (substitute a b t) (substitute a b u)
  43
  44 reduce :: LTerm -> LTerm
  45 reduce (Var x) = Var x
  46 reduce (Lam x t) = Lam x (reduce t)
  47 reduce (App t u) = app (reduce t) u
  48   where app (Lam x v) w = reduce $ substitute x w v
  49         app a b = App a (reduce b)
  50
  51 data Strategy = Eager | Lazy
  52
  53 reduceStep :: LTerm -> LTerm
  54 reduceStep (RedEx x s t) = substitute x t s
  55 reduceStep t = t
  56
  57 data Z = R LTerm Z | L Z LTerm | ZL VarName Z | E
  58 data D = Up | Down
  59 type TermZipper = (LTerm, Z, D)
  60
  61 move :: TermZipper -> TermZipper
  62 move (App l r, c, Down) = (l, L c r, Down)
  63 move (Lam x t, c, Down) = (t, ZL x c, Down)
  64 move (Var x, c, Down) = (Var x, c, Up)
  65 move (t, L c r, Up) = (r, R t c, Down)
  66 move (t, R l c, Up) = (App l t, c, Up)
  67 move (t, ZL x c, Up) = (Lam x t, c, Up)
  68 move (t, E, Up) = (t, E, Up)
  69
  70 unmove :: TermZipper -> TermZipper
  71 unmove (t, L c r, Down) = (App t r, c, Down)
  72 unmove x = x
  73
  74 -- getTerm :: TermZipper -> Term
  75
  76 travPost :: (Monad m) => (LTerm -> m LTerm) -> LTerm -> m LTerm
  77 travPost fnc term = tr fnc (term, E, Down)
  78   where
  79     tr f (t@RedEx{}, c, Up) = do
  80       nt <- f t
  81       tr f (nt, c, Down)
  82     tr _ (t, E, Up) = return t
  83     tr f (t, c, Up) = tr f $ move (t, c, Up)
  84     tr f (t, c, Down) = tr f $ move (t, c, Down)
  85
  86 travPre :: (Monad m) => (LTerm -> m LTerm) -> LTerm -> m LTerm
  87 travPre fnc term = tr fnc (term, E, Down)
  88   where
  89     tr f (t@RedEx{}, c, Down) = do
  90       nt <- f t
  91       tr f $ unmove (nt, c, Down)
  92     tr _ (t, E, Up) = return t
  93     tr f (t, c, Up) = tr f $ move (t, c, Up)
  94     tr f (t, c, Down) = tr f $ move (t, c, Down)
  95
  96 -- |
  97 --
  98 -- >>> toNormalForm Eager 100 cI
  99 -- Just (λx.x)
 100 --
 101 -- >>> toNormalForm Eager 100 $ App cI cI
 102 -- Just (λx.x)
 103 --
 104 -- >>> toNormalForm Eager 100 $ (App (App cK cI) cY)
 105 -- Nothing
 106 --
 107 -- >>> toNormalForm Lazy 100 $ (App (App cK cI) cY)
 108 -- Just (λx.x)
 109 --
 110 -- prop> within 10000000 $ (\ t u -> t == u || t == Nothing || u == Nothing) (alphaNorm <$> toNormalForm Lazy 100 x) (alphaNorm <$> toNormalForm Eager 100 x)
 111
 112 -- 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))"
 113
 114 toNormalForm :: Strategy -> Int -> LTerm -> Maybe LTerm
 115 toNormalForm Eager n = flip evalStateT 0 . travPost (cnt >=> short n >=> return . reduceStep)
 116 toNormalForm Lazy  n = flip evalStateT 0 . travPre  (cnt >=> short n >=> return . reduceStep)
 117
 118 cnt :: (Monad m) => LTerm -> StateT Int m LTerm
 119 cnt t@RedEx{} = do
 120   modify (+ 1)
 121   return t
 122 cnt t = return t
 123
 124 short :: Int -> LTerm -> StateT Int Maybe LTerm
 125 short maxN t = do
 126   n <- get
 127   if n > maxN
 128     then lift Nothing
 129     else return t