idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-25 04:33:45 +03:00
Code Issues Projects Releases Wiki Activity

Merge remote-tracking branch 'upstream/master'

Browse Source
This commit is contained in:
Edwin Brady 2020-05-25 09:11:54 +01:00
commit 3859f60d7a
34 changed files with 631 additions and 387 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
.gitignore vendored
View File

@ -1,3 +1,4 @@
idris2docs_venv
*~
*.ibc
*.ttc

4
docs/source/reference/envvars.rst
View File

@ -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

2
docs/source/reference/records.rst
View File

@ -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``

10
docs/source/tutorial/miscellany.rst
View File

@ -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:

6
docs/source/tutorial/theorems.rst
View File

@ -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

4
docs/source/tutorial/views.rst
View File

@ -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
==========================

4
docs/source/typedd/typedd.rst
View File

@ -461,4 +461,6 @@ In ``ATM.idr``, add:
Chapter 15
----------
TODO
.. todo::
This chapter.

4
idris2.ipkg
View File

@ -52,6 +52,7 @@ modules =
Data.Bool.Extra,
Data.IntMap,
Data.LengthMatch,
Data.List.Extra,
Data.NameMap,
Data.StringMap,
Data.These,
@ -83,9 +84,12 @@ modules =
Idris.Version,
Parser.Lexer.Common,
Parser.Lexer.Package,
Parser.Lexer.Source,
Parser.Rule.Common,
Parser.Rule.Package,
Parser.Rule.Source,
Parser.Package,
Parser.Source,
Parser.Support,
Parser.Unlit,

3
idris2api.ipkg
View File

@ -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,

3
src/Core/Core.idr
View File

@ -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

11
src/Data/List/Extra.idr Normal file
View File

@ -0,0 +1,11 @@
module Data.List.Extra
%default covering
||| Fetches the element at a given position.
||| Returns `Nothing` if the position beyond the list's end.
public export
elemAt : List a -> Nat -> Maybe a
elemAt [] _ = Nothing
elemAt (l :: _) Z = Just l
elemAt (_ :: ls) (S n) = elemAt ls n

51
src/Idris/IDEMode/CaseSplit.idr
View File

@ -19,19 +19,22 @@ import Idris.Resugar
import Idris.Syntax
import Data.List
import Data.List.Extra
import Data.Strings
import System.File
%default covering
getLine : Nat -> List String -> Maybe String
getLine Z (l :: ls) = Just l
getLine (S k) (l :: ls) = getLine k ls
getLine _ [] = Nothing
||| A series of updates is a mapping from `RawName` to `String`
||| `RawName` is currently just an alias for `String`
||| `String` is a rendered `List SourcePart`
Updates : Type
Updates = List (RawName, String)
||| Convert a RawImp update to a SourcePart one
toStrUpdate : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
(Name, RawImp) -> Core (List (String, String))
(Name, RawImp) -> Core Updates
toStrUpdate (UN n, term)
= do clause <- pterm term
pure [(n, show (bracket clause))]
@ -46,38 +49,30 @@ toStrUpdate (UN n, term)
bracket tm = PBracketed emptyFC tm
toStrUpdate _ = pure [] -- can't replace non user names
dump : SourcePart -> String
dump (Whitespace str) = str
dump (Name n) = n
dump (HoleName n) = "?" ++ n
dump LBrace = "{"
dump RBrace = "}"
dump Equal = "="
dump (Other str) = str
data UPD : Type where
doUpdates : {auto u : Ref UPD (List String)} ->
Defs -> List (String, String) -> List SourcePart ->
Defs -> Updates -> List SourcePart ->
Core (List SourcePart)
doUpdates defs ups [] = pure []
doUpdates defs ups (LBrace :: xs)
= case dropSpace xs of
= let (ws, nws) = spanSpace xs in map (LBrace :: ws ++) $
case nws of
Name n :: RBrace :: rest =>
pure (LBrace :: Name n ::
pure (Name n ::
Whitespace " " :: Equal :: Whitespace " " ::
!(doUpdates defs ups (Name n :: RBrace :: rest)))
Name n :: Equal :: rest =>
pure (LBrace :: Name n ::
pure (Name n ::
Whitespace " " :: Equal :: Whitespace " " ::
!(doUpdates defs ups rest))
_ => pure (LBrace :: !(doUpdates defs ups xs))
_ => doUpdates defs ups xs
where
dropSpace : List SourcePart -> List SourcePart
dropSpace [] = []
dropSpace (RBrace :: xs) = RBrace :: xs
dropSpace (Whitespace _ :: xs) = dropSpace xs
dropSpace (x :: xs) = x :: dropSpace xs
spanSpace : List SourcePart -> (List SourcePart, List SourcePart)
spanSpace [] = ([], [])
spanSpace (RBrace :: xs) = ([], RBrace :: xs)
spanSpace (w@(Whitespace _) :: xs) = mapFst (w ::) (spanSpace xs)
spanSpace (x :: xs) = map (x ::) (spanSpace xs)
doUpdates defs ups (Name n :: xs)
= case lookup n ups of
Nothing => pure (Name n :: !(doUpdates defs ups xs))
@ -94,20 +89,20 @@ doUpdates defs ups (x :: xs)
-- Update the token list with the string replacements for each match, and return
-- the newly generated strings.
updateAll : {auto u : Ref UPD (List String)} ->
Defs -> List SourcePart -> List (List (String, String)) ->
Defs -> List SourcePart -> List Updates ->
Core (List String)
updateAll defs l [] = pure []
updateAll defs l (rs :: rss)
= do l' <- doUpdates defs rs l
rss' <- updateAll defs l rss
pure (concat (map dump l') :: rss')
pure (concatMap toString l' :: rss')
-- Turn the replacements we got from 'getSplits' into a list of actual string
-- replacements
getReplaces : {auto c : Ref Ctxt Defs} ->
{auto s : Ref Syn SyntaxInfo} ->
{auto o : Ref ROpts REPLOpts} ->
List (Name, RawImp) -> Core (List (String, String))
List (Name, RawImp) -> Core Updates
getReplaces updates
= do strups <- traverse toStrUpdate updates
pure (concat strups)
@ -135,7 +130,7 @@ updateCase splits line col
Just f =>
do Right file <- coreLift $ readFile f
| Left err => throw (FileErr f err)
let thisline = getLine (integerToNat (cast line)) (lines file)
let thisline = elemAt (lines file) (integerToNat (cast line))
case thisline of
Nothing => throw (InternalError "File too short!")
Just l =>

28
src/Idris/IDEMode/Parser.idr
View File

@ -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)

24
src/Idris/IDEMode/TokenLine.idr
View File

@ -4,16 +4,38 @@ module Idris.IDEMode.TokenLine
import Parser.Lexer.Source
import Text.Lexer
public export
RawName : Type
RawName = String
public export
data SourcePart
= Whitespace String
| Name String
| Name RawName
| HoleName String
| LBrace
| RBrace
| Equal
| Other String
------------------------------------------------------------------------
-- Printer
------------------------------------------------------------------------
export
toString : SourcePart -> String
toString (Whitespace str) = str
toString (Name n) = n
toString (HoleName n) = "?" ++ n
toString LBrace = "{"
toString RBrace = "}"
toString Equal = "="
toString (Other str) = str
------------------------------------------------------------------------
-- Parser
------------------------------------------------------------------------
holeIdent : Lexer
holeIdent = is '?' <+> identNormal

77
src/Idris/Package.idr
View File

@ -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} ->

216
src/Idris/Parser.idr
View File

@ -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 = (["<expr>"], 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)

4
src/Idris/ProcessIdr.idr
View File

@ -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

2
src/Idris/REPL.idr
View File

@ -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)

27
src/Parser/Lexer/Common.idr
View File

@ -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)

65
src/Parser/Lexer/Package.idr Normal file
View File

@ -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

115
src/Parser/Lexer/Source.idr
View File

@ -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)

24
src/Parser/Package.idr Normal file
View File

@ -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)

79
src/Parser/Rule/Package.idr Normal file
View File

@ -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

99
src/Parser/Rule/Source.idr
View File

@ -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

14
src/Parser/Source.idr
View File

@ -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))

18
src/Parser/Support.idr
View File

@ -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

98
src/TTImp/Parser.idr
View File

@ -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

4
src/Text/Parser/Core.idr
View File

@ -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)

6
src/Utils/String.idr
View File

@ -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

1
tests/Main.idr
View File

@ -53,6 +53,7 @@ idrisTests
"interactive001", "interactive002", "interactive003", "interactive004",
"interactive005", "interactive006", "interactive007", "interactive008",
"interactive009", "interactive010", "interactive011", "interactive012",
"interactive013",
-- Literate
"literate001", "literate002", "literate003", "literate004",
"literate005", "literate006", "literate007", "literate008",

4
tests/idris2/interactive013/Spacing.idr Normal file
View File

@ -0,0 +1,4 @@
module Spacing
id : {n : Nat} -> Nat
id { n} = ?a

5
tests/idris2/interactive013/expected Normal file
View File

@ -0,0 +1,5 @@
1/1: Building Spacing (Spacing.idr)
Spacing> id { n = 0} = ?a_1
id { n = (S k)} = ?a_2
Spacing>
Bye for now!

2
tests/idris2/interactive013/input Normal file
View File

@ -0,0 +1,2 @@
:cs 4 6 n
:q

3
tests/idris2/interactive013/run Executable file
View File

@ -0,0 +1,3 @@
$1 --no-banner Spacing.idr < input
rm -rf build