File tree Expand file tree Collapse file tree 6 files changed +8
-8
lines changed Expand file tree Collapse file tree 6 files changed +8
-8
lines changed Original file line number Diff line number Diff line change @@ -260,7 +260,7 @@ applyEquation ::
260
260
applyEquation _ _term equation result = do
261
261
let results = OrPattern. fromPattern result
262
262
debugApplyEquation equation result
263
- simplificationLogHandle <- liftSimplifier $ asks Simplifier. tracingEnabled
263
+ simplificationLogHandle <- liftSimplifier $ asks Simplifier. simplificationLogHandle
264
264
when
265
265
(isJust simplificationLogHandle)
266
266
(liftIO $ emitEquationTrace (fromJust simplificationLogHandle))
Original file line number Diff line number Diff line change @@ -92,7 +92,7 @@ mkSimplifierEnv ::
92
92
SmtMetadataTools Attribute. Symbol ->
93
93
Map AxiomIdentifier [Equation VariableName ] ->
94
94
SMT Env
95
- mkSimplifierEnv tracingEnabled verifiedModule sortGraph overloadGraph metadataTools rawEquations =
95
+ mkSimplifierEnv simplificationLogHandle verifiedModule sortGraph overloadGraph metadataTools rawEquations =
96
96
runSimplifier earlyEnv initialize
97
97
where
98
98
! earlyEnv =
@@ -107,7 +107,7 @@ mkSimplifierEnv tracingEnabled verifiedModule sortGraph overloadGraph metadataTo
107
107
, injSimplifier
108
108
, overloadSimplifier
109
109
, hookedSymbols = Map. empty
110
- , tracingEnabled
110
+ , simplificationLogHandle
111
111
}
112
112
injSimplifier =
113
113
{-# SCC "evalSimplifier/injSimplifier" #-}
@@ -155,7 +155,7 @@ mkSimplifierEnv tracingEnabled verifiedModule sortGraph overloadGraph metadataTo
155
155
, overloadSimplifier
156
156
, hookedSymbols
157
157
, axiomEquations
158
- , tracingEnabled
158
+ , simplificationLogHandle
159
159
}
160
160
161
161
{- | Evaluate a simplifier computation, returning the result of only one branch.
Original file line number Diff line number Diff line change @@ -151,7 +151,7 @@ data Env = Env
151
151
, injSimplifier :: ! InjSimplifier
152
152
, overloadSimplifier :: ! OverloadSimplifier
153
153
, hookedSymbols :: ! (Map Id Text )
154
- , tracingEnabled :: Maybe IO. Handle
154
+ , simplificationLogHandle :: Maybe IO. Handle
155
155
}
156
156
157
157
data SimplifierTrace = SimplifierTrace
Original file line number Diff line number Diff line change @@ -245,7 +245,7 @@ testEnv =
245
245
, injSimplifier = testInjSimplifier
246
246
, overloadSimplifier = testOverloadSimplifier
247
247
, hookedSymbols = mkHookedSymbols $ indexedModuleSyntax verifiedModule
248
- , tracingEnabled = Nothing
248
+ , simplificationLogHandle = Nothing
249
249
}
250
250
251
251
simplify :: TermLike RewritingVariableName -> IO [Pattern RewritingVariableName ]
Original file line number Diff line number Diff line change @@ -1184,5 +1184,5 @@ testEnv =
1184
1184
[ mkHookedSymbols $ indexedModuleSyntax verifiedModule
1185
1185
, listHookedSymbols
1186
1186
]
1187
- , tracingEnabled = Nothing
1187
+ , simplificationLogHandle = Nothing
1188
1188
}
Original file line number Diff line number Diff line change @@ -2317,7 +2317,7 @@ env =
2317
2317
, injSimplifier = Test.Kore.Rewrite.MockSymbols. injSimplifier
2318
2318
, overloadSimplifier = Test.Kore.Rewrite.MockSymbols. overloadSimplifier
2319
2319
, hookedSymbols = Map. empty
2320
- , tracingEnabled = Nothing
2320
+ , simplificationLogHandle = Nothing
2321
2321
}
2322
2322
2323
2323
generatorSetup :: ConsistentKore. Setup
You can’t perform that action at this time.
0 commit comments