summaryrefslogtreecommitdiff
path: root/Library
diff options
context:
space:
mode:
authorJed Barber <jjbarber@y7mail.com>2012-09-28 23:54:15 +1000
committerJed Barber <jjbarber@y7mail.com>2012-09-28 23:54:15 +1000
commit102f42fa347b10190704562ae3638f5683772211 (patch)
tree856e70d4b54fe4d3df490026042671561137c633 /Library
parentec2487e62240dcc3b98a9a3f7c017574af34be2a (diff)
Types only tracked in alpha equivalence for bound variables
Diffstat (limited to 'Library')
-rw-r--r--Library/Term.hs12
-rw-r--r--Library/TypeVar.hs13
2 files changed, 7 insertions, 18 deletions
diff --git a/Library/Term.hs b/Library/Term.hs
index 814716f..ee5089c 100644
--- a/Library/Term.hs
+++ b/Library/Term.hs
@@ -38,8 +38,8 @@ type Substitution = ( [(Name,Type)], [(Var,Term)] )
instance Show Term where
- show (TVar a) = (show a)
- show (TConst a _) = show a
+ 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) ++ ")"
@@ -56,28 +56,28 @@ alphaEquiv a b =
let equiv = \term1 term2 varmap1 varmap2 depth ->
case (term1,term2) of
(TConst a1 b1, TConst a2 b2) ->
- a1 == a2 --&& b1 == b2
+ a1 == a2
(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) ->
- --type1 == type2 &&
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)) ->
- (name1 == name2 && Map.notMember (Var name1 type1) varmap1 && Map.notMember (Var name2 type2) varmap2) ||
+ (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 a ty) (TConst _ _) = TConst a ty
+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))
diff --git a/Library/TypeVar.hs b/Library/TypeVar.hs
index e8ce972..078d5d3 100644
--- a/Library/TypeVar.hs
+++ b/Library/TypeVar.hs
@@ -34,7 +34,7 @@ data TypeOp = TypeOp { tyOp :: Name } deriving (Eq, Ord)
data Type = TypeVar { typeVar :: Name }
| AType { aType :: [Type]
- , aTypeOp :: TypeOp } deriving (Ord)
+ , aTypeOp :: TypeOp } deriving (Eq, Ord)
data Const = Const { constName :: Name } deriving (Eq, Ord)
@@ -60,17 +60,6 @@ instance Show Var where
show (Var a _) = show a
-instance Eq Type where
- a == b = a `typeAlphaEquiv` b
-
-
-
-typeAlphaEquiv :: Type -> Type -> Bool
-typeAlphaEquiv (TypeVar a) (TypeVar b) = True
-typeAlphaEquiv (AType alist aop) (AType blist bop) =
- aop == bop && all (\(x,y) -> x == y) (zip alist blist)
-typeAlphaEquiv _ _ = True
-
mkEqualsType :: Type -> Type
mkEqualsType ty = typeFunc ty (typeFunc ty typeBool)