Last active
August 29, 2015 14:16
-
-
Save Cedev/087c3e50ecc53e0f04e9 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| import Control.Applicative | |
| import Data.List | |
| import Data.Maybe | |
| data Term = Var Int | Lam Int Term | App Term Term deriving (Show) | |
| data BTerm = BVar Int | BLam BTerm | BApp BTerm BTerm deriving (Show) -- BVar 0 refers to the closest lambda | |
| lam2db :: Term -> Maybe BTerm | |
| lam2db = go [] | |
| where | |
| go xs (Var x) = BVar <$> elemIndex x xs -- elemIndex is exploiting 0 being the first list index | |
| go xs (Lam x exp) = BLam <$> go (x:xs) exp | |
| go xs (App exp1 exp2) = BApp <$> go xs exp1 <*> go xs exp2 | |
| -- | Safe version of `!!` | |
| (!?) :: [a] -> Int -> Maybe a | |
| xs !? n = listToMaybe (drop n xs) | |
| db2lam :: BTerm -> Maybe Term | |
| db2lam = go [15..] [] | |
| where | |
| go names xs (BVar x) = Var <$> xs !? x -- exploiting 0 being the first list index. | |
| go (x:names) xs (BLam exp) = Lam x <$> go names (x:xs) exp | |
| go names xs (BApp exp1 exp2) = App <$> go names xs exp1 <*> go names xs exp2 | |
| main = do | |
| let b = BLam (BLam (BVar 1)) | |
| print b | |
| let l = db2lam b | |
| print l | |
| let b' = l >>= lam2db | |
| print b' |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment