summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJed Barber <jjbarber@y7mail.com>2012-10-04 22:23:41 +1000
committerJed Barber <jjbarber@y7mail.com>2012-10-04 22:23:41 +1000
commit986cc4ac3d0fe32417338671dd6db2eeb54442a3 (patch)
treef392f0caabb7c13fa9f96aeb1d39e125cab91b54
parent102f42fa347b10190704562ae3638f5683772211 (diff)
Alpha equivalence typing fixed
-rw-r--r--Library/Term.hs38
-rw-r--r--Library/TypeVar.hs19
2 files changed, 35 insertions, 22 deletions
diff --git a/Library/Term.hs b/Library/Term.hs
index ee5089c..bac25a0 100644
--- a/Library/Term.hs
+++ b/Library/Term.hs
@@ -20,6 +20,7 @@ module Library.Term (
import Data.List
+import Data.Maybe
import qualified Data.Set as Set
import qualified Data.Map as Map
import Library.TypeVar
@@ -56,7 +57,7 @@ alphaEquiv a b =
let equiv = \term1 term2 varmap1 varmap2 depth ->
case (term1,term2) of
(TConst a1 b1, TConst a2 b2) ->
- a1 == a2
+ a1 == a2 && b1 == b2
(TApp a1 b1, TApp a2 b2) ->
equiv a1 a2 varmap1 varmap2 depth &&
@@ -68,8 +69,8 @@ alphaEquiv a b =
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) ||
- Map.lookup (Var name1 type1) varmap1 == Map.lookup (Var name2 type2) varmap2
+ type1 == 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
@@ -88,34 +89,31 @@ alphaConvertList a b = map (\x -> alphaConvert (fst x) (snd x)) (zip a b)
substitute :: Substitution -> Term -> Term
-substitute (tymap,vmap) term =
+substitute (t,v) term =
let typesub =
(\x y ->
case y of
- (TConst a ty) -> if (ty == (TypeVar . fst $ x))
- then TConst a (snd x)
- else TConst a ty
+ (TConst a ty) -> TConst a (typeVarSub x ty)
(TApp a b) -> TApp (typesub x a) (typesub x b)
- (TAbs (TVar (Var n ty)) a) -> if (ty == (TypeVar . fst $ x))
- then TAbs (TVar (Var n (snd x))) (typesub x a)
- else TAbs (TVar (Var n ty)) (typesub x a)
- (TVar (Var n ty)) -> if (ty == (TypeVar . fst $ x))
- then TVar (Var n (snd x))
- else TVar (Var n ty))
+ (TAbs (TVar (Var n ty)) a) -> TAbs (TVar (Var n (typeVarSub x ty))) (typesub x a)
+ (TVar (Var n ty)) -> TVar (Var n (typeVarSub x ty)))
+
varsub =
(\x y ->
case y of
(TConst a ty) -> TConst a ty
(TApp a b) -> TApp (varsub x a) (varsub x b)
- (TVar v) -> if (v == (fst x))
- then snd x
+ (TVar v) -> if (Map.member v x)
+ then fromJust (Map.lookup v x)
else TVar v
- (TAbs v a) -> let safe = rename (TAbs v a) (Set.insert (fst x) (freeVars . snd $ x))
+ (TAbs v a) -> let safe = rename (TAbs v a) (Set.union (Map.keysSet x) (Set.unions . (map freeVars) . (Map.elems) $ x))
in case safe of
- (TAbs m n) -> TAbs m (varsub x n))
- tydone = foldl' (\x y -> typesub y x) term tymap
- vdone = foldl' (\x y -> varsub y x) tydone vmap
- in vdone
+ (TAbs m n) -> TAbs m (varsub x n))
+
+ tymap = foldl' (\z (x,y) -> Map.insert x y z) Map.empty t
+ vmap = foldl' (\z (x,y) -> Map.insert x y z) Map.empty v
+
+ in (varsub vmap) . (typesub tymap) $ term
boundVars :: Term -> Set.Set Var
diff --git a/Library/TypeVar.hs b/Library/TypeVar.hs
index 078d5d3..d2915e6 100644
--- a/Library/TypeVar.hs
+++ b/Library/TypeVar.hs
@@ -15,13 +15,17 @@ module Library.TypeVar (
typeFunc,
typeBool,
typeVarsInType,
- isTypeVar
+ isTypeVar,
+ typeVarSub
) where
import Data.List
+import Data.Maybe
import qualified Data.Set as Set
+import Data.Map( Map, (!) )
+import qualified Data.Map as Map
@@ -50,7 +54,9 @@ instance Show TypeOp where
show a = "typeOp " ++ (show $ tyOp a)
instance Show Type where
- show (TypeVar tyVar) = "typeVar " ++ (show tyVar)
+ show (TypeVar tyVar) = "V " ++ (show tyVar)
+ show (AType [] (TypeOp (Name [] "bool"))) = "bool"
+ show (AType [d,r] (TypeOp (Name [] "->"))) = "(" ++ show d ++ " -> " ++ show r ++ ")"
show (AType list typeOp) = "type " ++ (show $ tyOp typeOp) ++ " " ++ (show list)
instance Show Const where
@@ -82,3 +88,12 @@ isTypeVar :: Type -> Bool
isTypeVar (TypeVar _) = True
isTypeVar _ = False
+
+typeVarSub :: Map Name Type -> Type -> Type
+typeVarSub m (TypeVar a) =
+ if (Map.member a m)
+ then fromJust (Map.lookup a m)
+ else TypeVar a
+typeVarSub m (AType list op) =
+ AType (map (typeVarSub m) list) op
+