From c9b8ff93d4597c7852880dbaa746c583208fd86a Mon Sep 17 00:00:00 2001 From: Jakob Naucke Date: Mon, 13 May 2024 18:49:11 +0200 Subject: [PATCH] Move resolveStringName to utils and make failable for greater reuse --- src/Agda2Hs/Compile/ClassInstance.hs | 13 ------------- src/Agda2Hs/Compile/Utils.hs | 3 ++- 2 files changed, 2 insertions(+), 14 deletions(-) diff --git a/src/Agda2Hs/Compile/ClassInstance.hs b/src/Agda2Hs/Compile/ClassInstance.hs index ee619d89..44fecf6c 100644 --- a/src/Agda2Hs/Compile/ClassInstance.hs +++ b/src/Agda2Hs/Compile/ClassInstance.hs @@ -14,14 +14,10 @@ import Language.Haskell.Exts.Extension as Hs import Agda.Compiler.Backend import Agda.Compiler.Common ( curDefs, sortDefs ) -import Agda.Interaction.BasicOps ( parseName ) - import Agda.Syntax.Common hiding ( Ranged ) import Agda.Syntax.Internal import Agda.Syntax.Internal.Pattern ( patternToTerm ) -import Agda.Syntax.Position ( noRange ) import Agda.Syntax.Scope.Base -import Agda.Syntax.Scope.Monad ( resolveName ) import Agda.Syntax.Common.Pretty ( prettyShow ) import Agda.TypeChecking.Pretty @@ -321,15 +317,6 @@ findDefinitions p m = do map snd <$> filterM (uncurry p) inMod -resolveStringName :: String -> C QName -resolveStringName s = do - cqname <- liftTCM $ parseName noRange s - rname <- liftTCM $ resolveName cqname - case rname of - DefinedName _ aname _ -> return $ anameName aname - _ -> genericDocError =<< text ("Couldn't find " ++ s) - - lookupDefaultImplementations :: QName -> [Hs.Name ()] -> C [Definition] lookupDefaultImplementations recName fields = do let modName = qnameToMName recName diff --git a/src/Agda2Hs/Compile/Utils.hs b/src/Agda2Hs/Compile/Utils.hs index 9ff54f3f..d5fac4b8 100644 --- a/src/Agda2Hs/Compile/Utils.hs +++ b/src/Agda2Hs/Compile/Utils.hs @@ -13,13 +13,14 @@ import qualified Data.Map as M import qualified Language.Haskell.Exts as Hs import Agda.Compiler.Backend hiding ( Args ) +import Agda.Interaction.BasicOps ( parseName ) import Agda.Syntax.Common import qualified Agda.Syntax.Concrete.Name as C import Agda.Syntax.Internal import Agda.Syntax.Position ( noRange ) import Agda.Syntax.Scope.Base -import Agda.Syntax.Scope.Monad ( bindVariable, freshConcreteName, isDatatypeModule ) +import Agda.Syntax.Scope.Monad ( bindVariable, freshConcreteName, isDatatypeModule, resolveName ) import Agda.Syntax.Common.Pretty ( prettyShow ) import qualified Agda.Syntax.Common.Pretty as P