never executed always true always false
1 module Conjure.UI.ValidateSolution ( validateSolution ) where
2
3 -- conjure
4 import Conjure.Bug
5 import Conjure.Prelude
6 import Conjure.UserError
7 import Conjure.Language.Expression.Op
8 import Conjure.Language.Definition
9 import Conjure.Language.Constant
10 import Conjure.Language.Domain
11 import Conjure.Language.Pretty
12 import Conjure.Language.Type
13 import Conjure.Language.TypeOf
14 import Conjure.Language.Instantiate
15 import Conjure.Process.Enumerate ( EnumerateDomain )
16 import Conjure.Process.ValidateConstantForDomain ( validateConstantForDomain )
17
18
19 validateSolution ::
20 MonadFailDoc m =>
21 NameGen m =>
22 EnumerateDomain m =>
23 (?typeCheckerMode :: TypeCheckerMode) =>
24 Model -> -- essence model
25 Model -> -- essence param
26 Model -> -- essence solution
27 m ()
28 validateSolution essenceModel essenceParam essenceSolution = flip evalStateT [] $
29 forM_ (mStatements essenceModel) $ \ st -> do
30 mapM_ introduceRecordFields (universeBi st :: [Domain () Expression])
31 case st of
32 Declaration (FindOrGiven Given nm dom) ->
33 case [ val | Declaration (Letting nm2 val) <- mStatements essenceParam, nm == nm2 ] of
34 [val] -> do
35 valC <- gets id >>= flip instantiateExpression val
36 valC_typed <- case valC of
37 TypedConstant c tyc -> do
38 ty <- typeOfDomain dom
39 return $ TypedConstant c (mostDefined [ty, tyc])
40 _ -> return valC
41 DomainInConstant domC <- gets id >>= flip instantiateExpression (Domain dom)
42 failToUserError $ validateConstantForDomain nm valC domC
43 modify ((nm, Constant valC_typed) :)
44 [] -> userErr1 $ vcat [ "No value for" <+> pretty nm <+> "in the parameter file."
45 , "Its domain:" <++> pretty dom
46 ]
47 vals -> userErr1 $ vcat [ "Multiple values for" <+> pretty nm <+> "in the parameter file."
48 , "Its domain:" <++> pretty dom
49 , "Values:" <++> vcat (map pretty vals)
50 ]
51 Declaration (FindOrGiven Find nm dom) ->
52 case [ val | Declaration (Letting nm2 val) <- mStatements essenceSolution, nm == nm2 ] of
53 [val] -> do
54 valC <- gets id >>= flip instantiateExpression val
55 valC_typed <- case valC of
56 TypedConstant c tyc -> do
57 ty <- typeOfDomain dom
58 return $ TypedConstant c (mostDefined [ty, tyc])
59 _ -> return valC
60 DomainInConstant domC <- gets id >>= flip instantiateExpression (Domain dom)
61 failToUserError $ validateConstantForDomain nm valC domC
62 modify ((nm, Constant valC_typed) :)
63 [] -> userErr1 $ vcat [ "No value for" <+> pretty nm <+> "in the solution file."
64 , "Its domain:" <++> pretty dom
65 ]
66 vals -> userErr1 $ vcat [ "Multiple values for" <+> pretty nm <+> "in the solution file."
67 , "Its domain:" <++> pretty dom
68 , "Values:" <++> vcat (map pretty vals)
69 ]
70 Declaration (FindOrGiven Quantified _ _) ->
71 userErr1 $ vcat
72 [ "A quantified declaration at the top level."
73 , "This should never happen."
74 , "Statement:" <+> pretty st
75 ]
76 Declaration (FindOrGiven LocalFind _ _) ->
77 userErr1 $ vcat
78 [ "A local decision variable at the top level."
79 , "This should never happen."
80 , "Statement:" <+> pretty st
81 ]
82 Declaration (FindOrGiven CutFind _ _) ->
83 userErr1 $ vcat
84 [ "A 'cut' decision variable at the top level."
85 , "This should never happen."
86 , "Statement:" <+> pretty st
87 ]
88 Declaration (Letting nm val) -> modify ((nm, val) :)
89 Declaration (GivenDomainDefnEnum nm@(Name nmText)) ->
90 case [ val | Declaration (LettingDomainDefnEnum nm2 val) <- mStatements essenceParam, nm == nm2 ] of
91 [val] -> do
92 let domain = mkDomainIntBTagged (TagEnum nmText) 1 (fromInt (genericLength val))
93 let values = [ (n, Constant (ConstantInt (TagEnum nmText) i))
94 | (n, i) <- zip val allNats
95 ]
96 modify (((nm, Domain domain) : values) ++)
97 [] -> userErr1 $ vcat [ "No value for enum domain" <+> pretty nm <+> "in the parameter file."
98 ]
99 vals -> userErr1 $ vcat [ "Multiple values for enum domain" <+> pretty nm <+> "in the parameter file."
100 , "Values:" <++> vcat (map (prettyList prBraces ",") vals)
101 ]
102 Declaration GivenDomainDefnEnum{} ->
103 bug "validateSolution GivenDomainDefnEnum, some other type of Name"
104 Declaration (LettingDomainDefnEnum nm@(Name nmText) val) -> do
105 let domain = mkDomainIntBTagged (TagEnum nmText) 1 (fromInt (genericLength val))
106 let values = [ (n, Constant (ConstantInt (TagEnum nmText) i))
107 | (n, i) <- zip val allNats
108 ]
109 modify (((nm, Domain domain) : values) ++)
110 Declaration (LettingDomainDefnEnum{}) ->
111 bug "validateSolution LettingDomainDefnEnum, some other type of Name"
112 Declaration (LettingDomainDefnUnnamed nm@(Name nmText) _) ->
113 case [ nms | Declaration (LettingDomainDefnEnum nm2 nms) <- mStatements essenceSolution , nm == nm2 ] of
114 [nms] -> do
115 let domain = mkDomainIntBTagged (TagUnnamed nmText) 1 (fromInt (genericLength nms))
116 let values = [ (n, Constant (ConstantInt (TagUnnamed nmText) i))
117 | (i,n) <- zip allNats nms
118 ]
119 modify (((nm, Domain domain) : values) ++)
120 [] -> userErr1 $ vcat [ "No value for unnamed domain" <+> pretty nm <+> "in the solution file."
121 ]
122 vals -> userErr1 $ vcat [ "Multiple values for unnamed domain" <+> pretty nm <+> "in the solution file."
123 , "Values:" <++> vcat (map (prettyList prBraces ",") vals)
124 ]
125 Declaration (LettingDomainDefnUnnamed{}) ->
126 bug "validateSolution LettingDomainDefnUnnamed, some other type of Name"
127 SearchOrder{} -> return ()
128 SearchHeuristic{} -> return ()
129 Where xs -> do
130 vals <- gets id
131 forM_ xs $ \ x -> do
132 constant <- instantiateExpression vals x
133 case (constant, viewConstantMatrix constant) of
134 (ConstantBool True, _) -> return ()
135 (_, Just (_, bools)) | all (== ConstantBool True) bools -> return ()
136 _ -> userErr1 $ "Invalid." <++> vcat [ "Statement evaluates to:" <+> pretty constant
137 , "Original statement was:" <+> pretty x
138 , "Relevant values:" <++> vcat
139 [ "letting" <+> pretty nm <+> "be" <+> pretty val
140 | (nm, val) <- vals
141 , nm `elem` (universeBi x :: [Name])
142 ]
143 ]
144 Objective{} -> return ()
145 SuchThat xs -> do
146 vals <- gets id
147 -- Custom symmetry assertions are checked on the represented solver
148 -- model. Abstract values do not determine their representation key.
149 -- The modelling prologue prohibits nesting/reification of these.
150 let isSymmetryAssertion (Op MkOpApplySymmetries{}) = True
151 isSymmetryAssertion _ = False
152 forM_ (filter (not . isSymmetryAssertion) xs) $ \ x -> do
153 constant <- instantiateExpression vals x
154 case (constant, viewConstantMatrix constant) of
155 (ConstantBool True, _) -> return ()
156 (_, Just (_, bools)) | all (== ConstantBool True) bools -> return ()
157 _ -> userErr1 $ "Invalid." <++> vcat [ "Statement evaluates to:" <+> pretty constant
158 , "Original statement was:" <+> pretty x
159 , "Relevant values:" <++> vcat
160 [ "letting" <+> pretty nm <+> "be" <+> pretty val
161 | (nm, val) <- vals
162 , nm `elem` (universeBi x :: [Name])
163 ]
164 ]
165
166
167 introduceRecordFields ::
168 MonadFailDoc m =>
169 MonadState [(Name, Expression)] m =>
170 Pretty r =>
171 Pretty x =>
172 TypeOf x =>
173 (?typeCheckerMode :: TypeCheckerMode) =>
174 Domain r x -> m ()
175 introduceRecordFields (DomainRecord inners) =
176 forM_ inners $ \ (n, d) -> do
177 t <- typeOfDomain d
178 modify ((n, Constant (ConstantField n t)) :)
179 introduceRecordFields (DomainVariant inners) =
180 forM_ inners $ \ (n, d) -> do
181 t <- typeOfDomain d
182 modify ((n, Constant (ConstantField n t)) :)
183 introduceRecordFields _ = return ()