max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: don't allow whitespaces between . and field name

Browse source
This commit is contained in:
Leonardo de Moura 2021-04-05 07:11:14 -07:00
parent 9949aa653e
commit e6dec2dd79
4 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Elab/App.lean
View file

@ -812,9 +812,9 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
elabAppFn e (LVal.fieldIdx idxStx idx :: lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
match f with
| `($(e).$idx:fieldIdx) => elabFieldIdx e idx
| `($e |>. $idx:fieldIdx) => elabFieldIdx e idx
| `($e |>.$idx:fieldIdx) => elabFieldIdx e idx
| `($(e).$field:ident) => elabFieldName e field
| `($e |>. $field:ident) => elabFieldName e field
| `($e |>.$field:ident) => elabFieldName e field
| `($e[%$bracket $idx]) => elabAppFn e (LVal.getOp bracket idx :: lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
| `($id:ident@$t:term) =>
throwError "unexpected occurrence of named pattern"

4
src/Lean/Parser/Term.lean
View file

@ -203,7 +203,7 @@ def argument :=
-- argument precedence is `arg` (i.e. does not accept `lead` precedence)
@[builtinTermParser] def app := trailing_parser:leadPrec:maxPrec many1 argument
@[builtinTermParser] def proj := trailing_parser checkNoWsBefore >> "." >> (fieldIdx <|> ident)
@[builtinTermParser] def proj := trailing_parser checkNoWsBefore >> "." >> checkNoWsBefore >> (fieldIdx <|> ident)
@[builtinTermParser] def completion := trailing_parser checkNoWsBefore >> "."
@[builtinTermParser] def arrayRef := trailing_parser checkNoWsBefore >> "[" >> termParser >>"]"
@[builtinTermParser] def arrow := trailing_parser checkPrec 25 >> unicodeSymbol " → " " -> " >> termParser 25
@ -215,7 +215,7 @@ def isIdent (stx : Syntax) : Bool :=
@[builtinTermParser] def explicitUniv : TrailingParser := trailing_parser checkStackTop isIdent "expected preceding identifier" >> checkNoWsBefore "no space before '.{'" >> ".{" >> sepBy1 levelParser ", " >> "}"
@[builtinTermParser] def namedPattern : TrailingParser := trailing_parser checkStackTop isIdent "expected preceding identifier" >> checkNoWsBefore "no space before '@'" >> "@" >> termParser maxPrec
@[builtinTermParser] def pipeProj := trailing_parser:minPrec " |>." >> (fieldIdx <|> ident) >> many argument
@[builtinTermParser] def pipeProj := trailing_parser:minPrec " |>." >> checkNoWsBefore >> (fieldIdx <|> ident) >> many argument
@[builtinTermParser] def pipeCompletion := trailing_parser:minPrec " |>."
@[builtinTermParser] def subst := trailing_parser:75 " ▸ " >> sepBy1 (termParser 75) " ▸ "

2
tests/lean/run/305.lean
View file

@ -47,7 +47,7 @@ def readArgs : Id (Array Flag.Parsed) := panic! ""
def parse (c : Cmd) : Id Cmd.Parsed := do
let cmdName ← readSubCmds
let flags ← readArgs
let cmd := c.subCmdByFullName? cmdName |>. get!
let cmd := c.subCmdByFullName? cmdName |>.get!
let defaultedFlags : Array Flag.Parsed := #[]
-- If we uncomment /-: Cmd.Parsed -/ two lines below or comment the line below, the elaborator stops hanging.
let flags := defaultedFlags

2
tests/lean/run/KyleAlg.lean
View file

@ -225,7 +225,7 @@ def test8 {G : Type _} [Group G]: Group (G × G × G × G × G × G × G × G) :
namespace Lean
unsafe def Expr.dagSizeUnsafe (e : Expr) : IO Nat := do
let (_, s) ← visit e |>. run ({}, 0)
let (_, s) ← visit e |>.run ({}, 0)
return s.2
where
visit (e : Expr) : StateRefT (Std.HashSet USize × Nat) IO Unit := do