Move ElabTerm into Elab.Term
commitc3804217069870be284ba3149faed088eb224946
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateSun 12 Apr 2015, 12:45 (12 years ago)
parent8ab2814
idris.cabal+1−1
@@ -730,6 +730,7 @@ Library
730730 , Idris.Elab.Provider
731731 , Idris.Elab.Transform
732732 , Idris.Elab.Value
733+ , Idris.Elab.Term
733734
734735 , Idris.AbsSyntax
735736 , Idris.AbsSyntaxTree
@@ -748,7 +749,6 @@ Library
748749 , Idris.Docstrings
749750 , Idris.ElabDecls
750751 , Idris.ElabQuasiquote
751− , Idris.ElabTerm
752752 , Idris.Erasure
753753 , Idris.Error
754754 , Idris.ErrReverse
src/Idris/CaseSplit.hs+1−1
@@ -10,13 +10,13 @@ module Idris.CaseSplit(splitOnLine, replaceSplits,
1010import Idris.AbsSyntax
1111import Idris.AbsSyntaxTree (Idris, IState, PTerm)
1212import Idris.ElabDecls
13−import Idris.ElabTerm
1413import Idris.Delaborate
1514import Idris.Parser
1615import Idris.Error
1716import Idris.Output
1817
1918import Idris.Elab.Value
19+import Idris.Elab.Term
2020
2121import Idris.Core.TT
2222import Idris.Core.Typecheck
src/Idris/Elab/Class.hs+1−1
@@ -7,7 +7,7 @@ import Idris.DSL
77import Idris.Error
88import Idris.Delaborate
99import Idris.Imports
10−import Idris.ElabTerm
10+import Idris.Elab.Term
1111import Idris.Coverage
1212import Idris.DataOpts
1313import Idris.Providers
src/Idris/Elab/Clause.hs+1−1
@@ -7,7 +7,7 @@ import Idris.DSL
77import Idris.Error
88import Idris.Delaborate
99import Idris.Imports
10−import Idris.ElabTerm
10+import Idris.Elab.Term
1111import Idris.Coverage
1212import Idris.DataOpts
1313import Idris.Providers
src/Idris/Elab/Data.hs+1−1
@@ -7,7 +7,7 @@ import Idris.DSL
77import Idris.Error
88import Idris.Delaborate
99import Idris.Imports
10−import Idris.ElabTerm
10+import Idris.Elab.Term
1111import Idris.Coverage
1212import Idris.DataOpts
1313import Idris.Providers
src/Idris/Elab/Instance.hs+1−1
@@ -7,7 +7,6 @@ import Idris.DSL
77import Idris.Error
88import Idris.Delaborate
99import Idris.Imports
10−import Idris.ElabTerm
1110import Idris.Coverage
1211import Idris.DataOpts
1312import Idris.Providers
@@ -21,6 +20,7 @@ import IRTS.Lang
2120import Idris.Elab.Type
2221import Idris.Elab.Data
2322import Idris.Elab.Utils
23+import Idris.Elab.Term
2424
2525import Idris.Core.TT
2626import Idris.Core.Elaborate hiding (Tactic(..))
src/Idris/Elab/Provider.hs+1−1
@@ -7,7 +7,6 @@ import Idris.DSL
77import Idris.Error
88import Idris.Delaborate
99import Idris.Imports
10−import Idris.ElabTerm
1110import Idris.Coverage
1211import Idris.DataOpts
1312import Idris.Providers
@@ -22,6 +21,7 @@ import Idris.Elab.Type
2221import Idris.Elab.Clause
2322import Idris.Elab.Value
2423import Idris.Elab.Utils
24+import Idris.Elab.Term
2525
2626import Idris.Core.TT
2727import Idris.Core.Elaborate hiding (Tactic(..))
src/Idris/Elab/Record.hs+1−1
@@ -7,7 +7,7 @@ import Idris.DSL
77import Idris.Error
88import Idris.Delaborate
99import Idris.Imports
10−import Idris.ElabTerm
10+import Idris.Elab.Term
1111import Idris.Coverage
1212import Idris.DataOpts
1313import Idris.Providers
src/Idris/ElabTerm.hs → src/Idris/Elab/Term.hsrenamed+2−4
@@ -1,6 +1,6 @@
11{-# LANGUAGE PatternGuards, ViewPatterns #-}
22{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}
3−module Idris.ElabTerm where
3+module Idris.Elab.Term where
44
55import Idris.AbsSyntax
66import Idris.AbsSyntaxTree
@@ -262,9 +262,7 @@ elab ist info emode opts fn tm
262262 -- normally correct to call elabE - the ones that don't are desugarings
263263 -- typically
264264 elabE :: ElabCtxt -> Maybe FC -> PTerm -> ElabD ()
265− elabE ina fc' t =
266− --do g <- goal
267− --trace ("Elaborating " ++ show t ++ " : " ++ show g) $
265+ elabE ina fc' t =
268266 do solved <- get_recents
269267 as <- get_autos
270268 -- 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
77import Idris.Error
88import Idris.Delaborate
99import Idris.Imports
10−import Idris.ElabTerm
1110import Idris.Coverage
1211import Idris.DataOpts
1312import Idris.Providers
@@ -19,6 +18,7 @@ import Idris.Output (iputStrLn, pshow, iWarn)
1918import IRTS.Lang
2019
2120import Idris.Elab.Utils
21+import Idris.Elab.Term
2222
2323import Idris.Core.TT
2424import Idris.Core.Elaborate hiding (Tactic(..))
src/Idris/Elab/Type.hs+1−1
@@ -8,7 +8,7 @@ import Idris.DSL
88import Idris.Error
99import Idris.Delaborate
1010import Idris.Imports
11−import Idris.ElabTerm
11+import Idris.Elab.Term
1212import Idris.Coverage
1313import Idris.DataOpts
1414import Idris.Providers
src/Idris/Elab/Value.hs+1−1
@@ -8,7 +8,6 @@ import Idris.DSL
88import Idris.Error
99import Idris.Delaborate
1010import Idris.Imports
11−import Idris.ElabTerm
1211import Idris.Coverage
1312import Idris.DataOpts
1413import Idris.Providers
@@ -20,6 +19,7 @@ import Idris.Output (iputStrLn, pshow, iWarn)
2019import IRTS.Lang
2120
2221import Idris.Elab.Utils
22+import Idris.Elab.Term
2323
2424import Idris.Core.TT
2525import Idris.Core.Elaborate hiding (Tactic(..))
src/Idris/ElabDecls.hs+1−1
@@ -9,7 +9,7 @@ import Idris.DSL
99import Idris.Error
1010import Idris.Delaborate
1111import Idris.Imports
12−import Idris.ElabTerm
12+import Idris.Elab.Term
1313import Idris.Coverage
1414import Idris.DataOpts
1515import Idris.Providers
src/Idris/Interactive.hs+1−1
@@ -12,12 +12,12 @@ import Idris.Core.Evaluate
1212import Idris.CaseSplit
1313import Idris.AbsSyntax
1414import Idris.ElabDecls
15−import Idris.ElabTerm
1615import Idris.Error
1716import Idris.Delaborate
1817import Idris.Output
1918import Idris.IdeMode hiding (IdeModeCommand(..))
2019import Idris.Elab.Value
20+import Idris.Elab.Term
2121
2222import Util.Pretty
2323import Util.System
src/Idris/Parser.hs+1−1
@@ -25,8 +25,8 @@ import Idris.Imports
2525import Idris.Delaborate
2626import Idris.Error
2727import Idris.Elab.Value
28+import Idris.Elab.Term
2829import Idris.ElabDecls
29−import Idris.ElabTerm
3030import Idris.Coverage
3131import Idris.IBC
3232import Idris.Unlit
src/Idris/Prover.hs+1−1
@@ -9,13 +9,13 @@ import Idris.Core.Typecheck
99
1010import Idris.Elab.Utils
1111import Idris.Elab.Value
12+import Idris.Elab.Term
1213
1314import Idris.AbsSyntax
1415import Idris.AbsSyntaxTree
1516import Idris.Delaborate
1617import Idris.Docs (getDocs, pprintDocs, pprintConstDocs)
1718import Idris.ElabDecls
18−import Idris.ElabTerm
1919import Idris.Parser hiding (params)
2020import Idris.Error
2121import Idris.DataOpts
src/Idris/REPL.hs+1−1
@@ -8,7 +8,6 @@ import Idris.ASTUtils
88import Idris.Apropos (apropos, aproposModules)
99import Idris.REPLParser
1010import Idris.ElabDecls
11−import Idris.ElabTerm
1211import Idris.Erasure
1312import Idris.Error
1413import Idris.ErrReverse
@@ -39,6 +38,7 @@ import Idris.Elab.Type
3938import Idris.Elab.Clause
4039import Idris.Elab.Data
4140import Idris.Elab.Value
41+import Idris.Elab.Term
4242
4343import Version_idris (gitHash)
4444import Util.System