@@ -89,7 +89,7 @@ isDocCommentMarker _ = False
8989 -}
9090singleLineComment :: MonadicParsing m => m ()
9191singleLineComment = try (string "--" *> satisfy isEol *> pure ())
92− <|> try (string "--" *> satisfy (not . isDocCommentMarker) *> many (satisfy (not . isEol)) *> (satisfy isEol <?> "end of line") *> pure ())
92+ <|> string "--" *> satisfy (not . isDocCommentMarker) *> many (satisfy (not . isEol)) *> (satisfy isEol <?> "end of line") *> pure ()
9393 <?> "single-line comment"
9494
9595{- | Consumes a multi-line comment
@@ -107,14 +107,14 @@ singleLineComment = try (string "--" *> satisfy isEol *> pure ())
107107
108108multiLineComment :: MonadicParsing m => m ()
109109multiLineComment = try (string "{-" *> (string "-}") *> pure ())
110− <|> try (string "{-" *> satisfy (not . isDocCommentMarker) *> inCommentChars)
110+ <|> string "{-" *> satisfy (not . isDocCommentMarker) *> inCommentChars
111111 <?> "multi-line comment"
112112 where inCommentChars :: MonadicParsing m => m ()
113− inCommentChars = try (string "-}" *> pure ())
114− <|> try (multiLineComment *> inCommentChars)
115− <|> try (docComment '|' *> inCommentChars)
116− <|> try (docComment '^' *> inCommentChars)
117− <|> try (skipSome (noneOf startEnd) *> inCommentChars)
113+ inCommentChars = string "-}" *> pure ()
114+ <|> try (multiLineComment) *> inCommentChars
115+ <|> try (docComment '|') *> inCommentChars
116+ <|> try (docComment '^') *> inCommentChars
117+ <|> skipSome (noneOf startEnd) *> inCommentChars
118118 <|> oneOf startEnd *> inCommentChars
119119 <?> "end of comment"
120120 startEnd :: String
@@ -699,9 +699,9 @@ fnDecl' syn = try (do doc <- option "" (docComment '|')
699699 terminator
700700 addAcc n acc
701701 return (PTy doc syn fc opts' n ty))
702− <|> try (postulate syn)
703− <|> try (pattern syn)
704− <|> try (caf syn)
702+ <|> postulate syn
703+ <|> caf syn
704+ <|> pattern syn
705705 <?> "function declaration"
706706
707707
@@ -727,12 +727,12 @@ fnOpts :: [FnOpt] -> IdrisParser [FnOpt]
727727fnOpts opts
728728 = do reserved "total"; fnOpts (TotalFn : opts)
729729 <|> do reserved "partial"; fnOpts (PartialFn : (opts \\ [TotalFn]))
730− <|> try (do lchar '%'; reserved "export"; c <- stringLiteral;
731− fnOpts (CExport c : opts))
732− <|> try (do lchar '%'; reserved "assert_total";
733− fnOpts (AssertTotal : opts))
734− <|> try (do lchar '%'; reserved "reflection";
735− fnOpts (Reflection : opts))
730+ <|> do try (lchar '%' *> reserved "export"); c <- stringLiteral;
731+ fnOpts (CExport c : opts)
732+ <|> do try (lchar '%' *> reserved "assert_total");
733+ fnOpts (AssertTotal : opts)
734+ <|> do try (lchar '%' *> reserved "reflection");
735+ fnOpts (Reflection : opts)
736736 <|> do lchar '%'; reserved "specialise";
737737 lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'
738738 fnOpts (Specialise ns : opts)
@@ -775,9 +775,10 @@ Postulate ::=
775775 ;
776776-}
777777postulate :: SyntaxInfo -> IdrisParser PDecl
778−postulate syn = do doc <- option "" (docComment '|')
779− pushIndent
780− reserved "postulate"
778+postulate syn = do doc <- try $ do doc <- option "" (docComment '|')
779+ pushIndent
780+ reserved "postulate"
781+ return doc
781782 ist <- get
782783 let initOpts = if default_total ist
783784 then [TotalFn]
@@ -902,10 +903,10 @@ FixityType ::=
902903 ;
903904 -}
904905fixityType :: IdrisParser (Int -> Fixity)
905−fixityType = try (do reserved "infixl"; return Infixl)
906− <|> try (do reserved "infixr"; return Infixr)
907− <|> try (do reserved "infix"; return InfixN)
908− <|> try (do reserved "prefix"; return PrefixN)
906+fixityType = do reserved "infixl"; return Infixl
907+ <|> do reserved "infixr"; return Infixr
908+ <|> do reserved "infix"; return InfixN
909+ <|> do reserved "prefix"; return PrefixN
909910 <?> "fixity type"
910911
911912{- |Parses a methods block (for type classes and instances)
@@ -1441,8 +1442,8 @@ Arg ::=
14411442 ;
14421443-}
14431444arg :: SyntaxInfo -> IdrisParser PArg
1444−arg syn = try (implicitArg syn)
1445− <|> try (constraintArg syn)
1445+arg syn = implicitArg syn
1446+ <|> constraintArg syn
14461447 <|> do e <- simpleExpr syn
14471448 return (pexp e)
14481449 <?> "function argument"
@@ -1847,9 +1848,9 @@ do_ syn
18471848 fc <- getFC
18481849 e <- expr syn;
18491850 return (DoBindP fc i e))
1850− <|> try (do e <- expr syn
1851− fc <- getFC
1852− return (DoExp fc e))
1851+ <|> do e <- expr syn
1852+ fc <- getFC
1853+ return (DoExp fc e)
18531854 <?> "do block expression"
18541855
18551856{- |Parses an expression in idiom brackets
@@ -2152,116 +2153,108 @@ rhs syn n = do lchar '='; expr syn
21522153 addLet nm r = (PLet (UN "value") Placeholder r (PMetavar nm))
21532154
21542155{- |Parses a function clause
2155−Clause ::= FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHS WhereOrTerminator
2156+RHSOrWithBlock ::= RHS WhereOrTerminator
2157+ | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
2158+ ;
2159+Clause ::= WExpr+ RHSOrWithBlock
21562160 | SimpleExpr '<==' FnName RHS WhereOrTerminator
2157− | WExpr+ RHS WhereOrTerminator
2158− | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
2159− | WExpr+ 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
2160− | ArgExpr Operator ArgExpr WExpr* RHS WhereOrTerminator
2161− | ArgExpr Operator ArgExpr WExpr* 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
2161+ | ArgExpr Operator ArgExpr WExpr* RHSOrWithBlock {- Except "=" and "?=" operators to avoid ambiguity -}
2162+ | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock
21622163 ;
21632164ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
21642165WhereOrTerminator ::= WhereBlock | Terminator;
21652166-}
21662167clause :: SyntaxInfo -> IdrisParser PClause
21672168clause syn
2168− = try (do pushIndent
2169− n_in <- fnName; let n = expandNS syn n_in
2170− cargs <- many (constraintArg syn)
2171− fc <- getFC
2172− args <- many (try (implicitArg (syn { inPattern = True } ))
2173− <|> (fmap pexp (argExpr syn)))
2174− wargs <- many (wExpr syn)
2175− r <- rhs syn n
2176− ist <- get
2177− let ctxt = tt_ctxt ist
2178− let wsyn = syn { syn_namespace = [] }
2179− (wheres, nmap) <- choice [do x <- whereBlock n wsyn
2180− popIndent
2181− return x,
2182− do terminator
2183− return ([], [])]
2184− let capp = PApp fc (PRef fc n)
2185− (cargs ++ args)
2186− ist <- get
2187− put (ist { lastParse = Just n })
2188− return $ PClause fc n capp wargs r wheres)
2189− <|> try (do pushIndent
2190− ty <- simpleExpr syn
2191− symbol "<=="
2192− fc <- getFC
2193− n_in <- fnName; let n = expandNS syn n_in
2194− r <- rhs syn n
2195− ist <- get
2196− let ctxt = tt_ctxt ist
2197− let wsyn = syn { syn_namespace = [] }
2198− (wheres, nmap) <- choice [do x <- whereBlock n wsyn
2199− popIndent
2200− return x,
2201− do terminator
2202− return ([], [])]
2203− let capp = PLet (MN 0 "match")
2204− ty
2205− (PMatchApp fc n)
2206− (PRef fc (MN 0 "match"))
2207− ist <- get
2208− put (ist { lastParse = Just n })
2209− return $ PClause fc n capp [] r wheres)
2210− <|> try (do pushIndent
2211− wargs <- some (wExpr syn)
2212− ist <- get
2213− n <- case lastParse ist of
2214− Just t -> return t
2215− Nothing -> fail "Invalid clause"
2216− fc <- getFC
2217− r <- rhs syn n
2218− let ctxt = tt_ctxt ist
2219− let wsyn = syn { syn_namespace = [] }
2220− (wheres, nmap) <- choice [do x <- whereBlock n wsyn
2221− popIndent
2222− return x,
2223− do terminator
2224− return ([], [])]
2225− return $ PClauseR fc wargs r wheres)
2226−
2227− <|> try (do pushIndent
2228− n_in <- fnName; let n = expandNS syn n_in
2229− cargs <- many (constraintArg syn)
2230− fc <- getFC
2231− args <- many (try (implicitArg (syn { inPattern = True } ))
2232− <|> (fmap pexp (argExpr syn)))
2233− wargs <- many (wExpr syn)
2234− let capp = PApp fc (PRef fc n)
2235− (cargs ++ args)
2236− ist <- get
2237− put (ist { lastParse = Just n })
2238− reserved "with"
2239− wval <- simpleExpr syn
2240− openBlock
2241− ds <- some $ fnDecl syn
2242− let withs = map (fillLHSD n capp wargs) $ concat ds
2243− closeBlock
2169+ = do wargs <- try (do pushIndent; some (wExpr syn))
2170+ fc <- getFC
2171+ ist <- get
2172+ n <- case lastParse ist of
2173+ Just t -> return t
2174+ Nothing -> fail "Invalid clause"
2175+ (do r <- rhs syn n
2176+ let ctxt = tt_ctxt ist
2177+ let wsyn = syn { syn_namespace = [] }
2178+ (wheres, nmap) <- choice [do x <- whereBlock n wsyn
2179+ popIndent
2180+ return x,
2181+ do terminator
2182+ return ([], [])]
2183+ return $ PClauseR fc wargs r wheres) <|> (do
2184+ popIndent
2185+ reserved "with"
2186+ wval <- simpleExpr syn
2187+ openBlock
2188+ ds <- some $ fnDecl syn
2189+ let withs = concat ds
2190+ closeBlock
2191+ return $ PWithR fc wargs wval withs)
2192+ <|> do ty <- try (do pushIndent
2193+ ty <- simpleExpr syn
2194+ symbol "<=="
2195+ return ty)
2196+ fc <- getFC
2197+ n_in <- fnName; let n = expandNS syn n_in
2198+ r <- rhs syn n
2199+ ist <- get
2200+ let ctxt = tt_ctxt ist
2201+ let wsyn = syn { syn_namespace = [] }
2202+ (wheres, nmap) <- choice [do x <- whereBlock n wsyn
2203+ popIndent
2204+ return x,
2205+ do terminator
2206+ return ([], [])]
2207+ let capp = PLet (MN 0 "match")
2208+ ty
2209+ (PMatchApp fc n)
2210+ (PRef fc (MN 0 "match"))
2211+ ist <- get
2212+ put (ist { lastParse = Just n })
2213+ return $ PClause fc n capp [] r wheres
2214+ <|> do (l, op) <- try (do
2215+ pushIndent
2216+ l <- argExpr syn
2217+ op <- operator
2218+ when (op == "=" || op == "?=" ) (fail "infix clause definition with \"=\" and \"?=\" not supported ")
2219+ return (l, op))
2220+ let n = expandNS syn (UN op)
2221+ r <- argExpr syn
2222+ fc <- getFC
2223+ wargs <- many (wExpr syn)
2224+ (do rs <- rhs syn n
2225+ let wsyn = syn { syn_namespace = [] }
2226+ (wheres, nmap) <- choice [do x <- whereBlock n wsyn
2227+ popIndent
2228+ return x,
2229+ do terminator
2230+ return ([], [])]
2231+ ist <- get
2232+ let capp = PApp fc (PRef fc n) [pexp l, pexp r]
2233+ put (ist { lastParse = Just n })
2234+ return $ PClause fc n capp wargs rs wheres) <|> (do
22442235 popIndent
2245− return $ PWith fc n capp wargs wval withs)
2246−
2247− <|> try (do wargs <- some (wExpr syn)
2248− fc <- getFC
22492236 reserved "with"
22502237 wval <- simpleExpr syn
22512238 openBlock
22522239 ds <- some $ fnDecl syn
2253− let withs = concat ds
22542240 closeBlock
2255− return $ PWithR fc wargs wval withs)
2256−
2257− <|> try(do pushIndent
2258− l <- argExpr syn
2259− op <- operator
2260− let n = expandNS syn (UN op)
2261− r <- argExpr syn
2262− fc <- getFC
2263− wargs <- many (wExpr syn)
2264− rs <- rhs syn n
2241+ ist <- get
2242+ let capp = PApp fc (PRef fc n) [pexp l, pexp r]
2243+ let withs = map (fillLHSD n capp wargs) $ concat ds
2244+ put (ist { lastParse = Just n })
2245+ return $ PWith fc n capp wargs wval withs)
2246+ <|> do pushIndent
2247+ n_in <- fnName; let n = expandNS syn n_in
2248+ cargs <- many (constraintArg syn)
2249+ fc <- getFC
2250+ args <- many (try (implicitArg (syn { inPattern = True } ))
2251+ <|> (fmap pexp (argExpr syn)))
2252+ wargs <- many (wExpr syn)
2253+ let capp = PApp fc (PRef fc n)
2254+ (cargs ++ args)
2255+ (do r <- rhs syn n
2256+ ist <- get
2257+ let ctxt = tt_ctxt ist
22652258 let wsyn = syn { syn_namespace = [] }
22662259 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
22672260 popIndent
@@ -2269,26 +2262,18 @@ clause syn
22692262 do terminator
22702263 return ([], [])]
22712264 ist <- get
2272− let capp = PApp fc (PRef fc n) [pexp l, pexp r]
22732265 put (ist { lastParse = Just n })
2274− return $ PClause fc n capp wargs rs wheres)
2275−
2276− <|> do l <- argExpr syn
2277− op <- operator
2278− let n = expandNS syn (UN op)
2279− r <- argExpr syn
2280− fc <- getFC
2281− wargs <- many (wExpr syn)
2282− reserved "with"
2283− wval <- simpleExpr syn
2284− openBlock
2285− ds <- some $ fnDecl syn
2286− closeBlock
2287− ist <- get
2288− let capp = PApp fc (PRef fc n) [pexp l, pexp r]
2289− let withs = map (fillLHSD n capp wargs) $ concat ds
2290− put (ist { lastParse = Just n })
2291− return $ PWith fc n capp wargs wval withs
2266+ return $ PClause fc n capp wargs r wheres) <|> (do
2267+ reserved "with"
2268+ ist <- get
2269+ put (ist { lastParse = Just n })
2270+ wval <- simpleExpr syn
2271+ openBlock
2272+ ds <- some $ fnDecl syn
2273+ let withs = map (fillLHSD n capp wargs) $ concat ds
2274+ closeBlock
2275+ popIndent
2276+ return $ PWith fc n capp wargs wval withs)
22922277 <?> "function clause"
22932278 where
22942279 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause
@@ -2332,13 +2317,13 @@ Codegen ::= 'C'
23322317 ;
23332318-}
23342319codegen_ :: IdrisParser Codegen
2335−codegen_ = try (do reserved "C"; return ViaC)
2336− <|> try (do reserved "Java"; return ViaJava)
2337− <|> try (do reserved "JavaScript"; return ViaJavaScript)
2338− <|> try (do reserved "Node"; return ViaNode)
2339− <|> try (do reserved "LLVM"; return ViaLLVM)
2340− <|> try (do reserved "Bytecode"; return Bytecode)
2341− <?> "code generation language"
2320+codegen_ = do reserved "C"; return ViaC
2321+ <|> do reserved "Java"; return ViaJava
2322+ <|> do reserved "JavaScript"; return ViaJavaScript
2323+ <|> do reserved "Node"; return ViaNode
2324+ <|> do reserved "LLVM"; return ViaLLVM
2325+ <|> do reserved "Bytecode"; return Bytecode
2326+ <?> "code generation language"
23422327
23432328{- |Parses a compiler directive
23442329StringList ::=
@@ -2362,45 +2347,45 @@ Directive' ::= 'lib' CodeGen String_t
23622347 ;
23632348-}
23642349directive :: SyntaxInfo -> IdrisParser [PDecl]
2365−directive syn = try (do lchar '%'; reserved "lib"; cgn <- codegen_; lib <- stringLiteral;
2366− return [PDirective (do addLib cgn lib
2367− addIBC (IBCLib cgn lib))])
2368− <|> try (do lchar '%'; reserved "link"; cgn <- codegen_; obj <- stringLiteral;
2369− return [PDirective (do dirs <- allImportDirs
2370− o <- liftIO $ findInPath dirs obj
2371− addIBC (IBCObj cgn obj) -- just name, search on loading ibc
2372− addObjectFile cgn o)])
2373− <|> try (do lchar '%'; reserved "flag"; cgn <- codegen_;
2374− flag <- stringLiteral
2375− return [PDirective (do addIBC (IBCCGFlag cgn flag)
2376− addFlag cgn flag)])
2377− <|> try (do lchar '%'; reserved "include"; cgn <- codegen_; hdr <- stringLiteral;
2378− return [PDirective (do addHdr cgn hdr
2379− addIBC (IBCHeader cgn hdr))])
2380− <|> try (do lchar '%'; reserved "hide"; n <- iName []
2381− return [PDirective (do setAccessibility n Hidden
2382− addIBC (IBCAccess n Hidden))])
2383− <|> try (do lchar '%'; reserved "freeze"; n <- iName []
2384− return [PDirective (do setAccessibility n Frozen
2385− addIBC (IBCAccess n Frozen))])
2386− <|> try (do lchar '%'; reserved "access"; acc <- accessibility
2387− return [PDirective (do i <- get
2388− put(i { default_access = acc }))])
2389− <|> try (do lchar '%'; reserved "default"; tot <- totality
2390− i <- get
2391− put (i { default_total = tot } )
2392− return [PDirective (do i <- get
2393− put(i { default_total = tot }))])
2394− <|> try (do lchar '%'; reserved "logging"; i <- natural;
2395− return [PDirective (setLogLevel (fromInteger i))])
2396− <|> try (do lchar '%'; reserved "dynamic"; libs <- sepBy1 stringLiteral (lchar ',');
2397− return [PDirective (do added <- addDyLib libs
2398− case added of
2399− Left lib -> addIBC (IBCDyLib (lib_name lib))
2400− Right msg ->
2401− fail $ msg)])
2402− <|> try (do lchar '%'; reserved "language"; ext <- reserved "TypeProviders";
2403− return [PDirective (addLangExt TypeProviders)])
2350+directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- stringLiteral;
2351+ return [PDirective (do addLib cgn lib
2352+ addIBC (IBCLib cgn lib))]
2353+ <|> do try (lchar '%' *> reserved "link"); cgn <- codegen_; obj <- stringLiteral;
2354+ return [PDirective (do dirs <- allImportDirs
2355+ o <- liftIO $ findInPath dirs obj
2356+ addIBC (IBCObj cgn obj) -- just name, search on loading ibc
2357+ addObjectFile cgn o)]
2358+ <|> do try (lchar '%' *> reserved "flag"); cgn <- codegen_;
2359+ flag <- stringLiteral
2360+ return [PDirective (do addIBC (IBCCGFlag cgn flag)
2361+ addFlag cgn flag)]
2362+ <|> do try (lchar '%' *> reserved "include"); cgn <- codegen_; hdr <- stringLiteral;
2363+ return [PDirective (do addHdr cgn hdr
2364+ addIBC (IBCHeader cgn hdr))]
2365+ <|> do try (lchar '%' *> reserved "hide"); n <- iName []
2366+ return [PDirective (do setAccessibility n Hidden
2367+ addIBC (IBCAccess n Hidden))]
2368+ <|> do try (lchar '%' *> reserved "freeze"); n <- iName []
2369+ return [PDirective (do setAccessibility n Frozen
2370+ addIBC (IBCAccess n Frozen))]
2371+ <|> do try (lchar '%' *> reserved "access"); acc <- accessibility
2372+ return [PDirective (do i <- get
2373+ put(i { default_access = acc }))]
2374+ <|> do try (lchar '%' *> reserved "default"); tot <- totality
2375+ i <- get
2376+ put (i { default_total = tot } )
2377+ return [PDirective (do i <- get
2378+ put(i { default_total = tot }))]
2379+ <|> do try (lchar '%' *> reserved "logging"); i <- natural;
2380+ return [PDirective (setLogLevel (fromInteger i))]
2381+ <|> do try (lchar '%' *> reserved "dynamic"); libs <- sepBy1 stringLiteral (lchar ',');
2382+ return [PDirective (do added <- addDyLib libs
2383+ case added of
2384+ Left lib -> addIBC (IBCDyLib (lib_name lib))
2385+ Right msg ->
2386+ fail $ msg)]
2387+ <|> do try (lchar '%' *> reserved "language"); ext <- reserved "TypeProviders";
2388+ return [PDirective (addLangExt TypeProviders)]
24042389 <?> "directive"
24052390
24062391{- | Parses a totality
@@ -2769,4 +2754,3 @@ addHides xs = do i <- getIState
27692754
27702755 doHide (n, a) = do setAccessibility n a
27712756 addIBC (IBCAccess n a)
2772−