chore: move to new frontend
This commit is contained in:
Leonardo de Moura
parent
30ce419e06
commit
7030dc91f2
8 changed files with 371 additions and 368 deletions
|
|
@ -1,3 +1,4 @@
|
|||
#lang lean4
|
||||
/-
|
||||
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
|
@ -15,199 +16,204 @@ import Init.Control.MonadFunctor
|
|||
universes u v w u'
|
||||
|
||||
inductive Except (ε : Type u) (α : Type v)
|
||||
| error : ε → Except
|
||||
| ok : α → Except
|
||||
| error : ε → Except ε α
|
||||
| ok : α → Except ε α
|
||||
|
||||
attribute [unbox] Except
|
||||
|
||||
instance {ε : Type u} {α : Type v} [Inhabited ε] : Inhabited (Except ε α) :=
|
||||
⟨Except.error (arbitrary ε)⟩
|
||||
⟨Except.error (arbitrary ε)⟩
|
||||
|
||||
section
|
||||
variables {ε : Type u} {α : Type v}
|
||||
|
||||
protected def Except.toString [HasToString ε] [HasToString α] : Except ε α → String
|
||||
| Except.error e => "(error " ++ toString e ++ ")"
|
||||
| Except.ok a => "(ok " ++ toString a ++ ")"
|
||||
| Except.error e => "(error " ++ toString e ++ ")"
|
||||
| Except.ok a => "(ok " ++ toString a ++ ")"
|
||||
|
||||
protected def Except.repr [HasRepr ε] [HasRepr α] : Except ε α → String
|
||||
| Except.error e => "(error " ++ repr e ++ ")"
|
||||
| Except.ok a => "(ok " ++ repr a ++ ")"
|
||||
| Except.error e => "(error " ++ repr e ++ ")"
|
||||
| Except.ok a => "(ok " ++ repr a ++ ")"
|
||||
|
||||
instance [HasToString ε] [HasToString α] : HasToString (Except ε α) :=
|
||||
⟨Except.toString⟩
|
||||
|
||||
instance [HasRepr ε] [HasRepr α] : HasRepr (Except ε α) :=
|
||||
⟨Except.repr⟩
|
||||
instance [HasToString ε] [HasToString α] : HasToString (Except ε α) := ⟨Except.toString⟩
|
||||
instance [HasRepr ε] [HasRepr α] : HasRepr (Except ε α) := ⟨Except.repr⟩
|
||||
end
|
||||
|
||||
namespace Except
|
||||
variables {ε : Type u}
|
||||
|
||||
@[inline] protected def return {α : Type v} (a : α) : Except ε α :=
|
||||
Except.ok a
|
||||
@[inline] protected def pure {α : Type v} (a : α) : Except ε α :=
|
||||
Except.ok a
|
||||
|
||||
@[inline] protected def map {α β : Type v} (f : α → β) : Except ε α → Except ε β
|
||||
| Except.error err => Except.error err
|
||||
| Except.ok v => Except.ok $ f v
|
||||
| Except.error err => Except.error err
|
||||
| Except.ok v => Except.ok $ f v
|
||||
|
||||
@[inline] protected def mapError {ε' : Type u} {α : Type v} (f : ε → ε') : Except ε α → Except ε' α
|
||||
| Except.error err => Except.error $ f err
|
||||
| Except.ok v => Except.ok v
|
||||
| Except.error err => Except.error $ f err
|
||||
| Except.ok v => Except.ok v
|
||||
|
||||
@[inline] protected def bind {α β : Type v} (ma : Except ε α) (f : α → Except ε β) : Except ε β :=
|
||||
match ma with
|
||||
| (Except.error err) => Except.error err
|
||||
| (Except.ok v) => f v
|
||||
match ma with
|
||||
| Except.error err => Except.error err
|
||||
| Except.ok v => f v
|
||||
|
||||
@[inline] protected def toBool {α : Type v} : Except ε α → Bool
|
||||
| Except.ok _ => true
|
||||
| Except.error _ => false
|
||||
| Except.ok _ => true
|
||||
| Except.error _ => false
|
||||
|
||||
@[inline] protected def toOption {α : Type v} : Except ε α → Option α
|
||||
| Except.ok a => some a
|
||||
| Except.error _ => none
|
||||
| Except.ok a => some a
|
||||
| Except.error _ => none
|
||||
|
||||
@[inline] protected def tryCatch {α : Type u} (ma : Except ε α) (handle : ε → Except ε α) : Except ε α :=
|
||||
match ma with
|
||||
| Except.ok a => Except.ok a
|
||||
| Except.error e => handle e
|
||||
match ma with
|
||||
| Except.ok a => Except.ok a
|
||||
| Except.error e => handle e
|
||||
|
||||
instance : Monad (Except ε) := {
|
||||
pure := Except.pure,
|
||||
bind := Except.bind,
|
||||
map := Except.map
|
||||
}
|
||||
|
||||
instance : Monad (Except ε) :=
|
||||
{ pure := @Except.return _, bind := @Except.bind _, map := @Except.map _ }
|
||||
end Except
|
||||
|
||||
def ExceptT (ε : Type u) (m : Type u → Type v) (α : Type u) : Type v :=
|
||||
m (Except ε α)
|
||||
m (Except ε α)
|
||||
|
||||
@[inline] def ExceptT.mk {ε : Type u} {m : Type u → Type v} {α : Type u} (x : m (Except ε α)) : ExceptT ε m α :=
|
||||
x
|
||||
|
||||
@[inline] def ExceptT.run {ε : Type u} {m : Type u → Type v} {α : Type u} (x : ExceptT ε m α) : m (Except ε α) :=
|
||||
x
|
||||
@[inline] def ExceptT.mk {ε : Type u} {m : Type u → Type v} {α : Type u} (x : m (Except ε α)) : ExceptT ε m α := x
|
||||
@[inline] def ExceptT.run {ε : Type u} {m : Type u → Type v} {α : Type u} (x : ExceptT ε m α) : m (Except ε α) := x
|
||||
|
||||
namespace ExceptT
|
||||
|
||||
variables {ε : Type u} {m : Type u → Type v} [Monad m]
|
||||
|
||||
@[inline] protected def pure {α : Type u} (a : α) : ExceptT ε m α :=
|
||||
ExceptT.mk $ pure (Except.ok a)
|
||||
ExceptT.mk $ pure (Except.ok a)
|
||||
|
||||
@[inline] protected def bindCont {α β : Type u} (f : α → ExceptT ε m β) : Except ε α → m (Except ε β)
|
||||
| Except.ok a => f a
|
||||
| Except.error e => pure (Except.error e)
|
||||
| Except.ok a => f a
|
||||
| Except.error e => pure (Except.error e)
|
||||
|
||||
@[inline] protected def bind {α β : Type u} (ma : ExceptT ε m α) (f : α → ExceptT ε m β) : ExceptT ε m β :=
|
||||
ExceptT.mk $ ma >>= ExceptT.bindCont f
|
||||
ExceptT.mk $ ma >>= ExceptT.bindCont f
|
||||
|
||||
@[inline] protected def map {α β : Type u} (f : α → β) (x : ExceptT ε m α) : ExceptT ε m β :=
|
||||
ExceptT.mk $ x >>= fun a => match a with
|
||||
| (Except.ok a) => pure $ Except.ok (f a)
|
||||
| (Except.error e) => pure $ Except.error e
|
||||
ExceptT.mk $ x >>= fun a => match a with
|
||||
| (Except.ok a) => pure $ Except.ok (f a)
|
||||
| (Except.error e) => pure $ Except.error e
|
||||
|
||||
@[inline] protected def lift {α : Type u} (t : m α) : ExceptT ε m α :=
|
||||
ExceptT.mk $ Except.ok <$> t
|
||||
ExceptT.mk $ Except.ok <$> t
|
||||
|
||||
instance exceptTOfExcept : MonadLift (Except ε) (ExceptT ε m) :=
|
||||
⟨fun α e => ExceptT.mk $ pure e⟩
|
||||
|
||||
instance : MonadLift m (ExceptT ε m) :=
|
||||
⟨@ExceptT.lift _ _ _⟩
|
||||
instance : MonadLift (Except ε) (ExceptT ε m) := ⟨fun e => ExceptT.mk $ pure e⟩
|
||||
instance : MonadLift m (ExceptT ε m) := ⟨ExceptT.lift⟩
|
||||
|
||||
@[inline] protected def tryCatch {α : Type u} (ma : ExceptT ε m α) (handle : ε → ExceptT ε m α) : ExceptT ε m α :=
|
||||
ExceptT.mk $ ma >>= fun res => match res with
|
||||
| Except.ok a => pure (Except.ok a)
|
||||
| Except.error e => (handle e)
|
||||
ExceptT.mk $ ma >>= fun res => match res with
|
||||
| Except.ok a => pure (Except.ok a)
|
||||
| Except.error e => (handle e)
|
||||
|
||||
instance : MonadFunctor m (ExceptT ε m) :=
|
||||
⟨fun _ f x => f x⟩
|
||||
instance : MonadFunctor m (ExceptT ε m) := ⟨fun f x => f x⟩
|
||||
|
||||
instance : Monad (ExceptT ε m) :=
|
||||
{ pure := @ExceptT.pure _ _ _, bind := @ExceptT.bind _ _ _, map := @ExceptT.map _ _ _ }
|
||||
instance : Monad (ExceptT ε m) := {
|
||||
pure := ExceptT.pure,
|
||||
bind := ExceptT.bind,
|
||||
map := ExceptT.map
|
||||
}
|
||||
|
||||
@[inline] protected def adapt {ε' α : Type u} (f : ε → ε') : ExceptT ε m α → ExceptT ε' m α := fun x =>
|
||||
ExceptT.mk $ Except.mapError f <$> x
|
||||
|
||||
@[inline] protected def adapt {ε' α : Type u} (f : ε → ε') : ExceptT ε m α → ExceptT ε' m α :=
|
||||
fun x => ExceptT.mk $ Except.mapError f <$> x
|
||||
end ExceptT
|
||||
|
||||
/-- An implementation of [MonadError](https://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-Except.html#t:MonadError) -/
|
||||
class MonadExceptOf (ε : Type u) (m : Type v → Type w) :=
|
||||
(throw {α : Type v} : ε → m α)
|
||||
(tryCatch {α : Type v} : m α → (ε → m α) → m α)
|
||||
(throw {α : Type v} : ε → m α)
|
||||
(tryCatch {α : Type v} : m α → (ε → m α) → m α)
|
||||
|
||||
abbrev throwThe (ε : Type u) {m : Type v → Type w} [MonadExceptOf ε m] {α : Type v} (e : ε) : m α :=
|
||||
MonadExceptOf.throw e
|
||||
MonadExceptOf.throw e
|
||||
|
||||
abbrev tryCatchThe (ε : Type u) {m : Type v → Type w} [MonadExceptOf ε m] {α : Type v} (x : m α) (handle : ε → m α) : m α :=
|
||||
MonadExceptOf.tryCatch x handle
|
||||
MonadExceptOf.tryCatch x handle
|
||||
|
||||
instance ExceptT.monadExceptParent (m : Type u → Type v) (ε₁ : Type u) (ε₂ : Type u) [Monad m] [MonadExceptOf ε₁ m] : MonadExceptOf ε₁ (ExceptT ε₂ m) :=
|
||||
{ throw := fun α e => ExceptT.mk $ throwThe ε₁ e,
|
||||
tryCatch := fun α x handle => ExceptT.mk $ tryCatchThe ε₁ x handle }
|
||||
instance (m : Type u → Type v) (ε₁ : Type u) (ε₂ : Type u) [Monad m] [MonadExceptOf ε₁ m] : MonadExceptOf ε₁ (ExceptT ε₂ m) := {
|
||||
throw := fun e => ExceptT.mk $ throwThe ε₁ e,
|
||||
tryCatch := fun x handle => ExceptT.mk $ tryCatchThe ε₁ x handle
|
||||
}
|
||||
|
||||
instance ExceptT.monadExceptSelf (m : Type u → Type v) (ε : Type u) [Monad m] : MonadExceptOf ε (ExceptT ε m) :=
|
||||
{ throw := fun α e => ExceptT.mk $ pure (Except.error e),
|
||||
tryCatch := @ExceptT.tryCatch ε _ _ }
|
||||
instance (m : Type u → Type v) (ε : Type u) [Monad m] : MonadExceptOf ε (ExceptT ε m) := {
|
||||
throw := fun e => ExceptT.mk $ pure (Except.error e),
|
||||
tryCatch := ExceptT.tryCatch
|
||||
}
|
||||
|
||||
instance (ε) : MonadExceptOf ε (Except ε) :=
|
||||
{ throw := fun α => Except.error,
|
||||
tryCatch := @Except.tryCatch _ }
|
||||
instance (ε) : MonadExceptOf ε (Except ε) := {
|
||||
throw := Except.error,
|
||||
tryCatch := Except.tryCatch
|
||||
}
|
||||
|
||||
/-- Similar to `MonadExceptOf`, but `ε` is an outParam for convenience -/
|
||||
class MonadExcept (ε : outParam (Type u)) (m : Type v → Type w) :=
|
||||
(throw {α : Type v} : ε → m α)
|
||||
(tryCatch {α : Type v} : m α → (ε → m α) → m α)
|
||||
(throw {α : Type v} : ε → m α)
|
||||
(tryCatch {α : Type v} : m α → (ε → m α) → m α)
|
||||
|
||||
export MonadExcept (throw tryCatch)
|
||||
|
||||
instance MonadExceptOf.isMonadExcept (ε : outParam (Type u)) (m : Type v → Type w) [MonadExceptOf ε m] : MonadExcept ε m :=
|
||||
{ throw := fun _ e => throwThe ε e,
|
||||
tryCatch := fun _ x handle => tryCatchThe ε x handle }
|
||||
instance (ε : outParam (Type u)) (m : Type v → Type w) [MonadExceptOf ε m] : MonadExcept ε m := {
|
||||
throw := throwThe ε,
|
||||
tryCatch := tryCatchThe ε
|
||||
}
|
||||
|
||||
namespace MonadExcept
|
||||
variables {ε : Type u} {m : Type v → Type w}
|
||||
|
||||
@[inline] protected def orelse [MonadExcept ε m] {α : Type v} (t₁ t₂ : m α) : m α :=
|
||||
tryCatch t₁ $ fun _ => t₂
|
||||
tryCatch t₁ fun _ => t₂
|
||||
|
||||
instance [MonadExcept ε m] {α : Type v} : HasOrelse (m α) :=
|
||||
⟨MonadExcept.orelse⟩
|
||||
instance [MonadExcept ε m] {α : Type v} : HasOrelse (m α) := ⟨MonadExcept.orelse⟩
|
||||
|
||||
/-- Alternative orelse operator that allows to select which exception should be used.
|
||||
The default is to use the first exception since the standard `orelse` uses the second. -/
|
||||
@[inline] def orelse' [MonadExcept ε m] {α : Type v} (t₁ t₂ : m α) (useFirstEx := true) : m α :=
|
||||
tryCatch t₁ $ fun e₁ => tryCatch t₂ $ fun e₂ => throw (if useFirstEx then e₁ else e₂)
|
||||
tryCatch t₁ fun e₁ => tryCatch t₂ fun e₂ => throw (if useFirstEx then e₁ else e₂)
|
||||
|
||||
end MonadExcept
|
||||
|
||||
@[inline] def observing {ε α : Type u} {m : Type u → Type v} [Monad m] [MonadExcept ε m] (x : m α) : m (Except ε α) :=
|
||||
tryCatch (do a ← x; pure (Except.ok a)) (fun ex => pure (Except.error ex))
|
||||
tryCatch (do let a ← x; pure (Except.ok a)) (fun ex => pure (Except.error ex))
|
||||
|
||||
instance ExceptT.monadControl (ε : Type u) (m : Type u → Type v) [Monad m] : MonadControl m (ExceptT ε m) := {
|
||||
stM := fun α => Except ε α,
|
||||
liftWith := fun α f => liftM $ f fun β x => x.run,
|
||||
restoreM := fun α x => x,
|
||||
instance (ε : Type u) (m : Type u → Type v) [Monad m] : MonadControl m (ExceptT ε m) := {
|
||||
stM := Except ε,
|
||||
liftWith := fun f => liftM $ f fun x => x.run,
|
||||
restoreM := fun x => x
|
||||
}
|
||||
|
||||
class MonadFinally (m : Type u → Type v) :=
|
||||
(tryFinally' {α β} : m α → (Option α → m β) → m (α × β))
|
||||
(tryFinally' {α β} : m α → (Option α → m β) → m (α × β))
|
||||
|
||||
export MonadFinally (tryFinally')
|
||||
|
||||
/-- Execute `x` and then execute `finalizer` even if `x` threw an exception -/
|
||||
@[inline] abbrev tryFinally {m : Type u → Type v} {α β : Type u} [MonadFinally m] [Functor m] (x : m α) (finalizer : m β) : m α := do
|
||||
Prod.fst <$> tryFinally' x (fun _ => finalizer)
|
||||
@[inline] abbrev tryFinally {m : Type u → Type v} {α β : Type u} [MonadFinally m] [Functor m] (x : m α) (finalizer : m β) : m α :=
|
||||
let y := tryFinally' x (fun _ => finalizer)
|
||||
(·.1) <$> y
|
||||
|
||||
instance Id.finally : MonadFinally Id :=
|
||||
{ tryFinally' := fun α β x h =>
|
||||
let a := x;
|
||||
let b := h (some x);
|
||||
pure (a, b) }
|
||||
instance Id.finally : MonadFinally Id := {
|
||||
tryFinally' := fun x h =>
|
||||
let a := x
|
||||
let b := h (some x)
|
||||
pure (a, b)
|
||||
}
|
||||
|
||||
instance ExceptT.finally {m : Type u → Type v} {ε : Type u} [MonadFinally m] [Monad m] : MonadFinally (ExceptT ε m) :=
|
||||
{ tryFinally' := fun α β x h => ExceptT.mk do
|
||||
r ← tryFinally' x (fun e? => match e? with
|
||||
instance ExceptT.finally {m : Type u → Type v} {ε : Type u} [MonadFinally m] [Monad m] : MonadFinally (ExceptT ε m) := {
|
||||
tryFinally' := fun x h => ExceptT.mk do
|
||||
let r ← tryFinally' x fun e? => match e? with
|
||||
| some (Except.ok a) => h (some a)
|
||||
| _ => h none);
|
||||
| _ => h none
|
||||
match r with
|
||||
| (Except.ok a, Except.ok b) => pure (Except.ok (a, b))
|
||||
| (_, Except.error e) => pure (Except.error e) -- second error has precedence
|
||||
| (Except.error e, _) => pure (Except.error e) }
|
||||
| (Except.error e, _) => pure (Except.error e)
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,3 +1,4 @@
|
|||
#lang lean4
|
||||
/-
|
||||
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
|
@ -15,13 +16,13 @@ universes u v w
|
|||
|
||||
/-- An implementation of [ReaderT](https://hackage.haskell.org/package/transformers-0.5.5.0/docs/Control-Monad-Trans-Reader.html#t:ReaderT) -/
|
||||
def ReaderT (ρ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
|
||||
ρ → m α
|
||||
ρ → m α
|
||||
|
||||
instance ReaderT.inhabited (ρ : Type u) (m : Type u → Type v) (α : Type u) [Inhabited (m α)] : Inhabited (ReaderT ρ m α) :=
|
||||
⟨fun _ => arbitrary _⟩
|
||||
instance (ρ : Type u) (m : Type u → Type v) (α : Type u) [Inhabited (m α)] : Inhabited (ReaderT ρ m α) :=
|
||||
⟨fun _ => arbitrary _⟩
|
||||
|
||||
@[inline] def ReaderT.run {ρ : Type u} {m : Type u → Type v} {α : Type u} (x : ReaderT ρ m α) (r : ρ) : m α :=
|
||||
x r
|
||||
x r
|
||||
|
||||
@[reducible] def Reader (ρ : Type u) := ReaderT ρ id
|
||||
|
||||
|
|
@ -31,20 +32,20 @@ section
|
|||
variables {ρ : Type u} {m : Type u → Type v} {α : Type u}
|
||||
|
||||
@[inline] protected def lift (a : m α) : ReaderT ρ m α :=
|
||||
fun r => a
|
||||
fun r => a
|
||||
|
||||
instance : MonadLift m (ReaderT ρ m) :=
|
||||
⟨@ReaderT.lift ρ m⟩
|
||||
instance : MonadLift m (ReaderT ρ m) := ⟨ReaderT.lift⟩
|
||||
|
||||
instance (ε) [MonadExceptOf ε m] : MonadExceptOf ε (ReaderT ρ m) :=
|
||||
{ throw := fun α => ReaderT.lift ∘ throwThe ε,
|
||||
tryCatch := fun α x c r => tryCatchThe ε (x r) (fun e => (c e) r) }
|
||||
instance (ε) [MonadExceptOf ε m] : MonadExceptOf ε (ReaderT ρ m) := {
|
||||
throw := ReaderT.lift ∘ throwThe ε,
|
||||
tryCatch := fun x c r => tryCatchThe ε (x r) (fun e => (c e) r)
|
||||
}
|
||||
|
||||
@[inline] protected def orelse [Alternative m] {α : Type u} (x₁ x₂ : ReaderT ρ m α) : ReaderT ρ m α :=
|
||||
fun s => x₁ s <|> x₂ s
|
||||
fun s => x₁ s <|> x₂ s
|
||||
|
||||
@[inline] protected def failure [Alternative m] {α : Type u} : ReaderT ρ m α :=
|
||||
fun s => failure
|
||||
fun s => failure
|
||||
|
||||
end
|
||||
|
||||
|
|
@ -52,30 +53,32 @@ section
|
|||
variables {ρ : Type u} {m : Type u → Type v} [Monad m] {α β : Type u}
|
||||
|
||||
@[inline] protected def read : ReaderT ρ m ρ :=
|
||||
pure
|
||||
pure
|
||||
|
||||
@[inline] protected def pure (a : α) : ReaderT ρ m α :=
|
||||
fun r => pure a
|
||||
fun r => pure a
|
||||
|
||||
@[inline] protected def bind (x : ReaderT ρ m α) (f : α → ReaderT ρ m β) : ReaderT ρ m β :=
|
||||
fun r => do a ← x r; f a r
|
||||
fun r => do let a ← x r; f a r
|
||||
|
||||
@[inline] protected def map (f : α → β) (x : ReaderT ρ m α) : ReaderT ρ m β :=
|
||||
fun r => f <$> x r
|
||||
fun r => f <$> x r
|
||||
|
||||
instance : Monad (ReaderT ρ m) :=
|
||||
{ pure := @ReaderT.pure _ _ _, bind := @ReaderT.bind _ _ _, map := @ReaderT.map _ _ _ }
|
||||
instance : Monad (ReaderT ρ m) := {
|
||||
pure := ReaderT.pure,
|
||||
bind := ReaderT.bind,
|
||||
map := ReaderT.map
|
||||
}
|
||||
|
||||
instance (ρ m) [Monad m] : MonadFunctor m (ReaderT ρ m) :=
|
||||
⟨fun _ f x r => f (x r)⟩
|
||||
instance (ρ m) [Monad m] : MonadFunctor m (ReaderT ρ m) := ⟨fun f x r => f (x r)⟩
|
||||
|
||||
@[inline] protected def adapt {ρ' : Type u} [Monad m] {α : Type u} (f : ρ' → ρ) : ReaderT ρ m α → ReaderT ρ' m α :=
|
||||
fun x r => x (f r)
|
||||
fun x r => x (f r)
|
||||
|
||||
instance [Alternative m] : Alternative (ReaderT ρ m) :=
|
||||
{ ReaderT.Monad with
|
||||
failure := @ReaderT.failure _ _ _,
|
||||
orelse := @ReaderT.orelse _ _ _ }
|
||||
instance [Alternative m] : Alternative (ReaderT ρ m) := {
|
||||
failure := ReaderT.failure,
|
||||
orelse := ReaderT.orelse
|
||||
}
|
||||
|
||||
end
|
||||
end ReaderT
|
||||
|
|
@ -91,56 +94,56 @@ end ReaderT
|
|||
```
|
||||
-/
|
||||
class MonadReaderOf (ρ : Type u) (m : Type u → Type v) :=
|
||||
(read : m ρ)
|
||||
(read : m ρ)
|
||||
|
||||
@[inline] def readThe (ρ : Type u) {m : Type u → Type v} [MonadReaderOf ρ m] : m ρ :=
|
||||
MonadReaderOf.read
|
||||
MonadReaderOf.read
|
||||
|
||||
/-- Similar to `MonadReaderOf`, but `ρ` is an outParam for convenience -/
|
||||
class MonadReader (ρ : outParam (Type u)) (m : Type u → Type v) :=
|
||||
(read : m ρ)
|
||||
(read : m ρ)
|
||||
|
||||
export MonadReader (read)
|
||||
|
||||
instance MonadReaderOf.isMonadReader (ρ : Type u) (m : Type u → Type v) [MonadReaderOf ρ m] : MonadReader ρ m :=
|
||||
⟨readThe ρ⟩
|
||||
instance (ρ : Type u) (m : Type u → Type v) [MonadReaderOf ρ m] : MonadReader ρ m :=
|
||||
⟨readThe ρ⟩
|
||||
|
||||
instance monadReaderTrans {ρ : Type u} {m : Type u → Type v} {n : Type u → Type w}
|
||||
[MonadReaderOf ρ m] [MonadLift m n] : MonadReaderOf ρ n :=
|
||||
⟨monadLift (MonadReader.read : m ρ)⟩
|
||||
instance {ρ : Type u} {m : Type u → Type v} {n : Type u → Type w} [MonadReaderOf ρ m] [MonadLift m n] : MonadReaderOf ρ n :=
|
||||
⟨monadLift (MonadReader.read : m ρ)⟩
|
||||
|
||||
instance {ρ : Type u} {m : Type u → Type v} [Monad m] : MonadReaderOf ρ (ReaderT ρ m) :=
|
||||
⟨ReaderT.read⟩
|
||||
⟨ReaderT.read⟩
|
||||
|
||||
instance ReaderT.monadControl (ρ : Type u) (m : Type u → Type v) : MonadControl m (ReaderT ρ m) := {
|
||||
stM := fun α => α,
|
||||
liftWith := fun α f ctx => f fun β x => x ctx,
|
||||
restoreM := fun α x ctx => x,
|
||||
instance (ρ : Type u) (m : Type u → Type v) : MonadControl m (ReaderT ρ m) := {
|
||||
stM := id,
|
||||
liftWith := fun f ctx => f fun x => x ctx,
|
||||
restoreM := fun x ctx => x,
|
||||
}
|
||||
|
||||
instance ReaderT.tryFinally {m : Type u → Type v} {ρ : Type u} [MonadFinally m] [Monad m] : MonadFinally (ReaderT ρ m) :=
|
||||
{ tryFinally' := fun α β x h ctx => tryFinally' (x ctx) (fun a? => h a? ctx) }
|
||||
instance ReaderT.tryFinally {m : Type u → Type v} {ρ : Type u} [MonadFinally m] [Monad m] : MonadFinally (ReaderT ρ m) := {
|
||||
tryFinally' := fun x h ctx => tryFinally' (x ctx) (fun a? => h a? ctx)
|
||||
}
|
||||
|
||||
class MonadWithReaderOf (ρ : Type u) (m : Type u → Type v) :=
|
||||
(withReader {α : Type u} : (ρ → ρ) → m α → m α)
|
||||
(withReader {α : Type u} : (ρ → ρ) → m α → m α)
|
||||
|
||||
@[inline] def withTheReader (ρ : Type u) {m : Type u → Type v} [MonadWithReaderOf ρ m] {α : Type u} (f : ρ → ρ) (x : m α) : m α :=
|
||||
MonadWithReaderOf.withReader f x
|
||||
MonadWithReaderOf.withReader f x
|
||||
|
||||
class MonadWithReader (ρ : outParam (Type u)) (m : Type u → Type v) :=
|
||||
(withReader {α : Type u} : (ρ → ρ) → m α → m α)
|
||||
(withReader {α : Type u} : (ρ → ρ) → m α → m α)
|
||||
|
||||
export MonadWithReader (withReader)
|
||||
|
||||
instance MonadWithReaderOf.isMonadWithReader (ρ : Type u) (m : Type u → Type v) [MonadWithReaderOf ρ m] : MonadWithReader ρ m :=
|
||||
⟨fun α => withTheReader ρ⟩
|
||||
instance (ρ : Type u) (m : Type u → Type v) [MonadWithReaderOf ρ m] : MonadWithReader ρ m := ⟨withTheReader ρ⟩
|
||||
|
||||
section
|
||||
variables {ρ : Type u} {m : Type u → Type v}
|
||||
|
||||
instance monadWithReaderOfTrans {n : Type u → Type v} [MonadWithReaderOf ρ m] [MonadFunctor m n] : MonadWithReaderOf ρ n :=
|
||||
⟨fun α f => monadMap fun β => (withTheReader ρ f : m β → m β)⟩
|
||||
instance {n : Type u → Type v} [MonadWithReaderOf ρ m] [MonadFunctor m n] : MonadWithReaderOf ρ n :=
|
||||
⟨fun f => monadMap (m := m) (withTheReader ρ f)⟩
|
||||
|
||||
instance [Monad m] : MonadWithReaderOf ρ (ReaderT ρ m) :=
|
||||
⟨fun f x ctx => x (f ctx)⟩
|
||||
|
||||
instance ReaderT.monadWithReaderOf [Monad m] : MonadWithReaderOf ρ (ReaderT ρ m) :=
|
||||
⟨fun α f x ctx => x (f ctx)⟩
|
||||
end
|
||||
|
|
|
|||
|
|
@ -1,3 +1,4 @@
|
|||
#lang lean4
|
||||
/-
|
||||
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
|
@ -13,19 +14,24 @@ import Init.Control.Except
|
|||
universes u v w
|
||||
|
||||
def StateT (σ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
|
||||
σ → m (α × σ)
|
||||
σ → m (α × σ)
|
||||
|
||||
@[inline] def StateT.run {σ : Type u} {m : Type u → Type v} {α : Type u} (x : StateT σ m α) (s : σ) : m (α × σ) :=
|
||||
x s
|
||||
x s
|
||||
|
||||
@[inline] def StateT.run' {σ : Type u} {m : Type u → Type v} [Functor m] {α : Type u} (x : StateT σ m α) (s : σ) : m α :=
|
||||
Prod.fst <$> x s
|
||||
(·.1) <$> x s
|
||||
|
||||
@[reducible] def StateM (σ α : Type u) : Type u := StateT σ Id α
|
||||
|
||||
instance StateM.subsingleton {σ α} [Subsingleton σ] [Subsingleton α] : Subsingleton (StateM σ α) :=
|
||||
⟨λ x y => funext $ fun (s : σ) => match x s, y s with
|
||||
| (a₁, s₁), (a₂, s₂) => Subsingleton.elim a₁ a₂ ▸ Subsingleton.elim s₁ s₂ ▸ rfl⟩
|
||||
instance {σ α} [Subsingleton σ] [Subsingleton α] : Subsingleton (StateM σ α) := ⟨by
|
||||
intro x y
|
||||
apply funext
|
||||
intro s
|
||||
match x s, y s with
|
||||
| (a₁, s₁), (a₂, s₂) =>
|
||||
rw [Subsingleton.elim a₁ a₂, Subsingleton.elim s₁ s₂]
|
||||
exact rfl⟩
|
||||
|
||||
namespace StateT
|
||||
section
|
||||
|
|
@ -33,56 +39,51 @@ variables {σ : Type u} {m : Type u → Type v}
|
|||
variables [Monad m] {α β : Type u}
|
||||
|
||||
@[inline] protected def pure (a : α) : StateT σ m α :=
|
||||
fun s => pure (a, s)
|
||||
fun s => pure (a, s)
|
||||
|
||||
@[inline] protected def bind (x : StateT σ m α) (f : α → StateT σ m β) : StateT σ m β :=
|
||||
fun s => do (a, s) ← x s; f a s
|
||||
fun s => do let (a, s) ← x s; f a s
|
||||
|
||||
@[inline] protected def map (f : α → β) (x : StateT σ m α) : StateT σ m β :=
|
||||
fun s => do (a, s) ← x s; pure (f a, s)
|
||||
fun s => do let (a, s) ← x s; pure (f a, s)
|
||||
|
||||
instance : Monad (StateT σ m) :=
|
||||
{ pure := @StateT.pure _ _ _, bind := @StateT.bind _ _ _, map := @StateT.map _ _ _ }
|
||||
instance : Monad (StateT σ m) := {
|
||||
pure := StateT.pure,
|
||||
bind := StateT.bind,
|
||||
map := StateT.map
|
||||
}
|
||||
|
||||
@[inline] protected def orelse [Alternative m] {α : Type u} (x₁ x₂ : StateT σ m α) : StateT σ m α :=
|
||||
fun s => x₁ s <|> x₂ s
|
||||
fun s => x₁ s <|> x₂ s
|
||||
|
||||
@[inline] protected def failure [Alternative m] {α : Type u} : StateT σ m α :=
|
||||
fun s => failure
|
||||
fun s => failure
|
||||
|
||||
instance [Alternative m] : Alternative (StateT σ m) :=
|
||||
{ StateT.Monad with
|
||||
failure := @StateT.failure _ _ _ _,
|
||||
orelse := @StateT.orelse _ _ _ _ }
|
||||
instance [Alternative m] : Alternative (StateT σ m) := {
|
||||
failure := StateT.failure,
|
||||
orelse := StateT.orelse
|
||||
}
|
||||
|
||||
@[inline] protected def get : StateT σ m σ :=
|
||||
fun s => pure (s, s)
|
||||
fun s => pure (s, s)
|
||||
|
||||
@[inline] protected def set : σ → StateT σ m PUnit :=
|
||||
fun s' s => pure (⟨⟩, s')
|
||||
fun s' s => pure (⟨⟩, s')
|
||||
|
||||
@[inline] protected def modifyGet (f : σ → α × σ) : StateT σ m α :=
|
||||
fun s => pure (f s)
|
||||
fun s => pure (f s)
|
||||
|
||||
@[inline] protected def lift {α : Type u} (t : m α) : StateT σ m α :=
|
||||
fun s => do a ← t; pure (a, s)
|
||||
fun s => do let a ← t; pure (a, s)
|
||||
|
||||
instance : MonadLift m (StateT σ m) :=
|
||||
⟨@StateT.lift σ m _⟩
|
||||
instance : MonadLift m (StateT σ m) := ⟨StateT.lift⟩
|
||||
|
||||
instance (σ m) [Monad m] : MonadFunctor m (StateT σ m) :=
|
||||
⟨fun _ f x s => f (x s)⟩
|
||||
instance (σ m) [Monad m] : MonadFunctor m (StateT σ m) := ⟨fun f x s => f (x s)⟩
|
||||
|
||||
@[inline] protected def adapt {σ σ' σ'' α : Type u} {m : Type u → Type v} [Monad m] (split : σ → σ' × σ'')
|
||||
(join : σ' → σ'' → σ) (x : StateT σ' m α) : StateT σ m α :=
|
||||
fun st => do
|
||||
let (st, ctx) := split st;
|
||||
(a, st') ← x st;
|
||||
pure (a, join st' ctx)
|
||||
|
||||
instance (ε) [MonadExceptOf ε m] : MonadExceptOf ε (StateT σ m) :=
|
||||
{ throw := fun α => StateT.lift ∘ throwThe ε,
|
||||
tryCatch := fun α x c s => tryCatchThe ε (x s) (fun e => c e s) }
|
||||
instance (ε) [MonadExceptOf ε m] : MonadExceptOf ε (StateT σ m) := {
|
||||
throw := StateT.lift ∘ throwThe ε,
|
||||
tryCatch := fun x c s => tryCatchThe ε (x s) (fun e => c e s)
|
||||
}
|
||||
|
||||
end
|
||||
end StateT
|
||||
|
|
@ -91,73 +92,76 @@ end StateT
|
|||
In contrast to the Haskell implementation, we use overlapping instances to derive instances
|
||||
automatically from `monadLift`. -/
|
||||
class MonadStateOf (σ : Type u) (m : Type u → Type v) :=
|
||||
/- Obtain the top-most State of a Monad stack. -/
|
||||
(get : m σ)
|
||||
/- Set the top-most State of a Monad stack. -/
|
||||
(set : σ → m PUnit)
|
||||
/- Map the top-most State of a Monad stack.
|
||||
/- Obtain the top-most State of a Monad stack. -/
|
||||
(get : m σ)
|
||||
/- Set the top-most State of a Monad stack. -/
|
||||
(set : σ → m PUnit)
|
||||
/- Map the top-most State of a Monad stack.
|
||||
|
||||
Note: `modifyGet f` may be preferable to `do s <- get; let (a, s) := f s; put s; pure a`
|
||||
because the latter does not use the State linearly (without sufficient inlining). -/
|
||||
(modifyGet {α : Type u} : (σ → α × σ) → m α)
|
||||
Note: `modifyGet f` may be preferable to `do s <- get; let (a, s) := f s; put s; pure a`
|
||||
because the latter does not use the State linearly (without sufficient inlining). -/
|
||||
(modifyGet {α : Type u} : (σ → α × σ) → m α)
|
||||
|
||||
export MonadStateOf (set)
|
||||
|
||||
abbrev getThe (σ : Type u) {m : Type u → Type v} [MonadStateOf σ m] : m σ :=
|
||||
MonadStateOf.get
|
||||
MonadStateOf.get
|
||||
|
||||
@[inline] abbrev modifyThe (σ : Type u) {m : Type u → Type v} [MonadStateOf σ m] (f : σ → σ) : m PUnit :=
|
||||
MonadStateOf.modifyGet fun s => (PUnit.unit, f s)
|
||||
MonadStateOf.modifyGet fun s => (PUnit.unit, f s)
|
||||
|
||||
@[inline] abbrev modifyGetThe {α : Type u} (σ : Type u) {m : Type u → Type v} [MonadStateOf σ m] (f : σ → α × σ) : m α :=
|
||||
MonadStateOf.modifyGet f
|
||||
MonadStateOf.modifyGet f
|
||||
|
||||
/-- Similar to `MonadStateOf`, but `σ` is an outParam for convenience -/
|
||||
class MonadState (σ : outParam (Type u)) (m : Type u → Type v) :=
|
||||
(get : m σ)
|
||||
(set : σ → m PUnit)
|
||||
(modifyGet {α : Type u} : (σ → α × σ) → m α)
|
||||
(get : m σ)
|
||||
(set : σ → m PUnit)
|
||||
(modifyGet {α : Type u} : (σ → α × σ) → m α)
|
||||
|
||||
export MonadState (get modifyGet)
|
||||
|
||||
instance monadStateOf.isMonadState (σ : Type u) (m : Type u → Type v) [MonadStateOf σ m] : MonadState σ m :=
|
||||
{ set := MonadStateOf.set,
|
||||
instance (σ : Type u) (m : Type u → Type v) [MonadStateOf σ m] : MonadState σ m := {
|
||||
set := MonadStateOf.set,
|
||||
get := getThe σ,
|
||||
modifyGet := fun α f => MonadStateOf.modifyGet f }
|
||||
modifyGet := fun f => MonadStateOf.modifyGet f
|
||||
}
|
||||
|
||||
section
|
||||
variables {σ : Type u} {m : Type u → Type v}
|
||||
|
||||
@[inline] def modify [MonadState σ m] (f : σ → σ) : m PUnit :=
|
||||
modifyGet fun s => (PUnit.unit, f s)
|
||||
modifyGet fun s => (PUnit.unit, f s)
|
||||
|
||||
@[inline] def getModify [MonadState σ m] [Monad m] (f : σ → σ) : m σ := do
|
||||
modifyGet fun s => (s, f s)
|
||||
modifyGet fun s => (s, f s)
|
||||
|
||||
-- NOTE: The Ordering of the following two instances determines that the top-most `StateT` Monad layer
|
||||
-- will be picked first
|
||||
instance monadStateTrans {n : Type u → Type w} [MonadStateOf σ m] [MonadLift m n] : MonadStateOf σ n :=
|
||||
{ get := monadLift (MonadStateOf.get : m _),
|
||||
set := fun st => monadLift (MonadStateOf.set st : m _),
|
||||
modifyGet := fun α f => monadLift (MonadState.modifyGet f : m _) }
|
||||
instance {n : Type u → Type w} [MonadStateOf σ m] [MonadLift m n] : MonadStateOf σ n := {
|
||||
get := liftM (m := m) MonadStateOf.get,
|
||||
set := fun s => liftM (m := m) $ MonadStateOf.set s,
|
||||
modifyGet := fun f => monadLift (m := m) $ MonadState.modifyGet f
|
||||
}
|
||||
|
||||
instance [Monad m] : MonadStateOf σ (StateT σ m) :=
|
||||
{ get := StateT.get,
|
||||
set := StateT.set,
|
||||
modifyGet := @StateT.modifyGet _ _ _ }
|
||||
instance [Monad m] : MonadStateOf σ (StateT σ m) := {
|
||||
get := StateT.get,
|
||||
set := StateT.set,
|
||||
modifyGet := StateT.modifyGet
|
||||
}
|
||||
|
||||
end
|
||||
|
||||
instance StateT.monadControl (σ : Type u) (m : Type u → Type v) [Monad m] : MonadControl m (StateT σ m) := {
|
||||
stM := fun α => α × σ,
|
||||
liftWith := fun α f => do s ← get; liftM (f (fun β x => x.run s)),
|
||||
restoreM := fun α x => do (a, s) ← liftM x; set s; pure a
|
||||
liftWith := fun f => do let s ← get; liftM (f (fun x => x.run s)),
|
||||
restoreM := fun x => do let (a, s) ← liftM x; set s; pure a
|
||||
}
|
||||
|
||||
instance StateT.tryFinally {m : Type u → Type v} {σ : Type u} [MonadFinally m] [Monad m] : MonadFinally (StateT σ m) :=
|
||||
{ tryFinally' := fun α β x h s => do
|
||||
((a, _), (b, s'')) ← tryFinally' (x s)
|
||||
(fun p? => match p? with
|
||||
instance StateT.tryFinally {m : Type u → Type v} {σ : Type u} [MonadFinally m] [Monad m] : MonadFinally (StateT σ m) := {
|
||||
tryFinally' := fun x h s => do
|
||||
let ((a, _), (b, s'')) ← tryFinally' (x s) fun
|
||||
| some (a, s') => h (some a) s'
|
||||
| none => h none s);
|
||||
pure ((a, b), s'') }
|
||||
| none => h none s
|
||||
pure ((a, b), s'')
|
||||
}
|
||||
|
|
|
|||
|
|
@ -13,6 +13,9 @@ import Init.Control.Id
|
|||
import Init.Util
|
||||
universes u v w
|
||||
|
||||
namespace HasToString end HasToString -- Hack for old frontend
|
||||
open HasToString (toString) -- Hack for old frontend
|
||||
|
||||
/-
|
||||
The Compiler has special support for arrays.
|
||||
They are implemented using dynamic arrays: https://en.wikipedia.org/wiki/Dynamic_array
|
||||
|
|
|
|||
|
|
@ -1,3 +1,4 @@
|
|||
#lang lean4
|
||||
/-
|
||||
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
|
@ -15,62 +16,65 @@ available on the Haskell library
|
|||
|
||||
/- Interface for random number generators. -/
|
||||
class RandomGen (g : Type u) :=
|
||||
/- `range` returns the range of values returned by
|
||||
the generator. -/
|
||||
(range : g → Nat × Nat)
|
||||
/- `next` operation returns a natural number that is uniformly distributed
|
||||
the range returned by `range` (including both end points),
|
||||
and a new generator. -/
|
||||
(next : g → Nat × g)
|
||||
/-
|
||||
The 'split' operation allows one to obtain two distinct random number
|
||||
generators. This is very useful in functional programs (for example, when
|
||||
passing a random number generator down to recursive calls). -/
|
||||
(split : g → g × g)
|
||||
/- `range` returns the range of values returned by
|
||||
the generator. -/
|
||||
(range : g → Nat × Nat)
|
||||
/- `next` operation returns a natural number that is uniformly distributed
|
||||
the range returned by `range` (including both end points),
|
||||
and a new generator. -/
|
||||
(next : g → Nat × g)
|
||||
/-
|
||||
The 'split' operation allows one to obtain two distinct random number
|
||||
generators. This is very useful in functional programs (for example, when
|
||||
passing a random number generator down to recursive calls). -/
|
||||
(split : g → g × g)
|
||||
|
||||
/- "Standard" random number generator. -/
|
||||
structure StdGen :=
|
||||
(s1 : Nat) (s2 : Nat)
|
||||
(s1 : Nat)
|
||||
(s2 : Nat)
|
||||
|
||||
instance StdGen.inhabited : Inhabited StdGen := ⟨{ s1 := 0, s2 := 0 }⟩
|
||||
instance : Inhabited StdGen := ⟨{ s1 := 0, s2 := 0 }⟩
|
||||
|
||||
def stdRange := (1, 2147483562)
|
||||
|
||||
instance : HasRepr StdGen :=
|
||||
{ repr := fun ⟨s1, s2⟩ => "⟨" ++ toString s1 ++ ", " ++ toString s2 ++ "⟩" }
|
||||
instance : HasRepr StdGen := {
|
||||
repr := fun ⟨s1, s2⟩ => "⟨" ++ toString s1 ++ ", " ++ toString s2 ++ "⟩"
|
||||
}
|
||||
|
||||
def stdNext : StdGen → Nat × StdGen
|
||||
| ⟨s1, s2⟩ =>
|
||||
let k : Int := s1 / 53668;
|
||||
let s1' : Int := 40014 * ((s1 : Int) - k * 53668) - k * 12211;
|
||||
let s1'' : Int := if s1' < 0 then s1' + 2147483563 else s1';
|
||||
let k' : Int := s2 / 52774;
|
||||
let s2' : Int := 40692 * ((s2 : Int) - k' * 52774) - k' * 3791;
|
||||
let s2'' : Int := if s2' < 0 then s2' + 2147483399 else s2';
|
||||
let z : Int := s1'' - s2'';
|
||||
let z' : Int := if z < 1 then z + 2147483562 else z % 2147483562;
|
||||
(z'.toNat, ⟨s1''.toNat, s2''.toNat⟩)
|
||||
| ⟨s1, s2⟩ =>
|
||||
let k : Int := s1 / 53668
|
||||
let s1' : Int := 40014 * ((s1 : Int) - k * 53668) - k * 12211
|
||||
let s1'' : Int := if s1' < 0 then s1' + 2147483563 else s1'
|
||||
let k' : Int := s2 / 52774
|
||||
let s2' : Int := 40692 * ((s2 : Int) - k' * 52774) - k' * 3791
|
||||
let s2'' : Int := if s2' < 0 then s2' + 2147483399 else s2'
|
||||
let z : Int := s1'' - s2''
|
||||
let z' : Int := if z < 1 then z + 2147483562 else z % 2147483562
|
||||
(z'.toNat, ⟨s1''.toNat, s2''.toNat⟩)
|
||||
|
||||
def stdSplit : StdGen → StdGen × StdGen
|
||||
| g@⟨s1, s2⟩ =>
|
||||
let newS1 := if s1 = 2147483562 then 1 else s1 + 1;
|
||||
let newS2 := if s2 = 1 then 2147483398 else s2 - 1;
|
||||
let newG := (stdNext g).2;
|
||||
let leftG := StdGen.mk newS1 newG.2;
|
||||
let rightG := StdGen.mk newG.1 newS2;
|
||||
(leftG, rightG)
|
||||
| g@⟨s1, s2⟩ =>
|
||||
let newS1 := if s1 = 2147483562 then 1 else s1 + 1
|
||||
let newS2 := if s2 = 1 then 2147483398 else s2 - 1
|
||||
let newG := (stdNext g).2
|
||||
let leftG := StdGen.mk newS1 newG.2
|
||||
let rightG := StdGen.mk newG.1 newS2
|
||||
(leftG, rightG)
|
||||
|
||||
instance : RandomGen StdGen :=
|
||||
{range := fun _ => stdRange,
|
||||
next := stdNext,
|
||||
split := stdSplit}
|
||||
instance : RandomGen StdGen := {
|
||||
range := fun _ => stdRange,
|
||||
next := stdNext,
|
||||
split := stdSplit
|
||||
}
|
||||
|
||||
/-- Return a standard number generator. -/
|
||||
def mkStdGen (s : Nat := 0) : StdGen :=
|
||||
let q := s / 2147483562;
|
||||
let s1 := s % 2147483562;
|
||||
let s2 := q % 2147483398;
|
||||
⟨s1 + 1, s2 + 1⟩
|
||||
let q := s / 2147483562
|
||||
let s1 := s % 2147483562
|
||||
let s2 := q % 2147483398
|
||||
⟨s1 + 1, s2 + 1⟩
|
||||
|
||||
/-
|
||||
Auxiliary function for randomNatVal.
|
||||
|
|
@ -79,46 +83,42 @@ Generate random values until we exceed the target magnitude.
|
|||
The parameter `r` is the "remaining" magnitude.
|
||||
-/
|
||||
private partial def randNatAux {gen : Type u} [RandomGen gen] (genLo genMag : Nat) : Nat → (Nat × gen) → Nat × gen
|
||||
| 0, (v, g) => (v, g)
|
||||
| r'@(r+1), (v, g) =>
|
||||
let (x, g') := RandomGen.next g;
|
||||
let v' := v*genMag + (x - genLo);
|
||||
randNatAux (r' / genMag - 1) (v', g')
|
||||
| 0, (v, g) => (v, g)
|
||||
| r'@(r+1), (v, g) =>
|
||||
let (x, g') := RandomGen.next g
|
||||
let v' := v*genMag + (x - genLo)
|
||||
randNatAux genLo genMag (r' / genMag - 1) (v', g')
|
||||
|
||||
/-- Generate a random natural number in the interval [lo, hi]. -/
|
||||
def randNat {gen : Type u} [RandomGen gen] (g : gen) (lo hi : Nat) : Nat × gen :=
|
||||
let lo' := if lo > hi then hi else lo;
|
||||
let hi' := if lo > hi then lo else hi;
|
||||
let (genLo, genHi) := RandomGen.range g;
|
||||
let genMag := genHi - genLo + 1;
|
||||
/-
|
||||
Probabilities of the most likely and least likely result
|
||||
will differ at most by a factor of (1 +- 1/q). Assuming the RandomGen
|
||||
is uniform, of course
|
||||
-/
|
||||
let q := 1000;
|
||||
let k := hi' - lo' + 1;
|
||||
let tgtMag := k * q;
|
||||
let (v, g') := randNatAux genLo genMag tgtMag (0, g);
|
||||
let v' := lo' + (v % k);
|
||||
(v', g')
|
||||
let lo' := if lo > hi then hi else lo
|
||||
let hi' := if lo > hi then lo else hi
|
||||
let (genLo, genHi) := RandomGen.range g
|
||||
let genMag := genHi - genLo + 1
|
||||
/-
|
||||
Probabilities of the most likely and least likely result
|
||||
will differ at most by a factor of (1 +- 1/q). Assuming the RandomGen
|
||||
is uniform, of course
|
||||
-/
|
||||
let q := 1000
|
||||
let k := hi' - lo' + 1
|
||||
let tgtMag := k * q
|
||||
let (v, g') := randNatAux genLo genMag tgtMag (0, g)
|
||||
let v' := lo' + (v % k)
|
||||
(v', g')
|
||||
|
||||
/-- Generate a random Boolean. -/
|
||||
def randBool {gen : Type u} [RandomGen gen] (g : gen) : Bool × gen :=
|
||||
let (v, g') := randNat g 0 1;
|
||||
(v = 1, g')
|
||||
let (v, g') := randNat g 0 1
|
||||
(v = 1, g')
|
||||
|
||||
def IO.mkStdGenRef : IO (IO.Ref StdGen) :=
|
||||
IO.mkRef mkStdGen
|
||||
|
||||
@[init IO.mkStdGenRef]
|
||||
constant IO.stdGenRef : IO.Ref StdGen := arbitrary _
|
||||
initialize IO.stdGenRef : IO.Ref StdGen ← IO.mkRef mkStdGen
|
||||
|
||||
def IO.setRandSeed (n : Nat) : IO Unit :=
|
||||
IO.stdGenRef.set (mkStdGen n)
|
||||
IO.stdGenRef.set (mkStdGen n)
|
||||
|
||||
def IO.rand (lo hi : Nat) : IO Nat := do
|
||||
gen ← IO.stdGenRef.get;
|
||||
let (r, gen) := randNat gen lo hi;
|
||||
IO.stdGenRef.set gen;
|
||||
pure r
|
||||
let gen ← IO.stdGenRef.get
|
||||
let (r, gen) := randNat gen lo hi
|
||||
IO.stdGenRef.set gen
|
||||
pure r
|
||||
|
|
|
|||
|
|
@ -1,3 +1,4 @@
|
|||
#lang lean4
|
||||
/-
|
||||
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
|
@ -14,95 +15,97 @@ open Sum Subtype Nat
|
|||
universes u v
|
||||
|
||||
class HasToString (α : Type u) :=
|
||||
(toString : α → String)
|
||||
(toString : α → String)
|
||||
|
||||
export HasToString (toString)
|
||||
|
||||
-- This instance is needed because `id` is not reducible
|
||||
instance {α} [HasToString α] : HasToString (id α) :=
|
||||
inferInstanceAs (HasToString α)
|
||||
inferInstanceAs (HasToString α)
|
||||
|
||||
instance {α} [HasToString α] : HasToString (Id α) :=
|
||||
inferInstanceAs (HasToString α)
|
||||
inferInstanceAs (HasToString α)
|
||||
|
||||
instance : HasToString String :=
|
||||
⟨fun s => s⟩
|
||||
⟨fun s => s⟩
|
||||
|
||||
instance : HasToString Substring :=
|
||||
⟨fun s => s.toString⟩
|
||||
⟨fun s => s.toString⟩
|
||||
|
||||
instance : HasToString String.Iterator :=
|
||||
⟨fun it => it.remainingToString⟩
|
||||
⟨fun it => it.remainingToString⟩
|
||||
|
||||
instance : HasToString Bool :=
|
||||
⟨fun b => cond b "true" "false"⟩
|
||||
⟨fun b => cond b "true" "false"⟩
|
||||
|
||||
instance {p : Prop} : HasToString (Decidable p) :=
|
||||
⟨fun h => match h with
|
||||
instance {p : Prop} : HasToString (Decidable p) := ⟨fun h =>
|
||||
match h with
|
||||
| Decidable.isTrue _ => "true"
|
||||
| Decidable.isFalse _ => "false"⟩
|
||||
|
||||
protected def List.toStringAux {α : Type u} [HasToString α] : Bool → List α → String
|
||||
| b, [] => ""
|
||||
| true, x::xs => toString x ++ List.toStringAux false xs
|
||||
| false, x::xs => ", " ++ toString x ++ List.toStringAux false xs
|
||||
| b, [] => ""
|
||||
| true, x::xs => toString x ++ List.toStringAux false xs
|
||||
| false, x::xs => ", " ++ toString x ++ List.toStringAux false xs
|
||||
|
||||
protected def List.toString {α : Type u} [HasToString α] : List α → String
|
||||
| [] => "[]"
|
||||
| x::xs => "[" ++ List.toStringAux true (x::xs) ++ "]"
|
||||
| [] => "[]"
|
||||
| x::xs => "[" ++ List.toStringAux true (x::xs) ++ "]"
|
||||
|
||||
instance {α : Type u} [HasToString α] : HasToString (List α) :=
|
||||
⟨List.toString⟩
|
||||
⟨List.toString⟩
|
||||
|
||||
instance : HasToString PUnit.{u+1} :=
|
||||
⟨fun _ => "()"⟩
|
||||
⟨fun _ => "()"⟩
|
||||
|
||||
instance {α : Type u} [HasToString α] : HasToString (ULift.{v} α) :=
|
||||
⟨fun v => toString v.1⟩
|
||||
⟨fun v => toString v.1⟩
|
||||
|
||||
instance : HasToString Unit :=
|
||||
⟨fun u => "()"⟩
|
||||
⟨fun u => "()"⟩
|
||||
|
||||
instance : HasToString Nat :=
|
||||
⟨fun n => repr n⟩
|
||||
⟨fun n => repr n⟩
|
||||
|
||||
instance : HasToString Char :=
|
||||
⟨fun c => c.toString⟩
|
||||
⟨fun c => c.toString⟩
|
||||
|
||||
instance (n : Nat) : HasToString (Fin n) :=
|
||||
⟨fun f => toString (Fin.val f)⟩
|
||||
⟨fun f => toString (Fin.val f)⟩
|
||||
|
||||
instance : HasToString UInt8 :=
|
||||
⟨fun n => toString n.toNat⟩
|
||||
⟨fun n => toString n.toNat⟩
|
||||
|
||||
instance : HasToString UInt16 :=
|
||||
⟨fun n => toString n.toNat⟩
|
||||
⟨fun n => toString n.toNat⟩
|
||||
|
||||
instance : HasToString UInt32 :=
|
||||
⟨fun n => toString n.toNat⟩
|
||||
⟨fun n => toString n.toNat⟩
|
||||
|
||||
instance : HasToString UInt64 :=
|
||||
⟨fun n => toString n.toNat⟩
|
||||
⟨fun n => toString n.toNat⟩
|
||||
|
||||
instance : HasToString USize :=
|
||||
⟨fun n => toString n.toNat⟩
|
||||
⟨fun n => toString n.toNat⟩
|
||||
|
||||
def addParenHeuristic (s : String) : String :=
|
||||
if "(".isPrefixOf s || "[".isPrefixOf s || "{".isPrefixOf s || "#[".isPrefixOf s then s
|
||||
else if !s.any Char.isWhitespace then s
|
||||
else "(" ++ s ++ ")"
|
||||
if "(".isPrefixOf s || "[".isPrefixOf s || "{".isPrefixOf s || "#[".isPrefixOf s then s
|
||||
else if !s.any Char.isWhitespace then s
|
||||
else "(" ++ s ++ ")"
|
||||
|
||||
instance {α : Type u} [HasToString α] : HasToString (Option α) :=
|
||||
⟨fun o => match o with | none => "none" | (some a) => "(some " ++ addParenHeuristic (toString a) ++ ")"⟩
|
||||
instance {α : Type u} [HasToString α] : HasToString (Option α) := ⟨fun
|
||||
| none => "none"
|
||||
| (some a) => "(some " ++ addParenHeuristic (toString a) ++ ")"⟩
|
||||
|
||||
instance {α : Type u} {β : Type v} [HasToString α] [HasToString β] : HasToString (Sum α β) :=
|
||||
⟨fun s => match s with | (inl a) => "(inl " ++ addParenHeuristic (toString a) ++ ")" | (inr b) => "(inr " ++ addParenHeuristic (toString b) ++ ")"⟩
|
||||
instance {α : Type u} {β : Type v} [HasToString α] [HasToString β] : HasToString (Sum α β) := ⟨fun
|
||||
| (inl a) => "(inl " ++ addParenHeuristic (toString a) ++ ")"
|
||||
| (inr b) => "(inr " ++ addParenHeuristic (toString b) ++ ")"⟩
|
||||
|
||||
instance {α : Type u} {β : Type v} [HasToString α] [HasToString β] : HasToString (α × β) :=
|
||||
⟨fun ⟨a, b⟩ => "(" ++ toString a ++ ", " ++ toString b ++ ")"⟩
|
||||
instance {α : Type u} {β : Type v} [HasToString α] [HasToString β] : HasToString (α × β) := ⟨fun (a, b) =>
|
||||
"(" ++ toString a ++ ", " ++ toString b ++ ")"⟩
|
||||
|
||||
instance {α : Type u} {β : α → Type v} [HasToString α] [s : ∀ x, HasToString (β x)] : HasToString (Sigma β) :=
|
||||
⟨fun ⟨a, b⟩ => "⟨" ++ toString a ++ ", " ++ toString b ++ "⟩"⟩
|
||||
instance {α : Type u} {β : α → Type v} [HasToString α] [s : ∀ x, HasToString (β x)] : HasToString (Sigma β) := ⟨fun ⟨a, b⟩ =>
|
||||
"⟨" ++ toString a ++ ", " ++ toString b ++ "⟩"⟩
|
||||
|
||||
instance {α : Type u} {p : α → Prop} [HasToString α] : HasToString (Subtype p) :=
|
||||
⟨fun s => toString (val s)⟩
|
||||
instance {α : Type u} {p : α → Prop} [HasToString α] : HasToString (Subtype p) := ⟨fun s =>
|
||||
toString (val s)⟩
|
||||
|
|
|
|||
|
|
@ -1,3 +1,4 @@
|
|||
#lang lean4
|
||||
/-
|
||||
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
|
@ -6,7 +7,6 @@ Author: Leonardo de Moura
|
|||
prelude
|
||||
import Init.LeanInit
|
||||
import Init.Data.ToString.Basic
|
||||
new_frontend
|
||||
|
||||
syntax:max "s!" (interpolatedStr term) : term
|
||||
|
||||
|
|
|
|||
|
|
@ -1,3 +1,4 @@
|
|||
#lang lean4
|
||||
/-
|
||||
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
|
@ -10,76 +11,59 @@ import Init.Data.ToString.Basic
|
|||
universes u v
|
||||
/- debugging helper functions -/
|
||||
@[neverExtract, extern "lean_dbg_trace"]
|
||||
def dbgTrace {α : Type u} (s : String) (f : Unit → α) : α :=
|
||||
f ()
|
||||
def dbgTrace {α : Type u} (s : String) (f : Unit → α) : α := f ()
|
||||
|
||||
def dbgTraceVal {α : Type u} [HasToString α] (a : α) : α :=
|
||||
dbgTrace (toString a) (fun _ => a)
|
||||
dbgTrace (toString a) (fun _ => a)
|
||||
|
||||
/- Display the given message if `a` is shared, that is, RC(a) > 1 -/
|
||||
@[neverExtract, extern "lean_dbg_trace_if_shared"]
|
||||
def dbgTraceIfShared {α : Type u} (s : String) (a : α) : α :=
|
||||
a
|
||||
def dbgTraceIfShared {α : Type u} (s : String) (a : α) : α := a
|
||||
|
||||
@[extern "lean_dbg_sleep"]
|
||||
def dbgSleep {α : Type u} (ms : UInt32) (f : Unit → α) : α :=
|
||||
f ()
|
||||
def dbgSleep {α : Type u} (ms : UInt32) (f : Unit → α) : α := f ()
|
||||
|
||||
@[extern c inline "#3"]
|
||||
unsafe def unsafeCast {α : Type u} {β : Type v} (a : α) : β :=
|
||||
cast lcProof (PUnit.{v})
|
||||
cast lcProof (PUnit.{v})
|
||||
|
||||
@[neverExtract, extern "lean_panic_fn"]
|
||||
constant panic {α : Type u} [Inhabited α] (msg : String) : α := arbitrary _
|
||||
constant panic {α : Type u} [Inhabited α] (msg : String) : α
|
||||
|
||||
@[noinline] private def mkPanicMessage (modName : String) (line col : Nat) (msg : String) : String :=
|
||||
"PANIC at " ++ modName ++ ":" ++ toString line ++ ":" ++ toString col ++ ": " ++ msg
|
||||
"PANIC at " ++ modName ++ ":" ++ toString line ++ ":" ++ toString col ++ ": " ++ msg
|
||||
|
||||
@[neverExtract, inline] def panicWithPos {α : Type u} [Inhabited α] (modName : String) (line col : Nat) (msg : String) : α :=
|
||||
panic (mkPanicMessage modName line col msg)
|
||||
panic (mkPanicMessage modName line col msg)
|
||||
|
||||
@[noinline] private def mkPanicMessageWithDecl (modName : String) (declName : String) (line col : Nat) (msg : String) : String :=
|
||||
"PANIC at " ++ declName ++ " " ++ modName ++ ":" ++ toString line ++ ":" ++ toString col ++ ": " ++ msg
|
||||
"PANIC at " ++ declName ++ " " ++ modName ++ ":" ++ toString line ++ ":" ++ toString col ++ ": " ++ msg
|
||||
|
||||
@[neverExtract, inline] def panicWithPosWithDecl {α : Type u} [Inhabited α] (modName : String) (declName : String) (line col : Nat) (msg : String) : α :=
|
||||
panic (mkPanicMessageWithDecl modName declName line col msg)
|
||||
panic (mkPanicMessageWithDecl modName declName line col msg)
|
||||
|
||||
-- TODO: should be a macro
|
||||
@[neverExtract, noinline, nospecialize] def unreachable! {α : Type u} [Inhabited α] : α :=
|
||||
panic! "unreachable"
|
||||
-- TODO: delete after we delete old frontend
|
||||
@[neverExtract, noinline, nospecialize] def «unreachable!» {α : Type u} [Inhabited α] : α :=
|
||||
panic! "unreachable"
|
||||
|
||||
@[extern "lean_ptr_addr"]
|
||||
unsafe def ptrAddrUnsafe {α : Type u} (a : @& α) : USize := 0
|
||||
|
||||
@[inline] unsafe def withPtrAddrUnsafe {α : Type u} {β : Type v} (a : α) (k : USize → β) (h : ∀ u₁ u₂, k u₁ = k u₂) : β :=
|
||||
k (ptrAddrUnsafe a)
|
||||
k (ptrAddrUnsafe a)
|
||||
|
||||
@[inline] unsafe def withPtrEqUnsafe {α : Type u} (a b : α) (k : Unit → Bool) (h : a = b → k () = true) : Bool :=
|
||||
if ptrAddrUnsafe a == ptrAddrUnsafe b then true else k ()
|
||||
|
||||
inductive PtrEqResult {α : Type u} (x y : α) : Type
|
||||
| unknown : PtrEqResult
|
||||
| yesEqual (h : x = y) : PtrEqResult
|
||||
|
||||
@[inline] unsafe def withPtrEqResultUnsafe {α : Type u} {β : Type v} [Subsingleton β] (a b : α) (k : PtrEqResult a b → β) : β :=
|
||||
if ptrAddrUnsafe a == ptrAddrUnsafe b then k (PtrEqResult.yesEqual lcProof) else k PtrEqResult.unknown
|
||||
if ptrAddrUnsafe a == ptrAddrUnsafe b then true else k ()
|
||||
|
||||
@[implementedBy withPtrEqUnsafe]
|
||||
def withPtrEq {α : Type u} (a b : α) (k : Unit → Bool) (h : a = b → k () = true) : Bool :=
|
||||
k ()
|
||||
def withPtrEq {α : Type u} (a b : α) (k : Unit → Bool) (h : a = b → k () = true) : Bool := k ()
|
||||
|
||||
/-- `withPtrEq` for `DecidableEq` -/
|
||||
@[inline] def withPtrEqDecEq {α : Type u} (a b : α) (k : Unit → Decidable (a = b)) : Decidable (a = b) :=
|
||||
let b := withPtrEq a b (fun _ => toBoolUsing (k ())) (toBoolUsingEqTrue (k ()));
|
||||
condEq b
|
||||
(fun h => isTrue (ofBoolUsingEqTrue h))
|
||||
(fun h => isFalse (ofBoolUsingEqFalse h))
|
||||
|
||||
/-- Similar to `withPtrEq`, but executes the continuation `k` with the "result" of the pointer equality test. -/
|
||||
@[implementedBy withPtrEqResultUnsafe]
|
||||
def withPtrEqResult {α : Type u} {β : Type v} [Subsingleton β] (a b : α) (k : PtrEqResult a b → β) : β :=
|
||||
k PtrEqResult.unknown
|
||||
let b := withPtrEq a b (fun _ => toBoolUsing (k ())) (toBoolUsingEqTrue (k ()));
|
||||
condEq b
|
||||
(fun h => isTrue (ofBoolUsingEqTrue h))
|
||||
(fun h => isFalse (ofBoolUsingEqFalse h))
|
||||
|
||||
@[implementedBy withPtrAddrUnsafe]
|
||||
def withPtrAddr {α : Type u} {β : Type v} (a : α) (k : USize → β) (h : ∀ u₁ u₂, k u₁ = k u₂) : β :=
|
||||
k 0
|
||||
def withPtrAddr {α : Type u} {β : Type v} (a : α) (k : USize → β) (h : ∀ u₁ u₂, k u₁ = k u₂) : β := k 0
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue