1
2module Agda.Compiler.Backend
3  ( module Agda.Syntax.Treeless
4  , Backend
5  , activeBackendMayEraseType
6  , lookupBackend
7  )
8  where
9
10import Control.DeepSeq
11
12-- Explicitly adding the Agda.Syntax.Treeless import to the .hs-boot file
13-- so that the `Args` symbol can be hidden by the `SOURCE` import in
14-- TypeChecking.Monad.Base.
15--
16-- Without exporting it here, a `hiding` clause there causes a compilation
17-- error. But without hiding it there, the name conflicts with the one
18-- imported from Agda.Syntax.Internal.
19--
20-- This is only a problem with ghci, which will load a fully-compiled module if
21-- available; but that module will contain more symbols than just the few in
22-- the .hs-boot
23import Agda.Syntax.Treeless (TTerm, Args)
24
25import Agda.Syntax.Abstract.Name (QName)
26import {-# SOURCE #-} Agda.TypeChecking.Monad.Base (TCM, BackendName)
27
28data Backend
29
30instance NFData Backend
31
32activeBackendMayEraseType :: QName -> TCM Bool
33lookupBackend :: BackendName -> TCM (Maybe Backend)
34