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