chore(library/init): avoid wf_term_hack

library/init/control/monad.lean

@@ -21,3 +21,8 @@ class Monad (m : Type u → Type v) extends Applicative m, HasBind m : Type (max
 (Seq       := λ α β f x, f >>= (<$> x))
 (seqLeft  := λ α β x y, x >>= λ a, y >>= λ _, pure a)
 (seqRight := λ α β x y, x >>= λ _, y)
+
+/- We do not add this instance by default because it is rarely needed,
+   and it could slow down the current type class resolution procedure. -/
+def monadInhabited {α : Type u} {m : Type u → Type v} [Monad m] [Inhabited α] : Inhabited (m α) :=
+⟨pure $ default _⟩

library/init/data/list/basic.lean

@@ -380,4 +380,8 @@ def isPrefixOf [DecidableEq α] : List α → List α → Bool
 def isSuffixOf [DecidableEq α] (l₁ l₂ : List α) : Bool :=
 isPrefixOf l₁.reverse l₂.reverse
 
+@[specialize] def isEqv : List α → List α → (α → α → Bool) → Bool
+| []      []      _   := true
+| (a::as) (b::bs) eqv := eqv a b && isEqv as bs eqv
+| _       _       eqv := false
 end List

library/init/data/nat/bitwise.lean

@@ -7,7 +7,7 @@ prelude
 import init.data.nat.basic init.data.nat.div init.coe
 namespace Nat
 
-def bitwise (f : Bool → Bool → Bool) : Nat → Nat → Nat | n m :=
+partial def bitwise (f : Bool → Bool → Bool) : Nat → Nat → Nat | n m :=
 if n = 0 then      (if f false true then m else 0)
 else if m = 0 then (if f true false then n else 0)
 else

library/init/lean/compiler/ir.lean

@@ -184,24 +184,20 @@ def Expr.isPure : Expr → Bool
 | _                := false
 
 /-- `Fnbody.isPure b` return `true` Iff `b` is in the `λPure` fragment. -/
-mutual def Fnbody.isPure, Alts.isPure, Alt.isPure
-with Fnbody.isPure : Fnbody → Bool
+partial def Fnbody.isPure : Fnbody → Bool
 | (Fnbody.vdecl _ _ e b)    := e.isPure && b.isPure
 | (Fnbody.jdecl _ _ _ e b)  := e.isPure && b.isPure
 | (Fnbody.uset _ _ _ b)     := b.isPure
 | (Fnbody.sset _ _ _ _ _ b) := b.isPure
 | (Fnbody.mdata _ b)        := b.isPure
-| (Fnbody.case _ _ cs)      := Alts.isPure cs
+| (Fnbody.case _ _ alts)    := alts.any $ λ alt,
+  (match alt with
+   | (Alt.ctor _ b)  := b.isPure
+   | (Alt.default b) := false)
 | (Fnbody.ret _)            := true
 | (Fnbody.jmp _ _)          := true
 | Fnbody.unreachable        := true
 | _                         := false
-with Alts.isPure : List Alt → Bool
-| []      := true
-| (a::as) := a.isPure && Alts.isPure as
-with Alt.isPure : Alt → Bool
-| (Alt.ctor _ b)  := b.isPure
-| (Alt.default b) := false
 
 abbrev VarRenaming := NameMap Name
 
@@ -262,8 +258,7 @@ def addParamsRename : VarRenaming → List Param → List Param → Option VarRe
 | ρ []        []        := some ρ
 | _ _         _         := none
 
-mutual def Fnbody.alphaEqv, Alts.alphaEqv, Alt.alphaEqv
-with Fnbody.alphaEqv : VarRenaming → Fnbody → Fnbody → Bool
+partial def Fnbody.alphaEqv : VarRenaming → Fnbody → Fnbody → Bool
 | ρ (Fnbody.vdecl x₁ t₁ v₁ b₁)      (Fnbody.vdecl x₂ t₂ v₂ b₂)        := t₁ == t₂ && v₁ =[ρ]= v₂ && Fnbody.alphaEqv (addVarRename ρ x₁ x₂) b₁ b₂
 | ρ (Fnbody.jdecl j₁ ys₁ t₁ v₁ b₁)  (Fnbody.jdecl j₂ ys₂ t₂ v₂ b₂)    :=
   (match addParamsRename ρ ys₁ ys₂ with
@@ -277,19 +272,15 @@ with Fnbody.alphaEqv : VarRenaming → Fnbody → Fnbody → Bool
 | ρ (Fnbody.inc x₁ n₁ c₁ b₁)        (Fnbody.inc x₂ n₂ c₂ b₂)          := x₁ =[ρ]= x₂ && n₁ == n₂ && c₁ == c₂ && Fnbody.alphaEqv ρ b₁ b₂
 | ρ (Fnbody.dec x₁ n₁ c₁ b₁)        (Fnbody.dec x₂ n₂ c₂ b₂)          := x₁ =[ρ]= x₂ && n₁ == n₂ && c₁ == c₂ && Fnbody.alphaEqv ρ b₁ b₂
 | ρ (Fnbody.mdata m₁ b₁)            (Fnbody.mdata m₂ b₂)              := m₁ == m₂ && Fnbody.alphaEqv ρ b₁ b₂
-| ρ (Fnbody.case n₁ x₁ as₁)         (Fnbody.case n₂ x₂ as₂)           := n₁ == n₂ && x₁ =[ρ]= x₂ && Alts.alphaEqv ρ as₁ as₂
+| ρ (Fnbody.case n₁ x₁ alts₁)       (Fnbody.case n₂ x₂ alts₂)         := n₁ == n₂ && x₁ =[ρ]= x₂ && List.isEqv alts₁ alts₂ (λ alt₁ alt₂,
+   match alt₁, alt₂ with
+   | Alt.ctor i₁ b₁, Alt.ctor i₂ b₂ := i₁ == i₂ && Fnbody.alphaEqv ρ b₁ b₂
+   | Alt.default b₁, Alt.default b₂ := Fnbody.alphaEqv ρ b₁ b₂
+   | _,              _              := false)
 | ρ (Fnbody.jmp j₁ ys₁)             (Fnbody.jmp j₂ ys₂)               := j₁ == j₂ && ys₁ =[ρ]= ys₂
 | ρ (Fnbody.ret x₁)                 (Fnbody.ret x₂)                   := x₁ =[ρ]= x₂
 | _ Fnbody.unreachable              Fnbody.unreachable                := true
 | _ _                               _                                 := false
-with Alts.alphaEqv : VarRenaming → List Alt → List Alt → Bool
-| _ []        []        := true
-| ρ (a₁::as₁) (a₂::as₂) := Alt.alphaEqv ρ a₁ a₂ && Alts.alphaEqv ρ as₁ as₂
-| _ _         _         := false
-with Alt.alphaEqv : VarRenaming → Alt → Alt → Bool
-| ρ (Alt.ctor i₁ b₁) (Alt.ctor i₂ b₂) := i₁ == i₂ && Fnbody.alphaEqv ρ b₁ b₂
-| ρ (Alt.default b₁) (Alt.default b₂) := Fnbody.alphaEqv ρ b₁ b₂
-| _ _                _                := false
 
 def Fnbody.beq (b₁ b₂ : Fnbody) : Bool :=
 Fnbody.alphaEqv ∅  b₁ b₂
@@ -345,8 +336,7 @@ private def collectExpr : Expr → Collector
 | (Expr.isShared x)      := collectVar x
 | (Expr.isTaggedPtr x)   := collectVar x
 
-private mutual def collectFnBody, collectAlts, collectAlt
-with collectFnBody : Fnbody → Collector
+private partial def collectFnBody : Fnbody → Collector
 | (Fnbody.vdecl x _ v b)    := collectExpr v *> withBv x (collectFnBody b)
 | (Fnbody.jdecl j ys _ v b) := withParams ys (collectFnBody v) *> withBv j (collectFnBody b)
 | (Fnbody.set x _ y b)      := collectVar x *> collectVar y *> collectFnBody b
@@ -356,16 +346,14 @@ with collectFnBody : Fnbody → Collector
 | (Fnbody.inc x _ _ b)      := collectVar x *> collectFnBody b
 | (Fnbody.dec x _ _ b)      := collectVar x *> collectFnBody b
 | (Fnbody.mdata _ b)        := collectFnBody b
-| (Fnbody.case _ x as)      := collectVar x *> collectAlts as
+| (Fnbody.case _ x alts)    := collectVar x *> λ bv fv, alts.foldl (λ fv alt,
+   match alt with
+   | Alt.ctor _ b  := collectFnBody b bv fv
+   | Alt.default b := collectFnBody b bv fv)
+   fv
 | (Fnbody.jmp j ys)         := collectVar j *> collectArgs ys
 | (Fnbody.ret x)            := collectVar x
 | Fnbody.unreachable        := skip
-with collectAlts : List Alt → Collector
-| []      := skip
-| (a::as) := collectAlt a *> collectAlts as
-with collectAlt : Alt → Collector
-| (Alt.ctor _ b)  := collectFnBody b
-| (Alt.default b) := collectFnBody b
 
 def freeVars (b : Fnbody) : VarSet :=
 collectFnBody b ∅ ∅

library/init/lean/elaborator.lean

@@ -131,6 +131,9 @@ structure ElaboratorState :=
 def ElaboratorM := RecT Syntax Unit $ ReaderT ElaboratorConfig $ StateT ElaboratorState $ ExceptT Message id
 abbrev Elaborator := Syntax → ElaboratorM Unit
 
+instance elaboratorInh (α : Type) : Inhabited (ElaboratorM α) :=
+⟨λ _ _ _, Except.error (default _)⟩
+
 /-- Recursively elaborate any command. -/
 def command.elaborate : Elaborator := recurse
 
@@ -149,7 +152,7 @@ def modifyCurrentScope (f : Scope → Scope) : ElaboratorM Unit := do
 def mangleIdent (id : SyntaxIdent) : Name :=
 id.scopes.foldl Name.mkNumeral id.val
 
-def levelGetAppArgs : Syntax → ElaboratorM (Syntax × List Syntax)
+partial def levelGetAppArgs : Syntax → ElaboratorM (Syntax × List Syntax)
 | stx := do
   match stx.kind with
   | some Level.leading := pure (stx, [])
@@ -164,7 +167,7 @@ def levelAdd : Level → Nat → Level
 | l 0     := l
 | l (n+1) := (levelAdd l n).succ
 
-def toLevel : Syntax → ElaboratorM Level
+partial def toLevel : Syntax → ElaboratorM Level
 | stx := do
   (fn, args) ← levelGetAppArgs stx,
   sc ← currentScope,
@@ -198,7 +201,7 @@ def mkEqns (type : Expr) (eqns : List (Name × List Expr × Expr)): Expr :=
   } in
   Expr.mkAnnotation `preEquations $ Expr.mkCapp `_ eqns
 
-def toPexpr : Syntax → ElaboratorM Expr
+partial def toPexpr : Syntax → ElaboratorM Expr
 | stx@(Syntax.rawNode {kind := k, args := args}) := do
   e ← match k with
   | @identUnivs := do
@@ -970,7 +973,7 @@ def resolveContext : Name → ElaboratorM (List Name)
 
   -- TODO: projection notation
 
-def preresolve : Syntax → ElaboratorM Syntax
+partial def preresolve : Syntax → ElaboratorM Syntax
 | (Syntax.ident id) := do
   let n := mangleIdent id,
   ns ← resolveContext n,

library/init/lean/format.lean

@@ -20,6 +20,7 @@ inductive Format
 namespace Format
 instance : HasAppend Format     := ⟨compose false⟩
 instance : HasCoe String Format := ⟨text⟩
+instance : Inhabited Format     := ⟨nil⟩
 
 def join (xs : List Format) : Format :=
 xs.foldl (++) ""
@@ -44,10 +45,7 @@ structure SpaceResult :=
 (exceeded := false)
 (space    := 0)
 
-/-
-TODO: mark as `@[inline]` as soon as we fix the code inliner.
--/
-private def merge (w : Nat) (r₁ : SpaceResult) (r₂ : Thunk SpaceResult) : SpaceResult :=
+@[inline] private def merge (w : Nat) (r₁ : SpaceResult) (r₂ : Thunk SpaceResult) : SpaceResult :=
 if r₁.exceeded || r₁.found then r₁
 else let y := r₂.get in
      if y.exceeded || y.found then y
@@ -66,7 +64,7 @@ def spaceUptoLine' : List (Nat × Format) → Nat → SpaceResult
 | []      w := {}
 | (p::ps) w := merge w (spaceUptoLine p.2 w) (spaceUptoLine' ps w)
 
-def be : Nat → Nat → String → List (Nat × Format) → String
+partial def be : Nat → Nat → String → List (Nat × Format) → String
 | w k out []                           := out
 | w k out ((i, nil)::z)                := be w k out z
 | w k out ((i, (compose _ f₁ f₂))::z)  := be w k out ((i, f₁)::(i, f₂)::z)

library/init/lean/kvmap.lean

@@ -93,13 +93,16 @@ m.insert k (DataValue.ofBool v)
 def setName (m : KVMap) (k : Name) (v : Name) : KVMap :=
 m.insert k (DataValue.ofName v)
 
-def subset : KVMap → KVMap → Bool
-| ⟨[]⟩          m₂ := true
-| ⟨(k, v₁)::m₁⟩ m₂ :=
+def subsetAux : List (Name × DataValue) → KVMap → Bool
+| []            m₂ := true
+| ((k, v₁)::m₁) m₂ :=
   (match m₂.find k with
-   | some v₂ := v₁ == v₂ && subset ⟨m₁⟩ m₂
+   | some v₂ := v₁ == v₂ && subsetAux m₁ m₂
    | none    := false)
 
+def subset : KVMap → KVMap → Bool
+| ⟨m₁⟩ m₂ := subsetAux m₁ m₂
+
 def eqv (m₁ m₂ : KVMap) : Bool :=
 subset m₁ m₂ && subset m₂ m₁
 

library/init/lean/level.lean

@@ -90,11 +90,11 @@ def Result.succ : Result → Result
 
 def Result.max : Result → Result → Result
 | f (Result.maxNode Fs) := Result.maxNode (f::Fs)
-| f₁ f₂                  := Result.maxNode [f₁, f₂]
+| f₁ f₂                 := Result.maxNode [f₁, f₂]
 
 def Result.imax : Result → Result → Result
 | f (Result.imaxNode Fs) := Result.imaxNode (f::Fs)
-| f₁ f₂                   := Result.imaxNode [f₁, f₂]
+| f₁ f₂                  := Result.imaxNode [f₁, f₂]
 
 def parenIfFalse : Format → Bool → Format
 | f true  := f

library/init/lean/message.lean

@@ -31,6 +31,9 @@ msg.filename ++ ":" ++ toString msg.pos.line ++ ":" ++ toString msg.pos.column +
 (if msg.caption = "" then "" else msg.caption ++ ":\n") ++
 msg.text
 
+instance : Inhabited Message :=
+⟨{ filename := "", pos := ⟨0, 1⟩, text := ""}⟩
+
 instance : HasToString Message :=
 ⟨Message.toString⟩
 end Message

library/init/lean/name.lean

@@ -162,6 +162,8 @@ variable {α : Type}
 
 instance (α : Type) : HasEmptyc (NameMap α) := ⟨mkNameMap α⟩
 
+instance (α : Type) : Inhabited (NameMap α) := ⟨{}⟩
+
 def insert (m : NameMap α) (n : Name) (a : α) := RBMap.insert m n a
 
 def contains (m : NameMap α) (n : Name) : Bool := RBMap.contains m n
@@ -178,6 +180,8 @@ namespace NameSet
 
 instance : HasEmptyc NameSet := ⟨mkNameSet⟩
 
+instance : Inhabited NameSet := ⟨{}⟩
+
 def insert (s : NameSet) (n : Name)  := RBTree.insert s n
 
 def contains (s : NameSet) (n : Name) : Bool := RBMap.contains s n

library/init/lean/parser/syntax.lean

@@ -127,20 +127,17 @@ def isOfKind (k : SyntaxNodeKind) : Syntax → Bool
 
 section
 variables {m : Type → Type} [Monad m] (r : Syntax → m (Option Syntax))
+local attribute [instance] monadInhabited
 
-mutual def mreplace, mreplaceLst
-with mreplace : Syntax → m Syntax
+partial def mreplace : Syntax → m Syntax
 | stx@(rawNode n) := do
   o ← r stx,
   (match o with
   | some stx' := pure stx'
-  | none      := do args' ← mreplaceLst n.args, pure $ rawNode {n with args := args'})
+  | none      := do args' ← n.args.mmap mreplace, pure $ rawNode {n with args := args'})
 | stx := do
   o ← r stx,
   pure $ o.getOrElse stx
-with mreplaceLst : List Syntax → m (List Syntax)
-| []      := pure []
-| (s::ss) := List.cons <$> mreplace s <*> mreplaceLst ss
 
 def replace := @mreplace id _
 end
@@ -173,15 +170,11 @@ def updateLeading (source : String) : Syntax → Syntax :=
 λ stx, Prod.fst $ (mreplace updateLeadingAux stx).run source.mkOldIterator
 
 /-- Retrieve the left-most leaf's info in the Syntax tree. -/
-mutual def getHeadInfo, getHeadInfoLst
-with getHeadInfo : Syntax → Option SourceInfo
-| (atom a)   := a.info
-| (ident id) := id.info
-| (rawNode n) := getHeadInfoLst n.args
-| _ := none
-with getHeadInfoLst : List Syntax → Option SourceInfo
-| [] := none
-| (stx::stxs) := getHeadInfo stx <|> getHeadInfoLst stxs
+partial def getHeadInfo : Syntax → Option SourceInfo
+| (atom a)    := a.info
+| (ident id)  := id.info
+| (rawNode n) := n.args.foldr (λ s r, getHeadInfo s <|> r) none
+| _           := none
 
 def getPos (stx : Syntax) : Option Parsec.Position :=
 do i ← stx.getHeadInfo,
@@ -191,8 +184,7 @@ def reprintAtom : SyntaxAtom → String
 | ⟨some info, s⟩ := info.leading.toString ++ s ++ info.trailing.toString
 | ⟨none, s⟩      := s
 
-mutual def reprint, reprintLst
-with reprint : Syntax → Option String
+partial def reprint : Syntax → Option String
 | (atom ⟨some info, s⟩) := pure $ info.leading.toString ++ s ++ info.trailing.toString
 | (atom ⟨none, s⟩)      := pure s
 | (ident id@{info := some info, ..}) := pure $ info.leading.toString ++ id.rawVal.toString ++ info.trailing.toString
@@ -204,20 +196,13 @@ with reprint : Syntax → Option String
   -- check that every choice prints the same
   | n::ns := do
     s ← reprint n,
-    ss ← reprintLst ns,
+    ss ← ns.mmap reprint,
     guard $ ss.all (= s),
     pure s
-  else String.join <$> reprintLst n.args
+  else String.join <$> n.args.mmap reprint
 | missing := ""
-with reprintLst : List Syntax → Option (List String)
-| []      := pure []
-| (n::ns) := do
-  s ← reprint n,
-  ss ← reprintLst ns,
-  pure $ s::ss
 
-protected mutual def toFormat, toFormatLst
-with toFormat : Syntax → Format
+protected partial def toFormat : Syntax → Format
 | (atom ⟨_, s⟩) := toFmt $ repr s
 | (ident id)    :=
   let scopes := id.preresolved.map toFmt ++ id.scopes.reverse.map toFmt in
@@ -225,13 +210,10 @@ with toFormat : Syntax → Format
   toFmt "`" ++ toFmt id.val ++ scopes
 | stx@(rawNode n) :=
   let scopes := match n.scopes with [] := toFmt "" | _ := bracket "{" (joinSep n.scopes.reverse ", ") "}" in
-  if n.kind.name = `Lean.Parser.noKind then sbracket $ scopes ++ joinSep (toFormatLst n.args) line
+  if n.kind.name = `Lean.Parser.noKind then sbracket $ scopes ++ joinSep (n.args.map toFormat) line
   else let shorterName := n.kind.name.replacePrefix `Lean.Parser Name.anonymous
-       in paren $ joinSep ((toFmt shorterName ++ scopes) :: toFormatLst n.args) line
+       in paren $ joinSep ((toFmt shorterName ++ scopes) :: n.args.map toFormat) line
 | missing := "<missing>"
-with toFormatLst : List Syntax → List Format
-| []      := []
-| (s::ss) := toFormat s :: toFormatLst ss
 
 instance : HasToFormat Syntax := ⟨Syntax.toFormat⟩
 instance : HasToString Syntax := ⟨toString ∘ toFmt⟩

library/init/lean/parser/trie.lean

@@ -50,7 +50,7 @@ private def matchPrefixAux : Nat → Trie α → String.OldIterator → Option (
 def matchPrefix {α : Type} (t : Trie α) (it : String.OldIterator) : Option (String.OldIterator × α) :=
 matchPrefixAux it.remaining t it none
 
-private def toStringAux {α : Type} : Trie α → List Format
+private partial def toStringAux {α : Type} : Trie α → List Format
 | (Trie.Node val map) := flip RBNode.fold map (λ c t Fs,
   toFormat (repr c) :: (Format.group $ Format.nest 2 $ flip Format.joinSep Format.line $ toStringAux t) :: Fs) []
 

library/init/lean/trace.lean

@@ -19,7 +19,7 @@ instance : HasCoe Format Message :=
 inductive Trace
 | mk (msg : Message) (subtraces : List Trace)
 
-def Trace.pp : Trace → Format
+partial def Trace.pp : Trace → Format
 | (Trace.mk (Message.fromFormat fmt) subtraces) :=
 fmt ++ Format.nest 2 (Format.join $ subtraces.map (λ t, Format.line ++ t.pp))