diff options
-rw-r--r-- | Term.hs | 9 | ||||
-rw-r--r-- | TypeVar.hs | 5 |
2 files changed, 13 insertions, 1 deletions
@@ -147,7 +147,7 @@ rename (TAbs (TVar v) t) vars = typeOf :: Term -> Type -typeOf (TConst c ty) = ty +typeOf (TConst _ ty) = ty typeOf (TVar v) = varTy v typeOf (TAbs v t) = typeFunc (typeOf v) (typeOf t) typeOf (TApp f _) = @@ -155,6 +155,13 @@ typeOf (TApp f _) = last . aType . typeOf $ f +typeVarsInTerm :: Term -> Set Type +typeVarsInTerm (TConst _ ty) = typeVarsInType ty +typeVarsInTerm (TVar v) = typeVarsInType . varTy $ v +typeVarsInTerm (TAbs v t) = Set.union (typeVarsInType . varTy $ v) (typeVarsInTerm t) +typeVarsInTerm (TApp f x) = Set.union (typeVarsInTerm f) (typeVarsInTerm x) + + mkEquals :: Term -> Term -> Term mkEquals lhs rhs = let eqConst = TConst (Const (Name [] "=")) (mkEqualsType (typeOf lhs)) @@ -63,3 +63,8 @@ mkEqualsType ty = typeFunc (AType [] (TypeOp (Name [] "bool"))) (typeFunc ty ty) typeFunc :: Type -> Type -> Type typeFunc ty1 ty2 = AType [ty1,ty2] (TypeOp (Name [] "->")) + + +typeVarsInType :: Type -> Set Type +typeVarsInType (TypeVar t) = Set.singleton (TypeVar t) +typeVarsInType (AType list _) = unions . (map typeVarsInType) $ list |