use std::collections::BTreeMap;
use std::rc::Rc;
#[derive(Debug, Clone, Eq, PartialEq)]
pub enum Expression {
Unit,
One,
Type,
Void,
Var(String),
Sum(Branch),
Split(Branch),
Pi(Typed, Box<Self>),
Sigma(Typed, Box<Self>),
Lambda(Pattern, Option<AnonymousValue>, Box<Self>),
First(Box<Self>),
Second(Box<Self>),
Application(Box<Self>, Box<Self>),
Pair(Box<Self>, Box<Self>),
Constructor(String, Box<Self>),
Constant(Pattern, Box<Self>, Box<Self>),
Declaration(Box<Declaration>, Box<Self>),
}
#[derive(Debug, Clone)]
pub struct AnonymousValue {
pub internal: Box<Value>,
}
impl AnonymousValue {
pub fn new(value: Value) -> AnonymousValue {
AnonymousValue {
internal: Box::new(value),
}
}
pub fn some(value: Value) -> Option<AnonymousValue> {
Some(Self::new(value))
}
}
impl Eq for AnonymousValue {}
impl PartialEq<AnonymousValue> for AnonymousValue {
fn eq(&self, _other: &AnonymousValue) -> bool {
true
}
}
pub type Branch = BTreeMap<String, Box<Expression>>;
pub type Typed = (Pattern, Box<Expression>);
#[derive(Debug, Clone)]
pub enum Value {
Lambda(Closure),
Unit,
One,
Type,
Pi(Box<Self>, Closure),
Sigma(Box<Self>, Closure),
Pair(Box<Self>, Box<Self>),
Constructor(String, Box<Self>),
Split(CaseTree),
Sum(CaseTree),
Neutral(Neutral),
}
#[derive(Debug, Clone, Eq, PartialEq)]
pub enum GenericNeutral<Value: Clone> {
Generated(u32),
Application(Box<Self>, Box<Value>),
First(Box<Self>),
Second(Box<Self>),
Split(GenericCaseTree<Value>, Box<Self>),
}
pub type Neutral = GenericNeutral<Value>;
#[derive(Debug, Clone, Ord, PartialOrd, Eq, PartialEq)]
pub enum Pattern {
Pair(Box<Pattern>, Box<Pattern>),
Unit,
Var(String),
}
#[derive(Debug, Clone, Ord, PartialOrd, Eq, PartialEq)]
pub enum DeclarationType {
Simple,
Recursive,
}
#[derive(Debug, Clone, Eq, PartialEq)]
pub struct Declaration {
pub pattern: Pattern,
pub prefix_parameters: Vec<Typed>,
pub signature: Expression,
pub body: Expression,
pub declaration_type: DeclarationType,
}
impl Declaration {
pub fn new(
pattern: Pattern,
prefix_parameters: Vec<Typed>,
signature: Expression,
body: Expression,
declaration_type: DeclarationType,
) -> Self {
Self {
pattern,
prefix_parameters,
signature,
body,
declaration_type,
}
}
pub fn simple(
pattern: Pattern,
prefix_parameters: Vec<Typed>,
signature: Expression,
body: Expression,
) -> Self {
Self::new(
pattern,
prefix_parameters,
signature,
body,
DeclarationType::Simple,
)
}
pub fn recursive(
pattern: Pattern,
prefix_parameters: Vec<Typed>,
signature: Expression,
body: Expression,
) -> Self {
Self::new(
pattern,
prefix_parameters,
signature,
body,
DeclarationType::Recursive,
)
}
}
#[derive(Debug, Clone, Eq, PartialEq)]
pub enum GenericTelescope<Value: Clone> {
Nil,
UpDec(Rc<Self>, Declaration),
UpVar(Rc<Self>, Pattern, Value),
}
pub type TelescopeRaw = GenericTelescope<Value>;
pub type TelescopeRc<Value> = Rc<GenericTelescope<Value>>;
pub type Telescope = Rc<TelescopeRaw>;
pub fn up_var_rc<Value: Clone>(
me: TelescopeRc<Value>,
pattern: Pattern,
value: Value,
) -> TelescopeRc<Value> {
Rc::new(GenericTelescope::UpVar(me, pattern, value))
}
pub fn up_dec_rc<Value: Clone>(
me: TelescopeRc<Value>,
declaration: Declaration,
) -> TelescopeRc<Value> {
Rc::new(GenericTelescope::UpDec(me, declaration))
}
pub fn nil_rc<Value: Clone>() -> TelescopeRc<Value> {
Rc::new(GenericTelescope::Nil)
}
#[derive(Debug, Clone)]
pub enum Closure {
Abstraction(Pattern, Option<Box<Value>>, Expression, Box<Telescope>),
Value(Box<Value>),
Choice(Box<Self>, String),
}
pub type GenericCaseTree<Value> = (Box<Branch>, Box<Rc<GenericTelescope<Value>>>);
pub type CaseTree = GenericCaseTree<Value>;