Skip to main content

conjure_cp_core/parse/
parse_model.rs

1#![allow(clippy::unwrap_used)]
2#![allow(clippy::expect_used)]
3use std::cell::RefCell;
4use std::collections::HashMap;
5use std::rc::Rc;
6use std::sync::{Arc, RwLock};
7use ustr::Ustr;
8
9use serde_json::Map as JsonMap;
10use serde_json::Value;
11use serde_json::Value as JsonValue;
12
13use crate::ast::abstract_comprehension::AbstractComprehensionBuilder;
14use crate::ast::ac_operators::ACOperatorKind;
15use crate::ast::comprehension::ComprehensionBuilder;
16use crate::ast::records::RecordValue;
17use crate::ast::{
18    AbstractLiteral, Atom, DeclarationPtr, Domain, Expression, FuncAttr, IntVal, JectivityAttr,
19    Literal, Name, PartialityAttr, Range, RecordEntry, SetAttr, SymbolTable,
20};
21use crate::ast::{DeclarationKind, Moo};
22use crate::ast::{DomainPtr, Metadata};
23use crate::context::Context;
24use crate::error::{Error, Result};
25use crate::{Model, bug, error, into_matrix_expr, throw_error};
26
27#[allow(unused_macros)]
28macro_rules! parser_trace {
29    ($($arg:tt)+) => {
30        log::trace!(target:"jsonparser",$($arg)+)
31    };
32}
33
34#[allow(unused_macros)]
35macro_rules! parser_debug {
36    ($($arg:tt)+) => {
37        log::debug!(target:"jsonparser",$($arg)+)
38    };
39}
40
41pub fn model_from_json(str: &str, context: Arc<RwLock<Context<'static>>>) -> Result<Model> {
42    let mut m = Model::new(context);
43    let v: JsonValue = serde_json::from_str(str)?;
44    let statements = v["mStatements"]
45        .as_array()
46        .ok_or(error!("mStatements is not an array"))?;
47
48    for statement in statements {
49        let entry = statement
50            .as_object()
51            .ok_or(error!("mStatements contains a non-object"))?
52            .iter()
53            .next()
54            .ok_or(error!("mStatements contains an empty object"))?;
55
56        match entry.0.as_str() {
57            "Declaration" => {
58                let decl = entry
59                    .1
60                    .as_object()
61                    .ok_or(error!("Declaration is not an object".to_owned()))?;
62
63                // One field in the declaration should tell us what kind it is.
64                //
65                // Find it, ignoring the other fields.
66                //
67                // e.g. FindOrGiven,
68
69                let mut valid_decl: bool = false;
70                let scope = m.as_submodel().symbols_ptr_unchecked().clone();
71                let submodel = m.as_submodel_mut();
72                for (kind, value) in decl {
73                    match kind.as_str() {
74                        "FindOrGiven" => {
75                            parse_variable(value, &mut submodel.symbols_mut())?;
76                            valid_decl = true;
77                            break;
78                        }
79                        "Letting" => {
80                            parse_letting(value, &scope)?;
81                            valid_decl = true;
82                            break;
83                        }
84                        _ => continue,
85                    }
86                }
87
88                if !valid_decl {
89                    throw_error!("Declaration is not a valid kind")?;
90                }
91            }
92            "SuchThat" => {
93                let constraints_arr = match entry.1.as_array() {
94                    Some(x) => x,
95                    None => bug!("SuchThat is not a vector"),
96                };
97
98                let constraints: Vec<Expression> = constraints_arr
99                    .iter()
100                    .map(|x| {
101                        parse_expression(x, m.as_submodel_mut().symbols_ptr_unchecked()).unwrap()
102                    })
103                    .collect();
104                m.as_submodel_mut().add_constraints(constraints);
105                // println!("Nb constraints {}", m.constraints.len());
106            }
107            otherwise => bug!("Unhandled Statement {:#?}", otherwise),
108        }
109    }
110    Ok(m)
111}
112
113fn parse_variable(v: &JsonValue, symtab: &mut SymbolTable) -> Result<()> {
114    let arr = v.as_array().ok_or(error!("FindOrGiven is not an array"))?;
115    let name = arr[1]
116        .as_object()
117        .ok_or(error!("FindOrGiven[1] is not an object"))?["Name"]
118        .as_str()
119        .ok_or(error!("FindOrGiven[1].Name is not a string"))?;
120
121    let name = Name::User(Ustr::from(name));
122
123    let domain = arr[2]
124        .as_object()
125        .ok_or(error!("FindOrGiven[2] is not an object"))?
126        .iter()
127        .next()
128        .ok_or(error!("FindOrGiven[2] is an empty object"))?;
129
130    let domain = parse_domain(domain.0, domain.1, symtab)?;
131
132    symtab
133        .insert(DeclarationPtr::new_var(name.clone(), domain))
134        .ok_or(Error::Parse(format!(
135            "Could not add {name} to symbol table as it already exists"
136        )))
137}
138
139fn parse_letting(v: &JsonValue, scope: &Rc<RefCell<SymbolTable>>) -> Result<()> {
140    let arr = v.as_array().ok_or(error!("Letting is not an array"))?;
141    let name = arr[0]
142        .as_object()
143        .ok_or(error!("Letting[0] is not an object"))?["Name"]
144        .as_str()
145        .ok_or(error!("Letting[0].Name is not a string"))?;
146    let name = Name::User(Ustr::from(name));
147    // value letting
148    if let Some(value) = parse_expression(&arr[1], scope) {
149        let mut symtab = scope.borrow_mut();
150        symtab
151            .insert(DeclarationPtr::new_value_letting(name.clone(), value))
152            .ok_or(Error::Parse(format!(
153                "Could not add {name} to symbol table as it already exists"
154            )))
155    } else {
156        // domain letting
157        let domain = &arr[1]
158            .as_object()
159            .ok_or(error!("Letting[1] is not an object".to_owned()))?["Domain"]
160            .as_object()
161            .ok_or(error!("Letting[1].Domain is not an object"))?
162            .iter()
163            .next()
164            .ok_or(error!("Letting[1].Domain is an empty object"))?;
165
166        let mut symtab = scope.borrow_mut();
167        let domain = parse_domain(domain.0, domain.1, &mut symtab)?;
168
169        symtab
170            .insert(DeclarationPtr::new_domain_letting(name.clone(), domain))
171            .ok_or(Error::Parse(format!(
172                "Could not add {name} to symbol table as it already exists"
173            )))
174    }
175}
176
177fn parse_domain(
178    domain_name: &str,
179    domain_value: &JsonValue,
180    symbols: &mut SymbolTable,
181) -> Result<DomainPtr> {
182    match domain_name {
183        "DomainInt" => Ok(parse_int_domain(domain_value, symbols)?),
184        "DomainBool" => Ok(Domain::bool()),
185        "DomainReference" => {
186            let name = Name::user(
187                domain_value
188                    .as_array()
189                    .ok_or(error!("DomainReference is not an array"))?[0]
190                    .as_object()
191                    .ok_or(error!("DomainReference[0] is not an object"))?["Name"]
192                    .as_str()
193                    .ok_or(error!("DomainReference[0].Name is not a string"))?,
194            );
195            let ptr = symbols
196                .lookup(&name)
197                .ok_or(error!(format!("Name {name} not found")))?;
198            let dom =
199                Domain::reference(ptr).ok_or(error!("Could not construct reference domain"))?;
200            Ok(dom)
201        }
202        "DomainSet" => {
203            let dom = domain_value.get(2).and_then(|v| v.as_object());
204            let domain_obj = dom.expect("domain object exists");
205            let domain = domain_obj
206                .iter()
207                .next()
208                .ok_or(Error::Parse("DomainSet is an empty object".to_owned()))?;
209            let domain = parse_domain(domain.0.as_str(), domain.1, symbols)?;
210            let size = domain_value
211                .get(1)
212                .and_then(|v| v.as_object())
213                .ok_or(error!("Set size attributes is not an object"))?;
214            let size = parse_size_attr(size, symbols)?;
215            let attr: SetAttr<IntVal> = SetAttr { size };
216            Ok(Domain::set(attr, domain))
217        }
218
219        "DomainMatrix" => {
220            let domain_value = domain_value
221                .as_array()
222                .ok_or(error!("Domain matrix is not an array"))?;
223
224            let indexed_by_domain = domain_value[0].clone();
225            let (index_domain_name, index_domain_value) = indexed_by_domain
226                .as_object()
227                .ok_or(error!("DomainMatrix[0] is not an object"))?
228                .iter()
229                .next()
230                .ok_or(error!(""))?;
231
232            let (value_domain_name, value_domain_value) = domain_value[1]
233                .as_object()
234                .ok_or(error!(""))?
235                .iter()
236                .next()
237                .ok_or(error!(""))?;
238
239            // Conjure stores a 2-d matrix as a matrix of a matrix.
240            //
241            // Therefore, the index is always a Domain.
242
243            let mut index_domains: Vec<DomainPtr> = vec![];
244
245            index_domains.push(parse_domain(
246                index_domain_name,
247                index_domain_value,
248                symbols,
249            )?);
250
251            // We want to store 2-d matrices as a matrix with two index domains, not a matrix in a
252            // matrix.
253            //
254            // Walk through the value domain until it is not a DomainMatrix, adding the index to
255            // our list of indices.
256            let mut value_domain = parse_domain(value_domain_name, value_domain_value, symbols)?;
257            while let Some((new_value_domain, mut indices)) = value_domain.as_matrix() {
258                index_domains.append(&mut indices);
259                value_domain = new_value_domain.clone()
260            }
261
262            Ok(Domain::matrix(value_domain, index_domains))
263        }
264        "DomainTuple" => {
265            let domain_value = domain_value
266                .as_array()
267                .ok_or(error!("Domain tuple is not an array"))?;
268
269            //iterate through the array and parse each domain
270            let domain = domain_value
271                .iter()
272                .map(|x| {
273                    let domain = x
274                        .as_object()
275                        .ok_or(error!("DomainTuple[0] is not an object"))?
276                        .iter()
277                        .next()
278                        .ok_or(error!("DomainTuple[0] is an empty object"))?;
279                    parse_domain(domain.0, domain.1, symbols)
280                })
281                .collect::<Result<Vec<DomainPtr>>>()?;
282
283            Ok(Domain::tuple(domain))
284        }
285        "DomainRecord" => {
286            let domain_value = domain_value
287                .as_array()
288                .ok_or(error!("Domain Record is not a json array"))?;
289
290            let mut record_entries = vec![];
291
292            for item in domain_value {
293                //collect the name of the record field
294                let name = item[0]
295                    .as_object()
296                    .ok_or(error!("FindOrGiven[1] is not an object"))?["Name"]
297                    .as_str()
298                    .ok_or(error!("FindOrGiven[1].Name is not a string"))?;
299
300                let name = Name::User(Ustr::from(name));
301                // then collect the domain of the record field
302                let domain = item[1]
303                    .as_object()
304                    .ok_or(error!("FindOrGiven[2] is not an object"))?
305                    .iter()
306                    .next()
307                    .ok_or(error!("FindOrGiven[2] is an empty object"))?;
308
309                let domain = parse_domain(domain.0, domain.1, symbols)?;
310
311                let rec = RecordEntry { name, domain };
312
313                record_entries.push(rec);
314            }
315
316            // add record fields to symbol table
317            record_entries
318                .iter()
319                .cloned()
320                .map(DeclarationPtr::new_record_field)
321                .for_each(|decl| {
322                    symbols
323                        .insert(decl)
324                        .expect("record field to not already be in the symbol table")
325                });
326
327            Ok(Domain::record(record_entries))
328        }
329        "DomainFunction" => {
330            let domain = domain_value
331                .get(2)
332                .and_then(|v| v.as_object())
333                .ok_or(error!("Function domain is not an object"))?;
334            let domain = domain
335                .iter()
336                .next()
337                .ok_or(Error::Parse("DomainSet is an empty object".to_owned()))?;
338            let domain = parse_domain(domain.0.as_str(), domain.1, symbols)?;
339
340            let codomain = domain_value
341                .get(3)
342                .and_then(|v| v.as_object())
343                .ok_or(error!("Function codomain is not an object"))?;
344            let codomain = codomain
345                .iter()
346                .next()
347                .ok_or(Error::Parse("DomainSet is an empty object".to_owned()))?;
348            let codomain = parse_domain(codomain.0.as_str(), codomain.1, symbols)?;
349
350            // Attribute parsing
351            let attributes = domain_value
352                .get(1)
353                .and_then(|v| v.as_array())
354                .ok_or(error!("Function attributes is not a json array"))?;
355            let size = attributes
356                .first()
357                .and_then(|v| v.as_object())
358                .ok_or(error!("Function size attributes is not an object"))?;
359            let size = parse_size_attr(size, symbols)?;
360            let partiality = attributes
361                .get(1)
362                .and_then(|v| v.as_str())
363                .ok_or(error!("Function partiality is not a string"))?;
364            let partiality = match partiality {
365                "PartialityAttr_Partial" => Some(PartialityAttr::Partial),
366                "PartialityAttr_Total" => Some(PartialityAttr::Total),
367                _ => None,
368            };
369            if partiality.is_none() {
370                return Err(Error::Parse("Partiality is an unknown type".to_owned()));
371            }
372            let partiality = partiality.unwrap();
373            let jectivity = attributes
374                .get(2)
375                .and_then(|v| v.as_str())
376                .ok_or(error!("Function jectivity is not a string"))?;
377            let jectivity = match jectivity {
378                "JectivityAttr_Injective" => Some(JectivityAttr::Injective),
379                "JectivityAttr_Surjective" => Some(JectivityAttr::Surjective),
380                "JectivityAttr_Bijective" => Some(JectivityAttr::Bijective),
381                "JectivityAttr_None" => Some(JectivityAttr::None),
382                _ => None,
383            };
384            if jectivity.is_none() {
385                return Err(Error::Parse("Jectivity is an unknown type".to_owned()));
386            }
387            let jectivity = jectivity.unwrap();
388
389            let attr: FuncAttr<IntVal> = FuncAttr {
390                size,
391                partiality,
392                jectivity,
393            };
394
395            Ok(Domain::function(attr, domain, codomain))
396        }
397        _ => Err(Error::Parse(
398            "FindOrGiven[2] is an unknown object".to_owned(), // consider covered
399        )),
400    }
401}
402
403fn parse_size_attr(
404    attr_map: &JsonMap<String, JsonValue>,
405    symbols: &mut SymbolTable,
406) -> Result<Range<IntVal>> {
407    let attr_obj = attr_map
408        .iter()
409        .next()
410        .ok_or(Error::Parse("SizeAttr is an empty object".to_owned()))?;
411    match attr_obj.0.as_str() {
412        "SizeAttr_None" => Ok(Range::Unbounded),
413        "SizeAttr_MinSize" => {
414            let size_int = parse_domain_value_int(attr_obj.1, symbols)
415                .ok_or(error!("Could not parse int domain constant"))?;
416            Ok(Range::UnboundedR(size_int.into()))
417        }
418        "SizeAttr_MaxSize" => {
419            let size_int = parse_domain_value_int(attr_obj.1, symbols)
420                .ok_or(error!("Could not parse int domain constant"))?;
421            Ok(Range::UnboundedL(size_int.into()))
422        }
423        "SizeAttr_MinMaxSize" => {
424            let min_max = attr_obj
425                .1
426                .as_array()
427                .ok_or(error!("SizeAttr MinMaxSize is not a json array"))?;
428            let min = min_max
429                .first()
430                .ok_or(error!("SizeAttr Min is not present"))?;
431            let min_int = parse_domain_value_int(min, symbols)
432                .ok_or(error!("Could not parse int domain constant"))?;
433            let max = min_max
434                .get(1)
435                .ok_or(error!("SizeAttr Max is not present"))?;
436            let max_int = parse_domain_value_int(max, symbols)
437                .ok_or(error!("Could not parse int domain constant"))?;
438            Ok(Range::Bounded(min_int.into(), max_int.into()))
439        }
440        "SizeAttr_Size" => {
441            let size_int = parse_domain_value_int(attr_obj.1, symbols)
442                .ok_or(error!("Could not parse int domain constant"))?;
443            Ok(Range::Single(size_int.into()))
444        }
445        _ => Err(Error::Parse("SizeAttr is an unknown type".to_owned())),
446    }
447}
448
449fn parse_int_domain(v: &JsonValue, symbols: &SymbolTable) -> Result<DomainPtr> {
450    let mut ranges = Vec::new();
451    let arr = v
452        .as_array()
453        .ok_or(error!("DomainInt is not an array".to_owned()))?[1]
454        .as_array()
455        .ok_or(error!("DomainInt[1] is not an array".to_owned()))?;
456    for range in arr {
457        let range = range
458            .as_object()
459            .ok_or(error!("DomainInt[1] contains a non-object"))?
460            .iter()
461            .next()
462            .ok_or(error!("DomainInt[1] contains an empty object"))?;
463        match range.0.as_str() {
464            "RangeBounded" => {
465                let arr = range
466                    .1
467                    .as_array()
468                    .ok_or(error!("RangeBounded is not an array".to_owned()))?;
469                let mut nums = Vec::new();
470                for item in arr.iter() {
471                    let num = parse_domain_value_int(item, symbols)
472                        .ok_or(error!("Could not parse int domain constant"))?;
473                    nums.push(num);
474                }
475                ranges.push(Range::Bounded(nums[0], nums[1]));
476            }
477            "RangeSingle" => {
478                let num = parse_domain_value_int(range.1, symbols)
479                    .ok_or(error!("Could not parse int domain constant"))?;
480                ranges.push(Range::Single(num));
481            }
482            _ => return throw_error!("DomainInt[1] contains an unknown object"),
483        }
484    }
485    Ok(Domain::int(ranges))
486}
487
488/// Parses a (possibly) integer value inside the range of a domain
489///
490/// 1. (positive number) Constant/ConstantInt/1
491///
492/// 2. (negative number) Op/MkOpNegate/Constant/ConstantInt/1
493///
494/// Unlike `parse_constant` this handles the negation operator. `parse_constant` expects the
495/// negation to already have been handled as an expression; however, here we do not expect domain
496/// values to be part of larger expressions, only negated.
497///
498fn parse_domain_value_int(obj: &JsonValue, symbols: &SymbolTable) -> Option<i32> {
499    parser_trace!("trying to parse domain value: {}", obj);
500
501    fn try_parse_positive_int(obj: &JsonValue) -> Option<i32> {
502        parser_trace!(".. trying as a positive domain value: {}", obj);
503        // Positive number: Constant/ConstantInt/1
504
505        let leaf_node = obj
506            .pointer("/Constant/ConstantInt/1")
507            .or_else(|| obj.pointer("/ConstantInt/1"))?;
508
509        match leaf_node.as_i64()?.try_into() {
510            Ok(x) => {
511                parser_trace!(".. success!");
512                Some(x)
513            }
514            Err(_) => {
515                println!("Could not convert integer constant to i32: {leaf_node:#?}");
516                None
517            }
518        }
519    }
520
521    fn try_parse_negative_int(obj: &JsonValue) -> Option<i32> {
522        // Negative number: Op/MkOpNegate/Constant/ConstantInt/1
523
524        // Unwrap negation operator, giving us a Constant/ConstantInt/1
525        //
526        // This is just a positive constant, so try to parse it as such
527
528        parser_trace!(".. trying as a negative domain value: {}", obj);
529        let inner_constant_node = obj.pointer("/Op/MkOpNegate")?;
530        let inner_num = try_parse_positive_int(inner_constant_node)?;
531
532        parser_trace!(".. success!");
533        Some(-inner_num)
534    }
535
536    // it will be too annoying to store references inside all our int domain ranges, so just
537    // resolve them here.
538    //
539    // this matches savilerow, where lettings must be declared before they are used.
540    //
541    // TODO: we shouldn't do this long term, add support for ranges containing domain references.
542    fn try_parse_reference(obj: &JsonValue, symbols: &SymbolTable) -> Option<i32> {
543        parser_trace!(".. trying as a domain reference: {}", obj);
544        let inner_name = obj.pointer("/Reference/0/Name")?.as_str()?;
545        parser_trace!(
546            ".. found domain reference to {}, trying to resolve it",
547            inner_name
548        );
549        let name = Name::User(Ustr::from(inner_name));
550        let decl = symbols.lookup(&name)?;
551        let DeclarationKind::ValueLetting(d) = &decl.kind() as &DeclarationKind else {
552            parser_trace!(".. name exists but is not a value letting!");
553            return None;
554        };
555
556        let a = d.clone().into_literal()?;
557        let Literal::Int(a) = a else {
558            return None;
559        };
560
561        Some(a)
562    }
563
564    try_parse_positive_int(obj)
565        .or_else(|| try_parse_negative_int(obj))
566        .or_else(|| try_parse_reference(obj, symbols))
567}
568
569// this needs an explicit type signature to force the closures to have the same type
570type BinOp = Box<dyn Fn(Metadata, Moo<Expression>, Moo<Expression>) -> Expression>;
571type UnaryOp = Box<dyn Fn(Metadata, Moo<Expression>) -> Expression>;
572
573pub fn parse_expression(obj: &JsonValue, scope: &Rc<RefCell<SymbolTable>>) -> Option<Expression> {
574    let binary_operators: HashMap<&str, BinOp> = [
575        (
576            "MkOpIn",
577            Box::new(Expression::In) as Box<dyn Fn(_, _, _) -> _>,
578        ),
579        (
580            "MkOpUnion",
581            Box::new(Expression::Union) as Box<dyn Fn(_, _, _) -> _>,
582        ),
583        (
584            "MkOpIntersect",
585            Box::new(Expression::Intersect) as Box<dyn Fn(_, _, _) -> _>,
586        ),
587        (
588            "MkOpSupset",
589            Box::new(Expression::Supset) as Box<dyn Fn(_, _, _) -> _>,
590        ),
591        (
592            "MkOpSupsetEq",
593            Box::new(Expression::SupsetEq) as Box<dyn Fn(_, _, _) -> _>,
594        ),
595        (
596            "MkOpSubset",
597            Box::new(Expression::Subset) as Box<dyn Fn(_, _, _) -> _>,
598        ),
599        (
600            "MkOpSubsetEq",
601            Box::new(Expression::SubsetEq) as Box<dyn Fn(_, _, _) -> _>,
602        ),
603        (
604            "MkOpEq",
605            Box::new(Expression::Eq) as Box<dyn Fn(_, _, _) -> _>,
606        ),
607        (
608            "MkOpNeq",
609            Box::new(Expression::Neq) as Box<dyn Fn(_, _, _) -> _>,
610        ),
611        (
612            "MkOpGeq",
613            Box::new(Expression::Geq) as Box<dyn Fn(_, _, _) -> _>,
614        ),
615        (
616            "MkOpLeq",
617            Box::new(Expression::Leq) as Box<dyn Fn(_, _, _) -> _>,
618        ),
619        (
620            "MkOpGt",
621            Box::new(Expression::Gt) as Box<dyn Fn(_, _, _) -> _>,
622        ),
623        (
624            "MkOpLt",
625            Box::new(Expression::Lt) as Box<dyn Fn(_, _, _) -> _>,
626        ),
627        (
628            "MkOpGt",
629            Box::new(Expression::Gt) as Box<dyn Fn(_, _, _) -> _>,
630        ),
631        (
632            "MkOpLt",
633            Box::new(Expression::Lt) as Box<dyn Fn(_, _, _) -> _>,
634        ),
635        (
636            "MkOpLexLt",
637            Box::new(Expression::LexLt) as Box<dyn Fn(_, _, _) -> _>,
638        ),
639        (
640            "MkOpLexGt",
641            Box::new(Expression::LexGt) as Box<dyn Fn(_, _, _) -> _>,
642        ),
643        (
644            "MkOpLexLeq",
645            Box::new(Expression::LexLeq) as Box<dyn Fn(_, _, _) -> _>,
646        ),
647        (
648            "MkOpLexGeq",
649            Box::new(Expression::LexGeq) as Box<dyn Fn(_, _, _) -> _>,
650        ),
651        (
652            "MkOpDiv",
653            Box::new(Expression::UnsafeDiv) as Box<dyn Fn(_, _, _) -> _>,
654        ),
655        (
656            "MkOpMod",
657            Box::new(Expression::UnsafeMod) as Box<dyn Fn(_, _, _) -> _>,
658        ),
659        (
660            "MkOpMinus",
661            Box::new(Expression::Minus) as Box<dyn Fn(_, _, _) -> _>,
662        ),
663        (
664            "MkOpImply",
665            Box::new(Expression::Imply) as Box<dyn Fn(_, _, _) -> _>,
666        ),
667        (
668            "MkOpIff",
669            Box::new(Expression::Iff) as Box<dyn Fn(_, _, _) -> _>,
670        ),
671        (
672            "MkOpPow",
673            Box::new(Expression::UnsafePow) as Box<dyn Fn(_, _, _) -> _>,
674        ),
675        (
676            "MkOpImage",
677            Box::new(Expression::Image) as Box<dyn Fn(_, _, _) -> _>,
678        ),
679        (
680            "MkOpImageSet",
681            Box::new(Expression::ImageSet) as Box<dyn Fn(_, _, _) -> _>,
682        ),
683        (
684            "MkOpPreImage",
685            Box::new(Expression::PreImage) as Box<dyn Fn(_, _, _) -> _>,
686        ),
687        (
688            "MkOpInverse",
689            Box::new(Expression::Inverse) as Box<dyn Fn(_, _, _) -> _>,
690        ),
691        (
692            "MkOpRestrict",
693            Box::new(Expression::Restrict) as Box<dyn Fn(_, _, _) -> _>,
694        ),
695    ]
696    .into_iter()
697    .collect();
698
699    let unary_operators: HashMap<&str, UnaryOp> = [
700        (
701            "MkOpNot",
702            Box::new(Expression::Not) as Box<dyn Fn(_, _) -> _>,
703        ),
704        (
705            "MkOpNegate",
706            Box::new(Expression::Neg) as Box<dyn Fn(_, _) -> _>,
707        ),
708        (
709            "MkOpTwoBars",
710            Box::new(Expression::Abs) as Box<dyn Fn(_, _) -> _>,
711        ),
712        (
713            "MkOpAnd",
714            Box::new(Expression::And) as Box<dyn Fn(_, _) -> _>,
715        ),
716        (
717            "MkOpSum",
718            Box::new(Expression::Sum) as Box<dyn Fn(_, _) -> _>,
719        ),
720        (
721            "MkOpProduct",
722            Box::new(Expression::Product) as Box<dyn Fn(_, _) -> _>,
723        ),
724        ("MkOpOr", Box::new(Expression::Or) as Box<dyn Fn(_, _) -> _>),
725        (
726            "MkOpMin",
727            Box::new(Expression::Min) as Box<dyn Fn(_, _) -> _>,
728        ),
729        (
730            "MkOpMax",
731            Box::new(Expression::Max) as Box<dyn Fn(_, _) -> _>,
732        ),
733        (
734            "MkOpAllDiff",
735            Box::new(Expression::AllDiff) as Box<dyn Fn(_, _) -> _>,
736        ),
737        (
738            "MkOpToInt",
739            Box::new(Expression::ToInt) as Box<dyn Fn(_, _) -> _>,
740        ),
741        (
742            "MkOpDefined",
743            Box::new(Expression::Defined) as Box<dyn Fn(_, _) -> _>,
744        ),
745        (
746            "MkOpRange",
747            Box::new(Expression::Range) as Box<dyn Fn(_, _) -> _>,
748        ),
749    ]
750    .into_iter()
751    .collect();
752
753    let mut binary_operator_names = binary_operators.iter().map(|x| x.0);
754    let mut unary_operator_names = unary_operators.iter().map(|x| x.0);
755    #[allow(clippy::unwrap_used)]
756    match obj {
757        Value::Object(op) if op.contains_key("Op") => match &op["Op"] {
758            Value::Object(bin_op) if binary_operator_names.any(|key| bin_op.contains_key(*key)) => {
759                Some(parse_bin_op(bin_op, binary_operators, scope).unwrap())
760            }
761            Value::Object(un_op) if unary_operator_names.any(|key| un_op.contains_key(*key)) => {
762                Some(parse_unary_op(un_op, unary_operators, scope).unwrap())
763            }
764            Value::Object(op) if op.contains_key("MkOpFlatten") => parse_flatten_op(op, scope),
765            Value::Object(op)
766                if op.contains_key("MkOpIndexing") || op.contains_key("MkOpSlicing") =>
767            {
768                parse_indexing_slicing_op(op, scope)
769            }
770            otherwise => bug!("Unhandled Op {:#?}", otherwise),
771        },
772        Value::Object(comprehension) if comprehension.contains_key("Comprehension") => {
773            Some(parse_comprehension(comprehension, Rc::clone(scope), None).unwrap())
774        }
775        Value::Object(refe) if refe.contains_key("Reference") => {
776            let name = refe["Reference"].as_array()?[0].as_object()?["Name"].as_str()?;
777            let user_name = Name::User(Ustr::from(name));
778
779            let declaration: DeclarationPtr = scope
780                .borrow()
781                .lookup(&user_name)
782                .or_else(|| bug!("Could not find reference {user_name}"))?;
783
784            Some(Expression::Atomic(
785                Metadata::new(),
786                Atom::Reference(crate::ast::Reference::new(declaration)),
787            ))
788        }
789        Value::Object(abslit) if abslit.contains_key("AbstractLiteral") => {
790            if abslit["AbstractLiteral"]
791                .as_object()?
792                .contains_key("AbsLitSet")
793            {
794                Some(parse_abs_lit(&abslit["AbstractLiteral"]["AbsLitSet"], scope).unwrap())
795            } else if abslit["AbstractLiteral"]
796                .as_object()?
797                .contains_key("AbsLitFunction")
798            {
799                Some(
800                    parse_abs_function(&abslit["AbstractLiteral"]["AbsLitFunction"], scope)
801                        .unwrap(),
802                )
803            } else {
804                Some(parse_abstract_matrix_as_expr(obj, scope).unwrap())
805            }
806        }
807
808        Value::Object(constant) if constant.contains_key("Constant") => Some(
809            parse_constant(constant, scope)
810                .or_else(|| parse_abstract_matrix_as_expr(obj, scope))
811                .unwrap(),
812        ),
813
814        Value::Object(constant) if constant.contains_key("ConstantAbstract") => {
815            Some(parse_abstract_matrix_as_expr(obj, scope).unwrap())
816        }
817
818        Value::Object(constant) if constant.contains_key("ConstantInt") => {
819            Some(parse_constant(constant, scope).unwrap())
820        }
821        Value::Object(constant) if constant.contains_key("ConstantBool") => {
822            Some(parse_constant(constant, scope).unwrap())
823        }
824
825        _ => None,
826    }
827}
828
829fn parse_abs_lit(abs_set: &Value, scope: &Rc<RefCell<SymbolTable>>) -> Option<Expression> {
830    let values = abs_set.as_array()?; // Ensure it's an array
831    let expressions = values
832        .iter()
833        .map(|values| parse_expression(values, scope))
834        .map(|values| values.expect("invalid subexpression")) // Ensure valid expressions
835        .collect::<Vec<Expression>>(); // Collect all expressions
836
837    Some(Expression::AbstractLiteral(
838        Metadata::new(),
839        AbstractLiteral::Set(expressions),
840    ))
841}
842
843fn parse_abs_tuple(abs_tuple: &Value, scope: &Rc<RefCell<SymbolTable>>) -> Option<Expression> {
844    let values = abs_tuple.as_array()?; // Ensure it's an array
845    let expressions = values
846        .iter()
847        .map(|values| parse_expression(values, scope))
848        .map(|values| values.expect("invalid subexpression")) // Ensure valid expressions
849        .collect::<Vec<Expression>>(); // Collect all expressions
850
851    Some(Expression::AbstractLiteral(
852        Metadata::new(),
853        AbstractLiteral::Tuple(expressions),
854    ))
855}
856
857//parses an abstract record as an expression
858fn parse_abs_record(abs_record: &Value, scope: &Rc<RefCell<SymbolTable>>) -> Option<Expression> {
859    let entries = abs_record.as_array()?; // Ensure it's an array
860    let mut rec = vec![];
861
862    for entry in entries {
863        let entry = entry.as_array()?;
864        let name = entry[0].as_object()?["Name"].as_str()?;
865
866        let value = parse_expression(&entry[1], scope)?;
867
868        let name = Name::User(Ustr::from(name));
869        let rec_entry = RecordValue {
870            name: name.clone(),
871            value,
872        };
873        rec.push(rec_entry);
874    }
875
876    Some(Expression::AbstractLiteral(
877        Metadata::new(),
878        AbstractLiteral::Record(rec),
879    ))
880}
881
882//parses an abstract function as an expression
883fn parse_abs_function(
884    abs_function: &Value,
885    scope: &Rc<RefCell<SymbolTable>>,
886) -> Option<Expression> {
887    let entries = abs_function.as_array()?;
888    let mut assignments = vec![];
889
890    for entry in entries {
891        //expect("Explicit function assignment is not an array");
892        let entry = entry.as_array()?;
893        let expression = entry
894            .iter()
895            .map(|values| parse_expression(values, scope))
896            .map(|values| values.expect("invalid subexpression")) // Ensure valid expressions
897            .collect::<Vec<Expression>>(); // Collect all expressions
898        let domain_value = expression.first().expect("Invalid function domain");
899        let codomain_value = expression.get(1).expect("Invalid function codomain");
900        let tuple = (domain_value.clone(), codomain_value.clone());
901        assignments.push(tuple);
902    }
903    Some(Expression::AbstractLiteral(
904        Metadata::new(),
905        AbstractLiteral::Function(assignments),
906    ))
907}
908
909fn parse_comprehension(
910    comprehension: &serde_json::Map<String, Value>,
911    scope: Rc<RefCell<SymbolTable>>,
912    comprehension_kind: Option<ACOperatorKind>,
913) -> Option<Expression> {
914    let value = &comprehension["Comprehension"];
915    let mut comprehension = ComprehensionBuilder::new(Rc::clone(&scope));
916    let generator_symboltable = comprehension.generator_symboltable();
917    let return_expr_symboltable = comprehension.return_expr_symboltable();
918
919    let generators_and_guards = value.pointer("/1")?.as_array()?.iter();
920
921    for gen_or_guard in generators_and_guards {
922        let (name, inner) = gen_or_guard.as_object()?.iter().next()?;
923        comprehension = match name.as_str() {
924            "Generator" => {
925                // TODO: more things than GenDomainNoRepr and Single names here?
926                let (name, gen_inner) = inner.as_object()?.iter().next()?;
927                match name.as_str() {
928                    "GenDomainNoRepr" => {
929                        let name = gen_inner.pointer("/0/Single/Name")?.as_str()?;
930                        let (domain_name, domain_value) =
931                            gen_inner.pointer("/1")?.as_object()?.iter().next()?;
932                        let domain = parse_domain(
933                            domain_name,
934                            domain_value,
935                            &mut generator_symboltable.borrow_mut(),
936                        )
937                        .ok()?;
938                        comprehension.generator(DeclarationPtr::new_var(name.into(), domain))
939                    }
940                    // TODO: this is temporary until comprehensions support "in expr" generators
941                    // currently only supports a single generator of this type
942                    "GenInExpr" => return parse_in_expr_comprehension(scope, value, gen_inner),
943                    _ => {
944                        bug!("unknown generator type inside comprehension {name}");
945                    }
946                }
947            }
948
949            "Condition" => comprehension.guard(parse_expression(inner, &generator_symboltable)?),
950
951            x => {
952                bug!("unknown field inside comprehension {x}");
953            }
954        }
955    }
956
957    let expr = parse_expression(value.pointer("/0")?, &return_expr_symboltable)?;
958
959    Some(Expression::Comprehension(
960        Metadata::new(),
961        Moo::new(comprehension.with_return_value(expr, comprehension_kind)),
962    ))
963}
964
965fn parse_in_expr_comprehension(
966    scope: Rc<RefCell<SymbolTable>>,
967    comprehension_value: &Value,
968    gen_inner: &Value,
969) -> Option<Expression> {
970    let name = gen_inner.pointer("/0/Single/Name")?.as_str()?;
971    let expr = parse_expression(gen_inner.pointer("/1")?, &scope)?;
972
973    let comprehension =
974        AbstractComprehensionBuilder::new(&scope).new_expression_generator(expr, name.into());
975    let expr = parse_expression(
976        comprehension_value.pointer("/0")?,
977        &comprehension.return_expr_symbols(),
978    )?;
979
980    Some(Expression::AbstractComprehension(
981        Metadata::new(),
982        Moo::new(comprehension.with_return_value(expr)),
983    ))
984}
985
986fn parse_bin_op(
987    bin_op: &serde_json::Map<String, Value>,
988    binary_operators: HashMap<&str, BinOp>,
989    scope: &Rc<RefCell<SymbolTable>>,
990) -> Option<Expression> {
991    // we know there is a single key value pair in this object
992    // extract the value, ignore the key
993    let (key, value) = bin_op.into_iter().next()?;
994
995    let constructor = binary_operators.get(key.as_str())?;
996
997    match &value {
998        Value::Array(bin_op_args) if bin_op_args.len() == 2 => {
999            let arg1 = parse_expression(&bin_op_args[0], scope)?;
1000            let arg2 = parse_expression(&bin_op_args[1], scope)?;
1001            Some(constructor(Metadata::new(), Moo::new(arg1), Moo::new(arg2)))
1002        }
1003        otherwise => bug!("Unhandled parse_bin_op {:#?}", otherwise),
1004    }
1005}
1006
1007fn parse_indexing_slicing_op(
1008    op: &serde_json::Map<String, Value>,
1009    scope: &Rc<RefCell<SymbolTable>>,
1010) -> Option<Expression> {
1011    // we know there is a single key value pair in this object
1012    // extract the value, ignore the key
1013    let (key, value) = op.into_iter().next()?;
1014
1015    // we know that this is meant to be a mkopindexing, so anything that goes wrong from here is a
1016    // bug!
1017
1018    // Conjure does a[1,2,3] as MkOpIndexing(MkOpIndexing(MkOpIndexing(a,3),2),1).
1019    //
1020    // And  a[1,..,3] as MkOpIndexing(MkOpSlicing(MkOpIndexing(a,3)),1).
1021    //
1022    // However, we want this in a flattened form: Index(a, [1,2,3])
1023    let mut target: Expression;
1024    let mut indices: Vec<Option<Expression>> = vec![];
1025
1026    // true if this has no slicing, false otherwise.
1027    let mut all_known = true;
1028
1029    match key.as_str() {
1030        "MkOpIndexing" => {
1031            match &value {
1032                Value::Array(op_args) if op_args.len() == 2 => {
1033                    target = parse_expression(&op_args[0], scope).expect("expected an expression");
1034                    indices.push(Some(
1035                        parse_expression(&op_args[1], scope).expect("expected an expression"),
1036                    ));
1037                }
1038                otherwise => bug!("Unknown object inside MkOpIndexing: {:#?}", otherwise),
1039            };
1040        }
1041
1042        "MkOpSlicing" => {
1043            all_known = false;
1044            match &value {
1045                Value::Array(op_args) if op_args.len() == 3 => {
1046                    target = parse_expression(&op_args[0], scope).expect("expected an expression");
1047                    indices.push(None);
1048                }
1049                otherwise => bug!("Unknown object inside MkOpSlicing: {:#?}", otherwise),
1050            };
1051        }
1052
1053        _ => {
1054            return None;
1055        }
1056    }
1057
1058    loop {
1059        match &mut target {
1060            Expression::UnsafeIndex(_, new_target, new_indices) => {
1061                indices.extend(new_indices.iter().cloned().rev().map(Some));
1062                target = Moo::unwrap_or_clone(new_target.clone());
1063            }
1064
1065            Expression::UnsafeSlice(_, new_target, new_indices) => {
1066                all_known = false;
1067                indices.extend(new_indices.iter().cloned().rev());
1068                target = Moo::unwrap_or_clone(new_target.clone());
1069            }
1070
1071            _ => {
1072                // not a slice or an index, we have reached the target.
1073                break;
1074            }
1075        }
1076    }
1077
1078    indices.reverse();
1079
1080    if all_known {
1081        Some(Expression::UnsafeIndex(
1082            Metadata::new(),
1083            Moo::new(target),
1084            indices.into_iter().map(|x| x.unwrap()).collect(),
1085        ))
1086    } else {
1087        Some(Expression::UnsafeSlice(
1088            Metadata::new(),
1089            Moo::new(target),
1090            indices,
1091        ))
1092    }
1093}
1094
1095fn parse_flatten_op(
1096    op: &serde_json::Map<String, Value>,
1097    scope: &Rc<RefCell<SymbolTable>>,
1098) -> Option<Expression> {
1099    let args = op.get("MkOpFlatten")?.as_array()?;
1100
1101    let n = parse_expression(&args[0], scope);
1102    let matrix = parse_expression(&args[1], scope)?;
1103
1104    if let Some(n) = n {
1105        Some(Expression::Flatten(
1106            Metadata::new(),
1107            Some(Moo::new(n)),
1108            Moo::new(matrix),
1109        ))
1110    } else {
1111        Some(Expression::Flatten(Metadata::new(), None, Moo::new(matrix)))
1112    }
1113}
1114
1115fn parse_unary_op(
1116    un_op: &serde_json::Map<String, Value>,
1117    unary_operators: HashMap<&str, UnaryOp>,
1118    scope: &Rc<RefCell<SymbolTable>>,
1119) -> Option<Expression> {
1120    let (key, value) = un_op.into_iter().next()?;
1121    let constructor = unary_operators.get(key.as_str())?;
1122
1123    // unops are the main things that contain comprehensions
1124    //
1125    // if the current expr is a quantifier like and/or/sum and it contains a comprehension, let the comprehension know what it is inside.
1126    let arg = match value {
1127        Value::Object(comprehension) if comprehension.contains_key("Comprehension") => {
1128            let comprehension_kind = match key.as_str() {
1129                "MkOpOr" => Some(ACOperatorKind::Or),
1130                "MkOpAnd" => Some(ACOperatorKind::And),
1131                "MkOpSum" => Some(ACOperatorKind::Sum),
1132                "MkOpProduct" => Some(ACOperatorKind::Product),
1133                _ => None,
1134            };
1135            Some(parse_comprehension(comprehension, Rc::clone(scope), comprehension_kind).unwrap())
1136        }
1137        _ => parse_expression(value, scope),
1138    }?;
1139
1140    Some(constructor(Metadata::new(), Moo::new(arg)))
1141}
1142
1143// Takes in { AbstractLiteral: .... }
1144fn parse_abstract_matrix_as_expr(
1145    value: &serde_json::Value,
1146    scope: &Rc<RefCell<SymbolTable>>,
1147) -> Option<Expression> {
1148    parser_trace!("trying to parse an abstract literal matrix");
1149    let (values, domain_name, domain_value) =
1150        if let Some(abs_lit_matrix) = value.pointer("/AbstractLiteral/AbsLitMatrix") {
1151            parser_trace!(".. found JSON pointer /AbstractLiteral/AbstractLitMatrix");
1152            let (domain_name, domain_value) =
1153                abs_lit_matrix.pointer("/0")?.as_object()?.iter().next()?;
1154            let values = abs_lit_matrix.pointer("/1")?;
1155
1156            Some((values, domain_name, domain_value))
1157        }
1158        // the input of this expression is constant - e.g. or([]), or([false]), min([2]), etc.
1159        else if let Some(const_abs_lit_matrix) =
1160            value.pointer("/Constant/ConstantAbstract/AbsLitMatrix")
1161        {
1162            parser_trace!(".. found JSON pointer /Constant/ConstantAbstract/AbsLitMatrix");
1163            let (domain_name, domain_value) = const_abs_lit_matrix
1164                .pointer("/0")?
1165                .as_object()?
1166                .iter()
1167                .next()?;
1168            let values = const_abs_lit_matrix.pointer("/1")?;
1169
1170            Some((values, domain_name, domain_value))
1171        } else if let Some(const_abs_lit_matrix) = value.pointer("/ConstantAbstract/AbsLitMatrix") {
1172            parser_trace!(".. found JSON pointer /ConstantAbstract/AbsLitMatrix");
1173            let (domain_name, domain_value) = const_abs_lit_matrix
1174                .pointer("/0")?
1175                .as_object()?
1176                .iter()
1177                .next()?;
1178            let values = const_abs_lit_matrix.pointer("/1")?;
1179            Some((values, domain_name, domain_value))
1180        } else {
1181            None
1182        }?;
1183
1184    parser_trace!(".. found in domain and values in JSON:");
1185    parser_trace!(".. .. index domain name {domain_name}");
1186    parser_trace!(".. .. values {value}");
1187
1188    let args_parsed = values.as_array().map(|x| {
1189        x.iter()
1190            .map(|x| parse_expression(x, scope))
1191            .map(|x| x.expect("invalid subexpression"))
1192            .collect::<Vec<Expression>>()
1193    })?;
1194
1195    if !args_parsed.is_empty() {
1196        parser_trace!(
1197            ".. successfully parsed values as expressions: {}, ... ",
1198            args_parsed[0]
1199        );
1200    } else {
1201        parser_trace!(".. successfully parsed empty values ",);
1202    }
1203
1204    let mut symbols = scope.borrow_mut();
1205    match parse_domain(domain_name, domain_value, &mut symbols) {
1206        Ok(domain) => {
1207            parser_trace!("... sucessfully parsed domain as {domain}");
1208            Some(into_matrix_expr![args_parsed;domain])
1209        }
1210        Err(_) => {
1211            parser_trace!("... failed to parse domain, creating a matrix without one.");
1212            Some(into_matrix_expr![args_parsed])
1213        }
1214    }
1215}
1216
1217fn parse_constant(
1218    constant: &serde_json::Map<String, Value>,
1219    scope: &Rc<RefCell<SymbolTable>>,
1220) -> Option<Expression> {
1221    match &constant.get("Constant") {
1222        Some(Value::Object(int)) if int.contains_key("ConstantInt") => {
1223            let int_32: i32 = match int["ConstantInt"].as_array()?[1].as_i64()?.try_into() {
1224                Ok(x) => x,
1225                Err(_) => {
1226                    println!(
1227                        "Could not convert integer constant to i32: {:#?}",
1228                        int["ConstantInt"]
1229                    );
1230                    return None;
1231                }
1232            };
1233
1234            Some(Expression::Atomic(
1235                Metadata::new(),
1236                Atom::Literal(Literal::Int(int_32)),
1237            ))
1238        }
1239
1240        Some(Value::Object(b)) if b.contains_key("ConstantBool") => {
1241            let b: bool = b["ConstantBool"].as_bool()?;
1242            Some(Expression::Atomic(
1243                Metadata::new(),
1244                Atom::Literal(Literal::Bool(b)),
1245            ))
1246        }
1247
1248        Some(Value::Object(int)) if int.contains_key("ConstantAbstract") => {
1249            if let Some(Value::Object(obj)) = int.get("ConstantAbstract") {
1250                if let Some(arr) = obj.get("AbsLitSet") {
1251                    return parse_abs_lit(arr, scope);
1252                } else if let Some(arr) = obj.get("AbsLitMatrix") {
1253                    return parse_abstract_matrix_as_expr(arr, scope);
1254                } else if let Some(arr) = obj.get("AbsLitTuple") {
1255                    return parse_abs_tuple(arr, scope);
1256                } else if let Some(arr) = obj.get("AbsLitRecord") {
1257                    return parse_abs_record(arr, scope);
1258                } else if let Some(arr) = obj.get("AbsLitFunction") {
1259                    return parse_abs_function(arr, scope);
1260                }
1261            }
1262            None
1263        }
1264
1265        // sometimes (e.g. constant matrices) we can have a ConstantInt / Constant bool that is
1266        // not wrapped in Constant
1267        None => {
1268            let int_expr = constant
1269                .get("ConstantInt")
1270                .and_then(|x| x.as_array())
1271                .and_then(|x| x[1].as_i64())
1272                .and_then(|x| x.try_into().ok())
1273                .map(|x| Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(x))));
1274
1275            if let e @ Some(_) = int_expr {
1276                return e;
1277            }
1278
1279            let bool_expr = constant
1280                .get("ConstantBool")
1281                .and_then(|x| x.as_bool())
1282                .map(|x| Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Bool(x))));
1283
1284            if let e @ Some(_) = bool_expr {
1285                return e;
1286            }
1287
1288            bug!("Unhandled parse_constant {:#?}", constant);
1289        }
1290        otherwise => bug!("Unhandled parse_constant {:#?}", otherwise),
1291    }
1292}