git.iko.soy/Idris-dev
on master help sign in
Move ElabTerm into Elab.Term
c380421Edwin Brady
idris.cabal+1−1
compare with master
unifiedsplit
@@ -730,6 +730,7 @@ Library
730 , Idris.Elab.Provider
730 , Idris.Elab.Provider
731 , Idris.Elab.Transform
731 , Idris.Elab.Transform
732 , Idris.Elab.Value
732 , Idris.Elab.Value
733+ , Idris.Elab.Term
733
734
734 , Idris.AbsSyntax
735 , Idris.AbsSyntax
735 , Idris.AbsSyntaxTree
736 , Idris.AbsSyntaxTree
@@ -748,7 +749,6 @@ Library
748 , Idris.Docstrings
749 , Idris.Docstrings
749 , Idris.ElabDecls
750 , Idris.ElabDecls
750 , Idris.ElabQuasiquote
751 , Idris.ElabQuasiquote
751− , Idris.ElabTerm
752 , Idris.Erasure
752 , Idris.Erasure
753 , Idris.Error
753 , Idris.Error
754 , Idris.ErrReverse
754 , Idris.ErrReverse
src/Idris/CaseSplit.hs+1−1
@@ -10,13 +10,13 @@ module Idris.CaseSplit(splitOnLine, replaceSplits,
10import Idris.AbsSyntax
10import Idris.AbsSyntax
11import Idris.AbsSyntaxTree (Idris, IState, PTerm)
11import Idris.AbsSyntaxTree (Idris, IState, PTerm)
12import Idris.ElabDecls
12import Idris.ElabDecls
13−import Idris.ElabTerm
14import Idris.Delaborate
13import Idris.Delaborate
15import Idris.Parser
14import Idris.Parser
16import Idris.Error
15import Idris.Error
17import Idris.Output
16import Idris.Output
18
17
19import Idris.Elab.Value
18import Idris.Elab.Value
19+import Idris.Elab.Term
20
20
21import Idris.Core.TT
21import Idris.Core.TT
22import Idris.Core.Typecheck
22import Idris.Core.Typecheck
src/Idris/Elab/Class.hs+1−1
@@ -7,7 +7,7 @@ import Idris.DSL
7import Idris.Error
7import Idris.Error
8import Idris.Delaborate
8import Idris.Delaborate
9import Idris.Imports
9import Idris.Imports
10−import Idris.ElabTerm
10+import Idris.Elab.Term
11import Idris.Coverage
11import Idris.Coverage
12import Idris.DataOpts
12import Idris.DataOpts
13import Idris.Providers
13import Idris.Providers
src/Idris/Elab/Clause.hs+1−1
@@ -7,7 +7,7 @@ import Idris.DSL
7import Idris.Error
7import Idris.Error
8import Idris.Delaborate
8import Idris.Delaborate
9import Idris.Imports
9import Idris.Imports
10−import Idris.ElabTerm
10+import Idris.Elab.Term
11import Idris.Coverage
11import Idris.Coverage
12import Idris.DataOpts
12import Idris.DataOpts
13import Idris.Providers
13import Idris.Providers
src/Idris/Elab/Data.hs+1−1
@@ -7,7 +7,7 @@ import Idris.DSL
7import Idris.Error
7import Idris.Error
8import Idris.Delaborate
8import Idris.Delaborate
9import Idris.Imports
9import Idris.Imports
10−import Idris.ElabTerm
10+import Idris.Elab.Term
11import Idris.Coverage
11import Idris.Coverage
12import Idris.DataOpts
12import Idris.DataOpts
13import Idris.Providers
13import Idris.Providers
src/Idris/Elab/Instance.hs+1−1
@@ -7,7 +7,6 @@ import Idris.DSL
7import Idris.Error
7import Idris.Error
8import Idris.Delaborate
8import Idris.Delaborate
9import Idris.Imports
9import Idris.Imports
10−import Idris.ElabTerm
11import Idris.Coverage
10import Idris.Coverage
12import Idris.DataOpts
11import Idris.DataOpts
13import Idris.Providers
12import Idris.Providers
@@ -21,6 +20,7 @@ import IRTS.Lang
21import Idris.Elab.Type
20import Idris.Elab.Type
22import Idris.Elab.Data
21import Idris.Elab.Data
23import Idris.Elab.Utils
22import Idris.Elab.Utils
23+import Idris.Elab.Term
24
24
25import Idris.Core.TT
25import Idris.Core.TT
26import Idris.Core.Elaborate hiding (Tactic(..))
26import Idris.Core.Elaborate hiding (Tactic(..))
src/Idris/Elab/Provider.hs+1−1
@@ -7,7 +7,6 @@ import Idris.DSL
7import Idris.Error
7import Idris.Error
8import Idris.Delaborate
8import Idris.Delaborate
9import Idris.Imports
9import Idris.Imports
10−import Idris.ElabTerm
11import Idris.Coverage
10import Idris.Coverage
12import Idris.DataOpts
11import Idris.DataOpts
13import Idris.Providers
12import Idris.Providers
@@ -22,6 +21,7 @@ import Idris.Elab.Type
22import Idris.Elab.Clause
21import Idris.Elab.Clause
23import Idris.Elab.Value
22import Idris.Elab.Value
24import Idris.Elab.Utils
23import Idris.Elab.Utils
24+import Idris.Elab.Term
25
25
26import Idris.Core.TT
26import Idris.Core.TT
27import Idris.Core.Elaborate hiding (Tactic(..))
27import Idris.Core.Elaborate hiding (Tactic(..))
src/Idris/Elab/Record.hs+1−1
@@ -7,7 +7,7 @@ import Idris.DSL
7import Idris.Error
7import Idris.Error
8import Idris.Delaborate
8import Idris.Delaborate
9import Idris.Imports
9import Idris.Imports
10−import Idris.ElabTerm
10+import Idris.Elab.Term
11import Idris.Coverage
11import Idris.Coverage
12import Idris.DataOpts
12import Idris.DataOpts
13import Idris.Providers
13import Idris.Providers
src/Idris/ElabTerm.hs → src/Idris/Elab/Term.hsrenamed+2−4
@@ -1,6 +1,6 @@
1{-# LANGUAGE PatternGuards, ViewPatterns #-}
1{-# LANGUAGE PatternGuards, ViewPatterns #-}
2{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
2{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
3−module Idris.ElabTerm where
3+module Idris.Elab.Term where
4
4
5import Idris.AbsSyntax
5import Idris.AbsSyntax
6import Idris.AbsSyntaxTree
6import Idris.AbsSyntaxTree
@@ -262,9 +262,7 @@ elab ist info emode opts fn tm
262 -- normally correct to call elabE - the ones that don't are desugarings
262 -- normally correct to call elabE - the ones that don't are desugarings
263 -- typically
263 -- typically
264 elabE :: ElabCtxt -> Maybe FC -> PTerm -> ElabD ()
264 elabE :: ElabCtxt -> Maybe FC -> PTerm -> ElabD ()
265− elabE ina fc' t =
265+ elabE ina fc' t =
266− --do g <- goal
267− --trace ("Elaborating " ++ show t ++ " : " ++ show g) $
268 do solved <- get_recents
266 do solved <- get_recents
269 as <- get_autos
267 as <- get_autos
270 -- If any of the autos use variables which have recently been solved,
268 -- If any of the autos use variables which have recently been solved,
src/Idris/Elab/Transform.hs+1−1
@@ -7,7 +7,6 @@ import Idris.DSL
7import Idris.Error
7import Idris.Error
8import Idris.Delaborate
8import Idris.Delaborate
9import Idris.Imports
9import Idris.Imports
10−import Idris.ElabTerm
11import Idris.Coverage
10import Idris.Coverage
12import Idris.DataOpts
11import Idris.DataOpts
13import Idris.Providers
12import Idris.Providers
@@ -19,6 +18,7 @@ import Idris.Output (iputStrLn, pshow, iWarn)
19import IRTS.Lang
18import IRTS.Lang
20
19
21import Idris.Elab.Utils
20import Idris.Elab.Utils
21+import Idris.Elab.Term
22
22
23import Idris.Core.TT
23import Idris.Core.TT
24import Idris.Core.Elaborate hiding (Tactic(..))
24import Idris.Core.Elaborate hiding (Tactic(..))
src/Idris/Elab/Type.hs+1−1
@@ -8,7 +8,7 @@ import Idris.DSL
8import Idris.Error
8import Idris.Error
9import Idris.Delaborate
9import Idris.Delaborate
10import Idris.Imports
10import Idris.Imports
11−import Idris.ElabTerm
11+import Idris.Elab.Term
12import Idris.Coverage
12import Idris.Coverage
13import Idris.DataOpts
13import Idris.DataOpts
14import Idris.Providers
14import Idris.Providers
src/Idris/Elab/Value.hs+1−1
@@ -8,7 +8,6 @@ import Idris.DSL
8import Idris.Error
8import Idris.Error
9import Idris.Delaborate
9import Idris.Delaborate
10import Idris.Imports
10import Idris.Imports
11−import Idris.ElabTerm
12import Idris.Coverage
11import Idris.Coverage
13import Idris.DataOpts
12import Idris.DataOpts
14import Idris.Providers
13import Idris.Providers
@@ -20,6 +19,7 @@ import Idris.Output (iputStrLn, pshow, iWarn)
20import IRTS.Lang
19import IRTS.Lang
21
20
22import Idris.Elab.Utils
21import Idris.Elab.Utils
22+import Idris.Elab.Term
23
23
24import Idris.Core.TT
24import Idris.Core.TT
25import Idris.Core.Elaborate hiding (Tactic(..))
25import Idris.Core.Elaborate hiding (Tactic(..))
src/Idris/ElabDecls.hs+1−1
@@ -9,7 +9,7 @@ import Idris.DSL
9import Idris.Error
9import Idris.Error
10import Idris.Delaborate
10import Idris.Delaborate
11import Idris.Imports
11import Idris.Imports
12−import Idris.ElabTerm
12+import Idris.Elab.Term
13import Idris.Coverage
13import Idris.Coverage
14import Idris.DataOpts
14import Idris.DataOpts
15import Idris.Providers
15import Idris.Providers
src/Idris/Interactive.hs+1−1
@@ -12,12 +12,12 @@ import Idris.Core.Evaluate
12import Idris.CaseSplit
12import Idris.CaseSplit
13import Idris.AbsSyntax
13import Idris.AbsSyntax
14import Idris.ElabDecls
14import Idris.ElabDecls
15−import Idris.ElabTerm
16import Idris.Error
15import Idris.Error
17import Idris.Delaborate
16import Idris.Delaborate
18import Idris.Output
17import Idris.Output
19import Idris.IdeMode hiding (IdeModeCommand(..))
18import Idris.IdeMode hiding (IdeModeCommand(..))
20import Idris.Elab.Value
19import Idris.Elab.Value
20+import Idris.Elab.Term
21
21
22import Util.Pretty
22import Util.Pretty
23import Util.System
23import Util.System
src/Idris/Parser.hs+1−1
@@ -25,8 +25,8 @@ import Idris.Imports
25import Idris.Delaborate
25import Idris.Delaborate
26import Idris.Error
26import Idris.Error
27import Idris.Elab.Value
27import Idris.Elab.Value
28+import Idris.Elab.Term
28import Idris.ElabDecls
29import Idris.ElabDecls
29−import Idris.ElabTerm
30import Idris.Coverage
30import Idris.Coverage
31import Idris.IBC
31import Idris.IBC
32import Idris.Unlit
32import Idris.Unlit
src/Idris/Prover.hs+1−1
@@ -9,13 +9,13 @@ import Idris.Core.Typecheck
9
9
10import Idris.Elab.Utils
10import Idris.Elab.Utils
11import Idris.Elab.Value
11import Idris.Elab.Value
12+import Idris.Elab.Term
12
13
13import Idris.AbsSyntax
14import Idris.AbsSyntax
14import Idris.AbsSyntaxTree
15import Idris.AbsSyntaxTree
15import Idris.Delaborate
16import Idris.Delaborate
16import Idris.Docs (getDocs, pprintDocs, pprintConstDocs)
17import Idris.Docs (getDocs, pprintDocs, pprintConstDocs)
17import Idris.ElabDecls
18import Idris.ElabDecls
18−import Idris.ElabTerm
19import Idris.Parser hiding (params)
19import Idris.Parser hiding (params)
20import Idris.Error
20import Idris.Error
21import Idris.DataOpts
21import Idris.DataOpts
src/Idris/REPL.hs+1−1
@@ -8,7 +8,6 @@ import Idris.ASTUtils
8import Idris.Apropos (apropos, aproposModules)
8import Idris.Apropos (apropos, aproposModules)
9import Idris.REPLParser
9import Idris.REPLParser
10import Idris.ElabDecls
10import Idris.ElabDecls
11−import Idris.ElabTerm
12import Idris.Erasure
11import Idris.Erasure
13import Idris.Error
12import Idris.Error
14import Idris.ErrReverse
13import Idris.ErrReverse
@@ -39,6 +38,7 @@ import Idris.Elab.Type
39import Idris.Elab.Clause
38import Idris.Elab.Clause
40import Idris.Elab.Data
39import Idris.Elab.Data
41import Idris.Elab.Value
40import Idris.Elab.Value
41+import Idris.Elab.Term
42
42
43import Version_idris (gitHash)
43import Version_idris (gitHash)
44import Util.System
44import Util.System