Type alpha equivalence in limbo

2 files changed, 19 insertions, 8 deletions

diff --git a/Library/Term.hs b/Library/Term.hs
index 4377047..814716f 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 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) ++ ")"
@@ -56,21 +56,21 @@ 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 --&& 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) ->
-                    type1 == type2 &&
+                    --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 a1, TVar a2) ->
-                    a1 == a2 && Map.notMember a1 varmap1  && Map.notMember a2 varmap2 ||
-                    Map.lookup a1 varmap1 == Map.lookup a2 varmap2
+                (TVar (Var name1 type1), TVar (Var name2 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
diff --git a/Library/TypeVar.hs b/Library/TypeVar.hs
index 078d5d3..e8ce972 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 (Eq, Ord)
+                  , aTypeOp :: TypeOp } deriving (Ord)
 
 data Const = Const { constName :: Name } deriving (Eq, Ord)
 
@@ -60,6 +60,17 @@ 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)