1 | {-# LANGUAGE TypeFamilies, GADTs #-} |
---|
2 | |
---|
3 | module Lambda where |
---|
4 | |
---|
5 | import qualified Data.Supply as S |
---|
6 | import qualified Data.Char as C |
---|
7 | import Control.Monad.IO.Class (MonadIO, liftIO) |
---|
8 | import Data.IORef (newIORef, readIORef, writeIORef) |
---|
9 | |
---|
10 | {- |
---|
11 | - Lambda calculus beagyazas |
---|
12 | -} |
---|
13 | class Lambda l where |
---|
14 | lam :: (l a -> l b) -> l (a -> b) |
---|
15 | app :: l (a -> b) -> l a -> l b |
---|
16 | lit :: Int -> l Int |
---|
17 | |
---|
18 | {- |
---|
19 | - eval interpreter |
---|
20 | -} |
---|
21 | newtype Q a = Q { unQ :: a } |
---|
22 | instance Lambda Q where |
---|
23 | lit = Q |
---|
24 | lam a = Q (unQ.a.Q) |
---|
25 | app a b = Q $ unQ a (unQ b) |
---|
26 | |
---|
27 | eval :: Q a -> a |
---|
28 | eval = unQ |
---|
29 | |
---|
30 | {- |
---|
31 | - show interpreter |
---|
32 | -} |
---|
33 | showVar :: Int -> String -> String |
---|
34 | showVar x = if x>28 |
---|
35 | then showVar (x `div` 29) . showChar (C.chr $ C.ord 'a' + (x `mod` 29)) |
---|
36 | else showChar $ C.chr $ C.ord 'a' + x |
---|
37 | |
---|
38 | newtype S a = S { unS :: S.Supply Int -> Int -> ShowS } |
---|
39 | |
---|
40 | instance Lambda S where |
---|
41 | lit a = S (\_ p -> showsPrec p a) |
---|
42 | app (S fun) (S arg) = S (\s p -> |
---|
43 | let (s1, s2) = S.split2 s |
---|
44 | in showParen (p>6) $ fun s1 6 . showChar ' ' . arg s2 7) |
---|
45 | lam fun = S (\s p -> |
---|
46 | let (s1, s2) = S.split2 s |
---|
47 | v = S.supplyValue s1 |
---|
48 | showV = S $ \_ _ -> showVar v |
---|
49 | in showParen (p>0) $ showChar 'λ' . showVar v . showChar '.' . unS (fun showV) s2 0) |
---|
50 | |
---|
51 | ast :: S a -> IO ShowS |
---|
52 | ast a = do |
---|
53 | s <- S.newSupply 0 (+1) |
---|
54 | return $ unS a s 0 |
---|
55 | |
---|
56 | printAst :: S a -> IO () |
---|
57 | printAst l = ast l >>= (\s -> putStrLn $ s "") |
---|
58 | |
---|
59 | |
---|
60 | {- |
---|
61 | - reduction |
---|
62 | -} |
---|
63 | data IR h t where |
---|
64 | Lit :: Int -> IR h Int |
---|
65 | App :: IR h (a -> b) -> IR h a -> IR h b |
---|
66 | Lam :: (IR h a -> IR h b) -> IR h (a -> b) |
---|
67 | |
---|
68 | instance Lambda (IR h) where |
---|
69 | lam = Lam |
---|
70 | app = App |
---|
71 | lit = Lit |
---|
72 | |
---|
73 | toFinal :: (Lambda l) => IR h t |
---|