e95b013 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Made Parser submodules actual submodules.

e95b013Jan de Muijnck-Hughes11 years ago

idris.cabal+4−4

compare with master

unifiedsplit

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

904 , Idris.Interactive

905 , Idris.Output

906 , Idris.Parser

907− , Idris.ParseHelpers

907+ , Idris.Parser.Helpers

908− , Idris.ParseOps

908+ , Idris.Parser.Ops

909− , Idris.ParseExpr

909+ , Idris.Parser.Expr

910− , Idris.ParseData

910+ , Idris.Parser.Data

911 , Idris.PartialEval

912 , Idris.Primitives

913 , Idris.ProofSearch

src/Idris/Completion.hs+5−5

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

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

16import Control.Monad.State.Strict

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

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

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