never executed always true always false
1 module Conjure.UI.TranslateParameter ( translateParameter ) where
2
3 -- conjure
4 import Conjure.Prelude
5 import Conjure.Bug
6 import Conjure.UserError
7 import Conjure.Language.Definition
8 import Conjure.Language.Domain
9 import Conjure.Language.Constant
10 import Conjure.Language.Type
11 import Conjure.Language.Pretty
12 import Conjure.Language.Instantiate
13 import Conjure.Process.Enums ( removeEnumsFromParam )
14 import Conjure.Process.FiniteGivens ( finiteGivensParam )
15 import Conjure.Process.Enumerate ( EnumerateDomain )
16 import Conjure.Process.ValidateConstantForDomain ( validateConstantForDomain )
17 import Conjure.Representations ( downC )
18
19
20 translateParameter ::
21 MonadFailDoc m =>
22 MonadLog m =>
23 NameGen m =>
24 EnumerateDomain m =>
25 MonadIO m =>
26 (?typeCheckerMode :: TypeCheckerMode) =>
27 Bool -> -- Prepare input files for the Glasgow graph solver
28 Model -> -- eprime model
29 Model -> -- essence param
30 m Model -- eprime param
31
32 translateParameter graphSolver eprimeModel0 essenceParam0 = do
33 logDebug $ "[eprimeModel 0]" <+-> pretty eprimeModel0
34 logDebug $ "[essenceParam 0]" <+-> pretty essenceParam0
35 (eprimeModel, essenceParam1) <- removeEnumsFromParam eprimeModel0 essenceParam0
36 logDebug $ "[eprimeModel 1]" <+-> pretty eprimeModel
37 logDebug $ "[essenceParam 1]" <+-> pretty essenceParam1
38
39 let eprimeLettingsForEnums =
40 [ (nm, fromInt (genericLength vals))
41 | nm1 <- eprimeModel |> mInfo |> miEnumGivens
42 , Declaration (LettingDomainDefnEnum nm2 vals) <- essenceParam0 |> mStatements
43 , nm1 == nm2
44 , let nm = nm1 `mappend` "_EnumSize"
45 ]
46
47 (essenceParam, generatedLettingNames) <- finiteGivensParam eprimeModel essenceParam1 eprimeLettingsForEnums
48 logDebug $ "[essenceParam 2]" <+-> pretty essenceParam
49
50 let essenceLettings = extractLettings essenceParam
51 let essenceGivenNames = eprimeModel |> mInfo |> miGivens
52 let essenceGivens = eprimeModel |> mInfo |> miRepresentations
53 |> filter (\ (n,_) -> n `elem` essenceGivenNames )
54
55 logDebug $ "[essenceLettings ]" <+-> vcat [ pretty n <> ":" <+> pretty x | (n,x) <- essenceLettings ]
56 logDebug $ "[essenceGivenNames]" <+-> vcat (map pretty essenceGivenNames)
57 logDebug $ "[essenceGivens ]" <+-> vcat [ pretty n <> ":" <+> pretty x | (n,x) <- essenceGivens ]
58
59 -- some sanity checks here
60 -- TODO: check if for every given there is a letting (there can be more)
61 -- TODO: check if the same letting has multiple values for it
62 let missingLettings =
63 (essenceGivenNames ++ generatedLettingNames) \\
64 map fst essenceLettings
65 unless (null missingLettings) $
66 userErr1 $ "Missing values for parameters:" <++> prettyList id "," missingLettings
67
68 let extraLettings =
69 map fst essenceLettings \\
70 (essenceGivenNames ++ generatedLettingNames)
71 unless (null extraLettings) $
72 userErr1 $ "Too many letting statements in the parameter file:" <++> prettyList id "," extraLettings
73
74 let allLettings = (eprimeModel |> mInfo |> miLettings)
75 ++ essenceLettings
76 ++ map (second Constant) eprimeLettingsForEnums
77
78 essenceLettings' <- forM essenceLettings $ \ (name, val) -> do
79 constant <- instantiateExpression allLettings val
80 return (name, constant)
81 logDebug $ "[essenceLettings' ]" <+> vcat [ pretty n <> ":" <+-> pretty x | (n,x) <- essenceLettings' ]
82
83 essenceGivens' <- forM essenceGivens $ \ (name, dom) -> do
84 constant <- instantiateDomain allLettings dom
85 return (name, constant)
86 logDebug $ "[essenceGivens' ]" <+> vcat [ pretty n <> ":" <+-> pretty x | (n,x) <- essenceGivens' ]
87
88 essenceGivensAndLettings <- sequence
89 [ case lookup n essenceLettings' of
90 Nothing ->
91 if n `elem` map fst eprimeLettingsForEnums
92 then return Nothing
93 else userErr1 $ vcat
94 [ "No value for parameter:" <+> pretty n
95 , "With domain:" <+> pretty d
96 ]
97 Just v ->
98 if emptyCollection v
99 then do
100 (c, cTyMaybe) <- case v of
101 TypedConstant c cTy
102 | elem TypeAny (universe cTy) -- we may be able to do better!
103 -> return (c, Just cTy)
104 | otherwise
105 -> return (v, Nothing) -- already sufficiently typed
106 _ -> return (v, Just TypeAny) -- empty collection, unknown type
107 case cTyMaybe of
108 Nothing -> return $ Just (n, d, v)
109 Just cTy1 -> do
110 -- calculate the type of the domain, unify with the type we already have
111 cTy2 <- typeOfDomain d
112 let cTy = mostDefined [cTy1, cTy2]
113 if elem TypeAny (universe cTy)
114 then userErr1 $ vcat
115 [ "Cannot fully determine the type of parameter" <+> pretty n
116 , "Domain:" <+> pretty d
117 , "Value :" <+> pretty v
118 ]
119 else return $ Just (n, d, TypedConstant c cTy)
120 else return $ Just (n, d, v)
121 | (n, d) <- essenceGivens' ++ [ (n, DomainInt TagInt []) | n <- generatedLettingNames ]
122 ]
123 logDebug $ "[essenceGivensAndLettings ]" <+> vcat [ vcat [ "name :" <+> pretty n
124 , "domain :" <+> pretty d
125 , "constant:" <+-> pretty c
126 ]
127 | Just (n,d,c) <- essenceGivensAndLettings
128 ]
129
130 let f (Reference nm Nothing) =
131 case [ val | (nm2, val) <- eprimeLettingsForEnums, nm == nm2 ] of
132 [] -> bug ("translateParameter: No value for" <+> pretty nm)
133 [val] -> Constant val
134 _ -> bug ("translateParameter: Multiple values for" <+> pretty nm)
135 f p = p
136
137 let
138 essenceGivensAndLettings' :: [(Name, Domain HasRepresentation Constant, Constant)]
139 essenceGivensAndLettings' = transformBi f (catMaybes essenceGivensAndLettings)
140
141 logDebug $ "[essenceGivensAndLettings']" <+-> vcat [ vcat [ "name :" <+> pretty n
142 , "domain :" <+> pretty d
143 , "constant:" <+-> pretty c
144 ]
145 | (n,d,c) <- essenceGivensAndLettings'
146 ]
147
148 errs <- execWriterT $ forM_ essenceGivensAndLettings' $ \ (nm, dom, val) -> do
149 mres <- runExceptT $ validateConstantForDomain nm val dom
150 case mres of
151 Left err -> tell [err]
152 Right () -> return ()
153 unless (null errs) (userErr errs)
154
155 let
156 decorateWithType p@(_, _, TypedConstant{}) = return p
157 decorateWithType (name, domain, constant) | emptyCollection constant = do
158 ty <- typeOfDomain domain
159 return (name, domain, TypedConstant constant ty)
160 decorateWithType p = return p
161
162 when graphSolver $ do
163 forM_ essenceGivensAndLettings' $ \ (n,d,c) -> do
164 let pairs =
165 case d of
166 DomainFunction _ _ (DomainTuple [DomainInt{}, DomainInt{}]) _ ->
167 case c of
168 (viewConstantFunction -> Just rows) ->
169 [ case row of
170 (ConstantAbstract (AbsLitTuple [a, b]), _) -> [a,b]
171 _ -> []
172 | row <- rows ]
173 _ -> []
174 DomainRelation _ _ ([DomainInt{}, DomainInt{}, _]) ->
175 case c of
176 (viewConstantRelation -> Just rows) ->
177 [ case row of
178 [a, b, _] -> [a,b]
179 _ -> []
180 | row <- rows ]
181 _ -> []
182 _ -> []
183 let csvLines = [ pretty a <> "," <> pretty b | [a,b] <- sortNub pairs ]
184 unless (null pairs) $
185 liftIO $ writeFile ("given-" ++ show (pretty n) ++ ".csv") (render 100000 (vcat csvLines))
186
187 let essenceFindNames = eprimeModel |> mInfo |> miFinds
188 let essenceFinds = eprimeModel |> mInfo |> miRepresentations |> filter (\ (n,_) -> n `elem` essenceFindNames )
189 forM_ essenceFinds $ \ (n, d) -> do
190 case d of
191 DomainFunction _ _ (DomainInt _ [RangeBounded a b]) _ -> do
192 a' <- instantiateExpression allLettings a
193 b' <- instantiateExpression allLettings b
194 case (a', b') of
195 (ConstantInt _ a'', ConstantInt _ b'') -> do
196 let csvLines =
197 [ pretty i <> "," <> name
198 | i <- [a''..b'']
199 , let name = pretty n <> "_Function1D_" <> pretty (padLeft 5 '0' (show i))
200 ]
201 unless (null csvLines) $
202 liftIO $ writeFile ("find-" ++ show (pretty n) ++ ".csv") (render 100000 (vcat csvLines))
203 _ -> userErr1 $ "Unsupported domain for --graph-solver:" <+> pretty d
204 _ -> return ()
205
206
207 eprimeLettings
208 :: [(Name, Domain HasRepresentation Constant, Constant)]
209 <- failToUserError $ concatMapM downC essenceGivensAndLettings' >>= mapM decorateWithType
210 logDebug $ "[eprimeLettings ]" <+> vcat [ vcat [ "name :" <+> pretty n
211 , "domain :" <+> pretty d
212 , "constant:" <+-> pretty c
213 ]
214 | (n,d,c) <- eprimeLettings
215 ]
216
217 return $ languageEprime def
218 { mStatements = transformBi (\ _ -> TagInt) $
219 [ Declaration (Letting n (Constant x))
220 | (n, _, x) <- eprimeLettings
221 ] ++
222 [ Declaration (Letting n (Constant x))
223 | (n, x) <- eprimeLettingsForEnums
224 ]
225 }