From c3897fff31d50ce10d337476a298ffb9b479dbb5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 19 Oct 2020 12:15:48 -0700
Subject: [PATCH] chore: move to new frontend

---
 src/Lean/Meta/FunInfo.lean | 67 ++++++++++++++++++--------------------
 1 file changed, 32 insertions(+), 35 deletions(-)

diff --git a/src/Lean/Meta/FunInfo.lean b/src/Lean/Meta/FunInfo.lean
index 3245426cd4..ee4ce0506a 100644
--- a/src/Lean/Meta/FunInfo.lean
+++ b/src/Lean/Meta/FunInfo.lean
@@ -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