pub fn model_from_json(str: &str, context: Arc<RwLock<Context<'static>>>) -> Result<Model> {

    let mut m = Model::new(context);

    let v: JsonValue = serde_json::from_str(str)?;

    let statements = v["mStatements"]

        .as_array()

        .ok_or(error!("mStatements is not an array"))?;

    for statement in statements {

        let entry = statement

            .as_object()

            .ok_or(error!("mStatements contains a non-object"))?

            .iter()

            .next()

            .ok_or(error!("mStatements contains an empty object"))?;

        match entry.0.as_str() {

            "Declaration" => {

                let decl = entry

                    .1

                    .as_object()

                    .ok_or(error!("Declaration is not an object".to_owned()))?;

                let mut valid_decl: bool = false;

                let scope = m.symbols_ptr_unchecked().clone();

                let model = &mut m;

                for (kind, value) in decl {

                    match kind.as_str() {

                        "FindOrGiven" => {

                            parse_variable(value, &mut model.symbols_mut())?;

                            valid_decl = true;

                            break;

                        "Letting" => {

                            parse_letting(value, &scope)?;

                            valid_decl = true;

                            break;

                if !valid_decl {

                }

            "SuchThat" => {

                let constraints_arr = match entry.1.as_array() {

                    Some(x) => x,

                let constraints: Vec<Expression> = constraints_arr

                    .iter()

                    .map(|x| parse_expression(x, m.symbols_ptr_unchecked()))

                    .collect::<Result<Vec<_>>>()?;

                m.add_constraints(constraints);

    Ok(m)

}

fn parse_variable(v: &JsonValue, symtab: &mut SymbolTable) -> Result<()> {

    let arr = v.as_array().ok_or(error!("FindOrGiven is not an array"))?;

    let name = arr[1]

        .as_object()

        .ok_or(error!("FindOrGiven[1] is not an object"))?["Name"]

        .as_str()

        .ok_or(error!("FindOrGiven[1].Name is not a string"))?;

    let name = Name::User(Ustr::from(name));

    let domain = arr[2]

        .as_object()

        .ok_or(error!("FindOrGiven[2] is not an object"))?

        .iter()

        .next()

        .ok_or(error!("FindOrGiven[2] is an empty object"))?;

    let domain = parse_domain(domain.0, domain.1, symtab)?;

    symtab

        .insert(DeclarationPtr::new_find(name.clone(), domain))

        .ok_or(Error::Parse(format!(

            "Could not add {name} to symbol table as it already exists"

        )))

}

fn parse_letting(v: &JsonValue, scope: &SymbolTablePtr) -> Result<()> {

    let arr = v.as_array().ok_or(error!("Letting is not an array"))?;

    let name = arr[0]

        .as_object()

        .ok_or(error!("Letting[0] is not an object"))?["Name"]

        .as_str()

        .ok_or(error!("Letting[0].Name is not a string"))?;

    let name = Name::User(Ustr::from(name));

    if let Ok(value) = parse_expression(&arr[1], scope) {

        let mut symtab = scope.write();

        symtab

            .insert(DeclarationPtr::new_value_letting(name.clone(), value))

            .ok_or(Error::Parse(format!(

                "Could not add {name} to symbol table as it already exists"

            )))

    } else {

        let domain = &arr[1]

            .as_object()

            .ok_or(error!("Letting[1] is not an object".to_owned()))?["Domain"]

            .as_object()

            .ok_or(error!("Letting[1].Domain is not an object"))?

            .iter()

            .next()

            .ok_or(error!("Letting[1].Domain is an empty object"))?;

        let mut symtab = scope.write();

        let domain = parse_domain(domain.0, domain.1, &mut symtab)?;

        symtab

            .insert(DeclarationPtr::new_domain_letting(name.clone(), domain))

            .ok_or(Error::Parse(format!(

                "Could not add {name} to symbol table as it already exists"

            )))

    }

}

fn parse_domain(

    domain_name: &str,

    domain_value: &JsonValue,

    symbols: &mut SymbolTable,

) -> Result<DomainPtr> {

    match domain_name {

        "DomainInt" => Ok(parse_int_domain(domain_value, symbols)?),

        "DomainBool" => Ok(Domain::bool()),

        "DomainReference" => {

            let name = Name::user(

                domain_value

                    .as_array()

                    .ok_or(error!("DomainReference is not an array"))?[0]

                    .as_object()

                    .ok_or(error!("DomainReference[0] is not an object"))?["Name"]

                    .as_str()

                    .ok_or(error!("DomainReference[0].Name is not a string"))?,

            );

            let ptr = symbols

                .lookup(&name)

                .ok_or(error!(format!("Name {name} not found")))?;

            let dom =

                Domain::reference(ptr).ok_or(error!("Could not construct reference domain"))?;

            Ok(dom)

        }

        "DomainSet" => {

            let dom = domain_value.get(2).and_then(|v| v.as_object());

            let domain_obj = dom.ok_or(error!("DomainSet is missing domain object"))?;

            let domain = domain_obj

                .iter()

                .next()

                .ok_or(Error::Parse("DomainSet is an empty object".to_owned()))?;

            let domain = parse_domain(domain.0.as_str(), domain.1, symbols)?;

            let size = domain_value

                .get(1)

                .and_then(|v| v.as_object())

                .ok_or(error!("Set size attributes is not an object"))?;

            let size = parse_size_attr(size, symbols)?;

            let attr: SetAttr<IntVal> = SetAttr { size };

            Ok(Domain::set(attr, domain))

        }

        "DomainMSet" => {

            let dom = domain_value

                .get(2)

                .and_then(|v| v.as_object())

                .expect("domain object exists");

            let domain = dom

                .iter()

                .next()

                .ok_or(Error::Parse("DomainMSet is an empty object".to_owned()))?;

            let domain = parse_domain(domain.0.as_str(), domain.1, symbols)?;

            let attributes = domain_value

                .get(1)

                .and_then(|v| v.as_array())

                .ok_or(error!("MSet attributes is not a json array"))?;

            let size = attributes

                .first()

                .and_then(|v| v.as_object())

                .ok_or(error!("MSet size attributes is not an object"))?;

            let size = parse_size_attr(size, symbols)?;

            let occurrence = attributes

                .get(1)

                .and_then(|v| v.as_object())

                .ok_or(error!("MSet occurrence attributes is not an object"))?;

            let occurrence = parse_occur_attr(occurrence, symbols)?;

            let attr: MSetAttr<IntVal> = MSetAttr { size, occurrence };

            Ok(Domain::mset(attr, domain))

        }

        "DomainMatrix" => {

            let domain_value = domain_value

                .as_array()

                .ok_or(error!("Domain matrix is not an array"))?;

            let indexed_by_domain = domain_value[0].clone();

            let (index_domain_name, index_domain_value) = indexed_by_domain

                .as_object()

                .ok_or(error!("DomainMatrix[0] is not an object"))?

                .iter()

                .next()

                .ok_or(error!(""))?;

            let (value_domain_name, value_domain_value) = domain_value[1]

                .as_object()

                .ok_or(error!(""))?

                .iter()

                .next()

                .ok_or(error!(""))?;

            let mut index_domains: Vec<DomainPtr> = vec![];

            index_domains.push(parse_domain(

                index_domain_name,

                index_domain_value,

                symbols,

            let mut value_domain = parse_domain(value_domain_name, value_domain_value, symbols)?;

            while let Some((new_value_domain, mut indices)) = value_domain.as_matrix() {

                index_domains.append(&mut indices);

                value_domain = new_value_domain.clone()

            Ok(Domain::matrix(value_domain, index_domains))

        "DomainTuple" => {

            let domain_value = domain_value

                .as_array()

                .ok_or(error!("Domain tuple is not an array"))?;

            let domain = domain_value

                .iter()

                .map(|x| {

                    let domain = x

                        .as_object()

                        .ok_or(error!("DomainTuple[0] is not an object"))?

                        .iter()

                        .next()

                        .ok_or(error!("DomainTuple[0] is an empty object"))?;

                    parse_domain(domain.0, domain.1, symbols)

                })

                .collect::<Result<Vec<DomainPtr>>>()?;

            Ok(Domain::tuple(domain))

        }

        "DomainRecord" => {

            let domain_value = domain_value

                .as_array()

                .ok_or(error!("Domain Record is not a json array"))?;

            let mut record_entries = vec![];

            for item in domain_value {

                let name = item[0]

                    .as_object()

                    .ok_or(error!("FindOrGiven[1] is not an object"))?["Name"]

                    .as_str()

                    .ok_or(error!("FindOrGiven[1].Name is not a string"))?;

                let name = Name::User(Ustr::from(name));

                let domain = item[1]

                    .as_object()

                    .ok_or(error!("FindOrGiven[2] is not an object"))?

                    .iter()

                    .next()

                    .ok_or(error!("FindOrGiven[2] is an empty object"))?;

                let domain = parse_domain(domain.0, domain.1, symbols)?;

                let rec = RecordEntry { name, domain };

                record_entries.push(rec);

            }

            for decl in record_entries

                .iter()

                .cloned()

                .map(DeclarationPtr::new_record_field)

                symbols.insert(decl).ok_or(error!(

                ))?;

            Ok(Domain::record(record_entries))

        }

        "DomainFunction" => {

            let domain = domain_value

                .get(2)

                .and_then(|v| v.as_object())

                .ok_or(error!("Function domain is not an object"))?;

            let domain = domain

                .iter()

                .next()

                .ok_or(Error::Parse("DomainSet is an empty object".to_owned()))?;

            let domain = parse_domain(domain.0.as_str(), domain.1, symbols)?;

            let codomain = domain_value

                .get(3)

                .and_then(|v| v.as_object())

                .ok_or(error!("Function codomain is not an object"))?;

            let codomain = codomain

                .iter()

                .next()

                .ok_or(Error::Parse("DomainSet is an empty object".to_owned()))?;

            let codomain = parse_domain(codomain.0.as_str(), codomain.1, symbols)?;

            let attributes = domain_value

                .get(1)

                .and_then(|v| v.as_array())

                .ok_or(error!("Function attributes is not a json array"))?;

            let size = attributes

                .first()

                .and_then(|v| v.as_object())

                .ok_or(error!("Function size attributes is not an object"))?;

            let size = parse_size_attr(size, symbols)?;

            let partiality = attributes

                .get(1)

                .and_then(|v| v.as_str())

                .ok_or(error!("Function partiality is not a string"))?;

            let partiality = match partiality {

                "PartialityAttr_Partial" => Some(PartialityAttr::Partial),

                "PartialityAttr_Total" => Some(PartialityAttr::Total),

                _ => None,

            };

            let partiality =

                partiality.ok_or(Error::Parse("Partiality is an unknown type".to_owned()))?;

            let jectivity = attributes

                .get(2)

                .and_then(|v| v.as_str())

                .ok_or(error!("Function jectivity is not a string"))?;

            let jectivity = match jectivity {

                "JectivityAttr_Injective" => Some(JectivityAttr::Injective),

                "JectivityAttr_Surjective" => Some(JectivityAttr::Surjective),

                "JectivityAttr_Bijective" => Some(JectivityAttr::Bijective),

                "JectivityAttr_None" => Some(JectivityAttr::None),

                _ => None,

            };

            let jectivity =

                jectivity.ok_or(Error::Parse("Jectivity is an unknown type".to_owned()))?;

            let attr: FuncAttr<IntVal> = FuncAttr {

                size,

                partiality,

                jectivity,

            };

            Ok(Domain::function(attr, domain, codomain))

        _ => Err(Error::Parse(

    }

}

fn parse_size_attr(

    attr_map: &JsonMap<String, JsonValue>,

    symbols: &mut SymbolTable,

) -> Result<Range<IntVal>> {

    let scope = SymbolTablePtr::new();

    *scope.write() = symbols.clone();

    let attr_obj = attr_map

        .iter()

        .next()

        .ok_or(Error::Parse("SizeAttr is an empty object".to_owned()))?;

    match attr_obj.0.as_str() {

        "SizeAttr_None" => Ok(Range::Unbounded),

        "SizeAttr_MinSize" => {

            let size = parse_expression_to_int_val(attr_obj.1, &scope)?;

            Ok(Range::UnboundedR(size))

        }

        "SizeAttr_MaxSize" => {

            let size = parse_expression_to_int_val(attr_obj.1, &scope)?;

            Ok(Range::UnboundedL(size))

        }

        "SizeAttr_MinMaxSize" => {

            let min_max = attr_obj

                .1

                .as_array()

                .ok_or(error!("SizeAttr MinMaxSize is not a json array"))?;

            let min = min_max

                .first()

                .ok_or(error!("SizeAttr Min is not present"))?;

            let min_int = parse_expression_to_int_val(min, &scope)?;

            let max = min_max

                .get(1)

                .ok_or(error!("SizeAttr Max is not present"))?;

            let max_int = parse_expression_to_int_val(max, &scope)?;

            Ok(Range::Bounded(min_int, max_int))

        }

        "SizeAttr_Size" => {

            let size = parse_expression_to_int_val(attr_obj.1, &scope)?;

            Ok(Range::Single(size))

        }

        _ => Err(Error::Parse("SizeAttr is an unknown type".to_owned())),

    }

}

fn parse_occur_attr(

    attr_map: &JsonMap<String, JsonValue>,

    symbols: &mut SymbolTable,

) -> Result<Range<IntVal>> {

    let scope = SymbolTablePtr::new();

    *scope.write() = symbols.clone();

    let attr_obj = attr_map

        .iter()

        .next()

        .ok_or(Error::Parse("OccurAttr is an empty object".to_owned()))?;

    match attr_obj.0.as_str() {

        "OccurAttr_None" => Ok(Range::Unbounded),

        "OccurAttr_MinOccur" => {

            let size_int = parse_expression_to_int_val(attr_obj.1, &scope)?;

            Ok(Range::UnboundedR(size_int))

        }

        "OccurAttr_MaxOccur" => {

            let size_int = parse_expression_to_int_val(attr_obj.1, &scope)?;

            Ok(Range::UnboundedL(size_int))

        }

        "OccurAttr_MinMaxOccur" => {

            let min_max = attr_obj

                .1

                .as_array()

                .ok_or(error!("OccurAttr MinMaxOccur is not a json array"))?;

            let min = min_max

                .first()

                .ok_or(error!("OccurAttr Min is not present"))?;

            let min_int = parse_expression_to_int_val(min, &scope)?;

            let max = min_max

                .get(1)

                .ok_or(error!("OccurAttr Max is not present"))?;

            let max_int = parse_expression_to_int_val(max, &scope)?;

            Ok(Range::Bounded(min_int, max_int))

        }

        "OccurAttr_Size" => {

            let size_int = parse_expression_to_int_val(attr_obj.1, &scope)?;

            Ok(Range::Single(size_int))

        }

        _ => Err(Error::Parse("OccurAttr is an unknown type".to_owned())),

    }

}

fn parse_int_domain(v: &JsonValue, symbols: &SymbolTable) -> Result<DomainPtr> {

    let scope = SymbolTablePtr::new();

    *scope.write() = symbols.clone();

    let mut ranges = Vec::new();

    let arr = v

        .as_array()

        .ok_or(error!("DomainInt is not an array".to_owned()))?[1]

        .as_array()

        .ok_or(error!("DomainInt[1] is not an array".to_owned()))?;

    for range in arr {

        let range = range

            .as_object()

            .ok_or(error!("DomainInt[1] contains a non-object"))?

            .iter()

            .next()

            .ok_or(error!("DomainInt[1] contains an empty object"))?;

        match range.0.as_str() {

            "RangeBounded" => {

                let arr = range

                    .1

                    .as_array()

                    .ok_or(error!("RangeBounded is not an array".to_owned()))?;

                let mut nums = Vec::new();

                for item in arr.iter() {

                    let num = parse_expression_to_int_val(item, &scope)?;

                    nums.push(num);

                }

                let lower = nums

                    .first()

                    .cloned()

                    .ok_or(error!("RangeBounded lower bound missing"))?;

                let upper = nums

                    .get(1)

                    .cloned()

                    .ok_or(error!("RangeBounded upper bound missing"))?;

                ranges.push(Range::Bounded(lower, upper));

            }

            "RangeSingle" => {

                let num = parse_expression_to_int_val(range.1, &scope)?;

                ranges.push(Range::Single(num));

            }

            _ => return throw_error!("DomainInt[1] contains an unknown object"),

        }

    }

    Ok(Domain::int(ranges))

}

fn parse_expression_to_int_val(obj: &JsonValue, scope: &SymbolTablePtr) -> Result<IntVal> {

    parser_trace!("trying to parse domain value as expression: {}", obj);

    let expr = parse_expression(obj, scope)?;

    if let Some(Literal::Int(i)) = expr.clone().into_literal() {

        return Ok(IntVal::Const(i));

    }

    if let Expression::Atomic(_, Atom::Reference(reference)) = &expr

        && let Some(reference_val) = IntVal::new_ref(reference)

        return Ok(reference_val);

    }

    IntVal::new_expr(Moo::new(expr)).ok_or(error!("Could not parse integer expression"))

}

type BinOp = fn(Metadata, Moo<Expression>, Moo<Expression>) -> Expression;

fn binary_operator(op_name: &str) -> Option<BinOp> {

    match op_name {

        "MkOpIn" => Some(Expression::In),

        "MkOpUnion" => Some(Expression::Union),

        "MkOpIntersect" => Some(Expression::Intersect),

        "MkOpSupset" => Some(Expression::Supset),

        "MkOpSupsetEq" => Some(Expression::SupsetEq),

        "MkOpSubset" => Some(Expression::Subset),

        "MkOpSubsetEq" => Some(Expression::SubsetEq),

        "MkOpEq" => Some(Expression::Eq),

        "MkOpNeq" => Some(Expression::Neq),

        "MkOpGeq" => Some(Expression::Geq),

        "MkOpLeq" => Some(Expression::Leq),

        "MkOpGt" => Some(Expression::Gt),

        "MkOpLt" => Some(Expression::Lt),

        "MkOpLexLt" => Some(Expression::LexLt),

        "MkOpLexGt" => Some(Expression::LexGt),

        "MkOpLexLeq" => Some(Expression::LexLeq),

        "MkOpLexGeq" => Some(Expression::LexGeq),

        "MkOpDiv" => Some(Expression::UnsafeDiv),

        "MkOpMod" => Some(Expression::UnsafeMod),

        "MkOpMinus" => Some(Expression::Minus),

        "MkOpImply" => Some(Expression::Imply),

        "MkOpIff" => Some(Expression::Iff),

        "MkOpPow" => Some(Expression::UnsafePow),

        "MkOpImage" => Some(Expression::Image),

        "MkOpImageSet" => Some(Expression::ImageSet),

        "MkOpPreImage" => Some(Expression::PreImage),

        "MkOpInverse" => Some(Expression::Inverse),

        "MkOpRestrict" => Some(Expression::Restrict),

        _ => None,

    }

}

fn unary_operator(op_name: &str) -> Option<UnaryOp> {

    match op_name {

        "MkOpNot" => Some(Expression::Not),

        "MkOpNegate" => Some(Expression::Neg),

        "MkOpTwoBars" => Some(Expression::Abs),

        "MkOpAnd" => Some(Expression::And),

        "MkOpSum" => Some(Expression::Sum),

        "MkOpProduct" => Some(Expression::Product),

        "MkOpOr" => Some(Expression::Or),

        "MkOpMin" => Some(Expression::Min),

        "MkOpMax" => Some(Expression::Max),

        "MkOpAllDiff" => Some(Expression::AllDiff),

        "MkOpToInt" => Some(Expression::ToInt),

        "MkOpDefined" => Some(Expression::Defined),

        "MkOpRange" => Some(Expression::Range),

        _ => None,

    }

}

pub fn parse_expression(obj: &JsonValue, scope: &SymbolTablePtr) -> Result<Expression> {

    let fail = |stage: &str| -> Error {

        Error::Parse(format!(

            "Could not parse expression at stage `{stage}` for json `{obj}`"

        ))

    };

    match obj {

        Value::Object(op) if op.contains_key("Op") => {

            let op_obj = op

                .get("Op")

                .and_then(Value::as_object)

                .ok_or_else(|| fail("Op.as_object"))?;

            let (op_name, _) = op_obj.iter().next().ok_or_else(|| fail("Op.iter().next"))?;

            if op_obj.contains_key("MkOpFlatten") {

                parse_flatten_op(op_obj, scope)

            } else if op_obj.contains_key("MkOpTable") {

                parse_table_op(op_obj, scope)

            } else if op_obj.contains_key("MkOpIndexing") || op_obj.contains_key("MkOpSlicing") {

                parse_indexing_slicing_op(op_obj, scope)

            } else if binary_operator(op_name).is_some() {

                parse_bin_op(op_obj, scope)

            } else if unary_operator(op_name).is_some() {

                parse_unary_op(op_obj, scope)

                Err(fail("Op.unknown"))

            }

        }

        Value::Object(comprehension) if comprehension.contains_key("Comprehension") => {

            parse_comprehension(comprehension, scope.clone(), None)

        }

        Value::Object(refe) if refe.contains_key("Reference") => {

            let ref_arr = refe["Reference"]

                .as_array()

                .ok_or_else(|| fail("Reference.as_array"))?;

            let ref_obj = ref_arr

                .first()

                .and_then(|x| x.as_object())

                .ok_or_else(|| fail("Reference[0].as_object"))?;

            let name = ref_obj

                .get("Name")

                .and_then(|x| x.as_str())

                .ok_or_else(|| fail("Reference[0].Name.as_str"))?;

            let user_name = Name::User(Ustr::from(name));

            let declaration: DeclarationPtr = scope

                .read()

                .lookup(&user_name)

                .ok_or_else(|| fail("Reference.lookup"))?;

            Ok(Expression::Atomic(

                Metadata::new(),

                Atom::Reference(crate::ast::Reference::new(declaration)),

            ))

        }

        Value::Object(abslit) if abslit.contains_key("AbstractLiteral") => {

            let abstract_literal = abslit["AbstractLiteral"]

                .as_object()

                .ok_or_else(|| fail("AbstractLiteral.as_object"))?;

            if abstract_literal.contains_key("AbsLitSet") {

                parse_abs_lit(&abslit["AbstractLiteral"]["AbsLitSet"], scope)

            } else if abstract_literal.contains_key("AbsLitFunction") {

                parse_abs_function(&abslit["AbstractLiteral"]["AbsLitFunction"], scope)

            } else if abstract_literal.contains_key("AbsLitMSet") {

            } else {

                parse_abstract_matrix_as_expr(obj, scope)

            }

        }

        Value::Object(constant) if constant.contains_key("Constant") => {

            parse_constant(constant, scope).or_else(|_| parse_abstract_matrix_as_expr(obj, scope))

        }

        Value::Object(constant) if constant.contains_key("ConstantAbstract") => {

            parse_abstract_matrix_as_expr(obj, scope)

        Value::Object(constant) if constant.contains_key("ConstantInt") => {

            parse_constant(constant, scope)

        Value::Object(constant) if constant.contains_key("ConstantBool") => {

            parse_constant(constant, scope)

        _ => Err(fail("no_match")),

    }

}

fn parse_abs_lit(abs_set: &Value, scope: &SymbolTablePtr) -> Result<Expression> {

    let values = abs_set

        .as_array()

        .ok_or(error!("AbsLitSet is not an array"))?;

    let expressions = values

        .iter()

        .map(|values| parse_expression(values, scope))

        .collect::<Result<Vec<_>>>()?;

    Ok(Expression::AbstractLiteral(

        Metadata::new(),

        AbstractLiteral::Set(expressions),

    ))

}

fn parse_abs_mset(abs_mset: &Value, scope: &SymbolTablePtr) -> Result<Expression> {

    let values = abs_mset

        .as_array()

        .ok_or(error!("AbsLitMSet is not an array"))?;

    let expressions = values

        .iter()

        .map(|values| parse_expression(values, scope))

        .collect::<Result<Vec<_>>>()?;

    Ok(Expression::AbstractLiteral(

        Metadata::new(),

        AbstractLiteral::MSet(expressions),

    ))

}

fn parse_abs_tuple(abs_tuple: &Value, scope: &SymbolTablePtr) -> Result<Expression> {

    let values = abs_tuple

        .as_array()

        .ok_or(error!("AbsLitTuple is not an array"))?;

    let expressions = values

        .iter()

        .map(|values| parse_expression(values, scope))

        .collect::<Result<Vec<_>>>()?;

    Ok(Expression::AbstractLiteral(

        Metadata::new(),

        AbstractLiteral::Tuple(expressions),

    ))

}

fn parse_abs_record(abs_record: &Value, scope: &SymbolTablePtr) -> Result<Expression> {

    let entries = abs_record

        .as_array()

        .ok_or(error!("AbsLitRecord is not an array"))?;

    let mut rec = vec![];

    for entry in entries {

        let entry = entry

            .as_array()

            .ok_or(error!("AbsLitRecord entry is not an array"))?;

        let name = entry[0]

            .as_object()

            .ok_or(error!("AbsLitRecord field name is not an object"))?["Name"]

            .as_str()

            .ok_or(error!("AbsLitRecord field name is not a string"))?;

        let value = parse_expression(&entry[1], scope)?;

        let name = Name::User(Ustr::from(name));

        let rec_entry = RecordValue {

            name: name.clone(),

            value,

        };

        rec.push(rec_entry);

    }

    Ok(Expression::AbstractLiteral(

        Metadata::new(),

        AbstractLiteral::Record(rec),

    ))

}

fn parse_abs_function(abs_function: &Value, scope: &SymbolTablePtr) -> Result<Expression> {

    let entries = abs_function

        .as_array()

        .ok_or(error!("AbsLitFunction is not an array"))?;

    let mut assignments = vec![];

    for entry in entries {

        let entry = entry

            .as_array()

            .ok_or(error!("Explicit function assignment is not an array"))?;

        let expression = entry

            .iter()

            .map(|values| parse_expression(values, scope))

            .collect::<Result<Vec<_>>>()?;

        let domain_value = expression

            .first()

            .ok_or(error!("Invalid function domain"))?;

        let codomain_value = expression

            .get(1)

            .ok_or(error!("Invalid function codomain"))?;

        let tuple = (domain_value.clone(), codomain_value.clone());

        assignments.push(tuple);

    }

    Ok(Expression::AbstractLiteral(

        Metadata::new(),

        AbstractLiteral::Function(assignments),

    ))

}

fn parse_comprehension(

    comprehension: &serde_json::Map<String, Value>,

    scope: SymbolTablePtr,

    comprehension_kind: Option<ACOperatorKind>,

) -> Result<Expression> {

    let fail = |stage: &str| -> Error {

        Error::Parse(format!("Could not parse comprehension at stage `{stage}`"))

    };

    let value = &comprehension["Comprehension"];

    let mut comprehension = ComprehensionBuilder::new(scope.clone());

    let generator_symboltable = comprehension.generator_symboltable();

    let return_expr_symboltable = comprehension.return_expr_symboltable();

    let generators_and_guards_array = value

        .pointer("/1")

        .and_then(Value::as_array)

        .ok_or_else(|| fail("Comprehension.pointer(/1).as_array"))?;

    let generators_and_guards = generators_and_guards_array.iter();

    for gen_or_guard in generators_and_guards {

        let gen_or_guard_obj = gen_or_guard

            .as_object()

            .ok_or_else(|| fail("generator_or_guard.as_object"))?;

        let (name, inner) = gen_or_guard_obj

            .iter()

            .next()

            .ok_or_else(|| fail("generator_or_guard.iter().next"))?;

        comprehension = match name.as_str() {

            "Generator" => {

                let generator_obj = inner

                    .as_object()

                    .ok_or_else(|| fail("Generator.inner.as_object"))?;

                let (name, gen_inner) = generator_obj

                    .iter()

                    .next()

                    .ok_or_else(|| fail("Generator.inner.iter().next"))?;

                match name.as_str() {

                    "GenDomainNoRepr" => {

                        let name = gen_inner

                            .pointer("/0/Single/Name")

                            .and_then(Value::as_str)

                            .ok_or_else(|| {

                                fail("GenDomainNoRepr.pointer(/0/Single/Name).as_str")

                            })?;

                        let domain_obj = gen_inner

                            .pointer("/1")

                            .and_then(Value::as_object)

                            .ok_or_else(|| fail("GenDomainNoRepr.pointer(/1).as_object"))?;

                        let (domain_name, domain_value) = domain_obj

                            .iter()

                            .next()

                            .ok_or_else(|| fail("GenDomainNoRepr.domain.iter().next"))?;

                        let domain = parse_domain(

                            domain_name,

                            domain_value,

                            &mut generator_symboltable.write(),

                        )?;

                        comprehension.generator(DeclarationPtr::new_find(name.into(), domain))

                    }

                    "GenInExpr" => return parse_in_expr_comprehension(scope, value, gen_inner),

                    _ => {

                    }

                }

            }

            "Condition" => {

                let expr = parse_expression(inner, &generator_symboltable)

                    .map_err(|_| fail("Condition.parse_expression"))?;

                comprehension.guard(expr)

            }

    let return_expr_value = value

        .pointer("/0")

        .ok_or_else(|| fail("Comprehension.pointer(/0)"))?;

    let expr = parse_expression(return_expr_value, &return_expr_symboltable)

        .map_err(|_| fail("Comprehension.return_expr.parse_expression"))?;

    Ok(Expression::Comprehension(

        Metadata::new(),

        Moo::new(comprehension.with_return_value(expr, comprehension_kind)),

    ))

}

fn parse_in_expr_comprehension(

    scope: SymbolTablePtr,

    comprehension_value: &Value,

    gen_inner: &Value,

) -> Result<Expression> {

    let fail = |stage: &str| -> Error {

        Error::Parse(format!(

            "Could not parse GenInExpr comprehension at stage `{stage}`"

        ))

    };

    let name = gen_inner

        .pointer("/0/Single/Name")

        .and_then(Value::as_str)

        .ok_or_else(|| fail("GenInExpr.pointer(/0/Single/Name).as_str"))?;

    let generator_expr = gen_inner

        .pointer("/1")

        .ok_or_else(|| fail("GenInExpr.pointer(/1)"))?;

    let expr =

        parse_expression(generator_expr, &scope).map_err(|_| fail("GenInExpr.parse_expression"))?;

    let comprehension =

        AbstractComprehensionBuilder::new(&scope).new_expression_generator(expr, name.into());

    let return_expr_value = comprehension_value

        .pointer("/0")

        .ok_or_else(|| fail("comprehension_value.pointer(/0)"))?;

    let expr = parse_expression(return_expr_value, &comprehension.return_expr_symbols())

        .map_err(|_| fail("GenInExpr.return_expr.parse_expression"))?;

    Ok(Expression::AbstractComprehension(

        Metadata::new(),

        Moo::new(comprehension.with_return_value(expr)),

    ))

}

fn parse_bin_op(

    bin_op: &serde_json::Map<String, Value>,

    scope: &SymbolTablePtr,

) -> Result<Expression> {

    let (key, value) = bin_op

        .into_iter()

        .next()

        .ok_or(error!("Binary op object is empty"))?;

    let constructor = binary_operator(key.as_str())

        .ok_or(error!(format!("Unknown binary operator `{}`", key)))?;

    match &value {

        Value::Array(bin_op_args) if bin_op_args.len() == 2 => {

            let arg1 = parse_expression(&bin_op_args[0], scope)?;

            let arg2 = parse_expression(&bin_op_args[1], scope)?;

            Ok(constructor(Metadata::new(), Moo::new(arg1), Moo::new(arg2)))

        }

        _ => Err(error!("Binary operator arguments are not a 2-array")),

}

fn parse_table_op(

    op: &serde_json::Map<String, Value>,

    scope: &SymbolTablePtr,

) -> Result<Expression> {

    let args = op

        .get("MkOpTable")

        .ok_or(error!("MkOpTable missing"))?

        .as_array()

        .ok_or(error!("MkOpTable is not an array"))?;

    if args.len() != 2 {

        return Err(error!("MkOpTable arguments are not a 2-array"));

    }

    let tuple_expr = parse_expression(&args[0], scope)?;

    let allowed_rows_expr = parse_expression(&args[1], scope)?;

    let (tuple_elems, _) = tuple_expr

        .clone()

        .unwrap_matrix_unchecked()

        .ok_or(error!("MkOpTable first argument is not a matrix"))?;

    let (allowed_rows, _) = allowed_rows_expr

        .clone()

        .unwrap_matrix_unchecked()

        .ok_or(error!("MkOpTable second argument is not a matrix"))?;

    for row_expr in allowed_rows {

        let (row_elems, _) = row_expr

            .unwrap_matrix_unchecked()

            .ok_or(error!("MkOpTable row is not a matrix"))?;

        if row_elems.len() != tuple_elems.len() {

            return Err(error!("MkOpTable row width does not match tuple width"));

        }

    }

    Ok(Expression::Table(

        Metadata::new(),

        Moo::new(tuple_expr),

        Moo::new(allowed_rows_expr),

    ))

}

fn parse_indexing_slicing_op(

    op: &serde_json::Map<String, Value>,

    scope: &SymbolTablePtr,

) -> Result<Expression> {

    let (key, value) = op

        .into_iter()

        .next()

        .ok_or(error!("Indexing/Slicing op object is empty"))?;

    let mut target: Expression;

    let mut indices: Vec<Option<Expression>> = vec![];

    let mut all_known = true;

    match key.as_str() {

        "MkOpIndexing" => {

            match &value {

                Value::Array(op_args) if op_args.len() == 2 => {

                    target = parse_expression(&op_args[0], scope)?;

                    indices.push(Some(parse_expression(&op_args[1], scope)?));

                }

        }

        "MkOpSlicing" => {

            all_known = false;

            match &value {

                Value::Array(op_args) if op_args.len() == 3 => {

                    target = parse_expression(&op_args[0], scope)?;

                    indices.push(None);

        _ => return Err(error!("Unknown indexing/slicing operator")),

    }

    loop {

        match &mut target {

            Expression::UnsafeIndex(_, new_target, new_indices) => {

                indices.extend(new_indices.iter().cloned().rev().map(Some));

                target = Moo::unwrap_or_clone(new_target.clone());

            }

            Expression::UnsafeSlice(_, new_target, new_indices) => {

                all_known = false;

                indices.extend(new_indices.iter().cloned().rev());

                target = Moo::unwrap_or_clone(new_target.clone());

            }

            _ => {

                break;

            }

    }

    indices.reverse();

    if all_known {

            Metadata::new(),

            Moo::new(target),

            indices

                .into_iter()

                .collect::<Option<Vec<_>>>()

                .ok_or(error!("Missing index in fully-known indexing operation"))?,

    } else {

        Ok(Expression::UnsafeSlice(

            Metadata::new(),

            Moo::new(target),

            indices,

        ))

    }

}

fn parse_flatten_op(

    op: &serde_json::Map<String, Value>,

    scope: &SymbolTablePtr,

) -> Result<Expression> {

    let args = op

        .get("MkOpFlatten")

        .ok_or(error!("MkOpFlatten missing"))?

        .as_array()

        .ok_or(error!("MkOpFlatten is not an array"))?;

    let first = args

        .first()

        .ok_or(error!("MkOpFlatten missing first argument"))?;

    let second = args

        .get(1)

        .ok_or(error!("MkOpFlatten missing second argument"))?;

    let n = parse_expression(first, scope).ok();

    let matrix = parse_expression(second, scope)?;

    if let Some(n) = n {

            Metadata::new(),

            Some(Moo::new(n)),

            Moo::new(matrix),

        ))

    } else {

        Ok(Expression::Flatten(Metadata::new(), None, Moo::new(matrix)))

    }

}

fn parse_unary_op(

    un_op: &serde_json::Map<String, Value>,

    scope: &SymbolTablePtr,

) -> Result<Expression> {

    let fail = |stage: &str| -> Error {

    let (key, value) = un_op

        .iter()

        .next()

        .ok_or_else(|| fail("un_op.iter().next"))?;

    let constructor = unary_operator(key.as_str()).ok_or_else(|| fail("unary_operator"))?;

    let arg = match value {

        Value::Object(comprehension) if comprehension.contains_key("Comprehension") => {

            let comprehension_kind = match key.as_str() {

                "MkOpOr" => Some(ACOperatorKind::Or),

                "MkOpAnd" => Some(ACOperatorKind::And),

                "MkOpSum" => Some(ACOperatorKind::Sum),

                "MkOpProduct" => Some(ACOperatorKind::Product),

                _ => None,

            parse_comprehension(comprehension, scope.clone(), comprehension_kind)

                .map_err(|_| fail("value.Comprehension.parse_comprehension"))

        }

        _ => parse_expression(value, scope).map_err(|_| fail("value.parse_expression")),

    }

    .map_err(|_| fail("arg"))?;

    Ok(constructor(Metadata::new(), Moo::new(arg)))

}

fn parse_abstract_matrix_as_expr(

    value: &serde_json::Value,

    scope: &SymbolTablePtr,

) -> Result<Expression> {

    parser_trace!("trying to parse an abstract literal matrix");

    let (values, domain_name, domain_value) =

        if let Some(abs_lit_matrix) = value.pointer("/AbstractLiteral/AbsLitMatrix") {

            parser_trace!(".. found JSON pointer /AbstractLiteral/AbstractLitMatrix");

            let (domain_name, domain_value) = abs_lit_matrix

                .pointer("/0")

                .and_then(Value::as_object)

                .and_then(|x| x.iter().next())

                .ok_or(error!("AbsLitMatrix missing domain"))?;

            let values = abs_lit_matrix

                .pointer("/1")

                .ok_or(error!("AbsLitMatrix missing values"))?;

            Some((values, domain_name, domain_value))

        }

        else if let Some(const_abs_lit_matrix) =

            value.pointer("/Constant/ConstantAbstract/AbsLitMatrix")

        {

            parser_trace!(".. found JSON pointer /Constant/ConstantAbstract/AbsLitMatrix");

            let (domain_name, domain_value) = const_abs_lit_matrix

                .pointer("/0")

                .and_then(Value::as_object)

                .and_then(|x| x.iter().next())

                .ok_or(error!("ConstantAbstract AbsLitMatrix missing domain"))?;

            let values = const_abs_lit_matrix

                .pointer("/1")

                .ok_or(error!("ConstantAbstract AbsLitMatrix missing values"))?;

            Some((values, domain_name, domain_value))

        } else if let Some(const_abs_lit_matrix) = value.pointer("/ConstantAbstract/AbsLitMatrix") {

            parser_trace!(".. found JSON pointer /ConstantAbstract/AbsLitMatrix");

            let (domain_name, domain_value) = const_abs_lit_matrix

                .pointer("/0")

                .and_then(Value::as_object)

                .and_then(|x| x.iter().next())

                .ok_or(error!("ConstantAbstract/AbsLitMatrix missing domain"))?;

            let values = const_abs_lit_matrix

                .pointer("/1")

                .ok_or(error!("ConstantAbstract/AbsLitMatrix missing values"))?;

            Some((values, domain_name, domain_value))

        } else {

            None

        }

        .ok_or(error!("Could not parse abstract literal matrix"))?;

    parser_trace!(".. found in domain and values in JSON:");

    parser_trace!(".. .. index domain name {domain_name}");

    parser_trace!(".. .. values {value}");

    let args_parsed = values

        .as_array()

        .ok_or(error!("Matrix values are not an array"))?

        .iter()

        .map(|x| parse_expression(x, scope))

        .collect::<Result<Vec<Expression>>>()?;

    if !args_parsed.is_empty() {

        parser_trace!(

            ".. successfully parsed values as expressions: {}, ... ",

            args_parsed[0]

        );

    } else {

        parser_trace!(".. successfully parsed empty values ",);

    }

    let mut symbols = scope.write();

    match parse_domain(domain_name, domain_value, &mut symbols) {

        Ok(domain) => {

            parser_trace!("... sucessfully parsed domain as {domain}");

            Ok(into_matrix_expr![args_parsed;domain])

        }

            Ok(into_matrix_expr![args_parsed])

}

fn parse_constant(

    constant: &serde_json::Map<String, Value>,

    scope: &SymbolTablePtr,

) -> Result<Expression> {

    match &constant.get("Constant") {

        Some(Value::Object(int)) if int.contains_key("ConstantInt") => {

            let int_32: i32 = match int["ConstantInt"]

                .as_array()

                .ok_or(error!("ConstantInt is not an array"))?[1]

                .as_i64()

                .ok_or(error!("ConstantInt does not contain int"))?

                .try_into()

            {

                Ok(x) => x,

                Err(_) => return Err(error!("ConstantInt cannot be represented as i32")),

            };

            Ok(Expression::Atomic(

                Metadata::new(),

                Atom::Literal(Literal::Int(int_32)),

            ))

        }

        Some(Value::Object(b)) if b.contains_key("ConstantBool") => {

            let b: bool = b["ConstantBool"]

                .as_bool()

                .ok_or(error!("ConstantBool does not contain bool"))?;

            Ok(Expression::Atomic(

                Metadata::new(),

                Atom::Literal(Literal::Bool(b)),

            ))

        }

        Some(Value::Object(int)) if int.contains_key("ConstantAbstract") => {

            if let Some(Value::Object(obj)) = int.get("ConstantAbstract") {

                if let Some(arr) = obj.get("AbsLitSet") {

                    return parse_abs_lit(arr, scope);

                } else if let Some(arr) = obj.get("AbsLitMSet") {

                    return parse_abs_mset(arr, scope);

                } else if let Some(arr) = obj.get("AbsLitMatrix") {

                    return parse_abstract_matrix_as_expr(arr, scope);

                } else if let Some(arr) = obj.get("AbsLitTuple") {

                    return parse_abs_tuple(arr, scope);

                } else if let Some(arr) = obj.get("AbsLitRecord") {

                    return parse_abs_record(arr, scope);

                } else if let Some(arr) = obj.get("AbsLitFunction") {

                    return parse_abs_function(arr, scope);

                }

            }

            Err(error!("Unhandled ConstantAbstract literal type"))

        }

        None => {

            let int_expr = constant

                .get("ConstantInt")

                .and_then(|x| x.as_array())

                .and_then(|x| x[1].as_i64())

                .and_then(|x| x.try_into().ok())

                .map(|x| Expression::Atomic(Metadata::new(), Atom::Literal(Literal::Int(x))));

            if let Some(expr) = int_expr {

                return Ok(expr);