This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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⟩ |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 | |
/- |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 _ _ _} |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
import system.io | |
variables {δ ε ρ σ α : Type} | |
/- | |
- δ : backtrackable state | |
- ε : exception type | |
- ρ : environment | |
- σ : non backtrackable state | |
-/ |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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) |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
/- `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. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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) |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |