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

feat: allow keyword-like projection identifiers

Browse source
This commit is contained in:
Sebastian Ullrich 2022-05-10 17:14:26 +02:00 • committed by Leonardo de Moura
parent 37b2f74404
commit 392640d292
2 changed files with 9 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -260,7 +260,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 >> "." >> checkNoWsBefore >> (fieldIdx <|> ident)
@[builtinTermParser] def proj := trailing_parser checkNoWsBefore >> "." >> checkNoWsBefore >> (fieldIdx <|> rawIdent)
@[builtinTermParser] def completion := trailing_parser checkNoWsBefore >> "."
@[builtinTermParser] def arrayRef := trailing_parser checkNoWsBefore >> "[" >> termParser >>"]"
@[builtinTermParser] def arrow := trailing_parser checkPrec 25 >> unicodeSymbol " → " " -> " >> termParser 25
@ -272,7 +272,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 '@'" >> "@" >> optional (atomic (ident >> ":")) >> termParser maxPrec
@[builtinTermParser] def pipeProj := trailing_parser:minPrec " |>." >> checkNoWsBefore >> (fieldIdx <|> ident) >> many argument
@[builtinTermParser] def pipeProj := trailing_parser:minPrec " |>." >> checkNoWsBefore >> (fieldIdx <|> rawIdent) >> many argument
@[builtinTermParser] def pipeCompletion := trailing_parser:minPrec " |>."
@[builtinTermParser] def subst := trailing_parser:75 " ▸ " >> sepBy1 (termParser 75) " ▸ "
@ -299,7 +299,7 @@ def macroLastArg := macroDollarArg <|> macroArg
@[builtinTermParser] def dynamicQuot := leading_parser "`(" >> ident >> "|" >> incQuotDepth (parserOfStack 1) >> ")"
@[builtinTermParser] def dotIdent := leading_parser "." >> checkNoWsBefore >> ident
@[builtinTermParser] def dotIdent := leading_parser "." >> checkNoWsBefore >> rawIdent
end Term

12
tests/lean/run/constProp.lean
View file

@ -226,8 +226,8 @@ inductive Bigstep : State → Stmt → State → Prop where
| seq : (σ₁, s₁) ⇓ σ₂ → (σ₂, s₂) ⇓ σ₃ → (σ₁, s₁ ;; s₂) ⇓ σ₃
| ifTrue : evalTrue c σ₁ → (σ₁, t) ⇓ σ₂ → (σ₁, .ite c t e) ⇓ σ₂
| ifFalse : evalFalse c σ₁ → (σ₁, e) ⇓ σ₂ → (σ₁, .ite c t e) ⇓ σ₂
| whileTrue : evalTrue c σ₁ → (σ₁, b) ⇓ σ₂ → (σ₂, .«while» c b) ⇓ σ₃ → (σ₁, .«while» c b) ⇓ σ₃
| whileFalse : evalFalse c σ → (σ, .«while» c b) ⇓ σ
| whileTrue : evalTrue c σ₁ → (σ₁, b) ⇓ σ₂ → (σ₂, .while c b) ⇓ σ₃ → (σ₁, .while c b) ⇓ σ₃
| whileFalse : evalFalse c σ → (σ, .while c b) ⇓ σ
end
@ -268,7 +268,7 @@ def evalExpr (e : Expr) : EvalM Val := do
| .bool true => e.eval fuel
| .bool false => t.eval fuel
| _ => throw "Boolean expected"
| «while» c b =>
| .while c b =>
match (← evalExpr c) with
| .bool true => b.eval fuel; stmt.eval fuel
| .bool false => return ()
@ -324,10 +324,10 @@ instance : Repr State where
| .val (.bool true) => e.simplify
| .val (.bool false) => t.simplify
| c' => ite c' e.simplify t.simplify
| «while» c b =>
| .while c b =>
match c.simplify with
| .val (.bool false) => skip
| c' => «while» c' b.simplify
| c' => .while c' b.simplify
def example3 := `[Stmt|
if (1 < 2 + 3) {
@ -413,7 +413,7 @@ local notation "⊥" => []
| ite c s₁ s₂ =>
match s₁.constProp σ, s₂.constProp σ with
| (s₁', σ₁), (s₂', σ₂) => (ite (c.constProp σ) s₁' s₂', σ₁.join σ₂)
| «while» c b => («while» (c.constProp ⊥) (b.constProp ⊥).1, ⊥)
| .while c b => (.while (c.constProp ⊥) (b.constProp ⊥).1, ⊥)
def State.le (σ₁ σ₂ : State) : Prop :=
∀ ⦃x : Var⦄ ⦃v : Val⦄, σ₁.find? x = some v → σ₂.find? x = some v