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

conjure_cp_essence_parser/parser/
letting.rs
