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 import HM.Term (Literal)
  10
  11 type VarName = String
  12
  13 data LTerm = Var VarName | Lam VarName LTerm | Let VarName LTerm LTerm | App LTerm LTerm | Lit Literal deriving (Eq)
  14
  15 pattern RedEx x t s = App (Lam x t) s
  16
  17 convert :: HMT.TypedTerm -> LTerm
  18 convert (HMT.TTerm t _) = convert (HMT.NTTerm t)
  19 convert (HMT.NTTerm (HMT.Var x)) = Var x
  20 convert (HMT.NTTerm (HMT.Lam x t)) = Lam x $ convert t
  21 convert (HMT.NTTerm (HMT.Let x y z)) = Let x (convert y) (convert z)
  22 convert (HMT.NTTerm (HMT.App y z)) = App (convert y) (convert z)
  23 convert (HMT.NTTerm (HMT.Lit l)) = Lit l
  24
  25 isFreeIn :: VarName -> LTerm -> Bool
  26 isFreeIn x (Var v) = x == v
  27 isFreeIn _ (Lit _) = False
  28 isFreeIn x (App t u) = x `isFreeIn` t || x `isFreeIn` u
  29 isFreeIn x (Lam v t) = x /= v && x `isFreeIn` t
  30 isFreeIn x (Let v t u) = x `isFreeIn` t || x /= v && x `isFreeIn` u
  31
  32 rename :: LTerm -> LTerm
  33 rename (Lam x t) = Lam n (substitute x (Var n) t)
  34   where n = rnm x
  35         rnm v = if (v ++ "r") `isFreeIn` t then rnm (v ++ "r") else v ++ "r"
  36 rename (Let x t u) = Let n t (substitute x (Var n) u)
  37   where n = rnm x
  38         rnm v = if (v ++ "r") `isFreeIn` t then rnm (v ++ "r") else v ++ "r"
  39 rename t = t
  40
  41 substitute :: VarName -> LTerm -> LTerm -> LTerm
  42 substitute a b (Var x) = if x == a then b else Var x
  43 substitute a b (Lit l) = Lit l
  44 substitute a b (Lam x t)
  45   | x == a = Lam x t
  46   | x `isFreeIn` b = substitute a b $ rename (Lam x t)
  47   | otherwise = Lam x (substitute a b t)
  48 substitute a b (Let x t u)
  49   | x == a = Let x (substitute a b t) u
  50   | x `isFreeIn` b = substitute a b $ rename (Let x t u)
  51   | otherwise = Let x (substitute a b t) (substitute a b u)
  52 substitute a b (App t u) = App (substitute a b t) (substitute a b u)
  53
  54 reduce :: LTerm -> LTerm
  55 reduce (Var x) = Var x
  56 reduce (Lit l) = Lit l
  57 reduce (Lam x t) = Lam x (reduce t)
  58 reduce (Let x t u) = reduce $ substitute x t u
  59 reduce (App t u) = app (reduce t) u
  60   where app (Lam x v) w = reduce $ substitute x w v
  61         app a b = App a (reduce b)