ttt/
evaluate.rs

1use thiserror::Error;
2
3use crate::{PartialContext, SubstError, Context};
4
5#[derive(Debug, Error, PartialEq)]
6pub enum EvalError {
7    #[error(transparent)]
8    SubstError(#[from] SubstError),
9}
10
11pub trait Evaluate: Clone {
12    type Target;
13    type Error;
14    // type ContextEntry;
15    // type Context: Context<Entry = Option<Self::ContextEntry>>;
16    type Context: PartialContext<Self::Target>;
17
18    fn evaluate(
19        &self,
20        ctx: &Self::Context,
21        under_binders: bool,
22    ) -> Result<Self::Target, Self::Error>;
23
24    fn normalise(
25        &self,
26        ctx: &Self::Context,
27        under_binders: bool,
28    ) -> Result<Self, Self::Error>
29    where
30        Self::Target: Into<Self>,
31    {
32        self.evaluate(ctx, under_binders).map(Into::into)
33    }
34
35    fn evaluate_closed(
36        &self, 
37        under_binders: bool
38    ) -> Result<Self::Target, Self::Error> 
39    {
40        self.evaluate(&Self::Context::empty(), under_binders)
41    }
42
43    fn normalise_closed(
44        &self, 
45        under_binders: bool
46    ) -> Result<Self, Self::Error> 
47    where 
48        Self::Target: Into<Self>
49    {
50        self.normalise(&Self::Context::empty(), under_binders)
51    }
52
53    // It isn't sufficient to ask that Target: From<ContextEntry>, because, for example in the
54    // implementation for Box<T>, this requires Box<T::Target>: T::ContextEntry, which only
55    // would hold if `From` was resolved transitively from:
56    // Box<T::Target>: From<T::Target>, and
57    // T::Target: From<T::ContextEntry>
58    // fn from_context_entry(entry: Self::ContextEntry) -> Self::Target;
59}
60
61impl<T: Evaluate> Evaluate for Box<T> {
62    type Target = T::Target;
63
64    type Error = T::Error;
65
66    // type ContextEntry = T::ContextEntry;
67    type Context = T::Context;
68
69    fn evaluate(
70        &self,
71        ctx: &Self::Context,
72        under_binders: bool,
73    ) -> Result<Self::Target, Self::Error> {
74        (**self).evaluate(ctx, under_binders)
75    }
76
77    // fn from_context_entry(entry: Self::ContextEntry) -> Self::Target {
78    //     Box::new(T::from_context_entry(entry))
79    // }
80}
ttt/evaluate.rs

ttt/
evaluate.rs
