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};
7
8use serde_json::Value;
9use serde_json::Value as JsonValue;
10
11use crate::ast::comprehension::{ComprehensionBuilder, ComprehensionKind};
12use crate::ast::records::RecordValue;
13use crate::ast::{
14 AbstractLiteral, Atom, Domain, Expression, Literal, Name, Range, RecordEntry, SetAttr,
15 SymbolTable,
16};
17use crate::ast::{Declaration, DeclarationKind};
18use crate::context::Context;
19use crate::error::{Error, Result};
20use crate::metadata::Metadata;
21use crate::{bug, error, into_matrix_expr, throw_error, Model};
22
23#[allow(unused_macros)]
24macro_rules! parser_trace {
25 ($($arg:tt)+) => {
26 log::trace!(target:"jsonparser",$($arg)+)
27 };
28}
29
30#[allow(unused_macros)]
31macro_rules! parser_debug {
32 ($($arg:tt)+) => {
33 log::debug!(target:"jsonparser",$($arg)+)
34 };
35}
36
37pub fn model_from_json(str: &str, context: Arc<RwLock<Context<'static>>>) -> Result<Model> {
38 let mut m = Model::new(context);
39 let v: JsonValue = serde_json::from_str(str)?;
40 let statements = v["mStatements"]
41 .as_array()
42 .ok_or(error!("mStatements is not an array"))?;
43
44 for statement in statements {
45 let entry = statement
46 .as_object()
47 .ok_or(error!("mStatements contains a non-object"))?
48 .iter()
49 .next()
50 .ok_or(error!("mStatements contains an empty object"))?;
51
52 match entry.0.as_str() {
53 "Declaration" => {
54 let decl = entry
55 .1
56 .as_object()
57 .ok_or(error!("Declaration is not an object".to_owned()))?;
58
59 let mut valid_decl: bool = false;
66 let scope = m.as_submodel().symbols_ptr_unchecked().clone();
67 let submodel = m.as_submodel_mut();
68 for (kind, value) in decl {
69 match kind.as_str() {
70 "FindOrGiven" => {
71 parse_variable(value, &mut submodel.symbols_mut())?;
72 valid_decl = true;
73 break;
74 }
75 "Letting" => {
76 parse_letting(value, &scope)?;
77 valid_decl = true;
78 break;
79 }
80 _ => continue,
81 }
82 }
83
84 if !valid_decl {
85 throw_error!("Declaration is not a valid kind")?;
86 }
87 }
88 "SuchThat" => {
89 let constraints_arr = match entry.1.as_array() {
90 Some(x) => x,
91 None => bug!("SuchThat is not a vector"),
92 };
93
94 let constraints: Vec<Expression> = constraints_arr
95 .iter()
96 .map(|x| {
97 parse_expression(x, m.as_submodel_mut().symbols_ptr_unchecked()).unwrap()
98 })
99 .collect();
100 m.as_submodel_mut().add_constraints(constraints);
101 }
103 otherwise => bug!("Unhandled Statement {:#?}", otherwise),
104 }
105 }
106 Ok(m)
107}
108
109fn parse_variable(v: &JsonValue, symtab: &mut SymbolTable) -> Result<()> {
110 let arr = v.as_array().ok_or(error!("FindOrGiven is not an array"))?;
111 let name = arr[1]
112 .as_object()
113 .ok_or(error!("FindOrGiven[1] is not an object"))?["Name"]
114 .as_str()
115 .ok_or(error!("FindOrGiven[1].Name is not a string"))?;
116
117 let name = Name::User(name.to_owned());
118
119 let domain = arr[2]
120 .as_object()
121 .ok_or(error!("FindOrGiven[2] is not an object"))?
122 .iter()
123 .next()
124 .ok_or(error!("FindOrGiven[2] is an empty object"))?;
125
126 let domain = parse_domain(domain.0, domain.1, symtab)?;
127
128 symtab
129 .insert(Rc::new(Declaration::new_var(name.clone(), domain)))
130 .ok_or(Error::Parse(format!(
131 "Could not add {name} to symbol table as it already exists"
132 )))
133}
134
135fn parse_letting(v: &JsonValue, scope: &Rc<RefCell<SymbolTable>>) -> Result<()> {
136 let arr = v.as_array().ok_or(error!("Letting is not an array"))?;
137 let name = arr[0]
138 .as_object()
139 .ok_or(error!("Letting[0] is not an object"))?["Name"]
140 .as_str()
141 .ok_or(error!("Letting[0].Name is not a string"))?;
142 let name = Name::User(name.to_owned());
143 if let Some(value) = parse_expression(&arr[1], scope) {
145 let mut symtab = scope.borrow_mut();
146 symtab
147 .insert(Rc::new(Declaration::new_value_letting(name.clone(), value)))
148 .ok_or(Error::Parse(format!(
149 "Could not add {name} to symbol table as it already exists"
150 )))
151 } else {
152 let domain = &arr[1]
154 .as_object()
155 .ok_or(error!("Letting[1] is not an object".to_owned()))?["Domain"]
156 .as_object()
157 .ok_or(error!("Letting[1].Domain is not an object"))?
158 .iter()
159 .next()
160 .ok_or(error!("Letting[1].Domain is an empty object"))?;
161
162 let mut symtab = scope.borrow_mut();
163 let domain = parse_domain(domain.0, domain.1, &symtab)?;
164
165 symtab
166 .insert(Rc::new(Declaration::new_domain_letting(
167 name.clone(),
168 domain,
169 )))
170 .ok_or(Error::Parse(format!(
171 "Could not add {name} to symbol table as it already exists"
172 )))
173 }
174}
175
176fn parse_domain(
177 domain_name: &str,
178 domain_value: &JsonValue,
179 symbols: &SymbolTable,
180) -> Result<Domain> {
181 match domain_name {
182 "DomainInt" => Ok(parse_int_domain(domain_value, symbols)?),
183 "DomainBool" => Ok(Domain::Bool),
184 "DomainReference" => Ok(Domain::Reference(Name::User(
185 domain_value
186 .as_array()
187 .ok_or(error!("DomainReference is not an array"))?[0]
188 .as_object()
189 .ok_or(error!("DomainReference[0] is not an object"))?["Name"]
190 .as_str()
191 .ok_or(error!("DomainReference[0].Name is not a string"))?
192 .into(),
193 ))),
194 "DomainSet" => {
195 let dom = domain_value.get(2).and_then(|v| v.as_object());
196 let domain_obj = dom.expect("domain object exists");
197 let domain = domain_obj
198 .iter()
199 .next()
200 .ok_or(Error::Parse("DomainSet is an empty object".to_owned()))?;
201 let domain = parse_domain(domain.0.as_str(), domain.1, symbols)?;
202 Ok(Domain::Set(SetAttr::None, Box::new(domain)))
203 }
204
205 "DomainMatrix" => {
206 let domain_value = domain_value
207 .as_array()
208 .ok_or(error!("Domain matrix is not an array"))?;
209
210 let indexed_by_domain = domain_value[0].clone();
211 let (index_domain_name, index_domain_value) = indexed_by_domain
212 .as_object()
213 .ok_or(error!("DomainMatrix[0] is not an object"))?
214 .iter()
215 .next()
216 .ok_or(error!(""))?;
217
218 let (value_domain_name, value_domain_value) = domain_value[1]
219 .as_object()
220 .ok_or(error!(""))?
221 .iter()
222 .next()
223 .ok_or(error!(""))?;
224
225 let mut index_domains: Vec<Domain> = vec![];
230
231 index_domains.push(parse_domain(
232 index_domain_name,
233 index_domain_value,
234 symbols,
235 )?);
236
237 let mut value_domain = parse_domain(value_domain_name, value_domain_value, symbols)?;
243 while let Domain::Matrix(new_value_domain, mut indices) = value_domain {
244 index_domains.append(&mut indices);
245 value_domain = *new_value_domain.clone()
246 }
247
248 Ok(Domain::Matrix(Box::new(value_domain), index_domains))
249 }
250 "DomainTuple" => {
251 let domain_value = domain_value
252 .as_array()
253 .ok_or(error!("Domain tuple is not an array"))?;
254
255 let domain = domain_value
257 .iter()
258 .map(|x| {
259 let domain = x
260 .as_object()
261 .ok_or(error!("DomainTuple[0] is not an object"))?
262 .iter()
263 .next()
264 .ok_or(error!("DomainTuple[0] is an empty object"))?;
265 parse_domain(domain.0, domain.1, symbols)
266 })
267 .collect::<Result<Vec<Domain>>>()?;
268
269 Ok(Domain::Tuple(domain))
270 }
271 "DomainRecord" => {
272 let domain_value = domain_value
273 .as_array()
274 .ok_or(error!("Domain Record is not a json array"))?;
275
276 let mut record_entries = vec![];
277
278 for item in domain_value {
279 let name = item[0]
281 .as_object()
282 .ok_or(error!("FindOrGiven[1] is not an object"))?["Name"]
283 .as_str()
284 .ok_or(error!("FindOrGiven[1].Name is not a string"))?;
285
286 let name = Name::User(name.to_owned());
287 let domain = item[1]
289 .as_object()
290 .ok_or(error!("FindOrGiven[2] is not an object"))?
291 .iter()
292 .next()
293 .ok_or(error!("FindOrGiven[2] is an empty object"))?;
294
295 let domain = parse_domain(domain.0, domain.1, symbols)?;
296
297 let rec = RecordEntry { name, domain };
298 record_entries.push(rec);
299 }
300 Ok(Domain::Record(record_entries))
301 }
302
303 _ => Err(Error::Parse(
304 "FindOrGiven[2] is an unknown object".to_owned(), )),
306 }
307}
308
309fn parse_int_domain(v: &JsonValue, symbols: &SymbolTable) -> Result<Domain> {
310 let mut ranges = Vec::new();
311 let arr = v
312 .as_array()
313 .ok_or(error!("DomainInt is not an array".to_owned()))?[1]
314 .as_array()
315 .ok_or(error!("DomainInt[1] is not an array".to_owned()))?;
316 for range in arr {
317 let range = range
318 .as_object()
319 .ok_or(error!("DomainInt[1] contains a non-object"))?
320 .iter()
321 .next()
322 .ok_or(error!("DomainInt[1] contains an empty object"))?;
323 match range.0.as_str() {
324 "RangeBounded" => {
325 let arr = range
326 .1
327 .as_array()
328 .ok_or(error!("RangeBounded is not an array".to_owned()))?;
329 let mut nums = Vec::new();
330 for item in arr.iter() {
331 let num = parse_domain_value_int(item, symbols)
332 .ok_or(error!("Could not parse int domain constant"))?;
333 nums.push(num);
334 }
335 ranges.push(Range::Bounded(nums[0], nums[1]));
336 }
337 "RangeSingle" => {
338 let num = parse_domain_value_int(range.1, symbols)
339 .ok_or(error!("Could not parse int domain constant"))?;
340 ranges.push(Range::Single(num));
341 }
342 _ => return throw_error!("DomainInt[1] contains an unknown object"),
343 }
344 }
345 Ok(Domain::Int(ranges))
346}
347
348fn parse_domain_value_int(obj: &JsonValue, symbols: &SymbolTable) -> Option<i32> {
359 parser_trace!("trying to parse domain value: {}", obj);
360
361 fn try_parse_positive_int(obj: &JsonValue) -> Option<i32> {
362 parser_trace!(".. trying as a positive domain value: {}", obj);
363 let leaf_node = obj
366 .pointer("/Constant/ConstantInt/1")
367 .or_else(|| obj.pointer("/ConstantInt/1"))?;
368
369 match leaf_node.as_i64()?.try_into() {
370 Ok(x) => {
371 parser_trace!(".. success!");
372 Some(x)
373 }
374 Err(_) => {
375 println!(
376 "Could not convert integer constant to i32: {:#?}",
377 leaf_node
378 );
379 None
380 }
381 }
382 }
383
384 fn try_parse_negative_int(obj: &JsonValue) -> Option<i32> {
385 parser_trace!(".. trying as a negative domain value: {}", obj);
392 let inner_constant_node = obj.pointer("/Op/MkOpNegate")?;
393 let inner_num = try_parse_positive_int(inner_constant_node)?;
394
395 parser_trace!(".. success!");
396 Some(-inner_num)
397 }
398
399 fn try_parse_reference(obj: &JsonValue, symbols: &SymbolTable) -> Option<i32> {
406 parser_trace!(".. trying as a domain reference: {}", obj);
407 let inner_name = obj.pointer("/Reference/0/Name")?.as_str()?;
408 parser_trace!(
409 ".. found domain reference to {}, trying to resolve it",
410 inner_name
411 );
412 let name = Name::User(inner_name.to_string());
413 let decl = symbols.lookup(&name)?;
414 let DeclarationKind::ValueLetting(d) = decl.kind() else {
415 parser_trace!(".. name exists but is not a value letting!");
416 return None;
417 };
418
419 let a = d.clone().into_literal()?;
420 let Literal::Int(a) = a else {
421 return None;
422 };
423
424 Some(a)
425 }
426
427 try_parse_positive_int(obj)
428 .or_else(|| try_parse_negative_int(obj))
429 .or_else(|| try_parse_reference(obj, symbols))
430}
431
432type BinOp = Box<dyn Fn(Metadata, Box<Expression>, Box<Expression>) -> Expression>;
434type UnaryOp = Box<dyn Fn(Metadata, Box<Expression>) -> Expression>;
435
436pub fn parse_expression(obj: &JsonValue, scope: &Rc<RefCell<SymbolTable>>) -> Option<Expression> {
437 let binary_operators: HashMap<&str, BinOp> = [
438 (
439 "MkOpIn",
440 Box::new(Expression::In) as Box<dyn Fn(_, _, _) -> _>,
441 ),
442 (
443 "MkOpUnion",
444 Box::new(Expression::Union) as Box<dyn Fn(_, _, _) -> _>,
445 ),
446 (
447 "MkOpIntersect",
448 Box::new(Expression::Intersect) as Box<dyn Fn(_, _, _) -> _>,
449 ),
450 (
451 "MkOpSupset",
452 Box::new(Expression::Supset) as Box<dyn Fn(_, _, _) -> _>,
453 ),
454 (
455 "MkOpSupsetEq",
456 Box::new(Expression::SupsetEq) as Box<dyn Fn(_, _, _) -> _>,
457 ),
458 (
459 "MkOpSubset",
460 Box::new(Expression::Subset) as Box<dyn Fn(_, _, _) -> _>,
461 ),
462 (
463 "MkOpSubsetEq",
464 Box::new(Expression::SubsetEq) as Box<dyn Fn(_, _, _) -> _>,
465 ),
466 (
467 "MkOpEq",
468 Box::new(Expression::Eq) as Box<dyn Fn(_, _, _) -> _>,
469 ),
470 (
471 "MkOpNeq",
472 Box::new(Expression::Neq) as Box<dyn Fn(_, _, _) -> _>,
473 ),
474 (
475 "MkOpGeq",
476 Box::new(Expression::Geq) as Box<dyn Fn(_, _, _) -> _>,
477 ),
478 (
479 "MkOpLeq",
480 Box::new(Expression::Leq) as Box<dyn Fn(_, _, _) -> _>,
481 ),
482 (
483 "MkOpGt",
484 Box::new(Expression::Gt) as Box<dyn Fn(_, _, _) -> _>,
485 ),
486 (
487 "MkOpLt",
488 Box::new(Expression::Lt) as Box<dyn Fn(_, _, _) -> _>,
489 ),
490 (
491 "MkOpGt",
492 Box::new(Expression::Gt) as Box<dyn Fn(_, _, _) -> _>,
493 ),
494 (
495 "MkOpLt",
496 Box::new(Expression::Lt) as Box<dyn Fn(_, _, _) -> _>,
497 ),
498 (
499 "MkOpDiv",
500 Box::new(Expression::UnsafeDiv) as Box<dyn Fn(_, _, _) -> _>,
501 ),
502 (
503 "MkOpMod",
504 Box::new(Expression::UnsafeMod) as Box<dyn Fn(_, _, _) -> _>,
505 ),
506 (
507 "MkOpMinus",
508 Box::new(Expression::Minus) as Box<dyn Fn(_, _, _) -> _>,
509 ),
510 (
511 "MkOpImply",
512 Box::new(Expression::Imply) as Box<dyn Fn(_, _, _) -> _>,
513 ),
514 (
515 "MkOpIff",
516 Box::new(Expression::Iff) as Box<dyn Fn(_, _, _) -> _>,
517 ),
518 (
519 "MkOpPow",
520 Box::new(Expression::UnsafePow) as Box<dyn Fn(_, _, _) -> _>,
521 ),
522 ]
523 .into_iter()
524 .collect();
525
526 let unary_operators: HashMap<&str, UnaryOp> = [
527 (
528 "MkOpNot",
529 Box::new(Expression::Not) as Box<dyn Fn(_, _) -> _>,
530 ),
531 (
532 "MkOpNegate",
533 Box::new(Expression::Neg) as Box<dyn Fn(_, _) -> _>,
534 ),
535 (
536 "MkOpTwoBars",
537 Box::new(Expression::Abs) as Box<dyn Fn(_, _) -> _>,
538 ),
539 (
540 "MkOpAnd",
541 Box::new(Expression::And) as Box<dyn Fn(_, _) -> _>,
542 ),
543 (
544 "MkOpSum",
545 Box::new(Expression::Sum) as Box<dyn Fn(_, _) -> _>,
546 ),
547 (
548 "MkOpProduct",
549 Box::new(Expression::Product) as Box<dyn Fn(_, _) -> _>,
550 ),
551 ("MkOpOr", Box::new(Expression::Or) as Box<dyn Fn(_, _) -> _>),
552 (
553 "MkOpMin",
554 Box::new(Expression::Min) as Box<dyn Fn(_, _) -> _>,
555 ),
556 (
557 "MkOpMax",
558 Box::new(Expression::Max) as Box<dyn Fn(_, _) -> _>,
559 ),
560 (
561 "MkOpAllDiff",
562 Box::new(Expression::AllDiff) as Box<dyn Fn(_, _) -> _>,
563 ),
564 (
565 "MkOpToInt",
566 Box::new(Expression::ToInt) as Box<dyn Fn(_, _) -> _>,
567 ),
568 ]
569 .into_iter()
570 .collect();
571
572 let mut binary_operator_names = binary_operators.iter().map(|x| x.0);
573 let mut unary_operator_names = unary_operators.iter().map(|x| x.0);
574 #[allow(clippy::unwrap_used)]
575 match obj {
576 Value::Object(op) if op.contains_key("Op") => match &op["Op"] {
577 Value::Object(bin_op) if binary_operator_names.any(|key| bin_op.contains_key(*key)) => {
578 Some(parse_bin_op(bin_op, binary_operators, scope).unwrap())
579 }
580 Value::Object(un_op) if unary_operator_names.any(|key| un_op.contains_key(*key)) => {
581 Some(parse_unary_op(un_op, unary_operators, scope).unwrap())
582 }
583 Value::Object(op)
584 if op.contains_key("MkOpIndexing") || op.contains_key("MkOpSlicing") =>
585 {
586 parse_indexing_slicing_op(op, scope)
587 }
588 otherwise => bug!("Unhandled Op {:#?}", otherwise),
589 },
590 Value::Object(comprehension) if comprehension.contains_key("Comprehension") => {
591 Some(parse_comprehension(comprehension, Rc::clone(scope), None).unwrap())
592 }
593 Value::Object(refe) if refe.contains_key("Reference") => {
594 let name = refe["Reference"].as_array()?[0].as_object()?["Name"].as_str()?;
595 Some(Expression::Atomic(
596 Metadata::new(),
597 Atom::Reference(Name::User(name.to_string())),
598 ))
599 }
600 Value::Object(abslit) if abslit.contains_key("AbstractLiteral") => {
601 if abslit["AbstractLiteral"]
602 .as_object()?
603 .contains_key("AbsLitSet")
604 {
605 Some(parse_abs_lit(&abslit["AbstractLiteral"]["AbsLitSet"], scope).unwrap())
606 } else {
607 Some(parse_abstract_matrix_as_expr(obj, scope).unwrap())
608 }
609 }
610
611 Value::Object(constant) if constant.contains_key("Constant") => Some(
612 parse_constant(constant, scope)
613 .or_else(|| parse_abstract_matrix_as_expr(obj, scope))
614 .unwrap(),
615 ),
616
617 Value::Object(constant) if constant.contains_key("ConstantAbstract") => {
618 Some(parse_abstract_matrix_as_expr(obj, scope).unwrap())
619 }
620
621 Value::Object(constant) if constant.contains_key("ConstantInt") => {
622 Some(parse_constant(constant, scope).unwrap())
623 }
624 Value::Object(constant) if constant.contains_key("ConstantBool") => {
625 Some(parse_constant(constant, scope).unwrap())
626 }
627
628 _ => None,
629 }
630}
631
632fn parse_abs_lit(abs_set: &Value, scope: &Rc<RefCell<SymbolTable>>) -> Option<Expression> {
633 let values = abs_set.as_array()?; let expressions = values
635 .iter()
636 .map(|values| parse_expression(values, scope))
637 .map(|values| values.expect("invalid subexpression")) .collect::<Vec<Expression>>(); Some(Expression::AbstractLiteral(
641 Metadata::new(),
642 AbstractLiteral::Set(expressions),
643 ))
644}
645
646fn parse_abs_tuple(abs_tuple: &Value, scope: &Rc<RefCell<SymbolTable>>) -> Option<Expression> {
647 let values = abs_tuple.as_array()?; let expressions = values
649 .iter()
650 .map(|values| parse_expression(values, scope))
651 .map(|values| values.expect("invalid subexpression")) .collect::<Vec<Expression>>(); Some(Expression::AbstractLiteral(
655 Metadata::new(),
656 AbstractLiteral::Tuple(expressions),
657 ))
658}
659
660fn parse_abs_record(abs_record: &Value, scope: &Rc<RefCell<SymbolTable>>) -> Option<Expression> {
662 let entries = abs_record.as_array()?; let mut rec = vec![];
664
665 for entry in entries {
666 let entry = entry.as_array()?;
667 let name = entry[0].as_object()?["Name"].as_str()?;
668
669 let value = parse_expression(&entry[1], scope)?;
670
671 let name = Name::User(name.to_string());
672 let rec_entry = RecordValue {
673 name: name.clone(),
674 value,
675 };
676 rec.push(rec_entry);
677 }
678
679 Some(Expression::AbstractLiteral(
680 Metadata::new(),
681 AbstractLiteral::Record(rec),
682 ))
683}
684
685fn parse_comprehension(
686 comprehension: &serde_json::Map<String, Value>,
687 scope: Rc<RefCell<SymbolTable>>,
688 comprehension_kind: Option<ComprehensionKind>,
689) -> Option<Expression> {
690 let value = &comprehension["Comprehension"];
691 let mut comprehension = ComprehensionBuilder::new();
692 let expr = parse_expression(value.pointer("/0")?, &scope)?;
693
694 let generators_and_guards = value.pointer("/1")?.as_array()?.iter();
695
696 for value in generators_and_guards {
697 let value = value.as_object()?;
698 let (name, value) = value.iter().next()?;
699 comprehension = match name.as_str() {
700 "Generator" => {
701 let name = value.pointer("/GenDomainNoRepr/0/Single/Name")?.as_str()?;
703 let (domain_name, domain_value) = value
704 .pointer("/GenDomainNoRepr/1")?
705 .as_object()?
706 .iter()
707 .next()?;
708 let domain = parse_domain(domain_name, domain_value, &scope.borrow()).ok()?;
709 comprehension.generator(Name::User(name.to_string()), domain)
710 }
711
712 "Condition" => comprehension.guard(parse_expression(value, &scope)?),
713
714 x => {
715 bug!("unknown field inside comprehension {x}");
716 }
717 }
718 }
719
720 Some(Expression::Comprehension(
721 Metadata::new(),
722 Box::new(comprehension.with_return_value(expr, scope, comprehension_kind)),
723 ))
724}
725
726fn parse_bin_op(
727 bin_op: &serde_json::Map<String, Value>,
728 binary_operators: HashMap<&str, BinOp>,
729 scope: &Rc<RefCell<SymbolTable>>,
730) -> Option<Expression> {
731 let (key, value) = bin_op.into_iter().next()?;
734
735 let constructor = binary_operators.get(key.as_str())?;
736
737 match &value {
738 Value::Array(bin_op_args) if bin_op_args.len() == 2 => {
739 let arg1 = parse_expression(&bin_op_args[0], scope)?;
740 let arg2 = parse_expression(&bin_op_args[1], scope)?;
741 Some(constructor(Metadata::new(), Box::new(arg1), Box::new(arg2)))
742 }
743 otherwise => bug!("Unhandled parse_bin_op {:#?}", otherwise),
744 }
745}
746
747fn parse_indexing_slicing_op(
748 op: &serde_json::Map<String, Value>,
749 scope: &Rc<RefCell<SymbolTable>>,
750) -> Option<Expression> {
751 let (key, value) = op.into_iter().next()?;
754
755 let mut target: Expression;
764 let mut indices: Vec<Option<Expression>> = vec![];
765
766 let mut all_known = true;
768
769 match key.as_str() {
770 "MkOpIndexing" => {
771 match &value {
772 Value::Array(op_args) if op_args.len() == 2 => {
773 target = parse_expression(&op_args[0], scope).expect("expected an expression");
774 indices.push(Some(
775 parse_expression(&op_args[1], scope).expect("expected an expression"),
776 ));
777 }
778 otherwise => bug!("Unknown object inside MkOpIndexing: {:#?}", otherwise),
779 };
780 }
781
782 "MkOpSlicing" => {
783 all_known = false;
784 match &value {
785 Value::Array(op_args) if op_args.len() == 3 => {
786 target = parse_expression(&op_args[0], scope).expect("expected an expression");
787 indices.push(None);
788 }
789 otherwise => bug!("Unknown object inside MkOpSlicing: {:#?}", otherwise),
790 };
791 }
792
793 _ => {
794 return None;
795 }
796 }
797
798 loop {
799 match &mut target {
800 Expression::UnsafeIndex(_, new_target, new_indices) => {
801 indices.extend(new_indices.iter().cloned().map(Some));
802 target = *new_target.clone();
803 }
804
805 Expression::UnsafeSlice(_, new_target, new_indices) => {
806 all_known = false;
807 indices.append(new_indices);
808 target = *new_target.clone();
809 }
810
811 _ => {
812 break;
814 }
815 }
816 }
817
818 indices.reverse();
819
820 if all_known {
821 Some(Expression::UnsafeIndex(
822 Metadata::new(),
823 Box::new(target),
824 indices.into_iter().map(|x| x.unwrap()).collect(),
825 ))
826 } else {
827 Some(Expression::UnsafeSlice(
828 Metadata::new(),
829 Box::new(target),
830 indices,
831 ))
832 }
833}
834
835fn parse_unary_op(
836 un_op: &serde_json::Map<String, Value>,
837 unary_operators: HashMap<&str, UnaryOp>,
838 scope: &Rc<RefCell<SymbolTable>>,
839) -> Option<Expression> {
840 let (key, value) = un_op.into_iter().next()?;
841 let constructor = unary_operators.get(key.as_str())?;
842
843 let arg = match value {
847 Value::Object(comprehension) if comprehension.contains_key("Comprehension") => {
848 let comprehension_kind = match key.as_str() {
849 "MkOpOr" => Some(ComprehensionKind::Or),
850 "MkOpAnd" => Some(ComprehensionKind::And),
851 "MkOpSum" => Some(ComprehensionKind::Sum),
852 _ => None,
853 };
854 Some(parse_comprehension(comprehension, Rc::clone(scope), comprehension_kind).unwrap())
855 }
856 _ => parse_expression(value, scope),
857 }?;
858
859 Some(constructor(Metadata::new(), Box::new(arg)))
860}
861
862fn parse_abstract_matrix_as_expr(
864 value: &serde_json::Value,
865 scope: &Rc<RefCell<SymbolTable>>,
866) -> Option<Expression> {
867 parser_trace!("trying to parse an abstract literal matrix");
868 let (values, domain_name, domain_value) =
869 if let Some(abs_lit_matrix) = value.pointer("/AbstractLiteral/AbsLitMatrix") {
870 parser_trace!(".. found JSON pointer /AbstractLiteral/AbstractLitMatrix");
871 let (domain_name, domain_value) =
872 abs_lit_matrix.pointer("/0")?.as_object()?.iter().next()?;
873 let values = abs_lit_matrix.pointer("/1")?;
874
875 Some((values, domain_name, domain_value))
876 }
877 else if let Some(const_abs_lit_matrix) =
879 value.pointer("/Constant/ConstantAbstract/AbsLitMatrix")
880 {
881 parser_trace!(".. found JSON pointer /Constant/ConstantAbstract/AbsLitMatrix");
882 let (domain_name, domain_value) = const_abs_lit_matrix
883 .pointer("/0")?
884 .as_object()?
885 .iter()
886 .next()?;
887 let values = const_abs_lit_matrix.pointer("/1")?;
888
889 Some((values, domain_name, domain_value))
890 } else if let Some(const_abs_lit_matrix) = value.pointer("/ConstantAbstract/AbsLitMatrix") {
891 parser_trace!(".. found JSON pointer /ConstantAbstract/AbsLitMatrix");
892 let (domain_name, domain_value) = const_abs_lit_matrix
893 .pointer("/0")?
894 .as_object()?
895 .iter()
896 .next()?;
897 let values = const_abs_lit_matrix.pointer("/1")?;
898 Some((values, domain_name, domain_value))
899 } else {
900 None
901 }?;
902
903 parser_trace!(".. found in domain and values in JSON:");
904 parser_trace!(".. .. index domain name {domain_name}");
905 parser_trace!(".. .. values {value}");
906
907 let args_parsed = values.as_array().map(|x| {
908 x.iter()
909 .map(|x| parse_expression(x, scope))
910 .map(|x| x.expect("invalid subexpression"))
911 .collect::<Vec<Expression>>()
912 })?;
913
914 if !args_parsed.is_empty() {
915 parser_trace!(
916 ".. successfully parsed values as expressions: {}, ... ",
917 args_parsed[0]
918 );
919 } else {
920 parser_trace!(".. successfully parsed empty values ",);
921 }
922
923 let symbols = scope.borrow();
924 match parse_domain(domain_name, domain_value, &symbols) {
925 Ok(domain) => {
926 parser_trace!("... sucessfully parsed domain as {domain}");
927 Some(into_matrix_expr![args_parsed;domain])
928 }
929 Err(_) => {
930 parser_trace!("... failed to parse domain, creating a matrix without one.");
931 Some(into_matrix_expr![args_parsed])
932 }
933 }
934}
935
936fn parse_constant(
937 constant: &serde_json::Map<String, Value>,
938 scope: &Rc<RefCell<SymbolTable>>,
939) -> Option<Expression> {
940 match &constant.get("Constant") {
941 Some(Value::Object(int)) if int.contains_key("ConstantInt") => {
942 let int_32: i32 = match int["ConstantInt"].as_array()?[1].as_i64()?.try_into() {
943 Ok(x) => x,
944 Err(_) => {
945 println!(
946 "Could not convert integer constant to i32: {:#?}",
947 int["ConstantInt"]
948 );
949 return None;
950 }
951 };
952
953 Some(Expression::Atomic(
954 Metadata::new(),
955 Atom::Literal(Literal::Int(int_32)),
956 ))
957 }
958
959 Some(Value::Object(b)) if b.contains_key("ConstantBool") => {
960 let b: bool = b["ConstantBool"].as_bool()?;
961 Some(Expression::Atomic(
962 Metadata::new(),
963 Atom::Literal(Literal::Bool(b)),
964 ))
965 }
966
967 Some(Value::Object(int)) if int.contains_key("ConstantAbstract") => {
968 if let Some(Value::Object(obj)) = int.get("ConstantAbstract") {
969 if let Some(arr) = obj.get("AbsLitSet") {
970 return parse_abs_lit(arr, scope);
971 } else if let Some(arr) = obj.get("AbsLitMatrix") {
972 return parse_abstract_matrix_as_expr(arr, scope);
973 } else if let Some(arr) = obj.get("AbsLitTuple") {
974 return parse_abs_tuple(arr, scope);
975 } else if let Some(arr) = obj.get("AbsLitRecord") {
976 return parse_abs_record(arr, scope);
977 }
978 }
979 None
980 }
981
982 None => {
985 let int_expr = constant
986 .get("ConstantInt")
987 .and_then(|x| x.as_array())
988 .and_then(|x| x[1].as_i64())
989 .and_then(|x| x.try_into().ok())
990 .map(|x| Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(x))));
991
992 if let e @ Some(_) = int_expr {
993 return e;
994 }
995
996 let bool_expr = constant
997 .get("ConstantBool")
998 .and_then(|x| x.as_bool())
999 .map(|x| Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Bool(x))));
1000
1001 if let e @ Some(_) = bool_expr {
1002 return e;
1003 }
1004
1005 bug!("Unhandled parse_constant {:#?}", constant);
1006 }
1007 otherwise => bug!("Unhandled parse_constant {:#?}", otherwise),
1008 }
1009}