edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-11-30 12:14:17 +03:00
Code Issues Projects Releases Wiki Activity

Split Lexer/Parser into two: Source(.idr) and Package(.ipkg)

Browse Source
This commit is contained in:
Fabián Heredia Montiel 2020-05-16 21:53:01 -05:00
parent 892dee2c71
commit bf89dd0078
29 changed files with 870 additions and 721 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
idris2.ipkg
View File

@ -80,7 +80,14 @@ modules =
Idris.Syntax,
Idris.Version,
Parser.Lexer,
Parser.Lexer.Common,
Parser.Lexer.Source,
Parser.Lexer.Package,
Parser.Rules.Common,
Parser.Rules.Source,
Parser.Rules.Package,
Parser.Package,
Parser.Source,
Parser.Support,
Parser.Unlit,

9
idris2api.ipkg
View File

@ -76,7 +76,14 @@ modules =
Idris.Syntax,
Idris.Version,
Parser.Lexer,
Parser.Lexer.Common,
Parser.Lexer.Source,
Parser.Lexer.Package,
Parser.Rules.Common,
Parser.Rules.Source,
Parser.Rules.Package,
Parser.Package,
Parser.Source,
Parser.Support,
Parser.Unlit,

13
src/Core/Core.idr
View File

@ -1,12 +1,13 @@
module Core.Core
import Core.Env
import Core.TT
import Data.Vect
import Parser.Support
import public Control.Catchable
import public Data.IORef
import Core.Env
import Core.TT
import Data.Vect
import Parser.Source
import System
%default covering
@ -94,7 +95,7 @@ data Error
| GenericMsg FC String
| TTCError TTCErrorMsg
| FileErr String FileError
| ParseFail FC ParseError
| ParseFail FC (ParsingError SourceToken)
| ModuleNotFound FC (List String)
| CyclicImports (List (List String))
| ForceNeeded

4
src/Core/Primitives.idr
View File

@ -32,7 +32,9 @@ unaryOp _ _ = Nothing
castString : Vect 1 (NF vars) -> Maybe (NF vars)
castString [NPrimVal fc (I i)] = Just (NPrimVal fc (Str (show i)))
castString [NPrimVal fc (BI i)] = Just (NPrimVal fc (Str (show i)))
castString [NPrimVal fc (Ch i)] = Just (NPrimVal fc (Str (stripQuotes (show i))))
castString [NPrimVal fc (Ch i)] = case isLTE 2 (length $ show i) of
Yes prf => Just $ NPrimVal fc (Str $ stripQuotes $ show i)
No _ => Nothing
castString [NPrimVal fc (Db i)] = Just (NPrimVal fc (Str (show i)))
castString _ = Nothing

2
src/Idris/Desugar.idr
View File

@ -17,7 +17,7 @@ import Idris.Syntax
import Idris.Elab.Implementation
import Idris.Elab.Interface
import Parser.Lexer
import Parser.Lexer.Source
import TTImp.BindImplicits
import TTImp.Parser

2
src/Idris/Error.idr
View File

@ -9,7 +9,7 @@ import Core.Options
import Idris.Resugar
import Idris.Syntax
import Parser.Support
import Parser.Source
%default covering

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

@ -6,7 +6,7 @@ import Core.Metadata
import Core.TT
import Core.Value
import Parser.Lexer
import Parser.Lexer.Source
import Parser.Unlit
import TTImp.Interactive.CaseSplit

2
src/Idris/IDEMode/MakeClause.idr
View File

@ -1,7 +1,7 @@
module Idris.IDEMode.MakeClause
import Core.Name
import Parser.Lexer
import Parser.Lexer.Source
import Parser.Unlit
-- Implement make-with and make-case from the IDE mode

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

@ -6,26 +6,28 @@ module Idris.IDEMode.Parser
import Idris.IDEMode.Commands
import Text.Parser
import Parser.Lexer
import Parser.Lexer.Source
import Parser.Support
import Text.Lexer
import Utils.Either
import Utils.String
%hide Lexer.symbols
%hide Lexer.Source.symbols
ideTokens : TokenMap SourceToken
ideTokens =
map (\x => (exact x, Symbol)) symbols ++
[(digits, \x => IntegerLit (cast x)),
(stringLit, \x => case (isLTE 2 $ length x) of
Yes prf => StringLit (stripQuotes x)
No _ => Unrecognised x),
(identAllowDashes, \x => NSIdent [x]),
(space, Comment)]
where
symbols : List String
symbols = ["(", ":", ")"]
ideTokens : TokenMap Token
ideTokens =
map (\x => (exact x, Symbol)) symbols ++
[(digits, \x => Literal (cast x)),
(stringLit, \x => StrLit (stripQuotes x)),
(identAllowDashes, \x => NSIdent [x]),
(space, Comment)]
idelex : String -> Either (Int, Int, String) (List (TokenData Token))
idelex : String -> Either (Int, Int, String) (List (TokenData SourceToken))
idelex str
= case lex ideTokens str of
-- Add the EndInput token so that we'll have a line and column
@ -34,7 +36,7 @@ idelex str
[MkToken l c EndInput])
(_, fail) => Left fail
where
notComment : TokenData Token -> Bool
notComment : TokenData SourceToken -> Bool
notComment t = case tok t of
Comment _ => False
_ => True
@ -56,7 +58,7 @@ sexp
symbol ")"
pure (SExpList xs)
ideParser : String -> Grammar (TokenData Token) e ty -> Either ParseError ty
ideParser : String -> Grammar (TokenData SourceToken) e ty -> Either ParseError ty
ideParser str p
= do toks <- mapError LexFail $ idelex str
parsed <- mapError mapParseError $ parse p toks

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

@ -1,7 +1,7 @@
||| Tokenise a source line for easier processing
module Idris.IDEMode.TokenLine
import Parser.Lexer
import Parser.Lexer.Source
import Text.Lexer
public export

38
src/Idris/Package.idr
View File

@ -21,8 +21,7 @@ import Idris.REPLOpts
import Idris.SetOptions
import Idris.Syntax
import Idris.Version
import Parser.Lexer
import Parser.Support
import Parser.Package
import Utils.Binary
import System
@ -111,7 +110,7 @@ data DescField : Type where
PPreclean : FC -> String -> DescField
PPostclean : FC -> String -> DescField
field : String -> Rule DescField
field : String -> PackageRule DescField
field fname
= strField PVersion "version"
<|> strField PAuthors "authors"
@ -131,42 +130,41 @@ field fname
<|> strField PPostinstall "postinstall"
<|> strField PPreclean "preclean"
<|> strField PPostclean "postclean"
<|> do exactIdent "depends"; symbol "="
<|> do property "depends"; assignment
ds <- sepBy1 (symbol ",") unqualifiedName
pure (PDepends ds)
<|> do exactIdent "modules"; symbol "="
<|> do property "modules"; assignment
ms <- sepBy1 (symbol ",")
(do start <- location
ns <- nsIdent
end <- location
pure (MkFC fname start end, ns))
pure (PModules ms)
<|> do exactIdent "main"; symbol "="
<|> do property "main"; assignment
start <- location
m <- nsIdent
end <- location
pure (PMainMod (MkFC fname start end) m)
<|> do exactIdent "executable"; symbol "="
<|> do property "executable"; assignment
e <- unqualifiedName
pure (PExec e)
where
getStr : (FC -> String -> DescField) -> FC ->
String -> Constant -> EmptyRule DescField
getStr p fc fld (Str s) = pure (p fc s)
getStr p fc fld _ = fail $ fld ++ " field must be a string"
String -> String -> EmptyPackageRule DescField
getStr p fc fld s = pure (p fc s)
strField : (FC -> String -> DescField) -> String -> Rule DescField
strField : (FC -> String -> DescField) -> String -> PackageRule DescField
strField p f
= do start <- location
exactIdent f
symbol "="
c <- constant
property f
assignment
c <- string
end <- location
getStr p (MkFC fname start end) f c
parsePkgDesc : String -> Rule (String, List DescField)
parsePkgDesc : String -> PackageRule (String, List DescField)
parsePkgDesc fname
= do exactIdent "package"
= do property "package"
name <- unqualifiedName
fields <- many (field fname)
pure (name, fields)
@ -432,9 +430,9 @@ processPackage : {auto c : Ref Ctxt Defs} ->
{auto o : Ref ROpts REPLOpts} ->
PkgCommand -> String -> Core ()
processPackage cmd file
= do Right (pname, fs) <- coreLift $ parseFile file
= do Right (pname, fs) <- coreLift $ parsePackageFile file
(do desc <- parsePkgDesc file
eoi
eof
pure desc)
| Left err => throw (ParseFail (getParseErrorLoc file err) err)
pkg <- addFields fs (initPkgDesc pname)
@ -478,9 +476,9 @@ findIpkg fname
= do Just (dir, ipkgn, up) <- coreLift findIpkgFile
| Nothing => pure fname
coreLift $ changeDir dir
Right (pname, fs) <- coreLift $ parseFile ipkgn
Right (pname, fs) <- coreLift $ parsePackageFile ipkgn
(do desc <- parsePkgDesc ipkgn
eoi
eof
pure desc)
| Left err => throw (ParseFail (getParseErrorLoc ipkgn err) err)
pkg <- addFields fs (initPkgDesc pname)

223
src/Idris/Parser.idr
View File

@ -1,18 +1,17 @@
module Idris.Parser
import public Parser.Source
import Core.Options
import Data.List.Views
import Idris.Syntax
import public Parser.Support
import Parser.Lexer
import TTImp.TTImp
import public Text.Parser
import Data.List.Views
%default covering
-- Forward declare since they're used in the parser
topDecl : FileName -> IndentInfo -> Rule (List PDecl)
topDecl : FileName -> IndentInfo -> SourceRule (List PDecl)
collectDefs : List PDecl -> List PDecl
-- Some context for the parser
@ -39,7 +38,7 @@ export
plhs : ParseOpts
plhs = MkParseOpts False False
atom : FileName -> Rule PTerm
atom : FileName -> SourceRule PTerm
atom fname
= do start <- location
x <- constant
@ -78,30 +77,30 @@ atom fname
end <- location
pure (PRef (MkFC fname start end) x)
whereBlock : FileName -> Int -> Rule (List PDecl)
whereBlock : FileName -> Int -> SourceRule (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 -> Rule ()
commitKeyword : IndentInfo -> String -> SourceRule ()
commitKeyword indents req
= do mustContinue indents (Just req)
keyword req
mustContinue indents Nothing
commitSymbol : String -> Rule ()
commitSymbol : String -> SourceRule ()
commitSymbol req
= symbol req
<|> fatalError ("Expected '" ++ req ++ "'")
continueWith : IndentInfo -> String -> Rule ()
continueWith : IndentInfo -> String -> SourceRule ()
continueWith indents req
= do mustContinue indents (Just req)
symbol req
iOperator : Rule Name
iOperator : SourceRule Name
iOperator
= operator
<|> do symbol "`"
@ -115,7 +114,7 @@ data ArgType
| WithArg PTerm
mutual
appExpr : ParseOpts -> FileName -> IndentInfo -> Rule PTerm
appExpr : ParseOpts -> FileName -> IndentInfo -> SourceRule PTerm
appExpr q fname indents
= case_ fname indents
<|> lambdaCase fname indents
@ -145,11 +144,11 @@ mutual
applyExpImp start end f (WithArg exp :: args)
= applyExpImp start end (PWithApp (MkFC fname start end) f exp) args
argExpr : ParseOpts -> FileName -> IndentInfo -> Rule ArgType
argExpr : ParseOpts -> FileName -> IndentInfo -> SourceRule ArgType
argExpr q fname indents
= do continue indents
arg <- simpleExpr fname indents
the (EmptyRule _) $ case arg of
the (EmptySourceRule _) $ case arg of
PHole loc _ n => pure (ExpArg (PHole loc True n))
t => pure (ExpArg t)
<|> do continue indents
@ -162,7 +161,7 @@ mutual
pure (WithArg arg)
else fail "| not allowed here"
implicitArg : FileName -> IndentInfo -> Rule (Maybe Name, PTerm)
implicitArg : FileName -> IndentInfo -> SourceRule (Maybe Name, PTerm)
implicitArg fname indents
= do start <- location
symbol "{"
@ -181,7 +180,7 @@ mutual
symbol "}"
pure (Nothing, tm)
opExpr : ParseOpts -> FileName -> IndentInfo -> Rule PTerm
opExpr : ParseOpts -> FileName -> IndentInfo -> SourceRule PTerm
opExpr q fname indents
= do start <- location
l <- appExpr q fname indents
@ -201,7 +200,7 @@ mutual
pure (POp (MkFC fname start end) op l r))
<|> pure l
dpair : FileName -> FilePos -> IndentInfo -> Rule PTerm
dpair : FileName -> FilePos -> IndentInfo -> SourceRule PTerm
dpair fname start indents
= do x <- unqualifiedName
symbol ":"
@ -224,7 +223,7 @@ mutual
(PImplicit (MkFC fname start end))
rest)
bracketedExpr : FileName -> FilePos -> IndentInfo -> Rule PTerm
bracketedExpr : FileName -> FilePos -> IndentInfo -> SourceRule 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
@ -251,12 +250,12 @@ mutual
-- all the other bracketed expressions
tuple fname start indents e)
getInitRange : List PTerm -> EmptyRule (PTerm, Maybe PTerm)
getInitRange : List PTerm -> EmptySourceRule (PTerm, Maybe PTerm)
getInitRange [x] = pure (x, Nothing)
getInitRange [x, y] = pure (x, Just y)
getInitRange _ = fatalError "Invalid list range syntax"
listRange : FileName -> FilePos -> IndentInfo -> List PTerm -> Rule PTerm
listRange : FileName -> FilePos -> IndentInfo -> List PTerm -> SourceRule PTerm
listRange fname start indents xs
= do symbol "]"
end <- location
@ -270,7 +269,7 @@ mutual
rstate <- getInitRange xs
pure (PRange fc (fst rstate) (snd rstate) y)
listExpr : FileName -> FilePos -> IndentInfo -> Rule PTerm
listExpr : FileName -> FilePos -> IndentInfo -> SourceRule PTerm
listExpr fname start indents
= do ret <- expr pnowith fname indents
symbol "|"
@ -286,7 +285,7 @@ mutual
pure (PList (MkFC fname start end) xs))
-- A pair, dependent pair, or just a single expression
tuple : FileName -> FilePos -> IndentInfo -> PTerm -> Rule PTerm
tuple : FileName -> FilePos -> IndentInfo -> PTerm -> SourceRule PTerm
tuple fname start indents e
= do rest <- some (do symbol ","
estart <- location
@ -306,7 +305,7 @@ mutual
mergePairs end ((estart, exp) :: rest)
= PPair (MkFC fname estart end) exp (mergePairs end rest)
simpleExpr : FileName -> IndentInfo -> Rule PTerm
simpleExpr : FileName -> IndentInfo -> SourceRule PTerm
simpleExpr fname indents =
do
start <- location
@ -322,7 +321,7 @@ mutual
[] => root
fs => PRecordFieldAccess (MkFC fname start end) root recFields
simplerExpr : FileName -> IndentInfo -> Rule PTerm
simplerExpr : FileName -> IndentInfo -> SourceRule PTerm
simplerExpr fname indents
= do start <- location
x <- unqualifiedName
@ -377,7 +376,7 @@ mutual
end <- location
pure (PUnifyLog (MkFC fname start end) (cast lvl) e)
multiplicity : EmptyRule (Maybe Integer)
multiplicity : EmptySourceRule (Maybe Integer)
multiplicity
= do c <- intLit
pure (Just c)
@ -385,7 +384,7 @@ mutual
-- pure (Just 2) -- Borrowing, not implemented
<|> pure Nothing
getMult : Maybe Integer -> EmptyRule RigCount
getMult : Maybe Integer -> EmptySourceRule RigCount
getMult (Just 0) = pure erased
getMult (Just 1) = pure linear
getMult Nothing = pure top
@ -398,7 +397,7 @@ mutual
= PPi fc rig p n ty (pibindAll fc p rest scope)
bindList : FileName -> FilePos -> IndentInfo ->
Rule (List (RigCount, PTerm, PTerm))
SourceRule (List (RigCount, PTerm, PTerm))
bindList fname start indents
= sepBy1 (symbol ",")
(do rigc <- multiplicity
@ -411,7 +410,7 @@ mutual
pure (rig, pat, ty))
pibindListName : FileName -> FilePos -> IndentInfo ->
Rule (List (RigCount, Name, PTerm))
SourceRule (List (RigCount, Name, PTerm))
pibindListName fname start indents
= do rigc <- multiplicity
ns <- sepBy1 (symbol ",") unqualifiedName
@ -429,12 +428,12 @@ mutual
pure (rig, n, ty))
pibindList : FileName -> FilePos -> IndentInfo ->
Rule (List (RigCount, Maybe Name, PTerm))
SourceRule (List (RigCount, Maybe Name, PTerm))
pibindList fname start indents
= do params <- pibindListName fname start indents
pure $ map (\(rig, n, ty) => (rig, Just n, ty)) params
bindSymbol : Rule (PiInfo PTerm)
bindSymbol : SourceRule (PiInfo PTerm)
bindSymbol
= do symbol "->"
pure Explicit
@ -442,7 +441,7 @@ mutual
pure AutoImplicit
explicitPi : FileName -> IndentInfo -> Rule PTerm
explicitPi : FileName -> IndentInfo -> SourceRule PTerm
explicitPi fname indents
= do start <- location
symbol "("
@ -453,7 +452,7 @@ mutual
end <- location
pure (pibindAll (MkFC fname start end) exp binders scope)
autoImplicitPi : FileName -> IndentInfo -> Rule PTerm
autoImplicitPi : FileName -> IndentInfo -> SourceRule PTerm
autoImplicitPi fname indents
= do start <- location
symbol "{"
@ -466,7 +465,7 @@ mutual
end <- location
pure (pibindAll (MkFC fname start end) AutoImplicit binders scope)
defaultImplicitPi : FileName -> IndentInfo -> Rule PTerm
defaultImplicitPi : FileName -> IndentInfo -> SourceRule PTerm
defaultImplicitPi fname indents
= do start <- location
symbol "{"
@ -480,7 +479,7 @@ mutual
end <- location
pure (pibindAll (MkFC fname start end) (DefImplicit t) binders scope)
forall_ : FileName -> IndentInfo -> Rule PTerm
forall_ : FileName -> IndentInfo -> SourceRule PTerm
forall_ fname indents
= do start <- location
keyword "forall"
@ -495,7 +494,7 @@ mutual
end <- location
pure (pibindAll (MkFC fname start end) Implicit binders scope)
implicitPi : FileName -> IndentInfo -> Rule PTerm
implicitPi : FileName -> IndentInfo -> SourceRule PTerm
implicitPi fname indents
= do start <- location
symbol "{"
@ -506,7 +505,7 @@ mutual
end <- location
pure (pibindAll (MkFC fname start end) Implicit binders scope)
lam : FileName -> IndentInfo -> Rule PTerm
lam : FileName -> IndentInfo -> SourceRule PTerm
lam fname indents
= do start <- location
symbol "\\"
@ -523,7 +522,7 @@ mutual
= PLam fc rig Explicit pat ty (bindAll fc rest scope)
letBinder : FileName -> IndentInfo ->
Rule (FilePos, FilePos, RigCount, PTerm, PTerm, PTerm, List PClause)
SourceRule (FilePos, FilePos, RigCount, PTerm, PTerm, PTerm, List PClause)
letBinder fname indents
= do start <- location
rigc <- multiplicity
@ -562,7 +561,7 @@ mutual
= let fc = MkFC fname start end in
DoLetPat fc pat ty val alts :: buildDoLets fname rest
let_ : FileName -> IndentInfo -> Rule PTerm
let_ : FileName -> IndentInfo -> SourceRule PTerm
let_ fname indents
= do start <- location
keyword "let"
@ -581,7 +580,7 @@ mutual
end <- location
pure (PLocal (MkFC fname start end) (collectDefs (concat ds)) scope)
case_ : FileName -> IndentInfo -> Rule PTerm
case_ : FileName -> IndentInfo -> SourceRule PTerm
case_ fname indents
= do start <- location
keyword "case"
@ -591,7 +590,7 @@ mutual
end <- location
pure (PCase (MkFC fname start end) scr alts)
lambdaCase : FileName -> IndentInfo -> Rule PTerm
lambdaCase : FileName -> IndentInfo -> SourceRule PTerm
lambdaCase fname indents
= do start <- location
symbol "\\" *> keyword "case"
@ -606,13 +605,13 @@ mutual
PLam fcCase top Explicit (PRef fcCase n) (PInfer fcCase) $
PCase fc (PRef fcCase n) alts
caseAlt : FileName -> IndentInfo -> Rule PClause
caseAlt : FileName -> IndentInfo -> SourceRule PClause
caseAlt fname indents
= do start <- location
lhs <- opExpr plhs fname indents
caseRHS fname start indents lhs
caseRHS : FileName -> FilePos -> IndentInfo -> PTerm -> Rule PClause
caseRHS : FileName -> FilePos -> IndentInfo -> PTerm -> SourceRule PClause
caseRHS fname start indents lhs
= do symbol "=>"
mustContinue indents Nothing
@ -625,7 +624,7 @@ mutual
end <- location
pure (MkImpossible (MkFC fname start end) lhs)
if_ : FileName -> IndentInfo -> Rule PTerm
if_ : FileName -> IndentInfo -> SourceRule PTerm
if_ fname indents
= do start <- location
keyword "if"
@ -638,7 +637,7 @@ mutual
end <- location
pure (PIfThenElse (MkFC fname start end) x t e)
record_ : FileName -> IndentInfo -> Rule PTerm
record_ : FileName -> IndentInfo -> SourceRule PTerm
record_ fname indents
= do start <- location
keyword "record"
@ -649,7 +648,7 @@ mutual
end <- location
pure (PUpdate (MkFC fname start end) fs)
field : FileName -> IndentInfo -> Rule PFieldUpdate
field : FileName -> IndentInfo -> SourceRule PFieldUpdate
field fname indents
= do path <- map fieldName <$> [| name :: many recFieldCompat |]
upd <- (do symbol "="; pure PSetField)
@ -665,10 +664,10 @@ mutual
-- this allows the dotted syntax .field
-- but also the arrowed syntax ->field for compatibility with Idris 1
recFieldCompat : Rule Name
recFieldCompat : SourceRule Name
recFieldCompat = recField <|> (symbol "->" *> name)
rewrite_ : FileName -> IndentInfo -> Rule PTerm
rewrite_ : FileName -> IndentInfo -> SourceRule PTerm
rewrite_ fname indents
= do start <- location
keyword "rewrite"
@ -678,7 +677,7 @@ mutual
end <- location
pure (PRewrite (MkFC fname start end) rule tm)
doBlock : FileName -> IndentInfo -> Rule PTerm
doBlock : FileName -> IndentInfo -> SourceRule PTerm
doBlock fname indents
= do start <- location
keyword "do"
@ -690,13 +689,13 @@ mutual
lowerFirst "" = False
lowerFirst str = assert_total (isLower (strHead str))
validPatternVar : Name -> EmptyRule ()
validPatternVar : Name -> EmptySourceRule ()
validPatternVar (UN n)
= if lowerFirst n then pure ()
else fail "Not a pattern variable"
validPatternVar _ = fail "Not a pattern variable"
doAct : FileName -> IndentInfo -> Rule (List PDo)
doAct : FileName -> IndentInfo -> SourceRule (List PDo)
doAct fname indents
= do start <- location
n <- name
@ -736,12 +735,12 @@ mutual
end <- location
pure [DoBindPat (MkFC fname start end) e val alts])
patAlt : FileName -> IndentInfo -> Rule PClause
patAlt : FileName -> IndentInfo -> SourceRule PClause
patAlt fname indents
= do symbol "|"
caseAlt fname indents
lazy : FileName -> IndentInfo -> Rule PTerm
lazy : FileName -> IndentInfo -> SourceRule PTerm
lazy fname indents
= do start <- location
exactIdent "Lazy"
@ -764,7 +763,7 @@ mutual
end <- location
pure (PForce (MkFC fname start end) tm)
binder : FileName -> IndentInfo -> Rule PTerm
binder : FileName -> IndentInfo -> SourceRule PTerm
binder fname indents
= let_ fname indents
<|> autoImplicitPi fname indents
@ -774,7 +773,7 @@ mutual
<|> explicitPi fname indents
<|> lam fname indents
typeExpr : ParseOpts -> FileName -> IndentInfo -> Rule PTerm
typeExpr : ParseOpts -> FileName -> IndentInfo -> SourceRule PTerm
typeExpr q fname indents
= do start <- location
arg <- opExpr q fname indents
@ -793,10 +792,10 @@ mutual
(mkPi start end a as)
export
expr : ParseOpts -> FileName -> IndentInfo -> Rule PTerm
expr : ParseOpts -> FileName -> IndentInfo -> SourceRule PTerm
expr = typeExpr
visOption : Rule Visibility
visOption : SourceRule Visibility
visOption
= do keyword "public"
keyword "export"
@ -806,12 +805,12 @@ visOption
<|> do keyword "private"
pure Private
visibility : EmptyRule Visibility
visibility : EmptySourceRule Visibility
visibility
= visOption
<|> pure Private
tyDecl : FileName -> IndentInfo -> Rule PTypeDecl
tyDecl : FileName -> IndentInfo -> SourceRule PTypeDecl
tyDecl fname indents
= do start <- location
n <- name
@ -825,7 +824,7 @@ tyDecl fname indents
mutual
parseRHS : (withArgs : Nat) ->
FileName -> FilePos -> Int ->
IndentInfo -> (lhs : PTerm) -> Rule PClause
IndentInfo -> (lhs : PTerm) -> SourceRule PClause
parseRHS withArgs fname start col indents lhs
= do symbol "="
mustWork $
@ -846,7 +845,7 @@ mutual
end <- location
pure (MkImpossible (MkFC fname start end) lhs)
clause : Nat -> FileName -> IndentInfo -> Rule PClause
clause : Nat -> FileName -> IndentInfo -> SourceRule PClause
clause withArgs fname indents
= do start <- location
col <- column
@ -860,7 +859,7 @@ mutual
applyArgs f [] = f
applyArgs f ((fc, a) :: args) = applyArgs (PApp fc f a) args
parseWithArg : Rule (FC, PTerm)
parseWithArg : SourceRule (FC, PTerm)
parseWithArg
= do symbol "|"
start <- location
@ -889,7 +888,7 @@ mkDataConType fc ret (WithArg a :: xs)
= PImplicit fc -- This can't happen because we parse constructors without
-- withOK set
simpleCon : FileName -> PTerm -> IndentInfo -> Rule PTypeDecl
simpleCon : FileName -> PTerm -> IndentInfo -> SourceRule PTypeDecl
simpleCon fname ret indents
= do start <- location
cname <- name
@ -899,7 +898,7 @@ simpleCon fname ret indents
let cfc = MkFC fname start end
pure (MkPTy cfc cname (mkDataConType cfc ret params))
simpleData : FileName -> FilePos -> Name -> IndentInfo -> Rule PDataDecl
simpleData : FileName -> FilePos -> Name -> IndentInfo -> SourceRule PDataDecl
simpleData fname start n indents
= do params <- many name
tyend <- location
@ -913,7 +912,7 @@ simpleData fname start n indents
pure (MkPData (MkFC fname start end) n
(mkTyConType tyfc params) [] cons)
dataOpt : Rule DataOpt
dataOpt : SourceRule DataOpt
dataOpt
= do exactIdent "noHints"
pure NoHints
@ -928,7 +927,7 @@ dataOpt
pure NoNewtype
dataBody : FileName -> Int -> FilePos -> Name -> IndentInfo -> PTerm ->
EmptyRule PDataDecl
EmptySourceRule PDataDecl
dataBody fname mincol start n indents ty
= do atEndIndent indents
end <- location
@ -942,14 +941,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 -> Rule PDataDecl
gadtData : FileName -> Int -> FilePos -> Name -> IndentInfo -> SourceRule 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 -> Rule PDataDecl
dataDeclBody : FileName -> IndentInfo -> SourceRule PDataDecl
dataDeclBody fname indents
= do start <- location
col <- column
@ -958,7 +957,7 @@ dataDeclBody fname indents
simpleData fname start n indents
<|> gadtData fname col start n indents
dataDecl : FileName -> IndentInfo -> Rule PDecl
dataDecl : FileName -> IndentInfo -> SourceRule PDecl
dataDecl fname indents
= do start <- location
vis <- visibility
@ -973,19 +972,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 : Rule Bool
onoff : SourceRule Bool
onoff
= do exactIdent "on"
pure True
<|> do exactIdent "off"
pure False
extension : Rule LangExt
extension : SourceRule LangExt
extension
= do exactIdent "Borrowing"
pure Borrowing
totalityOpt : Rule TotalReq
totalityOpt : SourceRule TotalReq
totalityOpt
= do keyword "partial"
pure PartialOK
@ -994,7 +993,7 @@ totalityOpt
<|> do keyword "covering"
pure CoveringOnly
directive : FileName -> IndentInfo -> Rule Directive
directive : FileName -> IndentInfo -> SourceRule Directive
directive fname indents
= do pragma "hide"
n <- name
@ -1069,21 +1068,21 @@ directive fname indents
atEnd indents
pure (DefaultTotality tot)
fix : Rule Fixity
fix : SourceRule Fixity
fix
= do keyword "infixl"; pure InfixL
<|> do keyword "infixr"; pure InfixR
<|> do keyword "infix"; pure Infix
<|> do keyword "prefix"; pure Prefix
namespaceHead : Rule (List String)
namespaceHead : SourceRule (List String)
namespaceHead
= do keyword "namespace"
commit
ns <- nsIdent
pure ns
namespaceDecl : FileName -> IndentInfo -> Rule PDecl
namespaceDecl : FileName -> IndentInfo -> SourceRule PDecl
namespaceDecl fname indents
= do start <- location
ns <- namespaceHead
@ -1091,7 +1090,7 @@ namespaceDecl fname indents
ds <- assert_total (nonEmptyBlock (topDecl fname))
pure (PNamespace (MkFC fname start end) ns (concat ds))
transformDecl : FileName -> IndentInfo -> Rule PDecl
transformDecl : FileName -> IndentInfo -> SourceRule PDecl
transformDecl fname indents
= do start <- location
pragma "transform"
@ -1102,7 +1101,7 @@ transformDecl fname indents
end <- location
pure (PTransform (MkFC fname start end) n lhs rhs)
mutualDecls : FileName -> IndentInfo -> Rule PDecl
mutualDecls : FileName -> IndentInfo -> SourceRule PDecl
mutualDecls fname indents
= do start <- location
keyword "mutual"
@ -1111,7 +1110,7 @@ mutualDecls fname indents
end <- location
pure (PMutual (MkFC fname start end) (concat ds))
paramDecls : FileName -> IndentInfo -> Rule PDecl
paramDecls : FileName -> IndentInfo -> SourceRule PDecl
paramDecls fname indents
= do start <- location
keyword "parameters"
@ -1127,7 +1126,7 @@ paramDecls fname indents
end <- location
pure (PParameters (MkFC fname start end) ps (collectDefs (concat ds)))
usingDecls : FileName -> IndentInfo -> Rule PDecl
usingDecls : FileName -> IndentInfo -> SourceRule PDecl
usingDecls fname indents
= do start <- location
keyword "using"
@ -1145,11 +1144,11 @@ usingDecls fname indents
end <- location
pure (PUsing (MkFC fname start end) us (collectDefs (concat ds)))
fnOpt : Rule PFnOpt
fnOpt : SourceRule PFnOpt
fnOpt = do x <- totalityOpt
pure $ IFnOpt (Totality x)
fnDirectOpt : FileName -> Rule PFnOpt
fnDirectOpt : FileName -> SourceRule PFnOpt
fnDirectOpt fname
= do pragma "hint"
pure $ IFnOpt (Hint True)
@ -1171,7 +1170,7 @@ fnDirectOpt fname
cs <- block (expr pdef fname)
pure $ PForeign cs
visOpt : FileName -> Rule (Either Visibility PFnOpt)
visOpt : FileName -> SourceRule (Either Visibility PFnOpt)
visOpt fname
= do vis <- visOption
pure (Left vis)
@ -1181,7 +1180,7 @@ visOpt fname
pure (Right opt)
getVisibility : Maybe Visibility -> List (Either Visibility PFnOpt) ->
EmptyRule Visibility
EmptySourceRule Visibility
getVisibility Nothing [] = pure Private
getVisibility (Just vis) [] = pure vis
getVisibility Nothing (Left x :: xs) = getVisibility (Just x) xs
@ -1193,7 +1192,7 @@ getRight : Either a b -> Maybe b
getRight (Left _) = Nothing
getRight (Right v) = Just v
constraints : FileName -> IndentInfo -> EmptyRule (List (Maybe Name, PTerm))
constraints : FileName -> IndentInfo -> EmptySourceRule (List (Maybe Name, PTerm))
constraints fname indents
= do tm <- appExpr pdef fname indents
symbol "=>"
@ -1209,7 +1208,7 @@ constraints fname indents
pure ((Just n, tm) :: more)
<|> pure []
implBinds : FileName -> IndentInfo -> EmptyRule (List (Name, RigCount, PTerm))
implBinds : FileName -> IndentInfo -> EmptySourceRule (List (Name, RigCount, PTerm))
implBinds fname indents
= do symbol "{"
m <- multiplicity
@ -1223,7 +1222,7 @@ implBinds fname indents
pure ((n, rig, tm) :: more)
<|> pure []
ifaceParam : FileName -> IndentInfo -> Rule (Name, PTerm)
ifaceParam : FileName -> IndentInfo -> SourceRule (Name, PTerm)
ifaceParam fname indents
= do symbol "("
n <- name
@ -1236,7 +1235,7 @@ ifaceParam fname indents
end <- location
pure (n, PInfer (MkFC fname start end))
ifaceDecl : FileName -> IndentInfo -> Rule PDecl
ifaceDecl : FileName -> IndentInfo -> SourceRule PDecl
ifaceDecl fname indents
= do start <- location
vis <- visibility
@ -1257,7 +1256,7 @@ ifaceDecl fname indents
pure (PInterface (MkFC fname start end)
vis cons n params det dc (collectDefs (concat body)))
implDecl : FileName -> IndentInfo -> Rule PDecl
implDecl : FileName -> IndentInfo -> SourceRule PDecl
implDecl fname indents
= do start <- location
visOpts <- many (visOpt fname)
@ -1284,7 +1283,7 @@ implDecl fname indents
vis opts Single impls cons n params iname nusing
(map (collectDefs . concat) body))
fieldDecl : FileName -> IndentInfo -> Rule (List PField)
fieldDecl : FileName -> IndentInfo -> SourceRule (List PField)
fieldDecl fname indents
= do symbol "{"
commit
@ -1296,7 +1295,7 @@ fieldDecl fname indents
atEnd indents
pure fs
where
fieldBody : PiInfo PTerm -> Rule (List PField)
fieldBody : PiInfo PTerm -> SourceRule (List PField)
fieldBody p
= do start <- location
m <- multiplicity
@ -1308,7 +1307,7 @@ fieldDecl fname indents
end <- location
pure (map (\n => MkField (MkFC fname start end)
rig p n ty) ns)
recordParam : FileName -> IndentInfo -> Rule (List (Name, RigCount, PiInfo PTerm, PTerm))
recordParam : FileName -> IndentInfo -> SourceRule (List (Name, RigCount, PiInfo PTerm, PTerm))
recordParam fname indents
= do symbol "("
start <- location
@ -1317,7 +1316,7 @@ recordParam fname indents
pure $ map (\(c, n, tm) => (n, c, Explicit, tm)) params
<|> do symbol "{"
commit
info <- the (EmptyRule (PiInfo PTerm))
info <- the (EmptySourceRule (PiInfo PTerm))
(pure AutoImplicit <* keyword "auto"
<|>(do
keyword "default"
@ -1333,7 +1332,7 @@ recordParam fname indents
end <- location
pure [(n, top, Explicit, PInfer (MkFC fname start end))]
recordDecl : FileName -> IndentInfo -> Rule PDecl
recordDecl : FileName -> IndentInfo -> SourceRule PDecl
recordDecl fname indents
= do start <- location
vis <- visibility
@ -1348,13 +1347,13 @@ recordDecl fname indents
pure (PRecord (MkFC fname start end)
vis n params (fst dcflds) (concat (snd dcflds)))
where
ctor : IndentInfo -> Rule Name
ctor : IndentInfo -> SourceRule Name
ctor idt = do exactIdent "constructor"
n <- name
atEnd idt
pure n
claim : FileName -> IndentInfo -> Rule PDecl
claim : FileName -> IndentInfo -> SourceRule PDecl
claim fname indents
= do start <- location
visOpts <- many (visOpt fname)
@ -1366,14 +1365,14 @@ claim fname indents
end <- location
pure (PClaim (MkFC fname start end) rig vis opts cl)
definition : FileName -> IndentInfo -> Rule PDecl
definition : FileName -> IndentInfo -> SourceRule PDecl
definition fname indents
= do start <- location
nd <- clause 0 fname indents
end <- location
pure (PDef (MkFC fname start end) [nd])
fixDecl : FileName -> IndentInfo -> Rule (List PDecl)
fixDecl : FileName -> IndentInfo -> SourceRule (List PDecl)
fixDecl fname indents
= do start <- location
fixity <- fix
@ -1383,7 +1382,7 @@ fixDecl fname indents
end <- location
pure (map (PFixity (MkFC fname start end) fixity (cast prec)) ops)
directiveDecl : FileName -> IndentInfo -> Rule PDecl
directiveDecl : FileName -> IndentInfo -> SourceRule PDecl
directiveDecl fname indents
= do start <- location
(do d <- directive fname indents
@ -1397,7 +1396,7 @@ directiveDecl fname indents
pure (PReflect (MkFC fname start end) tm))
-- Declared at the top
-- topDecl : FileName -> IndentInfo -> Rule (List PDecl)
-- topDecl : FileName -> IndentInfo -> SourceRule (List PDecl)
topDecl fname indents
= do d <- dataDecl fname indents
pure [d]
@ -1466,7 +1465,7 @@ collectDefs (d :: ds)
= d :: collectDefs ds
export
import_ : FileName -> IndentInfo -> Rule Import
import_ : FileName -> IndentInfo -> SourceRule Import
import_ fname indents
= do start <- location
keyword "import"
@ -1480,7 +1479,7 @@ import_ fname indents
pure (MkImport (MkFC fname start end) reexp ns nsAs)
export
prog : FileName -> EmptyRule Module
prog : FileName -> EmptySourceRule Module
prog fname
= do start <- location
nspace <- option ["Main"]
@ -1493,7 +1492,7 @@ prog fname
nspace imports (collectDefs (concat ds)))
export
progHdr : FileName -> EmptyRule Module
progHdr : FileName -> EmptySourceRule Module
progHdr fname
= do start <- location
nspace <- option ["Main"]
@ -1504,7 +1503,7 @@ progHdr fname
pure (MkModule (MkFC fname start end)
nspace imports [])
parseMode : Rule REPLEval
parseMode : SourceRule REPLEval
parseMode
= do exactIdent "typecheck"
pure EvalTC
@ -1519,7 +1518,7 @@ parseMode
<|> do exactIdent "exec"
pure Execute
setVarOption : Rule REPLOpt
setVarOption : SourceRule REPLOpt
setVarOption
= do exactIdent "eval"
mode <- parseMode
@ -1531,7 +1530,7 @@ setVarOption
c <- unqualifiedName
pure (CG c)
setOption : Bool -> Rule REPLOpt
setOption : Bool -> SourceRule REPLOpt
setOption set
= do exactIdent "showimplicits"
pure (ShowImplicits set)
@ -1541,7 +1540,7 @@ setOption set
pure (ShowTypes set)
<|> if set then setVarOption else fatalError "Unrecognised option"
replCmd : List String -> Rule ()
replCmd : List String -> SourceRule ()
replCmd [] = fail "Unrecognised command"
replCmd (c :: cs)
= exactIdent c
@ -1549,7 +1548,7 @@ replCmd (c :: cs)
<|> replCmd cs
export
editCmd : Rule EditCmd
editCmd : SourceRule EditCmd
editCmd
= do replCmd ["typeat"]
line <- intLit
@ -1635,7 +1634,7 @@ data ParseCmd : Type where
ParseIdentCmd : String -> ParseCmd
CommandDefinition : Type
CommandDefinition = (List String, CmdArg, String, Rule REPLCmd)
CommandDefinition = (List String, CmdArg, String, SourceRule REPLCmd)
CommandTable : Type
CommandTable = List CommandDefinition
@ -1645,7 +1644,7 @@ extractNames (ParseREPLCmd names) = names
extractNames (ParseKeywordCmd keyword) = [keyword]
extractNames (ParseIdentCmd ident) = [ident]
runParseCmd : ParseCmd -> Rule ()
runParseCmd : ParseCmd -> SourceRule ()
runParseCmd (ParseREPLCmd names) = replCmd names
runParseCmd (ParseKeywordCmd keyword') = keyword keyword'
runParseCmd (ParseIdentCmd ident) = exactIdent ident
@ -1743,17 +1742,17 @@ help : List (List String, CmdArg, String)
help = (["<expr>"], NoArg, "Evaluate an expression") ::
[ (map (":" ++) names, args, text) | (names, args, text, _) <- parserCommandsForHelp ]
nonEmptyCommand : Rule REPLCmd
nonEmptyCommand : SourceRule REPLCmd
nonEmptyCommand =
choice [ parser | (_, _, _, parser) <- parserCommandsForHelp ]
eval : Rule REPLCmd
eval : SourceRule REPLCmd
eval = do
tm <- expr pdef "(interactive)" init
pure (Eval tm)
export
command : EmptyRule REPLCmd
command : EmptySourceRule REPLCmd
command
= do eoi
pure NOP

8
src/Idris/ProcessIdr.idr
View File

@ -192,7 +192,7 @@ modTime fname
pure t
export
getParseErrorLoc : String -> ParseError -> FC
getParseErrorLoc : String -> ParsingError SourceToken -> 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)
@ -204,13 +204,13 @@ readHeader : {auto c : Ref Ctxt Defs} ->
readHeader path
= do Right res <- coreLift (readFile path)
| Left err => throw (FileErr path err)
case runParserTo (isLitFile path) isColon res (progHdr path) of
case runSourceParserTo (isLitFile path) isColon res (progHdr path) of
Left err => throw (ParseFail (getParseErrorLoc path err) err)
Right mod => pure mod
where
-- Stop at the first :, that's definitely not part of the header, to
-- save lexing the whole file unnecessarily
isColon : TokenData Token -> Bool
isColon : TokenData SourceToken -> Bool
isColon t
= case tok t of
Symbol ":" => True
@ -262,7 +262,7 @@ processMod srcf ttcf msg sourcecode
else -- needs rebuilding
do iputStrLn msg
Right mod <- logTime ("Parsing " ++ srcf) $
pure (runParser (isLitFile srcf) sourcecode (do p <- prog srcf; eoi; pure p))
pure (runSourceParser (isLitFile srcf) sourcecode (do p <- prog srcf; eoi; pure p))
| Left err => pure (Just [ParseFail (getParseErrorLoc srcf err) err])
initHash
resetNextVar

8
src/Idris/REPL.idr
View File

@ -733,17 +733,17 @@ processCatch cmd
pure $ REPLError !(display err)
)
parseEmptyCmd : EmptyRule (Maybe REPLCmd)
parseEmptyCmd : EmptySourceRule (Maybe REPLCmd)
parseEmptyCmd = eoi *> (pure Nothing)
parseCmd : EmptyRule (Maybe REPLCmd)
parseCmd : EmptySourceRule (Maybe REPLCmd)
parseCmd = do c <- command; eoi; pure $ Just c
export
parseRepl : String -> Either ParseError (Maybe REPLCmd)
parseRepl : String -> Either (ParsingError SourceToken) (Maybe REPLCmd)
parseRepl inp
= case fnameCmd [(":load ", Load), (":l ", Load), (":cd ", CD)] inp of
Nothing => runParser Nothing inp (parseEmptyCmd <|> parseCmd)
Nothing => runSourceParser Nothing inp (parseEmptyCmd <|> parseCmd)
Just cmd => Right $ Just cmd
where
-- a right load of hackery - we can't tokenise the filename using the

11
src/Parser/Lexer/Common.idr Normal file
View File

@ -0,0 +1,11 @@
module Parser.CommonLexer
%default total
export
dotSep : List String -> String
dotSep [] = ""
dotSep [x] = x
dotSep l@(_::_)
= assert_total $ let rl@(_::_) = reverse l in
head rl ++ concat ["." ++ y | y <- tail rl]

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

@ -0,0 +1,18 @@
module Parser.Lexer.Package
import public Text.Lexer
%default total
public export
data PackageToken
= Assignment
| Comment
| EOF
| PackageName String
| Property String
| Module (List String)
| StringLit String
export
lexPackage : String -> Either (Int, Int, String) (List (TokenData PackageToken))

98
src/Parser/Lexer.idr → src/Parser/Lexer/Source.idr
View File

@ -1,6 +1,8 @@
module Parser.Lexer
module Parser.Lexer.Source
import public Text.Lexer
import Parser.Lexer.Common
import Utils.Hex
import Utils.Octal
import Utils.String
@ -8,45 +10,49 @@ import Utils.String
%default total
public export
data Token = NSIdent (List String)
| HoleIdent String
| Literal Integer
| StrLit String
| CharLit String
data SourceToken
-- Literals
= CharLit String
| DoubleLit Double
| IntegerLit Integer
| StringLit String
-- Identifiers
| HoleIdent String
| NSIdent (List String)
| Symbol String
| Keyword String
| Unrecognised String
-- Comments
| Comment String
| DocComment String
-- Special
| CGDirective String
| RecordField String
| Pragma String
| EndInput
| Keyword String
| Pragma String
| RecordField String
| Unrecognised String
export
Show Token where
show (HoleIdent x) = "hole identifier " ++ x
show (Literal x) = "literal " ++ show x
show (StrLit x) = "string " ++ show x
show (CharLit x) = "character " ++ show x
show (DoubleLit x) = "double " ++ show x
show (Symbol x) = "symbol " ++ x
show (Keyword x) = x
show (Unrecognised x) = "Unrecognised " ++ x
show (Comment _) = "comment"
show (DocComment _) = "doc comment"
show (CGDirective x) = "CGDirective " ++ x
show (RecordField x) = "record field " ++ x
show (Pragma x) = "pragma " ++ x
Show SourceToken where
-- Literals
show (CharLit c) = "character " ++ show c
show (DoubleLit d) = "double " ++ show d
show (IntegerLit n) = "integer " ++ show n
show (StringLit s) = "string " ++ s
-- Identifiers
show (HoleIdent i) = "hole identifier " ++ i
show (NSIdent [i]) = "identifier " ++ i
show (NSIdent ns) = "namespaced identifier " ++ dotSep ns
show (Symbol s) = "symbol " ++ s
-- Comments
show (Comment c) = "comment" ++ c
show (DocComment c) = "doc comment" ++ c
-- Special
show (CGDirective d) = "CGDirective " ++ d
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 k) = k
show (Pragma p) = "pragma " ++ p
show (RecordField f) = "record field " ++ f
show (Unrecognised x) = "Unrecognised " ++ x
||| In `comment` we are careful not to parse closing delimiters as
||| valid comments. i.e. you may not write many dashes followed by
@ -176,7 +182,7 @@ cgDirective
is '}')
<|> many (isNot '\n'))
mkDirective : String -> Token
mkDirective : String -> SourceToken
mkDirective str = CGDirective (trim (substr 3 (length str) str))
-- Reserved words
@ -239,7 +245,7 @@ fromOctLit str
Nothing => 0 -- can't happen if the literal lexed correctly
Just n => cast n
rawTokens : TokenMap Token
rawTokens : TokenMap SourceToken
rawTokens =
[(comment, Comment),
(blockComment, Comment),
@ -248,11 +254,15 @@ 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)),
(charLit, \x => CharLit (stripQuotes x)),
(hexLit, \x => IntegerLit (fromHexLit x)),
(octLit, \x => IntegerLit (fromOctLit x)),
(digits, \x => IntegerLit (cast x)),
(stringLit, \x => case isLTE 2 (length x) of
Yes prf => StringLit (stripQuotes x {ok=prf})
No _ => Unrecognised x),
(charLit, \x => case (isLTE 3 (length x) , isLTE 2 (length x)) of
(Yes _, Yes prf) => CharLit (stripQuotes x {ok=prf})
(_ , _ ) => Unrecognised x),
(recField, \x => RecordField (assert_total $ strTail x)),
(nsIdent, parseNSIdent),
(ident Normal, parseIdent),
@ -261,18 +271,18 @@ rawTokens =
(validSymbol, Symbol),
(symbol, Unrecognised)]
where
parseNSIdent : String -> Token
parseNSIdent : String -> SourceToken
parseNSIdent = NSIdent . reverse . split (== '.')
parseIdent : String -> Token
parseIdent : String -> SourceToken
parseIdent x =
if x `elem` keywords
then Keyword x
else NSIdent [x]
export
lexTo : (TokenData Token -> Bool) ->
String -> Either (Int, Int, String) (List (TokenData Token))
lexTo : (TokenData SourceToken -> Bool) ->
String -> Either (Int, Int, String) (List (TokenData SourceToken))
lexTo pred str
= case lexTo pred rawTokens str of
-- Add the EndInput token so that we'll have a line and column
@ -281,12 +291,12 @@ lexTo pred str
[MkToken l c EndInput])
(_, fail) => Left fail
where
notComment : TokenData Token -> Bool
notComment : TokenData SourceToken -> Bool
notComment t = case tok t of
Comment _ => False
DocComment _ => False -- TODO!
_ => True
export
lex : String -> Either (Int, Int, String) (List (TokenData Token))
lex : String -> Either (Int, Int, String) (List (TokenData SourceToken))
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.Rules.Common
import public Parser.Rules.Package
import public Text.Lexer
import public Text.Parser
import Utils.Either
export
runPackageParser : String -> Grammar (TokenData PackageToken) e ty -> Either (ParsingError PackageToken) ty
runPackageParser str p
= do toks <- mapError LexFail $ lexPackage str
parsed <- mapError mapParseError $ parse p toks
Right (fst parsed)
export
parsePackageFile : (filename : String) -> PackageRule ty -> IO (Either (ParsingError PackageToken) ty)
parsePackageFile filename p
= do Right content <- readFile filename
| Left error => pure (Left (FileFail error))
pure (runPackageParser content p)

20
src/Parser/Rules/Common.idr Normal file
View File

@ -0,0 +1,20 @@
module Parser.Rules.Common
import Text.Lexer
import Text.Parser
public export
EmptyRule : Type -> Type -> Type
EmptyRule token ty = Grammar (TokenData token) False ty
export
location : {token : Type} -> EmptyRule token (Int, Int)
location
= do tok <- peek
pure (line tok, col tok)
export
column : {token : Type} -> EmptyRule token Int
column
= do (line, col) <- location
pure col

44
src/Parser/Rules/Package.idr Normal file
View File

@ -0,0 +1,44 @@
module Parser.Rules.Package
import public Parser.Lexer.Package
import public Parser.Support
import public Text.Lexer
import public Text.Parser
public export
EmptyPackageRule : Type -> Type
EmptyPackageRule ty = Grammar (TokenData PackageToken) False ty
public export
PackageRule : Type -> Type
PackageRule ty = Grammar (TokenData PackageToken) True ty
export
eof : EmptyPackageRule ()
eof = do nextIs "Expected end of file" (isEOF . tok)
pure ()
where
isEOF : PackageToken -> Bool
isEOF EOF = True
isEOF _ = False
export
assignment : PackageRule ()
assignment = terminal "Expected assignment symbol"
(\x => case tok x of
Assignment => Just ()
_ => Nothing)
export
property : String -> PackageRule ()
property p = terminal "Expected property name"
(\x => case tok x of
Property name => if name == p then Just ()
else Nothing
_ => Nothing)
export
string : PackageRule String
string = terminal "Expected a string literal"
(\x => case tok x of
StringLit str => Just str
_ => Nothing)

400
src/Parser/Rules/Source.idr Normal file
View File

@ -0,0 +1,400 @@
module Parser.Rules.Source
import public Parser.Rules.Common
import Core.TT
import Data.List.Views
import Parser.Lexer.Source
import Parser.Support
import Parser.Unlit
import Text.Lexer
import Text.Parser
public export
EmptySourceRule : Type -> Type
EmptySourceRule ty = Grammar (TokenData SourceToken) False ty
public export
SourceRule : Type -> Type
SourceRule ty = Grammar (TokenData SourceToken) True ty
export
eoi : EmptySourceRule ()
eoi
= do nextIs "Expected end of input" (isEOI . tok)
pure ()
where
isEOI : SourceToken -> Bool
isEOI EndInput = True
isEOI _ = False
export
constant : SourceRule Constant
constant
= terminal "Expected constant"
(\x => case tok x of
IntegerLit n => Just (BI n)
StringLit s => Str <$> escape s
CharLit c => Ch <$> getCharLit 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
_ => Nothing)
export
intLit : SourceRule Integer
intLit
= terminal "Expected integer literal"
(\x => case tok x of
IntegerLit n => Just n
_ => Nothing)
export
strLit : SourceRule String
strLit
= terminal "Expected string literal"
(\x => case tok x of
StringLit s => Just s
_ => Nothing)
export
recField : SourceRule Name
recField
= terminal "Expected record field"
(\x => case tok x of
RecordField s => Just (RF s)
_ => Nothing)
export
symbol : String -> SourceRule ()
symbol req
= terminal ("Expected '" ++ req ++ "'")
(\x => case tok x of
Symbol s => if s == req then Just ()
else Nothing
_ => Nothing)
export
keyword : String -> SourceRule ()
keyword req
= terminal ("Expected '" ++ req ++ "'")
(\x => case tok x of
Keyword s => if s == req then Just ()
else Nothing
_ => Nothing)
export
exactIdent : String -> SourceRule ()
exactIdent req
= terminal ("Expected " ++ req)
(\x => case tok x of
NSIdent [s] => if s == req then Just ()
else Nothing
_ => Nothing)
export
pragma : String -> SourceRule ()
pragma n =
terminal ("Expected pragma " ++ n)
(\x => case tok x of
Pragma s =>
if s == n
then Just ()
else Nothing
_ => Nothing)
export
operator : SourceRule Name
operator
= terminal "Expected operator"
(\x => case tok x of
Symbol s =>
if s `elem` reservedSymbols
then Nothing
else Just (UN s)
_ => Nothing)
identPart : SourceRule String
identPart
= terminal "Expected name"
(\x => case tok x of
NSIdent [str] => Just str
_ => Nothing)
export
nsIdent : SourceRule (List String)
nsIdent
= terminal "Expected namespaced name"
(\x => case tok x of
NSIdent ns => Just ns
_ => Nothing)
export
unqualifiedName : SourceRule String
unqualifiedName = identPart
export
holeName : SourceRule String
holeName
= terminal "Expected hole name"
(\x => case tok x of
HoleIdent str => Just str
_ => Nothing)
reservedNames : List String
reservedNames
= ["Type", "Int", "Integer", "String", "Char", "Double",
"Lazy", "Inf", "Force", "Delay"]
export
name : SourceRule Name
name = opNonNS <|> do
ns <- nsIdent
opNS ns <|> nameNS ns
where
reserved : String -> Bool
reserved n = n `elem` reservedNames
nameNS : List String -> Grammar (TokenData SourceToken) False Name
nameNS [] = pure $ UN "IMPOSSIBLE"
nameNS [x] =
if reserved x
then fail $ "can't use reserved name " ++ x
else pure $ UN x
nameNS (x :: xs) =
if reserved x
then fail $ "can't use reserved name " ++ x
else pure $ NS xs (UN x)
opNonNS : SourceRule Name
opNonNS = symbol "(" *> (operator <|> recField) <* symbol ")"
opNS : List String -> SourceRule Name
opNS ns = do
symbol ".("
n <- (operator <|> recField)
symbol ")"
pure (NS ns n)
export
IndentInfo : Type
IndentInfo = Int
export
init : IndentInfo
init = 0
continueF : EmptySourceRule () -> (indent : IndentInfo) -> EmptySourceRule ()
continueF err indent
= do eoi; err
<|> do keyword "where"; err
<|> do col <- column
if (col <= indent)
then err
else pure ()
||| Fail if this is the end of a block entry or end of file
export
continue : (indent : IndentInfo) -> EmptySourceRule ()
continue = continueF (fail "Unexpected end of expression")
||| As 'continue' but failing is fatal (i.e. entire parse fails)
export
mustContinue : (indent : IndentInfo) -> Maybe String -> EmptySourceRule ()
mustContinue indent Nothing
= continueF (fatalError "Unexpected end of expression") indent
mustContinue indent (Just req)
= continueF (fatalError ("Expected '" ++ req ++ "'")) indent
data ValidIndent =
||| In {}, entries can begin in any column
AnyIndent |
||| Entry must begin in a specific column
AtPos Int |
||| Entry can begin in this column or later
AfterPos Int |
||| Block is finished
EndOfBlock
Show ValidIndent where
show AnyIndent = "[any]"
show (AtPos i) = "[col " ++ show i ++ "]"
show (AfterPos i) = "[after " ++ show i ++ "]"
show EndOfBlock = "[EOB]"
checkValid : ValidIndent -> Int -> EmptySourceRule ()
checkValid AnyIndent c = pure ()
checkValid (AtPos x) c = if c == x
then pure ()
else fail "Invalid indentation"
checkValid (AfterPos x) c = if c >= x
then pure ()
else fail "Invalid indentation"
checkValid EndOfBlock c = fail "End of block"
||| Any token which indicates the end of a statement/block
isTerminator : SourceToken -> Bool
isTerminator (Symbol ",") = True
isTerminator (Symbol "]") = True
isTerminator (Symbol ";") = True
isTerminator (Symbol "}") = True
isTerminator (Symbol ")") = True
isTerminator (Symbol "|") = True
isTerminator (Keyword "in") = True
isTerminator (Keyword "then") = True
isTerminator (Keyword "else") = True
isTerminator (Keyword "where") = True
isTerminator EndInput = True
isTerminator _ = False
||| Check we're at the end of a block entry, given the start column
||| of the block.
||| It's the end if we have a terminating token, or the next token starts
||| in or before indent. Works by looking ahead but not consuming.
export
atEnd : (indent : IndentInfo) -> EmptySourceRule ()
atEnd indent
= eoi
<|> do nextIs "Expected end of block" (isTerminator . tok)
pure ()
<|> do col <- column
if (col <= indent)
then pure ()
else fail "Not the end of a block entry"
-- Check we're at the end, but only by looking at indentation
export
atEndIndent : (indent : IndentInfo) -> EmptySourceRule ()
atEndIndent indent
= eoi
<|> do col <- column
if (col <= indent)
then pure ()
else fail "Not the end of a block entry"
-- Parse a terminator, return where the next block entry
-- must start, given where the current block entry started
terminator : ValidIndent -> Int -> EmptySourceRule ValidIndent
terminator valid laststart
= do eoi
pure EndOfBlock
<|> do symbol ";"
pure (afterSemi valid)
<|> do col <- column
afterDedent valid col
<|> pure EndOfBlock
where
-- Expected indentation for the next token can either be anything (if
-- we're inside a brace delimited block) or anywhere after the initial
-- column (if we're inside an indentation delimited block)
afterSemi : ValidIndent -> ValidIndent
afterSemi AnyIndent = AnyIndent -- in braces, anything goes
afterSemi (AtPos c) = AfterPos c -- not in braces, after the last start position
afterSemi (AfterPos c) = AfterPos c
afterSemi EndOfBlock = EndOfBlock
-- Expected indentation for the next token can either be anything (if
-- we're inside a brace delimited block) or in exactly the initial column
-- (if we're inside an indentation delimited block)
afterDedent : ValidIndent -> Int -> EmptySourceRule ValidIndent
afterDedent AnyIndent col
= if col <= laststart
then pure AnyIndent
else fail "Not the end of a block entry"
afterDedent (AfterPos c) col
= if col <= laststart
then pure (AtPos c)
else fail "Not the end of a block entry"
afterDedent (AtPos c) col
= if col <= laststart
then pure (AtPos c)
else fail "Not the end of a block entry"
afterDedent EndOfBlock col = pure EndOfBlock
-- Parse an entry in a block
blockEntry : ValidIndent -> (IndentInfo -> SourceRule ty) ->
SourceRule (ty, ValidIndent)
blockEntry valid rule
= do col <- column
checkValid valid col
p <- rule col
valid' <- terminator valid col
pure (p, valid')
blockEntries : ValidIndent -> (IndentInfo -> SourceRule ty) ->
EmptySourceRule (List ty)
blockEntries valid rule
= do eoi; pure []
<|> do res <- blockEntry valid rule
ts <- blockEntries (snd res) rule
pure (fst res :: ts)
<|> pure []
export
block : (IndentInfo -> SourceRule ty) -> EmptySourceRule (List ty)
block item
= do symbol "{"
commit
ps <- blockEntries AnyIndent item
symbol "}"
pure ps
<|> do col <- column
blockEntries (AtPos col) item
||| `blockAfter col rule` parses a `rule`-block indented by at
||| least `col` spaces (unless the block is explicitly delimited
||| by curly braces). `rule` is a function of the actual indentation
||| level.
export
blockAfter : Int -> (IndentInfo -> SourceRule ty) -> EmptySourceRule (List ty)
blockAfter mincol item
= do symbol "{"
commit
ps <- blockEntries AnyIndent item
symbol "}"
pure ps
<|> do col <- column
if col <= mincol
then pure []
else blockEntries (AtPos col) item
export
blockWithOptHeaderAfter : Int -> (IndentInfo -> SourceRule hd) -> (IndentInfo -> SourceRule ty) -> EmptySourceRule (Maybe hd, List ty)
blockWithOptHeaderAfter {ty} mincol header item
= do symbol "{"
commit
hidt <- optional $ blockEntry AnyIndent header
restOfBlock hidt
<|> do col <- column
if col <= mincol
then pure (Nothing, [])
else do hidt <- optional $ blockEntry (AtPos col) header
ps <- blockEntries (AtPos col) item
pure (map fst hidt, ps)
where
restOfBlock : Maybe (hd, ValidIndent) -> SourceRule (Maybe hd, List ty)
restOfBlock (Just (h, idt)) = do ps <- blockEntries idt item
symbol "}"
pure (Just h, ps)
restOfBlock Nothing = do ps <- blockEntries AnyIndent item
symbol "}"
pure (Nothing, ps)
export
nonEmptyBlock : (IndentInfo -> SourceRule ty) -> SourceRule (List ty)
nonEmptyBlock item
= do symbol "{"
commit
res <- blockEntry AnyIndent item
ps <- blockEntries (snd res) item
symbol "}"
pure (fst res :: ps)
<|> do col <- column
res <- blockEntry (AtPos col) item
ps <- blockEntries (snd res) item
pure (fst res :: ps)

31
src/Parser/Source.idr Normal file
View File

@ -0,0 +1,31 @@
module Parser.Source
import public Parser.Lexer.Source
import public Parser.Rules.Source
import public Parser.Support
import public Text.Lexer
import public Text.Literate
import public Text.Parser
import Utils.Either
export
runSourceParserTo : Maybe LiterateStyle -> (TokenData SourceToken -> Bool) ->
String -> Grammar (TokenData SourceToken) e ty -> Either (ParsingError SourceToken) ty
runSourceParserTo lit pred str p
= do str <- mapError LitFail $ unlit lit str
toks <- mapError LexFail $ lexTo pred str
parsed <- mapError mapParseError $ parse p toks
Right (fst parsed)
export
runSourceParser : Maybe LiterateStyle -> String -> Grammar (TokenData SourceToken) e ty -> Either (ParsingError SourceToken) ty
runSourceParser lit = runSourceParserTo lit (const False)
export
parseSourceFile : (filename : String) -> SourceRule ty -> IO (Either (ParsingError SourceToken) ty)
parseSourceFile filename p
= do Right content <- readFile filename
| Left error => pure (Left (FileFail error))
pure (runSourceParser (isLitFile filename) content p)

443
src/Parser/Support.idr
View File

@ -1,32 +1,22 @@
module Parser.Support
import public Text.Lexer
import public Parser.Lexer
import public Parser.Unlit
import public Text.Parser
import public Parser.Unlit
import Core.TT
import Data.List.Views
import Utils.Either
%default total
public export
Rule : Type -> Type
Rule ty = Grammar (TokenData Token) True ty
public export
EmptyRule : Type -> Type
EmptyRule ty = Grammar (TokenData Token) False ty
public export
data ParseError = ParseFail String (Maybe (Int, Int)) (List Token)
data ParsingError token
= ParseFail String (Maybe (Int, Int)) (List token)
| LexFail (Int, Int, String)
| FileFail FileError
| LitFail LiterateError
export
Show ParseError where
Show token => Show (ParsingError token) where
show (ParseFail err loc toks)
= "Parse error: " ++ err ++ " (next tokens: "
++ show (take 10 toks) ++ ")"
@ -38,53 +28,9 @@ Show ParseError where
= "Lit error(s) at " ++ show (c, l) ++ " input: " ++ str
export
eoi : EmptyRule ()
eoi
= do nextIs "Expected end of input" (isEOI . tok)
pure ()
where
isEOI : Token -> Bool
isEOI EndInput = True
isEOI _ = False
export
mapParseError : ParseError (TokenData Token) -> ParseError
mapParseError : ParseError (TokenData tokens) -> ParsingError tokens
mapParseError (Error err []) = ParseFail err Nothing []
mapParseError (Error err (t::ts)) = ParseFail err (Just (line t, col t)) (map tok (t::ts))
export
runParserTo : Maybe LiterateStyle -> (TokenData Token -> Bool) ->
String -> Grammar (TokenData Token) e ty -> Either ParseError 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
Right (fst parsed)
export
runParser : Maybe LiterateStyle -> String -> Grammar (TokenData Token) e ty -> Either ParseError ty
runParser lit = runParserTo lit (const False)
export
parseFile : (fn : String) -> Rule ty -> IO (Either ParseError ty)
parseFile fn p
= do Right str <- readFile fn
| Left err => pure (Left (FileFail err))
pure (runParser (isLitFile fn) str p)
-- Some basic parsers used by all the intermediate forms
export
location : EmptyRule (Int, Int)
location
= do tok <- peek
pure (line tok, col tok)
export
column : EmptyRule Int
column
= do (line, col) <- location
pure col
mapParseError (Error err ts@(t::_)) = ParseFail err (Just (line t, col t)) (map tok ts)
hex : Char -> Maybe Int
hex '0' = Just 0
@ -216,9 +162,11 @@ escape' ('\\' :: xs)
!(assert_total (escape' rest))
escape' (x :: xs) = Just $ x :: !(escape' xs)
export
escape : String -> Maybe String
escape x = pure $ pack !(escape' (unpack x))
export
getCharLit : String -> Maybe Char
getCharLit str
= do e <- escape str
@ -227,378 +175,3 @@ getCharLit str
else if length e == 0 -- parsed the NULL character that terminated the string!
then Just '\0000'
else Nothing
export
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
_ => Nothing)
export
intLit : Rule Integer
intLit
= terminal "Expected integer literal"
(\x => case tok x of
Literal i => Just i
_ => Nothing)
export
strLit : Rule String
strLit
= terminal "Expected string literal"
(\x => case tok x of
StrLit s => Just s
_ => Nothing)
export
recField : Rule Name
recField
= terminal "Expected record field"
(\x => case tok x of
RecordField s => Just (RF s)
_ => Nothing)
export
symbol : String -> Rule ()
symbol req
= terminal ("Expected '" ++ req ++ "'")
(\x => case tok x of
Symbol s => if s == req then Just ()
else Nothing
_ => Nothing)
export
keyword : String -> Rule ()
keyword req
= terminal ("Expected '" ++ req ++ "'")
(\x => case tok x of
Keyword s => if s == req then Just ()
else Nothing
_ => Nothing)
export
exactIdent : String -> Rule ()
exactIdent req
= terminal ("Expected " ++ req)
(\x => case tok x of
NSIdent [s] => if s == req then Just ()
else Nothing
_ => Nothing)
export
pragma : String -> Rule ()
pragma n =
terminal ("Expected pragma " ++ n)
(\x => case tok x of
Pragma s =>
if s == n
then Just ()
else Nothing
_ => Nothing)
export
operator : Rule Name
operator
= terminal "Expected operator"
(\x => case tok x of
Symbol s =>
if s `elem` reservedSymbols
then Nothing
else Just (UN s)
_ => Nothing)
identPart : Rule String
identPart
= terminal "Expected name"
(\x => case tok x of
NSIdent [str] => Just str
_ => Nothing)
export
nsIdent : Rule (List String)
nsIdent
= terminal "Expected namespaced name"
(\x => case tok x of
NSIdent ns => Just ns
_ => Nothing)
export
unqualifiedName : Rule String
unqualifiedName = identPart
export
holeName : Rule String
holeName
= terminal "Expected hole name"
(\x => case tok x of
HoleIdent str => Just str
_ => Nothing)
reservedNames : List String
reservedNames
= ["Type", "Int", "Integer", "String", "Char", "Double",
"Lazy", "Inf", "Force", "Delay"]
export
name : Rule Name
name = opNonNS <|> do
ns <- nsIdent
opNS ns <|> nameNS ns
where
reserved : String -> Bool
reserved n = n `elem` reservedNames
nameNS : List String -> Grammar (TokenData Token) False Name
nameNS [] = pure $ UN "IMPOSSIBLE"
nameNS [x] =
if reserved x
then fail $ "can't use reserved name " ++ x
else pure $ UN x
nameNS (x :: xs) =
if reserved x
then fail $ "can't use reserved name " ++ x
else pure $ NS xs (UN x)
opNonNS : Rule Name
opNonNS = symbol "(" *> (operator <|> recField) <* symbol ")"
opNS : List String -> Rule Name
opNS ns = do
symbol ".("
n <- (operator <|> recField)
symbol ")"
pure (NS ns n)
export
IndentInfo : Type
IndentInfo = Int
export
init : IndentInfo
init = 0
continueF : EmptyRule () -> (indent : IndentInfo) -> EmptyRule ()
continueF err indent
= do eoi; err
<|> do keyword "where"; err
<|> do col <- column
if (col <= indent)
then err
else pure ()
||| Fail if this is the end of a block entry or end of file
export
continue : (indent : IndentInfo) -> EmptyRule ()
continue = continueF (fail "Unexpected end of expression")
||| As 'continue' but failing is fatal (i.e. entire parse fails)
export
mustContinue : (indent : IndentInfo) -> Maybe String -> EmptyRule ()
mustContinue indent Nothing
= continueF (fatalError "Unexpected end of expression") indent
mustContinue indent (Just req)
= continueF (fatalError ("Expected '" ++ req ++ "'")) indent
data ValidIndent =
||| In {}, entries can begin in any column
AnyIndent |
||| Entry must begin in a specific column
AtPos Int |
||| Entry can begin in this column or later
AfterPos Int |
||| Block is finished
EndOfBlock
Show ValidIndent where
show AnyIndent = "[any]"
show (AtPos i) = "[col " ++ show i ++ "]"
show (AfterPos i) = "[after " ++ show i ++ "]"
show EndOfBlock = "[EOB]"
checkValid : ValidIndent -> Int -> EmptyRule ()
checkValid AnyIndent c = pure ()
checkValid (AtPos x) c = if c == x
then pure ()
else fail "Invalid indentation"
checkValid (AfterPos x) c = if c >= x
then pure ()
else fail "Invalid indentation"
checkValid EndOfBlock c = fail "End of block"
||| Any token which indicates the end of a statement/block
isTerminator : Token -> Bool
isTerminator (Symbol ",") = True
isTerminator (Symbol "]") = True
isTerminator (Symbol ";") = True
isTerminator (Symbol "}") = True
isTerminator (Symbol ")") = True
isTerminator (Symbol "|") = True
isTerminator (Keyword "in") = True
isTerminator (Keyword "then") = True
isTerminator (Keyword "else") = True
isTerminator (Keyword "where") = True
isTerminator EndInput = True
isTerminator _ = False
||| Check we're at the end of a block entry, given the start column
||| of the block.
||| It's the end if we have a terminating token, or the next token starts
||| in or before indent. Works by looking ahead but not consuming.
export
atEnd : (indent : IndentInfo) -> EmptyRule ()
atEnd indent
= eoi
<|> do nextIs "Expected end of block" (isTerminator . tok)
pure ()
<|> do col <- column
if (col <= indent)
then pure ()
else fail "Not the end of a block entry"
-- Check we're at the end, but only by looking at indentation
export
atEndIndent : (indent : IndentInfo) -> EmptyRule ()
atEndIndent indent
= eoi
<|> do col <- column
if (col <= indent)
then pure ()
else fail "Not the end of a block entry"
-- Parse a terminator, return where the next block entry
-- must start, given where the current block entry started
terminator : ValidIndent -> Int -> EmptyRule ValidIndent
terminator valid laststart
= do eoi
pure EndOfBlock
<|> do symbol ";"
pure (afterSemi valid)
<|> do col <- column
afterDedent valid col
<|> pure EndOfBlock
where
-- Expected indentation for the next token can either be anything (if
-- we're inside a brace delimited block) or anywhere after the initial
-- column (if we're inside an indentation delimited block)
afterSemi : ValidIndent -> ValidIndent
afterSemi AnyIndent = AnyIndent -- in braces, anything goes
afterSemi (AtPos c) = AfterPos c -- not in braces, after the last start position
afterSemi (AfterPos c) = AfterPos c
afterSemi EndOfBlock = EndOfBlock
-- Expected indentation for the next token can either be anything (if
-- we're inside a brace delimited block) or in exactly the initial column
-- (if we're inside an indentation delimited block)
afterDedent : ValidIndent -> Int -> EmptyRule ValidIndent
afterDedent AnyIndent col
= if col <= laststart
then pure AnyIndent
else fail "Not the end of a block entry"
afterDedent (AfterPos c) col
= if col <= laststart
then pure (AtPos c)
else fail "Not the end of a block entry"
afterDedent (AtPos c) col
= if col <= laststart
then pure (AtPos c)
else fail "Not the end of a block entry"
afterDedent EndOfBlock col = pure EndOfBlock
-- Parse an entry in a block
blockEntry : ValidIndent -> (IndentInfo -> Rule ty) ->
Rule (ty, ValidIndent)
blockEntry valid rule
= do col <- column
checkValid valid col
p <- rule col
valid' <- terminator valid col
pure (p, valid')
blockEntries : ValidIndent -> (IndentInfo -> Rule ty) ->
EmptyRule (List ty)
blockEntries valid rule
= do eoi; pure []
<|> do res <- blockEntry valid rule
ts <- blockEntries (snd res) rule
pure (fst res :: ts)
<|> pure []
export
block : (IndentInfo -> Rule ty) -> EmptyRule (List ty)
block item
= do symbol "{"
commit
ps <- blockEntries AnyIndent item
symbol "}"
pure ps
<|> do col <- column
blockEntries (AtPos col) item
||| `blockAfter col rule` parses a `rule`-block indented by at
||| least `col` spaces (unless the block is explicitly delimited
||| by curly braces). `rule` is a function of the actual indentation
||| level.
export
blockAfter : Int -> (IndentInfo -> Rule ty) -> EmptyRule (List ty)
blockAfter mincol item
= do symbol "{"
commit
ps <- blockEntries AnyIndent item
symbol "}"
pure ps
<|> do col <- column
if col <= mincol
then pure []
else blockEntries (AtPos col) item
export
blockWithOptHeaderAfter : Int -> (IndentInfo -> Rule hd) -> (IndentInfo -> Rule ty) -> EmptyRule (Maybe hd, List ty)
blockWithOptHeaderAfter {ty} mincol header item
= do symbol "{"
commit
hidt <- optional $ blockEntry AnyIndent header
restOfBlock hidt
<|> do col <- column
if col <= mincol
then pure (Nothing, [])
else do hidt <- optional $ blockEntry (AtPos col) header
ps <- blockEntries (AtPos col) item
pure (map fst hidt, ps)
where
restOfBlock : Maybe (hd, ValidIndent) -> Rule (Maybe hd, List ty)
restOfBlock (Just (h, idt)) = do ps <- blockEntries idt item
symbol "}"
pure (Just h, ps)
restOfBlock Nothing = do ps <- blockEntries AnyIndent item
symbol "}"
pure (Nothing, ps)
export
nonEmptyBlock : (IndentInfo -> Rule ty) -> Rule (List ty)
nonEmptyBlock item
= do symbol "{"
commit
res <- blockEntry AnyIndent item
ps <- blockEntries (snd res) item
symbol "}"
pure (fst res :: ps)
<|> do col <- column
res <- blockEntry (AtPos col) item
ps <- blockEntries (snd res) item
pure (fst res :: ps)

2
src/TTImp/Interactive/GenerateDef.idr
View File

@ -10,7 +10,7 @@ import Core.TT
import Core.Unify
import Core.Value
import Parser.Lexer
import Parser.Lexer.Source
import TTImp.Elab
import TTImp.Elab.Check

112
src/TTImp/Parser.idr
View File

@ -4,16 +4,18 @@ import Core.Context
import Core.Core
import Core.Env
import Core.TT
import Parser.Support
import Parser.Source
import TTImp.TTImp
topDecl : FileName -> IndentInfo -> Rule ImpDecl
topDecl : FileName -> IndentInfo -> SourceRule ImpDecl
-- All the clauses get parsed as one-clause definitions. Collect any
-- neighbouring clauses with the same function name into one definition.
export
collectDefs : List ImpDecl -> List ImpDecl
atom : FileName -> Rule RawImp
atom : FileName -> SourceRule RawImp
atom fname
= do start <- location
x <- constant
@ -49,7 +51,7 @@ atom fname
end <- location
pure (IHole (MkFC fname start end) x)
visOption : Rule Visibility
visOption : SourceRule Visibility
visOption
= do keyword "public"
keyword "export"
@ -59,12 +61,12 @@ visOption
<|> do keyword "private"
pure Private
visibility : EmptyRule Visibility
visibility : EmptySourceRule Visibility
visibility
= visOption
<|> pure Private
totalityOpt : Rule TotalReq
totalityOpt : SourceRule TotalReq
totalityOpt
= do keyword "partial"
pure PartialOK
@ -73,11 +75,11 @@ totalityOpt
<|> do keyword "covering"
pure CoveringOnly
fnOpt : Rule FnOpt
fnOpt : SourceRule FnOpt
fnOpt = do x <- totalityOpt
pure $ Totality x
fnDirectOpt : Rule FnOpt
fnDirectOpt : SourceRule FnOpt
fnDirectOpt
= do pragma "hint"
pure (Hint True)
@ -92,7 +94,7 @@ fnDirectOpt
<|> do pragma "extern"
pure ExternFn
visOpt : Rule (Either Visibility FnOpt)
visOpt : SourceRule (Either Visibility FnOpt)
visOpt
= do vis <- visOption
pure (Left vis)
@ -102,7 +104,7 @@ visOpt
pure (Right opt)
getVisibility : Maybe Visibility -> List (Either Visibility FnOpt) ->
EmptyRule Visibility
EmptySourceRule Visibility
getVisibility Nothing [] = pure Private
getVisibility (Just vis) [] = pure vis
getVisibility Nothing (Left x :: xs) = getVisibility (Just x) xs
@ -114,7 +116,7 @@ getRight : Either a b -> Maybe b
getRight (Left _) = Nothing
getRight (Right v) = Just v
bindSymbol : Rule (PiInfo RawImp)
bindSymbol : SourceRule (PiInfo RawImp)
bindSymbol
= do symbol "->"
pure Explicit
@ -122,7 +124,7 @@ bindSymbol
pure AutoImplicit
mutual
appExpr : FileName -> IndentInfo -> Rule RawImp
appExpr : FileName -> IndentInfo -> SourceRule RawImp
appExpr fname indents
= case_ fname indents
<|> lazy fname indents
@ -142,7 +144,7 @@ mutual
= applyExpImp start end (IImplicitApp (MkFC fname start end) f n imp) args
argExpr : FileName -> IndentInfo ->
Rule (Either RawImp (Maybe Name, RawImp))
SourceRule (Either RawImp (Maybe Name, RawImp))
argExpr fname indents
= do continue indents
arg <- simpleExpr fname indents
@ -151,7 +153,7 @@ mutual
arg <- implicitArg fname indents
pure (Right arg)
implicitArg : FileName -> IndentInfo -> Rule (Maybe Name, RawImp)
implicitArg : FileName -> IndentInfo -> SourceRule (Maybe Name, RawImp)
implicitArg fname indents
= do start <- location
symbol "{"
@ -170,7 +172,7 @@ mutual
symbol "}"
pure (Nothing, tm)
as : FileName -> IndentInfo -> Rule RawImp
as : FileName -> IndentInfo -> SourceRule RawImp
as fname indents
= do start <- location
x <- unqualifiedName
@ -179,7 +181,7 @@ mutual
end <- location
pure (IAs (MkFC fname start end) UseRight (UN x) pat)
simpleExpr : FileName -> IndentInfo -> Rule RawImp
simpleExpr : FileName -> IndentInfo -> SourceRule RawImp
simpleExpr fname indents
= as fname indents
<|> atom fname
@ -191,13 +193,13 @@ mutual
symbol ")"
pure e
multiplicity : EmptyRule (Maybe Integer)
multiplicity : EmptySourceRule (Maybe Integer)
multiplicity
= do c <- intLit
pure (Just c)
<|> pure Nothing
getMult : Maybe Integer -> EmptyRule RigCount
getMult : Maybe Integer -> EmptySourceRule RigCount
getMult (Just 0) = pure erased
getMult (Just 1) = pure linear
getMult Nothing = pure top
@ -210,7 +212,7 @@ mutual
= IPi fc rig p n ty (pibindAll fc p rest scope)
bindList : FileName -> FilePos -> IndentInfo ->
Rule (List (RigCount, Name, RawImp))
SourceRule (List (RigCount, Name, RawImp))
bindList fname start indents
= sepBy1 (symbol ",")
(do rigc <- multiplicity
@ -225,7 +227,7 @@ mutual
pibindListName : FileName -> FilePos -> IndentInfo ->
Rule (List (RigCount, Name, RawImp))
SourceRule (List (RigCount, Name, RawImp))
pibindListName fname start indents
= do rigc <- multiplicity
ns <- sepBy1 (symbol ",") unqualifiedName
@ -243,13 +245,13 @@ mutual
pure (rig, n, ty))
pibindList : FileName -> FilePos -> IndentInfo ->
Rule (List (RigCount, Maybe Name, RawImp))
SourceRule (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 -> Rule RawImp
autoImplicitPi : FileName -> IndentInfo -> SourceRule RawImp
autoImplicitPi fname indents
= do start <- location
symbol "{"
@ -262,7 +264,7 @@ mutual
end <- location
pure (pibindAll (MkFC fname start end) AutoImplicit binders scope)
forall_ : FileName -> IndentInfo -> Rule RawImp
forall_ : FileName -> IndentInfo -> SourceRule RawImp
forall_ fname indents
= do start <- location
keyword "forall"
@ -277,7 +279,7 @@ mutual
end <- location
pure (pibindAll (MkFC fname start end) Implicit binders scope)
implicitPi : FileName -> IndentInfo -> Rule RawImp
implicitPi : FileName -> IndentInfo -> SourceRule RawImp
implicitPi fname indents
= do start <- location
symbol "{"
@ -288,7 +290,7 @@ mutual
end <- location
pure (pibindAll (MkFC fname start end) Implicit binders scope)
explicitPi : FileName -> IndentInfo -> Rule RawImp
explicitPi : FileName -> IndentInfo -> SourceRule RawImp
explicitPi fname indents
= do start <- location
symbol "("
@ -299,7 +301,7 @@ mutual
end <- location
pure (pibindAll (MkFC fname start end) exp binders scope)
lam : FileName -> IndentInfo -> Rule RawImp
lam : FileName -> IndentInfo -> SourceRule RawImp
lam fname indents
= do start <- location
symbol "\\"
@ -315,7 +317,7 @@ mutual
bindAll fc ((rig, n, ty) :: rest) scope
= ILam fc rig Explicit (Just n) ty (bindAll fc rest scope)
let_ : FileName -> IndentInfo -> Rule RawImp
let_ : FileName -> IndentInfo -> SourceRule RawImp
let_ fname indents
= do start <- location
keyword "let"
@ -340,7 +342,7 @@ mutual
end <- location
pure (ILocal (MkFC fname start end) (collectDefs ds) scope)
case_ : FileName -> IndentInfo -> Rule RawImp
case_ : FileName -> IndentInfo -> SourceRule RawImp
case_ fname indents
= do start <- location
keyword "case"
@ -351,14 +353,14 @@ mutual
let fc = MkFC fname start end
pure (ICase fc scr (Implicit fc False) alts)
caseAlt : FileName -> IndentInfo -> Rule ImpClause
caseAlt : FileName -> IndentInfo -> SourceRule ImpClause
caseAlt fname indents
= do start <- location
lhs <- appExpr fname indents
caseRHS fname indents start lhs
caseRHS : FileName -> IndentInfo -> (Int, Int) -> RawImp ->
Rule ImpClause
SourceRule ImpClause
caseRHS fname indents start lhs
= do symbol "=>"
continue indents
@ -371,7 +373,7 @@ mutual
end <- location
pure (ImpossibleClause (MkFC fname start end) lhs)
record_ : FileName -> IndentInfo -> Rule RawImp
record_ : FileName -> IndentInfo -> SourceRule RawImp
record_ fname indents
= do start <- location
keyword "record"
@ -383,7 +385,7 @@ mutual
end <- location
pure (IUpdate (MkFC fname start end) fs sc)
field : FileName -> IndentInfo -> Rule IFieldUpdate
field : FileName -> IndentInfo -> SourceRule IFieldUpdate
field fname indents
= do path <- sepBy1 (symbol "->") unqualifiedName
upd <- (do symbol "="; pure ISetField)
@ -392,7 +394,7 @@ mutual
val <- appExpr fname indents
pure (upd path val)
rewrite_ : FileName -> IndentInfo -> Rule RawImp
rewrite_ : FileName -> IndentInfo -> SourceRule RawImp
rewrite_ fname indents
= do start <- location
keyword "rewrite"
@ -402,7 +404,7 @@ mutual
end <- location
pure (IRewrite (MkFC fname start end) rule tm)
lazy : FileName -> IndentInfo -> Rule RawImp
lazy : FileName -> IndentInfo -> SourceRule RawImp
lazy fname indents
= do start <- location
exactIdent "Lazy"
@ -426,7 +428,7 @@ mutual
pure (IForce (MkFC fname start end) tm)
binder : FileName -> IndentInfo -> Rule RawImp
binder : FileName -> IndentInfo -> SourceRule RawImp
binder fname indents
= autoImplicitPi fname indents
<|> forall_ fname indents
@ -435,7 +437,7 @@ mutual
<|> lam fname indents
<|> let_ fname indents
typeExpr : FileName -> IndentInfo -> Rule RawImp
typeExpr : FileName -> IndentInfo -> SourceRule RawImp
typeExpr fname indents
= do start <- location
arg <- appExpr fname indents
@ -454,10 +456,10 @@ mutual
(mkPi start end a as)
export
expr : FileName -> IndentInfo -> Rule RawImp
expr : FileName -> IndentInfo -> SourceRule RawImp
expr = typeExpr
tyDecl : FileName -> IndentInfo -> Rule ImpTy
tyDecl : FileName -> IndentInfo -> SourceRule ImpTy
tyDecl fname indents
= do start <- location
n <- name
@ -470,7 +472,7 @@ tyDecl fname indents
mutual
parseRHS : (withArgs : Nat) ->
FileName -> IndentInfo -> (Int, Int) -> RawImp ->
Rule (Name, ImpClause)
SourceRule (Name, ImpClause)
parseRHS withArgs fname indents start lhs
= do symbol "="
commit
@ -495,13 +497,13 @@ mutual
let fc = MkFC fname start end
pure (!(getFn lhs), ImpossibleClause fc lhs)
where
getFn : RawImp -> EmptyRule Name
getFn : RawImp -> EmptySourceRule Name
getFn (IVar _ n) = pure n
getFn (IApp _ f a) = getFn f
getFn (IImplicitApp _ f _ a) = getFn f
getFn _ = fail "Not a function application"
clause : Nat -> FileName -> IndentInfo -> Rule (Name, ImpClause)
clause : Nat -> FileName -> IndentInfo -> SourceRule (Name, ImpClause)
clause withArgs fname indents
= do start <- location
lhs <- expr fname indents
@ -514,7 +516,7 @@ mutual
applyArgs f [] = f
applyArgs f ((fc, a) :: args) = applyArgs (IApp fc f a) args
parseWithArg : Rule (FC, RawImp)
parseWithArg : SourceRule (FC, RawImp)
parseWithArg
= do symbol "|"
start <- location
@ -522,14 +524,14 @@ mutual
end <- location
pure (MkFC fname start end, tm)
definition : FileName -> IndentInfo -> Rule ImpDecl
definition : FileName -> IndentInfo -> SourceRule 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 : Rule DataOpt
dataOpt : SourceRule DataOpt
dataOpt
= do exactIdent "noHints"
pure NoHints
@ -539,7 +541,7 @@ dataOpt
ns <- some name
pure (SearchBy ns)
dataDecl : FileName -> IndentInfo -> Rule ImpData
dataDecl : FileName -> IndentInfo -> SourceRule ImpData
dataDecl fname indents
= do start <- location
keyword "data"
@ -555,7 +557,7 @@ dataDecl fname indents
end <- location
pure (MkImpData (MkFC fname start end) n ty opts cs)
recordParam : FileName -> IndentInfo -> Rule (List (Name, RigCount, PiInfo RawImp, RawImp))
recordParam : FileName -> IndentInfo -> SourceRule (List (Name, RigCount, PiInfo RawImp, RawImp))
recordParam fname indents
= do symbol "("
start <- location
@ -565,7 +567,7 @@ recordParam fname indents
<|> do symbol "{"
commit
start <- location
info <- the (EmptyRule (PiInfo RawImp))
info <- the (EmptySourceRule (PiInfo RawImp))
(pure AutoImplicit <* keyword "auto"
<|>(do
keyword "default"
@ -580,7 +582,7 @@ recordParam fname indents
end <- location
pure [(n, top, Explicit, Implicit (MkFC fname start end) False)]
fieldDecl : FileName -> IndentInfo -> Rule (List IField)
fieldDecl : FileName -> IndentInfo -> SourceRule (List IField)
fieldDecl fname indents
= do symbol "{"
commit
@ -592,7 +594,7 @@ fieldDecl fname indents
atEnd indents
pure fs
where
fieldBody : PiInfo RawImp -> Rule (List IField)
fieldBody : PiInfo RawImp -> SourceRule (List IField)
fieldBody p
= do start <- location
ns <- sepBy1 (symbol ",") unqualifiedName
@ -602,7 +604,7 @@ fieldDecl fname indents
pure (map (\n => MkIField (MkFC fname start end)
linear p (UN n) ty) ns)
recordDecl : FileName -> IndentInfo -> Rule ImpDecl
recordDecl : FileName -> IndentInfo -> SourceRule ImpDecl
recordDecl fname indents
= do start <- location
vis <- visibility
@ -620,14 +622,14 @@ recordDecl fname indents
let fc = MkFC fname start end
pure (IRecord fc Nothing vis (MkImpRecord fc n params dc (concat flds)))
namespaceDecl : Rule (List String)
namespaceDecl : SourceRule (List String)
namespaceDecl
= do keyword "namespace"
commit
ns <- nsIdent
pure ns
directive : FileName -> IndentInfo -> Rule ImpDecl
directive : FileName -> IndentInfo -> SourceRule ImpDecl
directive fname indents
= do pragma "logging"
commit
@ -653,7 +655,7 @@ directive fname indents
pure (IPragma (\c, nest, env => setRewrite {c} fc eq rw))
-- Declared at the top
-- topDecl : FileName -> IndentInfo -> Rule ImpDecl
-- topDecl : FileName -> IndentInfo -> SourceRule ImpDecl
topDecl fname indents
= do start <- location
vis <- visibility
@ -701,14 +703,14 @@ collectDefs (d :: ds)
-- full programs
export
prog : FileName -> Rule (List ImpDecl)
prog : FileName -> SourceRule (List ImpDecl)
prog fname
= do ds <- nonEmptyBlock (topDecl fname)
pure (collectDefs ds)
-- TTImp REPL commands
export
command : Rule ImpREPL
command : SourceRule ImpREPL
command
= do symbol ":"; exactIdent "t"
tm <- expr "(repl)" init

3
src/TTImp/ProcessDecls.idr
View File

@ -6,6 +6,7 @@ import Core.Env
import Core.Metadata
import Core.UnifyState
import Parser.Source
import Parser.Support
import TTImp.BindImplicits
@ -102,7 +103,7 @@ processTTImpFile : {auto c : Ref Ctxt Defs} ->
{auto u : Ref UST UState} ->
String -> Core Bool
processTTImpFile fname
= do Right tti <- logTime "Parsing" $ coreLift $ parseFile fname
= do Right tti <- logTime "Parsing" $ coreLift $ parseSourceFile fname
(do decls <- prog fname
eoi
pure decls)

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

@ -283,8 +283,8 @@ data ParseError tok = Error String (List tok)
||| 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)
parse : (act : Grammar tok c ty) -> (xs : List tok)
-> Either (ParseError tok) (ty, List tok)
parse act xs
= case doParse False xs act of
Failure _ _ msg ts => Left (Error msg ts)

5
src/Utils/String.idr
View File

@ -3,6 +3,5 @@ module Utils.String
%default total
export
stripQuotes : String -> String
-- ASSUMPTION! Only total because we know we're getting quoted strings.
stripQuotes = assert_total (strTail . reverse . strTail . reverse)
stripQuotes : (str : String) -> { auto ok : length str `GTE` 2 } -> String
stripQuotes str = substr 1 (length str - 2) str

4
src/Yaffle/REPL.idr
View File

@ -21,7 +21,7 @@ import TTImp.ProcessDecls
import TTImp.TTImp
import TTImp.Unelab
import Parser.Support
import Parser.Source
%default covering
@ -151,7 +151,7 @@ repl : {auto c : Ref Ctxt Defs} ->
repl
= do coreLift (putStr "Yaffle> ")
inp <- coreLift getLine
case runParser Nothing inp command of
case runSourceParser Nothing inp command of
Left err => do coreLift (printLn err)
repl
Right cmd =>