From 43c5075f6e032e00b837982cdf07acbab5b74f3d Mon Sep 17 00:00:00 2001 From: Jan de Muijnck-Hughes Date: Sat, 23 May 2020 19:57:50 +0100 Subject: [PATCH 1/6] Use reST directives to make warnings and TODOs explicit in the documentation. --- docs/source/reference/envvars.rst | 4 +++- docs/source/tutorial/miscellany.rst | 10 ++++++---- docs/source/tutorial/theorems.rst | 6 ++++-- docs/source/tutorial/views.rst | 4 +++- docs/source/typedd/typedd.rst | 4 +++- docs/source/updates/updates.rst | 7 +++++-- 6 files changed, 24 insertions(+), 11 deletions(-) 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/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 905d72f63..bd966c7ae 100644 --- a/docs/source/typedd/typedd.rst +++ b/docs/source/typedd/typedd.rst @@ -453,4 +453,6 @@ In ``ATM.idr``, add: Chapter 15 ---------- -TODO +.. todo:: + + This chapter. diff --git a/docs/source/updates/updates.rst b/docs/source/updates/updates.rst index 1a7d1a4c1..815217a36 100644 --- a/docs/source/updates/updates.rst +++ b/docs/source/updates/updates.rst @@ -428,8 +428,11 @@ used with care. Too many hints can lead to a large search space! Totality and Coverage --------------------- -``%default covering`` is now the default status [Actually still TODO, but -planned soon!] +``%default covering`` is now the default statusk + +.. note:: + + Actually still TODO, but planned soon! Build artefacts --------------- From 3e810b1de73e8c16858849c5996ccb4263508467 Mon Sep 17 00:00:00 2001 From: Jan de Muijnck-Hughes Date: Sat, 23 May 2020 20:03:36 +0100 Subject: [PATCH 2/6] Add venv for rtd docs to .gitignore. --- .gitignore | 1 + 1 file changed, 1 insertion(+) diff --git a/.gitignore b/.gitignore index 53c2314e3..2eedd56ad 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,4 @@ +idris2docs_venv *~ *.ibc *.ttc From 731a4160434bff960ddefc16d2fa89de04057934 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fabi=C3=A1n=20Heredia=20Montiel?= Date: Wed, 20 May 2020 22:25:25 -0500 Subject: [PATCH 3/6] Split Package Specific Lexer/Rules from Lexer/{Common,Source} and Refactor Idris/Package Co-authored-by: Matus Tejiscak --- docs/source/reference/records.rst | 2 +- idris2.ipkg | 3 + idris2api.ipkg | 3 + src/Core/Core.idr | 3 +- src/Idris/IDEMode/Parser.idr | 28 ++-- src/Idris/Package.idr | 77 ++++++----- src/Idris/Parser.idr | 216 +++++++++++++++--------------- src/Idris/ProcessIdr.idr | 4 +- src/Idris/REPL.idr | 2 +- src/Parser/Lexer/Common.idr | 27 +++- src/Parser/Lexer/Package.idr | 65 +++++++++ src/Parser/Lexer/Source.idr | 115 +++++++--------- src/Parser/Package.idr | 24 ++++ src/Parser/Rule/Package.idr | 79 +++++++++++ src/Parser/Rule/Source.idr | 99 +++++++------- src/Parser/Source.idr | 14 +- src/Parser/Support.idr | 18 +-- src/TTImp/Parser.idr | 98 +++++++------- src/Text/Parser/Core.idr | 4 +- src/Utils/String.idr | 6 + 20 files changed, 538 insertions(+), 349 deletions(-) create mode 100644 src/Parser/Lexer/Package.idr create mode 100644 src/Parser/Package.idr create mode 100644 src/Parser/Rule/Package.idr 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/idris2.ipkg b/idris2.ipkg index 54b6c23d0..a30c5b2b1 100644 --- a/idris2.ipkg +++ b/idris2.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/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 8f48dd32c..9c1f2d1c6 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/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/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 745533417..a6c3853a2 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 From 6c2b35d02dd18600119d67b38c0b8049948ec261 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Sun, 24 May 2020 22:13:38 +0100 Subject: [PATCH 4/6] Remove the erased argument check from CaseBuilder This is done elsewhere, and now just gives a meaningless error on overlapping cases in some circumstances, so best removed. (But we do need to find a way to warn on obviously overlapping cases!) --- src/Core/CaseBuilder.idr | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/src/Core/CaseBuilder.idr b/src/Core/CaseBuilder.idr index b1c2e2bd8..873ea9c13 100644 --- a/src/Core/CaseBuilder.idr +++ b/src/Core/CaseBuilder.idr @@ -614,13 +614,10 @@ sameType {ns} fc phase fn env (p :: xs) sameTypeAs : Phase -> NF ns -> List (ArgType ns) -> Core () sameTypeAs _ ty [] = pure () sameTypeAs ph ty (Known r t :: xs) = - if ph == RunTime && isErased r - -- Can't match on erased thing - then throw (CaseCompile fc fn (MatchErased (_ ** (env, mkTerm _ (firstPat p))))) - else do defs <- get Ctxt - if headEq ty !(nf defs env t) phase - then sameTypeAs ph ty xs - else throw (CaseCompile fc fn DifferingTypes) + do defs <- get Ctxt + if headEq ty !(nf defs env t) phase + then sameTypeAs ph ty xs + else throw (CaseCompile fc fn DifferingTypes) sameTypeAs p ty _ = throw (CaseCompile fc fn DifferingTypes) -- Check whether all the initial patterns are the same, or are all a variable. From 9970c66417b029872d8b4c4cf16bff7e7eae088e Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Mon, 25 May 2020 00:16:49 +0100 Subject: [PATCH 5/6] Warn on detecting unreachable patterns I don't know how complete this is, but it certainly detects some of the most obvious cases which are most likely to be bugs. While I'm at it, this is as good a time as any to add a general way of reporting warnings, similar to the way of reporting errors. --- src/Compiler/Common.idr | 8 +- src/Compiler/CompileExpr.idr | 2 +- src/Core/CaseBuilder.idr | 187 +++++++++++++---------- src/Core/CaseTree.idr | 14 +- src/Core/Context.idr | 19 ++- src/Core/Core.idr | 9 ++ src/Core/Coverage.idr | 4 +- src/Core/Hash.idr | 2 +- src/Core/LinearCheck.idr | 7 +- src/Core/Normalise.idr | 2 +- src/Core/TTC.idr | 4 +- src/Core/Unify.idr | 14 +- src/Idris/Error.idr | 15 ++ src/Idris/ModTree.idr | 7 +- src/Idris/REPL.idr | 2 +- src/Idris/REPLCommon.idr | 39 +++++ src/TTImp/Elab/Delayed.idr | 2 +- src/TTImp/ProcessDef.idr | 15 +- tests/Main.idr | 1 + tests/idris2/coverage009/expected | 3 + tests/idris2/coverage009/run | 3 + tests/idris2/coverage009/unreachable.idr | 5 + 22 files changed, 251 insertions(+), 113 deletions(-) create mode 100644 tests/idris2/coverage009/expected create mode 100755 tests/idris2/coverage009/run create mode 100644 tests/idris2/coverage009/unreachable.idr diff --git a/src/Compiler/Common.idr b/src/Compiler/Common.idr index 839f66227..b80abb19b 100644 --- a/src/Compiler/Common.idr +++ b/src/Compiler/Common.idr @@ -145,6 +145,11 @@ getAllDesc (n@(Resolved i) :: rest) arr defs getAllDesc (n :: rest) arr defs = getAllDesc rest arr defs +warnIfHole : Name -> NamedDef -> Core () +warnIfHole n (MkNmError _) + = coreLift $ putStrLn $ "Warning: compiling hole " ++ show n +warnIfHole n _ = pure () + getNamedDef : {auto c : Ref Ctxt Defs} -> Name -> Core (Maybe (Name, FC, NamedDef)) getNamedDef n @@ -153,7 +158,8 @@ getNamedDef n Nothing => pure Nothing Just def => case namedcompexpr def of Nothing => pure Nothing - Just d => pure (Just (n, location def, d)) + Just d => do warnIfHole n d + pure (Just (n, location def, d)) replaceEntry : {auto c : Ref Ctxt Defs} -> (Int, Maybe Binary) -> Core () diff --git a/src/Compiler/CompileExpr.idr b/src/Compiler/CompileExpr.idr index 7c843914b..66e99bb03 100644 --- a/src/Compiler/CompileExpr.idr +++ b/src/Compiler/CompileExpr.idr @@ -438,7 +438,7 @@ mutual = toCExpTree n sc toCExpTree' n (Case _ x scTy []) = pure $ CCrash (getLoc scTy) $ "Missing case tree in " ++ show n - toCExpTree' n (STerm tm) = toCExp n tm + toCExpTree' n (STerm _ tm) = toCExp n tm toCExpTree' n (Unmatched msg) = pure $ CCrash emptyFC msg toCExpTree' n Impossible diff --git a/src/Core/CaseBuilder.idr b/src/Core/CaseBuilder.idr index 873ea9c13..398886e21 100644 --- a/src/Core/CaseBuilder.idr +++ b/src/Core/CaseBuilder.idr @@ -188,22 +188,22 @@ take (x :: xs) (p :: ps) = p :: take xs ps data PatClause : (vars : List Name) -> (todo : List Name) -> Type where MkPatClause : List Name -> -- names matched so far (from original lhs) NamedPats vars todo -> - (rhs : Term vars) -> PatClause vars todo + Int -> (rhs : Term vars) -> PatClause vars todo getNPs : PatClause vars todo -> NamedPats vars todo -getNPs (MkPatClause _ lhs rhs) = lhs +getNPs (MkPatClause _ lhs pid rhs) = lhs {vars : _} -> {todo : _} -> Show (PatClause vars todo) where - show (MkPatClause _ ps rhs) + show (MkPatClause _ ps pid rhs) = show ps ++ " => " ++ show rhs substInClause : {a, vars, todo : _} -> {auto c : Ref Ctxt Defs} -> FC -> PatClause vars (a :: todo) -> Core (PatClause vars (a :: todo)) -substInClause {vars} {a} fc (MkPatClause pvars (MkInfo pat pprf fty :: pats) rhs) +substInClause {vars} {a} fc (MkPatClause pvars (MkInfo pat pprf fty :: pats) pid rhs) = do pats' <- substInPats fc a (mkTerm vars pat) pats - pure (MkPatClause pvars (MkInfo pat pprf fty :: pats') rhs) + pure (MkPatClause pvars (MkInfo pat pprf fty :: pats') pid rhs) data Partitions : List (PatClause vars todo) -> Type where ConClauses : {todo, vars, ps : _} -> @@ -244,7 +244,7 @@ clauseType : Phase -> PatClause vars (a :: as) -> ClauseType -- and don't see later, treat it as a variable -- Or, if we're compiling for runtime we won't be able to split on it, so -- also treat it as a variable -clauseType phase (MkPatClause pvars (MkInfo arg _ ty :: rest) rhs) +clauseType phase (MkPatClause pvars (MkInfo arg _ ty :: rest) pid rhs) = getClauseType phase arg ty where -- used to get the remaining clause types @@ -324,25 +324,25 @@ data Group : List Name -> -- variables in scope data GroupMatch : ConType -> List Pat -> Group vars todo -> Type where ConMatch : LengthMatch ps newargs -> GroupMatch (CName n tag) ps - (ConGroup {newargs} n tag (MkPatClause pvs pats rhs :: rest)) + (ConGroup {newargs} n tag (MkPatClause pvs pats pid rhs :: rest)) DelayMatch : GroupMatch CDelay [] - (DelayGroup {tyarg} {valarg} (MkPatClause pvs pats rhs :: rest)) + (DelayGroup {tyarg} {valarg} (MkPatClause pvs pats pid rhs :: rest)) ConstMatch : GroupMatch (CConst c) [] - (ConstGroup c (MkPatClause pvs pats rhs :: rest)) + (ConstGroup c (MkPatClause pvs pats pid rhs :: rest)) NoMatch : GroupMatch ct ps g checkGroupMatch : (c : ConType) -> (ps : List Pat) -> (g : Group vars todo) -> GroupMatch c ps g -checkGroupMatch (CName x tag) ps (ConGroup {newargs} x' tag' (MkPatClause pvs pats rhs :: rest)) +checkGroupMatch (CName x tag) ps (ConGroup {newargs} x' tag' (MkPatClause pvs pats pid rhs :: rest)) = case checkLengthMatch ps newargs of Nothing => NoMatch Just prf => case (nameEq x x', decEq tag tag') of (Just Refl, Yes Refl) => ConMatch prf _ => NoMatch checkGroupMatch (CName x tag) ps _ = NoMatch -checkGroupMatch CDelay [] (DelayGroup (MkPatClause pvs pats rhs :: rest)) +checkGroupMatch CDelay [] (DelayGroup (MkPatClause pvs pats pid rhs :: rest)) = DelayMatch -checkGroupMatch (CConst c) [] (ConstGroup c' (MkPatClause pvs pats rhs :: rest)) +checkGroupMatch (CConst c) [] (ConstGroup c' (MkPatClause pvs pats pid rhs :: rest)) = case constantEq c c' of Nothing => NoMatch Just Refl => ConstMatch @@ -434,14 +434,14 @@ groupCons fc fn pvars cs addConG : {vars', todo' : _} -> Name -> (tag : Int) -> List Pat -> NamedPats vars' todo' -> - (rhs : Term vars') -> + Int -> (rhs : Term vars') -> (acc : List (Group vars' todo')) -> Core (List (Group vars' todo')) -- Group all the clauses that begin with the same constructor, and -- add new pattern arguments for each of that constructor's arguments. -- The type of 'ConGroup' ensures that we refer to the arguments by -- the same name in each of the clauses - addConG {vars'} {todo'} n tag pargs pats rhs [] + addConG {vars'} {todo'} n tag pargs pats pid rhs [] = do cty <- the (Core (NF vars')) $ if n == UN "->" then pure $ NBind fc (MN "_" 0) (Pi top Explicit (NType fc)) $ (\d, a => pure $ NBind fc (MN "_" 1) (Pi top Explicit (NErased fc False)) @@ -458,11 +458,11 @@ groupCons fc fn pvars cs let clause = MkPatClause {todo = patnames ++ todo'} pvars (newargs ++ pats') - (weakenNs patnames rhs) + pid (weakenNs patnames rhs) pure [ConGroup n tag [clause]] - addConG {vars'} {todo'} n tag pargs pats rhs (g :: gs) with (checkGroupMatch (CName n tag) pargs g) - addConG {vars'} {todo'} n tag pargs pats rhs - ((ConGroup {newargs} n tag ((MkPatClause pvars ps tm) :: rest)) :: gs) + addConG {vars'} {todo'} n tag pargs pats pid rhs (g :: gs) with (checkGroupMatch (CName n tag) pargs g) + addConG {vars'} {todo'} n tag pargs pats pid rhs + ((ConGroup {newargs} n tag ((MkPatClause pvars ps tid tm) :: rest)) :: gs) | (ConMatch {newargs} lprf) = do let newps = newPats pargs lprf ps let pats' = updatePatNames (updateNames (zip newargs pargs)) @@ -470,13 +470,14 @@ groupCons fc fn pvars cs let newclause : PatClause (newargs ++ vars') (newargs ++ todo') = MkPatClause pvars (newps ++ pats') + pid (weakenNs newargs rhs) -- put the new clause at the end of the group, since we -- match the clauses top to bottom. - pure ((ConGroup n tag (MkPatClause pvars ps tm :: rest ++ [newclause])) + pure ((ConGroup n tag (MkPatClause pvars ps tid tm :: rest ++ [newclause])) :: gs) - addConG n tag pargs pats rhs (g :: gs) | NoMatch - = do gs' <- addConG n tag pargs pats rhs gs + addConG n tag pargs pats pid rhs (g :: gs) | NoMatch + = do gs' <- addConG n tag pargs pats pid rhs gs pure (g :: gs') -- This rather ugly special case is to deal with laziness, where Delay @@ -485,10 +486,10 @@ groupCons fc fn pvars cs -- and compiler) addDelayG : {vars', todo' : _} -> Pat -> Pat -> NamedPats vars' todo' -> - (rhs : Term vars') -> + Int -> (rhs : Term vars') -> (acc : List (Group vars' todo')) -> Core (List (Group vars' todo')) - addDelayG {vars'} {todo'} pty parg pats rhs [] + addDelayG {vars'} {todo'} pty parg pats pid rhs [] = do let dty = NBind fc (MN "a" 0) (Pi erased Explicit (NType fc)) $ (\d, a => do a' <- evalClosure d a @@ -502,11 +503,11 @@ groupCons fc fn pvars cs (weakenNs [tyname, argname] pats) let clause = MkPatClause {todo = tyname :: argname :: todo'} pvars (newargs ++ pats') - (weakenNs [tyname, argname] rhs) + pid (weakenNs [tyname, argname] rhs) pure [DelayGroup [clause]] - addDelayG {vars'} {todo'} pty parg pats rhs (g :: gs) with (checkGroupMatch CDelay [] g) - addDelayG {vars'} {todo'} pty parg pats rhs - ((DelayGroup {tyarg} {valarg} ((MkPatClause pvars ps tm) :: rest)) :: gs) + addDelayG {vars'} {todo'} pty parg pats pid rhs (g :: gs) with (checkGroupMatch CDelay [] g) + addDelayG {vars'} {todo'} pty parg pats pid rhs + ((DelayGroup {tyarg} {valarg} ((MkPatClause pvars ps tid tm) :: rest)) :: gs) | (DelayMatch {tyarg} {valarg}) = do let newps = newPats [pty, parg] (ConsMatch (ConsMatch NilMatch)) ps let pats' = updatePatNames (updateNames [(tyarg, pty), @@ -514,56 +515,56 @@ groupCons fc fn pvars cs (weakenNs [tyarg, valarg] pats) let newclause : PatClause (tyarg :: valarg :: vars') (tyarg :: valarg :: todo') - = MkPatClause pvars (newps ++ pats') + = MkPatClause pvars (newps ++ pats') pid (weakenNs [tyarg, valarg] rhs) - pure ((DelayGroup (MkPatClause pvars ps tm :: rest ++ [newclause])) + pure ((DelayGroup (MkPatClause pvars ps tid tm :: rest ++ [newclause])) :: gs) - addDelayG pty parg pats rhs (g :: gs) | NoMatch - = do gs' <- addDelayG pty parg pats rhs gs + addDelayG pty parg pats pid rhs (g :: gs) | NoMatch + = do gs' <- addDelayG pty parg pats pid rhs gs pure (g :: gs') addConstG : {vars', todo' : _} -> Constant -> NamedPats vars' todo' -> - (rhs : Term vars') -> + Int -> (rhs : Term vars') -> (acc : List (Group vars' todo')) -> Core (List (Group vars' todo')) - addConstG c pats rhs [] - = pure [ConstGroup c [MkPatClause pvars pats rhs]] - addConstG {todo'} {vars'} c pats rhs (g :: gs) with (checkGroupMatch (CConst c) [] g) - addConstG {todo'} {vars'} c pats rhs - ((ConstGroup c ((MkPatClause pvars ps tm) :: rest)) :: gs) | ConstMatch + addConstG c pats pid rhs [] + = pure [ConstGroup c [MkPatClause pvars pats pid rhs]] + addConstG {todo'} {vars'} c pats pid rhs (g :: gs) with (checkGroupMatch (CConst c) [] g) + addConstG {todo'} {vars'} c pats pid rhs + ((ConstGroup c ((MkPatClause pvars ps tid tm) :: rest)) :: gs) | ConstMatch = let newclause : PatClause vars' todo' - = MkPatClause pvars pats rhs in + = MkPatClause pvars pats pid rhs in pure ((ConstGroup c - (MkPatClause pvars ps tm :: rest ++ [newclause])) :: gs) - addConstG c pats rhs (g :: gs) | NoMatch - = do gs' <- addConstG c pats rhs gs + (MkPatClause pvars ps tid tm :: rest ++ [newclause])) :: gs) + addConstG c pats pid rhs (g :: gs) | NoMatch + = do gs' <- addConstG c pats pid rhs gs pure (g :: gs') addGroup : {vars, todo, idx : _} -> Pat -> (0 p : IsVar name idx vars) -> - NamedPats vars todo -> Term vars -> + NamedPats vars todo -> Int -> Term vars -> List (Group vars todo) -> Core (List (Group vars todo)) -- In 'As' replace the name on the RHS with a reference to the -- variable we're doing the case split on - addGroup (PAs fc n p) pprf pats rhs acc - = addGroup p pprf pats (substName n (Local fc (Just True) _ pprf) rhs) acc - addGroup (PCon cfc n t a pargs) pprf pats rhs acc + addGroup (PAs fc n p) pprf pats pid rhs acc + = addGroup p pprf pats pid (substName n (Local fc (Just True) _ pprf) rhs) acc + addGroup (PCon cfc n t a pargs) pprf pats pid rhs acc = if a == length pargs - then addConG n t pargs pats rhs acc + then addConG n t pargs pats pid rhs acc else throw (CaseCompile cfc fn (NotFullyApplied n)) - addGroup (PTyCon _ n a pargs) pprf pats rhs acc - = addConG n 0 pargs pats rhs acc - addGroup (PArrow _ _ s t) pprf pats rhs acc - = addConG (UN "->") 0 [s, t] pats rhs acc + addGroup (PTyCon _ n a pargs) pprf pats pid rhs acc + = addConG n 0 pargs pats pid rhs acc + addGroup (PArrow _ _ s t) pprf pats pid rhs acc + = addConG (UN "->") 0 [s, t] pats pid rhs acc -- Go inside the delay; we'll flag the case as needing to force its -- scrutinee (need to check in 'caseGroups below) - addGroup (PDelay _ _ pty parg) pprf pats rhs acc - = addDelayG pty parg pats rhs acc - addGroup (PConst _ c) pprf pats rhs acc - = addConstG c pats rhs acc - addGroup _ pprf pats rhs acc = pure acc -- Can't happen, not a constructor + addGroup (PDelay _ _ pty parg) pprf pats pid rhs acc + = addDelayG pty parg pats pid rhs acc + addGroup (PConst _ c) pprf pats pid rhs acc + = addConstG c pats pid rhs acc + addGroup _ pprf pats pid rhs acc = pure acc -- Can't happen, not a constructor -- -- FIXME: Is this possible to rule out with a type? Probably. gc : {a, vars, todo : _} -> @@ -571,8 +572,8 @@ groupCons fc fn pvars cs List (PatClause vars (a :: todo)) -> Core (List (Group vars todo)) gc acc [] = pure acc - gc {a} acc ((MkPatClause pvars (MkInfo pat pprf fty :: pats) rhs) :: cs) - = do acc' <- addGroup pat pprf pats rhs acc + gc {a} acc ((MkPatClause pvars (MkInfo pat pprf fty :: pats) pid rhs) :: cs) + = do acc' <- addGroup pat pprf pats pid rhs acc gc acc' cs getFirstPat : NamedPats ns (p :: ps) -> Pat @@ -728,7 +729,8 @@ moveFirst el nps = getPat el nps :: dropPat el nps shuffleVars : {idx : Nat} -> (0 el : IsVar name idx todo) -> PatClause vars todo -> PatClause vars (name :: dropVar todo el) -shuffleVars el (MkPatClause pvars lhs rhs) = MkPatClause pvars (moveFirst el lhs) rhs +shuffleVars el (MkPatClause pvars lhs pid rhs) + = MkPatClause pvars (moveFirst el lhs) pid rhs mutual {- 'PatClause' contains a list of patterns still to process (that's the @@ -756,10 +758,10 @@ mutual match {todo = []} fc fn phase [] err = maybe (pure (Unmatched "No patterns")) pure err - match {todo = []} fc fn phase ((MkPatClause pvars [] (Erased _ True)) :: _) err + match {todo = []} fc fn phase ((MkPatClause pvars [] pid (Erased _ True)) :: _) err = pure Impossible - match {todo = []} fc fn phase ((MkPatClause pvars [] rhs) :: _) err - = pure $ STerm rhs + match {todo = []} fc fn phase ((MkPatClause pvars [] pid rhs) :: _) err + = pure $ STerm pid rhs caseGroups : {pvar, vars, todo : _} -> {auto i : Ref PName Int} -> @@ -801,7 +803,7 @@ mutual -- the same variable (pprf) for the first argument. If not, the result -- will be a broken case tree... so we should find a way to express this -- in the type if we can. - conRule {a} fc fn phase cs@(MkPatClause pvars (MkInfo pat pprf fty :: pats) rhs :: rest) err + conRule {a} fc fn phase cs@(MkPatClause pvars (MkInfo pat pprf fty :: pats) pid rhs :: rest) err = do refinedcs <- traverse (substInClause fc) cs groups <- groupCons fc fn pvars refinedcs ty <- case fty of @@ -822,21 +824,21 @@ mutual where updateVar : PatClause vars (a :: todo) -> Core (PatClause vars todo) -- replace the name with the relevant variable on the rhs - updateVar (MkPatClause pvars (MkInfo (PLoc pfc n) prf fty :: pats) rhs) + updateVar (MkPatClause pvars (MkInfo (PLoc pfc n) prf fty :: pats) pid rhs) = pure $ MkPatClause (n :: pvars) !(substInPats fc a (Local pfc (Just False) _ prf) pats) - (substName n (Local pfc (Just False) _ prf) rhs) + pid (substName n (Local pfc (Just False) _ prf) rhs) -- If it's an as pattern, replace the name with the relevant variable on -- the rhs then continue with the inner pattern - updateVar (MkPatClause pvars (MkInfo (PAs pfc n pat) prf fty :: pats) rhs) + updateVar (MkPatClause pvars (MkInfo (PAs pfc n pat) prf fty :: pats) pid rhs) = do pats' <- substInPats fc a (mkTerm _ pat) pats let rhs' = substName n (Local pfc (Just True) _ prf) rhs - updateVar (MkPatClause pvars (MkInfo pat prf fty :: pats') rhs') + updateVar (MkPatClause pvars (MkInfo pat prf fty :: pats') pid rhs') -- match anything, name won't appear in rhs but need to update -- LHS pattern types based on what we've learned - updateVar (MkPatClause pvars (MkInfo pat prf fty :: pats) rhs) + updateVar (MkPatClause pvars (MkInfo pat prf fty :: pats) pid rhs) = pure $ MkPatClause pvars - !(substInPats fc a (mkTerm vars pat) pats) rhs + !(substInPats fc a (mkTerm vars pat) pats) pid rhs mixture : {a, vars, todo : _} -> {auto i : Ref PName Int} -> @@ -857,17 +859,18 @@ mutual mkPatClause : {auto c : Ref Ctxt Defs} -> FC -> Name -> - (args : List Name) -> ClosedTerm -> (List Pat, ClosedTerm) -> + (args : List Name) -> ClosedTerm -> + Int -> (List Pat, ClosedTerm) -> Core (PatClause args args) -mkPatClause fc fn args ty (ps, rhs) +mkPatClause fc fn args ty pid (ps, rhs) = maybe (throw (CaseCompile fc fn DifferingArgNumbers)) (\eq => do defs <- get Ctxt nty <- nf defs [] ty ns <- mkNames args ps eq (Just nty) - pure (MkPatClause [] ns - (rewrite sym (appendNilRightNeutral args) in - (weakenNs args rhs)))) + pure (MkPatClause [] ns pid + (rewrite sym (appendNilRightNeutral args) in + (weakenNs args rhs)))) (checkLengthMatch args ps) where mkNames : (vars : List Name) -> (ps : List Pat) -> @@ -903,7 +906,7 @@ patCompile fc fn phase ty [] def def patCompile fc fn phase ty (p :: ps) def = do let ns = getNames 0 (fst p) - pats <- traverse (mkPatClause fc fn ns ty) (p :: ps) + pats <- mkPatClausesFrom 0 ns (p :: ps) log 5 $ "Pattern clauses " ++ show pats i <- newRef PName (the Int 0) cases <- match fc fn phase pats @@ -911,6 +914,15 @@ patCompile fc fn phase ty (p :: ps) def map (TT.weakenNs ns) def) pure (_ ** cases) where + mkPatClausesFrom : Int -> (args : List Name) -> + List (List Pat, ClosedTerm) -> + Core (List (PatClause args args)) + mkPatClausesFrom i ns [] = pure [] + mkPatClausesFrom i ns (p :: ps) + = do p' <- mkPatClause fc fn ns ty i p + ps' <- mkPatClausesFrom (i + 1) ns ps + pure (p' :: ps') + getNames : Int -> List Pat -> List Name getNames i [] = [] getNames i (x :: xs) = MN "arg" i :: getNames (i + 1) xs @@ -947,16 +959,28 @@ simpleCase fc phase fn ty def clauses defs <- get Ctxt patCompile fc fn phase ty ps def +findReached : CaseTree ns -> List Int +findReached (Case _ _ _ alts) = concatMap findRAlts alts + where + findRAlts : CaseAlt ns' -> List Int + findRAlts (ConCase _ _ _ t) = findReached t + findRAlts (DelayCase _ _ t) = findReached t + findRAlts (ConstCase _ t) = findReached t + findRAlts (DefaultCase t) = findReached t +findReached (STerm i _) = [i] +findReached _ = [] + +-- Returns the case tree, and a list of the clauses that aren't reachable export getPMDef : {auto c : Ref Ctxt Defs} -> FC -> Phase -> Name -> ClosedTerm -> List Clause -> - Core (args ** CaseTree args) + Core (args ** (CaseTree args, List Clause)) -- If there's no clauses, make a definition with the right number of arguments -- for the type, which we can use in coverage checking to ensure that one of -- the arguments has an empty type getPMDef fc phase fn ty [] = do defs <- get Ctxt - pure (!(getArgs 0 !(nf defs [] ty)) ** Unmatched "No clauses") + pure (!(getArgs 0 !(nf defs [] ty)) ** (Unmatched "No clauses", [])) where getArgs : Int -> NF [] -> Core (List Name) getArgs i (NBind fc x (Pi _ _ _) sc) @@ -967,8 +991,17 @@ getPMDef fc phase fn ty [] getPMDef fc phase fn ty clauses = do defs <- get Ctxt let cs = map (toClosed defs) (labelPat 0 clauses) - simpleCase fc phase fn ty Nothing cs + (_ ** t) <- simpleCase fc phase fn ty Nothing cs + let reached = findReached t + pure (_ ** (t, getUnreachable 0 reached clauses)) where + getUnreachable : Int -> List Int -> List Clause -> List Clause + getUnreachable i is [] = [] + getUnreachable i is (c :: cs) + = if i `elem` is + then getUnreachable (i + 1) is cs + else c :: getUnreachable (i + 1) is cs + labelPat : Int -> List a -> List (String, a) labelPat i [] = [] labelPat i (x :: xs) = ("pat" ++ show i ++ ":", x) :: labelPat (i + 1) xs diff --git a/src/Core/CaseTree.idr b/src/Core/CaseTree.idr index d874c12af..6fed505d4 100644 --- a/src/Core/CaseTree.idr +++ b/src/Core/CaseTree.idr @@ -20,7 +20,9 @@ mutual (scTy : Term vars) -> List (CaseAlt vars) -> CaseTree vars ||| RHS: no need for further inspection - STerm : Term vars -> CaseTree vars + ||| The Int is a clause id that allows us to see which of the + ||| initial clauses are reached in the tree + STerm : Int -> Term vars -> CaseTree vars ||| error from a partial match Unmatched : (msg : String) -> CaseTree vars ||| Absurd context @@ -60,7 +62,7 @@ mutual show (Case {name} idx prf ty alts) = "case " ++ show name ++ "[" ++ show idx ++ "] : " ++ show ty ++ " of { " ++ showSep " | " (assert_total (map show alts)) ++ " }" - show (STerm tm) = show tm + show (STerm i tm) = "[" ++ show i ++ "] " ++ show tm show (Unmatched msg) = "Error: " ++ show msg show Impossible = "Impossible" @@ -83,7 +85,7 @@ mutual = i == i && length alts == length alts && allTrue (zipWith eqAlt alts alts') - eqTree (STerm t) (STerm t') = eqTerm t t' + eqTree (STerm _ t) (STerm _ t') = eqTerm t t' eqTree (Unmatched _) (Unmatched _) = True eqTree Impossible Impossible = True eqTree _ _ = False @@ -118,7 +120,7 @@ mutual = let MkNVar prf' = insertNVarNames {outer} {inner} {ns} _ prf in Case _ prf' (insertNames {outer} ns scTy) (map (insertCaseAltNames {outer} {inner} ns) alts) - insertCaseNames {outer} ns (STerm x) = STerm (insertNames {outer} ns x) + insertCaseNames {outer} ns (STerm i x) = STerm i (insertNames {outer} ns x) insertCaseNames ns (Unmatched msg) = Unmatched msg insertCaseNames ns Impossible = Impossible @@ -146,7 +148,7 @@ thinTree : {outer, inner : _} -> thinTree n (Case idx prf scTy alts) = let MkNVar prf' = insertNVar {n} _ prf in Case _ prf' (thin n scTy) (map (insertCaseAltNames [n]) alts) -thinTree n (STerm tm) = STerm (thin n tm) +thinTree n (STerm i tm) = STerm i (thin n tm) thinTree n (Unmatched msg) = Unmatched msg thinTree n Impossible = Impossible @@ -172,7 +174,7 @@ getNames add ns sc = getSet ns sc getSet : NameMap Bool -> CaseTree vs -> NameMap Bool getSet ns (Case _ x ty xs) = getAltSets ns xs - getSet ns (STerm tm) = add ns tm + getSet ns (STerm i tm) = add ns tm getSet ns (Unmatched msg) = ns getSet ns Impossible = ns diff --git a/src/Core/Context.idr b/src/Core/Context.idr index 7fff6be8b..2bdd27aff 100644 --- a/src/Core/Context.idr +++ b/src/Core/Context.idr @@ -617,14 +617,14 @@ mutual HasNames (CaseTree vars) where full gam (Case i v ty alts) = pure $ Case i v !(full gam ty) !(traverse (full gam) alts) - full gam (STerm tm) - = pure $ STerm !(full gam tm) + full gam (STerm i tm) + = pure $ STerm i !(full gam tm) full gam t = pure t resolved gam (Case i v ty alts) = pure $ Case i v !(resolved gam ty) !(traverse (resolved gam) alts) - resolved gam (STerm tm) - = pure $ STerm !(resolved gam tm) + resolved gam (STerm i tm) + = pure $ STerm i !(resolved gam tm) resolved gam t = pure t export @@ -859,6 +859,8 @@ record Defs where -- again timings : StringMap (Bool, Integer) -- ^ record of timings from logTimeRecord + warnings : List Warning + -- ^ as yet unreported warnings -- Label for context references export @@ -876,7 +878,7 @@ initDefs = do gam <- initCtxt pure (MkDefs gam [] ["Main"] [] defaults empty 100 empty empty empty [] [] empty [] - empty 5381 [] [] [] [] [] empty empty empty empty) + empty 5381 [] [] [] [] [] empty empty empty empty []) -- Reset the context, except for the options export @@ -2178,6 +2180,13 @@ setSession sopts = do defs <- get Ctxt put Ctxt (record { options->session = sopts } defs) +export +recordWarning : {auto c : Ref Ctxt Defs} -> + Warning -> Core () +recordWarning w + = do defs <- get Ctxt + put Ctxt (record { warnings $= (w ::) } defs) + -- Log message with a term, translating back to human readable names first export logTerm : {vars : _} -> diff --git a/src/Core/Core.idr b/src/Core/Core.idr index 8f48dd32c..dc6f4c6b8 100644 --- a/src/Core/Core.idr +++ b/src/Core/Core.idr @@ -130,6 +130,11 @@ data Error : Type where InLHS : FC -> Name -> Error -> Error InRHS : FC -> Name -> Error -> Error +public export +data Warning : Type where + UnreachableClause : {vars : _} -> + FC -> Env Term vars -> Term vars -> Warning + export Show TTCErrorMsg where show (Format file ver exp) = @@ -361,6 +366,10 @@ getErrorLoc (InCon _ _ err) = getErrorLoc err getErrorLoc (InLHS _ _ err) = getErrorLoc err getErrorLoc (InRHS _ _ err) = getErrorLoc err +export +getWarningLoc : Warning -> Maybe FC +getWarningLoc (UnreachableClause fc _ _) = Just fc + -- Core is a wrapper around IO that is specialised for efficiency. export record Core t where diff --git a/src/Core/Coverage.idr b/src/Core/Coverage.idr index fb672af20..de90bf2fb 100644 --- a/src/Core/Coverage.idr +++ b/src/Core/Coverage.idr @@ -168,7 +168,7 @@ emptyRHS fc (Case idx el sc alts) = Case idx el sc (map emptyRHSalt alts) emptyRHSalt (DelayCase c arg sc) = DelayCase c arg (emptyRHS fc sc) emptyRHSalt (ConstCase c sc) = ConstCase c (emptyRHS fc sc) emptyRHSalt (DefaultCase sc) = DefaultCase (emptyRHS fc sc) -emptyRHS fc (STerm s) = STerm (Erased fc False) +emptyRHS fc (STerm i s) = STerm i (Erased fc False) emptyRHS fc sc = sc mkAlt : {vars : _} -> @@ -357,7 +357,7 @@ buildArgs fc defs known not ps cs@(Case {name = var} idx el ty altsIn) buildArgsAlt not' (c :: cs) = pure $ !(buildArgAlt not' c) ++ !(buildArgsAlt not' cs) -buildArgs fc defs known not ps (STerm vs) +buildArgs fc defs known not ps (STerm _ vs) = pure [] -- matched, so return nothing buildArgs fc defs known not ps (Unmatched msg) = pure [ps] -- unmatched, so return it diff --git a/src/Core/Hash.idr b/src/Core/Hash.idr index 64b4d231c..2bdd97d17 100644 --- a/src/Core/Hash.idr +++ b/src/Core/Hash.idr @@ -152,7 +152,7 @@ mutual Hashable (CaseTree vars) where hashWithSalt h (Case idx x scTy xs) = h `hashWithSalt` 0 `hashWithSalt` idx `hashWithSalt` xs - hashWithSalt h (STerm x) + hashWithSalt h (STerm _ x) = h `hashWithSalt` 1 `hashWithSalt` x hashWithSalt h (Unmatched msg) = h `hashWithSalt` 2 diff --git a/src/Core/LinearCheck.idr b/src/Core/LinearCheck.idr index 70fa73e43..331e6ff80 100644 --- a/src/Core/LinearCheck.idr +++ b/src/Core/LinearCheck.idr @@ -222,8 +222,9 @@ mutual rig logC 10 $ do def <- the (Core String) $ case definition gdef of - PMDef _ _ (STerm tm) _ _ => do tm' <- toFullNames tm - pure (show tm') + PMDef _ _ (STerm _ tm) _ _ => + do tm' <- toFullNames tm + pure (show tm') _ => pure "" pure (show rig ++ ": " ++ show n ++ " " ++ show fc ++ "\n" ++ show def) @@ -614,7 +615,7 @@ mutual RigCount -> (erase : Bool) -> Env Term vars -> Name -> Int -> Def -> List (Term vars) -> Core (Term vars, Glued vars, Usage vars) - expandMeta rig erase env n idx (PMDef _ [] (STerm fn) _ _) args + expandMeta rig erase env n idx (PMDef _ [] (STerm _ fn) _ _) args = do tm <- substMeta (embed fn) args [] lcheck rig erase env tm where diff --git a/src/Core/Normalise.idr b/src/Core/Normalise.idr index 8d1db399b..56efbd927 100644 --- a/src/Core/Normalise.idr +++ b/src/Core/Normalise.idr @@ -326,7 +326,7 @@ parameters (defs : Defs, topopts : EvalOpts) = do xval <- evalLocal env fc Nothing idx (varExtend x) [] loc let loc' = updateLocal idx (varExtend x) loc xval findAlt env loc' opts fc stk xval alts def - evalTree env loc opts fc stk (STerm tm) def + evalTree env loc opts fc stk (STerm _ tm) def = case fuel opts of Nothing => evalWithOpts defs opts env loc (embed tm) stk Just Z => def diff --git a/src/Core/TTC.idr b/src/Core/TTC.idr index f19f06a67..3d6aa8041 100644 --- a/src/Core/TTC.idr +++ b/src/Core/TTC.idr @@ -343,7 +343,7 @@ mutual {vars : _} -> TTC (CaseTree vars) where toBuf b (Case {name} idx x scTy xs) = do tag 0; toBuf b name; toBuf b idx; toBuf b xs - toBuf b (STerm x) + toBuf b (STerm _ x) = do tag 1; toBuf b x toBuf b (Unmatched msg) = do tag 2; toBuf b msg @@ -355,7 +355,7 @@ mutual xs <- fromBuf b pure (Case {name} idx (mkPrf idx) (Erased emptyFC False) xs) 1 => do x <- fromBuf b - pure (STerm x) + pure (STerm 0 x) 2 => do msg <- fromBuf b pure (Unmatched msg) 3 => pure Impossible diff --git a/src/Core/Unify.idr b/src/Core/Unify.idr index 16be52262..2b2d0926e 100644 --- a/src/Core/Unify.idr +++ b/src/Core/Unify.idr @@ -202,7 +202,7 @@ chaseMetas (n :: ns) all = case lookup n all of Just _ => chaseMetas ns all _ => do defs <- get Ctxt - Just (PMDef _ _ (STerm soln) _ _) <- + Just (PMDef _ _ (STerm _ soln) _ _) <- lookupDefExact n (gamma defs) | _ => chaseMetas ns (insert n () all) let sns = keys (getMetas soln) @@ -472,7 +472,7 @@ instantiate {newvars} loc mode env mname mref num mdef locs otm tm logTerm 5 "Definition" rhs let simpleDef = MkPMDefInfo (SolvedHole num) (isSimple rhs) let newdef = record { definition = - PMDef simpleDef [] (STerm rhs) (STerm rhs) [] + PMDef simpleDef [] (STerm 0 rhs) (STerm 0 rhs) [] } mdef addDef (Resolved mref) newdef removeHole mref @@ -1359,7 +1359,7 @@ retryGuess mode smode (hid, (loc, hname)) handleUnify (do tm <- search loc rig (smode == Defaults) depth defining (type def) [] - let gdef = record { definition = PMDef defaultPI [] (STerm tm) (STerm tm) [] } def + let gdef = record { definition = PMDef defaultPI [] (STerm 0 tm) (STerm 0 tm) [] } def logTermNF 5 ("Solved " ++ show hname) [] tm addDef (Resolved hid) gdef removeGuess hid @@ -1390,7 +1390,7 @@ retryGuess mode smode (hid, (loc, hname)) logTerm 5 "Retry Delay" tm pure $ delayMeta r envb !(getTerm ty) tm let gdef = record { definition = PMDef (MkPMDefInfo NotHole True) - [] (STerm tm') (STerm tm') [] } def + [] (STerm 0 tm') (STerm 0 tm') [] } def logTerm 5 ("Resolved " ++ show hname) tm' addDef (Resolved hid) gdef removeGuess hid @@ -1416,7 +1416,7 @@ retryGuess mode smode (hid, (loc, hname)) -- proper definition and remove it from the -- hole list [] => do let gdef = record { definition = PMDef (MkPMDefInfo NotHole True) - [] (STerm tm) (STerm tm) [] } def + [] (STerm 0 tm) (STerm 0 tm) [] } def logTerm 5 ("Resolved " ++ show hname) tm addDef (Resolved hid) gdef removeGuess hid @@ -1479,7 +1479,7 @@ checkArgsSame : {auto u : Ref UST UState} -> checkArgsSame [] = pure False checkArgsSame (x :: xs) = do defs <- get Ctxt - Just (PMDef _ [] (STerm def) _ _) <- + Just (PMDef _ [] (STerm 0 def) _ _) <- lookupDefExact (Resolved x) (gamma defs) | _ => checkArgsSame xs s <- anySame def xs @@ -1491,7 +1491,7 @@ checkArgsSame (x :: xs) anySame tm [] = pure False anySame tm (t :: ts) = do defs <- get Ctxt - Just (PMDef _ [] (STerm def) _ _) <- + Just (PMDef _ [] (STerm 0 def) _ _) <- lookupDefExact (Resolved t) (gamma defs) | _ => anySame tm ts if !(convert defs [] tm def) diff --git a/src/Idris/Error.idr b/src/Idris/Error.idr index 7dab15ee4..de99e0a4f 100644 --- a/src/Idris/Error.idr +++ b/src/Idris/Error.idr @@ -258,6 +258,13 @@ perror (InRHS fc n err) = pure $ "While processing right hand side of " ++ !(prettyName n) ++ " at " ++ show fc ++ ":\n" ++ !(perror err) +export +pwarning : {auto c : Ref Ctxt Defs} -> + {auto s : Ref Syn SyntaxInfo} -> + Warning -> Core String +pwarning (UnreachableClause fc env tm) + = pure $ "Warning: unreachable clause: " ++ !(pshow env tm) + export display : {auto c : Ref Ctxt Defs} -> {auto s : Ref Syn SyntaxInfo} -> @@ -265,3 +272,11 @@ display : {auto c : Ref Ctxt Defs} -> display err = pure $ maybe "" (\f => show f ++ ":") (getErrorLoc err) ++ !(perror err) + +export +displayWarning : {auto c : Ref Ctxt Defs} -> + {auto s : Ref Syn SyntaxInfo} -> + Warning -> Core String +displayWarning w + = pure $ maybe "" (\f => show f ++ ":") (getWarningLoc w) ++ + !(pwarning w) diff --git a/src/Idris/ModTree.idr b/src/Idris/ModTree.idr index b3668d808..d693a4563 100644 --- a/src/Idris/ModTree.idr +++ b/src/Idris/ModTree.idr @@ -184,11 +184,14 @@ buildMod loc num len mod ": Building " ++ showMod ++ " (" ++ src ++ ")" [] <- process {u} {m} msg src - | errs => do traverse emitError errs + | errs => do emitWarnings + traverse emitError errs pure (ferrs ++ errs) + emitWarnings traverse_ emitError ferrs pure ferrs - else do traverse_ emitError ferrs + else do emitWarnings + traverse_ emitError ferrs pure ferrs where getEithers : List (Either a b) -> (List a, List b) diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index 745533417..55d6c33c2 100644 --- a/src/Idris/REPL.idr +++ b/src/Idris/REPL.idr @@ -399,7 +399,7 @@ processEdit (ExprSearch upd line name hints all) if upd then updateFile (proofSearch name res (integerToNat (cast (line - 1)))) else pure $ DisplayEdit [res] - [(n, nidx, PMDef pi [] (STerm tm) _ _)] => + [(n, nidx, PMDef pi [] (STerm _ tm) _ _)] => case holeInfo pi of NotHole => pure $ EditError "Not a searchable hole" SolvedHole locs => diff --git a/src/Idris/REPLCommon.idr b/src/Idris/REPLCommon.idr index 4cb924a55..4e3954c09 100644 --- a/src/Idris/REPLCommon.idr +++ b/src/Idris/REPLCommon.idr @@ -11,6 +11,7 @@ import Idris.IDEMode.Commands import public Idris.REPLOpts import Idris.Syntax +import Data.List -- Output informational messages, unless quiet flag is set export @@ -74,6 +75,44 @@ emitError err addOne : (Int, Int) -> (Int, Int) addOne (l, c) = (l + 1, c + 1) +export +emitWarning : {auto c : Ref Ctxt Defs} -> + {auto o : Ref ROpts REPLOpts} -> + {auto s : Ref Syn SyntaxInfo} -> + Warning -> Core () +emitWarning w + = do opts <- get ROpts + case idemode opts of + REPL _ => + do msg <- displayWarning w + coreLift $ putStrLn msg + IDEMode i _ f => + do msg <- pwarning w + case getWarningLoc w of + Nothing => iputStrLn msg + Just fc => + send f (SExpList [SymbolAtom "warning", + SExpList [toSExp (file fc), + toSExp (addOne (startPos fc)), + toSExp (addOne (endPos fc)), + toSExp msg, + -- highlighting; currently blank + SExpList []], + toSExp i]) + where + addOne : (Int, Int) -> (Int, Int) + addOne (l, c) = (l + 1, c + 1) + +export +emitWarnings : {auto c : Ref Ctxt Defs} -> + {auto o : Ref ROpts REPLOpts} -> + {auto s : Ref Syn SyntaxInfo} -> + Core () +emitWarnings + = do defs <- get Ctxt + traverse_ emitWarning (reverse (warnings defs)) + put Ctxt (record { warnings = [] } defs) + getFCLine : FC -> Int getFCLine fc = fst (startPos fc) diff --git a/src/TTImp/Elab/Delayed.idr b/src/TTImp/Elab/Delayed.idr index 7be3068a1..f233ab3c1 100644 --- a/src/TTImp/Elab/Delayed.idr +++ b/src/TTImp/Elab/Delayed.idr @@ -222,7 +222,7 @@ retryDelayed' errmode acc (d@(_, i, elab) :: ds) let ds' = reverse (delayedElab ust) ++ ds updateDef (Resolved i) (const (Just - (PMDef (MkPMDefInfo NotHole True) [] (STerm tm) (STerm tm) []))) + (PMDef (MkPMDefInfo NotHole True) [] (STerm 0 tm) (STerm 0 tm) []))) logTerm 5 ("Resolved delayed hole " ++ show i) tm logTermNF 5 ("Resolved delayed hole NF " ++ show i) [] tm removeHole i diff --git a/src/TTImp/ProcessDef.idr b/src/TTImp/ProcessDef.idr index aed2ce2ae..a71c815e9 100644 --- a/src/TTImp/ProcessDef.idr +++ b/src/TTImp/ProcessDef.idr @@ -650,7 +650,7 @@ mkRunTime fc n MissingCases _ => addErrorCase clauses_init _ => clauses_init - (rargs ** tree_rt) <- getPMDef (location gdef) RunTime n ty clauses + (rargs ** (tree_rt, _)) <- getPMDef (location gdef) RunTime n ty clauses log 5 $ show cov ++ ":\nRuntime tree for " ++ show (fullname gdef) ++ ": " ++ show tree_rt let Just Refl = nameListEq cargs rargs @@ -715,6 +715,11 @@ toPats : Clause -> (vs ** (Env Term vs, Term vs, Term vs)) toPats (MkClause {vars} env lhs rhs) = (_ ** (env, lhs, rhs)) +warnUnreachable : {auto c : Ref Ctxt Defs} -> + Clause -> Core () +warnUnreachable (MkClause env lhs rhs) + = recordWarning (UnreachableClause (getLoc lhs) env lhs) + export processDef : {vars : _} -> {auto c : Ref Ctxt Defs} -> @@ -738,7 +743,10 @@ processDef opts nest env fc n_in cs_in cs <- traverse (checkClause mult hashit nidx opts nest env) cs_in let pats = map toPats (rights cs) - (cargs ** tree_ct) <- getPMDef fc CompileTime n ty (rights cs) + (cargs ** (tree_ct, unreachable)) <- + getPMDef fc CompileTime n ty (rights cs) + + traverse_ warnUnreachable unreachable logC 2 (do t <- toFullNames tree_ct pure ("Case tree for " ++ show n ++ ": " ++ show t)) @@ -842,7 +850,8 @@ processDef opts nest env fc n_in cs_in checkCoverage n ty mult cs = do covcs' <- traverse getClause cs -- Make stand in LHS for impossible clauses let covcs = mapMaybe id covcs' - (_ ** ctree) <- getPMDef fc CompileTime (Resolved n) ty covcs + (_ ** (ctree, _)) <- + getPMDef fc CompileTime (Resolved n) ty covcs log 3 $ "Working from " ++ show !(toFullNames ctree) missCase <- if any catchAll covcs then do log 3 $ "Catch all case in " ++ show n diff --git a/tests/Main.idr b/tests/Main.idr index afd82a14f..c0bf859c7 100644 --- a/tests/Main.idr +++ b/tests/Main.idr @@ -43,6 +43,7 @@ idrisTests -- Coverage checking "coverage001", "coverage002", "coverage003", "coverage004", "coverage005", "coverage006", "coverage007", "coverage008", + "coverage009", -- Error messages "error001", "error002", "error003", "error004", "error005", "error006", "error007", "error008", "error009", "error010", diff --git a/tests/idris2/coverage009/expected b/tests/idris2/coverage009/expected new file mode 100644 index 000000000..0e4a28d72 --- /dev/null +++ b/tests/idris2/coverage009/expected @@ -0,0 +1,3 @@ +1/1: Building unreachable (unreachable.idr) +unreachable.idr:3:1--3:18:Warning: unreachable clause: foo Nothing True +unreachable.idr:5:1--5:19:Warning: unreachable clause: foo Nothing False diff --git a/tests/idris2/coverage009/run b/tests/idris2/coverage009/run new file mode 100755 index 000000000..84e1ec928 --- /dev/null +++ b/tests/idris2/coverage009/run @@ -0,0 +1,3 @@ +$1 --check unreachable.idr + +rm -rf build diff --git a/tests/idris2/coverage009/unreachable.idr b/tests/idris2/coverage009/unreachable.idr new file mode 100644 index 000000000..5cc5d6e26 --- /dev/null +++ b/tests/idris2/coverage009/unreachable.idr @@ -0,0 +1,5 @@ +foo : Maybe Int -> Bool -> Int +foo Nothing _ = 42 +foo Nothing True = 94 +foo (Just x) _ = x +foo Nothing False = 42 From 9c5594223e8186ab517276560c72c6dc75c5b7d1 Mon Sep 17 00:00:00 2001 From: Edwin Brady Date: Mon, 25 May 2020 01:02:07 +0100 Subject: [PATCH 6/6] Small documentation updates --- docs/source/tutorial/starting.rst | 6 +++--- docs/source/tutorial/typesfuns.rst | 31 ++++++++++++++++++++++++++++++ docs/source/updates/updates.rst | 15 +++++++++++++++ 3 files changed, 49 insertions(+), 3 deletions(-) diff --git a/docs/source/tutorial/starting.rst b/docs/source/tutorial/starting.rst index 985ddb415..2d7738227 100644 --- a/docs/source/tutorial/starting.rst +++ b/docs/source/tutorial/starting.rst @@ -28,14 +28,14 @@ You can download the Idris 2 source from the `Idris web site `_ or get the latest development version from `idris-lang/Idris2 `_ on Github. This includes the Idris 2 -source code and the Scheme code code generated from that. Once you have +source code and the Scheme code generated from that. Once you have unpacked the source, you can install it as follows:: make bootstrap SCHEME=chez Where `chez` is the executable name of the Chez Scheme compiler. This will -vary from system to system, but is often one of `scheme`, `chezscheme`, or -`chezscheme9.5`. If you are building via Racket, you can install it as +vary from system to system, but is often one of ``scheme``, ``chezscheme``, or +``chezscheme9.5``. If you are building via Racket, you can install it as follows:: make bootstrap-racket diff --git a/docs/source/tutorial/typesfuns.rst b/docs/source/tutorial/typesfuns.rst index 8b9d2f6a9..bdb504bf4 100644 --- a/docs/source/tutorial/typesfuns.rst +++ b/docs/source/tutorial/typesfuns.rst @@ -234,6 +234,37 @@ of how this works in practice: .. _sect-holes: +Totality and Covering +--------------------- + +By default, functions in Idris must be ``covering``. That is, there must be +patterns which cover all possible values of the inputs types. For example, +the following definition will give an error: + +.. code-block:: idris + + fromMaybe : Maybe a -> a + fromMaybe (Just x) = x + +This gives an error because ``fromMaybe Nothing`` is not defined. Idris +reports: + +:: + + frommaybe.idr:1:1--2:1:fromMaybe is not covering. Missing cases: + fromMaybe Nothing + +You can override this with a ``partial`` annotation: + +.. code-block:: idris + + partial fromMaybe : Maybe a -> a + fromMaybe (Just x) = x + +However, this is not advisable, and in general you should only do this during +the initial development of a function, or during debugging. If you try to +evaluate ``fromMaybe Nothing`` at run time you will get a run time error. + Holes ----- diff --git a/docs/source/updates/updates.rst b/docs/source/updates/updates.rst index 524402797..57beebad5 100644 --- a/docs/source/updates/updates.rst +++ b/docs/source/updates/updates.rst @@ -425,6 +425,21 @@ can see if we try evaluating ``myShow True`` at the REPL: In fact, this is how interfaces are elaborated. However, ``%hint`` should be used with care. Too many hints can lead to a large search space! +Record fields +------------- + +Record fields can now be accessed via a ``.``. For example, if you have: + +.. code-block:: idris + + record Person where + constructor MkPerson + firstName, middleName, lastName : String + age : Int + +and you have a record ``fred : Person``, then you can use ``fred.firstName`` +to access the ``firstName`` field. + Totality and Coverage ---------------------