From e438502b5fbbfa22d73927daaa0d93dc650a033b Mon Sep 17 00:00:00 2001 From: Jed Barber Date: Tue, 15 May 2012 18:02:02 +1000 Subject: Fixed alphaEquiv, again --- Term.hs | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/Term.hs b/Term.hs index 5067c1a..20c70ce 100644 --- a/Term.hs +++ b/Term.hs @@ -20,6 +20,7 @@ module Term ( import Data.List import qualified Data.Set as Set +import qualified Data.Map as Map import TypeVar @@ -51,27 +52,27 @@ instance Eq Term where alphaEquiv :: Term -> Term -> Bool alphaEquiv a b = - let equiv = \term1 term2 varmap -> + 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 varmap && - equiv b1 b2 varmap + 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 newmap - where newmap = ((Var name1 type1),(Var name2 type2)) : varmap + 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) -> - -- the order of the pair is important - (a1,a2) `elem` varmap || - a1 == a2 && not ((a1,a2) `elem` varmap) + a1 == a2 && Map.notMember a1 varmap1 && Map.notMember a2 varmap2 || + Map.lookup a1 varmap1 == Map.lookup a2 varmap2 (_,_) -> False - in equiv a b [] + in equiv a b Map.empty Map.empty 0 alphaConvert :: Term -> Term -> Term -- cgit