From 0ccea6c75cad366466a508e7ad6e95b01ea5cb7e Mon Sep 17 00:00:00 2001 From: Andrea Lattuada Date: Mon, 14 Oct 2024 18:54:49 +0200 Subject: [PATCH 01/13] start on field update support in AIR --- source/air/src/ast.rs | 3 ++- source/air/src/closure.rs | 5 +++-- source/air/src/parser.rs | 16 ++++++++++++++++ source/air/src/printer.rs | 3 +++ source/air/src/smt_verify.rs | 2 +- source/air/src/tests.rs | 14 ++++++++++++++ source/air/src/typecheck.rs | 8 ++++++++ source/air/src/visitor.rs | 4 ++-- 8 files changed, 49 insertions(+), 6 deletions(-) diff --git a/source/air/src/ast.rs b/source/air/src/ast.rs index 11a84a1d36..90d6abf299 100644 --- a/source/air/src/ast.rs +++ b/source/air/src/ast.rs @@ -56,7 +56,7 @@ pub enum Relation { PiecewiseLinearOrder, } -#[derive(Copy, Clone, Debug, PartialEq, Eq, Hash)] +#[derive(Clone, Debug, PartialEq, Eq, Hash)] pub enum BinaryOp { Implies, Eq, @@ -92,6 +92,7 @@ pub enum BinaryOp { LShr, Shl, BitConcat, + FieldUpdate(Ident), } #[derive(Copy, Clone, Debug, PartialEq, Eq, Hash)] diff --git a/source/air/src/closure.rs b/source/air/src/closure.rs index e8112d76cd..7ced319ef8 100644 --- a/source/air/src/closure.rs +++ b/source/air/src/closure.rs @@ -584,9 +584,10 @@ fn simplify_expr(ctxt: &mut Context, state: &mut State, expr: &Expr) -> (Typ, Ex (TypX::BitVec(n1), TypX::BitVec(n2)) => Arc::new(TypX::BitVec(n1 + n2)), _ => panic!("internal error during processing concat"), }, + BinaryOp::FieldUpdate(_) => ts[0].0.clone(), }; - let (es, t) = enclose(state, App::Binary(*op), es, ts); - (typ, Arc::new(ExprX::Binary(*op, es[0].clone(), es[1].clone())), t) + let (es, t) = enclose(state, App::Binary(op.clone()), es, ts); + (typ, Arc::new(ExprX::Binary(op.clone(), es[0].clone(), es[1].clone())), t) } ExprX::Multi(op, es) => { let typ = match op { diff --git a/source/air/src/parser.rs b/source/air/src/parser.rs index 23eb7f65df..fea38db52c 100644 --- a/source/air/src/parser.rs +++ b/source/air/src/parser.rs @@ -66,6 +66,15 @@ fn relation_binary_op(n1: &Node, n2: &Node) -> Option { } } +fn field_update_binary_op(n1: &Node, n2: &Node) -> Option { + match (n1, n2) { + (Node::Atom(s1), Node::Atom(s2)) if s1.as_str() == "update-field" => { + Some(BinaryOp::FieldUpdate(Arc::new(s2.clone()))) + } + _ => None, + } +} + fn map_nodes_to_vec(nodes: &[Node], f: &F) -> Result>, String> where F: Fn(&Node) -> Result, @@ -301,6 +310,13 @@ impl Parser { { relation_binary_op(&nodes[1], &nodes[2]) } + Node::List(nodes) + if nodes.len() == 3 + && nodes[0] == Node::Atom("_".to_string()) + && field_update_binary_op(&nodes[1], &nodes[2]).is_some() => + { + field_update_binary_op(&nodes[1], &nodes[2]) + } _ => None, }; let lop = match &nodes[0] { diff --git a/source/air/src/printer.rs b/source/air/src/printer.rs index ee80a961f3..0902501d9e 100644 --- a/source/air/src/printer.rs +++ b/source/air/src/printer.rs @@ -223,6 +223,9 @@ impl Printer { BinaryOp::AShr => "bvashr", BinaryOp::Shl => "bvshl", BinaryOp::BitConcat => "concat", + BinaryOp::FieldUpdate(field_ident) => { + todo!("TODO: emit (_ update-field )") + } }; Node::List(vec![str_to_node(sop), self.expr_to_node(lhs), self.expr_to_node(rhs)]) } diff --git a/source/air/src/smt_verify.rs b/source/air/src/smt_verify.rs index 84bd60c63c..f21dd62682 100644 --- a/source/air/src/smt_verify.rs +++ b/source/air/src/smt_verify.rs @@ -22,7 +22,7 @@ fn label_asserts<'ctx>( // asserts are on rhs of => // (slight hack to also allow rhs of == for quantified function definitions) Arc::new(ExprX::Binary( - *op, + op.clone(), lhs.clone(), label_asserts(context, infos, axiom_infos, rhs), )) diff --git a/source/air/src/tests.rs b/source/air/src/tests.rs index 3b7c378ea7..dac5905883 100644 --- a/source/air/src/tests.rs +++ b/source/air/src/tests.rs @@ -2102,3 +2102,17 @@ fn no_partial_order() { ) ) } + +#[test] +fn datatype_field_update() { + yes!( + (declare-datatypes ((A 0)) (((A_A (A_A_u Int))))) + (check-valid + (declare-var a A) + (block + (assign a ((_ update-field A_A_u) a 3)) + (assert (= (A_A_u a) 3)) + ) + ) + ) +} diff --git a/source/air/src/typecheck.rs b/source/air/src/typecheck.rs index e11d3e1057..95817673e8 100644 --- a/source/air/src/typecheck.rs +++ b/source/air/src/typecheck.rs @@ -262,6 +262,14 @@ fn check_expr(typing: &mut Typing, expr: &Expr) -> Result { )) } } + ExprX::Binary(BinaryOp::FieldUpdate(field_ident), e1, e2) => { + // TODO(andrea) we may need more information about the field we are accessing here + // I need to look into this a bit more. For now, let's assume that the typecheck is successful. + // The type of the result will be the type of `e1` (i.e. the datatype that we're updating) + let t1 = check_expr(typing, e1)?; + let t2 = check_expr(typing, e2)?; + Ok(t1) + } ExprX::Binary(BinaryOp::Le, e1, e2) => { check_exprs(typing, "<=", &[it(), it()], &bt(), &[e1.clone(), e2.clone()]) } diff --git a/source/air/src/visitor.rs b/source/air/src/visitor.rs index d71fb97bce..cba86c0043 100644 --- a/source/air/src/visitor.rs +++ b/source/air/src/visitor.rs @@ -25,13 +25,13 @@ pub(crate) fn map_expr_visitor Expr>(expr: &Expr, f: &mut F) } ExprX::Unary(op, e1) => { let expr1 = map_expr_visitor(e1, f); - let expr = Arc::new(ExprX::Unary(*op, expr1)); + let expr = Arc::new(ExprX::Unary(op.clone(), expr1)); f(&expr) } ExprX::Binary(op, e1, e2) => { let expr1 = map_expr_visitor(e1, f); let expr2 = map_expr_visitor(e2, f); - let expr = Arc::new(ExprX::Binary(*op, expr1, expr2)); + let expr = Arc::new(ExprX::Binary(op.clone(), expr1, expr2)); f(&expr) } ExprX::Multi(op, es) => { From 53db4952317e8e44239e6902ed8fe87625d1f8fc Mon Sep 17 00:00:00 2001 From: Tim Date: Wed, 16 Oct 2024 14:31:46 +0200 Subject: [PATCH 02/13] emitted update-field --- source/air/src/printer.rs | 63 ++++++++++++++++++++------------------- 1 file changed, 32 insertions(+), 31 deletions(-) diff --git a/source/air/src/printer.rs b/source/air/src/printer.rs index 0902501d9e..bf3a38c3cf 100644 --- a/source/air/src/printer.rs +++ b/source/air/src/printer.rs @@ -193,41 +193,42 @@ impl Printer { Node::List(vec![op, self.expr_to_node(lhs), self.expr_to_node(rhs)]) } ExprX::Binary(op, lhs, rhs) => { - let sop = match op { - BinaryOp::Implies => "=>", - BinaryOp::Eq => "=", - BinaryOp::Le => "<=", - BinaryOp::Ge => ">=", - BinaryOp::Lt => "<", - BinaryOp::Gt => ">", - BinaryOp::EuclideanDiv => "div", - BinaryOp::EuclideanMod => "mod", + let sop: Node = match op { + BinaryOp::Implies => str_to_node("=>"), + BinaryOp::Eq => str_to_node("="), + BinaryOp::Le => str_to_node("<="), + BinaryOp::Ge => str_to_node(">="), + BinaryOp::Lt => str_to_node("<"), + BinaryOp::Gt => str_to_node(">"), + BinaryOp::EuclideanDiv => str_to_node("div"), + BinaryOp::EuclideanMod => str_to_node("mod"), BinaryOp::Relation(..) => unreachable!(), - BinaryOp::BitXor => "bvxor", - BinaryOp::BitAnd => "bvand", - BinaryOp::BitOr => "bvor", - BinaryOp::BitAdd => "bvadd", - BinaryOp::BitSub => "bvsub", - BinaryOp::BitMul => "bvmul", - BinaryOp::BitUDiv => "bvudiv", - BinaryOp::BitUMod => "bvurem", - BinaryOp::BitULt => "bvult", - BinaryOp::BitUGt => "bvugt", - BinaryOp::BitULe => "bvule", - BinaryOp::BitUGe => "bvuge", - BinaryOp::BitSLt => "bvslt", - BinaryOp::BitSGt => "bvsgt", - BinaryOp::BitSLe => "bvsle", - BinaryOp::BitSGe => "bvsge", - BinaryOp::LShr => "bvlshr", - BinaryOp::AShr => "bvashr", - BinaryOp::Shl => "bvshl", - BinaryOp::BitConcat => "concat", + BinaryOp::BitXor => str_to_node("bvxor"), + BinaryOp::BitAnd => str_to_node("bvand"), + BinaryOp::BitOr => str_to_node("bvor"), + BinaryOp::BitAdd => str_to_node("bvadd"), + BinaryOp::BitSub => str_to_node("bvsub"), + BinaryOp::BitMul => str_to_node("bvmul"), + BinaryOp::BitUDiv => str_to_node("bvudiv"), + BinaryOp::BitUMod => str_to_node("bvurem"), + BinaryOp::BitULt => str_to_node("bvult"), + BinaryOp::BitUGt => str_to_node("bvugt"), + BinaryOp::BitULe => str_to_node("bvule"), + BinaryOp::BitUGe => str_to_node("bvuge"), + BinaryOp::BitSLt => str_to_node("bvslt"), + BinaryOp::BitSGt => str_to_node("bvsgt"), + BinaryOp::BitSLe => str_to_node("bvsle"), + BinaryOp::BitSGe => str_to_node("bvsge"), + BinaryOp::LShr => str_to_node("bvlshr"), + BinaryOp::AShr => str_to_node("bvashr"), + BinaryOp::Shl => str_to_node("bvshl"), + BinaryOp::BitConcat => str_to_node("concat"), BinaryOp::FieldUpdate(field_ident) => { - todo!("TODO: emit (_ update-field )") + //todo!("TODO: emit (_ update-field )") + Node::List(vec![str_to_node("_"), str_to_node("update-field"), str_to_node(&**field_ident)]) } }; - Node::List(vec![str_to_node(sop), self.expr_to_node(lhs), self.expr_to_node(rhs)]) + Node::List(vec![sop, self.expr_to_node(lhs), self.expr_to_node(rhs)]) } ExprX::Multi(op, exprs) => { let sop = match op { From 69223be09e27b75eceddf69bd8d83c39643a2e0c Mon Sep 17 00:00:00 2001 From: Andrea Lattuada Date: Thu, 17 Oct 2024 17:25:04 +0200 Subject: [PATCH 03/13] add negative typing test for field-update --- source/air/src/tests.rs | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) diff --git a/source/air/src/tests.rs b/source/air/src/tests.rs index dac5905883..d2f1eacb4c 100644 --- a/source/air/src/tests.rs +++ b/source/air/src/tests.rs @@ -2104,7 +2104,7 @@ fn no_partial_order() { } #[test] -fn datatype_field_update() { +fn datatype_field_update_pass() { yes!( (declare-datatypes ((A 0)) (((A_A (A_A_u Int))))) (check-valid @@ -2116,3 +2116,19 @@ fn datatype_field_update() { ) ) } + +#[test] +fn datatype_field_update_ill_typed() { + untyped!( + (declare-datatypes ((X 0)) (((X_X (X_X_u Int))))) + (declare-datatypes ((A 0)) (((A_A (A_A_u Int))))) + (check-valid + (declare-var a A) + (declare-const x X) + (block + (assign a ((_ update-field A_A_u) a x)) + (assert (= (A_A_u a) 3)) + ) + ) + ) +} From 8124f03e6d792bb0352275ba86b6758ae3828474 Mon Sep 17 00:00:00 2001 From: Tim Date: Thu, 17 Oct 2024 17:44:53 +0200 Subject: [PATCH 04/13] more update-field test --- source/air/src/printer.rs | 6 +++++- source/air/src/tests.rs | 42 +++++++++++++++++++++++++++++++++++++++ 2 files changed, 47 insertions(+), 1 deletion(-) diff --git a/source/air/src/printer.rs b/source/air/src/printer.rs index bf3a38c3cf..b8292881e4 100644 --- a/source/air/src/printer.rs +++ b/source/air/src/printer.rs @@ -225,7 +225,11 @@ impl Printer { BinaryOp::BitConcat => str_to_node("concat"), BinaryOp::FieldUpdate(field_ident) => { //todo!("TODO: emit (_ update-field )") - Node::List(vec![str_to_node("_"), str_to_node("update-field"), str_to_node(&**field_ident)]) + Node::List(vec![ + str_to_node("_"), + str_to_node("update-field"), + str_to_node(&**field_ident), + ]) } }; Node::List(vec![sop, self.expr_to_node(lhs), self.expr_to_node(rhs)]) diff --git a/source/air/src/tests.rs b/source/air/src/tests.rs index d2f1eacb4c..f229130129 100644 --- a/source/air/src/tests.rs +++ b/source/air/src/tests.rs @@ -2132,3 +2132,45 @@ fn datatype_field_update_ill_typed() { ) ) } + +#[test] +fn datatype_field_update2() { + no!( + (declare-datatypes ((A 0)) (((A_A (A_A_u Int))))) + (check-valid + (declare-var a A) + (block + (assign a ((_ update-field A_A_u) a 3)) + (assert (= (A_A_u a) 4)) + ) + ) + ) +} + +#[test] +fn datatype_field_update3() { + yes!( + (declare-datatypes ((A 0)) (((A_A (A_A_u Int) (A_A_v Int))))) + (check-valid + (declare-var a A) + (block + (assign a ((_ update-field A_A_u) a 3)) + (assert (= (A_A_u a) 3)) + ) + ) + ) +} + +#[test] +fn datatype_field_update4() { + no!( + (declare-datatypes ((A 0)) (((A_A (A_A_u Int) (A_A_v Int))))) + (check-valid + (declare-var a A) + (block + (assign a ((_ update-field A_A_u) a 3)) + (assert (= (A_A_u a) 4)) + ) + ) + ) +} From 43f27ad385831293e1f68f768ae39fc55b2a4a2b Mon Sep 17 00:00:00 2001 From: Tim Date: Tue, 22 Oct 2024 14:23:16 +0200 Subject: [PATCH 05/13] typechecked field-update --- source/air/src/typecheck.rs | 22 ++++++++++++++++++++-- 1 file changed, 20 insertions(+), 2 deletions(-) diff --git a/source/air/src/typecheck.rs b/source/air/src/typecheck.rs index 95817673e8..e58e87e05d 100644 --- a/source/air/src/typecheck.rs +++ b/source/air/src/typecheck.rs @@ -14,7 +14,7 @@ use std::collections::HashSet; use std::sync::Arc; pub(crate) type Declared = Arc; -#[derive(Clone)] +#[derive(Clone, Debug)] pub(crate) enum DeclaredX { Type, Var { typ: Typ, mutable: bool }, @@ -268,7 +268,25 @@ fn check_expr(typing: &mut Typing, expr: &Expr) -> Result { // The type of the result will be the type of `e1` (i.e. the datatype that we're updating) let t1 = check_expr(typing, e1)?; let t2 = check_expr(typing, e2)?; - Ok(t1) + + match &*t1 { + TypX::Named(s) => match typing.get(s) { + Some(DeclaredX::Type) => {} + _ => return Err(format!("{} is not a struct", "e1")), //TODO below + }, + _ => return Err(format!("{} is not a struct", "e1")), //TODO find out how to print e1 + } + + if let Some(DeclaredX::Fun(a, t)) = typing.get(field_ident) { + // t is the type of the field + if let [s] = &a[..] { + if t1 == *s && t2 == *t { + return Ok(t1); + } + } + } + + Err(format!("{} is not a struct accessor", field_ident)) // TODO more details here } ExprX::Binary(BinaryOp::Le, e1, e2) => { check_exprs(typing, "<=", &[it(), it()], &bt(), &[e1.clone(), e2.clone()]) From 96c5fd44990c7143954bf512a9a8b48a25fb2944 Mon Sep 17 00:00:00 2001 From: Tim Date: Wed, 23 Oct 2024 14:55:04 +0200 Subject: [PATCH 06/13] added nested datatype field update tests --- source/air/src/tests.rs | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/source/air/src/tests.rs b/source/air/src/tests.rs index f229130129..08483ada6b 100644 --- a/source/air/src/tests.rs +++ b/source/air/src/tests.rs @@ -2174,3 +2174,33 @@ fn datatype_field_update4() { ) ) } + +#[test] +fn nested_datatype_field_update_pass() { + yes!( + (declare-datatypes ((A 0)) (((A_A (A_A_u Int))))) + (declare-datatypes ((B 0)) (((B_B (B_B_a A))))) + (check-valid + (declare-var b B) + (block + (assign b ((_ update-field B_B_a) b ((_ update-field A_A_u) (B_B_a b) 3))) + (assert (= (A_A_u (B_B_a b)) 3)) + ) + ) + ) +} + +#[test] +fn nested_datatype_field_update_fail() { + no!( + (declare-datatypes ((A 0)) (((A_A (A_A_u Int))))) + (declare-datatypes ((B 0)) (((B_B (B_B_a A))))) + (check-valid + (declare-var b B) + (block + (assign b ((_ update-field B_B_a) b ((_ update-field A_A_u) (B_B_a b) 3))) + (assert (= (A_A_u (B_B_a b)) 4)) + ) + ) + ) +} From b658eaa40a3e968fff72a352fa4e6744f0b5a137 Mon Sep 17 00:00:00 2001 From: Tim Date: Wed, 23 Oct 2024 17:19:30 +0200 Subject: [PATCH 07/13] equipped DeclardX::Fun with Boolean to identify accessors --- source/air/src/closure.rs | 4 ++-- source/air/src/tests.rs | 15 +++++++++++++++ source/air/src/typecheck.rs | 22 +++++++++++----------- 3 files changed, 28 insertions(+), 13 deletions(-) diff --git a/source/air/src/closure.rs b/source/air/src/closure.rs index 7ced319ef8..37b3e8d7a0 100644 --- a/source/air/src/closure.rs +++ b/source/air/src/closure.rs @@ -76,7 +76,7 @@ pub(crate) struct ClosureTermX { // The function declarations live in scope outside the expression scope, so // we need to insert them into the typing's outer scope: fn insert_fun_typing(ctxt: &mut Context, x: &Ident, typs: &Typs, typ: &Typ) { - let fun = DeclaredX::Fun(typs.clone(), typ.clone()); + let fun = DeclaredX::Fun(typs.clone(), typ.clone(), false); // the maps that aren't ctxt.typing.decls (e.g. apply_map) are still in the outer scope, // so use one of them as the outer scope index: @@ -521,7 +521,7 @@ fn simplify_expr(ctxt: &mut Context, state: &mut State, expr: &Expr) -> (Typ, Ex } ExprX::Apply(x, args) => { let typ = match ctxt.typing.get(x) { - Some(DeclaredX::Fun(_, typ)) => typ.clone(), + Some(DeclaredX::Fun(_, typ, _)) => typ.clone(), _ => panic!("internal error: missing function {}", x), }; let (es, ts) = simplify_exprs(ctxt, state, &**args); diff --git a/source/air/src/tests.rs b/source/air/src/tests.rs index 08483ada6b..fe8f7f4410 100644 --- a/source/air/src/tests.rs +++ b/source/air/src/tests.rs @@ -2204,3 +2204,18 @@ fn nested_datatype_field_update_fail() { ) ) } + +#[test] +fn accessor_identifying() { + untyped!( + (declare-datatypes ((A 0)) (((A_A (A_A_u Int))))) + (declare-fun f (A) Int ) + (check-valid + (declare-var a A) + (block + (assign a ((_ update-field f) a 3)) + (assert (= (A_A_u a) 4)) + ) + ) + ) +} diff --git a/source/air/src/typecheck.rs b/source/air/src/typecheck.rs index e58e87e05d..660f25b27d 100644 --- a/source/air/src/typecheck.rs +++ b/source/air/src/typecheck.rs @@ -18,7 +18,7 @@ pub(crate) type Declared = Arc; pub(crate) enum DeclaredX { Type, Var { typ: Typ, mutable: bool }, - Fun(Typs, Typ), + Fun(Typs, Typ, bool), //args, ret, accessor TODO explicitly name this } pub struct Typing { @@ -214,7 +214,7 @@ fn check_expr(typing: &mut Typing, expr: &Expr) -> Result { (true, _) => Err(format!("use of undeclared variable {}", x)), }, ExprX::Apply(x, es) => match typing.get(x).cloned() { - Some(DeclaredX::Fun(f_typs, f_typ)) => check_exprs(typing, x, &f_typs, &f_typ, es), + Some(DeclaredX::Fun(f_typs, f_typ, _)) => check_exprs(typing, x, &f_typs, &f_typ, es), _ => Err(format!("use of undeclared function {}", x)), }, ExprX::ApplyFun(t, e0, es) => { @@ -272,12 +272,12 @@ fn check_expr(typing: &mut Typing, expr: &Expr) -> Result { match &*t1 { TypX::Named(s) => match typing.get(s) { Some(DeclaredX::Type) => {} - _ => return Err(format!("{} is not a struct", "e1")), //TODO below + _ => return Err(format!("in field update, the destination is not a datatype")), }, - _ => return Err(format!("{} is not a struct", "e1")), //TODO find out how to print e1 + _ => return Err(format!("in field update, the destination is not a datatype")), } - if let Some(DeclaredX::Fun(a, t)) = typing.get(field_ident) { + if let Some(DeclaredX::Fun(a, t, true)) = typing.get(field_ident) { // t is the type of the field if let [s] = &a[..] { if t1 == *s && t2 == *t { @@ -286,7 +286,7 @@ fn check_expr(typing: &mut Typing, expr: &Expr) -> Result { } } - Err(format!("{} is not a struct accessor", field_ident)) // TODO more details here + Err(format!("field update types do not match")) // TODO more details here } ExprX::Binary(BinaryOp::Le, e1, e2) => { check_exprs(typing, "<=", &[it(), it()], &bt(), &[e1.clone(), e2.clone()]) @@ -638,15 +638,15 @@ pub(crate) fn add_decl<'ctx>( for variant in datatype.a.iter() { let typ = Arc::new(TypX::Named(datatype.name.clone())); let typs = vec_map(&variant.a, |field| field.a.clone()); - let fun = DeclaredX::Fun(Arc::new(typs), typ.clone()); - context.typing.insert(&variant.name, Arc::new(fun))?; + let fun = DeclaredX::Fun(Arc::new(typs), typ.clone(), false); // Type of constructor + context.typing.insert(&variant.name, Arc::new(fun))?; // Add Constructor under variant name to typing let is_variant = Arc::new("is-".to_string() + &variant.name.to_string()); - let fun = DeclaredX::Fun(Arc::new(vec![typ.clone()]), bt()); + let fun = DeclaredX::Fun(Arc::new(vec![typ.clone()]), bt(), false); context.typing.insert(&is_variant, Arc::new(fun))?; for field in variant.a.iter() { check_typ(&context.typing, &field.a)?; let typs: Typs = Arc::new(vec![typ.clone()]); - let fun = DeclaredX::Fun(typs, field.a.clone()); + let fun = DeclaredX::Fun(typs, field.a.clone(), true); context.typing.insert(&field.name, Arc::new(fun))?; } } @@ -657,7 +657,7 @@ pub(crate) fn add_decl<'ctx>( context.typing.insert(x, var)?; } DeclX::Fun(x, typs, typ) => { - let fun = DeclaredX::Fun(typs.clone(), typ.clone()); + let fun = DeclaredX::Fun(typs.clone(), typ.clone(), false); context.typing.insert(x, Arc::new(fun))?; } DeclX::Var(x, typ) => { From ff888f03d4e865e3be2db37f944c944b7c69ed6e Mon Sep 17 00:00:00 2001 From: Andrea Lattuada Date: Wed, 23 Oct 2024 18:15:00 +0200 Subject: [PATCH 08/13] add test that using the field name fro m a different datatype causes a type error with update-field --- source/air/src/tests.rs | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) diff --git a/source/air/src/tests.rs b/source/air/src/tests.rs index fe8f7f4410..2b8cd54cad 100644 --- a/source/air/src/tests.rs +++ b/source/air/src/tests.rs @@ -2206,7 +2206,7 @@ fn nested_datatype_field_update_fail() { } #[test] -fn accessor_identifying() { +fn accessor_identifying_1() { untyped!( (declare-datatypes ((A 0)) (((A_A (A_A_u Int))))) (declare-fun f (A) Int ) @@ -2219,3 +2219,18 @@ fn accessor_identifying() { ) ) } + +#[test] +fn accessor_identifying_2() { + untyped!( + (declare-datatypes ((A 0)) (((A_A (A_A_u Int))))) + (declare-datatypes ((B 0)) (((B_B (B_B_u Int))))) + (check-valid + (declare-var a A) + (block + (assign a ((_ update-field B_B_u) a 3)) + (assert (= (A_A_u a) 4)) + ) + ) + ) +} From 21c2253358bb0ea548d72e8f541e7e50dfb71202 Mon Sep 17 00:00:00 2001 From: Tim Date: Wed, 23 Oct 2024 18:18:25 +0200 Subject: [PATCH 09/13] deleted todo --- source/air/src/typecheck.rs | 3 --- 1 file changed, 3 deletions(-) diff --git a/source/air/src/typecheck.rs b/source/air/src/typecheck.rs index 660f25b27d..72920804b8 100644 --- a/source/air/src/typecheck.rs +++ b/source/air/src/typecheck.rs @@ -263,9 +263,6 @@ fn check_expr(typing: &mut Typing, expr: &Expr) -> Result { } } ExprX::Binary(BinaryOp::FieldUpdate(field_ident), e1, e2) => { - // TODO(andrea) we may need more information about the field we are accessing here - // I need to look into this a bit more. For now, let's assume that the typecheck is successful. - // The type of the result will be the type of `e1` (i.e. the datatype that we're updating) let t1 = check_expr(typing, e1)?; let t2 = check_expr(typing, e2)?; From c87d09084b57ba51f3df4b740427906c7741af19 Mon Sep 17 00:00:00 2001 From: Tim Date: Wed, 23 Oct 2024 18:31:35 +0200 Subject: [PATCH 10/13] cleaned up comments --- source/air/src/printer.rs | 13 +++++-------- source/air/src/typecheck.rs | 6 +++--- 2 files changed, 8 insertions(+), 11 deletions(-) diff --git a/source/air/src/printer.rs b/source/air/src/printer.rs index b8292881e4..59044af20d 100644 --- a/source/air/src/printer.rs +++ b/source/air/src/printer.rs @@ -223,14 +223,11 @@ impl Printer { BinaryOp::AShr => str_to_node("bvashr"), BinaryOp::Shl => str_to_node("bvshl"), BinaryOp::BitConcat => str_to_node("concat"), - BinaryOp::FieldUpdate(field_ident) => { - //todo!("TODO: emit (_ update-field )") - Node::List(vec![ - str_to_node("_"), - str_to_node("update-field"), - str_to_node(&**field_ident), - ]) - } + BinaryOp::FieldUpdate(field_ident) => Node::List(vec![ + str_to_node("_"), + str_to_node("update-field"), + str_to_node(&**field_ident), + ]), }; Node::List(vec![sop, self.expr_to_node(lhs), self.expr_to_node(rhs)]) } diff --git a/source/air/src/typecheck.rs b/source/air/src/typecheck.rs index 72920804b8..48c9654ead 100644 --- a/source/air/src/typecheck.rs +++ b/source/air/src/typecheck.rs @@ -283,7 +283,7 @@ fn check_expr(typing: &mut Typing, expr: &Expr) -> Result { } } - Err(format!("field update types do not match")) // TODO more details here + Err(format!("field update types do not match")) } ExprX::Binary(BinaryOp::Le, e1, e2) => { check_exprs(typing, "<=", &[it(), it()], &bt(), &[e1.clone(), e2.clone()]) @@ -635,8 +635,8 @@ pub(crate) fn add_decl<'ctx>( for variant in datatype.a.iter() { let typ = Arc::new(TypX::Named(datatype.name.clone())); let typs = vec_map(&variant.a, |field| field.a.clone()); - let fun = DeclaredX::Fun(Arc::new(typs), typ.clone(), false); // Type of constructor - context.typing.insert(&variant.name, Arc::new(fun))?; // Add Constructor under variant name to typing + let fun = DeclaredX::Fun(Arc::new(typs), typ.clone(), false); + context.typing.insert(&variant.name, Arc::new(fun))?; let is_variant = Arc::new("is-".to_string() + &variant.name.to_string()); let fun = DeclaredX::Fun(Arc::new(vec![typ.clone()]), bt(), false); context.typing.insert(&is_variant, Arc::new(fun))?; From d8a87adfa383541f15233e0adffa282d44c465c6 Mon Sep 17 00:00:00 2001 From: Tim Date: Fri, 25 Oct 2024 21:25:06 +0200 Subject: [PATCH 11/13] cleaned up more todos --- source/air/src/printer.rs | 2 +- source/air/src/typecheck.rs | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/source/air/src/printer.rs b/source/air/src/printer.rs index 59044af20d..e7f08f109d 100644 --- a/source/air/src/printer.rs +++ b/source/air/src/printer.rs @@ -193,7 +193,7 @@ impl Printer { Node::List(vec![op, self.expr_to_node(lhs), self.expr_to_node(rhs)]) } ExprX::Binary(op, lhs, rhs) => { - let sop: Node = match op { + let sop = match op { BinaryOp::Implies => str_to_node("=>"), BinaryOp::Eq => str_to_node("="), BinaryOp::Le => str_to_node("<="), diff --git a/source/air/src/typecheck.rs b/source/air/src/typecheck.rs index 48c9654ead..8296a22d35 100644 --- a/source/air/src/typecheck.rs +++ b/source/air/src/typecheck.rs @@ -14,11 +14,11 @@ use std::collections::HashSet; use std::sync::Arc; pub(crate) type Declared = Arc; -#[derive(Clone, Debug)] +#[derive(Clone)] pub(crate) enum DeclaredX { Type, Var { typ: Typ, mutable: bool }, - Fun(Typs, Typ, bool), //args, ret, accessor TODO explicitly name this + Fun(Typs, Typ, bool), //args, ret, accessor } pub struct Typing { From da2e55aad9b6f398fdde372e4f260e089310e9c3 Mon Sep 17 00:00:00 2001 From: Andrea Lattuada Date: Sun, 27 Oct 2024 14:43:16 +0100 Subject: [PATCH 12/13] name field of AIR's DeclaredX::Fun --- source/air/src/closure.rs | 4 ++-- source/air/src/typecheck.rs | 35 ++++++++++++++++++++++++++--------- 2 files changed, 28 insertions(+), 11 deletions(-) diff --git a/source/air/src/closure.rs b/source/air/src/closure.rs index 37b3e8d7a0..3e8125c0e6 100644 --- a/source/air/src/closure.rs +++ b/source/air/src/closure.rs @@ -76,7 +76,7 @@ pub(crate) struct ClosureTermX { // The function declarations live in scope outside the expression scope, so // we need to insert them into the typing's outer scope: fn insert_fun_typing(ctxt: &mut Context, x: &Ident, typs: &Typs, typ: &Typ) { - let fun = DeclaredX::Fun(typs.clone(), typ.clone(), false); + let fun = DeclaredX::Fun { params: typs.clone(), ret: typ.clone(), field_accessor: false }; // the maps that aren't ctxt.typing.decls (e.g. apply_map) are still in the outer scope, // so use one of them as the outer scope index: @@ -521,7 +521,7 @@ fn simplify_expr(ctxt: &mut Context, state: &mut State, expr: &Expr) -> (Typ, Ex } ExprX::Apply(x, args) => { let typ = match ctxt.typing.get(x) { - Some(DeclaredX::Fun(_, typ, _)) => typ.clone(), + Some(DeclaredX::Fun { params: _, ret, field_accessor: _ }) => ret.clone(), _ => panic!("internal error: missing function {}", x), }; let (es, ts) = simplify_exprs(ctxt, state, &**args); diff --git a/source/air/src/typecheck.rs b/source/air/src/typecheck.rs index 8296a22d35..a609e3c870 100644 --- a/source/air/src/typecheck.rs +++ b/source/air/src/typecheck.rs @@ -18,7 +18,7 @@ pub(crate) type Declared = Arc; pub(crate) enum DeclaredX { Type, Var { typ: Typ, mutable: bool }, - Fun(Typs, Typ, bool), //args, ret, accessor + Fun { params: Typs, ret: Typ, field_accessor: bool }, //args, ret, accessor } pub struct Typing { @@ -214,7 +214,9 @@ fn check_expr(typing: &mut Typing, expr: &Expr) -> Result { (true, _) => Err(format!("use of undeclared variable {}", x)), }, ExprX::Apply(x, es) => match typing.get(x).cloned() { - Some(DeclaredX::Fun(f_typs, f_typ, _)) => check_exprs(typing, x, &f_typs, &f_typ, es), + Some(DeclaredX::Fun { params, ret, field_accessor: _ }) => { + check_exprs(typing, x, ¶ms, &ret, es) + } _ => Err(format!("use of undeclared function {}", x)), }, ExprX::ApplyFun(t, e0, es) => { @@ -274,10 +276,12 @@ fn check_expr(typing: &mut Typing, expr: &Expr) -> Result { _ => return Err(format!("in field update, the destination is not a datatype")), } - if let Some(DeclaredX::Fun(a, t, true)) = typing.get(field_ident) { + if let Some(DeclaredX::Fun { params, ret, field_accessor: true }) = + typing.get(field_ident) + { // t is the type of the field - if let [s] = &a[..] { - if t1 == *s && t2 == *t { + if let [s] = ¶ms[..] { + if t1 == *s && t2 == *ret { return Ok(t1); } } @@ -635,15 +639,27 @@ pub(crate) fn add_decl<'ctx>( for variant in datatype.a.iter() { let typ = Arc::new(TypX::Named(datatype.name.clone())); let typs = vec_map(&variant.a, |field| field.a.clone()); - let fun = DeclaredX::Fun(Arc::new(typs), typ.clone(), false); + let fun = DeclaredX::Fun { + params: Arc::new(typs), + ret: typ.clone(), + field_accessor: false, + }; context.typing.insert(&variant.name, Arc::new(fun))?; let is_variant = Arc::new("is-".to_string() + &variant.name.to_string()); - let fun = DeclaredX::Fun(Arc::new(vec![typ.clone()]), bt(), false); + let fun = DeclaredX::Fun { + params: Arc::new(vec![typ.clone()]), + ret: bt(), + field_accessor: false, + }; context.typing.insert(&is_variant, Arc::new(fun))?; for field in variant.a.iter() { check_typ(&context.typing, &field.a)?; let typs: Typs = Arc::new(vec![typ.clone()]); - let fun = DeclaredX::Fun(typs, field.a.clone(), true); + let fun = DeclaredX::Fun { + params: typs, + ret: field.a.clone(), + field_accessor: true, + }; context.typing.insert(&field.name, Arc::new(fun))?; } } @@ -654,7 +670,8 @@ pub(crate) fn add_decl<'ctx>( context.typing.insert(x, var)?; } DeclX::Fun(x, typs, typ) => { - let fun = DeclaredX::Fun(typs.clone(), typ.clone(), false); + let fun = + DeclaredX::Fun { params: typs.clone(), ret: typ.clone(), field_accessor: false }; context.typing.insert(x, Arc::new(fun))?; } DeclX::Var(x, typ) => { From 8324ea546ddeec818970e25dfe2cf145995a3eb4 Mon Sep 17 00:00:00 2001 From: Tim Date: Thu, 31 Oct 2024 11:07:35 +0100 Subject: [PATCH 13/13] additional nested datatype test --- source/air/src/tests.rs | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/source/air/src/tests.rs b/source/air/src/tests.rs index 2b8cd54cad..aa4913ee71 100644 --- a/source/air/src/tests.rs +++ b/source/air/src/tests.rs @@ -2190,6 +2190,21 @@ fn nested_datatype_field_update_pass() { ) } +#[test] +fn nested_datatype_field_update_pass2() { + yes!( + (declare-datatypes ((A 0)) (((A_A (A_A_u Int) (A_A_v Int))))) + (declare-datatypes ((B 0)) (((B_B (B_B_a1 A) (B_B_a2 A))))) + (check-valid + (declare-var b B) + (block + (assign b ((_ update-field B_B_a1) b ((_ update-field A_A_u) (B_B_a1 b) 3))) + (assert (= (A_A_u (B_B_a1 b)) 3)) + ) + ) + ) +} + #[test] fn nested_datatype_field_update_fail() { no!(