Merge pull request #49 from NethermindEth/ElijahVlasov/fixed-type-err…

…or-messages

Type error messages

pyproject.toml

@@ -18,7 +18,7 @@ skip_gitignore = true
 
 [tool.poetry]
 name = "horus-compile"
-version = "0.0.6.6"
+version = "0.0.6.7"
 authors = ["Nethermind <[email protected]>"]
 description = "Use formally verified annotations in your Cairo code"
 classifiers = [

src/horus/__init__.py

@@ -1 +1 @@
-__version__ = "0.0.6.6"
+__version__ = "0.0.6.7"

src/horus/compiler/code_elements.py

@@ -64,6 +64,7 @@ class BoolExprCompare(BoolFormula):
     a: Expression
     b: Expression
     comp: str
+    location: Optional[Location] = LocationField
 
     def get_children(self) -> Sequence[Optional["AstNode"]]:
         return [self.a, self.b]

src/horus/compiler/parser_transformer.py

@@ -131,21 +131,21 @@ def bool_expr_false(self):
     def bool_atom(self, expr):
         return BoolExprAtom(expr)
 
-    @lark.v_args(inline=True)
-    def bool_expr_le(self, lhs, rhs):
-        return BoolExprCompare(lhs, rhs, "<=")
+    @lark.v_args(inline=True, meta=True)
+    def bool_expr_le(self, meta, lhs, rhs):
+        return BoolExprCompare(lhs, rhs, "<=", location=self.meta2loc(meta))
 
-    @lark.v_args(inline=True)
-    def bool_expr_lt(self, lhs, rhs):
-        return BoolExprCompare(lhs, rhs, "<")
+    @lark.v_args(inline=True, meta=True)
+    def bool_expr_lt(self, meta, lhs, rhs):
+        return BoolExprCompare(lhs, rhs, "<", location=self.meta2loc(meta))
 
-    @lark.v_args(inline=True)
-    def bool_expr_ge(self, lhs, rhs):
-        return BoolExprCompare(lhs, rhs, ">=")
+    @lark.v_args(inline=True, meta=True)
+    def bool_expr_ge(self, meta, lhs, rhs):
+        return BoolExprCompare(lhs, rhs, ">=", location=self.meta2loc(meta))
 
-    @lark.v_args(inline=True)
-    def bool_expr_gt(self, lhs, rhs):
-        return BoolExprCompare(lhs, rhs, ">")
+    @lark.v_args(inline=True, meta=True)
+    def bool_expr_gt(self, meta, lhs, rhs):
+        return BoolExprCompare(lhs, rhs, ">", location=self.meta2loc(meta))
 
     @lark.v_args(inline=True)
     def bool_expr_parentheses(self, formula):

src/horus/compiler/z3_transformer.py

@@ -51,6 +51,7 @@
 )
 from starkware.cairo.lang.compiler.resolve_search_result import resolve_search_result
 from starkware.cairo.lang.compiler.scoped_name import ScopedName
+from starkware.cairo.lang.compiler.type_casts import CairoTypeError
 from starkware.cairo.lang.compiler.type_system_visitor import *
 from starkware.cairo.lang.compiler.type_system_visitor import simplify_type_system
 
@@ -411,7 +412,12 @@ def visit_BoolEqExpr(self, bool_expr: BoolEqExpr):
             self.storage_vars,
             self.is_post,
         )
-        assert a_type == b_type, "Types of lhs and rhs must coincide"
+
+        if a_type != b_type:
+            raise CairoTypeError(
+                f"Types of lhs and rhs must coincide. Got {a_type.format()} and {b_type.format()}",
+                bool_expr.location,
+            )
 
         if isinstance(a_type, TypeStruct):
             result = self.make_struct_eq(bool_expr.a, bool_expr.b, a_type)
@@ -443,7 +449,11 @@ def visit_BoolExprCompare(self, formula: BoolExprCompare):
             self.is_post,
         )
 
-        assert a_type == b_type, "Types of lhs and rhs must coincide"
+        if a_type != b_type:
+            raise CairoTypeError(
+                f"Types of lhs and rhs must coincide. Got {a_type.format()} and {b_type.format()}",
+                formula.location,
+            )
 
         if isinstance(a_type, (TypeFelt, TypePointer)):
             a = self.z3_expression_transformer.visit(a)
@@ -457,6 +467,11 @@ def visit_BoolExprCompare(self, formula: BoolExprCompare):
                 return a >= b
             elif formula.comp == ">":
                 return a > b
+        else:
+            raise CairoTypeError(
+                f"Cannot compare values of type {a_type.format()}",
+                location=formula.location,
+            )
 
     def visit_BoolConst(self, formula: BoolConst):
         return z3.BoolVal(formula.const)