git.iko.soy/Idris-dev
on master help sign in
Add a Cabal library
5000aebBrian McKenna
idris.cabal+118−9
compare with master
unifiedsplit
@@ -301,19 +301,128 @@ Flag FFI
301 Default: False
301 Default: False
302 manual: True
302 manual: True
303
303
304+Library
305+ hs-source-dirs: src
306+ Exposed-modules:
307+ Idris.Core.CaseTree
308+ , Idris.Core.Constraints
309+ , Idris.Core.Elaborate
310+ , Idris.Core.Evaluate
311+ , Idris.Core.Execute
312+ , Idris.Core.ProofState
313+ , Idris.Core.TT
314+ , Idris.Core.Typecheck
315+ , Idris.Core.Unify
316+
317+ , Idris.AbsSyntax
318+ , Idris.AbsSyntaxTree
319+ , Idris.CaseSplit
320+ , Idris.Chaser
321+ , Idris.Colours
322+ , Idris.Completion
323+ , Idris.Coverage
324+ , Idris.DSL
325+ , Idris.DataOpts
326+ , Idris.DeepSeq
327+ , Idris.Delaborate
328+ , Idris.Docs
329+ , Idris.ElabDecls
330+ , Idris.ElabTerm
331+ , Idris.Error
332+ , Idris.Help
333+ , Idris.IBC
334+ , Idris.IdeSlave
335+ , Idris.Imports
336+ , Idris.Inliner
337+ , Idris.Parser
338+ , Idris.ParseHelpers
339+ , Idris.ParseOps
340+ , Idris.ParseExpr
341+ , Idris.ParseData
342+ , Idris.PartialEval
343+ , Idris.Primitives
344+ , Idris.ProofSearch
345+ , Idris.Prover
346+ , Idris.Providers
347+ , Idris.REPL
348+ , Idris.REPLParser
349+ , Idris.Transforms
350+ , Idris.Unlit
351+ , Idris.UnusedArgs
352+
353+ , IRTS.BCImp
354+ , IRTS.Bytecode
355+ , IRTS.CodegenC
356+ , IRTS.CodegenCommon
357+ , IRTS.CodegenJava
358+ , IRTS.CodegenJavaScript
359+ , IRTS.Compiler
360+ , IRTS.Defunctionalise
361+ , IRTS.DumpBC
362+ , IRTS.Inliner
363+ , IRTS.Java.ASTBuilding
364+ , IRTS.Java.JTypes
365+ , IRTS.Java.Mangling
366+ , IRTS.Java.Pom
367+ , IRTS.Lang
368+ , IRTS.Simplified
369+
370+ Other-modules:
371+ Util.Pretty
372+ , Util.System
373+ , Util.DynamicLinker
374+ , Util.Net
375+
376+ , Pkg.Package
377+ , Pkg.PParser
378+
379+ -- Auto Generated
380+ Paths_idris
381+
382+ Extensions: MultiParamTypeClasses
383+ , FunctionalDependencies
384+ , FlexibleInstances
385+ , TemplateHaskell
386+
387+ ghc-prof-options: -auto-all -caf-all
388+ ghc-options: -threaded -rtsopts
389+
390+ if os(linux)
391+ cpp-options: -DLINUX
392+ build-depends: unix
393+ if os(freebsd)
394+ cpp-options: -DFREEBSD
395+ build-depends: unix
396+ if os(darwin)
397+ cpp-options: -DMACOSX
398+ build-depends: unix
399+ if os(windows)
400+ cpp-options: -DWINDOWS
401+ build-depends: Win32
402+ if flag(LLVM)
403+ other-modules: IRTS.CodegenLLVM
404+ cpp-options: -DIDRIS_LLVM
405+ build-depends: llvm-general == 3.3.8.*
406+ , llvm-general-pure == 3.3.8.*
407+ else
408+ other-modules: Util.LLVMStubs
409+ if flag(FFI)
410+ build-depends: libffi
411+ cpp-options: -DIDRIS_FFI
412+
304Executable idris
413Executable idris
305 Main-is: Main.hs
414 Main-is: Main.hs
306 hs-source-dirs: src
415 hs-source-dirs: src
307 Other-modules:
416 Other-modules:
308− Core.CaseTree
417+ Idris.Core.CaseTree
309− , Core.Constraints
418+ , Idris.Core.Constraints
310− , Core.Elaborate
419+ , Idris.Core.Elaborate
311− , Core.Evaluate
420+ , Idris.Core.Evaluate
312− , Core.Execute
421+ , Idris.Core.Execute
313− , Core.ProofState
422+ , Idris.Core.ProofState
314− , Core.TT
423+ , Idris.Core.TT
315− , Core.Typecheck
424+ , Idris.Core.Typecheck
316− , Core.Unify
425+ , Idris.Core.Unify
317
426
318 , Idris.AbsSyntax
427 , Idris.AbsSyntax
319 , Idris.AbsSyntaxTree
428 , Idris.AbsSyntaxTree
src/IRTS/BCImp.hs+1−1
@@ -5,7 +5,7 @@ module IRTS.BCImp where
5
5
6import IRTS.Lang
6import IRTS.Lang
7import IRTS.Simplified
7import IRTS.Simplified
8−import Core.TT
8+import Idris.Core.TT
9
9
10data Reg = RVal | L Int
10data Reg = RVal | L Int
11
11
src/IRTS/Bytecode.hs+1−1
@@ -5,7 +5,7 @@ module IRTS.Bytecode where
5
5
6import IRTS.Lang
6import IRTS.Lang
7import IRTS.Simplified
7import IRTS.Simplified
8−import Core.TT
8+import Idris.Core.TT
9import Data.Maybe
9import Data.Maybe
10
10
11{- We have:
11{- We have:
src/IRTS/CodegenC.hs+1−1
@@ -5,7 +5,7 @@ import IRTS.Bytecode
5import IRTS.Lang
5import IRTS.Lang
6import IRTS.Simplified
6import IRTS.Simplified
7import IRTS.CodegenCommon
7import IRTS.CodegenCommon
8−import Core.TT
8+import Idris.Core.TT
9import Paths_idris
9import Paths_idris
10import Util.System
10import Util.System
11
11
src/IRTS/CodegenCommon.hs+1−1
@@ -1,6 +1,6 @@
1module IRTS.CodegenCommon where
1module IRTS.CodegenCommon where
2
2
3−import Core.TT
3+import Idris.Core.TT
4import IRTS.Simplified
4import IRTS.Simplified
5
5
6import Control.Exception
6import Control.Exception
src/IRTS/CodegenJava.hs+1−1
@@ -1,7 +1,7 @@
1{-# LANGUAGE PatternGuards #-}
1{-# LANGUAGE PatternGuards #-}
2module IRTS.CodegenJava (codegenJava) where
2module IRTS.CodegenJava (codegenJava) where
3
3
4−import Core.TT hiding (mkApp)
4+import Idris.Core.TT hiding (mkApp)
5import IRTS.CodegenCommon
5import IRTS.CodegenCommon
6import IRTS.Java.ASTBuilding
6import IRTS.Java.ASTBuilding
7import IRTS.Java.JTypes
7import IRTS.Java.JTypes
src/IRTS/CodegenJavaScript.hs+1−1
@@ -7,7 +7,7 @@ import IRTS.Bytecode
7import IRTS.Lang
7import IRTS.Lang
8import IRTS.Simplified
8import IRTS.Simplified
9import IRTS.CodegenCommon
9import IRTS.CodegenCommon
10−import Core.TT
10+import Idris.Core.TT
11import Paths_idris
11import Paths_idris
12import Util.System
12import Util.System
13
13
src/IRTS/CodegenLLVM.hs+2−2
@@ -4,8 +4,8 @@ module IRTS.CodegenLLVM (codegenLLVM) where
4import IRTS.CodegenCommon
4import IRTS.CodegenCommon
5import IRTS.Lang
5import IRTS.Lang
6import IRTS.Simplified
6import IRTS.Simplified
7−import qualified Core.TT as TT
7+import qualified Idris.Core.TT as TT
8−import Core.TT (ArithTy(..), IntTy(..), NativeTy(..), nativeTyWidth)
8+import Idris.Core.TT (ArithTy(..), IntTy(..), NativeTy(..), nativeTyWidth)
9
9
10import Util.System
10import Util.System
11import Paths_idris
11import Paths_idris
src/IRTS/Compiler.hs+3−3
@@ -21,9 +21,9 @@ import Idris.AbsSyntax
21import Idris.UnusedArgs
21import Idris.UnusedArgs
22import Idris.Error
22import Idris.Error
23
23
24−import Core.TT
24+import Idris.Core.TT
25−import Core.Evaluate
25+import Idris.Core.Evaluate
26−import Core.CaseTree
26+import Idris.Core.CaseTree
27
27
28import Control.Monad.State
28import Control.Monad.State
29import Data.List
29import Data.List
src/IRTS/Defunctionalise.hs+1−1
@@ -2,7 +2,7 @@ module IRTS.Defunctionalise(module IRTS.Defunctionalise,
2 module IRTS.Lang) where
2 module IRTS.Lang) where
3
3
4import IRTS.Lang
4import IRTS.Lang
5−import Core.TT
5+import Idris.Core.TT
6
6
7import Debug.Trace
7import Debug.Trace
8import Data.Maybe
8import Data.Maybe
src/IRTS/DumpBC.hs+1−1
@@ -2,7 +2,7 @@ module IRTS.DumpBC where
2
2
3import IRTS.Lang
3import IRTS.Lang
4import IRTS.Simplified
4import IRTS.Simplified
5−import Core.TT
5+import Idris.Core.TT
6
6
7import IRTS.Bytecode
7import IRTS.Bytecode
8import Data.List
8import Data.List
src/IRTS/Inliner.hs+1−1
@@ -1,6 +1,6 @@
1module IRTS.Inliner where
1module IRTS.Inliner where
2
2
3−import Core.TT
3+import Idris.Core.TT
4
4
5import IRTS.Defunctionalise
5import IRTS.Defunctionalise
6
6
src/IRTS/Java/JTypes.hs+1−1
@@ -1,7 +1,7 @@
1{-# LANGUAGE PatternGuards #-}
1{-# LANGUAGE PatternGuards #-}
2module IRTS.Java.JTypes where
2module IRTS.Java.JTypes where
3
3
4−import Core.TT
4+import Idris.Core.TT
5import IRTS.Lang
5import IRTS.Lang
6import Language.Java.Syntax
6import Language.Java.Syntax
7import qualified Language.Java.Syntax as J
7import qualified Language.Java.Syntax as J
src/IRTS/Java/Mangling.hs+1−1
@@ -3,7 +3,7 @@
3
3
4module IRTS.Java.Mangling where
4module IRTS.Java.Mangling where
5
5
6−import Core.TT
6+import Idris.Core.TT
7import IRTS.Lang
7import IRTS.Lang
8import IRTS.Simplified
8import IRTS.Simplified
9
9
src/IRTS/Lang.hs+1−1
@@ -1,7 +1,7 @@
1module IRTS.Lang where
1module IRTS.Lang where
2
2
3import Control.Monad.State hiding (lift)
3import Control.Monad.State hiding (lift)
4−import Core.TT
4+import Idris.Core.TT
5import Data.List
5import Data.List
6import Debug.Trace
6import Debug.Trace
7
7
src/IRTS/Simplified.hs+1−1
@@ -1,7 +1,7 @@
1module IRTS.Simplified where
1module IRTS.Simplified where
2
2
3import IRTS.Defunctionalise
3import IRTS.Defunctionalise
4−import Core.TT
4+import Idris.Core.TT
5import Data.Maybe
5import Data.Maybe
6import Control.Monad.State
6import Control.Monad.State
7
7
src/Idris/AbsSyntax.hs+4−4
@@ -3,10 +3,10 @@
3
3
4module Idris.AbsSyntax(module Idris.AbsSyntax, module Idris.AbsSyntaxTree) where
4module Idris.AbsSyntax(module Idris.AbsSyntax, module Idris.AbsSyntaxTree) where
5
5
6−import Core.TT
6+import Idris.Core.TT
7−import Core.Evaluate
7+import Idris.Core.Evaluate
8−import Core.Elaborate hiding (Tactic(..))
8+import Idris.Core.Elaborate hiding (Tactic(..))
9−import Core.Typecheck
9+import Idris.Core.Typecheck
10import Idris.AbsSyntaxTree
10import Idris.AbsSyntaxTree
11import Idris.Colours
11import Idris.Colours
12import Idris.IdeSlave
12import Idris.IdeSlave
src/Idris/AbsSyntaxTree.hs+4−4
@@ -3,10 +3,10 @@
3
3
4module Idris.AbsSyntaxTree where
4module Idris.AbsSyntaxTree where
5
5
6−import Core.TT
6+import Idris.Core.TT
7−import Core.Evaluate
7+import Idris.Core.Evaluate
8−import Core.Elaborate hiding (Tactic(..))
8+import Idris.Core.Elaborate hiding (Tactic(..))
9−import Core.Typecheck
9+import Idris.Core.Typecheck
10import IRTS.Lang
10import IRTS.Lang
11import IRTS.CodegenCommon
11import IRTS.CodegenCommon
12import Util.Pretty
12import Util.Pretty
src/Idris/CaseSplit.hs+3−3
@@ -14,9 +14,9 @@ import Idris.Delaborate
14import Idris.Parser
14import Idris.Parser
15import Idris.Error
15import Idris.Error
16
16
17−import Core.TT
17+import Idris.Core.TT
18−import Core.Typecheck
18+import Idris.Core.Typecheck
19−import Core.Evaluate
19+import Idris.Core.Evaluate
20
20
21import Data.Maybe
21import Data.Maybe
22import Data.Char
22import Data.Char
src/Idris/Completion.hs+2−2
@@ -1,8 +1,8 @@
1-- | Support for command-line completion at the REPL and in the prover
1-- | Support for command-line completion at the REPL and in the prover
2module Idris.Completion (replCompletion, proverCompletion) where
2module Idris.Completion (replCompletion, proverCompletion) where
3
3
4−import Core.Evaluate (ctxtAlist)
4+import Idris.Core.Evaluate (ctxtAlist)
5−import Core.TT
5+import Idris.Core.TT
6
6
7import Idris.AbsSyntaxTree
7import Idris.AbsSyntaxTree
8import Idris.Help
8import Idris.Help
src/Core/CaseTree.hs → src/Idris/Core/CaseTree.hsrenamed+2−2
@@ -1,10 +1,10 @@
1{-# LANGUAGE PatternGuards, DeriveFunctor, TypeSynonymInstances #-}
1{-# LANGUAGE PatternGuards, DeriveFunctor, TypeSynonymInstances #-}
2
2
3−module Core.CaseTree(CaseDef(..), SC, SC'(..), CaseAlt, CaseAlt'(..),
3+module Idris.Core.CaseTree(CaseDef(..), SC, SC'(..), CaseAlt, CaseAlt'(..),
4 Phase(..), CaseTree,
4 Phase(..), CaseTree,
5 simpleCase, small, namesUsed, findCalls, findUsedArgs) where
5 simpleCase, small, namesUsed, findCalls, findUsedArgs) where
6
6
7−import Core.TT
7+import Idris.Core.TT
8
8
9import Control.Monad.State
9import Control.Monad.State
10import Data.Maybe
10import Data.Maybe
src/Core/Constraints.hs → src/Idris/Core/Constraints.hsrenamed+2−2
@@ -1,7 +1,7 @@
1-- | Check universe constraints.
1-- | Check universe constraints.
2−module Core.Constraints(ucheck) where
2+module Idris.Core.Constraints(ucheck) where
3
3
4−import Core.TT
4+import Idris.Core.TT
5
5
6import Control.Applicative
6import Control.Applicative
7import Control.Arrow
7import Control.Arrow
src/Core/Elaborate.hs → src/Idris/Core/Elaborate.hsrenamed+8−8
@@ -8,14 +8,14 @@
8 tactics out of the primitives.
8 tactics out of the primitives.
9-}
9-}
10
10
11−module Core.Elaborate(module Core.Elaborate,
11+module Idris.Core.Elaborate(module Idris.Core.Elaborate,
12− module Core.ProofState) where
12+ module Idris.Core.ProofState) where
13−
13+
14−import Core.ProofState
14+import Idris.Core.ProofState
15−import Core.TT
15+import Idris.Core.TT
16−import Core.Evaluate
16+import Idris.Core.Evaluate
17−import Core.Typecheck
17+import Idris.Core.Typecheck
18−import Core.Unify
18+import Idris.Core.Unify
19
19
20import Control.Monad.State
20import Control.Monad.State
21import Data.Char
21import Data.Char
src/Core/Evaluate.hs → src/Idris/Core/Evaluate.hsrenamed+3−3
@@ -1,7 +1,7 @@
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances,
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances,
2 PatternGuards #-}
2 PatternGuards #-}
3
3
4−module Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,
4+module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,
5 rt_simplify, simplify, specialise, hnf, convEq, convEq',
5 rt_simplify, simplify, specialise, hnf, convEq, convEq',
6 Def(..), CaseInfo(..), CaseDefs(..),
6 Def(..), CaseInfo(..), CaseDefs(..),
7 Accessibility(..), Totality(..), PReason(..),
7 Accessibility(..), Totality(..), PReason(..),
@@ -17,8 +17,8 @@ import Control.Monad.State
17import qualified Data.Binary as B
17import qualified Data.Binary as B
18import Data.Binary hiding (get, put)
18import Data.Binary hiding (get, put)
19
19
20−import Core.TT
20+import Idris.Core.TT
21−import Core.CaseTree
21+import Idris.Core.CaseTree
22
22
23data EvalState = ES { limited :: [(Name, Int)],
23data EvalState = ES { limited :: [(Name, Int)],
24 nexthole :: Int }
24 nexthole :: Int }
src/Core/Execute.hs → src/Idris/Core/Execute.hsrenamed+4−4
@@ -1,5 +1,5 @@
1{-# LANGUAGE PatternGuards, ExistentialQuantification, CPP #-}
1{-# LANGUAGE PatternGuards, ExistentialQuantification, CPP #-}
2−module Core.Execute (execute) where
2+module Idris.Core.Execute (execute) where
3
3
4import Idris.AbsSyntax
4import Idris.AbsSyntax
5import Idris.AbsSyntaxTree
5import Idris.AbsSyntaxTree
@@ -7,9 +7,9 @@ import IRTS.Lang(FType(..))
7
7
8import Idris.Primitives(Prim(..), primitives)
8import Idris.Primitives(Prim(..), primitives)
9
9
10−import Core.TT
10+import Idris.Core.TT
11−import Core.Evaluate
11+import Idris.Core.Evaluate
12−import Core.CaseTree
12+import Idris.Core.CaseTree
13
13
14import Debug.Trace
14import Debug.Trace
15
15
src/Core/ProofState.hs → src/Idris/Core/ProofState.hsrenamed+6−6
@@ -4,14 +4,14 @@
4 proofs, and some high level commands for introducing new theorems,
4 proofs, and some high level commands for introducing new theorems,
5 evaluation/checking inside the proof system, etc. --}
5 evaluation/checking inside the proof system, etc. --}
6
6
7−module Core.ProofState(ProofState(..), newProof, envAtFocus, goalAtFocus,
7+module Idris.Core.ProofState(ProofState(..), newProof, envAtFocus, goalAtFocus,
8 Tactic(..), Goal(..), processTactic,
8 Tactic(..), Goal(..), processTactic,
9 dropGiven, keepGiven) where
9 dropGiven, keepGiven) where
10
10
11−import Core.Typecheck
11+import Idris.Core.Typecheck
12−import Core.Evaluate
12+import Idris.Core.Evaluate
13−import Core.TT
13+import Idris.Core.TT
14−import Core.Unify
14+import Idris.Core.Unify
15
15
16import Control.Monad.State
16import Control.Monad.State
17import Control.Applicative hiding (empty)
17import Control.Applicative hiding (empty)
@@ -811,7 +811,7 @@ process t h = tactic (Just h) (mktac t)
811 mktac Solve = solve
811 mktac Solve = solve
812 mktac (StartUnify n) = start_unify n
812 mktac (StartUnify n) = start_unify n
813 mktac Compute = compute
813 mktac Compute = compute
814− mktac Simplify = Core.ProofState.simplify
814+ mktac Simplify = Idris.Core.ProofState.simplify
815 mktac HNF_Compute = hnf_compute
815 mktac HNF_Compute = hnf_compute
816 mktac (Intro n) = intro n
816 mktac (Intro n) = intro n
817 mktac (IntroTy ty n) = introTy ty n
817 mktac (IntroTy ty n) = introTy ty n
src/Core/TT.hs → src/Idris/Core/TT.hsrenamed+1−1
@@ -18,7 +18,7 @@
18 programs with implicit syntax into fully explicit terms.
18 programs with implicit syntax into fully explicit terms.
19-}
19-}
20
20
21−module Core.TT where
21+module Idris.Core.TT where
22
22
23import Control.Monad.State
23import Control.Monad.State
24import Control.Monad.Trans.Error (Error(..))
24import Control.Monad.Trans.Error (Error(..))
src/Core/Typecheck.hs → src/Idris/Core/Typecheck.hsrenamed+3−3
@@ -1,14 +1,14 @@
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,
2 PatternGuards #-}
2 PatternGuards #-}
3
3
4−module Core.Typecheck where
4+module Idris.Core.Typecheck where
5
5
6import Control.Monad.State
6import Control.Monad.State
7import Debug.Trace
7import Debug.Trace
8import qualified Data.Vector.Unboxed as V (length)
8import qualified Data.Vector.Unboxed as V (length)
9
9
10−import Core.TT
10+import Idris.Core.TT
11−import Core.Evaluate
11+import Idris.Core.Evaluate
12
12
13-- To check conversion, normalise each term wrt the current environment.
13-- To check conversion, normalise each term wrt the current environment.
14-- Since we haven't converted everything to de Bruijn indices yet, we'll have to
14-- Since we haven't converted everything to de Bruijn indices yet, we'll have to
src/Core/Unify.hs → src/Idris/Core/Unify.hsrenamed+3−3
@@ -1,9 +1,9 @@
1{-# LANGUAGE PatternGuards #-}
1{-# LANGUAGE PatternGuards #-}
2
2
3−module Core.Unify(match_unify, unify, Fails) where
3+module Idris.Core.Unify(match_unify, unify, Fails) where
4
4
5−import Core.TT
5+import Idris.Core.TT
6−import Core.Evaluate
6+import Idris.Core.Evaluate
7
7
8import Control.Monad
8import Control.Monad
9import Control.Monad.State
9import Control.Monad.State
src/Idris/Coverage.hs+3−3
@@ -2,9 +2,9 @@
2
2
3module Idris.Coverage where
3module Idris.Coverage where
4
4
5−import Core.TT
5+import Idris.Core.TT
6−import Core.Evaluate
6+import Idris.Core.Evaluate
7−import Core.CaseTree
7+import Idris.Core.CaseTree
8
8
9import Idris.AbsSyntax
9import Idris.AbsSyntax
10import Idris.Delaborate
10import Idris.Delaborate
src/Idris/DSL.hs+2−2
@@ -5,8 +5,8 @@ module Idris.DSL where
5import Idris.AbsSyntax
5import Idris.AbsSyntax
6import Paths_idris
6import Paths_idris
7
7
8−import Core.TT
8+import Idris.Core.TT
9−import Core.Evaluate
9+import Idris.Core.Evaluate
10
10
11import Control.Monad.State
11import Control.Monad.State
12import Debug.Trace
12import Debug.Trace
src/Idris/DataOpts.hs+1−1
@@ -5,7 +5,7 @@ module Idris.DataOpts where
5-- Forcing, detagging and collapsing
5-- Forcing, detagging and collapsing
6
6
7import Idris.AbsSyntax
7import Idris.AbsSyntax
8−import Core.TT
8+import Idris.Core.TT
9
9
10import Data.List
10import Data.List
11import Data.Maybe
11import Data.Maybe
src/Idris/DeepSeq.hs+1−1
@@ -1,6 +1,6 @@
1module Idris.DeepSeq where
1module Idris.DeepSeq where
2
2
3−import Core.TT
3+import Idris.Core.TT
4import Idris.AbsSyntax
4import Idris.AbsSyntax
5
5
6import Control.DeepSeq
6import Control.DeepSeq
src/Idris/Delaborate.hs+2−2
@@ -6,8 +6,8 @@ module Idris.Delaborate where
6-- purposes.
6-- purposes.
7
7
8import Idris.AbsSyntax
8import Idris.AbsSyntax
9−import Core.TT
9+import Idris.Core.TT
10−import Core.Evaluate
10+import Idris.Core.Evaluate
11
11
12import Debug.Trace
12import Debug.Trace
13
13
src/Idris/Docs.hs+2−2
@@ -3,8 +3,8 @@ module Idris.Docs where
3import Idris.AbsSyntax
3import Idris.AbsSyntax
4import Idris.AbsSyntaxTree
4import Idris.AbsSyntaxTree
5import Idris.Delaborate
5import Idris.Delaborate
6−import Core.TT
6+import Idris.Core.TT
7−import Core.Evaluate
7+import Idris.Core.Evaluate
8
8
9import Data.Maybe
9import Data.Maybe
10import Data.List
10import Data.List
src/Idris/ElabDecls.hs+6−6
@@ -19,12 +19,12 @@ import Idris.DeepSeq
19import IRTS.Lang
19import IRTS.Lang
20import Paths_idris
20import Paths_idris
21
21
22−import Core.TT
22+import Idris.Core.TT
23−import Core.Elaborate hiding (Tactic(..))
23+import Idris.Core.Elaborate hiding (Tactic(..))
24−import Core.Evaluate
24+import Idris.Core.Evaluate
25−import Core.Execute
25+import Idris.Core.Execute
26−import Core.Typecheck
26+import Idris.Core.Typecheck
27−import Core.CaseTree
27+import Idris.Core.CaseTree
28
28
29import Control.DeepSeq
29import Control.DeepSeq
30import Control.Monad
30import Control.Monad
src/Idris/ElabTerm.hs+3−3
@@ -7,9 +7,9 @@ import Idris.DSL
7import Idris.Delaborate
7import Idris.Delaborate
8import Idris.ProofSearch
8import Idris.ProofSearch
9
9
10−import Core.Elaborate hiding (Tactic(..))
10+import Idris.Core.Elaborate hiding (Tactic(..))
11−import Core.TT
11+import Idris.Core.TT
12−import Core.Evaluate
12+import Idris.Core.Evaluate
13
13
14import Control.Monad
14import Control.Monad
15import Control.Monad.State
15import Control.Monad.State
src/Idris/Error.hs+3−3
@@ -6,9 +6,9 @@ import Prelude hiding (catch)
6import Idris.AbsSyntax
6import Idris.AbsSyntax
7import Idris.Delaborate
7import Idris.Delaborate
8
8
9−import Core.TT
9+import Idris.Core.TT
10−import Core.Typecheck
10+import Idris.Core.Typecheck
11−import Core.Constraints
11+import Idris.Core.Constraints
12
12
13import System.Console.Haskeline
13import System.Console.Haskeline
14import System.Console.Haskeline.MonadException
14import System.Console.Haskeline.MonadException
src/Idris/IBC.hs+3−3
@@ -2,9 +2,9 @@
2
2
3module Idris.IBC where
3module Idris.IBC where
4
4
5−import Core.Evaluate
5+import Idris.Core.Evaluate
6−import Core.TT
6+import Idris.Core.TT
7−import Core.CaseTree
7+import Idris.Core.CaseTree
8import Idris.AbsSyntax
8import Idris.AbsSyntax
9import Idris.Imports
9import Idris.Imports
10import Idris.Error
10import Idris.Error
src/Idris/IdeSlave.hs+1−1
@@ -10,7 +10,7 @@ import qualified Data.ByteString.UTF8 as UTF8
10import Text.Trifecta hiding (Err)
10import Text.Trifecta hiding (Err)
11import Text.Trifecta.Delta
11import Text.Trifecta.Delta
12
12
13−import Core.TT
13+import Idris.Core.TT
14
14
15import Control.Applicative
15import Control.Applicative
16
16
src/Idris/Imports.hs+1−1
@@ -2,7 +2,7 @@ module Idris.Imports where
2
2
3import Idris.AbsSyntax
3import Idris.AbsSyntax
4
4
5−import Core.TT
5+import Idris.Core.TT
6import Paths_idris
6import Paths_idris
7
7
8import System.FilePath
8import System.FilePath
src/Idris/Inliner.hs+1−1
@@ -2,7 +2,7 @@
2
2
3module Idris.Inliner where
3module Idris.Inliner where
4
4
5−import Core.TT
5+import Idris.Core.TT
6import Idris.AbsSyntax
6import Idris.AbsSyntax
7
7
8inlineDef :: IState -> [([Name], Term, Term)] -> [([Name], Term, Term)]
8inlineDef :: IState -> [([Name], Term, Term)] -> [([Name], Term, Term)]
src/Idris/ParseData.hs+2−2
@@ -17,8 +17,8 @@ import Idris.ParseOps
17import Idris.ParseExpr
17import Idris.ParseExpr
18import Idris.DSL
18import Idris.DSL
19
19
20−import Core.TT
20+import Idris.Core.TT
21−import Core.Evaluate
21+import Idris.Core.Evaluate
22
22
23import Control.Applicative
23import Control.Applicative
24import Control.Monad
24import Control.Monad
src/Idris/ParseExpr.hs+2−2
@@ -16,7 +16,7 @@ import Idris.ParseHelpers
16import Idris.ParseOps
16import Idris.ParseOps
17import Idris.DSL
17import Idris.DSL
18
18
19−import Core.TT
19+import Idris.Core.TT
20
20
21import Control.Applicative
21import Control.Applicative
22import Control.Monad
22import Control.Monad
@@ -907,7 +907,7 @@ Constant ::=
907 | Char_t
907 | Char_t
908 ;
908 ;
909-}
909-}
910−constant :: IdrisParser Core.TT.Const
910+constant :: IdrisParser Idris.Core.TT.Const
911constant = do reserved "Integer";return (AType (ATInt ITBig))
911constant = do reserved "Integer";return (AType (ATInt ITBig))
912 <|> do reserved "Int"; return (AType (ATInt ITNative))
912 <|> do reserved "Int"; return (AType (ATInt ITNative))
913 <|> do reserved "Char"; return (AType (ATInt ITChar))
913 <|> do reserved "Char"; return (AType (ATInt ITChar))
src/Idris/ParseHelpers.hs+2−2
@@ -13,8 +13,8 @@ import qualified Text.Parser.Token.Highlight as Hi
13
13
14import Idris.AbsSyntax
14import Idris.AbsSyntax
15
15
16−import Core.TT
16+import Idris.Core.TT
17−import Core.Evaluate
17+import Idris.Core.Evaluate
18
18
19import Control.Applicative
19import Control.Applicative
20import Control.Monad
20import Control.Monad
src/Idris/ParseOps.hs+1−1
@@ -14,7 +14,7 @@ import qualified Text.Parser.Token.Highlight as Hi
14import Idris.AbsSyntax
14import Idris.AbsSyntax
15import Idris.ParseHelpers
15import Idris.ParseHelpers
16
16
17−import Core.TT
17+import Idris.Core.TT
18
18
19import Control.Applicative
19import Control.Applicative
20import Control.Monad
20import Control.Monad
src/Idris/Parser.hs+2−2
@@ -37,8 +37,8 @@ import Paths_idris
37
37
38import Util.DynamicLinker
38import Util.DynamicLinker
39
39
40−import Core.TT
40+import Idris.Core.TT
41−import Core.Evaluate
41+import Idris.Core.Evaluate
42
42
43import Control.Applicative
43import Control.Applicative
44import Control.Monad
44import Control.Monad
src/Idris/PartialEval.hs+2−2
@@ -6,8 +6,8 @@ module Idris.PartialEval(partial_eval, getSpecApps, specType,
6import Idris.AbsSyntax
6import Idris.AbsSyntax
7import Idris.Delaborate
7import Idris.Delaborate
8
8
9−import Core.TT
9+import Idris.Core.TT
10−import Core.Evaluate
10+import Idris.Core.Evaluate
11
11
12import Debug.Trace
12import Debug.Trace
13
13
src/Idris/Primitives.hs+2−2
@@ -6,8 +6,8 @@ import Idris.AbsSyntax
6
6
7import IRTS.Lang
7import IRTS.Lang
8
8
9−import Core.TT
9+import Idris.Core.TT
10−import Core.Evaluate
10+import Idris.Core.Evaluate
11import Data.Bits
11import Data.Bits
12import Data.Word
12import Data.Word
13import Data.Int
13import Data.Int
src/Idris/ProofSearch.hs+5−5
@@ -1,10 +1,10 @@
1module Idris.ProofSearch(trivial, proofSearch) where
1module Idris.ProofSearch(trivial, proofSearch) where
2
2
3−import Core.Elaborate hiding (Tactic(..))
3+import Idris.Core.Elaborate hiding (Tactic(..))
4−import Core.TT
4+import Idris.Core.TT
5−import Core.Evaluate
5+import Idris.Core.Evaluate
6−import Core.CaseTree
6+import Idris.Core.CaseTree
7−import Core.Typecheck
7+import Idris.Core.Typecheck
8
8
9import Idris.AbsSyntax
9import Idris.AbsSyntax
10import Idris.Delaborate
10import Idris.Delaborate
src/Idris/Prover.hs+5−5
@@ -1,10 +1,10 @@
1module Idris.Prover where
1module Idris.Prover where
2
2
3−import Core.Elaborate hiding (Tactic(..))
3+import Idris.Core.Elaborate hiding (Tactic(..))
4−import Core.TT
4+import Idris.Core.TT
5−import Core.Evaluate
5+import Idris.Core.Evaluate
6−import Core.CaseTree
6+import Idris.Core.CaseTree
7−import Core.Typecheck
7+import Idris.Core.Typecheck
8
8
9import Idris.AbsSyntax
9import Idris.AbsSyntax
10import Idris.Delaborate
10import Idris.Delaborate
src/Idris/Providers.hs+2−2
@@ -1,8 +1,8 @@
1{-# LANGUAGE PatternGuards #-}
1{-# LANGUAGE PatternGuards #-}
2module Idris.Providers (providerTy, getProvided) where
2module Idris.Providers (providerTy, getProvided) where
3
3
4−import Core.TT
4+import Idris.Core.TT
5−import Core.Evaluate
5+import Idris.Core.Evaluate
6import Idris.AbsSyntax
6import Idris.AbsSyntax
7import Idris.AbsSyntaxTree
7import Idris.AbsSyntaxTree
8import Idris.Error
8import Idris.Error
src/Idris/REPL.hs+4−4
@@ -30,10 +30,10 @@ import Util.System
30import Util.DynamicLinker
30import Util.DynamicLinker
31import Util.Net (listenOnLocalhost)
31import Util.Net (listenOnLocalhost)
32
32
33−import Core.Evaluate
33+import Idris.Core.Evaluate
34−import Core.Execute (execute)
34+import Idris.Core.Execute (execute)
35−import Core.TT
35+import Idris.Core.TT
36−import Core.Constraints
36+import Idris.Core.Constraints
37
37
38import IRTS.Compiler
38import IRTS.Compiler
39import IRTS.CodegenCommon
39import IRTS.CodegenCommon
src/Idris/REPLParser.hs+1−1
@@ -5,7 +5,7 @@ import System.Console.ANSI (Color(..))
5
5
6import Idris.Colours
6import Idris.Colours
7import Idris.AbsSyntax
7import Idris.AbsSyntax
8−import Core.TT
8+import Idris.Core.TT
9import qualified Idris.Parser as P
9import qualified Idris.Parser as P
10
10
11import Control.Applicative
11import Control.Applicative
src/Idris/Transforms.hs+2−2
@@ -3,8 +3,8 @@
3module Idris.Transforms where
3module Idris.Transforms where
4
4
5import Idris.AbsSyntax
5import Idris.AbsSyntax
6−import Core.CaseTree
6+import Idris.Core.CaseTree
7−import Core.TT
7+import Idris.Core.TT
8
8
9data TTOpt = TermTrans (TT Name -> TT Name) -- term transform
9data TTOpt = TermTrans (TT Name -> TT Name) -- term transform
10 | CaseTrans (SC -> SC) -- case expression transform
10 | CaseTrans (SC -> SC) -- case expression transform
src/Idris/Unlit.hs+1−1
@@ -1,6 +1,6 @@
1module Idris.Unlit(unlit) where
1module Idris.Unlit(unlit) where
2
2
3−import Core.TT
3+import Idris.Core.TT
4import Data.Char
4import Data.Char
5
5
6unlit :: FilePath -> String -> TC String
6unlit :: FilePath -> String -> TC String
src/Idris/UnusedArgs.hs+2−2
@@ -2,8 +2,8 @@ module Idris.UnusedArgs where
2
2
3import Idris.AbsSyntax
3import Idris.AbsSyntax
4
4
5−import Core.CaseTree
5+import Idris.Core.CaseTree
6−import Core.TT
6+import Idris.Core.TT
7
7
8import Control.Monad.State
8import Control.Monad.State
9import Data.Maybe
9import Data.Maybe
src/Main.hs+4−4
@@ -12,10 +12,10 @@ import Control.Monad.Trans.Error ( ErrorT(..) )
12import Control.Monad.Trans.State.Strict ( execStateT, get, put )
12import Control.Monad.Trans.State.Strict ( execStateT, get, put )
13import Control.Monad ( when )
13import Control.Monad ( when )
14
14
15−import Core.TT
15+import Idris.Core.TT
16−import Core.Typecheck
16+import Idris.Core.Typecheck
17−import Core.Evaluate
17+import Idris.Core.Evaluate
18−import Core.Constraints
18+import Idris.Core.Constraints
19
19
20import Idris.AbsSyntax
20import Idris.AbsSyntax
21import Idris.Parser
21import Idris.Parser
src/Pkg/PParser.hs+1−1
@@ -2,7 +2,7 @@ module Pkg.PParser where
2
2
3import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace)
3import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace)
4
4
5−import Core.TT
5+import Idris.Core.TT
6import Idris.REPL
6import Idris.REPL
7import Idris.AbsSyntaxTree
7import Idris.AbsSyntaxTree
8import Idris.ParseHelpers
8import Idris.ParseHelpers
src/Pkg/Package.hs+1−1
@@ -14,7 +14,7 @@ import Control.Monad
14import Data.List
14import Data.List
15import Data.List.Split(splitOn)
15import Data.List.Split(splitOn)
16
16
17−import Core.TT
17+import Idris.Core.TT
18import Idris.REPL
18import Idris.REPL
19import Idris.AbsSyntax
19import Idris.AbsSyntax
20
20
src/Util/LLVMStubs.hs+1−1
@@ -7,7 +7,7 @@ Replaces stuff from LLVM.General.Target and IRTS.CodegenLLVM.
7
7
8module Util.LLVMStubs where
8module Util.LLVMStubs where
9
9
10−import qualified Core.TT as TT
10+import qualified Idris.Core.TT as TT
11import IRTS.Simplified
11import IRTS.Simplified
12import IRTS.CodegenCommon
12import IRTS.CodegenCommon
13
13