idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-24 06:52:19 +03:00
Code Issues Projects Releases Wiki Activity

Support Multi-declarations (#1280)

Browse Source
This commit is contained in:
Ohad Kammar 2021-04-07 12:21:17 +01:00 committed by GitHub
parent 2ac4bea220
commit b65907f770
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
7 changed files with 57 additions and 31 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

56
src/Idris/Parser.idr
View File

@ -833,17 +833,19 @@ visibility
= visOption
<|> pure Private
tyDecl : Rule Name -> String -> FileName -> IndentInfo -> Rule PTypeDecl
tyDecl declName predoc fname indents
= do b <- bounds (do doc <- option "" documentation
n <- bounds declName
symbol ":"
mustWork $
do ty <- expr pdef fname indents
pure (doc, n.val, boundToFC fname n, ty))
tyDecls : Rule Name -> String -> FileName -> IndentInfo -> Rule (List1 PTypeDecl)
tyDecls declName predoc fname indents
= do bs <- do docns <- sepBy1 (symbol ",") (do
doc <- option "" documentation
n <- bounds declName
pure (doc, n))
symbol ":"
mustWork $ do ty <- expr pdef fname indents
pure $ map (\(doc, n) => (doc, n.val, boundToFC fname n, ty))
docns
atEnd indents
let (doc, n, nFC, ty) = b.val
pure (MkPTy (boundToFC fname b) nFC n (predoc ++ doc) ty)
pure $ map (\(doc, n, nFC, ty) => (MkPTy nFC nFC n (predoc ++ doc) ty))
bs
withFlags : SourceEmptyRule (List WithFlag)
withFlags
@ -963,8 +965,8 @@ dataBody fname mincol start n indents ty
dopts <- sepBy1 (symbol ",") dataOpt
symbol "]"
pure $ forget dopts)
cs <- blockAfter mincol (tyDecl (mustWork dataConstructorName) "" fname)
pure (opts, cs))
cs <- blockAfter mincol (tyDecls (mustWork dataConstructorName) "" fname)
pure (opts, concatMap forget cs))
(opts, cs) <- pure b.val
pure (MkPData (boundToFC fname (mergeBounds start b)) n ty opts cs)
@ -1392,18 +1394,20 @@ recordDecl fname indents
pure (\fc : FC => PRecord fc doc vis n params (fst dcflds) (concat (snd dcflds))))
pure (b.val (boundToFC fname b))
claim : FileName -> IndentInfo -> Rule PDecl
claim fname indents
= do b <- bounds (do doc <- option "" documentation
visOpts <- many (visOpt fname)
vis <- getVisibility Nothing visOpts
let opts = mapMaybe getRight visOpts
m <- multiplicity
rig <- getMult m
cl <- tyDecl name doc fname indents
pure (doc, vis, opts, rig, cl))
(doc, vis, opts, rig, cl) <- pure b.val
pure (PClaim (boundToFC fname b) rig vis opts cl)
claims : FileName -> IndentInfo -> Rule (List1 PDecl)
claims fname indents
= do bs <- bounds (do
doc <- option "" documentation
visOpts <- many (visOpt fname)
vis <- getVisibility Nothing visOpts
let opts = mapMaybe getRight visOpts
m <- multiplicity
rig <- getMult m
cls <- tyDecls name doc fname indents
pure $ map (\cl => the (Pair _ _) (doc, vis, opts, rig, cl)) cls)
pure $ map (\(doc, vis, opts, rig, cl) : Pair _ _ =>
PClaim (boundToFC fname bs) rig vis opts cl)
bs.val
definition : FileName -> IndentInfo -> Rule PDecl
definition fname indents
@ -1436,8 +1440,8 @@ directiveDecl fname indents
topDecl fname indents
= do d <- dataDecl fname indents
pure [d]
<|> do d <- claim fname indents
pure [d]
<|> do ds <- claims fname indents
pure (forget ds)
<|> do d <- definition fname indents
pure [d]
<|> fixDecl fname indents

2
tests/Main.idr
View File

@ -47,7 +47,7 @@ idrisTestsBasic = MkTestPool []
"basic041", "basic042", "basic043", "basic044", "basic045",
"basic046", "basic047", "basic048", "basic049", "basic050",
"basic051", "basic052", "basic053", "basic054", "basic055",
"basic056", "basic057", "basic058"]
"basic056", "basic057", "basic058", "basic059"]
idrisTestsCoverage : TestPool
idrisTestsCoverage = MkTestPool []

18
tests/idris2/basic059/MultiClaim.idr Normal file
View File

@ -0,0 +1,18 @@
data Foo : Type where
|||An A
A ,
||| Just a B
B : Foo
public export
foo1, foo2 : Foo
foo1 = A
foo2 = LocalB
where
LocalB, LocalA : Foo
LocalB = B
LocalA = let NestedLocalA, NestedLocalB : Foo
NestedLocalA = A
NestedLocalB = B
in NestedLocalA

1
tests/idris2/basic059/expected Normal file
View File

@ -0,0 +1 @@
1/1: Building MultiClaim (MultiClaim.idr)

3
tests/idris2/basic059/run Normal file
View File

@ -0,0 +1,3 @@
$1 --no-banner --no-color --console-width 0 --check MultiClaim.idr
rm -rf build

4
tests/idris2/error011/expected
View File

@ -7,11 +7,11 @@ ConstructorDuplicate.idr:1:14--1:15
Error: Main.D is already defined.
ConstructorDuplicate.idr:5:3--5:15
ConstructorDuplicate.idr:5:3--5:4
1 | data A = B | B
2 |
3 | data C : Type -> Type where
4 | D : C Int
5 | D : C String
^^^^^^^^^^^^
^

4
tests/idris2/reflection001/expected
View File

@ -32,7 +32,7 @@ quote.idr:37:1--37:21
Main> IApp (MkFC "quote.idr" (3, 12) (3, 23)) (IApp (MkFC "quote.idr" (3, 12) (3, 23)) (IVar (MkFC "quote.idr" (3, 12) (3, 23)) (UN "+")) (IApp (MkFC "quote.idr" (6, 13) (6, 14)) (IVar (MkFC "quote.idr" (6, 13) (6, 14)) (UN "fromInteger")) (IPrimVal (MkFC "quote.idr" (6, 13) (6, 14)) (BI 3)))) (IApp (MkFC "quote.idr" (6, 18) (6, 19)) (IVar (MkFC "quote.idr" (6, 18) (6, 19)) (UN "fromInteger")) (IPrimVal (MkFC "quote.idr" (6, 18) (6, 19)) (BI 4)))
Main> IApp (MkFC "quote.idr" (3, 12) (3, 23)) (IApp (MkFC "quote.idr" (3, 12) (3, 23)) (IVar (MkFC "quote.idr" (3, 12) (3, 23)) (UN "+")) (IVar (MkFC "(interactive)" (0, 6) (0, 10)) (UN "True"))) (IVar (MkFC "(interactive)" (0, 14) (0, 19)) (UN "False"))
Main> ILocal (MkFC "quote.idr" (10, 12) (11, 29)) [IClaim (MkFC "quote.idr" (10, 12) (10, 28)) MW Private [] (MkTy (MkFC "quote.idr" (10, 12) (10, 28)) (MkFC "quote.idr" (10, 12) (10, 15)) (UN "xfn") (IPi (MkFC "quote.idr" (10, 18) (10, 21)) MW ExplicitArg Nothing (IPrimVal (MkFC "quote.idr" (10, 18) (10, 21)) IntType) (IPrimVal (MkFC "quote.idr" (10, 25) (10, 28)) IntType))), IDef (MkFC "quote.idr" (11, 12) (11, 29)) (UN "xfn") [PatClause (MkFC "quote.idr" (11, 12) (11, 29)) (IApp (MkFC "quote.idr" (11, 12) (11, 19)) (IVar (MkFC "quote.idr" (11, 12) (11, 15)) (UN "xfn")) (IBindVar (MkFC "quote.idr" (11, 16) (11, 19)) "var")) (IApp (MkFC "quote.idr" (11, 22) (11, 29)) (IApp (MkFC "quote.idr" (11, 22) (11, 29)) (IVar (MkFC "quote.idr" (11, 22) (11, 29)) (UN "*")) (IVar (MkFC "quote.idr" (11, 22) (11, 25)) (UN "var"))) (IApp (MkFC "quote.idr" (11, 28) (11, 29)) (IVar (MkFC "quote.idr" (11, 28) (11, 29)) (UN "fromInteger")) (IPrimVal (MkFC "quote.idr" (11, 28) (11, 29)) (BI 2))))]] (IApp (MkFC "quote.idr" (12, 12) (12, 22)) (IVar (MkFC "quote.idr" (12, 12) (12, 15)) (UN "xfn")) (IApp (MkFC "(interactive)" (0, 9) (0, 22)) (IApp (MkFC "(interactive)" (0, 9) (0, 22)) (IVar (MkFC "(interactive)" (0, 9) (0, 12)) (UN "the")) (IPrimVal (MkFC "(interactive)" (0, 13) (0, 16)) IntType)) (IApp (MkFC "(interactive)" (0, 17) (0, 22)) (IVar (MkFC "(interactive)" (0, 17) (0, 22)) (UN "fromInteger")) (IPrimVal (MkFC "(interactive)" (0, 17) (0, 22)) (BI 99994)))))
Main> ILocal (MkFC "quote.idr" (16, 12) (17, 29)) [IClaim (MkFC "quote.idr" (16, 12) (16, 28)) MW Private [] (MkTy (MkFC "quote.idr" (16, 12) (16, 28)) (MkFC "quote.idr" (16, 12) (16, 15)) (UN "xfn") (IPi (MkFC "quote.idr" (16, 18) (16, 21)) MW ExplicitArg Nothing (IPrimVal (MkFC "quote.idr" (16, 18) (16, 21)) IntType) (IPrimVal (MkFC "quote.idr" (16, 25) (16, 28)) IntType))), IDef (MkFC "quote.idr" (17, 12) (17, 29)) (UN "xfn") [PatClause (MkFC "quote.idr" (17, 12) (17, 29)) (IApp (MkFC "quote.idr" (17, 12) (17, 19)) (IVar (MkFC "quote.idr" (17, 12) (17, 15)) (UN "xfn")) (IBindVar (MkFC "quote.idr" (17, 16) (17, 19)) "var")) (IApp (MkFC "quote.idr" (17, 22) (17, 29)) (IApp (MkFC "quote.idr" (17, 22) (17, 29)) (IVar (MkFC "quote.idr" (17, 22) (17, 29)) (UN "*")) (IVar (MkFC "quote.idr" (17, 22) (17, 25)) (UN "var"))) (IApp (MkFC "quote.idr" (17, 28) (17, 29)) (IVar (MkFC "quote.idr" (17, 28) (17, 29)) (UN "fromInteger")) (IPrimVal (MkFC "quote.idr" (17, 28) (17, 29)) (BI 2))))]] (IApp (MkFC "quote.idr" (18, 12) (18, 43)) (IVar (MkFC "quote.idr" (18, 12) (18, 15)) (UN "xfn")) (IPrimVal EmptyFC (I 99994)))
Main> ILocal (MkFC "quote.idr" (10, 12) (11, 29)) [IClaim (MkFC "quote.idr" (10, 12) (10, 28)) MW Private [] (MkTy (MkFC "quote.idr" (10, 12) (10, 15)) (MkFC "quote.idr" (10, 12) (10, 15)) (UN "xfn") (IPi (MkFC "quote.idr" (10, 18) (10, 21)) MW ExplicitArg Nothing (IPrimVal (MkFC "quote.idr" (10, 18) (10, 21)) IntType) (IPrimVal (MkFC "quote.idr" (10, 25) (10, 28)) IntType))), IDef (MkFC "quote.idr" (11, 12) (11, 29)) (UN "xfn") [PatClause (MkFC "quote.idr" (11, 12) (11, 29)) (IApp (MkFC "quote.idr" (11, 12) (11, 19)) (IVar (MkFC "quote.idr" (11, 12) (11, 15)) (UN "xfn")) (IBindVar (MkFC "quote.idr" (11, 16) (11, 19)) "var")) (IApp (MkFC "quote.idr" (11, 22) (11, 29)) (IApp (MkFC "quote.idr" (11, 22) (11, 29)) (IVar (MkFC "quote.idr" (11, 22) (11, 29)) (UN "*")) (IVar (MkFC "quote.idr" (11, 22) (11, 25)) (UN "var"))) (IApp (MkFC "quote.idr" (11, 28) (11, 29)) (IVar (MkFC "quote.idr" (11, 28) (11, 29)) (UN "fromInteger")) (IPrimVal (MkFC "quote.idr" (11, 28) (11, 29)) (BI 2))))]] (IApp (MkFC "quote.idr" (12, 12) (12, 22)) (IVar (MkFC "quote.idr" (12, 12) (12, 15)) (UN "xfn")) (IApp (MkFC "(interactive)" (0, 9) (0, 22)) (IApp (MkFC "(interactive)" (0, 9) (0, 22)) (IVar (MkFC "(interactive)" (0, 9) (0, 12)) (UN "the")) (IPrimVal (MkFC "(interactive)" (0, 13) (0, 16)) IntType)) (IApp (MkFC "(interactive)" (0, 17) (0, 22)) (IVar (MkFC "(interactive)" (0, 17) (0, 22)) (UN "fromInteger")) (IPrimVal (MkFC "(interactive)" (0, 17) (0, 22)) (BI 99994)))))
Main> ILocal (MkFC "quote.idr" (16, 12) (17, 29)) [IClaim (MkFC "quote.idr" (16, 12) (16, 28)) MW Private [] (MkTy (MkFC "quote.idr" (16, 12) (16, 15)) (MkFC "quote.idr" (16, 12) (16, 15)) (UN "xfn") (IPi (MkFC "quote.idr" (16, 18) (16, 21)) MW ExplicitArg Nothing (IPrimVal (MkFC "quote.idr" (16, 18) (16, 21)) IntType) (IPrimVal (MkFC "quote.idr" (16, 25) (16, 28)) IntType))), IDef (MkFC "quote.idr" (17, 12) (17, 29)) (UN "xfn") [PatClause (MkFC "quote.idr" (17, 12) (17, 29)) (IApp (MkFC "quote.idr" (17, 12) (17, 19)) (IVar (MkFC "quote.idr" (17, 12) (17, 15)) (UN "xfn")) (IBindVar (MkFC "quote.idr" (17, 16) (17, 19)) "var")) (IApp (MkFC "quote.idr" (17, 22) (17, 29)) (IApp (MkFC "quote.idr" (17, 22) (17, 29)) (IVar (MkFC "quote.idr" (17, 22) (17, 29)) (UN "*")) (IVar (MkFC "quote.idr" (17, 22) (17, 25)) (UN "var"))) (IApp (MkFC "quote.idr" (17, 28) (17, 29)) (IVar (MkFC "quote.idr" (17, 28) (17, 29)) (UN "fromInteger")) (IPrimVal (MkFC "quote.idr" (17, 28) (17, 29)) (BI 2))))]] (IApp (MkFC "quote.idr" (18, 12) (18, 43)) (IVar (MkFC "quote.idr" (18, 12) (18, 15)) (UN "xfn")) (IPrimVal EmptyFC (I 99994)))
Main> [UN "names", NS (MkNS ["Prelude"]) (UN "+")]
Main> Bye for now!