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

//! Convert from scoped to shared structures.

use super::{Intro, RTerm, Rc, Rule, Term};
use crate::scope::{Intro as SIntro, RTerm as SRTerm, Rule as SRule, Term as STerm};

impl<'s> From<STerm<'s>> for Term<'s> {
    fn from(tm: STerm<'s>) -> Self {
        tm.map(Rc::new, RTerm::from)
    }
}

impl<'s> From<SRTerm<'s>> for RTerm<'s> {
    fn from(tm: SRTerm<'s>) -> Self {
        Self::new(Term::from(tm.get()))
    }
}

impl<'s> From<SRule<'s>> for Rule<'s> {
    fn from(rule: SRule<'s>) -> Self {
        Self {
            ctx: rule.ctx,
            lhs: rule.lhs,
            rhs: RTerm::from(rule.rhs),
        }
    }
}

impl<'s> From<SIntro<'s>> for Intro<'s> {
    fn from(cmd: SIntro<'s>) -> Self {
        cmd.map_type(RTerm::from).map_term(RTerm::from)
    }
}