@@ -14,15 +14,16 @@ impl Visitor for DesugarConditionals {
1414 fn signature ( & mut self , sig : & mut ast:: Signature ) -> Action {
1515 // Process conditional constraints and convert them to facts
1616 let mut new_facts = Vec :: new ( ) ;
17-
17+
1818 for conditional_constraint in & sig. conditional_constraints {
19- let facts = self . desugar_conditional_constraint ( conditional_constraint) ;
19+ let facts =
20+ self . desugar_conditional_constraint ( conditional_constraint) ;
2021 new_facts. extend ( facts) ;
2122 }
22-
23+
2324 // Clear the conditional constraints since we've processed them
2425 sig. conditional_constraints . clear ( ) ;
25-
26+
2627 if !new_facts. is_empty ( ) {
2728 Action :: AddBefore ( new_facts)
2829 } else {
@@ -32,25 +33,38 @@ impl Visitor for DesugarConditionals {
3233}
3334
3435impl DesugarConditionals {
35- fn desugar_conditional_constraint ( & self , constraint : & Loc < ast:: FCons > ) -> Vec < ast:: Command > {
36+ fn desugar_conditional_constraint (
37+ & self ,
38+ constraint : & Loc < ast:: FCons > ,
39+ ) -> Vec < ast:: Command > {
3640 use ast:: FCons ;
37-
41+
3842 match & * * constraint {
39- FCons :: ConditionalC { condition, then_constraint, else_constraint } => {
43+ FCons :: ConditionalC {
44+ condition,
45+ then_constraint,
46+ else_constraint,
47+ } => {
4048 let mut facts = Vec :: new ( ) ;
41-
49+
4250 // Create: assume condition => then_constraint
43- if let Some ( then_fact) = self . create_assume_fact ( condition. clone ( ) , then_constraint) {
51+ if let Some ( then_fact) =
52+ self . create_assume_fact ( condition. clone ( ) , then_constraint)
53+ {
4454 facts. push ( ast:: Command :: Fact ( then_fact) ) ;
4555 }
46-
47- // Create: assume !condition => else_constraint
48- if let Some ( negated_condition) = self . negate_condition ( condition) {
49- if let Some ( else_fact) = self . create_assume_fact ( negated_condition, else_constraint) {
56+
57+ // Create: assume !condition => else_constraint
58+ if let Some ( negated_condition) =
59+ self . negate_condition ( condition)
60+ {
61+ if let Some ( else_fact) = self
62+ . create_assume_fact ( negated_condition, else_constraint)
63+ {
5064 facts. push ( ast:: Command :: Fact ( else_fact) ) ;
5165 }
5266 }
53-
67+
5468 facts
5569 }
5670 _ => {
@@ -59,25 +73,28 @@ impl DesugarConditionals {
5973 }
6074 }
6175 }
62-
76+
6377 fn create_assume_fact (
64- & self ,
65- condition : ast:: OrderConstraint < ast:: Expr > ,
66- constraint : & Box < ast:: FCons >
78+ & self ,
79+ condition : ast:: OrderConstraint < ast:: Expr > ,
80+ constraint : & ast:: FCons ,
6781 ) -> Option < ast:: Fact > {
68- // Convert FCons to OrderConstraint
82+ // Convert FCons to OrderConstraint
6983 let constraint_oc = self . fcons_to_order_constraint ( constraint) ?;
70-
84+
7185 // Create implication: condition => constraint
7286 let implication = ast:: Implication :: implies ( condition, constraint_oc) ;
73-
87+
7488 // Create assume fact
7589 Some ( ast:: Fact :: assume ( Loc :: unknown ( implication) ) )
7690 }
77-
78- fn fcons_to_order_constraint ( & self , fcons : & ast:: FCons ) -> Option < ast:: OrderConstraint < ast:: Expr > > {
91+
92+ fn fcons_to_order_constraint (
93+ & self ,
94+ fcons : & ast:: FCons ,
95+ ) -> Option < ast:: OrderConstraint < ast:: Expr > > {
7996 use ast:: FCons ;
80-
97+
8198 match fcons {
8299 FCons :: ExprC ( oc) => Some ( oc. clone ( ) ) ,
83100 FCons :: TimeC ( _) => {
@@ -92,19 +109,28 @@ impl DesugarConditionals {
92109 }
93110 }
94111 }
95-
96- fn negate_condition ( & self , condition : & ast:: OrderConstraint < ast:: Expr > ) -> Option < ast:: OrderConstraint < ast:: Expr > > {
112+
113+ fn negate_condition (
114+ & self ,
115+ condition : & ast:: OrderConstraint < ast:: Expr > ,
116+ ) -> Option < ast:: OrderConstraint < ast:: Expr > > {
97117 use ast:: OrderOp ;
98-
118+
99119 // For now, only handle simple negations
100120 match condition. op {
101121 OrderOp :: Gt => {
102122 // !(a > b) becomes (a <= b), which is (b >= a)
103- Some ( ast:: OrderConstraint :: gte ( condition. right . clone ( ) , condition. left . clone ( ) ) )
123+ Some ( ast:: OrderConstraint :: gte (
124+ condition. right . clone ( ) ,
125+ condition. left . clone ( ) ,
126+ ) )
104127 }
105128 OrderOp :: Gte => {
106- // !(a >= b) becomes (a < b), which is (b > a)
107- Some ( ast:: OrderConstraint :: gt ( condition. right . clone ( ) , condition. left . clone ( ) ) )
129+ // !(a >= b) becomes (a < b), which is (b > a)
130+ Some ( ast:: OrderConstraint :: gt (
131+ condition. right . clone ( ) ,
132+ condition. left . clone ( ) ,
133+ ) )
108134 }
109135 OrderOp :: Eq => {
110136 // !(a == b) is more complex - we can't easily represent != in the constraint system
@@ -113,4 +139,4 @@ impl DesugarConditionals {
113139 }
114140 }
115141 }
116- }
142+ }
0 commit comments