never executed always true always false
1 {-# LANGUAGE TupleSections #-}
2 {-# LANGUAGE QuasiQuotes #-}
3
4 module Conjure.UI.TypeCheck ( typeCheckModel_StandAlone, typeCheckModel ) where
5
6 -- conjure
7 import Conjure.Prelude
8 import Conjure.UserError
9 import Conjure.Language.Definition
10 import Conjure.Language.Domain
11 import Conjure.Language.Type
12 import Conjure.Language.TypeOf
13 import Conjure.Language.CategoryOf ( categoryChecking )
14 import Conjure.Language.Pretty
15 import Conjure.Language.Lenses
16 import Conjure.Language.TH ( essence )
17 import Conjure.Process.Enums ( removeEnumsFromModel )
18 import Conjure.Process.Unnameds ( removeUnnamedsFromModel )
19 import Conjure.Language.NameResolution ( resolveNames )
20 import Conjure.Process.Sanity ( sanityChecks )
21
22
23
24 typeCheckModel_StandAlone ::
25 MonadFailDoc m =>
26 MonadUserError m =>
27 MonadLog m =>
28 NameGen m =>
29 (?typeCheckerMode :: TypeCheckerMode) =>
30 Model -> m Model
31 typeCheckModel_StandAlone model0 = do
32 -- for better error messages, type-check and category-check before sanity-checking.
33 -- sanity checking will modify the model.
34 -- then, type-check once more just in case the newly generated
35 -- stuff is broken.
36 model1 <- return model0 >>= logDebugId "[input]"
37 >>= removeUnnamedsFromModel >>= logDebugId "[removeUnnamedsFromModel]"
38 >>= removeEnumsFromModel >>= logDebugId "[removeEnumsFromModel]"
39 >>= resolveNames >>= logDebugId "[resolveNames]"
40 >>= typeCheckModel >>= logDebugId "[typeCheckModel]"
41 >>= categoryChecking >>= logDebugId "[categoryChecking]"
42 >>= sanityChecks >>= logDebugId "[sanityChecks]"
43 >>= typeCheckModel >>= logDebugId "[typeCheckModel]"
44 return model1
45
46
47 typeCheckModel ::
48 MonadFail m =>
49 MonadUserError m =>
50 (?typeCheckerMode :: TypeCheckerMode) =>
51 Model -> m Model
52 typeCheckModel model1 = do
53 let model2 = fixRelationProj model1
54 (statements3, errs) <- runWriterT $ forM (mStatements model2) $ \ st ->
55 case st of
56 Declaration decl -> do
57 case decl of
58 FindOrGiven _ _ domain ->
59 case domain of
60 DomainReference{} ->
61 -- no need to raise an error here if this is a reference to another domain
62 -- because must have already we raised the error in the "letting" of that domain
63 return ()
64 _ -> do
65 mty <- runExceptT $ typeOfDomain domain
66 case mty of
67 Right _ -> return ()
68 Left err -> tell $ return $ vcat
69 [ "In a declaration statement:" <++> pretty st
70 , "Error:" <++> pretty err
71 ]
72 Letting _ x -> do
73 mty <- runExceptT $ case x of
74 Domain y -> typeOfDomain y
75 _ -> typeOf x
76 case mty of
77 Right _ -> return ()
78 Left err -> tell $ return $ vcat
79 [ "In a letting statement:" <++> pretty st
80 , "Error:" <++> pretty err
81 ]
82 GivenDomainDefnEnum{} -> return ()
83 LettingDomainDefnEnum{} -> return ()
84 LettingDomainDefnUnnamed _ x -> do
85 mty <- runExceptT $ typeOf x
86 case mty of
87 Right TypeInt{} -> return ()
88 Left err -> tell $ return $ vcat
89 [ "In the declaration of an unnamed type:" <++> pretty st
90 , "Error:" <++> pretty err
91 ]
92 Right ty -> tell $ return $ vcat
93 [ "In the declaration of an unnamed type:" <++> pretty st
94 , "Expected type `int`, but got:" <++> pretty ty
95 ]
96 return st
97 SearchOrder xs -> do
98 forM_ xs $ \case
99 BranchingOn{} -> return () -- TODO: check if the name is defined
100 Cut x -> do
101 mty <- runExceptT $ typeOf x
102 case mty of
103 Right TypeBool{} -> return ()
104 Left err -> tell $ return $ vcat
105 [ "In a 'branching on' statement:" <++> pretty x
106 , "Error:" <++> pretty err
107 ]
108 Right ty -> tell $ return $ vcat
109 [ "In a 'branching on' statement:" <++> pretty x
110 , "Expected type `bool`, but got:" <++> pretty ty
111 ]
112 return st
113 SearchHeuristic{} -> return st
114 Where xs -> do
115 xs' <- forM xs $ \ x -> do
116 mty <- runExceptT $ typeOf x
117 case mty of
118 Right TypeBool{} -> return x
119 Right (TypeList TypeBool) -> return (make opAnd x)
120 Right (TypeMatrix _ TypeBool) -> return (make opAnd x)
121 Left err -> do
122 tell $ return $ vcat
123 [ "In a 'where' statement:" <++> pretty x
124 , "Error:" <++> pretty err
125 ]
126 return x
127 Right ty -> do
128 tell $ return $ vcat
129 [ "In a 'where' statement:" <++> pretty x
130 , "Expected type `bool`, but got:" <++> pretty ty
131 ]
132 return x
133 return (Where xs')
134 Objective minMax x -> do
135 mty <- runExceptT $ typeOf x
136 let
137 go TypeInt{} o = return o
138 go (TypeTuple ts) o =
139 fromList <$> sequence [ go t [essence| &o[&i] |]
140 | (i', t) <- zip allNats ts
141 , let i :: Expression = fromInt i'
142 ]
143 go (TypeMatrix _ t) (AbstractLiteral (AbsLitMatrix _ os)) =
144 fromList <$> sequence [ go t o | o <- os ]
145 go t o = do
146 tell $ return $ vcat
147 [ "In the objective:" <++> pretty st
148 , "Expected type `int`, but got:" <++> pretty t
149 , "Expression:" <+> pretty o
150 ]
151 return o
152 case mty of
153 Right ty -> do
154 x' <- go ty x
155 return (Objective minMax x')
156 Left err -> do
157 tell $ return $ vcat
158 [ "In the objective:" <++> pretty st
159 , "Error:" <++> pretty err
160 ]
161 return st
162 SuchThat xs -> do
163 xs' <- forM xs $ \ x -> do
164 mty <- runExceptT $ typeOf x
165 case mty of
166 Right TypeBool{} -> return x
167 Right (TypeList TypeBool) -> return (make opAnd x)
168 Right (TypeMatrix _ TypeBool) -> return (make opAnd x)
169 Left err -> do
170 tell $ return $ vcat
171 [ "In a 'such that' statement:" <++> pretty x
172 , "Error:" <++> pretty err
173 ]
174 return x
175 Right ty -> do
176 tell $ return $ vcat
177 [ "In a 'such that' statement:" <++> pretty x
178 , "Expected type `bool`, but got:" <++> pretty ty
179 ]
180 return x
181 return (SuchThat xs')
182 unless (null errs) (userErr errs)
183
184 -- now that everything knows its type, we can recover
185 -- DomainInt [RangeSingle x] from DomainIntE x, if x has type int
186 let
187 domainIntERecover :: forall m . MonadFailDoc m => Domain () Expression -> m (Domain () Expression)
188 domainIntERecover d@(DomainIntE x) = do
189 ty <- runExceptT $ typeOf x
190 return $ case ty of
191 Right (TypeInt t) -> DomainInt t [RangeSingle x]
192 _ -> d
193 domainIntERecover d = return d
194 statements4 <- transformBiM domainIntERecover statements3
195
196 return model2 { mStatements = statements4 }
197