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