e95b013 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Made Parser submodules actual submodules.

commite95b013a10f3e8ce8f5cae0aaecfd6edc1808caf authorJan de Muijnck-Hughes <jfdm@st-andrews.ac.uk> dateSat 6 Feb 2016, 20:19 (11 years ago) parentc292d12

10 files changed+46−48

compare with master

unifiedsplit

idris.cabal+4−4 src/Idris/Completion.hs+5−5 src/Idris/Elab/Record.hs+1−1 src/Idris/IdrisDoc.hs+1−1 src/Idris/Parser.hs+8−8 src/Idris/ParseData.hs → src/Idris/Parser/Data.hs+4−4 src/Idris/ParseExpr.hs → src/Idris/Parser/Expr.hs+13−14 src/Idris/ParseHelpers.hs → src/Idris/Parser/Helpers.hs+7−7 src/Idris/ParseOps.hs → src/Idris/Parser/Ops.hs+2−3 src/Pkg/PParser.hs+1−1

idris.cabal+4−4

@@ -904,10 +904,10 @@ Library

904904 , Idris.Interactive

905905 , Idris.Output

906906 , Idris.Parser

907− , Idris.ParseHelpers

908− , Idris.ParseOps

909− , Idris.ParseExpr

910− , Idris.ParseData

907+ , Idris.Parser.Helpers

908+ , Idris.Parser.Ops

909+ , Idris.Parser.Expr

910+ , Idris.Parser.Data

911911 , Idris.PartialEval

912912 , Idris.Primitives

913913 , Idris.ProofSearch

src/Idris/Completion.hs+5−5

@@ -9,9 +9,9 @@ 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 (..))

12+import Idris.Parser.Helpers(opChars)

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

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

1515import Idris.REPL.Parser (allHelp, setOptions)

1616import Control.Monad.State.Strict

1717

@@ -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/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/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/Parser.hs+8−8

@@ -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

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

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

44import Prelude hiding (pi)

@@ -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

44import Prelude hiding (pi)

@@ -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

77import Prelude hiding (pi)

@@ -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

44import Prelude hiding (pi)

@@ -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/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