From 3faa0337050a2e4d85d03aac2bc65365cf9bd93f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 7 Nov 2019 06:18:46 -0800
Subject: [PATCH] refactor: add parametric `whnfCore`

Motivation: `WHNFUtil` will provide a parametric implementation for
WHNF. We will use it to implement `TypeUtil` and `matchPattern`.
---
 library/Init/Lean/ProjFns.lean  |  29 ------
 library/Init/Lean/TypeUtil.lean | 103 -------------------
 library/Init/Lean/WHNFUtil.lean | 173 ++++++++++++++++++++++++++++----
 3 files changed, 154 insertions(+), 151 deletions(-)

diff --git a/library/Init/Lean/ProjFns.lean b/library/Init/Lean/ProjFns.lean
index c1457d16be..b55ba1e1f9 100644
--- a/library/Init/Lean/ProjFns.lean
+++ b/library/Init/Lean/ProjFns.lean
@@ -51,33 +51,4 @@ match env.getModuleIdxFor n with
 | none        => (projectionFnInfoExt.getState env).contains n
 
 end Environment
-
-@[specialize] def reduceProjectionFnAux {α} {m : Type → Type} [Monad m]
-    (whnf : Expr → m Expr)
-    (env : Environment) (projInfo : ProjectionFunctionInfo) (projArgs : Array Expr)
-    (failK : Unit → m α)
-    (successK : Expr → m α) : m α :=
-let majorIdx := projInfo.nparams;
-if h : majorIdx < projArgs.size then do
-  let major := projArgs.get ⟨majorIdx, h⟩;
-  major ← whnf major;
-  matchConst env major.getAppFn failK $ fun majorInfo majorLvls =>
-    let i := projInfo.nparams + projInfo.i;
-    if i < major.getAppNumArgs then
-      successK $ mkAppRange (major.getArg! i) (majorIdx + 1) projArgs.size projArgs
-    else
-      failK ()
-else
-  failK ()
-
-@[specialize] def reduceProjectionFn {α} {m : Type → Type} [Monad m]
-    (whnf : Expr → m Expr)
-    (env : Environment) (e : Expr)
-    (failK : Unit → m α)
-    (successK : Expr → m α) : m α :=
-matchConst env e.getAppFn failK $ fun cinfo _ =>
-  match env.getProjectionFnInfo cinfo.name with
-  | some projInfo => reduceProjectionFnAux whnf env projInfo e.getAppArgs failK successK
-  | none => failK ()
-
 end Lean
diff --git a/library/Init/Lean/TypeUtil.lean b/library/Init/Lean/TypeUtil.lean
index a4221b659d..f595cf1458 100644
--- a/library/Init/Lean/TypeUtil.lean
+++ b/library/Init/Lean/TypeUtil.lean
@@ -8,8 +8,6 @@ import Init.Control.Reader
 import Init.Lean.NameGenerator
 import Init.Lean.Environment
 import Init.Lean.Trace
-import Init.Lean.InductiveUtil
-import Init.Lean.QuotUtil
 import Init.Lean.AuxRecursor
 import Init.Lean.ProjFns
 
@@ -105,107 +103,6 @@ fun _ s =>
 
 export AbstractMetavarContext (hasAssignableLevelMVar isReadOnlyLevelMVar auxMVarSupport getExprAssignment)
 
-/- ===========================
-   Weak Head Normal Form
-   =========================== -/
-
-/-- Auxiliary combinator for handling easy WHNF cases. It takes a function for handling the "hard" cases as an argument -/
-@[specialize] private partial def whnfEasyCases [AbstractMetavarContext σ] : Expr → (Expr → TypeUtilM σ ϕ Expr) → TypeUtilM σ ϕ Expr
-| e@(Expr.forallE _ _ _ _), _ => pure e
-| e@(Expr.lam _ _ _ _),     _ => pure e
-| e@(Expr.sort _),          _ => pure e
-| e@(Expr.lit _),           _ => pure e
-| e@(Expr.bvar _),          _ => unreachable!
-| Expr.mdata _ e,           k => whnfEasyCases e k
-| e@(Expr.letE _ _ _ _),    k => do
-  c ← useZeta;
-  if c then k e else pure e
-| e@(Expr.fvar fvarId),     k => do
-  ctx ← read;
-  let ldecl := (ctx.lctx.find fvarId).get!;
-  match ldecl.valueOpt with
-  | none   => pure e
-  | some v => do
-    c ← useZeta;
-    if c then
-      whnfEasyCases v k
-    else
-      pure e
-| e@(Expr.mvar mvarId),     k => do
-  mctx ← getMCtx;
-  match getExprAssignment mctx mvarId with
-  | some v => whnfEasyCases v k
-  | none   => pure e
-| e@(Expr.const _ _),       k => k e
-| e@(Expr.app _ _),         k => k e
-| e@(Expr.proj _ _ _),      k => k e
-
-/-- Return true iff term is of the form `idRhs ...` -/
-private def isIdRhsApp (e : Expr) : Bool :=
-e.isAppOf `idRhs
-
-/-- (@idRhs T f a_1 ... a_n) ==> (f a_1 ... a_n) -/
-private def extractIdRhs (e : Expr) : Expr :=
-if !isIdRhsApp e then e
-else
-  let args := e.getAppArgs;
-  if args.size < 2 then e
-  else mkAppRange (args.get! 1) 2 args.size args
-
-@[specialize] private def deltaBetaDefinition {α} (c : ConstantInfo) (lvls : List Level) (revArgs : Array Expr) (failK : Unit → α) (successK : Expr → α) : α :=
-if c.lparams.length != lvls.length then failK ()
-else
-  let val := c.instantiateValueLevelParams lvls;
-  let val := val.betaRev revArgs;
-  successK (extractIdRhs val)
-
-/--
-  Apply beta-reduction, zeta-reduction (i.e., unfold let local-decls), iota-reduction,
-  expand let-expressions, expand assigned meta-variables.
-
-  This method does *not* apply delta-reduction at the head.
-  Reason: we want to perform these reductions lazily at isDefEq.
-
-  Remark: this method delta-reduce (transparent) aux-recursors (e.g., casesOn, recOon) IF
-  `reduceAuxRec == true` -/
-@[specialize] private partial def whnfCore
-    [AbstractMetavarContext σ]
-    (whnf : Expr → TypeUtilM σ ϕ Expr)
-    (inferType : Expr → TypeUtilM σ ϕ Expr)
-    (isDefEq : Expr → Expr → TypeUtilM σ ϕ Bool)
-    (reduceAuxRec? : Bool) : Expr → TypeUtilM σ ϕ Expr
-| e => whnfEasyCases e $ fun e =>
-  match e with
-  | e@(Expr.const _ _)    => pure e
-  | e@(Expr.letE _ _ v b) => whnfCore $ b.instantiate1 v
-  | e@(Expr.app f _)      => do
-    let f := f.getAppFn;
-    f' ← whnfCore f;
-    if f'.isLambda then
-      let revArgs := e.getAppRevArgs;
-      whnfCore $ f.betaRev revArgs
-    else do
-      let done : Unit → TypeUtilM σ ϕ Expr := fun _ =>
-        if f == f' then pure e else pure $ e.updateFn f';
-      env ← getEnv;
-      matchConst env f' done $ fun cinfo lvls =>
-        match cinfo with
-        | ConstantInfo.recInfo rec    => reduceRecAux whnf inferType isDefEq env rec lvls e.getAppArgs done whnfCore
-        | ConstantInfo.quotInfo rec   => reduceQuotRecAux whnf env rec lvls e.getAppArgs done whnfCore
-        | c@(ConstantInfo.defnInfo _) =>
-          if reduceAuxRec? && isAuxRecursor env c.name then
-            deltaBetaDefinition c lvls e.getAppArgs done whnfCore
-          else
-            done()
-        | _ => done ()
-  | e@(Expr.proj _ i c) => do
-    c   ← whnf c;
-    env ← getEnv;
-    matchConst env c.getAppFn (fun _ => pure e) $ fun cinfo lvls =>
-      match cinfo with
-      | ConstantInfo.ctorInfo ctorVal => pure $ c.getArgD (ctorVal.nparams + i) e
-      | _ => pure e
-  | _ => unreachable!
 
 private def whnfAux
     [AbstractMetavarContext σ]
diff --git a/library/Init/Lean/WHNFUtil.lean b/library/Init/Lean/WHNFUtil.lean
index 61278b9ed9..423f9548bf 100644
--- a/library/Init/Lean/WHNFUtil.lean
+++ b/library/Init/Lean/WHNFUtil.lean
@@ -5,9 +5,15 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.Lean.Environment
+import Init.Lean.AuxRecursor
+import Init.Lean.ProjFns
 
 namespace Lean
 
+/- ===========================
+   Helper functions for reducing recursors
+   =========================== -/
+
 private def getFirstCtor (env : Environment) (d : Name) : Option Name :=
 match env.find d with
 | some (ConstantInfo.inductInfo { ctors := ctor::_, ..}) => some ctor
@@ -33,9 +39,9 @@ match major.getAppFn with
 | _ => none
 
 @[specialize] private def toCtorWhenK {m : Type → Type} [Monad m]
-    (whnf : Expr → m Expr)
+    (whnf      : Expr → m Expr)
     (inferType : Expr → m Expr)
-    (isDefEq : Expr → Expr → m Bool)
+    (isDefEq   : Expr → Expr → m Bool)
     (env : Environment) (rec : RecursorVal) (major : Expr) : m (Option Expr) :=
 do majorType ← inferType major;
    majorType ← whnf majorType;
@@ -54,13 +60,11 @@ do majorType ← inferType major;
 
 /-- Auxiliary function for reducing recursor applications. -/
 @[specialize] def reduceRecAux {α} {m : Type → Type} [Monad m]
-    (whnf : Expr → m Expr)
+    (whnf      : Expr → m Expr)
     (inferType : Expr → m Expr)
-    (isDefEq : Expr → Expr → m Bool)
-    (env : Environment)
-    (rec : RecursorVal) (recLvls : List Level) (recArgs : Array Expr)
-    (failK : Unit → m α)
-    (successK : Expr → m α) : m α :=
+    (isDefEq   : Expr → Expr → m Bool)
+    (env : Environment) (rec : RecursorVal) (recLvls : List Level) (recArgs : Array Expr)
+    (failK : Unit → m α) (successK : Expr → m α) : m α :=
 let majorIdx := rec.getMajorIdx;
 if h : majorIdx < recArgs.size then do
   let major := recArgs.get ⟨majorIdx, h⟩;
@@ -102,16 +106,15 @@ matchConst env e.getAppFn failK $ fun cinfo recLvls =>
 
 /-- Reduce recursor applications. -/
 @[specialize] def reduceRec {α} {m : Type → Type} [Monad m]
-    (whnf : Expr → m Expr)
+    (whnf      : Expr → m Expr)
     (inferType : Expr → m Expr)
-    (isDefEq : Expr → Expr → m Bool)
+    (isDefEq   : Expr → Expr → m Bool)
     (env : Environment) (e : Expr)
-    (failK : Unit → m α)
-    (successK : Expr → m α) : m α :=
+    (failK : Unit → m α) (successK : Expr → m α) : m α :=
 matchRecApp env e failK $ fun rec recLvls recArgs => reduceRecAux whnf inferType isDefEq env rec recLvls recArgs failK successK
 
 @[specialize] def isRecStuck {m : Type → Type} [Monad m]
-    (whnf : Expr → m Expr)
+    (whnf    : Expr → m Expr)
     (isStuck : Expr → m (Option Expr))
     (env : Environment) (e : Expr) : m (Option Expr) :=
 matchRecApp env e (fun _ => pure none) $ fun rec recLvls recArgs =>
@@ -127,14 +130,16 @@ matchRecApp env e (fun _ => pure none) $ fun rec recLvls recArgs =>
     else
       pure none
 
+/- ===========================
+   Helper functions for reducing Quot.lift and Quot.ind
+   =========================== -/
 
 /-- Auxiliary function for reducing `Quot.lift` and `Quot.ind` applications. -/
 @[specialize] def reduceQuotRecAux {α} {m : Type → Type} [Monad m]
     (whnf : Expr → m Expr)
-    (env : Environment)
-    (rec : QuotVal) (recLvls : List Level) (recArgs : Array Expr)
-    (failK : Unit → m α)
-    (successK : Expr → m α) : m α :=
+    (env  : Environment)
+    (rec  : QuotVal) (recLvls : List Level) (recArgs : Array Expr)
+    (failK : Unit → m α) (successK : Expr → m α) : m α :=
 let process (majorPos argPos : Nat) : m α :=
   if h : majorPos < recArgs.size then do
     let major := recArgs.get ⟨majorPos, h⟩;
@@ -166,8 +171,7 @@ matchConst env e.getAppFn failK $ fun cinfo recLvls =>
 @[specialize] def reduceQuotRec {α} {m : Type → Type} [Monad m]
     (whnf : Expr → m Expr)
     (env : Environment) (e : Expr)
-    (failK : Unit → m α)
-    (successK : Expr → m α) : m α :=
+    (failK : Unit → m α) (successK : Expr → m α) : m α :=
 matchQuotRecApp env e failK $ fun rec recLvls recArg => reduceQuotRecAux whnf env rec recLvls recArg failK successK
 
 @[specialize] def isQuotRecStuck {m : Type → Type} [Monad m]
@@ -187,5 +191,136 @@ matchQuotRecApp env e (fun _ => pure none) $ fun rec recLvls recArgs =>
   | QuotKind.ind  => process 4
   | _             => pure none
 
+/- ===========================
+   Helper functions for reducing user-facing projection functions
+   =========================== -/
+
+@[specialize] def reduceProjectionFnAux {α} {m : Type → Type} [Monad m]
+    (whnf : Expr → m Expr)
+    (env : Environment) (projInfo : ProjectionFunctionInfo) (projArgs : Array Expr)
+    (failK : Unit → m α) (successK : Expr → m α) : m α :=
+let majorIdx := projInfo.nparams;
+if h : majorIdx < projArgs.size then do
+  let major := projArgs.get ⟨majorIdx, h⟩;
+  major ← whnf major;
+  matchConst env major.getAppFn failK $ fun majorInfo majorLvls =>
+    let i := projInfo.nparams + projInfo.i;
+    if i < major.getAppNumArgs then
+      successK $ mkAppRange (major.getArg! i) (majorIdx + 1) projArgs.size projArgs
+    else
+      failK ()
+else
+  failK ()
+
+@[specialize] def reduceProjectionFn {α} {m : Type → Type} [Monad m]
+    (whnf : Expr → m Expr)
+    (env : Environment) (e : Expr)
+    (failK : Unit → m α) (successK : Expr → m α) : m α :=
+matchConst env e.getAppFn failK $ fun cinfo _ =>
+  match env.getProjectionFnInfo cinfo.name with
+  | some projInfo => reduceProjectionFnAux whnf env projInfo e.getAppArgs failK successK
+  | none => failK ()
+
+/- ===========================
+   Weak Head Normal Form auxiliary combinators
+   =========================== -/
+
+/-- Auxiliary combinator for handling easy WHNF cases. It takes a function for handling the "hard" cases as an argument -/
+@[specialize] private partial def whnfEasyCases {m : Type → Type} [Monad m]
+    (getLocalDecl      : Name → m LocalDecl)
+    (getMVarAssignment : Name → m (Option Expr))
+    : Expr → (Expr → m Expr) → m Expr
+| e@(Expr.forallE _ _ _ _), _ => pure e
+| e@(Expr.lam _ _ _ _),     _ => pure e
+| e@(Expr.sort _),          _ => pure e
+| e@(Expr.lit _),           _ => pure e
+| e@(Expr.bvar _),          _ => unreachable!
+| Expr.mdata _ e,           k => whnfEasyCases e k
+| e@(Expr.letE _ _ _ _),    k => k e
+| e@(Expr.fvar fvarId),     k => do
+  decl ← getLocalDecl fvarId;
+  match decl.valueOpt with
+  | none   => pure e
+  | some v => whnfEasyCases v k
+| e@(Expr.mvar mvarId),     k => do
+  optV ← getMVarAssignment mvarId;
+  match optV with
+  | some v => whnfEasyCases v k
+  | none   => pure e
+| e@(Expr.const _ _),       k => k e
+| e@(Expr.app _ _),         k => k e
+| e@(Expr.proj _ _ _),      k => k e
+
+/-- Return true iff term is of the form `idRhs ...` -/
+private def isIdRhsApp (e : Expr) : Bool :=
+e.isAppOf `idRhs
+
+/-- (@idRhs T f a_1 ... a_n) ==> (f a_1 ... a_n) -/
+private def extractIdRhs (e : Expr) : Expr :=
+if !isIdRhsApp e then e
+else
+  let args := e.getAppArgs;
+  if args.size < 2 then e
+  else mkAppRange (args.get! 1) 2 args.size args
+
+@[specialize] private def deltaBetaDefinition {α} (c : ConstantInfo) (lvls : List Level) (revArgs : Array Expr)
+    (failK : Unit → α) (successK : Expr → α) : α :=
+if c.lparams.length != lvls.length then failK ()
+else
+  let val := c.instantiateValueLevelParams lvls;
+  let val := val.betaRev revArgs;
+  successK (extractIdRhs val)
+
+/--
+  Apply beta-reduction, zeta-reduction (i.e., unfold let local-decls), iota-reduction,
+  expand let-expressions, expand assigned meta-variables.
+
+  This method does *not* apply delta-reduction at the head.
+  Reason: we want to perform these reductions lazily at isDefEq.
+
+  Remark: this method delta-reduce (transparent) aux-recursors (e.g., casesOn, recOon) IF
+  `reduceAuxRec? == true`, and user-facing projection functions if `reduceProjFn? == true` -/
+@[specialize] private partial def whnfCore {m : Type → Type} [Monad m]
+    (whnf              : Expr → m Expr)
+    (inferType         : Expr → m Expr)
+    (isDefEq           : Expr → Expr → m Bool)
+    (getLocalDecl      : Name → m LocalDecl)
+    (getMVarAssignment : Name → m (Option Expr))
+    (env : Environment)
+    (reduceAuxRec? : Bool) (reduceProjFn? : Bool) : Expr → m Expr
+| e => whnfEasyCases getLocalDecl getMVarAssignment e $ fun e =>
+  match e with
+  | e@(Expr.const _ _)    => pure e
+  | e@(Expr.letE _ _ v b) => whnfCore $ b.instantiate1 v
+  | e@(Expr.app f _)      => do
+    let f := f.getAppFn;
+    f' ← whnfCore f;
+    if f'.isLambda then
+      let revArgs := e.getAppRevArgs;
+      whnfCore $ f.betaRev revArgs
+    else do
+      let done : Unit → m Expr := fun _ =>
+        if f == f' then pure e else pure $ e.updateFn f';
+      matchConst env f' done $ fun cinfo lvls =>
+        match cinfo with
+        | ConstantInfo.recInfo rec    => reduceRecAux whnf inferType isDefEq env rec lvls e.getAppArgs done whnfCore
+        | ConstantInfo.quotInfo rec   => reduceQuotRecAux whnf env rec lvls e.getAppArgs done whnfCore
+        | c@(ConstantInfo.defnInfo _) =>
+          if reduceAuxRec? && isAuxRecursor env c.name then
+            deltaBetaDefinition c lvls e.getAppArgs done whnfCore
+          else if reduceProjFn? then
+            match env.getProjectionFnInfo cinfo.name with
+            | some projInfo => reduceProjectionFnAux whnf env projInfo e.getAppArgs done whnfCore
+            | none          => done ()
+          else
+            done ()
+        | _ => done ()
+  | e@(Expr.proj _ i c) => do
+    c   ← whnf c;
+    matchConst env c.getAppFn (fun _ => pure e) $ fun cinfo lvls =>
+      match cinfo with
+      | ConstantInfo.ctorInfo ctorVal => pure $ c.getArgD (ctorVal.nparams + i) e
+      | _ => pure e
+  | _ => unreachable!
 
 end Lean