Move ElabTerm into Elab.Term

idris.cabal

@@ -730,6 +730,7 @@ Library
                 , Idris.Elab.Provider
                 , Idris.Elab.Transform
                 , Idris.Elab.Value
+                , Idris.Elab.Term
 
                 , Idris.AbsSyntax
                 , Idris.AbsSyntaxTree
@@ -748,7 +749,6 @@ Library
                 , Idris.Docstrings
                 , Idris.ElabDecls
                 , Idris.ElabQuasiquote
-                , Idris.ElabTerm
                 , Idris.Erasure
                 , Idris.Error
                 , Idris.ErrReverse

src/Idris/CaseSplit.hs

@@ -10,13 +10,13 @@ module Idris.CaseSplit(splitOnLine, replaceSplits,
 import Idris.AbsSyntax
 import Idris.AbsSyntaxTree (Idris, IState, PTerm)
 import Idris.ElabDecls
-import Idris.ElabTerm
 import Idris.Delaborate
 import Idris.Parser
 import Idris.Error
 import Idris.Output
 
 import Idris.Elab.Value
+import Idris.Elab.Term
 
 import Idris.Core.TT
 import Idris.Core.Typecheck

src/Idris/Elab/Class.hs

@@ -7,7 +7,7 @@ import Idris.DSL
 import Idris.Error
 import Idris.Delaborate
 import Idris.Imports
-import Idris.ElabTerm
+import Idris.Elab.Term
 import Idris.Coverage
 import Idris.DataOpts
 import Idris.Providers

src/Idris/Elab/Clause.hs

@@ -7,7 +7,7 @@ import Idris.DSL
 import Idris.Error
 import Idris.Delaborate
 import Idris.Imports
-import Idris.ElabTerm
+import Idris.Elab.Term
 import Idris.Coverage
 import Idris.DataOpts
 import Idris.Providers

src/Idris/Elab/Data.hs

@@ -7,7 +7,7 @@ import Idris.DSL
 import Idris.Error
 import Idris.Delaborate
 import Idris.Imports
-import Idris.ElabTerm
+import Idris.Elab.Term
 import Idris.Coverage
 import Idris.DataOpts
 import Idris.Providers

src/Idris/Elab/Instance.hs

@@ -7,7 +7,6 @@ import Idris.DSL
 import Idris.Error
 import Idris.Delaborate
 import Idris.Imports
-import Idris.ElabTerm
 import Idris.Coverage
 import Idris.DataOpts
 import Idris.Providers
@@ -21,6 +20,7 @@ import IRTS.Lang
 import Idris.Elab.Type
 import Idris.Elab.Data
 import Idris.Elab.Utils
+import Idris.Elab.Term
 
 import Idris.Core.TT
 import Idris.Core.Elaborate hiding (Tactic(..))

src/Idris/Elab/Provider.hs

@@ -7,7 +7,6 @@ import Idris.DSL
 import Idris.Error
 import Idris.Delaborate
 import Idris.Imports
-import Idris.ElabTerm
 import Idris.Coverage
 import Idris.DataOpts
 import Idris.Providers
@@ -22,6 +21,7 @@ import Idris.Elab.Type
 import Idris.Elab.Clause
 import Idris.Elab.Value
 import Idris.Elab.Utils
+import Idris.Elab.Term
 
 import Idris.Core.TT
 import Idris.Core.Elaborate hiding (Tactic(..))

src/Idris/Elab/Record.hs

@@ -7,7 +7,7 @@ import Idris.DSL
 import Idris.Error
 import Idris.Delaborate
 import Idris.Imports
-import Idris.ElabTerm
+import Idris.Elab.Term
 import Idris.Coverage
 import Idris.DataOpts
 import Idris.Providers

src/Idris/Elab/Term.hs

@@ -1,6 +1,6 @@
 {-# LANGUAGE PatternGuards, ViewPatterns #-}
 {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
-module Idris.ElabTerm where
+module Idris.Elab.Term where
 
 import Idris.AbsSyntax
 import Idris.AbsSyntaxTree
@@ -262,9 +262,7 @@ elab ist info emode opts fn tm
     -- normally correct to call elabE - the ones that don't are desugarings
     -- typically
     elabE :: ElabCtxt -> Maybe FC -> PTerm -> ElabD ()
-    elabE ina fc' t =
-     --do g <- goal
-        --trace ("Elaborating " ++ show t ++ " : " ++ show g) $
+    elabE ina fc' t = 
      do solved <- get_recents
         as <- get_autos
         -- If any of the autos use variables which have recently been solved,

src/Idris/Elab/Transform.hs

@@ -7,7 +7,6 @@ import Idris.DSL
 import Idris.Error
 import Idris.Delaborate
 import Idris.Imports
-import Idris.ElabTerm
 import Idris.Coverage
 import Idris.DataOpts
 import Idris.Providers
@@ -19,6 +18,7 @@ import Idris.Output (iputStrLn, pshow, iWarn)
 import IRTS.Lang
 
 import Idris.Elab.Utils
+import Idris.Elab.Term
 
 import Idris.Core.TT
 import Idris.Core.Elaborate hiding (Tactic(..))

src/Idris/Elab/Type.hs

@@ -8,7 +8,7 @@ import Idris.DSL
 import Idris.Error
 import Idris.Delaborate
 import Idris.Imports
-import Idris.ElabTerm
+import Idris.Elab.Term
 import Idris.Coverage
 import Idris.DataOpts
 import Idris.Providers

src/Idris/Elab/Value.hs

@@ -8,7 +8,6 @@ import Idris.DSL
 import Idris.Error
 import Idris.Delaborate
 import Idris.Imports
-import Idris.ElabTerm
 import Idris.Coverage
 import Idris.DataOpts
 import Idris.Providers
@@ -20,6 +19,7 @@ import Idris.Output (iputStrLn, pshow, iWarn)
 import IRTS.Lang
 
 import Idris.Elab.Utils
+import Idris.Elab.Term
 
 import Idris.Core.TT
 import Idris.Core.Elaborate hiding (Tactic(..))

src/Idris/ElabDecls.hs

@@ -9,7 +9,7 @@ import Idris.DSL
 import Idris.Error
 import Idris.Delaborate
 import Idris.Imports
-import Idris.ElabTerm
+import Idris.Elab.Term
 import Idris.Coverage
 import Idris.DataOpts
 import Idris.Providers

src/Idris/Interactive.hs

@@ -12,12 +12,12 @@ import Idris.Core.Evaluate
 import Idris.CaseSplit
 import Idris.AbsSyntax
 import Idris.ElabDecls
-import Idris.ElabTerm
 import Idris.Error
 import Idris.Delaborate
 import Idris.Output
 import Idris.IdeMode hiding (IdeModeCommand(..))
 import Idris.Elab.Value
+import Idris.Elab.Term
 
 import Util.Pretty
 import Util.System

src/Idris/Parser.hs

@@ -25,8 +25,8 @@ import Idris.Imports
 import Idris.Delaborate
 import Idris.Error
 import Idris.Elab.Value
+import Idris.Elab.Term
 import Idris.ElabDecls
-import Idris.ElabTerm
 import Idris.Coverage
 import Idris.IBC
 import Idris.Unlit

src/Idris/Prover.hs

@@ -9,13 +9,13 @@ import Idris.Core.Typecheck
 
 import Idris.Elab.Utils
 import Idris.Elab.Value
+import Idris.Elab.Term
 
 import Idris.AbsSyntax
 import Idris.AbsSyntaxTree
 import Idris.Delaborate
 import Idris.Docs (getDocs, pprintDocs, pprintConstDocs)
 import Idris.ElabDecls
-import Idris.ElabTerm
 import Idris.Parser hiding (params)
 import Idris.Error
 import Idris.DataOpts

src/Idris/REPL.hs

@@ -8,7 +8,6 @@ import Idris.ASTUtils
 import Idris.Apropos (apropos, aproposModules)
 import Idris.REPLParser
 import Idris.ElabDecls
-import Idris.ElabTerm
 import Idris.Erasure
 import Idris.Error
 import Idris.ErrReverse
@@ -39,6 +38,7 @@ import Idris.Elab.Type
 import Idris.Elab.Clause
 import Idris.Elab.Data
 import Idris.Elab.Value
+import Idris.Elab.Term
 
 import Version_idris (gitHash)
 import Util.System