chore: cleanup and style
This commit is contained in:
Leonardo de Moura
parent
9333fb4cf6
commit
5249fdc24d
13 changed files with 161 additions and 207 deletions
|
|
@ -63,66 +63,52 @@ abbrev coeFun {α : Sort u} {γ : α → Sort v} (a : α) [CoeFun α γ] : γ a
|
|||
abbrev coeSort {α : Sort u} {β : Sort v} (a : α) [CoeSort α β] : β :=
|
||||
CoeSort.coe a
|
||||
|
||||
instance coeTrans {α : Sort u} {β : Sort v} {δ : Sort w} [CoeTC α β] [Coe β δ] : CoeTC α δ := {
|
||||
coe := fun a => coeB (coeTC a : β)
|
||||
}
|
||||
instance coeTrans {α : Sort u} {β : Sort v} {δ : Sort w} [CoeTC α β] [Coe β δ] : CoeTC α δ where
|
||||
coe a := coeB (coeTC a : β)
|
||||
|
||||
instance coeBase {α : Sort u} {β : Sort v} [Coe α β] : CoeTC α β := {
|
||||
coe := fun a => coeB a
|
||||
}
|
||||
instance coeBase {α : Sort u} {β : Sort v} [Coe α β] : CoeTC α β where
|
||||
coe a := coeB a
|
||||
|
||||
instance coeOfHeafOfTCOfTail {α : Sort u} {β : Sort v} {δ : Sort w} {γ : Sort w'} (a : α) [CoeTC β δ] [CoeTail δ γ] [CoeHead α β] : CoeT α a γ := {
|
||||
instance coeOfHeafOfTCOfTail {α : Sort u} {β : Sort v} {δ : Sort w} {γ : Sort w'} (a : α) [CoeTC β δ] [CoeTail δ γ] [CoeHead α β] : CoeT α a γ where
|
||||
coe := coeTail (coeTC (coeHead a : β) : δ)
|
||||
}
|
||||
|
||||
instance coeOfHeadOfTC {α : Sort u} {β : Sort v} {δ : Sort w} (a : α) [CoeTC β δ] [CoeHead α β] : CoeT α a δ := {
|
||||
instance coeOfHeadOfTC {α : Sort u} {β : Sort v} {δ : Sort w} (a : α) [CoeTC β δ] [CoeHead α β] : CoeT α a δ where
|
||||
coe := coeTC (coeHead a : β)
|
||||
}
|
||||
|
||||
instance coeOfTCOfTail {α : Sort u} {β : Sort v} {δ : Sort w} (a : α) [CoeTC α β] [CoeTail β δ] : CoeT α a δ := {
|
||||
instance coeOfTCOfTail {α : Sort u} {β : Sort v} {δ : Sort w} (a : α) [CoeTC α β] [CoeTail β δ] : CoeT α a δ where
|
||||
coe := coeTail (coeTC a : β)
|
||||
}
|
||||
|
||||
instance coeOfHead {α : Sort u} {β : Sort v} (a : α) [CoeHead α β] : CoeT α a β := {
|
||||
instance coeOfHead {α : Sort u} {β : Sort v} (a : α) [CoeHead α β] : CoeT α a β where
|
||||
coe := coeHead a
|
||||
}
|
||||
|
||||
instance coeOfTail {α : Sort u} {β : Sort v} (a : α) [CoeTail α β] : CoeT α a β := {
|
||||
instance coeOfTail {α : Sort u} {β : Sort v} (a : α) [CoeTail α β] : CoeT α a β where
|
||||
coe := coeTail a
|
||||
}
|
||||
|
||||
instance coeOfTC {α : Sort u} {β : Sort v} (a : α) [CoeTC α β] : CoeT α a β := {
|
||||
instance coeOfTC {α : Sort u} {β : Sort v} (a : α) [CoeTC α β] : CoeT α a β where
|
||||
coe := coeTC a
|
||||
}
|
||||
|
||||
instance coeOfDep {α : Sort u} {β : Sort v} (a : α) [CoeDep α a β] : CoeT α a β := {
|
||||
instance coeOfDep {α : Sort u} {β : Sort v} (a : α) [CoeDep α a β] : CoeT α a β where
|
||||
coe := coeD a
|
||||
}
|
||||
|
||||
instance coeId {α : Sort u} (a : α) : CoeT α a α := {
|
||||
instance coeId {α : Sort u} (a : α) : CoeT α a α where
|
||||
coe := a
|
||||
}
|
||||
|
||||
/- Basic instances -/
|
||||
|
||||
@[inline] instance boolToProp : Coe Bool Prop := {
|
||||
coe := fun b => b = true
|
||||
}
|
||||
@[inline] instance boolToProp : Coe Bool Prop where
|
||||
coe b := b = true
|
||||
|
||||
@[inline] instance coeDecidableEq (x : Bool) : Decidable (coe x) :=
|
||||
inferInstanceAs (Decidable (x = true))
|
||||
inferInstanceAs (Decidable (x = true))
|
||||
|
||||
instance decPropToBool (p : Prop) [Decidable p] : CoeDep Prop p Bool := {
|
||||
instance decPropToBool (p : Prop) [Decidable p] : CoeDep Prop p Bool where
|
||||
coe := decide p
|
||||
}
|
||||
|
||||
instance optionCoe {α : Type u} : CoeTail α (Option α) := {
|
||||
instance optionCoe {α : Type u} : CoeTail α (Option α) where
|
||||
coe := some
|
||||
}
|
||||
|
||||
instance subtypeCoe {α : Sort u} {p : α → Prop} : CoeHead { x // p x } α := {
|
||||
coe := fun v => v.val
|
||||
}
|
||||
instance subtypeCoe {α : Sort u} {p : α → Prop} : CoeHead { x // p x } α where
|
||||
coe v := v.val
|
||||
|
||||
/- Coe & OfNat bridge -/
|
||||
|
||||
|
|
|
|||
|
|
@ -47,7 +47,8 @@ class ToBool (α : Type u) where
|
|||
|
||||
export ToBool (toBool)
|
||||
|
||||
instance : ToBool Bool := ⟨id⟩
|
||||
instance : ToBool Bool where
|
||||
toBool b := b
|
||||
|
||||
@[macroInline] def bool {β : Type u} {α : Type v} [ToBool β] (f t : α) (b : β) : α :=
|
||||
match toBool b with
|
||||
|
|
@ -90,7 +91,6 @@ instance (m n o) [MonadControlT m n] [MonadControl n o] : MonadControlT m o wher
|
|||
liftWith f := MonadControl.liftWith fun x₂ => liftWith fun x₁ => f (x₁ ∘ x₂)
|
||||
restoreM := MonadControl.restoreM ∘ restoreM
|
||||
|
||||
|
||||
instance (m : Type u → Type v) [Pure m] : MonadControlT m m where
|
||||
stM α := α
|
||||
liftWith f := f fun x => x
|
||||
|
|
|
|||
|
|
@ -12,17 +12,15 @@ namespace EStateM
|
|||
|
||||
variables {ε σ α : Type u}
|
||||
|
||||
instance [ToString ε] [ToString α] : ToString (Result ε σ α) := {
|
||||
toString := fun
|
||||
instance [ToString ε] [ToString α] : ToString (Result ε σ α) where
|
||||
toString
|
||||
| Result.ok a _ => "ok: " ++ toString a
|
||||
| Result.error e _ => "error: " ++ toString e
|
||||
}
|
||||
|
||||
instance [Repr ε] [Repr α] : Repr (Result ε σ α) := {
|
||||
repr := fun
|
||||
instance [Repr ε] [Repr α] : Repr (Result ε σ α) where
|
||||
repr
|
||||
| Result.error e _ => "(error " ++ repr e ++ ")"
|
||||
| Result.ok a _ => "(ok " ++ repr a ++ ")"
|
||||
}
|
||||
|
||||
end EStateM
|
||||
|
||||
|
|
|
|||
|
|
@ -14,11 +14,10 @@ def Id (type : Type u) : Type u := type
|
|||
|
||||
namespace Id
|
||||
|
||||
instance : Monad Id := {
|
||||
pure := fun x => x
|
||||
bind := fun x f => f x
|
||||
map := fun f x => f x
|
||||
}
|
||||
instance : Monad Id where
|
||||
pure x := x
|
||||
bind x f := f x
|
||||
map f x := f x
|
||||
|
||||
@[inline] protected def run (x : Id α) : α := x
|
||||
|
||||
|
|
|
|||
|
|
@ -18,19 +18,16 @@ namespace ReaderT
|
|||
@[inline] protected def failure [Alternative m] : ReaderT ρ m α :=
|
||||
fun s => failure
|
||||
|
||||
instance [Monad m] [Alternative m] : Alternative (ReaderT ρ m) := {
|
||||
instance [Monad m] [Alternative m] : Alternative (ReaderT ρ m) where
|
||||
failure := ReaderT.failure
|
||||
orElse := ReaderT.orElse
|
||||
}
|
||||
|
||||
end ReaderT
|
||||
|
||||
instance : MonadControl m (ReaderT ρ m) := {
|
||||
instance : MonadControl m (ReaderT ρ m) where
|
||||
stM := id
|
||||
liftWith := fun f ctx => f fun x => x ctx
|
||||
restoreM := fun x ctx => x
|
||||
}
|
||||
liftWith f ctx := f fun x => x ctx
|
||||
restoreM x ctx := x
|
||||
|
||||
instance ReaderT.tryFinally [MonadFinally m] [Monad m] : MonadFinally (ReaderT ρ m) := {
|
||||
tryFinally' := fun x h ctx => tryFinally' (x ctx) (fun a? => h a? ctx)
|
||||
}
|
||||
instance ReaderT.tryFinally [MonadFinally m] [Monad m] : MonadFinally (ReaderT ρ m) where
|
||||
tryFinally' x h ctx := tryFinally' (x ctx) (fun a? => h a? ctx)
|
||||
|
|
|
|||
|
|
@ -8,24 +8,20 @@ import Init.Data.UInt
|
|||
import Init.Data.String
|
||||
universes u
|
||||
|
||||
instance : Hashable Nat := {
|
||||
hash := fun n => USize.ofNat n
|
||||
}
|
||||
instance : Hashable Nat where
|
||||
hash n := USize.ofNat n
|
||||
|
||||
instance [Hashable α] [Hashable β] : Hashable (α × β) := {
|
||||
hash := fun (a, b) => mixHash (hash a) (hash b)
|
||||
}
|
||||
instance [Hashable α] [Hashable β] : Hashable (α × β) where
|
||||
hash | (a, b) => mixHash (hash a) (hash b)
|
||||
|
||||
protected def Option.hash [Hashable α] : Option α → USize
|
||||
| none => 11
|
||||
| some a => mixHash (hash a) 13
|
||||
|
||||
instance [Hashable α] : Hashable (Option α) := {
|
||||
hash := fun
|
||||
instance [Hashable α] : Hashable (Option α) where
|
||||
hash
|
||||
| none => 11
|
||||
| some a => mixHash (hash a) 13
|
||||
}
|
||||
|
||||
instance [Hashable α] : Hashable (List α) := {
|
||||
hash := fun as => as.foldl (fun r a => mixHash r (hash a)) 7
|
||||
}
|
||||
instance [Hashable α] : Hashable (List α) where
|
||||
hash as := as.foldl (fun r a => mixHash r (hash a)) 7
|
||||
|
|
|
|||
|
|
@ -270,8 +270,8 @@ def mkSep (a : Array Syntax) (sep : Syntax) : Syntax :=
|
|||
def SepArray.ofElems {sep} (elems : Array Syntax) : SepArray sep :=
|
||||
⟨mkSepArray elems (mkAtom sep)⟩
|
||||
|
||||
instance (sep) : Coe (Array Syntax) (SepArray sep) :=
|
||||
⟨SepArray.ofElems⟩
|
||||
instance (sep) : Coe (Array Syntax) (SepArray sep) where
|
||||
coe := SepArray.ofElems
|
||||
|
||||
/-- Create syntax representing a Lean term application, but avoid degenerate empty applications. -/
|
||||
def mkApp (fn : Syntax) : (args : Array Syntax) → Syntax
|
||||
|
|
@ -613,23 +613,26 @@ private def quoteName : Name → Syntax
|
|||
|
||||
instance : Quote Name := ⟨quoteName⟩
|
||||
|
||||
instance {α β : Type} [Quote α] [Quote β] : Quote (α × β) :=
|
||||
⟨fun ⟨a, b⟩ => Syntax.mkCApp ``Prod.mk #[quote a, quote b]⟩
|
||||
instance {α β : Type} [Quote α] [Quote β] : Quote (α × β) where
|
||||
quote
|
||||
| ⟨a, b⟩ => Syntax.mkCApp ``Prod.mk #[quote a, quote b]
|
||||
|
||||
private def quoteList {α : Type} [Quote α] : List α → Syntax
|
||||
| [] => mkCIdent ``List.nil
|
||||
| (x::xs) => Syntax.mkCApp ``List.cons #[quote x, quoteList xs]
|
||||
|
||||
instance {α : Type} [Quote α] : Quote (List α) := ⟨quoteList⟩
|
||||
instance {α : Type} [Quote α] : Quote (List α) where
|
||||
quote := quoteList
|
||||
|
||||
instance {α : Type} [Quote α] : Quote (Array α) :=
|
||||
⟨fun xs => Syntax.mkCApp ``List.toArray #[quote xs.toList]⟩
|
||||
instance {α : Type} [Quote α] : Quote (Array α) where
|
||||
quote xs := Syntax.mkCApp ``List.toArray #[quote xs.toList]
|
||||
|
||||
private def quoteOption {α : Type} [Quote α] : Option α → Syntax
|
||||
| none => mkIdent ``none
|
||||
| (some x) => Syntax.mkCApp ``some #[quote x]
|
||||
|
||||
instance Option.hasQuote {α : Type} [Quote α] : Quote (Option α) := ⟨quoteOption⟩
|
||||
instance Option.hasQuote {α : Type} [Quote α] : Quote (Option α) where
|
||||
quote := quoteOption
|
||||
|
||||
end Lean
|
||||
|
||||
|
|
@ -684,10 +687,10 @@ end Array
|
|||
namespace Lean.Syntax.SepArray
|
||||
|
||||
def getElems {sep} (sa : SepArray sep) : Array Syntax :=
|
||||
sa.elemsAndSeps.getSepElems
|
||||
sa.elemsAndSeps.getSepElems
|
||||
|
||||
instance (sep) : Coe (SepArray sep) (Array Syntax) :=
|
||||
⟨getElems⟩
|
||||
instance (sep) : Coe (SepArray sep) (Array Syntax) where
|
||||
coe := getElems
|
||||
|
||||
end Lean.Syntax.SepArray
|
||||
|
||||
|
|
|
|||
|
|
@ -172,10 +172,9 @@ def sizeofMeasure (α : Sort u) [SizeOf α] : α → α → Prop :=
|
|||
def sizeofMeasureWf (α : Sort u) [SizeOf α] : WellFounded (sizeofMeasure α) :=
|
||||
measureWf sizeOf
|
||||
|
||||
instance hasWellFoundedOfSizeOf (α : Sort u) [SizeOf α] : WellFoundedRelation α := {
|
||||
r := sizeofMeasure α,
|
||||
instance hasWellFoundedOfSizeOf (α : Sort u) [SizeOf α] : WellFoundedRelation α where
|
||||
r := sizeofMeasure α
|
||||
wf := sizeofMeasureWf α
|
||||
}
|
||||
|
||||
namespace Prod
|
||||
open WellFounded
|
||||
|
|
@ -228,10 +227,9 @@ def rprodWf (ha : WellFounded ra) (hb : WellFounded rb) : WellFounded (Rprod ra
|
|||
|
||||
end
|
||||
|
||||
instance {α : Type u} {β : Type v} [s₁ : WellFoundedRelation α] [s₂ : WellFoundedRelation β] : WellFoundedRelation (α × β) := {
|
||||
r := Lex s₁.r s₂.r,
|
||||
instance {α : Type u} {β : Type v} [s₁ : WellFoundedRelation α] [s₂ : WellFoundedRelation β] : WellFoundedRelation (α × β) where
|
||||
r := Lex s₁.r s₂.r
|
||||
wf := lexWf s₁.wf s₂.wf
|
||||
}
|
||||
|
||||
end Prod
|
||||
|
||||
|
|
@ -274,7 +272,7 @@ def lexNdep (r : α → α → Prop) (s : β → β → Prop) :=
|
|||
Lex r (fun a => s)
|
||||
|
||||
def lexNdepWf {r : α → α → Prop} {s : β → β → Prop} (ha : WellFounded r) (hb : WellFounded s) : WellFounded (lexNdep r s) :=
|
||||
WellFounded.intro fun ⟨a, b⟩ => lexAccessible (WellFounded.apply ha a) (fun x => hb) b
|
||||
WellFounded.intro fun ⟨a, b⟩ => lexAccessible (WellFounded.apply ha a) (fun x => hb) b
|
||||
end
|
||||
|
||||
section
|
||||
|
|
@ -318,9 +316,8 @@ def mkSkipLeft {α : Type u} {β : Type v} {b₁ b₂ : β} {s : β → β → P
|
|||
RevLex.right _ _ h
|
||||
end
|
||||
|
||||
instance WellFoundedRelation {α : Type u} {β : α → Type v} [s₁ : WellFoundedRelation α] [s₂ : ∀ a, WellFoundedRelation (β a)] : WellFoundedRelation (PSigma β) := {
|
||||
r := Lex s₁.r (fun a => (s₂ a).r),
|
||||
instance WellFoundedRelation {α : Type u} {β : α → Type v} [s₁ : WellFoundedRelation α] [s₂ : ∀ a, WellFoundedRelation (β a)] : WellFoundedRelation (PSigma β) where
|
||||
r := Lex s₁.r (fun a => (s₂ a).r)
|
||||
wf := lexWf s₁.wf (fun a => (s₂ a).wf)
|
||||
}
|
||||
|
||||
end PSigma
|
||||
|
|
|
|||
|
|
@ -35,51 +35,44 @@ abbrev CoreM := ReaderT Context $ StateRefT State (EIO Exception)
|
|||
|
||||
instance : Inhabited (CoreM α) := ⟨fun _ _ => throw arbitrary⟩
|
||||
|
||||
instance : MonadRef CoreM := {
|
||||
getRef := do let ctx ← read; pure ctx.ref,
|
||||
withRef := fun ref x => withReader (fun ctx => { ctx with ref := ref }) x
|
||||
}
|
||||
instance : MonadRef CoreM where
|
||||
getRef := return (← read).ref
|
||||
withRef ref x := withReader (fun ctx => { ctx with ref := ref }) x
|
||||
|
||||
instance : MonadEnv CoreM := {
|
||||
getEnv := do pure (← get).env,
|
||||
modifyEnv := fun f => modify fun s => { s with env := f s.env }
|
||||
}
|
||||
|
||||
instance : MonadOptions CoreM := {
|
||||
getOptions := do pure (← read).options
|
||||
}
|
||||
instance : MonadEnv CoreM where
|
||||
getEnv := return (← get).env
|
||||
modifyEnv f := modify fun s => { s with env := f s.env }
|
||||
|
||||
instance : AddMessageContext CoreM := {
|
||||
instance : MonadOptions CoreM where
|
||||
getOptions := return (← read).options
|
||||
|
||||
instance : AddMessageContext CoreM where
|
||||
addMessageContext := addMessageContextPartial
|
||||
}
|
||||
|
||||
instance : MonadNameGenerator CoreM := {
|
||||
getNGen := do pure (← get).ngen,
|
||||
setNGen := fun ngen => modify fun s => { s with ngen := ngen } }
|
||||
instance : MonadNameGenerator CoreM where
|
||||
getNGen := return (← get).ngen
|
||||
setNGen ngen := modify fun s => { s with ngen := ngen }
|
||||
|
||||
instance : MonadRecDepth CoreM := {
|
||||
withRecDepth := fun d x => withReader (fun ctx => { ctx with currRecDepth := d }) x,
|
||||
getRecDepth := do pure (← read).currRecDepth,
|
||||
getMaxRecDepth := do pure (← read).maxRecDepth
|
||||
}
|
||||
instance : MonadRecDepth CoreM where
|
||||
withRecDepth d x := withReader (fun ctx => { ctx with currRecDepth := d }) x
|
||||
getRecDepth := return (← read).currRecDepth
|
||||
getMaxRecDepth := return (← read).maxRecDepth
|
||||
|
||||
instance : MonadResolveName CoreM := {
|
||||
getCurrNamespace := do pure (← read).currNamespace,
|
||||
getOpenDecls := do pure (← read).openDecls
|
||||
}
|
||||
instance : MonadResolveName CoreM where
|
||||
getCurrNamespace := return (← read).currNamespace
|
||||
getOpenDecls := return (← read).openDecls
|
||||
|
||||
@[inline] def liftIOCore (x : IO α) : CoreM α := do
|
||||
let ref ← getRef
|
||||
IO.toEIO (fun (err : IO.Error) => Exception.error ref (toString err)) x
|
||||
|
||||
instance : MonadLift IO CoreM := {
|
||||
instance : MonadLift IO CoreM where
|
||||
monadLift := liftIOCore
|
||||
}
|
||||
|
||||
instance : MonadTrace CoreM := {
|
||||
getTraceState := do pure (← get).traceState,
|
||||
modifyTraceState := fun f => modify fun s => { s with traceState := f s.traceState }
|
||||
}
|
||||
instance : MonadTrace CoreM where
|
||||
getTraceState := return (← get).traceState
|
||||
modifyTraceState f := modify fun s => { s with traceState := f s.traceState }
|
||||
|
||||
private def mkFreshNameImp (n : Name) : CoreM Name := do
|
||||
let fresh ← modifyGet fun s => (s.nextMacroScope, { s with nextMacroScope := s.nextMacroScope + 1 })
|
||||
|
|
@ -101,12 +94,11 @@ def mkFreshUserName [MonadLiftT CoreM m] (n : Name) : m Name :=
|
|||
| Except.error (Exception.internal id _) => throw $ IO.userError $ "internal exception #" ++ toString id.idx
|
||||
| Except.ok a => pure a
|
||||
|
||||
instance [MetaEval α] : MetaEval (CoreM α) := {
|
||||
eval := fun env opts x _ => do
|
||||
instance [MetaEval α] : MetaEval (CoreM α) where
|
||||
eval env opts x _ := do
|
||||
let x : CoreM α := do try x finally printTraces
|
||||
let (a, s) ← x.toIO { maxRecDepth := getMaxRecDepth opts, options := opts } { env := env }
|
||||
MetaEval.eval s.env opts a (hideUnit := true)
|
||||
}
|
||||
|
||||
-- withIncRecDepth for a monad `m` such that `[MonadControlT CoreM n]`
|
||||
protected def withIncRecDepth [Monad m] [MonadControlT CoreM m] (x : m α) : m α :=
|
||||
|
|
|
|||
|
|
@ -36,9 +36,9 @@ structure State where
|
|||
instance : Inhabited State := ⟨{ env := arbitrary, maxRecDepth := 0 }⟩
|
||||
|
||||
def mkState (env : Environment) (messages : MessageLog := {}) (opts : Options := {}) : State := {
|
||||
env := env,
|
||||
messages := messages,
|
||||
scopes := [{ header := "", opts := opts }],
|
||||
env := env
|
||||
messages := messages
|
||||
scopes := [{ header := "", opts := opts }]
|
||||
maxRecDepth := getMaxRecDepth opts
|
||||
}
|
||||
|
||||
|
|
@ -61,38 +61,33 @@ abbrev Linter := Syntax → CommandElabM Unit
|
|||
builtin_initialize lintersRef : IO.Ref (Array Linter) ← IO.mkRef #[]
|
||||
|
||||
def addLinter (l : Linter) : IO Unit := do
|
||||
let ls ← lintersRef.get
|
||||
lintersRef.set (ls.push l)
|
||||
let ls ← lintersRef.get
|
||||
lintersRef.set (ls.push l)
|
||||
|
||||
instance : MonadEnv CommandElabM := {
|
||||
getEnv := do pure (← get).env,
|
||||
modifyEnv := fun f => modify fun s => { s with env := f s.env }
|
||||
}
|
||||
instance : MonadEnv CommandElabM where
|
||||
getEnv := do pure (← get).env
|
||||
modifyEnv f := modify fun s => { s with env := f s.env }
|
||||
|
||||
instance : MonadOptions CommandElabM := {
|
||||
instance : MonadOptions CommandElabM where
|
||||
getOptions := do pure (← get).scopes.head!.opts
|
||||
}
|
||||
|
||||
protected def getRef : CommandElabM Syntax := do
|
||||
pure (← read).ref
|
||||
protected def getRef : CommandElabM Syntax :=
|
||||
return (← read).ref
|
||||
|
||||
instance : AddMessageContext CommandElabM := {
|
||||
instance : AddMessageContext CommandElabM where
|
||||
addMessageContext := addMessageContextPartial
|
||||
}
|
||||
|
||||
instance : MonadRef CommandElabM := {
|
||||
getRef := Command.getRef,
|
||||
withRef := fun ref x => withReader (fun ctx => { ctx with ref := ref }) x
|
||||
}
|
||||
instance : MonadRef CommandElabM where
|
||||
getRef := Command.getRef
|
||||
withRef ref x := withReader (fun ctx => { ctx with ref := ref }) x
|
||||
|
||||
instance : AddErrorMessageContext CommandElabM := {
|
||||
add := fun ref msg => do
|
||||
instance : AddErrorMessageContext CommandElabM where
|
||||
add ref msg := do
|
||||
let ctx ← read
|
||||
let ref := getBetterRef ref ctx.macroStack
|
||||
let msg ← addMessageContext msg
|
||||
let msg ← addMacroStack msg ctx.macroStack
|
||||
pure (ref, msg)
|
||||
}
|
||||
return (ref, msg)
|
||||
|
||||
def mkMessageAux (ctx : Context) (ref : Syntax) (msgData : MessageData) (severity : MessageSeverity) : Message :=
|
||||
mkMessageCore ctx.fileName ctx.fileMap msgData severity (ref.getPos.getD ctx.cmdPos)
|
||||
|
|
@ -132,21 +127,19 @@ instance : MonadLiftT IO CommandElabM := { monadLift := liftIO }
|
|||
|
||||
def getScope : CommandElabM Scope := do pure (← get).scopes.head!
|
||||
|
||||
instance : MonadResolveName CommandElabM := {
|
||||
getCurrNamespace := do pure (← getScope).currNamespace,
|
||||
getOpenDecls := do pure (← getScope).openDecls
|
||||
}
|
||||
instance : MonadResolveName CommandElabM where
|
||||
getCurrNamespace := return (← getScope).currNamespace
|
||||
getOpenDecls := return (← getScope).openDecls
|
||||
|
||||
instance : MonadLog CommandElabM := {
|
||||
getRef := getRef,
|
||||
getFileMap := do pure (← read).fileMap,
|
||||
getFileName := do pure (← read).fileName,
|
||||
logMessage := fun msg => do
|
||||
instance : MonadLog CommandElabM where
|
||||
getRef := getRef
|
||||
getFileMap := return (← read).fileMap
|
||||
getFileName := return (← read).fileName
|
||||
logMessage msg := do
|
||||
let currNamespace ← getCurrNamespace
|
||||
let openDecls ← getOpenDecls
|
||||
let msg := { msg with data := MessageData.withNamingContext { currNamespace := currNamespace, openDecls := openDecls } msg.data }
|
||||
modify fun s => { s with messages := s.messages.add msg }
|
||||
}
|
||||
|
||||
def runLinters (stx : Syntax) : CommandElabM Unit := do
|
||||
let linters ← lintersRef.get
|
||||
|
|
@ -167,11 +160,10 @@ protected def getMainModule : CommandElabM Name := do pure (← getEnv).main
|
|||
let fresh ← modifyGet (fun st => (st.nextMacroScope, { st with nextMacroScope := st.nextMacroScope + 1 }))
|
||||
withReader (fun ctx => { ctx with currMacroScope := fresh }) x
|
||||
|
||||
instance : MonadQuotation CommandElabM := {
|
||||
getCurrMacroScope := Command.getCurrMacroScope,
|
||||
getMainModule := Command.getMainModule,
|
||||
instance : MonadQuotation CommandElabM where
|
||||
getCurrMacroScope := Command.getCurrMacroScope
|
||||
getMainModule := Command.getMainModule
|
||||
withFreshMacroScope := Command.withFreshMacroScope
|
||||
}
|
||||
|
||||
unsafe def mkCommandElabAttributeUnsafe : IO (KeyedDeclsAttribute CommandElab) :=
|
||||
mkElabAttribute CommandElab `Lean.Elab.Command.commandElabAttribute `builtinCommandElab `commandElab `Lean.Parser.Command `Lean.Elab.Command.CommandElab "command"
|
||||
|
|
@ -192,17 +184,15 @@ private def elabCommandUsing (s : State) (stx : Syntax) : List CommandElab → C
|
|||
@[inline] def withMacroExpansion {α} (beforeStx afterStx : Syntax) (x : CommandElabM α) : CommandElabM α :=
|
||||
withReader (fun ctx => { ctx with macroStack := { before := beforeStx, after := afterStx } :: ctx.macroStack }) x
|
||||
|
||||
instance : MonadMacroAdapter CommandElabM := {
|
||||
getCurrMacroScope := getCurrMacroScope,
|
||||
getNextMacroScope := do pure (← get).nextMacroScope,
|
||||
setNextMacroScope := fun next => modify fun s => { s with nextMacroScope := next }
|
||||
}
|
||||
instance : MonadMacroAdapter CommandElabM where
|
||||
getCurrMacroScope := getCurrMacroScope
|
||||
getNextMacroScope := return (← get).nextMacroScope
|
||||
setNextMacroScope next := modify fun s => { s with nextMacroScope := next }
|
||||
|
||||
instance : MonadRecDepth CommandElabM := {
|
||||
withRecDepth := fun d x => withReader (fun ctx => { ctx with currRecDepth := d }) x,
|
||||
getRecDepth := return (← read).currRecDepth,
|
||||
instance : MonadRecDepth CommandElabM where
|
||||
withRecDepth d x := withReader (fun ctx => { ctx with currRecDepth := d }) x
|
||||
getRecDepth := return (← read).currRecDepth
|
||||
getMaxRecDepth := return (← get).maxRecDepth
|
||||
}
|
||||
|
||||
@[inline] def withLogging (x : CommandElabM Unit) : CommandElabM Unit :=
|
||||
try
|
||||
|
|
@ -219,7 +209,7 @@ instance : MonadRecDepth CommandElabM := {
|
|||
builtin_initialize registerTraceClass `Elab.command
|
||||
|
||||
partial def elabCommand (stx : Syntax) : CommandElabM Unit :=
|
||||
withLogging $ withRef stx $ withIncRecDepth $ withFreshMacroScope do
|
||||
withLogging <| withRef stx <| withIncRecDepth <| withFreshMacroScope do
|
||||
runLinters stx
|
||||
match stx with
|
||||
| Syntax.node k args =>
|
||||
|
|
@ -258,11 +248,11 @@ private def mkMetaContext : Meta.Context := {
|
|||
}
|
||||
|
||||
private def mkTermContext (ctx : Context) (s : State) (declName? : Option Name) : Term.Context :=
|
||||
let scope := s.scopes.head!;
|
||||
{ macroStack := ctx.macroStack,
|
||||
fileName := ctx.fileName,
|
||||
fileMap := ctx.fileMap,
|
||||
currMacroScope := ctx.currMacroScope,
|
||||
let scope := s.scopes.head!
|
||||
{ macroStack := ctx.macroStack
|
||||
fileName := ctx.fileName
|
||||
fileMap := ctx.fileMap
|
||||
currMacroScope := ctx.currMacroScope
|
||||
declName? := declName? }
|
||||
|
||||
private def addTraceAsMessages (ctx : Context) (log : MessageLog) (traceState : TraceState) : MessageLog :=
|
||||
|
|
@ -285,9 +275,9 @@ def liftTermElabM {α} (declName? : Option Name) (x : TermElabM α) : CommandEla
|
|||
let x : EIO _ _ := x.run (mkCoreContext ctx s) { env := s.env, ngen := s.ngen, nextMacroScope := s.nextMacroScope }
|
||||
let (((ea, termS), _), coreS) ← liftEIO x
|
||||
modify fun s => { s with
|
||||
env := coreS.env,
|
||||
messages := addTraceAsMessages ctx (messages ++ termS.messages) coreS.traceState,
|
||||
nextMacroScope := coreS.nextMacroScope,
|
||||
env := coreS.env
|
||||
messages := addTraceAsMessages ctx (messages ++ termS.messages) coreS.traceState
|
||||
nextMacroScope := coreS.nextMacroScope
|
||||
ngen := coreS.ngen
|
||||
}
|
||||
match ea with
|
||||
|
|
@ -472,7 +462,7 @@ def elabOpenOnly (n : SyntaxNode) : CommandElabM Unit := do
|
|||
if env.contains declName then
|
||||
addOpenDecl (OpenDecl.explicit id declName)
|
||||
else
|
||||
withRef idStx $ logUnknownDecl declName
|
||||
withRef idStx do logUnknownDecl declName
|
||||
|
||||
-- `open` id `hiding` id+
|
||||
def elabOpenHiding (n : SyntaxNode) : CommandElabM Unit := do
|
||||
|
|
@ -480,13 +470,13 @@ def elabOpenHiding (n : SyntaxNode) : CommandElabM Unit := do
|
|||
let ns ← resolveNamespace ns
|
||||
let idsStx := n.getArg 2
|
||||
let env ← getEnv
|
||||
let ids : List Name ← idsStx.foldArgsM (fun idStx ids => do
|
||||
let ids ← idsStx.foldArgsM (fun idStx ids => do
|
||||
let id := idStx.getId
|
||||
let declName := ns ++ id
|
||||
if env.contains declName then
|
||||
pure (id::ids)
|
||||
else do
|
||||
withRef idStx $ logUnknownDecl declName
|
||||
withRef idStx do logUnknownDecl declName
|
||||
pure ids)
|
||||
[]
|
||||
addOpenDecl (OpenDecl.simple ns ids)
|
||||
|
|
@ -504,7 +494,7 @@ def elabOpenRenaming (n : SyntaxNode) : CommandElabM Unit := do
|
|||
if env.contains declName then
|
||||
addOpenDecl (OpenDecl.explicit toId declName)
|
||||
else
|
||||
withRef stx $ logUnknownDecl declName
|
||||
withRef stx do logUnknownDecl declName
|
||||
|
||||
@[builtinCommandElab «open»] def elabOpen : CommandElab := fun n => do
|
||||
let body := (n.getArg 1).asNode
|
||||
|
|
@ -538,7 +528,7 @@ open Meta
|
|||
|
||||
@[builtinCommandElab Lean.Parser.Command.check] def elabCheck : CommandElab := fun stx => do
|
||||
let term := stx[1]
|
||||
withoutModifyingEnv $ runTermElabM (some `_check) $ fun _ => do
|
||||
withoutModifyingEnv $ runTermElabM (some `_check) fun _ => do
|
||||
let e ← Term.elabTerm term none
|
||||
Term.synthesizeSyntheticMVarsNoPostponing
|
||||
let (e, _) ← Term.levelMVarToParam (← instantiateMVars e)
|
||||
|
|
@ -548,7 +538,7 @@ open Meta
|
|||
|
||||
@[builtinCommandElab Lean.Parser.Command.reduce] def elabReduce : CommandElab := fun stx => do
|
||||
let term := stx[1]
|
||||
withoutModifyingEnv $ runTermElabM (some `_check) $ fun _ => do
|
||||
withoutModifyingEnv $ runTermElabM (some `_check) fun _ => do
|
||||
let e ← Term.elabTerm term none
|
||||
Term.synthesizeSyntheticMVarsNoPostponing
|
||||
let (e, _) ← Term.levelMVarToParam (← instantiateMVars e)
|
||||
|
|
@ -582,7 +572,7 @@ def failIfSucceeds (x : CommandElabM Unit) : CommandElabM Unit := do
|
|||
throwError "unexpected success"
|
||||
|
||||
@[builtinCommandElab «check_failure»] def elabCheckFailure : CommandElab := fun stx =>
|
||||
failIfSucceeds $ elabCheck stx
|
||||
failIfSucceeds <| elabCheck stx
|
||||
|
||||
unsafe def elabEvalUnsafe : CommandElab := fun stx => do
|
||||
let ref := stx
|
||||
|
|
@ -644,7 +634,7 @@ constant elabEval : CommandElab
|
|||
pure ()
|
||||
|
||||
def setOption (optionName : Name) (val : DataValue) : CommandElabM Unit := do
|
||||
let decl ← liftIO $ getOptionDecl optionName
|
||||
let decl ← liftIO <| getOptionDecl optionName
|
||||
unless decl.defValue.sameCtor val do throwError "type mismatch at set_option"
|
||||
modifyScope fun scope => { scope with opts := scope.opts.insert optionName val }
|
||||
match optionName, val with
|
||||
|
|
|
|||
|
|
@ -674,7 +674,8 @@ def replaceFVarId (e : Expr) (fvarId : FVarId) (v : Expr) : Expr :=
|
|||
def replaceFVars (e : Expr) (fvars : Array Expr) (vs : Array Expr) : Expr :=
|
||||
(e.abstract fvars).instantiateRev vs
|
||||
|
||||
instance : ToString Expr := ⟨Expr.dbgToString⟩
|
||||
instance : ToString Expr where
|
||||
toString := Expr.dbgToString
|
||||
|
||||
-- TODO: should not use dbgToString, but constructors.
|
||||
instance : Repr Expr := ⟨Expr.dbgToString⟩
|
||||
|
|
|
|||
|
|
@ -9,8 +9,8 @@ structure InternalExceptionId where
|
|||
idx : Nat := 0
|
||||
|
||||
instance : Inhabited InternalExceptionId := ⟨{}⟩
|
||||
instance : BEq InternalExceptionId :=
|
||||
⟨fun id₁ id₂ => id₁.idx == id₂.idx⟩
|
||||
instance : BEq InternalExceptionId where
|
||||
beq id₁ id₂ := id₁.idx == id₂.idx
|
||||
|
||||
builtin_initialize internalExceptionsRef : IO.Ref (Array Name) ← IO.mkRef #[]
|
||||
|
||||
|
|
|
|||
|
|
@ -21,15 +21,13 @@ match (← MonadCache.findCached? a) with
|
|||
MonadCache.cache a b
|
||||
pure b
|
||||
|
||||
instance {α β ρ : Type} {m : Type → Type} [MonadCache α β m] : MonadCache α β (ReaderT ρ m) := {
|
||||
findCached? := fun a r => MonadCache.findCached? a,
|
||||
cache := fun a b r => MonadCache.cache a b
|
||||
}
|
||||
instance {α β ρ : Type} {m : Type → Type} [MonadCache α β m] : MonadCache α β (ReaderT ρ m) where
|
||||
findCached? a r := MonadCache.findCached? a
|
||||
cache a b r := MonadCache.cache a b
|
||||
|
||||
instance {α β ε : Type} {m : Type → Type} [MonadCache α β m] [Monad m] : MonadCache α β (ExceptT ε m) := {
|
||||
findCached? := fun a => ExceptT.lift $ MonadCache.findCached? a,
|
||||
cache := fun a b => ExceptT.lift $ MonadCache.cache a b
|
||||
}
|
||||
instance {α β ε : Type} {m : Type → Type} [MonadCache α β m] [Monad m] : MonadCache α β (ExceptT ε m) where
|
||||
findCached? a := ExceptT.lift $ MonadCache.findCached? a
|
||||
cache a b := ExceptT.lift $ MonadCache.cache a b
|
||||
|
||||
open Std (HashMap)
|
||||
|
||||
|
|
@ -48,10 +46,9 @@ namespace MonadHashMapCacheAdapter
|
|||
@[inline] def cache {α β : Type} {m : Type → Type} [BEq α] [Hashable α] [MonadHashMapCacheAdapter α β m] (a : α) (b : β) : m Unit :=
|
||||
modifyCache fun s => s.insert a b
|
||||
|
||||
instance {α β : Type} {m : Type → Type} [BEq α] [Hashable α] [Monad m] [MonadHashMapCacheAdapter α β m] : MonadCache α β m := {
|
||||
findCached? := MonadHashMapCacheAdapter.findCached?,
|
||||
instance {α β : Type} {m : Type → Type} [BEq α] [Hashable α] [Monad m] [MonadHashMapCacheAdapter α β m] : MonadCache α β m where
|
||||
findCached? := MonadHashMapCacheAdapter.findCached?
|
||||
cache := MonadHashMapCacheAdapter.cache
|
||||
}
|
||||
|
||||
end MonadHashMapCacheAdapter
|
||||
|
||||
|
|
@ -61,10 +58,9 @@ namespace MonadCacheT
|
|||
|
||||
variables {ω α β : Type} {m : Type → Type} [STWorld ω m] [BEq α] [Hashable α] [MonadLiftT (ST ω) m] [Monad m]
|
||||
|
||||
instance : MonadHashMapCacheAdapter α β (MonadCacheT α β m) := {
|
||||
getCache := (get : StateRefT' ..),
|
||||
modifyCache := fun f => (modify f : StateRefT' ..)
|
||||
}
|
||||
instance : MonadHashMapCacheAdapter α β (MonadCacheT α β m) where
|
||||
getCache := (get : StateRefT' ..)
|
||||
modifyCache f := (modify f : StateRefT' ..)
|
||||
|
||||
@[inline] def run {σ} (x : MonadCacheT α β m σ) : m σ :=
|
||||
x.run' Std.mkHashMap
|
||||
|
|
@ -85,10 +81,9 @@ namespace MonadStateCacheT
|
|||
|
||||
variables {ω α β : Type} {m : Type → Type} [STWorld ω m] [BEq α] [Hashable α] [MonadLiftT (ST ω) m] [Monad m]
|
||||
|
||||
instance : MonadHashMapCacheAdapter α β (MonadStateCacheT α β m) := {
|
||||
getCache := (get : StateT ..),
|
||||
modifyCache := fun f => (modify f : StateT ..)
|
||||
}
|
||||
instance : MonadHashMapCacheAdapter α β (MonadStateCacheT α β m) where
|
||||
getCache := (get : StateT ..)
|
||||
modifyCache f := (modify f : StateT ..)
|
||||
|
||||
@[inline] def run {σ} (x : MonadStateCacheT α β m σ) : m σ :=
|
||||
x.run' Std.mkHashMap
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue