chore: update stage0

2021-08-10 15:07:16 -07:00 · 2021-08-10 15:07:16 -07:00 · 702a24913f
commit 702a24913f
parent 16ea00586d
12 changed files with 6311 additions and 2593 deletions
--- a/stage0/src/Init/Control/StateRef.lean
+++ b/stage0/src/Init/Control/StateRef.lean
@ -32,6 +32,7 @@ variable {ω σ : Type} {m : Type → Type} {α : Type}
 instance [Monad m] : Monad (StateRefT' ω σ m) := inferInstanceAs (Monad (ReaderT _ _))
 instance : MonadLift m (StateRefT' ω σ m) := ⟨StateRefT'.lift⟩
 instance (σ m) [Monad m] : MonadFunctor m (StateRefT' ω σ m) := inferInstanceAs (MonadFunctor m (ReaderT _ _))
+instance [Alternative m] [Monad m] : Alternative (StateRefT' ω σ m) := inferInstanceAs (Alternative (ReaderT _ _))

@[inline] protected def get [Monad m] [MonadLiftT (ST ω) m] : StateRefT' ω σ m σ :=
  fun ref => ref.get
@ -42,16 +43,14 @@ instance (σ m) [Monad m] : MonadFunctor m (StateRefT' ω σ m) := inferInstance
@[inline] protected def modifyGet [Monad m] [MonadLiftT (ST ω) m] (f : σ → α × σ) : StateRefT' ω σ m α :=
  fun ref => ref.modifyGet f

-instance [MonadLiftT (ST ω) m] [Monad m] : MonadStateOf σ (StateRefT' ω σ m) := {
+instance [MonadLiftT (ST ω) m] [Monad m] : MonadStateOf σ (StateRefT' ω σ m) where
  get       := StateRefT'.get
  set       := StateRefT'.set
  modifyGet := StateRefT'.modifyGet
-}

-instance (ε) [MonadExceptOf ε m] : MonadExceptOf ε (StateRefT' ω σ m) := {
+instance (ε) [MonadExceptOf ε m] : MonadExceptOf ε (StateRefT' ω σ m) where
  throw    := StateRefT'.lift ∘ throwThe ε
  tryCatch := fun x c s => tryCatchThe ε (x s) (fun e => c e s)
-}

 end StateRefT'

--- a/stage0/src/Lean/Elab/Structure.lean
+++ b/stage0/src/Lean/Elab/Structure.lean
@ -238,7 +238,7 @@ private def containsFieldName (infos : Array StructFieldInfo) (fieldName : Name)
  (findFieldInfo? infos fieldName).isSome

 register_builtin_option structureDiamondWarning : Bool := {
-  defValue := true -- TODO: set as false after finishing support for diamonds
+  defValue := false
  descr    := "enable/disable warning messages for structure diamonds"
 }

@ -318,36 +318,47 @@ private def getFieldType (infos : Array StructFieldInfo) (parentStructName : Nam
        return TransformStep.visit e
    Meta.transform projType (pre := visit)

-private partial def copyNewFieldsFrom (structDeclName : Name) (infos : Array StructFieldInfo) (parentType : Expr) (parentStructName : Name) (k : Array StructFieldInfo → TermElabM α) : TermElabM α := do
-  let fieldNames := getStructureFieldsFlattened (← getEnv) parentStructName (includeSubobjectFields := false)
-  -- trace[Meta.debug] "field names: {fieldNames}"
-  let rec go (i : Nat) (infos : Array StructFieldInfo) : TermElabM α := do
-    if h : i < fieldNames.size then
-      let fieldName := fieldNames.get ⟨i, h⟩
-      let fieldType ← getFieldType infos parentStructName parentType fieldName
-      match (← findFieldInfo? infos fieldName) with
-      | some existingFieldInfo =>
-        let existingFieldType ← inferType existingFieldInfo.fvar
-        unless (← isDefEq fieldType existingFieldType) do
-          throwError "parent field type mismatch, field '{fieldName}' from parent '{parentStructName}' {← mkHasTypeButIsExpectedMsg fieldType existingFieldType}"
-        -- TODO: if new field has a default value, it should probably override the default at `infos` (if it has one)
-        go (i+1) infos
-      | none =>
-        /- TODO: we are ignoring the following information from the `fieldName` declaraion at `parentStructName`.
-           - Binder annotation
-           - Visibility annotation (private/protected)
-           - `inferMod`
-           - Default value.
-         -/
-        withLocalDeclD fieldName fieldType fun fieldFVar => do
-          -- trace[Meta.debug] "copying field {fieldName} : {← inferType fieldFVar}"
-          let fieldDeclName := structDeclName ++ fieldName
-          let infos := infos.push { name := fieldName, declName := fieldDeclName, fvar := fieldFVar, value? := none,
-                                    kind := StructFieldKind.newField, inferMod := false }
-          go (i+1) infos
-    else
-      k infos
-  go 0 infos
+private partial def copyNewFieldsFrom (structDeclName : Name) (infos : Array StructFieldInfo) (parentType : Expr) (k : Array StructFieldInfo → TermElabM α) : TermElabM α := do
+  copyFields infos parentType k
+where
+  copyFields (infos : Array StructFieldInfo) (parentType : Expr) (k : Array StructFieldInfo → TermElabM α) : TermElabM α := do
+    let parentStructName ← getStructureName parentType
+    let fieldNames := getStructureFields (← getEnv) parentStructName
+    let rec copy (i : Nat) (infos : Array StructFieldInfo) : TermElabM α := do
+      if h : i < fieldNames.size then
+        let fieldName := fieldNames.get ⟨i, h⟩
+        let fieldType ← getFieldType infos parentStructName parentType fieldName
+        match (← findFieldInfo? infos fieldName) with
+        | some existingFieldInfo =>
+          let existingFieldType ← inferType existingFieldInfo.fvar
+          unless (← isDefEq fieldType existingFieldType) do
+            throwError "parent field type mismatch, field '{fieldName}' from parent '{parentStructName}' {← mkHasTypeButIsExpectedMsg fieldType existingFieldType}"
+          -- TODO: if new field has a default value, it should probably override the default at `infos` (if it has one)
+          copy (i+1) infos
+        | none =>
+          let some fieldInfo ← getFieldInfo? (← getEnv) parentStructName fieldName | unreachable!
+          let addNewField : TermElabM α := do
+            /- TODO: we are ignoring the following information from the `fieldName` declaraion at `parentStructName`.
+               - Visibility annotation (private/protected)
+               - Default value.
+             -/
+            withLocalDecl fieldName fieldInfo.binderInfo fieldType fun fieldFVar => do
+              -- trace[Meta.debug] "copying field {fieldName} : {← inferType fieldFVar}"
+              let fieldDeclName := structDeclName ++ fieldName
+              let infos := infos.push { name := fieldName, declName := fieldDeclName, fvar := fieldFVar, value? := none,
+                                        kind := StructFieldKind.newField, inferMod := fieldInfo.inferMod }
+              copy (i+1) infos
+          if fieldInfo.subobject?.isSome then
+            let fieldParentStructName ← getStructureName fieldType
+            if (← findExistingField? infos fieldParentStructName).isSome then
+              copyFields infos fieldType (fun infos => copy (i+1) infos)
+            else
+              addNewField
+          else
+            addNewField
+      else
+        k infos
+    copy 0 infos

 private def mkToParentName (parentStructName : Name) : Name :=
  Name.mkSimple $ "to" ++ parentStructName.eraseMacroScopes.getString! -- erase macro scopes?
@ -359,12 +370,12 @@ where
    if h : i < view.parents.size then
      let parentStx := view.parents.get ⟨i, h⟩
      withRef parentStx do
-      let parent ← Term.elabType parentStx
-      let parentStructName ← getStructureName parent
+      let parentType ← Term.elabType parentStx
+      let parentStructName ← getStructureName parentType
      if let some existingFieldName ← findExistingField? infos parentStructName then
        if structureDiamondWarning.get (← getOptions) then
          logWarning s!"field '{existingFieldName}' from '{parentStructName}' has already been declared"
-        copyNewFieldsFrom view.declName infos parent parentStructName fun infos => go (i+1) infos (copiedParents.push parent)
+        copyNewFieldsFrom view.declName infos parentType fun infos => go (i+1) infos (copiedParents.push parentType)
        -- TODO: if `class`, then we need to create a let-decl that stores the local instance for the `parentStructure`
      else
        let toParentName := mkToParentName parentStructName
@ -372,14 +383,13 @@ where
          throwErrorAt parentStx "field '{toParentName}' has already been declared"
        let env ← getEnv
        let binfo := if view.isClass && isClass env parentStructName then BinderInfo.instImplicit else BinderInfo.default
-        withLocalDecl toParentName binfo parent fun parentFVar =>
+        withLocalDecl toParentName binfo parentType fun parentFVar =>
          let infos := infos.push { name := toParentName, declName := view.declName ++ toParentName, fvar := parentFVar, kind := StructFieldKind.subobject }
          let subfieldNames := getStructureFieldsFlattened env parentStructName
          processSubfields view.declName parentFVar parentStructName subfieldNames infos fun infos => go (i+1) infos copiedParents
    else
      k infos copiedParents

-
 private def elabFieldTypeValue (view : StructFieldView) : TermElabM (Option Expr × Option Expr) := do
  Term.withAutoBoundImplicit <| Term.elabBinders view.binders.getArgs fun params => do
    match view.type? with
@ -611,15 +621,16 @@ private def addDefaults (lctx : LocalContext) (defaultAuxDecls : Array (Name ×
      setReducibleAttribute declName

 private partial def mkCoercionToCopiedParent (levelParams : List Name) (params : Array Expr) (view : StructView) (parentType : Expr) : MetaM Unit := do
+  let env ← getEnv
  let structName := view.declName
-  let sourceFieldNames := getStructureFieldsFlattened (← getEnv) structName
+  let sourceFieldNames := getStructureFieldsFlattened env structName
  let structType ← mkAppN (Lean.mkConst structName (levelParams.map mkLevelParam)) params
-  -- TODO: binder annotation for instances
-  withLocalDeclD `source structType fun source => do
-    let declType ← mkForallFVars params (← mkArrow structType parentType)
+  let Expr.const parentStructName us _ ← pure parentType.getAppFn | unreachable!
+  let binfo := if view.isClass && isClass env parentStructName then BinderInfo.instImplicit else BinderInfo.default
+  withLocalDecl `self binfo structType fun source => do
+    let declType ← instantiateMVars (← mkForallFVars params (← mkForallFVars #[source] parentType))
    let declType := declType.inferImplicit params.size true
    let rec copyFields (parentType : Expr) : MetaM Expr := do
-      let env ← getEnv
      let Expr.const parentStructName us _ ← pure parentType.getAppFn | unreachable!
      let parentCtor := getStructureCtor env parentStructName
      let mut result := mkAppN (mkConst parentCtor.name us) parentType.getAppArgs
@ -636,9 +647,10 @@ private partial def mkCoercionToCopiedParent (levelParams : List Name) (params :
          let fieldVal ← copyFields resultType.bindingDomain!
          result := mkApp result fieldVal
      return result
-    let declVal ← mkLambdaFVars params (← mkLambdaFVars #[source] (← copyFields parentType))
+    let declVal ← instantiateMVars (← mkLambdaFVars params (← mkLambdaFVars #[source] (← copyFields parentType)))
    let declName := structName ++ mkToParentName (← getStructureName parentType)
-    -- TODO: nice error message if `declName` already exists
+    if env.contains declName then
+      throwError "failed to create coercion '{declName}' to parent structure '{parentStructName}', environment already contains a declaration with the same name"
    addAndCompile <| Declaration.defnDecl {
      name        := declName
      levelParams := levelParams
@ -647,7 +659,10 @@ private partial def mkCoercionToCopiedParent (levelParams : List Name) (params :
      hints       := ReducibilityHints.abbrev
      safety      := if view.modifiers.isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe
    }
-    -- TODO: attributes
+    if binfo.isInstImplicit then
+      addInstance declName AttributeKind.global (eval_prio default)
+    else
+      setReducibleAttribute declName

 private def elabStructureView (view : StructView) : TermElabM Unit := do
  view.fields.forM fun field => do
@ -658,7 +673,7 @@ private def elabStructureView (view : StructView) : TermElabM Unit := do
  let type ← Term.elabType view.type
  unless validStructType type do throwErrorAt view.type "expected Type"
  withRef view.ref do
-  withParents view fun fieldInfos copiedParents =>
+  withParents view fun fieldInfos copiedParents => do
  withFields view.fields 0 fieldInfos fun fieldInfos => do
    Term.synthesizeSyntheticMVarsNoPostponing
    let u ← getResultUniverse type
--- a/stage0/src/Lean/Elab/Syntax.lean
+++ b/stage0/src/Lean/Elab/Syntax.lean
@ -315,10 +315,10 @@ def resolveSyntaxKind (k : Name) : CommandElabM Name := do
  let declName := mkIdentFrom stx name
  let d ←
    if let some lhsPrec := lhsPrec? then
-      `($[$doc?:docComment]? @[$attrKind:attrKind $catParserId:ident $(quote prio):numLit] def $declName : Lean.TrailingParserDescr :=
+      `($[$doc?:docComment]? @[$attrKind:attrKind $catParserId:ident $(quote prio):numLit] def $declName:ident : Lean.TrailingParserDescr :=
        ParserDescr.trailingNode $(quote stxNodeKind) $(quote prec) $(quote lhsPrec) $val)
    else
-      `($[$doc?:docComment]? @[$attrKind:attrKind $catParserId:ident $(quote prio):numLit] def $declName : Lean.ParserDescr :=
+      `($[$doc?:docComment]? @[$attrKind:attrKind $catParserId:ident $(quote prio):numLit] def $declName:ident : Lean.ParserDescr :=
        ParserDescr.node $(quote stxNodeKind) $(quote prec) $val)
  trace `Elab fun _ => d
  withMacroExpansion stx d <| elabCommand d
@ -331,7 +331,7 @@ def syntaxAbbrev  := leading_parser "syntax " >> ident >> " := " >> many1 syntax
  -- TODO: nonatomic names
  let (val, _) ← runTermElabM none $ fun _ => Term.toParserDescr stx[3] Name.anonymous
  let stxNodeKind := (← getCurrNamespace) ++ declName.getId
-  let stx' ← `(def $declName : Lean.ParserDescr := ParserDescr.nodeWithAntiquot $(quote (toString declName.getId)) $(quote stxNodeKind) $val)
+  let stx' ← `(def $declName:ident : Lean.ParserDescr := ParserDescr.nodeWithAntiquot $(quote (toString declName.getId)) $(quote stxNodeKind) $val)
  withMacroExpansion stx stx' $ elabCommand stx'

 def checkRuleKind (given expected : SyntaxNodeKind) : Bool :=
--- a/stage0/src/Lean/Elab/Term.lean
+++ b/stage0/src/Lean/Elab/Term.lean
@ -590,6 +590,42 @@ def throwTypeMismatchError (header? : Option String) (expectedType : Expr) (eTyp
 def withoutMacroStackAtErr (x : TermElabM α) : TermElabM α :=
  withTheReader Core.Context (fun (ctx : Core.Context) => { ctx with options := pp.macroStack.set ctx.options false }) x

+namespace ContainsPendingMVar
+
+abbrev M := MonadCacheT Expr Unit (OptionT TermElabM)
+
+/-- See `containsPostponedTerm` -/
+partial def visit (e : Expr) : M Unit := do
+  checkCache e fun _ => do
+    match e with
+    | Expr.forallE _ d b _   => visit d; visit b
+    | Expr.lam _ d b _       => visit d; visit b
+    | Expr.letE _ t v b _    => visit t; visit v; visit b
+    | Expr.app f a _         => visit f; visit a
+    | Expr.mdata _ b _       => visit b
+    | Expr.proj _ _ b _      => visit b
+    | Expr.fvar fvarId ..    =>
+      match (← getLocalDecl fvarId) with
+      | LocalDecl.cdecl .. => return ()
+      | LocalDecl.ldecl (value := v) .. => visit v
+    | Expr.mvar mvarId ..    =>
+      let e' ← instantiateMVars e
+      if e' != e then
+        visit e'
+      else
+        match (← getDelayedAssignment? mvarId) with
+        | some d => visit d.val
+        | none   => failure
+    | _ => return ()
+
+end ContainsPendingMVar
+
+/-- Return `true` if `e` contains a pending metavariable. Remark: it also visits let-declarations. -/
+def containsPendingMVar (e : Expr) : TermElabM Bool := do
+  match (← ContainsPendingMVar.visit e |>.run.run) with
+  | some _ => return false
+  | none   => return true
+
 /- Try to synthesize metavariable using type class resolution.
   This method assumes the local context and local instances of `instMVar` coincide
   with the current local context and local instances.
@ -606,6 +642,26 @@ def synthesizeInstMVarCore (instMVar : MVarId) (maxResultSize? : Option Nat := n
    if (← isExprMVarAssigned instMVar) then
      let oldVal ← instantiateMVars (mkMVar instMVar)
      unless (← isDefEq oldVal val) do
+        if (← containsPendingMVar oldVal <||> containsPendingMVar val) then
+          /- If `val` or `oldVal` contains metavariables directly or indirectly (e.g., in a let-declaration),
+             we return `false` to indicate we should try again later. This is very course grain since
+             the metavariable may not be responsible for the failure. We should refine the test in the future if needed.
+             This check has been added to address dependencies between postponed metavariables. The following
+             example demonstrates the issue fixed by this test.
+             ```
+               structure Point where
+                 x : Nat
+                 y : Nat
+
+               def Point.compute (p : Point) : Point :=
+                 let p := { p with x := 1 }
+                 let p := { p with y := 0 }
+                 if (p.x - p.y) > p.x then p else p
+             ```
+             The `isDefEq` test above fails for `Decidable (p.x - p.y ≤ p.x)` when the structure instance assigned to
+             `p` has not been elaborated yet.
+           -/
+          return false -- we will try again later
        let oldValType ← inferType oldVal
        let valType ← inferType val
        unless (← isDefEq oldValType valType) do
--- a/stage0/src/Lean/Meta/Reduce.lean
+++ b/stage0/src/Lean/Meta/Reduce.lean
@ -32,9 +32,10 @@ partial def reduce (e : Expr) (explicitOnly skipTypes skipProofs := true) : Meta
            else
              args ← args.modifyM i visit
          pure (mkAppN f args)
-        | Expr.lam ..     => lambdaTelescope e fun xs b => do mkLambdaFVars xs (← visit b)
-        | Expr.forallE .. => forallTelescope e fun xs b => do mkForallFVars xs (← visit b)
-        | _               => return e
+        | Expr.lam ..        => lambdaTelescope e fun xs b => do mkLambdaFVars xs (← visit b)
+        | Expr.forallE ..    => forallTelescope e fun xs b => do mkForallFVars xs (← visit b)
+        | Expr.proj n i s .. => return mkProj n i (← visit s)
+        | _                  => return e
  visit e |>.run

 end Lean.Meta
--- a/stage0/src/Lean/Util/MonadCache.lean
+++ b/stage0/src/Lean/Util/MonadCache.lean
@ -71,6 +71,7 @@ instance (ε) [MonadExceptOf ε m] : MonadExceptOf ε (MonadCacheT α β m) := i
 instance : MonadControl m (MonadCacheT α β m) := inferInstanceAs (MonadControl m (StateRefT' _ _ _))
 instance [MonadFinally m] : MonadFinally (MonadCacheT α β m) := inferInstanceAs (MonadFinally (StateRefT' _ _ _))
 instance [MonadRef m] : MonadRef (MonadCacheT α β m) := inferInstanceAs (MonadRef (StateRefT' _ _ _))
+instance [Alternative m] : Alternative (MonadCacheT α β m) := inferInstanceAs (Alternative (StateRefT' _ _ _))

 end MonadCacheT

--- a/stage0/stdlib/Init/Control/StateRef.c
+++ b/stage0/stdlib/Init/Control/StateRef.c
@ -50,6 +50,7 @@ lean_object* l_StateRefT_x27_instMonadExceptOfStateRefT_x27___rarg___lambda__2(l
 lean_object* l_StateRefT_x27_instMonadStateOfStateRefT_x27___rarg(lean_object*, lean_object*);
 lean_object* l_StateRefT_x27_get(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_instMonadFinallyStateRefT_x27___rarg(lean_object*, lean_object*);
+lean_object* l_StateRefT_x27_instAlternativeStateRefT_x27(lean_object*, lean_object*, lean_object*);
 lean_object* l_StateRefT_x27_run_x27___rarg___lambda__1(lean_object*, lean_object*);
 lean_object* l_StateRefT_x27_run___rarg___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_StateRefT_x27_set___rarg(lean_object*, lean_object*, lean_object*);
@ -65,6 +66,8 @@ lean_object* l_ST_Prim_Ref_modifyGetUnsafe___rarg___boxed(lean_object*, lean_obj
 lean_object* l_instMonadControlReaderT___lambda__2(lean_object*, lean_object*, lean_object*);
 static lean_object* l_instMonadControlStateRefT_x27___closed__3;
 lean_object* l_ReaderT_instMonadReaderT___rarg(lean_object*);
+lean_object* l_StateRefT_x27_instAlternativeStateRefT_x27___rarg(lean_object*, lean_object*);
+lean_object* l_ReaderT_instAlternativeReaderT___rarg(lean_object*, lean_object*);
 lean_object* l_StateRefT_x27_instMonadStateRefT_x27___rarg(lean_object*);
 lean_object* l_StateRefT_x27_run___rarg___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
@ -297,6 +300,22 @@ x_4 = lean_alloc_closure((void*)(l_StateRefT_x27_instMonadFunctorStateRefT_x27__
 return x_4;
 }
 }
+lean_object* l_StateRefT_x27_instAlternativeStateRefT_x27___rarg(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = l_ReaderT_instAlternativeReaderT___rarg(x_1, x_2);
+return x_3;
+}
+}
+lean_object* l_StateRefT_x27_instAlternativeStateRefT_x27(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+lean_object* x_4; 
+x_4 = lean_alloc_closure((void*)(l_StateRefT_x27_instAlternativeStateRefT_x27___rarg), 2, 0);
+return x_4;
+}
+}
 lean_object* l_StateRefT_x27_get___rarg(lean_object* x_1, lean_object* x_2) {
 _start:
 {
--- a/stage0/stdlib/Lean/Elab/Structure.c
+++ b/stage0/stdlib/Lean/Elab/Structure.c
--- a/stage0/stdlib/Lean/Elab/Syntax.c
+++ b/stage0/stdlib/Lean/Elab/Syntax.c
--- a/stage0/stdlib/Lean/Elab/Term.c
+++ b/stage0/stdlib/Lean/Elab/Term.c
--- a/stage0/stdlib/Lean/Meta/Reduce.c
+++ b/stage0/stdlib/Lean/Meta/Reduce.c
@ -44,11 +44,12 @@ lean_object* l_Std_HashMap_insert___rarg(lean_object*, lean_object*, lean_object
 lean_object* l___private_Lean_Expr_0__Lean_Expr_getAppArgsAux(lean_object*, lean_object*, lean_object*);
 lean_object* lean_array_fget(lean_object*, lean_object*);
 lean_object* l_Lean_Core_withIncRecDepth___at_Lean_Meta_reduce_visit___spec__8(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_mkProj(lean_object*, lean_object*, lean_object*);
 uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
 lean_object* l_Lean_Meta_reduce_visit___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_st_ref_take(lean_object*, lean_object*);
 lean_object* lean_nat_sub(lean_object*, lean_object*);
-lean_object* l_Lean_Meta_reduce_visit_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_Meta_reduce_visit_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_Meta_mkLambdaFVars(lean_object*, lean_object*, uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_HashMapImp_find_x3f___at_Lean_Meta_reduce_visit___spec__1(lean_object*, lean_object*);
@ -95,70 +96,93 @@ lean_object* l_Lean_Meta_isType(lean_object*, lean_object*, lean_object*, lean_o
 uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
 lean_object* l_Std_mkHashMap___at_Lean_Meta_reduce___spec__1___boxed(lean_object*);
 lean_object* l_Lean_Core_withIncRecDepth___at_Lean_Meta_reduce_visit___spec__8___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
-lean_object* l_Lean_Meta_reduce_visit_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
+lean_object* l_Lean_Meta_reduce_visit_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
 _start:
 {
 switch (lean_obj_tag(x_1)) {
 case 5:
 {
-lean_object* x_6; lean_object* x_7; uint64_t x_8; lean_object* x_9; lean_object* x_10; 
+lean_object* x_7; lean_object* x_8; uint64_t x_9; lean_object* x_10; lean_object* x_11; 
+lean_dec(x_6);
 lean_dec(x_5);
 lean_dec(x_4);
 lean_dec(x_3);
-x_6 = lean_ctor_get(x_1, 0);
-lean_inc(x_6);
-x_7 = lean_ctor_get(x_1, 1);
+x_7 = lean_ctor_get(x_1, 0);
 lean_inc(x_7);
-x_8 = lean_ctor_get_uint64(x_1, sizeof(void*)*2);
+x_8 = lean_ctor_get(x_1, 1);
+lean_inc(x_8);
+x_9 = lean_ctor_get_uint64(x_1, sizeof(void*)*2);
 lean_dec(x_1);
-x_9 = lean_box_uint64(x_8);
-x_10 = lean_apply_3(x_2, x_6, x_7, x_9);
-return x_10;
+x_10 = lean_box_uint64(x_9);
+x_11 = lean_apply_3(x_2, x_7, x_8, x_10);
+return x_11;
 }
 case 6:
 {
-lean_object* x_11; lean_object* x_12; lean_object* x_13; uint64_t x_14; lean_object* x_15; lean_object* x_16; 
+lean_object* x_12; lean_object* x_13; lean_object* x_14; uint64_t x_15; lean_object* x_16; lean_object* x_17; 
+lean_dec(x_6);
 lean_dec(x_5);
 lean_dec(x_4);
 lean_dec(x_2);
-x_11 = lean_ctor_get(x_1, 0);
-lean_inc(x_11);
-x_12 = lean_ctor_get(x_1, 1);
+x_12 = lean_ctor_get(x_1, 0);
 lean_inc(x_12);
-x_13 = lean_ctor_get(x_1, 2);
+x_13 = lean_ctor_get(x_1, 1);
 lean_inc(x_13);
-x_14 = lean_ctor_get_uint64(x_1, sizeof(void*)*3);
+x_14 = lean_ctor_get(x_1, 2);
+lean_inc(x_14);
+x_15 = lean_ctor_get_uint64(x_1, sizeof(void*)*3);
 lean_dec(x_1);
-x_15 = lean_box_uint64(x_14);
-x_16 = lean_apply_4(x_3, x_11, x_12, x_13, x_15);
-return x_16;
+x_16 = lean_box_uint64(x_15);
+x_17 = lean_apply_4(x_3, x_12, x_13, x_14, x_16);
+return x_17;
 }
 case 7:
 {
-lean_object* x_17; lean_object* x_18; lean_object* x_19; uint64_t x_20; lean_object* x_21; lean_object* x_22; 
+lean_object* x_18; lean_object* x_19; lean_object* x_20; uint64_t x_21; lean_object* x_22; lean_object* x_23; 
+lean_dec(x_6);
 lean_dec(x_5);
 lean_dec(x_3);
 lean_dec(x_2);
-x_17 = lean_ctor_get(x_1, 0);
-lean_inc(x_17);
-x_18 = lean_ctor_get(x_1, 1);
+x_18 = lean_ctor_get(x_1, 0);
 lean_inc(x_18);
-x_19 = lean_ctor_get(x_1, 2);
+x_19 = lean_ctor_get(x_1, 1);
 lean_inc(x_19);
-x_20 = lean_ctor_get_uint64(x_1, sizeof(void*)*3);
+x_20 = lean_ctor_get(x_1, 2);
+lean_inc(x_20);
+x_21 = lean_ctor_get_uint64(x_1, sizeof(void*)*3);
 lean_dec(x_1);
-x_21 = lean_box_uint64(x_20);
-x_22 = lean_apply_4(x_4, x_17, x_18, x_19, x_21);
-return x_22;
+x_22 = lean_box_uint64(x_21);
+x_23 = lean_apply_4(x_4, x_18, x_19, x_20, x_22);
+return x_23;
 }
-default: 
+case 11:
 {
-lean_object* x_23; 
+lean_object* x_24; lean_object* x_25; lean_object* x_26; uint64_t x_27; lean_object* x_28; lean_object* x_29; 
+lean_dec(x_6);
 lean_dec(x_4);
 lean_dec(x_3);
 lean_dec(x_2);
-x_23 = lean_apply_1(x_5, x_1);
-return x_23;
+x_24 = lean_ctor_get(x_1, 0);
+lean_inc(x_24);
+x_25 = lean_ctor_get(x_1, 1);
+lean_inc(x_25);
+x_26 = lean_ctor_get(x_1, 2);
+lean_inc(x_26);
+x_27 = lean_ctor_get_uint64(x_1, sizeof(void*)*3);
+lean_dec(x_1);
+x_28 = lean_box_uint64(x_27);
+x_29 = lean_apply_4(x_5, x_24, x_25, x_26, x_28);
+return x_29;
+}
+default: 
+{
+lean_object* x_30; 
+lean_dec(x_5);
+lean_dec(x_4);
+lean_dec(x_3);
+lean_dec(x_2);
+x_30 = lean_apply_1(x_6, x_1);
+return x_30;
 }
 }
 }
@ -167,7 +191,7 @@ lean_object* l_Lean_Meta_reduce_visit_match__1(lean_object* x_1) {
 _start:
 {
 lean_object* x_2; 
-x_2 = lean_alloc_closure((void*)(l_Lean_Meta_reduce_visit_match__1___rarg), 5, 0);
+x_2 = lean_alloc_closure((void*)(l_Lean_Meta_reduce_visit_match__1___rarg), 6, 0);
 return x_2;
 }
 }
@ -1082,61 +1106,61 @@ if (x_4 == 0)
 {
 x_12 = x_4;
 x_13 = x_11;
-goto block_67;
+goto block_83;
 }
 else
 {
-lean_object* x_68; 
+lean_object* x_84; 
 lean_inc(x_10);
 lean_inc(x_9);
 lean_inc(x_8);
 lean_inc(x_7);
 lean_inc(x_1);
-x_68 = l_Lean_Meta_isProof(x_1, x_7, x_8, x_9, x_10, x_11);
-if (lean_obj_tag(x_68) == 0)
+x_84 = l_Lean_Meta_isProof(x_1, x_7, x_8, x_9, x_10, x_11);
+if (lean_obj_tag(x_84) == 0)
 {
-lean_object* x_69; lean_object* x_70; uint8_t x_71; 
-x_69 = lean_ctor_get(x_68, 0);
-lean_inc(x_69);
-x_70 = lean_ctor_get(x_68, 1);
-lean_inc(x_70);
-lean_dec(x_68);
-x_71 = lean_unbox(x_69);
-lean_dec(x_69);
-x_12 = x_71;
-x_13 = x_70;
-goto block_67;
+lean_object* x_85; lean_object* x_86; uint8_t x_87; 
+x_85 = lean_ctor_get(x_84, 0);
+lean_inc(x_85);
+x_86 = lean_ctor_get(x_84, 1);
+lean_inc(x_86);
+lean_dec(x_84);
+x_87 = lean_unbox(x_85);
+lean_dec(x_85);
+x_12 = x_87;
+x_13 = x_86;
+goto block_83;
 }
 else
 {
-uint8_t x_72; 
+uint8_t x_88; 
 lean_dec(x_10);
 lean_dec(x_9);
 lean_dec(x_8);
 lean_dec(x_7);
 lean_dec(x_6);
 lean_dec(x_1);
-x_72 = !lean_is_exclusive(x_68);
-if (x_72 == 0)
+x_88 = !lean_is_exclusive(x_84);
+if (x_88 == 0)
 {
-return x_68;
+return x_84;
 }
 else
 {
-lean_object* x_73; lean_object* x_74; lean_object* x_75; 
-x_73 = lean_ctor_get(x_68, 0);
-x_74 = lean_ctor_get(x_68, 1);
-lean_inc(x_74);
-lean_inc(x_73);
-lean_dec(x_68);
-x_75 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_75, 0, x_73);
-lean_ctor_set(x_75, 1, x_74);
-return x_75;
+lean_object* x_89; lean_object* x_90; lean_object* x_91; 
+x_89 = lean_ctor_get(x_84, 0);
+x_90 = lean_ctor_get(x_84, 1);
+lean_inc(x_90);
+lean_inc(x_89);
+lean_dec(x_84);
+x_91 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_91, 0, x_89);
+lean_ctor_set(x_91, 1, x_90);
+return x_91;
 }
 }
 }
-block_67:
+block_83:
 {
 if (x_12 == 0)
 {
@ -1306,91 +1330,157 @@ lean_closure_set(x_56, 2, x_55);
 x_57 = l_Lean_Meta_forallTelescope___at_Lean_Meta_reduce_visit___spec__7___rarg(x_15, x_56, x_6, x_7, x_8, x_9, x_10, x_52);
 return x_57;
 }
+case 11:
+{
+lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; 
+x_58 = lean_ctor_get(x_14, 1);
+lean_inc(x_58);
+lean_dec(x_14);
+x_59 = lean_ctor_get(x_15, 0);
+lean_inc(x_59);
+x_60 = lean_ctor_get(x_15, 1);
+lean_inc(x_60);
+x_61 = lean_ctor_get(x_15, 2);
+lean_inc(x_61);
+lean_dec(x_15);
+x_62 = l_Lean_Meta_reduce_visit(x_2, x_3, x_4, x_61, x_6, x_7, x_8, x_9, x_10, x_58);
+if (lean_obj_tag(x_62) == 0)
+{
+uint8_t x_63; 
+x_63 = !lean_is_exclusive(x_62);
+if (x_63 == 0)
+{
+lean_object* x_64; lean_object* x_65; 
+x_64 = lean_ctor_get(x_62, 0);
+x_65 = l_Lean_mkProj(x_59, x_60, x_64);
+lean_ctor_set(x_62, 0, x_65);
+return x_62;
+}
+else
+{
+lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; 
+x_66 = lean_ctor_get(x_62, 0);
+x_67 = lean_ctor_get(x_62, 1);
+lean_inc(x_67);
+lean_inc(x_66);
+lean_dec(x_62);
+x_68 = l_Lean_mkProj(x_59, x_60, x_66);
+x_69 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_69, 0, x_68);
+lean_ctor_set(x_69, 1, x_67);
+return x_69;
+}
+}
+else
+{
+uint8_t x_70; 
+lean_dec(x_60);
+lean_dec(x_59);
+x_70 = !lean_is_exclusive(x_62);
+if (x_70 == 0)
+{
+return x_62;
+}
+else
+{
+lean_object* x_71; lean_object* x_72; lean_object* x_73; 
+x_71 = lean_ctor_get(x_62, 0);
+x_72 = lean_ctor_get(x_62, 1);
+lean_inc(x_72);
+lean_inc(x_71);
+lean_dec(x_62);
+x_73 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_73, 0, x_71);
+lean_ctor_set(x_73, 1, x_72);
+return x_73;
+}
+}
+}
 default: 
 {
-uint8_t x_58; 
+uint8_t x_74; 
 lean_dec(x_10);
 lean_dec(x_9);
 lean_dec(x_8);
 lean_dec(x_7);
 lean_dec(x_6);
-x_58 = !lean_is_exclusive(x_14);
-if (x_58 == 0)
+x_74 = !lean_is_exclusive(x_14);
+if (x_74 == 0)
 {
-lean_object* x_59; 
-x_59 = lean_ctor_get(x_14, 0);
-lean_dec(x_59);
+lean_object* x_75; 
+x_75 = lean_ctor_get(x_14, 0);
+lean_dec(x_75);
 return x_14;
 }
 else
 {
-lean_object* x_60; lean_object* x_61; 
-x_60 = lean_ctor_get(x_14, 1);
-lean_inc(x_60);
+lean_object* x_76; lean_object* x_77; 
+x_76 = lean_ctor_get(x_14, 1);
+lean_inc(x_76);
 lean_dec(x_14);
-x_61 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_61, 0, x_15);
-lean_ctor_set(x_61, 1, x_60);
-return x_61;
+x_77 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_77, 0, x_15);
+lean_ctor_set(x_77, 1, x_76);
+return x_77;
 }
 }
 }
 }
 else
 {
-uint8_t x_62; 
+uint8_t x_78; 
 lean_dec(x_10);
 lean_dec(x_9);
 lean_dec(x_8);
 lean_dec(x_7);
 lean_dec(x_6);
-x_62 = !lean_is_exclusive(x_14);
-if (x_62 == 0)
+x_78 = !lean_is_exclusive(x_14);
+if (x_78 == 0)
 {
 return x_14;
 }
 else
 {
-lean_object* x_63; lean_object* x_64; lean_object* x_65; 
-x_63 = lean_ctor_get(x_14, 0);
-x_64 = lean_ctor_get(x_14, 1);
-lean_inc(x_64);
-lean_inc(x_63);
+lean_object* x_79; lean_object* x_80; lean_object* x_81; 
+x_79 = lean_ctor_get(x_14, 0);
+x_80 = lean_ctor_get(x_14, 1);
+lean_inc(x_80);
+lean_inc(x_79);
 lean_dec(x_14);
-x_65 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_65, 0, x_63);
-lean_ctor_set(x_65, 1, x_64);
-return x_65;
+x_81 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_81, 0, x_79);
+lean_ctor_set(x_81, 1, x_80);
+return x_81;
 }
 }
 }
 else
 {
-lean_object* x_66; 
+lean_object* x_82; 
 lean_dec(x_10);
 lean_dec(x_9);
 lean_dec(x_8);
 lean_dec(x_7);
 lean_dec(x_6);
-x_66 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_66, 0, x_1);
-lean_ctor_set(x_66, 1, x_13);
-return x_66;
+x_82 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_82, 0, x_1);
+lean_ctor_set(x_82, 1, x_13);
+return x_82;
 }
 }
 }
 else
 {
-lean_object* x_76; 
+lean_object* x_92; 
 lean_dec(x_10);
 lean_dec(x_9);
 lean_dec(x_8);
 lean_dec(x_7);
 lean_dec(x_6);
-x_76 = lean_alloc_ctor(0, 2, 0);
-lean_ctor_set(x_76, 0, x_1);
-lean_ctor_set(x_76, 1, x_11);
-return x_76;
+x_92 = lean_alloc_ctor(0, 2, 0);
+lean_ctor_set(x_92, 0, x_1);
+lean_ctor_set(x_92, 1, x_11);
+return x_92;
 }
 }
 }
--- a/stage0/stdlib/Lean/Util/MonadCache.c
+++ b/stage0/stdlib/Lean/Util/MonadCache.c
@ -26,6 +26,7 @@ lean_object* l_Lean_MonadCacheT_instMonadMonadCacheT___boxed(lean_object*, lean_
 lean_object* l_Lean_MonadCacheT_instMonadControlMonadCacheT___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_MonadCacheT_run___rarg___lambda__4(lean_object*, lean_object*);
 lean_object* l_ReaderT_tryFinally___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_MonadCacheT_instAlternativeMonadCacheT(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_MonadStateCacheT_instMonadMonadStateCacheT(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_modify___at_Lean_MonadCacheT_instMonadHashMapCacheAdapterMonadCacheT___spec__1___rarg___lambda__1(lean_object*, lean_object*);
 lean_object* l_Lean_MonadCacheT_run(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -55,10 +56,12 @@ lean_object* l_Lean_checkCache_match__1(lean_object*, lean_object*);
 lean_object* l_StateRefT_x27_lift(lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_modify___at_Lean_MonadStateCacheT_instMonadHashMapCacheAdapterMonadStateCacheT___spec__1___rarg(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_HashMapImp_find_x3f___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_MonadCacheT_instAlternativeMonadCacheT___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_MonadHashMapCacheAdapter_findCached_x3f(lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_checkCache___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_MonadStateCacheT_instMonadControlMonadStateCacheT(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_MonadStateCacheT_instMonadFinallyMonadStateCacheT___rarg(lean_object*, lean_object*);
+lean_object* l_Lean_MonadCacheT_instAlternativeMonadCacheT___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_MonadStateCacheT_instMonadMonadStateCacheT___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_StateT_get___rarg(lean_object*, lean_object*);
 lean_object* l_ST_Prim_Ref_get___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -131,6 +134,7 @@ lean_object* l_Lean_MonadCacheT_instMonadControlMonadCacheT(lean_object*, lean_o
 lean_object* l_Lean_instMonadCacheExceptT___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_MonadCacheT_instMonadFinallyMonadCacheT(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_instMonadRef___rarg(lean_object*, lean_object*, lean_object*);
+lean_object* l_ReaderT_instAlternativeReaderT___rarg(lean_object*, lean_object*);
 lean_object* l_Lean_MonadStateCacheT_instMonadControlMonadStateCacheT___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_checkCache_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
@ -948,6 +952,33 @@ lean_dec(x_5);
 return x_8;
 }
 }
+lean_object* l_Lean_MonadCacheT_instAlternativeMonadCacheT___rarg(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; 
+x_3 = l_ReaderT_instAlternativeReaderT___rarg(x_2, x_1);
+return x_3;
+}
+}
+lean_object* l_Lean_MonadCacheT_instAlternativeMonadCacheT(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
+_start:
+{
+lean_object* x_8; 
+x_8 = lean_alloc_closure((void*)(l_Lean_MonadCacheT_instAlternativeMonadCacheT___rarg), 2, 0);
+return x_8;
+}
+}
+lean_object* l_Lean_MonadCacheT_instAlternativeMonadCacheT___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
+_start:
+{
+lean_object* x_8; 
+x_8 = l_Lean_MonadCacheT_instAlternativeMonadCacheT(x_1, x_2, x_3, x_4, x_5, x_6, x_7);
+lean_dec(x_7);
+lean_dec(x_6);
+lean_dec(x_5);
+return x_8;
+}
+}
 lean_object* l_modify___at_Lean_MonadStateCacheT_instMonadHashMapCacheAdapterMonadStateCacheT___spec__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
 _start:
 {