conjure_cp_essence_parser/parser/
letting.rs

1#![allow(clippy::legacy_numeric_constants)]
2use crate::field;
3use std::collections::BTreeSet;
4use tree_sitter::Node;
5
6use super::ParseContext;
7use super::domain::parse_domain;
8use super::keyword_checks::is_keyword_identifier;
9use super::util::named_children;
10use crate::diagnostics::diagnostics_api::SymbolKind;
11use crate::diagnostics::source_map::{HoverInfo, span_with_hover};
12use crate::errors::{FatalParseError, RecoverableParseError};
13use crate::expression::parse_expression;
14use conjure_cp_core::ast::DeclarationPtr;
15use conjure_cp_core::ast::{
16    Domain, DomainPtr, Expression, IntVal, Literal, Moo, Name, Range, ReturnType, SymbolTable,
17    Typeable, eval_constant,
18};
19
20/// Infer and retain the domain of a value letting when it enters the symbol table.
21///
22/// Integer lettings denote a single (possibly parameter-dependent) value:
23///
24/// - Constant integers become a ground singleton so dependent domains such as
25///   `int(1..10**n)` stay tight after the letting is installed.
26/// - Non-constant integers become a symbolic [`IntVal::Expr`] singleton. This remains
27///   resolvable after referenced `given` declarations are instantiated and, unlike eager
28///   interval evaluation, also works when those declarations currently have unbounded or
29///   full-width (`int`) domains.
30///
31/// Eager `Expression::domain_of` must not run here for non-constant integers: arithmetic
32/// over bare `int` givens would materialise Cartesian products of
33/// `OXIDE_INT_MIN..OXIDE_INT_MAX` via `GroundDomain::apply_i32` during parse
34/// (e.g. BIBD `letting b be (l*v*(v-1))/(k*(k-1))`).
35fn value_letting_domain(expr: &Expression) -> Option<DomainPtr> {
36    match expr.return_type() {
37        ReturnType::Bool => Some(Domain::bool()),
38        ReturnType::Int => {
39            if let Some(Literal::Int(value)) = eval_constant(expr) {
40                return Some(Domain::int(vec![Range::Single(value)]));
41            }
42            IntVal::new_expr(Moo::new(expr.clone()))
43                .ok()
44                .map(|value| Domain::int(vec![Range::Single(value)]))
45        }
46        _ => expr.domain_of(),
47    }
48}
49
50/// Parse a letting statement into a SymbolTable containing the declared symbols
51pub fn parse_letting_statement(
52    ctx: &mut ParseContext,
53    letting_statement: Node,
54) -> Result<Option<SymbolTable>, FatalParseError> {
55    let Some(keyword) = field!(recover, ctx, letting_statement, "letting_keyword") else {
56        return Ok(None);
57    };
58    span_with_hover(
59        &keyword,
60        ctx.source_code,
61        ctx.source_map,
62        HoverInfo {
63            description: "Letting keyword".to_string(),
64            doc_key: None,
65            kind: Some(SymbolKind::Letting),
66            ty: None,
67            decl_span: None,
68        },
69    );
70
71    let mut symbol_table = SymbolTable::new();
72
73    for variable_decl in named_children(&letting_statement) {
74        let mut temp_symbols = BTreeSet::new();
75
76        let Some(variable_list) = field!(recover, ctx, variable_decl, "variable_list") else {
77            return Ok(None);
78        };
79        for variable in named_children(&variable_list) {
80            let variable_name = &ctx.source_code[variable.start_byte()..variable.end_byte()];
81
82            if is_keyword_identifier(variable_name) {
83                ctx.errors.push(RecoverableParseError::new(
84                    format!("Keyword '{variable_name}' used as identifier"),
85                    Some(variable.range()),
86                ));
87                // still add variable to symbol table to avoid follow-up errors
88            }
89
90            // Check for duplicate within the same statement
91            if temp_symbols.contains(variable_name) {
92                ctx.errors.push(RecoverableParseError::new(
93                    format!(
94                        "Variable '{}' is already declared in this letting statement",
95                        variable_name
96                    ),
97                    Some(variable.range()),
98                ));
99                // don't return here, as we can still add the other variables to the symbol table
100                continue;
101            }
102
103            // Check for duplicate declaration across statements
104            let name = Name::user(variable_name);
105            if let Some(symbols) = &ctx.symbols
106                && symbols.read().lookup(&name).is_some()
107            {
108                let previous_line = ctx.lookup_decl_line(&name);
109                ctx.errors.push(RecoverableParseError::new(
110                    match previous_line {
111                        Some(line) => format!(
112                            "Variable '{}' is already declared in a previous statement on line {}",
113                            variable_name, line
114                        ),
115                        None => format!(
116                            "Variable '{}' is already declared in a previous statement",
117                            variable_name
118                        ),
119                    },
120                    Some(variable.range()),
121                ));
122                // don't return here, as we can still add the other variables to the symbol table
123                continue;
124            }
125
126            temp_symbols.insert(variable_name);
127            let hover = HoverInfo {
128                description: format!("Letting variable: {variable_name}"),
129                doc_key: None,
130                kind: Some(SymbolKind::LettingVar),
131                ty: None,
132                decl_span: None,
133            };
134            let span_id = span_with_hover(&variable, ctx.source_code, ctx.source_map, hover);
135            ctx.save_decl_span(name, span_id);
136        }
137
138        let Some(expr_or_domain) = field!(recover, ctx, variable_decl, "expr_or_domain") else {
139            return Ok(None);
140        };
141
142        if variable_decl.child_by_field_name("domain").is_some() {
143            for name in temp_symbols {
144                let Some(domain) = parse_domain(ctx, expr_or_domain)? else {
145                    continue;
146                };
147
148                symbol_table.insert(DeclarationPtr::new_domain_letting(Name::user(name), domain));
149            }
150        } else {
151            for name in temp_symbols {
152                let Some(expr) = parse_expression(ctx, expr_or_domain)? else {
153                    continue;
154                };
155                let declaration = match value_letting_domain(&expr) {
156                    Some(domain) => DeclarationPtr::new_value_letting_with_domain(
157                        Name::user(name),
158                        expr,
159                        domain,
160                    ),
161                    None => DeclarationPtr::new_value_letting(Name::user(name), expr),
162                };
163                symbol_table.insert(declaration);
164            }
165        }
166    }
167
168    Ok(Some(symbol_table))
169}
170
171#[cfg(test)]
172mod tests {
173    use super::*;
174    use crate::parser::parse_model::parse_essence;
175    use conjure_cp_core::ast::{DeclarationKind, Name};
176    use std::ops::Deref;
177    use std::time::{Duration, Instant};
178
179    /// Arithmetic lettings over bare `int` givens must use a symbolic singleton domain and
180    /// finish parsing quickly (not enumerate the full Oxide integer range).
181    #[test]
182    fn arithmetic_letting_over_bare_int_givens_uses_symbolic_domain() {
183        let src = r#"
184language ESSENCE' 1.0
185given v, k, l : int
186letting b be (l*v*(v-1))/(k*(k-1))
187find x: bool
188such that x
189"#;
190        let started = Instant::now();
191        let (model, _) = parse_essence(src).expect("model should parse");
192        assert!(
193            started.elapsed() < Duration::from_secs(2),
194            "parse hung for {:?}; eager domain_of over bare int is likely back",
195            started.elapsed()
196        );
197
198        let symbols = model.symbols();
199        let decl = symbols
200            .lookup(&Name::user("b"))
201            .expect("letting b should be in the symbol table");
202        match decl.kind().deref() {
203            DeclarationKind::ValueLetting(_, Some(domain)) => {
204                let ranges = domain.as_int().expect("letting b domain should be int");
205                assert_eq!(
206                    ranges.len(),
207                    1,
208                    "expected a singleton domain, got {ranges:?}"
209                );
210                assert!(
211                    matches!(&ranges[0], Range::Single(IntVal::Expr(_))),
212                    "expected symbolic IntVal::Expr singleton, got {:?}",
213                    ranges[0]
214                );
215            }
216            other => panic!("expected ValueLetting with retained domain, got {other:?}"),
217        }
218    }
219
220    /// Constant integer lettings must keep a ground singleton so dependent domains stay tight.
221    #[test]
222    fn constant_int_letting_keeps_ground_singleton_domain() {
223        let src = r#"
224language ESSENCE' 1.0
225letting n be 3
226find x: int(1..10**n)
227such that x = 1
228"#;
229        let (model, _) = parse_essence(src).expect("model should parse");
230        let symbols = model.symbols();
231        let decl = symbols
232            .lookup(&Name::user("n"))
233            .expect("letting n should be in the symbol table");
234        match decl.kind().deref() {
235            DeclarationKind::ValueLetting(_, Some(domain)) => {
236                let ranges = domain.as_int().expect("letting n domain should be int");
237                assert_eq!(
238                    ranges.len(),
239                    1,
240                    "expected a singleton domain, got {ranges:?}"
241                );
242                assert!(
243                    matches!(&ranges[0], Range::Single(IntVal::Const(3))),
244                    "expected ground IntVal::Const(3) singleton, got {:?}",
245                    ranges[0]
246                );
247            }
248            other => panic!("expected ValueLetting with retained domain, got {other:?}"),
249        }
250    }
251}
conjure_cp_essence_parser/parser/letting.rs

conjure_cp_essence_parser/parser/
letting.rs
