|
8
|
1 module Untyped where
|
|
|
2
|
|
9
|
3 import Data.Either
|
|
|
4 import Data.Functor
|
|
|
5
|
|
8
|
6 type Index = Int
|
|
|
7 type ContextSize = Int
|
|
|
8 type Name = String
|
|
|
9 data Binding = NameBind deriving Show
|
|
|
10 type Context = [(Name, Binding)]
|
|
|
11
|
|
|
12 data Term = TmVar Index ContextSize |
|
|
|
13 TmAbs String Term |
|
|
|
14 TmApp Term Term
|
|
|
15 deriving Show
|
|
|
16
|
|
|
17 -- my implementation
|
|
|
18 index2name :: Context -> Index -> String
|
|
|
19 index2name ctx i = fst $ ctx !! i
|
|
|
20
|
|
|
21 pickFreshName :: Context -> Name -> (Context, Name)
|
|
|
22 pickFreshName ctx n = (((freshName, NameBind) : ctx), freshName)
|
|
|
23 where
|
|
|
24 freshName = head . dropWhile (flip elem $ map fst ctx) $ iterate (++ "'") n
|
|
|
25
|
|
|
26
|
|
|
27 -- from book
|
|
|
28 showTerm :: Context -> Term -> String
|
|
|
29 showTerm ctx (TmAbs x t) = let (ctx', x') = pickFreshName ctx x
|
|
|
30 in "(lambda " ++ x' ++ ". " ++ (showTerm ctx' t) ++ ")"
|
|
|
31 showTerm ctx (TmApp t1 t2) = "(" ++ (showTerm ctx t1) ++ " " ++ (showTerm ctx t2) ++ ")"
|
|
|
32 showTerm ctx (TmVar i n)
|
|
|
33 | length ctx == n = index2name ctx i
|
|
|
34 | otherwise = "[bad index]"
|
|
|
35
|
|
|
36 termShift :: Int -> Term -> Term
|
|
|
37 termShift d t = walk 0 t
|
|
|
38 where
|
|
|
39 walk c (TmVar x n)
|
|
|
40 | x >= c = TmVar (x+d) (n+d)
|
|
|
41 | otherwise = TmVar x (n+d)
|
|
|
42 walk c (TmAbs x t1) = TmAbs x (walk (c+1) t1)
|
|
|
43 walk c (TmApp t1 t2) = TmApp (walk c t1) (walk c t2)
|
|
|
44
|
|
9
|
45 termSubst :: Index -> Term -> Term -> Term
|
|
|
46 termSubst j s t = walk 0 t
|
|
|
47 where
|
|
|
48 walk c (TmVar x n)
|
|
|
49 | x == (j+c) = termShift c s
|
|
|
50 | otherwise = TmVar x n
|
|
|
51 walk c (TmAbs x t1) = TmAbs x (walk (c+1) t1)
|
|
|
52 walk c (TmApp t1 t2) = TmApp (walk c t1) (walk c t2)
|
|
|
53
|
|
|
54 termSubstTop s t = termShift (-1) (termSubst 0 (termShift 1 s) t)
|
|
|
55
|
|
|
56 isVal :: Context -> Term -> Bool
|
|
|
57 isVal ctx (TmAbs _ _) = True
|
|
|
58 isval _ _ = False
|
|
|
59
|
|
|
60 eval1 :: Context -> Term -> Either String Term
|
|
|
61 eval1 ctx (TmApp (TmAbs x t12) v2)
|
|
|
62 | isVal ctx v2 = return $ termSubstTop v2 t12
|
|
|
63 | otherwise = Left $ show v2 ++ " is not variable."
|
|
|
64 eval1 ctx (TmApp t1 t2)
|
|
|
65 | isVal ctx t1 = eval1 ctx t2 >>= (\t -> return $ TmApp t1 t)
|
|
|
66 | otherwise = eval1 ctx t1 >>= (\t -> return $ TmApp t t2)
|
|
|
67 eval1 _ _ = Left "No Rule Applies"
|
|
|
68
|
|
|
69
|
|
|
70 -- x
|
|
|
71 sampleContext1 = [("x", NameBind)]
|
|
|
72 sampleTerm1 = TmVar 0 1
|
|
|
73
|
|
|
74 -- \y -> y
|
|
|
75 sampleContext2 = []
|
|
|
76 sampleTerm2 = TmAbs "y" (TmVar 0 1)
|
|
|
77
|
|
|
78 -- (\x -> x) (\x -> x x) == \x' -> x' x'
|
|
|
79 sampleContext3 = []
|
|
|
80 sampleTerm3 = (TmApp (TmAbs "x" (TmVar 0 1)) (TmAbs "x" (TmApp (TmVar 0 1) (TmVar 0 1))))
|
|
|
81
|
|
|
82 -- (\y -> (\x -> y)) (\x -> x x)
|
|
|
83 sampleContext4 = []
|
|
|
84 sampleTerm3 = (TmApp (TmAbs "x" (TmVar 0 1)) (TmAbs "x" (TmApp (TmVar 0 1) (TmVar 0 1))))
|
|
|
85 sampleTerm4 = TmApp (TmAbs "y" (TmAbs "x" (TmVar 1 2))) (TmAbs "x" (TmApp (TmVar 0 1) (TmVar 0 1)))
|
