mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-09-11 08:55:23 +03:00
Clean up unused imports (#4065)
This commit is contained in:
parent
be8523f834
commit
d4bd8e6353
@ -1,7 +1,6 @@
|
||||
module Main where
|
||||
|
||||
import Idris.AbsSyntax
|
||||
import Idris.Core.TT
|
||||
import Idris.ElabDecls
|
||||
import Idris.Main
|
||||
import Idris.Options
|
||||
@ -10,8 +9,6 @@ import IRTS.Compiler
|
||||
|
||||
import Util.System
|
||||
|
||||
import Paths_idris
|
||||
|
||||
import Control.Monad
|
||||
import System.Environment
|
||||
import System.Exit
|
||||
|
@ -1,15 +1,12 @@
|
||||
module Main where
|
||||
|
||||
import Idris.AbsSyntax
|
||||
import Idris.Core.TT
|
||||
import Idris.ElabDecls
|
||||
import Idris.Main
|
||||
import Idris.Options
|
||||
import IRTS.CodegenJavaScript
|
||||
import IRTS.Compiler
|
||||
|
||||
import Paths_idris
|
||||
|
||||
import System.Environment
|
||||
import System.Exit
|
||||
|
||||
|
@ -1,15 +1,12 @@
|
||||
module Main where
|
||||
|
||||
import Idris.AbsSyntax
|
||||
import Idris.Core.TT
|
||||
import Idris.ElabDecls
|
||||
import Idris.Main
|
||||
import Idris.Options
|
||||
import IRTS.CodegenJavaScript
|
||||
import IRTS.Compiler
|
||||
|
||||
import Paths_idris
|
||||
|
||||
import System.Environment
|
||||
import System.Exit
|
||||
|
||||
|
@ -226,7 +226,6 @@ Library
|
||||
, Idris.WhoCalls
|
||||
, Idris.CmdOptions
|
||||
|
||||
, IRTS.BCImp
|
||||
, IRTS.Bytecode
|
||||
, IRTS.CodegenC
|
||||
, IRTS.CodegenCommon
|
||||
|
@ -2,9 +2,7 @@ module Main where
|
||||
|
||||
import System.Exit (ExitCode(..), exitSuccess, exitWith)
|
||||
|
||||
import Control.Monad (unless, when, (>=>))
|
||||
import Data.Foldable (foldrM)
|
||||
import Data.Maybe (fromMaybe)
|
||||
import Control.Monad (unless, when)
|
||||
|
||||
import Idris.AbsSyntax
|
||||
import Idris.CmdOptions
|
||||
@ -16,9 +14,6 @@ import Idris.Package
|
||||
|
||||
import Util.System (setupBundledCC)
|
||||
|
||||
import System.Exit (ExitCode(..), exitWith)
|
||||
import Util.System (setupBundledCC)
|
||||
|
||||
processShowOptions :: [Opt] -> Idris ()
|
||||
processShowOptions opts = runIO $ do
|
||||
when (ShowAll `elem` opts) $ showExitIdrisInfo
|
||||
|
@ -1,23 +0,0 @@
|
||||
{-|
|
||||
Module : IRTS.BCImp
|
||||
Description : Bytecode for a register/variable based VM (e.g. for generating code in an imperative language where we let the language deal with GC)
|
||||
Copyright :
|
||||
License : BSD3
|
||||
Maintainer : The Idris Community.
|
||||
-}
|
||||
module IRTS.BCImp where
|
||||
|
||||
import Idris.Core.TT
|
||||
import IRTS.Lang
|
||||
import IRTS.Simplified
|
||||
|
||||
data Reg = RVal | L Int
|
||||
|
||||
data BC = NOP
|
||||
|
||||
toBC :: (Name, SDecl) -> (Name, [BC])
|
||||
toBC (n, SFun n' args locs exp)
|
||||
= (n, bc RVal exp)
|
||||
|
||||
bc :: Reg -> SExp -> [BC]
|
||||
bc = undefined
|
@ -23,7 +23,6 @@ module IRTS.Bytecode where
|
||||
|
||||
import Idris.Core.TT
|
||||
import IRTS.Defunctionalise
|
||||
import IRTS.Lang
|
||||
import IRTS.Simplified
|
||||
|
||||
import Data.Maybe
|
||||
|
@ -9,12 +9,10 @@ Maintainer : The Idris Community.
|
||||
|
||||
module IRTS.CodegenC (codegenC) where
|
||||
|
||||
import Idris.AbsSyntax
|
||||
import Idris.Core.TT
|
||||
import IRTS.Bytecode
|
||||
import IRTS.CodegenCommon
|
||||
import IRTS.Defunctionalise
|
||||
import IRTS.Lang
|
||||
import IRTS.Simplified
|
||||
import IRTS.System
|
||||
|
||||
@ -24,9 +22,7 @@ import Control.Monad
|
||||
import Data.Bits
|
||||
import Data.Char
|
||||
import Data.List (intercalate, nubBy)
|
||||
import Debug.Trace
|
||||
import Numeric
|
||||
import System.Directory
|
||||
import System.Exit
|
||||
import System.FilePath ((<.>), (</>))
|
||||
import System.IO
|
||||
|
@ -10,7 +10,6 @@ Maintainer : The Idris Community.
|
||||
module IRTS.Compiler(compile, generate) where
|
||||
|
||||
import Idris.AbsSyntax
|
||||
import Idris.AbsSyntaxTree
|
||||
import Idris.ASTUtils
|
||||
import Idris.Core.CaseTree
|
||||
import Idris.Core.Evaluate
|
||||
@ -21,33 +20,24 @@ import Idris.Options
|
||||
import Idris.Output
|
||||
import IRTS.CodegenC
|
||||
import IRTS.CodegenCommon
|
||||
import IRTS.CodegenJavaScript
|
||||
import IRTS.Defunctionalise
|
||||
import IRTS.DumpBC
|
||||
import IRTS.Exports
|
||||
import IRTS.Inliner
|
||||
import IRTS.Lang
|
||||
import IRTS.LangOpts
|
||||
import IRTS.Portable
|
||||
import IRTS.Simplified
|
||||
|
||||
import Prelude hiding (id, (.))
|
||||
|
||||
import Control.Applicative
|
||||
import Control.Category
|
||||
import Control.Monad.State
|
||||
import Data.IntSet (IntSet)
|
||||
import qualified Data.IntSet as IS
|
||||
import Data.List
|
||||
import qualified Data.Map as M
|
||||
import Data.Maybe
|
||||
import Data.Ord
|
||||
import qualified Data.Set as S
|
||||
import Debug.Trace
|
||||
import System.Directory
|
||||
import System.Environment
|
||||
import System.Exit
|
||||
import System.FilePath (addTrailingPathSeparator, (</>))
|
||||
import System.IO
|
||||
import System.Process
|
||||
|
||||
|
@ -32,7 +32,6 @@ import Control.Monad
|
||||
import Control.Monad.State
|
||||
import Data.List
|
||||
import Data.Maybe
|
||||
import Debug.Trace
|
||||
|
||||
data DExp = DV Name
|
||||
| DApp Bool Name [DExp] -- True = tail call
|
||||
|
@ -9,7 +9,6 @@ module IRTS.DumpBC where
|
||||
|
||||
import Idris.Core.TT
|
||||
import IRTS.Bytecode
|
||||
import IRTS.Lang
|
||||
import IRTS.Simplified
|
||||
|
||||
import Data.List
|
||||
|
@ -12,23 +12,18 @@ module IRTS.JavaScript.LangTransforms( removeDeadCode
|
||||
) where
|
||||
|
||||
|
||||
import Control.DeepSeq
|
||||
import Control.Monad.Trans.State
|
||||
import Data.List
|
||||
import Data.Map.Strict (Map)
|
||||
import qualified Data.Map.Strict as Map
|
||||
import Data.Maybe
|
||||
import Data.Set (Set)
|
||||
import qualified Data.Set as Set
|
||||
import Data.Text (Text)
|
||||
import qualified Data.Text as T
|
||||
import Idris.Core.CaseTree
|
||||
import Idris.Core.TT
|
||||
import IRTS.Lang
|
||||
|
||||
import Data.Data
|
||||
import Data.Generics.Uniplate.Data
|
||||
import GHC.Generics (Generic)
|
||||
|
||||
deriving instance Typeable FDesc
|
||||
deriving instance Data FDesc
|
||||
|
@ -20,12 +20,9 @@ module IRTS.JavaScript.Name
|
||||
) where
|
||||
|
||||
import Data.Char
|
||||
import Data.List
|
||||
import qualified Data.Map.Strict as Map
|
||||
import Data.Text (Text)
|
||||
import qualified Data.Text as T
|
||||
import Idris.Core.TT
|
||||
import IRTS.JavaScript.AST
|
||||
|
||||
jsEscape :: String -> String
|
||||
jsEscape = concatMap jschar
|
||||
|
@ -16,11 +16,7 @@ module IRTS.JavaScript.PrimOp
|
||||
, jsPrimCoerce
|
||||
) where
|
||||
|
||||
import Data.Char
|
||||
import Data.List
|
||||
import qualified Data.Map.Strict as Map
|
||||
import Data.Text (Text)
|
||||
import qualified Data.Text as T
|
||||
import Idris.Core.TT
|
||||
import IRTS.JavaScript.AST
|
||||
import IRTS.Lang
|
||||
|
@ -17,10 +17,7 @@ module IRTS.JavaScript.Specialize
|
||||
, qualifyN
|
||||
) where
|
||||
|
||||
import Data.Char
|
||||
import Data.List
|
||||
import qualified Data.Map.Strict as Map
|
||||
import Data.Text (Text)
|
||||
import qualified Data.Text as T
|
||||
import Idris.Core.TT
|
||||
import IRTS.JavaScript.AST
|
||||
|
@ -13,12 +13,10 @@ module IRTS.Lang where
|
||||
import Idris.Core.CaseTree
|
||||
import Idris.Core.TT
|
||||
|
||||
import Control.Applicative hiding (Const)
|
||||
import Control.Monad.State hiding (lift)
|
||||
import Data.Data (Data)
|
||||
import Data.List
|
||||
import Data.Typeable (Typeable)
|
||||
import Debug.Trace
|
||||
import GHC.Generics (Generic)
|
||||
|
||||
data Endianness = Native | BE | LE deriving (Show, Eq)
|
||||
|
@ -9,14 +9,10 @@ Maintainer : The Idris Community.
|
||||
|
||||
module IRTS.LangOpts where
|
||||
|
||||
import Idris.Core.CaseTree
|
||||
import Idris.Core.TT
|
||||
import IRTS.Lang
|
||||
|
||||
import Control.Applicative hiding (Const)
|
||||
import Control.Monad.State hiding (lift)
|
||||
import Data.List
|
||||
import Debug.Trace
|
||||
|
||||
inlineAll :: [(Name, LDecl)] -> [(Name, LDecl)]
|
||||
inlineAll lds = let defs = addAlist lds emptyContext in
|
||||
|
@ -14,12 +14,10 @@ import Idris.Core.TT
|
||||
import IRTS.Bytecode
|
||||
import IRTS.CodegenCommon
|
||||
import IRTS.Defunctionalise
|
||||
import IRTS.Lang
|
||||
import IRTS.Simplified
|
||||
|
||||
import Data.Aeson
|
||||
import qualified Data.ByteString.Lazy as B
|
||||
import qualified Data.Text as T
|
||||
import System.IO
|
||||
|
||||
data CodegenFile = CGFile {
|
||||
|
@ -10,12 +10,9 @@ module IRTS.Simplified(simplifyDefs, SDecl(..), SExp(..), SAlt(..)) where
|
||||
|
||||
import Idris.Core.CaseTree
|
||||
import Idris.Core.TT
|
||||
import Idris.Core.Typecheck
|
||||
import IRTS.Defunctionalise
|
||||
|
||||
import Control.Monad.State
|
||||
import Data.Maybe
|
||||
import Debug.Trace
|
||||
|
||||
data SExp = SV LVar
|
||||
| SApp Bool Name [LVar]
|
||||
|
@ -52,7 +52,6 @@ import Idris.Options
|
||||
|
||||
import Prelude hiding (id, (.))
|
||||
|
||||
import Control.Applicative
|
||||
import Control.Category
|
||||
import Control.Monad.State.Class
|
||||
import Data.Maybe
|
||||
|
@ -46,7 +46,6 @@ import qualified Data.Text as T
|
||||
import Data.Traversable (Traversable)
|
||||
import Data.Typeable
|
||||
import GHC.Generics (Generic)
|
||||
import Network.Socket (PortNumber)
|
||||
|
||||
|
||||
data ElabWhat = ETypes | EDefns | EAll
|
||||
|
@ -11,7 +11,7 @@ module Idris.Apropos (apropos, aproposModules) where
|
||||
import Idris.AbsSyntax
|
||||
import Idris.Core.Evaluate (Def(..), ctxtAlist)
|
||||
import Idris.Core.TT (Binder(..), Const(..), Name(..), NameType(..), TT(..),
|
||||
Type, lookupCtxtExact, toAlist)
|
||||
Type, toAlist)
|
||||
import Idris.Docstrings (DocTerm, Docstring, containsText)
|
||||
|
||||
import Data.List (intersperse, nub, nubBy)
|
||||
|
@ -16,19 +16,15 @@ module Idris.Chaser(
|
||||
import Idris.AbsSyntax
|
||||
import Idris.Core.TT
|
||||
import Idris.Error
|
||||
import Idris.IBC
|
||||
import Idris.Imports
|
||||
import Idris.Parser
|
||||
import Idris.Unlit
|
||||
|
||||
import Control.Monad.State
|
||||
import Control.Monad.Trans
|
||||
import Data.List
|
||||
import Data.Time.Clock
|
||||
import Debug.Trace
|
||||
import System.Directory
|
||||
import System.FilePath
|
||||
import Util.System (readSource, writeSource)
|
||||
import Util.System (readSource)
|
||||
|
||||
data ModuleTree = MTree { mod_path :: IFileType,
|
||||
mod_needsRecheck :: Bool,
|
||||
|
@ -13,14 +13,10 @@ module Idris.Core.Binary where
|
||||
import Idris.Core.TT
|
||||
|
||||
import Control.Applicative ((<$>), (<*>))
|
||||
import Control.DeepSeq (($!!))
|
||||
import Control.Monad (liftM2)
|
||||
import Data.Binary
|
||||
import Data.Binary.Get
|
||||
import Data.Binary.Put
|
||||
import qualified Data.Text as T
|
||||
import qualified Data.Text.Encoding as E
|
||||
import Data.Vector.Binary
|
||||
|
||||
instance Binary ErrorReportPart where
|
||||
put (TextPart msg) = do putWord8 0 ; put msg
|
||||
|
@ -31,14 +31,11 @@ module Idris.Core.CaseTree (
|
||||
|
||||
import Idris.Core.TT
|
||||
|
||||
import Control.Applicative hiding (Const)
|
||||
import Control.Monad.Reader
|
||||
import Control.Monad.State
|
||||
import Data.List hiding (partition)
|
||||
import qualified Data.List (partition)
|
||||
import Data.Maybe
|
||||
import qualified Data.Set as S
|
||||
import Debug.Trace
|
||||
import GHC.Generics (Generic)
|
||||
|
||||
data CaseDef = CaseDef [Name] !SC [Term]
|
||||
|
@ -8,15 +8,13 @@ Maintainer : The Idris Community.
|
||||
-}
|
||||
module Idris.Core.Constraints ( ucheck ) where
|
||||
|
||||
import Idris.Core.TT (ConstraintFC(..), Err'(..), FC(..), TC(..),
|
||||
UConstraint(..), UExp(..))
|
||||
import Idris.Core.TT (ConstraintFC(..), Err'(..), TC(..), UConstraint(..),
|
||||
UExp(..))
|
||||
|
||||
import Control.Applicative
|
||||
import Control.Monad.State.Strict
|
||||
import Data.List (partition)
|
||||
import qualified Data.Map.Strict as M
|
||||
import qualified Data.Set as S
|
||||
import Debug.Trace
|
||||
|
||||
-- | Check that a list of universe constraints can be satisfied.
|
||||
ucheck :: S.Set ConstraintFC -> TC ()
|
||||
|
@ -16,7 +16,6 @@ module Idris.Core.Elaborate (
|
||||
, module Idris.Core.ProofState
|
||||
) where
|
||||
|
||||
import Idris.Core.DeepSeq
|
||||
import Idris.Core.Evaluate
|
||||
import Idris.Core.ProofState
|
||||
import Idris.Core.ProofTerm (bound_in, bound_in_term, getProofTerm, mkProofTerm,
|
||||
@ -24,15 +23,9 @@ import Idris.Core.ProofTerm (bound_in, bound_in_term, getProofTerm, mkProofTerm,
|
||||
import Idris.Core.TT
|
||||
import Idris.Core.Typecheck
|
||||
import Idris.Core.Unify
|
||||
import Idris.Core.WHNF
|
||||
|
||||
import Util.Pretty hiding (fill)
|
||||
|
||||
import Control.DeepSeq
|
||||
import Control.Monad.State.Strict
|
||||
import Data.Char
|
||||
import Data.List
|
||||
import Debug.Trace
|
||||
|
||||
data ElabState aux = ES (ProofState, aux) String (Maybe (ElabState aux))
|
||||
deriving Show
|
||||
|
@ -11,7 +11,6 @@ Maintainer : The Idris Community.
|
||||
module Idris.Core.Execute (execute) where
|
||||
|
||||
import Idris.AbsSyntax
|
||||
import Idris.AbsSyntaxTree
|
||||
import Idris.Core.CaseTree
|
||||
import Idris.Core.Evaluate
|
||||
import Idris.Core.TT
|
||||
@ -22,15 +21,11 @@ import IRTS.Lang (FDesc(..), FType(..))
|
||||
import Util.DynamicLinker
|
||||
import Util.System
|
||||
|
||||
import Control.Applicative hiding (Const)
|
||||
import Control.Exception
|
||||
import Control.Monad hiding (forM)
|
||||
import Control.Monad.Trans
|
||||
import Control.Monad.Trans.Except (ExceptT, runExceptT, throwE)
|
||||
import Control.Monad.Trans.State.Strict
|
||||
import Data.Bits
|
||||
import Data.IORef
|
||||
import qualified Data.Map as M
|
||||
import Data.Maybe
|
||||
import Data.Time.Clock.POSIX (getPOSIXTime)
|
||||
import Data.Traversable (forM)
|
||||
@ -42,7 +37,6 @@ import System.IO.Unsafe
|
||||
#ifdef IDRIS_FFI
|
||||
import Foreign.C.String
|
||||
import Foreign.LibFFI
|
||||
import Foreign.Marshal.Alloc (free)
|
||||
import Foreign.Ptr
|
||||
#endif
|
||||
|
||||
|
@ -28,11 +28,9 @@ import Idris.Core.WHNF
|
||||
|
||||
import Util.Pretty hiding (fill)
|
||||
|
||||
import Control.Applicative hiding (empty)
|
||||
import Control.Arrow ((***))
|
||||
import Control.Monad.State.Strict
|
||||
import Data.List
|
||||
import Debug.Trace
|
||||
|
||||
data ProofState = PS { thname :: Name,
|
||||
holes :: [Name], -- ^ holes still to be solved
|
||||
|
@ -18,11 +18,8 @@ module Idris.Core.ProofTerm(
|
||||
|
||||
import Idris.Core.Evaluate
|
||||
import Idris.Core.TT
|
||||
import Idris.Core.Typecheck
|
||||
|
||||
import Control.Monad.State.Strict
|
||||
import Data.List
|
||||
import Debug.Trace
|
||||
|
||||
-- | A zipper over terms, in order to efficiently update proof terms.
|
||||
data TermPath = Top
|
||||
|
@ -60,29 +60,24 @@ import Util.Pretty hiding (Str)
|
||||
-- Work around AMP without CPP
|
||||
import Prelude (Bool(..), Double, Enum(..), Eq(..), FilePath, Functor(..), Int,
|
||||
Integer, Maybe(..), Monad(..), Num(..), Ord(..), Ordering(..),
|
||||
Read(..), Show(..), String, div, error, flip, fst, mod, not,
|
||||
otherwise, read, snd, ($), (&&), (.), (||))
|
||||
Show(..), String, div, error, fst, mod, not, otherwise, read,
|
||||
snd, ($), (&&), (.), (||))
|
||||
|
||||
import Control.Applicative (Alternative, Applicative(..))
|
||||
import qualified Control.Applicative as A (Alternative(..))
|
||||
import Control.DeepSeq (($!!))
|
||||
import Control.Monad.State.Strict
|
||||
import Control.Monad.Trans.Except (Except(..))
|
||||
import Data.Binary hiding (get, put)
|
||||
import qualified Data.Binary as B
|
||||
import Data.Char
|
||||
import Data.Data (Data)
|
||||
import Data.Foldable (Foldable)
|
||||
import Data.List hiding (group, insert)
|
||||
import qualified Data.Map.Strict as Map
|
||||
import Data.Maybe (listToMaybe)
|
||||
import Data.Monoid (mconcat)
|
||||
import Data.Set (Set, fromList, insert, member)
|
||||
import qualified Data.Text as T
|
||||
import Data.Traversable (Traversable)
|
||||
import Data.Typeable (Typeable)
|
||||
import Data.Vector.Unboxed (Vector)
|
||||
import qualified Data.Vector.Unboxed as V
|
||||
import Debug.Trace
|
||||
import Foreign.Storable (sizeOf)
|
||||
import GHC.Generics (Generic)
|
||||
|
@ -13,11 +13,8 @@ module Idris.Core.Typecheck where
|
||||
|
||||
import Idris.Core.Evaluate
|
||||
import Idris.Core.TT
|
||||
import Idris.Core.WHNF
|
||||
|
||||
import Control.Monad.State
|
||||
import qualified Data.Vector.Unboxed as V (length)
|
||||
import Debug.Trace
|
||||
|
||||
-- To check conversion, normalise each term wrt the current environment.
|
||||
-- Since we haven't converted everything to de Bruijn indices yet, we'll have to
|
||||
|
@ -22,11 +22,9 @@ module Idris.Core.Unify(
|
||||
import Idris.Core.Evaluate
|
||||
import Idris.Core.TT
|
||||
|
||||
import Control.Monad
|
||||
import Control.Monad.State.Strict
|
||||
import Data.List
|
||||
import Data.Maybe
|
||||
import Debug.Trace
|
||||
|
||||
-- terms which need to be injective, with the things we're trying to unify
|
||||
-- at the time
|
||||
|
@ -12,11 +12,8 @@ module Idris.Core.WHNF(whnf, whnfArgs, WEnv) where
|
||||
|
||||
import Idris.Core.CaseTree
|
||||
import Idris.Core.Evaluate hiding (quote)
|
||||
import qualified Idris.Core.Evaluate as Evaluate
|
||||
import Idris.Core.TT
|
||||
|
||||
import Debug.Trace
|
||||
|
||||
-- | A stack entry consists of a term and the environment it is to be
|
||||
-- evaluated in (i.e. it's a thunk)
|
||||
type StackEntry = (Term, WEnv)
|
||||
|
@ -16,14 +16,11 @@ import Idris.Core.TT
|
||||
import Idris.Delaborate
|
||||
import Idris.Elab.Utils
|
||||
import Idris.Error
|
||||
import Idris.Output (iWarn, iputStrLn)
|
||||
|
||||
import Control.Monad.State.Strict
|
||||
import Data.Char
|
||||
import Data.Either
|
||||
import Data.List
|
||||
import Data.Maybe
|
||||
import Debug.Trace
|
||||
|
||||
-- | Generate a pattern from an 'impossible' LHS.
|
||||
--
|
||||
|
@ -11,12 +11,10 @@ Maintainer : The Idris Community.
|
||||
module Idris.DSL where
|
||||
|
||||
import Idris.AbsSyntax
|
||||
import Idris.Core.Evaluate
|
||||
import Idris.Core.TT
|
||||
|
||||
import Control.Monad.State.Strict
|
||||
import Data.Generics.Uniplate.Data (transform)
|
||||
import Debug.Trace
|
||||
|
||||
debindApp :: SyntaxInfo -> PTerm -> PTerm
|
||||
debindApp syn t = debind (dsl_bind (dsl_info syn)) t
|
||||
|
@ -10,14 +10,8 @@ Maintainer : The Idris Community.
|
||||
module Idris.DataOpts(applyOpts) where
|
||||
|
||||
import Idris.AbsSyntax
|
||||
import Idris.AbsSyntaxTree
|
||||
import Idris.Core.TT
|
||||
|
||||
import Control.Applicative
|
||||
import Data.List
|
||||
import Data.Maybe
|
||||
import Debug.Trace
|
||||
|
||||
class Optimisable term where
|
||||
applyOpts :: term -> Idris term
|
||||
|
||||
|
@ -24,7 +24,6 @@ import IRTS.Lang (PrimFn(..))
|
||||
|
||||
import Util.DynamicLinker
|
||||
|
||||
import qualified Cheapskate.Types as CT
|
||||
import Control.DeepSeq
|
||||
import Network.Socket (PortNumber)
|
||||
|
||||
|
@ -26,10 +26,9 @@ import Prelude hiding ((<$>))
|
||||
import Control.Applicative (Alternative((<|>)))
|
||||
import Control.Monad.State
|
||||
import Data.Generics.Uniplate.Data (transform)
|
||||
import Data.List (intersperse, nub)
|
||||
import Data.List (nub)
|
||||
import Data.Maybe (mapMaybe)
|
||||
import qualified Data.Text as T
|
||||
import Debug.Trace
|
||||
|
||||
bugaddr = "https://github.com/idris-lang/Idris-dev/issues"
|
||||
|
||||
|
@ -8,7 +8,6 @@ Maintainer : The Idris Community.
|
||||
module Idris.Directives(directiveAction) where
|
||||
|
||||
import Idris.AbsSyntax
|
||||
import Idris.ASTUtils
|
||||
import Idris.Core.Evaluate
|
||||
import Idris.Core.TT
|
||||
import Idris.Imports
|
||||
|
@ -10,7 +10,6 @@ module Idris.Elab.AsPat(desugarAs) where
|
||||
import Idris.AbsSyntax
|
||||
import Idris.Core.TT
|
||||
|
||||
import Control.Applicative
|
||||
import Control.Monad.State.Strict
|
||||
import Data.Generics.Uniplate.Data (transformM, universe)
|
||||
|
||||
|
@ -13,51 +13,38 @@ import Idris.ASTUtils
|
||||
import Idris.Core.CaseTree
|
||||
import Idris.Core.Elaborate hiding (Tactic(..))
|
||||
import Idris.Core.Evaluate
|
||||
import Idris.Core.Execute
|
||||
import Idris.Core.TT
|
||||
import Idris.Core.Typecheck
|
||||
import Idris.Core.WHNF
|
||||
import Idris.Coverage
|
||||
import Idris.DataOpts
|
||||
import Idris.DeepSeq
|
||||
import Idris.DeepSeq ()
|
||||
import Idris.Delaborate
|
||||
import Idris.Docstrings hiding (Unchecked)
|
||||
import Idris.DSL
|
||||
import Idris.Elab.AsPat
|
||||
import Idris.Elab.Term
|
||||
import Idris.Elab.Transform
|
||||
import Idris.Elab.Type
|
||||
import Idris.Elab.Utils
|
||||
import Idris.Error
|
||||
import Idris.Imports
|
||||
import Idris.Inliner
|
||||
import Idris.Options
|
||||
import Idris.Output (iRenderResult, iWarn, iputStrLn, pshow, sendHighlighting)
|
||||
import Idris.Output (iputStrLn, pshow, sendHighlighting)
|
||||
import Idris.PartialEval
|
||||
import Idris.Primitives
|
||||
import Idris.Providers
|
||||
import Idris.Termination
|
||||
import Idris.Transforms
|
||||
import IRTS.Lang
|
||||
|
||||
import Util.Pretty hiding ((<$>))
|
||||
import Util.Pretty (pretty, text)
|
||||
|
||||
import Prelude hiding (id, (.))
|
||||
|
||||
import Control.Applicative hiding (Const)
|
||||
import Control.Category
|
||||
import Control.DeepSeq
|
||||
import Control.Monad
|
||||
import qualified Control.Monad.State.Lazy as LState
|
||||
import Control.Monad.State.Strict as State
|
||||
import Data.Char (isLetter, toLower)
|
||||
import Data.List
|
||||
import Data.List.Split (splitOn)
|
||||
import qualified Data.Map as Map
|
||||
import Data.Maybe
|
||||
import qualified Data.Set as S
|
||||
import qualified Data.Text as T
|
||||
import Data.Word
|
||||
import Debug.Trace
|
||||
import Numeric
|
||||
|
@ -10,49 +10,30 @@ module Idris.Elab.Data(elabData) where
|
||||
|
||||
import Idris.AbsSyntax
|
||||
import Idris.ASTUtils
|
||||
import Idris.Core.CaseTree
|
||||
import Idris.Core.Elaborate hiding (Tactic(..))
|
||||
import Idris.Core.Evaluate
|
||||
import Idris.Core.Execute
|
||||
import Idris.Core.TT
|
||||
import Idris.Core.Typecheck
|
||||
import Idris.Coverage
|
||||
import Idris.DataOpts
|
||||
import Idris.DeepSeq
|
||||
import Idris.Delaborate
|
||||
import Idris.Docstrings
|
||||
import Idris.DSL
|
||||
import Idris.Elab.Rewrite
|
||||
import Idris.Elab.Term
|
||||
import Idris.Elab.Type
|
||||
import Idris.Elab.Utils
|
||||
import Idris.Elab.Value
|
||||
import Idris.Error
|
||||
import Idris.Imports
|
||||
import Idris.Inliner
|
||||
import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)
|
||||
import Idris.PartialEval
|
||||
import Idris.Primitives
|
||||
import Idris.Providers
|
||||
import IRTS.Lang
|
||||
import Idris.Output (iWarn, sendHighlighting)
|
||||
|
||||
import Util.Pretty
|
||||
|
||||
import Prelude hiding (id, (.))
|
||||
|
||||
import Control.Applicative hiding (Const)
|
||||
import Control.Category
|
||||
import Control.DeepSeq
|
||||
import Control.Monad
|
||||
import Control.Monad.State.Strict as State
|
||||
import Data.Char (isLetter, toLower)
|
||||
import Data.List
|
||||
import Data.List.Split (splitOn)
|
||||
import qualified Data.Map as Map
|
||||
import Data.Maybe
|
||||
import qualified Data.Set as S
|
||||
import qualified Data.Text as T
|
||||
import Debug.Trace
|
||||
|
||||
warnLC :: FC -> Name -> Idris ()
|
||||
warnLC fc n
|
||||
|
@ -9,50 +9,27 @@ Maintainer : The Idris Community.
|
||||
module Idris.Elab.Implementation(elabImplementation) where
|
||||
|
||||
import Idris.AbsSyntax
|
||||
import Idris.ASTUtils
|
||||
import Idris.Core.CaseTree
|
||||
import Idris.Core.Elaborate hiding (Tactic(..))
|
||||
import Idris.Core.Evaluate
|
||||
import Idris.Core.Execute
|
||||
import Idris.Core.TT
|
||||
import Idris.Core.Typecheck
|
||||
import Idris.Coverage
|
||||
import Idris.DataOpts
|
||||
import Idris.DeepSeq
|
||||
import Idris.Delaborate
|
||||
import Idris.Docstrings
|
||||
import Idris.DSL
|
||||
import Idris.Elab.Data
|
||||
import Idris.Elab.Term
|
||||
import Idris.Elab.Type
|
||||
import Idris.Elab.Utils
|
||||
import Idris.Error
|
||||
import Idris.Imports
|
||||
import Idris.Inliner
|
||||
import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)
|
||||
import Idris.PartialEval
|
||||
import Idris.Primitives
|
||||
import Idris.Providers
|
||||
import IRTS.Lang
|
||||
import Idris.Output (iWarn, sendHighlighting)
|
||||
|
||||
import Util.Pretty (pretty, text)
|
||||
import Util.Pretty (text)
|
||||
|
||||
import Prelude hiding (id, (.))
|
||||
|
||||
import Control.Applicative hiding (Const)
|
||||
import Control.Category
|
||||
import Control.DeepSeq
|
||||
import Control.Monad
|
||||
import Control.Monad.State.Strict as State
|
||||
import Data.Char (isLetter, toLower)
|
||||
import Data.List
|
||||
import Data.List.Split (splitOn)
|
||||
import qualified Data.Map as Map
|
||||
import Data.Maybe
|
||||
import qualified Data.Set as S
|
||||
import qualified Data.Text as T
|
||||
import Debug.Trace
|
||||
|
||||
|
||||
elabImplementation :: ElabInfo
|
||||
-> SyntaxInfo
|
||||
|
@ -10,51 +10,22 @@ Maintainer : The Idris Community.
|
||||
module Idris.Elab.Interface(elabInterface) where
|
||||
|
||||
import Idris.AbsSyntax
|
||||
import Idris.ASTUtils
|
||||
import Idris.Core.CaseTree
|
||||
import Idris.Core.Elaborate hiding (Tactic(..))
|
||||
import Idris.Core.Evaluate
|
||||
import Idris.Core.Execute
|
||||
import Idris.Core.TT
|
||||
import Idris.Core.Typecheck
|
||||
import Idris.Coverage
|
||||
import Idris.DataOpts
|
||||
import Idris.DeepSeq
|
||||
import Idris.Delaborate
|
||||
import Idris.Docstrings
|
||||
import Idris.DSL
|
||||
import Idris.Elab.Data
|
||||
import Idris.Elab.Term
|
||||
import Idris.Elab.Type
|
||||
import Idris.Elab.Utils
|
||||
import Idris.Error
|
||||
import Idris.Imports
|
||||
import Idris.Inliner
|
||||
import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)
|
||||
import Idris.PartialEval
|
||||
import Idris.Primitives
|
||||
import Idris.Providers
|
||||
import IRTS.Lang
|
||||
|
||||
import Util.Pretty (pretty, text)
|
||||
import Idris.Output (sendHighlighting)
|
||||
|
||||
import Prelude hiding (id, (.))
|
||||
|
||||
import Control.Applicative hiding (Const)
|
||||
import Control.Category
|
||||
import Control.DeepSeq
|
||||
import Control.Monad
|
||||
import Control.Monad.State.Strict as State
|
||||
import Data.Char (isLetter, toLower)
|
||||
import Data.Generics.Uniplate.Data (transform)
|
||||
import Data.List
|
||||
import Data.List.Split (splitOn)
|
||||
import qualified Data.Map as Map
|
||||
import Data.Maybe
|
||||
import qualified Data.Set as S
|
||||
import qualified Data.Text as T
|
||||
import Debug.Trace
|
||||
|
||||
|
||||
data MArgTy = IA Name | EA Name | CA deriving Show
|
||||
|
||||
|
@ -9,51 +9,24 @@ Maintainer : The Idris Community.
|
||||
module Idris.Elab.Provider(elabProvider) where
|
||||
|
||||
import Idris.AbsSyntax
|
||||
import Idris.ASTUtils
|
||||
import Idris.Core.CaseTree
|
||||
import Idris.Core.Elaborate hiding (Tactic(..))
|
||||
import Idris.Core.Evaluate
|
||||
import Idris.Core.Execute
|
||||
import Idris.Core.TT
|
||||
import Idris.Core.Typecheck
|
||||
import Idris.Coverage
|
||||
import Idris.DataOpts
|
||||
import Idris.DeepSeq
|
||||
import Idris.Delaborate
|
||||
import Idris.Docstrings
|
||||
import Idris.DSL
|
||||
import Idris.Elab.Clause
|
||||
import Idris.Elab.Term
|
||||
import Idris.Elab.Type
|
||||
import Idris.Elab.Utils
|
||||
import Idris.Elab.Value
|
||||
import Idris.Error
|
||||
import Idris.Imports
|
||||
import Idris.Inliner
|
||||
import Idris.Options
|
||||
import Idris.Output (iWarn, iputStrLn, pshow)
|
||||
import Idris.PartialEval
|
||||
import Idris.Primitives
|
||||
import Idris.Providers
|
||||
import IRTS.Lang
|
||||
|
||||
import Util.Pretty (pretty, text)
|
||||
|
||||
import Prelude hiding (id, (.))
|
||||
|
||||
import Control.Applicative hiding (Const)
|
||||
import Control.Category
|
||||
import Control.DeepSeq
|
||||
import Control.Monad
|
||||
import Control.Monad.State.Strict as State
|
||||
import Data.Char (isLetter, toLower)
|
||||
import Data.List
|
||||
import Data.List.Split (splitOn)
|
||||
import qualified Data.Map as Map
|
||||
import Data.Maybe
|
||||
import qualified Data.Set as S
|
||||
import qualified Data.Text as T
|
||||
import Debug.Trace
|
||||
|
||||
-- | Elaborate a type provider
|
||||
elabProvider :: Docstring (Either Err PTerm) -> ElabInfo -> SyntaxInfo -> FC -> FC -> ProvideWhat -> Name -> Idris ()
|
||||
|
@ -11,25 +11,12 @@ module Idris.Elab.Record(elabRecord) where
|
||||
import Idris.AbsSyntax
|
||||
import Idris.Core.Evaluate
|
||||
import Idris.Core.TT
|
||||
import Idris.Coverage
|
||||
import Idris.DataOpts
|
||||
import Idris.DeepSeq
|
||||
import Idris.Delaborate
|
||||
import Idris.Docstrings
|
||||
import Idris.Elab.Data
|
||||
import Idris.Elab.Data
|
||||
import Idris.Elab.Term
|
||||
import Idris.Elab.Type
|
||||
import Idris.Elab.Utils
|
||||
import Idris.Error
|
||||
import Idris.Imports
|
||||
import Idris.Inliner
|
||||
import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)
|
||||
import Idris.Output (sendHighlighting)
|
||||
import Idris.Parser.Expr (tryFullExpr)
|
||||
import Idris.PartialEval
|
||||
import Idris.Primitives
|
||||
import Idris.Providers
|
||||
import IRTS.Lang
|
||||
|
||||
import Control.Monad
|
||||
import Data.List
|
||||
|
@ -10,7 +10,6 @@ Maintainer : The Idris Community.
|
||||
module Idris.Elab.Rewrite(elabRewrite, elabRewriteLemma) where
|
||||
|
||||
import Idris.AbsSyntax
|
||||
import Idris.AbsSyntaxTree
|
||||
import Idris.Core.Elaborate
|
||||
import Idris.Core.Evaluate
|
||||
import Idris.Core.TT
|
||||
@ -20,8 +19,6 @@ import Idris.Error
|
||||
|
||||
import Control.Monad
|
||||
import Control.Monad.State.Strict
|
||||
import Data.List
|
||||
import Debug.Trace
|
||||
|
||||
elabRewrite :: (PTerm -> ElabD ()) -> IState ->
|
||||
FC -> Maybe Name -> PTerm -> PTerm -> Maybe PTerm -> ElabD ()
|
||||
|
@ -9,14 +9,12 @@ module Idris.Elab.RunElab (elabRunElab) where
|
||||
|
||||
import Idris.AbsSyntax
|
||||
import Idris.Core.Elaborate hiding (Tactic(..))
|
||||
import Idris.Core.Evaluate
|
||||
import Idris.Core.Execute
|
||||
import Idris.Core.TT
|
||||
import Idris.Core.Typecheck
|
||||
import Idris.Elab.Term
|
||||
import Idris.Elab.Value (elabVal)
|
||||
import Idris.Error
|
||||
import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)
|
||||
import Idris.Output (sendHighlighting)
|
||||
|
||||
elabScriptTy :: Type
|
||||
elabScriptTy = App Complete (P Ref (sNS (sUN "Elab") ["Elab", "Reflection", "Language"]) Erased)
|
||||
|
@ -10,40 +10,34 @@ Maintainer : The Idris Community.
|
||||
module Idris.Elab.Term where
|
||||
|
||||
import Idris.AbsSyntax
|
||||
import Idris.AbsSyntaxTree
|
||||
import Idris.Core.CaseTree (SC, SC'(STerm), findCalls, findUsedArgs)
|
||||
import Idris.Core.CaseTree (SC'(STerm), findCalls)
|
||||
import Idris.Core.Elaborate hiding (Tactic(..))
|
||||
import Idris.Core.Evaluate
|
||||
import Idris.Core.ProofTerm (getProofTerm)
|
||||
import Idris.Core.TT
|
||||
import Idris.Core.Typecheck (check, converts, isType, recheck)
|
||||
import Idris.Core.Unify
|
||||
import Idris.Core.WHNF (whnf, whnfArgs)
|
||||
import Idris.Coverage (genClauses, recoverableCoverage, validCoverageCase)
|
||||
import Idris.Core.WHNF (whnf)
|
||||
import Idris.Coverage (genClauses, recoverableCoverage)
|
||||
import Idris.Delaborate
|
||||
import Idris.DSL
|
||||
import Idris.Elab.Quasiquote (extractUnquotes)
|
||||
import Idris.Elab.Rewrite
|
||||
import Idris.Elab.Utils
|
||||
import Idris.Error
|
||||
import Idris.ErrReverse (errReverse)
|
||||
import Idris.Options
|
||||
import Idris.Output (pshow)
|
||||
import Idris.ProofSearch
|
||||
import Idris.Reflection
|
||||
import Idris.Termination (buildSCG, checkDeclTotality, checkPositive)
|
||||
|
||||
import qualified Util.Pretty as U
|
||||
|
||||
import Control.Applicative ((<$>))
|
||||
import Control.Monad
|
||||
import Control.Monad.State.Strict
|
||||
import Data.Foldable (for_)
|
||||
import Data.List
|
||||
import qualified Data.Map as M
|
||||
import Data.Maybe (catMaybes, fromMaybe, mapMaybe, maybeToList)
|
||||
import Data.Maybe (fromMaybe, mapMaybe, maybeToList)
|
||||
import qualified Data.Set as S
|
||||
import qualified Data.Text as T
|
||||
import Debug.Trace
|
||||
|
||||
data ElabMode = ETyDecl | ETransLHS | ELHS | EImpossible | ERHS
|
||||
|
@ -9,47 +9,19 @@ Maintainer : The Idris Community.
|
||||
module Idris.Elab.Transform where
|
||||
|
||||
import Idris.AbsSyntax
|
||||
import Idris.ASTUtils
|
||||
import Idris.Core.CaseTree
|
||||
import Idris.Core.Elaborate hiding (Tactic(..))
|
||||
import Idris.Core.Evaluate
|
||||
import Idris.Core.Execute
|
||||
import Idris.Core.TT
|
||||
import Idris.Core.Typecheck
|
||||
import Idris.Coverage
|
||||
import Idris.DataOpts
|
||||
import Idris.DeepSeq
|
||||
import Idris.Delaborate
|
||||
import Idris.Docstrings
|
||||
import Idris.DSL
|
||||
import Idris.Elab.Term
|
||||
import Idris.Elab.Utils
|
||||
import Idris.Error
|
||||
import Idris.Imports
|
||||
import Idris.Inliner
|
||||
import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)
|
||||
import Idris.PartialEval
|
||||
import Idris.Primitives
|
||||
import Idris.Providers
|
||||
import IRTS.Lang
|
||||
|
||||
import Util.Pretty (pretty, text)
|
||||
import Idris.Output (sendHighlighting)
|
||||
|
||||
import Prelude hiding (id, (.))
|
||||
|
||||
import Control.Applicative hiding (Const)
|
||||
import Control.Category
|
||||
import Control.DeepSeq
|
||||
import Control.Monad
|
||||
import Control.Monad.State.Strict as State
|
||||
import Data.Char (isLetter, toLower)
|
||||
import Data.List
|
||||
import Data.List.Split (splitOn)
|
||||
import qualified Data.Map as Map
|
||||
import Data.Maybe
|
||||
import qualified Data.Set as S
|
||||
import qualified Data.Text as T
|
||||
import Debug.Trace
|
||||
|
||||
elabTransform :: ElabInfo -> FC -> Bool -> PTerm -> PTerm -> Idris (Term, Term)
|
||||
elabTransform info fc safe lhs_in@(PApp _ (PRef _ _ tf) _) rhs_in
|
||||
|
@ -13,50 +13,23 @@ module Idris.Elab.Type (
|
||||
|
||||
import Idris.AbsSyntax
|
||||
import Idris.ASTUtils
|
||||
import Idris.Core.CaseTree
|
||||
import Idris.Core.Elaborate hiding (Tactic(..))
|
||||
import Idris.Core.Evaluate
|
||||
import Idris.Core.Execute
|
||||
import Idris.Core.TT
|
||||
import Idris.Core.Typecheck
|
||||
import Idris.Core.WHNF
|
||||
import Idris.Coverage
|
||||
import Idris.DataOpts
|
||||
import Idris.DeepSeq
|
||||
import Idris.Delaborate
|
||||
import Idris.Docstrings (Docstring)
|
||||
import Idris.DSL
|
||||
import Idris.Elab.Term
|
||||
import Idris.Elab.Utils
|
||||
import Idris.Elab.Value
|
||||
import Idris.Error
|
||||
import Idris.Imports
|
||||
import Idris.Inliner
|
||||
import Idris.Options
|
||||
import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)
|
||||
import Idris.PartialEval
|
||||
import Idris.Primitives
|
||||
import Idris.Providers
|
||||
import IRTS.Lang
|
||||
|
||||
import Util.Pretty (pretty, text)
|
||||
import Idris.Output (sendHighlighting)
|
||||
|
||||
import Prelude hiding (id, (.))
|
||||
|
||||
import Control.Applicative hiding (Const)
|
||||
import Control.Category
|
||||
import Control.DeepSeq
|
||||
import Control.Monad
|
||||
import Control.Monad.State.Strict as State
|
||||
import Data.Char (isLetter, toLower)
|
||||
import Data.List
|
||||
import Data.List.Split (splitOn)
|
||||
import qualified Data.Map as Map
|
||||
import Data.Maybe
|
||||
import qualified Data.Set as S
|
||||
import qualified Data.Text as T
|
||||
import qualified Data.Traversable as Traversable
|
||||
import Debug.Trace
|
||||
|
||||
buildType :: ElabInfo
|
||||
-> SyntaxInfo
|
||||
|
@ -14,7 +14,6 @@ import Idris.Core.Evaluate
|
||||
import Idris.Core.TT
|
||||
import Idris.Core.Typecheck
|
||||
import Idris.Core.WHNF
|
||||
import Idris.DeepSeq
|
||||
import Idris.Delaborate
|
||||
import Idris.Docstrings
|
||||
import Idris.Error
|
||||
@ -22,14 +21,11 @@ import Idris.Output
|
||||
|
||||
import Util.Pretty
|
||||
|
||||
import Control.Applicative hiding (Const)
|
||||
import Control.Monad
|
||||
import Control.Monad.State
|
||||
import Data.List
|
||||
import qualified Data.Map as Map
|
||||
import Data.Maybe
|
||||
import qualified Data.Traversable as Traversable
|
||||
import Debug.Trace
|
||||
|
||||
recheckC = recheckC_borrowing False True []
|
||||
|
||||
|
@ -13,48 +13,20 @@ module Idris.Elab.Value(
|
||||
) where
|
||||
|
||||
import Idris.AbsSyntax
|
||||
import Idris.ASTUtils
|
||||
import Idris.Core.CaseTree
|
||||
import Idris.Core.Elaborate hiding (Tactic(..))
|
||||
import Idris.Core.Evaluate hiding (Unchecked)
|
||||
import Idris.Core.Execute
|
||||
import Idris.Core.TT
|
||||
import Idris.Core.Typecheck
|
||||
import Idris.Coverage
|
||||
import Idris.DataOpts
|
||||
import Idris.DeepSeq
|
||||
import Idris.Delaborate
|
||||
import Idris.Docstrings
|
||||
import Idris.DSL
|
||||
import Idris.Elab.Term
|
||||
import Idris.Elab.Utils
|
||||
import Idris.Error
|
||||
import Idris.Imports
|
||||
import Idris.Inliner
|
||||
import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)
|
||||
import Idris.PartialEval
|
||||
import Idris.Primitives
|
||||
import Idris.Providers
|
||||
import IRTS.Lang
|
||||
|
||||
import Util.Pretty (pretty, text)
|
||||
import Idris.Output (sendHighlighting)
|
||||
|
||||
import Prelude hiding (id, (.))
|
||||
|
||||
import Control.Applicative hiding (Const)
|
||||
import Control.Category
|
||||
import Control.DeepSeq
|
||||
import Control.Monad
|
||||
import Control.Monad.State.Strict as State
|
||||
import Data.Char (isLetter, toLower)
|
||||
import Data.List
|
||||
import Data.List.Split (splitOn)
|
||||
import qualified Data.Map as Map
|
||||
import Data.Maybe
|
||||
import qualified Data.Set as S
|
||||
import qualified Data.Text as T
|
||||
import Data.Char (toLower)
|
||||
import qualified Data.Traversable as Traversable
|
||||
import Debug.Trace
|
||||
|
||||
-- | Elaborate a value, returning any new bindings created (this will only
|
||||
-- happen if elaborating as a pattern clause)
|
||||
|
@ -12,20 +12,10 @@ Maintainer : The Idris Community.
|
||||
module Idris.ElabDecls where
|
||||
|
||||
import Idris.AbsSyntax
|
||||
import Idris.ASTUtils
|
||||
import Idris.Core.CaseTree
|
||||
import Idris.Core.Elaborate hiding (Tactic(..))
|
||||
import Idris.Core.Evaluate
|
||||
import Idris.Core.Execute
|
||||
import Idris.Core.TT
|
||||
import Idris.Core.Typecheck
|
||||
import Idris.Coverage
|
||||
import Idris.DataOpts
|
||||
import Idris.DeepSeq
|
||||
import Idris.Delaborate
|
||||
import Idris.Directives
|
||||
import Idris.Docstrings hiding (Unchecked)
|
||||
import Idris.DSL
|
||||
import Idris.Elab.Clause
|
||||
import Idris.Elab.Data
|
||||
import Idris.Elab.Implementation
|
||||
@ -36,36 +26,21 @@ import Idris.Elab.RunElab
|
||||
import Idris.Elab.Term
|
||||
import Idris.Elab.Transform
|
||||
import Idris.Elab.Type
|
||||
import Idris.Elab.Utils
|
||||
import Idris.Elab.Value
|
||||
import Idris.Error
|
||||
import Idris.Imports
|
||||
import Idris.Inliner
|
||||
import Idris.Options
|
||||
import Idris.Output (iWarn, iputStrLn, pshow, sendHighlighting)
|
||||
import Idris.PartialEval
|
||||
import Idris.Output (sendHighlighting)
|
||||
import Idris.Primitives
|
||||
import Idris.Providers
|
||||
import Idris.Termination
|
||||
import IRTS.Lang
|
||||
|
||||
import Util.Pretty (pretty, text)
|
||||
|
||||
import Prelude hiding (id, (.))
|
||||
|
||||
import Control.Applicative hiding (Const)
|
||||
import Control.Category
|
||||
import Control.DeepSeq
|
||||
import Control.Monad
|
||||
import Control.Monad.State.Strict as State
|
||||
import Data.Char (isLetter, toLower)
|
||||
import Data.List
|
||||
import Data.List.Split (splitOn)
|
||||
import qualified Data.Map as Map
|
||||
import Data.Maybe
|
||||
import qualified Data.Set as S
|
||||
import qualified Data.Text as T
|
||||
import Debug.Trace
|
||||
|
||||
-- | Top level elaborator info, supporting recursive elaboration
|
||||
recinfo :: FC -> ElabInfo
|
||||
|
@ -20,7 +20,6 @@ import Idris.Primitives
|
||||
|
||||
import Prelude hiding (id, (.))
|
||||
|
||||
import Control.Applicative
|
||||
import Control.Arrow
|
||||
import Control.Category
|
||||
import Control.Monad.State
|
||||
@ -36,8 +35,6 @@ import Data.Set (Set)
|
||||
import qualified Data.Set as S
|
||||
import Data.Text (pack)
|
||||
import qualified Data.Text as T
|
||||
import Debug.Trace
|
||||
import System.IO.Unsafe
|
||||
|
||||
-- | UseMap maps names to the set of used (reachable) argument
|
||||
-- positions.
|
||||
|
@ -15,7 +15,6 @@ import Idris.Core.TT
|
||||
import Util.Pretty
|
||||
|
||||
import Data.List
|
||||
import Debug.Trace
|
||||
|
||||
-- | For display purposes, apply any 'error reversal' transformations
|
||||
-- so that errors will be more readable,
|
||||
|
@ -14,23 +14,16 @@ import Idris.AbsSyntax
|
||||
import Idris.Core.Constraints
|
||||
import Idris.Core.Evaluate (ctxtAlist)
|
||||
import Idris.Core.TT
|
||||
import Idris.Core.Typecheck
|
||||
import Idris.Delaborate
|
||||
import Idris.Output
|
||||
|
||||
import Prelude hiding (catch)
|
||||
|
||||
import Control.Monad (when)
|
||||
import Control.Monad.State.Strict
|
||||
import Data.Char
|
||||
import qualified Data.Foldable as Foldable
|
||||
import Data.List (intercalate, isPrefixOf)
|
||||
import qualified Data.Set as S
|
||||
import qualified Data.Text as T
|
||||
import qualified Data.Traversable as Traversable
|
||||
import Data.Typeable
|
||||
import System.Console.Haskeline
|
||||
import System.Console.Haskeline.MonadException
|
||||
import System.IO.Error (ioeGetErrorString, isUserError)
|
||||
|
||||
iucheck :: Idris ()
|
||||
|
@ -11,7 +11,7 @@ Maintainer : The Idris Community.
|
||||
|
||||
module Idris.IdeMode(parseMessage, convSExp, WhatDocs(..), IdeModeCommand(..), sexpToCommand, toSExp, SExp(..), SExpable, Opt(..), ideModeEpoch, getLen, getNChar, sExpToString) where
|
||||
|
||||
import Idris.Core.Binary
|
||||
import Idris.Core.Binary ()
|
||||
import Idris.Core.TT
|
||||
|
||||
import Control.Applicative hiding (Const)
|
||||
|
@ -10,11 +10,10 @@ Maintainer : The Idris Community.
|
||||
module Idris.IdrisDoc (generateDocs) where
|
||||
|
||||
import Idris.AbsSyntax
|
||||
import Idris.Core.Evaluate (Accessibility(..), Def(..), ctxtAlist, isDConName,
|
||||
isFnName, isTConName, lookupDefAcc)
|
||||
import Idris.Core.TT (Name(..), OutputAnnotation(..), SpecialName(..),
|
||||
TextFormatting(..), constIsType, nsroot, sUN, str,
|
||||
toAlist, txt)
|
||||
import Idris.Core.Evaluate (Accessibility(..), ctxtAlist, isDConName, isFnName,
|
||||
isTConName, lookupDefAcc)
|
||||
import Idris.Core.TT (Name(..), OutputAnnotation(..), TextFormatting(..),
|
||||
constIsType, nsroot, sUN, str, toAlist, txt)
|
||||
import Idris.Docs
|
||||
import Idris.Docstrings (nullDocstring)
|
||||
import qualified Idris.Docstrings as Docstrings
|
||||
@ -26,17 +25,13 @@ import Control.Applicative ((<|>))
|
||||
import Control.Monad (forM_)
|
||||
import Control.Monad.Trans.Except
|
||||
import Control.Monad.Trans.State.Strict
|
||||
import qualified Data.ByteString as BS
|
||||
import qualified Data.ByteString.Lazy as BS2
|
||||
import qualified Data.List as L
|
||||
import qualified Data.List.Split as LS
|
||||
import qualified Data.Map as M hiding ((!))
|
||||
import Data.Maybe
|
||||
import Data.Monoid (mempty)
|
||||
import qualified Data.Ord (compare)
|
||||
import qualified Data.Set as S
|
||||
import qualified Data.Text as T
|
||||
import qualified Data.Text.Encoding as E
|
||||
import System.Directory
|
||||
import System.FilePath
|
||||
import System.IO
|
||||
|
@ -13,7 +13,6 @@ module Idris.Imports(
|
||||
import Idris.AbsSyntax
|
||||
import Idris.Core.TT
|
||||
import Idris.Error
|
||||
import Idris.Output
|
||||
import IRTS.System (getIdrisLibDir)
|
||||
|
||||
import Control.Applicative ((<$>))
|
||||
|
@ -29,7 +29,6 @@ import Idris.Imports (installedPackages)
|
||||
import Idris.Options (loggingCatsStr)
|
||||
import qualified IRTS.System as S
|
||||
|
||||
import Paths_idris
|
||||
import Version_idris (gitHash)
|
||||
|
||||
import Data.Version
|
||||
|
@ -13,7 +13,7 @@ module Idris.Output where
|
||||
|
||||
import Idris.AbsSyntax
|
||||
import Idris.Colours (hEndColourise, hStartColourise)
|
||||
import Idris.Core.Evaluate (isDConName, isFnName, isTConName, normaliseAll)
|
||||
import Idris.Core.Evaluate (normaliseAll)
|
||||
import Idris.Core.TT
|
||||
import Idris.Delaborate
|
||||
import Idris.Docstrings
|
||||
@ -27,13 +27,12 @@ import Util.System (isATTY)
|
||||
import Prelude hiding ((<$>))
|
||||
|
||||
import Control.Monad.Trans.Except (ExceptT(ExceptT), runExceptT)
|
||||
import Data.Char (isAlpha)
|
||||
import Data.List (intersperse, nub)
|
||||
import Data.Maybe (fromMaybe)
|
||||
import System.Console.Haskeline.MonadException (MonadException(controlIO),
|
||||
RunIO(RunIO))
|
||||
import System.FilePath (replaceExtension)
|
||||
import System.IO (Handle, hPutStr, hPutStrLn, stdout)
|
||||
import System.IO (Handle, hPutStr, hPutStrLn)
|
||||
|
||||
instance MonadException m => MonadException (ExceptT Err m) where
|
||||
controlIO f = ExceptT $ controlIO $ \(RunIO run) -> let
|
||||
|
@ -12,7 +12,7 @@ import System.Directory
|
||||
import System.Directory (copyFile, createDirectoryIfMissing)
|
||||
import System.Exit
|
||||
import System.FilePath (addExtension, addTrailingPathSeparator, dropExtension,
|
||||
hasExtension, normalise, takeDirectory, takeExtension,
|
||||
hasExtension, takeDirectory, takeExtension,
|
||||
takeFileName, (</>))
|
||||
import System.IO
|
||||
import System.Process
|
||||
@ -23,10 +23,8 @@ import Control.Monad
|
||||
import Control.Monad.Trans.Except (runExceptT)
|
||||
import Control.Monad.Trans.State.Strict (execStateT)
|
||||
import Data.Either (partitionEithers)
|
||||
import Data.Either (partitionEithers)
|
||||
import Data.List
|
||||
import Data.List.Split (splitOn)
|
||||
import Data.Maybe (fromMaybe)
|
||||
|
||||
import Idris.AbsSyntax
|
||||
import Idris.Core.TT
|
||||
@ -38,7 +36,6 @@ import Idris.Main (idris, idrisMain)
|
||||
import Idris.Options
|
||||
import Idris.Output
|
||||
import Idris.Parser (loadModule)
|
||||
import Idris.REPL
|
||||
|
||||
import Idris.Package.Common
|
||||
import Idris.Package.Parser
|
||||
|
@ -8,19 +8,13 @@ Maintainer : The Idris Community.
|
||||
{-# LANGUAGE CPP, ConstraintKinds, FlexibleInstances, TypeSynonymInstances #-}
|
||||
module Idris.Package.Parser where
|
||||
|
||||
import Idris.AbsSyntaxTree
|
||||
import Idris.CmdOptions
|
||||
import Idris.Core.TT
|
||||
import Idris.Package.Common
|
||||
import Idris.Parser.Helpers hiding (stringLiteral)
|
||||
import Idris.REPL
|
||||
|
||||
import Util.System
|
||||
|
||||
import Control.Applicative
|
||||
import Control.Monad.State.Strict
|
||||
import Data.List (union)
|
||||
import Data.Maybe (fromJust, isNothing)
|
||||
import System.Directory (doesFileExist)
|
||||
import System.Exit
|
||||
import System.FilePath (isValid, takeExtension, takeFileName)
|
||||
|
@ -12,7 +12,6 @@ import Idris.AbsSyntax
|
||||
import Idris.Core.Evaluate
|
||||
import Idris.Core.TT
|
||||
import Idris.Docstrings
|
||||
import Idris.DSL
|
||||
import Idris.Options
|
||||
import Idris.Parser.Expr
|
||||
import Idris.Parser.Helpers
|
||||
@ -21,25 +20,11 @@ import Idris.Parser.Ops
|
||||
import Prelude hiding (pi)
|
||||
|
||||
import Control.Applicative
|
||||
import Control.Monad
|
||||
import Control.Monad.State.Strict
|
||||
import qualified Data.ByteString.UTF8 as UTF8
|
||||
import Data.Char
|
||||
import qualified Data.HashSet as HS
|
||||
import Data.List
|
||||
import qualified Data.List.Split as Spl
|
||||
import Data.Maybe
|
||||
import Data.Monoid
|
||||
import qualified Data.Text as T
|
||||
import Debug.Trace
|
||||
import qualified Text.Parser.Char as Chr
|
||||
import Text.Parser.Expression
|
||||
import Text.Parser.LookAhead
|
||||
import qualified Text.Parser.Token as Tok
|
||||
import qualified Text.Parser.Token.Highlight as Hi
|
||||
import Text.Trifecta hiding (Err, char, charLiteral, natural, span, string,
|
||||
stringLiteral, symbol, whiteSpace)
|
||||
import Text.Trifecta.Delta
|
||||
|
||||
{- | Parses a record type declaration
|
||||
Record ::=
|
||||
|
@ -21,24 +21,12 @@ import Prelude hiding (pi)
|
||||
import Control.Applicative
|
||||
import Control.Monad
|
||||
import Control.Monad.State.Strict
|
||||
import qualified Data.ByteString.UTF8 as UTF8
|
||||
import Data.Char
|
||||
import Data.Function (on)
|
||||
import qualified Data.HashSet as HS
|
||||
import Data.List
|
||||
import qualified Data.List.Split as Spl
|
||||
import Data.Maybe
|
||||
import Data.Monoid
|
||||
import qualified Data.Text as T
|
||||
import Debug.Trace
|
||||
import qualified Text.Parser.Char as Chr
|
||||
import Text.Parser.Expression
|
||||
import Text.Parser.LookAhead
|
||||
import qualified Text.Parser.Token as Tok
|
||||
import qualified Text.Parser.Token.Highlight as Hi
|
||||
import Text.Trifecta hiding (Err, char, charLiteral, natural, span, string,
|
||||
stringLiteral, symbol, whiteSpace)
|
||||
import Text.Trifecta.Delta
|
||||
|
||||
-- | Allow implicit type declarations
|
||||
allowImp :: SyntaxInfo -> SyntaxInfo
|
||||
|
@ -18,8 +18,6 @@ import Idris.Docstrings
|
||||
import Idris.Options
|
||||
import Idris.Output (iWarn)
|
||||
|
||||
import qualified Util.Pretty as Pretty (text)
|
||||
|
||||
import Prelude hiding (pi)
|
||||
|
||||
import Control.Applicative
|
||||
@ -29,15 +27,11 @@ import qualified Data.ByteString.UTF8 as UTF8
|
||||
import Data.Char
|
||||
import qualified Data.HashSet as HS
|
||||
import Data.List
|
||||
import qualified Data.List.Split as Spl
|
||||
import qualified Data.Map as M
|
||||
import Data.Maybe
|
||||
import Data.Monoid
|
||||
import qualified Data.Text as T
|
||||
import Debug.Trace
|
||||
import System.FilePath
|
||||
import qualified Text.Parser.Char as Chr
|
||||
import Text.Parser.Expression
|
||||
import Text.Parser.LookAhead
|
||||
import qualified Text.Parser.Token as Tok
|
||||
import qualified Text.Parser.Token.Highlight as Hi
|
||||
|
@ -18,23 +18,10 @@ import Prelude hiding (pi)
|
||||
import Control.Applicative
|
||||
import Control.Monad
|
||||
import Control.Monad.State.Strict
|
||||
import qualified Data.ByteString.UTF8 as UTF8
|
||||
import Data.Char
|
||||
import qualified Data.HashSet as HS
|
||||
import Data.List
|
||||
import qualified Data.List.Split as Spl
|
||||
import Data.Maybe
|
||||
import Data.Monoid
|
||||
import qualified Data.Text as T
|
||||
import Debug.Trace
|
||||
import qualified Text.Parser.Char as Chr
|
||||
import Text.Parser.Expression
|
||||
import Text.Parser.LookAhead
|
||||
import qualified Text.Parser.Token as Tok
|
||||
import qualified Text.Parser.Token.Highlight as Hi
|
||||
import Text.Trifecta hiding (char, charLiteral, natural, span, string,
|
||||
stringLiteral, symbol, whiteSpace)
|
||||
import Text.Trifecta.Delta
|
||||
|
||||
-- | Creates table for fixity declarations to build expression parser
|
||||
-- using pre-build and user-defined operator/fixity declarations
|
||||
|
@ -19,10 +19,7 @@ import Idris.Core.Evaluate
|
||||
import Idris.Core.TT
|
||||
import Idris.Delaborate
|
||||
|
||||
import Control.Applicative
|
||||
import Control.Monad.State
|
||||
import Data.Maybe
|
||||
import Debug.Trace
|
||||
|
||||
-- | Data type representing binding-time annotations for partial evaluation of arguments
|
||||
data PEArgType = ImplicitS Name -- ^ Implicit static argument
|
||||
|
@ -9,7 +9,6 @@ Maintainer : The Idris Community.
|
||||
|
||||
module Idris.Primitives(primitives, Prim(..)) where
|
||||
|
||||
import Idris.AbsSyntax
|
||||
import Idris.Core.Evaluate
|
||||
import Idris.Core.TT
|
||||
import IRTS.Lang
|
||||
@ -18,9 +17,7 @@ import Data.Bits
|
||||
import Data.Char
|
||||
import Data.Function (on)
|
||||
import Data.Int
|
||||
import qualified Data.Vector.Unboxed as V
|
||||
import Data.Word
|
||||
import Debug.Trace
|
||||
|
||||
data Prim = Prim { p_name :: Name,
|
||||
p_type :: Type,
|
||||
|
@ -16,14 +16,11 @@ module Idris.ProofSearch(
|
||||
) where
|
||||
|
||||
import Idris.AbsSyntax
|
||||
import Idris.Core.CaseTree
|
||||
import Idris.Core.Elaborate hiding (Tactic(..))
|
||||
import Idris.Core.Evaluate
|
||||
import Idris.Core.TT
|
||||
import Idris.Core.Typecheck
|
||||
import Idris.Core.Unify
|
||||
import Idris.Delaborate
|
||||
import Idris.Error
|
||||
|
||||
import Control.Applicative ((<$>))
|
||||
import Control.Monad
|
||||
|
@ -11,12 +11,11 @@ module Idris.Prover (prover, showProof, showRunElab) where
|
||||
-- Hack for GHC 7.10 and earlier compat without CPP or warnings
|
||||
-- This exludes (<$>) as fmap, because wl-pprint uses it for newline
|
||||
import Prelude (Bool(..), Either(..), Eq(..), Maybe(..), Show(..), String,
|
||||
concatMap, elem, error, flip, foldl, foldr, fst, id, init,
|
||||
length, lines, map, not, null, repeat, reverse, tail, zip, ($),
|
||||
(&&), (++), (.), (||))
|
||||
concatMap, elem, error, foldl, foldr, fst, id, init, length,
|
||||
lines, map, not, null, repeat, reverse, tail, zip, ($), (&&),
|
||||
(++), (.), (||))
|
||||
|
||||
import Idris.AbsSyntax
|
||||
import Idris.AbsSyntaxTree
|
||||
import Idris.Completion
|
||||
import Idris.Core.CaseTree
|
||||
import Idris.Core.Elaborate hiding (Tactic(..))
|
||||
@ -41,7 +40,6 @@ import Util.Pretty
|
||||
|
||||
import Control.DeepSeq
|
||||
import Control.Monad.State.Strict
|
||||
import Debug.Trace
|
||||
import System.Console.Haskeline
|
||||
import System.Console.Haskeline.History
|
||||
import System.IO (Handle, hPutStrLn, stdin, stdout)
|
||||
|
@ -13,8 +13,6 @@ module Idris.Providers (
|
||||
) where
|
||||
|
||||
import Idris.AbsSyntax
|
||||
import Idris.AbsSyntaxTree
|
||||
import Idris.Core.Evaluate
|
||||
import Idris.Core.TT
|
||||
import Idris.Error
|
||||
|
||||
|
@ -21,17 +21,14 @@ import Idris.REPL.Commands
|
||||
|
||||
import Control.Applicative
|
||||
import Control.Monad.State.Strict
|
||||
import qualified Data.ByteString.UTF8 as UTF8
|
||||
import Data.Char (isSpace, toLower)
|
||||
import Data.List
|
||||
import Data.List.Split (splitOn)
|
||||
import Debug.Trace
|
||||
import System.Console.ANSI (Color(..))
|
||||
import System.FilePath ((</>))
|
||||
import Text.Parser.Char (anyChar, oneOf)
|
||||
import Text.Parser.Combinators
|
||||
import Text.Trifecta (Result, parseString)
|
||||
import Text.Trifecta.Delta
|
||||
import Text.Trifecta (Result)
|
||||
|
||||
parseCmd :: IState -> String -> String -> Result (Either String Command)
|
||||
parseCmd i inputname = P.runparser pCmd i inputname . trim
|
||||
|
@ -15,10 +15,9 @@ import Idris.Core.TT
|
||||
import Idris.Delaborate
|
||||
import Idris.Error
|
||||
import Idris.Options
|
||||
import Idris.Output (iWarn, iputStrLn)
|
||||
import Idris.Output (iWarn)
|
||||
|
||||
import Control.Monad.State.Strict
|
||||
import Data.Char
|
||||
import Data.Either
|
||||
import Data.List
|
||||
import Data.Maybe
|
||||
|
@ -16,11 +16,8 @@ module Idris.Transforms(
|
||||
) where
|
||||
|
||||
import Idris.AbsSyntax
|
||||
import Idris.Core.CaseTree
|
||||
import Idris.Core.TT
|
||||
|
||||
import Debug.Trace
|
||||
|
||||
transformPats :: IState -> [Either Term (Term, Term)] ->
|
||||
[Either Term (Term, Term)]
|
||||
transformPats ist ps = map tClause ps where
|
||||
|
@ -14,7 +14,7 @@ module Idris.TypeSearch (
|
||||
) where
|
||||
|
||||
import Idris.AbsSyntax (addImpl, addUsingConstraints, getIState, implicit,
|
||||
logLvl, putIState)
|
||||
putIState)
|
||||
import Idris.AbsSyntaxTree (IState(idris_docstrings, idris_interfaces, idris_outputmode, tt_ctxt),
|
||||
Idris, InterfaceInfo, OutputMode(..), PTerm,
|
||||
defaultSyntax, eqTy, implicitAllowed,
|
||||
|
@ -13,22 +13,29 @@ module Util.DynamicLinker ( ForeignFun(..)
|
||||
) where
|
||||
|
||||
#ifdef IDRIS_FFI
|
||||
import Foreign.LibFFI
|
||||
import Foreign.Ptr (FunPtr, Ptr, castPtrToFunPtr, nullFunPtr, nullPtr)
|
||||
import System.Directory
|
||||
#ifndef mingw32_HOST_OS
|
||||
import Control.Exception (IOException, throwIO, try)
|
||||
import Data.Array (Array, bounds, inRange, (!))
|
||||
import Data.Functor ((<$>))
|
||||
import Data.Maybe (catMaybes)
|
||||
import System.FilePath.Posix ((</>))
|
||||
import System.Posix.DynamicLinker
|
||||
import Text.Regex.TDFA
|
||||
#else
|
||||
#ifdef mingw32_HOST_OS
|
||||
import qualified Control.Exception as Exception (IOException, catch)
|
||||
import Foreign.Ptr (FunPtr, castPtrToFunPtr, nullFunPtr, nullPtr)
|
||||
import System.FilePath.Windows ((</>))
|
||||
import System.Win32.DLL
|
||||
import System.Win32.Types
|
||||
#else
|
||||
import Control.Exception (IOException, throwIO, try)
|
||||
import Foreign.Ptr (FunPtr, nullFunPtr, nullPtr)
|
||||
#ifdef linux_HOST_OS
|
||||
import Data.Array (bounds, inRange, (!))
|
||||
import Data.Functor ((<$>))
|
||||
import Data.Maybe (catMaybes)
|
||||
#else
|
||||
import Data.Array (bounds, (!))
|
||||
#endif
|
||||
import System.FilePath.Posix ((</>))
|
||||
import System.Posix.DynamicLinker
|
||||
import Text.Regex.TDFA
|
||||
#endif
|
||||
|
||||
#ifdef mingw32_HOST_OS
|
||||
type DL = HMODULE
|
||||
#endif
|
||||
|
||||
|
@ -9,6 +9,9 @@ flags:
|
||||
FFI: true
|
||||
GMP: true
|
||||
|
||||
ghc-options:
|
||||
idris: -fwarn-unused-imports -fwarn-unused-binds
|
||||
|
||||
extra-deps:
|
||||
- binary-0.8.5.1
|
||||
- cheapskate-0.1.1
|
||||
|
Loading…
Reference in New Issue
Block a user