moar

Author: rachitnigam

crates/filament/src/ast_passes/desugar_conditionals.rs

@@ -1,7 +1,7 @@
 use crate::ast_visitor::{Action, Visitor};
 use fil_ast as ast;
 use fil_ast::Loc;
-use fil_utils::{Error, FilamentResult};
+use fil_utils::{Error, FilamentResult, GPosIdx};
 
 /// Desugars conditional constraints into assume statements
 #[derive(Default)]
@@ -48,6 +48,8 @@ impl DesugarConditionals {
     ) -> FilamentResult<Vec<ast::Command>> {
         use ast::FCons;
 
+        let original_loc = constraint.pos(); // Capture original location
+
         match &**constraint {
             FCons::ConditionalC {
                 condition,
@@ -57,12 +59,12 @@ impl DesugarConditionals {
                 let mut facts = Vec::new();
 
                 // Create: assume condition => then_constraint
-                let then_fact = self.create_assume_fact(condition.clone(), then_constraint)?;
+                let then_fact = self.create_assume_fact(condition.clone(), then_constraint, original_loc)?;
                 facts.push(ast::Command::Fact(then_fact));
 
                 // Create: assume !condition => else_constraint
                 let negated_condition = self.negate_condition(condition)?;
-                let else_fact = self.create_assume_fact(negated_condition, else_constraint)?;
+                let else_fact = self.create_assume_fact(negated_condition, else_constraint, original_loc)?;
                 facts.push(ast::Command::Fact(else_fact));
 
                 Ok(facts)
@@ -79,15 +81,16 @@ impl DesugarConditionals {
         &self,
         condition: ast::OrderConstraint<ast::Expr>,
         constraint: &ast::FCons,
+        original_loc: GPosIdx,
     ) -> FilamentResult<ast::Fact> {
         // Convert FCons to OrderConstraint
         let constraint_oc = self.fcons_to_order_constraint(constraint)?;
 
         // Create implication: condition => constraint
         let implication = ast::Implication::implies(condition, constraint_oc);
 
-        // Create assume fact
-        Ok(ast::Fact::assume(Loc::unknown(implication)))
+        // Create assume fact with original location
+        Ok(ast::Fact::assume(Loc::new(implication, original_loc)))
     }
 
     fn fcons_to_order_constraint(

tests/errors/conditional/complex-equality-error.expect

@@ -2,7 +2,12 @@
 1
 ---STDERR---
 error: cannot prove source-level fact
- = Elaborated during monomorphization.
+  ┌─ tests/errors/conditional/complex-equality-error.fil:2:54
+  │
+2 │ comp ComplexEqualityError[A, B]<'G: 1>() -> () where A + B == B * 2 ? A == 1 : A == 0 {
+  │                                                      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ cannot prove source-level fact
+  │
+  = Elaborated during monomorphization.
 
 Compilation failed with 1 errors.
 Run with --show-models to generate assignments for failing constraints.

tests/errors/constraints/conditional-lt-violation.expect

@@ -2,7 +2,12 @@
 1
 ---STDERR---
 error: cannot prove source-level fact
- = Elaborated during monomorphization.
+  ┌─ tests/errors/constraints/conditional-lt-violation.fil:2:56
+  │
+2 │ comp ConditionalLtViolation[W, L]<'G: 1>() -> () where W < 10 ? L == 1 : L == 2 {
+  │                                                        ^^^^^^^^^^^^^^^^^^^^^^^^^ cannot prove source-level fact
+  │
+  = Elaborated during monomorphization.
 
 Compilation failed with 1 errors.
 Run with --show-models to generate assignments for failing constraints.