idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-13 05:48:39 +03:00
Code Issues Projects Releases Wiki Activity

Fix DPair parsing

Browse Source
This commit is contained in:
russoul 2020-09-05 12:03:35 +03:00 committed by G. Allais
parent 937aa8fc43
commit 9565f6cf8b
4 changed files with 28 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
src/Idris/Parser.idr
View File

@ -211,7 +211,7 @@ mutual
pure (x, ty))
(x, ty) <- pure loc.val
(do symbol "**"
rest <- bounds ((nestedDpair fname loc indents <|> expr pdef fname indents) <* symbol ")")
rest <- bounds (nestedDpair fname loc indents <|> expr pdef fname indents)
pure (PDPair (boundToFC fname (mergeBounds start rest))
(PRef (boundToFC fname loc) (UN x))
ty
@ -223,7 +223,7 @@ mutual
= dpairType fname start indents
<|> do l <- expr pdef fname indents
loc <- bounds (symbol "**")
rest <- bounds (nestedDpair fname loc indents <* symbol ")")
rest <- bounds (nestedDpair fname loc indents <|> expr pdef fname indents)
pure (PDPair (boundToFC fname (mergeBounds start rest))
l
(PImplicit (boundToFC fname (mergeBounds start rest)))
@ -249,7 +249,7 @@ mutual
<|> do b <- bounds (continueWith indents ")")
pure (PUnit (boundToFC fname (mergeBounds s b)))
-- dependent pairs with type annotation (so, the type form)
<|> do dpairType fname s indents
<|> do dpairType fname s indents <* symbol ")"
<|> do here <- location
e <- bounds (expr pdef fname indents)
-- dependent pairs with no type annotation

2
tests/idris2/perf005/Lambda.idr
View File

@ -1,6 +1,8 @@
module Lambda
import NoRegression
%default total
data Ty = TyFunc Ty Ty | TyNat

14
tests/idris2/perf005/NoRegression.idr Normal file
View File

@ -0,0 +1,14 @@
module NoRegression
import Data.Vect
data Dep : (n : Nat) -> (a : Type) -> Vect n a -> Type where
MkDep : Dep n a v
dpairParse : ( n : Nat
** a : Type
** v : Vect n a
** Dep n a v
)
dpairParse = (_ ** _ ** ["a", "b"] ** MkDep)

17
tests/idris2/perf005/expected
View File

@ -1,12 +1,13 @@
1/1: Building Lambda (Lambda.idr)
1/2: Building NoRegression (NoRegression.idr)
2/2: Building Lambda (Lambda.idr)
Error: While processing right hand side of term. When unifying Term ?g (TyFunc ?tyA (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat TyNat)))))))) and Term Empty (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat (TyFunc TyNat TyNat))))))).
Mismatch between: TyFunc TyNat TyNat and TyNat.
Lambda.idr:60:3--86:9
60 | Func
61 | (Func
62 | (Func
63 | (Func
64 | (Func
65 | (Func
Lambda.idr:62:3--88:9
62 | Func
63 | (Func
64 | (Func
65 | (Func
66 | (Func
67 | (Func