module Idris.Parser import        Core.Optionsimport        Idris.Syntaximport public Parser.Supportimport        Parser.Lexerimport        TTImp.TTImp import public Text.Parserimport        Data.List.Views %default covering -- Forward declare since they're used in the parsertopDecl : FileName -> IndentInfo -> Rule (List PDecl)collectDefs : List PDecl -> List PDecl -- Some context for the parserpublic exportrecord ParseOpts where  constructor MkParseOpts  eqOK : Bool -- = operator is parseable  withOK : Bool -- = with applications are parseable peq : ParseOpts -> ParseOptspeq = record { eqOK = True } pnoeq : ParseOpts -> ParseOptspnoeq = record { eqOK = False } exportpdef : ParseOptspdef = MkParseOpts True True pnowith : ParseOptspnowith = MkParseOpts True False exportplhs : ParseOptsplhs = MkParseOpts False False atom : FileName -> Rule PTermatom fname    = do start <- location         x <- constant         end <- location         pure (PPrimVal (MkFC fname start end) x)  <|> do start <- location         exactIdent "Type"         end <- location         pure (PType (MkFC fname start end))  <|> do start <- location         symbol "_"         end <- location         pure (PImplicit (MkFC fname start end))  <|> do start <- location         symbol "?"         end <- location         pure (PInfer (MkFC fname start end))  <|> do start <- location         x <- holeName         end <- location         pure (PHole (MkFC fname start end) False x)  <|> do start <- location         pragma "MkWorld"         end <- location         pure (PPrimVal (MkFC fname start end) WorldVal)  <|> do start <- location         pragma "World"         end <- location         pure (PPrimVal (MkFC fname start end) WorldType)  <|> do start <- location         pragma "search"         end <- location         pure (PSearch (MkFC fname start end) 50)  <|> do start <- location         x <- name         end <- location         pure (PRef (MkFC fname start end) x) whereBlock : FileName -> Int -> Rule (List PDecl)whereBlock fname col    = do keyword "where"         ds <- blockAfter col (topDecl fname)         pure (collectDefs (concat ds)) -- Expect a keyword, but if we get anything else it's a fatal errorcommitKeyword : IndentInfo -> String -> Rule ()commitKeyword indents req    = do mustContinue indents (Just req)         keyword req         mustContinue indents Nothing commitSymbol : String -> Rule ()commitSymbol req    = symbol req       <|> fatalError ("Expected '" ++ req ++ "'") continueWith : IndentInfo -> String -> Rule ()continueWith indents req    = do mustContinue indents (Just req)         symbol req iOperator : Rule NameiOperator    = operator  <|> do symbol "`"         n <- name         symbol "`"         pure n data ArgType    = ExpArg PTerm    | ImpArg (Maybe Name) PTerm    | WithArg PTerm mutual  appExpr : ParseOpts -> FileName -> IndentInfo -> Rule PTerm  appExpr q fname indents      = case_ fname indents    <|> lambdaCase fname indents    <|> lazy fname indents    <|> if_ fname indents    <|> doBlock fname indents    <|> do start <- location           f <- simpleExpr fname indents           args <- many (argExpr q fname indents)           end <- location           pure (applyExpImp start end f args)    <|> do start <- location           op <- iOperator           arg <- expr pdef fname indents           end <- location           pure (PPrefixOp (MkFC fname start end) op arg)    <|> fail "Expected 'case', 'if', 'do', application or operator expression"    where      applyExpImp : FilePos -> FilePos -> PTerm ->                    List ArgType ->                    PTerm      applyExpImp start end f [] = f      applyExpImp start end f (ExpArg exp :: args)          = applyExpImp start end (PApp (MkFC fname start end) f exp) args      applyExpImp start end f (ImpArg n imp :: args)          = applyExpImp start end (PImplicitApp (MkFC fname start end) f n imp) args      applyExpImp start end f (WithArg exp :: args)          = applyExpImp start end (PWithApp (MkFC fname start end) f exp) args   argExpr : ParseOpts -> FileName -> IndentInfo -> Rule ArgType  argExpr q fname indents      = do continue indents           arg <- simpleExpr fname indents           the (EmptyRule _) $ case arg of                PHole loc _ n => pure (ExpArg (PHole loc True n))                t => pure (ExpArg t)    <|> do continue indents           arg <- implicitArg fname indents           pure (ImpArg (fst arg) (snd arg))    <|> if withOK q           then do continue indents                   symbol "|"                   arg <- expr (record { withOK = False} q) fname indents                   pure (WithArg arg)           else fail "| not allowed here"   implicitArg : FileName -> IndentInfo -> Rule (Maybe Name, PTerm)  implicitArg fname indents      = do start <- location           symbol "{"           x <- unqualifiedName           (do symbol "="               commit               tm <- expr pdef fname indents               symbol "}"               pure (Just (UN x), tm))             <|> (do symbol "}"                     end <- location                     pure (Just (UN x), PRef (MkFC fname start end) (UN x)))    <|> do symbol "@{"           commit           tm <- expr pdef fname indents           symbol "}"           pure (Nothing, tm)   opExpr : ParseOpts -> FileName -> IndentInfo -> Rule PTerm  opExpr q fname indents      = do start <- location           l <- appExpr q fname indents           (if eqOK q               then do continue indents                       symbol "="                       r <- opExpr q fname indents                       end <- location                       pure (POp (MkFC fname start end) (UN "=") l r)               else fail "= not allowed")             <|>             (do continue indents                 op <- iOperator                 middle <- location                 r <- opExpr q fname indents                 end <- location                 pure (POp (MkFC fname start end) op l r))               <|> pure l   dpair : FileName -> FilePos -> IndentInfo -> Rule PTerm  dpair fname start indents      = do x <- unqualifiedName           symbol ":"           ty <- expr pdef fname indents           loc <- location           symbol "**"           rest <- dpair fname loc indents <|> expr pdef fname indents           end <- location           pure (PDPair (MkFC fname start end)                        (PRef (MkFC fname start loc) (UN x))                        ty                        rest)    <|> do l <- expr pdef fname indents           loc <- location           symbol "**"           rest <- dpair fname loc indents <|> expr pdef fname indents           end <- location           pure (PDPair (MkFC fname start end)                        l                        (PImplicit (MkFC fname start end))                        rest)   bracketedExpr : FileName -> FilePos -> IndentInfo -> Rule PTerm  bracketedExpr fname start indents      -- left section. This may also be a prefix operator, but we'll sort      -- that out when desugaring: if the operator is infix, treat it as a      -- section otherwise treat it as prefix      = do op <- iOperator           e <- expr pdef fname indents           continueWith indents ")"           end <- location           pure (PSectionL (MkFC fname start end) op e)      -- unit type/value    <|> do continueWith indents ")"           end <- location           pure (PUnit (MkFC fname start end))      -- right section (1-tuple is just an expression)    <|> do p <- dpair fname start indents           symbol ")"           pure p    <|> do e <- expr pdef fname indents           (do op <- iOperator               symbol ")"               end <- location               pure (PSectionR (MkFC fname start end) e op)             <|>            -- all the other bracketed expressions            tuple fname start indents e)   getInitRange : List PTerm -> EmptyRule (PTerm, Maybe PTerm)  getInitRange [x] = pure (x, Nothing)  getInitRange [x, y] = pure (x, Just y)  getInitRange _ = fatalError "Invalid list range syntax"   listRange : FileName -> FilePos -> IndentInfo -> List PTerm -> Rule PTerm  listRange fname start indents xs      = do symbol "]"           end <- location           let fc = MkFC fname start end           rstate <- getInitRange xs           pure (PRangeStream fc (fst rstate) (snd rstate))    <|> do y <- expr pdef fname indents           symbol "]"           end <- location           let fc = MkFC fname start end           rstate <- getInitRange xs           pure (PRange fc (fst rstate) (snd rstate) y)   listExpr : FileName -> FilePos -> IndentInfo -> Rule PTerm  listExpr fname start indents      = do ret <- expr pnowith fname indents           symbol "|"           conds <- sepBy1 (symbol ",") (doAct fname indents)           symbol "]"           end <- location           pure (PComprehension (MkFC fname start end) ret (concat conds))    <|> do xs <- sepBy (symbol ",") (expr pdef fname indents)           (do symbol ".."               listRange fname start indents xs)             <|> (do symbol "]"                     end <- location                     pure (PList (MkFC fname start end) xs))   -- A pair, dependent pair, or just a single expression  tuple : FileName -> FilePos -> IndentInfo -> PTerm -> Rule PTerm  tuple fname start indents e      = do rest <- some (do symbol ","                            estart <- location                            el <- expr pdef fname indents                            pure (estart, el))           continueWith indents ")"           end <- location           pure (PPair (MkFC fname start end) e                       (mergePairs end rest))     <|> do continueWith indents ")"            end <- location            pure (PBracketed (MkFC fname start end) e)    where      mergePairs : FilePos -> List (FilePos, PTerm) -> PTerm      mergePairs end [] = PUnit (MkFC fname start end)      mergePairs end [(estart, exp)] = exp      mergePairs end ((estart, exp) :: rest)          = PPair (MkFC fname estart end) exp (mergePairs end rest)   simpleExpr : FileName -> IndentInfo -> Rule PTerm  simpleExpr fname indents =        do          start <- location          recFields <- some recField          end <- location          pure $ PRecordProjection (MkFC fname start end) recFields    <|> do          start <- location          root <- simplerExpr fname indents          recFields <- many recField          end <- location          pure $ case recFields of            [] => root            fs => PRecordFieldAccess (MkFC fname start end) root recFields   simplerExpr : FileName -> IndentInfo -> Rule PTerm  simplerExpr fname indents      = do start <- location           x <- unqualifiedName           symbol "@"           commit           expr <- simpleExpr fname indents           end <- location           pure (PAs (MkFC fname start end) (UN x) expr)    <|> atom fname    <|> binder fname indents    <|> rewrite_ fname indents    <|> record_ fname indents    <|> do start <- location           symbol ".("           commit           e <- expr pdef fname indents           symbol ")"           end <- location           pure (PDotted (MkFC fname start end) e)    <|> do start <- location           symbol "`("           e <- expr pdef fname indents           symbol ")"           end <- location           pure (PQuote (MkFC fname start end) e)    <|> do start <- location           symbol "~"           e <- simpleExpr fname indents           end <- location           pure (PUnquote (MkFC fname start end) e)    <|> do start <- location           symbol "("           bracketedExpr fname start indents    <|> do start <- location           symbol "["           listExpr fname start indents    <|> do start <- location           symbol "!"           e <- simpleExpr fname indents           end <- location           pure (PBang (MkFC fname start end) e)    <|> do start <- location           symbol "[|"           e <- expr pdef fname indents           symbol "|]"           end <- location           pure (PIdiom (MkFC fname start end) e)    <|> do start <- location           pragma "logging"           lvl <- intLit           e <- expr pdef fname indents           end <- location           pure (PUnifyLog (MkFC fname start end) (cast lvl) e)   multiplicity : EmptyRule (Maybe Integer)  multiplicity      = do c <- intLit           pure (Just c)--     <|> do symbol "&"--            pure (Just 2) -- Borrowing, not implemented    <|> pure Nothing   getMult : Maybe Integer -> EmptyRule RigCount  getMult (Just 0) = pure erased  getMult (Just 1) = pure linear  getMult Nothing = pure top  getMult _ = fatalError "Invalid multiplicity (must be 0 or 1)"   pibindAll : FC -> PiInfo PTerm -> List (RigCount, Maybe Name, PTerm) ->              PTerm -> PTerm  pibindAll fc p [] scope = scope  pibindAll fc p ((rig, n, ty) :: rest) scope           = PPi fc rig p n ty (pibindAll fc p rest scope)   bindList : FileName -> FilePos -> IndentInfo ->             Rule (List (RigCount, PTerm, PTerm))  bindList fname start indents      = sepBy1 (symbol ",")               (do rigc <- multiplicity                   pat <- simpleExpr fname indents                   ty <- option                            (PInfer (MkFC fname start start))                            (do symbol ":"                                opExpr pdef fname indents)                   rig <- getMult rigc                   pure (rig, pat, ty))   pibindListName : FileName -> FilePos -> IndentInfo ->                   Rule (List (RigCount, Name, PTerm))  pibindListName fname start indents       = do rigc <- multiplicity            ns <- sepBy1 (symbol ",") unqualifiedName            symbol ":"            ty <- expr pdef fname indents            atEnd indents            rig <- getMult rigc            pure (map (\n => (rig, UN n, ty)) ns)     <|> sepBy1 (symbol ",")                (do rigc <- multiplicity                    n <- name                    symbol ":"                    ty <- expr pdef fname indents                    rig <- getMult rigc                    pure (rig, n, ty))   pibindList : FileName -> FilePos -> IndentInfo ->               Rule (List (RigCount, Maybe Name, PTerm))  pibindList fname start indents    = do params <- pibindListName fname start indents         pure $ map (\(rig, n, ty) => (rig, Just n, ty)) params   bindSymbol : Rule (PiInfo PTerm)  bindSymbol      = do symbol "->"           pure Explicit    <|> do symbol "=>"           pure AutoImplicit    explicitPi : FileName -> IndentInfo -> Rule PTerm  explicitPi fname indents      = do start <- location           symbol "("           binders <- pibindList fname start indents           symbol ")"           exp <- bindSymbol           scope <- typeExpr pdef fname indents           end <- location           pure (pibindAll (MkFC fname start end) exp binders scope)   autoImplicitPi : FileName -> IndentInfo -> Rule PTerm  autoImplicitPi fname indents      = do start <- location           symbol "{"           keyword "auto"           commit           binders <- pibindList fname start indents           symbol "}"           symbol "->"           scope <- typeExpr pdef fname indents           end <- location           pure (pibindAll (MkFC fname start end) AutoImplicit binders scope)   defaultImplicitPi : FileName -> IndentInfo -> Rule PTerm  defaultImplicitPi fname indents      = do start <- location           symbol "{"           keyword "default"           commit           t <- simpleExpr fname indents           binders <- pibindList fname start indents           symbol "}"           symbol "->"           scope <- typeExpr pdef fname indents           end <- location           pure (pibindAll (MkFC fname start end) (DefImplicit t) binders scope)   forall_ : FileName -> IndentInfo -> Rule PTerm  forall_ fname indents      = do start <- location           keyword "forall"           commit           nstart <- location           ns <- sepBy1 (symbol ",") unqualifiedName           nend <- location           let nfc = MkFC fname nstart nend           let binders = map (\n => (erased, Just (UN n), PImplicit nfc)) ns           symbol "."           scope <- typeExpr pdef fname indents           end <- location           pure (pibindAll (MkFC fname start end) Implicit binders scope)   implicitPi : FileName -> IndentInfo -> Rule PTerm  implicitPi fname indents      = do start <- location

Lines 1–500 of 1764. Load more