From 7030dc91f2d1013acfaa7be62442355e4a7ca11a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 23 Oct 2020 12:19:22 -0700 Subject: [PATCH] chore: move to new frontend --- src/Init/Control/Except.lean | 202 +++++++++++++++--------------- src/Init/Control/Reader.lean | 101 +++++++-------- src/Init/Control/State.lean | 144 ++++++++++----------- src/Init/Data/Array/Basic.lean | 3 + src/Init/Data/Random.lean | 146 ++++++++++----------- src/Init/Data/ToString/Basic.lean | 81 ++++++------ src/Init/Data/ToString/Macro.lean | 2 +- src/Init/Util.lean | 60 ++++----- 8 files changed, 371 insertions(+), 368 deletions(-) diff --git a/src/Init/Control/Except.lean b/src/Init/Control/Except.lean index 679f1d610b..29ab1fafb7 100644 --- a/src/Init/Control/Except.lean +++ b/src/Init/Control/Except.lean @@ -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) +} diff --git a/src/Init/Control/Reader.lean b/src/Init/Control/Reader.lean index 4306ad1011..369c70465f 100644 --- a/src/Init/Control/Reader.lean +++ b/src/Init/Control/Reader.lean @@ -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 diff --git a/src/Init/Control/State.lean b/src/Init/Control/State.lean index 7b9c4a7989..ca81c3bbce 100644 --- a/src/Init/Control/State.lean +++ b/src/Init/Control/State.lean @@ -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'') +} diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index 0de0bdb4b7..7c03595362 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -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 diff --git a/src/Init/Data/Random.lean b/src/Init/Data/Random.lean index 76fe642730..dc5c1ee404 100644 --- a/src/Init/Data/Random.lean +++ b/src/Init/Data/Random.lean @@ -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 diff --git a/src/Init/Data/ToString/Basic.lean b/src/Init/Data/ToString/Basic.lean index 65c19eb13c..7405a56b4d 100644 --- a/src/Init/Data/ToString/Basic.lean +++ b/src/Init/Data/ToString/Basic.lean @@ -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)⟩ diff --git a/src/Init/Data/ToString/Macro.lean b/src/Init/Data/ToString/Macro.lean index e60e6f0d9f..e7bed997ff 100644 --- a/src/Init/Data/ToString/Macro.lean +++ b/src/Init/Data/ToString/Macro.lean @@ -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 diff --git a/src/Init/Util.lean b/src/Init/Util.lean index 7c4d1c8483..d43a6476ae 100644 --- a/src/Init/Util.lean +++ b/src/Init/Util.lean @@ -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