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

idris.cabal+6−6

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

876876 , Idris.Elab.Transform

877877 , Idris.Elab.Value

878878 , Idris.Elab.Term

879+ , Idris.Elab.Quasiquote

879880

880881 , Idris.REPL.Browse

881882

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

896897 , Idris.Docs

897898 , Idris.Docstrings

898899 , Idris.ElabDecls

899− , Idris.ElabQuasiquote

900900 , Idris.Erasure

901901 , Idris.Error

902902 , Idris.ErrReverse

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

909909 , Idris.Interactive

910910 , Idris.Output

911911 , Idris.Parser

912− , Idris.ParseHelpers

913− , Idris.ParseOps

914− , Idris.ParseExpr

915− , Idris.ParseData

912+ , Idris.Parser.Helpers

913+ , Idris.Parser.Ops

914+ , Idris.Parser.Expr

915+ , Idris.Parser.Data

916916 , Idris.PartialEval

917917 , Idris.Primitives

918918 , Idris.ProofSearch

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

920920 , Idris.Providers

921921 , Idris.Reflection

922922 , Idris.REPL

923− , Idris.REPLParser

923+ , Idris.REPL.Parser

924924 , Idris.Transforms

925925 , Idris.TypeSearch

926926 , Idris.Unlit

src/Idris/Completion.hs+6−6

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

99import Idris.Help

1010import Idris.Imports (installedPackages)

1111import Idris.Colours

12−import Idris.ParseHelpers(opChars)

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

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

15−import Idris.REPLParser (allHelp, setOptions)

12+import Idris.Parser.Helpers(opChars)

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

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

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

1616import Control.Monad.State.Strict

1717

1818import Data.List

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

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

2727

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

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

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

3030 , name <- names ]

3131tactics = map fst tacticArgs

3232

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

4848 let ctxt = tt_ctxt i

4949 return . nub $

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

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

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

5252

5353metavars :: Idris [String]

5454metavars = 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

22

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

44import Idris.Core.TT

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

171171extractUnquotes n (PConstSugar fc tm)

172172 = extractUnquotes n tm

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

174−

175−

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

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

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

1818import IRTS.Lang

1919

20−import Idris.ParseExpr (tryFullExpr)

20+import Idris.Parser.Expr (tryFullExpr)

2121

2222import Idris.Elab.Type

2323import Idris.Elab.Data

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

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

2020import Idris.Core.WHNF (whnf)

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

2222import Idris.ErrReverse (errReverse)

23−import Idris.ElabQuasiquote (extractUnquotes)

23+import Idris.Elab.Quasiquote (extractUnquotes)

2424import Idris.Elab.Utils

2525import Idris.Reflection

2626import qualified Util.Pretty as U

src/Idris/IdrisDoc.hs+1−1

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

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

1111 Accessibility (..), isDConName, isFnName,

1212 isTConName)

13−import Idris.ParseHelpers (opChars)

13+import Idris.Parser.Helpers (opChars)

1414import Idris.AbsSyntax

1515import Idris.Docs

1616import Idris.Docstrings (nullDocstring)

src/Idris/Interactive.hs+22−22

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

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

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

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

79−

79+

8080 getAppName (PApp _ r _) = getAppName r

8181 getAppName (PRef _ _ r) = r

8282 getAppName (PTyped n _) = getAppName n

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

120120 if updatefile

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

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

123− ++ extras ++

123+ ++ extras ++

124124 (if null extras then ""

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

126126 runIO $ copyFile fb fn

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

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

194194 Just (before, pos, after) ->

195195 [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 ' ') ++

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

198198 ++ after]

199199 Nothing -> fail "No such metavariable"

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

208208

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

210210

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

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

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

213213 findSubstr' acc i n [] = Nothing

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

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

217217

218218

219219

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

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

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

222222doProofSearch fn updatefile rec l n hints Nothing

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

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

230230 [] -> return n

231231 ns -> ierror (CantResolveAlts ns)

232232 i <- getIState

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

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

234234 = case lookup mn (idris_metavars i) of

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

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

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

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

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

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

284−updateMeta (c:cs) n new

284+updateMeta (c:cs) n new

285285 = c : updateMeta cs n new

286286updateMeta [] n new = ""

287287

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

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

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

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

299−guessBrackets brack (c:cs) n new

299+guessBrackets brack (c:cs) n new

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

301301guessBrackets brack [] n new = ""

302302

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

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

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

310310 isProv' _ [] n = False

311−

311+

312312addBracket False new = new

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

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

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

322322

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

324324 -- as a lemma in a provisional definition

325−

325+

326326 let isProv = checkProv tyline (show n)

327327

328328 ctxt <- getContext

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

339339 let skip = guessImps i (tt_ctxt i) mty

340340 let classes = guessClasses i (tt_ctxt i) mty

341341

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

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

343343 constraints i classes mty ++

344344 showTmOpts (defaultPPOption { ppopt_pinames = True })

345345 (stripMNBind skip margs (delab i mty))

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

379379 where getIndent s = length (takeWhile isSpace s)

380380

381381 appArgs skip 0 _ = ""

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

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

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

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

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

386386 appArgs skip i _ = ""

387387

388388 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)

390390 | n `notElem` skip ||

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

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

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

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

400400

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

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

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

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

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

405405 showConstraints _ _ _ = []

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

410410 -- Also, make type class instances implicit

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

412412 -- 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)

414414 = n : guessImps ist ctxt sc

415415 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)

417417 = n : guessImps ist ctxt sc

418418 | isClass ist ty

419419 = n : guessImps ist ctxt sc

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

421421 | ignoreName n = n : guessImps ist ctxt sc

422422 | otherwise = guessImps ist ctxt sc

423423 guessImps ist ctxt _ = []

424−

424+

425425 paramty (TType _) = True

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

427427 paramty _ = False

428−

428+

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

430430 ignoreName n = case show n of

431431 "_aX" -> True

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

444444 Just _ -> True

445445 _ -> False

446446 | otherwise = False

447−

447+

448448 isParamClass ist t

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

450450 = case lookupCtxtExact n (idris_classes ist) of

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

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

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

462462-- | 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)

464464 = guarded ctxt n t || guarded ctxt n sc

465465 guarded ctxt n _ = False

466466

467467 blank = all isSpace

468468

469469 addLem before tyline lem lem_app later

470− = let (bef_end, blankline : bef_start)

470+ = let (bef_end, blankline : bef_start)

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

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

473473 x -> x

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

481481 = case span (not . blank) later of

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

483483 x -> x in

484− unlines $ before ++ tyline :

484+ unlines $ before ++ tyline :

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

486486 later_end)

src/Idris/Parser.hs+12−12

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

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

22{-# OPTIONS_GHC -O0 #-}

33module Idris.Parser(module Idris.Parser,

4− module Idris.ParseExpr,

5− module Idris.ParseData,

6− module Idris.ParseHelpers,

7− module Idris.ParseOps) where

4+ module Idris.Parser.Expr,

5+ module Idris.Parser.Data,

6+ module Idris.Parser.Helpers,

7+ module Idris.Parser.Ops) where

88

99import Prelude hiding (pi)

1010

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

3535import Idris.Providers

3636import Idris.Output

3737

38−import Idris.ParseHelpers

39−import Idris.ParseOps

40−import Idris.ParseExpr

41−import Idris.ParseData

38+import Idris.Parser.Helpers

39+import Idris.Parser.Ops

40+import Idris.Parser.Expr

41+import Idris.Parser.Data

4242

4343import Idris.Docstrings hiding (Unchecked)

4444

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

211211 declBody continue)

212212 <|> fail "End of readable input"

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

214− declBody b =

214+ declBody b =

215215 try (instance_ True syn)

216216 <|> declBody' b

217217 <|> using_ syn

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

879879 where

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

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

882−

882+

883883 classKeyword :: IdrisParser ()

884884 classKeyword = reservedHL "interface"

885885 <|> do reservedHL "class"

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

906906@

907907-}

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

909−instance_ kwopt syn

909+instance_ kwopt syn

910910 = do acc <- accessibility

911911 (doc, argDocs)

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

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

13611361 return [PDirective (DAutoImplicits b)]

13621362 <?> "directive"

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

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

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

13651365

13661366pLangExt :: IdrisParser LanguageExt

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

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

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

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

2−module Idris.ParseData where

2+module Idris.Parser.Data where

33

44import Prelude hiding (pi)

55

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

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

1313

1414import Idris.AbsSyntax

15−import Idris.ParseHelpers

16−import Idris.ParseOps

17−import Idris.ParseExpr

15+import Idris.Parser.Helpers

16+import Idris.Parser.Ops

17+import Idris.Parser.Expr

1818import Idris.DSL

1919

2020import Idris.Core.TT

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

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

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

2−module Idris.ParseExpr where

2+module Idris.Parser.Expr where

33

44import Prelude hiding (pi)

55

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

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

1313

1414import Idris.AbsSyntax

15−import Idris.ParseHelpers

16−import Idris.ParseOps

15+import Idris.Parser.Helpers

16+import Idris.Parser.Ops

1717import Idris.DSL

1818

1919import Idris.Core.TT

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

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

162162 highlightP fc AnnKeyword

163163 return Nothing

164−

164+

165165 flatten :: PTerm -> PTerm -- flatten application

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

167167 flatten t = t

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

252252

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

254254 updTacImp _ x = x

255−

255+

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

257257 dropn n [] = []

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

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

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

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

478478 lchar ')'

479− return (Just o))

479+ return (Just o))

480480 fc0 <- getFC

481481 case op of

482482 Nothing -> bracketedExpr syn open l

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

584584 return $ PRunElab fc tm (syn_namespace syn)

585585 <?> "new-style tactics expression"

586586

587−{- | Parses a disambiguation expression

587+{- | Parses a disambiguation expression

588588Disamb ::=

589589 '%' 'disamb' NameList Expr

590590 ;

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

10061006@

10071007 -}

10081008

1009−bindsymbol opts st syn

1009+bindsymbol opts st syn

10101010 = do symbol "->"

10111011 return (Exp opts st False)

10121012

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

10151015 binder <- bindsymbol opts st syn

10161016 sc <- expr syn

10171017 return (bindList (PPi binder) xt sc)

1018−

1018+

10191019autoImplicit opts st syn

10201020 = do kw <- reservedFC "auto"

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

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

10251025 sc <- expr syn

10261026 highlightP kw AnnKeyword

10271027 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)

10291029

10301030defaultImplicit opts st syn = do

10311031 kw <- reservedFC "default"

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

10511051 constraint)

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

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

1054− return (bindList (PPi im) xt

1054+ return (bindList (PPi im) xt

10551055 (bindList (PPi cl) cs sc))

10561056

10571057implicitPi opts st syn =

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

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

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

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

1446−tactics =

1446+tactics =

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

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

14491449 , noArgs ["intros"] Intros

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

15271527 imp :: IdrisParser Bool

15281528 imp = do lchar '?'; return False

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

1530−

1530+

15311531

15321532tactic :: SyntaxInfo -> IdrisParser PTactic

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

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

15501550fullTactic syn = do t <- tactic syn

15511551 eof

15521552 return t

1553−

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

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

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

33{-# LANGUAGE OverlappingInstances #-}

44#endif

5−module Idris.ParseHelpers where

5+module Idris.Parser.Helpers where

66

77import Prelude hiding (pi)

88

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

254254 "case", "of", "total", "partial", "mutual",

255255 "infix", "infixl", "infixr", "rewrite",

256256 "where", "with", "syntax", "proof", "postulate",

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

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

258258 "interface", "implementation", "parameters",

259259 "public", "private", "export", "abstract", "implicit",

260260 "quoteGoal", "constructor",

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

621621

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

623623accessibility' :: IdrisParser Accessibility

624−accessibility'

625− = do reserved "public";

624+accessibility'

625+ = do reserved "public";

626626 gotexp <- optional (reserved "export")

627627 case gotexp of

628628 Just _ -> return ()

629629 Nothing -> do

630630 ist <- get

631631 fc <- getFC

632− put ist { parserWarnings =

632+ put ist { parserWarnings =

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

634634 : parserWarnings ist }

635635 return Public

636− <|> do reserved "abstract";

636+ <|> do reserved "abstract";

637637 ist <- get

638638 fc <- getFC

639− put ist { parserWarnings =

639+ put ist { parserWarnings =

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

641641 : parserWarnings ist }

642642 return Frozen

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

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

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

2−module Idris.ParseOps where

2+module Idris.Parser.Ops where

33

44import Prelude hiding (pi)

55

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

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

1313

1414import Idris.AbsSyntax

15−import Idris.ParseHelpers

15+import Idris.Parser.Helpers

1616

1717import Idris.Core.TT

1818

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

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

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

172172 <?> "fixity type"

173−

src/Idris/REPL.hs+2−2

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

88import Idris.AbsSyntax

99import Idris.ASTUtils

1010import Idris.Apropos (apropos, aproposModules)

11−import Idris.REPLParser

12−import Idris.ElabDecls

11+import Idris.REPL.Parser

1312import Idris.Erasure

1413import Idris.Error

1514import Idris.IBC

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

3938

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

4140

41+import Idris.ElabDecls

4242import Idris.Elab.Type

4343import Idris.Elab.Clause

4444import Idris.Elab.Data

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

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

11

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

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

33

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

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

src/Pkg/PParser.hs+1−1

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

99import Idris.Core.TT

1010import Idris.REPL

1111import Idris.AbsSyntaxTree

12−import Idris.ParseHelpers hiding (stringLiteral)

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

1313import Idris.CmdOptions

1414

1515import Control.Monad.State.Strict