sax_dependent_types.rs

//! 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
}

streaming_elaborator.md

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);
    }
}