Pull-based tree processing for lambda calculi.

pull-processing-syntax-trees.rs

//! See [this twitter thread](https://twitter.com/brendanzab/status/1191233778854662144).
//!
//! Traditional syntax trees suffer from lots of pointer indirections and poor data locality!
//! Could we stream things instead, using [pull-based events](http://www.xmlpull.org/history/index.html)
//! as opposed to trees? This should be equivalent to our tree based approaches, but might
//! require us to think carefully about what our core calculus looks like in order to make
//! this kind of thing easier.

use std::sync::Arc;

/// Types as a tree, for checkpointing.
#[derive(Clone, Debug)]
pub enum TypeTree {
    /// Base type.
    Base,
    /// Function type.
    Function {
        parameter_ty: Arc<TypeTree>,
        body_ty: Arc<TypeTree>,
    },
    /// Pair type.
    Pair {
        first_ty: Arc<TypeTree>,
        second_ty: Arc<TypeTree>,
    },
}

/// Terms in event form, for pull-based tree processing.
#[derive(Copy, Clone, Debug)]
pub enum TypeEvent {
    /// Base type.
    Base,
    /// Start a function type.
    FunctionStart,
    /// End a function type.
    FunctionEnd,
    /// Start a pair type.
    PairStart,
    /// End a pair type.
    PairEnd,
}

/// Terms as a tree, for checkpointing.
#[derive(Clone, Debug)]
pub enum TermTree<Binder, Var> {
    /// A variable that refers to a binder.
    Var(Var),
    /// A term that is explicitly annotated with a type.
    The {
        term_ty: Arc<TypeTree>,
        term: Arc<TermTree<Binder, Var>>,
    },
    /// Function term.
    ///
    /// Also known as:
    /// - anonymous function
    /// - lambda abstraction
    FunctionTerm {
        binder: Binder,
        body: Arc<TermTree<Binder, Var>>,
    },
    // TODO: Dependent types
    // /// Function type.
    // ///
    // /// Also known as:
    // /// - Π type
    // /// - dependent function type
    // /// - dependent product
    // FunctionType {
    //     parameter_ty: Arc<TermTree<Binder, Var>>,
    //     parameter_binder: Binder,
    //     body_ty: Arc<TermTree<Binder, Var>>,
    // },
    /// Function elimination.
    ///
    /// Also known as:
    /// - function application
    FunctionElim {
        head: Arc<TermTree<Binder, Var>>,
        argument: Arc<TermTree<Binder, Var>>,
    },
    // TODO: Dependent types
    // /// Pair type.
    // ///
    // /// Also known as:
    // /// - Σ type
    // /// - dependent pair type
    // /// - dependent sum
    // PairType {
    //     first_ty: Arc<TermTree<Binder, Var>>,
    //     first_binder: Binder,
    //     second_ty: Arc<TermTree<Binder, Var>>,
    // },
    /// Pair term.
    PairTerm {
        first: Arc<TermTree<Binder, Var>>,
        second: Arc<TermTree<Binder, Var>>,
    },
    /// Pair elimination.
    PairElim {
        head: Arc<TermTree<Binder, Var>>,
        binders: (Binder, Binder),
        body: Arc<TermTree<Binder, Var>>,
    },
}

/// Terms in event form, for pull-based tree processing.
#[derive(Copy, Clone, Debug)]
pub enum TermEvent<Binder, Var> {
    /// A variable that refers to a binder.
    Var(Var),

    /// Start an annotated term.
    TheStart,
    /// End an annotated term.
    TheEnd,

    /// Start a function term.
    FunctionTermStart(Binder),
    /// End a function term.
    FunctionTermEnd,
    /// Start a function elimination.
    FunctionElimStart,
    /// End a function elimination.
    FunctionElimEnd,

    /// Start a pair term.
    PairTermStart,
    /// End a pair term.
    PairTermEnd,
    /// Start a pair elimination.
    PairElimStart,
    /// Pair binder.
    PairElimBinders(Binder, Binder),
    /// End a pair elimination.
    PairElimEnd,

    /// A type event.
    Type(TypeEvent),
}

////////////////////////////////////////////////////////////////////////////////////////////////////
//
// Type event processing
//
////////////////////////////////////////////////////////////////////////////////////////////////////

/// An error produced when attempting to call `TypeTree::from_events`.
#[derive(Clone, Debug)]
pub enum FromTypeEventError {
    ExpectedFunctionEnd,
    ExpectedPairEnd,
    UnexpectedFunctionEnd,
    UnexpectedPairEnd,
    UnexpectedEof,
}

impl TypeTree {
    /// Convert this type tree into a stream of type events.
    pub fn into_events(self) -> impl Iterator<Item = TypeEvent> {
        // TODO: Implement this!
        match self {
            TypeTree::Base => Some(TypeEvent::Base).into_iter(),
            TypeTree::Function {
                parameter_ty,
                body_ty,
            } => None.into_iter(),
            TypeTree::Pair {
                first_ty,
                second_ty,
            } => None.into_iter(),
        }
    }

    /// Create a type tree from a stream of type events.
    pub fn from_events(
        events: &mut impl Iterator<Item = TypeEvent>,
    ) -> Result<TypeTree, FromTypeEventError> {
        // TODO: Error recovery.
        match events.next().ok_or(FromTypeEventError::UnexpectedEof)? {
            TypeEvent::Base => Ok(TypeTree::Base),
            TypeEvent::FunctionStart => {
                // Stack depth?
                let parameter_ty = Arc::new(TypeTree::from_events(events)?);
                let body_ty = Arc::new(TypeTree::from_events(events)?);
                match events.next().ok_or(FromTypeEventError::UnexpectedEof)? {
                    TypeEvent::FunctionEnd => Ok(TypeTree::Function {
                        parameter_ty,
                        body_ty,
                    }),
                    _ => Err(FromTypeEventError::ExpectedFunctionEnd),
                }
            }
            TypeEvent::FunctionEnd => Err(FromTypeEventError::ExpectedFunctionEnd),
            TypeEvent::PairStart => {
                // Stack depth?
                let first_ty = Arc::new(TypeTree::from_events(events)?);
                let second_ty = Arc::new(TypeTree::from_events(events)?);
                match events.next().ok_or(FromTypeEventError::UnexpectedEof)? {
                    TypeEvent::PairEnd => Ok(TypeTree::Pair {
                        first_ty,
                        second_ty,
                    }),
                    _ => Err(FromTypeEventError::ExpectedPairEnd),
                }
            }
            TypeEvent::PairEnd => Err(FromTypeEventError::ExpectedPairEnd),
        }
    }
}

////////////////////////////////////////////////////////////////////////////////////////////////////
//
// Term event processing
//
////////////////////////////////////////////////////////////////////////////////////////////////////

/// An error produced when attempting to call `TermTree::from_events`.
#[derive(Clone, Debug)]
pub enum FromTermEventError {
    ExpectedTheEnd,
    ExpectedFunctionTermEnd,
    ExpectedFunctionElimEnd,
    ExpectedPairTermEnd,
    ExpectedPairElimBinders,
    ExpectedPairElimEnd,
    UnexpectedTheEnd,
    UnexpectedFunctionTermEnd,
    UnexpectedFunctionElimEnd,
    UnexpectedPairTermEnd,
    UnexpectedPairElimBinders,
    UnexpectedPairElimEnd,
    UnexpectedType,
    FromTypeEvent(FromTypeEventError),
    UnexpectedEof,
}

impl From<FromTypeEventError> for FromTermEventError {
    fn from(src: FromTypeEventError) -> FromTermEventError {
        FromTermEventError::FromTypeEvent(src)
    }
}

impl<Binder, Var> TermTree<Binder, Var> {
    /// Convert this term tree into a stream of term events.
    pub fn into_events(self) -> impl Iterator<Item = TermEvent<Binder, Var>> {
        // TODO: Implement this!
        match self {
            TermTree::Var(var) => Some(TermEvent::Var(var)).into_iter(),
            TermTree::The { term_ty, term } => None.into_iter(),
            TermTree::FunctionTerm { binder, body } => None.into_iter(),
            TermTree::FunctionElim { head, argument } => None.into_iter(),
            TermTree::PairTerm { first, second } => None.into_iter(),
            TermTree::PairElim {
                head,
                binders,
                body,
            } => None.into_iter(),
        }
    }

    /// Create a term tree from a stream of term events.
    pub fn from_events(
        events: &mut impl Iterator<Item = TermEvent<Binder, Var>>,
    ) -> Result<TermTree<Binder, Var>, FromTermEventError> {
        // TODO: Error recovery.
        match events.next().ok_or(FromTermEventError::UnexpectedEof)? {
            TermEvent::Var(var) => Ok(TermTree::Var(var)),
            TermEvent::TheStart => {
                // Stack depth?
                let term_ty =
                    Arc::new(TypeTree::from_events(&mut events.by_ref().map(
                        |event| match event {
                            TermEvent::Type(ty) => ty,
                            _ => unimplemented!(), // FIXME
                        },
                    ))?);
                let term = Arc::new(TermTree::from_events(events)?);
                match events.next().ok_or(FromTermEventError::UnexpectedEof)? {
                    TermEvent::TheEnd => Ok(TermTree::The { term_ty, term }),
                    _ => Err(FromTermEventError::ExpectedTheEnd),
                }
            }
            TermEvent::FunctionTermStart(binder) => {
                // Stack depth?
                let body = Arc::new(TermTree::from_events(events)?);
                match events.next().ok_or(FromTermEventError::UnexpectedEof)? {
                    TermEvent::FunctionTermEnd => Ok(TermTree::FunctionTerm { binder, body }),
                    _ => Err(FromTermEventError::ExpectedFunctionTermEnd),
                }
            }
            TermEvent::FunctionElimStart => {
                // Stack depth?
                let head = Arc::new(TermTree::from_events(events)?);
                let argument = Arc::new(TermTree::from_events(events)?);
                match events.next().ok_or(FromTermEventError::UnexpectedEof)? {
                    TermEvent::FunctionElimEnd => Ok(TermTree::FunctionElim { head, argument }),
                    _ => Err(FromTermEventError::ExpectedFunctionElimEnd),
                }
            }
            TermEvent::PairTermStart => {
                // Stack depth?
                let first = Arc::new(TermTree::from_events(events)?);
                let second = Arc::new(TermTree::from_events(events)?);
                match events.next().ok_or(FromTermEventError::UnexpectedEof)? {
                    TermEvent::PairTermEnd => Ok(TermTree::PairTerm { first, second }),
                    _ => Err(FromTermEventError::ExpectedPairTermEnd),
                }
            }
            TermEvent::PairElimStart => {
                // Stack depth?
                let head = Arc::new(TermTree::from_events(events)?);
                let binders = match events.next().ok_or(FromTermEventError::UnexpectedEof)? {
                    TermEvent::PairElimBinders(first, second) => (first, second),
                    _ => return Err(FromTermEventError::ExpectedPairElimBinders),
                };
                let body = Arc::new(TermTree::from_events(events)?);
                match events.next().ok_or(FromTermEventError::UnexpectedEof)? {
                    TermEvent::PairElimEnd => Ok(TermTree::PairElim {
                        head,
                        binders,
                        body,
                    }),
                    _ => Err(FromTermEventError::ExpectedPairElimEnd),
                }
            }
            TermEvent::TheEnd => Err(FromTermEventError::UnexpectedTheEnd),
            TermEvent::FunctionTermEnd => Err(FromTermEventError::UnexpectedFunctionTermEnd),
            TermEvent::FunctionElimEnd => Err(FromTermEventError::UnexpectedFunctionElimEnd),
            TermEvent::PairTermEnd => Err(FromTermEventError::UnexpectedPairTermEnd),
            TermEvent::PairElimBinders(_, _) => Err(FromTermEventError::UnexpectedPairElimBinders),
            TermEvent::PairElimEnd => Err(FromTermEventError::UnexpectedPairElimEnd),
            TermEvent::Type(_) => Err(FromTermEventError::UnexpectedType),
        }
    }
}

////////////////////////////////////////////////////////////////////////////////////////////////////
//
// Renaming pass
//
////////////////////////////////////////////////////////////////////////////////////////////////////

/// A locally nameless variable.
pub enum LnVar<Name> {
    /// Free variables.
    Free(Name),
    /// De Bruijn index. This is the number of binders we need to skip to get to
    /// the binder that bound this variable.
    Bound(usize),
}

/// Erase variable names where possible, turning them into locally nameless variables.
pub fn remove_names<'a, Binder: Clone + PartialEq<Var> + 'a, Var>(
    named_events: &'a mut impl Iterator<Item = TermEvent<Binder, Var>>,
) -> impl Iterator<Item = TermEvent<Binder, LnVar<Var>>> + 'a {
    named_events.scan(Vec::new(), |names, named_event| match named_event {
        TermEvent::Var(var) => match names.iter().rposition(|name| *name == var) {
            None => Some(TermEvent::Var(LnVar::Free(var))),
            Some(index) => Some(TermEvent::Var(LnVar::Bound(index))),
        },
        TermEvent::TheStart => Some(TermEvent::TheStart),
        TermEvent::TheEnd => Some(TermEvent::TheEnd),
        TermEvent::FunctionTermStart(binder) => {
            names.push(binder.clone());
            Some(TermEvent::FunctionTermStart(binder))
        }
        TermEvent::FunctionTermEnd => {
            names.pop();
            Some(TermEvent::FunctionTermEnd)
        }
        TermEvent::FunctionElimStart => Some(TermEvent::FunctionElimStart),
        TermEvent::FunctionElimEnd => Some(TermEvent::FunctionElimEnd),
        TermEvent::PairTermStart => Some(TermEvent::PairTermStart),
        TermEvent::PairTermEnd => Some(TermEvent::PairTermEnd),
        TermEvent::PairElimStart => Some(TermEvent::PairElimStart),
        TermEvent::PairElimBinders(first, second) => {
            names.push(first.clone());
            names.push(second.clone());
            Some(TermEvent::PairElimBinders(first, second))
        }
        TermEvent::PairElimEnd => {
            names.pop();
            names.pop();
            Some(TermEvent::PairElimEnd)
        }
        TermEvent::Type(event) => Some(TermEvent::Type(event)),
    })
}

////////////////////////////////////////////////////////////////////////////////////////////////////
//
// Typing
//
////////////////////////////////////////////////////////////////////////////////////////////////////

pub fn check<Binder, Var>(
    state: &mut Vec<(&str, TypeTree)>, // TODO
    term_events: &mut impl Iterator<Item = TermEvent<Binder, Var>>,
    expected_type: &TypeTree,
) -> Option<bool> {
    match term_events.next()? {
        TermEvent::FunctionTermStart(binding) => {
            // TODO:
            unimplemented!()
        }
        event => {
            // TODO: conversion checking
            unimplemented!()
        }
    }
}

pub fn synth<Binder, Var>(
    state: &mut Vec<(&str, TypeTree)>, // TODO
    term_events: &mut impl Iterator<Item = TermEvent<Binder, Var>>,
) -> Option<TypeTree> {
    match term_events.next()? {
        TermEvent::Var(var) => unimplemented!(), // TODO: lookup in context
        TermEvent::TheStart => {
            let term_ty =
                TypeTree::from_events(&mut term_events.by_ref().map(|event| match event {
                    TermEvent::Type(ty) => ty,
                    _ => unimplemented!(), // FIXME
                }))
                .ok()?;

            if check(state, term_events, &term_ty)? {
                // TODO: expect TheEnd
                Some(term_ty)
            } else {
                None
            }

            // FIXME: errors
        }
        TermEvent::FunctionElimStart => {
            // TODO: synth head
            // TODO: check body
            unimplemented!()
        }
        TermEvent::PairTermStart => {
            // TODO: synth first
            // TODO: synth second
            unimplemented!()
        }
        TermEvent::PairElimStart => {
            // TODO: synth head
            // TODO: expect binders
            // TODO: synth body
            unimplemented!()
        }
        _ => None,
    }
}

Interesting links:

• https://fullyfaithful.nl/blog/pulldown-cmark/
• https://fullyfaithful.nl/blog/scanner-denial-of-service/
• https://xi.zulipchat.com/#narrow/stream/147932-chatter/topic/Push.2FPull.20parsing.20for.20compiler.20passes/near/181084848