diff options
| -rw-r--r-- | Library/Term.hs | 38 | ||||
| -rw-r--r-- | Library/TypeVar.hs | 19 |
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 + |