kontroli/
share.rs

1//! Convert from scoped to shared structures.
2
3use crate::parse::term::{AppH, Atom};
4use crate::parse::{self, Symb};
5use crate::{Comb, LTerm, Symbol, Symbols};
6use alloc::string::{String, ToString};
7use alloc::vec::Vec;
8use core::borrow::Borrow;
9
10type Result<T> = core::result::Result<T, Error>;
11
12type PTerm<S> = parse::Term<Atom<Symb<S>>, S>;
13
14pub type Command<'s> = crate::Command<String, Intro<'s>, Rule<'s>>;
15
16/// The way we introduce a new name.
17pub type Intro<'s> = crate::Intro<LTerm<'s>>;
18
19/// Rewrite rules with strings as bound variable identifiers,
20/// a top pattern (symbol application) as left-hand side, and
21/// a shared term as right-hand side.
22pub type Rule<'s> = crate::Rule<(String, Option<LTerm<'s>>), TopPattern<'s>, LTerm<'s>>;
23
24/// Pattern at the left-hand side of a rewrite rule.
25pub type TopPattern<'s> = crate::pattern::TopPattern<Symbol<'s>>;
26
27/// Rewrite pattern.
28pub type Pattern<'s> = crate::Pattern<Symbol<'s>>;
29
30pub trait Share<'s, Target> {
31    fn share(self, syms: &Symbols<'s>) -> Result<Target>;
32}
33
34#[derive(Debug, Eq, PartialEq)]
35pub enum Error {
36    UndeclaredSymbol(String),
37    NoPrepattern,
38    NoTopPattern,
39}
40
41impl<'s, S: Borrow<str> + Ord> Share<'s, Symbol<'s>> for Symb<S> {
42    fn share(self, syms: &Symbols<'s>) -> Result<Symbol<'s>> {
43        syms.get(&self.path, &self.name)
44            .ok_or_else(|| self.map(|s| s.borrow().to_string()).to_string())
45            .map_err(Error::UndeclaredSymbol)
46    }
47}
48
49impl<'s, R: Borrow<str> + Ord> Share<'s, LTerm<'s>> for AppH<Atom<Symb<R>>, R> {
50    fn share(self, syms: &Symbols<'s>) -> Result<LTerm<'s>> {
51        match self {
52            Self::Atom(Atom::Const(symb)) => Ok(LTerm::Const(symb.share(syms)?)),
53            Self::Atom(Atom::Var(v)) => Ok(LTerm::Var(v)),
54            Self::Atom(Atom::Type) => Ok(LTerm::Type),
55            Self::Prod(x, ty, tm) => {
56                let id = x
57                    .map(|x| x.borrow().to_string())
58                    .unwrap_or_else(|| "$".to_string());
59                let ty = ty.share(syms)?;
60                Ok(LTerm::Comb(Comb::Prod(id, ty, tm.share(syms)?).into()))
61            }
62            Self::Abst(x, ty, tm) => {
63                let id = x.borrow().to_string();
64                let ty = ty.map(|ty| (*ty).share(syms)).transpose()?;
65                Ok(LTerm::Comb(Comb::Abst(id, ty, tm.share(syms)?).into()))
66            }
67        }
68    }
69}
70
71impl<'s, R: Borrow<str> + Ord> Share<'s, LTerm<'s>> for PTerm<R> {
72    fn share(self, syms: &Symbols<'s>) -> Result<LTerm<'s>> {
73        let head = self.head.share(syms)?;
74        if self.args.is_empty() {
75            Ok(head)
76        } else {
77            let tail: Result<_> = self.args.into_iter().map(|tm| tm.share(syms)).collect();
78            Ok(LTerm::Comb(Comb::Appl(head, tail?).into()))
79        }
80    }
81}
82
83impl<'s> TryFrom<LTerm<'s>> for Pattern<'s> {
84    type Error = Error;
85
86    fn try_from(tm: LTerm<'s>) -> Result<Self> {
87        match tm {
88            LTerm::Const(c) => Ok(Self::Symb(c, Vec::new())),
89            LTerm::Var(v) => Ok(Self::MVar(v)),
90            LTerm::Comb(comb) => match *comb {
91                Comb::Appl(head, args2) => match Self::try_from(head)? {
92                    Self::Symb(s, mut args) => {
93                        let args2 = args2.into_iter().map(Self::try_from);
94                        args.append(&mut args2.collect::<Result<_>>()?);
95                        Ok(Self::Symb(s, args))
96                    }
97                    // TODO: rename this to `NoPattern`
98                    _ => Err(Error::NoPrepattern),
99                },
100                _ => Err(Error::NoPrepattern),
101            },
102            _ => Err(Error::NoPrepattern),
103        }
104    }
105}
106
107impl<'s, R: Borrow<str> + Ord> Share<'s, Rule<'s>> for parse::Rule<R, PTerm<R>> {
108    fn share(self, syms: &Symbols<'s>) -> Result<Rule<'s>> {
109        let joker = self.ctx.len();
110        let ctx = self.ctx.into_iter().map(|(id, ty)| {
111            let id = id.borrow().to_string();
112            let ty = ty.map(|ty| ty.share(syms)).transpose()?;
113            Ok((id, ty))
114        });
115        let ctx = ctx.collect::<Result<_>>()?;
116
117        let lhs = self.lhs.share(syms)?;
118        let lhs = Pattern::try_from(lhs)?;
119        let lhs = lhs.joke(joker);
120        let lhs = TopPattern::try_from(lhs).map_err(|_| Error::NoTopPattern)?;
121
122        let rhs = self.rhs.share(syms)?;
123
124        Ok(Rule { ctx, lhs, rhs })
125    }
126}
127
128impl<'s, Tm: Share<'s, LTerm<'s>>> Share<'s, Intro<'s>> for parse::Intro<Tm> {
129    fn share(self, syms: &Symbols<'s>) -> Result<Intro<'s>> {
130        match self {
131            Self::Definition(ty, tm) => Ok(Intro::Definition(
132                ty.map(|ty| ty.share(syms)).transpose()?,
133                tm.map(|tm| tm.share(syms)).transpose()?,
134            )),
135            Self::Theorem(ty, tm) => Ok(Intro::Theorem(ty.share(syms)?, tm.share(syms)?)),
136            Self::Declaration(ty) => Ok(Intro::Declaration(ty.share(syms)?)),
137        }
138    }
139}
140
141impl<'s, R: Borrow<str> + Ord> Share<'s, Command<'s>> for parse::Command<R, R, PTerm<R>> {
142    fn share(self, syms: &Symbols<'s>) -> Result<Command<'s>> {
143        match self {
144            Self::Intro(id, args, it) => {
145                let mut args = args.into_iter().rev();
146                let it = args.try_fold(it.share(syms)?, |it, (name, aty)| {
147                    let id = name.borrow().to_string();
148                    let aty = aty.share(syms)?;
149                    Ok(it
150                        .map_type(|ty| LTerm::Comb(Comb::Prod(id.clone(), aty.clone(), ty).into()))
151                        .map_term(|tm| LTerm::Comb(Comb::Abst(id.clone(), Some(aty), tm).into())))
152                })?;
153                Ok(Command::Intro(id.borrow().to_string(), it))
154            }
155            Self::Rules(rules) => {
156                let rules: Result<_> = rules.into_iter().map(|r| r.share(syms)).collect();
157                Ok(Command::Rules(rules?))
158            }
159        }
160    }
161}
kontroli/share.rs

kontroli/
share.rs
