Mercurial > hg > Members > atton > tapl

comparison untyped/Untyped.hs @ 9:4bfeb679ef15

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add eval1 in Untyped
author atton
date Tue, 01 Nov 2016 04:53:18 +0000
parents 5fa32bb75df6
children
comparison
equal deleted inserted replaced
8:5fa32bb75df6 9:4bfeb679ef15
1 module Untyped where 1 module Untyped where
2
3 import Data.Either
4 import Data.Functor
2 5
3 type Index = Int 6 type Index = Int
4 type ContextSize = Int 7 type ContextSize = Int
5 type Name = String 8 type Name = String
6 data Binding = NameBind deriving Show 9 data Binding = NameBind deriving Show
13 16
14 -- my implementation 17 -- my implementation
15 index2name :: Context -> Index -> String 18 index2name :: Context -> Index -> String
16 index2name ctx i = fst $ ctx !! i 19 index2name ctx i = fst $ ctx !! i
17 20
18 -- my implementation
19 pickFreshName :: Context -> Name -> (Context, Name) 21 pickFreshName :: Context -> Name -> (Context, Name)
20 pickFreshName ctx n = (((freshName, NameBind) : ctx), freshName) 22 pickFreshName ctx n = (((freshName, NameBind) : ctx), freshName)
21 where 23 where
22 freshName = head . dropWhile (flip elem $ map fst ctx) $ iterate (++ "'") n 24 freshName = head . dropWhile (flip elem $ map fst ctx) $ iterate (++ "'") n
23 25
29 showTerm ctx (TmApp t1 t2) = "(" ++ (showTerm ctx t1) ++ " " ++ (showTerm ctx t2) ++ ")" 31 showTerm ctx (TmApp t1 t2) = "(" ++ (showTerm ctx t1) ++ " " ++ (showTerm ctx t2) ++ ")"
30 showTerm ctx (TmVar i n) 32 showTerm ctx (TmVar i n)
31 | length ctx == n = index2name ctx i 33 | length ctx == n = index2name ctx i
32 | otherwise = "[bad index]" 34 | otherwise = "[bad index]"
33 35
34 -- from book
35 termShift :: Int -> Term -> Term 36 termShift :: Int -> Term -> Term
36 termShift d t = walk 0 t 37 termShift d t = walk 0 t
37 where 38 where
38 walk c (TmVar x n) 39 walk c (TmVar x n)
39 | x >= c = TmVar (x+d) (n+d) 40 | x >= c = TmVar (x+d) (n+d)
40 | otherwise = TmVar x (n+d) 41 | otherwise = TmVar x (n+d)
41 walk c (TmAbs x t1) = TmAbs x (walk (c+1) t1) 42 walk c (TmAbs x t1) = TmAbs x (walk (c+1) t1)
42 walk c (TmApp t1 t2) = TmApp (walk c t1) (walk c t2) 43 walk c (TmApp t1 t2) = TmApp (walk c t1) (walk c t2)
43 44
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)))