edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2024-09-11 16:05:51 +03:00
Code Issues Projects Releases Wiki Activity

Parse primitive types as identifiers

Browse Source 
This way we can use them as parts of namespaces - they don't need to be
reserved keywords, just reserved names. Fixes #111
This commit is contained in:
Edwin Brady 2020-02-22 18:36:46 +00:00
parent 03bdc3145c
commit 5c86552e56
8 changed files with 40 additions and 27 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
src/Idris/Parser.idr
View File

@ -46,7 +46,7 @@ atom fname
end <- location
pure (PPrimVal (MkFC fname start end) x)
<|> do start <- location
keyword "Type"
exactIdent "Type"
end <- location
pure (PType (MkFC fname start end))
<|> do start <- location
@ -685,22 +685,22 @@ mutual
lazy : FileName -> IndentInfo -> Rule PTerm
lazy fname indents
= do start <- location
keyword "Lazy"
exactIdent "Lazy"
tm <- simpleExpr fname indents
end <- location
pure (PDelayed (MkFC fname start end) LLazy tm)
<|> do start <- location
keyword "Inf"
exactIdent "Inf"
tm <- simpleExpr fname indents
end <- location
pure (PDelayed (MkFC fname start end) LInf tm)
<|> do start <- location
keyword "Delay"
exactIdent "Delay"
tm <- simpleExpr fname indents
end <- location
pure (PDelay (MkFC fname start end) tm)
<|> do start <- location
keyword "Force"
exactIdent "Force"
tm <- simpleExpr fname indents
end <- location
pure (PForce (MkFC fname start end) tm)

4
src/Parser/Lexer.idr
View File

@ -102,9 +102,7 @@ keywords = ["data", "module", "where", "let", "in", "do", "record",
"using", "interface", "implementation", "open", "import",
"public", "export", "private",
"infixl", "infixr", "infix", "prefix",
"Type", "Int", "Integer", "String", "Char", "Double",
"total", "partial", "covering",
"Lazy", "Inf", "Delay", "Force"]
"total", "partial", "covering"]
-- Reserved words for internal syntax
special : List String

35
src/Parser/Support.idr
View File

@ -238,11 +238,11 @@ constant
Nothing => Nothing
Just c' => Just (Ch c')
DoubleLit d => Just (Db d)
Keyword "Int" => Just IntType
Keyword "Integer" => Just IntegerType
Keyword "String" => Just StringType
Keyword "Char" => Just CharType
Keyword "Double" => Just DoubleType
Ident "Int" => Just IntType
Ident "Integer" => Just IntegerType
Ident "String" => Just StringType
Ident "Char" => Just CharType
Ident "Double" => Just DoubleType
_ => Nothing)
export
@ -330,6 +330,11 @@ holeName
HoleIdent str => Just str
_ => Nothing)
reservedNames : List String
reservedNames
= ["Type", "Int", "Integer", "String", "Char", "Double",
"Lazy", "Inf", "Force", "Delay"]
export
name : Rule Name
name
@ -338,16 +343,26 @@ name
op <- operator
symbol ")"
pure (NS ns (UN op))) <|>
(pure (mkFullName ns))
(either (\n => fail ("Can't use reserved name " ++ n))
pure (mkFullName ns))
<|> do symbol "("
op <- operator
symbol ")"
pure (UN op)
where
mkFullName : List String -> Name
mkFullName [] = UN "NONE" -- Can't happen :)
mkFullName [n] = UN n
mkFullName (n :: ns) = NS ns (UN n)
reserved : String -> Bool
reserved n = n `elem` reservedNames
mkFullName : List String -> Either String Name
mkFullName [] = Right $ UN "NONE" -- Can't happen :)
mkFullName [n]
= if reserved n
then Left n
else Right (UN n)
mkFullName (n :: ns)
= if reserved n
then Left n
else Right (NS ns (UN n))
export
IndentInfo : Type

10
src/TTImp/Parser.idr
View File

@ -20,7 +20,7 @@ atom fname
end <- location
pure (IPrimVal (MkFC fname start end) x)
<|> do start <- location
keyword "Type"
exactIdent "Type"
end <- location
pure (IType (MkFC fname start end))
<|> do start <- location
@ -396,22 +396,22 @@ mutual
lazy : FileName -> IndentInfo -> Rule RawImp
lazy fname indents
= do start <- location
keyword "Lazy"
exactIdent "Lazy"
tm <- simpleExpr fname indents
end <- location
pure (IDelayed (MkFC fname start end) LLazy tm)
<|> do start <- location
keyword "Inf"
exactIdent "Inf"
tm <- simpleExpr fname indents
end <- location
pure (IDelayed (MkFC fname start end) LInf tm)
<|> do start <- location
keyword "Delay"
exactIdent "Delay"
tm <- simpleExpr fname indents
end <- location
pure (IDelay (MkFC fname start end) tm)
<|> do start <- location
keyword "Force"
exactIdent "Force"
tm <- simpleExpr fname indents
end <- location
pure (IForce (MkFC fname start end) tm)

2
tests/idris2/perror002/expected
View File

@ -1,2 +1,2 @@
1/1: Building PError (PError.idr)
PError.idr:7:1--7:1:Parse error: Expected ')' (next tokens: [identifier baz, symbol :, Int, symbol ->, Int, identifier baz, identifier x, symbol =, identifier x, end of input])
PError.idr:7:1--7:1:Parse error: Expected ')' (next tokens: [identifier baz, symbol :, identifier Int, symbol ->, identifier Int, identifier baz, identifier x, symbol =, identifier x, end of input])

2
tests/idris2/perror003/expected
View File

@ -1,2 +1,2 @@
1/1: Building PError (PError.idr)
PError.idr:5:17--5:17:Parse error: Expected 'case', 'if', 'do', application or operator expression (next tokens: [symbol (, literal 42, in, identifier y, symbol +, identifier x, identifier baz, symbol :, Int, symbol ->])
PError.idr:5:17--5:17:Parse error: Expected 'case', 'if', 'do', application or operator expression (next tokens: [symbol (, literal 42, in, identifier y, symbol +, identifier x, identifier baz, symbol :, identifier Int, symbol ->])

2
tests/idris2/perror005/expected
View File

@ -1,2 +1,2 @@
1/1: Building PError (PError.idr)
PError.idr:7:1--7:1:Parse error: Expected 'in' (next tokens: [identifier baz, symbol :, Int, symbol ->, Int, identifier baz, identifier x, symbol =, identifier x, end of input])
PError.idr:7:1--7:1:Parse error: Expected 'in' (next tokens: [identifier baz, symbol :, identifier Int, symbol ->, identifier Int, identifier baz, identifier x, symbol =, identifier x, end of input])

2
tests/idris2/perror006/expected
View File

@ -1,2 +1,2 @@
1/1: Building PError (PError.idr)
PError.idr:7:1--7:1:Parse error: Expected 'else' (next tokens: [identifier baz, symbol :, Int, symbol ->, Int, identifier baz, identifier x, symbol =, identifier x, end of input])
PError.idr:7:1--7:1:Parse error: Expected 'else' (next tokens: [identifier baz, symbol :, identifier Int, symbol ->, identifier Int, identifier baz, identifier x, symbol =, identifier x, end of input])