use std::fmt;
use std::sync::Arc;
use crate::jet::Jet;
use crate::node::{
CoreConstructible, DisconnectConstructible, JetConstructible, NoDisconnect,
WitnessConstructible,
};
use crate::types::{Context, Error, Final, Type};
use crate::value::Word;
use super::variable::new_name;
#[derive(Debug)]
pub struct Arrow<'brand> {
pub source: Type<'brand>,
pub target: Type<'brand>,
pub inference_context: Context<'brand>,
}
impl Clone for Arrow<'_> {
fn clone(&self) -> Self {
self.shallow_clone()
}
}
impl fmt::Display for Arrow<'_> {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
write!(f, "{} → {}", self.source, self.target)
}
}
#[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Debug, Hash)]
pub struct FinalArrow {
pub source: Arc<Final>,
pub target: Arc<Final>,
}
impl fmt::Display for FinalArrow {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
write!(f, "{} → {}", self.source, self.target)
}
}
impl FinalArrow {
pub fn shallow_clone(&self) -> Self {
FinalArrow {
source: Arc::clone(&self.source),
target: Arc::clone(&self.target),
}
}
}
impl<'brand> Arrow<'brand> {
pub fn finalize(&self) -> Result<FinalArrow, Error> {
Ok(FinalArrow {
source: self.source.finalize()?,
target: self.target.finalize()?,
})
}
pub fn shallow_clone(&self) -> Self {
Arrow {
source: self.source.shallow_clone(),
target: self.target.shallow_clone(),
inference_context: self.inference_context.shallow_clone(),
}
}
fn for_case(lchild_arrow: Option<&Self>, rchild_arrow: Option<&Self>) -> Result<Self, Error> {
if let (Some(left), Some(right)) = (lchild_arrow, rchild_arrow) {
left.inference_context.check_eq(&right.inference_context)?;
}
let ctx = match (lchild_arrow, rchild_arrow) {
(Some(left), _) => left.inference_context.shallow_clone(),
(_, Some(right)) => right.inference_context.shallow_clone(),
(None, None) => panic!("called `for_case` with no children"),
};
let a = Type::free(&ctx, new_name("case_a_"));
let b = Type::free(&ctx, new_name("case_b_"));
let c = Type::free(&ctx, new_name("case_c_"));
let sum_a_b = Type::sum(&ctx, a.shallow_clone(), b.shallow_clone());
let prod_sum_a_b_c = Type::product(&ctx, sum_a_b, c.shallow_clone());
let target = Type::free(&ctx, String::new());
if let Some(lchild_arrow) = lchild_arrow {
ctx.bind_product(
&lchild_arrow.source,
&a,
&c,
"case combinator: left source = A × C",
)?;
ctx.unify(&target, &lchild_arrow.target, "").unwrap();
}
if let Some(rchild_arrow) = rchild_arrow {
ctx.bind_product(
&rchild_arrow.source,
&b,
&c,
"case combinator: left source = B × C",
)?;
ctx.unify(
&target,
&rchild_arrow.target,
"case combinator: left target = right target",
)?;
}
Ok(Arrow {
source: prod_sum_a_b_c,
target,
inference_context: ctx,
})
}
fn for_disconnect(lchild_arrow: &Self, rchild_arrow: &Self) -> Result<Self, Error> {
lchild_arrow
.inference_context
.check_eq(&rchild_arrow.inference_context)?;
let ctx = lchild_arrow.inference_context();
let a = Type::free(ctx, new_name("disconnect_a_"));
let b = Type::free(ctx, new_name("disconnect_b_"));
let c = rchild_arrow.source.shallow_clone();
let d = rchild_arrow.target.shallow_clone();
ctx.bind_product(
&lchild_arrow.source,
&Type::two_two_n(ctx, 8),
&a,
"disconnect combinator: left source = 2^256 × A",
)?;
ctx.bind_product(
&lchild_arrow.target,
&b,
&c,
"disconnect combinator: left target = B × C",
)?;
let prod_b_d = Type::product(ctx, b, d);
Ok(Arrow {
source: a,
target: prod_b_d,
inference_context: lchild_arrow.inference_context.shallow_clone(),
})
}
}
impl<'brand> CoreConstructible<'brand> for Arrow<'brand> {
fn iden(inference_context: &Context<'brand>) -> Self {
let new = Type::free(inference_context, new_name("iden_src_"));
Arrow {
source: new.shallow_clone(),
target: new,
inference_context: inference_context.shallow_clone(),
}
}
fn unit(inference_context: &Context<'brand>) -> Self {
Arrow {
source: Type::free(inference_context, new_name("unit_src_")),
target: Type::unit(inference_context),
inference_context: inference_context.shallow_clone(),
}
}
fn injl(child: &Self) -> Self {
Arrow {
source: child.source.shallow_clone(),
target: Type::sum(
&child.inference_context,
child.target.shallow_clone(),
Type::free(&child.inference_context, new_name("injl_tgt_")),
),
inference_context: child.inference_context.shallow_clone(),
}
}
fn injr(child: &Self) -> Self {
Arrow {
source: child.source.shallow_clone(),
target: Type::sum(
&child.inference_context,
Type::free(&child.inference_context, new_name("injr_tgt_")),
child.target.shallow_clone(),
),
inference_context: child.inference_context.shallow_clone(),
}
}
fn take(child: &Self) -> Self {
Arrow {
source: Type::product(
&child.inference_context,
child.source.shallow_clone(),
Type::free(&child.inference_context, new_name("take_src_")),
),
target: child.target.shallow_clone(),
inference_context: child.inference_context.shallow_clone(),
}
}
fn drop_(child: &Self) -> Self {
Arrow {
source: Type::product(
&child.inference_context,
Type::free(&child.inference_context, new_name("drop_src_")),
child.source.shallow_clone(),
),
target: child.target.shallow_clone(),
inference_context: child.inference_context.shallow_clone(),
}
}
fn comp(left: &Self, right: &Self) -> Result<Self, Error> {
left.inference_context.check_eq(&right.inference_context)?;
left.inference_context.unify(
&left.target,
&right.source,
"comp combinator: left target = right source",
)?;
Ok(Arrow {
source: left.source.shallow_clone(),
target: right.target.shallow_clone(),
inference_context: left.inference_context.shallow_clone(),
})
}
fn case(left: &Self, right: &Self) -> Result<Self, Error> {
Self::for_case(Some(left), Some(right))
}
fn assertl(left: &Self, _: crate::Cmr) -> Result<Self, Error> {
Self::for_case(Some(left), None)
}
fn assertr(_: crate::Cmr, right: &Self) -> Result<Self, Error> {
Self::for_case(None, Some(right))
}
fn pair(left: &Self, right: &Self) -> Result<Self, Error> {
left.inference_context.check_eq(&right.inference_context)?;
left.inference_context.unify(
&left.source,
&right.source,
"pair combinator: left source = right source",
)?;
Ok(Arrow {
source: left.source.shallow_clone(),
target: Type::product(
&left.inference_context,
left.target.shallow_clone(),
right.target.shallow_clone(),
),
inference_context: left.inference_context.shallow_clone(),
})
}
fn fail(inference_context: &Context<'brand>, _: crate::FailEntropy) -> Self {
Arrow {
source: Type::free(inference_context, new_name("fail_src_")),
target: Type::free(inference_context, new_name("fail_tgt_")),
inference_context: inference_context.shallow_clone(),
}
}
fn const_word(inference_context: &Context<'brand>, word: Word) -> Self {
Arrow {
source: Type::unit(inference_context),
target: Type::two_two_n(inference_context, word.n() as usize), inference_context: inference_context.shallow_clone(),
}
}
fn inference_context(&self) -> &Context<'brand> {
&self.inference_context
}
}
impl<'brand> DisconnectConstructible<'brand, Arrow<'brand>> for Arrow<'brand> {
fn disconnect(left: &Self, right: &Self) -> Result<Self, Error> {
Self::for_disconnect(left, right)
}
}
impl<'brand> DisconnectConstructible<'brand, NoDisconnect> for Arrow<'brand> {
fn disconnect(left: &Self, _: &NoDisconnect) -> Result<Self, Error> {
let source = Type::free(&left.inference_context, "disc_src".into());
let target = Type::free(&left.inference_context, "disc_tgt".into());
Self::for_disconnect(
left,
&Arrow {
source,
target,
inference_context: left.inference_context.shallow_clone(),
},
)
}
}
impl<'brand> DisconnectConstructible<'brand, Option<&Arrow<'brand>>> for Arrow<'brand> {
fn disconnect(left: &Self, right: &Option<&Self>) -> Result<Self, Error> {
match *right {
Some(right) => Self::disconnect(left, right),
None => Self::disconnect(left, &NoDisconnect),
}
}
}
impl<'brand, J: Jet> JetConstructible<'brand, J> for Arrow<'brand> {
fn jet(inference_context: &Context<'brand>, jet: J) -> Self {
Arrow {
source: jet.source_ty().to_type(inference_context),
target: jet.target_ty().to_type(inference_context),
inference_context: inference_context.shallow_clone(),
}
}
}
impl<'brand, W> WitnessConstructible<'brand, W> for Arrow<'brand> {
fn witness(inference_context: &Context<'brand>, _: W) -> Self {
Arrow {
source: Type::free(inference_context, new_name("witness_src_")),
target: Type::free(inference_context, new_name("witness_tgt_")),
inference_context: inference_context.shallow_clone(),
}
}
}