Permalink
Browse files

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.
  • Loading branch information...
1 parent c459480 commit 5000aeb2560393a1f3c5f16b0795d5b7dd14bb8d @puffnfresh puffnfresh committed Nov 29, 2013
Showing with 252 additions and 143 deletions.
  1. +118 −9 idris.cabal
  2. +1 −1 src/IRTS/BCImp.hs
  3. +1 −1 src/IRTS/Bytecode.hs
  4. +1 −1 src/IRTS/CodegenC.hs
  5. +1 −1 src/IRTS/CodegenCommon.hs
  6. +1 −1 src/IRTS/CodegenJava.hs
  7. +1 −1 src/IRTS/CodegenJavaScript.hs
  8. +2 −2 src/IRTS/CodegenLLVM.hs
  9. +3 −3 src/IRTS/Compiler.hs
  10. +1 −1 src/IRTS/Defunctionalise.hs
  11. +1 −1 src/IRTS/DumpBC.hs
  12. +1 −1 src/IRTS/Inliner.hs
  13. +1 −1 src/IRTS/Java/JTypes.hs
  14. +1 −1 src/IRTS/Java/Mangling.hs
  15. +1 −1 src/IRTS/Lang.hs
  16. +1 −1 src/IRTS/Simplified.hs
  17. +4 −4 src/Idris/AbsSyntax.hs
  18. +4 −4 src/Idris/AbsSyntaxTree.hs
  19. +3 −3 src/Idris/CaseSplit.hs
  20. +2 −2 src/Idris/Completion.hs
  21. +2 −2 src/{ → Idris}/Core/CaseTree.hs
  22. +2 −2 src/{ → Idris}/Core/Constraints.hs
  23. +8 −8 src/{ → Idris}/Core/Elaborate.hs
  24. +3 −3 src/{ → Idris}/Core/Evaluate.hs
  25. +4 −4 src/{ → Idris}/Core/Execute.hs
  26. +6 −6 src/{ → Idris}/Core/ProofState.hs
  27. +1 −1 src/{ → Idris}/Core/TT.hs
  28. +3 −3 src/{ → Idris}/Core/Typecheck.hs
  29. +3 −3 src/{ → Idris}/Core/Unify.hs
  30. +3 −3 src/Idris/Coverage.hs
  31. +2 −2 src/Idris/DSL.hs
  32. +1 −1 src/Idris/DataOpts.hs
  33. +1 −1 src/Idris/DeepSeq.hs
  34. +2 −2 src/Idris/Delaborate.hs
  35. +2 −2 src/Idris/Docs.hs
  36. +6 −6 src/Idris/ElabDecls.hs
  37. +3 −3 src/Idris/ElabTerm.hs
  38. +3 −3 src/Idris/Error.hs
  39. +3 −3 src/Idris/IBC.hs
  40. +1 −1 src/Idris/IdeSlave.hs
  41. +1 −1 src/Idris/Imports.hs
  42. +1 −1 src/Idris/Inliner.hs
  43. +2 −2 src/Idris/ParseData.hs
  44. +2 −2 src/Idris/ParseExpr.hs
  45. +2 −2 src/Idris/ParseHelpers.hs
  46. +1 −1 src/Idris/ParseOps.hs
  47. +2 −2 src/Idris/Parser.hs
  48. +2 −2 src/Idris/PartialEval.hs
  49. +2 −2 src/Idris/Primitives.hs
  50. +5 −5 src/Idris/ProofSearch.hs
  51. +5 −5 src/Idris/Prover.hs
  52. +2 −2 src/Idris/Providers.hs
  53. +4 −4 src/Idris/REPL.hs
  54. +1 −1 src/Idris/REPLParser.hs
  55. +2 −2 src/Idris/Transforms.hs
  56. +1 −1 src/Idris/Unlit.hs
  57. +2 −2 src/Idris/UnusedArgs.hs
  58. +4 −4 src/Main.hs
  59. +1 −1 src/Pkg/PParser.hs
  60. +1 −1 src/Pkg/Package.hs
  61. +1 −1 src/Util/LLVMStubs.hs
View
@@ -301,19 +301,128 @@ Flag FFI
Default: False
manual: True
+Library
+ hs-source-dirs: src
+ Exposed-modules:
+ Idris.Core.CaseTree
+ , Idris.Core.Constraints
+ , Idris.Core.Elaborate
+ , Idris.Core.Evaluate
+ , Idris.Core.Execute
+ , Idris.Core.ProofState
+ , Idris.Core.TT
+ , Idris.Core.Typecheck
+ , Idris.Core.Unify
+
+ , Idris.AbsSyntax
+ , Idris.AbsSyntaxTree
+ , Idris.CaseSplit
+ , Idris.Chaser
+ , Idris.Colours
+ , Idris.Completion
+ , Idris.Coverage
+ , Idris.DSL
+ , Idris.DataOpts
+ , Idris.DeepSeq
+ , Idris.Delaborate
+ , Idris.Docs
+ , Idris.ElabDecls
+ , Idris.ElabTerm
+ , Idris.Error
+ , Idris.Help
+ , Idris.IBC
+ , Idris.IdeSlave
+ , Idris.Imports
+ , Idris.Inliner
+ , Idris.Parser
+ , Idris.ParseHelpers
+ , Idris.ParseOps
+ , Idris.ParseExpr
+ , Idris.ParseData
+ , Idris.PartialEval
+ , Idris.Primitives
+ , Idris.ProofSearch
+ , Idris.Prover
+ , Idris.Providers
+ , Idris.REPL
+ , Idris.REPLParser
+ , Idris.Transforms
+ , Idris.Unlit
+ , Idris.UnusedArgs
+
+ , IRTS.BCImp
+ , IRTS.Bytecode
+ , IRTS.CodegenC
+ , IRTS.CodegenCommon
+ , IRTS.CodegenJava
+ , IRTS.CodegenJavaScript
+ , IRTS.Compiler
+ , IRTS.Defunctionalise
+ , IRTS.DumpBC
+ , IRTS.Inliner
+ , IRTS.Java.ASTBuilding
+ , IRTS.Java.JTypes
+ , IRTS.Java.Mangling
+ , IRTS.Java.Pom
+ , IRTS.Lang
+ , IRTS.Simplified
+
+ Other-modules:
+ Util.Pretty
+ , Util.System
+ , Util.DynamicLinker
+ , Util.Net
+
+ , Pkg.Package
+ , Pkg.PParser
+
+ -- Auto Generated
+ Paths_idris
+
+ Extensions: MultiParamTypeClasses
+ , FunctionalDependencies
+ , FlexibleInstances
+ , TemplateHaskell
+
+ ghc-prof-options: -auto-all -caf-all
+ ghc-options: -threaded -rtsopts
+
+ if os(linux)
+ cpp-options: -DLINUX
+ build-depends: unix
+ if os(freebsd)
+ cpp-options: -DFREEBSD
+ build-depends: unix
+ if os(darwin)
+ cpp-options: -DMACOSX
+ build-depends: unix
+ if os(windows)
+ cpp-options: -DWINDOWS
+ build-depends: Win32
+ if flag(LLVM)
+ other-modules: IRTS.CodegenLLVM
+ cpp-options: -DIDRIS_LLVM
+ build-depends: llvm-general == 3.3.8.*
+ , llvm-general-pure == 3.3.8.*
+ else
+ other-modules: Util.LLVMStubs
+ if flag(FFI)
+ build-depends: libffi
+ cpp-options: -DIDRIS_FFI
+
Executable idris
Main-is: Main.hs
hs-source-dirs: src
Other-modules:
- Core.CaseTree
- , Core.Constraints
- , Core.Elaborate
- , Core.Evaluate
- , Core.Execute
- , Core.ProofState
- , Core.TT
- , Core.Typecheck
- , Core.Unify
+ Idris.Core.CaseTree
+ , Idris.Core.Constraints
+ , Idris.Core.Elaborate
+ , Idris.Core.Evaluate
+ , Idris.Core.Execute
+ , Idris.Core.ProofState
+ , Idris.Core.TT
+ , Idris.Core.Typecheck
+ , Idris.Core.Unify
, Idris.AbsSyntax
, Idris.AbsSyntaxTree
View
@@ -5,7 +5,7 @@ module IRTS.BCImp where
import IRTS.Lang
import IRTS.Simplified
-import Core.TT
+import Idris.Core.TT
data Reg = RVal | L Int
@@ -5,7 +5,7 @@ module IRTS.Bytecode where
import IRTS.Lang
import IRTS.Simplified
-import Core.TT
+import Idris.Core.TT
import Data.Maybe
{- We have:
@@ -5,7 +5,7 @@ import IRTS.Bytecode
import IRTS.Lang
import IRTS.Simplified
import IRTS.CodegenCommon
-import Core.TT
+import Idris.Core.TT
import Paths_idris
import Util.System
@@ -1,6 +1,6 @@
module IRTS.CodegenCommon where
-import Core.TT
+import Idris.Core.TT
import IRTS.Simplified
import Control.Exception
@@ -1,7 +1,7 @@
{-# LANGUAGE PatternGuards #-}
module IRTS.CodegenJava (codegenJava) where
-import Core.TT hiding (mkApp)
+import Idris.Core.TT hiding (mkApp)
import IRTS.CodegenCommon
import IRTS.Java.ASTBuilding
import IRTS.Java.JTypes
@@ -7,7 +7,7 @@ import IRTS.Bytecode
import IRTS.Lang
import IRTS.Simplified
import IRTS.CodegenCommon
-import Core.TT
+import Idris.Core.TT
import Paths_idris
import Util.System
@@ -4,8 +4,8 @@ module IRTS.CodegenLLVM (codegenLLVM) where
import IRTS.CodegenCommon
import IRTS.Lang
import IRTS.Simplified
-import qualified Core.TT as TT
-import Core.TT (ArithTy(..), IntTy(..), NativeTy(..), nativeTyWidth)
+import qualified Idris.Core.TT as TT
+import Idris.Core.TT (ArithTy(..), IntTy(..), NativeTy(..), nativeTyWidth)
import Util.System
import Paths_idris
@@ -21,9 +21,9 @@ import Idris.AbsSyntax
import Idris.UnusedArgs
import Idris.Error
-import Core.TT
-import Core.Evaluate
-import Core.CaseTree
+import Idris.Core.TT
+import Idris.Core.Evaluate
+import Idris.Core.CaseTree
import Control.Monad.State
import Data.List
@@ -2,7 +2,7 @@ module IRTS.Defunctionalise(module IRTS.Defunctionalise,
module IRTS.Lang) where
import IRTS.Lang
-import Core.TT
+import Idris.Core.TT
import Debug.Trace
import Data.Maybe
View
@@ -2,7 +2,7 @@ module IRTS.DumpBC where
import IRTS.Lang
import IRTS.Simplified
-import Core.TT
+import Idris.Core.TT
import IRTS.Bytecode
import Data.List
View
@@ -1,6 +1,6 @@
module IRTS.Inliner where
-import Core.TT
+import Idris.Core.TT
import IRTS.Defunctionalise
@@ -1,7 +1,7 @@
{-# LANGUAGE PatternGuards #-}
module IRTS.Java.JTypes where
-import Core.TT
+import Idris.Core.TT
import IRTS.Lang
import Language.Java.Syntax
import qualified Language.Java.Syntax as J
@@ -3,7 +3,7 @@
module IRTS.Java.Mangling where
-import Core.TT
+import Idris.Core.TT
import IRTS.Lang
import IRTS.Simplified
View
@@ -1,7 +1,7 @@
module IRTS.Lang where
import Control.Monad.State hiding (lift)
-import Core.TT
+import Idris.Core.TT
import Data.List
import Debug.Trace
@@ -1,7 +1,7 @@
module IRTS.Simplified where
import IRTS.Defunctionalise
-import Core.TT
+import Idris.Core.TT
import Data.Maybe
import Control.Monad.State
@@ -3,10 +3,10 @@
module Idris.AbsSyntax(module Idris.AbsSyntax, module Idris.AbsSyntaxTree) where
-import Core.TT
-import Core.Evaluate
-import Core.Elaborate hiding (Tactic(..))
-import Core.Typecheck
+import Idris.Core.TT
+import Idris.Core.Evaluate
+import Idris.Core.Elaborate hiding (Tactic(..))
+import Idris.Core.Typecheck
import Idris.AbsSyntaxTree
import Idris.Colours
import Idris.IdeSlave
@@ -3,10 +3,10 @@
module Idris.AbsSyntaxTree where
-import Core.TT
-import Core.Evaluate
-import Core.Elaborate hiding (Tactic(..))
-import Core.Typecheck
+import Idris.Core.TT
+import Idris.Core.Evaluate
+import Idris.Core.Elaborate hiding (Tactic(..))
+import Idris.Core.Typecheck
import IRTS.Lang
import IRTS.CodegenCommon
import Util.Pretty
@@ -14,9 +14,9 @@ import Idris.Delaborate
import Idris.Parser
import Idris.Error
-import Core.TT
-import Core.Typecheck
-import Core.Evaluate
+import Idris.Core.TT
+import Idris.Core.Typecheck
+import Idris.Core.Evaluate
import Data.Maybe
import Data.Char
@@ -1,8 +1,8 @@
-- | Support for command-line completion at the REPL and in the prover
module Idris.Completion (replCompletion, proverCompletion) where
-import Core.Evaluate (ctxtAlist)
-import Core.TT
+import Idris.Core.Evaluate (ctxtAlist)
+import Idris.Core.TT
import Idris.AbsSyntaxTree
import Idris.Help
@@ -1,10 +1,10 @@
{-# LANGUAGE PatternGuards, DeriveFunctor, TypeSynonymInstances #-}
-module Core.CaseTree(CaseDef(..), SC, SC'(..), CaseAlt, CaseAlt'(..),
+module Idris.Core.CaseTree(CaseDef(..), SC, SC'(..), CaseAlt, CaseAlt'(..),
Phase(..), CaseTree,
simpleCase, small, namesUsed, findCalls, findUsedArgs) where
-import Core.TT
+import Idris.Core.TT
import Control.Monad.State
import Data.Maybe
@@ -1,7 +1,7 @@
-- | Check universe constraints.
-module Core.Constraints(ucheck) where
+module Idris.Core.Constraints(ucheck) where
-import Core.TT
+import Idris.Core.TT
import Control.Applicative
import Control.Arrow
@@ -8,14 +8,14 @@
tactics out of the primitives.
-}
-module Core.Elaborate(module Core.Elaborate,
- module Core.ProofState) where
-
-import Core.ProofState
-import Core.TT
-import Core.Evaluate
-import Core.Typecheck
-import Core.Unify
+module Idris.Core.Elaborate(module Idris.Core.Elaborate,
+ module Idris.Core.ProofState) where
+
+import Idris.Core.ProofState
+import Idris.Core.TT
+import Idris.Core.Evaluate
+import Idris.Core.Typecheck
+import Idris.Core.Unify
import Control.Monad.State
import Data.Char
@@ -1,7 +1,7 @@
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances,
PatternGuards #-}
-module Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,
+module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,
rt_simplify, simplify, specialise, hnf, convEq, convEq',
Def(..), CaseInfo(..), CaseDefs(..),
Accessibility(..), Totality(..), PReason(..),
@@ -17,8 +17,8 @@ import Control.Monad.State
import qualified Data.Binary as B
import Data.Binary hiding (get, put)
-import Core.TT
-import Core.CaseTree
+import Idris.Core.TT
+import Idris.Core.CaseTree
data EvalState = ES { limited :: [(Name, Int)],
nexthole :: Int }
Oops, something went wrong.

0 comments on commit 5000aeb

Please sign in to comment.