Skip to content

Commit 289886e

Browse files
rachitnigamrachitnigam
committed
moar
1 parent 649404e commit 289886e

33 files changed

+475
-79
lines changed

‎crates/ast/src/constraint.rs‎

Lines changed: 21 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -6,13 +6,19 @@ pub enum OrderOp {
66
Gt,
77
Gte,
88
Eq,
9+
Lt,
10+
Lte,
11+
Neq,
912
}
1013
impl std::fmt::Display for OrderOp {
1114
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
1215
let op = match self {
1316
OrderOp::Gt => ">",
14-
OrderOp::Eq => "=",
1517
OrderOp::Gte => ">=",
18+
OrderOp::Lt => "<",
19+
OrderOp::Lte => "<=",
20+
OrderOp::Eq => "=",
21+
OrderOp::Neq => "!=",
1622
};
1723
write!(f, "{op}")
1824
}
@@ -48,9 +54,9 @@ where
4854

4955
pub fn lt(l: T, r: T) -> Self {
5056
Self {
51-
left: r,
52-
right: l,
53-
op: OrderOp::Gt,
57+
left: l,
58+
right: r,
59+
op: OrderOp::Lt,
5460
}
5561
}
5662

@@ -72,9 +78,17 @@ where
7278

7379
pub fn lte(l: T, r: T) -> Self {
7480
OrderConstraint {
75-
left: r,
76-
right: l,
77-
op: OrderOp::Gte,
81+
left: l,
82+
right: r,
83+
op: OrderOp::Lte,
84+
}
85+
}
86+
87+
pub fn neq(l: T, r: T) -> Self {
88+
OrderConstraint {
89+
left: l,
90+
right: r,
91+
op: OrderOp::Neq,
7892
}
7993
}
8094
}

‎crates/ast/src/expr.rs‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -365,6 +365,9 @@ impl ECtx {
365365
OrderOp::Gt => ">",
366366
OrderOp::Gte => ">=",
367367
OrderOp::Eq => "=",
368+
OrderOp::Lt => "<",
369+
OrderOp::Lte => "<=",
370+
OrderOp::Neq => "!=",
368371
};
369372
let then = self.print(then);
370373
let alt = self.print(alt);

‎crates/ast/src/parser.rs‎

Lines changed: 12 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -553,16 +553,20 @@ impl FilamentParser {
553553
fn eq(input: Node) -> ParseResult<()> {
554554
Ok(())
555555
}
556+
fn neq(input: Node) -> ParseResult<()> {
557+
Ok(())
558+
}
556559

557560
/// Returns the order operation and whether it is reversed
558561
fn order_op(input: Node) -> ParseResult<(ast::OrderOp, bool)> {
559562
match_nodes!(
560563
input.into_children();
561564
[gt(_)] => Ok((ast::OrderOp::Gt, false)),
562-
[lt(_)] => Ok((ast::OrderOp::Gt, true)),
565+
[lt(_)] => Ok((ast::OrderOp::Lt, false)),
563566
[gte(_)] => Ok((ast::OrderOp::Gte, false)),
564-
[lte(_)] => Ok((ast::OrderOp::Gte, true)),
567+
[lte(_)] => Ok((ast::OrderOp::Lte, false)),
565568
[eq(_)] => Ok((ast::OrderOp::Eq, false)),
569+
[neq(_)] => Ok((ast::OrderOp::Neq, false)),
566570
)
567571
}
568572

@@ -575,28 +579,20 @@ impl FilamentParser {
575579
] => Ok(cond_c),
576580
[
577581
time(l),
578-
order_op((op, rev)),
582+
order_op((op, _)),
579583
time(r)
580584
] => {
581585
let l = l.take();
582586
let r = r.take();
583-
let con = if !rev {
584-
ast::OrderConstraint::new(l, r, op)
585-
} else {
586-
ast::OrderConstraint::new(r, l, op)
587-
};
587+
let con = ast::OrderConstraint::new(l, r, op);
588588
Ok(Loc::new(FCons::TimeC(con), sp))
589589
},
590590
[
591591
expr(l),
592-
order_op((op, rev)),
592+
order_op((op, _)),
593593
expr(r)
594594
] => {
595-
let con = if !rev {
596-
ast::OrderConstraint::new(l.take(), r.take(), op)
597-
} else {
598-
ast::OrderConstraint::new(r.take(), l.take(), op)
599-
};
595+
let con = ast::OrderConstraint::new(l.take(), r.take(), op);
600596
Ok(Loc::new(FCons::ExprC(con), sp))
601597
}
602598
)
@@ -725,12 +721,8 @@ impl FilamentParser {
725721
fn expr_cmp(input: Node) -> ParseResult<ast::OrderConstraint<ast::Expr>> {
726722
Ok(match_nodes!(
727723
input.into_children();
728-
[expr(l), order_op((op, rev)), expr(r)] => {
729-
if !rev {
730-
ast::OrderConstraint::new(l.take(), r.take(), op)
731-
} else {
732-
ast::OrderConstraint::new(r.take(), l.take(), op)
733-
}
724+
[expr(l), order_op((op, _)), expr(r)] => {
725+
ast::OrderConstraint::new(l.take(), r.take(), op)
734726
}
735727
))
736728
}

‎crates/ast/src/syntax.pest‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,8 @@ gte = { ">=" }
3333
lt = { "<" }
3434
lte = { "<=" }
3535
eq = { "==" }
36-
order_op = { gte | gt | lte | lt | eq }
36+
neq = { "!=" }
37+
order_op = { gte | gt | lte | lt | neq | eq }
3738

3839
conditional_constraint = {
3940
expr_cmp ~ "?" ~ constraint ~ ":" ~ constraint

‎crates/filament/src/ast_passes/desugar_conditionals.rs‎

Lines changed: 34 additions & 45 deletions
Original file line numberDiff line numberDiff line change
@@ -15,13 +15,15 @@ impl Visitor for DesugarConditionals {
1515
fn signature(&mut self, sig: &mut ast::Signature) -> Action {
1616
// Process conditional constraints and convert them to facts
1717
let mut new_facts = Vec::new();
18-
18+
1919
for conditional_constraint in &sig.conditional_constraints {
2020
match self.desugar_conditional_constraint(conditional_constraint) {
2121
Ok(facts) => new_facts.extend(facts),
2222
Err(err) => {
2323
// Report error immediately and exit
24-
eprintln!("[ERROR] Conditional constraint desugaring failed:");
24+
eprintln!(
25+
"[ERROR] Conditional constraint desugaring failed:"
26+
);
2527
eprintln!(" - {}", err.kind);
2628
std::process::exit(1);
2729
}
@@ -37,7 +39,6 @@ impl Visitor for DesugarConditionals {
3739
Action::Continue
3840
}
3941
}
40-
4142
}
4243

4344
impl DesugarConditionals {
@@ -131,58 +132,46 @@ impl DesugarConditionals {
131132
// Handle all comparison operators
132133
match condition.op {
133134
OrderOp::Gt => {
134-
// !(a > b) becomes (a <= b), which we represent as (b >= a)
135-
Ok(ast::OrderConstraint::gte(
136-
condition.right.clone(),
135+
// !(a > b) becomes (a <= b)
136+
Ok(ast::OrderConstraint::lte(
137137
condition.left.clone(),
138+
condition.right.clone(),
138139
))
139140
}
140141
OrderOp::Gte => {
141-
// !(a >= b) becomes (a < b), which we represent as (b > a)
142+
// !(a >= b) becomes (a < b)
143+
Ok(ast::OrderConstraint::lt(
144+
condition.left.clone(),
145+
condition.right.clone(),
146+
))
147+
}
148+
OrderOp::Lt => {
149+
// !(a < b) becomes (a >= b)
150+
Ok(ast::OrderConstraint::gte(
151+
condition.left.clone(),
152+
condition.right.clone(),
153+
))
154+
}
155+
OrderOp::Lte => {
156+
// !(a <= b) becomes (a > b)
142157
Ok(ast::OrderConstraint::gt(
158+
condition.left.clone(),
143159
condition.right.clone(),
160+
))
161+
}
162+
OrderOp::Neq => {
163+
// !(a != b) becomes (a == b)
164+
Ok(ast::OrderConstraint::eq(
144165
condition.left.clone(),
166+
condition.right.clone(),
145167
))
146168
}
147169
OrderOp::Eq => {
148-
// !(a == b) - Handle binary/boolean domain cases
149-
if let ast::Expr::Concrete(n) = &condition.right {
150-
// For boolean/binary domains, flip 0<->1
151-
if *n == 0 || *n == 1 {
152-
let negated_val = if *n == 0 { 1 } else { 0 };
153-
Ok(ast::OrderConstraint::eq(
154-
condition.left.clone(),
155-
ast::Expr::concrete(negated_val),
156-
))
157-
} else {
158-
Err(Error::misc(format!(
159-
"Cannot negate equality condition with non-boolean literal: {} == {}",
160-
"expr", n
161-
)))
162-
}
163-
} else if let ast::Expr::Concrete(n) = &condition.left {
164-
// Handle case where left side is the literal
165-
if *n == 0 || *n == 1 {
166-
let negated_val = if *n == 0 { 1 } else { 0 };
167-
Ok(ast::OrderConstraint::eq(
168-
condition.right.clone(),
169-
ast::Expr::concrete(negated_val),
170-
))
171-
} else {
172-
Err(Error::misc(format!(
173-
"Cannot negate equality condition with non-boolean literal: {} == {}",
174-
n, "expr"
175-
)))
176-
}
177-
} else {
178-
// For complex expressions, we can't negate equality directly
179-
// This would require disjunction (A != B means A < B || A > B)
180-
// Since Filament doesn't have disjunction, this is unsupported
181-
Err(Error::misc(
182-
"Cannot negate equality between complex expressions. \
183-
Consider restructuring your constraint to use comparison operators.".to_string()
184-
))
185-
}
170+
// !(a == b) becomes (a != b)
171+
Ok(ast::OrderConstraint::neq(
172+
condition.left.clone(),
173+
condition.right.clone(),
174+
))
186175
}
187176
}
188177
}

‎crates/ir/src/from_ast/astconv.rs‎

Lines changed: 42 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -303,8 +303,28 @@ impl BuildCtx<'_> {
303303
ast::OrderOp::Gt => Cmp::Gt,
304304
ast::OrderOp::Gte => Cmp::Gte,
305305
ast::OrderOp::Eq => Cmp::Eq,
306+
ast::OrderOp::Lt => Cmp::Gt, // Convert a < b to b > a
307+
ast::OrderOp::Lte => Cmp::Gte, // Convert a <= b to b >= a
308+
ast::OrderOp::Neq => {
309+
// Handle != by creating NOT(a == b)
310+
let eq_prop = self.comp().add(ir::Prop::Cmp(ir::CmpOp {
311+
lhs,
312+
op: Cmp::Eq,
313+
rhs,
314+
}));
315+
return Ok(eq_prop.not(self.comp()));
316+
}
317+
};
318+
// For Lt and Lte, we need to swap operands
319+
let (final_lhs, final_rhs) = match cons.op {
320+
ast::OrderOp::Lt | ast::OrderOp::Lte => (rhs, lhs),
321+
_ => (lhs, rhs),
306322
};
307-
Ok(self.comp().add(ir::Prop::Cmp(ir::CmpOp { lhs, op, rhs })))
323+
Ok(self.comp().add(ir::Prop::Cmp(ir::CmpOp {
324+
lhs: final_lhs,
325+
op,
326+
rhs: final_rhs,
327+
})))
308328
}
309329

310330
fn event_cons(
@@ -317,10 +337,28 @@ impl BuildCtx<'_> {
317337
ast::OrderOp::Gt => Cmp::Gt,
318338
ast::OrderOp::Gte => Cmp::Gte,
319339
ast::OrderOp::Eq => Cmp::Eq,
340+
ast::OrderOp::Lt => Cmp::Gt, // Convert a < b to b > a
341+
ast::OrderOp::Lte => Cmp::Gte, // Convert a <= b to b >= a
342+
ast::OrderOp::Neq => {
343+
// Handle != by creating NOT(a == b)
344+
let eq_prop = self.comp().add(ir::Prop::TimeCmp(ir::CmpOp {
345+
lhs,
346+
op: Cmp::Eq,
347+
rhs,
348+
}));
349+
return Ok(eq_prop.not(self.comp()));
350+
}
351+
};
352+
// For Lt and Lte, we need to swap operands
353+
let (final_lhs, final_rhs) = match cons.op {
354+
ast::OrderOp::Lt | ast::OrderOp::Lte => (rhs, lhs),
355+
_ => (lhs, rhs),
320356
};
321-
Ok(self
322-
.comp()
323-
.add(ir::Prop::TimeCmp(ir::CmpOp { lhs, op, rhs })))
357+
Ok(self.comp().add(ir::Prop::TimeCmp(ir::CmpOp {
358+
lhs: final_lhs,
359+
op,
360+
rhs: final_rhs,
361+
})))
324362
}
325363

326364
fn implication(

‎tests/check/comprehensive-operators.expect‎

Whitespace-only changes.

‎tests/check/comprehensive-operators.fil‎

Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,57 @@
1+
// Comprehensive test demonstrating all operators work correctly
2+
// This test verifies constraint satisfaction for all 6 comparison operators
3+
4+
// Test direct constraints with new operators
5+
comp DirectConstraints[A, B, C]<'G: 1>() -> () where
6+
A < 20, // Less than
7+
B <= A, // Less than or equal
8+
C != 0 // Not equal
9+
{
10+
}
11+
12+
// Test conditional constraints with all operators
13+
comp AllConditionals[W1, L1, W2, L2, W3, L3, W4, L4, W5, L5, W6, L6]<'G: 1>() -> () where
14+
W1 > 10 ? L1 == 1 : L1 == 0, // Greater than
15+
W2 >= 10 ? L2 == 1 : L2 == 0, // Greater than or equal
16+
W3 < 10 ? L3 == 1 : L3 == 0, // Less than
17+
W4 <= 10 ? L4 == 1 : L4 == 0, // Less than or equal
18+
W5 == 10 ? L5 == 1 : L5 == 0, // Equal
19+
W6 != 10 ? L6 == 1 : L6 == 0 // Not equal
20+
{
21+
}
22+
23+
// Test transitivity and consistency
24+
comp TransitiveConstraints[X, Y, Z]<'G: 1>() -> () where
25+
X < Y,
26+
Y < Z,
27+
X < Z // This should be satisfied by transitivity
28+
{
29+
}
30+
31+
comp main<'G: 1>() -> () {
32+
// Test direct constraints
33+
D1 := new DirectConstraints[15, 10, 5]; // 15 < 20, 10 <= 15, 5 != 0
34+
D2 := new DirectConstraints[10, 10, 1]; // 10 < 20, 10 <= 10, 1 != 0
35+
36+
// Test all conditional operators
37+
// W1=15 > 10 is true, so L1=1
38+
// W2=10 >= 10 is true, so L2=1
39+
// W3=5 < 10 is true, so L3=1
40+
// W4=10 <= 10 is true, so L4=1
41+
// W5=10 == 10 is true, so L5=1
42+
// W6=5 != 10 is true, so L6=1
43+
C1 := new AllConditionals[15, 1, 10, 1, 5, 1, 10, 1, 10, 1, 5, 1];
44+
45+
// Test opposite conditions
46+
// W1=5 > 10 is false, so L1=0
47+
// W2=5 >= 10 is false, so L2=0
48+
// W3=15 < 10 is false, so L3=0
49+
// W4=15 <= 10 is false, so L4=0
50+
// W5=5 == 10 is false, so L5=0
51+
// W6=10 != 10 is false, so L6=0
52+
C2 := new AllConditionals[5, 0, 5, 0, 15, 0, 15, 0, 5, 0, 10, 0];
53+
54+
// Test transitivity
55+
T1 := new TransitiveConstraints[5, 10, 15]; // 5 < 10 < 15
56+
T2 := new TransitiveConstraints[1, 100, 200]; // 1 < 100 < 200
57+
}

‎tests/check/lt-conditional-simple.expect‎

Whitespace-only changes.

‎tests/check/lt-conditional-simple.fil‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
// Simple conditional test for less-than operator
2+
comp LtCond[W, L]<'G: 1>() -> () where W < 5 ? L == 1 : L == 2 {
3+
}
4+
5+
comp main<'G: 1>() -> () {
6+
// W=3 < 5 is true, so L must be 1
7+
T1 := new LtCond[3, 1];
8+
9+
// W=7 < 5 is false, so L must be 2
10+
T2 := new LtCond[7, 2];
11+
}

0 commit comments

Comments
 (0)