@@ -1,6 +1,7 @@
11{-# LANGUAGE GeneralizedNewtypeDeriving, ConstraintKinds, PatternGuards #-}
22module Idris.Parser(module Idris.Parser,
3− module Idris.ParseExpr,
3+ module Idris.ParseExpr,
4+ module Idris.ParseData,
45 module Idris.ParseHelpers,
56 module Idris.ParseOps) where
67
@@ -28,6 +29,7 @@ import Idris.Providers
2829import Idris.ParseHelpers
2930import Idris.ParseOps
3031import Idris.ParseExpr
32+import Idris.ParseData
3133
3234import Paths_idris
3335
@@ -62,25 +64,6 @@ import System.FilePath
6264 RULE{n} = rule repeated n times
6365-}
6466
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−
8467{- * Main grammar -}
8568
8669{- | Parses module definition
@@ -342,15 +325,6 @@ fnOpts opts
342325 return (Just (fromInteger reds)))
343326 return (n, t)
344327
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−
354328{- | Parses a postulate
355329
356330Postulate ::=
@@ -444,55 +418,6 @@ namespace syn =
444418 return [PNamespace n (concat ds)]
445419 <?> "namespace declaration"
446420
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−
496421{- |Parses a methods block (for type classes and instances)
497422 MethodsBlock ::= 'where' OpenBlock FnDecl* CloseBlock
498423 -}
@@ -601,185 +526,6 @@ usingDecl syn = try (do x <- fnName
601526 return (UConstraint c xs)
602527 <?> "using declaration"
603528
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−
783529{- | Parse a clause with patterns
784530Pattern ::= Clause;
785531-}
@@ -1173,36 +919,6 @@ parseProg syn fname input mrk
1173919 i' <- get
1174920 return (ds, i')
1175921
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−
1206922{- | Load idris module -}
1207923loadModule :: FilePath -> Idris String
1208924loadModule f