From 97c93ec5579432bad3c4990236d6814e4bfddacf Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 27 Oct 2020 16:42:58 -0700 Subject: [PATCH] chore: prepare to rename --- src/Init/Control/Applicative.lean | 12 ++++++ src/Init/Control/Conditional.lean | 3 ++ src/Init/Control/Monad.lean | 3 ++ src/Init/Core.lean | 23 +++++++++++ src/Init/Data/List/Basic.lean | 4 +- src/Init/LeanInit.lean | 3 ++ src/Init/System/IO.lean | 6 +++ src/Init/WF.lean | 4 ++ src/Lean/Compiler/ConstFolding.lean | 4 +- src/Lean/Compiler/IR/Basic.lean | 3 ++ src/Lean/Data/Json/FromToJson.lean | 6 +++ src/Lean/Elab/App.lean | 2 +- src/Lean/Elab/BuiltinNotation.lean | 44 ++++++++++----------- src/Lean/Elab/Command.lean | 4 +- src/Lean/Elab/Do.lean | 60 ++++++++++++++--------------- src/Lean/Elab/Quotation.lean | 2 +- src/Lean/Elab/Term.lean | 10 ++--- src/Lean/Meta/AppBuilder.lean | 14 +++---- src/Lean/Meta/DiscrTree.lean | 12 +++--- src/Lean/Meta/Offset.lean | 12 +++--- src/Lean/Meta/ReduceEval.lean | 3 ++ 21 files changed, 150 insertions(+), 84 deletions(-) diff --git a/src/Init/Control/Applicative.lean b/src/Init/Control/Applicative.lean index 6081d8380c..c46005fcd4 100644 --- a/src/Init/Control/Applicative.lean +++ b/src/Init/Control/Applicative.lean @@ -22,6 +22,18 @@ class HasSeqLeft (f : Type u → Type v) : Type (max (u+1) v) := class HasSeqRight (f : Type u → Type v) : Type (max (u+1) v) := (seqRight : {β : Type u} → f PUnit → f β → f β) +class Pure (f : Type u → Type v) := + (pure {α : Type u} : α → f α) + +class Seq (f : Type u → Type v) : Type (max (u+1) v) := + (seq : {α β : Type u} → f (α → β) → f α → f β) + +class SeqLeft (f : Type u → Type v) : Type (max (u+1) v) := + (seqLeft : {α : Type u} → f α → f PUnit → f α) + +class SeqRight (f : Type u → Type v) : Type (max (u+1) v) := + (seqRight : {β : Type u} → f PUnit → f β → f β) + class Applicative (f : Type u → Type v) extends Functor f, HasPure f, HasSeq f, HasSeqLeft f, HasSeqRight f := (map := fun x y => pure x <*> y) (seqLeft := fun a b => const _ <$> a <*> b) diff --git a/src/Init/Control/Conditional.lean b/src/Init/Control/Conditional.lean index d96e820338..4a72b58ce9 100644 --- a/src/Init/Control/Conditional.lean +++ b/src/Init/Control/Conditional.lean @@ -11,6 +11,9 @@ universes u v class HasToBool (α : Type u) := (toBool : α → Bool) +class ToBool (α : Type u) := + (toBool : α → Bool) + export HasToBool (toBool) instance : HasToBool Bool := ⟨id⟩ diff --git a/src/Init/Control/Monad.lean b/src/Init/Control/Monad.lean index afd2c3b437..2ab86ef0ab 100644 --- a/src/Init/Control/Monad.lean +++ b/src/Init/Control/Monad.lean @@ -13,6 +13,9 @@ open Function class HasBind (m : Type u → Type v) := (bind : {α β : Type u} → m α → (α → m β) → m β) +class Bind (m : Type u → Type v) := + (bind : {α β : Type u} → m α → (α → m β) → m β) + export HasBind (bind) @[inline] def mcomp {α : Type u} {β δ : Type v} {m : Type v → Type w} [HasBind m] (f : α → m β) (g : β → m δ) : α → m δ := diff --git a/src/Init/Core.lean b/src/Init/Core.lean index 70224d4e08..018e17aaa8 100644 --- a/src/Init/Core.lean +++ b/src/Init/Core.lean @@ -275,6 +275,9 @@ class HasOfNat (α : Type u) := export HasOfNat (ofNat) +class OfNat (α : Type u) := + (ofNat : Nat → α) + instance : HasOfNat Nat := ⟨id⟩ /- Auxiliary axiom used to implement `sorry`. @@ -300,6 +303,23 @@ class HasEquiv (α : Sort u) := (Equiv : α → α → Prop) class HasEmptyc (α : Type u) := (emptyc : α) class HasPow (α : Type u) (β : Type v) := (pow : α → β → α) +class Add (α : Type u) := (add : α → α → α) +class Mul (α : Type u) := (mul : α → α → α) +class Neg (α : Type u) := (neg : α → α) +class Sub (α : Type u) := (sub : α → α → α) +class Div (α : Type u) := (div : α → α → α) +class Mod (α : Type u) := (mod : α → α → α) +class ModN (α : Type u) := (modn : α → Nat → α) +class LessEq (α : Type u) := (LessEq : α → α → Prop) +class Less (α : Type u) := (Less : α → α → Prop) +class Beq (α : Type u) := (beq : α → α → Bool) +class Append (α : Type u) := (append : α → α → α) +class OrElse (α : Type u) := (orElse : α → α → α) +class AndThen (α : Type u) := (andThen : α → α → α) +class Equiv (α : Sort u) := (Equiv : α → α → Prop) +class EmptyCollection (α : Type u) := (emptyCollection : α) +class Pow (α : Type u) (β : Type v) := (pow : α → β → α) + @[reducible] def GreaterEq {α : Type u} [HasLessEq α] (a b : α) : Prop := HasLessEq.LessEq b a @[reducible] def Greater {α : Type u} [HasLess α] (a b : α) : Prop := HasLess.Less b a @@ -388,6 +408,9 @@ class HasSizeof (α : Sort u) := export HasSizeof (sizeof) +class SizeOf (α : Sort u) := + (sizeOf : α → Nat) + /- Declare sizeof instances and theorems for types declared before HasSizeof. From now on, the inductive Compiler will automatically generate sizeof instances and theorems. diff --git a/src/Init/Data/List/Basic.lean b/src/Init/Data/List/Basic.lean index fe7f73909d..36b7b62615 100644 --- a/src/Init/Data/List/Basic.lean +++ b/src/Init/Data/List/Basic.lean @@ -303,7 +303,7 @@ inductive Less [HasLess α] : List α → List α → Prop | head {a : α} (as : List α) {b : α} (bs : List α) : a < b → Less (a::as) (b::bs) | tail {a : α} {as : List α} {b : α} {bs : List α} : ¬ a < b → ¬ b < a → Less as bs → Less (a::as) (b::bs) -instance [HasLess α] : HasLess (List α) := ⟨List.Less⟩ +instance less [HasLess α] : HasLess (List α) := ⟨List.Less⟩ instance hasDecidableLt [HasLess α] [h : DecidableRel (α:=α) (·<·)] : (l₁ l₂ : List α) → Decidable (l₁ < l₂) | [], [] => isFalse (fun h => nomatch h) @@ -326,7 +326,7 @@ instance hasDecidableLt [HasLess α] [h : DecidableRel (α:=α) (·<·)] : (l₁ @[reducible] protected def LessEq [HasLess α] (a b : List α) : Prop := ¬ b < a -instance [HasLess α] : HasLessEq (List α) := ⟨List.LessEq⟩ +instance lessEq [HasLess α] : HasLessEq (List α) := ⟨List.LessEq⟩ instance [HasLess α] [h : DecidableRel (HasLess.Less : α → α → Prop)] : (l₁ l₂ : List α) → Decidable (l₁ ≤ l₂) := fun a b => inferInstanceAs (Decidable (Not _)) diff --git a/src/Init/LeanInit.lean b/src/Init/LeanInit.lean index 8356a6d9f1..72e73b7bf5 100644 --- a/src/Init/LeanInit.lean +++ b/src/Init/LeanInit.lean @@ -849,6 +849,9 @@ class HasQuote (α : Type) := export HasQuote (quote) +class Quote (α : Type) := + (quote : α → Syntax) + instance : HasQuote Syntax := ⟨id⟩ instance : HasQuote String := ⟨mkStxStrLit⟩ instance : HasQuote Nat := ⟨fun n => mkStxNumLit $ toString n⟩ diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean index 900b67a83a..23c5d444a3 100644 --- a/src/Init/System/IO.lean +++ b/src/Init/System/IO.lean @@ -468,6 +468,12 @@ class HasEval (α : Type u) := -- We take `Unit → α` instead of `α` because ‵α` may contain effectful debugging primitives (e.g., `dbgTrace!`) (eval : (Unit → α) → forall (hideUnit : optParam Bool true), IO Unit) +class Eval (α : Type u) := + -- We default `hideUnit` to `true`, but set it to `false` in the direct call from `#eval` + -- so that `()` output is hidden in chained instances such as for some `m Unit`. + -- We take `Unit → α` instead of `α` because ‵α` may contain effectful debugging primitives (e.g., `dbgTrace!`) + (eval : (Unit → α) → forall (hideUnit : optParam Bool true), IO Unit) + instance {α : Type u} [Repr α] : HasEval α := ⟨fun a _ => IO.println (repr (a ()))⟩ diff --git a/src/Init/WF.lean b/src/Init/WF.lean index d516003406..aa15be8b88 100644 --- a/src/Init/WF.lean +++ b/src/Init/WF.lean @@ -42,6 +42,10 @@ class HasWellFounded (α : Sort u) : Type u := (r : α → α → Prop) (wf : WellFounded r) +class WellFoundedRelation (α : Sort u) : Type u := + (r : α → α → Prop) + (wf : WellFounded r) + namespace WellFounded def apply {α : Sort u} {r : α → α → Prop} (wf : WellFounded r) (a : α) : Acc r a := WellFounded.recOn (motive := fun x => (y : α) → Acc r y) diff --git a/src/Lean/Compiler/ConstFolding.lean b/src/Lean/Compiler/ConstFolding.lean index 0b44171986..354d549e2c 100644 --- a/src/Lean/Compiler/ConstFolding.lean +++ b/src/Lean/Compiler/ConstFolding.lean @@ -96,10 +96,10 @@ def mkNatEq (a b : Expr) : Expr := mkAppN (mkConst `Eq [levelOne]) #[(mkConst `Nat), a, b] def mkNatLt (a b : Expr) : Expr := - mkAppN (mkConst `HasLt.lt [levelZero]) #[mkConst `Nat, mkConst `Nat.HasLt, a, b] + mkAppN (mkConst `Less.Less [levelZero]) #[mkConst `Nat, mkConst `Nat.less, a, b] def mkNatLe (a b : Expr) : Expr := - mkAppN (mkConst `HasLt.le [levelZero]) #[mkConst `Nat, mkConst `Nat.HasLe, a, b] + mkAppN (mkConst `LessEq.LessEq [levelZero]) #[mkConst `Nat, mkConst `Nat.lessEq, a, b] def toDecidableExpr (beforeErasure : Bool) (pred : Expr) (r : Bool) : Expr := match beforeErasure, r with diff --git a/src/Lean/Compiler/IR/Basic.lean b/src/Lean/Compiler/IR/Basic.lean index d8e9eeff4f..13a7c57fd9 100644 --- a/src/Lean/Compiler/IR/Basic.lean +++ b/src/Lean/Compiler/IR/Basic.lean @@ -494,6 +494,9 @@ abbrev IndexRenaming := RBMap Index Index Index.lt class HasAlphaEqv (α : Type) := (aeqv : IndexRenaming → α → α → Bool) +class AlphaEqv (α : Type) := + (aeqv : IndexRenaming → α → α → Bool) + export HasAlphaEqv (aeqv) def VarId.alphaEqv (ρ : IndexRenaming) (v₁ v₂ : VarId) : Bool := diff --git a/src/Lean/Data/Json/FromToJson.lean b/src/Lean/Data/Json/FromToJson.lean index 4ade066fd9..74621fb3da 100644 --- a/src/Lean/Data/Json/FromToJson.lean +++ b/src/Lean/Data/Json/FromToJson.lean @@ -13,8 +13,14 @@ universes u class HasFromJson (α : Type u) := (fromJson? : Json → Option α) +class FromJson (α : Type u) := + (fromJson? : Json → Option α) + export HasFromJson (fromJson?) +class ToJson (α : Type u) := + (toJson : α → Json) + class HasToJson (α : Type u) := (toJson : α → Json) diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index 81aa291467..46e2daf4c5 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -213,7 +213,7 @@ private partial def getForallBody : Nat → List NamedArg → Expr → Option Ex Auxiliary method for propagating the expected type. We call it as soon as we find the first explict argument. The goal is to propagate the expected type in applications of functions such as ```lean - HasAdd.add {α : Type u} : α → α → α + Add.add {α : Type u} : α → α → α List.cons {α : Type u} : α → List α → List α ``` This is particularly useful when there applicable coercions. For example, diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean index ca96fea528..ace42a2d48 100644 --- a/src/Lean/Elab/BuiltinNotation.lean +++ b/src/Lean/Elab/BuiltinNotation.lean @@ -99,10 +99,10 @@ private def elabParserMacroAux (prec : Syntax) (e : Syntax) : TermElabM Syntax : let p ← `(Lean.Parser.leadingNode $kind $prec $e) if scps == [] then -- TODO simplify the following quotation as soon as we have coercions - `(HasOrelse.orelse (Lean.Parser.mkAntiquot $s (some $kind)) $p) + `(OrElse.orElse (Lean.Parser.mkAntiquot $s (some $kind)) $p) else -- if the parser decl is hidden by hygiene, it doesn't make sense to provide an antiquotation kind - `(HasOrelse.orelse (Lean.Parser.mkAntiquot $s none) $p) + `(OrElse.orElse (Lean.Parser.mkAntiquot $s none) $p) | _ => throwError "invalid `parser!` macro, unexpected declaration name" @[builtinTermElab «parser!»] def elabParserMacro : TermElab := @@ -208,24 +208,24 @@ def expandPrefixOp (op : Name) : Macro := fun stx => do @[builtinMacro Lean.Parser.Term.prod] def expandProd : Macro := expandInfixOp `Prod @[builtinMacro Lean.Parser.Term.fcomp] def ExpandFComp : Macro := expandInfixOp `Function.comp -@[builtinMacro Lean.Parser.Term.add] def expandAdd : Macro := expandInfixOp `HasAdd.add -@[builtinMacro Lean.Parser.Term.sub] def expandSub : Macro := expandInfixOp `HasSub.sub -@[builtinMacro Lean.Parser.Term.mul] def expandMul : Macro := expandInfixOp `HasMul.mul -@[builtinMacro Lean.Parser.Term.div] def expandDiv : Macro := expandInfixOp `HasDiv.div -@[builtinMacro Lean.Parser.Term.mod] def expandMod : Macro := expandInfixOp `HasMod.mod -@[builtinMacro Lean.Parser.Term.modN] def expandModN : Macro := expandInfixOp `HasModN.modn -@[builtinMacro Lean.Parser.Term.pow] def expandPow : Macro := expandInfixOp `HasPow.pow +@[builtinMacro Lean.Parser.Term.add] def expandAdd : Macro := expandInfixOp `Add.add +@[builtinMacro Lean.Parser.Term.sub] def expandSub : Macro := expandInfixOp `Sub.sub +@[builtinMacro Lean.Parser.Term.mul] def expandMul : Macro := expandInfixOp `Mul.mul +@[builtinMacro Lean.Parser.Term.div] def expandDiv : Macro := expandInfixOp `Div.div +@[builtinMacro Lean.Parser.Term.mod] def expandMod : Macro := expandInfixOp `Mod.mod +@[builtinMacro Lean.Parser.Term.modN] def expandModN : Macro := expandInfixOp `ModN.modn +@[builtinMacro Lean.Parser.Term.pow] def expandPow : Macro := expandInfixOp `Pow.pow -@[builtinMacro Lean.Parser.Term.le] def expandLE : Macro := expandInfixOp `HasLessEq.LessEq +@[builtinMacro Lean.Parser.Term.le] def expandLE : Macro := expandInfixOp `LessEq.LessEq @[builtinMacro Lean.Parser.Term.ge] def expandGE : Macro := expandInfixOp `GreaterEq -@[builtinMacro Lean.Parser.Term.lt] def expandLT : Macro := expandInfixOp `HasLess.Less +@[builtinMacro Lean.Parser.Term.lt] def expandLT : Macro := expandInfixOp `Less.Less @[builtinMacro Lean.Parser.Term.gt] def expandGT : Macro := expandInfixOp `Greater @[builtinMacro Lean.Parser.Term.eq] def expandEq : Macro := expandInfixOp `Eq @[builtinMacro Lean.Parser.Term.ne] def expandNe : Macro := expandInfixOp `Ne -@[builtinMacro Lean.Parser.Term.beq] def expandBEq : Macro := expandInfixOp `HasBeq.beq +@[builtinMacro Lean.Parser.Term.beq] def expandBEq : Macro := expandInfixOp `BEq.beq @[builtinMacro Lean.Parser.Term.bne] def expandBNe : Macro := expandInfixOp `bne @[builtinMacro Lean.Parser.Term.heq] def expandHEq : Macro := expandInfixOp `HEq -@[builtinMacro Lean.Parser.Term.equiv] def expandEquiv : Macro := expandInfixOp `HasEquiv.Equiv +@[builtinMacro Lean.Parser.Term.equiv] def expandEquiv : Macro := expandInfixOp `Equiv.Equiv @[builtinMacro Lean.Parser.Term.and] def expandAnd : Macro := expandInfixOp `And @[builtinMacro Lean.Parser.Term.or] def expandOr : Macro := expandInfixOp `Or @@ -234,26 +234,26 @@ def expandPrefixOp (op : Name) : Macro := fun stx => do @[builtinMacro Lean.Parser.Term.band] def expandBAnd : Macro := expandInfixOp `and @[builtinMacro Lean.Parser.Term.bor] def expandBOr : Macro := expandInfixOp `or -@[builtinMacro Lean.Parser.Term.append] def expandAppend : Macro := expandInfixOp `HasAppend.append +@[builtinMacro Lean.Parser.Term.append] def expandAppend : Macro := expandInfixOp `Append.append @[builtinMacro Lean.Parser.Term.cons] def expandCons : Macro := expandInfixOp `List.cons -@[builtinMacro Lean.Parser.Term.andthen] def expandAndThen : Macro := expandInfixOp `HasAndthen.andthen -@[builtinMacro Lean.Parser.Term.bindOp] def expandBind : Macro := expandInfixOp `HasBind.bind +@[builtinMacro Lean.Parser.Term.andthen] def expandAndThen : Macro := expandInfixOp `AndThen.andThen +@[builtinMacro Lean.Parser.Term.bindOp] def expandBind : Macro := expandInfixOp `Bind.bind -@[builtinMacro Lean.Parser.Term.seq] def expandseq : Macro := expandInfixOp `HasSeq.seq -@[builtinMacro Lean.Parser.Term.seqLeft] def expandseqLeft : Macro := expandInfixOp `HasSeqLeft.seqLeft -@[builtinMacro Lean.Parser.Term.seqRight] def expandseqRight : Macro := expandInfixOp `HasSeqRight.seqRight +@[builtinMacro Lean.Parser.Term.seq] def expandSeq : Macro := expandInfixOp `Seq.seq +@[builtinMacro Lean.Parser.Term.seqLeft] def expandSeqLeft : Macro := expandInfixOp `SeqLeft.seqLeft +@[builtinMacro Lean.Parser.Term.seqRight] def expandSeqRight : Macro := expandInfixOp `SeqRight.seqRight @[builtinMacro Lean.Parser.Term.map] def expandMap : Macro := expandInfixOp `Functor.map @[builtinMacro Lean.Parser.Term.mapRev] def expandMapRev : Macro := expandInfixOp `Functor.mapRev -@[builtinMacro Lean.Parser.Term.orelse] def expandOrElse : Macro := expandInfixOp `HasOrelse.orelse +@[builtinMacro Lean.Parser.Term.orelse] def expandOrElse : Macro := expandInfixOp `OrElse.orElse @[builtinMacro Lean.Parser.Term.orM] def expandOrM : Macro := expandInfixOp `orM @[builtinMacro Lean.Parser.Term.andM] def expandAndM : Macro := expandInfixOp `andM @[builtinMacro Lean.Parser.Term.not] def expandNot : Macro := expandPrefixOp `Not @[builtinMacro Lean.Parser.Term.bnot] def expandBNot : Macro := expandPrefixOp `not -@[builtinMacro Lean.Parser.Term.uminus] def expandUMinus : Macro := expandPrefixOp `HasNeg.neg +@[builtinMacro Lean.Parser.Term.uminus] def expandUMinus : Macro := expandPrefixOp `Neg.neg @[builtinTermElab panic] def elabPanic : TermElab := fun stx expectedType? => do let arg := stx[1] @@ -287,7 +287,7 @@ def expandPrefixOp (op : Name) : Macro := fun stx => do `(sorryAx _ false) @[builtinTermElab emptyC] def expandEmptyC : TermElab := fun stx expectedType? => do - let stxNew ← `(HasEmptyc.emptyc) + let stxNew ← `(EmptyCollection.emptyCollection) withMacroExpansion stx stxNew $ elabTerm stxNew expectedType? /-- Return syntax `Prod.mk elems[0] (Prod.mk elems[1] ... (Prod.mk elems[elems.size - 2] elems[elems.size - 1])))` -/ diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index 59b4488fe1..012044859d 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -577,7 +577,7 @@ unsafe def elabEvalUnsafe : CommandElab := fun stx => do | Except.error e => throwError e.toString | Except.ok env => do setEnv env; pure () let elabEval : CommandElabM Unit := runTermElabM (some n) fun _ => do - -- fall back to non-meta eval if MetaHasEval hasn't been defined yet + -- fall back to non-meta eval if MetaEval hasn't been defined yet -- modify e to `runEval e` let e ← Term.elabTerm term none let e := mkSimpleThunk e @@ -590,7 +590,7 @@ unsafe def elabEvalUnsafe : CommandElab := fun stx => do match res with | Except.error e => throwError e.toString | Except.ok _ => pure () - if (← getEnv).contains `Lean.MetaHasEval then do + if (← getEnv).contains `Lean.MetaEval then do elabMetaEval else elabEval diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean index 688e97d51a..d3bca52f8a 100644 --- a/src/Lean/Elab/Do.lean +++ b/src/Lean/Elab/Do.lean @@ -55,7 +55,7 @@ private def extractBind (expectedType? : Option Expr) : TermElabM ExtractMonadRe match type with | Expr.app m α _ => try - let bindInstType ← mkAppM `HasBind #[m] + let bindInstType ← mkAppM `Bind #[m] let bindInstVal ← synthesizeInst bindInstType pure { m := m, hasBindInst := bindInstVal, α := α } catch _ => @@ -319,7 +319,7 @@ partial def pullExitPointsAux : NameSet → Code → StateRefT (Array JPDecl) Te -- We use `mkAuxDeclFor` because `e` is not pure. mkAuxDeclFor e fun y => let ref := e - mkJmp ref rs y (fun yFresh => do pure $ Code.action (← `(HasPure.pure $yFresh))) + mkJmp ref rs y (fun yFresh => do pure $ Code.action (← `(Pure.pure $yFresh))) /- Auxiliary operation for adding new variables to the collection of updated variables in a CodeBlock. @@ -485,7 +485,7 @@ private def mkUnit (ref : Syntax) : MacroM Syntax := do private def mkPureUnit (ref : Syntax) : MacroM Syntax := do let unit ← mkUnit ref - let pureUnit ← `(HasPure.pure $(unit.copyInfo ref)) + let pureUnit ← `(Pure.pure $(unit.copyInfo ref)) pure $ pureUnit.copyInfo ref def mkPureUnitAction (ref : Syntax) : MacroM CodeBlock := do @@ -672,7 +672,7 @@ We use `MProd` instead of `Prod` to group values when expanding the The motivation is to generate simpler universe constraints in code that was not written by the user. Note that we are not restricting the macro power since the -`HasBind.bind` combinator already forces values computed by monadic +`Bind.bind` combinator already forces values computed by monadic actions to be in the same universe. -/ private def mkTuple (ref : Syntax) (elems : Array Syntax) : MacroM Syntax := do @@ -808,13 +808,13 @@ def returnToTermCore (ref : Syntax) (val : Syntax) : M Syntax := do let ctx ← read let u ← mkUVarTuple ref match ctx.kind with - | Kind.regular => if ctx.uvars.isEmpty then `(HasPure.pure $val) else `(HasPure.pure (MProd.mk $val $u)) - | Kind.forIn => `(HasPure.pure (ForInStep.done $u)) - | Kind.forInWithReturn => `(HasPure.pure (ForInStep.done (MProd.mk (some $val) $u))) + | Kind.regular => if ctx.uvars.isEmpty then `(Pure.pure $val) else `(Pure.pure (MProd.mk $val $u)) + | Kind.forIn => `(Pure.pure (ForInStep.done $u)) + | Kind.forInWithReturn => `(Pure.pure (ForInStep.done (MProd.mk (some $val) $u))) | Kind.nestedBC => unreachable! - | Kind.nestedPR => `(HasPure.pure (DoResultPR.«return» $val $u)) - | Kind.nestedSBC => `(HasPure.pure (DoResultSBC.«pureReturn» $val $u)) - | Kind.nestedPRBC => `(HasPure.pure (DoResultPRBC.«return» $val $u)) + | Kind.nestedPR => `(Pure.pure (DoResultPR.«return» $val $u)) + | Kind.nestedSBC => `(Pure.pure (DoResultSBC.«pureReturn» $val $u)) + | Kind.nestedPRBC => `(Pure.pure (DoResultPRBC.«return» $val $u)) def returnToTerm (ref : Syntax) (val : Syntax) : M Syntax := do let r ← returnToTermCore ref val @@ -825,12 +825,12 @@ def continueToTermCore (ref : Syntax) : M Syntax := do let u ← mkUVarTuple ref match ctx.kind with | Kind.regular => unreachable! - | Kind.forIn => `(HasPure.pure (ForInStep.yield $u)) - | Kind.forInWithReturn => `(HasPure.pure (ForInStep.yield (MProd.mk none $u))) - | Kind.nestedBC => `(HasPure.pure (DoResultBC.«continue» $u)) + | Kind.forIn => `(Pure.pure (ForInStep.yield $u)) + | Kind.forInWithReturn => `(Pure.pure (ForInStep.yield (MProd.mk none $u))) + | Kind.nestedBC => `(Pure.pure (DoResultBC.«continue» $u)) | Kind.nestedPR => unreachable! - | Kind.nestedSBC => `(HasPure.pure (DoResultSBC.«continue» $u)) - | Kind.nestedPRBC => `(HasPure.pure (DoResultPRBC.«continue» $u)) + | Kind.nestedSBC => `(Pure.pure (DoResultSBC.«continue» $u)) + | Kind.nestedPRBC => `(Pure.pure (DoResultPRBC.«continue» $u)) def continueToTerm (ref : Syntax) : M Syntax := do let r ← continueToTermCore ref @@ -841,12 +841,12 @@ def breakToTermCore (ref : Syntax) : M Syntax := do let u ← mkUVarTuple ref match ctx.kind with | Kind.regular => unreachable! - | Kind.forIn => `(HasPure.pure (ForInStep.done $u)) - | Kind.forInWithReturn => `(HasPure.pure (ForInStep.done (MProd.mk none $u))) - | Kind.nestedBC => `(HasPure.pure (DoResultBC.«break» $u)) + | Kind.forIn => `(Pure.pure (ForInStep.done $u)) + | Kind.forInWithReturn => `(Pure.pure (ForInStep.done (MProd.mk none $u))) + | Kind.nestedBC => `(Pure.pure (DoResultBC.«break» $u)) | Kind.nestedPR => unreachable! - | Kind.nestedSBC => `(HasPure.pure (DoResultSBC.«break» $u)) - | Kind.nestedPRBC => `(HasPure.pure (DoResultPRBC.«break» $u)) + | Kind.nestedSBC => `(Pure.pure (DoResultSBC.«break» $u)) + | Kind.nestedPRBC => `(Pure.pure (DoResultPRBC.«break» $u)) def breakToTerm (ref : Syntax) : M Syntax := do let r ← breakToTermCore ref @@ -857,13 +857,13 @@ def actionTerminalToTermCore (action : Syntax) : M Syntax := withFreshMacroScope let ctx ← read let u ← mkUVarTuple ref match ctx.kind with - | Kind.regular => if ctx.uvars.isEmpty then pure action else `(HasBind.bind $action fun y => HasPure.pure (MProd.mk y $u)) - | Kind.forIn => `(HasBind.bind $action fun (_ : PUnit) => HasPure.pure (ForInStep.yield $u)) - | Kind.forInWithReturn => `(HasBind.bind $action fun (_ : PUnit) => HasPure.pure (ForInStep.yield (MProd.mk none $u))) + | Kind.regular => if ctx.uvars.isEmpty then pure action else `(Bind.bind $action fun y => Pure.pure (MProd.mk y $u)) + | Kind.forIn => `(Bind.bind $action fun (_ : PUnit) => Pure.pure (ForInStep.yield $u)) + | Kind.forInWithReturn => `(Bind.bind $action fun (_ : PUnit) => Pure.pure (ForInStep.yield (MProd.mk none $u))) | Kind.nestedBC => unreachable! - | Kind.nestedPR => `(HasBind.bind $action fun y => (HasPure.pure (DoResultPR.«pure» y $u))) - | Kind.nestedSBC => `(HasBind.bind $action fun y => (HasPure.pure (DoResultSBC.«pureReturn» y $u))) - | Kind.nestedPRBC => `(HasBind.bind $action fun y => (HasPure.pure (DoResultPRBC.«pure» y $u))) + | Kind.nestedPR => `(Bind.bind $action fun y => (Pure.pure (DoResultPR.«pure» y $u))) + | Kind.nestedSBC => `(Bind.bind $action fun y => (Pure.pure (DoResultSBC.«pureReturn» y $u))) + | Kind.nestedPRBC => `(Bind.bind $action fun y => (Pure.pure (DoResultPRBC.«pure» y $u))) def actionTerminalToTerm (action : Syntax) : M Syntax := do let ref := action @@ -878,7 +878,7 @@ def seqToTermCore (action : Syntax) (k : Syntax) : MacroM Syntax := withFreshMac let cond := action[1] `(assert! $cond; $k) else - `(HasBind.bind $action (fun _ => $k)) + `(Bind.bind $action (fun _ => $k)) def seqToTerm (action : Syntax) (k : Syntax) : MacroM Syntax := do let r ← seqToTermCore action k @@ -902,7 +902,7 @@ def declToTermCore (decl : Syntax) (k : Syntax) : M Syntax := withFreshMacroScop let doElem := arg[3] -- `doElem` must be a `doExpr action`. See `doLetArrowToCode` match isDoExpr? doElem with - | some action => `(HasBind.bind $action (fun ($id:ident : $type) => $k)) + | some action => `(Bind.bind $action (fun ($id:ident : $type) => $k)) | none => Macro.throwError decl "unexpected kind of 'do' declaration" else Macro.throwError decl "unexpected kind of 'do' declaration" @@ -1287,7 +1287,7 @@ def doForToCode (doSeqToCode : List Syntax → M CodeBlock) (doFor : Syntax) (do let auxDo ← `(do let r ← $forInTerm:term; $uvarsTuple:term := r.2; match r.1 with - | none => HasPure.pure (ensureExpectedType! "type mismatch, 'for'" PUnit.unit) + | none => Pure.pure (ensureExpectedType! "type mismatch, 'for'" PUnit.unit) | some a => return ensureExpectedType! "type mismatch, 'for'" a) doSeqToCode (getDoSeqElems (getDoSeq auxDo) ++ doElems) else @@ -1295,7 +1295,7 @@ def doForToCode (doSeqToCode : List Syntax → M CodeBlock) (doFor : Syntax) (do if doElems.isEmpty then let auxDo ← `(do let r ← $forInTerm:term; $uvarsTuple:term := r; - HasPure.pure (ensureExpectedType! "type mismatch, 'for'" PUnit.unit)) + Pure.pure (ensureExpectedType! "type mismatch, 'for'" PUnit.unit)) doSeqToCode $ getDoSeqElems (getDoSeq auxDo) else let auxDo ← `(do let r ← $forInTerm:term; $uvarsTuple:term := r) diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean index 65eea3e84c..cf9f98b116 100644 --- a/src/Lean/Elab/Quotation.lean +++ b/src/Lean/Elab/Quotation.lean @@ -101,7 +101,7 @@ def stxQuot.expand (stx : Syntax) : TermElabM Syntax := do including it literally in a syntax quotation. -/ -- TODO: simplify to `(do scp ← getCurrMacroScope; pure $(quoteSyntax quoted)) stx ← quoteSyntax (elimAntiquotChoices quoted); - `(bind getCurrMacroScope (fun scp => bind getMainModule (fun mainModule => pure $stx))) + `(Bind.bind getCurrMacroScope (fun scp => Bind.bind getMainModule (fun mainModule => Pure.pure $stx))) /- NOTE: It may seem like the newly introduced binding `scp` may accidentally capture identifiers in an antiquotation introduced by `quoteSyntax`. However, note that the syntax quotation above enjoys the same hygiene guarantees as diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 86dfc5a8c9..5ae33ae098 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -660,7 +660,7 @@ def synthesizeInst (type : Expr) : TermElabM Expr := do ``` def f (x : Bool) : IO Nat := do IO.prinln x - x + x -- Error: failed to synthesize `HasAdd (IO Nat)` + x + x -- Error: failed to synthesize `Add (IO Nat)` ``` -/ private def tryPureCoe? (errorMsgHeader? : Option String) (m β α a : Expr) : TermElabM (Option Expr) := do @@ -729,10 +729,10 @@ Let's assume there is no other occurrence of `v` in `h`. Thus, we have that the expected of `g x` is `StateT Nat IO ?α`, and the given type is `IO Nat`. So, even if we add a coercion. ``` -instance {α m n} [HasLiftT m n] {α} : Coe (m α) (n α) := ... +instance {α m n} [MonadLiftT m n] {α} : Coe (m α) (n α) := ... ``` It is not applicable because TC would have to assign `?α := Nat`. -On the other hand, TC can easily solve `[HasLiftT IO (StateT Nat IO)]` +On the other hand, TC can easily solve `[MonadLiftT IO (StateT Nat IO)]` since this goal does not contain any metavariables. And then, we convert `g x` into `liftM $ g x`. -/ @@ -1226,8 +1226,8 @@ def resolveName (n : Name) (preresolved : List (Name × List String)) (explicitL | _ => pure () let u ← getLevel typeMVar let u ← decLevel u - let mvar ← mkInstMVar (mkApp (Lean.mkConst `HasOfNat [u]) typeMVar) - pure $ mkApp3 (Lean.mkConst `HasOfNat.ofNat [u]) typeMVar mvar val + let mvar ← mkInstMVar (mkApp (Lean.mkConst `OfNat [u]) typeMVar) + pure $ mkApp3 (Lean.mkConst `OfNat.ofNat [u]) typeMVar mvar val @[builtinTermElab charLit] def elabCharLit : TermElab := fun stx _ => do match stx.isCharLit? with diff --git a/src/Lean/Meta/AppBuilder.lean b/src/Lean/Meta/AppBuilder.lean index c33300b85f..638f0d4c8c 100644 --- a/src/Lean/Meta/AppBuilder.lean +++ b/src/Lean/Meta/AppBuilder.lean @@ -270,14 +270,14 @@ private partial def mkAppOptMAux (f : Expr) (xs : Array (Option Expr)) : Nat → /-- Similar to `mkAppM`, but it allows us to specify which arguments are provided explicitly using `Option` type. Example: - Given `HasPure.pure {m : Type u → Type v} [HasPure m] {α : Type u} (a : α) : m α`, + Given `Pure.pure {m : Type u → Type v} [HasPure m] {α : Type u} (a : α) : m α`, ``` - mkAppOptM `HasPure.pure #[m, none, none, a] + mkAppOptM `Pure.pure #[m, none, none, a] ``` - returns a `HasPure.pure` application if the instance `HasPure m` can be synthesized, and the universes match. + returns a `Pure.pure` application if the instance `HasPure m` can be synthesized, and the universes match. Note that, ``` - mkAppM `HasPure.pure #[a] + mkAppM `Pure.pure #[a] ``` fails because the only explicit argument `(a : α)` is not sufficient for inferring the remaining arguments, we would need the expected type. -/ @@ -338,7 +338,7 @@ def mkNoConfusion (target : Expr) (h : Expr) : m Expr := liftMetaM $ mkNoConfusionImp target h def mkPure (monad : Expr) (e : Expr) : m Expr := - mkAppOptM `HasPure.pure #[monad, none, none, e] + mkAppOptM `Pure.pure #[monad, none, none, e] /-- `mkProjection s fieldName` return an expression for accessing field `fieldName` of the structure `s`. @@ -410,11 +410,11 @@ def mkDecideProof (p : Expr) : m Expr := liftMetaM do /-- Return `a < b` -/ def mkLt (a b : Expr) : m Expr := - mkAppM `HasLess.Less #[a, b] + mkAppM `Less.Less #[a, b] /-- Return `a <= b` -/ def mkLe (a b : Expr) : m Expr := - mkAppM `HasLessEq.LessEq #[a, b] + mkAppM `LessEq.LessEq #[a, b] /-- Return `arbitrary α` -/ def mkArbitrary (α : Expr) : m Expr := diff --git a/src/Lean/Meta/DiscrTree.lean b/src/Lean/Meta/DiscrTree.lean index c11a9e1c9c..1180a56df3 100644 --- a/src/Lean/Meta/DiscrTree.lean +++ b/src/Lean/Meta/DiscrTree.lean @@ -29,18 +29,18 @@ namespace Lean.Meta.DiscrTree discrimination tree. Recall that projections from classes are **NOT** reducible. - For example, the expressions `HasAdd.add α (ringHasAdd ?α ?s) ?x ?x` - and `HasAdd.add Nat Nat.hasAdd a b` generates paths with the following keys + For example, the expressions `Add.add α (ringHasAdd ?α ?s) ?x ?x` + and `Add.add Nat Nat.hasAdd a b` generates paths with the following keys respctively ``` ⟨HasAdd.add, 4⟩, *, *, *, * ⟨HasAdd.add, 4⟩, *, *, ⟨a,0⟩, ⟨b,0⟩ ``` - That is, we don't reduce `HasAdd.add Nat Nat.HasAdd a b` into `Nat.add a b`. - We say the `HasAdd.add` applications are the de-facto canonical forms in + That is, we don't reduce `Add.add Nat inst a b` into `Nat.add a b`. + We say the `Add.add` applications are the de-facto canonical forms in the metaprogramming framework. Moreover, it is the metaprogrammer's responsibility to re-pack applications such as - `Nat.add a b` into `HasAdd.add Nat Nat.hasAdd a b`. + `Nat.add a b` into `Add.add Nat inst a b`. Remark: we store the arity in the keys 1- To be able to implement the "skip" operation when retrieving "candidate" @@ -151,7 +151,7 @@ private partial def whnfEta (e : Expr) : MetaM Expr := do Then, `DiscrTree` users may control which symbols should be treated as wildcards. Different `DiscrTree` users may populate this set using, for example, attributes. -/ private def shouldAddAsStar (constName : Name) : Bool := - constName == `Nat.zero || constName == `Nat.succ || constName == `Nat.add || constName == `HasAdd.add + constName == `Nat.zero || constName == `Nat.succ || constName == `Nat.add || constName == `Add.add private def pushArgs (todo : Array Expr) (e : Expr) : MetaM (Key × Array Expr) := do let e ← whnfEta e diff --git a/src/Lean/Meta/Offset.lean b/src/Lean/Meta/Offset.lean index f05418b918..a18348857d 100644 --- a/src/Lean/Meta/Offset.lean +++ b/src/Lean/Meta/Offset.lean @@ -32,19 +32,19 @@ partial def evalNat : Expr → Option Nat let v₁ ← evalNat (e.getArg! 0) let v₂ ← evalNat (e.getArg! 1) pure $ v₁ * v₂ - else if c == `HasAdd.add && nargs == 4 then + else if c == `Add.add && nargs == 4 then let v₁ ← evalNat (e.getArg! 2) let v₂ ← evalNat (e.getArg! 3) pure $ v₁ + v₂ - else if c == `HasAdd.sub && nargs == 4 then + else if c == `Sub.sub && nargs == 4 then let v₁ ← evalNat (e.getArg! 2) let v₂ ← evalNat (e.getArg! 3) pure $ v₁ - v₂ - else if c == `HasAdd.mul && nargs == 4 then + else if c == `Mul.mul && nargs == 4 then let v₁ ← evalNat (e.getArg! 2) let v₂ ← evalNat (e.getArg! 3) pure $ v₁ * v₂ - else if c == `HasOfNat.ofNat && nargs == 3 then + else if c == `OfNat.ofNat && nargs == 3 then evalNat (e.getArg! 2) else none @@ -65,7 +65,7 @@ private partial def getOffsetAux : Expr → Bool → Option (Expr × Nat) let v ← evalNat (e.getArg! 1) let (s, k) ← getOffsetAux (e.getArg! 0) false pure (s, k+v) - else if c == `HasAdd.add && nargs == 4 then do + else if c == `Add.add && nargs == 4 then do let v ← evalNat (e.getArg! 3) let (s, k) ← getOffsetAux (e.getArg! 2) false pure (s, k+v) @@ -82,7 +82,7 @@ private partial def isOffset : Expr → Option (Expr × Nat) match fn with | Expr.const c _ _ => let nargs := e.getAppNumArgs - if (c == `Nat.succ && nargs == 1) || (c == `Nat.add && nargs == 2) || (c == `HasAdd.add && nargs == 4) then + if (c == `Nat.succ && nargs == 1) || (c == `Nat.add && nargs == 2) || (c == `Add.add && nargs == 4) then getOffset e else none | _ => none diff --git a/src/Lean/Meta/ReduceEval.lean b/src/Lean/Meta/ReduceEval.lean index 61f6d117db..f32804644b 100644 --- a/src/Lean/Meta/ReduceEval.lean +++ b/src/Lean/Meta/ReduceEval.lean @@ -13,6 +13,9 @@ namespace Lean.Meta class HasReduceEval (α : Type) := (reduceEval : Expr → MetaM α) +class ReduceEval (α : Type) := + (reduceEval : Expr → MetaM α) + def reduceEval {α : Type} [HasReduceEval α] (e : Expr) : MetaM α := withAtLeastTransparency TransparencyMode.default $ HasReduceEval.reduceEval e