5000aeb · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add a Cabal library

Moves Core to Idris.Core The library allows using the Idris' backend from other Haskell code. For example, we could use Idris as a general TT compiler with multiple backends: run :: Idris () run = do let ddir = "libs" -- TODO: Use Idris.Util addImportDir $ ddir </> "prelude" addImportDir $ ddir </> "base" elabPrims _ <- loadModule stdout "Builtins" _ <- loadModule stdout "Prelude" pterm <- fmap (flip delab program) getIState elabDecls toplevel [makeDecl pterm] compile ViaNode "wow.js" runProgram Everything but Main, Util, Pkg and Paths_idris is currently exported.

commit5000aeb2560393a1f3c5f16b0795d5b7dd14bb8d authorBrian McKenna <brian@brianmckenna.org> dateFri 29 Nov 2013, 10:07 (13 years ago) parentc459480

61 files changed+252−143

compare with master

unifiedsplit

idris.cabal+118−9

@@ -301,19 +301,128 @@ Flag FFI

301301 Default: False

302302 manual: True

303303

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+

304413Executable idris

305414 Main-is: Main.hs

306415 hs-source-dirs: src

307416 Other-modules:

308− Core.CaseTree

309− , Core.Constraints

310− , Core.Elaborate

311− , Core.Evaluate

312− , Core.Execute

313− , Core.ProofState

314− , Core.TT

315− , Core.Typecheck

316− , Core.Unify

417+ Idris.Core.CaseTree

418+ , Idris.Core.Constraints

419+ , Idris.Core.Elaborate

420+ , Idris.Core.Evaluate

421+ , Idris.Core.Execute

422+ , Idris.Core.ProofState

423+ , Idris.Core.TT

424+ , Idris.Core.Typecheck

425+ , Idris.Core.Unify

317426

318427 , Idris.AbsSyntax

319428 , Idris.AbsSyntaxTree

src/IRTS/BCImp.hs+1−1

@@ -5,7 +5,7 @@ module IRTS.BCImp where

66import IRTS.Lang

77import IRTS.Simplified

8−import Core.TT

8+import Idris.Core.TT

1010data Reg = RVal | L Int

1111

src/IRTS/Bytecode.hs+1−1

@@ -5,7 +5,7 @@ module IRTS.Bytecode where

66import IRTS.Lang

77import IRTS.Simplified

8−import Core.TT

8+import Idris.Core.TT

99import Data.Maybe

1010

1111{- We have:

src/IRTS/CodegenC.hs+1−1

@@ -5,7 +5,7 @@ import IRTS.Bytecode

55import IRTS.Lang

66import IRTS.Simplified

77import IRTS.CodegenCommon

8−import Core.TT

8+import Idris.Core.TT

99import Paths_idris

1010import Util.System

1111

src/IRTS/CodegenCommon.hs+1−1

@@ -1,6 +1,6 @@

11module IRTS.CodegenCommon where

3−import Core.TT

3+import Idris.Core.TT

44import IRTS.Simplified

66import Control.Exception

src/IRTS/CodegenJava.hs+1−1

@@ -1,7 +1,7 @@

11{-# LANGUAGE PatternGuards #-}

22module IRTS.CodegenJava (codegenJava) where

4−import Core.TT hiding (mkApp)

4+import Idris.Core.TT hiding (mkApp)

55import IRTS.CodegenCommon

66import IRTS.Java.ASTBuilding

77import IRTS.Java.JTypes

src/IRTS/CodegenJavaScript.hs+1−1

@@ -7,7 +7,7 @@ import IRTS.Bytecode

77import IRTS.Lang

88import IRTS.Simplified

99import IRTS.CodegenCommon

10−import Core.TT

10+import Idris.Core.TT

1111import Paths_idris

1212import Util.System

1313

src/IRTS/CodegenLLVM.hs+2−2

@@ -4,8 +4,8 @@ module IRTS.CodegenLLVM (codegenLLVM) where

44import IRTS.CodegenCommon

55import IRTS.Lang

66import IRTS.Simplified

7−import qualified Core.TT as TT

8−import Core.TT (ArithTy(..), IntTy(..), NativeTy(..), nativeTyWidth)

7+import qualified Idris.Core.TT as TT

8+import Idris.Core.TT (ArithTy(..), IntTy(..), NativeTy(..), nativeTyWidth)

1010import Util.System

1111import Paths_idris

src/IRTS/Compiler.hs+3−3

@@ -21,9 +21,9 @@ import Idris.AbsSyntax

2121import Idris.UnusedArgs

2222import Idris.Error

2323

24−import Core.TT

25−import Core.Evaluate

26−import Core.CaseTree

24+import Idris.Core.TT

25+import Idris.Core.Evaluate

26+import Idris.Core.CaseTree

2727

2828import Control.Monad.State

2929import Data.List

src/IRTS/Defunctionalise.hs+1−1

@@ -2,7 +2,7 @@ module IRTS.Defunctionalise(module IRTS.Defunctionalise,

22 module IRTS.Lang) where

44import IRTS.Lang

5−import Core.TT

5+import Idris.Core.TT

77import Debug.Trace

88import Data.Maybe

src/IRTS/DumpBC.hs+1−1

@@ -2,7 +2,7 @@ module IRTS.DumpBC where

33import IRTS.Lang

44import IRTS.Simplified

5−import Core.TT

5+import Idris.Core.TT

77import IRTS.Bytecode

88import Data.List

src/IRTS/Inliner.hs+1−1

@@ -1,6 +1,6 @@

11module IRTS.Inliner where

3−import Core.TT

3+import Idris.Core.TT

55import IRTS.Defunctionalise

src/IRTS/Java/JTypes.hs+1−1

@@ -1,7 +1,7 @@

11{-# LANGUAGE PatternGuards #-}

22module IRTS.Java.JTypes where

4−import Core.TT

4+import Idris.Core.TT

55import IRTS.Lang

66import Language.Java.Syntax

77import qualified Language.Java.Syntax as J

src/IRTS/Java/Mangling.hs+1−1

@@ -3,7 +3,7 @@

44module IRTS.Java.Mangling where

6−import Core.TT

6+import Idris.Core.TT

77import IRTS.Lang

88import IRTS.Simplified

src/IRTS/Lang.hs+1−1

@@ -1,7 +1,7 @@

11module IRTS.Lang where

33import Control.Monad.State hiding (lift)

4−import Core.TT

4+import Idris.Core.TT

55import Data.List

66import Debug.Trace

src/IRTS/Simplified.hs+1−1

@@ -1,7 +1,7 @@

11module IRTS.Simplified where

33import IRTS.Defunctionalise

4−import Core.TT

4+import Idris.Core.TT

55import Data.Maybe

66import Control.Monad.State

src/Idris/AbsSyntax.hs+4−4

@@ -3,10 +3,10 @@

44module Idris.AbsSyntax(module Idris.AbsSyntax, module Idris.AbsSyntaxTree) where

6−import Core.TT

7−import Core.Evaluate

8−import Core.Elaborate hiding (Tactic(..))

9−import Core.Typecheck

6+import Idris.Core.TT

7+import Idris.Core.Evaluate

8+import Idris.Core.Elaborate hiding (Tactic(..))

9+import Idris.Core.Typecheck

1010import Idris.AbsSyntaxTree

1111import Idris.Colours

1212import Idris.IdeSlave

src/Idris/AbsSyntaxTree.hs+4−4

@@ -3,10 +3,10 @@

44module Idris.AbsSyntaxTree where

6−import Core.TT

7−import Core.Evaluate

8−import Core.Elaborate hiding (Tactic(..))

9−import Core.Typecheck

6+import Idris.Core.TT

7+import Idris.Core.Evaluate

8+import Idris.Core.Elaborate hiding (Tactic(..))

9+import Idris.Core.Typecheck

1010import IRTS.Lang

1111import IRTS.CodegenCommon

1212import Util.Pretty

src/Idris/CaseSplit.hs+3−3

@@ -14,9 +14,9 @@ import Idris.Delaborate

1414import Idris.Parser

1515import Idris.Error

1616

17−import Core.TT

18−import Core.Typecheck

19−import Core.Evaluate

17+import Idris.Core.TT

18+import Idris.Core.Typecheck

19+import Idris.Core.Evaluate

2020

2121import Data.Maybe

2222import Data.Char

src/Idris/Completion.hs+2−2

@@ -1,8 +1,8 @@

11-- | Support for command-line completion at the REPL and in the prover

22module Idris.Completion (replCompletion, proverCompletion) where

4−import Core.Evaluate (ctxtAlist)

5−import Core.TT

4+import Idris.Core.Evaluate (ctxtAlist)

5+import Idris.Core.TT

77import Idris.AbsSyntaxTree

88import Idris.Help

src/Core/CaseTree.hs → src/Idris/Core/CaseTree.hsrenamed+2−2

@@ -1,10 +1,10 @@

11{-# LANGUAGE PatternGuards, DeriveFunctor, TypeSynonymInstances #-}

3−module Core.CaseTree(CaseDef(..), SC, SC'(..), CaseAlt, CaseAlt'(..),

3+module Idris.Core.CaseTree(CaseDef(..), SC, SC'(..), CaseAlt, CaseAlt'(..),

44 Phase(..), CaseTree,

55 simpleCase, small, namesUsed, findCalls, findUsedArgs) where

7−import Core.TT

7+import Idris.Core.TT

99import Control.Monad.State

1010import Data.Maybe

src/Core/Constraints.hs → src/Idris/Core/Constraints.hsrenamed+2−2

@@ -1,7 +1,7 @@

11-- | Check universe constraints.

2−module Core.Constraints(ucheck) where

2+module Idris.Core.Constraints(ucheck) where

4−import Core.TT

4+import Idris.Core.TT

66import Control.Applicative

77import Control.Arrow

src/Core/Elaborate.hs → src/Idris/Core/Elaborate.hsrenamed+8−8

@@ -8,14 +8,14 @@

88 tactics out of the primitives.

99-}

1010

11−module Core.Elaborate(module Core.Elaborate,

12− module Core.ProofState) where

13−

14−import Core.ProofState

15−import Core.TT

16−import Core.Evaluate

17−import Core.Typecheck

18−import Core.Unify

11+module Idris.Core.Elaborate(module Idris.Core.Elaborate,

12+ module Idris.Core.ProofState) where

13+

14+import Idris.Core.ProofState

15+import Idris.Core.TT

16+import Idris.Core.Evaluate

17+import Idris.Core.Typecheck

18+import Idris.Core.Unify

1919

2020import Control.Monad.State

2121import Data.Char

src/Core/Evaluate.hs → src/Idris/Core/Evaluate.hsrenamed+3−3

@@ -1,7 +1,7 @@

11{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances,

22 PatternGuards #-}

4−module Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,

4+module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,

55 rt_simplify, simplify, specialise, hnf, convEq, convEq',

66 Def(..), CaseInfo(..), CaseDefs(..),

77 Accessibility(..), Totality(..), PReason(..),

@@ -17,8 +17,8 @@ import Control.Monad.State

1717import qualified Data.Binary as B

1818import Data.Binary hiding (get, put)

1919

20−import Core.TT

21−import Core.CaseTree

20+import Idris.Core.TT

21+import Idris.Core.CaseTree

2222

2323data EvalState = ES { limited :: [(Name, Int)],

2424 nexthole :: Int }

src/Core/Execute.hs → src/Idris/Core/Execute.hsrenamed+4−4

@@ -1,5 +1,5 @@

11{-# LANGUAGE PatternGuards, ExistentialQuantification, CPP #-}

2−module Core.Execute (execute) where

2+module Idris.Core.Execute (execute) where

44import Idris.AbsSyntax

55import Idris.AbsSyntaxTree

@@ -7,9 +7,9 @@ import IRTS.Lang(FType(..))

88import Idris.Primitives(Prim(..), primitives)

10−import Core.TT

11−import Core.Evaluate

12−import Core.CaseTree

10+import Idris.Core.TT

11+import Idris.Core.Evaluate

12+import Idris.Core.CaseTree

1313

1414import Debug.Trace

1515

src/Core/ProofState.hs → src/Idris/Core/ProofState.hsrenamed+6−6

@@ -4,14 +4,14 @@

44 proofs, and some high level commands for introducing new theorems,

55 evaluation/checking inside the proof system, etc. --}

7−module Core.ProofState(ProofState(..), newProof, envAtFocus, goalAtFocus,

7+module Idris.Core.ProofState(ProofState(..), newProof, envAtFocus, goalAtFocus,

88 Tactic(..), Goal(..), processTactic,

99 dropGiven, keepGiven) where

1010

11−import Core.Typecheck

12−import Core.Evaluate

13−import Core.TT

14−import Core.Unify

11+import Idris.Core.Typecheck

12+import Idris.Core.Evaluate

13+import Idris.Core.TT

14+import Idris.Core.Unify

1515

1616import Control.Monad.State

1717import Control.Applicative hiding (empty)

@@ -811,7 +811,7 @@ process t h = tactic (Just h) (mktac t)

811811 mktac Solve = solve

812812 mktac (StartUnify n) = start_unify n

813813 mktac Compute = compute

814− mktac Simplify = Core.ProofState.simplify

814+ mktac Simplify = Idris.Core.ProofState.simplify

815815 mktac HNF_Compute = hnf_compute

816816 mktac (Intro n) = intro n

817817 mktac (IntroTy ty n) = introTy ty n

src/Core/TT.hs → src/Idris/Core/TT.hsrenamed+1−1

@@ -18,7 +18,7 @@

1818 programs with implicit syntax into fully explicit terms.

1919-}

2020

21−module Core.TT where

21+module Idris.Core.TT where

2222

2323import Control.Monad.State

2424import Control.Monad.Trans.Error (Error(..))

src/Core/Typecheck.hs → src/Idris/Core/Typecheck.hsrenamed+3−3

@@ -1,14 +1,14 @@

11{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor,

22 PatternGuards #-}

4−module Core.Typecheck where

4+module Idris.Core.Typecheck where

66import Control.Monad.State

77import Debug.Trace

88import qualified Data.Vector.Unboxed as V (length)

10−import Core.TT

11−import Core.Evaluate

10+import Idris.Core.TT

11+import Idris.Core.Evaluate

1212

1313-- To check conversion, normalise each term wrt the current environment.

1414-- 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 @@

11{-# LANGUAGE PatternGuards #-}

3−module Core.Unify(match_unify, unify, Fails) where

3+module Idris.Core.Unify(match_unify, unify, Fails) where

5−import Core.TT

6−import Core.Evaluate

5+import Idris.Core.TT

6+import Idris.Core.Evaluate

88import Control.Monad

99import Control.Monad.State

src/Idris/Coverage.hs+3−3

@@ -2,9 +2,9 @@

33module Idris.Coverage where

5−import Core.TT

6−import Core.Evaluate

7−import Core.CaseTree

5+import Idris.Core.TT

6+import Idris.Core.Evaluate

7+import Idris.Core.CaseTree

99import Idris.AbsSyntax

1010import Idris.Delaborate

src/Idris/DSL.hs+2−2

@@ -5,8 +5,8 @@ module Idris.DSL where

55import Idris.AbsSyntax

66import Paths_idris

8−import Core.TT

9−import Core.Evaluate

8+import Idris.Core.TT

9+import Idris.Core.Evaluate

1010

1111import Control.Monad.State

1212import Debug.Trace

src/Idris/DataOpts.hs+1−1

@@ -5,7 +5,7 @@ module Idris.DataOpts where

55-- Forcing, detagging and collapsing

77import Idris.AbsSyntax

8−import Core.TT

8+import Idris.Core.TT

1010import Data.List

1111import Data.Maybe

src/Idris/DeepSeq.hs+1−1

@@ -1,6 +1,6 @@

11module Idris.DeepSeq where

3−import Core.TT

3+import Idris.Core.TT

44import Idris.AbsSyntax

66import Control.DeepSeq

src/Idris/Delaborate.hs+2−2

@@ -6,8 +6,8 @@ module Idris.Delaborate where

66-- purposes.

88import Idris.AbsSyntax

9−import Core.TT

10−import Core.Evaluate

9+import Idris.Core.TT

10+import Idris.Core.Evaluate

1111

1212import Debug.Trace

1313

src/Idris/Docs.hs+2−2

@@ -3,8 +3,8 @@ module Idris.Docs where

33import Idris.AbsSyntax

44import Idris.AbsSyntaxTree

55import Idris.Delaborate

6−import Core.TT

7−import Core.Evaluate

6+import Idris.Core.TT

7+import Idris.Core.Evaluate

99import Data.Maybe

1010import Data.List

src/Idris/ElabDecls.hs+6−6

@@ -19,12 +19,12 @@ import Idris.DeepSeq

1919import IRTS.Lang

2020import Paths_idris

2121

22−import Core.TT

23−import Core.Elaborate hiding (Tactic(..))

24−import Core.Evaluate

25−import Core.Execute

26−import Core.Typecheck

27−import Core.CaseTree

22+import Idris.Core.TT

23+import Idris.Core.Elaborate hiding (Tactic(..))

24+import Idris.Core.Evaluate

25+import Idris.Core.Execute

26+import Idris.Core.Typecheck

27+import Idris.Core.CaseTree

2828

2929import Control.DeepSeq

3030import Control.Monad

src/Idris/ElabTerm.hs+3−3

@@ -7,9 +7,9 @@ import Idris.DSL

77import Idris.Delaborate

88import Idris.ProofSearch

10−import Core.Elaborate hiding (Tactic(..))

11−import Core.TT

12−import Core.Evaluate

10+import Idris.Core.Elaborate hiding (Tactic(..))

11+import Idris.Core.TT

12+import Idris.Core.Evaluate

1313

1414import Control.Monad

1515import Control.Monad.State

src/Idris/Error.hs+3−3

@@ -6,9 +6,9 @@ import Prelude hiding (catch)

66import Idris.AbsSyntax

77import Idris.Delaborate

9−import Core.TT

10−import Core.Typecheck

11−import Core.Constraints

9+import Idris.Core.TT

10+import Idris.Core.Typecheck

11+import Idris.Core.Constraints

1212

1313import System.Console.Haskeline

1414import System.Console.Haskeline.MonadException

src/Idris/IBC.hs+3−3

@@ -2,9 +2,9 @@

33module Idris.IBC where

5−import Core.Evaluate

6−import Core.TT

7−import Core.CaseTree

5+import Idris.Core.Evaluate

6+import Idris.Core.TT

7+import Idris.Core.CaseTree

88import Idris.AbsSyntax

99import Idris.Imports

1010import Idris.Error

src/Idris/IdeSlave.hs+1−1

@@ -10,7 +10,7 @@ import qualified Data.ByteString.UTF8 as UTF8

1010import Text.Trifecta hiding (Err)

1111import Text.Trifecta.Delta

1212

13−import Core.TT

13+import Idris.Core.TT

1414

1515import Control.Applicative

1616

src/Idris/Imports.hs+1−1

@@ -2,7 +2,7 @@ module Idris.Imports where

33import Idris.AbsSyntax

5−import Core.TT

5+import Idris.Core.TT

66import Paths_idris

88import System.FilePath

src/Idris/Inliner.hs+1−1

@@ -2,7 +2,7 @@

33module Idris.Inliner where

5−import Core.TT

5+import Idris.Core.TT

66import Idris.AbsSyntax

88inlineDef :: IState -> [([Name], Term, Term)] -> [([Name], Term, Term)]

src/Idris/ParseData.hs+2−2

@@ -17,8 +17,8 @@ import Idris.ParseOps

1717import Idris.ParseExpr

1818import Idris.DSL

1919

20−import Core.TT

21−import Core.Evaluate

20+import Idris.Core.TT

21+import Idris.Core.Evaluate

2222

2323import Control.Applicative

2424import Control.Monad

src/Idris/ParseExpr.hs+2−2

@@ -16,7 +16,7 @@ import Idris.ParseHelpers

1616import Idris.ParseOps

1717import Idris.DSL

1818

19−import Core.TT

19+import Idris.Core.TT

2020

2121import Control.Applicative

2222import Control.Monad

@@ -907,7 +907,7 @@ Constant ::=

907907 | Char_t

908908 ;

909909-}

910−constant :: IdrisParser Core.TT.Const

910+constant :: IdrisParser Idris.Core.TT.Const

911911constant = do reserved "Integer";return (AType (ATInt ITBig))

912912 <|> do reserved "Int"; return (AType (ATInt ITNative))

913913 <|> 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

1313

1414import Idris.AbsSyntax

1515

16−import Core.TT

17−import Core.Evaluate

16+import Idris.Core.TT

17+import Idris.Core.Evaluate

1818

1919import Control.Applicative

2020import Control.Monad

src/Idris/ParseOps.hs+1−1

@@ -14,7 +14,7 @@ import qualified Text.Parser.Token.Highlight as Hi

1414import Idris.AbsSyntax

1515import Idris.ParseHelpers

1616

17−import Core.TT

17+import Idris.Core.TT

1818

1919import Control.Applicative

2020import Control.Monad

src/Idris/Parser.hs+2−2

@@ -37,8 +37,8 @@ import Paths_idris

3737

3838import Util.DynamicLinker

3939

40−import Core.TT

41−import Core.Evaluate

40+import Idris.Core.TT

41+import Idris.Core.Evaluate

4242

4343import Control.Applicative

4444import Control.Monad

src/Idris/PartialEval.hs+2−2

@@ -6,8 +6,8 @@ module Idris.PartialEval(partial_eval, getSpecApps, specType,

66import Idris.AbsSyntax

77import Idris.Delaborate

9−import Core.TT

10−import Core.Evaluate

9+import Idris.Core.TT

10+import Idris.Core.Evaluate

1111

1212import Debug.Trace

1313

src/Idris/Primitives.hs+2−2

@@ -6,8 +6,8 @@ import Idris.AbsSyntax

77import IRTS.Lang

9−import Core.TT

10−import Core.Evaluate

9+import Idris.Core.TT

10+import Idris.Core.Evaluate

1111import Data.Bits

1212import Data.Word

1313import Data.Int

src/Idris/ProofSearch.hs+5−5

@@ -1,10 +1,10 @@

11module Idris.ProofSearch(trivial, proofSearch) where

3−import Core.Elaborate hiding (Tactic(..))

4−import Core.TT

5−import Core.Evaluate

6−import Core.CaseTree

7−import Core.Typecheck

3+import Idris.Core.Elaborate hiding (Tactic(..))

4+import Idris.Core.TT

5+import Idris.Core.Evaluate

6+import Idris.Core.CaseTree

7+import Idris.Core.Typecheck

99import Idris.AbsSyntax

1010import Idris.Delaborate

src/Idris/Prover.hs+5−5

@@ -1,10 +1,10 @@

11module Idris.Prover where

3−import Core.Elaborate hiding (Tactic(..))

4−import Core.TT

5−import Core.Evaluate

6−import Core.CaseTree

7−import Core.Typecheck

3+import Idris.Core.Elaborate hiding (Tactic(..))

4+import Idris.Core.TT

5+import Idris.Core.Evaluate

6+import Idris.Core.CaseTree

7+import Idris.Core.Typecheck

99import Idris.AbsSyntax

1010import Idris.Delaborate

src/Idris/Providers.hs+2−2

@@ -1,8 +1,8 @@

11{-# LANGUAGE PatternGuards #-}

22module Idris.Providers (providerTy, getProvided) where

4−import Core.TT

5−import Core.Evaluate

4+import Idris.Core.TT

5+import Idris.Core.Evaluate

66import Idris.AbsSyntax

77import Idris.AbsSyntaxTree

88import Idris.Error

src/Idris/REPL.hs+4−4

@@ -30,10 +30,10 @@ import Util.System

3030import Util.DynamicLinker

3131import Util.Net (listenOnLocalhost)

3232

33−import Core.Evaluate

34−import Core.Execute (execute)

35−import Core.TT

36−import Core.Constraints

33+import Idris.Core.Evaluate

34+import Idris.Core.Execute (execute)

35+import Idris.Core.TT

36+import Idris.Core.Constraints

3737

3838import IRTS.Compiler

3939import IRTS.CodegenCommon

src/Idris/REPLParser.hs+1−1

@@ -5,7 +5,7 @@ import System.Console.ANSI (Color(..))

66import Idris.Colours

77import Idris.AbsSyntax

8−import Core.TT

8+import Idris.Core.TT

99import qualified Idris.Parser as P

1010

1111import Control.Applicative

src/Idris/Transforms.hs+2−2

@@ -3,8 +3,8 @@

33module Idris.Transforms where

55import Idris.AbsSyntax

6−import Core.CaseTree

7−import Core.TT

6+import Idris.Core.CaseTree

7+import Idris.Core.TT

99data TTOpt = TermTrans (TT Name -> TT Name) -- term transform

1010 | CaseTrans (SC -> SC) -- case expression transform

src/Idris/Unlit.hs+1−1

@@ -1,6 +1,6 @@

11module Idris.Unlit(unlit) where

3−import Core.TT

3+import Idris.Core.TT

44import Data.Char

66unlit :: FilePath -> String -> TC String

src/Idris/UnusedArgs.hs+2−2

@@ -2,8 +2,8 @@ module Idris.UnusedArgs where

33import Idris.AbsSyntax

5−import Core.CaseTree

6−import Core.TT

5+import Idris.Core.CaseTree

6+import Idris.Core.TT

88import Control.Monad.State

99import Data.Maybe

src/Main.hs+4−4

@@ -12,10 +12,10 @@ import Control.Monad.Trans.Error ( ErrorT(..) )

1212import Control.Monad.Trans.State.Strict ( execStateT, get, put )

1313import Control.Monad ( when )

1414

15−import Core.TT

16−import Core.Typecheck

17−import Core.Evaluate

18−import Core.Constraints

15+import Idris.Core.TT

16+import Idris.Core.Typecheck

17+import Idris.Core.Evaluate

18+import Idris.Core.Constraints

1919

2020import Idris.AbsSyntax

2121import Idris.Parser

src/Pkg/PParser.hs+1−1

@@ -2,7 +2,7 @@ module Pkg.PParser where

33import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace)

5−import Core.TT

5+import Idris.Core.TT

66import Idris.REPL

77import Idris.AbsSyntaxTree

88import Idris.ParseHelpers

src/Pkg/Package.hs+1−1

@@ -14,7 +14,7 @@ import Control.Monad

1414import Data.List

1515import Data.List.Split(splitOn)

1616

17−import Core.TT

17+import Idris.Core.TT

1818import Idris.REPL

1919import Idris.AbsSyntax

2020

src/Util/LLVMStubs.hs+1−1

@@ -7,7 +7,7 @@ Replaces stuff from LLVM.General.Target and IRTS.CodegenLLVM.

88module Util.LLVMStubs where

10−import qualified Core.TT as TT

10+import qualified Idris.Core.TT as TT

1111import IRTS.Simplified

1212import IRTS.CodegenCommon

1313