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

chore: prepare for Name refactoring

Browse source
This commit is contained in:
Gabriel Ebner 2022-07-07 13:40:40 +02:00 • committed by Leonardo de Moura
parent c100f45b77
commit 23113501f4
2 changed files with 5 additions and 24 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
src/Lean/Elab/PatternVar.lean
View file

@ -109,19 +109,6 @@ private def processVar (idStx : Syntax) : M Syntax := do
modify fun s => { s with vars := s.vars.push idStx, found := s.found.insert id }
return idStx
private def nameToPattern : Name → TermElabM Term
| Name.anonymous => `(Name.anonymous)
| Name.str p s _ => do let p ← nameToPattern p; `(Name.str $p $(quote s) _)
| Name.num p n _ => do let p ← nameToPattern p; `(Name.num $p $(quote n) _)
private def quotedNameToPattern (stx : Syntax) : TermElabM Syntax :=
match stx[0].isNameLit? with
| some val => nameToPattern val
| none => throwIllFormedSyntax
private def doubleQuotedNameToPattern (stx : Syntax) : TermElabM Syntax := do
nameToPattern (← resolveGlobalConstNoOverloadWithInfo stx[2])
private def samePatternsVariables (startingAt : Nat) (s₁ s₂ : State) : Bool :=
if h : s₁.vars.size = s₂.vars.size then
Array.isEqvAux s₁.vars s₂.vars h (.==.) startingAt
@ -191,14 +178,8 @@ partial def collect (stx : Syntax) : M Syntax := withRef stx <| withFreshMacroSc
return stx
else if k == charLitKind then
return stx
else if k == ``Lean.Parser.Term.quotedName then
/- Quoted names have an elaboration function associated with them, and they will not be macro expanded.
Note that macro expansion is not a good option since it produces a term using the smart constructors `Name.mkStr`, `Name.mkNum`
instead of the constructors `Name.str` and `Name.num` -/
quotedNameToPattern stx
else if k == ``Lean.Parser.Term.doubleQuotedName then
/- Similar to previous case -/
doubleQuotedNameToPattern stx
else if k == ``Lean.Parser.Term.quotedName || k == ``Lean.Parser.Term.doubleQuotedName then
return stx
else if k == choiceKind then
/- Remark: If there are `Term.structInst` alternatives, we keep only them. This is a hack to get rid of
Set-like notation in patterns. Recall that in Mathlib `{a, b}` can be a set with two elements or the

6
src/Lean/ToExpr.lean
View file

@ -35,9 +35,9 @@ instance : ToExpr Unit where
toTypeExpr := mkConst ``Unit
def Name.toExprAux : Name → Expr
| Name.anonymous => mkConst `Lean.Name.anonymous
| Name.str p s _ => mkAppB (mkConst ``Lean.Name.mkStr) (toExprAux p) (toExpr s)
| Name.num p n _ => mkAppB (mkConst ``Lean.Name.mkNum) (toExprAux p) (toExpr n)
| .anonymous => mkConst ``Lean.Name.anonymous
| .str p s ..=> mkApp2 (mkConst ``Lean.Name.str) (toExprAux p) (toExpr s)
| .num p n ..=> mkApp2 (mkConst ``Lean.Name.num) (toExprAux p) (toExpr n)
instance : ToExpr Name where
toExpr := Name.toExprAux