Skip to content

Commit

Permalink
Move resolveStringName to utils and make failable
Browse files Browse the repository at this point in the history
for greater reuse
  • Loading branch information
naucke committed Sep 23, 2024
1 parent 691eb44 commit c9b8ff9
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 14 deletions.
13 changes: 0 additions & 13 deletions src/Agda2Hs/Compile/ClassInstance.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
3 changes: 2 additions & 1 deletion src/Agda2Hs/Compile/Utils.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down

0 comments on commit c9b8ff9

Please sign in to comment.