phase_rs/
command.rs

1//! A syntax of commands and their parsing.
2//!
3//! A `Command` is the top level structure accepted by the executable
4//! They allow a sequence of gates to be defined before taking a term to evaluate.
5
6use std::ops::Range;
7
8use winnow::{
9    LocatingSlice, ModalResult, Parser,
10    ascii::{multispace0, multispace1},
11    combinator::{cut_err, preceded, repeat, seq, terminated},
12    error::{StrContext, StrContextValue},
13};
14
15use crate::{
16    raw_syntax::TermR,
17    text::{HasParser, Name, Span, comment_parser},
18    typecheck::{Env, TypeCheckError},
19    typed_syntax::TermT,
20};
21
22/// The Command structure: a runnable program.
23#[derive(Clone, Debug)]
24pub struct Command<S> {
25    /// List of gates to define, with the name to bind them to.
26    pub gates: Vec<(Name, TermR<S>)>,
27    /// Final term to evaluate.
28    pub term: TermR<S>,
29}
30
31impl<S: Span> Command<S> {
32    /// Typecheck a command, building an `Env` with gate definitions.
33    pub fn check(&self) -> Result<(Env, TermT), TypeCheckError<S>> {
34        let mut env = Env::default();
35        for (name, tm) in &self.gates {
36            let t = tm.check(&env, None)?;
37            env.0.insert(name.clone(), t);
38        }
39        let tm = self.term.check(&env, None)?;
40        Ok((env, tm))
41    }
42}
43
44impl HasParser for Command<Range<usize>> {
45    fn parser(input: &mut LocatingSlice<&str>) -> ModalResult<Self> {
46        let gate = preceded(
47	"gate",
48	cut_err(seq!(_: multispace1,
49		     Name::parser,
50		     _: (multispace0, "=", multispace0).context(StrContext::Expected(StrContextValue::CharLiteral('='))),
51		     TermR::parser,
52		     _: (multispace0, ","))).context(StrContext::Label("gate definition"))
53	);
54
55        comment_parser.parse_next(input)?;
56        let gates = repeat(0.., terminated(gate, comment_parser)).parse_next(input)?;
57        let term = TermR::parser
58            .context(StrContext::Label("Term"))
59            .parse_next(input)?;
60        comment_parser.parse_next(input)?;
61        Ok(Command { gates, term })
62    }
63}
phase_rs/command.rs

phase_rs/
command.rs
