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