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
6311
pub fn parse_expression(
14
6311
    ctx: &mut ParseContext,
15
6311
    node: Node,
16
6311
) -> Result<Option<Expression>, FatalParseError> {
17
6311
    match node.kind() {
18
6311
        "atom" => parse_atom(ctx, &node),
19
1835
        "bool_expr" => parse_boolean_expression(ctx, &node),
20
1284
        "arithmetic_expr" => parse_arithmetic_expression(ctx, &node),
21
943
        "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
6311
}
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
341
fn parse_arithmetic_expression(
64
341
    ctx: &mut ParseContext,
65
341
    node: &Node,
66
341
) -> Result<Option<Expression>, FatalParseError> {
67
341
    ctx.typechecking_context = TypecheckingContext::Arithmetic;
68
341
    let inner = named_child!(node);
69
341
    match inner.kind() {
70
341
        "atom" => parse_atom(ctx, &inner),
71
341
        "negative_expr" | "abs_value" | "sub_arith_expr" | "toInt_expr" => {
72
88
            parse_unary_expression(ctx, &inner)
73
        }
74
253
        "exponent" | "product_expr" | "sum_expr" => parse_binary_expression(ctx, &inner),
75
22
        "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
341
}
83

            
84
943
fn parse_comparison_expression(
85
943
    ctx: &mut ParseContext,
86
943
    node: &Node,
87
943
) -> Result<Option<Expression>, FatalParseError> {
88
943
    let inner = named_child!(node);
89
943
    match inner.kind() {
90
943
        "arithmetic_comparison" => {
91
            // Arithmetic comparisons require arithmetic operands
92
168
            ctx.typechecking_context = TypecheckingContext::Arithmetic;
93
168
            parse_binary_expression(ctx, &inner)
94
        }
95
775
        "equality_comparison" => {
96
            // Equality works on any type
97
            // TODO: add type checking to ensure both sides have the same type
98
445
            ctx.typechecking_context = TypecheckingContext::Unknown;
99
445
            parse_binary_expression(ctx, &inner)
100
        }
101
330
        "set_comparison" => {
102
            // Set comparisons require set operands (no specific type checking for now)
103
            // TODO: add typechecking for sets
104
330
            ctx.typechecking_context = TypecheckingContext::Unknown;
105
330
            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
943
}
113

            
114
551
fn parse_boolean_expression(
115
551
    ctx: &mut ParseContext,
116
551
    node: &Node,
117
551
) -> Result<Option<Expression>, FatalParseError> {
118
551
    ctx.typechecking_context = TypecheckingContext::Boolean;
119
551
    let inner = named_child!(node);
120
551
    match inner.kind() {
121
551
        "atom" => parse_atom(ctx, &inner),
122
551
        "not_expr" | "sub_bool_expr" => parse_unary_expression(ctx, &inner),
123
199
        "and_expr" | "or_expr" | "implication" | "iff_expr" => parse_binary_expression(ctx, &inner),
124
45
        "list_combining_expr_bool" => parse_list_combining_expression(ctx, &inner),
125
22
        "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
551
}
132

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

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

            
144
23
    match operator_str {
145
23
        "and" => Ok(Some(Expression::And(Metadata::new(), Moo::new(inner)))),
146
12
        "or" => Ok(Some(Expression::Or(Metadata::new(), Moo::new(inner)))),
147
12
        "sum" => Ok(Some(Expression::Sum(Metadata::new(), Moo::new(inner)))),
148
1
        "product" => Ok(Some(Expression::Product(Metadata::new(), Moo::new(inner)))),
149
1
        "min" => Ok(Some(Expression::Min(Metadata::new(), Moo::new(inner)))),
150
1
        "max" => Ok(Some(Expression::Max(Metadata::new(), Moo::new(inner)))),
151
1
        "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
45
}
158

            
159
440
fn parse_unary_expression(
160
440
    ctx: &mut ParseContext,
161
440
    node: &Node,
162
440
) -> Result<Option<Expression>, FatalParseError> {
163
440
    let Some(inner) = parse_expression(ctx, field!(node, "expression"))? else {
164
        return Ok(None);
165
    };
166
440
    match node.kind() {
167
440
        "negative_expr" => Ok(Some(Expression::Neg(Metadata::new(), Moo::new(inner)))),
168
418
        "abs_value" => Ok(Some(Expression::Abs(Metadata::new(), Moo::new(inner)))),
169
407
        "not_expr" => Ok(Some(Expression::Not(Metadata::new(), Moo::new(inner)))),
170
319
        "toInt_expr" => Ok(Some(Expression::ToInt(Metadata::new(), Moo::new(inner)))),
171
297
        "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
440
}
178

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

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

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

            
195
1251
    let mut description = format!("Operator '{op_str}'");
196
1251
    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
1251
        "+" => Ok(Some(Expression::Sum(
202
128
            Metadata::new(),
203
128
            Moo::new(matrix_expr![left, right; domain_int!(1..)]),
204
128
        ))),
205
1123
        "-" => Ok(Some(Expression::Minus(
206
44
            Metadata::new(),
207
44
            Moo::new(left),
208
44
            Moo::new(right),
209
44
        ))),
210
1079
        "*" => Ok(Some(Expression::Product(
211
33
            Metadata::new(),
212
33
            Moo::new(matrix_expr![left, right; domain_int!(1..)]),
213
33
        ))),
214
1046
        "/\\" => Ok(Some(Expression::And(
215
44
            Metadata::new(),
216
44
            Moo::new(matrix_expr![left, right; domain_int!(1..)]),
217
44
        ))),
218
1002
        "\\/" => Ok(Some(Expression::Or(
219
11
            Metadata::new(),
220
11
            Moo::new(matrix_expr![left, right; domain_int!(1..)]),
221
11
        ))),
222
991
        "**" => Ok(Some(Expression::UnsafePow(
223
            Metadata::new(),
224
            Moo::new(left),
225
            Moo::new(right),
226
        ))),
227
991
        "/" => {
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
987
        "%" => {
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
987
        "=" => Ok(Some(Expression::Eq(
244
346
            Metadata::new(),
245
346
            Moo::new(left),
246
346
            Moo::new(right),
247
346
        ))),
248
641
        "!=" => Ok(Some(Expression::Neq(
249
44
            Metadata::new(),
250
44
            Moo::new(left),
251
44
            Moo::new(right),
252
44
        ))),
253
597
        "<=" => Ok(Some(Expression::Leq(
254
44
            Metadata::new(),
255
44
            Moo::new(left),
256
44
            Moo::new(right),
257
44
        ))),
258
553
        ">=" => Ok(Some(Expression::Geq(
259
35
            Metadata::new(),
260
35
            Moo::new(left),
261
35
            Moo::new(right),
262
35
        ))),
263
518
        "<" => Ok(Some(Expression::Lt(
264
12
            Metadata::new(),
265
12
            Moo::new(left),
266
12
            Moo::new(right),
267
12
        ))),
268
506
        ">" => Ok(Some(Expression::Gt(
269
44
            Metadata::new(),
270
44
            Moo::new(left),
271
44
            Moo::new(right),
272
44
        ))),
273
462
        "->" => Ok(Some(Expression::Imply(
274
55
            Metadata::new(),
275
55
            Moo::new(left),
276
55
            Moo::new(right),
277
55
        ))),
278
407
        "<->" => Ok(Some(Expression::Iff(
279
11
            Metadata::new(),
280
11
            Moo::new(left),
281
11
            Moo::new(right),
282
11
        ))),
283
396
        "<lex" => Ok(Some(Expression::LexLt(
284
            Metadata::new(),
285
            Moo::new(left),
286
            Moo::new(right),
287
        ))),
288
396
        ">lex" => Ok(Some(Expression::LexGt(
289
            Metadata::new(),
290
            Moo::new(left),
291
            Moo::new(right),
292
        ))),
293
396
        "<=lex" => Ok(Some(Expression::LexLeq(
294
            Metadata::new(),
295
            Moo::new(left),
296
            Moo::new(right),
297
        ))),
298
396
        ">=lex" => Ok(Some(Expression::LexGeq(
299
            Metadata::new(),
300
            Moo::new(left),
301
            Moo::new(right),
302
        ))),
303
396
        "in" => Ok(Some(Expression::In(
304
143
            Metadata::new(),
305
143
            Moo::new(left),
306
143
            Moo::new(right),
307
143
        ))),
308
253
        "subset" => Ok(Some(Expression::Subset(
309
55
            Metadata::new(),
310
55
            Moo::new(left),
311
55
            Moo::new(right),
312
55
        ))),
313
198
        "subsetEq" => Ok(Some(Expression::SubsetEq(
314
44
            Metadata::new(),
315
44
            Moo::new(left),
316
44
            Moo::new(right),
317
44
        ))),
318
154
        "supset" => Ok(Some(Expression::Supset(
319
44
            Metadata::new(),
320
44
            Moo::new(left),
321
44
            Moo::new(right),
322
44
        ))),
323
110
        "supsetEq" => Ok(Some(Expression::SupsetEq(
324
44
            Metadata::new(),
325
44
            Moo::new(left),
326
44
            Moo::new(right),
327
44
        ))),
328
66
        "union" => {
329
33
            description = "set union: combines the elements from both operands".to_string();
330
33
            Ok(Some(Expression::Union(
331
33
                Metadata::new(),
332
33
                Moo::new(left),
333
33
                Moo::new(right),
334
33
            )))
335
        }
336
33
        "intersect" => {
337
33
            description =
338
33
                "set intersection: keeps only elements common to both operands".to_string();
339
33
            Ok(Some(Expression::Intersect(
340
33
                Metadata::new(),
341
33
                Moo::new(left),
342
33
                Moo::new(right),
343
33
            )))
344
        }
345
        _ => Err(FatalParseError::internal_error(
346
            format!("Invalid operator: '{op_str}'"),
347
            Some(op_node.range()),
348
        )),
349
    };
350

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

            
361
1251
    expr
362
1394
}