Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
//! Dependent type system that uses a SAX-style event streams between passes.
//!
//! It would be really neat to have a simple state machine language to describe this.
/// Handler for a state machine that accepts input events.
trait InputHandler {
fn on_bytes(self, bytes: &[u8]>);
fn on_list_start(self);
fn on_list_end(self);
}
/// Handler for a state machine that accepts diagnostic events.
trait DiagnosticHandler {
// TODO: severity?
// TODO: position information?
fn on_diagnostic(self, message: &str);
}
/// Handler for a state machine that accepts Core events.
trait CoreHandler {
fn on_universe(self);
fn on_variable(self, name: String);
fn on_let(self /*, TODO */);
fn on_function_type(self /*, TODO */);
fn on_function_term(self /*, TODO */);
fn on_function_elim(self /*, TODO */);
fn on_record_type(self /*, TODO */);
fn on_record_term(self /*, TODO */);
fn on_record_elim(self /*, TODO */);
fn on_equal_type(self /*, TODO */);
fn on_equal_term(self /*, TODO */);
fn on_equal_elim(self /*, TODO */);
}
/// Handler for a state machine that accepts A-Normal Form events.
trait AnfHandler {
// TODO
}
/// Handler for a state machine that accepts Closure Converted events.
trait CcHandler {
// TODO
}
trait WasmHandler {
// TODO
}
mod input_to_term {
//! State machine that converts input events into core events.
use super::*;
enum State {
Top,
Term,
Universe,
FunctionType,
FunctionTerm,
FunctionElim,
RecordType,
RecordTerm,
RecordElim,
EqualType,
EqualTerm,
EqualElim,
UnknownTerm,
}
pub struct Handler<D> {
downstream: D,
state: State,
}
impl<D> Handler<D> {
fn new(downstream: D) -> Handler<D> {
Handler {
downstream,
state: State::Top,
}
}
}
impl<D> InputHandler &mut Handler<D> where
&mut D: CoreHandler,
{
fn on_bytes(self, bytes: &[u8]) {
match (self.state, bytes.as_ref()) {
(State::Top, _) => {} // TODO: warn: "skipping top-level bytes"
(State::Term, b"universe") => self.state = State::Universe;
(State::Term, b"variable") => self.state = State::Variable;
(State::Term, b"function/type") => self.state = State::FunctionType;
(State::Term, b"function/term") => self.state = State::FunctionTerm;
(State::Term, b"function/elim") => self.state = State::FunctionElim;
(State::Term, b"record/type") => self.state = State::RecordType;
(State::Term, b"record/term") => self.state = State::RecordTerm;
(State::Term, b"record/elim") => self.state = State::RecordElim;
(State::Term, b"equal/type") => self.state = State::EqualType;
(State::Term, b"equal/term") => self.state = State::EqualTerm;
(State::Term, b"equal/elim") => self.state = State::EqualElim;
(State::Term, _) => self.state = State::UnknownTerm;
(State::Universe, _) => {}, // TODO: warn: "skipping"
(State::Variable, _) => {}, // TODO: warn: "skipping"
(State::FunctionType, _) => {}, // TODO: warn: "skipping"
(State::FunctionTerm, _) => {}, // TODO: warn: "skipping"
(State::FunctionElim, _) => {}, // TODO: warn: "skipping"
(State::RecordType, _) => {}, // TODO: warn: "skipping"
(State::RecordTerm, _) => {}, // TODO: warn: "skipping"
(State::RecordElim, _) => {}, // TODO: warn: "skipping"
(State::EqualType, _) => {}, // TODO: warn: "skipping"
(State::EqualTerm, _) => {}, // TODO: warn: "skipping"
(State::EqualElim, _) => {}, // TODO: warn: "skipping"
}
}
fn on_list_start(self) {
match self.state {
State::Top => self.state = State::Term,
State::Term => unimplemented!(), // TODO: warn: "skipping"
State::Universe => unimplemented!(), // TODO: warn: "skipping"
State::Variable => unimplemented!(),
State::FunctionType => unimplemented!(),
State::FunctionTerm => unimplemented!(),
State::FunctionElim => unimplemented!(),
State::RecordType => unimplemented!(),
State::RecordTerm => unimplemented!(),
State::RecordElim => unimplemented!(),
State::EqualType => unimplemented!(),
State::EqualTerm => unimplemented!(),
State::EqualElim => unimplemented!(),
}
}
fn on_list_end(self) {
match self.state {
State::Top => self.state = State::Term,
State::Term => unimplemented!(),
State::Universe => {
self.downstream.on_universe();
self.state = State::Top;
},
State::Variable => {
self.downstream.on_variable();
self.state = State::Top;
},
State::FunctionType => {
self.downstream.on_function_type();
self.state = State::Top;
},
State::FunctionTerm => {
self.downstream.on_function_term();
self.state = State::Top;
},
State::FunctionElim => {
self.downstream.on_function_elim();
self.state = State::Top;
},
State::RecordType => {
self.downstream.on_record_type();
self.state = State::Top;
},
State::RecordTerm => {
self.downstream.on_record_term();
self.state = State::Top;
},
State::RecordElim => {
self.downstream.on_record_elim();
self.state = State::Top;
},
State::EqualType => {
self.downstream.on_equal_type();
self.state = State::Top;
},
State::EqualTerm => {
self.downstream.on_equal_term();
self.state = State::Top;
},
State::EqualElim => {
self.downstream.on_equal_elim();
self.state = State::Top;
},
}
}
}
}
mod core_to_diagnostic {
//! State machine that converts core events into validation diagnostic events.
use super::*;
enum State {
Top,
}
enum Value {
Universe,
}
pub struct Handler<D> {
downstream: D,
state: State,
context: Vec<Value>,
}
impl<D> Handler<D> {
fn new(downstream: D) -> Handler<D> {
Handler {
downstream,
state: State::Top,
context: Vec::new(),
}
}
}
impl<D> CoreHandler &mut Handler<D> where
&mut D: DiagnosticHandler,
{
fn on_universe(self) {
unimplemented!() // TODO
}
fn on_variable(self, name: String) {
unimplemented!() // TODO
}
fn on_let(self /*, TODO */) {
unimplemented!() // TODO
}
fn on_function_type(self /*, TODO */) {
unimplemented!() // TODO
}
fn on_function_term(self /*, TODO */) {
unimplemented!() // TODO
}
fn on_function_elim(self /*, TODO */) {
unimplemented!() // TODO
}
fn on_record_type(self /*, TODO */) {
unimplemented!() // TODO
}
fn on_record_term(self /*, TODO */) {
unimplemented!() // TODO
}
fn on_record_elim(self /*, TODO */) {
unimplemented!() // TODO
}
fn on_equal_type(self /*, TODO */) {
unimplemented!() // TODO
}
fn on_equal_term(self /*, TODO */) {
unimplemented!() // TODO
}
fn on_equal_elim(self /*, TODO */) {
unimplemented!() // TODO
}
}
}
mod core_to_anf {
//! State machine that converts core events into anf events.
// TODO
}
mod anf_to_cc {
//! State machine that converts anf events into cc events.
// TODO
}
mod cc_to_wasm {
//! State machine that converts cc events into wasm events.
// TODO
}

implement using stream processing protocol for matching on streams and pulling out data forwards-compatible, extensible stream format with error recovery

elab/check context ty = {
    ... => ...
}

elab/synth context = {
    [:universe] => 
        {:term [:universe],
         :type [:universe]}
    [:variable {:name name}] =>
        [index type] <- lookup-ty name context
        {:term [:variable index],
         :type type}
    [:let {:items items, :body body}] =>
        ...

    [:function/type {:params params, :body body}] => ...
    [:function/term {:params params, :body body}] => ...
    [:function/elim {:head head, :arguments arguments}] => ...

    [:record/type ..] => ...
    [:record/term ..] => ...
    [:record/elim ..] => ...

    [:equal/type ..] => ...
    [:equal/term ..] => ...
    [:equal/elim ..] => ...
}
stream_match! {
    [Universe] => {
        yield {};
        yield bar;
        yield baz;
    [Variable { name: String }] => {
    }
}
use tokio::prelude::*;

use async_stream::stream;
use futures_util::pin_mut;

enum SExprEvent {
    NodeStart,
    NodeEnd,
    Leaf(Vec<u8>),
    RecoveryPoint,
}

enum TermEvent {
    Universe,
    Variable(String),
    Error,
}

fn s_exprs() -> impl Stream<Item = SExprEvent> {
    stream! {}
}

fn double<S: Stream<Item = SExprEvent>>(input: S)
    -> impl Stream<Item = u32>
{
    stream! {
        pin_mut!(input);
        while let Some(value) = input.next().await {
            match value {
                SExprEvent::NodeStart => match input.next().await {
                    Some(SExprEvent::Leaf(b"universe")) => yield TermEvent::Universe,
                    Some(SExprEvent::Leaf(b"variable")) => yield value * 2,
                    None => yield TermEvent::Error,
                },
                SExprEvent::NodeEnd => Leaf(data) => yield TermEvent::Error,
            }
        }
    }
}

#[tokio::main]
async fn main() {
    let s = s_exprs_to_terms(s_exprs()));
    pin_mut!(s); // needed for iteration

    while let Some(value) = s.next().await {
        println!("got {}", value);
    }
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.