use std::cmp::min;
use std::usize;
use chalk_derive::{Fold, HasInterner, Visit};
use chalk_ir::interner::Interner;
use chalk_ir::visit::ControlFlow;
use chalk_ir::{
AnswerSubst, Canonical, ConstrainedSubst, Constraint, DebruijnIndex, Goal, InEnvironment,
Substitution,
};
pub mod context;
mod derived;
pub mod forest;
mod logic;
mod normalize_deep;
mod simplify;
pub mod slg;
pub mod solve;
mod stack;
mod strand;
mod table;
mod tables;
index_struct! {
pub struct TableIndex { value: usize,
}
}
#[derive(Clone, Debug, PartialEq, Eq, Hash, Fold, Visit, HasInterner)]
pub struct ExClause<I: Interner> {
pub subst: Substitution<I>,
pub ambiguous: bool,
pub constraints: Vec<InEnvironment<Constraint<I>>>,
pub subgoals: Vec<Literal<I>>,
pub delayed_subgoals: Vec<InEnvironment<Goal<I>>>,
pub answer_time: TimeStamp,
pub floundered_subgoals: Vec<FlounderedSubgoal<I>>,
}
#[derive(Copy, Clone, Debug, Default, PartialEq, Eq, PartialOrd, Ord, Hash)]
pub struct TimeStamp {
clock: u64,
}
impl TimeStamp {
const MAX: TimeStamp = TimeStamp {
clock: ::std::u64::MAX,
};
fn increment(&mut self) {
self.clock += 1;
}
}
#[derive(Clone, Debug, PartialEq, Eq, Hash, Fold, Visit)]
pub struct FlounderedSubgoal<I: Interner> {
pub floundered_literal: Literal<I>,
pub floundered_time: TimeStamp,
}
#[derive(Clone, Debug)]
pub struct Answer<I: Interner> {
pub subst: Canonical<AnswerSubst<I>>,
pub ambiguous: bool,
}
#[derive(Clone, Debug)]
pub struct CompleteAnswer<I: Interner> {
pub subst: Canonical<ConstrainedSubst<I>>,
pub ambiguous: bool,
}
#[derive(Clone, Debug, Fold, Visit)]
pub enum Literal<I: Interner> {
Positive(InEnvironment<Goal<I>>),
Negative(InEnvironment<Goal<I>>),
}
#[derive(Copy, Clone, Debug)]
struct Minimums {
positive: TimeStamp,
negative: TimeStamp,
}
impl Minimums {
const MAX: Minimums = Minimums {
positive: TimeStamp::MAX,
negative: TimeStamp::MAX,
};
fn take_minimums(&mut self, other: &Minimums) {
self.positive = min(self.positive, other.positive);
self.negative = min(self.negative, other.negative);
}
fn minimum_of_pos_and_neg(&self) -> TimeStamp {
min(self.positive, self.negative)
}
}
#[derive(Copy, Clone, Debug)]
pub(crate) enum AnswerMode {
Complete,
Ambiguous,
}
chalk_ir::copy_fold!(TableIndex);
chalk_ir::copy_fold!(TimeStamp);
chalk_ir::const_visit!(TableIndex);
chalk_ir::const_visit!(TimeStamp);
#[macro_export]
macro_rules! index_struct {
($(#[$m:meta])* $v:vis struct $n:ident {
$vf:vis value: usize,
}) => {
#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
$(#[$m])*
$v struct $n {
$vf value: usize,
}
impl $n {
#[allow(dead_code)]
$v fn get_and_increment(&mut self) -> Self {
let old_value = *self;
self.increment();
old_value
}
#[allow(dead_code)]
$v fn increment(&mut self) {
self.value += 1;
}
#[allow(dead_code)]
pub fn iterate_range(range: ::std::ops::Range<Self>) -> impl Iterator<Item = $n> {
(range.start.value..range.end.value).into_iter().map(|i| Self { value: i })
}
}
impl ::std::fmt::Debug for $n {
fn fmt(&self, fmt: &mut ::std::fmt::Formatter<'_>) -> ::std::fmt::Result {
write!(fmt, "{}({})", stringify!($n), self.value)
}
}
impl From<usize> for $n {
fn from(value: usize) -> Self {
Self { value }
}
}
}
}