code.hs

module Search where

import Agda.Syntax.Parser
-- import Agda.Syntax.Abstract as Abstract
import Agda.Syntax.Concrete as Concrete
-- import Agda.Syntax.Translation.ConcreteToAbstract
import Agda.Syntax.Scope.Monad
import Agda.Utils.FileName

import Data.Text.Lazy as T
import Agda.Utils.Pretty

{-
Extracting Definitions From a Library File

1. Open File and getContents
2. Parse the module

-}

testFile :: AbsolutePath
testFile = mkAbsolute "/home/jpm61704/Documents/Research/ProgramSearch/res/library.agda"

parseModule :: AbsolutePath -> PM Module
parseModule path = do f <- readFilePM path
                      fmap fst $ parseFile moduleParser path (T.unpack f)


withModule :: AbsolutePath -> (Module -> a) -> PM a
withModule path f = do mod <- parseModule path
                       return (f mod)

allTypeSigs :: Module -> [ Declaration ]
allTypeSigs (ps, ds) = Prelude.filter isTypeSig ds

isTypeSig :: Declaration -> Bool
isTypeSig (TypeSig _ _ _ _) = True
isTypeSig _ = False

https://github.com/agda/agda/blob/master/examples/Introduction/Basics.agda