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
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
|
module Library.Term (
Term(..),
Substitution,
alphaEquiv,
alphaConvert,
alphaConvertList,
substitute,
boundVars,
freeVars,
rename,
typeOf,
typeVarsInTerm,
mkEquals,
isEq,
getlhs,
getrhs
) where
import Data.List
import Data.Maybe
import qualified Data.Set as Set
import qualified Data.Map as Map
import Library.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 v) = (show v)
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 varmap1 varmap2 depth =
case (term1,term2) of
(TConst a1 b1, TConst a2 b2) ->
a1 == a2 && b1 == b2
(TApp a1 b1, TApp a2 b2) ->
equiv a1 a2 varmap1 varmap2 depth &&
equiv b1 b2 varmap1 varmap2 depth
(TAbs (TVar (Var name1 type1)) b1, TAbs (TVar (Var name2 type2)) b2) ->
equiv b1 b2 newmap1 newmap2 (depth+1)
where newmap1 = Map.insert (Var name1 type1) depth varmap1
newmap2 = Map.insert (Var name2 type2) depth varmap2
(TVar (Var name1 type1), TVar (Var name2 type2)) ->
type1 == type2 && ((name1 == name2 && Map.notMember (Var name1 type1) varmap1 && Map.notMember (Var name2 type2) varmap2) ||
Map.lookup (Var name1 type1) varmap1 == Map.lookup (Var name2 type2) varmap2)
(_,_) -> False
in equiv a b Map.empty Map.empty 0
alphaConvert :: Term -> Term -> Term
alphaConvert (TConst _ _) (TConst a ty) = TConst a ty
alphaConvert (TApp a1 b1) (TApp a2 b2) = TApp (alphaConvert a1 a2) (alphaConvert b1 b2)
alphaConvert (TVar _) (TVar v) = 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 (t,v) term =
let typesub x y =
case y of
(TConst a ty) -> TConst a (typeVarSub x ty)
(TApp a b) -> TApp (typesub x a) (typesub x b)
(TAbs (TVar (Var n ty)) a) -> TAbs (TVar (Var n (typeVarSub x ty))) (typesub x a)
(TVar (Var n ty)) -> TVar (Var n (typeVarSub x ty))
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 (Map.member v x)
then fromJust (Map.lookup v x)
else TVar v
(TAbs v a) -> let safe = rename (TAbs v a) (Set.union (Map.keysSet x) (Set.unions . (map freeVars) . (Map.elems) $ x))
in case safe of
(TAbs m n) -> TAbs m (varsub x n)
tymap = foldl' (\z (x,y) -> Map.insert x y z) Map.empty t
vmap = foldl' (\z (x,y) -> Map.insert x y z) Map.empty v
in (varsub vmap) . (typesub tymap) $ term
boundVars :: Term -> Set.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 (tVar a) (boundVars b)
freeVars :: Term -> Set.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 (tVar a) (freeVars b)
rename :: Term -> Set.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 _ 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
typeVarsInTerm :: Term -> Set.Set Type
typeVarsInTerm (TConst _ ty) = typeVarsInType ty
typeVarsInTerm (TVar v) = typeVarsInType . varTy $ v
typeVarsInTerm (TAbs v t) = Set.union (typeVarsInType . varTy . tVar $ v) (typeVarsInTerm t)
typeVarsInTerm (TApp f x) = Set.union (typeVarsInTerm f) (typeVarsInTerm x)
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
|
