chore: prepare to rename
This commit is contained in:
Leonardo de Moura
parent
1fba699b2c
commit
97c93ec557
21 changed files with 150 additions and 84 deletions
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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⟩
|
||||
|
|
|
|||
|
|
@ -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 δ :=
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
|
|
|||
|
|
@ -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 _))
|
||||
|
|
|
|||
|
|
@ -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⟩
|
||||
|
|
|
|||
|
|
@ -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 ()))⟩
|
||||
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 :=
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
||||
|
|
|
|||
|
|
@ -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,
|
||||
|
|
|
|||
|
|
@ -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])))` -/
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 :=
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue