Skip to content

Commit

Permalink
Fixed some type error messages
Browse files Browse the repository at this point in the history
  • Loading branch information
ElijahVlasov committed Jan 23, 2023
1 parent 30a8c35 commit e65224d
Show file tree
Hide file tree
Showing 5 changed files with 32 additions and 16 deletions.
2 changes: 1 addition & 1 deletion pyproject.toml
Original file line number Diff line number Diff line change
Expand Up @@ -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 = [
Expand Down
2 changes: 1 addition & 1 deletion src/horus/__init__.py
Original file line number Diff line number Diff line change
@@ -1 +1 @@
__version__ = "0.0.6.6"
__version__ = "0.0.6.7"
1 change: 1 addition & 0 deletions src/horus/compiler/code_elements.py
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand Down
24 changes: 12 additions & 12 deletions src/horus/compiler/parser_transformer.py
Original file line number Diff line number Diff line change
Expand Up @@ -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):
Expand Down
19 changes: 17 additions & 2 deletions src/horus/compiler/z3_transformer.py
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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)
Expand All @@ -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)
Expand Down

0 comments on commit e65224d

Please sign in to comment.