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

chore: move to new frontend

Browse source
This commit is contained in:
Leonardo de Moura 2020-10-19 12:15:48 -07:00
parent ab047cc4d1
commit c3897fff31
1 changed files with 32 additions and 35 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

67
src/Lean/Meta/FunInfo.lean
View file

@ -1,3 +1,4 @@
#lang lean4
/-
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
@ -6,37 +7,35 @@ Authors: Leonardo de Moura
import Lean.Meta.Basic
import Lean.Meta.InferType
namespace Lean
namespace Meta
namespace Lean.Meta
@[inline] private def checkFunInfoCache (fn : Expr) (maxArgs? : Option Nat) (k : MetaM FunInfo) : MetaM FunInfo := do
s ← get;
t ← getTransparency;
let s ← get
let t ← getTransparency
match s.cache.funInfo.find? ⟨t, fn, maxArgs?⟩ with
| some finfo => pure finfo
| none => do
finfo ← k;
modify $ fun s => { s with cache := { s.cache with funInfo := s.cache.funInfo.insert ⟨t, fn, maxArgs?⟩ finfo } };
let finfo ← k
modify fun s => { s with cache := { s.cache with funInfo := s.cache.funInfo.insert ⟨t, fn, maxArgs?⟩ finfo } }
pure finfo
@[inline] private def whenHasVar {α} (e : Expr) (deps : α) (k : α → α) : α :=
if e.hasFVar then k deps else deps
private def collectDepsAux (fvars : Array Expr) : Expr → Array Nat → Array Nat
| e@(Expr.app f a _), deps => whenHasVar e deps (collectDepsAux a ∘ collectDepsAux f)
| e@(Expr.forallE _ d b _), deps => whenHasVar e deps (collectDepsAux b ∘ collectDepsAux d)
| e@(Expr.lam _ d b _), deps => whenHasVar e deps (collectDepsAux b ∘ collectDepsAux d)
| e@(Expr.letE _ t v b _), deps => whenHasVar e deps (collectDepsAux b ∘ collectDepsAux v ∘ collectDepsAux t)
| Expr.proj _ _ e _, deps => collectDepsAux e deps
| Expr.mdata _ e _, deps => collectDepsAux e deps
private def collectDeps (fvars : Array Expr) (e : Expr) : Array Nat :=
let rec visit : Expr → Array Nat → Array Nat
| e@(Expr.app f a _), deps => whenHasVar e deps (visit a ∘ visit f)
| e@(Expr.forallE _ d b _), deps => whenHasVar e deps (visit b ∘ visit d)
| e@(Expr.lam _ d b _), deps => whenHasVar e deps (visit b ∘ visit d)
| e@(Expr.letE _ t v b _), deps => whenHasVar e deps (visit b ∘ visit v ∘ visit t)
| Expr.proj _ _ e _, deps => visit e deps
| Expr.mdata _ e _, deps => visit e deps
| e@(Expr.fvar _ _), deps =>
match fvars.indexOf? e with
| none => deps
| some i => if deps.contains i.val then deps else deps.push i.val
| _, deps => deps
private def collectDeps (fvars : Array Expr) (e : Expr) : Array Nat :=
let deps := collectDepsAux fvars e #[];
let deps := visit e #[]
deps.qsort (fun i j => i < j)
/-- Update `hasFwdDeps` fields using new `backDeps` -/
@ -45,7 +44,7 @@ if backDeps.size == 0 then
pinfo
else
-- update hasFwdDeps fields
pinfo.mapIdx $ fun i info =>
pinfo.mapIdx fun i info =>
if info.hasFwdDeps then info
else if backDeps.contains i then
{ info with hasFwdDeps := true }
@ -53,23 +52,22 @@ else
info
private def getFunInfoAux (fn : Expr) (maxArgs? : Option Nat) : MetaM FunInfo :=
checkFunInfoCache fn maxArgs? $ do
fnType ← inferType fn;
checkFunInfoCache fn maxArgs? do
let fnType ← inferType fn
withTransparency TransparencyMode.default $
forallBoundedTelescope fnType maxArgs? $ fun fvars type => do
pinfo ← fvars.size.foldM
(fun (i : Nat) (pinfo : Array ParamInfo) => do
let fvar := fvars.get! i;
decl ← getFVarLocalDecl fvar;
let backDeps := collectDeps fvars decl.type;
let pinfo := updateHasFwdDeps pinfo backDeps;
pure $ pinfo.push {
backDeps := backDeps,
implicit := decl.binderInfo == BinderInfo.implicit,
instImplicit := decl.binderInfo == BinderInfo.instImplicit })
#[];
let resultDeps := collectDeps fvars type;
let pinfo := updateHasFwdDeps pinfo resultDeps;
forallBoundedTelescope fnType maxArgs? fun fvars type => do
let pinfo := #[]
for i in [:fvars.size] do
let fvar := fvars[i]
let decl ← getFVarLocalDecl fvar
let backDeps := collectDeps fvars decl.type
let pinfo := updateHasFwdDeps pinfo backDeps
pinfo := pinfo.push {
backDeps := backDeps,
implicit := decl.binderInfo == BinderInfo.implicit,
instImplicit := decl.binderInfo == BinderInfo.instImplicit }
let resultDeps := collectDeps fvars type
let pinfo := updateHasFwdDeps pinfo resultDeps
pure { resultDeps := resultDeps, paramInfo := pinfo }
def getFunInfo (fn : Expr) : MetaM FunInfo :=
@ -78,5 +76,4 @@ getFunInfoAux fn none
def getFunInfoNArgs (fn : Expr) (nargs : Nat) : MetaM FunInfo :=
getFunInfoAux fn (some nargs)
end Meta
end Lean
end Lean.Meta