dedukti_parse/
cmd.rs

1use crate::Token;
2use alloc::vec::Vec;
3use core::fmt::{self, Display};
4
5/// Command of a Dedukti theory.
6#[derive(Clone, Debug)]
7pub enum Command<C, V, Tm> {
8    // Introduce a new symbol with arguments
9    Intro(C, Vec<(V, Tm)>, Intro<Tm>),
10    // Add rewrite rules
11    Rules(Vec<Rule<V, Tm>>),
12}
13
14/// A command that introduces a new constant.
15#[derive(Clone, Debug)]
16pub enum Intro<Ty, Tm = Ty> {
17    Definition(Option<Ty>, Option<Tm>),
18    Theorem(Ty, Tm),
19    Declaration(Ty),
20}
21
22/// A command that introduces a set of rewrite rules.
23#[derive(Clone, Debug)]
24pub struct Rule<V, Tm> {
25    /// context (bound variables)
26    pub ctx: Vec<(V, Option<Tm>)>,
27    /// left-hand side (pattern to match with)
28    pub lhs: Tm,
29    /// right-hand side (term to replace with)
30    pub rhs: Tm,
31}
32
33impl<C, V, Tm> Command<C, V, Tm> {
34    /// Apply a function to the constant introduced by an introduction.
35    pub fn map_const<C2>(self, f: impl FnOnce(C) -> C2) -> Command<C2, V, Tm> {
36        match self {
37            Self::Intro(x, args, it) => Command::Intro(f(x), args, it),
38            Self::Rules(rules) => Command::Rules(rules),
39        }
40    }
41}
42
43impl<Ty, Tm> Intro<Ty, Tm> {
44    /// Only constants introduced by definitions are rewritable.
45    pub fn rewritable(&self) -> bool {
46        match self {
47            Self::Definition(..) => true,
48            Self::Declaration(_) | Self::Theorem(..) => false,
49        }
50    }
51
52    /// Apply a function to the type of the introduced constant, if given.
53    pub fn map_type<U>(self, f: impl FnOnce(Ty) -> U) -> Intro<U, Tm> {
54        match self {
55            Self::Definition(ty, tm) => Intro::Definition(ty.map(f), tm),
56            Self::Theorem(ty, tm) => Intro::Theorem(f(ty), tm),
57            Self::Declaration(ty) => Intro::Declaration(f(ty)),
58        }
59    }
60
61    /// Apply a function to the term of the introduced constant, if given.
62    pub fn map_term<U>(self, f: impl FnOnce(Tm) -> U) -> Intro<Ty, U> {
63        match self {
64            Self::Definition(ty, tm) => Intro::Definition(ty, tm.map(f)),
65            Self::Theorem(ty, tm) => Intro::Theorem(ty, f(tm)),
66            Self::Declaration(ty) => Intro::Declaration(ty),
67        }
68    }
69}
70
71impl<C: Display, V: Display, Tm: Display> Display for Command<C, V, Tm> {
72    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
73        match self {
74            Self::Intro(x, args, it) => {
75                match it {
76                    Intro::Theorem(_, _) => write!(f, "thm ")?,
77                    Intro::Definition(_, _) => write!(f, "def ")?,
78                    Intro::Declaration(_) => (),
79                };
80                write!(f, "{}", x)?;
81                args.iter()
82                    .try_for_each(|(x, ty)| write!(f, " ({} : {})", x, ty))?;
83                match it {
84                    Intro::Definition(ty, tm) => {
85                        ty.iter().try_for_each(|ty| write!(f, " : {}", ty))?;
86                        tm.iter().try_for_each(|tm| write!(f, " := {}", tm))
87                    }
88                    Intro::Theorem(ty, tm) => write!(f, " : {} := {}", ty, tm),
89                    Intro::Declaration(ty) => write!(f, " : {}", ty),
90                }
91            }
92            Self::Rules(rules) => rules.iter().try_for_each(|rule| rule.fmt(f)),
93        }
94    }
95}
96
97impl<V: Display, Tm: Display> Display for Rule<V, Tm> {
98    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
99        write!(f, "[")?;
100        let mut ctx = self.ctx.iter().peekable();
101        while let Some((x, ty)) = ctx.next() {
102            write!(f, "{}", x)?;
103            ty.iter().try_for_each(|ty| write!(f, ": {}", ty))?;
104            ctx.peek().iter().try_for_each(|_| write!(f, ", "))?;
105        }
106        write!(f, "] {} --> {}", self.lhs, self.rhs)
107    }
108}
109
110#[derive(Debug)]
111pub(crate) enum DefThm {
112    Def,
113    Thm,
114}
115
116#[derive(Debug)]
117pub(crate) enum OfEq {
118    Of,
119    Eq,
120}
121
122#[derive(Debug)]
123pub struct RuleCtx<V, Tm> {
124    rules: Vec<Rule<V, Tm>>,
125    vars: Vec<Option<Tm>>,
126}
127
128impl<V, Tm> Default for RuleCtx<V, Tm> {
129    fn default() -> Self {
130        Self {
131            rules: Default::default(),
132            vars: Default::default(),
133        }
134    }
135}
136
137impl<V, Tm> RuleCtx<V, Tm> {
138    fn add(mut self, bound: &mut Vec<V>, lhs: Tm, rhs: Tm) -> Self {
139        let ctx = core::mem::take(&mut self.vars);
140        let ctx = bound.drain(..).zip(ctx).collect();
141        self.rules.push(Rule { ctx, lhs, rhs });
142        self
143    }
144}
145
146/// Error occurring during the parsing of a command.
147#[derive(Debug, PartialEq)]
148pub enum Error {
149    ExpectedColon,
150    ExpectedColonEq,
151    ExpectedColonOrColonEq,
152    ExpectedLongArrow,
153    ExpectedIdent,
154    ExpectedCommaOrRBrk,
155    ExpectedRPar,
156    ExpectedCmd,
157    UnexpectedPath,
158    UnexpectedToken,
159}
160
161type Result<T> = core::result::Result<T, Error>;
162
163/// State of the command parser.
164#[derive(Debug)]
165pub(crate) enum State<C, V, Tm> {
166    /// nothing
167    Init,
168
169    /// `def`
170    Def,
171    /// `thm`
172    Thm,
173
174    /// `s` followed by `:` if true
175    Decl(C, bool),
176
177    /// `def/thm s (x1 : t1) .. (xn : tn)`
178    Args(DefThm, C, Vec<Tm>),
179    /// `def/thm s (x1 : t1) .. (`
180    /// followed by `x`   if `Some((x, false))`
181    /// followed by `x :` if `Some((x,  true))`
182    ArgsIn(DefThm, C, Vec<Tm>, Option<(V, bool)>),
183    /// `def/thm s (x1 : t1) ... (xn: tn) : ty :=`
184    DefThmEq(DefThm, C, Vec<Tm>, Tm),
185
186    /// `def s (x1 : t1) .. (xn : tn)` followed by `:` or `:=`
187    DefOfEq(C, Vec<Tm>, OfEq),
188    /// `thm s (x1 : t1) .. (xn : tn)` followed by `:`
189    ThmOf(C, Vec<Tm>),
190
191    /// `[x1 : t1, ..,`
192    /// followed by `x`   if `Some((x, false))`
193    /// followed by `x :` if `Some((x,  true))`
194    RuleCtx(RuleCtx<V, Tm>, Option<(V, bool)>),
195
196    /// `[x1 : t1, .., xn : tn]`
197    RuleL(RuleCtx<V, Tm>),
198    /// `[x1 : t1, .., xn : tn] tm -->`
199    RuleR(RuleCtx<V, Tm>, Tm),
200
201    Command(Command<C, V, Tm>),
202}
203
204impl<C, V, Tm> Default for State<C, V, Tm> {
205    fn default() -> Self {
206        Self::Init
207    }
208}
209
210pub trait Joker {
211    fn joker() -> Self;
212}
213
214impl<'s> Joker for &'s str {
215    fn joker() -> Self {
216        "_"
217    }
218}
219
220impl Joker for alloc::string::String {
221    fn joker() -> Self {
222        "_".into()
223    }
224}
225
226impl<C, V: Joker, Tm> State<C, V, Tm> {
227    pub fn parse<S>(self, bound: &mut Vec<V>, token: Token<S>) -> Result<State<C, V, Tm>>
228    where
229        S: Into<C> + Into<V>,
230    {
231        match (self, token) {
232            (state, Token::Symb(s)) if s.path.is_empty() => state.apply_name(s.name),
233            (_, Token::Symb(_)) => Err(Error::UnexpectedPath),
234
235            // starting commands
236            (State::Init, Token::Def) => Ok(State::Def),
237            (State::Init, Token::Thm) => Ok(State::Thm),
238            (State::Init, Token::LBrk) => Ok(State::RuleCtx(Default::default(), None)),
239            (State::Init, _) => Err(Error::ExpectedCmd),
240
241            // s + :
242            (State::Decl(s, false), Token::Colon) => Ok(State::Decl(s, true)),
243            (State::Decl(_, false), _) => Err(Error::ExpectedColon),
244
245            (State::Def | State::Thm, _) => Err(Error::ExpectedIdent),
246
247            // def/thm s + (
248            (State::Args(dt, s, ctx), Token::LPar) => Ok(State::ArgsIn(dt, s, ctx, None)),
249
250            // thm s (..) + :
251            (State::Args(DefThm::Thm, s, c), Token::Colon) => Ok(State::ThmOf(s, c)),
252            // def s (..) + :
253            (State::Args(DefThm::Def, s, c), Token::Colon) => Ok(State::DefOfEq(s, c, OfEq::Of)),
254            // def s (..) + :=
255            (State::Args(DefThm::Def, s, c), Token::ColonEq) => Ok(State::DefOfEq(s, c, OfEq::Eq)),
256            (State::Args(DefThm::Thm, _, _), _) => Err(Error::ExpectedColon),
257            (State::Args(DefThm::Def, _, _), _) => Err(Error::ExpectedColonOrColonEq),
258
259            (State::ArgsIn(_, _, _, None), _) => Err(Error::ExpectedIdent),
260
261            // def s (x + :
262            (State::ArgsIn(dt, s, c, Some((x, false))), Token::Colon) => {
263                Ok(State::ArgsIn(dt, s, c, Some((x, true))))
264            }
265            (State::ArgsIn(_, _, _, Some((_, false))), _) => Err(Error::ExpectedColon),
266
267            // [x1 : t1, .., + ]
268            (State::RuleCtx(c, None), Token::RBrk) => Ok(Self::rulel(bound, c)),
269            (State::RuleCtx(_, None), _) => Err(Error::ExpectedCommaOrRBrk),
270
271            // [x1 : t1, .., x + :
272            (State::RuleCtx(c, Some((x, false))), Token::Colon) => {
273                Ok(State::RuleCtx(c, Some((x, true))))
274            }
275            // [x1 : t1, .., x + ,
276            (State::RuleCtx(mut c, Some((s, false))), Token::Comma) => {
277                bound.push(s);
278                c.vars.push(None);
279                Ok(State::RuleCtx(c, None))
280            }
281            // [x1 : t1, .., x + ]
282            (State::RuleCtx(mut c, Some((s, false))), Token::RBrk) => {
283                bound.push(s);
284                c.vars.push(None);
285                Ok(Self::rulel(bound, c))
286            }
287            // TODO: comma, rbrk, OR colon!
288            (State::RuleCtx(_, Some((_, false))), _) => Err(Error::ExpectedCommaOrRBrk),
289
290            _ => Err(Error::UnexpectedToken),
291        }
292    }
293
294    pub fn apply_name(self, name: impl Into<C> + Into<V>) -> Result<State<C, V, Tm>> {
295        match self {
296            State::Init => Ok(State::Decl(name.into(), false)),
297            // def/thm + s
298            State::Def => Ok(State::Args(DefThm::Def, name.into(), Vec::new())),
299            State::Thm => Ok(State::Args(DefThm::Thm, name.into(), Vec::new())),
300            // def/thm s ( + x
301            State::ArgsIn(dt, s, c, None) => {
302                Ok(State::ArgsIn(dt, s, c, Some((name.into(), false))))
303            }
304            // [x1 : t1, .., + x
305            State::RuleCtx(c, None) => Ok(State::RuleCtx(c, Some((name.into(), false)))),
306            _ => Err(Error::UnexpectedToken),
307        }
308    }
309
310    pub fn expects_term(&self) -> bool {
311        matches!(
312            self,
313            State::Decl(_, true)
314                | State::ThmOf(..)
315                | State::DefOfEq(..)
316                | State::DefThmEq(..)
317                | State::ArgsIn(.., Some((_, true)))
318                | State::RuleCtx(_, Some((_, true)))
319                | State::RuleL(_)
320                | State::RuleR(..)
321        )
322    }
323
324    pub fn rulel(bound: &mut Vec<V>, ctx: RuleCtx<V, Tm>) -> Self {
325        bound.insert(0, V::joker());
326        Self::RuleL(ctx)
327    }
328
329    pub fn apply<S>(self, bound: &mut Vec<V>, tm: Tm, token: Token<S>) -> Result<State<C, V, Tm>> {
330        match (self, token) {
331            (State::ArgsIn(dt, s, mut ctx, Some((x, true))), Token::RPar) => {
332                bound.push(x);
333                ctx.push(tm);
334                Ok(State::Args(dt, s, ctx))
335            }
336
337            (State::RuleL(ctx), Token::LongArrow) => {
338                // kill the joker
339                bound.remove(0);
340                Ok(State::RuleR(ctx, tm))
341            }
342            (State::RuleL(..), _) => Err(Error::ExpectedLongArrow),
343            (State::RuleR(ctx, lhs), Token::LBrk) => {
344                Ok(State::RuleCtx(ctx.add(bound, lhs, tm), None))
345            }
346            (State::RuleCtx(mut ctx, Some((s, true))), Token::RBrk) => {
347                bound.push(s);
348                ctx.vars.push(Some(tm));
349                Ok(Self::rulel(bound, ctx))
350            }
351            (State::RuleCtx(mut ctx, Some((s, true))), Token::Comma) => {
352                bound.push(s);
353                ctx.vars.push(Some(tm));
354                Ok(State::RuleCtx(ctx, None))
355            }
356            (State::RuleCtx(..), _) => Err(Error::ExpectedCommaOrRBrk),
357            (State::ThmOf(x, ctx), Token::ColonEq) => Ok(State::DefThmEq(DefThm::Thm, x, ctx, tm)),
358            (State::DefOfEq(x, ctx, OfEq::Of), Token::ColonEq) => {
359                Ok(State::DefThmEq(DefThm::Def, x, ctx, tm))
360            }
361            (State::ThmOf(..), _) => Err(Error::ExpectedColonEq),
362
363            (State::ArgsIn(_, _, _, Some((_, true))), _) => Err(Error::ExpectedRPar),
364
365            (cur, Token::Dot) => Ok(State::Command(cur.close(bound, tm)?)),
366            _ => Err(Error::UnexpectedToken),
367        }
368    }
369
370    fn close(self, bound: &mut Vec<V>, tm: Tm) -> Result<Command<C, V, Tm>> {
371        match self {
372            State::Decl(x, true) => Ok(Command::Intro(x, Vec::new(), Intro::Declaration(tm))),
373            State::DefOfEq(x, ctx, ofeq) => {
374                let it = match ofeq {
375                    OfEq::Eq => Intro::Definition(None, Some(tm)),
376                    OfEq::Of => Intro::Definition(Some(tm), None),
377                };
378                let ctx = bound.drain(..).zip(ctx).collect();
379                Ok(Command::Intro(x, ctx, it))
380            }
381            State::DefThmEq(dt, x, ctx, ty) => {
382                let it = match dt {
383                    DefThm::Thm => Intro::Theorem(ty, tm),
384                    DefThm::Def => Intro::Definition(Some(ty), Some(tm)),
385                };
386                let ctx = bound.drain(..).zip(ctx).collect();
387                Ok(Command::Intro(x, ctx, it))
388            }
389            State::RuleR(ctx, lhs) => Ok(Command::Rules(ctx.add(bound, lhs, tm).rules)),
390            _ => Err(Error::ExpectedCmd),
391        }
392    }
393}
dedukti_parse/cmd.rs

dedukti_parse/
cmd.rs
