631fc46 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Further splitting of Parser

631fc46Edwin Brady13 years ago

idris.cabal+1

compare with master

unifiedsplit

@@ -312,6 +312,7 @@ Executable idris

312 , Idris.ParseHelpers

313 , Idris.ParseOps

314 , Idris.ParseExpr

315+ , Idris.ParseData

315 , Idris.PartialEval

316 , Idris.PartialEval

316 , Idris.Primitives

317 , Idris.Primitives

317 , Idris.Prover

318 , Idris.Prover

src/Idris/ParseData.hsnew file+215

@@ -0,0 +1,215 @@

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

2+module Idris.ParseData where

4+import Prelude hiding (pi)

6+import Text.Trifecta.Delta

7+import Text.Trifecta hiding (span, stringLiteral, charLiteral, natural, symbol, char, string, whiteSpace)

8+import Text.Parser.LookAhead

9+import Text.Parser.Expression

10+import qualified Text.Parser.Token as Tok

11+import qualified Text.Parser.Char as Chr

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

13+

14+import Idris.AbsSyntax

15+import Idris.ParseHelpers

16+import Idris.ParseOps

17+import Idris.ParseExpr

18+import Idris.DSL

19+

20+import Core.TT

21+import Core.Evaluate

22+

23+import Control.Applicative

24+import Control.Monad

25+import Control.Monad.State.Strict

26+

27+import Data.Maybe

28+import qualified Data.List.Split as Spl

29+import Data.List

30+import Data.Monoid

31+import Data.Char

32+import qualified Data.HashSet as HS

33+import qualified Data.Text as T

34+import qualified Data.ByteString.UTF8 as UTF8

35+

36+{- |Parses a record type declaration

37+Record ::=

38+ DocComment Accessibility? 'record' FnName TypeSig 'where' OpenBlock Constructor KeepTerminator CloseBlock;

39+-}

40+record :: SyntaxInfo -> IdrisParser PDecl

41+record syn = do (doc, acc) <- try (do

42+ doc <- option "" (docComment '|')

43+ acc <- optional accessibility

44+ reserved "record"

45+ return (doc, acc))

46+ fc <- getFC

47+ tyn_in <- fnName

48+ lchar ':'

49+ ty <- typeExpr (allowImp syn)

50+ let tyn = expandNS syn tyn_in

51+ reserved "where"

52+ (cdoc, cn, cty, _) <- indentedBlockS (constructor syn)

53+ accData acc tyn [cn]

54+ let rsyn = syn { syn_namespace = show (nsroot tyn) :

55+ syn_namespace syn }

56+ let fns = getRecNames rsyn cty

57+ mapM_ (\n -> addAcc n acc) fns

58+ return $ PRecord doc rsyn fc tyn ty cdoc cn cty

59+ <?> "record type declaration"

60+ where

61+ getRecNames :: SyntaxInfo -> PTerm -> [Name]

62+ getRecNames syn (PPi _ n _ sc) = [expandNS syn n, expandNS syn (mkType n)]

63+ ++ getRecNames syn sc

64+ getRecNames _ _ = []

65+

66+ toFreeze :: Maybe Accessibility -> Maybe Accessibility

67+ toFreeze (Just Frozen) = Just Hidden

68+ toFreeze x = x

69+

70+{- | Parses data declaration type (normal or codata)

71+DataI ::= 'data' | 'codata';

72+-}

73+dataI :: IdrisParser Bool

74+dataI = do reserved "data"; return False

75+ <|> do reserved "codata"; return True

76+

77+{- | Parses a data type declaration

78+Data ::= DocComment? Accessibility? DataI FnName TypeSig ExplicitTypeDataRest?

79+ | DocComment? Accessibility? DataI FnName Name* DataRest?

80+ ;

81+Constructor' ::= Constructor KeepTerminator;

82+ExplicitTypeDataRest ::= 'where' OpenBlock Constructor'* CloseBlock;

83+

84+DataRest ::= '=' SimpleConstructorList Terminator

85+ | 'where'!

86+ ;

87+SimpleConstructorList ::=

88+ SimpleConstructor

89+ | SimpleConstructor '|' SimpleConstructorList

90+ ;

91+-}

92+data_ :: SyntaxInfo -> IdrisParser PDecl

93+data_ syn = do (doc, acc, co) <- try (do

94+ doc <- option "" (docComment '|')

95+ pushIndent

96+ acc <- optional accessibility

97+ co <- dataI

98+ return (doc, acc, co))

99+ fc <- getFC

100+ tyn_in <- fnName

101+ (do try (lchar ':')

102+ popIndent

103+ ty <- typeExpr (allowImp syn)

104+ let tyn = expandNS syn tyn_in

105+ option (PData doc syn fc co (PLaterdecl tyn ty)) (do

106+ reserved "where"

107+ cons <- indentedBlock (constructor syn)

108+ accData acc tyn (map (\ (_, n, _, _) -> n) cons)

109+ return $ PData doc syn fc co (PDatadecl tyn ty cons))) <|> (do

110+ args <- many name

111+ let ty = bindArgs (map (const PType) args) PType

112+ let tyn = expandNS syn tyn_in

113+ option (PData doc syn fc co (PLaterdecl tyn ty)) (do

114+ try (lchar '=') <|> do reserved "where"

115+ let kw = (if co then "co" else "") ++ "data "

116+ let n = show tyn_in ++ " "

117+ let s = kw ++ n

118+ let as = concat (intersperse " " $ map show args) ++ " "

119+ let ns = concat (intersperse " -> " $ map ((\x -> "(" ++ x ++ " : Type)") . show) args)

120+ let ss = concat (intersperse " -> " $ map (const "Type") args)

121+ let fix1 = s ++ as ++ " = ..."

122+ let fix2 = s ++ ": " ++ ns ++ " -> Type where\n ..."

123+ let fix3 = s ++ ": " ++ ss ++ " -> Type where\n ..."

124+ fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]

125+ cons <- sepBy1 (simpleConstructor syn) (lchar '|')

126+ terminator

127+ let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)

128+ cons' <- mapM (\ (doc, x, cargs, cfc) ->

129+ do let cty = bindArgs cargs conty

130+ return (doc, x, cty, cfc)) cons

131+ accData acc tyn (map (\ (_, n, _, _) -> n) cons')

132+ return $ PData doc syn fc co (PDatadecl tyn ty cons')))

133+ <?> "data type declaration"

134+ where

135+ mkPApp :: FC -> PTerm -> [PTerm] -> PTerm

136+ mkPApp fc t [] = t

137+ mkPApp fc t xs = PApp fc t (map pexp xs)

138+ bindArgs :: [PTerm] -> PTerm -> PTerm

139+ bindArgs xs t = foldr (PPi expl (MN 0 "t")) t xs

140+

141+

142+{- | Parses a type constructor declaration

143+ Constructor ::= DocComment? FnName TypeSig;

144+-}

145+constructor :: SyntaxInfo -> IdrisParser (String, Name, PTerm, FC)

146+constructor syn

147+ = do doc <- option "" (docComment '|')

148+ cn_in <- fnName; fc <- getFC

149+ let cn = expandNS syn cn_in

150+ lchar ':'

151+ ty <- typeExpr (allowImp syn)

152+ return (doc, cn, ty, fc)

153+ <?> "constructor"

154+

155+{- | Parses a constructor for simple discriminative union data types

156+ SimpleConstructor ::= FnName SimpleExpr* DocComment?

157+-}

158+simpleConstructor :: SyntaxInfo -> IdrisParser (String, Name, [PTerm], FC)

159+simpleConstructor syn

160+ = do cn_in <- fnName

161+ let cn = expandNS syn cn_in

162+ fc <- getFC

163+ args <- many (do notEndApp

164+ simpleExpr syn)

165+ doc <- option "" (docComment '^')

166+ return (doc, cn, args, fc)

167+ <?> "constructor"

168+

169+{- | Parses a dsl block declaration

170+DSL ::= 'dsl' FnName OpenBlock Overload'+ CloseBlock;

171+ -}

172+dsl :: SyntaxInfo -> IdrisParser PDecl

173+dsl syn = do reserved "dsl"

174+ n <- fnName

175+ bs <- indentedBlock (overload syn)

176+ let dsl = mkDSL bs (dsl_info syn)

177+ checkDSL dsl

178+ i <- get

179+ put (i { idris_dsls = addDef n dsl (idris_dsls i) })

180+ return (PDSL n dsl)

181+ <?> "dsl block declaration"

182+ where mkDSL :: [(String, PTerm)] -> DSL -> DSL

183+ mkDSL bs dsl = let var = lookup "variable" bs

184+ first = lookup "index_first" bs

185+ next = lookup "index_next" bs

186+ leto = lookup "let" bs

187+ lambda = lookup "lambda" bs in

188+ initDSL { dsl_var = var,

189+ index_first = first,

190+ index_next = next,

191+ dsl_lambda = lambda,

192+ dsl_let = leto }

193+

194+{- | Checks DSL for errors -}

195+-- FIXME: currently does nothing, check if DSL is really sane

196+checkDSL :: DSL -> IdrisParser ()

197+checkDSL dsl = return ()

198+

199+{- | Parses a DSL overload declaration

200+OverloadIdentifier ::= 'let' | Identifier;

201+Overload ::= OverloadIdentifier '=' Expr;

202+-}

203+overload :: SyntaxInfo -> IdrisParser (String, PTerm)

204+overload syn = do o <- identifier <|> do reserved "let"

205+ return "let"

206+ if o `notElem` overloadable

207+ then fail $ show o ++ " is not an overloading"

208+ else do

209+ lchar '='

210+ t <- expr syn

211+ return (o, t)

212+ <?> "dsl overload declaratioN"

213+ where overloadable = ["let","lambda","index_first","index_next","variable"]

214+

215+

src/Idris/ParseHelpers.hs+58

@@ -14,6 +14,7 @@ import qualified Text.Parser.Token.Highlight as Hi

14import Idris.AbsSyntax

16import Core.TT

17+import Core.Evaluate

18import Control.Applicative

19import Control.Applicative

19import Control.Monad

20import Control.Monad

@@ -401,3 +402,60 @@ notOpenBraces = do ist <- get

401 when (hasNothing $ brace_stack ist) $ fail "end of input"

402 when (hasNothing $ brace_stack ist) $ fail "end of input"

402 where hasNothing :: [Maybe a] -> Bool

403 where hasNothing :: [Maybe a] -> Bool

403 hasNothing = any isNothing

404 hasNothing = any isNothing

405+

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

407+accessibility :: IdrisParser Accessibility

408+accessibility = do reserved "public"; return Public

409+ <|> do reserved "abstract"; return Frozen

410+ <|> do reserved "private"; return Hidden

411+ <?> "accessibility modifier"

412+

413+-- | Adds accessibility option for function

414+addAcc :: Name -> Maybe Accessibility -> IdrisParser ()

415+addAcc n a = do i <- get

416+ put (i { hide_list = (n, a) : hide_list i })

417+

418+{- | Add accessbility option for data declarations

419+ (works for classes too - 'abstract' means the data/class is visible but members not) -}

420+accData :: Maybe Accessibility -> Name -> [Name] -> IdrisParser ()

421+accData (Just Frozen) n ns = do addAcc n (Just Frozen)

422+ mapM_ (\n -> addAcc n (Just Hidden)) ns

423+accData a n ns = do addAcc n a

424+ mapM_ (`addAcc` a) ns

425+

426+

427+{- * Error reporting helpers -}

428+{- | Error message with possible fixes list -}

429+fixErrorMsg :: String -> [String] -> String

430+fixErrorMsg msg fixes = msg ++ ", possible fixes:\n" ++ (concat $ intersperse "\n\nor\n\n" fixes)

431+

432+-- | Collect 'PClauses' with the same function name

433+collect :: [PDecl] -> [PDecl]

434+collect (c@(PClauses _ o _ _) : ds)

435+ = clauses (cname c) [] (c : ds)

436+ where clauses :: Maybe Name -> [PClause] -> [PDecl] -> [PDecl]

437+ clauses j@(Just n) acc (PClauses fc _ _ [PClause fc' n' l ws r w] : ds)

438+ | n == n' = clauses j (PClause fc' n' l ws r (collect w) : acc) ds

439+ clauses j@(Just n) acc (PClauses fc _ _ [PWith fc' n' l ws r w] : ds)

440+ | n == n' = clauses j (PWith fc' n' l ws r (collect w) : acc) ds

441+ clauses (Just n) acc xs = PClauses (fcOf c) o n (reverse acc) : collect xs

442+ clauses Nothing acc (x:xs) = collect xs

443+ clauses Nothing acc [] = []

444+

445+ cname :: PDecl -> Maybe Name

446+ cname (PClauses fc _ _ [PClause _ n _ _ _ _]) = Just n

447+ cname (PClauses fc _ _ [PWith _ n _ _ _ _]) = Just n

448+ cname (PClauses fc _ _ [PClauseR _ _ _ _]) = Nothing

449+ cname (PClauses fc _ _ [PWithR _ _ _ _]) = Nothing

450+ fcOf :: PDecl -> FC

451+ fcOf (PClauses fc _ _ _) = fc

452+collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds

453+collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds

454+collect (PNamespace ns ps : ds) = PNamespace ns (collect ps) : collect ds

455+collect (PClass doc f s cs n ps ds : ds')

456+ = PClass doc f s cs n ps (collect ds) : collect ds'

457+collect (PInstance f s cs n ps t en ds : ds')

458+ = PInstance f s cs n ps t en (collect ds) : collect ds'

459+collect (d : ds) = d : collect ds

460+collect [] = []

461+

src/Idris/ParseOps.hs+49

@@ -86,3 +86,52 @@ operatorFront = maybeWithNS (lchar '(' *> operator <* lchar ')') False []

86fnName :: IdrisParser Name

87fnName = try operatorFront <|> name <?> "function name"

89+{- | Parses a fixity declaration

90+

91+Fixity ::=

92+ FixityType Natural_t OperatorList Terminator

93+ ;

94+-}

95+fixity :: IdrisParser PDecl

96+fixity = do pushIndent

97+ f <- fixityType; i <- natural; ops <- sepBy1 operator (lchar ',')

98+ terminator

99+ let prec = fromInteger i

100+ istate <- get

101+ let infixes = idris_infixes istate

102+ let fs = map (Fix (f prec)) ops

103+ let redecls = map (alreadyDeclared infixes) fs

104+ let ill = filter (not . checkValidity) redecls

105+ if null ill

106+ then do put (istate { idris_infixes = nub $ sort (fs ++ infixes)

107+ , ibc_write = map IBCFix fs ++ ibc_write istate

108+ })

109+ fc <- getFC

110+ return (PFix fc (f prec) ops)

111+ else fail $ concatMap (\(f, (x:xs)) -> "Illegal redeclaration of fixity:\n\t\""

112+ ++ show f ++ "\" overrides \"" ++ show x ++ "\"") ill

113+ <?> "fixity declaration"

114+ where alreadyDeclared :: [FixDecl] -> FixDecl -> (FixDecl, [FixDecl])

115+ alreadyDeclared fs f = (f, filter ((extractName f ==) . extractName) fs)

116+

117+ checkValidity :: (FixDecl, [FixDecl]) -> Bool

118+ checkValidity (f, fs) = all (== f) fs

119+

120+ extractName :: FixDecl -> String

121+ extractName (Fix _ n) = n

122+

123+{- | Parses a fixity declaration type (i.e. infix or prefix, associtavity)

124+FixityType ::=

125+ 'infixl'

126+ | 'infixr'

127+ | 'infix'

128+ | 'prefix'

129+ ;

130+ -}

131+fixityType :: IdrisParser (Int -> Fixity)

132+fixityType = do reserved "infixl"; return Infixl

133+ <|> do reserved "infixr"; return Infixr

134+ <|> do reserved "infix"; return InfixN

135+ <|> do reserved "prefix"; return PrefixN

136+ <?> "fixity type"

137+

src/Idris/Parser.hs+3−287

@@ -1,6 +1,7 @@

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

2module Idris.Parser(module Idris.Parser,

3− module Idris.ParseExpr,

3+ module Idris.ParseExpr,

4+ module Idris.ParseData,

4 module Idris.ParseHelpers,

5 module Idris.ParseHelpers,

5 module Idris.ParseOps) where

6 module Idris.ParseOps) where

@@ -28,6 +29,7 @@ import Idris.Providers

28import Idris.ParseHelpers

29import Idris.ParseHelpers

29import Idris.ParseOps

30import Idris.ParseOps

30import Idris.ParseExpr

31import Idris.ParseExpr

32+import Idris.ParseData

32import Paths_idris

34import Paths_idris

@@ -62,25 +64,6 @@ import System.FilePath

62 RULE{n} = rule repeated n times

64 RULE{n} = rule repeated n times

63-}

65-}

65−-- | Adds accessibility option for function

66−addAcc :: Name -> Maybe Accessibility -> IdrisParser ()

67−addAcc n a = do i <- get

68− put (i { hide_list = (n, a) : hide_list i })

69−

70−{- | Add accessbility option for data declarations

71− (works for classes too - 'abstract' means the data/class is visible but members not) -}

72−accData :: Maybe Accessibility -> Name -> [Name] -> IdrisParser ()

73−accData (Just Frozen) n ns = do addAcc n (Just Frozen)

74− mapM_ (\n -> addAcc n (Just Hidden)) ns

75−accData a n ns = do addAcc n a

76− mapM_ (`addAcc` a) ns

77−

78−

79−{- * Error reporting helpers -}

80−{- | Error message with possible fixes list -}

81−fixErrorMsg :: String -> [String] -> String

82−fixErrorMsg msg fixes = msg ++ ", possible fixes:\n" ++ (concat $ intersperse "\n\nor\n\n" fixes)

83−

84{- * Main grammar -}

67{- * Main grammar -}

86{- | Parses module definition

69{- | Parses module definition

@@ -342,15 +325,6 @@ fnOpts opts

342 return (Just (fromInteger reds)))

325 return (Just (fromInteger reds)))

343 return (n, t)

326 return (n, t)

344

327

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

346−accessibility :: IdrisParser Accessibility

347−accessibility = do reserved "public"; return Public

348− <|> do reserved "abstract"; return Frozen

349− <|> do reserved "private"; return Hidden

350− <?> "accessibility modifier"

351−

352−

353−

354{- | Parses a postulate

328{- | Parses a postulate

355

329

356Postulate ::=

330Postulate ::=

@@ -444,55 +418,6 @@ namespace syn =

444 return [PNamespace n (concat ds)]

418 return [PNamespace n (concat ds)]

445 <?> "namespace declaration"

419 <?> "namespace declaration"

446

420

447−{- | Parses a fixity declaration

448−

449−Fixity ::=

450− FixityType Natural_t OperatorList Terminator

451− ;

452−-}

453−fixity :: IdrisParser PDecl

454−fixity = do pushIndent

455− f <- fixityType; i <- natural; ops <- sepBy1 operator (lchar ',')

456− terminator

457− let prec = fromInteger i

458− istate <- get

459− let infixes = idris_infixes istate

460− let fs = map (Fix (f prec)) ops

461− let redecls = map (alreadyDeclared infixes) fs

462− let ill = filter (not . checkValidity) redecls

463− if null ill

464− then do put (istate { idris_infixes = nub $ sort (fs ++ infixes)

465− , ibc_write = map IBCFix fs ++ ibc_write istate

466− })

467− fc <- getFC

468− return (PFix fc (f prec) ops)

469− else fail $ concatMap (\(f, (x:xs)) -> "Illegal redeclaration of fixity:\n\t\""

470− ++ show f ++ "\" overrides \"" ++ show x ++ "\"") ill

471− <?> "fixity declaration"

472− where alreadyDeclared :: [FixDecl] -> FixDecl -> (FixDecl, [FixDecl])

473− alreadyDeclared fs f = (f, filter ((extractName f ==) . extractName) fs)

474−

475− checkValidity :: (FixDecl, [FixDecl]) -> Bool

476− checkValidity (f, fs) = all (== f) fs

477−

478− extractName :: FixDecl -> String

479− extractName (Fix _ n) = n

480−

481−{- | Parses a fixity declaration type (i.e. infix or prefix, associtavity)

482−FixityType ::=

483− 'infixl'

484− | 'infixr'

485− | 'infix'

486− | 'prefix'

487− ;

488− -}

489−fixityType :: IdrisParser (Int -> Fixity)

490−fixityType = do reserved "infixl"; return Infixl

491− <|> do reserved "infixr"; return Infixr

492− <|> do reserved "infix"; return InfixN

493− <|> do reserved "prefix"; return PrefixN

494− <?> "fixity type"

495−

496{- |Parses a methods block (for type classes and instances)

421{- |Parses a methods block (for type classes and instances)

497 MethodsBlock ::= 'where' OpenBlock FnDecl* CloseBlock

422 MethodsBlock ::= 'where' OpenBlock FnDecl* CloseBlock

498 -}

423 -}

@@ -601,185 +526,6 @@ usingDecl syn = try (do x <- fnName

601 return (UConstraint c xs)

526 return (UConstraint c xs)

602 <?> "using declaration"

527 <?> "using declaration"

603

528

604−{- |Parses a record type declaration

605−Record ::=

606− DocComment Accessibility? 'record' FnName TypeSig 'where' OpenBlock Constructor KeepTerminator CloseBlock;

607−-}

608−record :: SyntaxInfo -> IdrisParser PDecl

609−record syn = do (doc, acc) <- try (do

610− doc <- option "" (docComment '|')

611− acc <- optional accessibility

612− reserved "record"

613− return (doc, acc))

614− fc <- getFC

615− tyn_in <- fnName

616− lchar ':'

617− ty <- typeExpr (allowImp syn)

618− let tyn = expandNS syn tyn_in

619− reserved "where"

620− (cdoc, cn, cty, _) <- indentedBlockS (constructor syn)

621− accData acc tyn [cn]

622− let rsyn = syn { syn_namespace = show (nsroot tyn) :

623− syn_namespace syn }

624− let fns = getRecNames rsyn cty

625− mapM_ (\n -> addAcc n acc) fns

626− return $ PRecord doc rsyn fc tyn ty cdoc cn cty

627− <?> "record type declaration"

628− where

629− getRecNames :: SyntaxInfo -> PTerm -> [Name]

630− getRecNames syn (PPi _ n _ sc) = [expandNS syn n, expandNS syn (mkType n)]

631− ++ getRecNames syn sc

632− getRecNames _ _ = []

633−

634− toFreeze :: Maybe Accessibility -> Maybe Accessibility

635− toFreeze (Just Frozen) = Just Hidden

636− toFreeze x = x

637−

638−{- | Parses data declaration type (normal or codata)

639−DataI ::= 'data' | 'codata';

640−-}

641−dataI :: IdrisParser Bool

642−dataI = do reserved "data"; return False

643− <|> do reserved "codata"; return True

644−

645−{- | Parses a data type declaration

646−Data ::= DocComment? Accessibility? DataI FnName TypeSig ExplicitTypeDataRest?

647− | DocComment? Accessibility? DataI FnName Name* DataRest?

648− ;

649−Constructor' ::= Constructor KeepTerminator;

650−ExplicitTypeDataRest ::= 'where' OpenBlock Constructor'* CloseBlock;

651−

652−DataRest ::= '=' SimpleConstructorList Terminator

653− | 'where'!

654− ;

655−SimpleConstructorList ::=

656− SimpleConstructor

657− | SimpleConstructor '|' SimpleConstructorList

658− ;

659−-}

660−data_ :: SyntaxInfo -> IdrisParser PDecl

661−data_ syn = do (doc, acc, co) <- try (do

662− doc <- option "" (docComment '|')

663− pushIndent

664− acc <- optional accessibility

665− co <- dataI

666− return (doc, acc, co))

667− fc <- getFC

668− tyn_in <- fnName

669− (do try (lchar ':')

670− popIndent

671− ty <- typeExpr (allowImp syn)

672− let tyn = expandNS syn tyn_in

673− option (PData doc syn fc co (PLaterdecl tyn ty)) (do

674− reserved "where"

675− cons <- indentedBlock (constructor syn)

676− accData acc tyn (map (\ (_, n, _, _) -> n) cons)

677− return $ PData doc syn fc co (PDatadecl tyn ty cons))) <|> (do

678− args <- many name

679− let ty = bindArgs (map (const PType) args) PType

680− let tyn = expandNS syn tyn_in

681− option (PData doc syn fc co (PLaterdecl tyn ty)) (do

682− try (lchar '=') <|> do reserved "where"

683− let kw = (if co then "co" else "") ++ "data "

684− let n = show tyn_in ++ " "

685− let s = kw ++ n

686− let as = concat (intersperse " " $ map show args) ++ " "

687− let ns = concat (intersperse " -> " $ map ((\x -> "(" ++ x ++ " : Type)") . show) args)

688− let ss = concat (intersperse " -> " $ map (const "Type") args)

689− let fix1 = s ++ as ++ " = ..."

690− let fix2 = s ++ ": " ++ ns ++ " -> Type where\n ..."

691− let fix3 = s ++ ": " ++ ss ++ " -> Type where\n ..."

692− fail $ fixErrorMsg "unexpected \"where\"" [fix1, fix2, fix3]

693− cons <- sepBy1 (simpleConstructor syn) (lchar '|')

694− terminator

695− let conty = mkPApp fc (PRef fc tyn) (map (PRef fc) args)

696− cons' <- mapM (\ (doc, x, cargs, cfc) ->

697− do let cty = bindArgs cargs conty

698− return (doc, x, cty, cfc)) cons

699− accData acc tyn (map (\ (_, n, _, _) -> n) cons')

700− return $ PData doc syn fc co (PDatadecl tyn ty cons')))

701− <?> "data type declaration"

702− where

703− mkPApp :: FC -> PTerm -> [PTerm] -> PTerm

704− mkPApp fc t [] = t

705− mkPApp fc t xs = PApp fc t (map pexp xs)

706− bindArgs :: [PTerm] -> PTerm -> PTerm

707− bindArgs xs t = foldr (PPi expl (MN 0 "t")) t xs

708−

709−

710−{- | Parses a type constructor declaration

711− Constructor ::= DocComment? FnName TypeSig;

712−-}

713−constructor :: SyntaxInfo -> IdrisParser (String, Name, PTerm, FC)

714−constructor syn

715− = do doc <- option "" (docComment '|')

716− cn_in <- fnName; fc <- getFC

717− let cn = expandNS syn cn_in

718− lchar ':'

719− ty <- typeExpr (allowImp syn)

720− return (doc, cn, ty, fc)

721− <?> "constructor"

722−

723−{- | Parses a constructor for simple discriminative union data types

724− SimpleConstructor ::= FnName SimpleExpr* DocComment?

725−-}

726−simpleConstructor :: SyntaxInfo -> IdrisParser (String, Name, [PTerm], FC)

727−simpleConstructor syn

728− = do cn_in <- fnName

729− let cn = expandNS syn cn_in

730− fc <- getFC

731− args <- many (do notEndApp

732− simpleExpr syn)

733− doc <- option "" (docComment '^')

734− return (doc, cn, args, fc)

735− <?> "constructor"

736−

737−{- | Parses a dsl block declaration

738−DSL ::= 'dsl' FnName OpenBlock Overload'+ CloseBlock;

739− -}

740−dsl :: SyntaxInfo -> IdrisParser PDecl

741−dsl syn = do reserved "dsl"

742− n <- fnName

743− bs <- indentedBlock (overload syn)

744− let dsl = mkDSL bs (dsl_info syn)

745− checkDSL dsl

746− i <- get

747− put (i { idris_dsls = addDef n dsl (idris_dsls i) })

748− return (PDSL n dsl)

749− <?> "dsl block declaration"

750− where mkDSL :: [(String, PTerm)] -> DSL -> DSL

751− mkDSL bs dsl = let var = lookup "variable" bs

752− first = lookup "index_first" bs

753− next = lookup "index_next" bs

754− leto = lookup "let" bs

755− lambda = lookup "lambda" bs in

756− initDSL { dsl_var = var,

757− index_first = first,

758− index_next = next,

759− dsl_lambda = lambda,

760− dsl_let = leto }

761−

762−{- | Checks DSL for errors -}

763−-- FIXME: currently does nothing, check if DSL is really sane

764−checkDSL :: DSL -> IdrisParser ()

765−checkDSL dsl = return ()

766−

767−{- | Parses a DSL overload declaration

768−OverloadIdentifier ::= 'let' | Identifier;

769−Overload ::= OverloadIdentifier '=' Expr;

770−-}

771−overload :: SyntaxInfo -> IdrisParser (String, PTerm)

772−overload syn = do o <- identifier <|> do reserved "let"

773− return "let"

774− if o `notElem` overloadable

775− then fail $ show o ++ " is not an overloading"

776− else do

777− lchar '='

778− t <- expr syn

779− return (o, t)

780− <?> "dsl overload declaratioN"

781− where overloadable = ["let","lambda","index_first","index_next","variable"]

782−

783{- | Parse a clause with patterns

529{- | Parse a clause with patterns

784Pattern ::= Clause;

530Pattern ::= Clause;

785-}

531-}

@@ -1173,36 +919,6 @@ parseProg syn fname input mrk

1173 i' <- get

919 i' <- get

1174 return (ds, i')

920 return (ds, i')

1175

921

1176−-- | Collect 'PClauses' with the same function name

1177−collect :: [PDecl] -> [PDecl]

1178−collect (c@(PClauses _ o _ _) : ds)

1179− = clauses (cname c) [] (c : ds)

1180− where clauses :: Maybe Name -> [PClause] -> [PDecl] -> [PDecl]

1181− clauses j@(Just n) acc (PClauses fc _ _ [PClause fc' n' l ws r w] : ds)

1182− | n == n' = clauses j (PClause fc' n' l ws r (collect w) : acc) ds

1183− clauses j@(Just n) acc (PClauses fc _ _ [PWith fc' n' l ws r w] : ds)

1184− | n == n' = clauses j (PWith fc' n' l ws r (collect w) : acc) ds

1185− clauses (Just n) acc xs = PClauses (fcOf c) o n (reverse acc) : collect xs

1186− clauses Nothing acc (x:xs) = collect xs

1187− clauses Nothing acc [] = []

1188−

1189− cname :: PDecl -> Maybe Name

1190− cname (PClauses fc _ _ [PClause _ n _ _ _ _]) = Just n

1191− cname (PClauses fc _ _ [PWith _ n _ _ _ _]) = Just n

1192− cname (PClauses fc _ _ [PClauseR _ _ _ _]) = Nothing

1193− cname (PClauses fc _ _ [PWithR _ _ _ _]) = Nothing

1194− fcOf :: PDecl -> FC

1195− fcOf (PClauses fc _ _ _) = fc

1196−collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds

1197−collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds

1198−collect (PNamespace ns ps : ds) = PNamespace ns (collect ps) : collect ds

1199−collect (PClass doc f s cs n ps ds : ds')

1200− = PClass doc f s cs n ps (collect ds) : collect ds'

1201−collect (PInstance f s cs n ps t en ds : ds')

1202− = PInstance f s cs n ps t en (collect ds) : collect ds'

1203−collect (d : ds) = d : collect ds

1204−collect [] = []

1205−

1206{- | Load idris module -}

922{- | Load idris module -}

1207loadModule :: FilePath -> Idris String

923loadModule :: FilePath -> Idris String

1208loadModule f

924loadModule f