Skip to content

Instantly share code, notes, and snippets.

View leodemoura's full-sized avatar

Leonardo de Moura leodemoura

View GitHub Profile
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
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⟩
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
/-
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 _ _ _}
import system.io
variables {δ ε ρ σ α : Type}
/-
- δ : backtrackable state
- ε : exception type
- ρ : environment
- σ : non backtrackable state
-/
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
def {u} run_state {σ : Type u} (m : Type u → Type u) {n n' : Type u → Type u} {α : Type u} [monad_functor_t (state_t σ m) m n n'] [monad n] [monad_state σ n] [monad m]
(x : n α) (st : σ) : n' (α × σ) :=
monad_map (λ α (x : state_t σ m α), prod.fst <$> x.run st) (prod.mk <$> x <*> get)
def {u} run_reader {ρ : Type u} (m : Type u → Type u) {n n' : Type u → Type u} {α : Type u} [monad_functor_t (reader_t ρ m) m n n'] [monad n] [monad_reader ρ n] [monad m]
(x : n α) (env : ρ) : n' α :=
monad_map (λ α (x : reader_t ρ m α), x.run env) x
structure eff_types :=
(ε : option Type := none)
/- `unpack` will be a hint to the code generator.
It is similar to the Haskell `unpack` annotation. -/
@[reducible] def {u} unpack (t : Type u) := t
structure term_app (term : Type) :=
(depth : nat) (hash : nat) (fn : term) (arg : term)
/- When implementing `expr`, `hash` will be an `uint32`.
For `depth`, it is not clear what we should do.
The C++ implementation uses `uint32`, and relies on the fact
that will we will probably run out of memory before producing an overflow here.
universes u
/-
Existential types in Haskell can be used to simulate
object-oriented virtual dispatch tables.
First we define a type class for the dispatch table.
-/
class shape_vtable (α : Type u) :=
(perimeter : α → nat)
universes u
inductive term
| app : term → term → term
| var : nat → term
/--
Given `@use_ptr_eq _ a b r`, the compiler generates the following code
if addr_of(a) = addr_of(b) then