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

chore: cleanup

Browse source
This commit is contained in:
Leonardo de Moura 2022-07-25 22:39:56 -07:00
parent 30199745ad
commit 3896244c55
29 changed files with 136 additions and 136 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/Lean/Compiler/IR/Basic.lean
View file

@ -406,23 +406,23 @@ inductive Decl where
namespace Decl
def name : Decl → FunId
| Decl.fdecl f .. => f
| Decl.extern f .. => f
| .fdecl f .. => f
| .extern f .. => f
def params : Decl → Array Param
| Decl.fdecl (xs := xs) .. => xs
| Decl.extern (xs := xs) .. => xs
| .fdecl (xs := xs) .. => xs
| .extern (xs := xs) .. => xs
def resultType : Decl → IRType
| Decl.fdecl (type := t) .. => t
| Decl.extern (type := t) .. => t
| .fdecl (type := t) .. => t
| .extern (type := t) .. => t
def isExtern : Decl → Bool
| Decl.extern .. => true
| .extern .. => true
| _ => false
def getInfo : Decl → DeclInfo
| Decl.fdecl (info := info) .. => info
| .fdecl (info := info) .. => info
| _ => {}
def updateBody! (d : Decl) (bNew : FnBody) : Decl :=

4
src/Lean/Compiler/IR/Borrow.lean
View file

@ -90,7 +90,7 @@ partial def visitFnBody (fnid : FunId) : FnBody → StateM ParamMap Unit
def visitDecls (env : Environment) (decls : Array Decl) : StateM ParamMap Unit :=
decls.forM fun decl => match decl with
| Decl.fdecl (f := f) (xs := xs) (body := b) .. => do
| .fdecl (f := f) (xs := xs) (body := b) .. => do
let exported := isExport env f
modify fun m => m.insert (ParamMap.Key.decl f) (initBorrowIfNotExported exported xs)
visitFnBody f b
@ -281,7 +281,7 @@ partial def collectFnBody : FnBody → M Unit
| e => do unless e.isTerminal do collectFnBody e.body
partial def collectDecl : Decl → M Unit
| Decl.fdecl (f := f) (xs := ys) (body := b) .. =>
| .fdecl (f := f) (xs := ys) (body := b) .. =>
withReader (fun ctx => let ctx := updateParamSet ctx ys; { ctx with currFn := f }) do
collectFnBody b
updateParamMap (ParamMap.Key.decl f)

2
src/Lean/Compiler/IR/Boxing.lean
View file

@ -327,7 +327,7 @@ def run (env : Environment) (decls : Array Decl) : Array Decl :=
let ctx : BoxingContext := { decls := decls, env := env }
let decls := decls.foldl (init := #[]) fun newDecls decl =>
match decl with
| Decl.fdecl (f := f) (xs := xs) (type := t) (body := b) .. =>
| .fdecl (f := f) (xs := xs) (type := t) (body := b) .. =>
let nextIdx := decl.maxIndex + 1
let (b, s) := (withParams xs (visitFnBody b) { ctx with f := f, resultType := t }).run { nextIdx := nextIdx }
let newDecls := newDecls ++ s.auxDecls

32
src/Lean/Compiler/IR/Checker.lean
View file

@ -146,30 +146,30 @@ def checkExpr (ty : IRType) : Expr → M Unit
withReader (fun _ => { ctx with localCtx := localCtx }) k
partial def checkFnBody : FnBody → M Unit
| FnBody.vdecl x t v b => do
| .vdecl x t v b => do
checkExpr t v
markVar x
withReader (fun ctx => { ctx with localCtx := ctx.localCtx.addLocal x t v }) (checkFnBody b)
| FnBody.jdecl j ys v b => do
| .jdecl j ys v b => do
markJP j
withParams ys (checkFnBody v)
withReader (fun ctx => { ctx with localCtx := ctx.localCtx.addJP j ys v }) (checkFnBody b)
| FnBody.set x _ y b => checkVar x *> checkArg y *> checkFnBody b
| FnBody.uset x _ y b => checkVar x *> checkVar y *> checkFnBody b
| FnBody.sset x _ _ y _ b => checkVar x *> checkVar y *> checkFnBody b
| FnBody.setTag x _ b => checkVar x *> checkFnBody b
| FnBody.inc x _ _ _ b => checkVar x *> checkFnBody b
| FnBody.dec x _ _ _ b => checkVar x *> checkFnBody b
| FnBody.del x b => checkVar x *> checkFnBody b
| FnBody.mdata _ b => checkFnBody b
| FnBody.jmp j ys => checkJP j *> checkArgs ys
| FnBody.ret x => checkArg x
| FnBody.case _ x _ alts => checkVar x *> alts.forM (fun alt => checkFnBody alt.body)
| FnBody.unreachable => pure ()
| .set x _ y b => checkVar x *> checkArg y *> checkFnBody b
| .uset x _ y b => checkVar x *> checkVar y *> checkFnBody b
| .sset x _ _ y _ b => checkVar x *> checkVar y *> checkFnBody b
| .setTag x _ b => checkVar x *> checkFnBody b
| .inc x _ _ _ b => checkVar x *> checkFnBody b
| .dec x _ _ _ b => checkVar x *> checkFnBody b
| .del x b => checkVar x *> checkFnBody b
| .mdata _ b => checkFnBody b
| .jmp j ys => checkJP j *> checkArgs ys
| .ret x => checkArg x
| .case _ x _ alts => checkVar x *> alts.forM (fun alt => checkFnBody alt.body)
| .unreachable => pure ()
def checkDecl : Decl → M Unit
| Decl.fdecl (xs := xs) (body := b) .. => withParams xs (checkFnBody b)
| Decl.extern (xs := xs) .. => withParams xs (pure ())
| .fdecl (xs := xs) (body := b) .. => withParams xs (checkFnBody b)
| .extern (xs := xs) .. => withParams xs (pure ())
end Checker

2
src/Lean/Compiler/IR/CompilerM.lean
View file

@ -142,7 +142,7 @@ def getDecl' (n : Name) (decls : Array Decl) : CompilerM Decl := do
@[export lean_decl_get_sorry_dep]
def getSorryDep (env : Environment) (declName : Name) : Option Name :=
match (declMapExt.getState env).find? declName with
| some (Decl.fdecl (info := { sorryDep? := dep?, .. }) ..) => dep?
| some (.fdecl (info := { sorryDep? := dep?, .. }) ..) => dep?
| _ => none
end IR

6
src/Lean/Compiler/IR/ElimDeadBranches.lean
View file

@ -271,7 +271,7 @@ def inferStep : M Bool := do
modify fun s => { s with assignments := ctx.decls.map fun _ => {} }
ctx.decls.size.foldM (init := false) fun idx modified => do
match ctx.decls[idx]! with
| Decl.fdecl (xs := ys) (body := b) .. => do
| .fdecl (xs := ys) (body := b) .. => do
let s ← get
let currVals := s.funVals[idx]!
withReader (fun ctx => { ctx with currFnIdx := idx }) do
@ -280,7 +280,7 @@ def inferStep : M Bool := do
let s ← get
let newVals := s.funVals[idx]!
pure (modified || currVals != newVals)
| Decl.extern .. => pure modified
| .extern .. => pure modified
partial def inferMain : M Unit := do
let modified ← inferStep
@ -305,7 +305,7 @@ partial def elimDeadAux (assignment : Assignment) : FnBody → FnBody
partial def elimDead (assignment : Assignment) (d : Decl) : Decl :=
match d with
| Decl.fdecl (body := b) .. => d.updateBody! <| elimDeadAux assignment b
| .fdecl (body := b) .. => d.updateBody! <| elimDeadAux assignment b
| other => other
end UnreachableBranches

2
src/Lean/Compiler/IR/ElimDeadVars.lean
View file

@ -41,7 +41,7 @@ partial def FnBody.elimDead (b : FnBody) : FnBody :=
/-- Eliminate dead let-declarations and join points -/
def Decl.elimDead (d : Decl) : Decl :=
match d with
| Decl.fdecl (body := b) .. => d.updateBody! b.elimDead
| .fdecl (body := b) .. => d.updateBody! b.elimDead
| other => other
end Lean.IR

4
src/Lean/Compiler/IR/EmitC.lean
View file

@ -137,7 +137,7 @@ def emitFnDecls : M Unit := do
def emitMainFn : M Unit := do
let d ← getDecl `main
match d with
| Decl.fdecl (xs := xs) .. => do
| .fdecl (xs := xs) .. => do
unless xs.size == 2 || xs.size == 1 do throw "invalid main function, incorrect arity when generating code"
let env ← getEnv
let usesLeanAPI := usesModuleFrom env `Lean
@ -644,7 +644,7 @@ def emitDeclAux (d : Decl) : M Unit := do
withReader (fun ctx => { ctx with jpMap := jpMap }) do
unless hasInitAttr env d.name do
match d with
| Decl.fdecl (f := f) (xs := xs) (type := t) (body := b) .. =>
| .fdecl (f := f) (xs := xs) (type := t) (body := b) .. =>
let baseName ← toCName f;
if xs.size == 0 then
emit "static "

26
src/Lean/Compiler/IR/EmitUtil.lean
View file

@ -26,13 +26,13 @@ abbrev M := ReaderT Environment (StateM NameSet)
modify fun s => s.insert f
partial def collectFnBody : FnBody → M Unit
| FnBody.vdecl _ _ v b =>
| .vdecl _ _ v b =>
match v with
| Expr.fap f _ => collect f *> collectFnBody b
| Expr.pap f _ => collect f *> collectFnBody b
| _ => collectFnBody b
| FnBody.jdecl _ _ v b => collectFnBody v *> collectFnBody b
| FnBody.case _ _ _ alts => alts.forM fun alt => collectFnBody alt.body
| .fap f _ => collect f *> collectFnBody b
| .pap f _ => collect f *> collectFnBody b
| _ => collectFnBody b
| .jdecl _ _ v b => collectFnBody v *> collectFnBody b
| .case _ _ _ alts => alts.forM fun alt => collectFnBody alt.body
| e => do unless e.isTerminal do collectFnBody e.body
def collectInitDecl (fn : Name) : M Unit := do
@ -42,8 +42,8 @@ def collectInitDecl (fn : Name) : M Unit := do
| _ => pure ()
def collectDecl : Decl → M NameSet
| Decl.fdecl (f := f) (body := b) .. => collectInitDecl f *> CollectUsedDecls.collectFnBody b *> get
| Decl.extern (f := f) .. => collectInitDecl f *> get
| .fdecl (f := f) (body := b) .. => collectInitDecl f *> CollectUsedDecls.collectFnBody b *> get
| .extern (f := f) .. => collectInitDecl f *> get
end CollectUsedDecls
@ -64,13 +64,13 @@ def collectParams (ps : Array Param) : Collector :=
/-- `collectFnBody` assumes the variables in -/
partial def collectFnBody : FnBody → Collector
| FnBody.vdecl x t _ b => collectVar x t ∘ collectFnBody b
| FnBody.jdecl j xs v b => collectJP j xs ∘ collectParams xs ∘ collectFnBody v ∘ collectFnBody b
| FnBody.case _ _ _ alts => fun s => alts.foldl (fun s alt => collectFnBody alt.body s) s
| e => if e.isTerminal then id else collectFnBody e.body
| .vdecl x t _ b => collectVar x t ∘ collectFnBody b
| .jdecl j xs v b => collectJP j xs ∘ collectParams xs ∘ collectFnBody v ∘ collectFnBody b
| .case _ _ _ alts => fun s => alts.foldl (fun s alt => collectFnBody alt.body s) s
| e => if e.isTerminal then id else collectFnBody e.body
def collectDecl : Decl → Collector
| Decl.fdecl (xs := xs) (body := b) .. => collectParams xs ∘ collectFnBody b
| .fdecl (xs := xs) (body := b) .. => collectParams xs ∘ collectFnBody b
| _ => id
end CollectMaps

34
src/Lean/Compiler/IR/ExpandResetReuse.lean
View file

@ -14,23 +14,23 @@ namespace CollectProjMap
abbrev Collector := ProjMap → ProjMap
@[inline] def collectVDecl (x : VarId) (v : Expr) : Collector := fun m =>
match v with
| Expr.proj .. => m.insert x v
| Expr.sproj .. => m.insert x v
| Expr.uproj .. => m.insert x v
| _ => m
| .proj .. => m.insert x v
| .sproj .. => m.insert x v
| .uproj .. => m.insert x v
| _ => m
partial def collectFnBody : FnBody → Collector
| FnBody.vdecl x _ v b => collectVDecl x v ∘ collectFnBody b
| FnBody.jdecl _ _ v b => collectFnBody v ∘ collectFnBody b
| FnBody.case _ _ _ alts => fun s => alts.foldl (fun s alt => collectFnBody alt.body s) s
| e => if e.isTerminal then id else collectFnBody e.body
| .vdecl x _ v b => collectVDecl x v ∘ collectFnBody b
| .jdecl _ _ v b => collectFnBody v ∘ collectFnBody b
| .case _ _ _ alts => fun s => alts.foldl (fun s alt => collectFnBody alt.body s) s
| e => if e.isTerminal then id else collectFnBody e.body
end CollectProjMap
/-- Create a mapping from variables to projections.
This function assumes variable ids have been normalized -/
def mkProjMap (d : Decl) : ProjMap :=
match d with
| Decl.fdecl (body := b) .. => CollectProjMap.collectFnBody b {}
| .fdecl (body := b) .. => CollectProjMap.collectFnBody b {}
| _ => {}
structure Context where
@ -39,12 +39,12 @@ structure Context where
/-- Return true iff `x` is consumed in all branches of the current block.
Here consumption means the block contains a `dec x` or `reuse x ...`. -/
partial def consumed (x : VarId) : FnBody → Bool
| FnBody.vdecl _ _ v b =>
| .vdecl _ _ v b =>
match v with
| Expr.reuse y _ _ _ => x == y || consumed x b
| _ => consumed x b
| FnBody.dec y _ _ _ b => x == y || consumed x b
| FnBody.case _ _ _ alts => alts.all fun alt => consumed x alt.body
| .dec y _ _ _ b => x == y || consumed x b
| .case _ _ _ alts => alts.all fun alt => consumed x alt.body
| e => !e.isTerminal && consumed x e.body
abbrev Mask := Array (Option VarId)
@ -57,13 +57,13 @@ partial def eraseProjIncForAux (y : VarId) (bs : Array FnBody) (mask : Mask) (ke
else
let b := bs.back
match b with
| (FnBody.vdecl _ _ (Expr.sproj _ _ _) _) => keepInstr b
| (FnBody.vdecl _ _ (Expr.uproj _ _) _) => keepInstr b
| (FnBody.inc z n c p _) =>
| .vdecl _ _ (.sproj _ _ _) _ => keepInstr b
| .vdecl _ _ (.uproj _ _) _ => keepInstr b
| .inc z n c p _ =>
if n == 0 then done () else
let b' := bs[bs.size - 2]!
match b' with
| (FnBody.vdecl w _ (Expr.proj i x) _) =>
| .vdecl w _ (.proj i x) _ =>
if w == z && y == x then
/- Found
```
@ -264,7 +264,7 @@ partial def searchAndExpand : FnBody → Array FnBody → M FnBody
def main (d : Decl) : Decl :=
match d with
| Decl.fdecl (body := b) .. =>
| .fdecl (body := b) .. =>
let m := mkProjMap d
let nextIdx := d.maxIndex + 1
let bNew := (searchAndExpand b #[] { projMap := m }).run' nextIdx

4
src/Lean/Compiler/IR/FreeVars.lean
View file

@ -73,8 +73,8 @@ partial def collectFnBody : FnBody → Collector
| FnBody.unreachable => skip
partial def collectDecl : Decl → Collector
| Decl.fdecl (xs := xs) (body := b) .. => collectParams xs >> collectFnBody b
| Decl.extern (xs := xs) .. => collectParams xs
| .fdecl (xs := xs) (body := b) .. => collectParams xs >> collectFnBody b
| .extern (xs := xs) .. => collectParams xs
end MaxIndex

12
src/Lean/Compiler/IR/NormIds.lean
View file

@ -18,14 +18,14 @@ def checkParams (ps : Array Param) : M Bool :=
ps.allM fun p => checkId p.x.idx
partial def checkFnBody : FnBody → M Bool
| FnBody.vdecl x _ _ b => checkId x.idx <&&> checkFnBody b
| FnBody.jdecl j ys _ b => checkId j.idx <&&> checkParams ys <&&> checkFnBody b
| FnBody.case _ _ _ alts => alts.allM fun alt => checkFnBody alt.body
| b => if b.isTerminal then pure true else checkFnBody b.body
| .vdecl x _ _ b => checkId x.idx <&&> checkFnBody b
| .jdecl j ys _ b => checkId j.idx <&&> checkParams ys <&&> checkFnBody b
| .case _ _ _ alts => alts.allM fun alt => checkFnBody alt.body
| b => if b.isTerminal then pure true else checkFnBody b.body
partial def checkDecl : Decl → M Bool
| Decl.fdecl (xs := xs) (body := b) .. => checkParams xs <&&> checkFnBody b
| Decl.extern (xs := xs) .. => checkParams xs
| .fdecl (xs := xs) (body := b) .. => checkParams xs <&&> checkFnBody b
| .extern (xs := xs) .. => checkParams xs
end UniqueIds

4
src/Lean/Compiler/IR/PushProj.lean
View file

@ -40,7 +40,7 @@ partial def FnBody.pushProj (b : FnBody) : FnBody :=
let (bs, term) := b.flatten
let bs := modifyJPs bs pushProj
match term with
| FnBody.case tid x xType alts =>
| .case tid x xType alts =>
let altsF := alts.map fun alt => alt.body.freeIndices
let (bs, alts) := pushProjs bs alts altsF #[] (mkIndexSet x.idx)
let alts := alts.map fun alt => alt.modifyBody pushProj
@ -51,7 +51,7 @@ partial def FnBody.pushProj (b : FnBody) : FnBody :=
/-- Push projections inside `case` branches. -/
def Decl.pushProj (d : Decl) : Decl :=
match d with
| Decl.fdecl (body := b) .. => d.updateBody! b.pushProj |>.normalizeIds
| .fdecl (body := b) .. => d.updateBody! b.pushProj |>.normalizeIds
| other => other
end Lean.IR

2
src/Lean/Compiler/IR/RC.lean
View file

@ -266,7 +266,7 @@ partial def visitFnBody : FnBody → Context → (FnBody × LiveVarSet)
partial def visitDecl (env : Environment) (decls : Array Decl) (d : Decl) : Decl :=
match d with
| Decl.fdecl (xs := xs) (body := b) .. =>
| .fdecl (xs := xs) (body := b) .. =>
let ctx : Context := { env := env, decls := decls }
let ctx := updateVarInfoWithParams ctx xs
let (b, bLiveVars) := visitFnBody b ctx

2
src/Lean/Compiler/IR/ResetReuse.lean
View file

@ -150,7 +150,7 @@ open ResetReuse
def Decl.insertResetReuse (d : Decl) : Decl :=
match d with
| Decl.fdecl (body := b) ..=>
| .fdecl (body := b) ..=>
let nextIndex := d.maxIndex + 1
let bNew := (R b {}).run' nextIndex
d.updateBody! bNew

2
src/Lean/Compiler/IR/SimpCase.lean
View file

@ -71,7 +71,7 @@ partial def FnBody.simpCase (b : FnBody) : FnBody :=
- Merge most common branches using `Alt.default`. -/
def Decl.simpCase (d : Decl) : Decl :=
match d with
| Decl.fdecl (body := b) .. => d.updateBody! b.simpCase
| .fdecl (body := b) .. => d.updateBody! b.simpCase
| other => other
end Lean.IR

14
src/Lean/Compiler/IR/Sorry.lean
View file

@ -30,14 +30,14 @@ where
else if let some g := (← get).localSorryMap.find? f then
found g
else match (← findDecl f) with
| Decl.fdecl (info := { sorryDep? := some g, .. }) .. => found g
| some (.fdecl (info := { sorryDep? := some g, .. }) ..) => found g
| _ => return ()
partial def visitFndBody (b : FnBody) : ExceptT Name M Unit := do
match b with
| FnBody.vdecl _ _ v b => visitExpr v; visitFndBody b
| FnBody.jdecl _ _ v b => visitFndBody v; visitFndBody b
| FnBody.case _ _ _ alts => alts.forM fun alt => visitFndBody alt.body
| .vdecl _ _ v b => visitExpr v; visitFndBody b
| .jdecl _ _ v b => visitFndBody v; visitFndBody b
| .case _ _ _ alts => alts.forM fun alt => visitFndBody alt.body
| _ =>
unless b.isTerminal do
let (_, b) := b.split
@ -45,13 +45,13 @@ partial def visitFndBody (b : FnBody) : ExceptT Name M Unit := do
def visitDecl (d : Decl) : M Unit := do
match d with
| Decl.fdecl (f := f) (body := b) .. =>
| .fdecl (f := f) (body := b) .. =>
match (← get).localSorryMap.find? f with
| some _ => return ()
| none =>
match (← visitFndBody b |>.run) with
| Except.ok _ => return ()
| Except.error g =>
| .ok _ => return ()
| .error g =>
modify fun s => {
localSorryMap := s.localSorryMap.insert f g
modified := true

4
src/Lean/Elab/InfoTree/Main.lean
View file

@ -115,8 +115,8 @@ def TermInfo.format (ctx : ContextInfo) (info : TermInfo) : IO Format := do
def CompletionInfo.format (ctx : ContextInfo) (info : CompletionInfo) : IO Format :=
match info with
| CompletionInfo.dot i (expectedType? := expectedType?) .. => return f!"[.] {← i.format ctx} : {expectedType?}"
| CompletionInfo.id stx _ _ lctx expectedType? => ctx.runMetaM lctx do return f!"[.] {stx} : {expectedType?} @ {formatStxRange ctx info.stx}"
| .dot i (expectedType? := expectedType?) .. => return f!"[.] {← i.format ctx} : {expectedType?}"
| .id stx _ _ lctx expectedType? => ctx.runMetaM lctx do return f!"[.] {stx} : {expectedType?} @ {formatStxRange ctx info.stx}"
| _ => return f!"[.] {info.stx} @ {formatStxRange ctx info.stx}"
def CommandInfo.format (ctx : ContextInfo) (info : CommandInfo) : IO Format := do

2
src/Lean/Elab/Term.lean
View file

@ -678,7 +678,7 @@ partial def visit (e : Expr) : M Unit := do
| .fvar fvarId .. =>
match (← fvarId.getDecl) with
| .cdecl .. => return ()
| LocalDecl.ldecl (value := v) .. => visit v
| .ldecl (value := v) .. => visit v
| .mvar mvarId .. =>
let e' ← instantiateMVars e
if e' != e then

4
src/Lean/Meta/Basic.lean
View file

@ -1420,10 +1420,10 @@ end Methods
def isInductivePredicate (declName : Name) : MetaM Bool := do
match (← getEnv).find? declName with
| some (ConstantInfo.inductInfo { type := type, ..}) =>
| some (.inductInfo { type := type, ..}) =>
forallTelescopeReducing type fun _ type => do
match (← whnfD type) with
| Expr.sort u .. => return u == levelZero
| .sort u .. => return u == levelZero
| _ => return false
| _ => return false

4
src/Lean/Meta/Check.lean
View file

@ -163,10 +163,10 @@ where
xs.forM fun x => do
let xDecl ← getFVarLocalDecl x;
match xDecl with
| LocalDecl.cdecl (type := t) .. =>
| .cdecl (type := t) .. =>
ensureType t
check t
| LocalDecl.ldecl (type := t) (value := v) .. =>
| .ldecl (type := t) (value := v) .. =>
ensureType t
check t
let vType ← inferType v

4
src/Lean/Meta/CollectFVars.lean
View file

@ -16,8 +16,8 @@ def Expr.collectFVars (e : Expr) : StateRefT CollectFVars.State MetaM Unit := do
def LocalDecl.collectFVars (localDecl : LocalDecl) : StateRefT CollectFVars.State MetaM Unit := do
match localDecl with
| LocalDecl.cdecl (type := type) .. => type.collectFVars
| LocalDecl.ldecl (type := type) (value := value) .. => type.collectFVars; value.collectFVars
| .cdecl (type := type) .. => type.collectFVars
| .ldecl (type := type) (value := value) .. => type.collectFVars; value.collectFVars
/-- For each variable in `s.fvarSet`, include its dependencies. -/
partial def CollectFVars.State.addDependencies (s : CollectFVars.State) : MetaM CollectFVars.State := do

8
src/Lean/Meta/DiscrTree.lean
View file

@ -541,7 +541,7 @@ partial def getUnify (d : DiscrTree α) (e : Expr) : MetaM (Array α) :=
withReducible do
let (k, args) ← getUnifyKeyArgs e (root := true)
match k with
| Key.star => d.root.foldlM (init := #[]) fun result k c => process k.arity #[] c result
| .star => d.root.foldlM (init := #[]) fun result k c => process k.arity #[] c result
| _ =>
let result := getStarResult d
match d.root.find? k with
@ -575,9 +575,9 @@ where
| none => return result
| some c => process 0 (todo ++ args) c.2 result
match k with
| Key.star => cs.foldlM (init := result) fun result ⟨k, c⟩ => process k.arity todo c result
| .star => cs.foldlM (init := result) fun result ⟨k, c⟩ => process k.arity todo c result
-- See comment a `getMatch` regarding non-dependent arrows vs dependent arrows
| Key.arrow => visitNonStar Key.other #[] (← visitNonStar k args (← visitStar result))
| _ => visitNonStar k args (← visitStar result)
| .arrow => visitNonStar Key.other #[] (← visitNonStar k args (← visitStar result))
| _ => visitNonStar k args (← visitStar result)
end Lean.Meta.DiscrTree

2
src/Lean/Meta/ExprDefEq.lean
View file

@ -673,7 +673,7 @@ mutual
else
let lctx := ctxMeta.lctx
match lctx.findFVar? fvar with
| some (LocalDecl.ldecl (value := v) ..) => visit check v
| some (.ldecl (value := v) ..) => visit check v
| _ =>
if ctx.fvars.contains fvar then pure fvar
else

28
src/Lean/Meta/WHNF.lean
View file

@ -283,21 +283,21 @@ end
/-- Auxiliary combinator for handling easy WHNF cases. It takes a function for handling the "hard" cases as an argument -/
@[specialize] partial def whnfEasyCases (e : Expr) (k : Expr → MetaM Expr) : MetaM Expr := do
match e with
| Expr.forallE .. => return e
| Expr.lam .. => return e
| Expr.sort .. => return e
| Expr.lit .. => return e
| Expr.bvar .. => unreachable!
| Expr.letE .. => k e
| Expr.const .. => k e
| Expr.app .. => k e
| Expr.proj .. => k e
| Expr.mdata _ e => whnfEasyCases e k
| Expr.fvar fvarId =>
| .forallE .. => return e
| .lam .. => return e
| .sort .. => return e
| .lit .. => return e
| .bvar .. => unreachable!
| .letE .. => k e
| .const .. => k e
| .app .. => k e
| .proj .. => k e
| .mdata _ e => whnfEasyCases e k
| .fvar fvarId =>
let decl ← fvarId.getDecl
match decl with
| LocalDecl.cdecl .. => return e
| LocalDecl.ldecl (value := v) (nonDep := nonDep) .. =>
| .cdecl .. => return e
| .ldecl (value := v) (nonDep := nonDep) .. =>
let cfg ← getConfig
if nonDep && !cfg.zetaNonDep then
return e
@ -305,7 +305,7 @@ end
if cfg.trackZeta then
modify fun s => { s with zetaFVarIds := s.zetaFVarIds.insert fvarId }
whnfEasyCases v k
| Expr.mvar mvarId =>
| .mvar mvarId =>
match (← getExprMVarAssignment? mvarId) with
| some v => whnfEasyCases v k
| none => return e

4
src/Lean/MetavarContext.lean
View file

@ -676,8 +676,8 @@ end DependsOn
depends on a free variable `x` s.t. `pf x` is `true` or an unassigned metavariable `?m` s.t. `pm ?m` is true. -/
@[inline] def findLocalDeclDependsOn [Monad m] [MonadMCtx m] (localDecl : LocalDecl) (pf : FVarId → Bool := fun _ => false) (pm : MVarId → Bool := fun _ => false) : m Bool := do
match localDecl with
| LocalDecl.cdecl (type := t) .. => findExprDependsOn t pf pm
| LocalDecl.ldecl (type := t) (value := v) .. =>
| .cdecl (type := t) .. => findExprDependsOn t pf pm
| .ldecl (type := t) (value := v) .. =>
let (result, { mctx, .. }) := (DependsOn.main pf pm t <||> DependsOn.main pf pm v).run { mctx := (← getMCtx) }
setMCtx mctx
return result

8
src/Lean/Server/Completion.lean
View file

@ -421,10 +421,10 @@ partial def find? (fileMap : FileMap) (hoverPos : String.Pos) (infoTree : InfoTr
match infoTree.foldInfo (init := none) (choose fileMap hoverLine) with
| some (hoverInfo, ctx, Info.ofCompletionInfo info) =>
match info with
| CompletionInfo.dot info (expectedType? := expectedType?) .. => dotCompletion ctx info hoverInfo expectedType?
| CompletionInfo.id _ id danglingDot lctx expectedType? => idCompletion ctx lctx id hoverInfo danglingDot expectedType?
| CompletionInfo.option stx => optionCompletion ctx stx caps
| CompletionInfo.tactic .. => tacticCompletion ctx
| .dot info (expectedType? := expectedType?) .. => dotCompletion ctx info hoverInfo expectedType?
| .id _ id danglingDot lctx expectedType? => idCompletion ctx lctx id hoverInfo danglingDot expectedType?
| .option stx => optionCompletion ctx stx caps
| .tactic .. => tacticCompletion ctx
| _ => return none
| _ =>
-- TODO try to extract id from `fileMap` and some `ContextInfo` from `InfoTree`

8
src/Lean/Structure.lean
View file

@ -68,7 +68,7 @@ def getStructureInfo? (env : Environment) (structName : Name) : Option Structure
def getStructureCtor (env : Environment) (constName : Name) : ConstructorVal :=
match env.find? constName with
| some (ConstantInfo.inductInfo { isRec := false, ctors := [ctorName], .. }) =>
| some (.inductInfo { isRec := false, ctors := [ctorName], .. }) =>
match env.find? ctorName with
| some (ConstantInfo.ctorInfo val) => val
| _ => panic! "ill-formed environment"
@ -193,15 +193,15 @@ def getPathToBaseStructure? (env : Environment) (baseStructName : Name) (structN
/-- Return true iff `constName` is the a non-recursive inductive datatype that has only one constructor. -/
def isStructureLike (env : Environment) (constName : Name) : Bool :=
match env.find? constName with
| some (ConstantInfo.inductInfo { isRec := false, ctors := [_], numIndices := 0, .. }) => true
| some (.inductInfo { isRec := false, ctors := [_], numIndices := 0, .. }) => true
| _ => false
/-- Return number of fields for a structure-like type -/
def getStructureLikeNumFields (env : Environment) (constName : Name) : Nat :=
match env.find? constName with
| some (ConstantInfo.inductInfo { isRec := false, ctors := [ctor], numIndices := 0, .. }) =>
| some (.inductInfo { isRec := false, ctors := [ctor], numIndices := 0, .. }) =>
match env.find? ctor with
| some (ConstantInfo.ctorInfo { numFields := n, .. }) => n
| some (.ctorInfo { numFields := n, .. }) => n
| _ => 0
| _ => 0

28
src/Lean/Util/FindLevelMVar.lean
View file

@ -16,26 +16,26 @@ mutual
if s.isSome || !e.hasLevelMVar then s else main p e s
partial def main (p : LMVarId → Bool) : Expr → Visitor
| Expr.sort l => visitLevel p l
| Expr.const _ ls => ls.foldr (init := id) fun l acc => visitLevel p l ∘ acc
| Expr.forallE _ d b _ => visit p b ∘ visit p d
| Expr.lam _ d b _ => visit p b ∘ visit p d
| Expr.letE _ t v b _ => visit p b ∘ visit p v ∘ visit p t
| Expr.app f a => visit p a ∘ visit p f
| Expr.mdata _ b => visit p b
| Expr.proj _ _ e => visit p e
| .sort l => visitLevel p l
| .const _ ls => ls.foldr (init := id) fun l acc => visitLevel p l ∘ acc
| .forallE _ d b _ => visit p b ∘ visit p d
| .lam _ d b _ => visit p b ∘ visit p d
| .letE _ t v b _ => visit p b ∘ visit p v ∘ visit p t
| .app f a => visit p a ∘ visit p f
| .mdata _ b => visit p b
| .proj _ _ e => visit p e
| _ => id
partial def visitLevel (p : LMVarId → Bool) (l : Level) : Visitor := fun s =>
if s.isSome || !l.hasMVar then s else mainLevel p l s
partial def mainLevel (p : LMVarId → Bool) : Level → Visitor
| Level.zero => id
| Level.succ l => visitLevel p l
| Level.max l₁ l₂ => visitLevel p l₁ ∘ visitLevel p l₂
| Level.imax l₁ l₂ => visitLevel p l₁ ∘ visitLevel p l₂
| Level.param _ => id
| Level.mvar mvarId => fun s => if p mvarId then some mvarId else s
| .zero => id
| .succ l => visitLevel p l
| .max l₁ l₂ => visitLevel p l₁ ∘ visitLevel p l₂
| .imax l₁ l₂ => visitLevel p l₁ ∘ visitLevel p l₂
| .param _ => id
| .mvar mvarId => fun s => if p mvarId then some mvarId else s
end
end FindLevelMVar