1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
|
module Term (
Term(..),
alphaEquiv,
alphaConvert,
alphaConvertList,
substitute,
containsVars,
rename,
typeOf,
mkEquals,
isEq,
getlhs,
getrhs
) where
import qualified Data.Set as Set
import TypeVar
data Term = TVar { tVar :: Var }
| TConst { tConst :: Const
, tConstType :: Type }
| TApp { tAppLeft :: Term
, tAppRight :: Term }
| TAbs { tAbsVar :: Term
, tAbsTerm :: Term } deriving (Ord)
type Substitution = ( [(Name,Type)], [(Var,Term)] )
instance Show Term where
show (TVar a) = show a
show (TConst a _) = show a
show (TApp (TApp eq lhs) rhs)
| isEq eq = "(" ++ (show lhs) ++ " = " ++ (show rhs) ++ ")"
show (TApp a b) = "(" ++ (show a) ++ " " ++ (show b) ++ ")"
show (TAbs a b) = "(\\" ++ (show a) ++ " -> " ++ (show b) ++ ")"
instance Eq Term where
a == b = a `alphaEquiv` b
alphaEquiv :: Term -> Term -> Bool
alphaEquiv a b =
let equiv = \term1 term2 varmap lambdaDepth ->
case (term1,term2) of
(TConst a1 b1, TConst a2 b2) ->
a1 == a2 && b1 == b2
(TApp a1 b1, TApp a2 b2) ->
equiv a1 a2 varmap lambdaDepth &&
equiv b1 b2 varmap lambdaDepth
(TAbs (TVar (Var name1 type1)) b1, TAbs (TVar (Var name2 type2)) b2) ->
type1 == type2 &&
equiv b1 b2 newmap (lambdaDepth + 1)
where newmap = (lambdaDepth + 1, ((Var name1 type1),(Var name2 type2))) : varmap
(TVar a1, TVar a2) ->
-- the order of the pair is important
(lambdaDepth, (a1,a2)) `elem` varmap ||
not ((lambdaDepth, (a1,a2)) `elem` varmap) && a1 == a2
(_,_) -> False
in equiv a b [] 0
alphaConvert :: Term -> Term -> Term
alphaConvert (TConst a ty) (TConst _ _) = TConst a ty
alphaConvert (TApp a1 b1) (TApp a2 b2) = TApp (alphaConvert a1 a2) (alphaConvert b1 b2)
alphaConvert (TVar v) (TVar _) = TVar v
alphaConvert (TAbs v1 a) (TAbs v2 b) = substitute ([],[(tVar v1,v2)]) (TAbs v1 (alphaConvert a b))
alphaConvertList :: [Term] -> [Term] -> [Term]
alphaConvertList a b = map (\x -> alphaConvert (fst x) (snd x)) (zip a b)
substitute :: Substitution -> Term -> Term
substitute (tymap,vmap) term =
let typesub =
(\x y ->
case y of
(TConst a ty) -> if (ty == (TypeVar . fst $ x))
then TConst a (snd x)
else TConst a ty
(TApp a b) -> TApp (typesub x a) (typesub x b)
(TAbs v a) -> TAbs v (typesub x a)
(TVar v) -> TVar v)
varsub =
(\x y ->
case y of
(TConst a ty) -> TConst a ty
(TApp a b) -> TApp (varsub x a) (varsub x b)
(TVar v) -> if (v == (fst x))
then snd x
else TVar v
(TAbs v a) -> let safe = rename (TAbs v a) (freeVars . snd $ x)
in case safe of
(TAbs m n) -> TAbs m (varsub x n))
tydone = foldl' (\x y -> typesub y x) term tymap
vdone = foldl' (\x y -> varsub y x) tydone vmap
in vdone
boundVars :: Term -> Set Var
boundVars (TConst a b) = Set.empty
boundVars (TApp a b) = Set.union (boundVars a) (boundVars b)
boundVars (TVar a) = Set.empty
boundVars (TAbs a b) = Set.insert a (boundVars b)
freeVars :: Term -> Set Var
freeVars (TConst a b) = Set.empty
freeVars (TApp a b) = Set.union (freeVars a) (freeVars b)
freeVars (TVar a) = Set.singleton a
freeVars (TAbs a b) = Set.delete a (freeVars b)
rename :: Term -> Set Var -> Term
rename (TAbs (TVar v) t) vars =
let doRename =
(\x y z -> case x of
(TAbs (TVar a) b) -> if (a == y)
then TAbs (TVar z) (doRename b y z)
else TAbs (TVar a) (doRename b y z)
(TConst a b) -> TConst a b
(TApp a b) -> TApp (doRename a y z) (doRename b y z)
(TVar a) -> if (a == y)
then TVar z
else TVar a)
findSafe =
(\x y -> if (Set.member x y)
then case x of
(Var a b) ->
case a of
(Name c d) -> findSafe (Var (Name c (d ++ "'")) b) y
else x)
in if (Set.member v vars)
then doRename (TAbs (TVar v) t) v (findSafe v vars)
else TAbs (TVar v) t
typeOf :: Term -> Type
typeOf (TConst c ty) = ty
typeOf (TVar v) = varTy v
typeOf (TAbs v t) = typeFunc (typeOf v) (typeOf t)
typeOf (TApp f _) =
-- type of f is of the form [[a,b], "->"]
last . aType . typeOf $ f
mkEquals :: Term -> Term -> Term
mkEquals lhs rhs =
let eqConst = TConst (Const (Name [] "=")) (mkEqualsType (typeOf lhs))
in TApp (TApp eqConst lhs) rhs
getlhs :: Term -> Term
getlhs (TApp (TApp eq lhs) _)
| (isEq eq) = lhs
getrhs :: Term -> Term
getrhs (TApp (TApp eq _) rhs)
| (isEq eq) = rhs
isEq :: Term -> Bool
isEq (TConst (Const (Name [] "=")) _) = True
isEq _ = False
|
