Skip to content

Commit bf80f0d

Browse files
committed
Attempting to add bus constraints parsing, may need rework
1 parent 94875cd commit bf80f0d

File tree

11 files changed

+185
-15
lines changed

11 files changed

+185
-15
lines changed

air/src/passes/translate_from_ast.rs

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -297,7 +297,8 @@ impl<'a> AirBuilder<'a> {
297297
}
298298
ast::Statement::Enforce(_)
299299
| ast::Statement::EnforceIf(_, _)
300-
| ast::Statement::EnforceAll(_) => {
300+
| ast::Statement::EnforceAll(_)
301+
| ast::Statement::BusEnforce(_) => {
301302
unreachable!()
302303
}
303304
}
@@ -447,7 +448,9 @@ impl<'a> AirBuilder<'a> {
447448
panic!("expected scalar expression to produce scalar value, got: {invalid:?}")
448449
}
449450
},
450-
ast::ScalarExpr::Call(_) | ast::ScalarExpr::BoundedSymbolAccess(_) => unreachable!(),
451+
ast::ScalarExpr::Call(_)
452+
| ast::ScalarExpr::BoundedSymbolAccess(_)
453+
| ast::ScalarExpr::BusOperation(_) => unreachable!(),
451454
}
452455
}
453456

mir/src/passes/translate.rs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -373,6 +373,7 @@ impl<'a> MirBuilder<'a> {
373373
ast::Statement::Enforce(enf) => self.translate_enforce(enf),
374374
ast::Statement::EnforceIf(enf, cond) => self.translate_enforce_if(enf, cond),
375375
ast::Statement::EnforceAll(list_comp) => self.translate_enforce_all(list_comp),
376+
ast::Statement::BusEnforce(_) => todo!(),
376377
}
377378
}
378379
fn translate_let(&mut self, let_stmt: &'a ast::Let) -> Result<Link<Op>, CompileError> {
@@ -807,6 +808,7 @@ impl<'a> MirBuilder<'a> {
807808
ast::ScalarExpr::Binary(b) => self.translate_binary_op(b),
808809
ast::ScalarExpr::Call(c) => self.translate_call(c),
809810
ast::ScalarExpr::Let(l) => self.translate_let(l),
811+
ast::ScalarExpr::BusOperation(_) => todo!(),
810812
}
811813
}
812814

parser/src/ast/declarations.rs

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -104,6 +104,22 @@ pub enum BusType {
104104
Mult,
105105
}
106106

107+
#[derive(Debug, Clone, PartialEq, Eq)]
108+
pub enum BusOperator {
109+
/// Add a tuple to the bus
110+
Add,
111+
/// Remove a tuple from the bus
112+
Rem,
113+
}
114+
impl std::fmt::Display for BusOperator {
115+
fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
116+
match self {
117+
Self::Add => write!(f, "add"),
118+
Self::Rem => write!(f, "rem"),
119+
}
120+
}
121+
}
122+
107123
impl Eq for Bus {}
108124
impl PartialEq for Bus {
109125
fn eq(&self, other: &Self) -> bool {

parser/src/ast/display.rs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -111,6 +111,7 @@ impl<'a> fmt::Display for DisplayStatement<'a> {
111111
write!(f, "enf {}", expr)
112112
}
113113
Statement::Expr(ref expr) => write!(f, "return {}", expr),
114+
Statement::BusEnforce(ref expr) => write!(f, "bus_enf {}", expr),
114115
}
115116
}
116117
}

parser/src/ast/expression.rs

Lines changed: 53 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -441,6 +441,7 @@ impl TryFrom<ScalarExpr> for Expr {
441441
Err(InvalidExprError::BoundedSymbolAccess(expr.span()))
442442
}
443443
ScalarExpr::Let(expr) => Ok(Self::Let(expr)),
444+
ScalarExpr::BusOperation(_) => todo!(),
444445
}
445446
}
446447
}
@@ -489,6 +490,8 @@ pub enum ScalarExpr {
489490
/// binary expressions or function calls to a block of statements, and only when the result
490491
/// of evaluating the `let` produces a valid scalar expression.
491492
Let(Box<Let>),
493+
/// A bus operation
494+
BusOperation(BusOperation),
492495
}
493496
impl ScalarExpr {
494497
/// Returns true if this is a constant value
@@ -523,6 +526,7 @@ impl ScalarExpr {
523526
},
524527
Self::Call(ref expr) => Ok(expr.ty),
525528
Self::Let(ref expr) => Ok(expr.ty()),
529+
Self::BusOperation(_) => todo!(),
526530
}
527531
}
528532
}
@@ -579,6 +583,7 @@ impl fmt::Debug for ScalarExpr {
579583
Self::Binary(ref expr) => f.debug_tuple("Binary").field(expr).finish(),
580584
Self::Call(ref expr) => f.debug_tuple("Call").field(expr).finish(),
581585
Self::Let(ref expr) => write!(f, "{:#?}", expr),
586+
Self::BusOperation(ref expr) => f.debug_tuple("BusOp").field(expr).finish(),
582587
}
583588
}
584589
}
@@ -598,6 +603,7 @@ impl fmt::Display for ScalarExpr {
598603
};
599604
write!(f, "{display}")
600605
}
606+
Self::BusOperation(ref expr) => write!(f, "{}", expr),
601607
}
602608
}
603609
}
@@ -1256,6 +1262,53 @@ impl fmt::Display for ListComprehension {
12561262
}
12571263
}
12581264

1265+
#[derive(Clone, Spanned)]
1266+
pub struct BusOperation {
1267+
#[span]
1268+
pub span: SourceSpan,
1269+
pub bus: ResolvableIdentifier,
1270+
pub op: BusOperator,
1271+
pub args: Vec<Expr>,
1272+
}
1273+
1274+
impl BusOperation {
1275+
pub fn new(span: SourceSpan, bus: Identifier, op: BusOperator, args: Vec<Expr>) -> Self {
1276+
Self {
1277+
span,
1278+
bus: ResolvableIdentifier::Unresolved(NamespacedIdentifier::Bus(bus)),
1279+
op,
1280+
args,
1281+
}
1282+
}
1283+
}
1284+
1285+
impl Eq for BusOperation {}
1286+
impl PartialEq for BusOperation {
1287+
fn eq(&self, other: &Self) -> bool {
1288+
self.bus == other.bus && self.args == other.args && self.op == other.op
1289+
}
1290+
}
1291+
impl fmt::Debug for BusOperation {
1292+
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
1293+
f.debug_struct("BusOperation")
1294+
.field("bus", &self.bus)
1295+
.field("op", &self.op)
1296+
.field("args", &self.args)
1297+
.finish()
1298+
}
1299+
}
1300+
impl fmt::Display for BusOperation {
1301+
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
1302+
write!(
1303+
f,
1304+
"{}{}{}",
1305+
self.bus,
1306+
self.op,
1307+
DisplayTuple(self.args.as_slice())
1308+
)
1309+
}
1310+
}
1311+
12591312
/// Represents a function call (either a pure function or an evaluator).
12601313
///
12611314
/// Calls are permitted in a scalar expression context, but arguments to the

parser/src/ast/statement.rs

Lines changed: 10 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -60,6 +60,8 @@ pub enum Statement {
6060
/// Just like `Enforce`, except the constraint is contained in the body of a list comprehension,
6161
/// and must be enforced on every value produced by that comprehension.
6262
EnforceAll(ListComprehension),
63+
/// Declares a bus related constraint
64+
BusEnforce(ListComprehension),
6365
}
6466
impl Statement {
6567
/// Checks this statement to see if it contains any constraints
@@ -69,7 +71,10 @@ impl Statement {
6971
/// one or more constraints in its body.
7072
pub fn has_constraints(&self) -> bool {
7173
match self {
72-
Self::Enforce(_) | Self::EnforceIf(_, _) | Self::EnforceAll(_) => true,
74+
Self::Enforce(_)
75+
| Self::EnforceIf(_, _)
76+
| Self::EnforceAll(_)
77+
| Self::BusEnforce(_) => true,
7378
Self::Let(Let { body, .. }) => body.iter().any(|s| s.has_constraints()),
7479
Self::Expr(_) => false,
7580
}
@@ -161,9 +166,10 @@ impl Let {
161166
last = let_expr.body.last();
162167
}
163168
Statement::Expr(ref expr) => return expr.ty(),
164-
Statement::Enforce(_) | Statement::EnforceIf(_, _) | Statement::EnforceAll(_) => {
165-
break
166-
}
169+
Statement::Enforce(_)
170+
| Statement::EnforceIf(_, _)
171+
| Statement::EnforceAll(_)
172+
| Statement::BusEnforce(_) => break,
167173
}
168174
}
169175

parser/src/ast/visit.rs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -586,6 +586,7 @@ where
586586
}
587587
ast::Statement::EnforceAll(ref mut expr) => visitor.visit_mut_enforce_all(expr),
588588
ast::Statement::Expr(ref mut expr) => visitor.visit_mut_expr(expr),
589+
ast::Statement::BusEnforce(ref mut _expr) => todo!(),
589590
}
590591
}
591592

@@ -647,6 +648,7 @@ where
647648
ast::ScalarExpr::Binary(ref mut expr) => visitor.visit_mut_binary_expr(expr),
648649
ast::ScalarExpr::Call(ref mut expr) => visitor.visit_mut_call(expr),
649650
ast::ScalarExpr::Let(ref mut expr) => visitor.visit_mut_let(expr),
651+
ast::ScalarExpr::BusOperation(ref mut _expr) => todo!(),
650652
}
651653
}
652654

parser/src/lexer/mod.rs

Lines changed: 16 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -84,6 +84,8 @@ pub enum Token {
8484
DeclIdentRef(Symbol),
8585
/// A function identifier
8686
FunctionIdent(Symbol),
87+
/// A bus identifier
88+
BusIdent(Symbol),
8789
/// Integers should only contain numeric characters.
8890
Num(u64),
8991

@@ -122,8 +124,14 @@ pub enum Token {
122124
Buses,
123125
/// Used to represent a multiset bus declaration.
124126
Unit,
125-
/// Used to represent a logup bus declaration.
127+
/// Used to represent a logup bus declaration.
126128
Mult,
129+
/// Used to represent an empty bus
130+
Null,
131+
/// Used to represent the addition of a given tuple to a bus
132+
Add,
133+
/// Used to represent the removal of a given tuple to a bus
134+
Rem,
127135

128136
// BOUNDARY CONSTRAINT KEYWORDS
129137
// --------------------------------------------------------------------------------------------
@@ -199,6 +207,9 @@ impl Token {
199207
"buses" => Self::Buses,
200208
"unit" => Self::Unit,
201209
"mult" => Self::Mult,
210+
"null" => Self::Null,
211+
"add" => Self::Add,
212+
"rem" => Self::Rem,
202213
"boundary_constraints" => Self::BoundaryConstraints,
203214
"integrity_constraints" => Self::IntegrityConstraints,
204215
"first" => Self::First,
@@ -257,6 +268,7 @@ impl fmt::Display for Token {
257268
Self::Ident(ref id) => write!(f, "{}", id),
258269
Self::DeclIdentRef(ref id) => write!(f, "{}", id),
259270
Self::FunctionIdent(ref id) => write!(f, "{}", id),
271+
Self::BusIdent(ref id) => write!(f, "{}", id),
260272
Self::Num(ref i) => write!(f, "{}", i),
261273
Self::Def => write!(f, "def"),
262274
Self::Mod => write!(f, "mod"),
@@ -275,6 +287,9 @@ impl fmt::Display for Token {
275287
Self::Buses => write!(f, "buses"),
276288
Self::Unit => write!(f, "unit"),
277289
Self::Mult => write!(f, "mult"),
290+
Self::Null => write!(f, "null"),
291+
Self::Add => write!(f, "add"),
292+
Self::Rem => write!(f, "rem"),
278293
Self::BoundaryConstraints => write!(f, "boundary_constraints"),
279294
Self::First => write!(f, "first"),
280295
Self::Last => write!(f, "last"),

parser/src/parser/grammar.lalrpop

Lines changed: 54 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -361,6 +361,7 @@ ConstraintStatements: Vec<Statement> = {
361361
ConstraintStatement: Vec<Statement> = {
362362
"enf" "match" "{" <MatchArm+> "}" ";" => <>,
363363
"enf" <ConstraintExpr> ";" => vec![<>],
364+
<BusConstraintExpr> ";" => vec![<>],
364365
}
365366

366367
ReturnStatement: Expr = {
@@ -426,15 +427,60 @@ ConstraintExpr: Statement = {
426427
}
427428
}
428429

430+
// 1. `p.add(a, b) when s`
431+
// 2. `q.add(a, b) for m`
432+
BusConstraintExpr: Statement = {
433+
<l:@L> <expr: ScalarBusConstraintExpr> <selector: WithSelector> <r:@R> => {
434+
let generated_name = format!("%{}", *next_var);
435+
*next_var += 1;
436+
let generated_binding = Identifier::new(SourceSpan::UNKNOWN, Symbol::intern(generated_name));
437+
let context = vec![(generated_binding, Expr::Range(RangeExpr::from(0..1)))];
438+
Statement::BusEnforce(ListComprehension::new(span!(l, r), expr, context, Some(selector)))
439+
},
440+
<l:@L> <expr: ScalarBusConstraintExpr> <multiplicity: WithMultiplicity> <r:@R> => {
441+
let generated_name = format!("%{}", *next_var);
442+
*next_var += 1;
443+
let generated_binding = Identifier::new(SourceSpan::UNKNOWN, Symbol::intern(generated_name));
444+
let context = vec![(generated_binding, Expr::Range(RangeExpr::from(0..1)))];
445+
Statement::BusEnforce(ListComprehension::new(span!(l, r), expr, context, Some(multiplicity)))
446+
}
447+
}
448+
449+
// 1. `p.first = null`
450+
// 2. `q.first = ???` To define
451+
BoundaryBusConstraintExpr: Statement = {
452+
<l:@L> <expr: ScalarBusConstraintExpr> <r:@R> => {
453+
let generated_name = format!("%{}", *next_var);
454+
*next_var += 1;
455+
let generated_binding = Identifier::new(SourceSpan::UNKNOWN, Symbol::intern(generated_name));
456+
let context = vec![(generated_binding, Expr::Range(RangeExpr::from(0..1)))];
457+
Statement::BusEnforce(ListComprehension::new(span!(l, r), expr, context, None))
458+
}
459+
}
460+
429461
ScalarConstraintExpr: ScalarExpr = {
430462
FunctionCall,
431463
<l:@L> <lhs: ScalarExpr> "=" <rhs: ScalarExpr> <r:@R>
432464
=> ScalarExpr::Binary(BinaryExpr::new(span!(l, r), BinaryOp::Eq, lhs, rhs)),
433465
}
434466

467+
ScalarBusConstraintExpr: ScalarExpr = {
468+
<l:@L> <bus: BusIdentifier> "." <bus_operation: BusOperator> "(" <args: Comma<Expr>> ")" <r:@R> => {
469+
ScalarExpr::BusOperation(BusOperation::new(span!(l, r), bus, bus_operation, args))
470+
}
471+
}
472+
473+
BusOperator: BusOperator = {
474+
"add" => BusOperator::Add,
475+
"rem" => BusOperator::Rem
476+
}
477+
435478
WithSelector: ScalarExpr = {
436479
"when" <ScalarExpr>,
437480
}
481+
WithMultiplicity: ScalarExpr = {
482+
"for" <ScalarExpr>,
483+
}
438484

439485
Expr: Expr = {
440486
<ScalarExpr> =>? {
@@ -634,6 +680,10 @@ FunctionIdentifier: Identifier = {
634680
<l:@L> <name:function_identifier> <r:@R> => Identifier::new(span!(l, r), name)
635681
}
636682

683+
BusIdentifier: Identifier = {
684+
<l:@L> <name:bus_identifier> <r:@R> => Identifier::new(span!(l, r), name)
685+
}
686+
637687
Int: Span<u64> = {
638688
<l:@L> <i:Num_u64> <r:@R> => Span::new(span!(l, r), i),
639689
}
@@ -653,6 +703,7 @@ extern {
653703
identifier => Token::Ident(<Symbol>),
654704
decl_ident_ref => Token::DeclIdentRef(<Symbol>),
655705
function_identifier => Token::FunctionIdent(<Symbol>),
706+
bus_identifier => Token::BusIdent(<Symbol>),
656707
int => Token::Num(<u64>),
657708
"def" => Token::Def,
658709
"mod" => Token::Mod,
@@ -670,6 +721,9 @@ extern {
670721
"buses" => Token::Buses,
671722
"unit" => Token::Unit,
672723
"mult" => Token::Mult,
724+
"null" => Token::Null,
725+
"add" => Token::Add,
726+
"rem" => Token::Rem,
673727
"boundary_constraints" => Token::BoundaryConstraints,
674728
"first" => Token::First,
675729
"last" => Token::Last,

parser/src/transforms/constant_propagation.rs

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -275,12 +275,14 @@ impl<'a> VisitMut<SemanticAnalysisError> for ConstantPropagation<'a> {
275275
}
276276
Statement::Enforce(_)
277277
| Statement::EnforceIf(_, _)
278-
| Statement::EnforceAll(_) => unreachable!(),
278+
| Statement::EnforceAll(_)
279+
| Statement::BusEnforce(_) => unreachable!(),
279280
},
280281
Err(err) => return ControlFlow::Break(err),
281282
}
282283
ControlFlow::Continue(())
283284
}
285+
ScalarExpr::BusOperation(_) => todo!(),
284286
}
285287
}
286288

@@ -591,7 +593,8 @@ impl<'a> VisitMut<SemanticAnalysisError> for ConstantPropagation<'a> {
591593
}
592594
Statement::Enforce(_)
593595
| Statement::EnforceIf(_, _)
594-
| Statement::EnforceAll(_) => unreachable!(),
596+
| Statement::EnforceAll(_)
597+
| Statement::BusEnforce(_) => unreachable!(),
595598
},
596599
Err(err) => return ControlFlow::Break(err),
597600
}
@@ -642,6 +645,7 @@ impl<'a> VisitMut<SemanticAnalysisError> for ConstantPropagation<'a> {
642645
}
643646
// This statement type is only present in the AST after inlining
644647
Statement::EnforceIf(_, _) => unreachable!(),
648+
Statement::BusEnforce(_) => todo!(),
645649
}
646650

647651
// If we have a non-empty buffer, then we are collapsing a let into the current block,

0 commit comments

Comments
 (0)