mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-11-10 05:07:15 +03:00
Refactor grammar for dependent pairs
As it was, there was significant backtracking for big expressions, getting to the end, not finding a **, so having to try again for application expressions. Fixes #532
This commit is contained in:
Edwin Brady
parent
28bb45c61f
commit
b786621ed6
@ -230,23 +230,28 @@ mutual
|
||||
pure (POp (MkFC fname start end) op l r))
|
||||
<|> pure l
|
||||
|
||||
dpair : FileName -> FilePos -> IndentInfo -> Rule PTerm
|
||||
dpair fname start indents
|
||||
dpairType : FileName -> FilePos -> IndentInfo -> Rule PTerm
|
||||
dpairType fname start indents
|
||||
= do x <- unqualifiedName
|
||||
symbol ":"
|
||||
ty <- expr pdef fname indents
|
||||
loc <- pure $ endPos $ getPTermLoc ty
|
||||
symbol "**"
|
||||
rest <- dpair fname loc indents <|> expr pdef fname indents
|
||||
end <- pure $ endPos $ getPTermLoc rest
|
||||
pure (PDPair (MkFC fname start end)
|
||||
(PRef (MkFC fname start loc) (UN x))
|
||||
ty
|
||||
rest)
|
||||
(do loc <- pure $ endPos $ getPTermLoc ty
|
||||
symbol "**"
|
||||
rest <- nestedDpair fname loc indents <|> expr pdef fname indents
|
||||
end <- pure $ endPos $ getPTermLoc rest
|
||||
pure (PDPair (MkFC fname start end)
|
||||
(PRef (MkFC fname start loc) (UN x))
|
||||
ty
|
||||
rest))
|
||||
<|> pure ty
|
||||
|
||||
nestedDpair : FileName -> FilePos -> IndentInfo -> Rule PTerm
|
||||
nestedDpair fname start indents
|
||||
= dpairType fname start indents
|
||||
<|> do l <- expr pdef fname indents
|
||||
loc <- location
|
||||
symbol "**"
|
||||
rest <- dpair fname loc indents <|> expr pdef fname indents
|
||||
rest <- nestedDpair fname loc indents
|
||||
end <- pure $ endPos $ getPTermLoc rest
|
||||
pure (PDPair (MkFC fname start end)
|
||||
l
|
||||
@ -274,18 +279,30 @@ mutual
|
||||
<|> do continueWith indents ")"
|
||||
end <- location
|
||||
pure (PUnit (MkFC fname start end))
|
||||
-- right section (1-tuple is just an expression)
|
||||
<|> do p <- dpair fname start indents
|
||||
-- dependent pairs with type annotation (so, the type form)
|
||||
<|> do p <- dpairType fname start indents
|
||||
symbol ")"
|
||||
pure p
|
||||
<|> do e <- expr pdef fname indents
|
||||
(do op <- iOperator
|
||||
end <- endLocation
|
||||
<|> do here <- location
|
||||
e <- expr pdef fname indents
|
||||
-- dependent pairs with no type annotation
|
||||
(do loc <- location
|
||||
symbol "**"
|
||||
rest <- nestedDpair fname loc indents <|> expr pdef fname indents
|
||||
end <- pure $ endPos $ getPTermLoc rest
|
||||
symbol ")"
|
||||
pure (PSectionR (MkFC fname start end) e op)
|
||||
<|>
|
||||
-- all the other bracketed expressions
|
||||
tuple fname start indents e)
|
||||
pure (PDPair (MkFC fname start end)
|
||||
e
|
||||
(PImplicit (MkFC fname start end))
|
||||
rest)) <|>
|
||||
-- right sections
|
||||
((do op <- iOperator
|
||||
end <- endLocation
|
||||
symbol ")"
|
||||
pure (PSectionR (MkFC fname start end) e op)
|
||||
<|>
|
||||
-- all the other bracketed expressions
|
||||
tuple fname start indents e))
|
||||
|
||||
getInitRange : List PTerm -> SourceEmptyRule (PTerm, Maybe PTerm)
|
||||
getInitRange [x] = pure (x, Nothing)
|
||||
|
||||
@ -262,7 +262,7 @@ checkValid (AfterPos x) c = if c >= x
|
||||
else fail "Invalid indentation"
|
||||
checkValid EndOfBlock c = fail "End of block"
|
||||
|
||||
||| Any token which indicates the end of a statement/block
|
||||
||| Any token which indicates the end of a statement/block/expression
|
||||
isTerminator : Token -> Bool
|
||||
isTerminator (Symbol ",") = True
|
||||
isTerminator (Symbol "]") = True
|
||||
@ -270,6 +270,7 @@ 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
|
||||
|
||||
@ -84,7 +84,7 @@ idrisTests
|
||||
"params001",
|
||||
-- Performance: things which have been slow in the past, or which
|
||||
-- pose interesting challenges for the elaborator
|
||||
"perf001", "perf002", "perf003", "perf004",
|
||||
"perf001", "perf002", "perf003", "perf004", "perf005",
|
||||
-- Parse errors
|
||||
"perror001", "perror002", "perror003", "perror004", "perror005",
|
||||
"perror006",
|
||||
|
||||
86
tests/idris2/perf005/Lambda.idr
Normal file
86
tests/idris2/perf005/Lambda.idr
Normal file
@ -0,0 +1,86 @@
|
||||
|
||||
module Lambda
|
||||
|
||||
%default total
|
||||
|
||||
data Ty = TyFunc Ty Ty | TyNat
|
||||
|
||||
data Context = Empty | Extend Context Ty
|
||||
|
||||
data Contains : Context -> Ty -> Type where
|
||||
Here : Contains (Extend g ty) ty
|
||||
There : (rest : Contains g ty)
|
||||
-> Contains (Extend g not_ty) ty
|
||||
|
||||
data Term : Context -> Ty -> Type where
|
||||
Var : (idx : Contains g ty)
|
||||
-> Term g ty
|
||||
|
||||
Func : (body : Term (Extend g tyA) tyB)
|
||||
-> Term g (TyFunc tyA tyB)
|
||||
|
||||
App : (func : Term g (TyFunc tyA tyB))
|
||||
-> (var : Term g tyA)
|
||||
-> Term g tyB
|
||||
|
||||
Zero : Term g TyNat
|
||||
|
||||
Next : (inner : Term g TyNat)
|
||||
-> Term g TyNat
|
||||
|
||||
Case : (scrutinee : Term g TyNat)
|
||||
-> (zero : Term g tyA)
|
||||
-> (next : Term (Extend g TyNat) tyA)
|
||||
-> Term g tyA
|
||||
|
||||
Plus : Term g TyNat
|
||||
-> Term g TyNat
|
||||
-> Term g TyNat
|
||||
|
||||
Rec : (body : Term (Extend g tyA) tyA)
|
||||
-> Term g tyA
|
||||
|
||||
term : Term Empty
|
||||
(TyFunc TyNat -- (Var Here) -
|
||||
(TyFunc TyNat -- (Var (There Here)) -
|
||||
(TyFunc TyNat -- (Var (There (There Here))) -
|
||||
(TyFunc TyNat -- (Var (There (There (There Here)))) -
|
||||
(TyFunc TyNat -- (Var (There (There (There (There Here))))) -
|
||||
(TyFunc TyNat -- (Var (There (There (There (There (There Here)))))) -
|
||||
(TyFunc TyNat -- (Var (There (There (There (There (There (There Here)))))))
|
||||
TyNat
|
||||
)
|
||||
)
|
||||
)
|
||||
)
|
||||
)
|
||||
)
|
||||
)
|
||||
term =
|
||||
Func
|
||||
(Func
|
||||
(Func
|
||||
(Func
|
||||
(Func
|
||||
(Func
|
||||
(Func
|
||||
(Func (Plus (Var Here)
|
||||
(Plus (Var (There Here))
|
||||
(Plus (Var (There (There Here)))
|
||||
(Plus (Var (There (There (There Here))))
|
||||
(Plus (Var (There (There (There (There Here)))))
|
||||
(Plus (Var (There (There (There (There (There Here))))))
|
||||
(Var (There (There (There (There (There (There Here)))))))
|
||||
)
|
||||
)
|
||||
)
|
||||
)
|
||||
)
|
||||
)
|
||||
)
|
||||
)
|
||||
)
|
||||
)
|
||||
)
|
||||
)
|
||||
)
|
||||
36
tests/idris2/perf005/expected
Normal file
36
tests/idris2/perf005/expected
Normal file
@ -0,0 +1,36 @@
|
||||
1/1: Building Lambda (Lambda.idr)
|
||||
Lambda.idr:60:3--87:1:While processing right hand side of term at Lambda.idr:59:1--87:1:
|
||||
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
|
||||
at:
|
||||
60 Func
|
||||
61 (Func
|
||||
62 (Func
|
||||
63 (Func
|
||||
64 (Func
|
||||
65 (Func
|
||||
66 (Func
|
||||
67 (Func (Plus (Var Here)
|
||||
68 (Plus (Var (There Here))
|
||||
69 (Plus (Var (There (There Here)))
|
||||
70 (Plus (Var (There (There (There Here))))
|
||||
71 (Plus (Var (There (There (There (There Here)))))
|
||||
72 (Plus (Var (There (There (There (There (There Here))))))
|
||||
73 (Var (There (There (There (There (There (There Here)))))))
|
||||
74 )
|
||||
75 )
|
||||
76 )
|
||||
77 )
|
||||
78 )
|
||||
79 )
|
||||
80 )
|
||||
81 )
|
||||
82 )
|
||||
83 )
|
||||
84 )
|
||||
85 )
|
||||
86 )
|
||||
|
||||
3
tests/idris2/perf005/run
Executable file
3
tests/idris2/perf005/run
Executable file
@ -0,0 +1,3 @@
|
||||
$1 --check Lambda.idr
|
||||
|
||||
rm -rf build
|
||||
Loading…
Reference in New Issue
Block a user