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, PiInfo PTerm))
656 | bindList fname indents
657 | = forget <$> sepBy1 (decoratedSymbol fname ",") (explicitBind <|> implicitBind)
659 | explicitBind : Rule (RigCount, WithBounds PTerm, PTerm, PiInfo PTerm)
661 | rig <- multiplicity fname
662 | pat <- bounds (simpleExpr fname indents)
664 | (PInfer (boundToFC fname pat))
665 | (decoratedSymbol fname ":" *> opExpr pdef fname indents)
666 | pure (rig, pat, ty, Explicit)
668 | implicitBind : Rule (RigCount, WithBounds PTerm, PTerm, PiInfo PTerm)
669 | implicitBind = curly fname $
do
670 | rig <- multiplicity fname
671 | pat <- bounds (simpleExpr fname indents)
673 | (PInfer (boundToFC fname pat))
674 | (decoratedSymbol fname ":" *> opExpr pdef fname indents)
675 | pure (rig, pat, ty, Implicit)
680 | pibindListName : OriginDesc -> IndentInfo ->
681 | Rule BasicMultiBinder
682 | pibindListName fname indents
683 | = do rig <- multiplicity fname
684 | ns <- sepBy1 (decoratedSymbol fname ",")
685 | (fcBounds binderName)
686 | decoratedSymbol fname ":"
687 | ty <- typeExpr pdef fname indents
689 | pure (MkBasicMultiBinder rig ns ty)
692 | binderName : Rule Name
693 | binderName = decoratedSimpleBinderUName fname
694 | <|> decorate fname Bound (UN <$> symbol "_" $> Underscore)
699 | bindSymbol : OriginDesc -> Rule (PiInfo PTerm)
701 | = (decoratedSymbol fname "->" $> Explicit)
702 | <|> (decoratedSymbol fname "=>" $> AutoImplicit)
707 | explicitPi : OriginDesc -> IndentInfo -> Rule PTerm
708 | explicitPi fname indents
709 | = NewPi <$> fcBounds (do
710 | b <- bounds $
parens fname $
pibindListName fname indents
711 | exp <- mustWorkBecause b.bounds "Cannot return a named argument"
713 | scope <- mustWork $
typeExpr pdef fname indents
714 | pure (MkPBinderScope (MkPBinder exp b.val) scope))
719 | autoImplicitPi : OriginDesc -> IndentInfo -> Rule PTerm
720 | autoImplicitPi fname indents
721 | = NewPi <$> fcBounds (do
722 | b <- bounds $
curly fname $
do
723 | decoratedKeyword fname "auto"
725 | binders <- pibindListName fname indents
727 | mustWorkBecause b.bounds "Cannot return an auto implicit argument"
728 | $
decoratedSymbol fname "->"
729 | scope <- mustWork $
typeExpr pdef fname indents
730 | pure (MkPBinderScope (MkPBinder AutoImplicit b.val) scope)
736 | defaultImplicitPi : OriginDesc -> IndentInfo -> Rule PTerm
737 | defaultImplicitPi fname indents
738 | = NewPi <$> fcBounds (do
739 | b <- bounds $
curly fname $
do
740 | decoratedKeyword fname "default"
742 | t <- simpleExpr fname indents
743 | binders <- pibindListName fname indents
744 | pure (MkPBinder (DefImplicit t) binders)
745 | mustWorkBecause b.bounds "Cannot return a default implicit argument"
746 | $
decoratedSymbol fname "->"
747 | scope <- mustWork $
typeExpr pdef fname indents
748 | pure (MkPBinderScope b.val scope)
754 | forall_ : OriginDesc -> IndentInfo -> Rule PTerm
755 | forall_ fname indents
756 | = Forall <$> fcBounds (do
758 | decoratedKeyword fname "forall"
760 | ns <- sepBy1 (decoratedSymbol fname ",")
761 | (fcBounds (decoratedSimpleBinderUName fname))
764 | mustWorkBecause b'.bounds "Expected ',' or '.'"
765 | $
decoratedSymbol fname "."
766 | scope <- mustWork $
typeExpr pdef fname indents
767 | pure (b.val, scope))
772 | implicitPi : OriginDesc -> IndentInfo -> Rule PTerm
773 | implicitPi fname indents
774 | = NewPi <$> fcBounds (do
775 | b <- bounds $
curly fname $
pibindListName fname indents
776 | mustWorkBecause b.bounds "Cannot return an implicit argument"
777 | $
decoratedSymbol fname "->"
778 | scope <- mustWork $
typeExpr pdef fname indents
779 | pure (MkPBinderScope (MkPBinder Implicit b.val) scope)
782 | lam : OriginDesc -> IndentInfo -> Rule PTerm
784 | = do decoratedSymbol fname "\\"
786 | switch <- optional (bounds $
decoratedKeyword fname "case")
788 | Nothing => continueLamImpossible <|> continueLam
789 | Just r => continueLamCase r
792 | continueLamImpossible : Rule PTerm
793 | continueLamImpossible = do
794 | lhs <- bounds (opExpr plhs fname indents)
795 | end <- bounds (decoratedKeyword fname "impossible")
797 | let fc = boundToFC fname (mergeBounds lhs end)
798 | alt = (MkImpossible fc lhs.val)
799 | fcCase = boundToFC fname lhs
800 | n = MN "lcase" 0 in
801 | (PLam fcCase top Explicit (PRef fcCase n) (PInfer fcCase) $
802 | PCase (virtualiseFC fc) [] (PRef fcCase n) [alt]))
804 | bindAll : List (RigCount, WithBounds PTerm, PTerm, PiInfo PTerm) -> PTerm -> PTerm
805 | bindAll [] scope = scope
806 | bindAll ((rig, pat, ty, icit) :: rest) scope
807 | = PLam (boundToFC fname pat) rig icit pat.val ty
808 | (bindAll rest scope)
810 | continueLam : Rule PTerm
812 | binders <- bindList fname indents
813 | commitSymbol fname "=>"
814 | mustContinue indents Nothing
815 | scope <- typeExpr pdef fname indents
816 | pure (bindAll binders scope)
818 | continueLamCase : WithBounds () -> Rule PTerm
819 | continueLamCase endCase = do
820 | b <- bounds (forget <$> nonEmptyBlock (caseAlt fname))
822 | (let fc = boundToFC fname b
823 | fcCase = virtualiseFC $
boundToFC fname endCase
824 | n = MN "lcase" 0 in
825 | PLam fcCase top Explicit (PRef fcCase n) (PInfer fcCase) $
826 | PCase (virtualiseFC fc) [] (PRef fcCase n) b.val)
828 | letBlock : OriginDesc -> IndentInfo -> Rule (WithBounds (Either LetBinder LetDecl))
829 | letBlock fname indents = bounds (letBinder <||> letDecl) where
831 | letBinder : Rule LetBinder
832 | letBinder = do s <- bounds (MkPair <$> multiplicity fname <*> expr plhs fname indents)
833 | (rig, pat) <- pure s.val
834 | ty <- option (PImplicit (virtualiseFC $
boundToFC fname s))
835 | (decoratedSymbol fname ":" *> typeExpr (pnoeq pdef) fname indents)
836 | (decoratedSymbol fname "=" <|> decoratedSymbol fname ":=")
837 | val <- typeExpr pnowith fname indents
838 | alts <- block (patAlt fname)
839 | pure (MkLetBinder rig pat ty val alts)
841 | letDecl : Rule LetDecl
842 | letDecl = collectDefs . forget <$> nonEmptyBlock (try . topDecl fname)
844 | let_ : OriginDesc -> IndentInfo -> Rule PTerm
846 | = do decoratedKeyword fname "let"
848 | res <- nonEmptyBlock (letBlock fname)
849 | commitKeyword fname indents "in"
850 | scope <- typeExpr pdef fname indents
851 | pure (mkLets fname res scope)
853 | case_ : OriginDesc -> IndentInfo -> Rule PTerm
854 | case_ fname indents
855 | = do opts <- many (fnDirectOpt fname)
856 | b <- bounds (do decoratedKeyword fname "case"
857 | scr <- expr pdef fname indents
858 | mustWork (commitKeyword fname indents "of")
859 | alts <- block (caseAlt fname)
861 | (scr, alts) <- pure b.val
862 | pure (PCase (virtualiseFC $
boundToFC fname b) opts scr alts)
865 | caseAlt : OriginDesc -> IndentInfo -> Rule PClause
866 | caseAlt fname indents
867 | = do lhs <- bounds (opExpr plhs fname indents)
868 | caseRHS fname lhs indents lhs.val
870 | caseRHS : OriginDesc -> WithBounds t -> IndentInfo -> PTerm -> Rule PClause
871 | caseRHS fname start indents lhs
872 | = do rhs <- bounds $
do
873 | decoratedSymbol fname "=>"
874 | mustContinue indents Nothing
875 | typeExpr pdef fname indents
877 | let fc = boundToFC fname (mergeBounds start rhs)
878 | pure (MkPatClause fc lhs rhs.val [])
879 | <|> do end <- bounds (decoratedKeyword fname "impossible")
881 | pure (MkImpossible (boundToFC fname (mergeBounds start end)) lhs)
882 | <|> fatalError ("Expected '=>' or 'impossible'")
884 | if_ : OriginDesc -> IndentInfo -> Rule PTerm
886 | = do b <- bounds (do decoratedKeyword fname "if"
888 | x <- expr pdef fname indents
889 | commitKeyword fname indents "then"
890 | t <- typeExpr pdef fname indents
891 | commitKeyword fname indents "else"
892 | e <- typeExpr pdef fname indents
894 | mustWork $
atEnd indents
895 | (x, t, e) <- pure b.val
896 | pure (PIfThenElse (boundToFC fname b) x t e)
898 | record_ : OriginDesc -> IndentInfo -> Rule PTerm
899 | record_ fname indents
902 | withWarning oldSyntaxWarning (
904 | decoratedKeyword fname "record"
909 | bounds (body False))
910 | pure (PUpdate (boundToFC fname b) (forget b.val))
912 | oldSyntaxWarning : String
913 | oldSyntaxWarning = unlines
914 | [ "DEPRECATED: old record update syntax."
915 | , #" Use "{ f := v } p" instead of "record { f = v } p""#
916 | , #" and "{ f $= v } p" instead of "record { f $= v } p""#
919 | body : Bool -> Rule (List1 PFieldUpdate)
920 | body kw = curly fname $
do
922 | sepBy1 (decoratedSymbol fname ",") (field kw fname indents)
924 | field : Bool -> OriginDesc -> IndentInfo -> Rule PFieldUpdate
925 | field kw fname indents
926 | = do path <- map fieldName <$> [| decorate fname Function name :: many recFieldCompat |]
927 | upd <- (ifThenElse kw (decoratedSymbol fname "=") (decoratedSymbol fname ":=") $> PSetField)
929 | (decoratedSymbol fname "$=" $> PSetFieldApp)
930 | val <- typeExpr plhs fname indents
931 | pure (upd path val)
933 | fieldName : Name -> String
934 | fieldName (UN (Basic s)) = s
935 | fieldName (UN (Field s)) = s
936 | fieldName _ = "_impossible"
940 | recFieldCompat : Rule Name
941 | recFieldCompat = decorate fname Function postfixProj
942 | <|> (decoratedSymbol fname "->"
943 | *> decorate fname Function name)
945 | rewrite_ : OriginDesc -> IndentInfo -> Rule PTerm
946 | rewrite_ fname indents
947 | = do b <- bounds (do decoratedKeyword fname "rewrite"
948 | rule <- expr pdef fname indents
949 | commitKeyword fname indents "in"
950 | tm <- typeExpr pdef fname indents
952 | (rule, tm) <- pure b.val
953 | pure (PRewrite (boundToFC fname b) rule tm)
955 | doBlock : OriginDesc -> IndentInfo -> Rule PTerm
956 | doBlock fname indents
957 | = do b <- bounds $
decoratedKeyword fname "do" *> block (doAct fname)
959 | pure (PDoBlock (virtualiseFC $
boundToFC fname b) Nothing (concat b.val))
960 | <|> do nsdo <- bounds namespacedIdent
962 | the (EmptyRule PTerm) $
case nsdo.val of
965 | actions <- Core.bounds (block (doAct fname))
966 | let fc = virtualiseFC $
967 | boundToFC fname (mergeBounds nsdo actions)
968 | pure (PDoBlock fc ns (concat actions.val))
969 | _ => fail "Not a namespaced 'do'"
971 | validPatternVar : Name -> EmptyRule ()
972 | validPatternVar (UN Underscore) = pure ()
973 | validPatternVar (UN (Basic n))
974 | = unless (lowerFirst n) $
975 | fail "Not a pattern variable"
976 | validPatternVar _ = fail "Not a pattern variable"
978 | doAct : OriginDesc -> IndentInfo -> Rule (List PDo)
979 | doAct fname indents
980 | = do b <- bounds (do rig <- multiplicity fname
981 | n <- bounds (name <|> UN Underscore <$ symbol "_")
984 | validPatternVar n.val
985 | ty <- optional (decoratedSymbol fname ":" *> typeExpr (pnoeq pdef) fname indents)
986 | decoratedSymbol fname "<-"
987 | val <- expr pdef fname indents
988 | pure (n, rig, ty, val))
990 | let (n, rig, ty, val) = b.val
991 | pure [DoBind (boundToFC fname b) (boundToFC fname n) n.val rig ty val]
992 | <|> do decoratedKeyword fname "let"
994 | res <- nonEmptyBlock (letBlock fname)
995 | do b <- bounds (decoratedKeyword fname "in")
996 | fatalLoc {c = True} b.bounds "Let-in not supported in do block. Did you mean (let ... in ...)?"
999 | pure (mkDoLets fname res)
1000 | <|> do b <- bounds (decoratedKeyword fname "rewrite" *> expr pdef fname indents)
1002 | pure [DoRewrite (boundToFC fname b) b.val]
1003 | <|> do e <- bounds (expr plhs fname indents)
1004 | (atEnd indents $> [DoExp (virtualiseFC $
boundToFC fname e) e.val])
1005 | <|> (do ty <- optional (decoratedSymbol fname ":" *> typeExpr (pnoeq pdef) fname indents)
1006 | b <- bounds $
decoratedSymbol fname "<-" *> [| (expr pnowith fname indents, block (patAlt fname)) |]
1009 | let fc = virtualiseFC $
boundToFC fname (mergeBounds e b)
1010 | pure [DoBindPat fc e.val ty v alts])
1012 | patAlt : OriginDesc -> IndentInfo -> Rule PClause
1014 | = do decoratedSymbol fname "|"
1017 | lazy : OriginDesc -> IndentInfo -> Rule PTerm
1019 | = do tm <- bounds (decorate fname Typ (exactIdent "Lazy")
1020 | *> simpleExpr fname indents
1021 | <* mustFailBecause "Lazy only takes one argument" (continue indents >> simpleExpr fname indents))
1022 | pure (PDelayed (boundToFC fname tm) LLazy tm.val)
1023 | <|> do tm <- bounds (decorate fname Typ (exactIdent "Inf")
1024 | *> simpleExpr fname indents
1025 | <* mustFailBecause "Inf only takes one argument" (continue indents >> simpleExpr fname indents))
1026 | pure (PDelayed (boundToFC fname tm) LInf tm.val)
1027 | <|> do tm <- bounds (decorate fname Data (exactIdent "Delay")
1028 | *> simpleExpr fname indents
1029 | <* mustFailBecause "Delay only takes one argument" (continue indents >> simpleExpr fname indents))
1030 | pure (PDelay (boundToFC fname tm) tm.val)
1031 | <|> do tm <- bounds (decorate fname Data (exactIdent "Force")
1032 | *> simpleExpr fname indents
1033 | <* mustFailBecause "Force only takes one argument" (continue indents >> simpleExpr fname indents))
1034 | pure (PForce (boundToFC fname tm) tm.val)
1036 | binder : OriginDesc -> IndentInfo -> Rule PTerm
1038 | = autoImplicitPi fname indents
1039 | <|> defaultImplicitPi fname indents
1040 | <|> forall_ fname indents
1041 | <|> implicitPi fname indents
1042 | <|> autobindOp pdef fname indents
1043 | <|> explicitPi fname indents
1046 | typeExpr : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm
1047 | typeExpr q fname indents
1050 | arg <- expr q fname indents
1051 | mscope <- optional $
do
1054 | scope <- mustWork $
typeExpr q fname indents
1058 | let fc = boundToFC fname arg_mscope
1059 | (arg, mscope) = arg_mscope.val
1063 | mkPi : FC -> PTerm -> Maybe (PiInfo PTerm, PTerm) -> PTerm
1064 | mkPi _ arg Nothing = arg
1065 | mkPi fc arg (Just (exp, a))
1066 | = PPi fc top exp Nothing arg a
1069 | expr : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm
1072 | <|> rewrite_ fname indents
1074 | do decoratedPragma fname "runElab"
1075 | expr pdef fname indents
1076 | pure (PRunElab (boundToFC fname b) b.val)
1077 | <|> opExpr q fname indents
1079 | interpBlock : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm
1080 | interpBlock q fname idents = interpBegin *> (mustWork $
expr q fname idents <* interpEnd)
1083 | singlelineStr : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm
1084 | singlelineStr q fname idents
1085 | = decorate fname Data $
1086 | do b <- bounds $
do begin <- bounds strBegin
1088 | xs <- many $
bounds $
(interpBlock q fname idents) <||> strLitLines
1089 | pstrs <- case traverse toPStr xs of
1090 | Left err => fatalLoc begin.bounds err
1091 | Right pstrs => pure $
pstrs
1093 | pure (begin.val, pstrs)
1094 | pure $
let (hashtag, str) = b.val in
1095 | PString (boundToFC fname b) hashtag str
1097 | toPStr : (WithBounds $
Either PTerm (List1 String)) -> Either String PStr
1098 | toPStr x = case x.val of
1099 | Right (str:::[]) => Right $
StrLiteral (boundToFC fname x) str
1100 | Right (_:::strs) => Left "Multi-line string is expected to begin with \"\"\""
1101 | Left tm => Right $
StrInterp (boundToFC fname x) tm
1104 | multilineStr : ParseOpts -> OriginDesc -> IndentInfo -> Rule PTerm
1105 | multilineStr q fname idents
1106 | = decorate fname Data $
1107 | do b <- bounds $
do hashtag <- multilineBegin
1109 | xs <- many $
bounds $
(interpBlock q fname idents) <||> strLitLines
1112 | pure (hashtag, endloc, toLines xs [<] [<])
1113 | pure $
let (hashtag, (_, col), xs) = b.val in
1114 | PMultiline (boundToFC fname b) hashtag (fromInteger $
cast col) xs
1116 | toLines : List (WithBounds $
Either PTerm (List1 String)) ->
1117 | SnocList PStr -> SnocList (List PStr) -> List (List PStr)
1118 | toLines [] line acc = acc <>> [line <>> []]
1119 | toLines (x::xs) line acc = case x.val of
1121 | toLines xs (line :< StrInterp (boundToFC fname x) tm) acc
1123 | toLines xs (line :< StrLiteral (boundToFC fname x) str) acc
1124 | Right (str:::strs@(_::_)) =>
1125 | let fc = boundToFC fname x in
1126 | toLines xs [< StrLiteral fc (last strs)]
1127 | $
acc :< (line <>> [StrLiteral fc str])
1128 | <>< map (\str => [StrLiteral fc str]) (init strs)
1130 | fnDirectOpt : OriginDesc -> Rule PFnOpt
1132 | = do decoratedPragma fname "hint"
1133 | pure $
IFnOpt (Hint True)
1134 | <|> do decoratedPragma fname "globalhint"
1135 | pure $
IFnOpt (GlobalHint False)
1136 | <|> do decoratedPragma fname "defaulthint"
1137 | pure $
IFnOpt (GlobalHint True)
1138 | <|> do decoratedPragma fname "inline"
1141 | <|> do decoratedPragma fname "unsafe"
1144 | <|> do decoratedPragma fname "noinline"
1147 | <|> do decoratedPragma fname "deprecate"
1149 | pure $
IFnOpt Deprecate
1150 | <|> do decoratedPragma fname "tcinline"
1153 | <|> do decoratedPragma fname "extern"
1155 | <|> do decoratedPragma fname "macro"
1157 | <|> do decoratedPragma fname "spec"
1158 | ns <- sepBy (decoratedSymbol fname ",") name
1159 | pure $
IFnOpt (SpecArgs ns)
1160 | <|> do decoratedPragma fname "foreign"
1161 | cs <- block (expr pdef fname)
1163 | <|> do (decoratedPragma fname "export"
1164 | <|> withWarning noMangleWarning
1165 | (decoratedPragma fname "nomangle"))
1166 | cs <- block (expr pdef fname)
1167 | pure $
PForeignExport cs
1169 | noMangleWarning : String
1171 | DEPRECATED: "%nomangle".
1176 | visOption : OriginDesc -> Rule Visibility
1178 | = (decoratedKeyword fname "public" *> decoratedKeyword fname "export" $> Public)
1181 | <|> (bounds (decoratedKeyword fname "public") >>= \x : WithBounds ()
1182 | => the (Rule Visibility) (fatalLoc x.bounds
1183 | #""public" keyword by itself is not an export modifier, did you mean "public export"?"#))
1184 | <|> (decoratedKeyword fname "export" $> Export)
1185 | <|> (decoratedKeyword fname "private" $> Private)
1188 | visibility : OriginDesc -> EmptyRule (WithDefault Visibility Private)
1190 | = (specified <$> visOption fname)
1193 | exportVisibility : OriginDesc -> EmptyRule (WithDefault Visibility Export)
1195 | = (specified <$> visOption fname)
1201 | plainBinder : (fname : OriginDesc) => (indents : IndentInfo) => Rule PlainBinder
1202 | plainBinder = do name <- fcBounds (decoratedSimpleBinderUName fname)
1203 | decoratedSymbol fname ":"
1204 | ty <- typeExpr pdef fname indents
1210 | basicMultiBinder : (fname : OriginDesc) => (indents : IndentInfo) => Rule BasicMultiBinder
1212 | = do rig <- multiplicity fname
1213 | names <- sepBy1 (decoratedSymbol fname ",")
1214 | $
fcBounds (decoratedSimpleBinderUName fname)
1215 | decoratedSymbol fname ":"
1216 | ty <- typeExpr pdef fname indents
1217 | pure $
MkBasicMultiBinder rig names ty
1219 | tyDecls : Rule Name -> String -> OriginDesc -> IndentInfo -> Rule PTypeDecl
1220 | tyDecls declName predoc fname indents
1222 | docns <- sepBy1 (decoratedSymbol fname ",")
1223 | [| (optDocumentation fname, fcBounds declName) |]
1224 | b <- bounds $
decoratedSymbol fname ":"
1225 | mustWorkBecause b.bounds "Expected a type declaration" $
do
1226 | ty <- the (Rule PTerm) (typeExpr pdef fname indents)
1227 | pure $
MkPTy docns predoc ty
1231 | withFlags : OriginDesc -> EmptyRule (List WithFlag)
1233 | = (do decoratedPragma fname "syntactic"
1234 | (Syntactic ::) <$> withFlags fname)
1238 | withProblem : OriginDesc -> Int -> IndentInfo -> Rule PWithProblem
1239 | withProblem fname col indents
1240 | = do rig <- multiplicity fname
1241 | start <- mustWork $
bounds (decoratedSymbol fname "(")
1242 | wval <- bracketedExpr fname start indents
1244 | decoratedKeyword fname "proof"
1245 | pure (!(multiplicity fname), !(decoratedSimpleBinderUName fname))
1246 | pure (MkPWithProblem rig wval prf)
1249 | parseRHS : (withArgs : Nat) ->
1250 | OriginDesc -> WithBounds t -> Int ->
1251 | IndentInfo -> (lhs : (PTerm, List (FC, PTerm))) -> Rule PClause
1252 | parseRHS withArgs fname start col indents lhs
1254 | decoratedSymbol fname "="
1257 | rhs <- typeExpr pdef fname indents
1258 | ws <- option [] $
whereBlock fname col
1261 | mustWorkBecause b'.bounds "Not the end of a block entry, check indentation" $
atEnd indents
1262 | (rhs, ws) <- pure b.val
1263 | let fc = boundToFC fname (mergeBounds start b)
1264 | pure (MkPatClause fc (uncurry applyWithArgs lhs) rhs ws)
1265 | <|> do b <- bounds $
do
1266 | decoratedKeyword fname "with"
1268 | flags <- withFlags fname
1269 | wps <- sepBy1 (decoratedSymbol fname "|") (withProblem fname col indents)
1270 | ws <- mustWork $
nonEmptyBlockAfter col
1271 | $
clause (S (length wps.tail) + withArgs) (Just lhs) fname
1272 | pure (flags, wps, forget ws)
1273 | (flags, wps, ws) <- pure b.val
1274 | let fc = boundToFC fname (mergeBounds start b)
1275 | pure (MkWithClause fc (uncurry applyWithArgs lhs) wps flags ws)
1276 | <|> do end <- bounds (decoratedKeyword fname "impossible")
1278 | pure $
let fc = boundToFC fname (mergeBounds start end) in
1279 | MkImpossible fc (uncurry applyWithArgs lhs)
1281 | clause : (withArgs : Nat) ->
1282 | IMaybe (isSucc withArgs) (PTerm, List (FC, PTerm)) ->
1283 | OriginDesc -> IndentInfo -> Rule PClause
1284 | clause withArgs mlhs fname indents
1285 | = do b <- bounds (do col <- column
1286 | lhsws <- clauseLHS fname indents mlhs
1287 | extra <- many parseWithArg
1288 | pure (col, mapSnd (++ extra) lhsws))
1289 | let col = Builtin.fst b.val
1290 | let lhs = Builtin.snd b.val
1291 | let extra = Builtin.snd lhs
1294 | ifThenElse (withArgs /= length extra)
1295 | (fatalError $
"Wrong number of 'with' arguments:"
1296 | ++ " expected " ++ show withArgs
1297 | ++ " but got " ++ show (length extra))
1298 | (parseRHS withArgs fname b col indents lhs)
1301 | clauseLHS : OriginDesc -> IndentInfo ->
1302 | IMaybe b (PTerm, List (FC, PTerm)) ->
1303 | Rule (PTerm, List (FC, PTerm))
1305 | clauseLHS fname indent Nothing
1306 | = (,[]) <$> opExpr plhs fname indents
1308 | clauseLHS fname indent (Just lhs)
1309 | = do e <- opExpr plhs fname indents
1312 | let vfc = virtualiseFC fc in
1313 | bimap (substFC vfc) (map (map $
substFC vfc)) lhs
1316 | parseWithArg : Rule (FC, PTerm)
1318 | = do decoratedSymbol fname "|"
1319 | tm <- bounds (expr plhs fname indents)
1320 | pure (boundToFC fname tm, tm.val)
1322 | mkTyConType : OriginDesc -> FC -> List (WithBounds Name) -> PTerm
1323 | mkTyConType fname fc [] = PType (virtualiseFC fc)
1324 | mkTyConType fname fc (x :: xs)
1325 | = let bfc = boundToFC fname x in
1326 | PPi bfc top Explicit Nothing (PType (virtualiseFC fc))
1327 | $
mkTyConType fname fc xs
1329 | mkDataConType : PTerm -> List (WithFC ArgType) -> Maybe PTerm
1330 | mkDataConType ret [] = Just ret
1331 | mkDataConType ret (con@(MkWithData _ (UnnamedExpArg x)) :: xs)
1332 | = PPi con.fc top Explicit Nothing x <$> mkDataConType ret xs
1333 | mkDataConType ret (con@(MkWithData _ (UnnamedAutoArg x)) :: xs)
1334 | = PPi con.fc top AutoImplicit Nothing x <$> mkDataConType ret xs
1338 | simpleCon : OriginDesc -> PTerm -> IndentInfo -> Rule PTypeDecl
1339 | simpleCon fname ret indents
1340 | = do b <- bounds (do cdoc <- optDocumentation fname
1341 | cname <- fcBounds $
decoratedDataConstructorName fname
1342 | params <- the (EmptyRule $
List $
WithFC $
List ArgType)
1343 | $
many (fcBounds $
argExpr plhs fname indents)
1344 | let conType = the (Maybe PTerm) (mkDataConType ret
1345 | (concat (map distribData params)))
1346 | fromMaybe (fatalError "Named arguments not allowed in ADT constructors")
1347 | (pure . MkPTy (singleton ("", cname)) cdoc <$> conType)
1352 | simpleData : OriginDesc -> WithBounds t ->
1353 | WithBounds Name -> IndentInfo -> Rule PDataDecl
1354 | simpleData fname start tyName indents
1355 | = do b <- bounds (do params <- many (bounds $
decorate fname Bound name)
1356 | tyend <- bounds (decoratedSymbol fname "=")
1358 | let tyfc = boundToFC fname (mergeBounds start tyend)
1359 | let tyCon = PRef (boundToFC fname tyName) tyName.val
1360 | let toPRef = \ t => PRef (boundToFC fname t) t.val
1361 | let conRetTy = papply tyfc tyCon (map toPRef params)
1362 | cons <- sepBy1 (decoratedSymbol fname "|") (simpleCon fname conRetTy indents)
1363 | pure (params, tyfc, forget cons))
1364 | (params, tyfc, cons) <- pure b.val
1365 | pure (MkPData (boundToFC fname (mergeBounds start b)) tyName.val
1366 | (Just (mkTyConType fname tyfc params)) [] cons)
1368 | dataOpt : OriginDesc -> Rule DataOpt
1370 | = (decorate fname Keyword (exactIdent "noHints") $> NoHints)
1371 | <|> (decorate fname Keyword (exactIdent "uniqueSearch") $> UniqueSearch)
1372 | <|> (do b <- bounds $
decorate fname Keyword (exactIdent "search")
1373 | det <- mustWorkBecause b.bounds "Expected list of determining parameters" $
1374 | some (decorate fname Bound name)
1376 | <|> (decorate fname Keyword (exactIdent "external") $> External)
1377 | <|> (decorate fname Keyword (exactIdent "noNewtype") $> NoNewtype)
1379 | dataOpts : OriginDesc -> EmptyRule (List DataOpt)
1380 | dataOpts fname = option [] $
do
1381 | decoratedSymbol fname "["
1382 | opts <- sepBy1 (decoratedSymbol fname ",") (dataOpt fname)
1383 | decoratedSymbol fname "]"
1386 | dataBody : OriginDesc -> Int -> WithBounds t -> Name -> IndentInfo -> Maybe PTerm ->
1388 | dataBody fname mincol start n indents ty
1389 | = do ty <- maybe (fail "Telescope is not optional in forward declaration") pure ty
1391 | pure (MkPLater (boundToFC fname start) n ty)
1392 | <|> do b <- bounds (do (mustWork $
decoratedKeyword fname "where")
1394 | cs <- blockAfter mincol (tyDecls (mustWork $
decoratedDataConstructorName fname) "" fname)
1396 | (opts, cs) <- pure b.val
1397 | pure (MkPData (boundToFC fname (mergeBounds start b)) n ty opts cs)
1399 | gadtData : OriginDesc -> Int -> WithBounds t ->
1400 | WithBounds Name -> IndentInfo -> EmptyRule PDataDecl
1401 | gadtData fname mincol start tyName indents
1403 | do decoratedSymbol fname ":"
1405 | typeExpr pdef fname indents
1406 | dataBody fname mincol start tyName.val indents ty
1408 | dataDeclBody : OriginDesc -> IndentInfo -> Rule PDataDecl
1409 | dataDeclBody fname indents
1410 | = do b <- bounds (do col <- column
1411 | decoratedKeyword fname "data"
1412 | n <- mustWork (bounds $
decoratedDataTypeName fname)
1415 | simpleData fname b n indents <|> gadtData fname col b n indents
1418 | dataVisOpt : OriginDesc -> EmptyRule (WithDefault Visibility Private, Maybe TotalReq)
1420 | = do {
vis <- visOption fname ;
mbtot <- optional (totalityOpt fname) ;
pure (specified vis, mbtot) }
1421 | <|> do {
tot <- totalityOpt fname ;
vis <- visibility fname ;
pure (vis, Just tot) }
1422 | <|> pure (defaulted, Nothing)
1424 | dataDecl : (fname : OriginDesc) => (indents : IndentInfo) => Rule PDeclNoFC
1426 | = do doc <- optDocumentation fname
1427 | (vis,mbTot) <- dataVisOpt fname
1428 | dat <- dataDeclBody fname indents
1429 | pure (PData doc vis mbTot dat)
1431 | stripBraces : String -> String
1432 | stripBraces str = pack (drop '{' (reverse (drop '}' (reverse (unpack str)))))
1434 | drop : Char -> List Char -> List Char
1436 | drop c (c' :: xs) = if c == c' then drop c xs else c' :: xs
1440 | = (exactIdent "on" $> True)
1441 | <|> (exactIdent "off" $> False)
1442 | <|> fail "expected 'on' or 'off'"
1444 | extension : Rule LangExt
1446 | = (exactIdent "ElabReflection" $> ElabReflection)
1447 | <|> fail "expected 'ElabReflection'"
1449 | logLevel : OriginDesc -> Rule (Maybe LogLevel)
1451 | = (Nothing <$ decorate fname Keyword (exactIdent "off"))
1452 | <|> do topic <- optional (split ('.' ==) <$> simpleStr)
1454 | pure (Just (mkLogLevel' topic (fromInteger lvl)))
1455 | <|> fail "expected a log level"
1457 | directive : (fname : OriginDesc) => (indents : IndentInfo) => Rule Directive
1459 | = do decoratedPragma fname "hide"
1460 | n <- (fixityNS <|> (HideName <$> name))
1463 | <|> do decoratedPragma fname "unhide"
1467 | <|> do decoratedPragma fname "foreign_impl"
1469 | cs <- block (expr pdef fname)
1471 | pure (ForeignImpl n cs)
1476 | <|> do decoratedPragma fname "logging"
1480 | <|> do decoratedPragma fname "auto_lazy"
1484 | <|> do decoratedPragma fname "unbound_implicits"
1487 | pure (UnboundImplicits b)
1488 | <|> do decoratedPragma fname "prefix_record_projections"
1491 | pure (PrefixRecordProjections b)
1492 | <|> do decoratedPragma fname "totality_depth"
1493 | lvl <- decorate fname Keyword $
intLit
1495 | pure (TotalityDepth (fromInteger lvl))
1496 | <|> do decoratedPragma fname "ambiguity_depth"
1497 | lvl <- decorate fname Keyword $
intLit
1499 | pure (AmbigDepth (fromInteger lvl))
1500 | <|> do decoratedPragma fname "auto_implicit_depth"
1501 | dpt <- decorate fname Keyword $
intLit
1503 | pure (AutoImplicitDepth (fromInteger dpt))
1504 | <|> do decoratedPragma fname "nf_metavar_threshold"
1505 | dpt <- decorate fname Keyword $
intLit
1507 | pure (NFMetavarThreshold (fromInteger dpt))
1508 | <|> do decoratedPragma fname "search_timeout"
1509 | t <- decorate fname Keyword $
intLit
1512 | <|> do decoratedPragma fname "pair"
1517 | pure (PairNames ty f s)
1518 | <|> do decoratedPragma fname "rewrite"
1522 | pure (RewriteName eq rw)
1523 | <|> do decoratedPragma fname "integerLit"
1527 | <|> do decoratedPragma fname "stringLit"
1531 | <|> do decoratedPragma fname "charLit"
1535 | <|> do decoratedPragma fname "doubleLit"
1539 | <|> do decoratedPragma fname "TTImpLit"
1543 | <|> do decoratedPragma fname "nameLit"
1547 | <|> do decoratedPragma fname "declsLit"
1551 | <|> do decoratedPragma fname "name"
1553 | ns <- sepBy1 (decoratedSymbol fname ",")
1554 | (decoratedSimpleBinderUName fname)
1556 | pure (Names n (forget (map nameRoot ns)))
1557 | <|> do decoratedPragma fname "start"
1558 | e <- expr pdef fname indents
1561 | <|> do decoratedPragma fname "allow_overloads"
1565 | <|> do decoratedPragma fname "language"
1566 | e <- mustWork extension
1569 | <|> do decoratedPragma fname "default"
1570 | tot <- totalityOpt fname
1572 | pure (DefaultTotality tot)
1576 | = (keyword "infixl" $> InfixL)
1577 | <|> (keyword "infixr" $> InfixR)
1578 | <|> (keyword "infix" $> Infix)
1579 | <|> (keyword "prefix" $> Prefix)
1581 | namespaceHead : OriginDesc -> Rule Namespace
1583 | = do decoratedKeyword fname "namespace"
1584 | decorate fname Namespace $
mustWork namespaceId
1586 | parameters {auto fname : OriginDesc} {auto indents : IndentInfo}
1587 | namespaceDecl : Rule PDeclNoFC
1589 | = do doc <- optDocumentation fname
1591 | ns <- namespaceHead fname
1592 | ds <- blockAfter col (topDecl fname)
1593 | pure (PNamespace ns (collectDefs ds))
1595 | transformDecl : Rule PDeclNoFC
1597 | = do decoratedPragma fname "transform"
1599 | lhs <- expr plhs fname indents
1600 | decoratedSymbol fname "="
1601 | rhs <- expr pnowith fname indents
1602 | pure (PTransform n lhs rhs)
1604 | runElabDecl : Rule PDeclNoFC
1607 | decoratedPragma fname "runElab"
1608 | tm <- expr pnowith fname indents
1612 | failDecls : Rule PDeclNoFC
1616 | decoratedKeyword fname "failing"
1618 | msg <- optional (decorate fname Data (simpleMultiStr <|> simpleStr ))
1619 | ds <- nonEmptyBlockAfter col (topDecl fname)
1620 | pure $
PFail msg (collectDefs $
forget ds)
1623 | mutualDecls : Rule PDeclNoFC
1627 | decoratedKeyword fname "mutual"
1629 | ds <- nonEmptyBlockAfter col (topDecl fname)
1630 | pure (PMutual (forget ds))
1632 | usingDecls : Rule PDeclNoFC
1635 | decoratedKeyword fname "using"
1637 | decoratedSymbol fname "("
1638 | us <- sepBy (decoratedSymbol fname ",")
1639 | (do n <- optional $
userName <* decoratedSymbol fname ":"
1640 | ty <- typeExpr pdef fname indents
1642 | decoratedSymbol fname ")"
1643 | ds <- nonEmptyBlockAfter col (topDecl fname)
1644 | pure (PUsing us (collectDefs (forget ds)))
1647 | builtinDecl : Rule PDeclNoFC
1649 | = do decoratedPragma fname "builtin"
1655 | visOpt : OriginDesc -> Rule (Either Visibility PFnOpt)
1657 | = do vis <- visOption fname
1659 | <|> do tot <- fnOpt fname
1661 | <|> do opt <- fnDirectOpt fname
1664 | getVisibility : Maybe Visibility -> List (Either Visibility PFnOpt) ->
1666 | getVisibility Nothing [] = pure Private
1667 | getVisibility (Just vis) [] = pure vis
1668 | getVisibility Nothing (Left x :: xs) = getVisibility (Just x) xs
1669 | getVisibility (Just vis) (Left x :: xs)
1670 | = fatalError "Multiple visibility modifiers"
1671 | getVisibility v (_ :: xs) = getVisibility v xs
1673 | recordConstructor : OriginDesc -> Rule (WithDoc $
AddFC Name)
1674 | recordConstructor fname
1675 | = do doc <- optDocumentation fname
1676 | decorate fname Keyword $
exactIdent "constructor"
1677 | n <- fcBounds $
mustWork $
decoratedDataConstructorName fname
1680 | autoImplicitField : OriginDesc -> IndentInfo -> Rule (PiInfo t)
1681 | autoImplicitField fname _ = AutoImplicit <$ decoratedKeyword fname "auto"
1683 | defImplicitField : OriginDesc -> IndentInfo -> Rule (PiInfo PTerm)
1684 | defImplicitField fname indents = do
1685 | decoratedKeyword fname "default"
1687 | t <- simpleExpr fname indents
1690 | constraints : OriginDesc -> IndentInfo -> EmptyRule (List (Maybe Name, PTerm))
1691 | constraints fname indents
1692 | = do tm <- appExpr pdef fname indents
1693 | decoratedSymbol fname "=>"
1694 | more <- constraints fname indents
1695 | pure ((Nothing, tm) :: more)
1696 | <|> do decoratedSymbol fname "("
1697 | n <- decorate fname Bound name
1698 | decoratedSymbol fname ":"
1699 | tm <- typeExpr pdef fname indents
1700 | decoratedSymbol fname ")"
1701 | decoratedSymbol fname "=>"
1702 | more <- constraints fname indents
1703 | pure ((Just n, tm) :: more)
1706 | implBinds : OriginDesc -> IndentInfo -> (namedImpl : Bool) ->
1707 | EmptyRule (List (AddFC (ImpParameter' PTerm)))
1708 | implBinds fname indents namedImpl = concatMap (map adjust) <$> go where
1710 | adjust : ImpParameter' PTerm -> AddFC (ImpParameter' PTerm)
1711 | adjust param = virtualiseFC param.name.fc :+ param
1713 | isDefaultImplicit : PiInfo a -> Bool
1714 | isDefaultImplicit (DefImplicit _) = True
1715 | isDefaultImplicit _ = False
1717 | go : EmptyRule (List (List (ImpParameter' PTerm)))
1718 | go = do decoratedSymbol fname "{"
1719 | piInfo <- bounds $
option Implicit $
defImplicitField fname indents
1720 | when (not namedImpl && isDefaultImplicit piInfo.val) $
1721 | fatalLoc piInfo.bounds "Default implicits are allowed only for named implementations"
1722 | ns <- map (\case (MkBasicMultiBinder rig names type) => map (\nm => Mk [rig, nm] (MkPiBindData piInfo.val type)) (forget names))
1723 | (pibindListName fname indents)
1724 | let ns = the (List (ImpParameter' PTerm)) ns
1726 | commitSymbol fname "->"
1731 | fieldDecl : (fname : OriginDesc) => IndentInfo -> Rule PField
1733 | = do doc <- optDocumentation fname
1734 | decoratedSymbol fname "{"
1736 | impl <- option Implicit (autoImplicitField fname indents <|> defImplicitField fname indents)
1737 | fs <- addFCBounds (fieldBody doc impl)
1738 | decoratedSymbol fname "}"
1741 | <|> do doc <- optDocumentation fname
1742 | fs <- addFCBounds (fieldBody doc Explicit)
1746 | fieldBody : String -> PiInfo PTerm -> Rule (RecordField' Name)
1748 | = do rig <- multiplicity fname
1749 | ns <- sepBy1 (decoratedSymbol fname ",")
1750 | (fcBounds (decorate fname Function name
1751 | <|> (do b <- bounds (symbol "_")
1752 | fatalLoc {c = True} b.bounds "Fields have to be named")))
1753 | decoratedSymbol fname ":"
1754 | ty <- typeExpr pdef fname indents
1755 | pure (Mk [doc, rig, forget ns] (MkPiBindData p ty))
1757 | parameters {auto fname : OriginDesc} {auto indents : IndentInfo}
1759 | ifaceParam : Rule BasicMultiBinder
1761 | = parens fname basicMultiBinder
1762 | <|> do n <- fcBounds (decorate fname Bound name)
1763 | pure (MkBasicMultiBinder erased (singleton n) (PInfer n.fc))
1765 | ifaceDecl : Rule PDeclNoFC
1767 | = do doc <- optDocumentation fname
1768 | vis <- visibility fname
1770 | decoratedKeyword fname "interface"
1772 | cons <- constraints fname indents
1773 | n <- decorate fname Typ name
1774 | params <- many ifaceParam
1776 | b <- bounds $
decoratedSymbol fname "|"
1777 | mustWorkBecause b.bounds "Expected list of determining parameters" $
1778 | sepBy1 (decoratedSymbol fname ",") (decorate fname Bound name)
1779 | decoratedKeyword fname "where"
1780 | dc <- optional (recordConstructor fname)
1781 | body <- blockAfter col (topDecl fname)
1783 | vis cons n doc params det dc (collectDefs body))
1785 | implDecl : Rule PDeclNoFC
1787 | = do doc <- optDocumentation fname
1788 | visOpts <- many (visOpt fname)
1789 | vis <- getVisibility Nothing visOpts
1790 | let opts = mapMaybe getRight visOpts
1792 | option () (decoratedKeyword fname "implementation")
1793 | iname <- optional $
decoratedSymbol fname "["
1794 | *> decorate fname Function name
1795 | <* decoratedSymbol fname "]"
1796 | impls <- implBinds fname indents (isJust iname)
1797 | cons <- constraints fname indents
1798 | n <- decorate fname Typ name
1799 | params <- many (continue indents *> simpleExpr fname indents)
1800 | nusing <- option [] $
decoratedKeyword fname "using"
1801 | *> forget <$> some (decorate fname Function name)
1802 | body <- optional $
decoratedKeyword fname "where" *> blockAfter col (topDecl fname)
1805 | PImplementation vis opts Single impls cons n params iname nusing
1808 | localClaim : Rule PClaimData
1810 | = do doc <- optDocumentation fname
1811 | visOpts <- many (visOpt fname)
1812 | vis <- getVisibility Nothing visOpts
1813 | let opts = mapMaybe getRight visOpts
1814 | rig <- multiplicity fname
1815 | cls <- tyDecls (decorate fname Function name)
1817 | pure $
MkPClaim rig vis opts cls
1821 | typedArg : Rule PBinder
1823 | = do params <- parens fname $
pibindListName fname indents
1824 | pure $
MkPBinder Explicit params
1825 | <|> do decoratedSymbol fname "{"
1828 | (pure AutoImplicit <* decoratedKeyword fname "auto"
1829 | <|> (decoratedKeyword fname "default" *> DefImplicit <$> simpleExpr fname indents)
1831 | params <- pibindListName fname indents
1832 | decoratedSymbol fname "}"
1833 | pure $
MkPBinder info params
1838 | recordParam : Rule PBinder
1841 | <|> do n <- fcBounds (decoratedSimpleBinderUName fname)
1842 | pure (MkFullBinder Explicit top n $
PInfer n.fc)
1845 | recordBody : String -> WithDefault Visibility Private ->
1851 | recordBody doc vis mbtot col n params
1852 | = do atEndIndent indents
1853 | pure (PRecord doc vis mbtot (MkPRecordLater n params))
1854 | <|> do mustWork $
decoratedKeyword fname "where"
1856 | dcflds <- blockWithOptHeaderAfter col
1857 | (\ idt => recordConstructor fname <* atEnd idt)
1859 | pure (PRecord doc vis mbtot
1860 | (MkPRecord n params opts (fst dcflds) (snd dcflds)))
1862 | recordDecl : Rule PDeclNoFC
1864 | = do doc <- optDocumentation fname
1865 | (vis,mbtot) <- dataVisOpt fname
1867 | decoratedKeyword fname "record"
1868 | n <- mustWork (decoratedDataTypeName fname)
1869 | paramss <- many (continue indents >> recordParam)
1870 | recordBody doc vis mbtot col n paramss
1875 | paramDecls : Rule PDeclNoFC
1878 | b1 <- decoratedKeyword fname "parameters"
1880 | args <- Right <$> newParamDecls
1881 | <|> Left <$> withWarning "DEPRECATED: old parameter syntax https://github.com/idris-lang/Idris2/issues/3447" oldParamDecls
1883 | declarations <- nonEmptyBlockAfter startCol (topDecl fname)
1885 | (collectDefs (forget declarations)))
1888 | oldParamDecls : Rule (List1 PlainBinder)
1890 | = parens fname $
sepBy1 (decoratedSymbol fname ",") plainBinder
1892 | newParamDecls : Rule (List1 PBinder)
1893 | newParamDecls = some typedArg
1896 | definition : Rule PDeclNoFC
1898 | = do nd <- clause 0 Nothing fname indents
1899 | pure (PDef (singleton nd))
1901 | operatorBindingKeyword : EmptyRule BindingModifier
1903 | = (decoratedKeyword fname "autobind" >> pure Autobind)
1904 | <|> (decoratedKeyword fname "typebind" >> pure Typebind)
1909 | = do vis <- exportVisibility fname
1910 | binding <- operatorBindingKeyword
1911 | b <- fcBounds (do fixity <- decorate fname Keyword $
fix
1913 | prec <- decorate fname Keyword $
intLit
1914 | ops <- sepBy1 (decoratedSymbol fname ",") iOperator
1915 | pure (MkPFixityData vis binding fixity (fromInteger prec) ops)
1922 | cgDirectiveDecl : Rule PDeclNoFC
1924 | = (>>=) {c1 = True, c2 = False} cgDirective $
\dir =>
1925 | let (cg1, cg2) = span isAlphaNum dir
1926 | in the (EmptyRule PDeclNoFC) $
pure $
1927 | PDirective (CGAction cg1 (stripBraces (trim cg2)))
1934 | = do id <- anyReservedIdent
1935 | the (Rule PDecl) $
fatalLoc id.bounds "Cannot begin a declaration with a reserved identifier"
1937 | <|> fcBounds (PClaim <$> localClaim)
1938 | <|> fcBounds (PDirective <$> directive)
1940 | <|> fcBounds definition
1943 | <|> fcBounds recordDecl
1944 | <|> fcBounds namespaceDecl
1946 | <|> fcBounds mutualDecls
1947 | <|> fcBounds paramDecls
1948 | <|> fcBounds usingDecls
1949 | <|> fcBounds builtinDecl
1950 | <|> fcBounds runElabDecl
1951 | <|> fcBounds transformDecl
1952 | <|> fcBounds cgDirectiveDecl
1954 | <|> do kw <- bounds $
keyword "import"
1955 | the (Rule PDecl) $
fatalLoc kw.bounds "Imports must go before any declarations or directives"
1957 | <|> do kw <- bounds anyKeyword
1958 | the (Rule PDecl) $
fatalLoc kw.bounds "Keyword '\{kw.val}' is not a valid start to a declaration"
1959 | <|> fatalError "Couldn't parse declaration"
1969 | collectDefs (def@(MkWithData _ (PDef cs)) :: ds)
1970 | = let (csWithFC, rest) = spanBy isPDef ds
1971 | cs' = cs ++ concat (map val csWithFC)
1972 | annot' = foldr {t=List}
1973 | (\fc1, fc2 => fromMaybe EmptyFC (mergeFC fc1 fc2))
1977 | MkFCVal annot' (PDef cs') :: assert_total (collectDefs rest)
1978 | collectDefs (MkWithData annot (PNamespace ns nds) :: ds)
1979 | = MkWithData annot (PNamespace ns (collectDefs nds)) :: collectDefs ds
1980 | collectDefs (MkWithData fc (PMutual nds) :: ds)
1981 | = MkWithData fc (PMutual (collectDefs nds)) :: collectDefs ds
1986 | import_ : OriginDesc -> IndentInfo -> Rule Import
1988 | = do b <- bounds (do decoratedKeyword fname "import"
1989 | reexp <- option False (decoratedKeyword fname "public" $> True)
1990 | ns <- decorate fname Module $
mustWork moduleIdent
1991 | nsAs <- option (miAsNamespace ns)
1992 | (do decorate fname Keyword $
exactIdent "as"
1993 | decorate fname Namespace $
mustWork namespaceId)
1994 | pure (reexp, ns, nsAs))
1996 | (reexp, ns, nsAs) <- pure b.val
1997 | pure (MkImport (boundToFC fname b) reexp ns nsAs)
2000 | progHdr : OriginDesc -> EmptyRule Module
2002 | = do b <- bounds (do doc <- optDocumentation fname
2003 | nspace <- option (nsAsModuleIdent mainNS)
2004 | (do decoratedKeyword fname "module"
2005 | decorate fname Module $
mustWork moduleIdent)
2006 | imports <- block (import_ fname)
2007 | pure (doc, nspace, imports))
2008 | (doc, nspace, imports) <- pure b.val
2009 | pure (MkModule (boundToFC fname b)
2013 | prog : OriginDesc -> EmptyRule Module
2015 | = do mod <- progHdr fname
2016 | ds <- block (topDecl fname)
2017 | pure $
{ decls := collectDefs ds} mod
2019 | parseMode : Rule REPLEval
2021 | = do exactIdent "typecheck"
2025 | <|> do exactIdent "normalise"
2027 | <|> do exactIdent "default"
2029 | <|> do exactIdent "normal"
2031 | <|> do exactIdent "normalize"
2033 | <|> do exactIdent "execute"
2035 | <|> do exactIdent "exec"
2037 | <|> do exactIdent "scheme"
2040 | setVarOption : Rule REPLOpt
2043 | mode <- option NormaliseAll parseMode
2045 | <|> do exactIdent "editor"
2052 | setOption : Bool -> Rule REPLOpt
2054 | = do exactIdent "showimplicits"
2055 | pure (ShowImplicits set)
2056 | <|> do exactIdent "shownamespace"
2057 | pure (ShowNamespace set)
2058 | <|> do exactIdent "showmachinenames"
2059 | pure (ShowMachineNames set)
2060 | <|> do exactIdent "showtypes"
2062 | <|> do exactIdent "profile"
2064 | <|> do exactIdent "evaltiming"
2066 | <|> if set then setVarOption else fatalError "Unrecognised option"
2068 | replCmd : List String -> Rule ()
2069 | replCmd [] = fail "Unrecognised command"
2075 | cmdName : String -> Rule String
2077 | _ <- optional (symbol ":")
2078 | terminal ("Unrecognised REPL command '" ++ str ++ "'") $
2080 | (Ident s) => if s == str then Just s else Nothing
2081 | (Keyword kw) => if kw == str then Just kw else Nothing
2082 | (Symbol "?") => Just "?"
2083 | (Symbol ":?") => Just "?"
2087 | data CmdArg : Type where
2125 | NamedCmdArg : String -> CmdArg -> CmdArg
2128 | WithDefaultArg : String -> CmdArg -> CmdArg
2131 | CSVArg : CmdArg -> CmdArg
2134 | Args : List CmdArg -> CmdArg
2138 | showCmdArg : CmdArg -> String
2140 | showCmdArg NameArg = "name"
2141 | showCmdArg ExprArg = "expr"
2142 | showCmdArg DocArg = "keyword|expr"
2143 | showCmdArg DeclsArg = "decls"
2144 | showCmdArg NumberArg = "number"
2145 | showCmdArg AutoNumberArg = "number|auto"
2146 | showCmdArg OptionArg = "option"
2147 | showCmdArg FileArg = "file"
2148 | showCmdArg ModuleArg = "module"
2149 | showCmdArg StringArg = "string"
2150 | showCmdArg OnOffArg = "(on|off)"
2151 | showCmdArg (CSVArg arg) = "[" ++ showCmdArg arg ++ "]"
2152 | showCmdArg (WithDefaultArg value arg) = showCmdArg arg ++ "|" ++ value
2153 | showCmdArg (NamedCmdArg name arg) = name ++ ":" ++ showCmdArg arg
2154 | showCmdArg args@(Args _) = show args
2160 | show OnOffArg = "(on|off)"
2161 | show (Args args) = showSep " " (map show args)
2162 | show arg = "<" ++ showCmdArg arg ++ ">"
2165 | knownCommands : List (String, String)
2167 | explain ["t", "type"] "Check the type of an expression" ++
2168 | [ ("ti", "Check the type of an expression, showing implicit arguments")
2169 | , ("printdef", "Show the definition of a pattern-matching function")
2171 | explain ["s", "search"] "Search for values by type" ++
2172 | [ ("di", "Show debugging information for a name")
2174 | explain ["module", "import"] "Import an extra module" ++
2175 | [ ("package", "Import every module of the package")
2177 | explain ["q", "quit", "exit"] "Exit the Idris system" ++
2178 | [ ("cwd", "Displays the current working directory")
2179 | , ("cd", "Change the current working directory")
2180 | , ("sh", "Run a shell command")
2184 | , " eval specify what evaluation mode to use:"
2186 | , " normalise|normalize|normal"
2190 | , " editor specify the name of the editor command"
2192 | , " cg specify the codegen/backend to use"
2193 | , " builtin codegens are:"
2199 | , " showimplicits enable displaying implicit arguments as part of the"
2202 | , " shownamespace enable displaying namespaces as part of the output"
2204 | , " showmachinenames enable displaying machine names as part of the"
2207 | , " showtypes enable displaying the type of the term as part of"
2212 | , " evaltiming enable timing how long evaluation takes and"
2213 | , " displaying this before the printing of the output"
2216 | , ("unset", "Unset an option")
2217 | , ("opts", "Show current options settings")
2219 | explain ["c", "compile"] "Compile to an executable" ++
2220 | [ ("exec", "Compile to an executable and run")
2221 | , ("directive", "Set a codegen-specific directive")
2223 | explain ["l", "load"] "Load a file" ++
2224 | explain ["r", "reload"] "Reload current file" ++
2225 | explain ["e", "edit"] "Edit current file using $EDITOR or $VISUAL" ++
2226 | explain ["miss", "missing"] "Show missing clauses" ++
2227 | [ ("total", "Check the totality of a name")
2228 | , ("doc", "Show documentation for a keyword, a name, or a primitive")
2229 | , ("browse", "Browse contents of a namespace")
2231 | explain ["log", "logging"] "Set logging level" ++
2232 | [ ("consolewidth", "Set the width of the console output (0 for unbounded) (auto by default)")
2234 | explain ["colour", "color"] "Whether to use colour for the console output (enabled by default)" ++
2235 | explain ["m", "metavars"] "Show remaining proof obligations (metavariables or holes)" ++
2236 | [ ("typeat", "Show type of term <n> defined on line <l> and column <c>")
2238 | explain ["cs", "casesplit"] "Case split term <n> defined on line <l> and column <c>" ++
2239 | explain ["ac", "addclause"] "Add clause to term <n> defined on line <l>" ++
2240 | explain ["ml", "makelemma"] "Make lemma for term <n> defined on line <l>" ++
2241 | explain ["mc", "makecase"] "Make case on term <n> defined on line <l>" ++
2242 | explain ["mw", "makewith"] "Add with expression on term <n> defined on line <l>" ++
2243 | [ ("intro", "Introduce unambiguous constructor in hole <n> defined on line <l>")
2244 | , ("refine", "Refine hole <h> with identifier <n> on line <l>")
2246 | explain ["ps", "proofsearch"] "Search for a proof" ++
2247 | [ ("psnext", "Show next proof")
2248 | , ("gd", "Try to generate a definition using proof-search")
2249 | , ("gdnext", "Show next definition")
2250 | , ("version", "Display the Idris version")
2252 | explain ["?", "h", "help"] (unlines
2253 | [ "Display help text, optionally of a specific command.\n"
2254 | , "If run without arguments, lists all the REPL commands along with their"
2255 | , "initial line of help text.\n"
2256 | , "More detailed help can then be obtained by running the :help command"
2257 | , "with another command as an argument, e.g."
2260 | , "(the leading ':' in the command argument is optional)"
2266 | First, declare the type of your new value, e.g.
2267 | :let myValue : List Nat
2269 | Then, define the value:
2270 | :let myValue = [1, 2, 3]
2272 | Now the value is in scope at the REPL:
2278 | explain ["fs", "fsearch"] """
2279 | Search for global definitions by sketching the names distribution of the wanted type(s).
2281 | 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.
2283 | Idris will return all of the entries in the context that have all of the names in A
2284 | in some argument and all of the names in B within the return type.
2290 | will match (among other things):
2292 | Prelude.List.mapMaybe : (a -> Maybe b) -> List a -> List b
2294 | Note that the query 'List Nat -> String' does not describe the type 'List Nat',
2295 | rather it describes both 'List a' and 'Nat' in the arguments.
2299 | explain : List String -> String -> List (String, String)
2300 | explain cmds expl = map (\s => (s, expl)) cmds
2303 | KnownCommand : String -> Type
2304 | KnownCommand cmd = IsJust (lookup cmd knownCommands)
2307 | data ParseCmd : Type where
2308 | ParseREPLCmd : (cmds : List String)
2309 | -> {auto 0 _ : All KnownCommand cmds}
2312 | ParseKeywordCmd : (cmds : List String)
2313 | -> {auto 0 _ : All KnownCommand cmds}
2316 | ParseIdentCmd : (cmd : String)
2317 | -> {auto 0 _ : KnownCommand cmd}
2321 | CommandDefinition : Type
2322 | CommandDefinition = (List String, CmdArg, String, Rule REPLCmd)
2326 | CommandTable = List CommandDefinition
2328 | extractNames : ParseCmd -> List String
2329 | extractNames (ParseREPLCmd names) = names
2330 | extractNames (ParseKeywordCmd keywords) = keywords
2331 | extractNames (ParseIdentCmd ident) = [ident]
2333 | runParseCmd : ParseCmd -> Rule ()
2334 | runParseCmd (ParseREPLCmd names) = replCmd names
2335 | runParseCmd (ParseKeywordCmd keywords) = choice $
map keyword keywords
2336 | runParseCmd (ParseIdentCmd ident) = exactIdent ident
2339 | noArgCmd : ParseCmd -> REPLCmd -> String -> CommandDefinition
2340 | noArgCmd parseCmd command doc = (names, NoArg, doc, parse)
2343 | names = extractNames parseCmd
2351 | nameArgCmd : ParseCmd -> (Name -> REPLCmd) -> String -> CommandDefinition
2352 | nameArgCmd parseCmd command doc = (names, NameArg, doc, parse)
2355 | names = extractNames parseCmd
2364 | stringArgCmd : ParseCmd -> (String -> REPLCmd) -> String -> CommandDefinition
2365 | stringArgCmd parseCmd command doc = (names, StringArg, doc, parse)
2368 | names = extractNames parseCmd
2374 | s <- mustWork simpleStr
2377 | getHelpType : EmptyRule HelpType
2379 | optCmd <- optional $
choice $
(cmdName . fst) <$> knownCommands
2383 | Just cmd => DetailedHelp $
fromMaybe "Unrecognised command '\{cmd}'"
2384 | $
lookup cmd knownCommands
2387 | -> (HelpType -> REPLCmd)
2390 | helpCmd parseCmd command doc = (names, StringArg, doc, parse)
2393 | names = extractNames parseCmd
2399 | helpType <- getHelpType
2400 | pure (command helpType)
2402 | moduleArgCmd : ParseCmd -> (ModuleIdent -> REPLCmd) -> String -> CommandDefinition
2403 | moduleArgCmd parseCmd command doc = (names, ModuleArg, doc, parse)
2406 | names = extractNames parseCmd
2412 | n <- mustWork moduleIdent
2415 | exprArgCmd : ParseCmd -> (PTerm -> REPLCmd) -> String -> CommandDefinition
2416 | exprArgCmd parseCmd command doc = (names, ExprArg, doc, parse)
2419 | names = extractNames parseCmd
2425 | tm <- mustWork $
typeExpr pdef (Virtual Interactive) init
2428 | docArgCmd : ParseCmd -> (DocDirective -> REPLCmd) -> String -> CommandDefinition
2429 | docArgCmd parseCmd command doc = (names, DocArg, doc, parse)
2432 | names = extractNames parseCmd
2436 | docLazyPrim : Rule PTerm
2438 | let placeholeder : PTerm' Name
2439 | placeholeder = PHole EmptyFC False "lazyDocPlaceholeder"
2440 | in do exactIdent "Lazy"
2441 | pure (PDelayed EmptyFC LLazy placeholeder)
2442 | <|> do exactIdent "Inf"
2443 | pure (PDelayed EmptyFC LInf placeholeder)
2444 | <|> do exactIdent "Delay"
2445 | pure (PDelay EmptyFC placeholeder)
2446 | <|> do exactIdent "Force"
2447 | pure (PForce EmptyFC placeholeder)
2454 | AModule <$ keyword "module" <*> moduleIdent
2455 | <|> Keyword <$> anyKeyword
2456 | <|> Symbol <$> (anyReservedSymbol <* eoi
2457 | <|> parens (Virtual Interactive) anyReservedSymbol <* eoi)
2459 | IdiomBrackets <$ symbol "[|" <* symbol "|]"
2460 | <|> NameQuote <$ symbol "`{" <* symbol "}"
2461 | <|> TermQuote <$ symbol "`(" <* symbol ")"
2462 | <|> DeclQuote <$ symbol "`[" <* symbol "]"
2466 | <|> typeExpr pdef (Virtual Interactive) init
2470 | declsArgCmd : ParseCmd -> (List PDecl -> REPLCmd) -> String -> CommandDefinition
2471 | declsArgCmd parseCmd command doc = (names, DeclsArg, doc, parse)
2474 | names = extractNames parseCmd
2479 | tm <- mustWork $
topDecl (Virtual Interactive) init
2482 | optArgCmd : ParseCmd -> (REPLOpt -> REPLCmd) -> Bool -> String -> CommandDefinition
2483 | optArgCmd parseCmd command set doc = (names, OptionArg, doc, parse)
2486 | names = extractNames parseCmd
2492 | opt <- mustWork $
setOption set
2495 | numberArgCmd : ParseCmd -> (Nat -> REPLCmd) -> String -> CommandDefinition
2496 | numberArgCmd parseCmd command doc = (names, NumberArg, doc, parse)
2499 | names = extractNames parseCmd
2506 | pure (command (fromInteger i))
2508 | autoNumberArgCmd : ParseCmd -> (Maybe Nat -> REPLCmd) -> String -> CommandDefinition
2509 | autoNumberArgCmd parseCmd command doc = (names, AutoNumberArg, doc, parse)
2512 | names = extractNames parseCmd
2514 | autoNumber : Rule (Maybe Nat)
2515 | autoNumber = Nothing <$ keyword "auto"
2516 | <|> Just . fromInteger <$> intLit
2522 | mi <- mustWork autoNumber
2525 | onOffArgCmd : ParseCmd -> (Bool -> REPLCmd) -> String -> CommandDefinition
2526 | onOffArgCmd parseCmd command doc = (names, OnOffArg, doc, parse)
2529 | names = extractNames parseCmd
2538 | compileArgsCmd : ParseCmd -> (PTerm -> String -> REPLCmd) -> String -> CommandDefinition
2539 | compileArgsCmd parseCmd command doc
2540 | = (names, Args [FileArg, ExprArg], doc, parse)
2543 | names = extractNames parseCmd
2549 | n <- mustWork unqualifiedName
2550 | tm <- mustWork $
expr pdef (Virtual Interactive) init
2553 | loggingArgCmd : ParseCmd -> (Maybe LogLevel -> REPLCmd) -> String -> CommandDefinition
2554 | loggingArgCmd parseCmd command doc = (names, Args [StringArg, NumberArg], doc, parse) where
2557 | names = extractNames parseCmd
2563 | lvl <- mustWork $
logLevel (Virtual Interactive)
2566 | editLineNameArgCmd : ParseCmd -> (Bool -> Int -> Name -> EditCmd) -> String -> CommandDefinition
2567 | editLineNameArgCmd parseCmd command doc = (names, Args [NamedCmdArg "l" NumberArg, NamedCmdArg "n" StringArg], doc, parse) where
2570 | names = extractNames parseCmd
2576 | upd <- option False (symbol "!" $> True)
2577 | line <- fromInteger <$> mustWork intLit
2579 | pure (Editing $
command upd line n)
2581 | editLineColNameArgCmd : ParseCmd -> (Bool -> Int -> Int -> Name -> EditCmd) -> String -> CommandDefinition
2582 | editLineColNameArgCmd parseCmd command doc =
2584 | , Args [ NamedCmdArg "l" NumberArg
2585 | , NamedCmdArg "c" NumberArg
2586 | , NamedCmdArg "n" StringArg
2593 | names = extractNames parseCmd
2599 | upd <- option False (symbol "!" $> True)
2600 | line <- fromInteger <$> mustWork intLit
2601 | col <- fromInteger <$> mustWork intLit
2603 | pure (Editing $
command upd line col n)
2605 | editLineNamePTermArgCmd : ParseCmd -> (Bool -> Int -> Name -> PTerm -> EditCmd) -> String -> CommandDefinition
2606 | editLineNamePTermArgCmd parseCmd command doc =
2608 | , Args [ NamedCmdArg "l" NumberArg
2609 | , NamedCmdArg "h" StringArg
2610 | , NamedCmdArg "e" ExprArg
2617 | names = extractNames parseCmd
2623 | upd <- option False (symbol "!" $> True)
2624 | line <- fromInteger <$> mustWork intLit
2626 | n <- mustWork $
typeExpr pdef (Virtual Interactive) init
2627 | pure (Editing $
command upd line h n)
2629 | editLineNameCSVArgCmd : ParseCmd
2630 | -> (Bool -> Int -> Name -> List Name -> EditCmd)
2633 | editLineNameCSVArgCmd parseCmd command doc =
2635 | , Args [ NamedCmdArg "l" NumberArg
2636 | , NamedCmdArg "n" StringArg
2637 | , NamedCmdArg "h" (CSVArg NameArg)
2644 | names = extractNames parseCmd
2650 | upd <- option False (symbol "!" $> True)
2651 | line <- fromInteger <$> mustWork intLit
2653 | hints <- mustWork $
sepBy (symbol ",") name
2654 | pure (Editing $
command upd line n hints)
2656 | editLineNameOptionArgCmd : ParseCmd
2657 | -> (Bool -> Int -> Name -> Nat -> EditCmd)
2660 | editLineNameOptionArgCmd parseCmd command doc =
2662 | , Args [ NamedCmdArg "l" NumberArg
2663 | , NamedCmdArg "n" StringArg
2664 | , NamedCmdArg "r" (WithDefaultArg "0" NumberArg)
2671 | names = extractNames parseCmd
2677 | upd <- option False (symbol "!" $> True)
2678 | line <- fromInteger <$> mustWork intLit
2680 | nreject <- fromInteger <$> option 0 intLit
2681 | pure (Editing $
command upd line n nreject)
2683 | firstHelpLine : (cmd : String) -> {auto 0 _ : KnownCommand cmd} -> String
2685 | head . (split ((==) '\n')) $
2686 | fromMaybe "Failed to look up '\{cmd}' (SHOULDN'T HAPPEN!)" $
2687 | lookup cmd knownCommands
2690 | parserCommandsForHelp : CommandTable
2691 | parserCommandsForHelp =
2692 | [ exprArgCmd (ParseREPLCmd ["t", "type"]) Check (firstHelpLine "t")
2693 | , exprArgCmd (ParseREPLCmd ["ti"]) CheckWithImplicits (firstHelpLine "ti")
2694 | , exprArgCmd (ParseREPLCmd ["printdef"]) PrintDef (firstHelpLine "printdef")
2695 | , exprArgCmd (ParseREPLCmd ["s", "search"]) TypeSearch (firstHelpLine "s")
2696 | , nameArgCmd (ParseIdentCmd "di") DebugInfo (firstHelpLine "di")
2697 | , moduleArgCmd (ParseKeywordCmd ["module", "import"]) ImportMod (firstHelpLine "module")
2698 | , stringArgCmd (ParseREPLCmd ["package"]) ImportPackage (firstHelpLine "package")
2699 | , noArgCmd (ParseREPLCmd ["q", "quit", "exit"]) Quit (firstHelpLine "q")
2700 | , noArgCmd (ParseREPLCmd ["cwd"]) CWD (firstHelpLine "cwd")
2701 | , stringArgCmd (ParseREPLCmd ["cd"]) CD (firstHelpLine "cd")
2702 | , stringArgCmd (ParseREPLCmd ["sh"]) RunShellCommand (firstHelpLine "sh")
2703 | , optArgCmd (ParseIdentCmd "set") SetOpt True (firstHelpLine "set")
2704 | , optArgCmd (ParseIdentCmd "unset") SetOpt False (firstHelpLine "unset")
2705 | , noArgCmd (ParseREPLCmd ["opts"]) GetOpts (firstHelpLine "opts")
2706 | , compileArgsCmd (ParseREPLCmd ["c", "compile"]) Compile (firstHelpLine "c")
2707 | , exprArgCmd (ParseIdentCmd "exec") Exec (firstHelpLine "exec")
2708 | , stringArgCmd (ParseIdentCmd "directive") CGDirective (firstHelpLine "directive")
2709 | , stringArgCmd (ParseREPLCmd ["l", "load"]) Load (firstHelpLine "l")
2710 | , noArgCmd (ParseREPLCmd ["r", "reload"]) Reload (firstHelpLine "r")
2711 | , noArgCmd (ParseREPLCmd ["e", "edit"]) Edit (firstHelpLine "e")
2712 | , nameArgCmd (ParseREPLCmd ["miss", "missing"]) Missing (firstHelpLine "miss")
2713 | , nameArgCmd (ParseKeywordCmd ["total"]) Total (firstHelpLine "total")
2714 | , docArgCmd (ParseIdentCmd "doc") Doc (firstHelpLine "doc")
2715 | , moduleArgCmd (ParseIdentCmd "browse") (Browse . miAsNamespace) (firstHelpLine "browse")
2716 | , loggingArgCmd (ParseREPLCmd ["log", "logging"]) SetLog (firstHelpLine "log")
2717 | , autoNumberArgCmd (ParseREPLCmd ["consolewidth"]) SetConsoleWidth (firstHelpLine "consolewidth")
2718 | , onOffArgCmd (ParseREPLCmd ["colour", "color"]) SetColor (firstHelpLine "colour")
2719 | , noArgCmd (ParseREPLCmd ["m", "metavars"]) Metavars (firstHelpLine "m")
2720 | , editLineColNameArgCmd (ParseREPLCmd ["typeat"]) (const TypeAt) (firstHelpLine "typeat")
2721 | , editLineColNameArgCmd (ParseREPLCmd ["cs", "casesplit"]) CaseSplit (firstHelpLine "cs")
2722 | , editLineNameArgCmd (ParseREPLCmd ["ac", "addclause"]) AddClause (firstHelpLine "ac")
2723 | , editLineNameArgCmd (ParseREPLCmd ["ml", "makelemma"]) MakeLemma (firstHelpLine "ml")
2724 | , editLineNameArgCmd (ParseREPLCmd ["mc", "makecase"]) MakeCase (firstHelpLine "mc")
2725 | , editLineNameArgCmd (ParseREPLCmd ["mw", "makewith"]) MakeWith (firstHelpLine "mw")
2726 | , editLineNameArgCmd (ParseREPLCmd ["intro"]) Intro (firstHelpLine "intro")
2727 | , editLineNamePTermArgCmd (ParseREPLCmd ["refine"]) Refine (firstHelpLine "refine")
2728 | , editLineNameCSVArgCmd (ParseREPLCmd ["ps", "proofsearch"]) ExprSearch (firstHelpLine "ps")
2729 | , noArgCmd (ParseREPLCmd ["psnext"]) (Editing ExprSearchNext) (firstHelpLine "psnext")
2730 | , editLineNameOptionArgCmd (ParseREPLCmd ["gd"]) GenerateDef (firstHelpLine "gd")
2731 | , noArgCmd (ParseREPLCmd ["gdnext"]) (Editing GenerateDefNext) (firstHelpLine "gdnext")
2732 | , noArgCmd (ParseREPLCmd ["version"]) ShowVersion (firstHelpLine "version")
2733 | , helpCmd (ParseREPLCmd ["?", "h", "help"]) Help (firstHelpLine "?")
2734 | , declsArgCmd (ParseKeywordCmd ["let"]) NewDefn (firstHelpLine "let")
2735 | , exprArgCmd (ParseREPLCmd ["fs", "fsearch"]) FuzzyTypeSearch (firstHelpLine "fs")
2739 | help : List (List String, CmdArg, String)
2740 | help = (["<expr>"], NoArg, "Evaluate an expression") ::
2741 | map (\ (names, args, text, _) =>
2742 | (map (":" ++) names, args, text)) parserCommandsForHelp
2744 | nonEmptyCommand : Rule REPLCmd
2746 | choice (map (\ (_, _, _, parser) => parser) parserCommandsForHelp)
2750 | tm <- typeExpr pdef (Virtual Interactive) init
2755 | aPTerm = typeExpr pdef (Virtual Interactive) init
2758 | command : EmptyRule REPLCmd
2763 | helpType <- getHelpType