dedukti_parse/
term.rs

1//! Terms of the lambda-Pi calculus.
2
3use crate::{Symb, Token};
4use alloc::{boxed::Box, vec::Vec};
5use core::borrow::Borrow;
6use core::fmt::{self, Display};
7
8/// A term is an application of terms to an application head.
9pub type Term<A, V> = App<AppH<A, V>>;
10
11/// Application of applications to a head.
12#[derive(Clone, Debug)]
13pub struct App<H> {
14    /// head of the application
15    pub head: H,
16    /// arguments applied to the head (which are again applications)
17    pub args: Vec<Self>,
18}
19
20/// Head of an application.
21#[derive(Clone, Debug)]
22pub enum AppH<A, V> {
23    /// atom (constants, variables)
24    Atom(A),
25    /// abstraction (`x : A => t`)
26    Abst(V, Option<Box<App<Self>>>, Box<App<Self>>),
27    /// dependent product (`x : A -> t`)
28    Prod(Option<V>, Box<App<Self>>, Box<App<Self>>),
29}
30
31/// Term without subterms.
32#[derive(Clone, Debug)]
33pub enum Atom<C> {
34    /// constant
35    Const(C),
36    /// variable (de Bruijn index)
37    Var(usize),
38    /// "Type"
39    Type,
40}
41
42impl<H: Display> Display for App<H> {
43    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
44        if !self.args.is_empty() {
45            write!(f, "(")?;
46        }
47        self.head.fmt(f)?;
48        self.args.iter().try_for_each(|a| write!(f, " {}", a))?;
49        if !self.args.is_empty() {
50            write!(f, ")")?;
51        }
52        Ok(())
53    }
54}
55
56impl<C: Display> Display for Atom<C> {
57    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
58        match self {
59            Self::Const(c) => c.fmt(f),
60            Self::Var(v) => v.fmt(f),
61            Self::Type => "Type".fmt(f),
62        }
63    }
64}
65
66impl<A: Display, V: Display> Display for AppH<A, V> {
67    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
68        match self {
69            Self::Atom(a) => a.fmt(f),
70            Self::Abst(x, Some(ty), tm) => write!(f, "({} : {} => {})", x, ty, tm),
71            Self::Abst(x, None, tm) => write!(f, "({} => {})", x, tm),
72            Self::Prod(None, ty, tm) => write!(f, "({} -> {})", ty, tm),
73            Self::Prod(Some(x), ty, tm) => write!(f, "({} : {} -> {})", x, ty, tm),
74        }
75    }
76}
77
78/// Parse error.
79#[derive(Debug, PartialEq)]
80pub enum Error {
81    ExpectedIdentOrLPar,
82    AnonymousLambda,
83    AbstWithoutRhs,
84    UnclosedLPar,
85}
86
87type Result<T> = core::result::Result<T, Error>;
88
89impl<H> App<H> {
90    /// Create an application with a head and no applied arguments.
91    pub fn new(head: H) -> Self {
92        let args = Vec::new();
93        Self { head, args }
94    }
95}
96
97/// A left parenthesis possibly preceded by an abstraction and/or an application.
98#[derive(Debug)]
99struct LPar<A, V> {
100    x: Option<V>,
101    app: Option<Term<A, V>>,
102}
103
104/// State of the term parser.
105#[derive(Debug)]
106pub(crate) enum State<S, A, V> {
107    /// nothing
108    Init,
109    /// `s` (we do not know at this point whether it is a variable or a constant)
110    Symb(S),
111    /// `s :`
112    VarOf(V),
113    /// possibly `x :`, followed by `t1 ... tn`.
114    ATerm(Option<V>, Term<A, V>),
115}
116
117impl<S, A, V> State<S, A, V> {
118    pub fn map_symb<T>(self, f: impl FnOnce(S) -> T) -> State<T, A, V> {
119        match self {
120            Self::Init => State::Init,
121            Self::Symb(s) => State::Symb(f(s)),
122            Self::VarOf(v) => State::VarOf(v),
123            Self::ATerm(v, tm) => State::ATerm(v, tm),
124        }
125    }
126}
127
128impl<S, A, V> Default for State<S, A, V> {
129    fn default() -> Self {
130        Self::Init
131    }
132}
133
134/// Unfinished term that surrounds the currently parsed term.
135#[derive(Debug)]
136enum Cont<A, V> {
137    /// `x`, possibly followed by `: ty`, followed by `=>`,
138    Abst(V, Option<Term<A, V>>),
139    /// possibly `x :`, followed by `ty ->`,
140    Prod(Option<V>, Term<A, V>),
141
142    /// possibly `x :`,
143    /// possibly followed by `t1 .. tn`,
144    /// followed by `(`
145    LPar(LPar<A, V>),
146}
147
148/// Context in which a term is parsed.
149#[derive(Debug)]
150pub struct Ctx<A, V> {
151    /// variables that were bound outside the term
152    bound: Vec<V>,
153    /// open constructs around the term
154    stack: Vec<Cont<A, V>>,
155}
156
157impl<A, V> Ctx<A, V> {
158    /// Return the bound variables for mutation.
159    pub(crate) fn bound_mut(&mut self) -> &mut Vec<V> {
160        &mut self.bound
161    }
162
163    /// If a symbol is bound in a superterm, return its Bruijn variable.
164    ///
165    /// This implementation is not particularly efficient,
166    /// because it traverses all superterms in the worst case,
167    /// including superterms that can not even bind variables.
168    /// However, because we commit to not cloning symbols,
169    /// this is one of the best things we can do.
170    ///
171    /// Previously, I kept all bound variables in `bound`,
172    /// removing them from the stack.
173    /// However, when we reduce the stack, we need to obtain the variables,
174    /// and this is quite error-prone and ugly.
175    fn find<S: Eq + ?Sized>(&self, s: &S) -> Option<usize>
176    where
177        V: Borrow<S>,
178    {
179        let mut i = 0;
180        for cont in self.stack.iter().rev() {
181            match cont {
182                Cont::Abst(x, _) | Cont::Prod(Some(x), _) => {
183                    if x.borrow() == s {
184                        return Some(i);
185                    } else {
186                        i += 1;
187                    }
188                }
189                Cont::Prod(None, _) => i += 1,
190                Cont::LPar(_) => (),
191            }
192        }
193        for x in self.bound.iter().rev() {
194            if x.borrow() == s {
195                return Some(i);
196            } else {
197                i += 1
198            }
199        }
200        None
201    }
202}
203
204impl<A, V> Default for Ctx<A, V> {
205    fn default() -> Self {
206        Self {
207            bound: Vec::new(),
208            stack: Vec::new(),
209        }
210    }
211}
212
213/// Convert a symbol to a given type of atoms.
214pub trait Scope<S, V>
215where
216    Self: Sized,
217{
218    /// Convert a symbol to a given type of atoms.
219    fn scope(symb: Symb<S>, ctx: &Ctx<Self, V>) -> Self;
220
221    /// Convenience function to convert a symbol to a term.
222    fn go(symb: Symb<S>, ctx: &Ctx<Self, V>) -> Term<Self, V> {
223        Term::new(AppH::Atom(Self::scope(symb, ctx)))
224    }
225}
226
227/// The trivial scoper, mapping symbols to something they can be trivially converted to (including themselves).
228impl<S: Into<S2>, S2, V> Scope<S, V> for Symb<S2> {
229    fn scope(symb: Symb<S>, _: &Ctx<Self, V>) -> Self {
230        symb.map(S::into)
231    }
232}
233
234/// Distinguish symbols into constants and variables.
235impl<S: Borrow<str> + Into<C> + Eq, C, V: Borrow<str>> Scope<S, V> for Atom<Symb<C>> {
236    fn scope(symb: Symb<S>, ctx: &Ctx<Self, V>) -> Self {
237        if symb.path.is_empty() {
238            if let Some(v) = ctx.find(symb.name.borrow()) {
239                return Atom::Var(v);
240            } else if symb.name.borrow() == "Type" {
241                return Atom::Type;
242            }
243        }
244        Atom::Const(symb.map(|s| s.into()))
245    }
246}
247
248impl<A, V> Term<A, V> {
249    fn reduce(mut self, ctx: &mut Ctx<A, V>) -> (Option<LPar<A, V>>, Self) {
250        while let Some(cur) = ctx.stack.pop() {
251            match cur {
252                Cont::Abst(x, ty) => self = App::new(AppH::Abst(x, ty.map(Box::new), self.into())),
253                Cont::Prod(x, ty) => self = App::new(AppH::Prod(x, Box::new(ty), self.into())),
254                Cont::LPar(lpar) => return (Some(lpar), self),
255            }
256        }
257        (None, self)
258    }
259}
260
261/// Should I stay or should I go?
262enum Loop<T> {
263    Return(T),
264    Continue,
265}
266
267type OTok<S> = Option<Token<S>>;
268
269impl<S: Into<V>, A: Scope<S, V>, V> State<S, A, V> {
270    pub fn parse<I>(self, ctx: &mut Ctx<A, V>, iter: &mut I) -> Result<(Self, OTok<S>)>
271    where
272        I: Iterator<Item = Token<S>>,
273    {
274        match self.resume(ctx, iter)? {
275            Loop::Continue => Self::init(ctx, iter),
276            Loop::Return(ret) => Ok(ret),
277        }
278    }
279
280    fn resume<I>(self, ctx: &mut Ctx<A, V>, iter: &mut I) -> Result<Loop<(Self, OTok<S>)>>
281    where
282        I: Iterator<Item = Token<S>>,
283    {
284        match self {
285            Self::Init => Ok(Loop::Continue),
286            Self::Symb(s1) => Self::symb(Symb::new(s1), ctx, iter),
287            Self::VarOf(v) => Self::varof(v, ctx, iter),
288            Self::ATerm(x, app) => Self::aterm(x, app, ctx, iter),
289        }
290    }
291
292    fn init<I>(ctx: &mut Ctx<A, V>, iter: &mut I) -> Result<(Self, OTok<S>)>
293    where
294        I: Iterator<Item = Token<S>>,
295    {
296        loop {
297            match iter.next() {
298                tok @ (None | Some(Token::Comment(_))) => return Ok((Self::Init, tok)),
299                Some(Token::Symb(s)) => match Self::symb(s, ctx, iter)? {
300                    Loop::Continue => (),
301                    Loop::Return(ret) => return Ok(ret),
302                },
303                Some(Token::LPar) => ctx.stack.push(Cont::LPar(LPar { x: None, app: None })),
304                _ => return Err(Error::ExpectedIdentOrLPar),
305            }
306        }
307    }
308
309    fn symb<I>(s: Symb<S>, ctx: &mut Ctx<A, V>, iter: &mut I) -> Result<Loop<(Self, OTok<S>)>>
310    where
311        I: Iterator<Item = Token<S>>,
312    {
313        if !s.path.is_empty() {
314            return Self::aterm(None, A::go(s, ctx), ctx, iter);
315        }
316        match iter.next() {
317            tok @ (None | Some(Token::Comment(_))) => Ok(Loop::Return((Self::Symb(s.name), tok))),
318            Some(Token::FatArrow) => {
319                ctx.stack.push(Cont::Abst(s.name.into(), None));
320                Ok(Loop::Continue)
321            }
322            Some(Token::Colon) => Self::varof(s.name.into(), ctx, iter),
323            Some(tok) => {
324                let iter = &mut core::iter::once(tok).chain(iter);
325                Self::aterm(None, A::go(s, ctx), ctx, iter)
326            }
327        }
328    }
329
330    fn varof<I>(v: V, ctx: &mut Ctx<A, V>, iter: &mut I) -> Result<Loop<(Self, OTok<S>)>>
331    where
332        I: Iterator<Item = Token<S>>,
333    {
334        match iter.next() {
335            tok @ (None | Some(Token::Comment(_))) => Ok(Loop::Return((Self::VarOf(v), tok))),
336            Some(Token::Symb(s)) => Self::aterm(Some(v), A::go(s, ctx), ctx, iter),
337            Some(Token::LPar) => {
338                let x = Some(v);
339                ctx.stack.push(Cont::LPar(LPar { x, app: None }));
340                Ok(Loop::Continue)
341            }
342            Some(_) => Err(Error::ExpectedIdentOrLPar),
343        }
344    }
345
346    fn aterm(
347        mut x: Option<V>,
348        mut app: Term<A, V>,
349        ctx: &mut Ctx<A, V>,
350        iter: &mut impl Iterator<Item = Token<S>>,
351    ) -> Result<Loop<(Self, OTok<S>)>> {
352        loop {
353            match iter.next() {
354                tok @ (None | Some(Token::Comment(_))) => {
355                    return Ok(Loop::Return((State::ATerm(x, app), tok)))
356                }
357                Some(Token::Symb(s)) => app.args.push(A::go(s, ctx)),
358                Some(Token::Arrow) => {
359                    ctx.stack.push(Cont::Prod(x, app));
360                    return Ok(Loop::Continue);
361                }
362                Some(Token::FatArrow) => match x {
363                    None => return Err(Error::AnonymousLambda),
364                    Some(x) => {
365                        ctx.stack.push(Cont::Abst(x, Some(app)));
366                        return Ok(Loop::Continue);
367                    }
368                },
369                Some(Token::LPar) => {
370                    ctx.stack.push(Cont::LPar(LPar { x, app: Some(app) }));
371                    return Ok(Loop::Continue);
372                }
373                Some(_) if x.is_some() => return Err(Error::AbstWithoutRhs),
374                Some(tok) => match app.reduce(ctx) {
375                    // if we found a matching left parenthesis
376                    (Some(lpar), tm) if matches!(tok, Token::RPar) => {
377                        x = lpar.x;
378                        app = match lpar.app {
379                            None => tm,
380                            Some(mut app) => {
381                                app.args.push(tm);
382                                app
383                            }
384                        }
385                    }
386                    (Some(_lpar), _) => return Err(Error::UnclosedLPar),
387                    (None, tm) => return Ok(Loop::Return((State::ATerm(x, tm), Some(tok)))),
388                },
389            }
390        }
391    }
392}
393
394#[cfg(test)]
395impl<A, V> Term<A, V> {
396    /// Parse a term from a stream of tokens and put it into context.
397    ///
398    /// The context is mutated during parsing.
399    /// If this function returns `Ok(..)`, then
400    /// `ctx` should have the same value as before calling this function.
401    fn parse<S: Into<V>, I>(ctx: &mut Ctx<A, V>, iter: &mut I) -> Result<(Self, Token<S>)>
402    where
403        I: Iterator<Item = Token<S>>,
404        A: Scope<S, V>,
405        V: Borrow<S>,
406    {
407        match State::init(ctx, iter)? {
408            (State::ATerm(None, tm), Some(tok)) => Ok((tm, tok)),
409            (State::Init | State::VarOf(_), _) => Err(Error::ExpectedIdentOrLPar),
410            (State::Symb(_) | State::ATerm(..), _) => panic!("expected input"),
411        }
412    }
413}
414
415#[cfg(test)]
416impl<'s> Term<Atom<Symb<&'s str>>, &'s str> {
417    /// Parse a scoped term from a string.
418    fn parse_str(s: &'s str) -> Result<Self> {
419        use logos::Logos;
420        let mut ctx = Ctx::default();
421        let mut iter = Token::lexer(s).chain(core::iter::once(Token::Dot));
422        let (tm, tok) = Self::parse(&mut ctx, &mut iter)?;
423        assert_eq!(iter.next(), None);
424        assert_eq!(tok, Token::Dot);
425        Ok(tm)
426    }
427}
428
429#[test]
430fn positive() -> Result<()> {
431    Term::parse_str("x => y : a => z")?;
432    Term::parse_str("a -> x : b -> c")?;
433    Term::parse_str("(a)")?;
434    Term::parse_str("(a b)")?;
435    Term::parse_str("(a b) (c d) e")?;
436    Term::parse_str("a (b c) (d e)")?;
437    Term::parse_str("((a (((b)))))")?;
438    Term::parse_str("m1.a m2.b")?;
439    Ok(())
440}
441
442#[test]
443fn negative() {
444    use Error::*;
445    assert_eq!(Term::parse_str("->").unwrap_err(), ExpectedIdentOrLPar);
446    assert_eq!(Term::parse_str("x : ->").unwrap_err(), ExpectedIdentOrLPar);
447    assert_eq!(Term::parse_str("(a ").unwrap_err(), UnclosedLPar);
448    assert_eq!(Term::parse_str("(a b ").unwrap_err(), UnclosedLPar);
449    assert_eq!(Term::parse_str("a b => c").unwrap_err(), AnonymousLambda);
450    assert_eq!(Term::parse_str("(a : b)").unwrap_err(), AbstWithoutRhs);
451    assert_eq!(Term::parse_str("a : b.").unwrap_err(), AbstWithoutRhs);
452}
dedukti_parse/term.rs

dedukti_parse/
term.rs
