4 | import Idris.Syntax.Traversals
5 | import public Parser.Source
8 | import public Libraries.Text.Parser
10 | import Libraries.Data.IMaybe
11 | import Data.List.Quantifiers
16 | import Libraries.Utils.String
17 | import Libraries.Data.WithDefault
19 | import Idris.Parser.Let
23 | fcBounds : OriginDesc => Rule a -> Rule (WithFC a)
24 | fcBounds a = (.withFC) <$> bounds a
26 | addFCBounds : OriginDesc => Rule (WithData ls a) -> Rule (WithData (FC' :: ls) a)
27 | addFCBounds a = (.addFC) <$> bounds a
29 | decorate : {a : Type} -> OriginDesc -> Decoration -> Rule a -> Rule a
30 | decorate fname decor rule = do
32 | actD (decorationFromBounded fname decor res)
35 | dependentDecorate : {a : Type} -> OriginDesc -> Rule a -> (a -> Decoration) -> Rule a
36 | dependentDecorate fname rule decor = do
38 | actD (decorationFromBounded fname (decor res.val) res)
41 | decoratedKeyword : OriginDesc -> String -> Rule ()
42 | decoratedKeyword fname kwd = decorate fname Keyword (keyword kwd)
44 | decorateKeywords : {a : Type} -> OriginDesc -> List (WithBounds a) -> EmptyRule ()
45 | decorateKeywords fname xs
46 | = act $
MkState (cast (map (decorationFromBounded fname Keyword) xs)) []
48 | decoratedPragma : OriginDesc -> String -> Rule ()
49 | decoratedPragma fname prg = decorate fname Keyword (pragma prg)
51 | decoratedSymbol : OriginDesc -> String -> Rule ()
52 | decoratedSymbol fname smb = decorate fname Keyword (symbol smb)
54 | decoratedNamespacedSymbol : OriginDesc -> String -> Rule (Maybe Namespace)
55 | decoratedNamespacedSymbol fname smb =
56 | decorate fname Keyword $
namespacedSymbol smb
58 | parens : {b : _} -> OriginDesc -> BRule b a -> Rule a
60 | = pure id <* decoratedSymbol fname "("
62 | <* decoratedSymbol fname ")"
64 | curly : {b : _} -> OriginDesc -> BRule b a -> Rule a
66 | = pure id <* decoratedSymbol fname "{"
68 | <* decoratedSymbol fname "}"
70 | decoratedDataTypeName : OriginDesc -> Rule Name
71 | decoratedDataTypeName fname = decorate fname Typ dataTypeName
73 | decoratedDataConstructorName : OriginDesc -> Rule Name
74 | decoratedDataConstructorName fname = decorate fname Data dataConstructorName
76 | decoratedSimpleBinderUName : OriginDesc -> Rule Name
77 | decoratedSimpleBinderUName fname = decorate fname Bound userName
79 | decoratedSimpleNamedArg : OriginDesc -> Rule String
80 | decoratedSimpleNamedArg fname
81 | = decorate fname Bound unqualifiedName
82 | <|> parens fname (decorate fname Bound unqualifiedOperatorName)
85 | topDecl : OriginDesc -> IndentInfo -> Rule PDecl
86 | collectDefs : List PDecl -> List PDecl
90 | record ParseOpts where
91 | constructor MkParseOpts
95 | peq : ParseOpts -> ParseOpts
96 | peq = { eqOK := True }
98 | pnoeq : ParseOpts -> ParseOpts
99 | pnoeq = { eqOK := False }
103 | pdef = MkParseOpts {eqOK = True, withOK = True}
105 | pnowith : ParseOpts
106 | pnowith = MkParseOpts {eqOK = True, withOK = False}
110 | plhs = MkParseOpts {eqOK = False, withOK = False}
113 | %hide Prelude.(>>=)
114 | %hide Core.Core.(>>)
115 | %hide Core.Core.(>>=)
117 | %hide Core.Core.pure
118 | %hide Prelude.(<*>)
119 | %hide Core.Core.(<*>)
121 | atom : OriginDesc -> Rule PTerm
123 | = do x <- bounds $
decorate fname Typ $
exactIdent "Type"
124 | pure (PType (boundToFC fname x))
125 | <|> do x <- bounds $
name
126 | pure (PRef (boundToFC fname x) x.val)
127 | <|> do x <- bounds $
dependentDecorate fname constant $
\c =>
131 | pure (PPrimVal (boundToFC fname x) x.val)
132 | <|> do x <- bounds $
decoratedSymbol fname "_"
133 | pure (PImplicit (boundToFC fname x))
134 | <|> do x <- bounds $
symbol "?"
135 | pure (PInfer (boundToFC fname x))
136 | <|> do x <- bounds $
holeName
138 | pure (PHole (boundToFC fname x) False x.val)
139 | <|> do x <- bounds $
decorate fname Data $
pragma "MkWorld"
140 | pure (PPrimVal (boundToFC fname x) WorldVal)
141 | <|> do x <- bounds $
decorate fname Typ $
pragma "World"
142 | pure (PPrimVal (boundToFC fname x) $
PrT WorldType)
143 | <|> do x <- bounds $
decoratedPragma fname "search"
144 | pure (PSearch (boundToFC fname x) 50)
146 | whereBlock : OriginDesc -> Int -> Rule (List PDecl)
147 | whereBlock fname col
148 | = do decoratedKeyword fname "where"
149 | ds <- blockAfter col (topDecl fname)
150 | pure (collectDefs ds)
153 | commitKeyword : OriginDesc -> IndentInfo -> String -> Rule ()
154 | commitKeyword fname indents req
155 | = do mustContinue indents (Just req)
156 | decoratedKeyword fname req
157 | <|> the (Rule ()) (fatalError ("Expected '" ++ req ++ "'"))
158 | mustContinue indents Nothing
160 | commitSymbol : OriginDesc -> String -> Rule ()
161 | commitSymbol fname req
162 | = decoratedSymbol fname req
163 | <|> fatalError ("Expected '" ++ req ++ "'")
165 | continueWithDecorated : OriginDesc -> IndentInfo -> String -> Rule ()
166 | continueWithDecorated fname indents req
167 | = mustContinue indents (Just req) *> decoratedSymbol fname req
170 | continueWith : IndentInfo -> String -> Rule ()
171 | continueWith indents req
172 | = mustContinue indents (Just req) *> symbol req
174 | iOperator : Rule OpStr
176 | = OpSymbols <$> operator
177 | <|> Backticked <$> (symbol "`" *> name <* symbol "`")
180 | = UnnamedExpArg PTerm
181 | | UnnamedAutoArg PTerm
182 | | NamedArg Name PTerm
185 | argTerm : ArgType -> PTerm
186 | argTerm (UnnamedExpArg t) = t
187 | argTerm (UnnamedAutoArg t) = t
188 | argTerm (NamedArg _ t) = t
189 | argTerm (WithArg t) = t
192 | debugString : OriginDesc -> Rule PTerm
193 | debugString fname = do
194 | di <- bounds debugInfo
195 | pure $
PPrimVal (boundToFC fname di) $
Str $
case di.val of
197 | let bnds = di.bounds in
199 | [ "File \{show fname}"
200 | , "line \{show (startLine bnds)}"
201 | , "characters \{show (startCol bnds)}\{
202 | ifThenElse (startLine bnds == endLine bnds)
203 | ("-\{show (endCol bnds)}")
207 | DebugFile => "\{show fname}"
208 | DebugLine => "\{show (startLine di.bounds)}"
209 | DebugCol => "\{show (startCol di.bounds)}"
211 | totalityOpt : OriginDesc -> Rule TotalReq
213 | = (decoratedKeyword fname "partial" $> PartialOK)
214 | <|> (decoratedKeyword fname "total" $> Total)
215 | <|> (decoratedKeyword fname "covering" $> CoveringOnly)
217 | fnOpt : OriginDesc -> Rule PFnOpt
219 | = do x <- totalityOpt fname
220 | pure $
IFnOpt (Totality x)
223 | appExpr : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm
224 | appExpr q fname indents
225 | = case_ fname indents
226 | <|> doBlock fname indents
227 | <|> lam fname indents
228 | <|> lazy fname indents
229 | <|> if_ fname indents
230 | <|> with_ fname indents
231 | <|> do b <- bounds (MkPair <$> simpleExpr fname indents <*> many (argExpr q fname indents))
232 | (f, args) <- pure b.val
233 | pure (applyExpImp (start b) (end b) f (concat args))
234 | <|> do b <- fcBounds (MkPair <$> fcBounds iOperator <*> expr pdef fname indents)
235 | (op, arg) <- pure b.val
236 | pure (PPrefixOp b.fc op arg)
237 | <|> fail "Expected 'case', 'if', 'do', application or operator expression"
239 | applyExpImp : FilePos -> FilePos -> PTerm ->
242 | applyExpImp start end f [] = f
243 | applyExpImp start end f (UnnamedExpArg exp :: args)
244 | = applyExpImp start end (PApp (MkFC fname start end) f exp) args
245 | applyExpImp start end f (UnnamedAutoArg imp :: args)
246 | = applyExpImp start end (PAutoApp (MkFC fname start end) f imp) args
247 | applyExpImp start end f (NamedArg n imp :: args)
248 | = let fc = MkFC fname start end in
249 | applyExpImp start end (PNamedApp fc f n imp) args
250 | applyExpImp start end f (WithArg exp :: args)
251 | = applyExpImp start end (PWithApp (MkFC fname start end) f exp) args
253 | argExpr : ParseOpts -> OriginDesc -> IndentInfo -> Rule (List ArgType)
254 | argExpr q fname indents
255 | = do continue indents
256 | arg <- simpleExpr fname indents
257 | the (EmptyRule _) $
case arg of
258 | PHole loc _ n => pure [UnnamedExpArg (PHole loc True n)]
259 | t => pure [UnnamedExpArg t]
260 | <|> do continue indents
261 | braceArgs fname indents
263 | then do continue indents
264 | decoratedSymbol fname "|"
265 | arg <- expr ({withOK := False} q) fname indents
267 | else fail "| not allowed here"
269 | underscore : FC -> ArgType
270 | underscore fc = NamedArg (UN Underscore) (PImplicit fc)
272 | braceArgs : OriginDesc -> IndentInfo -> Rule (List ArgType)
273 | braceArgs fname indents
274 | = do start <- bounds (decoratedSymbol fname "{")
276 | list <- sepBy (decoratedSymbol fname ",")
277 | $
do x <- bounds (UN . Basic <$> decoratedSimpleNamedArg fname)
278 | let fc = boundToFC fname x
279 | option (NamedArg x.val $
PRef fc x.val)
280 | $
do tm <- decoratedSymbol fname "=" *> typeExpr pdef fname indents
281 | pure (NamedArg x.val tm)
282 | matchAny <- option [] (if isCons list then
283 | do decoratedSymbol fname ","
284 | x <- bounds (decoratedSymbol fname "_")
285 | pure [underscore (boundToFC fname x)]
286 | else fail "non-empty list required")
287 | end <- bounds (decoratedSymbol fname "}")
288 | matchAny <- do let fc = boundToFC fname (mergeBounds start end)
289 | pure $
if isNil list
290 | then [underscore fc]
292 | pure $
matchAny ++ list
294 | <|> do decoratedSymbol fname "@{"
296 | tm <- typeExpr pdef fname indents
297 | decoratedSymbol fname "}"
298 | pure [UnnamedAutoArg tm]
300 | with_ : OriginDesc -> IndentInfo -> Rule PTerm
301 | with_ fname indents
302 | = do b <- bounds (do decoratedKeyword fname "with"
304 | ns <- singleName <|> nameList
306 | rhs <- expr pdef fname indents
308 | (ns, rhs) <- pure b.val
309 | pure (PWithUnambigNames (boundToFC fname b) ns rhs)
311 | singleName : Rule (List (FC, Name))
314 | pure [(boundToFC fname n, n.val)]
316 | nameList : Rule (List (FC, Name))
318 | decoratedSymbol fname "["
320 | ns <- sepBy1 (decoratedSymbol fname ",") (bounds name)
321 | decoratedSymbol fname "]"
322 | pure (map (\ n => (boundToFC fname n, n.val)) $
forget ns)
326 | opBinderTypes : OriginDesc -> IndentInfo -> WithBounds PTerm -> Rule (OperatorLHSInfo PTerm)
327 | opBinderTypes fname indents boundName =
328 | do decoratedSymbol fname ":"
329 | ty <- typeExpr pdef fname indents
330 | decoratedSymbol fname "<-"
331 | exp <- expr pdef fname indents
332 | pure (BindExplicitType boundName.val ty exp)
333 | <|> do decoratedSymbol fname "<-"
334 | exp <- expr pdef fname indents
335 | pure (BindExpr boundName.val exp)
336 | <|> do decoratedSymbol fname ":"
337 | ty <- typeExpr pdef fname indents
338 | pure (BindType boundName.val ty)
340 | opBinder : OriginDesc -> IndentInfo -> Rule (OperatorLHSInfo PTerm)
341 | opBinder fname indents
342 | = do boundName <- bounds (expr plhs fname indents)
343 | opBinderTypes fname indents boundName
345 | autobindOp : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm
346 | autobindOp q fname indents
347 | = do b <- fcBounds $
do
348 | binder <- fcBounds $
parens fname (opBinder fname indents)
350 | op <- fcBounds iOperator
352 | e <- expr q fname indents
353 | pure (binder, op, e)
354 | pure (POp b.fc (fst b.val) (fst (snd b.val)) (snd (snd b.val)))
356 | opExprBase : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm
357 | opExprBase q fname indents
358 | = do l <- bounds (appExpr q fname indents)
360 | then do r <- bounds (continue indents
361 | *> decoratedSymbol fname "="
362 | *> opExprBase q fname indents)
364 | let fc = boundToFC fname (mergeBounds l r)
365 | opFC = virtualiseFC fc
366 | in POp fc (map NoBinder l.withFC)
367 | (MkFCVal opFC (OpSymbols $
UN $
Basic "="))
369 | else fail "= not allowed")
371 | (do b <- bounds $
do
373 | op <- fcBounds iOperator
374 | e <- case op.val of
375 | OpSymbols (UN (Basic "$")) => typeExpr q fname indents
376 | _ => expr q fname indents
378 | (op, r) <- pure b.val
379 | let fc = boundToFC fname (mergeBounds l b)
380 | pure (POp fc (map NoBinder l.withFC) op r))
383 | opExpr : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm
384 | opExpr q fname indents = autobindOp q fname indents
385 | <|> opExprBase q fname indents
387 | dpairType : OriginDesc -> WithBounds t -> IndentInfo -> Rule PTerm
388 | dpairType fname start indents
389 | = do loc <- bounds (do x <- decoratedSimpleBinderUName fname
390 | decoratedSymbol fname ":"
391 | ty <- typeExpr pdef fname indents
393 | (x, ty) <- pure loc.val
394 | op <- bounds (symbol "**")
395 | rest <- bounds (nestedDpair fname loc indents <|> typeExpr pdef fname indents)
396 | pure (PDPair (boundToFC fname (mergeBounds start rest))
397 | (boundToFC fname op)
398 | (PRef (boundToFC fname loc) x)
402 | nestedDpair : OriginDesc -> WithBounds t -> IndentInfo -> Rule PTerm
403 | nestedDpair fname start indents
404 | = dpairType fname start indents
405 | <|> do l <- expr pdef fname indents
406 | loc <- bounds (symbol "**")
407 | rest <- bounds (nestedDpair fname loc indents <|> expr pdef fname indents)
408 | pure (PDPair (boundToFC fname (mergeBounds start rest))
409 | (boundToFC fname loc)
411 | (PImplicit (boundToFC fname (mergeBounds start rest)))
414 | bracketedExpr : OriginDesc -> WithBounds t -> IndentInfo -> Rule PTerm
415 | bracketedExpr fname s indents
419 | = do b <- bounds (do op <- fcBounds iOperator
420 | e <- expr pdef fname indents
421 | continueWithDecorated fname indents ")"
423 | (op, e) <- pure b.val
424 | actD (toNonEmptyFC $
boundToFC fname s, Keyword, Nothing)
425 | let fc = boundToFC fname (mergeBounds s b)
426 | pure (PSectionL fc op e)
428 | b <- bounds $
forget <$> some (bounds postfixProj)
429 | decoratedSymbol fname ")"
430 | actD (toNonEmptyFC $
boundToFC fname s, Keyword, Nothing)
431 | let projs = map (\ proj => (boundToFC fname proj, proj.val)) b.val
432 | pure $
PPostfixAppPartial (boundToFC fname b) projs
434 | <|> do b <- bounds (continueWith indents ")")
435 | pure (PUnit (boundToFC fname (mergeBounds s b)))
437 | <|> do dpairType fname s indents <* (decorate fname Typ $
symbol ")")
438 | <* actD (toNonEmptyFC $
boundToFC fname s, Typ, Nothing)
439 | <|> do e <- bounds (typeExpr pdef fname indents)
441 | (do loc <- bounds (symbol "**")
442 | rest <- bounds ((nestedDpair fname loc indents <|> expr pdef fname indents) <* symbol ")")
443 | pure (PDPair (boundToFC fname (mergeBounds s rest))
444 | (boundToFC fname loc)
446 | (PImplicit (boundToFC fname (mergeBounds s rest)))
449 | ((do op <- bounds (fcBounds iOperator <* decoratedSymbol fname ")")
450 | actD (toNonEmptyFC $
boundToFC fname s, Keyword, Nothing)
451 | let fc = boundToFC fname (mergeBounds s op)
452 | pure (PSectionR fc e.val op.val)
455 | tuple fname s indents e.val))
456 | <|> do here <- location
457 | let fc = MkFC fname here here
458 | let var = PRef fc (MN "__leftTupleSection" 0)
459 | ts <- bounds (nonEmptyTuple fname s indents var)
460 | pure (PLam fc top Explicit var (PInfer fc) ts.val)
462 | getInitRange : List (WithBounds PTerm) -> EmptyRule (PTerm, Maybe PTerm)
463 | getInitRange [x] = pure (x.val, Nothing)
464 | getInitRange [x,y] = pure (x.val, Just y.val)
465 | getInitRange _ = fatalError "Invalid list range syntax"
467 | listRange : OriginDesc -> WithBounds t -> IndentInfo -> List (WithBounds PTerm) -> Rule PTerm
468 | listRange fname s indents xs
469 | = do b <- bounds (decoratedSymbol fname "]")
470 | let fc = boundToFC fname (mergeBounds s b)
471 | rstate <- getInitRange xs
472 | decorateKeywords fname xs
473 | pure (PRangeStream fc (fst rstate) (snd rstate))
474 | <|> do y <- bounds (expr pdef fname indents <* decoratedSymbol fname "]")
475 | let fc = boundToFC fname (mergeBounds s y)
476 | rstate <- getInitRange xs
477 | decorateKeywords fname xs
478 | pure (PRange fc (fst rstate) (snd rstate) y.val)
480 | listExpr : OriginDesc -> WithBounds () -> IndentInfo -> Rule PTerm
481 | listExpr fname s indents
482 | = do b <- bounds (do ret <- expr pnowith fname indents
483 | decoratedSymbol fname "|"
484 | conds <- sepBy1 (decoratedSymbol fname ",") (doAct fname indents)
485 | decoratedSymbol fname "]"
487 | (ret, conds) <- pure b.val
488 | pure (PComprehension (boundToFC fname (mergeBounds s b)) ret (concat conds))
489 | <|> do xs <- option [] $
do
490 | hd <- expr pdef fname indents
491 | tl <- many $
do b <- bounds (symbol ",")
492 | x <- mustWork $
expr pdef fname indents
494 | pure ((hd <$ s) :: tl)
495 | (do decoratedSymbol fname ".."
496 | listRange fname s indents xs)
497 | <|> (do b <- bounds (symbol "]")
499 | let fc = boundToFC fname (mergeBounds s b)
500 | nilFC = if null xs then fc else boundToFC fname b
501 | in PList fc nilFC (cast (map (\ t => (boundToFC fname t, t.val)) xs)))
503 | snocListExpr : OriginDesc -> WithBounds () -> IndentInfo -> Rule PTerm
504 | snocListExpr fname s indents
506 | do mHeadTail <- optional $
do
507 | hd <- many $
do x <- expr pdef fname indents
508 | b <- bounds (symbol ",")
510 | tl <- expr pdef fname indents
513 | b <- bounds (symbol "]")
515 | let xs : SnocList (WithBounds PTerm)
516 | = case mHeadTail of
518 | Just (hd,tl) => ([<] <>< hd) :< (tl <$ b)
519 | fc = boundToFC fname (mergeBounds s b)
520 | nilFC = ifThenElse (null xs) fc (boundToFC fname s)
521 | in PSnocList fc nilFC (map (\ t => (boundToFC fname t, t.val)) xs)
523 | nonEmptyTuple : OriginDesc -> WithBounds t -> IndentInfo -> PTerm -> Rule PTerm
524 | nonEmptyTuple fname s indents e
525 | = do vals <- some $
do b <- bounds (symbol ",")
526 | exp <- optional (typeExpr pdef fname indents)
527 | pure (boundToFC fname b, exp)
528 | end <- continueWithDecorated fname indents ")"
529 | actD (toNonEmptyFC (boundToFC fname s), Keyword, Nothing)
530 | pure $
let (start ::: rest) = vals in
531 | buildOutput (fst start) (mergePairs 0 start rest)
534 | lams : List (FC, PTerm) -> PTerm -> PTerm
536 | lams ((fc, var) :: vars) e
537 | = let vfc = virtualiseFC fc in
538 | PLam vfc top Explicit var (PInfer vfc) $
lams vars e
540 | buildOutput : FC -> (List (FC, PTerm), PTerm) -> PTerm
541 | buildOutput fc (vars, scope) = lams vars $
PPair fc e scope
543 | optionalPair : Int ->
544 | (FC, Maybe PTerm) -> (Int, (List (FC, PTerm), PTerm))
545 | optionalPair i (fc, Just e) = (i, ([], e))
546 | optionalPair i (fc, Nothing) =
547 | let var = PRef fc (MN "__infixTupleSection" i) in
548 | (i+1, ([(fc, var)], var))
550 | mergePairs : Int -> (FC, Maybe PTerm) ->
551 | List (FC, Maybe PTerm) -> (List (FC, PTerm), PTerm)
552 | mergePairs i hd [] = snd (optionalPair i hd)
553 | mergePairs i hd (exp :: rest)
554 | = let (j, (var, t)) = optionalPair i hd in
555 | let (vars, ts) = mergePairs j exp rest in
556 | (var ++ vars, PPair (fst exp) t ts)
559 | tuple : OriginDesc -> WithBounds t -> IndentInfo -> PTerm -> Rule PTerm
560 | tuple fname s indents e
561 | = nonEmptyTuple fname s indents e
562 | <|> do end <- bounds (continueWithDecorated fname indents ")")
563 | actD (toNonEmptyFC $
boundToFC fname s, Keyword, Nothing)
564 | pure (PBracketed (boundToFC fname (mergeBounds s end)) e)
566 | simpleExpr : OriginDesc -> IndentInfo -> Rule PTerm
567 | simpleExpr fname indents
569 | b <- bounds (do root <- simplerExpr fname indents
570 | projs <- many (bounds postfixProj)
571 | pure (root, projs))
572 | (root, projs) <- pure b.val
573 | let projs = map (\ proj => (boundToFC fname proj, proj.val)) projs
574 | pure $
case projs of
576 | _ => PPostfixApp (boundToFC fname b) root projs
577 | <|> debugString fname
578 | <|> do b <- bounds (forget <$> some (bounds postfixProj))
579 | pure $
let projs = map (\ proj => (boundToFC fname proj, proj.val)) b.val in
580 | PPostfixAppPartial (boundToFC fname b) projs
582 | simplerExpr : OriginDesc -> IndentInfo -> Rule PTerm
583 | simplerExpr fname indents
584 | = do b <- bounds (do x <- bounds (decoratedSimpleBinderUName fname)
585 | decoratedSymbol fname "@"
587 | expr <- simpleExpr fname indents
589 | (x, expr) <- pure b.val
590 | pure (PAs (boundToFC fname b) (boundToFC fname x) x.val expr)
591 | <|> do b <- bounds $
do
592 | mns <- decoratedNamespacedSymbol fname "[|"
593 | t <- expr pdef fname indents
594 | decoratedSymbol fname "|]"
596 | pure (PIdiom (boundToFC fname b) (snd b.val) (fst b.val))
598 | <|> record_ fname indents
599 | <|> singlelineStr pdef fname indents
600 | <|> multilineStr pdef fname indents
601 | <|> do b <- bounds $
do
602 | decoratedSymbol fname ".("
604 | t <- typeExpr pdef fname indents
605 | decoratedSymbol fname ")"
607 | pure (PDotted (boundToFC fname b) b.val)
608 | <|> do b <- bounds $
do
609 | decoratedSymbol fname "`("
610 | t <- typeExpr pdef fname indents
611 | decoratedSymbol fname ")"
613 | pure (PQuote (boundToFC fname b) b.val)
614 | <|> do b <- bounds $
do
615 | decoratedSymbol fname "`{"
617 | decoratedSymbol fname "}"
619 | pure (PQuoteName (boundToFC fname b) b.val)
620 | <|> do b <- bounds $
do
621 | decoratedSymbol fname "`["
622 | ts <- nonEmptyBlock (topDecl fname)
623 | decoratedSymbol fname "]"
625 | pure (PQuoteDecl (boundToFC fname b) (collectDefs (forget b.val)))
626 | <|> do b <- bounds (decoratedSymbol fname "~" *> simplerExpr fname indents)
627 | pure (PUnquote (boundToFC fname b) b.val)
628 | <|> do start <- bounds (symbol "(")
629 | bracketedExpr fname start indents
630 | <|> do start <- bounds (symbol "[<")
631 | snocListExpr fname start indents
632 | <|> do start <- bounds (symbol "[>" <|> symbol "[")
633 | listExpr fname start indents
634 | <|> do b <- bounds (decoratedSymbol fname "!" *> simpleExpr fname indents)
635 | pure (PBang (virtualiseFC $
boundToFC fname b) b.val)
636 | <|> do b <- bounds $
do decoratedPragma fname "logging"
637 | topic <- optional (split (('.') ==) <$> simpleStr)
639 | e <- expr pdef fname indents
640 | pure (MkPair (mkLogLevel' topic (integerToNat lvl)) e)
641 | (lvl, e) <- pure b.val
642 | pure (PUnifyLog (boundToFC fname b) lvl e)
643 | <|> withWarning "DEPRECATED: trailing lambda. Use a $ or parens"
644 | (lam fname indents)
646 | multiplicity : OriginDesc -> EmptyRule RigCount
648 | = case !(optional $
decorate fname Keyword intLit) of
649 | (Just 0) => pure erased
650 | (Just 1) => pure linear
651 | Nothing => pure top
652 | _ => fail "Invalid multiplicity (must be 0 or 1)"
654 | bindList : OriginDesc -> IndentInfo ->
655 | Rule (List (RigCount, WithBounds PTerm, PTerm))
656 | bindList fname indents
657 | = forget <$> sepBy1 (decoratedSymbol fname ",")
658 | (do rig <- multiplicity fname
659 | pat <- bounds (simpleExpr fname indents)
661 | (PInfer (boundToFC fname pat))
662 | (decoratedSymbol fname ":" *> opExpr pdef fname indents)
663 | pure (rig, pat, ty))
668 | pibindListName : OriginDesc -> IndentInfo ->
669 | Rule BasicMultiBinder
670 | pibindListName fname indents
671 | = do rig <- multiplicity fname
672 | ns <- sepBy1 (decoratedSymbol fname ",")
673 | (fcBounds binderName)
674 | decoratedSymbol fname ":"
675 | ty <- typeExpr pdef fname indents
677 | pure (MkBasicMultiBinder rig ns ty)
680 | binderName : Rule Name
681 | binderName = decoratedSimpleBinderUName fname
682 | <|> decorate fname Bound (UN <$> symbol "_" $> Underscore)
687 | bindSymbol : OriginDesc -> Rule (PiInfo PTerm)
689 | = (decoratedSymbol fname "->" $> Explicit)
690 | <|> (decoratedSymbol fname "=>" $> AutoImplicit)
695 | explicitPi : OriginDesc -> IndentInfo -> Rule PTerm
696 | explicitPi fname indents
697 | = NewPi <$> fcBounds (do
698 | b <- bounds $
parens fname $
pibindListName fname indents
699 | exp <- mustWorkBecause b.bounds "Cannot return a named argument"
701 | scope <- mustWork $
typeExpr pdef fname indents
702 | pure (MkPBinderScope (MkPBinder exp b.val) scope))
707 | autoImplicitPi : OriginDesc -> IndentInfo -> Rule PTerm
708 | autoImplicitPi fname indents
709 | = NewPi <$> fcBounds (do
710 | b <- bounds $
curly fname $
do
711 | decoratedKeyword fname "auto"
713 | binders <- pibindListName fname indents
715 | mustWorkBecause b.bounds "Cannot return an auto implicit argument"
716 | $
decoratedSymbol fname "->"
717 | scope <- mustWork $
typeExpr pdef fname indents
718 | pure (MkPBinderScope (MkPBinder AutoImplicit b.val) scope)
724 | defaultImplicitPi : OriginDesc -> IndentInfo -> Rule PTerm
725 | defaultImplicitPi fname indents
726 | = NewPi <$> fcBounds (do
727 | b <- bounds $
curly fname $
do
728 | decoratedKeyword fname "default"
730 | t <- simpleExpr fname indents
731 | binders <- pibindListName fname indents
732 | pure (MkPBinder (DefImplicit t) binders)
733 | mustWorkBecause b.bounds "Cannot return a default implicit argument"
734 | $
decoratedSymbol fname "->"
735 | scope <- mustWork $
typeExpr pdef fname indents
736 | pure (MkPBinderScope b.val scope)
742 | forall_ : OriginDesc -> IndentInfo -> Rule PTerm
743 | forall_ fname indents
744 | = Forall <$> fcBounds (do
746 | decoratedKeyword fname "forall"
748 | ns <- sepBy1 (decoratedSymbol fname ",")
749 | (fcBounds (decoratedSimpleBinderUName fname))
752 | mustWorkBecause b'.bounds "Expected ',' or '.'"
753 | $
decoratedSymbol fname "."
754 | scope <- mustWork $
typeExpr pdef fname indents
755 | pure (b.val, scope))
760 | implicitPi : OriginDesc -> IndentInfo -> Rule PTerm
761 | implicitPi fname indents
762 | = NewPi <$> fcBounds (do
763 | b <- bounds $
curly fname $
pibindListName fname indents
764 | mustWorkBecause b.bounds "Cannot return an implicit argument"
765 | $
decoratedSymbol fname "->"
766 | scope <- mustWork $
typeExpr pdef fname indents
767 | pure (MkPBinderScope (MkPBinder Implicit b.val) scope)
770 | lam : OriginDesc -> IndentInfo -> Rule PTerm
772 | = do decoratedSymbol fname "\\"
774 | switch <- optional (bounds $
decoratedKeyword fname "case")
776 | Nothing => continueLamImpossible <|> continueLam
777 | Just r => continueLamCase r
780 | continueLamImpossible : Rule PTerm
781 | continueLamImpossible = do
782 | lhs <- bounds (opExpr plhs fname indents)
783 | end <- bounds (decoratedKeyword fname "impossible")
785 | let fc = boundToFC fname (mergeBounds lhs end)
786 | alt = (MkImpossible fc lhs.val)
787 | fcCase = boundToFC fname lhs
788 | n = MN "lcase" 0 in
789 | (PLam fcCase top Explicit (PRef fcCase n) (PInfer fcCase) $
790 | PCase (virtualiseFC fc) [] (PRef fcCase n) [alt]))
792 | bindAll : List (RigCount, WithBounds PTerm, PTerm) -> PTerm -> PTerm
793 | bindAll [] scope = scope
794 | bindAll ((rig, pat, ty) :: rest) scope
795 | = PLam (boundToFC fname pat) rig Explicit pat.val ty
796 | (bindAll rest scope)
798 | continueLam : Rule PTerm
800 | binders <- bindList fname indents
801 | commitSymbol fname "=>"
802 | mustContinue indents Nothing
803 | scope <- typeExpr pdef fname indents
804 | pure (bindAll binders scope)
806 | continueLamCase : WithBounds () -> Rule PTerm
807 | continueLamCase endCase = do
808 | b <- bounds (forget <$> nonEmptyBlock (caseAlt fname))
810 | (let fc = boundToFC fname b
811 | fcCase = virtualiseFC $
boundToFC fname endCase
812 | n = MN "lcase" 0 in
813 | PLam fcCase top Explicit (PRef fcCase n) (PInfer fcCase) $
814 | PCase (virtualiseFC fc) [] (PRef fcCase n) b.val)
816 | letBlock : OriginDesc -> IndentInfo -> Rule (WithBounds (Either LetBinder LetDecl))
817 | letBlock fname indents = bounds (letBinder <||> letDecl) where
819 | letBinder : Rule LetBinder
820 | letBinder = do s <- bounds (MkPair <$> multiplicity fname <*> expr plhs fname indents)
821 | (rig, pat) <- pure s.val
822 | ty <- option (PImplicit (virtualiseFC $
boundToFC fname s))
823 | (decoratedSymbol fname ":" *> typeExpr (pnoeq pdef) fname indents)
824 | (decoratedSymbol fname "=" <|> decoratedSymbol fname ":=")
825 | val <- typeExpr pnowith fname indents
826 | alts <- block (patAlt fname)
827 | pure (MkLetBinder rig pat ty val alts)
829 | letDecl : Rule LetDecl
830 | letDecl = collectDefs . forget <$> nonEmptyBlock (try . topDecl fname)
832 | let_ : OriginDesc -> IndentInfo -> Rule PTerm
834 | = do decoratedKeyword fname "let"
836 | res <- nonEmptyBlock (letBlock fname)
837 | commitKeyword fname indents "in"
838 | scope <- typeExpr pdef fname indents
839 | pure (mkLets fname res scope)
841 | case_ : OriginDesc -> IndentInfo -> Rule PTerm
842 | case_ fname indents
843 | = do opts <- many (fnDirectOpt fname)
844 | b <- bounds (do decoratedKeyword fname "case"
845 | scr <- expr pdef fname indents
846 | mustWork (commitKeyword fname indents "of")
847 | alts <- block (caseAlt fname)
849 | (scr, alts) <- pure b.val
850 | pure (PCase (virtualiseFC $
boundToFC fname b) opts scr alts)
853 | caseAlt : OriginDesc -> IndentInfo -> Rule PClause
854 | caseAlt fname indents
855 | = do lhs <- bounds (opExpr plhs fname indents)
856 | caseRHS fname lhs indents lhs.val
858 | caseRHS : OriginDesc -> WithBounds t -> IndentInfo -> PTerm -> Rule PClause
859 | caseRHS fname start indents lhs
860 | = do rhs <- bounds $
do
861 | decoratedSymbol fname "=>"
862 | mustContinue indents Nothing
863 | typeExpr pdef fname indents
865 | let fc = boundToFC fname (mergeBounds start rhs)
866 | pure (MkPatClause fc lhs rhs.val [])
867 | <|> do end <- bounds (decoratedKeyword fname "impossible")
869 | pure (MkImpossible (boundToFC fname (mergeBounds start end)) lhs)
870 | <|> fatalError ("Expected '=>' or 'impossible'")
872 | if_ : OriginDesc -> IndentInfo -> Rule PTerm
874 | = do b <- bounds (do decoratedKeyword fname "if"
876 | x <- expr pdef fname indents
877 | commitKeyword fname indents "then"
878 | t <- typeExpr pdef fname indents
879 | commitKeyword fname indents "else"
880 | e <- typeExpr pdef fname indents
882 | mustWork $
atEnd indents
883 | (x, t, e) <- pure b.val
884 | pure (PIfThenElse (boundToFC fname b) x t e)
886 | record_ : OriginDesc -> IndentInfo -> Rule PTerm
887 | record_ fname indents
890 | withWarning oldSyntaxWarning (
892 | decoratedKeyword fname "record"
897 | bounds (body False))
898 | pure (PUpdate (boundToFC fname b) (forget b.val))
900 | oldSyntaxWarning : String
901 | oldSyntaxWarning = unlines
902 | [ "DEPRECATED: old record update syntax."
903 | , #" Use "{ f := v } p" instead of "record { f = v } p""#
904 | , #" and "{ f $= v } p" instead of "record { f $= v } p""#
907 | body : Bool -> Rule (List1 PFieldUpdate)
908 | body kw = curly fname $
do
910 | sepBy1 (decoratedSymbol fname ",") (field kw fname indents)
912 | field : Bool -> OriginDesc -> IndentInfo -> Rule PFieldUpdate
913 | field kw fname indents
914 | = do path <- map fieldName <$> [| decorate fname Function name :: many recFieldCompat |]
915 | upd <- (ifThenElse kw (decoratedSymbol fname "=") (decoratedSymbol fname ":=") $> PSetField)
917 | (decoratedSymbol fname "$=" $> PSetFieldApp)
918 | val <- typeExpr plhs fname indents
919 | pure (upd path val)
921 | fieldName : Name -> String
922 | fieldName (UN (Basic s)) = s
923 | fieldName (UN (Field s)) = s
924 | fieldName _ = "_impossible"
928 | recFieldCompat : Rule Name
929 | recFieldCompat = decorate fname Function postfixProj
930 | <|> (decoratedSymbol fname "->"
931 | *> decorate fname Function name)
933 | rewrite_ : OriginDesc -> IndentInfo -> Rule PTerm
934 | rewrite_ fname indents
935 | = do b <- bounds (do decoratedKeyword fname "rewrite"
936 | rule <- expr pdef fname indents
937 | commitKeyword fname indents "in"
938 | tm <- typeExpr pdef fname indents
940 | (rule, tm) <- pure b.val
941 | pure (PRewrite (boundToFC fname b) rule tm)
943 | doBlock : OriginDesc -> IndentInfo -> Rule PTerm
944 | doBlock fname indents
945 | = do b <- bounds $
decoratedKeyword fname "do" *> block (doAct fname)
947 | pure (PDoBlock (virtualiseFC $
boundToFC fname b) Nothing (concat b.val))
948 | <|> do nsdo <- bounds namespacedIdent
950 | the (EmptyRule PTerm) $
case nsdo.val of
953 | actions <- Core.bounds (block (doAct fname))
954 | let fc = virtualiseFC $
955 | boundToFC fname (mergeBounds nsdo actions)
956 | pure (PDoBlock fc ns (concat actions.val))
957 | _ => fail "Not a namespaced 'do'"
959 | validPatternVar : Name -> EmptyRule ()
960 | validPatternVar (UN Underscore) = pure ()
961 | validPatternVar (UN (Basic n))
962 | = unless (lowerFirst n) $
963 | fail "Not a pattern variable"
964 | validPatternVar _ = fail "Not a pattern variable"
966 | doAct : OriginDesc -> IndentInfo -> Rule (List PDo)
967 | doAct fname indents
968 | = do b <- bounds (do rig <- multiplicity fname
969 | n <- bounds (name <|> UN Underscore <$ symbol "_")
972 | validPatternVar n.val
973 | ty <- optional (decoratedSymbol fname ":" *> typeExpr (pnoeq pdef) fname indents)
974 | decoratedSymbol fname "<-"
975 | val <- expr pdef fname indents
976 | pure (n, rig, ty, val))
978 | let (n, rig, ty, val) = b.val
979 | pure [DoBind (boundToFC fname b) (boundToFC fname n) n.val rig ty val]
980 | <|> do decoratedKeyword fname "let"
982 | res <- nonEmptyBlock (letBlock fname)
983 | do b <- bounds (decoratedKeyword fname "in")
984 | fatalLoc {c = True} b.bounds "Let-in not supported in do block. Did you mean (let ... in ...)?"
987 | pure (mkDoLets fname res)
988 | <|> do b <- bounds (decoratedKeyword fname "rewrite" *> expr pdef fname indents)
990 | pure [DoRewrite (boundToFC fname b) b.val]
991 | <|> do e <- bounds (expr plhs fname indents)
992 | (atEnd indents $> [DoExp (virtualiseFC $
boundToFC fname e) e.val])
993 | <|> (do ty <- optional (decoratedSymbol fname ":" *> typeExpr (pnoeq pdef) fname indents)
994 | b <- bounds $
decoratedSymbol fname "<-" *> [| (expr pnowith fname indents, block (patAlt fname)) |]
996 | let (v, alts) = b.val
997 | let fc = virtualiseFC $
boundToFC fname (mergeBounds e b)
998 | pure [DoBindPat fc e.val ty v alts])
1000 | patAlt : OriginDesc -> IndentInfo -> Rule PClause
1002 | = do decoratedSymbol fname "|"
1005 | lazy : OriginDesc -> IndentInfo -> Rule PTerm
1007 | = do tm <- bounds (decorate fname Typ (exactIdent "Lazy")
1008 | *> simpleExpr fname indents
1009 | <* mustFailBecause "Lazy only takes one argument" (continue indents >> simpleExpr fname indents))
1010 | pure (PDelayed (boundToFC fname tm) LLazy tm.val)
1011 | <|> do tm <- bounds (decorate fname Typ (exactIdent "Inf")
1012 | *> simpleExpr fname indents
1013 | <* mustFailBecause "Inf only takes one argument" (continue indents >> simpleExpr fname indents))
1014 | pure (PDelayed (boundToFC fname tm) LInf tm.val)
1015 | <|> do tm <- bounds (decorate fname Data (exactIdent "Delay")
1016 | *> simpleExpr fname indents
1017 | <* mustFailBecause "Delay only takes one argument" (continue indents >> simpleExpr fname indents))
1018 | pure (PDelay (boundToFC fname tm) tm.val)
1019 | <|> do tm <- bounds (decorate fname Data (exactIdent "Force")
1020 | *> simpleExpr fname indents
1021 | <* mustFailBecause "Force only takes one argument" (continue indents >> simpleExpr fname indents))
1022 | pure (PForce (boundToFC fname tm) tm.val)
1024 | binder : OriginDesc -> IndentInfo -> Rule PTerm
1026 | = autoImplicitPi fname indents
1027 | <|> defaultImplicitPi fname indents
1028 | <|> forall_ fname indents
1029 | <|> implicitPi fname indents
1030 | <|> autobindOp pdef fname indents
1031 | <|> explicitPi fname indents
1034 | typeExpr : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm
1035 | typeExpr q fname indents
1038 | arg <- expr q fname indents
1039 | mscope <- optional $
do
1042 | scope <- mustWork $
typeExpr q fname indents
1046 | let fc = boundToFC fname arg_mscope
1047 | (arg, mscope) = arg_mscope.val
1051 | mkPi : FC -> PTerm -> Maybe (PiInfo PTerm, PTerm) -> PTerm
1052 | mkPi _ arg Nothing = arg
1053 | mkPi fc arg (Just (exp, a))
1054 | = PPi fc top exp Nothing arg a
1057 | expr : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm
1060 | <|> rewrite_ fname indents
1062 | do decoratedPragma fname "runElab"
1063 | expr pdef fname indents
1064 | pure (PRunElab (boundToFC fname b) b.val)
1065 | <|> opExpr q fname indents
1067 | interpBlock : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm
1068 | interpBlock q fname idents = interpBegin *> (mustWork $
expr q fname idents <* interpEnd)
1071 | singlelineStr : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm
1072 | singlelineStr q fname idents
1073 | = decorate fname Data $
1074 | do b <- bounds $
do begin <- bounds strBegin
1076 | xs <- many $
bounds $
(interpBlock q fname idents) <||> strLitLines
1077 | pstrs <- case traverse toPStr xs of
1078 | Left err => fatalLoc begin.bounds err
1079 | Right pstrs => pure $
pstrs
1081 | pure (begin.val, pstrs)
1082 | pure $
let (hashtag, str) = b.val in
1083 | PString (boundToFC fname b) hashtag str
1085 | toPStr : (WithBounds $
Either PTerm (List1 String)) -> Either String PStr
1086 | toPStr x = case x.val of
1087 | Right (str:::[]) => Right $
StrLiteral (boundToFC fname x) str
1088 | Right (_:::strs) => Left "Multi-line string is expected to begin with \"\"\""
1089 | Left tm => Right $
StrInterp (boundToFC fname x) tm
1092 | multilineStr : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm
1093 | multilineStr q fname idents
1094 | = decorate fname Data $
1095 | do b <- bounds $
do hashtag <- multilineBegin
1097 | xs <- many $
bounds $
(interpBlock q fname idents) <||> strLitLines
1100 | pure (hashtag, endloc, toLines xs [<] [<])
1101 | pure $
let (hashtag, (_, col), xs) = b.val in
1102 | PMultiline (boundToFC fname b) hashtag (fromInteger $
cast col) xs
1104 | toLines : List (WithBounds $
Either PTerm (List1 String)) ->
1105 | SnocList PStr -> SnocList (List PStr) -> List (List PStr)
1106 | toLines [] line acc = acc <>> [line <>> []]
1107 | toLines (x::xs) line acc = case x.val of
1109 | toLines xs (line :< StrInterp (boundToFC fname x) tm) acc
1111 | toLines xs (line :< StrLiteral (boundToFC fname x) str) acc
1112 | Right (str:::strs@(_::_)) =>
1113 | let fc = boundToFC fname x in
1114 | toLines xs [< StrLiteral fc (last strs)]
1115 | $
acc :< (line <>> [StrLiteral fc str])
1116 | <>< map (\str => [StrLiteral fc str]) (init strs)
1118 | fnDirectOpt : OriginDesc -> Rule PFnOpt
1120 | = do decoratedPragma fname "hint"
1121 | pure $
IFnOpt (Hint True)
1122 | <|> do decoratedPragma fname "globalhint"
1123 | pure $
IFnOpt (GlobalHint False)
1124 | <|> do decoratedPragma fname "defaulthint"
1125 | pure $
IFnOpt (GlobalHint True)
1126 | <|> do decoratedPragma fname "inline"
1129 | <|> do decoratedPragma fname "unsafe"
1132 | <|> do decoratedPragma fname "noinline"
1135 | <|> do decoratedPragma fname "deprecate"
1137 | pure $
IFnOpt Deprecate
1138 | <|> do decoratedPragma fname "tcinline"
1141 | <|> do decoratedPragma fname "extern"
1143 | <|> do decoratedPragma fname "macro"
1145 | <|> do decoratedPragma fname "spec"
1146 | ns <- sepBy (decoratedSymbol fname ",") name
1147 | pure $
IFnOpt (SpecArgs ns)
1148 | <|> do decoratedPragma fname "foreign"
1149 | cs <- block (expr pdef fname)
1151 | <|> do (decoratedPragma fname "export"
1152 | <|> withWarning noMangleWarning
1153 | (decoratedPragma fname "nomangle"))
1154 | cs <- block (expr pdef fname)
1155 | pure $
PForeignExport cs
1157 | noMangleWarning : String
1159 | DEPRECATED: "%nomangle".
1164 | visOption : OriginDesc -> Rule Visibility
1166 | = (decoratedKeyword fname "public" *> decoratedKeyword fname "export" $> Public)
1169 | <|> (bounds (decoratedKeyword fname "public") >>= \x : WithBounds ()
1170 | => the (Rule Visibility) (fatalLoc x.bounds
1171 | #""public" keyword by itself is not an export modifier, did you mean "public export"?"#))
1172 | <|> (decoratedKeyword fname "export" $> Export)
1173 | <|> (decoratedKeyword fname "private" $> Private)
1176 | visibility : OriginDesc -> EmptyRule (WithDefault Visibility Private)
1178 | = (specified <$> visOption fname)
1181 | exportVisibility : OriginDesc -> EmptyRule (WithDefault Visibility Export)
1183 | = (specified <$> visOption fname)
1189 | plainBinder : (fname : OriginDesc) => (indents : IndentInfo) => Rule PlainBinder
1190 | plainBinder = do name <- fcBounds (decoratedSimpleBinderUName fname)
1191 | decoratedSymbol fname ":"
1192 | ty <- typeExpr pdef fname indents
1198 | basicMultiBinder : (fname : OriginDesc) => (indents : IndentInfo) => Rule BasicMultiBinder
1200 | = do rig <- multiplicity fname
1201 | names <- sepBy1 (decoratedSymbol fname ",")
1202 | $
fcBounds (decoratedSimpleBinderUName fname)
1203 | decoratedSymbol fname ":"
1204 | ty <- typeExpr pdef fname indents
1205 | pure $
MkBasicMultiBinder rig names ty
1207 | tyDecls : Rule Name -> String -> OriginDesc -> IndentInfo -> Rule PTypeDecl
1208 | tyDecls declName predoc fname indents
1210 | docns <- sepBy1 (decoratedSymbol fname ",")
1211 | [| (optDocumentation fname, fcBounds declName) |]
1212 | b <- bounds $
decoratedSymbol fname ":"
1213 | mustWorkBecause b.bounds "Expected a type declaration" $
do
1214 | ty <- the (Rule PTerm) (typeExpr pdef fname indents)
1215 | pure $
MkPTy docns predoc ty
1219 | withFlags : OriginDesc -> EmptyRule (List WithFlag)
1221 | = (do decoratedPragma fname "syntactic"
1222 | (Syntactic ::) <$> withFlags fname)
1226 | withProblem : OriginDesc -> Int -> IndentInfo -> Rule PWithProblem
1227 | withProblem fname col indents
1228 | = do rig <- multiplicity fname
1229 | start <- mustWork $
bounds (decoratedSymbol fname "(")
1230 | wval <- bracketedExpr fname start indents
1232 | decoratedKeyword fname "proof"
1233 | pure (!(multiplicity fname), !(decoratedSimpleBinderUName fname))
1234 | pure (MkPWithProblem rig wval prf)
1237 | parseRHS : (withArgs : Nat) ->
1238 | OriginDesc -> WithBounds t -> Int ->
1239 | IndentInfo -> (lhs : (PTerm, List (FC, PTerm))) -> Rule PClause
1240 | parseRHS withArgs fname start col indents lhs
1242 | decoratedSymbol fname "="
1245 | rhs <- typeExpr pdef fname indents
1246 | ws <- option [] $
whereBlock fname col
1249 | mustWorkBecause b'.bounds "Not the end of a block entry, check indentation" $
atEnd indents
1250 | (rhs, ws) <- pure b.val
1251 | let fc = boundToFC fname (mergeBounds start b)
1252 | pure (MkPatClause fc (uncurry applyWithArgs lhs) rhs ws)
1253 | <|> do b <- bounds $
do
1254 | decoratedKeyword fname "with"
1256 | flags <- withFlags fname
1257 | wps <- sepBy1 (decoratedSymbol fname "|") (withProblem fname col indents)
1258 | ws <- mustWork $
nonEmptyBlockAfter col
1259 | $
clause (S (length wps.tail) + withArgs) (Just lhs) fname
1260 | pure (flags, wps, forget ws)
1261 | (flags, wps, ws) <- pure b.val
1262 | let fc = boundToFC fname (mergeBounds start b)
1263 | pure (MkWithClause fc (uncurry applyWithArgs lhs) wps flags ws)
1264 | <|> do end <- bounds (decoratedKeyword fname "impossible")
1266 | pure $
let fc = boundToFC fname (mergeBounds start end) in
1267 | MkImpossible fc (uncurry applyWithArgs lhs)
1269 | clause : (withArgs : Nat) ->
1270 | IMaybe (isSucc withArgs) (PTerm, List (FC, PTerm)) ->
1271 | OriginDesc -> IndentInfo -> Rule PClause
1272 | clause withArgs mlhs fname indents
1273 | = do b <- bounds (do col <- column
1274 | lhsws <- clauseLHS fname indents mlhs
1275 | extra <- many parseWithArg
1276 | pure (col, mapSnd (++ extra) lhsws))
1277 | let col = Builtin.fst b.val
1278 | let lhs = Builtin.snd b.val
1279 | let extra = Builtin.snd lhs
1282 | ifThenElse (withArgs /= length extra)
1283 | (fatalError $
"Wrong number of 'with' arguments:"
1284 | ++ " expected " ++ show withArgs
1285 | ++ " but got " ++ show (length extra))
1286 | (parseRHS withArgs fname b col indents lhs)
1289 | clauseLHS : OriginDesc -> IndentInfo ->
1290 | IMaybe b (PTerm, List (FC, PTerm)) ->
1291 | Rule (PTerm, List (FC, PTerm))
1293 | clauseLHS fname indent Nothing
1294 | = (,[]) <$> opExpr plhs fname indents
1296 | clauseLHS fname indent (Just lhs)
1297 | = do e <- opExpr plhs fname indents
1300 | let vfc = virtualiseFC fc in
1301 | bimap (substFC vfc) (map (map $
substFC vfc)) lhs
1304 | parseWithArg : Rule (FC, PTerm)
1306 | = do decoratedSymbol fname "|"
1307 | tm <- bounds (expr plhs fname indents)
1308 | pure (boundToFC fname tm, tm.val)
1310 | mkTyConType : OriginDesc -> FC -> List (WithBounds Name) -> PTerm
1311 | mkTyConType fname fc [] = PType (virtualiseFC fc)
1312 | mkTyConType fname fc (x :: xs)
1313 | = let bfc = boundToFC fname x in
1314 | PPi bfc top Explicit Nothing (PType (virtualiseFC fc))
1315 | $
mkTyConType fname fc xs
1317 | mkDataConType : PTerm -> List (WithFC ArgType) -> Maybe PTerm
1318 | mkDataConType ret [] = Just ret
1319 | mkDataConType ret (con@(MkWithData _ (UnnamedExpArg x)) :: xs)
1320 | = PPi con.fc top Explicit Nothing x <$> mkDataConType ret xs
1321 | mkDataConType ret (con@(MkWithData _ (UnnamedAutoArg x)) :: xs)
1322 | = PPi con.fc top AutoImplicit Nothing x <$> mkDataConType ret xs
1326 | simpleCon : OriginDesc -> PTerm -> IndentInfo -> Rule PTypeDecl
1327 | simpleCon fname ret indents
1328 | = do b <- bounds (do cdoc <- optDocumentation fname
1329 | cname <- fcBounds $
decoratedDataConstructorName fname
1330 | params <- the (EmptyRule $
List $
WithFC $
List ArgType)
1331 | $
many (fcBounds $
argExpr plhs fname indents)
1332 | let conType = the (Maybe PTerm) (mkDataConType ret
1333 | (concat (map distribData params)))
1334 | fromMaybe (fatalError "Named arguments not allowed in ADT constructors")
1335 | (pure . MkPTy (singleton ("", cname)) cdoc <$> conType)
1340 | simpleData : OriginDesc -> WithBounds t ->
1341 | WithBounds Name -> IndentInfo -> Rule PDataDecl
1342 | simpleData fname start tyName indents
1343 | = do b <- bounds (do params <- many (bounds $
decorate fname Bound name)
1344 | tyend <- bounds (decoratedSymbol fname "=")
1346 | let tyfc = boundToFC fname (mergeBounds start tyend)
1347 | let tyCon = PRef (boundToFC fname tyName) tyName.val
1348 | let toPRef = \ t => PRef (boundToFC fname t) t.val
1349 | let conRetTy = papply tyfc tyCon (map toPRef params)
1350 | cons <- sepBy1 (decoratedSymbol fname "|") (simpleCon fname conRetTy indents)
1351 | pure (params, tyfc, forget cons))
1352 | (params, tyfc, cons) <- pure b.val
1353 | pure (MkPData (boundToFC fname (mergeBounds start b)) tyName.val
1354 | (Just (mkTyConType fname tyfc params)) [] cons)
1356 | dataOpt : OriginDesc -> Rule DataOpt
1358 | = (decorate fname Keyword (exactIdent "noHints") $> NoHints)
1359 | <|> (decorate fname Keyword (exactIdent "uniqueSearch") $> UniqueSearch)
1360 | <|> (do b <- bounds $
decorate fname Keyword (exactIdent "search")
1361 | det <- mustWorkBecause b.bounds "Expected list of determining parameters" $
1362 | some (decorate fname Bound name)
1364 | <|> (decorate fname Keyword (exactIdent "external") $> External)
1365 | <|> (decorate fname Keyword (exactIdent "noNewtype") $> NoNewtype)
1367 | dataOpts : OriginDesc -> EmptyRule (List DataOpt)
1368 | dataOpts fname = option [] $
do
1369 | decoratedSymbol fname "["
1370 | opts <- sepBy1 (decoratedSymbol fname ",") (dataOpt fname)
1371 | decoratedSymbol fname "]"
1374 | dataBody : OriginDesc -> Int -> WithBounds t -> Name -> IndentInfo -> Maybe PTerm ->
1376 | dataBody fname mincol start n indents ty
1377 | = do ty <- maybe (fail "Telescope is not optional in forward declaration") pure ty
1379 | pure (MkPLater (boundToFC fname start) n ty)
1380 | <|> do b <- bounds (do (mustWork $
decoratedKeyword fname "where")
1382 | cs <- blockAfter mincol (tyDecls (mustWork $
decoratedDataConstructorName fname) "" fname)
1384 | (opts, cs) <- pure b.val
1385 | pure (MkPData (boundToFC fname (mergeBounds start b)) n ty opts cs)
1387 | gadtData : OriginDesc -> Int -> WithBounds t ->
1388 | WithBounds Name -> IndentInfo -> EmptyRule PDataDecl
1389 | gadtData fname mincol start tyName indents
1391 | do decoratedSymbol fname ":"
1393 | typeExpr pdef fname indents
1394 | dataBody fname mincol start tyName.val indents ty
1396 | dataDeclBody : OriginDesc -> IndentInfo -> Rule PDataDecl
1397 | dataDeclBody fname indents
1398 | = do b <- bounds (do col <- column
1399 | decoratedKeyword fname "data"
1400 | n <- mustWork (bounds $
decoratedDataTypeName fname)
1403 | simpleData fname b n indents <|> gadtData fname col b n indents
1406 | dataVisOpt : OriginDesc -> EmptyRule (WithDefault Visibility Private, Maybe TotalReq)
1408 | = do {
vis <- visOption fname ;
mbtot <- optional (totalityOpt fname) ;
pure (specified vis, mbtot) }
1409 | <|> do {
tot <- totalityOpt fname ;
vis <- visibility fname ;
pure (vis, Just tot) }
1410 | <|> pure (defaulted, Nothing)
1412 | dataDecl : (fname : OriginDesc) => (indents : IndentInfo) => Rule PDeclNoFC
1414 | = do doc <- optDocumentation fname
1415 | (vis,mbTot) <- dataVisOpt fname
1416 | dat <- dataDeclBody fname indents
1417 | pure (PData doc vis mbTot dat)
1419 | stripBraces : String -> String
1420 | stripBraces str = pack (drop '{' (reverse (drop '}' (reverse (unpack str)))))
1422 | drop : Char -> List Char -> List Char
1424 | drop c (c' :: xs) = if c == c' then drop c xs else c' :: xs
1428 | = (exactIdent "on" $> True)
1429 | <|> (exactIdent "off" $> False)
1430 | <|> fail "expected 'on' or 'off'"
1432 | extension : Rule LangExt
1434 | = (exactIdent "ElabReflection" $> ElabReflection)
1435 | <|> (exactIdent "Borrowing" $> Borrowing)
1436 | <|> fail "expected either 'ElabReflection' or 'Borrowing'"
1438 | logLevel : OriginDesc -> Rule (Maybe LogLevel)
1440 | = (Nothing <$ decorate fname Keyword (exactIdent "off"))
1441 | <|> do topic <- optional (split ('.' ==) <$> simpleStr)
1443 | pure (Just (mkLogLevel' topic (fromInteger lvl)))
1444 | <|> fail "expected a log level"
1446 | directive : (fname : OriginDesc) => (indents : IndentInfo) => Rule Directive
1448 | = do decoratedPragma fname "hide"
1449 | n <- (fixityNS <|> (HideName <$> name))
1452 | <|> do decoratedPragma fname "unhide"
1456 | <|> do decoratedPragma fname "foreign_impl"
1458 | cs <- block (expr pdef fname)
1460 | pure (ForeignImpl n cs)
1465 | <|> do decoratedPragma fname "logging"
1469 | <|> do decoratedPragma fname "auto_lazy"
1473 | <|> do decoratedPragma fname "unbound_implicits"
1476 | pure (UnboundImplicits b)
1477 | <|> do decoratedPragma fname "prefix_record_projections"
1480 | pure (PrefixRecordProjections b)
1481 | <|> do decoratedPragma fname "totality_depth"
1482 | lvl <- decorate fname Keyword $
intLit
1484 | pure (TotalityDepth (fromInteger lvl))
1485 | <|> do decoratedPragma fname "ambiguity_depth"
1486 | lvl <- decorate fname Keyword $
intLit
1488 | pure (AmbigDepth (fromInteger lvl))
1489 | <|> do decoratedPragma fname "auto_implicit_depth"
1490 | dpt <- decorate fname Keyword $
intLit
1492 | pure (AutoImplicitDepth (fromInteger dpt))
1493 | <|> do decoratedPragma fname "nf_metavar_threshold"
1494 | dpt <- decorate fname Keyword $
intLit
1496 | pure (NFMetavarThreshold (fromInteger dpt))
1497 | <|> do decoratedPragma fname "search_timeout"
1498 | t <- decorate fname Keyword $
intLit
1501 | <|> do decoratedPragma fname "pair"
1506 | pure (PairNames ty f s)
1507 | <|> do decoratedPragma fname "rewrite"
1511 | pure (RewriteName eq rw)
1512 | <|> do decoratedPragma fname "integerLit"
1516 | <|> do decoratedPragma fname "stringLit"
1520 | <|> do decoratedPragma fname "charLit"
1524 | <|> do decoratedPragma fname "doubleLit"
1528 | <|> do decoratedPragma fname "TTImpLit"
1532 | <|> do decoratedPragma fname "nameLit"
1536 | <|> do decoratedPragma fname "declsLit"
1540 | <|> do decoratedPragma fname "name"
1542 | ns <- sepBy1 (decoratedSymbol fname ",")
1543 | (decoratedSimpleBinderUName fname)
1545 | pure (Names n (forget (map nameRoot ns)))
1546 | <|> do decoratedPragma fname "start"
1547 | e <- expr pdef fname indents
1550 | <|> do decoratedPragma fname "allow_overloads"
1554 | <|> do decoratedPragma fname "language"
1555 | e <- mustWork extension
1558 | <|> do decoratedPragma fname "default"
1559 | tot <- totalityOpt fname
1561 | pure (DefaultTotality tot)
1565 | = (keyword "infixl" $> InfixL)
1566 | <|> (keyword "infixr" $> InfixR)
1567 | <|> (keyword "infix" $> Infix)
1568 | <|> (keyword "prefix" $> Prefix)
1570 | namespaceHead : OriginDesc -> Rule Namespace
1572 | = do decoratedKeyword fname "namespace"
1573 | decorate fname Namespace $
mustWork namespaceId
1575 | parameters {auto fname : OriginDesc} {auto indents : IndentInfo}
1576 | namespaceDecl : Rule PDeclNoFC
1578 | = do doc <- optDocumentation fname
1580 | ns <- namespaceHead fname
1581 | ds <- blockAfter col (topDecl fname)
1582 | pure (PNamespace ns (collectDefs ds))
1584 | transformDecl : Rule PDeclNoFC
1586 | = do decoratedPragma fname "transform"
1588 | lhs <- expr plhs fname indents
1589 | decoratedSymbol fname "="
1590 | rhs <- expr pnowith fname indents
1591 | pure (PTransform n lhs rhs)
1593 | runElabDecl : Rule PDeclNoFC
1596 | decoratedPragma fname "runElab"
1597 | tm <- expr pnowith fname indents
1601 | failDecls : Rule PDeclNoFC
1605 | decoratedKeyword fname "failing"
1607 | msg <- optional (decorate fname Data (simpleMultiStr <|> simpleStr ))
1608 | ds <- nonEmptyBlockAfter col (topDecl fname)
1609 | pure $
PFail msg (collectDefs $
forget ds)
1612 | mutualDecls : Rule PDeclNoFC
1616 | decoratedKeyword fname "mutual"
1618 | ds <- nonEmptyBlockAfter col (topDecl fname)
1619 | pure (PMutual (forget ds))
1621 | usingDecls : Rule PDeclNoFC
1624 | decoratedKeyword fname "using"
1626 | decoratedSymbol fname "("
1627 | us <- sepBy (decoratedSymbol fname ",")
1628 | (do n <- optional $
userName <* decoratedSymbol fname ":"
1629 | ty <- typeExpr pdef fname indents
1631 | decoratedSymbol fname ")"
1632 | ds <- nonEmptyBlockAfter col (topDecl fname)
1633 | pure (PUsing us (collectDefs (forget ds)))
1636 | builtinDecl : Rule PDeclNoFC
1638 | = do decoratedPragma fname "builtin"
1644 | visOpt : OriginDesc -> Rule (Either Visibility PFnOpt)
1646 | = do vis <- visOption fname
1648 | <|> do tot <- fnOpt fname
1650 | <|> do opt <- fnDirectOpt fname
1653 | getVisibility : Maybe Visibility -> List (Either Visibility PFnOpt) ->
1655 | getVisibility Nothing [] = pure Private
1656 | getVisibility (Just vis) [] = pure vis
1657 | getVisibility Nothing (Left x :: xs) = getVisibility (Just x) xs
1658 | getVisibility (Just vis) (Left x :: xs)
1659 | = fatalError "Multiple visibility modifiers"
1660 | getVisibility v (_ :: xs) = getVisibility v xs
1662 | recordConstructor : OriginDesc -> Rule (WithDoc $
AddFC Name)
1663 | recordConstructor fname
1664 | = do doc <- optDocumentation fname
1665 | decorate fname Keyword $
exactIdent "constructor"
1666 | n <- fcBounds $
mustWork $
decoratedDataConstructorName fname
1669 | autoImplicitField : OriginDesc -> IndentInfo -> Rule (PiInfo t)
1670 | autoImplicitField fname _ = AutoImplicit <$ decoratedKeyword fname "auto"
1672 | defImplicitField : OriginDesc -> IndentInfo -> Rule (PiInfo PTerm)
1673 | defImplicitField fname indents = do
1674 | decoratedKeyword fname "default"
1676 | t <- simpleExpr fname indents
1679 | constraints : OriginDesc -> IndentInfo -> EmptyRule (List (Maybe Name, PTerm))
1680 | constraints fname indents
1681 | = do tm <- appExpr pdef fname indents
1682 | decoratedSymbol fname "=>"
1683 | more <- constraints fname indents
1684 | pure ((Nothing, tm) :: more)
1685 | <|> do decoratedSymbol fname "("
1686 | n <- decorate fname Bound name
1687 | decoratedSymbol fname ":"
1688 | tm <- typeExpr pdef fname indents
1689 | decoratedSymbol fname ")"
1690 | decoratedSymbol fname "=>"
1691 | more <- constraints fname indents
1692 | pure ((Just n, tm) :: more)
1695 | implBinds : OriginDesc -> IndentInfo -> (namedImpl : Bool) ->
1696 | EmptyRule (List (AddFC (ImpParameter' PTerm)))
1697 | implBinds fname indents namedImpl = concatMap (map adjust) <$> go where
1699 | adjust : ImpParameter' PTerm -> AddFC (ImpParameter' PTerm)
1700 | adjust param = virtualiseFC param.name.fc :+ param
1702 | isDefaultImplicit : PiInfo a -> Bool
1703 | isDefaultImplicit (DefImplicit _) = True
1704 | isDefaultImplicit _ = False
1706 | go : EmptyRule (List (List (ImpParameter' PTerm)))
1707 | go = do decoratedSymbol fname "{"
1708 | piInfo <- bounds $
option Implicit $
defImplicitField fname indents
1709 | when (not namedImpl && isDefaultImplicit piInfo.val) $
1710 | fatalLoc piInfo.bounds "Default implicits are allowed only for named implementations"
1711 | ns <- map (\case (MkBasicMultiBinder rig names type) => map (\nm => Mk [rig, nm] (MkPiBindData piInfo.val type)) (forget names))
1712 | (pibindListName fname indents)
1713 | let ns = the (List (ImpParameter' PTerm)) ns
1715 | commitSymbol fname "->"
1720 | fieldDecl : (fname : OriginDesc) => IndentInfo -> Rule PField
1722 | = do doc <- optDocumentation fname
1723 | decoratedSymbol fname "{"
1725 | impl <- option Implicit (autoImplicitField fname indents <|> defImplicitField fname indents)
1726 | fs <- addFCBounds (fieldBody doc impl)
1727 | decoratedSymbol fname "}"
1730 | <|> do doc <- optDocumentation fname
1731 | fs <- addFCBounds (fieldBody doc Explicit)
1735 | fieldBody : String -> PiInfo PTerm -> Rule (RecordField' Name)
1737 | = do rig <- multiplicity fname
1738 | ns <- sepBy1 (decoratedSymbol fname ",")
1739 | (fcBounds (decorate fname Function name
1740 | <|> (do b <- bounds (symbol "_")
1741 | fatalLoc {c = True} b.bounds "Fields have to be named")))
1742 | decoratedSymbol fname ":"
1743 | ty <- typeExpr pdef fname indents
1744 | pure (Mk [doc, rig, forget ns] (MkPiBindData p ty))
1746 | parameters {auto fname : OriginDesc} {auto indents : IndentInfo}
1748 | ifaceParam : Rule BasicMultiBinder
1750 | = parens fname basicMultiBinder
1751 | <|> do n <- fcBounds (decorate fname Bound name)
1752 | pure (MkBasicMultiBinder erased (singleton n) (PInfer n.fc))
1754 | ifaceDecl : Rule PDeclNoFC
1756 | = do doc <- optDocumentation fname
1757 | vis <- visibility fname
1759 | decoratedKeyword fname "interface"
1761 | cons <- constraints fname indents
1762 | n <- decorate fname Typ name
1763 | params <- many ifaceParam
1765 | b <- bounds $
decoratedSymbol fname "|"
1766 | mustWorkBecause b.bounds "Expected list of determining parameters" $
1767 | sepBy1 (decoratedSymbol fname ",") (decorate fname Bound name)
1768 | decoratedKeyword fname "where"
1769 | dc <- optional (recordConstructor fname)
1770 | body <- blockAfter col (topDecl fname)
1772 | vis cons n doc params det dc (collectDefs body))
1774 | implDecl : Rule PDeclNoFC
1776 | = do doc <- optDocumentation fname
1777 | visOpts <- many (visOpt fname)
1778 | vis <- getVisibility Nothing visOpts
1779 | let opts = mapMaybe getRight visOpts
1781 | option () (decoratedKeyword fname "implementation")
1782 | iname <- optional $
decoratedSymbol fname "["
1783 | *> decorate fname Function name
1784 | <* decoratedSymbol fname "]"
1785 | impls <- implBinds fname indents (isJust iname)
1786 | cons <- constraints fname indents
1787 | n <- decorate fname Typ name
1788 | params <- many (continue indents *> simpleExpr fname indents)
1789 | nusing <- option [] $
decoratedKeyword fname "using"
1790 | *> forget <$> some (decorate fname Function name)
1791 | body <- optional $
decoratedKeyword fname "where" *> blockAfter col (topDecl fname)
1794 | PImplementation vis opts Single impls cons n params iname nusing
1797 | localClaim : Rule PClaimData
1799 | = do doc <- optDocumentation fname
1800 | visOpts <- many (visOpt fname)
1801 | vis <- getVisibility Nothing visOpts
1802 | let opts = mapMaybe getRight visOpts
1803 | rig <- multiplicity fname
1804 | cls <- tyDecls (decorate fname Function name)
1806 | pure $
MkPClaim rig vis opts cls
1810 | typedArg : Rule PBinder
1812 | = do params <- parens fname $
pibindListName fname indents
1813 | pure $
MkPBinder Explicit params
1814 | <|> do decoratedSymbol fname "{"
1817 | (pure AutoImplicit <* decoratedKeyword fname "auto"
1818 | <|> (decoratedKeyword fname "default" *> DefImplicit <$> simpleExpr fname indents)
1820 | params <- pibindListName fname indents
1821 | decoratedSymbol fname "}"
1822 | pure $
MkPBinder info params
1827 | recordParam : Rule PBinder
1830 | <|> do n <- fcBounds (decoratedSimpleBinderUName fname)
1831 | pure (MkFullBinder Explicit top n $
PInfer n.fc)
1834 | recordBody : String -> WithDefault Visibility Private ->
1840 | recordBody doc vis mbtot col n params
1841 | = do atEndIndent indents
1842 | pure (PRecord doc vis mbtot (MkPRecordLater n params))
1843 | <|> do mustWork $
decoratedKeyword fname "where"
1845 | dcflds <- blockWithOptHeaderAfter col
1846 | (\ idt => recordConstructor fname <* atEnd idt)
1848 | pure (PRecord doc vis mbtot
1849 | (MkPRecord n params opts (fst dcflds) (snd dcflds)))
1851 | recordDecl : Rule PDeclNoFC
1853 | = do doc <- optDocumentation fname
1854 | (vis,mbtot) <- dataVisOpt fname
1856 | decoratedKeyword fname "record"
1857 | n <- mustWork (decoratedDataTypeName fname)
1858 | paramss <- many (continue indents >> recordParam)
1859 | recordBody doc vis mbtot col n paramss
1864 | paramDecls : Rule PDeclNoFC
1867 | b1 <- decoratedKeyword fname "parameters"
1869 | args <- Right <$> newParamDecls
1870 | <|> Left <$> withWarning "DEPRECATED: old parameter syntax https://github.com/idris-lang/Idris2/issues/3447" oldParamDecls
1872 | declarations <- nonEmptyBlockAfter startCol (topDecl fname)
1874 | (collectDefs (forget declarations)))
1877 | oldParamDecls : Rule (List1 PlainBinder)
1879 | = parens fname $
sepBy1 (decoratedSymbol fname ",") plainBinder
1881 | newParamDecls : Rule (List1 PBinder)
1882 | newParamDecls = some typedArg
1885 | definition : Rule PDeclNoFC
1887 | = do nd <- clause 0 Nothing fname indents
1888 | pure (PDef (singleton nd))
1890 | operatorBindingKeyword : EmptyRule BindingModifier
1892 | = (decoratedKeyword fname "autobind" >> pure Autobind)
1893 | <|> (decoratedKeyword fname "typebind" >> pure Typebind)
1898 | = do vis <- exportVisibility fname
1899 | binding <- operatorBindingKeyword
1900 | b <- fcBounds (do fixity <- decorate fname Keyword $
fix
1902 | prec <- decorate fname Keyword $
intLit
1903 | ops <- sepBy1 (decoratedSymbol fname ",") iOperator
1904 | pure (MkPFixityData vis binding fixity (fromInteger prec) ops)
1911 | cgDirectiveDecl : Rule PDeclNoFC
1913 | = (>>=) {c1 = True, c2 = False} cgDirective $
\dir =>
1914 | let (cg1, cg2) = span isAlphaNum dir
1915 | in the (EmptyRule PDeclNoFC) $
pure $
1916 | PDirective (CGAction cg1 (stripBraces (trim cg2)))
1923 | = do id <- anyReservedIdent
1924 | the (Rule PDecl) $
fatalLoc id.bounds "Cannot begin a declaration with a reserved identifier"
1926 | <|> fcBounds (PClaim <$> localClaim)
1927 | <|> fcBounds (PDirective <$> directive)
1929 | <|> fcBounds definition
1932 | <|> fcBounds recordDecl
1933 | <|> fcBounds namespaceDecl
1935 | <|> fcBounds mutualDecls
1936 | <|> fcBounds paramDecls
1937 | <|> fcBounds usingDecls
1938 | <|> fcBounds builtinDecl
1939 | <|> fcBounds runElabDecl
1940 | <|> fcBounds transformDecl
1941 | <|> fcBounds cgDirectiveDecl
1943 | <|> do kw <- bounds $
keyword "import"
1944 | the (Rule PDecl) $
fatalLoc kw.bounds "Imports must go before any declarations or directives"
1946 | <|> do kw <- bounds anyKeyword
1947 | the (Rule PDecl) $
fatalLoc kw.bounds "Keyword '\{kw.val}' is not a valid start to a declaration"
1948 | <|> fatalError "Couldn't parse declaration"
1958 | collectDefs (def@(MkWithData _ (PDef cs)) :: ds)
1959 | = let (csWithFC, rest) = spanBy isPDef ds
1960 | cs' = cs ++ concat (map val csWithFC)
1961 | annot' = foldr {t=List}
1962 | (\fc1, fc2 => fromMaybe EmptyFC (mergeFC fc1 fc2))
1966 | MkFCVal annot' (PDef cs') :: assert_total (collectDefs rest)
1967 | collectDefs (MkWithData annot (PNamespace ns nds) :: ds)
1968 | = MkWithData annot (PNamespace ns (collectDefs nds)) :: collectDefs ds
1969 | collectDefs (MkWithData fc (PMutual nds) :: ds)
1970 | = MkWithData fc (PMutual (collectDefs nds)) :: collectDefs ds
1975 | import_ : OriginDesc -> IndentInfo -> Rule Import
1977 | = do b <- bounds (do decoratedKeyword fname "import"
1978 | reexp <- option False (decoratedKeyword fname "public" $> True)
1979 | ns <- decorate fname Module $
mustWork moduleIdent
1980 | nsAs <- option (miAsNamespace ns)
1981 | (do decorate fname Keyword $
exactIdent "as"
1982 | decorate fname Namespace $
mustWork namespaceId)
1983 | pure (reexp, ns, nsAs))
1985 | (reexp, ns, nsAs) <- pure b.val
1986 | pure (MkImport (boundToFC fname b) reexp ns nsAs)
1989 | progHdr : OriginDesc -> EmptyRule Module
1991 | = do b <- bounds (do doc <- optDocumentation fname
1992 | nspace <- option (nsAsModuleIdent mainNS)
1993 | (do decoratedKeyword fname "module"
1994 | decorate fname Module $
mustWork moduleIdent)
1995 | imports <- block (import_ fname)
1996 | pure (doc, nspace, imports))
1997 | (doc, nspace, imports) <- pure b.val
1998 | pure (MkModule (boundToFC fname b)
2002 | prog : OriginDesc -> EmptyRule Module
2004 | = do mod <- progHdr fname
2005 | ds <- block (topDecl fname)
2006 | pure $
{ decls := collectDefs ds} mod
2008 | parseMode : Rule REPLEval
2010 | = do exactIdent "typecheck"
2014 | <|> do exactIdent "normalise"
2016 | <|> do exactIdent "default"
2018 | <|> do exactIdent "normal"
2020 | <|> do exactIdent "normalize"
2022 | <|> do exactIdent "execute"
2024 | <|> do exactIdent "exec"
2026 | <|> do exactIdent "scheme"
2029 | setVarOption : Rule REPLOpt
2032 | mode <- option NormaliseAll parseMode
2034 | <|> do exactIdent "editor"
2041 | setOption : Bool -> Rule REPLOpt
2043 | = do exactIdent "showimplicits"
2044 | pure (ShowImplicits set)
2045 | <|> do exactIdent "shownamespace"
2046 | pure (ShowNamespace set)
2047 | <|> do exactIdent "showmachinenames"
2048 | pure (ShowMachineNames set)
2049 | <|> do exactIdent "showtypes"
2051 | <|> do exactIdent "profile"
2053 | <|> do exactIdent "evaltiming"
2055 | <|> if set then setVarOption else fatalError "Unrecognised option"
2057 | replCmd : List String -> Rule ()
2058 | replCmd [] = fail "Unrecognised command"
2064 | cmdName : String -> Rule String
2066 | _ <- optional (symbol ":")
2067 | terminal ("Unrecognised REPL command '" ++ str ++ "'") $
2069 | (Ident s) => if s == str then Just s else Nothing
2070 | (Keyword kw) => if kw == str then Just kw else Nothing
2071 | (Symbol "?") => Just "?"
2072 | (Symbol ":?") => Just "?"
2076 | data CmdArg : Type where
2114 | NamedCmdArg : String -> CmdArg -> CmdArg
2117 | WithDefaultArg : String -> CmdArg -> CmdArg
2120 | CSVArg : CmdArg -> CmdArg
2123 | Args : List CmdArg -> CmdArg
2127 | showCmdArg : CmdArg -> String
2129 | showCmdArg NameArg = "name"
2130 | showCmdArg ExprArg = "expr"
2131 | showCmdArg DocArg = "keyword|expr"
2132 | showCmdArg DeclsArg = "decls"
2133 | showCmdArg NumberArg = "number"
2134 | showCmdArg AutoNumberArg = "number|auto"
2135 | showCmdArg OptionArg = "option"
2136 | showCmdArg FileArg = "file"
2137 | showCmdArg ModuleArg = "module"
2138 | showCmdArg StringArg = "string"
2139 | showCmdArg OnOffArg = "(on|off)"
2140 | showCmdArg (CSVArg arg) = "[" ++ showCmdArg arg ++ "]"
2141 | showCmdArg (WithDefaultArg value arg) = showCmdArg arg ++ "|" ++ value
2142 | showCmdArg (NamedCmdArg name arg) = name ++ ":" ++ showCmdArg arg
2143 | showCmdArg args@(Args _) = show args
2149 | show OnOffArg = "(on|off)"
2150 | show (Args args) = showSep " " (map show args)
2151 | show arg = "<" ++ showCmdArg arg ++ ">"
2154 | knownCommands : List (String, String)
2156 | explain ["t", "type"] "Check the type of an expression" ++
2157 | [ ("ti", "Check the type of an expression, showing implicit arguments")
2158 | , ("printdef", "Show the definition of a pattern-matching function")
2160 | explain ["s", "search"] "Search for values by type" ++
2161 | [ ("di", "Show debugging information for a name")
2163 | explain ["module", "import"] "Import an extra module" ++
2164 | [ ("package", "Import every module of the package")
2166 | explain ["q", "quit", "exit"] "Exit the Idris system" ++
2167 | [ ("cwd", "Displays the current working directory")
2168 | , ("cd", "Change the current working directory")
2169 | , ("sh", "Run a shell command")
2173 | , " eval specify what evaluation mode to use:"
2175 | , " normalise|normalize|normal"
2179 | , " editor specify the name of the editor command"
2181 | , " cg specify the codegen/backend to use"
2182 | , " builtin codegens are:"
2188 | , " showimplicits enable displaying implicit arguments as part of the"
2191 | , " shownamespace enable displaying namespaces as part of the output"
2193 | , " showmachinenames enable displaying machine names as part of the"
2196 | , " showtypes enable displaying the type of the term as part of"
2201 | , " evaltiming enable timing how long evaluation takes and"
2202 | , " displaying this before the printing of the output"
2205 | , ("unset", "Unset an option")
2206 | , ("opts", "Show current options settings")
2208 | explain ["c", "compile"] "Compile to an executable" ++
2209 | [ ("exec", "Compile to an executable and run")
2210 | , ("directive", "Set a codegen-specific directive")
2212 | explain ["l", "load"] "Load a file" ++
2213 | explain ["r", "reload"] "Reload current file" ++
2214 | explain ["e", "edit"] "Edit current file using $EDITOR or $VISUAL" ++
2215 | explain ["miss", "missing"] "Show missing clauses" ++
2216 | [ ("total", "Check the totality of a name")
2217 | , ("doc", "Show documentation for a keyword, a name, or a primitive")
2218 | , ("browse", "Browse contents of a namespace")
2220 | explain ["log", "logging"] "Set logging level" ++
2221 | [ ("consolewidth", "Set the width of the console output (0 for unbounded) (auto by default)")
2223 | explain ["colour", "color"] "Whether to use colour for the console output (enabled by default)" ++
2224 | explain ["m", "metavars"] "Show remaining proof obligations (metavariables or holes)" ++
2225 | [ ("typeat", "Show type of term <n> defined on line <l> and column <c>")
2227 | explain ["cs", "casesplit"] "Case split term <n> defined on line <l> and column <c>" ++
2228 | explain ["ac", "addclause"] "Add clause to term <n> defined on line <l>" ++
2229 | explain ["ml", "makelemma"] "Make lemma for term <n> defined on line <l>" ++
2230 | explain ["mc", "makecase"] "Make case on term <n> defined on line <l>" ++
2231 | explain ["mw", "makewith"] "Add with expression on term <n> defined on line <l>" ++
2232 | [ ("intro", "Introduce unambiguous constructor in hole <n> defined on line <l>")
2233 | , ("refine", "Refine hole <h> with identifier <n> on line <l>")
2235 | explain ["ps", "proofsearch"] "Search for a proof" ++
2236 | [ ("psnext", "Show next proof")
2237 | , ("gd", "Try to generate a definition using proof-search")
2238 | , ("gdnext", "Show next definition")
2239 | , ("version", "Display the Idris version")
2241 | explain ["?", "h", "help"] (unlines
2242 | [ "Display help text, optionally of a specific command.\n"
2243 | , "If run without arguments, lists all the REPL commands along with their"
2244 | , "initial line of help text.\n"
2245 | , "More detailed help can then be obtained by running the :help command"
2246 | , "with another command as an argument, e.g."
2249 | , "(the leading ':' in the command argument is optional)"
2255 | First, declare the type of your new value, e.g.
2256 | :let myValue : List Nat
2258 | Then, define the value:
2259 | :let myValue = [1, 2, 3]
2261 | Now the value is in scope at the REPL:
2267 | explain ["fs", "fsearch"] """
2268 | Search for global definitions by sketching the names distribution of the wanted type(s).
2270 | The parameter must be in one of the forms A -> B, A -> _, or B, where A and B are space-delimited lists of global names.
2272 | Idris will return all of the entries in the context that have all of the names in A
2273 | in some argument and all of the names in B within the return type.
2279 | will match (among other things):
2281 | Prelude.List.mapMaybe : (a -> Maybe b) -> List a -> List b
2283 | Note that the query 'List Nat -> String' does not describe the type 'List Nat',
2284 | rather it describes both 'List a' and 'Nat' in the arguments.
2288 | explain : List String -> String -> List (String, String)
2289 | explain cmds expl = map (\s => (s, expl)) cmds
2292 | KnownCommand : String -> Type
2293 | KnownCommand cmd = IsJust (lookup cmd knownCommands)
2296 | data ParseCmd : Type where
2297 | ParseREPLCmd : (cmds : List String)
2298 | -> {auto 0 _ : All KnownCommand cmds}
2301 | ParseKeywordCmd : (cmds : List String)
2302 | -> {auto 0 _ : All KnownCommand cmds}
2305 | ParseIdentCmd : (cmd : String)
2306 | -> {auto 0 _ : KnownCommand cmd}
2310 | CommandDefinition : Type
2311 | CommandDefinition = (List String, CmdArg, String, Rule REPLCmd)
2315 | CommandTable = List CommandDefinition
2317 | extractNames : ParseCmd -> List String
2318 | extractNames (ParseREPLCmd names) = names
2319 | extractNames (ParseKeywordCmd keywords) = keywords
2320 | extractNames (ParseIdentCmd ident) = [ident]
2322 | runParseCmd : ParseCmd -> Rule ()
2323 | runParseCmd (ParseREPLCmd names) = replCmd names
2324 | runParseCmd (ParseKeywordCmd keywords) = choice $
map keyword keywords
2325 | runParseCmd (ParseIdentCmd ident) = exactIdent ident
2328 | noArgCmd : ParseCmd -> REPLCmd -> String -> CommandDefinition
2329 | noArgCmd parseCmd command doc = (names, NoArg, doc, parse)
2332 | names = extractNames parseCmd
2340 | nameArgCmd : ParseCmd -> (Name -> REPLCmd) -> String -> CommandDefinition
2341 | nameArgCmd parseCmd command doc = (names, NameArg, doc, parse)
2344 | names = extractNames parseCmd
2353 | stringArgCmd : ParseCmd -> (String -> REPLCmd) -> String -> CommandDefinition
2354 | stringArgCmd parseCmd command doc = (names, StringArg, doc, parse)
2357 | names = extractNames parseCmd
2363 | s <- mustWork simpleStr
2366 | getHelpType : EmptyRule HelpType
2368 | optCmd <- optional $
choice $
(cmdName . fst) <$> knownCommands
2372 | Just cmd => DetailedHelp $
fromMaybe "Unrecognised command '\{cmd}'"
2373 | $
lookup cmd knownCommands
2376 | -> (HelpType -> REPLCmd)
2379 | helpCmd parseCmd command doc = (names, StringArg, doc, parse)
2382 | names = extractNames parseCmd
2388 | helpType <- getHelpType
2389 | pure (command helpType)
2391 | moduleArgCmd : ParseCmd -> (ModuleIdent -> REPLCmd) -> String -> CommandDefinition
2392 | moduleArgCmd parseCmd command doc = (names, ModuleArg, doc, parse)
2395 | names = extractNames parseCmd
2401 | n <- mustWork moduleIdent
2404 | exprArgCmd : ParseCmd -> (PTerm -> REPLCmd) -> String -> CommandDefinition
2405 | exprArgCmd parseCmd command doc = (names, ExprArg, doc, parse)
2408 | names = extractNames parseCmd
2414 | tm <- mustWork $
typeExpr pdef (Virtual Interactive) init
2417 | docArgCmd : ParseCmd -> (DocDirective -> REPLCmd) -> String -> CommandDefinition
2418 | docArgCmd parseCmd command doc = (names, DocArg, doc, parse)
2421 | names = extractNames parseCmd
2425 | docLazyPrim : Rule PTerm
2427 | let placeholeder : PTerm' Name
2428 | placeholeder = PHole EmptyFC False "lazyDocPlaceholeder"
2429 | in do exactIdent "Lazy"
2430 | pure (PDelayed EmptyFC LLazy placeholeder)
2431 | <|> do exactIdent "Inf"
2432 | pure (PDelayed EmptyFC LInf placeholeder)
2433 | <|> do exactIdent "Delay"
2434 | pure (PDelay EmptyFC placeholeder)
2435 | <|> do exactIdent "Force"
2436 | pure (PForce EmptyFC placeholeder)
2443 | AModule <$ keyword "module" <*> moduleIdent
2444 | <|> Keyword <$> anyKeyword
2445 | <|> Symbol <$> (anyReservedSymbol <* eoi
2446 | <|> parens (Virtual Interactive) anyReservedSymbol <* eoi)
2448 | IdiomBrackets <$ symbol "[|" <* symbol "|]"
2449 | <|> NameQuote <$ symbol "`{" <* symbol "}"
2450 | <|> TermQuote <$ symbol "`(" <* symbol ")"
2451 | <|> DeclQuote <$ symbol "`[" <* symbol "]"
2455 | <|> typeExpr pdef (Virtual Interactive) init
2459 | declsArgCmd : ParseCmd -> (List PDecl -> REPLCmd) -> String -> CommandDefinition
2460 | declsArgCmd parseCmd command doc = (names, DeclsArg, doc, parse)
2463 | names = extractNames parseCmd
2468 | tm <- mustWork $
topDecl (Virtual Interactive) init
2471 | optArgCmd : ParseCmd -> (REPLOpt -> REPLCmd) -> Bool -> String -> CommandDefinition
2472 | optArgCmd parseCmd command set doc = (names, OptionArg, doc, parse)
2475 | names = extractNames parseCmd
2481 | opt <- mustWork $
setOption set
2484 | numberArgCmd : ParseCmd -> (Nat -> REPLCmd) -> String -> CommandDefinition
2485 | numberArgCmd parseCmd command doc = (names, NumberArg, doc, parse)
2488 | names = extractNames parseCmd
2495 | pure (command (fromInteger i))
2497 | autoNumberArgCmd : ParseCmd -> (Maybe Nat -> REPLCmd) -> String -> CommandDefinition
2498 | autoNumberArgCmd parseCmd command doc = (names, AutoNumberArg, doc, parse)
2501 | names = extractNames parseCmd
2503 | autoNumber : Rule (Maybe Nat)
2504 | autoNumber = Nothing <$ keyword "auto"
2505 | <|> Just . fromInteger <$> intLit
2511 | mi <- mustWork autoNumber
2514 | onOffArgCmd : ParseCmd -> (Bool -> REPLCmd) -> String -> CommandDefinition
2515 | onOffArgCmd parseCmd command doc = (names, OnOffArg, doc, parse)
2518 | names = extractNames parseCmd
2527 | compileArgsCmd : ParseCmd -> (PTerm -> String -> REPLCmd) -> String -> CommandDefinition
2528 | compileArgsCmd parseCmd command doc
2529 | = (names, Args [FileArg, ExprArg], doc, parse)
2532 | names = extractNames parseCmd
2538 | n <- mustWork unqualifiedName
2539 | tm <- mustWork $
expr pdef (Virtual Interactive) init
2542 | loggingArgCmd : ParseCmd -> (Maybe LogLevel -> REPLCmd) -> String -> CommandDefinition
2543 | loggingArgCmd parseCmd command doc = (names, Args [StringArg, NumberArg], doc, parse) where
2546 | names = extractNames parseCmd
2552 | lvl <- mustWork $
logLevel (Virtual Interactive)
2555 | editLineNameArgCmd : ParseCmd -> (Bool -> Int -> Name -> EditCmd) -> String -> CommandDefinition
2556 | editLineNameArgCmd parseCmd command doc = (names, Args [NamedCmdArg "l" NumberArg, NamedCmdArg "n" StringArg], doc, parse) where
2559 | names = extractNames parseCmd
2565 | upd <- option False (symbol "!" $> True)
2566 | line <- fromInteger <$> mustWork intLit
2568 | pure (Editing $
command upd line n)
2570 | editLineColNameArgCmd : ParseCmd -> (Bool -> Int -> Int -> Name -> EditCmd) -> String -> CommandDefinition
2571 | editLineColNameArgCmd parseCmd command doc =
2573 | , Args [ NamedCmdArg "l" NumberArg
2574 | , NamedCmdArg "c" NumberArg
2575 | , NamedCmdArg "n" StringArg
2582 | names = extractNames parseCmd
2588 | upd <- option False (symbol "!" $> True)
2589 | line <- fromInteger <$> mustWork intLit
2590 | col <- fromInteger <$> mustWork intLit
2592 | pure (Editing $
command upd line col n)
2594 | editLineNamePTermArgCmd : ParseCmd -> (Bool -> Int -> Name -> PTerm -> EditCmd) -> String -> CommandDefinition
2595 | editLineNamePTermArgCmd parseCmd command doc =
2597 | , Args [ NamedCmdArg "l" NumberArg
2598 | , NamedCmdArg "h" StringArg
2599 | , NamedCmdArg "e" ExprArg
2606 | names = extractNames parseCmd
2612 | upd <- option False (symbol "!" $> True)
2613 | line <- fromInteger <$> mustWork intLit
2615 | n <- mustWork $
typeExpr pdef (Virtual Interactive) init
2616 | pure (Editing $
command upd line h n)
2618 | editLineNameCSVArgCmd : ParseCmd
2619 | -> (Bool -> Int -> Name -> List Name -> EditCmd)
2622 | editLineNameCSVArgCmd parseCmd command doc =
2624 | , Args [ NamedCmdArg "l" NumberArg
2625 | , NamedCmdArg "n" StringArg
2626 | , NamedCmdArg "h" (CSVArg NameArg)
2633 | names = extractNames parseCmd
2639 | upd <- option False (symbol "!" $> True)
2640 | line <- fromInteger <$> mustWork intLit
2642 | hints <- mustWork $
sepBy (symbol ",") name
2643 | pure (Editing $
command upd line n hints)
2645 | editLineNameOptionArgCmd : ParseCmd
2646 | -> (Bool -> Int -> Name -> Nat -> EditCmd)
2649 | editLineNameOptionArgCmd parseCmd command doc =
2651 | , Args [ NamedCmdArg "l" NumberArg
2652 | , NamedCmdArg "n" StringArg
2653 | , NamedCmdArg "r" (WithDefaultArg "0" NumberArg)
2660 | names = extractNames parseCmd
2666 | upd <- option False (symbol "!" $> True)
2667 | line <- fromInteger <$> mustWork intLit
2669 | nreject <- fromInteger <$> option 0 intLit
2670 | pure (Editing $
command upd line n nreject)
2672 | firstHelpLine : (cmd : String) -> {auto 0 _ : KnownCommand cmd} -> String
2674 | head . (split ((==) '\n')) $
2675 | fromMaybe "Failed to look up '\{cmd}' (SHOULDN'T HAPPEN!)" $
2676 | lookup cmd knownCommands
2679 | parserCommandsForHelp : CommandTable
2680 | parserCommandsForHelp =
2681 | [ exprArgCmd (ParseREPLCmd ["t", "type"]) Check (firstHelpLine "t")
2682 | , exprArgCmd (ParseREPLCmd ["ti"]) CheckWithImplicits (firstHelpLine "ti")
2683 | , exprArgCmd (ParseREPLCmd ["printdef"]) PrintDef (firstHelpLine "printdef")
2684 | , exprArgCmd (ParseREPLCmd ["s", "search"]) TypeSearch (firstHelpLine "s")
2685 | , nameArgCmd (ParseIdentCmd "di") DebugInfo (firstHelpLine "di")
2686 | , moduleArgCmd (ParseKeywordCmd ["module", "import"]) ImportMod (firstHelpLine "module")
2687 | , stringArgCmd (ParseREPLCmd ["package"]) ImportPackage (firstHelpLine "package")
2688 | , noArgCmd (ParseREPLCmd ["q", "quit", "exit"]) Quit (firstHelpLine "q")
2689 | , noArgCmd (ParseREPLCmd ["cwd"]) CWD (firstHelpLine "cwd")
2690 | , stringArgCmd (ParseREPLCmd ["cd"]) CD (firstHelpLine "cd")
2691 | , stringArgCmd (ParseREPLCmd ["sh"]) RunShellCommand (firstHelpLine "sh")
2692 | , optArgCmd (ParseIdentCmd "set") SetOpt True (firstHelpLine "set")
2693 | , optArgCmd (ParseIdentCmd "unset") SetOpt False (firstHelpLine "unset")
2694 | , noArgCmd (ParseREPLCmd ["opts"]) GetOpts (firstHelpLine "opts")
2695 | , compileArgsCmd (ParseREPLCmd ["c", "compile"]) Compile (firstHelpLine "c")
2696 | , exprArgCmd (ParseIdentCmd "exec") Exec (firstHelpLine "exec")
2697 | , stringArgCmd (ParseIdentCmd "directive") CGDirective (firstHelpLine "directive")
2698 | , stringArgCmd (ParseREPLCmd ["l", "load"]) Load (firstHelpLine "l")
2699 | , noArgCmd (ParseREPLCmd ["r", "reload"]) Reload (firstHelpLine "r")
2700 | , noArgCmd (ParseREPLCmd ["e", "edit"]) Edit (firstHelpLine "e")
2701 | , nameArgCmd (ParseREPLCmd ["miss", "missing"]) Missing (firstHelpLine "miss")
2702 | , nameArgCmd (ParseKeywordCmd ["total"]) Total (firstHelpLine "total")
2703 | , docArgCmd (ParseIdentCmd "doc") Doc (firstHelpLine "doc")
2704 | , moduleArgCmd (ParseIdentCmd "browse") (Browse . miAsNamespace) (firstHelpLine "browse")
2705 | , loggingArgCmd (ParseREPLCmd ["log", "logging"]) SetLog (firstHelpLine "log")
2706 | , autoNumberArgCmd (ParseREPLCmd ["consolewidth"]) SetConsoleWidth (firstHelpLine "consolewidth")
2707 | , onOffArgCmd (ParseREPLCmd ["colour", "color"]) SetColor (firstHelpLine "colour")
2708 | , noArgCmd (ParseREPLCmd ["m", "metavars"]) Metavars (firstHelpLine "m")
2709 | , editLineColNameArgCmd (ParseREPLCmd ["typeat"]) (const TypeAt) (firstHelpLine "typeat")
2710 | , editLineColNameArgCmd (ParseREPLCmd ["cs", "casesplit"]) CaseSplit (firstHelpLine "cs")
2711 | , editLineNameArgCmd (ParseREPLCmd ["ac", "addclause"]) AddClause (firstHelpLine "ac")
2712 | , editLineNameArgCmd (ParseREPLCmd ["ml", "makelemma"]) MakeLemma (firstHelpLine "ml")
2713 | , editLineNameArgCmd (ParseREPLCmd ["mc", "makecase"]) MakeCase (firstHelpLine "mc")
2714 | , editLineNameArgCmd (ParseREPLCmd ["mw", "makewith"]) MakeWith (firstHelpLine "mw")
2715 | , editLineNameArgCmd (ParseREPLCmd ["intro"]) Intro (firstHelpLine "intro")
2716 | , editLineNamePTermArgCmd (ParseREPLCmd ["refine"]) Refine (firstHelpLine "refine")
2717 | , editLineNameCSVArgCmd (ParseREPLCmd ["ps", "proofsearch"]) ExprSearch (firstHelpLine "ps")
2718 | , noArgCmd (ParseREPLCmd ["psnext"]) (Editing ExprSearchNext) (firstHelpLine "psnext")
2719 | , editLineNameOptionArgCmd (ParseREPLCmd ["gd"]) GenerateDef (firstHelpLine "gd")
2720 | , noArgCmd (ParseREPLCmd ["gdnext"]) (Editing GenerateDefNext) (firstHelpLine "gdnext")
2721 | , noArgCmd (ParseREPLCmd ["version"]) ShowVersion (firstHelpLine "version")
2722 | , helpCmd (ParseREPLCmd ["?", "h", "help"]) Help (firstHelpLine "?")
2723 | , declsArgCmd (ParseKeywordCmd ["let"]) NewDefn (firstHelpLine "let")
2724 | , exprArgCmd (ParseREPLCmd ["fs", "fsearch"]) FuzzyTypeSearch (firstHelpLine "fs")
2728 | help : List (List String, CmdArg, String)
2729 | help = (["<expr>"], NoArg, "Evaluate an expression") ::
2730 | map (\ (names, args, text, _) =>
2731 | (map (":" ++) names, args, text)) parserCommandsForHelp
2733 | nonEmptyCommand : Rule REPLCmd
2735 | choice (map (\ (_, _, _, parser) => parser) parserCommandsForHelp)
2739 | tm <- typeExpr pdef (Virtual Interactive) init
2744 | aPTerm = typeExpr pdef (Virtual Interactive) init
2747 | command : EmptyRule REPLCmd
2752 | helpType <- getHelpType