diff --git a/tamer/src/asg/graph/object/expr.rs b/tamer/src/asg/graph/object/expr.rs index 3b094fde..c0b39295 100644 --- a/tamer/src/asg/graph/object/expr.rs +++ b/tamer/src/asg/graph/object/expr.rs @@ -41,7 +41,7 @@ use super::ObjectKind; /// all child expressions, /// but also any applicable closing span. #[derive(Debug, PartialEq, Eq)] -pub struct Expr(ExprOp, ExprDim, Span); +pub struct Expr(pub ExprOp, ExprDim, Span); impl Expr { pub fn new(op: ExprOp, span: Span) -> Self { @@ -102,12 +102,15 @@ pub enum ExprOp { Conj, /// Logical disjunction (∨) Disj, + /// Equality predicate (=) + Eq, } impl Display for ExprOp { fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result { use ExprOp::*; + // "{self} expression" match self { Sum => write!(f, "sum (+)"), Product => write!(f, "product (×)"), @@ -115,6 +118,7 @@ impl Display for ExprOp { Floor => write!(f, "floor (⌊)"), Conj => write!(f, "conjunctive (∧)"), Disj => write!(f, "disjunctive (∨)"), + Eq => write!(f, "equality (=)"), } } } diff --git a/tamer/src/asg/graph/xmli.rs b/tamer/src/asg/graph/xmli.rs index 50c08e70..cd216c04 100644 --- a/tamer/src/asg/graph/xmli.rs +++ b/tamer/src/asg/graph/xmli.rs @@ -191,8 +191,8 @@ impl<'a> TreeContext<'a> { depth, )), - Object::Expr((expr, _)) => { - self.emit_expr(expr, paired_rel.source(), depth) + Object::Expr((expr, oi_expr)) => { + self.emit_expr(expr, *oi_expr, paired_rel.source(), depth) } Object::Tpl((tpl, oi_tpl)) => { @@ -243,6 +243,7 @@ impl<'a> TreeContext<'a> { fn emit_expr( &mut self, expr: &Expr, + oi_expr: ObjectIndex, src: &Object, depth: Depth, ) -> Option { @@ -250,7 +251,25 @@ impl<'a> TreeContext<'a> { Object::Ident((ident, _)) => { self.emit_expr_ident(expr, ident, depth) } - _ => Some(expr_ele(expr, depth)), + Object::Expr((pexpr, _)) => match (pexpr.op(), expr.op()) { + (ExprOp::Conj | ExprOp::Disj, ExprOp::Eq) => { + Some(self.emit_match(expr, oi_expr, depth)) + } + _ => Some(expr_ele(expr, oi_expr, depth)), + }, + // TODO: See `:tamer/tests/xmli/template` regarding `match` and + // `when`/`c:*`; + // this is not an ambiguity that can be resolved without + // adding more information to the graph, + // but is hopefully one that we can avoid. + Object::Tpl(..) => match expr.op() { + ExprOp::Eq => Some(self.emit_match(expr, oi_expr, depth)), + _ => Some(expr_ele(expr, oi_expr, depth)), + }, + // TODO: Perhaps errors for Root and Meta? + Object::Root(_) | Object::Pkg(_) | Object::Meta(_) => { + Some(expr_ele(expr, oi_expr, depth)) + } } } @@ -268,7 +287,11 @@ impl<'a> TreeContext<'a> { ExprOp::Sum => (QN_RATE, QN_YIELDS), ExprOp::Conj => (QN_CLASSIFY, QN_AS), - ExprOp::Product | ExprOp::Ceil | ExprOp::Floor | ExprOp::Disj => { + ExprOp::Product + | ExprOp::Ceil + | ExprOp::Floor + | ExprOp::Disj + | ExprOp::Eq => { todo!("stmt: {expr:?}") } }; @@ -283,6 +306,47 @@ impl<'a> TreeContext<'a> { )) } + /// Emit a match expression. + /// + /// This is intended as a classify/any/all child. + fn emit_match( + &mut self, + expr: &Expr, + oi_expr: ObjectIndex, + depth: Depth, + ) -> Xirf { + let mut edges = oi_expr.edges_filtered::(self.asg); + + // note: the edges are reversed (TODO?) + let value = edges + .next() + .diagnostic_expect( + || vec![oi_expr.note("for this match")], + "missing @value ref", + ) + .resolve(self.asg); + + let on = edges + .next() + .diagnostic_expect( + || vec![oi_expr.note("for this match")], + "missing @on ref", + ) + .resolve(self.asg); + + if let Some(unexpected) = edges.next() { + diagnostic_panic!( + vec![unexpected.error("a third ref was unexpected")], + "unexpected third ref during match generation", + ); + } + + self.push(attr_value(value.name())); + self.push(attr_on(on.name())); + + Xirf::open(QN_MATCH, OpenSpan::without_name_span(expr.span()), depth) + } + /// Emit a template definition or application. fn emit_template( &mut self, @@ -450,11 +514,15 @@ fn attr_name(name: SPair) -> Xirf { Xirf::attr(QN_NAME, name, (name.span(), name.span())) } +fn attr_on(on: SPair) -> Xirf { + Xirf::attr(QN_ON, on, (on.span(), on.span())) +} + fn attr_value(val: SPair) -> Xirf { Xirf::attr(QN_VALUE, val, (val.span(), val.span())) } -fn expr_ele(expr: &Expr, depth: Depth) -> Xirf { +fn expr_ele(expr: &Expr, oi_expr: ObjectIndex, depth: Depth) -> Xirf { use ExprOp::*; let qname = match expr.op() { @@ -464,6 +532,11 @@ fn expr_ele(expr: &Expr, depth: Depth) -> Xirf { Floor => QN_C_FLOOR, Conj => QN_ALL, Disj => QN_ANY, + + Eq => diagnostic_panic!( + vec![oi_expr.error("unsupported expression type in this context")], + "cannot derive expression of this type in this context", + ), }; Xirf::open(qname, OpenSpan::without_name_span(expr.span()), depth) diff --git a/tamer/src/nir.rs b/tamer/src/nir.rs index 5a276d6c..5f8bf190 100644 --- a/tamer/src/nir.rs +++ b/tamer/src/nir.rs @@ -228,6 +228,8 @@ pub enum NirEntity { All, /// Disjunctive (∨) expression. Any, + /// Logical predicate. + Match, /// Template. Tpl, @@ -275,6 +277,7 @@ impl Display for NirEntity { Classify => write!(f, "classification"), All => write!(f, "conjunctive (∧) expression"), Any => write!(f, "disjunctive (∨) expression"), + Match => write!(f, "logical predicate (match)"), Tpl => write!(f, "template"), TplParam => write!(f, "template param (metavariable)"), diff --git a/tamer/src/nir/air.rs b/tamer/src/nir/air.rs index 18e948a8..1cced448 100644 --- a/tamer/src/nir/air.rs +++ b/tamer/src/nir/air.rs @@ -21,8 +21,14 @@ use super::Nir; use crate::{ - asg::air::Air, diagnose::Diagnostic, parse::prelude::*, span::UNKNOWN_SPAN, + asg::air::Air, + diagnose::{Annotate, Diagnostic}, + fmt::{DisplayWrapper, TtQuote}, + parse::prelude::*, + span::{Span, UNKNOWN_SPAN}, + sym::{st::raw::U_TRUE, SymbolId}, }; +use arrayvec::ArrayVec; use std::{error::Error, fmt::Display}; // These are also used by the `test` module which imports `super`. @@ -36,6 +42,13 @@ use crate::{ pub enum NirToAir { #[default] Ready, + + /// Predicate opened but its subject is not yet known. + PredOpen(Span), + + /// A predicate has been partially applied to its subject, + /// but we do not yet know its function or comparison value. + PredPartial(Span, SPair), } impl Display for NirToAir { @@ -44,17 +57,30 @@ impl Display for NirToAir { match self { Ready => write!(f, "ready to lower NIR to AIR"), + PredOpen(_) => { + write!(f, "awaiting information about open predicate") + } + PredPartial(_, name) => write!( + f, + "waiting to determine type of predicate for identifier {}", + TtQuote::wrap(name), + ), } } } -type QueuedObj = Option; +/// Stack of [`Air`] objects to yield on subsequent iterations. +type ObjStack = ArrayVec; + +/// The symbol to use when lexically expanding shorthand notations to +/// compare against values of `1`. +pub const SYM_TRUE: SymbolId = U_TRUE; impl ParseState for NirToAir { type Token = Nir; type Object = Air; type Error = NirToAirError; - type Context = QueuedObj; + type Context = ObjStack; #[cfg(not(feature = "wip-asg-derived-xmli"))] fn parse_token( @@ -72,14 +98,14 @@ impl ParseState for NirToAir { fn parse_token( self, tok: Self::Token, - queue: &mut Self::Context, + stack: &mut Self::Context, ) -> TransitionResult { use NirToAir::*; + use NirToAirError::*; - use crate::{diagnose::Annotate, diagnostic_panic}; + use crate::diagnostic_panic; - // Single-item "queue". - if let Some(obj) = queue.take() { + if let Some(obj) = stack.pop() { return Transition(Ready).ok(obj).with_lookahead(tok); } @@ -111,6 +137,41 @@ impl ParseState for NirToAir { Transition(Ready).ok(Air::ExprStart(ExprOp::Disj, span)) } + // Match + (Ready, Open(Match, span)) => { + Transition(PredOpen(span)).incomplete() + } + (PredOpen(ospan), RefSubject(on)) => { + Transition(PredPartial(ospan, on)).incomplete() + } + (PredPartial(ospan, on), Ref(value)) => { + stack.push(Air::RefIdent(value)); + stack.push(Air::RefIdent(on)); + Transition(Ready).ok(Air::ExprStart(ExprOp::Eq, ospan)) + } + (PredPartial(ospan, on), Close(Match, cspan)) => { + stack.push(Air::RefIdent(SPair(SYM_TRUE, ospan))); + stack.push(Air::RefIdent(on)); + Transition(Ready) + .ok(Air::ExprStart(ExprOp::Eq, ospan)) + .with_lookahead(Close(Match, cspan)) + } + // Special case of the general error below, + // since recovery here involves discarding the nonsense match. + (PredOpen(ospan), Close(Match, span)) => Transition(Ready) + .err(MatchSubjectExpected(ospan, Close(Match, span))), + (PredOpen(ospan), tok) => Transition(PredOpen(ospan)) + .err(MatchSubjectExpected(ospan, tok)), + (Ready, Close(Match, cspan)) => { + Transition(Ready).ok(Air::ExprEnd(cspan)) + } + (PredPartial(ospan, on), tok) => { + // TODO: Until match body is supported, + // error and discard tokens. + Transition(PredPartial(ospan, on)) + .err(TodoMatchBody(ospan, tok.span())) + } + (Ready, Open(Tpl, span)) => { Transition(Ready).ok(Air::TplStart(span)) } @@ -183,14 +244,23 @@ impl ParseState for NirToAir { } } - fn is_accepting(&self, _: &Self::Context) -> bool { - true + fn is_accepting(&self, stack: &Self::Context) -> bool { + matches!(self, Self::Ready) && stack.is_empty() } } #[derive(Debug, PartialEq, Eq)] pub enum NirToAirError { - Todo, + /// Expected a match subject, + /// but encountered some other token. + /// + /// TODO: "match subject" is not familiar terminology to the user; + /// we'll want to introduce a layer permitting XML-specific augmenting + /// with `@on` when derived from an XML source. + MatchSubjectExpected(Span, Nir), + + /// Match body is not yet supported. + TodoMatchBody(Span, Span), } impl Display for NirToAirError { @@ -198,17 +268,40 @@ impl Display for NirToAirError { use NirToAirError::*; match self { - Todo => write!(f, "TODO"), + MatchSubjectExpected(_, nir) => { + write!(f, "expected match subject, found {nir}") + } + + TodoMatchBody(_, _) => { + write!(f, "match body is not yet supported by TAMER") + } } } } impl Error for NirToAirError {} +// TODO: We need to be able to augment with useful context, +// e.g. XML suggestions. impl Diagnostic for NirToAirError { fn describe(&self) -> Vec { - // TODO - vec![] + use NirToAirError::*; + + match self { + MatchSubjectExpected(ospan, given) => vec![ + ospan.note("for this match"), + given + .span() + .error("comparison value provided before subject"), + ], + + TodoMatchBody(ospan, given) => vec![ + ospan.note("for this match"), + given.error( + "tokens in match body are not yet supported by TAMER", + ), + ], + } } } diff --git a/tamer/src/nir/air/test.rs b/tamer/src/nir/air/test.rs index 7a247139..a3fb1e92 100644 --- a/tamer/src/nir/air/test.rs +++ b/tamer/src/nir/air/test.rs @@ -22,7 +22,7 @@ use crate::{parse::util::SPair, span::dummy::*}; type Sut = NirToAir; -use Parsed::Object as O; +use Parsed::{Incomplete, Object as O}; #[test] fn package_to_pkg() { @@ -213,3 +213,133 @@ fn apply_template_long_form_args() { Sut::parse(toks.into_iter()).collect(), ); } + +// Short-hand matches with no value desugar to an equality check +// against `TRUE`. +#[test] +fn match_short_no_value() { + let name = SPair("matchOn".into(), S2); + + #[rustfmt::skip] + let toks = vec![ + Open(Match, S1), + RefSubject(name), // @on + Close(Match, S3), + ]; + + assert_eq!( + #[rustfmt::skip] + Ok(vec![ + // When first encountering a `Match`, + // we do not know what predicate needs to be emitted for AIR. + Incomplete, + // Nor do we know when encountering an identifier, + // which serves as the first argument to the yet-to-be-known + // predicate. + Incomplete, + // Once closing, + // we default to an equality check against `TRUE`. + O(Air::ExprStart(ExprOp::Eq, S1)), + O(Air::RefIdent(name)), + O(Air::RefIdent(SPair(SYM_TRUE, S1))), + O(Air::ExprEnd(S3)), + ]), + Sut::parse(toks.into_iter()).collect(), + ); +} + +// Same as above but _not_ defaulted to `TRUE`. +#[test] +fn match_short_with_value() { + let name = SPair("matchOn".into(), S2); + let value = SPair("value".into(), S3); + + #[rustfmt::skip] + let toks = vec![ + Open(Match, S1), + RefSubject(name), // @on + Ref(value), // @value + Close(Match, S4), + ]; + + // See notes from `match_short_no_value`, + // which are not duplicated here. + assert_eq!( + #[rustfmt::skip] + Ok(vec![ + Incomplete, + Incomplete, + O(Air::ExprStart(ExprOp::Eq, S1)), + O(Air::RefIdent(name)), + // Rather than defaulting to `SYM_TRUE` as above, + // we use the _user-provided_ value. + O(Air::RefIdent(value)), + O(Air::ExprEnd(S4)), + ]), + Sut::parse(toks.into_iter()).collect(), + ); +} + +// Equivalently stated in XML: `match/@value` before `match/@on`; +// NIR imposes ordering, +// such that the `@on` must come first. +#[test] +fn match_short_value_before_subject_err() { + let name = SPair("matchOn".into(), S2); + + #[rustfmt::skip] + let toks = vec![ + Open(Match, S1), + Ref(name), // @value, not @on + + // RECOVERY: Provide the subject + RefSubject(name), + Close(Match, S3), + ]; + + assert_eq!( + #[rustfmt::skip] + vec![ + Ok(Incomplete), // Open + // We were expecting RefSubject (@on) but got Ref (@value) + Err(ParseError::StateError( + NirToAirError::MatchSubjectExpected(S1, Ref(name)) + )), + // RECOVERY: Subject is provided. + Ok(Incomplete), + // And we then close as an eq match on TRUE, + // because no value has been provided + // (rather the value was consumed in the error). + Ok(O(Air::ExprStart(ExprOp::Eq, S1))), + Ok(O(Air::RefIdent(name))), + Ok(O(Air::RefIdent(SPair(SYM_TRUE, S1)))), + Ok(O(Air::ExprEnd(S3))), + ], + Sut::parse(toks.into_iter()).collect::>>(), + ); +} + +// Closing a match before providing any arguments. +#[test] +fn match_no_args_err() { + #[rustfmt::skip] + let toks = vec![ + Open(Match, S1), + // No refs. + Close(Match, S2), + // RECOVERY: We have no choice but to discard the above match. + ]; + + assert_eq!( + #[rustfmt::skip] + vec![ + Ok(Incomplete), // Open + // We were expecting RefSubject (@on) but closed instead. + Err(ParseError::StateError( + NirToAirError::MatchSubjectExpected(S1, Close(Match, S2)) + )), + // RECOVERY: Useless match above discarded. + ], + Sut::parse(toks.into_iter()).collect::>>(), + ); +} diff --git a/tamer/src/nir/parse.rs b/tamer/src/nir/parse.rs index 0591449c..9cfa7e25 100644 --- a/tamer/src/nir/parse.rs +++ b/tamer/src/nir/parse.rs @@ -581,13 +581,14 @@ ele_parse! { /// /// The dimensionality of the expression will be automatically /// determined by the dimensionality of the matches' [`@on`](QN_ON). - MatchExpr := QN_MATCH { + MatchExpr := QN_MATCH(_, ospan) { @ { - QN_ON => TodoAttr, - QN_VALUE => TodoAttr, + QN_ON => RefSubject, + QN_VALUE => Ref, QN_INDEX => TodoAttr, QN_ANY_OF => TodoAttr, - } => Todo, + } => NirEntity::Match.open(ospan), + /(cspan) => NirEntity::Match.close(cspan), CalcPredExpr, }; diff --git a/tamer/src/sym/prefill.rs b/tamer/src/sym/prefill.rs index 688413b6..2f2b82ee 100644 --- a/tamer/src/sym/prefill.rs +++ b/tamer/src/sym/prefill.rs @@ -725,6 +725,8 @@ pub mod st { L_RETMAP_UUUHEAD: str ":retmap:___head", L_RETMAP_UUUTAIL: str ":retmap:___tail", + U_TRUE: cid "TRUE", + URI_LV_CALC: uri "http://www.lovullo.com/calc", URI_LV_LINKER: uri "http://www.lovullo.com/rater/linker", URI_LV_PREPROC: uri "http://www.lovullo.com/rater/preproc", diff --git a/tamer/tests/xmli/classify/expected.xml b/tamer/tests/xmli/classify/expected.xml index 28d4f96e..f4a63f5f 100644 --- a/tamer/tests/xmli/classify/expected.xml +++ b/tamer/tests/xmli/classify/expected.xml @@ -13,5 +13,13 @@ + + + + + + + + diff --git a/tamer/tests/xmli/classify/src.xml b/tamer/tests/xmli/classify/src.xml index 0982ae30..781beca0 100644 --- a/tamer/tests/xmli/classify/src.xml +++ b/tamer/tests/xmli/classify/src.xml @@ -13,5 +13,13 @@ + + + + + + + + diff --git a/tamer/tests/xmli/template/expected.xml b/tamer/tests/xmli/template/expected.xml index 3e634c96..76312f7f 100644 --- a/tamer/tests/xmli/template/expected.xml +++ b/tamer/tests/xmli/template/expected.xml @@ -170,5 +170,19 @@ + + + + + + + + + + + + diff --git a/tamer/tests/xmli/template/src.xml b/tamer/tests/xmli/template/src.xml index 889dbe25..cb6d558a 100644 --- a/tamer/tests/xmli/template/src.xml +++ b/tamer/tests/xmli/template/src.xml @@ -170,5 +170,19 @@ + This next one is a bit awkward, + because it creates an ambiguity when regenerating XML. + Each of `match`, `when`, and `c:*` are represented the same on the graph, + so it will not be clear until expansion how the body of the below + + The ambiguity will go away once template application is performed by + TAMER in the near future; + until that time, + we cannot support the generation of each of those things within + templates. + +