diff --git a/uvls/src/core/ast/transform.rs b/uvls/src/core/ast/transform.rs index 6d632c5a..6dd014f3 100644 --- a/uvls/src/core/ast/transform.rs +++ b/uvls/src/core/ast/transform.rs @@ -8,6 +8,7 @@ use parse::*; use ropey::Rope; use semantic::FileID; use std::borrow::{Borrow, Cow}; +use std::collections::HashSet; use tokio::time::Instant; use tower_lsp::lsp_types::{DiagnosticSeverity, Url}; use tree_sitter::{Node, Tree, TreeCursor}; @@ -668,6 +669,30 @@ fn opt_aggregate(state: &mut VisitorState) -> Option { state.push_error(10, "tailing comma not allowed"); } let args = opt_function_args(state)?; + + let argnames: HashSet = + HashSet::from_iter(args.iter().flat_map(|p| p.names.clone()).into_iter()); + let check_arg_type_number = || -> bool { + state + .ast + .all_attributes() + .filter_map(|sym| { + if let Symbol::Attribute(aidx) = sym { + Some(state.ast.get_attribute(aidx)) + } else { + None + } + }) + .find(|attr| { + argnames.contains(&attr.unwrap().name.name) + && matches!(attr.unwrap().value.value, Value::Number(..)) + }) + .is_some() + }; + if !check_arg_type_number() { + state.push_error(30, "invalid argument. number attribute expected"); + } + match args.len() { 0 => { state.push_error(30, "missing arguments"); @@ -684,7 +709,7 @@ fn opt_aggregate(state: &mut VisitorState) -> Option { context: Some(state.add_ref_direct(args[0].clone())), }), _ => { - state.push_error(30, "to many arguments"); + state.push_error(30, "too many arguments"); None } } diff --git a/uvls/src/core/module.rs b/uvls/src/core/module.rs index c66d3b43..a59b20b5 100644 --- a/uvls/src/core/module.rs +++ b/uvls/src/core/module.rs @@ -439,7 +439,9 @@ impl ConfigModule { //Turns a the set of linear configuration values of this module into theire recusive from //used in json pub fn serialize(&self) -> Vec { - let ConfigEntry::Import(_,v) = self.serialize_rec(&[],InstanceID(0)) else {unreachable!()}; + let ConfigEntry::Import(_, v) = self.serialize_rec(&[], InstanceID(0)) else { + unreachable!() + }; v } } diff --git a/uvls/src/smt/parse.rs b/uvls/src/smt/parse.rs index ba64fd60..aa236962 100644 --- a/uvls/src/smt/parse.rs +++ b/uvls/src/smt/parse.rs @@ -176,17 +176,29 @@ mod tests { _ => Type::Real, }, }; - let (i,(_,ConfigValue::Number(n))) = parser.parse(i).unwrap() else {panic!()}; + let (i, (_, ConfigValue::Number(n))) = parser.parse(i).unwrap() else { + panic!() + }; assert_approx_eq!(n, -1.0); - let (i,(_,ConfigValue::Number(n))) = parser.parse(i).unwrap() else {panic!()}; + let (i, (_, ConfigValue::Number(n))) = parser.parse(i).unwrap() else { + panic!() + }; assert_approx_eq!(n, -1.0 / 103.0); - let (i,(_,ConfigValue::Number(n))) = parser.parse(i).unwrap() else {panic!()}; + let (i, (_, ConfigValue::Number(n))) = parser.parse(i).unwrap() else { + panic!() + }; assert_approx_eq!(n, 100.0 - 1.333 / 102.0); - let (i,(_,ConfigValue::String(n))) = parser.parse(i).unwrap() else {panic!()}; + let (i, (_, ConfigValue::String(n))) = parser.parse(i).unwrap() else { + panic!() + }; assert_eq!(n, "test"); - let (i,(_,ConfigValue::Bool(n))) = parser.parse(i).unwrap() else {panic!()}; + let (i, (_, ConfigValue::Bool(n))) = parser.parse(i).unwrap() else { + panic!() + }; assert_eq!(n, true); - let (_i,(_,ConfigValue::Number(n))) = parser.parse(i).unwrap() else {panic!()}; + let (_i, (_, ConfigValue::Number(n))) = parser.parse(i).unwrap() else { + panic!() + }; assert_approx_eq!(n, 1.0); } } diff --git a/uvls/src/smt/smt_lib.rs b/uvls/src/smt/smt_lib.rs index 3d681d0c..dc8e00f2 100644 --- a/uvls/src/smt/smt_lib.rs +++ b/uvls/src/smt/smt_lib.rs @@ -570,29 +570,37 @@ pub fn uvl2smt(module: &Module, config: &HashMap) -> return true; } let ms = m.sym(a); - let Some((val, n)) = config.get(&ms).map(|v|( v.clone().into() ,AssertName::Config )).or_else(|| { - file.value(a) - .and_then(|v| match v { - ast::Value::Bool(x) => Some(Expr::Bool(*x)), - ast::Value::Number(x) => Some(Expr::Real(*x)), - ast::Value::String(x) => Some(Expr::String(x.clone())), - _ => None, - }) - .map(|v| (v, AssertName::Attribute)) - }) else {return true} ; + let Some((val, n)) = config + .get(&ms) + .map(|v| (v.clone().into(), AssertName::Config)) + .or_else(|| { + file.value(a) + .and_then(|v| match v { + ast::Value::Bool(x) => Some(Expr::Bool(*x)), + ast::Value::Number(x) => Some(Expr::Real(*x)), + ast::Value::String(x) => Some(Expr::String(x.clone())), + _ => None, + }) + .map(|v| (v, AssertName::Attribute)) + }) + else { + return true; + }; let zero = match val { Expr::Bool(..) => Expr::Bool(false), Expr::Real(..) => Expr::Real(0.0), Expr::String(..) => Expr::String("".into()), - _=>unreachable!() + _ => unreachable!(), }; let attrib_var = builder.push_var(ms); let feat_var = builder.pseudo_bool(m.sym(f)); - builder.assert.push(Assert(Some(AssertInfo(ms, n)),Expr::Equal(vec![ - Expr::Ite(feat_var.into(), - val.into(), - zero.into()), - attrib_var] ) )); + builder.assert.push(Assert( + Some(AssertInfo(ms, n)), + Expr::Equal(vec![ + Expr::Ite(feat_var.into(), val.into(), zero.into()), + attrib_var, + ]), + )); true }); } diff --git a/uvls/src/webview/frontend.rs b/uvls/src/webview/frontend.rs index b479d38d..9ee28db6 100644 --- a/uvls/src/webview/frontend.rs +++ b/uvls/src/webview/frontend.rs @@ -422,8 +422,15 @@ where .map(|(_, vn)| vn.depth <= v.depth) .unwrap_or(true); //Resolve link - if let UIEntryValue::Link{name,tgt,..} = &v.value{ - let UIEntryValue::Feature { config, smt_value, ty, unsat,.. } = &state.entries[tgt].value else{ + if let UIEntryValue::Link { name, tgt, .. } = &v.value { + let UIEntryValue::Feature { + config, + smt_value, + ty, + unsat, + .. + } = &state.entries[tgt].value + else { panic!() }; @@ -441,8 +448,7 @@ where } },leaf:leaf,sym:*tgt,key:"{k:?}",tag:tag} } - } - else{ + } else { rsx! { FileEntry{node:v.clone(),leaf:leaf,sym:*k,key:"{k:?}",tag:tag} }