on 96dfd88 help sign in
elk/src/Type/ExtraChecks.hs
155 lines 5.9 kB history raw
1{-# OPTIONS_GHC -Wall #-}
3{-| This module contains checks to be run *after* type inference has completed
4successfully. At that point we still need to do occurs checks and ensure that
5`main` has an acceptable type.
6-}
7module Type.ExtraChecks (mainType, occurs, portTypes) where
9import Control.Applicative ((<$>),(<*>))
10import Control.Monad.Error
11import Control.Monad.State
12import qualified Data.Map as Map
13import qualified Data.Traversable as Traverse
14import qualified Data.UnionFind.IO as UF
15import Text.PrettyPrint as P
17import qualified AST.Annotation as A
18import qualified AST.Expression.Canonical as Canonical
19import qualified AST.PrettyPrint as PP
20import qualified AST.Type as ST
21import qualified AST.Variable as V
22import qualified Transform.Expression as Expr
23import qualified Type.Type as TT
24import qualified Type.State as TS
26throw :: [Doc] -> Either [Doc] a
27throw err = Left [ P.vcat err ]
29mainType :: TS.Env -> ErrorT [P.Doc] IO (Map.Map String ST.CanonicalType)
30mainType environment =
31 do environment' <- liftIO $ Traverse.traverse TT.toSrcType environment
32 mainCheck environment'
33 where
34 mainCheck :: (Monad m) => Map.Map String ST.CanonicalType
35 -> ErrorT [P.Doc] m (Map.Map String ST.CanonicalType)
36 mainCheck env =
37 case Map.lookup "main" env of
38 Nothing -> return env
39 Just typeOfMain
40 | tipe `elem` acceptable -> return env
41 | otherwise -> throwError err
42 where
43 acceptable = [ "Graphics.Element.Element"
44 , "Signal.Signal Graphics.Element.Element" ]
46 tipe = PP.renderPretty typeOfMain
47 err = [ P.text "Type Error: 'main' must have type Element or (Signal Element)."
48 , P.text "Instead 'main' has type:\n"
49 , P.nest 4 (PP.pretty typeOfMain)
50 , P.text " " ]
52data Direction = In | Out
54portTypes :: (Monad m) => Canonical.Expr -> ErrorT [P.Doc] m ()
55portTypes expr =
56 case Expr.checkPorts (check In) (check Out) expr of
57 Left err -> throwError err
58 Right _ -> return ()
59 where
60 check = isValid True False False
61 isValid isTopLevel seenFunc seenSignal direction name tipe =
62 case tipe of
63 ST.Aliased _ t -> valid t
65 ST.Type v ->
66 case any ($ v) [ V.isJson, V.isPrimitive, V.isTuple ] of
67 True -> return ()
68 False -> err "an unsupported type"
70 ST.App t [] -> valid t
72 ST.App (ST.Type v) [t]
73 | V.isSignal v -> handleSignal t
74 | V.isMaybe v -> valid t
75 | V.isArray v -> valid t
76 | V.isList v -> valid t
78 ST.App (ST.Type v) ts
79 | V.isTuple v -> mapM_ valid ts
81 ST.App _ _ -> err "an unsupported type"
83 ST.Var _ -> err "free type variables"
85 ST.Lambda _ _ ->
86 case direction of
87 In -> err "functions"
88 Out | seenFunc -> err "higher-order functions"
89 | seenSignal -> err "signals that contain functions"
90 | otherwise ->
91 forM_ (ST.collectLambdas tipe)
92 (isValid' True seenSignal direction name)
94 ST.Record _ (Just _) -> err "extended records with free type variables"
96 ST.Record fields Nothing ->
97 mapM_ (\(k,v) -> (,) k <$> valid v) fields
99 where
100 isValid' = isValid False
101 valid = isValid' seenFunc seenSignal direction name
103 handleSignal t
104 | seenFunc = err "functions that involve signals"
105 | seenSignal = err "signals-of-signals"
106 | isTopLevel = isValid' seenFunc True direction name t
107 | otherwise = err "a signal within a data stucture"
109 dir inMsg outMsg = case direction of { In -> inMsg ; Out -> outMsg }
110 txt = P.text . concat
112 err kind =
113 throw $
114 [ txt [ "Type Error: the value ", dir "coming in" "sent out"
115 , " through port '", name, "' is invalid." ]
116 , txt [ "It contains ", kind, ":\n" ]
117 , P.nest 4 (PP.pretty tipe) <> P.text "\n"
118 , txt [ "Acceptable values for ", dir "incoming" "outgoing", " ports include:" ]
119 , txt [ " Ints, Floats, Bools, Strings, Maybes, Lists, Arrays, Tuples, unit values," ]
120 , txt [ " Json.Values, ", dir "" "first-order functions, ", "and concrete records." ]
121 ]
123occurs :: (String, TT.Variable) -> StateT TS.SolverState IO ()
124occurs (name, variable) =
125 do vars <- liftIO $ infiniteVars [] variable
126 case vars of
127 [] -> return ()
128 var:_ -> do
129 desc <- liftIO $ UF.descriptor var
130 case TT.structure desc of
131 Nothing ->
132 modify $ \s -> s { TS.sErrors = P.text msg : TS.sErrors s }
133 Just _ ->
134 do liftIO $ UF.setDescriptor var (desc { TT.structure = Nothing })
135 var' <- liftIO $ UF.fresh desc
136 TS.addError (A.None (P.text name)) (Just msg) var var'
137 where
138 msg = "Infinite types are not allowed"
140 infiniteVars :: [TT.Variable] -> TT.Variable -> IO [TT.Variable]
141 infiniteVars seen var =
142 let go = infiniteVars (var:seen) in
143 if var `elem` seen
144 then return [var]
145 else do
146 desc <- UF.descriptor var
147 case TT.structure desc of
148 Nothing -> return []
149 Just struct ->
150 case struct of
151 TT.App1 a b -> (++) <$> go a <*> go b
152 TT.Fun1 a b -> (++) <$> go a <*> go b
153 TT.Var1 a -> go a
154 TT.EmptyRecord1 -> return []
155 TT.Record1 fields ext -> concat <$> mapM go (ext : concat (Map.elems fields))