2028acc · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #2949 from jfdm/code-movement

2028accJan de Muijnck-Hughes11 years ago

idris.cabal+6−6

compare with master

unifiedsplit

@@ -876,6 +876,7 @@ Library

876 , Idris.Elab.Transform

877 , Idris.Elab.Value

878 , Idris.Elab.Term

879+ , Idris.Elab.Quasiquote

879

880

880 , Idris.REPL.Browse

881 , Idris.REPL.Browse

881

882

@@ -896,7 +897,6 @@ Library

896 , Idris.Docs

897 , Idris.Docs

897 , Idris.Docstrings

898 , Idris.Docstrings

898 , Idris.ElabDecls

899 , Idris.ElabDecls

899− , Idris.ElabQuasiquote

900 , Idris.Erasure

901 , Idris.Error

902 , Idris.ErrReverse

@@ -909,10 +909,10 @@ Library

909 , Idris.Interactive

910 , Idris.Output

911 , Idris.Parser

912− , Idris.ParseHelpers

912+ , Idris.Parser.Helpers

913− , Idris.ParseOps

913+ , Idris.Parser.Ops

914− , Idris.ParseExpr

914+ , Idris.Parser.Expr

915− , Idris.ParseData

915+ , Idris.Parser.Data

916 , Idris.PartialEval

917 , Idris.Primitives

918 , Idris.ProofSearch

@@ -920,7 +920,7 @@ Library

920 , Idris.Providers

921 , Idris.Reflection

922 , Idris.REPL

923− , Idris.REPLParser

923+ , Idris.REPL.Parser

924 , Idris.Transforms

925 , Idris.TypeSearch

926 , Idris.Unlit

src/Idris/Completion.hs+6−6

@@ -9,10 +9,10 @@ import Idris.AbsSyntaxTree

9import Idris.Help

10import Idris.Imports (installedPackages)

11import Idris.Colours

12−import Idris.ParseHelpers(opChars)

12+import Idris.Parser.Helpers(opChars)

13−import qualified Idris.ParseExpr (constants, tactics)

13+import qualified Idris.Parser.Expr (constants, tactics)

14−import Idris.ParseExpr (TacticArg (..))

14+import Idris.Parser.Expr (TacticArg (..))

15−import Idris.REPLParser (allHelp, setOptions)

15+import Idris.REPL.Parser (allHelp, setOptions)

16import Control.Monad.State.Strict

18import Data.List

@@ -26,7 +26,7 @@ import System.Console.ANSI (Color)

26commands = [ n | (names, _, _) <- allHelp ++ extraHelp, n <- names ]

28tacticArgs :: [(String, Maybe TacticArg)]

29−tacticArgs = [ (name, args) | (names, args, _) <- Idris.ParseExpr.tactics

29+tacticArgs = [ (name, args) | (names, args, _) <- Idris.Parser.Expr.tactics

30 , name <- names ]

31tactics = map fst tacticArgs

@@ -48,7 +48,7 @@ names = do i <- get

48 let ctxt = tt_ctxt i

49 return . nub $

50 mapMaybe (nameString . fst) (ctxtAlist ctxt) ++

51− "Type" : map fst Idris.ParseExpr.constants

51+ "Type" : map fst Idris.Parser.Expr.constants

53metavars :: Idris [String]

54metavars = do i <- get

src/Idris/ElabQuasiquote.hs → src/Idris/Elab/Quasiquote.hsrenamed+1−3

@@ -1,4 +1,4 @@

1−module Idris.ElabQuasiquote (extractUnquotes) where

1+module Idris.Elab.Quasiquote (extractUnquotes) where

3import Idris.Core.Elaborate hiding (Tactic(..))

4import Idris.Core.TT

@@ -171,5 +171,3 @@ extractUnquotes n (PRunElab fc tm ns)

171extractUnquotes n (PConstSugar fc tm)

172 = extractUnquotes n tm

173extractUnquotes n x = return (x, []) -- no subterms!

174−

175−

src/Idris/Elab/Record.hs+1−1

@@ -17,7 +17,7 @@ import Idris.DeepSeq

17import Idris.Output (iputStrLn, pshow, iWarn, sendHighlighting)

18import IRTS.Lang

20−import Idris.ParseExpr (tryFullExpr)

20+import Idris.Parser.Expr (tryFullExpr)

22import Idris.Elab.Type

23import Idris.Elab.Data

src/Idris/Elab/Term.hs+1−1

@@ -20,7 +20,7 @@ import Idris.Core.Typecheck (check, recheck, converts, isType)

20import Idris.Core.WHNF (whnf)

21import Idris.Coverage (buildSCG, checkDeclTotality, genClauses, recoverableCoverage, validCoverageCase)

22import Idris.ErrReverse (errReverse)

23−import Idris.ElabQuasiquote (extractUnquotes)

23+import Idris.Elab.Quasiquote (extractUnquotes)

24import Idris.Elab.Utils

25import Idris.Reflection

26import qualified Util.Pretty as U

src/Idris/IdrisDoc.hs+1−1

@@ -10,7 +10,7 @@ import Idris.Core.TT (Name (..), sUN, SpecialName (..), OutputAnnotation (..),

10import Idris.Core.Evaluate (ctxtAlist, Def (..), lookupDefAcc,

11 Accessibility (..), isDConName, isFnName,

12 isTConName)

13−import Idris.ParseHelpers (opChars)

13+import Idris.Parser.Helpers (opChars)

14import Idris.AbsSyntax

15import Idris.Docs

16import Idris.Docstrings (nullDocstring)

src/Idris/Interactive.hs+22−22

@@ -76,7 +76,7 @@ addClauseFrom fn updatefile l n = do

76 getIndent i n xs | take 9 xs == "instance " = i

77 getIndent i n xs | take (length n) xs == n = i

78 getIndent i n (x : xs) = getIndent (i + 1) n xs

79−

79+

80 getAppName (PApp _ r _) = getAppName r

81 getAppName (PRef _ _ r) = r

82 getAppName (PTyped n _) = getAppName n

@@ -120,7 +120,7 @@ addMissing fn updatefile l n

120 if updatefile

121 then do let fb = fn ++ "~"

122 runIO $ writeSource fb (unlines (before ++ nonblank)

123− ++ extras ++

123+ ++ extras ++

124 (if null extras then ""

125 else "\n" ++ unlines rest))

126 runIO $ copyFile fb fn

@@ -193,7 +193,7 @@ makeCase fn updatefile l n

193 case findSubstr ('?':n) line of

194 Just (before, pos, after) ->

195 [before ++ (if b then "(" else "") ++ "case _ of",

196− take (pos + (if b then 6 else 5)) (repeat ' ') ++

196+ take (pos + (if b then 6 else 5)) (repeat ' ') ++

197 "case_val => ?" ++ n ++ (if b then ")" else "")

198 ++ after]

199 Nothing -> fail "No such metavariable"

@@ -208,7 +208,7 @@ makeCase fn updatefile l n

208

209 findSubstr n xs = findSubstr' [] 0 n xs

210

211− findSubstr' acc i n xs | take (length n) xs == n

211+ findSubstr' acc i n xs | take (length n) xs == n

212 = Just (reverse acc, i, drop (length n) xs)

213 findSubstr' acc i n [] = Nothing

214 findSubstr' acc i n (x : xs) = findSubstr' (x : acc) (i + 1) n xs

@@ -217,7 +217,7 @@ makeCase fn updatefile l n

217

218

219

220−doProofSearch :: FilePath -> Bool -> Bool ->

220+doProofSearch :: FilePath -> Bool -> Bool ->

221 Int -> Name -> [Name] -> Maybe Int -> Idris ()

222doProofSearch fn updatefile rec l n hints Nothing

223 = doProofSearch fn updatefile rec l n hints (Just 20)

@@ -230,7 +230,7 @@ doProofSearch fn updatefile rec l n hints (Just depth)

230 [] -> return n

231 ns -> ierror (CantResolveAlts ns)

232 i <- getIState

233− let (top, envlen, psnames, _)

233+ let (top, envlen, psnames, _)

234 = case lookup mn (idris_metavars i) of

235 Just (t, e, ns, False) -> (t, e, ns, False)

236 _ -> (Nothing, 0, [], True)

@@ -281,7 +281,7 @@ updateMeta ('?':cs) n new

281 (mv, []) -> if (mv == n) then new else '?' : mv

282updateMeta ('=':'>':cs) n new = '=':'>':updateMeta cs n new

283updateMeta ('=':cs) n new = '=':updateMeta cs n new

284−updateMeta (c:cs) n new

284+updateMeta (c:cs) n new

285 = c : updateMeta cs n new

286updateMeta [] n new = ""

287

@@ -296,7 +296,7 @@ guessBrackets brack ('?':cs) n new

296guessBrackets brack ('=':'>':cs) n new = guessBrackets False cs n new

297guessBrackets brack ('-':'>':cs) n new = guessBrackets False cs n new

298guessBrackets brack ('=':cs) n new = guessBrackets False cs n new

299−guessBrackets brack (c:cs) n new

299+guessBrackets brack (c:cs) n new

300 = guessBrackets (brack || not (isSpace c)) cs n new

301guessBrackets brack [] n new = ""

302

@@ -308,7 +308,7 @@ checkProv line n = isProv' False line n

308 isProv' _ ('}':cs) n = isProv' True cs n

309 isProv' p (_:cs) n = isProv' p cs n

310 isProv' _ [] n = False

311−

311+

312addBracket False new = new

313addBracket True new@('(':xs) | last xs == ')' = new

314addBracket True new | any isSpace new = '(' : new ++ ")"

@@ -322,7 +322,7 @@ makeLemma fn updatefile l n

322

323 -- if the name is in braces, rather than preceded by a ?, treat it

324 -- as a lemma in a provisional definition

325−

325+

326 let isProv = checkProv tyline (show n)

327

328 ctxt <- getContext

@@ -339,7 +339,7 @@ makeLemma fn updatefile l n

339 let skip = guessImps i (tt_ctxt i) mty

340 let classes = guessClasses i (tt_ctxt i) mty

341

342− let lem = show n ++ " : " ++

342+ let lem = show n ++ " : " ++

343 constraints i classes mty ++

344 showTmOpts (defaultPPOption { ppopt_pinames = True })

345 (stripMNBind skip margs (delab i mty))

@@ -379,14 +379,14 @@ makeLemma fn updatefile l n

379 where getIndent s = length (takeWhile isSpace s)

380

381 appArgs skip 0 _ = ""

382− appArgs skip i (Bind n@(UN c) (Pi _ _ _) sc)

382+ appArgs skip i (Bind n@(UN c) (Pi _ _ _) sc)

383 | (thead c /= '_' && n `notElem` skip)

384 = " " ++ show n ++ appArgs skip (i - 1) sc

385 appArgs skip i (Bind _ (Pi _ _ _) sc) = appArgs skip (i - 1) sc

386 appArgs skip i _ = ""

387

388 stripMNBind _ args t | args <= 0 = t

389− stripMNBind skip args (PPi b n@(UN c) _ ty sc)

389+ stripMNBind skip args (PPi b n@(UN c) _ ty sc)

390 | n `notElem` skip ||

391 take 4 (str c) == "__pi" -- keep in type, but not in app

392 = PPi b n NoFC ty (stripMNBind skip (args - 1) sc)

@@ -399,7 +399,7 @@ makeLemma fn updatefile l n

399 constraints i ns ty = "(" ++ showSep ", " (showConstraints i ns ty) ++ ") => "

400

401 showConstraints i ns (Bind n (Pi _ ty _) sc)

402− | n `elem` ns = show (delab i ty) :

402+ | n `elem` ns = show (delab i ty) :

403 showConstraints i ns (substV (P Bound n Erased) sc)

404 | otherwise = showConstraints i ns (substV (P Bound n Erased) sc)

405 showConstraints _ _ _ = []

@@ -410,10 +410,10 @@ makeLemma fn updatefile l n

410 -- Also, make type class instances implicit

411 guessImps :: IState -> Context -> Term -> [Name]

412 -- machine names aren't lifted

413− guessImps ist ctxt (Bind n@(MN _ _) (Pi _ ty _) sc)

413+ guessImps ist ctxt (Bind n@(MN _ _) (Pi _ ty _) sc)

414 = n : guessImps ist ctxt sc

415 guessImps ist ctxt (Bind n (Pi _ ty _) sc)

416− | guarded ctxt n (substV (P Bound n Erased) sc)

416+ | guarded ctxt n (substV (P Bound n Erased) sc)

417 = n : guessImps ist ctxt sc

418 | isClass ist ty

419 = n : guessImps ist ctxt sc

@@ -421,11 +421,11 @@ makeLemma fn updatefile l n

421 | ignoreName n = n : guessImps ist ctxt sc

422 | otherwise = guessImps ist ctxt sc

423 guessImps ist ctxt _ = []

424−

424+

425 paramty (TType _) = True

426 paramty (Bind _ (Pi _ (TType _) _) sc) = paramty sc

427 paramty _ = False

428−

428+

429 -- TMP HACK unusable name so don't lift

430 ignoreName n = case show n of

431 "_aX" -> True

@@ -444,7 +444,7 @@ makeLemma fn updatefile l n

444 Just _ -> True

445 _ -> False

446 | otherwise = False

447−

447+

448 isParamClass ist t

449 | (P _ n _, args) <- unApply t

450 = case lookupCtxtExact n (idris_classes ist) of

@@ -460,14 +460,14 @@ makeLemma fn updatefile l n

460 isConName f ctxt = any (guarded ctxt n) args

461-- guarded ctxt n (Bind (UN cn) (Pi t) sc) -- ignore shadows

462-- | thead cn /= '_' = guarded ctxt n t || guarded ctxt n sc

463− guarded ctxt n (Bind _ (Pi _ t _) sc)

463+ guarded ctxt n (Bind _ (Pi _ t _) sc)

464 = guarded ctxt n t || guarded ctxt n sc

465 guarded ctxt n _ = False

466

467 blank = all isSpace

468

469 addLem before tyline lem lem_app later

470− = let (bef_end, blankline : bef_start)

470+ = let (bef_end, blankline : bef_start)

471 = case span (not . blank) (reverse before) of

472 (bef, []) -> (bef, "" : [])

473 x -> x

@@ -481,6 +481,6 @@ makeLemma fn updatefile l n

481 = case span (not . blank) later of

482 (bef, []) -> (bef, "" : [])

483 x -> x in

484− unlines $ before ++ tyline :

484+ unlines $ before ++ tyline :

485 (later_bef ++ [blankline, lem_app, blankline] ++

486 later_end)

src/Idris/Parser.hs+12−12

@@ -1,10 +1,10 @@

1{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards #-}

2{-# OPTIONS_GHC -O0 #-}

3module Idris.Parser(module Idris.Parser,

4− module Idris.ParseExpr,

4+ module Idris.Parser.Expr,

5− module Idris.ParseData,

5+ module Idris.Parser.Data,

6− module Idris.ParseHelpers,

6+ module Idris.Parser.Helpers,

7− module Idris.ParseOps) where

7+ module Idris.Parser.Ops) where

9import Prelude hiding (pi)

@@ -35,10 +35,10 @@ import Idris.Unlit

35import Idris.Providers

36import Idris.Output

38−import Idris.ParseHelpers

38+import Idris.Parser.Helpers

39−import Idris.ParseOps

39+import Idris.Parser.Ops

40−import Idris.ParseExpr

40+import Idris.Parser.Expr

41−import Idris.ParseData

41+import Idris.Parser.Data

43import Idris.Docstrings hiding (Unchecked)

@@ -211,7 +211,7 @@ internalDecl syn

211 declBody continue)

212 <|> fail "End of readable input"

213 where declBody :: Bool -> IdrisParser [PDecl]

214− declBody b =

214+ declBody b =

215 try (instance_ True syn)

216 <|> declBody' b

217 <|> using_ syn

@@ -879,7 +879,7 @@ class_ syn = do (doc, argDocs, acc)

879 where

880 fundeps :: IdrisParser [(Name, FC)]

881 fundeps = do lchar '|'; sepBy name (lchar ',')

882−

882+

883 classKeyword :: IdrisParser ()

884 classKeyword = reservedHL "interface"

885 <|> do reservedHL "class"

@@ -906,7 +906,7 @@ InstanceName ::= '[' Name ']';

906@

907-}

908instance_ :: Bool -> SyntaxInfo -> IdrisParser [PDecl]

909−instance_ kwopt syn

909+instance_ kwopt syn

910 = do acc <- accessibility

911 (doc, argDocs)

912 <- try (docstring syn <* if kwopt then optional instanceKeyword

@@ -1361,7 +1361,7 @@ directive syn = do try (lchar '%' *> reserved "lib")

1361 return [PDirective (DAutoImplicits b)]

1362 <?> "directive"

1363 where on_off = do reserved "on"; return True

1364− <|> do reserved "off"; return False

1364+ <|> do reserved "off"; return False

1365

1366pLangExt :: IdrisParser LanguageExt

1367pLangExt = (reserved "TypeProviders" >> return TypeProviders)

src/Idris/ParseData.hs → src/Idris/Parser/Data.hsrenamed+4−4

@@ -1,5 +1,5 @@

1{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards #-}

2−module Idris.ParseData where

2+module Idris.Parser.Data where

4import Prelude hiding (pi)

@@ -12,9 +12,9 @@ import qualified Text.Parser.Char as Chr

12import qualified Text.Parser.Token.Highlight as Hi

14import Idris.AbsSyntax

15−import Idris.ParseHelpers

15+import Idris.Parser.Helpers

16−import Idris.ParseOps

16+import Idris.Parser.Ops

17−import Idris.ParseExpr

17+import Idris.Parser.Expr

18import Idris.DSL

20import Idris.Core.TT

src/Idris/ParseExpr.hs → src/Idris/Parser/Expr.hsrenamed+13−14

@@ -1,5 +1,5 @@

1{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards, TupleSections #-}

2−module Idris.ParseExpr where

2+module Idris.Parser.Expr where

4import Prelude hiding (pi)

@@ -12,8 +12,8 @@ import qualified Text.Parser.Char as Chr

12import qualified Text.Parser.Token.Highlight as Hi

14import Idris.AbsSyntax

15−import Idris.ParseHelpers

15+import Idris.Parser.Helpers

16−import Idris.ParseOps

16+import Idris.Parser.Ops

17import Idris.DSL

19import Idris.Core.TT

@@ -161,7 +161,7 @@ extension syn ns rules =

161 extensionSymbol (Symbol s) = do fc <- symbolFC s

162 highlightP fc AnnKeyword

163 return Nothing

164−

164+

165 flatten :: PTerm -> PTerm -- flatten application

166 flatten (PApp fc (PApp _ f as) bs) = flatten (PApp fc f (as ++ bs))

167 flatten t = t

@@ -252,7 +252,7 @@ updateSynMatch = update

252

253 updTacImp ns (TacImp o st scr) = TacImp o st (update ns scr)

254 updTacImp _ x = x

255−

255+

256 dropn :: Name -> [(Name, a)] -> [(Name, a)]

257 dropn n [] = []

258 dropn n ((x,t) : xs) | n == x = xs

@@ -476,7 +476,7 @@ bracketed' open syn =

476 <|> try (do l <- simpleExpr syn

477 op <- option Nothing (do o <- operator

478 lchar ')'

479− return (Just o))

479+ return (Just o))

480 fc0 <- getFC

481 case op of

482 Nothing -> bracketedExpr syn open l

@@ -584,7 +584,7 @@ runElab syn = do (FC fn (sl, sc) kwEnd) <- try (lchar '%' *> reservedFC "runElab

584 return $ PRunElab fc tm (syn_namespace syn)

585 <?> "new-style tactics expression"

586

587−{- | Parses a disambiguation expression

587+{- | Parses a disambiguation expression

588Disamb ::=

589 '%' 'disamb' NameList Expr

590 ;

@@ -1006,7 +1006,7 @@ Pi' ::=

1006@

1007 -}

1008

1009−bindsymbol opts st syn

1009+bindsymbol opts st syn

1010 = do symbol "->"

1011 return (Exp opts st False)

1012

@@ -1015,7 +1015,7 @@ explicitPi opts st syn

1015 binder <- bindsymbol opts st syn

1016 sc <- expr syn

1017 return (bindList (PPi binder) xt sc)

1018−

1018+

1019autoImplicit opts st syn

1020 = do kw <- reservedFC "auto"

1021 when (st == Static) $ fail "auto implicits can not be static"

@@ -1025,7 +1025,7 @@ autoImplicit opts st syn

1025 sc <- expr syn

1026 highlightP kw AnnKeyword

1027 return (bindList (PPi

1028− (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing [] []]))) xt sc)

1028+ (TacImp [] Dynamic (PTactics [ProofSearch True True 100 Nothing [] []]))) xt sc)

1029

1030defaultImplicit opts st syn = do

1031 kw <- reservedFC "default"

@@ -1051,7 +1051,7 @@ normalImplicit opts st syn = do

1051 constraint)

1052 else (Imp opts st False (Just (Impl False False)),

1053 Imp opts st False (Just (Impl True False)))

1054− return (bindList (PPi im) xt

1054+ return (bindList (PPi im) xt

1055 (bindList (PPi cl) cs sc))

1056

1057implicitPi opts st syn =

@@ -1443,7 +1443,7 @@ data TacticArg = NameTArg -- ^ Names: n1, n2, n3, ... n

1443-- https://github.com/idris-lang/Idris-dev/issues/1766

1444-- | A list of available tactics and their argument requirements

1445tactics :: [([String], Maybe TacticArg, SyntaxInfo -> IdrisParser PTactic)]

1446−tactics =

1446+tactics =

1447 [ (["intro"], Nothing, const $ -- FIXME syntax for intro (fresh name)

1448 do ns <- sepBy (spaced (fst <$> name)) (lchar ','); return $ Intro ns)

1449 , noArgs ["intros"] Intros

@@ -1527,7 +1527,7 @@ tactics =

1527 imp :: IdrisParser Bool

1528 imp = do lchar '?'; return False

1529 <|> do lchar '_'; return True

1530−

1530+

1531

1532tactic :: SyntaxInfo -> IdrisParser PTactic

1533tactic syn = choice [ do choice (map reserved names); parser syn

@@ -1550,4 +1550,3 @@ fullTactic :: SyntaxInfo -> IdrisParser PTactic

1550fullTactic syn = do t <- tactic syn

1551 eof

1552 return t

1553−

src/Idris/ParseHelpers.hs → src/Idris/Parser/Helpers.hsrenamed+7−7

@@ -2,7 +2,7 @@

2#if !(MIN_VERSION_base(4,8,0))

3{-# LANGUAGE OverlappingInstances #-}

4#endif

5−module Idris.ParseHelpers where

5+module Idris.Parser.Helpers where

7import Prelude hiding (pi)

@@ -254,7 +254,7 @@ idrisStyle = IdentifierStyle _styleName _styleStart _styleLetter _styleReserved

254 "case", "of", "total", "partial", "mutual",

255 "infix", "infixl", "infixr", "rewrite",

256 "where", "with", "syntax", "proof", "postulate",

257− "using", "namespace", "class", "instance",

257+ "using", "namespace", "class", "instance",

258 "interface", "implementation", "parameters",

259 "public", "private", "export", "abstract", "implicit",

260 "quoteGoal", "constructor",

@@ -621,22 +621,22 @@ notOpenBraces = do ist <- get

621

622{- | Parses an accessibilty modifier (e.g. public, private) -}

623accessibility' :: IdrisParser Accessibility

624−accessibility'

624+accessibility'

625− = do reserved "public";

625+ = do reserved "public";

626 gotexp <- optional (reserved "export")

627 case gotexp of

628 Just _ -> return ()

629 Nothing -> do

630 ist <- get

631 fc <- getFC

632− put ist { parserWarnings =

632+ put ist { parserWarnings =

633 (fc, Msg "'public' is deprecated. Use 'public export' instead.")

634 : parserWarnings ist }

635 return Public

636− <|> do reserved "abstract";

636+ <|> do reserved "abstract";

637 ist <- get

638 fc <- getFC

639− put ist { parserWarnings =

639+ put ist { parserWarnings =

640 (fc, Msg "The 'abstract' keyword is deprecated. Use 'export' instead.")

641 : parserWarnings ist }

642 return Frozen

src/Idris/ParseOps.hs → src/Idris/Parser/Ops.hsrenamed+2−3

@@ -1,5 +1,5 @@

1{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards #-}

2−module Idris.ParseOps where

2+module Idris.Parser.Ops where

4import Prelude hiding (pi)

@@ -12,7 +12,7 @@ import qualified Text.Parser.Char as Chr

12import qualified Text.Parser.Token.Highlight as Hi

14import Idris.AbsSyntax

15−import Idris.ParseHelpers

15+import Idris.Parser.Helpers

17import Idris.Core.TT

@@ -170,4 +170,3 @@ fixityType = do reserved "infixl"; return Infixl

170 <|> do reserved "infix"; return InfixN

171 <|> do reserved "prefix"; return PrefixN

172 <?> "fixity type"

173−

src/Idris/REPL.hs+2−2

@@ -8,8 +8,7 @@ module Idris.REPL(getClient, getPkg, getPkgCheck, getPkgClean, getPkgMkDoc,

8import Idris.AbsSyntax

9import Idris.ASTUtils

10import Idris.Apropos (apropos, aproposModules)

11−import Idris.REPLParser

11+import Idris.REPL.Parser

12−import Idris.ElabDecls

13import Idris.Erasure

12import Idris.Erasure

14import Idris.Error

13import Idris.Error

15import Idris.IBC

14import Idris.IBC

@@ -39,6 +38,7 @@ import Idris.IBC (loadPkgIndex, writePkgIndex)

40import Idris.REPL.Browse (namesInNS, namespacesInNS)

39import Idris.REPL.Browse (namesInNS, namespacesInNS)

41+import Idris.ElabDecls

42import Idris.Elab.Type

43import Idris.Elab.Clause

44import Idris.Elab.Data

src/Idris/REPLParser.hs → src/Idris/REPL/Parser.hsrenamed+1−1

@@ -1,5 +1,5 @@

2−module Idris.REPLParser (parseCmd, help, allHelp, setOptions) where

2+module Idris.REPL.Parser (parseCmd, help, allHelp, setOptions) where

4import System.FilePath ((</>))

5import System.Console.ANSI (Color(..))

src/Pkg/PParser.hs+1−1

@@ -9,7 +9,7 @@ import qualified Text.PrettyPrint.ANSI.Leijen as PP

9import Idris.Core.TT

10import Idris.REPL

11import Idris.AbsSyntaxTree

12−import Idris.ParseHelpers hiding (stringLiteral)

12+import Idris.Parser.Helpers hiding (stringLiteral)

13import Idris.CmdOptions

15import Control.Monad.State.Strict