1
use crate::diagnostics::diagnostics_api::SymbolKind;
2
use crate::diagnostics::source_map::{HoverInfo, span_with_hover};
3
use crate::errors::FatalParseError;
4
use crate::parser::ParseContext;
5
use crate::parser::atom::parse_atom;
6
use crate::parser::comprehension::parse_quantifier_or_aggregate_expr;
7
use crate::util::TypecheckingContext;
8
use crate::{field, named_child};
9
use conjure_cp_core::ast::{Expression, Metadata, Moo};
10
use conjure_cp_core::{domain_int, matrix_expr, range};
11
use tree_sitter::Node;
12

            
13
9773
pub fn parse_expression(
14
9773
    ctx: &mut ParseContext,
15
9773
    node: Node,
16
9773
) -> Result<Option<Expression>, FatalParseError> {
17
9773
    match node.kind() {
18
9773
        "atom" => parse_atom(ctx, &node),
19
2440
        "bool_expr" => parse_boolean_expression(ctx, &node),
20
1794
        "arithmetic_expr" => parse_arithmetic_expression(ctx, &node),
21
1380
        "comparison_expr" => parse_comparison_expression(ctx, &node),
22
        "dominance_relation" => parse_dominance_relation(ctx, &node),
23
        _ => Err(FatalParseError::internal_error(
24
            format!("Unexpected expression type: '{}'", node.kind()),
25
            Some(node.range()),
26
        )),
27
    }
28
9773
}
29

            
30
fn parse_dominance_relation(
31
    ctx: &mut ParseContext,
32
    node: &Node,
33
) -> Result<Option<Expression>, FatalParseError> {
34
    if ctx.root.kind() == "dominance_relation" {
35
        return Err(FatalParseError::internal_error(
36
            "Nested dominance relations are not allowed".to_string(),
37
            Some(node.range()),
38
        ));
39
    }
40

            
41
    // NB: In all other cases, we keep the root the same;
42
    // However, here we create a new context with the new root so downstream functions
43
    // know we are inside a dominance relation
44
    let mut inner_ctx = ParseContext {
45
        source_code: ctx.source_code,
46
        root: node,
47
        symbols: ctx.symbols.clone(),
48
        errors: ctx.errors,
49
        source_map: &mut *ctx.source_map,
50
        typechecking_context: ctx.typechecking_context,
51
    };
52

            
53
    let Some(inner) = parse_expression(&mut inner_ctx, field!(node, "expression"))? else {
54
        return Ok(None);
55
    };
56

            
57
    Ok(Some(Expression::DominanceRelation(
58
        Metadata::new(),
59
        Moo::new(inner),
60
    )))
61
}
62

            
63
414
fn parse_arithmetic_expression(
64
414
    ctx: &mut ParseContext,
65
414
    node: &Node,
66
414
) -> Result<Option<Expression>, FatalParseError> {
67
414
    ctx.typechecking_context = TypecheckingContext::Arithmetic;
68
414
    let inner = named_child!(node);
69
414
    match inner.kind() {
70
414
        "atom" => parse_atom(ctx, &inner),
71
414
        "negative_expr" | "abs_value" | "sub_arith_expr" | "toInt_expr" => {
72
85
            parse_unary_expression(ctx, &inner)
73
        }
74
329
        "exponent" | "product_expr" | "sum_expr" => parse_binary_expression(ctx, &inner),
75
20
        "list_combining_expr_arith" => parse_list_combining_expression(ctx, &inner),
76
        "aggregate_expr" => parse_quantifier_or_aggregate_expr(ctx, &inner),
77
        _ => Err(FatalParseError::internal_error(
78
            format!("Expected arithmetic expression, found: {}", inner.kind()),
79
            Some(inner.range()),
80
        )),
81
    }
82
414
}
83

            
84
1380
fn parse_comparison_expression(
85
1380
    ctx: &mut ParseContext,
86
1380
    node: &Node,
87
1380
) -> Result<Option<Expression>, FatalParseError> {
88
1380
    let inner = named_child!(node);
89
1380
    match inner.kind() {
90
1380
        "arithmetic_comparison" => {
91
            // Arithmetic comparisons require arithmetic operands
92
166
            ctx.typechecking_context = TypecheckingContext::Arithmetic;
93
166
            parse_binary_expression(ctx, &inner)
94
        }
95
1214
        "equality_comparison" => {
96
            // Equality works on any type
97
            // TODO: add type checking to ensure both sides have the same type
98
658
            ctx.typechecking_context = TypecheckingContext::Unknown;
99
658
            parse_binary_expression(ctx, &inner)
100
        }
101
556
        "set_comparison" => {
102
            // Set comparisons require set operands (no specific type checking for now)
103
            // TODO: add typechecking for sets
104
556
            ctx.typechecking_context = TypecheckingContext::Unknown;
105
556
            parse_binary_expression(ctx, &inner)
106
        }
107
        _ => Err(FatalParseError::internal_error(
108
            format!("Expected comparison expression, found '{}'", inner.kind()),
109
            Some(inner.range()),
110
        )),
111
    }
112
1380
}
113

            
114
646
fn parse_boolean_expression(
115
646
    ctx: &mut ParseContext,
116
646
    node: &Node,
117
646
) -> Result<Option<Expression>, FatalParseError> {
118
646
    ctx.typechecking_context = TypecheckingContext::Boolean;
119
646
    let inner = named_child!(node);
120
646
    match inner.kind() {
121
646
        "atom" => parse_atom(ctx, &inner),
122
646
        "not_expr" | "sub_bool_expr" => parse_unary_expression(ctx, &inner),
123
198
        "and_expr" | "or_expr" | "implication" | "iff_expr" => parse_binary_expression(ctx, &inner),
124
66
        "list_combining_expr_bool" => parse_list_combining_expression(ctx, &inner),
125
44
        "quantifier_expr" => parse_quantifier_or_aggregate_expr(ctx, &inner),
126
        _ => Err(FatalParseError::internal_error(
127
            format!("Expected boolean expression, found '{}'", inner.kind()),
128
            Some(inner.range()),
129
        )),
130
    }
131
646
}
132

            
133
42
fn parse_list_combining_expression(
134
42
    ctx: &mut ParseContext,
135
42
    node: &Node,
136
42
) -> Result<Option<Expression>, FatalParseError> {
137
42
    let operator_node = field!(node, "operator");
138
42
    let operator_str = &ctx.source_code[operator_node.start_byte()..operator_node.end_byte()];
139

            
140
42
    let Some(inner) = parse_atom(ctx, &field!(node, "arg"))? else {
141
22
        return Ok(None);
142
    };
143

            
144
20
    match operator_str {
145
20
        "and" => Ok(Some(Expression::And(Metadata::new(), Moo::new(inner)))),
146
11
        "or" => Ok(Some(Expression::Or(Metadata::new(), Moo::new(inner)))),
147
11
        "sum" => Ok(Some(Expression::Sum(Metadata::new(), Moo::new(inner)))),
148
2
        "product" => Ok(Some(Expression::Product(Metadata::new(), Moo::new(inner)))),
149
2
        "min" => Ok(Some(Expression::Min(Metadata::new(), Moo::new(inner)))),
150
2
        "max" => Ok(Some(Expression::Max(Metadata::new(), Moo::new(inner)))),
151
2
        "allDiff" => Ok(Some(Expression::AllDiff(Metadata::new(), Moo::new(inner)))),
152
        _ => Err(FatalParseError::internal_error(
153
            format!("Invalid operator: '{operator_str}'"),
154
            Some(operator_node.range()),
155
        )),
156
    }
157
42
}
158

            
159
533
fn parse_unary_expression(
160
533
    ctx: &mut ParseContext,
161
533
    node: &Node,
162
533
) -> Result<Option<Expression>, FatalParseError> {
163
533
    let Some(inner) = parse_expression(ctx, field!(node, "expression"))? else {
164
        return Ok(None);
165
    };
166
533
    match node.kind() {
167
533
        "negative_expr" => Ok(Some(Expression::Neg(Metadata::new(), Moo::new(inner)))),
168
515
        "abs_value" => Ok(Some(Expression::Abs(Metadata::new(), Moo::new(inner)))),
169
493
        "not_expr" => Ok(Some(Expression::Not(Metadata::new(), Moo::new(inner)))),
170
421
        "toInt_expr" => Ok(Some(Expression::ToInt(Metadata::new(), Moo::new(inner)))),
171
403
        "sub_bool_expr" | "sub_arith_expr" => Ok(Some(inner)),
172
        _ => Err(FatalParseError::internal_error(
173
            format!("Unrecognised unary operation: '{}'", node.kind()),
174
            Some(node.range()),
175
        )),
176
    }
177
533
}
178

            
179
1953
pub fn parse_binary_expression(
180
1953
    ctx: &mut ParseContext,
181
1953
    node: &Node,
182
1953
) -> Result<Option<Expression>, FatalParseError> {
183
3807
    let mut parse_subexpr = |expr: Node| parse_expression(ctx, expr);
184

            
185
1953
    let Some(left) = parse_subexpr(field!(node, "left"))? else {
186
99
        return Ok(None);
187
    };
188
1854
    let Some(right) = parse_subexpr(field!(node, "right"))? else {
189
66
        return Ok(None);
190
    };
191

            
192
1788
    let op_node = field!(node, "operator");
193
1788
    let op_str = &ctx.source_code[op_node.start_byte()..op_node.end_byte()];
194

            
195
1788
    let mut description = format!("Operator '{op_str}'");
196
1788
    let expr = match op_str {
197
        // NB: We are deliberately setting the index domain to 1.., not 1..2.
198
        // Semantically, this means "a list that can grow/shrink arbitrarily".
199
        // This is expected by rules which will modify the terms of the sum expression
200
        // (e.g. by partially evaluating them).
201
1788
        "+" => Ok(Some(Expression::Sum(
202
194
            Metadata::new(),
203
194
            Moo::new(matrix_expr![left, right; domain_int!(1..)]),
204
194
        ))),
205
1594
        "-" => Ok(Some(Expression::Minus(
206
62
            Metadata::new(),
207
62
            Moo::new(left),
208
62
            Moo::new(right),
209
62
        ))),
210
1532
        "*" => Ok(Some(Expression::Product(
211
27
            Metadata::new(),
212
27
            Moo::new(matrix_expr![left, right; domain_int!(1..)]),
213
27
        ))),
214
1505
        "/\\" => Ok(Some(Expression::And(
215
36
            Metadata::new(),
216
36
            Moo::new(matrix_expr![left, right; domain_int!(1..)]),
217
36
        ))),
218
1469
        "\\/" => Ok(Some(Expression::Or(
219
9
            Metadata::new(),
220
9
            Moo::new(matrix_expr![left, right; domain_int!(1..)]),
221
9
        ))),
222
1460
        "**" => Ok(Some(Expression::UnsafePow(
223
            Metadata::new(),
224
            Moo::new(left),
225
            Moo::new(right),
226
        ))),
227
1460
        "/" => {
228
            //TODO: add checks for if division is safe or not
229
4
            Ok(Some(Expression::UnsafeDiv(
230
4
                Metadata::new(),
231
4
                Moo::new(left),
232
4
                Moo::new(right),
233
4
            )))
234
        }
235
1456
        "%" => {
236
            //TODO: add checks for if mod is safe or not
237
            Ok(Some(Expression::UnsafeMod(
238
                Metadata::new(),
239
                Moo::new(left),
240
                Moo::new(right),
241
            )))
242
        }
243
1456
        "=" => Ok(Some(Expression::Eq(
244
541
            Metadata::new(),
245
541
            Moo::new(left),
246
541
            Moo::new(right),
247
541
        ))),
248
915
        "!=" => Ok(Some(Expression::Neq(
249
40
            Metadata::new(),
250
40
            Moo::new(left),
251
40
            Moo::new(right),
252
40
        ))),
253
875
        "<=" => Ok(Some(Expression::Leq(
254
36
            Metadata::new(),
255
36
            Moo::new(left),
256
36
            Moo::new(right),
257
36
        ))),
258
839
        ">=" => Ok(Some(Expression::Geq(
259
31
            Metadata::new(),
260
31
            Moo::new(left),
261
31
            Moo::new(right),
262
31
        ))),
263
808
        "<" => Ok(Some(Expression::Lt(
264
11
            Metadata::new(),
265
11
            Moo::new(left),
266
11
            Moo::new(right),
267
11
        ))),
268
797
        ">" => Ok(Some(Expression::Gt(
269
55
            Metadata::new(),
270
55
            Moo::new(left),
271
55
            Moo::new(right),
272
55
        ))),
273
742
        "->" => Ok(Some(Expression::Imply(
274
45
            Metadata::new(),
275
45
            Moo::new(left),
276
45
            Moo::new(right),
277
45
        ))),
278
697
        "<->" => Ok(Some(Expression::Iff(
279
9
            Metadata::new(),
280
9
            Moo::new(left),
281
9
            Moo::new(right),
282
9
        ))),
283
688
        "<lex" => Ok(Some(Expression::LexLt(
284
            Metadata::new(),
285
            Moo::new(left),
286
            Moo::new(right),
287
        ))),
288
688
        ">lex" => Ok(Some(Expression::LexGt(
289
            Metadata::new(),
290
            Moo::new(left),
291
            Moo::new(right),
292
        ))),
293
688
        "<=lex" => Ok(Some(Expression::LexLeq(
294
            Metadata::new(),
295
            Moo::new(left),
296
            Moo::new(right),
297
        ))),
298
688
        ">=lex" => Ok(Some(Expression::LexGeq(
299
            Metadata::new(),
300
            Moo::new(left),
301
            Moo::new(right),
302
        ))),
303
688
        "in" => Ok(Some(Expression::In(
304
182
            Metadata::new(),
305
182
            Moo::new(left),
306
182
            Moo::new(right),
307
182
        ))),
308
506
        "subset" => Ok(Some(Expression::Subset(
309
110
            Metadata::new(),
310
110
            Moo::new(left),
311
110
            Moo::new(right),
312
110
        ))),
313
396
        "subsetEq" => Ok(Some(Expression::SubsetEq(
314
88
            Metadata::new(),
315
88
            Moo::new(left),
316
88
            Moo::new(right),
317
88
        ))),
318
308
        "supset" => Ok(Some(Expression::Supset(
319
88
            Metadata::new(),
320
88
            Moo::new(left),
321
88
            Moo::new(right),
322
88
        ))),
323
220
        "supsetEq" => Ok(Some(Expression::SupsetEq(
324
88
            Metadata::new(),
325
88
            Moo::new(left),
326
88
            Moo::new(right),
327
88
        ))),
328
132
        "union" => {
329
66
            description = "set union: combines the elements from both operands".to_string();
330
66
            Ok(Some(Expression::Union(
331
66
                Metadata::new(),
332
66
                Moo::new(left),
333
66
                Moo::new(right),
334
66
            )))
335
        }
336
66
        "intersect" => {
337
66
            description =
338
66
                "set intersection: keeps only elements common to both operands".to_string();
339
66
            Ok(Some(Expression::Intersect(
340
66
                Metadata::new(),
341
66
                Moo::new(left),
342
66
                Moo::new(right),
343
66
            )))
344
        }
345
        _ => Err(FatalParseError::internal_error(
346
            format!("Invalid operator: '{op_str}'"),
347
            Some(op_node.range()),
348
        )),
349
    };
350

            
351
1788
    if expr.is_ok() {
352
1788
        let hover = HoverInfo {
353
1788
            description,
354
1788
            kind: Some(SymbolKind::Function),
355
1788
            ty: None,
356
1788
            decl_span: None,
357
1788
        };
358
1788
        span_with_hover(&op_node, ctx.source_code, ctx.source_map, hover);
359
1788
    }
360

            
361
1788
    expr
362
1953
}