mirror of
https://github.com/ProvableHQ/leo.git
synced 2024-11-28 01:01:53 +03:00
impl membership type assertion error handling
This commit is contained in:
parent
dbade1f4fe
commit
f2a808cbe7
@ -17,6 +17,7 @@
|
|||||||
use crate::{
|
use crate::{
|
||||||
assert_satisfied,
|
assert_satisfied,
|
||||||
expect_compiler_error,
|
expect_compiler_error,
|
||||||
|
expect_dynamic_check_error,
|
||||||
get_output,
|
get_output,
|
||||||
parse_program,
|
parse_program,
|
||||||
parse_program_with_input,
|
parse_program_with_input,
|
||||||
@ -38,15 +39,6 @@ pub fn output_false(program: EdwardsTestCompiler) {
|
|||||||
assert_eq!(expected, actual.bytes().as_slice());
|
assert_eq!(expected, actual.bytes().as_slice());
|
||||||
}
|
}
|
||||||
|
|
||||||
fn fail_boolean_statement(program: EdwardsTestCompiler) {
|
|
||||||
match expect_compiler_error(program) {
|
|
||||||
CompilerError::FunctionError(FunctionError::StatementError(StatementError::ExpressionError(
|
|
||||||
ExpressionError::BooleanError(BooleanError::Error(_)),
|
|
||||||
))) => {}
|
|
||||||
_ => panic!("Expected boolean error, got {}"),
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
#[test]
|
#[test]
|
||||||
fn test_input_pass() {
|
fn test_input_pass() {
|
||||||
let program_bytes = include_bytes!("assert_eq_input.leo");
|
let program_bytes = include_bytes!("assert_eq_input.leo");
|
||||||
@ -139,9 +131,9 @@ fn test_false_or_false() {
|
|||||||
#[test]
|
#[test]
|
||||||
fn test_true_or_u32() {
|
fn test_true_or_u32() {
|
||||||
let bytes = include_bytes!("true_or_u32.leo");
|
let bytes = include_bytes!("true_or_u32.leo");
|
||||||
let program = parse_program(bytes).unwrap();
|
let error = parse_program(bytes).err().unwrap();
|
||||||
|
|
||||||
fail_boolean_statement(program);
|
expect_dynamic_check_error(error);
|
||||||
}
|
}
|
||||||
|
|
||||||
// Boolean and &&
|
// Boolean and &&
|
||||||
@ -173,9 +165,9 @@ fn test_false_and_false() {
|
|||||||
#[test]
|
#[test]
|
||||||
fn test_true_and_u32() {
|
fn test_true_and_u32() {
|
||||||
let bytes = include_bytes!("true_and_u32.leo");
|
let bytes = include_bytes!("true_and_u32.leo");
|
||||||
let program = parse_program(bytes).unwrap();
|
let error = parse_program(bytes).err().unwrap();
|
||||||
|
|
||||||
fail_boolean_statement(program);
|
expect_dynamic_check_error(error);
|
||||||
}
|
}
|
||||||
|
|
||||||
// All
|
// All
|
||||||
|
@ -178,6 +178,15 @@ pub(crate) fn expect_compiler_error(program: EdwardsTestCompiler) -> CompilerErr
|
|||||||
program.generate_constraints_helper(&mut cs).unwrap_err()
|
program.generate_constraints_helper(&mut cs).unwrap_err()
|
||||||
}
|
}
|
||||||
|
|
||||||
|
pub(crate) fn expect_dynamic_check_error(error: CompilerError) {
|
||||||
|
let is_dynamic_check = match error {
|
||||||
|
CompilerError::DynamicCheckError(_) => true,
|
||||||
|
_ => false,
|
||||||
|
};
|
||||||
|
|
||||||
|
assert!(is_dynamic_check)
|
||||||
|
}
|
||||||
|
|
||||||
// pub(crate) fn expect_synthesis_error(program: EdwardsTestCompiler) {
|
// pub(crate) fn expect_synthesis_error(program: EdwardsTestCompiler) {
|
||||||
// let mut cs = TestConstraintSystem::<Fq>::new();
|
// let mut cs = TestConstraintSystem::<Fq>::new();
|
||||||
// let _output = program.generate_constraints_helper(&mut cs).unwrap();
|
// let _output = program.generate_constraints_helper(&mut cs).unwrap();
|
||||||
|
@ -341,8 +341,8 @@ impl Frame {
|
|||||||
///
|
///
|
||||||
/// Creates a new membership type assertion between a given and set of types.
|
/// Creates a new membership type assertion between a given and set of types.
|
||||||
///
|
///
|
||||||
fn assert_membership(&mut self, given: Type, set: Vec<Type>) {
|
fn assert_membership(&mut self, given: Type, set: Vec<Type>, span: &Span) {
|
||||||
let type_assertion = TypeAssertion::new_membership(given, set);
|
let type_assertion = TypeAssertion::new_membership(given, set, span);
|
||||||
|
|
||||||
self.type_assertions.push(type_assertion);
|
self.type_assertions.push(type_assertion);
|
||||||
}
|
}
|
||||||
@ -350,28 +350,28 @@ impl Frame {
|
|||||||
///
|
///
|
||||||
/// Creates a new membership type assertion between a given and the set of negative integer types.
|
/// Creates a new membership type assertion between a given and the set of negative integer types.
|
||||||
///
|
///
|
||||||
fn assert_negative_integer(&mut self, given: &Type) {
|
fn assert_negative_integer(&mut self, given: &Type, span: &Span) {
|
||||||
let negative_integer_types = Type::negative_integer_types();
|
let negative_integer_types = Type::negative_integer_types();
|
||||||
|
|
||||||
self.assert_membership(given.clone(), negative_integer_types)
|
self.assert_membership(given.clone(), negative_integer_types, span)
|
||||||
}
|
}
|
||||||
|
|
||||||
///
|
///
|
||||||
/// Creates a new membership type assertion between a given and the set of all integer types.
|
/// Creates a new membership type assertion between a given and the set of all integer types.
|
||||||
///
|
///
|
||||||
fn assert_integer(&mut self, given: &Type) {
|
fn assert_integer(&mut self, given: &Type, span: &Span) {
|
||||||
let integer_types = Type::integer_types();
|
let integer_types = Type::integer_types();
|
||||||
|
|
||||||
self.assert_membership(given.clone(), integer_types)
|
self.assert_membership(given.clone(), integer_types, span)
|
||||||
}
|
}
|
||||||
|
|
||||||
///
|
///
|
||||||
/// Creates a new membership type assertion between a given and the set of index types.
|
/// Creates a new membership type assertion between a given and the set of index types.
|
||||||
///
|
///
|
||||||
fn assert_index(&mut self, given: &Type) {
|
fn assert_index(&mut self, given: &Type, span: &Span) {
|
||||||
let index_types = Type::index_types();
|
let index_types = Type::index_types();
|
||||||
|
|
||||||
self.assert_membership(given.clone(), index_types)
|
self.assert_membership(given.clone(), index_types, span)
|
||||||
}
|
}
|
||||||
|
|
||||||
///
|
///
|
||||||
@ -751,12 +751,12 @@ impl Frame {
|
|||||||
&mut self,
|
&mut self,
|
||||||
left: &Expression,
|
left: &Expression,
|
||||||
right: &Expression,
|
right: &Expression,
|
||||||
_span: &Span,
|
span: &Span,
|
||||||
) -> Result<Type, FrameError> {
|
) -> Result<Type, FrameError> {
|
||||||
let type_ = self.parse_binary_expression(left, right, _span)?;
|
let type_ = self.parse_binary_expression(left, right, span)?;
|
||||||
|
|
||||||
// Assert that the type is an integer.
|
// Assert that the type is an integer.
|
||||||
self.assert_integer(&type_);
|
self.assert_integer(&type_, span);
|
||||||
|
|
||||||
Ok(type_)
|
Ok(type_)
|
||||||
}
|
}
|
||||||
@ -780,12 +780,12 @@ impl Frame {
|
|||||||
///
|
///
|
||||||
/// Returns the `Type` of the expression being negated. Must be a negative integer type.
|
/// Returns the `Type` of the expression being negated. Must be a negative integer type.
|
||||||
///
|
///
|
||||||
fn parse_negate_expression(&mut self, expression: &Expression, _span: &Span) -> Result<Type, FrameError> {
|
fn parse_negate_expression(&mut self, expression: &Expression, span: &Span) -> Result<Type, FrameError> {
|
||||||
// Parse the expression type.
|
// Parse the expression type.
|
||||||
let type_ = self.parse_expression(expression)?;
|
let type_ = self.parse_expression(expression)?;
|
||||||
|
|
||||||
// Assert that this integer can be negated.
|
// Assert that this integer can be negated.
|
||||||
self.assert_negative_integer(&type_);
|
self.assert_negative_integer(&type_, span);
|
||||||
|
|
||||||
Ok(type_)
|
Ok(type_)
|
||||||
}
|
}
|
||||||
@ -958,12 +958,7 @@ impl Frame {
|
|||||||
///
|
///
|
||||||
/// Returns the type of the accessed array element.
|
/// Returns the type of the accessed array element.
|
||||||
///
|
///
|
||||||
fn parse_array_access(
|
fn parse_array_access(&mut self, type_: Type, r_or_e: &RangeOrExpression, span: &Span) -> Result<Type, FrameError> {
|
||||||
&mut self,
|
|
||||||
type_: Type,
|
|
||||||
r_or_e: &RangeOrExpression,
|
|
||||||
_span: &Span,
|
|
||||||
) -> Result<Type, FrameError> {
|
|
||||||
// Check the type is an array.
|
// Check the type is an array.
|
||||||
let (element_type, _dimensions) = match type_ {
|
let (element_type, _dimensions) = match type_ {
|
||||||
Type::Array(type_, dimensions) => (type_, dimensions),
|
Type::Array(type_, dimensions) => (type_, dimensions),
|
||||||
@ -980,14 +975,14 @@ impl Frame {
|
|||||||
// Parse the expression type.
|
// Parse the expression type.
|
||||||
let type_ = self.parse_expression(expression)?;
|
let type_ = self.parse_expression(expression)?;
|
||||||
|
|
||||||
self.assert_index(&type_);
|
self.assert_index(&type_, span);
|
||||||
}
|
}
|
||||||
|
|
||||||
if let Some(expression) = to {
|
if let Some(expression) = to {
|
||||||
// Parse the expression type.
|
// Parse the expression type.
|
||||||
let type_ = self.parse_expression(expression)?;
|
let type_ = self.parse_expression(expression)?;
|
||||||
|
|
||||||
self.assert_index(&type_);
|
self.assert_index(&type_, span);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
RangeOrExpression::Expression(expression) => {
|
RangeOrExpression::Expression(expression) => {
|
||||||
@ -995,7 +990,7 @@ impl Frame {
|
|||||||
let type_ = self.parse_expression(expression)?;
|
let type_ = self.parse_expression(expression)?;
|
||||||
|
|
||||||
// Assert the type is an index.
|
// Assert the type is an index.
|
||||||
self.assert_index(&type_);
|
self.assert_index(&type_, span);
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
@ -1423,8 +1418,8 @@ impl TypeAssertion {
|
|||||||
///
|
///
|
||||||
/// Returns a `TypeAssertion::Membership` predicate from given and set `Type`s.
|
/// Returns a `TypeAssertion::Membership` predicate from given and set `Type`s.
|
||||||
///
|
///
|
||||||
pub fn new_membership(given: Type, set: Vec<Type>) -> Self {
|
pub fn new_membership(given: Type, set: Vec<Type>, span: &Span) -> Self {
|
||||||
Self::Membership(TypeMembership::new(given, set))
|
Self::Membership(TypeMembership::new(given, set, span))
|
||||||
}
|
}
|
||||||
|
|
||||||
///
|
///
|
||||||
@ -1445,7 +1440,11 @@ impl TypeAssertion {
|
|||||||
pub fn solve(&self) -> Result<Option<TypeVariablePair>, TypeAssertionError> {
|
pub fn solve(&self) -> Result<Option<TypeVariablePair>, TypeAssertionError> {
|
||||||
match self {
|
match self {
|
||||||
TypeAssertion::Equality(equality) => equality.solve(),
|
TypeAssertion::Equality(equality) => equality.solve(),
|
||||||
TypeAssertion::Membership(_) => unimplemented!(),
|
TypeAssertion::Membership(membership) => {
|
||||||
|
membership.solve()?;
|
||||||
|
|
||||||
|
Ok(None)
|
||||||
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
@ -1455,14 +1454,19 @@ impl TypeAssertion {
|
|||||||
pub struct TypeMembership {
|
pub struct TypeMembership {
|
||||||
given: Type,
|
given: Type,
|
||||||
set: Vec<Type>,
|
set: Vec<Type>,
|
||||||
|
span: Span,
|
||||||
}
|
}
|
||||||
|
|
||||||
impl TypeMembership {
|
impl TypeMembership {
|
||||||
///
|
///
|
||||||
/// Returns a `TypeMembership` predicate from given and set `Type`s.
|
/// Returns a `TypeMembership` predicate from given and set `Type`s.
|
||||||
///
|
///
|
||||||
pub fn new(given: Type, set: Vec<Type>) -> Self {
|
pub fn new(given: Type, set: Vec<Type>, span: &Span) -> Self {
|
||||||
Self { given, set }
|
Self {
|
||||||
|
given,
|
||||||
|
set,
|
||||||
|
span: span.to_owned(),
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
///
|
///
|
||||||
@ -1476,8 +1480,16 @@ impl TypeMembership {
|
|||||||
///
|
///
|
||||||
/// Returns true if the given type is equal to a member of the set.
|
/// Returns true if the given type is equal to a member of the set.
|
||||||
///
|
///
|
||||||
pub fn evaluate(&self) -> bool {
|
pub fn solve(&self) -> Result<(), TypeAssertionError> {
|
||||||
self.set.contains(&self.given)
|
if self.set.contains(&self.given) {
|
||||||
|
Ok(())
|
||||||
|
} else {
|
||||||
|
Err(TypeAssertionError::membership_failed(
|
||||||
|
&self.given,
|
||||||
|
&self.set,
|
||||||
|
&self.span,
|
||||||
|
))
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
|
||||||
///
|
///
|
||||||
@ -1534,7 +1546,7 @@ impl TypeEquality {
|
|||||||
// Return None if the two types are equal (the equality is satisfied).
|
// Return None if the two types are equal (the equality is satisfied).
|
||||||
None
|
None
|
||||||
} else {
|
} else {
|
||||||
return Err(TypeAssertionError::assertion_failed(type1, type2, &self.span));
|
return Err(TypeAssertionError::equality_failed(type1, type2, &self.span));
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
})
|
})
|
||||||
|
@ -46,8 +46,20 @@ impl TypeAssertionError {
|
|||||||
///
|
///
|
||||||
/// Found mismatched types during program parsing.
|
/// Found mismatched types during program parsing.
|
||||||
///
|
///
|
||||||
pub fn assertion_failed(left: &Type, right: &Type, span: &Span) -> Self {
|
pub fn equality_failed(left: &Type, right: &Type, span: &Span) -> Self {
|
||||||
let message = format!("Mismatched types expected type `{}`, found type `{}`", left, right);
|
let message = format!("Mismatched types. Expected type `{}`, found type `{}`.", left, right);
|
||||||
|
|
||||||
|
Self::new_from_span(message, span.to_owned())
|
||||||
|
}
|
||||||
|
|
||||||
|
///
|
||||||
|
/// Given type is not a member of the set of expected types.
|
||||||
|
///
|
||||||
|
pub fn membership_failed(given: &Type, set: &Vec<Type>, span: &Span) -> Self {
|
||||||
|
let message = format!(
|
||||||
|
"Mismatched types. Given type `{}` is not in the expected type set `{:?}`.",
|
||||||
|
given, set
|
||||||
|
);
|
||||||
|
|
||||||
Self::new_from_span(message, span.to_owned())
|
Self::new_from_span(message, span.to_owned())
|
||||||
}
|
}
|
||||||
|
Loading…
Reference in New Issue
Block a user