1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133

//! Abstract machines for the lazy evaluation of terms.

use super::reduce::WState;
use super::{RTerm, Term};
use crate::stack;
use alloc::rc::Rc;
use core::cell::{Ref, RefCell, RefMut};
use lazy_st::Thunk;

/// An abstract machine representing arguments applied to a substituted term.
///
/// This representation allows for the lazy evaluation of terms.
///
/// See section 5.1 of the following reference:
/// Asperti, A.; Ricciotti, W.; Sacerdoti Coen, C.; Tassi, E. (2009).
/// "A compact kernel for the calculus of inductive constructions".
/// *Sadhana*. **34**: 71–144.
/// doi: [10.1007/s12046-009-0003-3](https://doi.org/10.1007%2Fs12046-009-0003-3).
#[derive(Clone, Default)]
pub struct State<'s> {
    pub ctx: Context<'s>,
    pub term: RTerm<'s>,
    pub stack: Stack<'s>,
}

impl<'s> State<'s> {
    /// Construct a new state from a reference to a term.
    ///
    /// This does not yet evaluate anything, as can be seen from following example:
    ///
    /// ~~~
    /// # use kontroli::Error;
    /// # use kontroli::scope::{Term as STerm, Symbols};
    /// # use kontroli::rc::{RTerm, Signature, Term};
    /// # use kontroli::rc::state::State;
    /// let syms = Symbols::new();
    ///
    /// let term = Term::from(STerm::parse(r"(x => x) (x => x).", &syms)?);
    /// let rterm = RTerm::new(term);
    ///
    /// let state = State::new(rterm.clone());
    /// assert!(RTerm::ptr_eq(&RTerm::from(state), &rterm));
    /// # Ok::<(), Error>(())
    /// ~~~
    pub fn new(term: RTerm<'s>) -> Self {
        Self {
            ctx: Context::new(),
            term,
            stack: Stack::new(),
        }
    }
}

/// Map from de Bruijn indices in the term of the abstract machine to lazy terms.
pub type Context<'s> = stack::Stack<RTTerm<'s>>;

/// Arguments to the abstract machine term.
pub type Stack<'s> = stack::Stack<RState<'s>>;

/// A shared lazy term constructed from a shared mutable state.
#[derive(Clone)]
pub struct RTTerm<'s>(Rc<Thunk<RState<'s>, RTerm<'s>>>);

impl<'s> RTTerm<'s> {
    pub fn new(st: RState<'s>) -> Self {
        Self(Rc::new(Thunk::new(st)))
    }

    /// Force evaluation of the lazy term.
    pub fn force(&self) -> &RTerm<'s> {
        &**self.0
    }
}

/// A shared mutable state.
///
/// We use `RefCell` instead of `Thunk` here
/// because evaluation requires a signature and
/// because we sometimes wish to access the original state.
#[derive(Clone)]
pub struct RState<'s>(Rc<RefCell<WState<'s>>>);

impl<'s> RState<'s> {
    pub fn new(wst: WState<'s>) -> Self {
        Self(Rc::new(RefCell::new(wst)))
    }

    pub fn borrow(&self) -> Ref<WState<'s>> {
        self.0.borrow()
    }

    pub fn borrow_mut(&self) -> RefMut<WState<'s>> {
        self.0.borrow_mut()
    }
}

impl<'s> lazy_st::Evaluate<RTerm<'s>> for RState<'s> {
    fn evaluate(self) -> RTerm<'s> {
        RTerm::from(self)
    }
}

impl<'s> From<RState<'s>> for RTerm<'s> {
    fn from(s: RState<'s>) -> Self {
        RTerm::from(s.borrow_state().clone())
    }
}

impl<'s> From<State<'s>> for RTerm<'s> {
    fn from(state: State<'s>) -> Self {
        state
            .term
            .psubst(&state.ctx)
            .apply(state.stack.into_iter().map(Self::from).collect())
    }
}

impl<'s> RTerm<'s> {
    fn psubst(self, args: &Context<'s>) -> Self {
        if args.is_empty() {
            self
        } else {
            self.apply_subst(&psubst(args), 0)
        }
    }
}

fn psubst<'s, 'c>(args: &'c Context<'s>) -> impl Fn(usize, usize) -> RTerm<'s> + 'c {
    move |n: usize, k: usize| match args.get(n - k) {
        Some(arg) => arg.force().clone() << k,
        None => RTerm::new(Term::BVar(n - args.len())),
    }
}