use crate::syntax::*;
use std::fmt::Debug;
pub trait DebuggableNameTrait: NameTrait + Debug {}
impl<Name: DebuggableNameTrait> Pattern<Name> {
pub fn contains(&self, name: &Name) -> bool {
match self {
Pattern::Var(pattern_name) => pattern_name == name,
Pattern::Pair(first, second) => first.contains(name) || second.contains(name),
Pattern::Unit => false,
}
}
pub fn project(&self, name: &Name, val: Value<Name>) -> Value<Name> {
match self {
Pattern::Pair(first, second) => {
if first.contains(name) {
first.project(name, val.first())
} else if second.contains(name) {
second.project(name, val.second())
} else {
panic!("Cannot project with {:?}", name)
}
}
Pattern::Var(pattern_name) => {
if pattern_name == name {
val
} else {
panic!("Expected projection: {:?}, found: {:?}", pattern_name, name)
}
}
Pattern::Unit => panic!("Cannot project unit pattern"),
}
}
}
impl<Name: DebuggableNameTrait> Telescope<Name> {
pub fn resolve(&self, name: &Name) -> Value<Name> {
match self {
Telescope::Nil => panic!("Unresolved reference: {:?}", name),
Telescope::UpDec(context, Declaration::Simple(pattern, _, expression))
| Telescope::UpDec(context, Declaration::Recursive(pattern, _, expression)) => {
if pattern.contains(name) {
pattern.project(name, expression.clone().eval(context))
} else {
context.resolve(name)
}
}
Telescope::UpVar(context, pattern, val) => {
if pattern.contains(name) {
pattern.project(name, val.clone())
} else {
context.resolve(name)
}
}
}
}
}
impl<Name: DebuggableNameTrait> Closure<Name> {
pub fn instantiate(self, val: Value<Name>) -> Value<Name> {
match self {
Closure::Choice(pattern, expression, context) => {
expression.eval(&Telescope::UpVar(context, pattern, val))
}
Closure::Function(closure, name) => {
closure.instantiate(Value::Constructor(name, Box::new(val)))
}
}
}
}
impl<Name: DebuggableNameTrait> Value<Name> {
pub fn first(self) -> Value<Name> {
match self {
Value::Pair(first, _) => *first,
Value::Neutral(neutral) => Value::Neutral(Neutral::First(Box::new(neutral))),
e => panic!(format!("Cannot first: {:?}", e)),
}
}
pub fn second(self) -> Value<Name> {
match self {
Value::Pair(_, second) => *second,
Value::Neutral(neutral) => Value::Neutral(Neutral::Second(Box::new(neutral))),
e => panic!("Cannot second: {:?}", e),
}
}
pub fn apply(self, argument: Value<Name>) -> Value<Name> {
match self {
Value::Lambda(closure) => closure.instantiate(argument),
Value::Function((case_tree, context)) => match argument {
Value::Constructor(name, body) => case_tree
.get(&name)
.expect(format!("Cannot find constructor {:?}.", name).as_str())
.clone()
.eval(&context)
.apply(*body),
Value::Neutral(neutral) => Value::Neutral(Neutral::Function(
Box::new((case_tree, context)),
Box::new(neutral),
)),
e => panic!("Cannot apply a: {:?}", e),
},
Value::Neutral(neutral) => {
Value::Neutral(Neutral::Application(Box::new(neutral), Box::new(argument)))
}
e => panic!("Cannot apply on: {:?}", e),
}
}
}
impl<Name: DebuggableNameTrait> Expression<Name> {
pub fn eval(self, context: &Telescope<Name>) -> Value<Name> {
match self {
Expression::Unit => Value::Unit,
Expression::One => Value::One,
Expression::Type => Value::Type,
Expression::Var(name) => context.resolve(&name),
Expression::Sum(constructors) => {
Value::Sum((Box::new(constructors), Box::new(context.clone())))
}
Expression::Function(case_tree) => {
Value::Function((Box::new(case_tree), Box::new(context.clone())))
}
Expression::Pi(pattern, first, second) => Value::Pi(
Box::new(first.eval(context)),
Closure::Choice(pattern, *second, Box::new(context.clone())),
),
Expression::Sigma(pattern, first, second) => Value::Sigma(
Box::new(first.eval(context)),
Closure::Choice(pattern, *second, Box::new(context.clone())),
),
Expression::Lambda(pattern, body) => {
Value::Lambda(Closure::Choice(pattern, *body, Box::new(context.clone())))
}
Expression::First(pair) => pair.eval(context).first(),
Expression::Second(pair) => pair.eval(context).second(),
Expression::Application(function, argument) => {
function.eval(context).apply(argument.eval(context))
}
Expression::Pair(first, second) => Value::Pair(
Box::new(first.eval(context)),
Box::new(second.eval(context)),
),
Expression::Constructor(name, body) => {
Value::Constructor(name, Box::new(body.eval(context)))
}
Expression::Declaration(declaration, rest) => {
rest.eval(&Telescope::UpDec(Box::new(context.clone()), *declaration))
}
e => panic!("Cannot eval: {:?}", e),
}
}
}