pub fn expand_native(

    comprehension: Comprehension,

    parent_symbols: &mut SymbolTable,

) -> Result<Vec<Expression>, SolverError> {

    let mut expanded = Vec::new();

    expand_qualifiers(&comprehension, 0, &mut expanded, parent_symbols)?;

    Ok(expanded)

}

fn expand_qualifiers(

    comprehension: &Comprehension,

    qualifier_index: usize,

    expanded: &mut Vec<Expression>,

    parent_symbols: &mut SymbolTable,

) -> Result<(), SolverError> {

    if qualifier_index == comprehension.qualifiers.len() {

        let child_symbols = comprehension.symbols().clone();

        let return_expression =

            concretise_resolved_reference_atoms(comprehension.return_expression.clone());

        let Some(return_expression) = strip_guarded_safe_index_conditions(return_expression) else {

            return Ok(());

        let return_expression = simplify_expression(return_expression);

        let return_expression = lift_machine_references_into_parent_scope(

            return_expression,

            &child_symbols,

            parent_symbols,

        expanded.push(return_expression);

        return Ok(());

    }

    match &comprehension.qualifiers[qualifier_index] {

        ComprehensionQualifier::Generator { ptr } => {

            let name = ptr.name().clone();

            let domain = ptr.domain().expect("generator declaration has domain");

            let values = resolve_generator_values(&name, &domain)?;

            for literal in values {

                with_temporary_quantified_binding(ptr, &literal, || {

                    expand_qualifiers(comprehension, qualifier_index + 1, expanded, parent_symbols)

                })?;

        ComprehensionQualifier::Condition(condition) => {

            if evaluate_guard(condition)? {

                expand_qualifiers(comprehension, qualifier_index + 1, expanded, parent_symbols)?;

            }

    Ok(())

}

fn resolve_generator_values(name: &Name, domain: &DomainPtr) -> Result<Vec<Literal>, SolverError> {

    let resolved = domain.resolve().ok_or_else(|| {

    resolved.values().map(|iter| iter.collect()).map_err(|err| {

}

fn with_temporary_quantified_binding<T>(

    quantified: &DeclarationPtr,

    value: &Literal,

    f: impl FnOnce() -> Result<T, SolverError>,

) -> Result<T, SolverError> {

    let mut targets = vec![quantified.clone()];

    if let DeclarationKind::Quantified(inner) = &*quantified.kind()

        && let Some(generator) = inner.generator()

    }

    let mut originals = Vec::with_capacity(targets.len());

    for mut target in targets {

        let old_kind = target.replace_kind(DeclarationKind::TemporaryValueLetting(

            Expression::Atomic(Metadata::new(), Atom::Literal(value.clone())),

        ));

        originals.push((target, old_kind));

    }

    let result = f();

    for (mut target, old_kind) in originals.into_iter().rev() {

        let _ = target.replace_kind(old_kind);

    }

    result

}

fn evaluate_guard(guard: &Expression) -> Result<bool, SolverError> {

    let simplified = simplify_expression(guard.clone());

    match eval_constant(&simplified) {

        Some(Literal::Bool(value)) => Ok(value),

}

fn concretise_resolved_reference_atoms(expr: Expression) -> Expression {

    expr.transform_bi(&|atom: Atom| match atom {

        Atom::Reference(reference) => reference

            .resolve_constant()

            .map_or_else(|| Atom::Reference(reference), Atom::Literal),

        other => other,

    })

}