chore: cleanup
This commit is contained in:
Leonardo de Moura
parent
0795243a5e
commit
da69b10056
5 changed files with 91 additions and 85 deletions
|
|
@ -14,19 +14,21 @@ structure State where
|
|||
|
||||
abbrev Visitor := State → State
|
||||
|
||||
@[inline] def visit (f : Expr → Visitor) (e : Expr) : Visitor := fun s =>
|
||||
if !e.hasFVar || s.visitedExpr.contains e then s
|
||||
else f e { s with visitedExpr := s.visitedExpr.insert e }
|
||||
mutual
|
||||
partial def visit (e : Expr) : Visitor := fun s =>
|
||||
if !e.hasFVar || s.visitedExpr.contains e then s
|
||||
else main e { s with visitedExpr := s.visitedExpr.insert e }
|
||||
|
||||
partial def main : Expr → Visitor
|
||||
| Expr.proj _ _ e _ => visit main e
|
||||
| Expr.forallE _ d b _ => visit main b ∘ visit main d
|
||||
| Expr.lam _ d b _ => visit main b ∘ visit main d
|
||||
| Expr.letE _ t v b _ => visit main b ∘ visit main v ∘ visit main t
|
||||
| Expr.app f a _ => visit main a ∘ visit main f
|
||||
| Expr.mdata _ b _ => visit main b
|
||||
| Expr.fvar fvarId _ => fun s => { s with fvarSet := s.fvarSet.insert fvarId }
|
||||
| _ => id
|
||||
partial def main : Expr → Visitor
|
||||
| Expr.proj _ _ e _ => visit e
|
||||
| Expr.forallE _ d b _ => visit b ∘ visit d
|
||||
| Expr.lam _ d b _ => visit b ∘ visit d
|
||||
| Expr.letE _ t v b _ => visit b ∘ visit v ∘ visit t
|
||||
| Expr.app f a _ => visit a ∘ visit f
|
||||
| Expr.mdata _ b _ => visit b
|
||||
| Expr.fvar fvarId _ => fun s => { s with fvarSet := s.fvarSet.insert fvarId }
|
||||
| _ => id
|
||||
end
|
||||
|
||||
end CollectFVars
|
||||
|
||||
|
|
|
|||
|
|
@ -18,32 +18,36 @@ instance : Inhabited State := ⟨{}⟩
|
|||
|
||||
abbrev Visitor := State → State
|
||||
|
||||
@[inline] def visitLevel (f : Level → Visitor) (u : Level) : Visitor := fun s =>
|
||||
if !u.hasParam || s.visitedLevel.contains u then s
|
||||
else f u { s with visitedLevel := s.visitedLevel.insert u }
|
||||
mutual
|
||||
partial def visitLevel (u : Level) : Visitor := fun s =>
|
||||
if !u.hasParam || s.visitedLevel.contains u then s
|
||||
else collect u { s with visitedLevel := s.visitedLevel.insert u }
|
||||
|
||||
partial def collect : Level → Visitor
|
||||
| Level.succ v _ => visitLevel collect v
|
||||
| Level.max u v _ => visitLevel collect v ∘ visitLevel collect u
|
||||
| Level.imax u v _ => visitLevel collect v ∘ visitLevel collect u
|
||||
| Level.param n _ => fun s => { s with params := s.params.push n }
|
||||
| _ => id
|
||||
partial def collect : Level → Visitor
|
||||
| Level.succ v _ => visitLevel v
|
||||
| Level.max u v _ => visitLevel v ∘ visitLevel u
|
||||
| Level.imax u v _ => visitLevel v ∘ visitLevel u
|
||||
| Level.param n _ => fun s => { s with params := s.params.push n }
|
||||
| _ => id
|
||||
end
|
||||
|
||||
@[inline] def visitExpr (f : Expr → Visitor) (e : Expr) : Visitor := fun s =>
|
||||
if !e.hasLevelParam then s
|
||||
else if s.visitedExpr.contains e then s
|
||||
else f e { s with visitedExpr := s.visitedExpr.insert e }
|
||||
mutual
|
||||
partial def visitExpr (e : Expr) : Visitor := fun s =>
|
||||
if !e.hasLevelParam then s
|
||||
else if s.visitedExpr.contains e then s
|
||||
else main e { s with visitedExpr := s.visitedExpr.insert e }
|
||||
|
||||
partial def main : Expr → Visitor
|
||||
| Expr.proj _ _ s _ => visitExpr main s
|
||||
| Expr.forallE _ d b _ => visitExpr main b ∘ visitExpr main d
|
||||
| Expr.lam _ d b _ => visitExpr main b ∘ visitExpr main d
|
||||
| Expr.letE _ t v b _ => visitExpr main b ∘ visitExpr main v ∘ visitExpr main t
|
||||
| Expr.app f a _ => visitExpr main a ∘ visitExpr main f
|
||||
| Expr.mdata _ b _ => visitExpr main b
|
||||
| Expr.const _ us _ => fun s => us.foldl (fun s u => visitLevel collect u s) s
|
||||
| Expr.sort u _ => visitLevel collect u
|
||||
| _ => id
|
||||
partial def main : Expr → Visitor
|
||||
| Expr.proj _ _ s _ => visitExpr s
|
||||
| Expr.forallE _ d b _ => visitExpr b ∘ visitExpr d
|
||||
| Expr.lam _ d b _ => visitExpr b ∘ visitExpr d
|
||||
| Expr.letE _ t v b _ => visitExpr b ∘ visitExpr v ∘ visitExpr t
|
||||
| Expr.app f a _ => visitExpr a ∘ visitExpr f
|
||||
| Expr.mdata _ b _ => visitExpr b
|
||||
| Expr.const _ us _ => fun s => us.foldl (fun s u => visitLevel u s) s
|
||||
| Expr.sort u _ => visitLevel u
|
||||
| _ => id
|
||||
end
|
||||
|
||||
partial def State.getUnusedLevelParam (s : CollectLevelParams.State) (pre : Name := `v) : Level :=
|
||||
let v := mkLevelParam pre;
|
||||
|
|
|
|||
|
|
@ -17,23 +17,25 @@ instance : Inhabited State := ⟨{}⟩
|
|||
|
||||
abbrev Visitor := State → State
|
||||
|
||||
@[inline] def visit (f : Expr → Visitor) (e : Expr) : Visitor := fun s =>
|
||||
if !e.hasMVar || s.visitedExpr.contains e then s
|
||||
else f e { s with visitedExpr := s.visitedExpr.insert e }
|
||||
mutual
|
||||
partial def visit (e : Expr) : Visitor := fun s =>
|
||||
if !e.hasMVar || s.visitedExpr.contains e then s
|
||||
else main e { s with visitedExpr := s.visitedExpr.insert e }
|
||||
|
||||
partial def main : Expr → Visitor
|
||||
| Expr.proj _ _ e _ => visit main e
|
||||
| Expr.forallE _ d b _ => visit main b ∘ visit main d
|
||||
| Expr.lam _ d b _ => visit main b ∘ visit main d
|
||||
| Expr.letE _ t v b _ => visit main b ∘ visit main v ∘ visit main t
|
||||
| Expr.app f a _ => visit main a ∘ visit main f
|
||||
| Expr.mdata _ b _ => visit main b
|
||||
| Expr.mvar mvarId _ => fun s => { s with result := s.result.push mvarId }
|
||||
| _ => id
|
||||
partial def main : Expr → Visitor
|
||||
| Expr.proj _ _ e _ => visit e
|
||||
| Expr.forallE _ d b _ => visit b ∘ visit d
|
||||
| Expr.lam _ d b _ => visit b ∘ visit d
|
||||
| Expr.letE _ t v b _ => visit b ∘ visit v ∘ visit t
|
||||
| Expr.app f a _ => visit a ∘ visit f
|
||||
| Expr.mdata _ b _ => visit b
|
||||
| Expr.mvar mvarId _ => fun s => { s with result := s.result.push mvarId }
|
||||
| _ => id
|
||||
end
|
||||
|
||||
end CollectMVars
|
||||
|
||||
def Expr.collectMVars (s : CollectMVars.State) (e : Expr) : CollectMVars.State :=
|
||||
CollectMVars.visit CollectMVars.main e s
|
||||
CollectMVars.visit e s
|
||||
|
||||
end Lean
|
||||
|
|
|
|||
|
|
@ -12,33 +12,32 @@ namespace FindLevelMVar
|
|||
abbrev Visitor := Option MVarId → Option MVarId
|
||||
|
||||
mutual
|
||||
partial def visit (p : MVarId → Bool) (e : Expr) : Visitor := fun s =>
|
||||
if s.isSome || !e.hasLevelMVar then s else main p e s
|
||||
partial def visit (p : MVarId → Bool) (e : Expr) : Visitor := fun s =>
|
||||
if s.isSome || !e.hasLevelMVar then s else main p e s
|
||||
|
||||
@[specialize]
|
||||
partial def main (p : MVarId → 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
|
||||
| _ => id
|
||||
@[specialize]
|
||||
partial def main (p : MVarId → 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
|
||||
| _ => id
|
||||
|
||||
partial def visitLevel (p : MVarId → Bool) (l : Level) : Visitor := fun s =>
|
||||
if s.isSome || !l.hasMVar then s else mainLevel p l s
|
||||
|
||||
@[specialize]
|
||||
partial def mainLevel (p : MVarId → 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 n _ => id
|
||||
| Level.mvar mvarId _ => fun s => if p mvarId then some mvarId else s
|
||||
partial def visitLevel (p : MVarId → Bool) (l : Level) : Visitor := fun s =>
|
||||
if s.isSome || !l.hasMVar then s else mainLevel p l s
|
||||
|
||||
@[specialize]
|
||||
partial def mainLevel (p : MVarId → 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 n _ => id
|
||||
| Level.mvar mvarId _ => fun s => if p mvarId then some mvarId else s
|
||||
end
|
||||
|
||||
end FindLevelMVar
|
||||
|
|
|
|||
|
|
@ -12,20 +12,19 @@ namespace FindMVar
|
|||
abbrev Visitor := Option MVarId → Option MVarId
|
||||
|
||||
mutual
|
||||
partial def visit (p : MVarId → Bool) (e : Expr) : Visitor := fun s =>
|
||||
if s.isSome || !e.hasMVar then s else main p e s
|
||||
|
||||
@[specialize]
|
||||
partial def main (p : MVarId → Bool) : Expr → Visitor
|
||||
| Expr.proj _ _ e _ => visit p e
|
||||
| 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.mvar mvarId _ => fun s => if s.isNone && p mvarId then some mvarId else s
|
||||
| _ => id
|
||||
partial def visit (p : MVarId → Bool) (e : Expr) : Visitor := fun s =>
|
||||
if s.isSome || !e.hasMVar then s else main p e s
|
||||
|
||||
@[specialize]
|
||||
partial def main (p : MVarId → Bool) : Expr → Visitor
|
||||
| Expr.proj _ _ e _ => visit p e
|
||||
| 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.mvar mvarId _ => fun s => if s.isNone && p mvarId then some mvarId else s
|
||||
| _ => id
|
||||
end
|
||||
|
||||
end FindMVar
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue