use crate::types::{SideEffect, StackType, Type};
use crate::unification::{Subst, unify_stacks};
use super::TypeChecker;
impl TypeChecker {
pub(super) fn infer_dip(
&self,
span: &Option<crate::ast::Span>,
current_stack: StackType,
) -> Result<(StackType, Subst, Vec<SideEffect>), String> {
let line_prefix = self.line_prefix();
let (stack_after_quot, quot_type) = current_stack.clone().pop().ok_or_else(|| {
format!(
"{}dip: stack underflow - expected quotation on stack",
line_prefix
)
})?;
let quot_effect = match "_type {
Type::Quotation(effect) => (**effect).clone(),
Type::Closure { effect, .. } => (**effect).clone(),
Type::Var(_) => {
let effect = self
.lookup_word_effect("dip")
.ok_or_else(|| "Unknown word: 'dip'".to_string())?;
let fresh_effect = self.freshen_effect(&effect);
let (result_stack, subst) =
self.apply_effect(&fresh_effect, current_stack, "dip", span)?;
return Ok((result_stack, subst, vec![]));
}
_ => {
return Err(format!(
"{}dip: expected quotation or closure on top of stack, got {}",
line_prefix, quot_type
));
}
};
if quot_effect.has_yield() {
return Err("dip: quotation must not have Yield effects.\n\
Use strand.weave for quotations that yield."
.to_string());
}
let (rest_stack, preserved_type) = stack_after_quot.clone().pop().ok_or_else(|| {
format!(
"{}dip: stack underflow - expected a value below the quotation",
line_prefix
)
})?;
let fresh_effect = self.freshen_effect("_effect);
let (result_stack, subst) =
self.apply_effect(&fresh_effect, rest_stack, "dip (quotation)", span)?;
let resolved_preserved = subst.apply_type(&preserved_type);
let result_stack = result_stack.push(resolved_preserved);
let propagated_effects = fresh_effect.effects.clone();
Ok((result_stack, subst, propagated_effects))
}
pub(super) fn infer_keep(
&self,
span: &Option<crate::ast::Span>,
current_stack: StackType,
) -> Result<(StackType, Subst, Vec<SideEffect>), String> {
let line_prefix = self.line_prefix();
let (stack_after_quot, quot_type) = current_stack.clone().pop().ok_or_else(|| {
format!(
"{}keep: stack underflow - expected quotation on stack",
line_prefix
)
})?;
let quot_effect = match "_type {
Type::Quotation(effect) => (**effect).clone(),
Type::Closure { effect, .. } => (**effect).clone(),
Type::Var(_) => {
let effect = self
.lookup_word_effect("keep")
.ok_or_else(|| "Unknown word: 'keep'".to_string())?;
let fresh_effect = self.freshen_effect(&effect);
let (result_stack, subst) =
self.apply_effect(&fresh_effect, current_stack, "keep", span)?;
return Ok((result_stack, subst, vec![]));
}
_ => {
return Err(format!(
"{}keep: expected quotation or closure on top of stack, got {}",
line_prefix, quot_type
));
}
};
if quot_effect.has_yield() {
return Err("keep: quotation must not have Yield effects.\n\
Use strand.weave for quotations that yield."
.to_string());
}
let (_rest_stack, preserved_type) = stack_after_quot.clone().pop().ok_or_else(|| {
format!(
"{}keep: stack underflow - expected a value below the quotation",
line_prefix
)
})?;
let fresh_effect = self.freshen_effect("_effect);
let (result_stack, subst) =
self.apply_effect(&fresh_effect, stack_after_quot, "keep (quotation)", span)?;
let resolved_preserved = subst.apply_type(&preserved_type);
let result_stack = result_stack.push(resolved_preserved);
let propagated_effects = fresh_effect.effects.clone();
Ok((result_stack, subst, propagated_effects))
}
pub(super) fn infer_bi(
&self,
span: &Option<crate::ast::Span>,
current_stack: StackType,
) -> Result<(StackType, Subst, Vec<SideEffect>), String> {
let line_prefix = self.line_prefix();
let (stack1, quot2_type) = current_stack.clone().pop().ok_or_else(|| {
format!(
"{}bi: stack underflow - expected second quotation on stack",
line_prefix
)
})?;
let (stack2, quot1_type) = stack1.clone().pop().ok_or_else(|| {
format!(
"{}bi: stack underflow - expected first quotation on stack",
line_prefix
)
})?;
let quot1_effect = match "1_type {
Type::Quotation(effect) => (**effect).clone(),
Type::Closure { effect, .. } => (**effect).clone(),
Type::Var(_) => {
let effect = self
.lookup_word_effect("bi")
.ok_or_else(|| "Unknown word: 'bi'".to_string())?;
let fresh_effect = self.freshen_effect(&effect);
let (result_stack, subst) =
self.apply_effect(&fresh_effect, current_stack, "bi", span)?;
return Ok((result_stack, subst, vec![]));
}
_ => {
return Err(format!(
"{}bi: expected quotation or closure as first quotation, got {}",
line_prefix, quot1_type
));
}
};
let quot2_effect = match "2_type {
Type::Quotation(effect) => (**effect).clone(),
Type::Closure { effect, .. } => (**effect).clone(),
Type::Var(_) => {
let effect = self
.lookup_word_effect("bi")
.ok_or_else(|| "Unknown word: 'bi'".to_string())?;
let fresh_effect = self.freshen_effect(&effect);
let (result_stack, subst) =
self.apply_effect(&fresh_effect, current_stack, "bi", span)?;
return Ok((result_stack, subst, vec![]));
}
_ => {
return Err(format!(
"{}bi: expected quotation or closure as second quotation, got {}",
line_prefix, quot2_type
));
}
};
if quot1_effect.has_yield() || quot2_effect.has_yield() {
return Err("bi: quotations must not have Yield effects.\n\
Use strand.weave for quotations that yield."
.to_string());
}
let (_rest, preserved_type) = stack2.clone().pop().ok_or_else(|| {
format!(
"{}bi: stack underflow - expected a value below the quotations",
line_prefix
)
})?;
let fresh_effect1 = self.freshen_effect("1_effect);
let (after_quot1, subst1) =
self.apply_effect(&fresh_effect1, stack2, "bi (first quotation)", span)?;
let resolved_preserved = subst1.apply_type(&preserved_type);
let with_x = after_quot1.push(resolved_preserved);
let fresh_effect2 = self.freshen_effect("2_effect);
let (result_stack, subst2) =
self.apply_effect(&fresh_effect2, with_x, "bi (second quotation)", span)?;
let subst = subst1.compose(&subst2);
let mut effects = fresh_effect1.effects.clone();
for e in fresh_effect2.effects.clone() {
if !effects.contains(&e) {
effects.push(e);
}
}
Ok((result_stack, subst, effects))
}
pub(super) fn infer_if_combinator(
&self,
span: &Option<crate::ast::Span>,
current_stack: StackType,
) -> Result<(StackType, Subst, Vec<SideEffect>), String> {
let line_prefix = self.line_prefix();
let (stack1, else_quot_type) = current_stack.clone().pop().ok_or_else(|| {
format!(
"{}if: stack underflow - expected else-quotation on stack",
line_prefix
)
})?;
let (stack2, then_quot_type) = stack1.clone().pop().ok_or_else(|| {
format!(
"{}if: stack underflow - expected then-quotation below else-quotation",
line_prefix
)
})?;
let (stack_after_cond, cond_type) = stack2.clone().pop().ok_or_else(|| {
format!(
"{}if: stack underflow - expected Bool below the two quotations",
line_prefix
)
})?;
let cond_subst = unify_stacks(
&StackType::singleton(Type::Bool),
&StackType::singleton(cond_type),
)
.map_err(|e| format!("{}if: condition must be Bool: {}", line_prefix, e))?;
let stack_after_cond = cond_subst.apply_stack(&stack_after_cond);
let then_effect = match self.if_branch_effect(
&then_quot_type,
"then-branch",
current_stack.clone(),
span,
&line_prefix,
)? {
IfBranchEffect::Concrete(effect) => effect,
IfBranchEffect::Fallback(result_stack, subst) => {
return Ok((result_stack, subst, vec![]));
}
};
let else_effect = match self.if_branch_effect(
&else_quot_type,
"else-branch",
current_stack,
span,
&line_prefix,
)? {
IfBranchEffect::Concrete(effect) => effect,
IfBranchEffect::Fallback(result_stack, subst) => {
return Ok((result_stack, subst, vec![]));
}
};
let fresh_then = self.freshen_effect(&then_effect);
let (then_result, then_subst) = self.apply_effect(
&fresh_then,
stack_after_cond.clone(),
"if (then branch)",
span,
)?;
let fresh_else = self.freshen_effect(&else_effect);
let else_input = then_subst.apply_stack(&stack_after_cond);
let (else_result, else_subst) =
self.apply_effect(&fresh_else, else_input, "if (else branch)", span)?;
let then_result_after_else = else_subst.apply_stack(&then_result);
let if_line = span.as_ref().map(|s| s.line + 1).unwrap_or(0);
let merge_subst = unify_stacks(&then_result_after_else, &else_result).map_err(|e| {
if if_line > 0 {
format!(
"at line {}: if branches have incompatible stack effects:\n\
\x20 then branch produces: {}\n\
\x20 else branch produces: {}\n\
\x20 Both quotations of `if` must produce the same stack shape.\n\
\x20 Error: {}",
if_line, then_result_after_else, else_result, e
)
} else {
format!(
"if branches have incompatible stack effects:\n\
\x20 then branch produces: {}\n\
\x20 else branch produces: {}\n\
\x20 Error: {}",
then_result_after_else, else_result, e
)
}
})?;
let result_stack = merge_subst.apply_stack(&else_result);
let subst = cond_subst
.compose(&then_subst)
.compose(&else_subst)
.compose(&merge_subst);
let mut effects = fresh_then.effects.clone();
for e in fresh_else.effects.clone() {
if !effects.contains(&e) {
effects.push(e);
}
}
Ok((result_stack, subst, effects))
}
fn if_branch_effect(
&self,
quot_type: &Type,
slot_label: &str,
current_stack: StackType,
span: &Option<crate::ast::Span>,
line_prefix: &str,
) -> Result<IfBranchEffect, String> {
match quot_type {
Type::Quotation(effect) => Ok(IfBranchEffect::Concrete((**effect).clone())),
Type::Closure { effect, .. } => Ok(IfBranchEffect::Concrete((**effect).clone())),
Type::Var(_) => {
let effect = self
.lookup_word_effect("if")
.ok_or_else(|| "Unknown word: 'if'".to_string())?;
let fresh_effect = self.freshen_effect(&effect);
let (result_stack, subst) =
self.apply_effect(&fresh_effect, current_stack, "if", span)?;
Ok(IfBranchEffect::Fallback(result_stack, subst))
}
other => Err(format!(
"{}if: expected quotation or closure as {}, got {}",
line_prefix, slot_label, other
)),
}
}
}
enum IfBranchEffect {
Concrete(crate::types::Effect),
Fallback(StackType, Subst),
}