From 04dd12a2b2207bef9381378c28887b59aa50419e Mon Sep 17 00:00:00 2001 From: Andre Pacak Date: Sat, 28 Sep 2019 11:04:55 +0200 Subject: [PATCH] fo recursive type continue after failure transformation --- .../src/FORecursiveTypes/ContinueAfterFail.hs | 189 ++++++++++++++++++ .../FORecursiveTypes/ContinueAfterFailSpec.hs | 25 +++ 2 files changed, 214 insertions(+) create mode 100644 haskell/src/FORecursiveTypes/ContinueAfterFail.hs create mode 100644 haskell/test/FORecursiveTypes/ContinueAfterFailSpec.hs diff --git a/haskell/src/FORecursiveTypes/ContinueAfterFail.hs b/haskell/src/FORecursiveTypes/ContinueAfterFail.hs new file mode 100644 index 0000000..3be4812 --- /dev/null +++ b/haskell/src/FORecursiveTypes/ContinueAfterFail.hs @@ -0,0 +1,189 @@ +{-# LANGUAGE ConstraintKinds, TypeFamilies #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE RebindableSyntax #-} +module FORecursiveTypes.ContinueAfterFail where + +import Prelude hiding (Monad(..), (>=), (<=), lookup) +import GHC.Exts (Constraint) +import Data.List(find) +import Data.Map(Map) +import qualified Data.Map as Map + +import FORecursiveTypes.Language +import Util.ErrorMessages + +-- is needed because we use the RebindableSyntax extension +ifThenElse :: Bool -> a -> a -> a +ifThenElse True thn _ = thn +ifThenElse False _ els = els + +type Error = [String] + +data Infer a + = Inferred a + | NotInferred Error deriving (Eq, Show) + +type Check = Infer () + +instance Functor Infer where + fmap _ (NotInferred err) = NotInferred err + fmap f (Inferred ty) = Inferred $ f ty + +instance Applicative Infer where + pure = Inferred + (NotInferred err) <*> _ = NotInferred err + (Inferred a) <*> something = fmap a something + +class WithTop a where + top :: a + +instance WithTop Type where + top = AnyType + +instance WithTop () where + top = () + +instance (WithTop a, WithTop b) => WithTop (a, b) where + top = (top, top) + +instance WithTop a => WithTop [a] where + top = [top] + +instance WithTop a => WithTop (Map Name a) where + top = Map.empty + +-- Had to define an own monad type class. +-- It is not possible otherwise to get the type constraint WithTop a. +-- We use the extension ConstraintKinds to support this. +-- Could not find a simpler solution for this problem. +-- The restricted monad problem is common. +class RMonad m where + type RMonadCtx m a :: Constraint + return :: RMonadCtx m a => a -> m a + (>>=) :: (RMonadCtx m a, RMonadCtx m b) => m a -> (a -> m b) -> m b + (>>) :: (RMonadCtx m a, RMonadCtx m b) => m a -> m b -> m b + m >> k = m >>= \_ -> k + fail :: [String] -> m a + +instance RMonad Infer where + type RMonadCtx Infer a = WithTop a + return = Inferred + (Inferred ty) >>= f = f ty + NotInferred err1 >>= f = + -- we know that top is Inferred AnyType, (AnyType, AnyType) or () by definition + case f top of + Inferred _ -> fail err1 + NotInferred err2 -> fail $ err1 ++ err2 + fail = NotInferred + +-- matching functions that extract the inner types if possible +-- one problem is that we do not get as good error messages, because term is not known in these functions +matchNat :: Type -> String -> Check +matchNat Nat _ = return () +matchNat ty err = fail [natError ty err] + +matchFun :: Type -> String -> Infer (Type, Type) +matchFun (Fun ty1 ty2) _ = return (ty1, ty2) +matchFun ty err = fail [funError ty err] + +matchType :: Type -> Type -> String -> Check +matchType ty1 ty2 _ + | ty1 == ty2 = return () +matchType ty1 ty2 err = fail [generalError (show ty1) ty2 err] + +matchSum :: Type -> String -> Infer (Type, Type) +matchSum (Sum ty1 ty2) _ = return (ty1, ty2) +matchSum ty err = fail [sumError ty err] + +matchVariant :: Type -> String -> Infer (Map.Map Name Type) +matchVariant (Variant types) _ = return types +matchVariant ty err = fail [variantError ty err] + +lookupTypeVar :: TypeMap -> Name -> Infer Type +lookupTypeVar Empty x = fail ["Unbound type variable " ++ show x] +lookupTypeVar (Bind c x t) y + | x == y = return t + | otherwise = lookup c y + +matchTypeVar :: TypeMap -> Type -> Infer Type +matchTypeVar tymap (TypeVar x) = lookupTypeVar tymap x +matchTypeVar _ ty = return ty + +liftMaybe :: WithTop a => Maybe a -> String -> Infer a +liftMaybe (Just a) _ = return a +liftMaybe Nothing err = fail [err] + +lookup :: Ctx -> Name -> Infer Type +lookup Empty x = fail ["Unbound variable " ++ show x] +lookup (Bind c x t) y + | x == y = return t + | otherwise = lookup c y + +inferType :: Ctx -> TypeMap -> Term -> Infer Type +inferType _ _ (Unit _) = return UnitT +inferType _ _ (Zero _) = return Nat +inferType ctx tymap (Succ t _) = do + checkType ctx tymap t Nat + return Nat +inferType ctx tymap (Add t1 t2 _) = do + checkType ctx tymap t1 Nat + checkType ctx tymap t2 Nat + return Nat +inferType ctx tymap (Mult t1 t2 _) = do + checkType ctx tymap t1 Nat + checkType ctx tymap t2 Nat + return Nat +inferType ctx _ (Var name _) = lookup ctx name +inferType ctx tymap (Let name t body _) = do + tyt <- inferType ctx tymap t + inferType (Bind ctx name tyt) tymap body +inferType ctx tymap (Anno term ty _) = do + checkType ctx tymap term ty + return ty +inferType ctx tymap (App t1 t2 _) = do + ty <- inferType ctx tymap t1 + rty <- matchTypeVar tymap ty + (ty1, ty2) <- matchFun rty (show t1) + checkType ctx tymap t2 ty1 + return ty2 +inferType ctx tymap (LetType n ty t _) = inferType ctx (Bind tymap n ty) t +inferType _ _ t = fail ["Cannot infer type of term " ++ show t] + +checkType :: Ctx -> TypeMap -> Term -> Type -> Check +checkType ctx tymap p@(Lam name t _) ty = do + rty <- matchTypeVar tymap ty + (ty1, ty2) <- matchFun rty (show p) + checkType (Bind ctx name ty1) tymap t ty2 +checkType ctx tymap p@(InL t _) ty = do + rty <- matchTypeVar tymap ty + (ty1, ty2) <- matchSum rty (show p) + checkType ctx tymap t ty1 +checkType ctx tymap p@(InR t _) ty = do + rty <- matchTypeVar tymap ty + (ty1, ty2) <- matchSum rty (show p) + checkType ctx tymap t ty2 +checkType ctx tymap p@(Case e n1 t1 n2 t2 _) ty = do + ety <- inferType ctx tymap e + rty <- matchTypeVar tymap ety + (ty1, ty2) <- matchSum rty (show e) + checkType (Bind ctx n1 ty1) tymap t1 ty + checkType (Bind ctx n2 ty2) tymap t2 ty +checkType ctx tymap p@(Tag n t _) ty = do + rty <- matchTypeVar tymap ty + types <- matchVariant rty (show p) + let lty = Map.lookup n types + (maybe (fail [""]) (checkType ctx tymap t) lty) +checkType ctx tymap p@(Match m cases _) ty = do + ety <- inferType ctx tymap m + rty <- matchTypeVar tymap ety + types <- matchVariant rty (show m) + let subchecks = + map (\(l, x, t) -> do + lty <- liftMaybe (Map.lookup l types) "Could not find labeled type" + checkType (Bind ctx x lty) tymap t ty + ) cases + foldl (>>) (return ()) subchecks + +checkType ctx tymap t ty = do + ty' <- inferType ctx tymap t + matchType ty ty' (show t) diff --git a/haskell/test/FORecursiveTypes/ContinueAfterFailSpec.hs b/haskell/test/FORecursiveTypes/ContinueAfterFailSpec.hs new file mode 100644 index 0000000..f279ce4 --- /dev/null +++ b/haskell/test/FORecursiveTypes/ContinueAfterFailSpec.hs @@ -0,0 +1,25 @@ +{-# LANGUAGE FlexibleInstances #-} + +module FORecursiveTypes.ContinueAfterFailSpec where + +import Prelude hiding (lookup,(*), (**)) +import Test.Hspec + +import FORecursiveTypes.Base as B +import FORecursiveTypes.SharedSpecs +import FORecursiveTypes.ContinueAfterFail as C +import FORecursiveTypes.Language + + +instance ConvertToBInfer C.Infer where + convert (C.Inferred ty) = B.Inferred ty + convert (C.NotInferred err) = B.NotInferred $ head err + + +main :: IO () +main = hspec spec + +spec :: Spec +spec = sharedSpec $ C.inferType Empty Empty + + -- GitLab