diff options
| -rw-r--r-- | Library/Term.hs | 14 | ||||
| -rw-r--r-- | Library/TypeVar.hs | 13 |
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) |