diff --git a/src/mc/mod.rs b/src/mc/mod.rs index a370e603..9305020f 100644 --- a/src/mc/mod.rs +++ b/src/mc/mod.rs @@ -206,7 +206,7 @@ fn translate_variables( let decl = var_ref.borrow(); let mut comment = None; let initial_value = if let Some(initial_expr) = &decl.init { - if matches!(initial_expr.kind, ExprKind::Lit(_)) { + if is_constant(initial_expr) { Some(Box::new(translate_expr(initial_expr)?)) } else { let builder = ExprBuilder::new(Span::dummy_span()); @@ -418,3 +418,12 @@ fn extract_embed(expr: &Expr) -> Option { } None } + +/// Whether an expression is a constant value and can be evaluated without any +/// other variables. +/// +/// Right now, we just check directly that it is a literal. In the future, one +/// could allow more complex (constant) expressions as well. +fn is_constant(expr: &Expr) -> bool { + matches!(expr.kind, ExprKind::Lit(_)) +} diff --git a/src/mc/opsem.rs b/src/mc/opsem.rs index 1d64be18..ac3b0076 100644 --- a/src/mc/opsem.rs +++ b/src/mc/opsem.rs @@ -16,7 +16,9 @@ use crate::{ tyctx::TyCtx, }; -use super::{specs::SpecAutomaton, translate_expr, translate_ident, JaniConversionError}; +use super::{ + is_constant, specs::SpecAutomaton, translate_expr, translate_ident, JaniConversionError, +}; /// Intermediate structure to build the JANI automaton for pGCL semantics with /// expected rewards. @@ -86,7 +88,7 @@ fn translate_stmt( StmtKind::Var(decl_ref) => { let decl = decl_ref.borrow(); match &decl.init { - Some(init) if !is_pure(init) => { + Some(init) if !is_constant(init) => { translate_assign(automaton, span, translate_ident(decl.name), init, next) } Some(_) => Ok(next), @@ -339,10 +341,6 @@ pub fn translate_block( translate_stmts(automaton, &block.node, next) } -fn is_pure(expr: &Expr) -> bool { - !matches!(expr.kind, ExprKind::Call(_, _)) -} - fn translate_assign( automaton: &mut OpAutomaton, span: Span,