From c3804217069870be284ba3149faed088eb224946 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Sun, 12 Apr 2015 12:45:42 +0100 Subject: [PATCH] Move ElabTerm into Elab.Term --- idris.cabal | 2 +- src/Idris/CaseSplit.hs | 2 +- src/Idris/Elab/Class.hs | 2 +- src/Idris/Elab/Clause.hs | 2 +- src/Idris/Elab/Data.hs | 2 +- src/Idris/Elab/Instance.hs | 2 +- src/Idris/Elab/Provider.hs | 2 +- src/Idris/Elab/Record.hs | 2 +- src/Idris/{ElabTerm.hs => Elab/Term.hs} | 6 ++---- src/Idris/Elab/Transform.hs | 2 +- src/Idris/Elab/Type.hs | 2 +- src/Idris/Elab/Value.hs | 2 +- src/Idris/ElabDecls.hs | 2 +- src/Idris/Interactive.hs | 2 +- src/Idris/Parser.hs | 2 +- src/Idris/Prover.hs | 2 +- src/Idris/REPL.hs | 2 +- 17 files changed, 18 insertions(+), 20 deletions(-) rename src/Idris/{ElabTerm.hs => Elab/Term.hs} (99%) diff --git a/idris.cabal b/idris.cabal index f27aca962..b2dced6c2 100644 --- a/idris.cabal +++ b/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 diff --git a/src/Idris/CaseSplit.hs b/src/Idris/CaseSplit.hs index bda6bb876..3b3d44b1a 100644 --- a/src/Idris/CaseSplit.hs +++ b/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 diff --git a/src/Idris/Elab/Class.hs b/src/Idris/Elab/Class.hs index cf4337a5c..061a7c1e1 100644 --- a/src/Idris/Elab/Class.hs +++ b/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 diff --git a/src/Idris/Elab/Clause.hs b/src/Idris/Elab/Clause.hs index cb1c6bf7d..5f95d98d3 100644 --- a/src/Idris/Elab/Clause.hs +++ b/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 diff --git a/src/Idris/Elab/Data.hs b/src/Idris/Elab/Data.hs index 8c24d1a1b..006660cde 100644 --- a/src/Idris/Elab/Data.hs +++ b/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 diff --git a/src/Idris/Elab/Instance.hs b/src/Idris/Elab/Instance.hs index 209508347..c4512088e 100644 --- a/src/Idris/Elab/Instance.hs +++ b/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(..)) diff --git a/src/Idris/Elab/Provider.hs b/src/Idris/Elab/Provider.hs index eece52464..980b1d958 100644 --- a/src/Idris/Elab/Provider.hs +++ b/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(..)) diff --git a/src/Idris/Elab/Record.hs b/src/Idris/Elab/Record.hs index 3d4b8d39b..bd8bf8d23 100644 --- a/src/Idris/Elab/Record.hs +++ b/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 diff --git a/src/Idris/ElabTerm.hs b/src/Idris/Elab/Term.hs similarity index 99% rename from src/Idris/ElabTerm.hs rename to src/Idris/Elab/Term.hs index b156a291f..0dc69655c 100644 --- a/src/Idris/ElabTerm.hs +++ b/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, diff --git a/src/Idris/Elab/Transform.hs b/src/Idris/Elab/Transform.hs index a2d17c62f..a1bc0ab7c 100644 --- a/src/Idris/Elab/Transform.hs +++ b/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(..)) diff --git a/src/Idris/Elab/Type.hs b/src/Idris/Elab/Type.hs index 4e3a9005a..ae6791446 100644 --- a/src/Idris/Elab/Type.hs +++ b/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 diff --git a/src/Idris/Elab/Value.hs b/src/Idris/Elab/Value.hs index 4efc07a68..5c7c74d8c 100644 --- a/src/Idris/Elab/Value.hs +++ b/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(..)) diff --git a/src/Idris/ElabDecls.hs b/src/Idris/ElabDecls.hs index b24d98599..997568d7d 100644 --- a/src/Idris/ElabDecls.hs +++ b/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 diff --git a/src/Idris/Interactive.hs b/src/Idris/Interactive.hs index a18f08e48..d453e94e9 100644 --- a/src/Idris/Interactive.hs +++ b/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 diff --git a/src/Idris/Parser.hs b/src/Idris/Parser.hs index 01f731594..f30e8b3e5 100644 --- a/src/Idris/Parser.hs +++ b/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 diff --git a/src/Idris/Prover.hs b/src/Idris/Prover.hs index 64307d95f..27cf0bec4 100644 --- a/src/Idris/Prover.hs +++ b/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 diff --git a/src/Idris/REPL.hs b/src/Idris/REPL.hs index 9733e9a4d..873644847 100644 --- a/src/Idris/REPL.hs +++ b/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