leodemoura

import Lean

opaque g (n : Nat) : Nat

@[simp] def f (i n m : Nat) :=
  if i < n then
    f (i+1) n (g m)
  else
    m
termination_by n - i

leodemoura

import Std.Data.HashMap

open Std

/-
In Lean, a hash map has type

def HashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] :=
  ...

leodemoura

/-
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
-/
prelude
import init.core init.data.nat.basic
open Decidable List

universes u v w

leodemoura

static object * map1(object * l) {
    if (obj_tag(l) == 0) {
        return l;
    } else {
        object * h     = cnstr_obj(l, 0);
        object * t     = cnstr_obj(l, 1);
        object * new_h = box(unbox(h) + 1);
        object * new_t = map1(t);
        object * r     = alloc_cnstr(1, 2, 0);

leodemoura

import system.io 

universes u v w r 

/-- 
   Asymmetric coroutines `coroutine α δ β` takes inputs of type `α`, yields elements of type `δ`,
   and produces an element of type `β`. 

   Asymmetric coroutines are so called because they involve two types of control transfer operations:
   one for resuming/invoking a coroutine and one for suspending it, the latter returning

leodemoura

universes u v w

structure maybe_t (m : Type u → Type v) (α : Type u) :=
(run : Π {β : Type u}, (α → m β) → (unit → m β) → m β)

section
variables {m : Type u → Type v} {α β : Type u}

def maybe_t.return (a : α) : maybe_t m α :=
⟨λ _ k₁ k₂, k₁ a⟩

leodemoura

universes u v

@[reducible] def partial.fuel := nat
private def partial.huge := 1000

/- Remark: I could not use (reader_t partial.fuel (except unit α)) because of universe
   constraints. `partial.fuel` is at (Type 0), but α is in (Type u) -/
structure partial (α : Type u) :=
(run_prv : partial.fuel → except unit α) -- TODO: mark as private
/-

leodemoura

universes u v w

class monad_state' (σ : Type u) (m : Type u → Type v) :=
(lift {} {α : Type u} : state σ α → m α)

section
variables {σ : Type u} {m : Type u → Type v}

instance ss' [s : monad_state σ m] : monad_state' σ m :=
{lift := @monad_state.lift _ _ _}

leodemoura

import system.io

variables {δ ε ρ σ α : Type}
/-
- δ : backtrackable state
- ε : exception type
- ρ : environment
- σ : non backtrackable state
-/

leodemoura

universes u

def eff (effs : list ((Type u → Type u) → Type u → Type u)) : Type u → Type u :=
effs.foldr ($) id

section
local attribute [reducible] eff list.foldr
variables {ε ρ σ : Type u}

instance eff.m1 : monad $ eff [except_t ε, reader_t ρ, state_t σ] := infer_instance