diff --git a/.gitignore b/.gitignore index d4dcc9ec4..e7780a7e8 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,4 @@ +idris2docs_venv *~ *.ibc *.ttc diff --git a/docs/source/reference/envvars.rst b/docs/source/reference/envvars.rst index a044b1d0b..582b9447e 100644 --- a/docs/source/reference/envvars.rst +++ b/docs/source/reference/envvars.rst @@ -4,4 +4,6 @@ Environment Variables ********************* -[TODO: Fill in the environment variables recognised by Idris 2] +.. todo:: + + Fill in the environment variables recognised by Idris 2 diff --git a/docs/source/reference/records.rst b/docs/source/reference/records.rst index 62439f87e..8c6799db5 100644 --- a/docs/source/reference/records.rst +++ b/docs/source/reference/records.rst @@ -14,7 +14,7 @@ Lexical structure constructor ``RF "foo"``) * ``Foo.bar.baz`` starting with uppercase ``F`` is one lexeme, a namespaced - identifier: ``NSIdent ["baz", "bar", "Foo"]`` + identifier: ``DotSepIdent ["baz", "bar", "Foo"]`` * ``foo.bar.baz`` starting with lowercase ``f`` is three lexemes: ``foo``, ``.bar``, ``.baz`` diff --git a/docs/source/tutorial/miscellany.rst b/docs/source/tutorial/miscellany.rst index bd1d65bd9..2f8aba3e9 100644 --- a/docs/source/tutorial/miscellany.rst +++ b/docs/source/tutorial/miscellany.rst @@ -81,9 +81,9 @@ number as 0), we could write: .. code-block:: idris - fibonacci : {default 0 lag : Nat} -> {default 1 lead : Nat} -> (n : Nat) -> Nat - fibonacci {lag} Z = lag - fibonacci {lag} {lead} (S n) = fibonacci {lag=lead} {lead=lag+lead} n + fibonacci : {default 0 lag : Nat} -> {default 1 lead : Nat} -> (n : Nat) -> Nat + fibonacci {lag} Z = lag + fibonacci {lag} {lead} (S n) = fibonacci {lag=lead} {lead=lag+lead} n After this definition, ``fibonacci 5`` is equivalent to ``fibonacci {lag=0} {lead=1} 5``, and will return the 5th fibonacci number. Note that while this works, this is not the @@ -114,7 +114,9 @@ any other character). Cumulativity ============ -[NOT YET IN IDRIS 2] +.. warning:: + + NOT YET IN IDRIS 2 Since values can appear in types and *vice versa*, it is natural that types themselves have types. For example: diff --git a/docs/source/tutorial/theorems.rst b/docs/source/tutorial/theorems.rst index e5a11e637..268ec6192 100644 --- a/docs/source/tutorial/theorems.rst +++ b/docs/source/tutorial/theorems.rst @@ -126,7 +126,7 @@ To see more detail on what's going on, we can replace the recursive call to ``plusReducesZ`` with a hole: .. code-block:: idris - + plusReducesZ (S k) = cong S ?help Then inspecting the type of the hole at the REPL shows us: @@ -361,7 +361,9 @@ total, a function ``f`` must: Directives and Compiler Flags for Totality ------------------------------------------ -[NOTE: Not all of this is implemented yet for Idris 2] +.. warning:: + + Not all of this is implemented yet for Idris 2 By default, Idris allows all well-typed definitions, whether total or not. However, it is desirable for functions to be total as far as possible, as this diff --git a/docs/source/tutorial/views.rst b/docs/source/tutorial/views.rst index a9fe7fc57..4840050cf 100644 --- a/docs/source/tutorial/views.rst +++ b/docs/source/tutorial/views.rst @@ -4,7 +4,9 @@ Views and the “``with``” rule ***************************** -[NOT UPDATED FOR IDRIS 2 YET] +.. warning:: + + NOT UPDATED FOR IDRIS 2 YET Dependent pattern matching ========================== diff --git a/docs/source/typedd/typedd.rst b/docs/source/typedd/typedd.rst index d73ef6048..a0943d7c8 100644 --- a/docs/source/typedd/typedd.rst +++ b/docs/source/typedd/typedd.rst @@ -461,4 +461,6 @@ In ``ATM.idr``, add: Chapter 15 ---------- -TODO +.. todo:: + + This chapter. diff --git a/idris2.ipkg b/idris2.ipkg index 54b6c23d0..96a47ba31 100644 --- a/idris2.ipkg +++ b/idris2.ipkg @@ -52,6 +52,7 @@ modules = Data.Bool.Extra, Data.IntMap, Data.LengthMatch, + Data.List.Extra, Data.NameMap, Data.StringMap, Data.These, @@ -83,9 +84,12 @@ modules = Idris.Version, Parser.Lexer.Common, + Parser.Lexer.Package, Parser.Lexer.Source, Parser.Rule.Common, + Parser.Rule.Package, Parser.Rule.Source, + Parser.Package, Parser.Source, Parser.Support, Parser.Unlit, diff --git a/idris2api.ipkg b/idris2api.ipkg index e530493e7..3b6cff3af 100644 --- a/idris2api.ipkg +++ b/idris2api.ipkg @@ -83,9 +83,12 @@ modules = Idris.Version, Parser.Lexer.Common, + Parser.Lexer.Package, Parser.Lexer.Source, Parser.Rule.Common, + Parser.Rule.Package, Parser.Rule.Source, + Parser.Package, Parser.Source, Parser.Support, Parser.Unlit, diff --git a/src/Core/Core.idr b/src/Core/Core.idr index dc6f4c6b8..f505d2fe4 100644 --- a/src/Core/Core.idr +++ b/src/Core/Core.idr @@ -119,7 +119,8 @@ data Error : Type where GenericMsg : FC -> String -> Error TTCError : TTCErrorMsg -> Error FileErr : String -> FileError -> Error - ParseFail : FC -> ParseError -> Error + ParseFail : Show token => + FC -> ParseError token -> Error ModuleNotFound : FC -> List String -> Error CyclicImports : List (List String) -> Error ForceNeeded : Error diff --git a/src/Data/List/Extra.idr b/src/Data/List/Extra.idr new file mode 100644 index 000000000..ca19f6f8e --- /dev/null +++ b/src/Data/List/Extra.idr @@ -0,0 +1,11 @@ +module Data.List.Extra + +%default covering + +||| Fetches the element at a given position. +||| Returns `Nothing` if the position beyond the list's end. +public export +elemAt : List a -> Nat -> Maybe a +elemAt [] _ = Nothing +elemAt (l :: _) Z = Just l +elemAt (_ :: ls) (S n) = elemAt ls n diff --git a/src/Idris/IDEMode/CaseSplit.idr b/src/Idris/IDEMode/CaseSplit.idr index 24e455c20..899fb3d33 100644 --- a/src/Idris/IDEMode/CaseSplit.idr +++ b/src/Idris/IDEMode/CaseSplit.idr @@ -19,19 +19,22 @@ import Idris.Resugar import Idris.Syntax import Data.List +import Data.List.Extra import Data.Strings import System.File %default covering -getLine : Nat -> List String -> Maybe String -getLine Z (l :: ls) = Just l -getLine (S k) (l :: ls) = getLine k ls -getLine _ [] = Nothing +||| A series of updates is a mapping from `RawName` to `String` +||| `RawName` is currently just an alias for `String` +||| `String` is a rendered `List SourcePart` +Updates : Type +Updates = List (RawName, String) +||| Convert a RawImp update to a SourcePart one toStrUpdate : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> - (Name, RawImp) -> Core (List (String, String)) + (Name, RawImp) -> Core Updates toStrUpdate (UN n, term) = do clause <- pterm term pure [(n, show (bracket clause))] @@ -46,38 +49,30 @@ toStrUpdate (UN n, term) bracket tm = PBracketed emptyFC tm toStrUpdate _ = pure [] -- can't replace non user names -dump : SourcePart -> String -dump (Whitespace str) = str -dump (Name n) = n -dump (HoleName n) = "?" ++ n -dump LBrace = "{" -dump RBrace = "}" -dump Equal = "=" -dump (Other str) = str - data UPD : Type where doUpdates : {auto u : Ref UPD (List String)} -> - Defs -> List (String, String) -> List SourcePart -> + Defs -> Updates -> List SourcePart -> Core (List SourcePart) doUpdates defs ups [] = pure [] doUpdates defs ups (LBrace :: xs) - = case dropSpace xs of + = let (ws, nws) = spanSpace xs in map (LBrace :: ws ++) $ + case nws of Name n :: RBrace :: rest => - pure (LBrace :: Name n :: + pure (Name n :: Whitespace " " :: Equal :: Whitespace " " :: !(doUpdates defs ups (Name n :: RBrace :: rest))) Name n :: Equal :: rest => - pure (LBrace :: Name n :: + pure (Name n :: Whitespace " " :: Equal :: Whitespace " " :: !(doUpdates defs ups rest)) - _ => pure (LBrace :: !(doUpdates defs ups xs)) + _ => doUpdates defs ups xs where - dropSpace : List SourcePart -> List SourcePart - dropSpace [] = [] - dropSpace (RBrace :: xs) = RBrace :: xs - dropSpace (Whitespace _ :: xs) = dropSpace xs - dropSpace (x :: xs) = x :: dropSpace xs + spanSpace : List SourcePart -> (List SourcePart, List SourcePart) + spanSpace [] = ([], []) + spanSpace (RBrace :: xs) = ([], RBrace :: xs) + spanSpace (w@(Whitespace _) :: xs) = mapFst (w ::) (spanSpace xs) + spanSpace (x :: xs) = map (x ::) (spanSpace xs) doUpdates defs ups (Name n :: xs) = case lookup n ups of Nothing => pure (Name n :: !(doUpdates defs ups xs)) @@ -94,20 +89,20 @@ doUpdates defs ups (x :: xs) -- Update the token list with the string replacements for each match, and return -- the newly generated strings. updateAll : {auto u : Ref UPD (List String)} -> - Defs -> List SourcePart -> List (List (String, String)) -> + Defs -> List SourcePart -> List Updates -> Core (List String) updateAll defs l [] = pure [] updateAll defs l (rs :: rss) = do l' <- doUpdates defs rs l rss' <- updateAll defs l rss - pure (concat (map dump l') :: rss') + pure (concatMap toString l' :: rss') -- Turn the replacements we got from 'getSplits' into a list of actual string -- replacements getReplaces : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> {auto o : Ref ROpts REPLOpts} -> - List (Name, RawImp) -> Core (List (String, String)) + List (Name, RawImp) -> Core Updates getReplaces updates = do strups <- traverse toStrUpdate updates pure (concat strups) @@ -135,7 +130,7 @@ updateCase splits line col Just f => do Right file <- coreLift $ readFile f | Left err => throw (FileErr f err) - let thisline = getLine (integerToNat (cast line)) (lines file) + let thisline = elemAt (lines file) (integerToNat (cast line)) case thisline of Nothing => throw (InternalError "File too short!") Just l => diff --git a/src/Idris/IDEMode/Parser.idr b/src/Idris/IDEMode/Parser.idr index 47e847732..d6054d4a2 100644 --- a/src/Idris/IDEMode/Parser.idr +++ b/src/Idris/IDEMode/Parser.idr @@ -5,31 +5,30 @@ module Idris.IDEMode.Parser import Idris.IDEMode.Commands -import Text.Parser +import Data.List +import Data.Strings import Parser.Lexer.Source import Parser.Source import Text.Lexer +import Text.Parser import Utils.Either import Utils.String -import Data.List -import Data.Strings - %hide Text.Lexer.symbols %hide Parser.Lexer.Source.symbols symbols : List String symbols = ["(", ":", ")"] -ideTokens : TokenMap SourceToken +ideTokens : TokenMap Token ideTokens = map (\x => (exact x, Symbol)) symbols ++ - [(digits, \x => Literal (cast x)), - (stringLit, \x => StrLit (stripQuotes x)), - (identAllowDashes, \x => NSIdent [x]), + [(digits, \x => IntegerLit (cast x)), + (stringLit, \x => StringLit (stripQuotes x)), + (identAllowDashes, \x => Ident x), (space, Comment)] -idelex : String -> Either (Int, Int, String) (List (TokenData SourceToken)) +idelex : String -> Either (Int, Int, String) (List (TokenData Token)) idelex str = case lex ideTokens str of -- Add the EndInput token so that we'll have a line and column @@ -38,12 +37,12 @@ idelex str [MkToken l c EndInput]) (_, fail) => Left fail where - notComment : TokenData SourceToken -> Bool + notComment : TokenData Token -> Bool notComment t = case tok t of Comment _ => False _ => True -sexp : SourceRule SExp +sexp : Rule SExp sexp = do symbol ":"; exactIdent "True" pure (BoolAtom True) @@ -60,15 +59,14 @@ sexp symbol ")" pure (SExpList xs) -ideParser : {e : _} -> - String -> Grammar (TokenData SourceToken) e ty -> Either ParseError ty +ideParser : {e : _} -> String -> Grammar (TokenData Token) e ty -> Either (ParseError Token) ty ideParser str p = do toks <- mapError LexFail $ idelex str - parsed <- mapError mapParseError $ parse p toks + parsed <- mapError toGenericParsingError $ parse p toks Right (fst parsed) export -parseSExp : String -> Either ParseError SExp +parseSExp : String -> Either (ParseError Token) SExp parseSExp inp = ideParser inp (do c <- sexp; eoi; pure c) diff --git a/src/Idris/IDEMode/TokenLine.idr b/src/Idris/IDEMode/TokenLine.idr index 63926a5ce..db5b986aa 100644 --- a/src/Idris/IDEMode/TokenLine.idr +++ b/src/Idris/IDEMode/TokenLine.idr @@ -4,16 +4,38 @@ module Idris.IDEMode.TokenLine import Parser.Lexer.Source import Text.Lexer +public export +RawName : Type +RawName = String + public export data SourcePart = Whitespace String - | Name String + | Name RawName | HoleName String | LBrace | RBrace | Equal | Other String +------------------------------------------------------------------------ +-- Printer +------------------------------------------------------------------------ + +export +toString : SourcePart -> String +toString (Whitespace str) = str +toString (Name n) = n +toString (HoleName n) = "?" ++ n +toString LBrace = "{" +toString RBrace = "}" +toString Equal = "=" +toString (Other str) = str + +------------------------------------------------------------------------ +-- Parser +------------------------------------------------------------------------ + holeIdent : Lexer holeIdent = is '?' <+> identNormal diff --git a/src/Idris/Package.idr b/src/Idris/Package.idr index f537f6431..709b4a420 100644 --- a/src/Idris/Package.idr +++ b/src/Idris/Package.idr @@ -15,6 +15,12 @@ import Data.Strings import Data.StringTrie import Data.These +import Parser.Package +import System +import Text.Parser +import Utils.Binary +import Utils.String + import Idris.CommandLine import Idris.ModTree import Idris.ProcessIdr @@ -23,13 +29,6 @@ import Idris.REPLOpts import Idris.SetOptions import Idris.Syntax import Idris.Version -import Parser.Lexer.Source -import Parser.Source -import Utils.Binary - -import System -import Text.Parser - import IdrisPaths %default covering @@ -114,7 +113,7 @@ data DescField : Type where PPreclean : FC -> String -> DescField PPostclean : FC -> String -> DescField -field : String -> SourceRule DescField +field : String -> Rule DescField field fname = strField PVersion "version" <|> strField PAuthors "authors" @@ -134,43 +133,41 @@ field fname <|> strField PPostinstall "postinstall" <|> strField PPreclean "preclean" <|> strField PPostclean "postclean" - <|> do exactIdent "depends"; symbol "=" - ds <- sepBy1 (symbol ",") unqualifiedName + <|> do exactProperty "depends" + equals + ds <- sep packageName pure (PDepends ds) - <|> do exactIdent "modules"; symbol "=" - ms <- sepBy1 (symbol ",") - (do start <- location - ns <- nsIdent - end <- location - Parser.Core.pure (MkFC fname start end, ns)) - Parser.Core.pure (PModules ms) - <|> do exactIdent "main"; symbol "=" + <|> do exactProperty "modules" + equals + ms <- sep (do start <- location + m <- moduleIdent + end <- location + pure (MkFC fname start end, m)) + pure (PModules ms) + <|> do exactProperty "main" + equals start <- location - m <- nsIdent + m <- namespacedIdent end <- location - Parser.Core.pure (PMainMod (MkFC fname start end) m) - <|> do exactIdent "executable"; symbol "=" - e <- unqualifiedName - Parser.Core.pure (PExec e) + pure (PMainMod (MkFC fname start end) m) + <|> do exactProperty "executable" + equals + e <- (stringLit <|> packageName) + pure (PExec e) where - getStr : (FC -> String -> DescField) -> FC -> - String -> Constant -> SourceEmptyRule DescField - getStr p fc fld (Str s) = pure (p fc s) - getStr p fc fld _ = fail $ fld ++ " field must be a string" - - strField : (FC -> String -> DescField) -> String -> SourceRule DescField - strField p f + strField : (FC -> String -> DescField) -> String -> Rule DescField + strField fieldConstructor fieldName = do start <- location - exactIdent f - symbol "=" - c <- constant + exactProperty fieldName + equals + str <- stringLit end <- location - getStr p (MkFC fname start end) f c + pure $ fieldConstructor (MkFC fname start end) str -parsePkgDesc : String -> SourceRule (String, List DescField) +parsePkgDesc : String -> Rule (String, List DescField) parsePkgDesc fname - = do exactIdent "package" - name <- unqualifiedName + = do exactProperty "package" + name <- packageName fields <- many (field fname) pure (name, fields) @@ -425,6 +422,12 @@ clean pkg delete $ ttFile ++ ".ttc" delete $ ttFile ++ ".ttm" +getParseErrorLoc : String -> ParseError Token -> FC +getParseErrorLoc fname (ParseFail _ (Just pos) _) = MkFC fname pos pos +getParseErrorLoc fname (LexFail (l, c, _)) = MkFC fname (l, c) (l, c) +getParseErrorLoc fname (LitFail _) = MkFC fname (0, 0) (0, 0) -- TODO: Remove this unused case +getParseErrorLoc fname _ = replFC + -- Just load the 'Main' module, if it exists, which will involve building -- it if necessary runRepl : {auto c : Ref Ctxt Defs} -> diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 5bd4f1d30..966fbb3e8 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -14,7 +14,7 @@ import Data.Strings %default covering -- Forward declare since they're used in the parser -topDecl : FileName -> IndentInfo -> SourceRule (List PDecl) +topDecl : FileName -> IndentInfo -> Rule (List PDecl) collectDefs : List PDecl -> List PDecl -- Some context for the parser @@ -46,7 +46,7 @@ plhs = MkParseOpts False False %hide Prelude.pure %hide Core.Core.pure -atom : FileName -> SourceRule PTerm +atom : FileName -> Rule PTerm atom fname = do start <- location x <- constant @@ -85,30 +85,30 @@ atom fname end <- location pure (PRef (MkFC fname start end) x) -whereBlock : FileName -> Int -> SourceRule (List PDecl) +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 error -commitKeyword : IndentInfo -> String -> SourceRule () +commitKeyword : IndentInfo -> String -> Rule () commitKeyword indents req = do mustContinue indents (Just req) keyword req mustContinue indents Nothing -commitSymbol : String -> SourceRule () +commitSymbol : String -> Rule () commitSymbol req = symbol req <|> fatalError ("Expected '" ++ req ++ "'") -continueWith : IndentInfo -> String -> SourceRule () +continueWith : IndentInfo -> String -> Rule () continueWith indents req = do mustContinue indents (Just req) symbol req -iOperator : SourceRule Name +iOperator : Rule Name iOperator = operator <|> do symbol "`" @@ -122,7 +122,7 @@ data ArgType | WithArg PTerm mutual - appExpr : ParseOpts -> FileName -> IndentInfo -> SourceRule PTerm + appExpr : ParseOpts -> FileName -> IndentInfo -> Rule PTerm appExpr q fname indents = case_ fname indents <|> lambdaCase fname indents @@ -153,7 +153,7 @@ mutual applyExpImp start end f (WithArg exp :: args) = applyExpImp start end (PWithApp (MkFC fname start end) f exp) args - argExpr : ParseOpts -> FileName -> IndentInfo -> SourceRule ArgType + argExpr : ParseOpts -> FileName -> IndentInfo -> Rule ArgType argExpr q fname indents = do continue indents arg <- simpleExpr fname indents @@ -170,7 +170,7 @@ mutual pure (WithArg arg) else fail "| not allowed here" - implicitArg : FileName -> IndentInfo -> SourceRule (Maybe Name, PTerm) + implicitArg : FileName -> IndentInfo -> Rule (Maybe Name, PTerm) implicitArg fname indents = do start <- location symbol "{" @@ -189,7 +189,7 @@ mutual symbol "}" pure (Nothing, tm) - with_ : FileName -> IndentInfo -> SourceRule PTerm + with_ : FileName -> IndentInfo -> Rule PTerm with_ fname indents = do start <- location keyword "with" @@ -199,12 +199,12 @@ mutual rhs <- expr pdef fname indents pure (PWithUnambigNames (MkFC fname start end) ns rhs) where - singleName : SourceRule (List Name) + singleName : Rule (List Name) singleName = do n <- name pure [n] - nameList : SourceRule (List Name) + nameList : Rule (List Name) nameList = do symbol "[" commit @@ -212,7 +212,7 @@ mutual symbol "]" pure ns - opExpr : ParseOpts -> FileName -> IndentInfo -> SourceRule PTerm + opExpr : ParseOpts -> FileName -> IndentInfo -> Rule PTerm opExpr q fname indents = do start <- location l <- appExpr q fname indents @@ -232,7 +232,7 @@ mutual pure (POp (MkFC fname start end) op l r)) <|> pure l - dpair : FileName -> FilePos -> IndentInfo -> SourceRule PTerm + dpair : FileName -> FilePos -> IndentInfo -> Rule PTerm dpair fname start indents = do x <- unqualifiedName symbol ":" @@ -255,7 +255,7 @@ mutual (PImplicit (MkFC fname start end)) rest) - bracketedExpr : FileName -> FilePos -> IndentInfo -> SourceRule PTerm + 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 @@ -287,7 +287,7 @@ mutual getInitRange [x, y] = pure (x, Just y) getInitRange _ = fatalError "Invalid list range syntax" - listRange : FileName -> FilePos -> IndentInfo -> List PTerm -> SourceRule PTerm + listRange : FileName -> FilePos -> IndentInfo -> List PTerm -> Rule PTerm listRange fname start indents xs = do symbol "]" end <- location @@ -301,7 +301,7 @@ mutual rstate <- getInitRange xs pure (PRange fc (fst rstate) (snd rstate) y) - listExpr : FileName -> FilePos -> IndentInfo -> SourceRule PTerm + listExpr : FileName -> FilePos -> IndentInfo -> Rule PTerm listExpr fname start indents = do ret <- expr pnowith fname indents symbol "|" @@ -317,7 +317,7 @@ mutual pure (PList (MkFC fname start end) xs)) -- A pair, dependent pair, or just a single expression - tuple : FileName -> FilePos -> IndentInfo -> PTerm -> SourceRule PTerm + tuple : FileName -> FilePos -> IndentInfo -> PTerm -> Rule PTerm tuple fname start indents e = do rest <- some (do symbol "," estart <- location @@ -337,7 +337,7 @@ mutual mergePairs end ((estart, exp) :: rest) = PPair (MkFC fname estart end) exp (mergePairs end rest) - simpleExpr : FileName -> IndentInfo -> SourceRule PTerm + simpleExpr : FileName -> IndentInfo -> Rule PTerm simpleExpr fname indents = do start <- location @@ -353,7 +353,7 @@ mutual [] => root fs => PRecordFieldAccess (MkFC fname start end) root recFields - simplerExpr : FileName -> IndentInfo -> SourceRule PTerm + simplerExpr : FileName -> IndentInfo -> Rule PTerm simplerExpr fname indents = do start <- location x <- unqualifiedName @@ -429,7 +429,7 @@ mutual = PPi fc rig p n ty (pibindAll fc p rest scope) bindList : FileName -> FilePos -> IndentInfo -> - SourceRule (List (RigCount, PTerm, PTerm)) + Rule (List (RigCount, PTerm, PTerm)) bindList fname start indents = sepBy1 (symbol ",") (do rigc <- multiplicity @@ -442,7 +442,7 @@ mutual pure (rig, pat, ty)) pibindListName : FileName -> FilePos -> IndentInfo -> - SourceRule (List (RigCount, Name, PTerm)) + Rule (List (RigCount, Name, PTerm)) pibindListName fname start indents = do rigc <- multiplicity ns <- sepBy1 (symbol ",") unqualifiedName @@ -460,12 +460,12 @@ mutual pure (rig, n, ty)) pibindList : FileName -> FilePos -> IndentInfo -> - SourceRule (List (RigCount, Maybe Name, PTerm)) + 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 : SourceRule (PiInfo PTerm) + bindSymbol : Rule (PiInfo PTerm) bindSymbol = do symbol "->" pure Explicit @@ -473,7 +473,7 @@ mutual pure AutoImplicit - explicitPi : FileName -> IndentInfo -> SourceRule PTerm + explicitPi : FileName -> IndentInfo -> Rule PTerm explicitPi fname indents = do start <- location symbol "(" @@ -484,7 +484,7 @@ mutual end <- location pure (pibindAll (MkFC fname start end) exp binders scope) - autoImplicitPi : FileName -> IndentInfo -> SourceRule PTerm + autoImplicitPi : FileName -> IndentInfo -> Rule PTerm autoImplicitPi fname indents = do start <- location symbol "{" @@ -497,7 +497,7 @@ mutual end <- location pure (pibindAll (MkFC fname start end) AutoImplicit binders scope) - defaultImplicitPi : FileName -> IndentInfo -> SourceRule PTerm + defaultImplicitPi : FileName -> IndentInfo -> Rule PTerm defaultImplicitPi fname indents = do start <- location symbol "{" @@ -511,7 +511,7 @@ mutual end <- location pure (pibindAll (MkFC fname start end) (DefImplicit t) binders scope) - forall_ : FileName -> IndentInfo -> SourceRule PTerm + forall_ : FileName -> IndentInfo -> Rule PTerm forall_ fname indents = do start <- location keyword "forall" @@ -527,7 +527,7 @@ mutual end <- location pure (pibindAll (MkFC fname start end) Implicit binders scope) - implicitPi : FileName -> IndentInfo -> SourceRule PTerm + implicitPi : FileName -> IndentInfo -> Rule PTerm implicitPi fname indents = do start <- location symbol "{" @@ -538,7 +538,7 @@ mutual end <- location pure (pibindAll (MkFC fname start end) Implicit binders scope) - lam : FileName -> IndentInfo -> SourceRule PTerm + lam : FileName -> IndentInfo -> Rule PTerm lam fname indents = do start <- location symbol "\\" @@ -555,7 +555,7 @@ mutual = PLam fc rig Explicit pat ty (bindAll fc rest scope) letBinder : FileName -> IndentInfo -> - SourceRule (FilePos, FilePos, RigCount, PTerm, PTerm, PTerm, List PClause) + Rule (FilePos, FilePos, RigCount, PTerm, PTerm, PTerm, List PClause) letBinder fname indents = do start <- location rigc <- multiplicity @@ -594,7 +594,7 @@ mutual = let fc = MkFC fname start end in DoLetPat fc pat ty val alts :: buildDoLets fname rest - let_ : FileName -> IndentInfo -> SourceRule PTerm + let_ : FileName -> IndentInfo -> Rule PTerm let_ fname indents = do start <- location keyword "let" @@ -613,7 +613,7 @@ mutual end <- location pure (PLocal (MkFC fname start end) (collectDefs (concat ds)) scope) - case_ : FileName -> IndentInfo -> SourceRule PTerm + case_ : FileName -> IndentInfo -> Rule PTerm case_ fname indents = do start <- location keyword "case" @@ -623,7 +623,7 @@ mutual end <- location pure (PCase (MkFC fname start end) scr alts) - lambdaCase : FileName -> IndentInfo -> SourceRule PTerm + lambdaCase : FileName -> IndentInfo -> Rule PTerm lambdaCase fname indents = do start <- location symbol "\\" *> keyword "case" @@ -638,13 +638,13 @@ mutual PLam fcCase top Explicit (PRef fcCase n) (PInfer fcCase) $ PCase fc (PRef fcCase n) alts) - caseAlt : FileName -> IndentInfo -> SourceRule PClause + caseAlt : FileName -> IndentInfo -> Rule PClause caseAlt fname indents = do start <- location lhs <- opExpr plhs fname indents caseRHS fname start indents lhs - caseRHS : FileName -> FilePos -> IndentInfo -> PTerm -> SourceRule PClause + caseRHS : FileName -> FilePos -> IndentInfo -> PTerm -> Rule PClause caseRHS fname start indents lhs = do symbol "=>" mustContinue indents Nothing @@ -657,7 +657,7 @@ mutual end <- location pure (MkImpossible (MkFC fname start end) lhs) - if_ : FileName -> IndentInfo -> SourceRule PTerm + if_ : FileName -> IndentInfo -> Rule PTerm if_ fname indents = do start <- location keyword "if" @@ -670,7 +670,7 @@ mutual end <- location pure (PIfThenElse (MkFC fname start end) x t e) - record_ : FileName -> IndentInfo -> SourceRule PTerm + record_ : FileName -> IndentInfo -> Rule PTerm record_ fname indents = do start <- location keyword "record" @@ -681,7 +681,7 @@ mutual end <- location pure (PUpdate (MkFC fname start end) fs) - field : FileName -> IndentInfo -> SourceRule PFieldUpdate + field : FileName -> IndentInfo -> Rule PFieldUpdate field fname indents = do path <- map fieldName <$> [| name :: many recFieldCompat |] upd <- (do symbol "="; pure PSetField) @@ -697,10 +697,10 @@ mutual -- this allows the dotted syntax .field -- but also the arrowed syntax ->field for compatibility with Idris 1 - recFieldCompat : SourceRule Name + recFieldCompat : Rule Name recFieldCompat = recField <|> (symbol "->" *> name) - rewrite_ : FileName -> IndentInfo -> SourceRule PTerm + rewrite_ : FileName -> IndentInfo -> Rule PTerm rewrite_ fname indents = do start <- location keyword "rewrite" @@ -710,7 +710,7 @@ mutual end <- location pure (PRewrite (MkFC fname start end) rule tm) - doBlock : FileName -> IndentInfo -> SourceRule PTerm + doBlock : FileName -> IndentInfo -> Rule PTerm doBlock fname indents = do start <- location keyword "do" @@ -728,7 +728,7 @@ mutual else fail "Not a pattern variable" validPatternVar _ = fail "Not a pattern variable" - doAct : FileName -> IndentInfo -> SourceRule (List PDo) + doAct : FileName -> IndentInfo -> Rule (List PDo) doAct fname indents = do start <- location n <- name @@ -768,12 +768,12 @@ mutual end <- location pure [DoBindPat (MkFC fname start end) e val alts]) - patAlt : FileName -> IndentInfo -> SourceRule PClause + patAlt : FileName -> IndentInfo -> Rule PClause patAlt fname indents = do symbol "|" caseAlt fname indents - lazy : FileName -> IndentInfo -> SourceRule PTerm + lazy : FileName -> IndentInfo -> Rule PTerm lazy fname indents = do start <- location exactIdent "Lazy" @@ -796,7 +796,7 @@ mutual end <- location pure (PForce (MkFC fname start end) tm) - binder : FileName -> IndentInfo -> SourceRule PTerm + binder : FileName -> IndentInfo -> Rule PTerm binder fname indents = let_ fname indents <|> autoImplicitPi fname indents @@ -806,7 +806,7 @@ mutual <|> explicitPi fname indents <|> lam fname indents - typeExpr : ParseOpts -> FileName -> IndentInfo -> SourceRule PTerm + typeExpr : ParseOpts -> FileName -> IndentInfo -> Rule PTerm typeExpr q fname indents = do start <- location arg <- opExpr q fname indents @@ -825,10 +825,10 @@ mutual (mkPi start end a as) export - expr : ParseOpts -> FileName -> IndentInfo -> SourceRule PTerm + expr : ParseOpts -> FileName -> IndentInfo -> Rule PTerm expr = typeExpr -visOption : SourceRule Visibility +visOption : Rule Visibility visOption = do keyword "public" keyword "export" @@ -843,7 +843,7 @@ visibility = visOption <|> pure Private -tyDecl : FileName -> IndentInfo -> SourceRule PTypeDecl +tyDecl : FileName -> IndentInfo -> Rule PTypeDecl tyDecl fname indents = do start <- location n <- name @@ -857,7 +857,7 @@ tyDecl fname indents mutual parseRHS : (withArgs : Nat) -> FileName -> FilePos -> Int -> - IndentInfo -> (lhs : PTerm) -> SourceRule PClause + IndentInfo -> (lhs : PTerm) -> Rule PClause parseRHS withArgs fname start col indents lhs = do symbol "=" mustWork $ @@ -882,7 +882,7 @@ mutual ifThenElse True t e = t ifThenElse False t e = e - clause : Nat -> FileName -> IndentInfo -> SourceRule PClause + clause : Nat -> FileName -> IndentInfo -> Rule PClause clause withArgs fname indents = do start <- location col <- column @@ -898,7 +898,7 @@ mutual applyArgs f [] = f applyArgs f ((fc, a) :: args) = applyArgs (PApp fc f a) args - parseWithArg : SourceRule (FC, PTerm) + parseWithArg : Rule (FC, PTerm) parseWithArg = do symbol "|" start <- location @@ -927,7 +927,7 @@ mkDataConType fc ret (WithArg a :: xs) = PImplicit fc -- This can't happen because we parse constructors without -- withOK set -simpleCon : FileName -> PTerm -> IndentInfo -> SourceRule PTypeDecl +simpleCon : FileName -> PTerm -> IndentInfo -> Rule PTypeDecl simpleCon fname ret indents = do start <- location cname <- name @@ -937,7 +937,7 @@ simpleCon fname ret indents pure (let cfc = MkFC fname start end in MkPTy cfc cname (mkDataConType cfc ret params)) -simpleData : FileName -> FilePos -> Name -> IndentInfo -> SourceRule PDataDecl +simpleData : FileName -> FilePos -> Name -> IndentInfo -> Rule PDataDecl simpleData fname start n indents = do params <- many name tyend <- location @@ -951,7 +951,7 @@ simpleData fname start n indents pure (MkPData (MkFC fname start end) n (mkTyConType tyfc params) [] cons) -dataOpt : SourceRule DataOpt +dataOpt : Rule DataOpt dataOpt = do exactIdent "noHints" pure NoHints @@ -980,14 +980,14 @@ dataBody fname mincol start n indents ty end <- location pure (MkPData (MkFC fname start end) n ty opts cs) -gadtData : FileName -> Int -> FilePos -> Name -> IndentInfo -> SourceRule PDataDecl +gadtData : FileName -> Int -> FilePos -> Name -> IndentInfo -> Rule PDataDecl gadtData fname mincol start n indents = do symbol ":" commit ty <- expr pdef fname indents dataBody fname mincol start n indents ty -dataDeclBody : FileName -> IndentInfo -> SourceRule PDataDecl +dataDeclBody : FileName -> IndentInfo -> Rule PDataDecl dataDeclBody fname indents = do start <- location col <- column @@ -996,7 +996,7 @@ dataDeclBody fname indents simpleData fname start n indents <|> gadtData fname col start n indents -dataDecl : FileName -> IndentInfo -> SourceRule PDecl +dataDecl : FileName -> IndentInfo -> Rule PDecl dataDecl fname indents = do start <- location vis <- visibility @@ -1011,19 +1011,19 @@ stripBraces str = pack (drop '{' (reverse (drop '}' (reverse (unpack str))))) drop c [] = [] drop c (c' :: xs) = if c == c' then drop c xs else c' :: xs -onoff : SourceRule Bool +onoff : Rule Bool onoff = do exactIdent "on" pure True <|> do exactIdent "off" pure False -extension : SourceRule LangExt +extension : Rule LangExt extension = do exactIdent "Borrowing" pure Borrowing -totalityOpt : SourceRule TotalReq +totalityOpt : Rule TotalReq totalityOpt = do keyword "partial" pure PartialOK @@ -1032,7 +1032,7 @@ totalityOpt <|> do keyword "covering" pure CoveringOnly -directive : FileName -> IndentInfo -> SourceRule Directive +directive : FileName -> IndentInfo -> Rule Directive directive fname indents = do pragma "hide" n <- name @@ -1107,21 +1107,21 @@ directive fname indents atEnd indents pure (DefaultTotality tot) -fix : SourceRule Fixity +fix : Rule Fixity fix = do keyword "infixl"; pure InfixL <|> do keyword "infixr"; pure InfixR <|> do keyword "infix"; pure Infix <|> do keyword "prefix"; pure Prefix -namespaceHead : SourceRule (List String) +namespaceHead : Rule (List String) namespaceHead = do keyword "namespace" commit - ns <- nsIdent + ns <- namespacedIdent pure ns -namespaceDecl : FileName -> IndentInfo -> SourceRule PDecl +namespaceDecl : FileName -> IndentInfo -> Rule PDecl namespaceDecl fname indents = do start <- location ns <- namespaceHead @@ -1129,7 +1129,7 @@ namespaceDecl fname indents ds <- assert_total (nonEmptyBlock (topDecl fname)) pure (PNamespace (MkFC fname start end) ns (concat ds)) -transformDecl : FileName -> IndentInfo -> SourceRule PDecl +transformDecl : FileName -> IndentInfo -> Rule PDecl transformDecl fname indents = do start <- location pragma "transform" @@ -1140,7 +1140,7 @@ transformDecl fname indents end <- location pure (PTransform (MkFC fname start end) n lhs rhs) -mutualDecls : FileName -> IndentInfo -> SourceRule PDecl +mutualDecls : FileName -> IndentInfo -> Rule PDecl mutualDecls fname indents = do start <- location keyword "mutual" @@ -1149,7 +1149,7 @@ mutualDecls fname indents end <- location pure (PMutual (MkFC fname start end) (concat ds)) -paramDecls : FileName -> IndentInfo -> SourceRule PDecl +paramDecls : FileName -> IndentInfo -> Rule PDecl paramDecls fname indents = do start <- location keyword "parameters" @@ -1165,7 +1165,7 @@ paramDecls fname indents end <- location pure (PParameters (MkFC fname start end) ps (collectDefs (concat ds))) -usingDecls : FileName -> IndentInfo -> SourceRule PDecl +usingDecls : FileName -> IndentInfo -> Rule PDecl usingDecls fname indents = do start <- location keyword "using" @@ -1183,11 +1183,11 @@ usingDecls fname indents end <- location pure (PUsing (MkFC fname start end) us (collectDefs (concat ds))) -fnOpt : SourceRule PFnOpt +fnOpt : Rule PFnOpt fnOpt = do x <- totalityOpt pure $ IFnOpt (Totality x) -fnDirectOpt : FileName -> SourceRule PFnOpt +fnDirectOpt : FileName -> Rule PFnOpt fnDirectOpt fname = do pragma "hint" pure $ IFnOpt (Hint True) @@ -1212,7 +1212,7 @@ fnDirectOpt fname cs <- block (expr pdef fname) pure $ PForeign cs -visOpt : FileName -> SourceRule (Either Visibility PFnOpt) +visOpt : FileName -> Rule (Either Visibility PFnOpt) visOpt fname = do vis <- visOption pure (Left vis) @@ -1264,7 +1264,7 @@ implBinds fname indents pure ((n, rig, tm) :: more) <|> pure [] -ifaceParam : FileName -> IndentInfo -> SourceRule (Name, PTerm) +ifaceParam : FileName -> IndentInfo -> Rule (Name, PTerm) ifaceParam fname indents = do symbol "(" n <- name @@ -1277,7 +1277,7 @@ ifaceParam fname indents end <- location pure (n, PInfer (MkFC fname start end)) -ifaceDecl : FileName -> IndentInfo -> SourceRule PDecl +ifaceDecl : FileName -> IndentInfo -> Rule PDecl ifaceDecl fname indents = do start <- location vis <- visibility @@ -1298,7 +1298,7 @@ ifaceDecl fname indents pure (PInterface (MkFC fname start end) vis cons n params det dc (collectDefs (concat body))) -implDecl : FileName -> IndentInfo -> SourceRule PDecl +implDecl : FileName -> IndentInfo -> Rule PDecl implDecl fname indents = do start <- location visOpts <- many (visOpt fname) @@ -1325,7 +1325,7 @@ implDecl fname indents vis opts Single impls cons n params iname nusing (map (collectDefs . concat) body)) -fieldDecl : FileName -> IndentInfo -> SourceRule (List PField) +fieldDecl : FileName -> IndentInfo -> Rule (List PField) fieldDecl fname indents = do symbol "{" commit @@ -1337,7 +1337,7 @@ fieldDecl fname indents atEnd indents pure fs where - fieldBody : PiInfo PTerm -> SourceRule (List PField) + fieldBody : PiInfo PTerm -> Rule (List PField) fieldBody p = do start <- location m <- multiplicity @@ -1349,7 +1349,7 @@ fieldDecl fname indents end <- location pure (map (\n => MkField (MkFC fname start end) rig p n ty) ns) -recordParam : FileName -> IndentInfo -> SourceRule (List (Name, RigCount, PiInfo PTerm, PTerm)) +recordParam : FileName -> IndentInfo -> Rule (List (Name, RigCount, PiInfo PTerm, PTerm)) recordParam fname indents = do symbol "(" start <- location @@ -1374,7 +1374,7 @@ recordParam fname indents end <- location pure [(n, top, Explicit, PInfer (MkFC fname start end))] -recordDecl : FileName -> IndentInfo -> SourceRule PDecl +recordDecl : FileName -> IndentInfo -> Rule PDecl recordDecl fname indents = do start <- location vis <- visibility @@ -1389,13 +1389,13 @@ recordDecl fname indents pure (PRecord (MkFC fname start end) vis n params (fst dcflds) (concat (snd dcflds))) where - ctor : IndentInfo -> SourceRule Name + ctor : IndentInfo -> Rule Name ctor idt = do exactIdent "constructor" n <- name atEnd idt pure n -claim : FileName -> IndentInfo -> SourceRule PDecl +claim : FileName -> IndentInfo -> Rule PDecl claim fname indents = do start <- location visOpts <- many (visOpt fname) @@ -1407,14 +1407,14 @@ claim fname indents end <- location pure (PClaim (MkFC fname start end) rig vis opts cl) -definition : FileName -> IndentInfo -> SourceRule PDecl +definition : FileName -> IndentInfo -> Rule PDecl definition fname indents = do start <- location nd <- clause 0 fname indents end <- location pure (PDef (MkFC fname start end) [nd]) -fixDecl : FileName -> IndentInfo -> SourceRule (List PDecl) +fixDecl : FileName -> IndentInfo -> Rule (List PDecl) fixDecl fname indents = do start <- location fixity <- fix @@ -1424,7 +1424,7 @@ fixDecl fname indents end <- location pure (map (PFixity (MkFC fname start end) fixity (fromInteger prec)) ops) -directiveDecl : FileName -> IndentInfo -> SourceRule PDecl +directiveDecl : FileName -> IndentInfo -> Rule PDecl directiveDecl fname indents = do start <- location (do d <- directive fname indents @@ -1438,7 +1438,7 @@ directiveDecl fname indents pure (PReflect (MkFC fname start end) tm)) -- Declared at the top --- topDecl : FileName -> IndentInfo -> SourceRule (List PDecl) +-- topDecl : FileName -> IndentInfo -> Rule (List PDecl) topDecl fname indents = do d <- dataDecl fname indents pure [d] @@ -1507,15 +1507,15 @@ collectDefs (d :: ds) = d :: collectDefs ds export -import_ : FileName -> IndentInfo -> SourceRule Import +import_ : FileName -> IndentInfo -> Rule Import import_ fname indents = do start <- location keyword "import" reexp <- option False (do keyword "public" pure True) - ns <- nsIdent + ns <- namespacedIdent nsAs <- option ns (do exactIdent "as" - nsIdent) + namespacedIdent) end <- location atEnd indents pure (MkImport (MkFC fname start end) reexp ns nsAs) @@ -1526,7 +1526,7 @@ prog fname = do start <- location nspace <- option ["Main"] (do keyword "module" - nsIdent) + namespacedIdent) end <- location imports <- block (import_ fname) ds <- block (topDecl fname) @@ -1539,13 +1539,13 @@ progHdr fname = do start <- location nspace <- option ["Main"] (do keyword "module" - nsIdent) + namespacedIdent) end <- location imports <- block (import_ fname) pure (MkModule (MkFC fname start end) nspace imports []) -parseMode : SourceRule REPLEval +parseMode : Rule REPLEval parseMode = do exactIdent "typecheck" pure EvalTC @@ -1560,7 +1560,7 @@ parseMode <|> do exactIdent "exec" pure Execute -setVarOption : SourceRule REPLOpt +setVarOption : Rule REPLOpt setVarOption = do exactIdent "eval" mode <- parseMode @@ -1572,7 +1572,7 @@ setVarOption c <- unqualifiedName pure (CG c) -setOption : Bool -> SourceRule REPLOpt +setOption : Bool -> Rule REPLOpt setOption set = do exactIdent "showimplicits" pure (ShowImplicits set) @@ -1582,7 +1582,7 @@ setOption set pure (ShowTypes set) <|> if set then setVarOption else fatalError "Unrecognised option" -replCmd : List String -> SourceRule () +replCmd : List String -> Rule () replCmd [] = fail "Unrecognised command" replCmd (c :: cs) = exactIdent c @@ -1590,7 +1590,7 @@ replCmd (c :: cs) <|> replCmd cs export -editCmd : SourceRule EditCmd +editCmd : Rule EditCmd editCmd = do replCmd ["typeat"] line <- intLit @@ -1676,7 +1676,7 @@ data ParseCmd : Type where ParseIdentCmd : String -> ParseCmd CommandDefinition : Type -CommandDefinition = (List String, CmdArg, String, SourceRule REPLCmd) +CommandDefinition = (List String, CmdArg, String, Rule REPLCmd) CommandTable : Type CommandTable = List CommandDefinition @@ -1686,7 +1686,7 @@ extractNames (ParseREPLCmd names) = names extractNames (ParseKeywordCmd keyword) = [keyword] extractNames (ParseIdentCmd ident) = [ident] -runParseCmd : ParseCmd -> SourceRule () +runParseCmd : ParseCmd -> Rule () runParseCmd (ParseREPLCmd names) = replCmd names runParseCmd (ParseKeywordCmd keyword') = keyword keyword' runParseCmd (ParseIdentCmd ident) = exactIdent ident @@ -1697,7 +1697,7 @@ noArgCmd parseCmd command doc = (names, NoArg, doc, parse) names : List String names = extractNames parseCmd - parse : SourceRule REPLCmd + parse : Rule REPLCmd parse = do symbol ":" runParseCmd parseCmd @@ -1709,7 +1709,7 @@ nameArgCmd parseCmd command doc = (names, NameArg, doc, parse) names : List String names = extractNames parseCmd - parse : SourceRule REPLCmd + parse : Rule REPLCmd parse = do symbol ":" runParseCmd parseCmd @@ -1722,7 +1722,7 @@ exprArgCmd parseCmd command doc = (names, ExprArg, doc, parse) names : List String names = extractNames parseCmd - parse : SourceRule REPLCmd + parse : Rule REPLCmd parse = do symbol ":" runParseCmd parseCmd @@ -1735,7 +1735,7 @@ optArgCmd parseCmd command set doc = (names, OptionArg, doc, parse) names : List String names = extractNames parseCmd - parse : SourceRule REPLCmd + parse : Rule REPLCmd parse = do symbol ":" runParseCmd parseCmd @@ -1748,7 +1748,7 @@ numberArgCmd parseCmd command doc = (names, NumberArg, doc, parse) names : List String names = extractNames parseCmd - parse : SourceRule REPLCmd + parse : Rule REPLCmd parse = do symbol ":" runParseCmd parseCmd @@ -1761,7 +1761,7 @@ compileArgsCmd parseCmd command doc = (names, FileArg, doc, parse) names : List String names = extractNames parseCmd - parse : SourceRule REPLCmd + parse : Rule REPLCmd parse = do symbol ":" runParseCmd parseCmd @@ -1797,11 +1797,11 @@ help = ([""], NoArg, "Evaluate an expression") :: map (\ (names, args, text, _) => (map (":" ++) names, args, text)) parserCommandsForHelp -nonEmptyCommand : SourceRule REPLCmd +nonEmptyCommand : Rule REPLCmd nonEmptyCommand = choice (map (\ (_, _, _, parser) => parser) parserCommandsForHelp) -eval : SourceRule REPLCmd +eval : Rule REPLCmd eval = do tm <- expr pdef "(interactive)" init pure (Eval tm) diff --git a/src/Idris/ProcessIdr.idr b/src/Idris/ProcessIdr.idr index b2ec38513..e150da538 100644 --- a/src/Idris/ProcessIdr.idr +++ b/src/Idris/ProcessIdr.idr @@ -177,7 +177,7 @@ modTime fname pure (cast t) export -getParseErrorLoc : String -> ParseError -> FC +getParseErrorLoc : String -> ParseError Token -> FC getParseErrorLoc fname (ParseFail _ (Just pos) _) = MkFC fname pos pos getParseErrorLoc fname (LexFail (l, c, _)) = MkFC fname (l, c) (l, c) getParseErrorLoc fname (LitFail (MkLitErr l c _)) = MkFC fname (l, 0) (l, 0) @@ -195,7 +195,7 @@ readHeader path where -- Stop at the first :, that's definitely not part of the header, to -- save lexing the whole file unnecessarily - isColon : TokenData SourceToken -> Bool + isColon : TokenData Token -> Bool isColon t = case tok t of Symbol ":" => True diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index 55d6c33c2..9ddd82a7d 100644 --- a/src/Idris/REPL.idr +++ b/src/Idris/REPL.idr @@ -749,7 +749,7 @@ parseCmd : SourceEmptyRule (Maybe REPLCmd) parseCmd = do c <- command; eoi; pure $ Just c export -parseRepl : String -> Either ParseError (Maybe REPLCmd) +parseRepl : String -> Either (ParseError Token) (Maybe REPLCmd) parseRepl inp = case fnameCmd [(":load ", Load), (":l ", Load), (":cd ", CD)] inp of Nothing => runParser Nothing inp (parseEmptyCmd <|> parseCmd) diff --git a/src/Parser/Lexer/Common.idr b/src/Parser/Lexer/Common.idr index afd2851e8..1d5f44b4b 100644 --- a/src/Parser/Lexer/Common.idr +++ b/src/Parser/Lexer/Common.idr @@ -18,15 +18,13 @@ comment -- There are multiple variants. public export -data Flavour = Capitalised | AllowDashes | Normal +data Flavour = AllowDashes | Capitalised | Normal -export isIdentStart : Flavour -> Char -> Bool isIdentStart _ '_' = True isIdentStart Capitalised x = isUpper x || x > chr 160 isIdentStart _ x = isAlpha x || x > chr 160 -export isIdentTrailing : Flavour -> Char -> Bool isIdentTrailing AllowDashes '-' = True isIdentTrailing _ '\'' = True @@ -45,3 +43,26 @@ ident : Flavour -> Lexer ident flavour = (pred $ isIdentStart flavour) <+> (many . pred $ isIdentTrailing flavour) + +export +isIdentNormal : String -> Bool +isIdentNormal = isIdent Normal + +export +identNormal : Lexer +identNormal = ident Normal + +export +identAllowDashes : Lexer +identAllowDashes = ident AllowDashes + +namespaceIdent : Lexer +namespaceIdent = ident Capitalised <+> many (is '.' <+> ident Capitalised <+> expect (is '.')) + +export +namespacedIdent : Lexer +namespacedIdent = namespaceIdent <+> opt (is '.' <+> identNormal) + +export +spacesOrNewlines : Lexer +spacesOrNewlines = some (space <|> newline) diff --git a/src/Parser/Lexer/Package.idr b/src/Parser/Lexer/Package.idr new file mode 100644 index 000000000..2fc2ebc9e --- /dev/null +++ b/src/Parser/Lexer/Package.idr @@ -0,0 +1,65 @@ +module Parser.Lexer.Package + +import public Parser.Lexer.Common +import public Text.Lexer +import public Text.Parser + +import Data.List +import Data.Strings +import Data.String.Extra +import Utils.String + +%default total + +public export +data Token + = Comment String + | EndOfInput + | Equals + | DotSepIdent (List String) + | Separator + | Space + | StringLit String + +public export +Show Token where + show (Comment str) = "Comment: " ++ str + show EndOfInput = "EndOfInput" + show Equals = "Equals" + show (DotSepIdent dsid) = "DotSepIdentifier: " ++ dotSep dsid + show Separator = "Separator" + show Space = "Space" + show (StringLit s) = "StringLit: " ++ s + +equals : Lexer +equals = is '=' + +separator : Lexer +separator = is ',' + +rawTokens : TokenMap Token +rawTokens = + [ (equals, const Equals) + , (comment, Comment . drop 2) + , (namespacedIdent, DotSepIdent . splitNamespace) + , (identAllowDashes, DotSepIdent . pure) + , (separator, const Separator) + , (spacesOrNewlines, const Space) + , (stringLit, \s => StringLit (stripQuotes s)) + ] + where + splitNamespace : String -> List String + splitNamespace = Data.Strings.split (== '.') + +export +lex : String -> Either (Int, Int, String) (List (TokenData Token)) +lex str = + case lexTo (const False) rawTokens str of + (tokenData, (l, c, "")) => + Right $ (filter (useful . tok) tokenData) ++ [MkToken l c EndOfInput] + (_, fail) => Left fail + where + useful : Token -> Bool + useful (Comment c) = False + useful Space = False + useful _ = True diff --git a/src/Parser/Lexer/Source.idr b/src/Parser/Lexer/Source.idr index 661a7571b..832fbfed2 100644 --- a/src/Parser/Lexer/Source.idr +++ b/src/Parser/Lexer/Source.idr @@ -12,46 +12,50 @@ import Utils.String %default total public export -data SourceToken - = NSIdent (List String) - | HoleIdent String - | Literal Integer - | StrLit String - | CharLit String +data Token + -- Literals + = CharLit String | DoubleLit Double + | IntegerLit Integer + | StringLit String + -- Identifiers + | HoleIdent String + | Ident String + | DotSepIdent (List String) + | RecordField String | Symbol String - | Keyword String - | Unrecognised String + -- Comments | Comment String | DocComment String + -- Special | CGDirective String - | RecordField String - | Pragma String | EndInput + | Keyword String + | Pragma String + | Unrecognised String export -Show SourceToken where - show (HoleIdent x) = "hole identifier " ++ x - show (Literal x) = "literal " ++ show x - show (StrLit x) = "string " ++ show x +Show Token where + -- Literals show (CharLit x) = "character " ++ show x show (DoubleLit x) = "double " ++ show x + show (IntegerLit x) = "literal " ++ show x + show (StringLit x) = "string " ++ show x + -- Identifiers + show (HoleIdent x) = "hole identifier " ++ x + show (Ident x) = "identifier " ++ x + show (DotSepIdent xs) = "namespaced identifier " ++ dotSep (reverse xs) + show (RecordField x) = "record field " ++ x show (Symbol x) = "symbol " ++ x - show (Keyword x) = x - show (Unrecognised x) = "Unrecognised " ++ x + -- Comments show (Comment _) = "comment" show (DocComment _) = "doc comment" + -- Special show (CGDirective x) = "CGDirective " ++ x - show (RecordField x) = "record field " ++ x - show (Pragma x) = "pragma " ++ x show EndInput = "end of input" - show (NSIdent [x]) = "identifier " ++ x - show (NSIdent xs) = "namespaced identifier " ++ dotSep (reverse xs) - where - dotSep : List String -> String - dotSep [] = "" - dotSep [x] = x - dotSep (x :: xs) = x ++ concat ["." ++ y | y <- xs] + show (Keyword x) = x + show (Pragma x) = "pragma " ++ x + show (Unrecognised x) = "Unrecognised " ++ x mutual ||| The mutually defined functions represent different states in a @@ -102,29 +106,14 @@ blockComment = is '{' <+> is '-' <+> toEndComment 1 docComment : Lexer docComment = is '|' <+> is '|' <+> is '|' <+> many (isNot '\n') -export -isIdentNormal : String -> Bool -isIdentNormal = isIdent Normal - -export -identNormal : Lexer -identNormal = ident Normal - -export -identAllowDashes : Lexer -identAllowDashes = ident AllowDashes - holeIdent : Lexer -holeIdent = is '?' <+> ident Normal - -nsIdent : Lexer -nsIdent = ident Capitalised <+> many (is '.' <+> ident Normal) +holeIdent = is '?' <+> identNormal recField : Lexer -recField = is '.' <+> ident Normal +recField = is '.' <+> identNormal pragma : Lexer -pragma = is '%' <+> ident Normal +pragma = is '%' <+> identNormal doubleLit : Lexer doubleLit @@ -142,7 +131,7 @@ cgDirective is '}') <|> many (isNot '\n')) -mkDirective : String -> SourceToken +mkDirective : String -> Token mkDirective str = CGDirective (trim (substr 3 (length str) str)) -- Reserved words @@ -171,7 +160,6 @@ symbols "(", ")", "{", "}", "[", "]", ",", ";", "_", "`(", "`"] - export isOpChar : Char -> Bool isOpChar c = c `elem` (unpack ":!#$%&*+./<=>?@\\^|-~") @@ -205,7 +193,7 @@ fromOctLit str Nothing => 0 -- can't happen if the literal lexed correctly Just n => cast n -rawTokens : TokenMap SourceToken +rawTokens : TokenMap Token rawTokens = [(comment, Comment), (blockComment, Comment), @@ -214,31 +202,30 @@ rawTokens = (holeIdent, \x => HoleIdent (assert_total (strTail x)))] ++ map (\x => (exact x, Symbol)) symbols ++ [(doubleLit, \x => DoubleLit (cast x)), - (hexLit, \x => Literal (fromHexLit x)), - (octLit, \x => Literal (fromOctLit x)), - (digits, \x => Literal (cast x)), - (stringLit, \x => StrLit (stripQuotes x)), + (hexLit, \x => IntegerLit (fromHexLit x)), + (octLit, \x => IntegerLit (fromOctLit x)), + (digits, \x => IntegerLit (cast x)), + (stringLit, \x => StringLit (stripQuotes x)), (charLit, \x => CharLit (stripQuotes x)), (recField, \x => RecordField (assert_total $ strTail x)), - (nsIdent, parseNSIdent), - (ident Normal, parseIdent), + (namespacedIdent, parseNamespace), + (identNormal, parseIdent), (pragma, \x => Pragma (assert_total $ strTail x)), (space, Comment), (validSymbol, Symbol), (symbol, Unrecognised)] where - parseNSIdent : String -> SourceToken - parseNSIdent = NSIdent . reverse . split (== '.') - - parseIdent : String -> SourceToken - parseIdent x = - if x `elem` keywords - then Keyword x - else NSIdent [x] + parseIdent : String -> Token + parseIdent x = if x `elem` keywords then Keyword x + else Ident x + parseNamespace : String -> Token + parseNamespace ns = case Data.List.reverse . split (== '.') $ ns of + [ident] => parseIdent ident + ns => DotSepIdent ns export -lexTo : (TokenData SourceToken -> Bool) -> - String -> Either (Int, Int, String) (List (TokenData SourceToken)) +lexTo : (TokenData Token -> Bool) -> + String -> Either (Int, Int, String) (List (TokenData Token)) lexTo pred str = case lexTo pred rawTokens str of -- Add the EndInput token so that we'll have a line and column @@ -247,12 +234,12 @@ lexTo pred str [MkToken l c EndInput]) (_, fail) => Left fail where - notComment : TokenData SourceToken -> Bool + notComment : TokenData Token -> Bool notComment t = case tok t of Comment _ => False DocComment _ => False -- TODO! _ => True export -lex : String -> Either (Int, Int, String) (List (TokenData SourceToken)) +lex : String -> Either (Int, Int, String) (List (TokenData Token)) lex = lexTo (const False) diff --git a/src/Parser/Package.idr b/src/Parser/Package.idr new file mode 100644 index 000000000..6b1089595 --- /dev/null +++ b/src/Parser/Package.idr @@ -0,0 +1,24 @@ +module Parser.Package + +import public Parser.Lexer.Package +import public Parser.Rule.Package +import public Text.Lexer +import public Text.Parser +import public Parser.Support + +import System.File +import Utils.Either + +export +runParser : String -> Rule ty -> Either (ParseError Token) ty +runParser str p + = do toks <- mapError LexFail $ lex str + parsed <- mapError toGenericParsingError $ parse p toks + Right (fst parsed) + +export +parseFile : (fn : String) -> Rule ty -> IO (Either (ParseError Token) ty) +parseFile fn p + = do Right str <- readFile fn + | Left err => pure (Left (FileFail err)) + pure (runParser str p) diff --git a/src/Parser/Rule/Package.idr b/src/Parser/Rule/Package.idr new file mode 100644 index 000000000..7ff6dbabb --- /dev/null +++ b/src/Parser/Rule/Package.idr @@ -0,0 +1,79 @@ +module Parser.Rule.Package + +import public Parser.Lexer.Package +import public Parser.Rule.Common + +import Data.List + +%default total + +public export +Rule : Type -> Type +Rule = Rule Token + +public export +PackageEmptyRule : Type -> Type +PackageEmptyRule = EmptyRule Token + +export +equals : Rule () +equals = terminal "Expected equals" + (\x => case tok x of + Equals => Just () + _ => Nothing) + +export +eoi : Rule () +eoi = terminal "Expected end of input" + (\x => case tok x of + EndOfInput => Just () + _ => Nothing) + +export +exactProperty : String -> Rule String +exactProperty p = terminal ("Expected property " ++ p) + (\x => case tok x of + DotSepIdent [p'] => + if p == p' then Just p + else Nothing + _ => Nothing) + +export +stringLit : Rule String +stringLit = terminal "Expected string" + (\x => case tok x of + StringLit str => Just str + _ => Nothing) + +export +namespacedIdent : Rule (List String) +namespacedIdent = terminal "Expected namespaced identifier" + (\x => case tok x of + DotSepIdent nsid => Just $ reverse nsid + _ => Nothing) + +export +moduleIdent : Rule (List String) +moduleIdent = terminal "Expected module identifier" + (\x => case tok x of + DotSepIdent m => Just $ reverse m + _ => Nothing) + +export +packageName : Rule String +packageName = terminal "Expected package name" + (\x => case tok x of + DotSepIdent [str] => + if isIdent AllowDashes str then Just str + else Nothing + _ => Nothing) + +sep' : Rule () +sep' = terminal "Expected separator" + (\x => case tok x of + Separator => Just () + _ => Nothing) + +export +sep : Rule t -> Rule (List t) +sep rule = sepBy1 sep' rule diff --git a/src/Parser/Rule/Source.idr b/src/Parser/Rule/Source.idr index 49c302ddc..c54c2f666 100644 --- a/src/Parser/Rule/Source.idr +++ b/src/Parser/Rule/Source.idr @@ -9,12 +9,12 @@ import Core.TT %default total public export -SourceRule : Type -> Type -SourceRule = Rule SourceToken +Rule : Type -> Type +Rule = Rule Token public export SourceEmptyRule : Type -> Type -SourceEmptyRule = EmptyRule SourceToken +SourceEmptyRule = EmptyRule Token export eoi : SourceEmptyRule () @@ -22,48 +22,48 @@ eoi = do nextIs "Expected end of input" (isEOI . tok) pure () where - isEOI : SourceToken -> Bool + isEOI : Token -> Bool isEOI EndInput = True isEOI _ = False export -constant : SourceRule Constant +constant : Rule Constant constant = terminal "Expected constant" (\x => case tok x of - Literal i => Just (BI i) - StrLit s => case escape s of - Nothing => Nothing - Just s' => Just (Str s') CharLit c => case getCharLit c of Nothing => Nothing Just c' => Just (Ch c') - DoubleLit d => Just (Db d) - NSIdent ["Int"] => Just IntType - NSIdent ["Integer"] => Just IntegerType - NSIdent ["String"] => Just StringType - NSIdent ["Char"] => Just CharType - NSIdent ["Double"] => Just DoubleType + DoubleLit d => Just (Db d) + IntegerLit i => Just (BI i) + StringLit s => case escape s of + Nothing => Nothing + Just s' => Just (Str s') + Ident "Char" => Just CharType + Ident "Double" => Just DoubleType + Ident "Int" => Just IntType + Ident "Integer" => Just IntegerType + Ident "String" => Just StringType _ => Nothing) export -intLit : SourceRule Integer +intLit : Rule Integer intLit = terminal "Expected integer literal" (\x => case tok x of - Literal i => Just i + IntegerLit i => Just i _ => Nothing) export -strLit : SourceRule String +strLit : Rule String strLit = terminal "Expected string literal" (\x => case tok x of - StrLit s => Just s + StringLit s => Just s _ => Nothing) export -recField : SourceRule Name +recField : Rule Name recField = terminal "Expected record field" (\x => case tok x of @@ -71,7 +71,7 @@ recField _ => Nothing) export -symbol : String -> SourceRule () +symbol : String -> Rule () symbol req = terminal ("Expected '" ++ req ++ "'") (\x => case tok x of @@ -80,7 +80,7 @@ symbol req _ => Nothing) export -keyword : String -> SourceRule () +keyword : String -> Rule () keyword req = terminal ("Expected '" ++ req ++ "'") (\x => case tok x of @@ -89,16 +89,16 @@ keyword req _ => Nothing) export -exactIdent : String -> SourceRule () +exactIdent : String -> Rule () exactIdent req = terminal ("Expected " ++ req) (\x => case tok x of - NSIdent [s] => if s == req then Just () - else Nothing + Ident s => if s == req then Just () + else Nothing _ => Nothing) export -pragma : String -> SourceRule () +pragma : String -> Rule () pragma n = terminal ("Expected pragma " ++ n) (\x => case tok x of @@ -109,7 +109,7 @@ pragma n = _ => Nothing) export -operator : SourceRule Name +operator : Rule Name operator = terminal "Expected operator" (\x => case tok x of @@ -119,27 +119,28 @@ operator else Just (UN s) _ => Nothing) -identPart : SourceRule String +identPart : Rule String identPart = terminal "Expected name" (\x => case tok x of - NSIdent [str] => Just str + Ident str => Just str _ => Nothing) export -nsIdent : SourceRule (List String) -nsIdent +namespacedIdent : Rule (List String) +namespacedIdent = terminal "Expected namespaced name" (\x => case tok x of - NSIdent ns => Just ns + DotSepIdent ns => Just ns + Ident i => Just $ [i] _ => Nothing) export -unqualifiedName : SourceRule String +unqualifiedName : Rule String unqualifiedName = identPart export -holeName : SourceRule String +holeName : Rule String holeName = terminal "Expected hole name" (\x => case tok x of @@ -152,17 +153,17 @@ reservedNames "Lazy", "Inf", "Force", "Delay"] export -name : SourceRule Name +name : Rule Name name = opNonNS <|> do - ns <- nsIdent + ns <- namespacedIdent opNS ns <|> nameNS ns where reserved : String -> Bool reserved n = n `elem` reservedNames - nameNS : List String -> Grammar (TokenData SourceToken) False Name + nameNS : List String -> SourceEmptyRule Name nameNS [] = pure $ UN "IMPOSSIBLE" - nameNS [x] = + nameNS [x] = if reserved x then fail $ "can't use reserved name " ++ x else pure $ UN x @@ -171,10 +172,10 @@ name = opNonNS <|> do then fail $ "can't use reserved name " ++ x else pure $ NS xs (UN x) - opNonNS : SourceRule Name + opNonNS : Rule Name opNonNS = symbol "(" *> (operator <|> recField) <* symbol ")" - opNS : List String -> SourceRule Name + opNS : List String -> Rule Name opNS ns = do symbol ".(" n <- (operator <|> recField) @@ -238,7 +239,7 @@ checkValid (AfterPos x) c = if c >= x checkValid EndOfBlock c = fail "End of block" ||| Any token which indicates the end of a statement/block -isTerminator : SourceToken -> Bool +isTerminator : Token -> Bool isTerminator (Symbol ",") = True isTerminator (Symbol "]") = True isTerminator (Symbol ";") = True @@ -318,8 +319,8 @@ terminator valid laststart afterDedent EndOfBlock col = pure EndOfBlock -- Parse an entry in a block -blockEntry : ValidIndent -> (IndentInfo -> SourceRule ty) -> - SourceRule (ty, ValidIndent) +blockEntry : ValidIndent -> (IndentInfo -> Rule ty) -> + Rule (ty, ValidIndent) blockEntry valid rule = do col <- column checkValid valid col @@ -327,7 +328,7 @@ blockEntry valid rule valid' <- terminator valid col pure (p, valid') -blockEntries : ValidIndent -> (IndentInfo -> SourceRule ty) -> +blockEntries : ValidIndent -> (IndentInfo -> Rule ty) -> SourceEmptyRule (List ty) blockEntries valid rule = do eoi; pure [] @@ -337,7 +338,7 @@ blockEntries valid rule <|> pure [] export -block : (IndentInfo -> SourceRule ty) -> SourceEmptyRule (List ty) +block : (IndentInfo -> Rule ty) -> SourceEmptyRule (List ty) block item = do symbol "{" commit @@ -353,7 +354,7 @@ block item ||| by curly braces). `rule` is a function of the actual indentation ||| level. export -blockAfter : Int -> (IndentInfo -> SourceRule ty) -> SourceEmptyRule (List ty) +blockAfter : Int -> (IndentInfo -> Rule ty) -> SourceEmptyRule (List ty) blockAfter mincol item = do symbol "{" commit @@ -366,7 +367,7 @@ blockAfter mincol item else blockEntries (AtPos col) item export -blockWithOptHeaderAfter : Int -> (IndentInfo -> SourceRule hd) -> (IndentInfo -> SourceRule ty) -> SourceEmptyRule (Maybe hd, List ty) +blockWithOptHeaderAfter : Int -> (IndentInfo -> Rule hd) -> (IndentInfo -> Rule ty) -> SourceEmptyRule (Maybe hd, List ty) blockWithOptHeaderAfter {ty} mincol header item = do symbol "{" commit @@ -379,7 +380,7 @@ blockWithOptHeaderAfter {ty} mincol header item ps <- blockEntries (AtPos col) item pure (map fst hidt, ps) where - restOfBlock : Maybe (hd, ValidIndent) -> SourceRule (Maybe hd, List ty) + restOfBlock : Maybe (hd, ValidIndent) -> Rule (Maybe hd, List ty) restOfBlock (Just (h, idt)) = do ps <- blockEntries idt item symbol "}" pure (Just h, ps) @@ -388,7 +389,7 @@ blockWithOptHeaderAfter {ty} mincol header item pure (Nothing, ps) export -nonEmptyBlock : (IndentInfo -> SourceRule ty) -> SourceRule (List ty) +nonEmptyBlock : (IndentInfo -> Rule ty) -> Rule (List ty) nonEmptyBlock item = do symbol "{" commit diff --git a/src/Parser/Source.idr b/src/Parser/Source.idr index 5517a73f3..050177082 100644 --- a/src/Parser/Source.idr +++ b/src/Parser/Source.idr @@ -3,8 +3,6 @@ module Parser.Source import public Parser.Lexer.Source import public Parser.Rule.Source import public Parser.Unlit -import public Text.Lexer -import public Text.Parser import System.File import Utils.Either @@ -13,21 +11,21 @@ import Utils.Either export runParserTo : {e : _} -> - Maybe LiterateStyle -> (TokenData SourceToken -> Bool) -> - String -> Grammar (TokenData SourceToken) e ty -> Either ParseError ty + Maybe LiterateStyle -> (TokenData Token -> Bool) -> + String -> Grammar (TokenData Token) e ty -> Either (ParseError Token) ty runParserTo lit pred str p = do str <- mapError LitFail $ unlit lit str toks <- mapError LexFail $ lexTo pred str - parsed <- mapError mapParseError $ parse p toks + parsed <- mapError toGenericParsingError $ parse p toks Right (fst parsed) export runParser : {e : _} -> - Maybe LiterateStyle -> String -> Grammar (TokenData SourceToken) e ty -> Either ParseError ty + Maybe LiterateStyle -> String -> Grammar (TokenData Token) e ty -> Either (ParseError Token) ty runParser lit = runParserTo lit (const False) -export covering -- readFile might not terminate -parseFile : (fn : String) -> SourceRule ty -> IO (Either ParseError ty) +export covering +parseFile : (fn : String) -> Rule ty -> IO (Either (ParseError Token) ty) parseFile fn p = do Right str <- readFile fn | Left err => pure (Left (FileFail err)) diff --git a/src/Parser/Support.idr b/src/Parser/Support.idr index 2246dbce4..d9201c260 100644 --- a/src/Parser/Support.idr +++ b/src/Parser/Support.idr @@ -1,6 +1,5 @@ module Parser.Support -import public Parser.Lexer.Source import public Text.Lexer import public Text.Parser @@ -13,13 +12,14 @@ import System.File %default total public export -data ParseError = ParseFail String (Maybe (Int, Int)) (List SourceToken) - | LexFail (Int, Int, String) - | FileFail FileError - | LitFail LiterateError +data ParseError tok + = ParseFail String (Maybe (Int, Int)) (List tok) + | LexFail (Int, Int, String) + | FileFail FileError + | LitFail LiterateError export -Show ParseError where +Show tok => Show (ParseError tok) where show (ParseFail err loc toks) = "Parse error: " ++ err ++ " (next tokens: " ++ show (take 10 toks) ++ ")" @@ -31,9 +31,9 @@ Show ParseError where = "Lit error(s) at " ++ show (c, l) ++ " input: " ++ str export -mapParseError : ParseError (TokenData SourceToken) -> ParseError -mapParseError (Error err []) = ParseFail err Nothing [] -mapParseError (Error err (t::ts)) = ParseFail err (Just (line t, col t)) (map tok (t::ts)) +toGenericParsingError : ParsingError (TokenData token) -> ParseError token +toGenericParsingError (Error err []) = ParseFail err Nothing [] +toGenericParsingError (Error err (t::ts)) = ParseFail err (Just (line t, col t)) (map tok (t::ts)) export hex : Char -> Maybe Int diff --git a/src/TTImp/Parser.idr b/src/TTImp/Parser.idr index 70eb13b43..9784ab98f 100644 --- a/src/TTImp/Parser.idr +++ b/src/TTImp/Parser.idr @@ -12,7 +12,7 @@ import Data.List import Data.List.Views import Data.Strings -topDecl : FileName -> IndentInfo -> SourceRule ImpDecl +topDecl : FileName -> IndentInfo -> Rule ImpDecl -- All the clauses get parsed as one-clause definitions. Collect any -- neighbouring clauses with the same function name into one definition. export @@ -26,7 +26,7 @@ collectDefs : List ImpDecl -> List ImpDecl %hide Lexer.Core.(<|>) %hide Prelude.(<|>) -atom : FileName -> SourceRule RawImp +atom : FileName -> Rule RawImp atom fname = do start <- location x <- constant @@ -62,7 +62,7 @@ atom fname end <- location pure (IHole (MkFC fname start end) x) -visOption : SourceRule Visibility +visOption : Rule Visibility visOption = do keyword "public" keyword "export" @@ -77,7 +77,7 @@ visibility = visOption <|> pure Private -totalityOpt : SourceRule TotalReq +totalityOpt : Rule TotalReq totalityOpt = do keyword "partial" pure PartialOK @@ -86,11 +86,11 @@ totalityOpt <|> do keyword "covering" pure CoveringOnly -fnOpt : SourceRule FnOpt +fnOpt : Rule FnOpt fnOpt = do x <- totalityOpt pure $ Totality x -fnDirectOpt : SourceRule FnOpt +fnDirectOpt : Rule FnOpt fnDirectOpt = do pragma "hint" pure (Hint True) @@ -105,7 +105,7 @@ fnDirectOpt <|> do pragma "extern" pure ExternFn -visOpt : SourceRule (Either Visibility FnOpt) +visOpt : Rule (Either Visibility FnOpt) visOpt = do vis <- visOption pure (Left vis) @@ -127,7 +127,7 @@ getRight : Either a b -> Maybe b getRight (Left _) = Nothing getRight (Right v) = Just v -bindSymbol : SourceRule (PiInfo RawImp) +bindSymbol : Rule (PiInfo RawImp) bindSymbol = do symbol "->" pure Explicit @@ -135,7 +135,7 @@ bindSymbol pure AutoImplicit mutual - appExpr : FileName -> IndentInfo -> SourceRule RawImp + appExpr : FileName -> IndentInfo -> Rule RawImp appExpr fname indents = case_ fname indents <|> lazy fname indents @@ -155,7 +155,7 @@ mutual = applyExpImp start end (IImplicitApp (MkFC fname start end) f n imp) args argExpr : FileName -> IndentInfo -> - SourceRule (Either RawImp (Maybe Name, RawImp)) + Rule (Either RawImp (Maybe Name, RawImp)) argExpr fname indents = do continue indents arg <- simpleExpr fname indents @@ -164,7 +164,7 @@ mutual arg <- implicitArg fname indents pure (Right arg) - implicitArg : FileName -> IndentInfo -> SourceRule (Maybe Name, RawImp) + implicitArg : FileName -> IndentInfo -> Rule (Maybe Name, RawImp) implicitArg fname indents = do start <- location symbol "{" @@ -183,7 +183,7 @@ mutual symbol "}" pure (Nothing, tm) - as : FileName -> IndentInfo -> SourceRule RawImp + as : FileName -> IndentInfo -> Rule RawImp as fname indents = do start <- location x <- unqualifiedName @@ -192,7 +192,7 @@ mutual end <- location pure (IAs (MkFC fname start end) UseRight (UN x) pat) - simpleExpr : FileName -> IndentInfo -> SourceRule RawImp + simpleExpr : FileName -> IndentInfo -> Rule RawImp simpleExpr fname indents = as fname indents <|> atom fname @@ -223,7 +223,7 @@ mutual = IPi fc rig p n ty (pibindAll fc p rest scope) bindList : FileName -> FilePos -> IndentInfo -> - SourceRule (List (RigCount, Name, RawImp)) + Rule (List (RigCount, Name, RawImp)) bindList fname start indents = sepBy1 (symbol ",") (do rigc <- multiplicity @@ -238,7 +238,7 @@ mutual pibindListName : FileName -> FilePos -> IndentInfo -> - SourceRule (List (RigCount, Name, RawImp)) + Rule (List (RigCount, Name, RawImp)) pibindListName fname start indents = do rigc <- multiplicity ns <- sepBy1 (symbol ",") unqualifiedName @@ -256,13 +256,13 @@ mutual pure (rig, n, ty)) pibindList : FileName -> FilePos -> IndentInfo -> - SourceRule (List (RigCount, Maybe Name, RawImp)) + Rule (List (RigCount, Maybe Name, RawImp)) pibindList fname start indents = do params <- pibindListName fname start indents pure $ map (\(rig, n, ty) => (rig, Just n, ty)) params - autoImplicitPi : FileName -> IndentInfo -> SourceRule RawImp + autoImplicitPi : FileName -> IndentInfo -> Rule RawImp autoImplicitPi fname indents = do start <- location symbol "{" @@ -275,7 +275,7 @@ mutual end <- location pure (pibindAll (MkFC fname start end) AutoImplicit binders scope) - forall_ : FileName -> IndentInfo -> SourceRule RawImp + forall_ : FileName -> IndentInfo -> Rule RawImp forall_ fname indents = do start <- location keyword "forall" @@ -290,7 +290,7 @@ mutual end <- location pure (pibindAll (MkFC fname start end) Implicit binders scope) - implicitPi : FileName -> IndentInfo -> SourceRule RawImp + implicitPi : FileName -> IndentInfo -> Rule RawImp implicitPi fname indents = do start <- location symbol "{" @@ -301,7 +301,7 @@ mutual end <- location pure (pibindAll (MkFC fname start end) Implicit binders scope) - explicitPi : FileName -> IndentInfo -> SourceRule RawImp + explicitPi : FileName -> IndentInfo -> Rule RawImp explicitPi fname indents = do start <- location symbol "(" @@ -312,7 +312,7 @@ mutual end <- location pure (pibindAll (MkFC fname start end) exp binders scope) - lam : FileName -> IndentInfo -> SourceRule RawImp + lam : FileName -> IndentInfo -> Rule RawImp lam fname indents = do start <- location symbol "\\" @@ -328,7 +328,7 @@ mutual bindAll fc ((rig, n, ty) :: rest) scope = ILam fc rig Explicit (Just n) ty (bindAll fc rest scope) - let_ : FileName -> IndentInfo -> SourceRule RawImp + let_ : FileName -> IndentInfo -> Rule RawImp let_ fname indents = do start <- location keyword "let" @@ -353,7 +353,7 @@ mutual end <- location pure (ILocal (MkFC fname start end) (collectDefs ds) scope) - case_ : FileName -> IndentInfo -> SourceRule RawImp + case_ : FileName -> IndentInfo -> Rule RawImp case_ fname indents = do start <- location keyword "case" @@ -364,14 +364,14 @@ mutual pure (let fc = MkFC fname start end in ICase fc scr (Implicit fc False) alts) - caseAlt : FileName -> IndentInfo -> SourceRule ImpClause + caseAlt : FileName -> IndentInfo -> Rule ImpClause caseAlt fname indents = do start <- location lhs <- appExpr fname indents caseRHS fname indents start lhs caseRHS : FileName -> IndentInfo -> (Int, Int) -> RawImp -> - SourceRule ImpClause + Rule ImpClause caseRHS fname indents start lhs = do symbol "=>" continue indents @@ -384,7 +384,7 @@ mutual end <- location pure (ImpossibleClause (MkFC fname start end) lhs) - record_ : FileName -> IndentInfo -> SourceRule RawImp + record_ : FileName -> IndentInfo -> Rule RawImp record_ fname indents = do start <- location keyword "record" @@ -396,7 +396,7 @@ mutual end <- location pure (IUpdate (MkFC fname start end) fs sc) - field : FileName -> IndentInfo -> SourceRule IFieldUpdate + field : FileName -> IndentInfo -> Rule IFieldUpdate field fname indents = do path <- sepBy1 (symbol "->") unqualifiedName upd <- (do symbol "="; pure ISetField) @@ -405,7 +405,7 @@ mutual val <- appExpr fname indents pure (upd path val) - rewrite_ : FileName -> IndentInfo -> SourceRule RawImp + rewrite_ : FileName -> IndentInfo -> Rule RawImp rewrite_ fname indents = do start <- location keyword "rewrite" @@ -415,7 +415,7 @@ mutual end <- location pure (IRewrite (MkFC fname start end) rule tm) - lazy : FileName -> IndentInfo -> SourceRule RawImp + lazy : FileName -> IndentInfo -> Rule RawImp lazy fname indents = do start <- location exactIdent "Lazy" @@ -439,7 +439,7 @@ mutual pure (IForce (MkFC fname start end) tm) - binder : FileName -> IndentInfo -> SourceRule RawImp + binder : FileName -> IndentInfo -> Rule RawImp binder fname indents = autoImplicitPi fname indents <|> forall_ fname indents @@ -448,7 +448,7 @@ mutual <|> lam fname indents <|> let_ fname indents - typeExpr : FileName -> IndentInfo -> SourceRule RawImp + typeExpr : FileName -> IndentInfo -> Rule RawImp typeExpr fname indents = do start <- location arg <- appExpr fname indents @@ -467,10 +467,10 @@ mutual (mkPi start end a as) export - expr : FileName -> IndentInfo -> SourceRule RawImp + expr : FileName -> IndentInfo -> Rule RawImp expr = typeExpr -tyDecl : FileName -> IndentInfo -> SourceRule ImpTy +tyDecl : FileName -> IndentInfo -> Rule ImpTy tyDecl fname indents = do start <- location n <- name @@ -483,7 +483,7 @@ tyDecl fname indents mutual parseRHS : (withArgs : Nat) -> FileName -> IndentInfo -> (Int, Int) -> RawImp -> - SourceRule (Name, ImpClause) + Rule (Name, ImpClause) parseRHS withArgs fname indents start lhs = do symbol "=" commit @@ -518,7 +518,7 @@ mutual ifThenElse True t e = t ifThenElse False t e = e - clause : Nat -> FileName -> IndentInfo -> SourceRule (Name, ImpClause) + clause : Nat -> FileName -> IndentInfo -> Rule (Name, ImpClause) clause withArgs fname indents = do start <- location lhs <- expr fname indents @@ -531,7 +531,7 @@ mutual applyArgs f [] = f applyArgs f ((fc, a) :: args) = applyArgs (IApp fc f a) args - parseWithArg : SourceRule (FC, RawImp) + parseWithArg : Rule (FC, RawImp) parseWithArg = do symbol "|" start <- location @@ -539,14 +539,14 @@ mutual end <- location pure (MkFC fname start end, tm) -definition : FileName -> IndentInfo -> SourceRule ImpDecl +definition : FileName -> IndentInfo -> Rule ImpDecl definition fname indents = do start <- location nd <- clause 0 fname indents end <- location pure (IDef (MkFC fname start end) (fst nd) [snd nd]) -dataOpt : SourceRule DataOpt +dataOpt : Rule DataOpt dataOpt = do exactIdent "noHints" pure NoHints @@ -556,7 +556,7 @@ dataOpt ns <- some name pure (SearchBy ns) -dataDecl : FileName -> IndentInfo -> SourceRule ImpData +dataDecl : FileName -> IndentInfo -> Rule ImpData dataDecl fname indents = do start <- location keyword "data" @@ -572,7 +572,7 @@ dataDecl fname indents end <- location pure (MkImpData (MkFC fname start end) n ty opts cs) -recordParam : FileName -> IndentInfo -> SourceRule (List (Name, RigCount, PiInfo RawImp, RawImp)) +recordParam : FileName -> IndentInfo -> Rule (List (Name, RigCount, PiInfo RawImp, RawImp)) recordParam fname indents = do symbol "(" start <- location @@ -597,7 +597,7 @@ recordParam fname indents end <- location pure [(n, top, Explicit, Implicit (MkFC fname start end) False)] -fieldDecl : FileName -> IndentInfo -> SourceRule (List IField) +fieldDecl : FileName -> IndentInfo -> Rule (List IField) fieldDecl fname indents = do symbol "{" commit @@ -609,7 +609,7 @@ fieldDecl fname indents atEnd indents pure fs where - fieldBody : PiInfo RawImp -> SourceRule (List IField) + fieldBody : PiInfo RawImp -> Rule (List IField) fieldBody p = do start <- location ns <- sepBy1 (symbol ",") unqualifiedName @@ -619,7 +619,7 @@ fieldDecl fname indents pure (map (\n => MkIField (MkFC fname start end) linear p (UN n) ty) ns) -recordDecl : FileName -> IndentInfo -> SourceRule ImpDecl +recordDecl : FileName -> IndentInfo -> Rule ImpDecl recordDecl fname indents = do start <- location vis <- visibility @@ -638,14 +638,14 @@ recordDecl fname indents IRecord fc Nothing vis (MkImpRecord fc n params dc (concat flds))) -namespaceDecl : SourceRule (List String) +namespaceDecl : Rule (List String) namespaceDecl = do keyword "namespace" commit - ns <- nsIdent + ns <- namespacedIdent pure ns -directive : FileName -> IndentInfo -> SourceRule ImpDecl +directive : FileName -> IndentInfo -> Rule ImpDecl directive fname indents = do pragma "logging" commit @@ -672,7 +672,7 @@ directive fname indents IPragma (\c, nest, env => setRewrite {c} fc eq rw)) -} -- Declared at the top --- topDecl : FileName -> IndentInfo -> SourceRule ImpDecl +-- topDecl : FileName -> IndentInfo -> Rule ImpDecl topDecl fname indents = do start <- location vis <- visibility @@ -720,14 +720,14 @@ collectDefs (d :: ds) -- full programs export -prog : FileName -> SourceRule (List ImpDecl) +prog : FileName -> Rule (List ImpDecl) prog fname = do ds <- nonEmptyBlock (topDecl fname) pure (collectDefs ds) -- TTImp REPL commands export -command : SourceRule ImpREPL +command : Rule ImpREPL command = do symbol ":"; exactIdent "t" tm <- expr "(repl)" init diff --git a/src/Text/Parser/Core.idr b/src/Text/Parser/Core.idr index e30fbd0e8..cb95c3626 100644 --- a/src/Text/Parser/Core.idr +++ b/src/Text/Parser/Core.idr @@ -272,14 +272,14 @@ mutual -- doParse _ _ _ = Failure True True "Help the coverage checker!" [] public export -data ParseError tok = Error String (List tok) +data ParsingError tok = Error String (List tok) ||| Parse a list of tokens according to the given grammar. If successful, ||| returns a pair of the parse result and the unparsed tokens (the remaining ||| input). export parse : {c : Bool} -> (act : Grammar tok c ty) -> (xs : List tok) -> - Either (ParseError tok) (ty, List tok) + Either (ParsingError tok) (ty, List tok) parse act xs = case doParse False act xs of Failure _ _ msg ts => Left (Error msg ts) diff --git a/src/Utils/String.idr b/src/Utils/String.idr index f90f365c8..fc4f6a7e2 100644 --- a/src/Utils/String.idr +++ b/src/Utils/String.idr @@ -2,6 +2,12 @@ module Utils.String %default total +export +dotSep : List String -> String +dotSep [] = "" +dotSep [x] = x +dotSep (x :: xs) = x ++ concat ["." ++ y | y <- xs] + export stripQuotes : (str : String) -> String stripQuotes str = prim__strSubstr 1 (lengthInt - 2) str diff --git a/tests/Main.idr b/tests/Main.idr index c0bf859c7..5c4b7f930 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -53,6 +53,7 @@ idrisTests "interactive001", "interactive002", "interactive003", "interactive004", "interactive005", "interactive006", "interactive007", "interactive008", "interactive009", "interactive010", "interactive011", "interactive012", + "interactive013", -- Literate "literate001", "literate002", "literate003", "literate004", "literate005", "literate006", "literate007", "literate008", diff --git a/tests/idris2/interactive013/Spacing.idr b/tests/idris2/interactive013/Spacing.idr new file mode 100644 index 000000000..52f369bd5 --- /dev/null +++ b/tests/idris2/interactive013/Spacing.idr @@ -0,0 +1,4 @@ +module Spacing + +id : {n : Nat} -> Nat +id { n} = ?a diff --git a/tests/idris2/interactive013/expected b/tests/idris2/interactive013/expected new file mode 100644 index 000000000..3145378c8 --- /dev/null +++ b/tests/idris2/interactive013/expected @@ -0,0 +1,5 @@ +1/1: Building Spacing (Spacing.idr) +Spacing> id { n = 0} = ?a_1 +id { n = (S k)} = ?a_2 +Spacing> +Bye for now! diff --git a/tests/idris2/interactive013/input b/tests/idris2/interactive013/input new file mode 100644 index 000000000..6cc8ff48c --- /dev/null +++ b/tests/idris2/interactive013/input @@ -0,0 +1,2 @@ +:cs 4 6 n +:q \ No newline at end of file diff --git a/tests/idris2/interactive013/run b/tests/idris2/interactive013/run new file mode 100755 index 000000000..abb25f9e4 --- /dev/null +++ b/tests/idris2/interactive013/run @@ -0,0 +1,3 @@ +$1 --no-banner Spacing.idr < input + +rm -rf build