@@ -61,6 +61,7 @@ import Language.Haskell.Liquid.Types.Names
6161import Language.Haskell.Liquid.Types.RType
6262import Language.Haskell.Liquid.Types.RTypeOp
6363
64+ import Control.Monad.Except (ExceptT , runExceptT , throwError )
6465import Control.Monad ((<=<) , mplus , unless , void )
6566import Control.Monad.Identity
6667import Control.Monad.State.Strict
@@ -161,57 +162,60 @@ resolveLHNames
161162 -> BareSpecParsed
162163 -> TargetDependencies
163164 -> Either [Error ] (BareSpec , LogicNameEnv , LogicMap )
164- resolveLHNames cfg thisModule localVars impMods globalRdrEnv bareSpec0 dependencies = do
165- let ((bs, logicNameEnv, lmap2), ro) =
166- flip runState RenameOutput {roErrors = [] , roUsedNames = [] , roUsedDataCons = mempty } $ do
167- sp0 <- fixExpressionArgsOfTypeAliases taliases $ resolveBoundVarsInTypeAliases bareSpec0
168- -- First pass: A generic traversal that resolves names
169- -- of Haskell entities and type aliases.
170- sp1 <- mapMLocLHNames (\ l -> (<$ l) <$> resolveLHName l) sp0
171- -- Data decls contain fieldnames that introduce measures with the
172- -- same names. We resolve them before constructing the logic
173- -- environment.
174- dataDecls <- mapM (mapDataDeclFieldNamesM resolveFieldLogicName) (dataDecls sp1)
175- let sp2 = sp1 {dataDecls}
176-
177- es0 <- gets roErrors
178- if null es0 then do
179-
180- -- Second pass: a traversal to resolve logic names using the following
181- -- lookup environments.
182- let (inScopeEnv, logicNameEnv0, privateReflectNames) =
183- makeLogicEnvs impMods thisModule sp2 dependencies
184- -- Add resolved local defines to the logic map.
185- lmap1 =
186- lmap <> mkLogicMap (HM. fromList $
187- (\ (k , v) ->
188- let k' = lhNameToResolvedSymbol <$> k in
189- (F. val k', (val <$> v) { lmVar = k' }))
190- <$> defines sp2)
191- sp3 <- fromBareSpecLHName <$>
192- resolveLogicNames
193- cfg
194- thisModule
195- inScopeEnv
196- globalRdrEnv
197- lmap1
198- localVars
199- logicNameEnv0
200- privateReflectNames
201- depsInlinesAndDefines
202- sp2
203- dcs <- gets roUsedDataCons
204- return (sp3 {usedDataCons = dcs} , logicNameEnv0, lmap1)
205- else
206- return ( error " resolveLHNames: invalid spec"
207- , error " resolveLHNames: invalid logic environment"
208- , error " resolveLHNames: invalid logic map" )
209- logicNameEnv' = extendLogicNameEnv logicNameEnv (roUsedNames ro)
210- if null (roErrors ro) then
211- Right (bs, logicNameEnv', lmap2)
212- else
213- Left (roErrors ro)
165+ resolveLHNames cfg thisModule localVars impMods globalRdrEnv bareSpec0 dependencies =
166+ flip evalState RenameOutput { roErrors = [] , roUsedNames = [] , roUsedDataCons = mempty } $
167+ runExceptT $ do
168+ -- Prepare type aliases for resolution.
169+ sp0 <- lift $ fixExpressionArgsOfTypeAliases taliases $ resolveBoundVarsInTypeAliases bareSpec0
170+
171+ checkErrors
172+
173+ -- First resolution pass: A generic traversal that resolves names
174+ -- of Haskell entities and type alias binders.
175+ sp1 <- lift $ mapMLocLHNames (\ l -> (<$ l) <$> resolveLHName l) sp0
176+
177+ -- Data decls contain fieldnames that introduce measures with the
178+ -- same names. We resolve them before constructing the logic
179+ -- environments.
180+ dataDecls <- lift $ mapM (mapDataDeclFieldNamesM resolveFieldLogicName) (dataDecls sp1)
181+ let sp2 = sp1 {dataDecls}
182+
183+ checkErrors
184+
185+ -- Second resolution pass: a traversal to resolve logic names using the following
186+ -- lookup environments.
187+ let (inScopeEnv, logicNameEnv0, privateReflectNames) =
188+ makeLogicEnvs impMods thisModule sp2 dependencies
189+
190+ -- Add resolved local defines to the logic map.
191+ lmap1 = lmap <> mkLogicMap (HM. fromList $
192+ [ (F. val $ lhNameToResolvedSymbol <$> k,
193+ (val <$> v) { lmVar = lhNameToResolvedSymbol <$> k })
194+ | (k,v) <- defines sp2 ])
195+ sp3 <- lift $ fromBareSpecLHName <$>
196+ resolveLogicNames
197+ cfg
198+ thisModule
199+ inScopeEnv
200+ globalRdrEnv
201+ lmap1
202+ localVars
203+ logicNameEnv0
204+ privateReflectNames
205+ depsInlinesAndDefines
206+ sp2
207+
208+ checkErrors
209+
210+ dcs <- gets roUsedDataCons
211+ return (sp3 { usedDataCons = dcs }, logicNameEnv0, lmap1)
214212 where
213+ -- Early exit name resolution if errors are found and pass them to the output.
214+ checkErrors :: ExceptT [Error ] (StateT RenameOutput Identity ) ()
215+ checkErrors = do
216+ es <- gets roErrors
217+ unless (null es) (throwError es)
218+
215219 -- We collect type aliases before resolving names so we have a means to disambiguate
216220 -- imported and local ones (according to their resolution status).
217221 taliases = collectTypeAliases impMods thisModule bareSpec0 dependencies
0 commit comments