summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Term.hs19
1 files 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