From b66f5dcf5ca37fc6579f38113804488daa953972 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 27 Mar 2019 12:12:21 -0700 Subject: [PATCH] chore(library/init): avoid `wf_term_hack` --- library/init/control/monad.lean | 5 +++ library/init/data/list/basic.lean | 4 +++ library/init/data/nat/bitwise.lean | 2 +- library/init/lean/compiler/ir.lean | 46 ++++++++++------------------ library/init/lean/elaborator.lean | 11 ++++--- library/init/lean/format.lean | 8 ++--- library/init/lean/kvmap.lean | 11 ++++--- library/init/lean/level.lean | 4 +-- library/init/lean/message.lean | 3 ++ library/init/lean/name.lean | 4 +++ library/init/lean/parser/syntax.lean | 46 +++++++++------------------- library/init/lean/parser/trie.lean | 2 +- library/init/lean/trace.lean | 2 +- 13 files changed, 69 insertions(+), 79 deletions(-) diff --git a/library/init/control/monad.lean b/library/init/control/monad.lean index b93041f6e0..1c3a850290 100644 --- a/library/init/control/monad.lean +++ b/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 _⟩ diff --git a/library/init/data/list/basic.lean b/library/init/data/list/basic.lean index 352568778c..d5ca44cef2 100644 --- a/library/init/data/list/basic.lean +++ b/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 diff --git a/library/init/data/nat/bitwise.lean b/library/init/data/nat/bitwise.lean index 7c5f1dd78b..1642aa2299 100644 --- a/library/init/data/nat/bitwise.lean +++ b/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 diff --git a/library/init/lean/compiler/ir.lean b/library/init/lean/compiler/ir.lean index 59916e7e56..d5d7119cd6 100644 --- a/library/init/lean/compiler/ir.lean +++ b/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 ∅ ∅ diff --git a/library/init/lean/elaborator.lean b/library/init/lean/elaborator.lean index ab769db4f1..9ea22928f9 100644 --- a/library/init/lean/elaborator.lean +++ 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, diff --git a/library/init/lean/format.lean b/library/init/lean/format.lean index ad68cdcda8..020eb04d57 100644 --- a/library/init/lean/format.lean +++ b/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) diff --git a/library/init/lean/kvmap.lean b/library/init/lean/kvmap.lean index 9913d9b9e5..20859bf56a 100644 --- a/library/init/lean/kvmap.lean +++ b/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₁ diff --git a/library/init/lean/level.lean b/library/init/lean/level.lean index 2302037090..5b1fa9e6f9 100644 --- a/library/init/lean/level.lean +++ b/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 diff --git a/library/init/lean/message.lean b/library/init/lean/message.lean index 5d0adf713b..91c60eee85 100644 --- a/library/init/lean/message.lean +++ b/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 diff --git a/library/init/lean/name.lean b/library/init/lean/name.lean index a1e335478e..a5b0338b53 100644 --- a/library/init/lean/name.lean +++ b/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 diff --git a/library/init/lean/parser/syntax.lean b/library/init/lean/parser/syntax.lean index ec3b1a54c5..dd756745bf 100644 --- a/library/init/lean/parser/syntax.lean +++ b/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 := "" -with toFormatLst : List Syntax → List Format -| [] := [] -| (s::ss) := toFormat s :: toFormatLst ss instance : HasToFormat Syntax := ⟨Syntax.toFormat⟩ instance : HasToString Syntax := ⟨toString ∘ toFmt⟩ diff --git a/library/init/lean/parser/trie.lean b/library/init/lean/parser/trie.lean index 8e7880ef1b..63ac5cd6b8 100644 --- a/library/init/lean/parser/trie.lean +++ b/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) [] diff --git a/library/init/lean/trace.lean b/library/init/lean/trace.lean index 3218ef1b4a..340e577c13 100644 --- a/library/init/lean/trace.lean +++ b/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))