never executed always true always false
1 {-# LANGUAGE DeriveGeneric, DeriveDataTypeable #-}
2 {-# LANGUAGE Rank2Types #-}
3
4 module Conjure.Rules.Definition
5 ( Rule(..), RuleResult(..), namedRule, namedRuleZ
6 , Question(..), QuestionType(..), Answer(..)
7 , LogOrModel, LogOr
8 , Driver, Strategy(..), viewAuto, parseStrategy
9 , Config(..)
10 , UnnamedSymmetryBreaking(..), USBQuickOrComplete(..), USBScope(..), USBIndependentlyOrAltogether(..)
11 , ModelZipper, mkModelZipper, fromModelZipper
12 , ModelWIP(..), modelWIPOut, updateModelWIPInfo
13 , isAtomic
14 , representationOf, hasRepresentation
15 , sameRepresentation, sameRepresentationTree
16 , matchFirst
17 ) where
18
19 import Conjure.Prelude
20 import Conjure.UserError
21 import Conjure.Language.AdHoc ( expressionDepth )
22 import Conjure.Language.Definition
23 import Conjure.Language.Type ( TypeCheckerMode )
24 import Conjure.Language.Expression.Op
25
26 import Conjure.Language.RepresentationOf
27 import Conjure.Process.Enumerate ( EnumerateDomain )
28
29 -- uniplate
30 import Data.Generics.Uniplate.Zipper ( Zipper, fromZipper, zipperBi )
31
32 import qualified Data.HashMap.Strict as M -- unordered-containers
33
34
35 type LogOr a = Either (LogLevel, Doc) a
36 type LogOrModel = LogOr Model
37
38 data Question = Question
39 { qType :: QuestionType
40 , qHole :: Expression
41 , qAscendants :: [Expression]
42 , qAnswers :: [Answer]
43 }
44
45 data QuestionType
46 = ChooseRepr
47 | ChooseRepr_Find Name
48 | ChooseRepr_Given Name
49 | ChooseRepr_Auxiliary
50 | ChooseRepr_Quantified
51 | ChooseRepr_Cut Name
52 | ExpressionRefinement
53 deriving (Eq, Ord, Show, Generic)
54
55 instance Hashable QuestionType
56
57 data Answer = Answer
58 { aText :: Doc
59 , aBefore :: Expression
60 , aAnswer :: Expression
61 , aFullModel :: ModelWIP
62 , aRuleName :: Doc
63 , aDepth :: Int -- expression depth, precalculated depending on the rule. compact will use this to compare.
64 }
65
66 type Driver = (forall m . (MonadIO m, MonadLog m) => [Question] -> m [ModelWIP])
67
68 type ModelZipper = Zipper (LanguageVersion, [Statement]) Expression
69
70 mkModelZipper :: Model -> Maybe ModelZipper
71 mkModelZipper (Model lang stmts _) = zipperBi (lang, stmts)
72
73 fromModelZipper :: ModelZipper -> ModelInfo -> Model
74 fromModelZipper z info =
75 let (lang, stmts) = fromZipper z
76 in Model lang stmts info
77
78 data ModelWIP = StartOver Model | TryThisFirst ModelZipper ModelInfo
79
80 modelWIPOut :: ModelWIP -> Model
81 modelWIPOut (StartOver m) = m
82 modelWIPOut (TryThisFirst z minfo) =
83 let (lang, stmts) = fromZipper z
84 in Model lang stmts minfo
85
86 updateModelWIPInfo :: (ModelInfo -> ModelInfo) -> ModelWIP -> ModelWIP
87 updateModelWIPInfo upd (StartOver model) = StartOver model { mInfo = upd (mInfo model) }
88 updateModelWIPInfo upd (TryThisFirst z info) = TryThisFirst z (upd info)
89
90
91 data Config = Config
92 { logLevel :: LogLevel
93 , verboseTrail :: Bool
94 , rewritesTrail :: Bool
95 , logRuleFails :: Bool
96 , logRuleSuccesses :: Bool
97 , logRuleAttempts :: Bool
98 , logChoices :: Bool
99 , followTrail :: M.HashMap Int -- Question hash
100 Int -- Answer hash
101 , strategyQ :: Strategy
102 , strategyA :: Strategy
103 , representations :: Strategy
104 , representationsFinds :: Strategy
105 , representationsGivens :: Strategy
106 , representationsAuxiliaries :: Strategy
107 , representationsQuantifieds :: Strategy
108 , representationsCuts :: Strategy
109 , outputDirectory :: FilePath
110 , channelling :: Bool
111 , representationLevels :: Bool
112 , unnamedSymmetryBreaking :: Maybe UnnamedSymmetryBreaking
113 , limitModels :: Maybe Int
114 , numberingStart :: Int
115 , smartFilenames :: Bool
116 , lineWidth :: Int
117 , responses :: Maybe [Int]
118 , responsesRepresentation :: Maybe [(Name, Int)]
119 , generateStreamliners :: Maybe [Int]
120 , estimateNumberOfModels :: Bool
121 }
122 deriving (Eq, Ord, Show, Data, Typeable)
123
124 instance Default Config where
125 def = Config
126 { logLevel = LogNone
127 , verboseTrail = False
128 , rewritesTrail = False
129 , logRuleFails = False
130 , logRuleSuccesses = False
131 , logRuleAttempts = False
132 , logChoices = False
133 , followTrail = M.empty
134 , strategyQ = Interactive
135 , strategyA = Interactive
136 , representations = Interactive
137 , representationsFinds = Interactive
138 , representationsGivens = Interactive
139 , representationsAuxiliaries = Interactive
140 , representationsQuantifieds = Interactive
141 , representationsCuts = Interactive
142 , outputDirectory = "conjure-output"
143 , channelling = True
144 , representationLevels = True
145 , unnamedSymmetryBreaking = Nothing
146 , limitModels = Nothing
147 , numberingStart = 1
148 , smartFilenames = False
149 , lineWidth = 120
150 , responses = Nothing
151 , responsesRepresentation = Nothing
152 , generateStreamliners = Nothing
153 , estimateNumberOfModels = False
154 }
155
156
157 -- 1. Quick/Complete. Quick is x .<= p(x)
158 -- Complete is x .<= y /\ y = p(x)
159 -- 2. Scope. Consecutive
160 -- AllPairs
161 -- AllPermutations
162 -- 3. Independently/Altogether
163 -- in addition, we have
164 -- none
165 -- fast: Quick-Consecutive-Independently
166 -- full: Complete-AllPermutations-Altogether
167 data UnnamedSymmetryBreaking =
168 UnnamedSymmetryBreaking
169 USBQuickOrComplete
170 USBScope
171 USBIndependentlyOrAltogether
172 deriving (Eq, Ord, Show, Read, Data, Typeable)
173 data USBQuickOrComplete = USBQuick | USBComplete
174 deriving (Eq, Ord, Show, Read, Data, Typeable)
175 data USBScope = USBConsecutive | USBAllPairs | USBAllPermutations
176 deriving (Eq, Ord, Show, Read, Data, Typeable)
177 data USBIndependentlyOrAltogether = USBIndependently | USBAltogether
178 deriving (Eq, Ord, Show, Read, Data, Typeable)
179
180
181 data RuleResult m = RuleResult
182 { ruleResultDescr :: Doc -- describe this transformation
183 , ruleResultType :: QuestionType
184 , ruleResult :: m Expression -- the result
185 , ruleResultHook :: Maybe (Model -> m Model) -- post-application hook
186 , ruleResultSize :: m Int -- expression depth, precalculated depending on the rule. compact will use this to compare.
187 }
188
189 data Rule = Rule
190 { rName :: Doc
191 , rApply
192 :: forall n m a .
193 ( MonadFailDoc n, MonadUserError n, MonadLog n
194 , NameGen n, EnumerateDomain n, MonadReader (Zipper a Expression) n
195 -- a fail in {n} means that the rule isn't applicable
196 , MonadFailDoc m, MonadUserError m, MonadLog m
197 , NameGen m, EnumerateDomain m
198 -- a failDoc in {m} means a bug
199 , ?typeCheckerMode :: TypeCheckerMode
200 )
201 => Zipper a Expression -- to query context
202 -> Expression
203 -> n [RuleResult m]
204 }
205
206 namedRule
207 :: Doc
208 -> (forall n m a .
209 ( MonadFailDoc n, MonadUserError n, MonadLog n
210 , NameGen n, EnumerateDomain n, MonadReader (Zipper a Expression) n
211 , MonadFailDoc m, MonadUserError m, MonadLog m
212 , NameGen m, EnumerateDomain m
213 , ?typeCheckerMode :: TypeCheckerMode
214 ) => Expression -> n (Doc, m Expression))
215 -> Rule
216 namedRule nm f = Rule
217 { rName = nm
218 , rApply = \ z x -> do
219 (rResultDescr, rResult) <- runReaderT (f x) z
220 return [RuleResult rResultDescr ExpressionRefinement rResult Nothing (expressionDepth <$> rResult)]
221 }
222
223 namedRuleZ
224 :: Doc
225 -> (forall n m a .
226 ( MonadFailDoc n, MonadUserError n, MonadLog n
227 , NameGen n, EnumerateDomain n, MonadReader (Zipper a Expression) n
228 , MonadFailDoc m, MonadUserError m, MonadLog m
229 , NameGen m, EnumerateDomain m
230 , ?typeCheckerMode :: TypeCheckerMode
231 ) => Zipper a Expression -> Expression -> n (Doc, m Expression))
232 -> Rule
233 namedRuleZ nm f = Rule
234 { rName = nm
235 , rApply = \ z x -> do
236 (rResultDescr, rResult) <- runReaderT (f z x) z
237 return [RuleResult rResultDescr ExpressionRefinement rResult Nothing (expressionDepth <$> rResult)]
238 }
239
240 isAtomic :: Expression -> Bool
241 isAtomic Reference{} = True
242 isAtomic (Op (MkOpIndexing (OpIndexing a _))) = isAtomic a
243 isAtomic _ = False
244
245
246 matchFirst
247 :: MonadFailDoc m
248 => [a] -- list of things to try matching on
249 -> (a -> Maybe b) -- the matcher
250 -> m ( [a] -- befores
251 , b -- the matching one
252 , [a] -- afters
253 )
254 matchFirst = helper []
255 where
256 helper _ [] _ = na "matchFirst"
257 helper befores (x:xs) f = case f x of
258 Nothing -> helper (x:befores) xs f
259 Just y -> return (reverse befores, y, xs)