@@ -89,8 +89,8 @@ 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 ())
93− <?> "single-line comment"
92+ <|> string "--" *> satisfy (not . isDocCommentMarker) *> many (satisfy (not . isEol)) *> (satisfy isEol <?> "end of line") *> pure ()
93+ <?> ""
9494
9595{- | Consumes a multi-line comment
9696 MultiLineComment_t ::=
@@ -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)
111− <?> "multi-line comment"
110+ <|> string "{-" *> satisfy (not . isDocCommentMarker) *> inCommentChars
111+ <?> ""
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
@@ -131,7 +131,7 @@ docComment marker | isDocCommentMarker marker = do dc <- docComment' marker; ret
131131 where docComment' :: MonadicParsing m => Char -> m String
132132 docComment' marker = string "--" *> char marker *> many (satisfy (not . isEol)) <* satisfy isEol
133133 <|> string "{-" *> char marker *> (manyTill anyChar (try (string "-}")) <?> "end of comment")
134− <?> "documentation comment"
134+ <?> ""
135135
136136-- | Consumes whitespace (and comments)
137137whiteSpace :: MonadicParsing m => m ()
@@ -555,9 +555,9 @@ decl syn = do notEndBlock
555555 <|> instance_ syn
556556 <|> do d <- dsl syn; return [d]
557557 <|> directive syn
558− <|> try(provider syn)
558+ <|> provider syn
559559 <|> transform syn
560− <|> try(do import_; fail "imports must be at top of file")
560+ <|> do import_; fail "imports must be at top of file"
561561 <?> "declaration"
562562 declBody' :: IdrisParser [PDecl]
563563 declBody' = do d <- decl' syn
@@ -575,11 +575,11 @@ Decl' ::=
575575 ;
576576-}
577577decl' :: SyntaxInfo -> IdrisParser PDecl
578−decl' syn = try fixity
579− <|> try (fnDecl' syn)
580− <|> try (data_ syn)
581− <|> try (record syn)
582− <|> try (syntaxDecl syn)
578+decl' syn = fixity
579+ <|> syntaxDecl syn
580+ <|> fnDecl' syn
581+ <|> data_ syn
582+ <|> record syn
583583 <?> "declaration"
584584
585585{- | Parses a syntax extension declaration (and adds the rule to parser state)
@@ -615,10 +615,12 @@ SyntaxSym ::= '[' Name_t ']'
615615-}
616616syntaxRule :: SyntaxInfo -> IdrisParser Syntax
617617syntaxRule syn
618− = do pushIndent
619− sty <- option AnySyntax (do reserved "term"; return TermSyntax
618+ = do sty <- try (do
619+ pushIndent
620+ sty <- option AnySyntax (do reserved "term"; return TermSyntax
620621 <|> do reserved "pattern"; return PatternSyntax)
621− reserved "syntax"
622+ reserved "syntax"
623+ return sty)
622624 syms <- some syntaxSym
623625 when (all isExpr syms) $ unexpected "missing keywords in syntax rule"
624626 let ns = mapMaybe getName syms
@@ -699,9 +701,9 @@ fnDecl' syn = try (do doc <- option "" (docComment '|')
699701 terminator
700702 addAcc n acc
701703 return (PTy doc syn fc opts' n ty))
702− <|> try (postulate syn)
703− <|> try (pattern syn)
704− <|> try (caf syn)
704+ <|> postulate syn
705+ <|> caf syn
706+ <|> pattern syn
705707 <?> "function declaration"
706708
707709
@@ -727,12 +729,12 @@ fnOpts :: [FnOpt] -> IdrisParser [FnOpt]
727729fnOpts opts
728730 = do reserved "total"; fnOpts (TotalFn : opts)
729731 <|> 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))
732+ <|> do try (lchar '%' *> reserved "export"); c <- stringLiteral;
733+ fnOpts (CExport c : opts)
734+ <|> do try (lchar '%' *> reserved "assert_total");
735+ fnOpts (AssertTotal : opts)
736+ <|> do try (lchar '%' *> reserved "reflection");
737+ fnOpts (Reflection : opts)
736738 <|> do lchar '%'; reserved "specialise";
737739 lchar '['; ns <- sepBy nameTimes (lchar ','); lchar ']'
738740 fnOpts (Specialise ns : opts)
@@ -775,9 +777,10 @@ Postulate ::=
775777 ;
776778-}
777779postulate :: SyntaxInfo -> IdrisParser PDecl
778−postulate syn = do doc <- option "" (docComment '|')
779− pushIndent
780− reserved "postulate"
780+postulate syn = do doc <- try $ do doc <- option "" (docComment '|')
781+ pushIndent
782+ reserved "postulate"
783+ return doc
781784 ist <- get
782785 let initOpts = if default_total ist
783786 then [TotalFn]
@@ -902,10 +905,10 @@ FixityType ::=
902905 ;
903906 -}
904907fixityType :: 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)
908+fixityType = do reserved "infixl"; return Infixl
909+ <|> do reserved "infixr"; return Infixr
910+ <|> do reserved "infix"; return InfixN
911+ <|> do reserved "prefix"; return PrefixN
909912 <?> "fixity type"
910913
911914{- |Parses a methods block (for type classes and instances)
@@ -931,8 +934,10 @@ Class ::=
931934 ;
932935-}
933936class_ :: SyntaxInfo -> IdrisParser [PDecl]
934−class_ syn = do doc <- option "" (docComment '|')
935− acc <- optional accessibility
937+class_ syn = do (doc, acc) <- try (do
938+ doc <- option "" (docComment '|')
939+ acc <- optional accessibility
940+ return (doc, acc))
936941 reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- name
937942 let n = expandNS syn n_in
938943 cs <- many carg
@@ -1441,8 +1446,8 @@ Arg ::=
14411446 ;
14421447-}
14431448arg :: SyntaxInfo -> IdrisParser PArg
1444−arg syn = try (implicitArg syn)
1445− <|> try (constraintArg syn)
1449+arg syn = implicitArg syn
1450+ <|> constraintArg syn
14461451 <|> do e <- simpleExpr syn
14471452 return (pexp e)
14481453 <?> "function argument"
@@ -1847,9 +1852,9 @@ do_ syn
18471852 fc <- getFC
18481853 e <- expr syn;
18491854 return (DoBindP fc i e))
1850− <|> try (do e <- expr syn
1851− fc <- getFC
1852− return (DoExp fc e))
1855+ <|> do e <- expr syn
1856+ fc <- getFC
1857+ return (DoExp fc e)
18531858 <?> "do block expression"
18541859
18551860{- |Parses an expression in idiom brackets
@@ -1922,9 +1927,11 @@ Record ::=
19221927 DocComment Accessibility? 'record' FnName TypeSig 'where' OpenBlock Constructor KeepTerminator CloseBlock;
19231928-}
19241929record :: SyntaxInfo -> IdrisParser PDecl
1925−record syn = do doc <- option "" (docComment '|')
1926− acc <- optional accessibility
1927− reserved "record"
1930+record syn = do (doc, acc) <- try (do
1931+ doc <- option "" (docComment '|')
1932+ acc <- optional accessibility
1933+ reserved "record"
1934+ return (doc, acc))
19281935 fc <- getFC
19291936 tyn_in <- fnName
19301937 ty <- typeSig (allowImp syn)
@@ -2152,116 +2159,108 @@ rhs syn n = do lchar '='; expr syn
21522159 addLet nm r = (PLet (UN "value") Placeholder r (PMetavar nm))
21532160
21542161{- |Parses a function clause
2155−Clause ::= FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHS WhereOrTerminator
2162+RHSOrWithBlock ::= RHS WhereOrTerminator
2163+ | 'with' SimpleExpr OpenBlock FnDecl+ CloseBlock
2164+ ;
2165+Clause ::= WExpr+ RHSOrWithBlock
21562166 | 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
2167+ | ArgExpr Operator ArgExpr WExpr* RHSOrWithBlock {- Except "=" and "?=" operators to avoid ambiguity -}
2168+ | FnName ConstraintArg* ImplicitOrArgExpr* WExpr* RHSOrWithBlock
21622169 ;
21632170ImplicitOrArgExpr ::= ImplicitArg | ArgExpr;
21642171WhereOrTerminator ::= WhereBlock | Terminator;
21652172-}
21662173clause :: SyntaxInfo -> IdrisParser PClause
21672174clause 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
2175+ = do wargs <- try (do pushIndent; some (wExpr syn))
2176+ fc <- getFC
2177+ ist <- get
2178+ n <- case lastParse ist of
2179+ Just t -> return t
2180+ Nothing -> fail "Invalid clause"
2181+ (do r <- rhs syn n
2182+ let ctxt = tt_ctxt ist
2183+ let wsyn = syn { syn_namespace = [] }
2184+ (wheres, nmap) <- choice [do x <- whereBlock n wsyn
2185+ popIndent
2186+ return x,
2187+ do terminator
2188+ return ([], [])]
2189+ return $ PClauseR fc wargs r wheres) <|> (do
2190+ popIndent
2191+ reserved "with"
2192+ wval <- simpleExpr syn
2193+ openBlock
2194+ ds <- some $ fnDecl syn
2195+ let withs = concat ds
2196+ closeBlock
2197+ return $ PWithR fc wargs wval withs)
2198+ <|> do ty <- try (do pushIndent
2199+ ty <- simpleExpr syn
2200+ symbol "<=="
2201+ return ty)
2202+ fc <- getFC
2203+ n_in <- fnName; let n = expandNS syn n_in
2204+ r <- rhs syn n
2205+ ist <- get
2206+ let ctxt = tt_ctxt ist
2207+ let wsyn = syn { syn_namespace = [] }
2208+ (wheres, nmap) <- choice [do x <- whereBlock n wsyn
2209+ popIndent
2210+ return x,
2211+ do terminator
2212+ return ([], [])]
2213+ let capp = PLet (MN 0 "match")
2214+ ty
2215+ (PMatchApp fc n)
2216+ (PRef fc (MN 0 "match"))
2217+ ist <- get
2218+ put (ist { lastParse = Just n })
2219+ return $ PClause fc n capp [] r wheres
2220+ <|> do (l, op) <- try (do
2221+ pushIndent
2222+ l <- argExpr syn
2223+ op <- operator
2224+ when (op == "=" || op == "?=" ) (fail "infix clause definition with \"=\" and \"?=\" not supported ")
2225+ return (l, op))
2226+ let n = expandNS syn (UN op)
2227+ r <- argExpr syn
2228+ fc <- getFC
2229+ wargs <- many (wExpr syn)
2230+ (do rs <- rhs syn n
2231+ let wsyn = syn { syn_namespace = [] }
2232+ (wheres, nmap) <- choice [do x <- whereBlock n wsyn
2233+ popIndent
2234+ return x,
2235+ do terminator
2236+ return ([], [])]
2237+ ist <- get
2238+ let capp = PApp fc (PRef fc n) [pexp l, pexp r]
2239+ put (ist { lastParse = Just n })
2240+ return $ PClause fc n capp wargs rs wheres) <|> (do
22442241 popIndent
2245− return $ PWith fc n capp wargs wval withs)
2246−
2247− <|> try (do wargs <- some (wExpr syn)
2248− fc <- getFC
22492242 reserved "with"
22502243 wval <- simpleExpr syn
22512244 openBlock
22522245 ds <- some $ fnDecl syn
2253− let withs = concat ds
22542246 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
2247+ ist <- get
2248+ let capp = PApp fc (PRef fc n) [pexp l, pexp r]
2249+ let withs = map (fillLHSD n capp wargs) $ concat ds
2250+ put (ist { lastParse = Just n })
2251+ return $ PWith fc n capp wargs wval withs)
2252+ <|> do pushIndent
2253+ n_in <- fnName; let n = expandNS syn n_in
2254+ cargs <- many (constraintArg syn)
2255+ fc <- getFC
2256+ args <- many (try (implicitArg (syn { inPattern = True } ))
2257+ <|> (fmap pexp (argExpr syn)))
2258+ wargs <- many (wExpr syn)
2259+ let capp = PApp fc (PRef fc n)
2260+ (cargs ++ args)
2261+ (do r <- rhs syn n
2262+ ist <- get
2263+ let ctxt = tt_ctxt ist
22652264 let wsyn = syn { syn_namespace = [] }
22662265 (wheres, nmap) <- choice [do x <- whereBlock n wsyn
22672266 popIndent
@@ -2269,26 +2268,18 @@ clause syn
22692268 do terminator
22702269 return ([], [])]
22712270 ist <- get
2272− let capp = PApp fc (PRef fc n) [pexp l, pexp r]
22732271 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
2272+ return $ PClause fc n capp wargs r wheres) <|> (do
2273+ reserved "with"
2274+ ist <- get
2275+ put (ist { lastParse = Just n })
2276+ wval <- simpleExpr syn
2277+ openBlock
2278+ ds <- some $ fnDecl syn
2279+ let withs = map (fillLHSD n capp wargs) $ concat ds
2280+ closeBlock
2281+ popIndent
2282+ return $ PWith fc n capp wargs wval withs)
22922283 <?> "function clause"
22932284 where
22942285 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause
@@ -2332,13 +2323,13 @@ Codegen ::= 'C'
23322323 ;
23332324-}
23342325codegen_ :: 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"
2326+codegen_ = do reserved "C"; return ViaC
2327+ <|> do reserved "Java"; return ViaJava
2328+ <|> do reserved "JavaScript"; return ViaJavaScript
2329+ <|> do reserved "Node"; return ViaNode
2330+ <|> do reserved "LLVM"; return ViaLLVM
2331+ <|> do reserved "Bytecode"; return Bytecode
2332+ <?> "code generation language"
23422333
23432334{- |Parses a compiler directive
23442335StringList ::=
@@ -2363,45 +2354,45 @@ Directive' ::= 'lib' CodeGen String_t
23632354 ;
23642355-}
23652356directive :: SyntaxInfo -> IdrisParser [PDecl]
2366−directive syn = try (do lchar '%'; reserved "lib"; cgn <- codegen_; lib <- stringLiteral;
2367− return [PDirective (do addLib cgn lib
2368− addIBC (IBCLib cgn lib))])
2369− <|> try (do lchar '%'; reserved "link"; cgn <- codegen_; obj <- stringLiteral;
2370− return [PDirective (do dirs <- allImportDirs
2371− o <- liftIO $ findInPath dirs obj
2372− addIBC (IBCObj cgn obj) -- just name, search on loading ibc
2373− addObjectFile cgn o)])
2374− <|> try (do lchar '%'; reserved "flag"; cgn <- codegen_;
2375− flag <- stringLiteral
2376− return [PDirective (do addIBC (IBCCGFlag cgn flag)
2377− addFlag cgn flag)])
2378− <|> try (do lchar '%'; reserved "include"; cgn <- codegen_; hdr <- stringLiteral;
2379− return [PDirective (do addHdr cgn hdr
2380− addIBC (IBCHeader cgn hdr))])
2381− <|> try (do lchar '%'; reserved "hide"; n <- iName []
2382− return [PDirective (do setAccessibility n Hidden
2383− addIBC (IBCAccess n Hidden))])
2384− <|> try (do lchar '%'; reserved "freeze"; n <- iName []
2385− return [PDirective (do setAccessibility n Frozen
2386− addIBC (IBCAccess n Frozen))])
2387− <|> try (do lchar '%'; reserved "access"; acc <- accessibility
2388− return [PDirective (do i <- get
2389− put(i { default_access = acc }))])
2390− <|> try (do lchar '%'; reserved "default"; tot <- totality
2391− i <- get
2392− put (i { default_total = tot } )
2393− return [PDirective (do i <- get
2394− put(i { default_total = tot }))])
2395− <|> try (do lchar '%'; reserved "logging"; i <- natural;
2396− return [PDirective (setLogLevel (fromInteger i))])
2397− <|> try (do lchar '%'; reserved "dynamic"; libs <- sepBy1 stringLiteral (lchar ',');
2398− return [PDirective (do added <- addDyLib libs
2399− case added of
2400− Left lib -> addIBC (IBCDyLib (lib_name lib))
2401− Right msg ->
2402− fail $ msg)])
2403− <|> try (do lchar '%'; reserved "language"; ext <- pLangExt;
2404− return [PDirective (addLangExt ext)])
2357+directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- stringLiteral;
2358+ return [PDirective (do addLib cgn lib
2359+ addIBC (IBCLib cgn lib))]
2360+ <|> do try (lchar '%' *> reserved "link"); cgn <- codegen_; obj <- stringLiteral;
2361+ return [PDirective (do dirs <- allImportDirs
2362+ o <- liftIO $ findInPath dirs obj
2363+ addIBC (IBCObj cgn obj) -- just name, search on loading ibc
2364+ addObjectFile cgn o)]
2365+ <|> do try (lchar '%' *> reserved "flag"); cgn <- codegen_;
2366+ flag <- stringLiteral
2367+ return [PDirective (do addIBC (IBCCGFlag cgn flag)
2368+ addFlag cgn flag)]
2369+ <|> do try (lchar '%' *> reserved "include"); cgn <- codegen_; hdr <- stringLiteral;
2370+ return [PDirective (do addHdr cgn hdr
2371+ addIBC (IBCHeader cgn hdr))]
2372+ <|> do try (lchar '%' *> reserved "hide"); n <- iName []
2373+ return [PDirective (do setAccessibility n Hidden
2374+ addIBC (IBCAccess n Hidden))]
2375+ <|> do try (lchar '%' *> reserved "freeze"); n <- iName []
2376+ return [PDirective (do setAccessibility n Frozen
2377+ addIBC (IBCAccess n Frozen))]
2378+ <|> do try (lchar '%' *> reserved "access"); acc <- accessibility
2379+ return [PDirective (do i <- get
2380+ put(i { default_access = acc }))]
2381+ <|> do try (lchar '%' *> reserved "default"); tot <- totality
2382+ i <- get
2383+ put (i { default_total = tot } )
2384+ return [PDirective (do i <- get
2385+ put(i { default_total = tot }))]
2386+ <|> do try (lchar '%' *> reserved "logging"); i <- natural;
2387+ return [PDirective (setLogLevel (fromInteger i))]
2388+ <|> do try (lchar '%' *> reserved "dynamic"); libs <- sepBy1 stringLiteral (lchar ',');
2389+ return [PDirective (do added <- addDyLib libs
2390+ case added of
2391+ Left lib -> addIBC (IBCDyLib (lib_name lib))
2392+ Right msg ->
2393+ fail $ msg)]
2394+ <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;
2395+ return [PDirective (addLangExt ext)]
24052396 <?> "directive"
24062397
24072398pLangExt :: IdrisParser LanguageExt
@@ -2420,7 +2411,7 @@ totality
24202411Provider ::= '%' 'provide' '(' FnName TypeSig ')' 'with' Expr;
24212412 -}
24222413provider :: SyntaxInfo -> IdrisParser [PDecl]
2423−provider syn = do lchar '%'; reserved "provide";
2414+provider syn = do try (lchar '%' *> reserved "provide");
24242415 lchar '('; n <- fnName; t <- typeSig syn; lchar ')'
24252416 fc <- getFC
24262417 reserved "with"
@@ -2432,7 +2423,7 @@ provider syn = do lchar '%'; reserved "provide";
24322423Transform ::= '%' 'transform' Expr '==>' Expr
24332424-}
24342425transform :: SyntaxInfo -> IdrisParser [PDecl]
2435−transform syn = do lchar '%'; reserved "transform";
2426+transform syn = do try (lchar '%' *> reserved "transform")
24362427 -- leave it unchecked, until we work out what this should
24372428 -- actually mean...
24382429-- safety <- option True (do reserved "unsafe"
@@ -2774,4 +2765,3 @@ addHides xs = do i <- getIState
27742765
27752766 doHide (n, a) = do setAccessibility n a
27762767 addIBC (IBCAccess n a)
2777−