edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-11-23 20:22:34 +03:00
Code Issues Projects Releases Wiki Activity

More fixups.

Browse Source
This commit is contained in:
Matus Tejiscak 2020-04-17 21:17:07 +02:00
parent ab04e95ce7
commit 898095a074
5 changed files with 8 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -34,7 +34,7 @@ ideTokens =
map (\x => (exact x, Symbol)) symbols ++
[(digits, \x => Literal (cast x)),
(stringLit, \x => StrLit (stripQuotes x)),
(ident, Ident),
(ident, \x => NSIdent [x]),
(space, Comment)]
where
stripQuotes : String -> String

4
src/Idris/Package.idr
View File

@ -137,13 +137,13 @@ field fname
<|> do exactIdent "modules"; symbol "="
ms <- sepBy1 (symbol ",")
(do start <- location
ns <- namespace_
ns <- nsIdent
end <- location
pure (MkFC fname start end, ns))
pure (PModules ms)
<|> do exactIdent "main"; symbol "="
start <- location
m <- namespace_
m <- nsIdent
end <- location
pure (PMainMod (MkFC fname start end) m)
<|> do exactIdent "executable"; symbol "="

3
src/Parser/Lexer.idr
View File

@ -81,7 +81,7 @@ holeIdent : Lexer
holeIdent = is '?' <+> ident False
nsIdent : Lexer
nsIdent = ident True <+> is '.' <+> many (ident False)
nsIdent = ident True <+> many (is '.' <+> ident False)
recField : Lexer
recField = is '.' <+> ident False
@ -173,6 +173,7 @@ rawTokens =
(charLit, \x => CharLit (stripQuotes x)),
(recField, \x => RecordField (assert_total $ strTail x)),
(nsIdent, parseNSIdent),
(ident False, \x => NSIdent [x]),
(space, Comment),
(validSymbol, Symbol),
(symbol, Unrecognised)]

2
src/TTImp/Parser.idr
View File

@ -606,7 +606,7 @@ namespaceDecl : Rule (List String)
namespaceDecl
= do keyword "namespace"
commit
ns <- namespace_
ns <- nsIdent
pure ns
directive : FileName -> IndentInfo -> Rule ImpDecl

4
src/TTImp/ProcessRecord.idr
View File

@ -122,14 +122,14 @@ elabRecord {vars} eopts fc env nest newns vis tn params conName_in fields
= apply (IVar fc con)
(replicate done (Implicit fc True) ++
(if imp == Explicit
then [IBindVar fc (nameRoot fldName)]
then [IBindVar fc (nameRoot gname)]
else []) ++
(replicate (countExp sc) (Implicit fc True)))
let lhs = IApp fc (IVar fc gname)
(if imp == Explicit
then lhs_exp
else IImplicitApp fc lhs_exp (Just n)
(IBindVar fc (nameRoot fldName)))
(IBindVar fc (nameRoot gname)))
log 5 $ "Projection LHS " ++ show lhs
processDecl [] nest env
(IClaim fc (if rc == Rig0