import Do.Mut

Early Return

open Lean

/- Disable the automatic monadic lifting feature described in the paper.
   We want to make it clear that we do not depend on it. -/
set_option autoLift false

def 
runCatch: {m : Type u_1 → Type u_2} → {α : Type u_1} → [inst : Monad m] → ExceptT α m α → m α
runCatch [
Monad: (Type ?u.9 → Type ?u.8) → Type (max (?u.9 + 1) ?u.8)
Monad 
m: Type u_1 → Type u_2
m] (
x: ExceptT α m α
x : 
ExceptT: Type u_1 → (Type u_1 → Type u_2) → Type u_1 → Type u_2
ExceptT 
α: Type u_1
α 
m: Type u_1 → Type u_2
m 
α: Type u_1
α) : 
m: Type u_1 → Type u_2
m 
α: Type u_1
α :=
  
ExceptT.run: {ε : Type u_1} → {m : Type u_1 → Type u_2} → {α : Type u_1} → ExceptT ε m α → m (Except ε α)
ExceptT.run 
x: ExceptT α m α
x >>= fun
    | 
Except.ok: {ε : Type ?u.57} → {α : Type ?u.56} → α → Except ε α
Except.ok 
x: α
x => 
pure: {f : Type u_1 → Type u_2} → [self : Pure f] → {α : Type u_1} → α → f α
pure 
x: α
x
    | 
Except.error: {ε : Type ?u.115} → {α : Type ?u.114} → ε → Except ε α
Except.error 
e: α
e => 
pure: {f : Type u_1 → Type u_2} → [self : Pure f] → {α : Type u_1} → α → f α
pure 
e: α
e

/-- Count syntax nodes satisfying `p`. -/
partial def 
Lean.Syntax.count: Syntax → (Syntax → Bool) → Nat
Lean.Syntax.count (
stx: Syntax
stx : 
Syntax: Type
Syntax) (
p: Syntax → Bool
p : 
Syntax: Type
Syntax → 
Bool: Type
Bool) : 
Nat: Type
Nat :=
  
stx: Syntax
stx.
getArgs: Syntax → Array Syntax
getArgs.
foldl: {α β : Type} → (β → α → β) → β → (as : Array α) → optParam Nat 0 → optParam Nat (Array.size as) → β
foldl (fun 
n: Nat
n 
arg: Syntax
arg => 
n: Nat
n + 
arg: Syntax
arg.
count: Syntax → (Syntax → Bool) → Nat
count 
p: Syntax → Bool
p) (if 
p: Syntax → Bool
p 
stx: Syntax
stx then 
1: Nat
1 else 
0: Nat
0)

syntax "return" term : stmt

syntax "return" : expander

macro_rules
  | `(do' $
s: TSyntax `stmt
s) => do  -- (1')
    -- optimization: fall back to original rule (1) if now `return` statement was expanded
    let 
s': TSyntax `stmt
s' ← 
expandStmt: TSyntax `stmt → MacroM (TSyntax `stmt)
expandStmt 
(← `(stmt| expand! return in $s)): TSyntax `stmt
(← `(stmt| 
(← `(stmt| expand! return in $s)): TSyntax `stmt
expand!
(← `(stmt| expand! return in $s)): TSyntax `stmt
 
(← `(stmt| expand! return in $s)): TSyntax `stmt
return
(← `(stmt| expand! return in $s)): TSyntax `stmt
 
(← `(stmt| expand! return in $s)): TSyntax `stmt
in
(← `(stmt| expand! return in $s)): TSyntax `stmt
 $
s: TSyntax `stmt
s
(← `(stmt| expand! return in $s)): TSyntax `stmt
))
    if 
s': TSyntax `stmt
s'.
raw: {ks : SyntaxNodeKinds} → TSyntax ks → Syntax
raw.
count: Syntax → (Syntax → Bool) → Nat
count (· matches `(stmt| return $_)) == 
s: TSyntax `stmt
s.
raw: {ks : SyntaxNodeKinds} → TSyntax ks → Syntax
raw.
count: Syntax → (Syntax → Bool) → Nat
count (· matches `(stmt| return $_)) then
      `(d! $
s: TSyntax `stmt
s)
    else
      `(ExceptCpsT.runCatch (d! $
s': TSyntax `stmt
s'))

macro_rules
  | `(stmt| expand! return in return $
e: TSyntax `term
e) => `(stmt| throw $
e: TSyntax `term
e)          -- (R1)
  | `(stmt| expand! return in $
e: TSyntax `term
e:term) => `(stmt| ExceptCpsT.lift $
e: TSyntax `term
e)  -- (R2)

variable [
Monad: (Type ?u.3135 → Type ?u.3134) → Type (max (?u.3135 + 1) ?u.3134)
Monad 
m: Type ?u.2574 → Type ?u.2573
m]
variable (
ma: m α
ma 
ma': m α
ma' : 
m: Type ?u.2585 → Type ?u.2584
m 
α: Type ?u.2585
α)
variable (
b: Bool
b : 
Bool: Type
Bool)


example: ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] (ma : m α) [inst_1 : LawfulMonad m],
  (ExceptCpsT.runCatch do
      let x ← ExceptCpsT.lift ma
      throw x) =
    ma
example [
LawfulMonad: (m : Type u_1 → Type u_2) → [inst : Monad m] → Prop
LawfulMonad 
m: Type u_1 → Type u_2
m] :
    (do' let 
x: α
x ← 
ma: m α
ma;
         return 
x: α
x)
    = 
ma: m α
ma
:= 
m: Type ?u.2639 → Type ?u.2638
α: Type ?u.2639
inst✝¹: Monad m
ma, ma': m α
b: Bool
(ExceptCpsT.runCatch do
    let x ← ExceptCpsT.lift ma
    throw x) =
  ma
 
Goals accomplished! 🐙



example: Id.run
    (ExceptCpsT.runCatch do
      let x ← ExceptCpsT.lift (pure 1)
      throw x) =
  1
example : 
Id.run: {α : Type} → Id α → α
Id.run
    (do' let 
x: Nat
x := 
1: Nat
1; return 
x: Nat
x)
    = 
1: Nat
1
:= 
rfl: ∀ {α : Type} {a : α}, a = a
rfl


example: ∀ {m : Type → Type u_1} {α : Type} [inst : Monad m] (ma ma' : m α) (b : Bool) [inst_1 : LawfulMonad m],
  (ExceptCpsT.runCatch do
      if b = true then do
          let x ← ExceptCpsT.lift ma
          throw x
        else ExceptCpsT.lift (pure ())
      ExceptCpsT.lift ma') =
    if b = true then ma else ma'
example [
LawfulMonad: (m : Type → Type u_1) → [inst : Monad m] → Prop
LawfulMonad 
m: Type → Type u_1
m] :
     (do' if 
b: Bool
b then {
            let 
x: α
x ← 
ma: m α
ma;
            return 
x: α
x
          };
          
ma': m α
ma')
     =
     (if 
b: Bool
b then 
ma: m α
ma else 
ma': m α
ma')
:= 
m: Type → Type ?u.3364
α: Type
inst✝¹: Monad m
ma, ma': m α
b: Bool
(ExceptCpsT.runCatch do
    if b = true then do
        let x ← ExceptCpsT.lift ma
        throw x
      else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift ma') =
  if b = true then ma else ma'
 
m: Type → Type ?u.3364
α: Type
inst✝¹: Monad m
ma, ma': m α
false
(ExceptCpsT.runCatch do
    if false = true then do
        let x ← ExceptCpsT.lift ma
        throw x
      else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift ma') =
  if false = true then ma else ma'
m: Type → Type ?u.3364
α: Type
inst✝¹: Monad m
ma, ma': m α
(ExceptCpsT.runCatch do
    if true = true then do
        let x ← ExceptCpsT.lift ma
        throw x
      else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift ma') =
  if true = true then ma else ma'
 
m: Type → Type ?u.3364
α: Type
inst✝¹: Monad m
ma, ma': m α
false
(ExceptCpsT.runCatch do
    if false = true then do
        let x ← ExceptCpsT.lift ma
        throw x
      else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift ma') =
  if false = true then ma else ma'
m: Type → Type ?u.3364
α: Type
inst✝¹: Monad m
ma, ma': m α
(ExceptCpsT.runCatch do
    if true = true then do
        let x ← ExceptCpsT.lift ma
        throw x
      else ExceptCpsT.lift (pure ())
    ExceptCpsT.lift ma') =
  if true = true then ma else ma'
 
Goals accomplished! 🐙



example: ∀ {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] (ma ma' : m α) (b : Bool) [inst_1 : LawfulMonad m],
  (ExceptCpsT.runCatch do
      let y ←
        if b = true then do
            let x ← ExceptCpsT.lift ma
            throw x
          else ExceptCpsT.lift ma'
      ExceptCpsT.lift (pure y)) =
    if b = true then ma else ma'
example [
LawfulMonad: (m : Type u_1 → Type u_2) → [inst : Monad m] → Prop
LawfulMonad 
m: Type u_1 → Type u_2
m] :
    (do' let 
y: α
y ←
           if 
b: Bool
b then {
             let 
x: α
x ← 
ma: m α
ma;
             return 
x: α
x
           } else {
             
ma': m α
ma'
           };
         
pure: {f : Type u_1 → Type u_2} → [self : Pure f] → {α : Type u_1} → α → f α
pure 
y: α
y)
    =
    (if 
b: Bool
b then 
ma: m α
ma else 
ma': m α
ma')
:= 
m: Type ?u.4867 → Type ?u.4866
α: Type ?u.4867
inst✝¹: Monad m
ma, ma': m α
b: Bool
(ExceptCpsT.runCatch do
    let y ←
      if b = true then do
          let x ← ExceptCpsT.lift ma
          throw x
        else ExceptCpsT.lift ma'
    ExceptCpsT.lift (pure y)) =
  if b = true then ma else ma'
 
m: Type ?u.4867 → Type ?u.4866
α: Type ?u.4867
inst✝¹: Monad m
ma, ma': m α
false
(ExceptCpsT.runCatch do
    let y ←
      if false = true then do
          let x ← ExceptCpsT.lift ma
          throw x
        else ExceptCpsT.lift ma'
    ExceptCpsT.lift (pure y)) =
  if false = true then ma else ma'
m: Type ?u.4867 → Type ?u.4866
α: Type ?u.4867
inst✝¹: Monad m
ma, ma': m α
(ExceptCpsT.runCatch do
    let y ←
      if true = true then do
          let x ← ExceptCpsT.lift ma
          throw x
        else ExceptCpsT.lift ma'
    ExceptCpsT.lift (pure y)) =
  if true = true then ma else ma'
 
m: Type ?u.4867 → Type ?u.4866
α: Type ?u.4867
inst✝¹: Monad m
ma, ma': m α
false
(ExceptCpsT.runCatch do
    let y ←
      if false = true then do
          let x ← ExceptCpsT.lift ma
          throw x
        else ExceptCpsT.lift ma'
    ExceptCpsT.lift (pure y)) =
  if false = true then ma else ma'
m: Type ?u.4867 → Type ?u.4866
α: Type ?u.4867
inst✝¹: Monad m
ma, ma': m α
(ExceptCpsT.runCatch do
    let y ←
      if true = true then do
          let x ← ExceptCpsT.lift ma
          throw x
        else ExceptCpsT.lift ma'
    ExceptCpsT.lift (pure y)) =
  if true = true then ma else ma'
 
Goals accomplished! 🐙