gollum-ir 0.4.0

//! PDDL → IR conversion.
//!
//! Converts PDDL [`Domain`] and [`Problem`] AST nodes into Gollum IR types
//! (`IrProgram`, `IrState`, goal terms).

use std::collections::HashMap;
use std::collections::HashSet;

use crate::{IrAction, IrClause, IrMetadata, IrProgram, IrState, IrTerm};

use gollum_pddl::*;
use super::error::PddlIrError;

// ── Object registry ─────────────────────────────────────────────────────────

/// Map from PDDL type name → list of objects of that type.
pub(crate) type ObjectRegistry = HashMap<String, Vec<String>>;

/// Build an object registry from domain constants and problem objects.
///
/// All objects are also available under the root type `"object"`.
pub(crate) fn build_object_registry(
    constants: &[TypedList],
    objects: &[TypedList],
) -> ObjectRegistry {
    let mut reg: ObjectRegistry = HashMap::new();
    for tl in constants.iter().chain(objects.iter()) {
        let ty = type_name_str(tl.type_name.as_ref());
        reg.entry(ty).or_default().extend(tl.items.clone());
    }
    // Every object is also of root type "object".
    let all: Vec<String> = reg.values().flatten().cloned().collect();
    if !all.is_empty() {
        let root = reg.entry("object".into()).or_default();
        for obj in all {
            if !root.contains(&obj) {
                root.push(obj);
            }
        }
    }
    reg
}

// ── PDDL-level substitution (for grounding quantifiers) ────────────────────

type PddlSubstitution = HashMap<String, String>;

fn apply_subst_term(term: &Term, subst: &PddlSubstitution) -> Term {
    match term {
        Term::Variable(v) => match subst.get(v.as_str()) {
            Some(obj) => Term::Name(obj.clone()),
            None => term.clone(),
        },
        Term::Name(_) => term.clone(),
    }
}

fn apply_subst_goal(gd: &GoalDesc, subst: &PddlSubstitution) -> GoalDesc {
    match gd {
        GoalDesc::Atom(pred, args) => GoalDesc::Atom(
            pred.clone(),
            args.iter().map(|t| apply_subst_term(t, subst)).collect(),
        ),
        GoalDesc::Not(inner) => GoalDesc::Not(Box::new(apply_subst_goal(inner, subst))),
        GoalDesc::And(gds) => {
            GoalDesc::And(gds.iter().map(|g| apply_subst_goal(g, subst)).collect())
        }
        GoalDesc::Or(gds) => {
            GoalDesc::Or(gds.iter().map(|g| apply_subst_goal(g, subst)).collect())
        }
        GoalDesc::Equal(a, b) => {
            GoalDesc::Equal(apply_subst_term(a, subst), apply_subst_term(b, subst))
        }
        GoalDesc::Imply(a, b) => GoalDesc::Imply(
            Box::new(apply_subst_goal(a, subst)),
            Box::new(apply_subst_goal(b, subst)),
        ),
        GoalDesc::Forall(params, inner) => {
            let filtered = filter_bound_vars(subst, params);
            GoalDesc::Forall(params.clone(), Box::new(apply_subst_goal(inner, &filtered)))
        }
        GoalDesc::Exists(params, inner) => {
            let filtered = filter_bound_vars(subst, params);
            GoalDesc::Exists(params.clone(), Box::new(apply_subst_goal(inner, &filtered)))
        }
        GoalDesc::FComp(comp, lhs, rhs) => GoalDesc::FComp(
            *comp,
            apply_subst_fexp(lhs, subst),
            apply_subst_fexp(rhs, subst),
        ),
        GoalDesc::Preference(name, inner) => GoalDesc::Preference(
            name.clone(),
            Box::new(apply_subst_goal(inner, subst)),
        ),
        GoalDesc::Empty => GoalDesc::Empty,
    }
}

fn apply_subst_fexp(fe: &FExp, subst: &PddlSubstitution) -> FExp {
    match fe {
        FExp::FHead(fh) => FExp::FHead(apply_subst_fhead(fh, subst)),
        FExp::Negate(inner) => FExp::Negate(Box::new(apply_subst_fexp(inner, subst))),
        FExp::BinaryOp(op, lhs, rhs) => FExp::BinaryOp(
            *op,
            Box::new(apply_subst_fexp(lhs, subst)),
            Box::new(apply_subst_fexp(rhs, subst)),
        ),
        other => other.clone(),
    }
}

fn apply_subst_fhead(fh: &FHead, subst: &PddlSubstitution) -> FHead {
    FHead {
        name: fh.name.clone(),
        args: fh.args.iter().map(|t| apply_subst_term(t, subst)).collect(),
    }
}

fn apply_subst_effect(eff: &Effect, subst: &PddlSubstitution) -> Effect {
    match eff {
        Effect::Add(pred, args) => Effect::Add(
            pred.clone(),
            args.iter().map(|t| apply_subst_term(t, subst)).collect(),
        ),
        Effect::Delete(pred, args) => Effect::Delete(
            pred.clone(),
            args.iter().map(|t| apply_subst_term(t, subst)).collect(),
        ),
        Effect::And(effs) => {
            Effect::And(effs.iter().map(|e| apply_subst_effect(e, subst)).collect())
        }
        Effect::When(cond, inner) => Effect::When(
            apply_subst_goal(cond, subst),
            Box::new(apply_subst_effect(inner, subst)),
        ),
        Effect::Forall(params, inner) => {
            let filtered = filter_bound_vars(subst, params);
            Effect::Forall(params.clone(), Box::new(apply_subst_effect(inner, &filtered)))
        }
        Effect::Assign(fh, fe) => {
            Effect::Assign(apply_subst_fhead(fh, subst), apply_subst_fexp(fe, subst))
        }
        Effect::Increase(fh, fe) => {
            Effect::Increase(apply_subst_fhead(fh, subst), apply_subst_fexp(fe, subst))
        }
        Effect::Decrease(fh, fe) => {
            Effect::Decrease(apply_subst_fhead(fh, subst), apply_subst_fexp(fe, subst))
        }
        Effect::ScaleUp(fh, fe) => {
            Effect::ScaleUp(apply_subst_fhead(fh, subst), apply_subst_fexp(fe, subst))
        }
        Effect::ScaleDown(fh, fe) => {
            Effect::ScaleDown(apply_subst_fhead(fh, subst), apply_subst_fexp(fe, subst))
        }
    }
}

/// Remove bound variables from substitution to avoid shadowing.
fn filter_bound_vars(subst: &PddlSubstitution, params: &[TypedList]) -> PddlSubstitution {
    let bound: HashSet<&str> = params
        .iter()
        .flat_map(|tl| tl.items.iter())
        .map(|s| s.as_str())
        .collect();
    subst
        .iter()
        .filter(|(k, _)| !bound.contains(k.as_str()))
        .map(|(k, v)| (k.clone(), v.clone()))
        .collect()
}

/// Compute all grounding substitutions for a set of typed quantifier variables.
///
/// Returns the Cartesian product of object sets for each variable.
fn compute_substitutions(
    params: &[TypedList],
    registry: &ObjectRegistry,
) -> Result<Vec<PddlSubstitution>, PddlIrError> {
    let mut var_domains: Vec<(String, Vec<String>)> = Vec::new();
    for tl in params {
        let ty = type_name_str(tl.type_name.as_ref());
        let objects = registry.get(&ty).ok_or_else(|| PddlIrError::ReconstructionError {
            reason: format!(
                "no objects of type '{ty}' available for grounding quantifier \
                 (use pddl_to_ir with a Problem to provide objects)"
            ),
        })?;
        if objects.is_empty() {
            return Ok(vec![]);
        }
        for var in &tl.items {
            var_domains.push((var.clone(), objects.clone()));
        }
    }

    let mut substitutions = vec![PddlSubstitution::new()];
    for (var, objects) in &var_domains {
        let mut next = Vec::with_capacity(substitutions.len() * objects.len());
        for subst in &substitutions {
            for obj in objects {
                let mut s = subst.clone();
                s.insert(var.clone(), obj.clone());
                next.push(s);
            }
        }
        substitutions = next;
    }

    Ok(substitutions)
}

// ── Public API ──────────────────────────────────────────────────────────────

/// Convert a PDDL domain + problem pair into IR representations.
///
/// Returns `(program, initial_state, goals)` where:
/// - `program.actions` contains the converted PDDL actions
/// - `program.clauses` contains derived predicates as rules
/// - `initial_state` is built from the problem's `:init` section
/// - `goals` are the flattened goal terms from the problem's `:goal`
pub fn pddl_to_ir(
    domain: &Domain,
    problem: &Problem,
) -> Result<(IrProgram, IrState, Vec<IrTerm>), PddlIrError> {
    let registry = build_object_registry(&domain.constants, &problem.objects);
    let mut program = domain_to_ir_inner(domain, &registry)?;

    // Add object type facts as clauses (useful for grounding).
    for tl in &problem.objects {
        let ty = type_name_str(tl.type_name.as_ref());
        for obj in &tl.items {
            program.clauses.push(IrClause {
                head: IrTerm::Structure {
                    name: ty.clone(),
                    args: vec![IrTerm::Atom(obj.clone())],
                },
                body: vec![],
                metadata: None,
            });
        }
    }

    let initial_state = convert_init(&problem.init)?;
    let goals = convert_goal(&problem.goal, &registry)?;

    Ok((program, initial_state, goals))
}

/// Extended IR result including PDDL 3.0 features (constraints, metric).
#[derive(Debug, Clone)]
pub struct PddlIrResult {
    /// The converted program (actions, clauses).
    pub program: IrProgram,
    /// The initial state from the problem.
    pub initial_state: IrState,
    /// Goal terms from the problem.
    pub goals: Vec<IrTerm>,
    /// Domain-level trajectory constraints (PDDL 3.0).
    pub domain_constraints: Option<IrTerm>,
    /// Problem-level preferences/constraints (PDDL 3.0).
    pub problem_constraints: Vec<IrTerm>,
    /// Optimization metric (PDDL 3.0).
    pub metric: Option<IrTerm>,
}

/// Convert a PDDL domain + problem pair into IR representations, including
/// PDDL 3.0 constraints, preferences, and metric.
pub fn pddl_to_ir_full(
    domain: &Domain,
    problem: &Problem,
) -> Result<PddlIrResult, PddlIrError> {
    let registry = build_object_registry(&domain.constants, &problem.objects);
    let mut program = domain_to_ir_inner(domain, &registry)?;

    for tl in &problem.objects {
        let ty = type_name_str(tl.type_name.as_ref());
        for obj in &tl.items {
            program.clauses.push(IrClause {
                head: IrTerm::Structure {
                    name: ty.clone(),
                    args: vec![IrTerm::Atom(obj.clone())],
                },
                body: vec![],
                metadata: None,
            });
        }
    }

    let initial_state = convert_init(&problem.init)?;
    let goals = convert_goal(&problem.goal, &registry)?;

    let domain_constraints = match &domain.constraints {
        Some(con) => Some(convert_con_gd(con, &registry)?),
        None => None,
    };

    let problem_constraints = match &problem.constraints {
        Some(pcg) => convert_pref_con_gd(pcg, &registry)?,
        None => vec![],
    };

    let metric = match &problem.metric {
        Some(m) => Some(convert_metric(m)?),
        None => None,
    };

    Ok(PddlIrResult {
        program,
        initial_state,
        goals,
        domain_constraints,
        problem_constraints,
        metric,
    })
}

/// Convert a PDDL domain (without a problem) into an `IrProgram`.
///
/// Useful when only the action schemas are needed. Quantifiers that reference
/// types with no known constants will produce an error; use [`pddl_to_ir`]
/// when the problem's objects are needed for grounding.
pub fn domain_to_ir(domain: &Domain) -> Result<IrProgram, PddlIrError> {
    let registry = build_object_registry(&domain.constants, &[]);
    domain_to_ir_inner(domain, &registry)
}

fn domain_to_ir_inner(
    domain: &Domain,
    registry: &ObjectRegistry,
) -> Result<IrProgram, PddlIrError> {
    let mut program = IrProgram::new();

    // Store the type hierarchy so it survives the round-trip.
    for td in &domain.types {
        program.type_hierarchy.push((
            td.names.clone(),
            td.parent.clone(),
        ));
    }

    for action in &domain.actions {
        program.actions.push(convert_action(action, registry)?);
    }

    for dp in &domain.derived_predicates {
        program.clauses.push(convert_derived(dp, registry)?);
    }

    // Add constant type facts as clauses.
    for tl in &domain.constants {
        let ty = type_name_str(tl.type_name.as_ref());
        for c in &tl.items {
            program.clauses.push(IrClause {
                head: IrTerm::Structure {
                    name: ty.clone(),
                    args: vec![IrTerm::Atom(c.clone())],
                },
                body: vec![],
                metadata: None,
            });
        }
    }

    for da in &domain.durative_actions {
        program.actions.push(convert_durative_action(da, registry)?);
    }
    for proc in &domain.processes {
        program.actions.push(convert_process(proc, registry)?);
    }
    for evt in &domain.events {
        program.actions.push(convert_event(evt, registry)?);
    }

    Ok(program)
}

// ── Term conversion ─────────────────────────────────────────────────────────

/// Convert a PDDL term to an IR term.
pub(crate) fn convert_term(term: &Term) -> IrTerm {
    match term {
        Term::Name(s) => IrTerm::Atom(s.clone()),
        Term::Variable(s) => IrTerm::Var(capitalize_var(s)),
    }
}

// ── GoalDesc conversion ─────────────────────────────────────────────────────

/// Convert a single goal description to an IR term.
pub(crate) fn convert_goal_desc(
    gd: &GoalDesc,
    registry: &ObjectRegistry,
) -> Result<IrTerm, PddlIrError> {
    match gd {
        GoalDesc::Atom(pred, args) => Ok(IrTerm::Structure {
            name: pred.clone(),
            args: args.iter().map(convert_term).collect(),
        }),
        GoalDesc::Equal(a, b) => Ok(IrTerm::Structure {
            name: "=".into(),
            args: vec![convert_term(a), convert_term(b)],
        }),
        GoalDesc::Not(inner) => Ok(IrTerm::Structure {
            name: "not".into(),
            args: vec![convert_goal_desc(inner, registry)?],
        }),
        GoalDesc::And(gds) => {
            let converted: Result<Vec<_>, _> =
                gds.iter().map(|g| convert_goal_desc(g, registry)).collect();
            Ok(IrTerm::Structure {
                name: "and".into(),
                args: converted?,
            })
        }
        GoalDesc::Empty => Ok(IrTerm::Atom("true".into())),

        GoalDesc::Forall(params, inner) => {
            // Ground: conjunction of body for each substitution.
            let subs = compute_substitutions(params, registry)?;
            if subs.is_empty() {
                // Vacuously true.
                return Ok(IrTerm::Atom("true".into()));
            }
            let mut terms = Vec::new();
            for sub in &subs {
                let grounded = apply_subst_goal(inner, sub);
                terms.push(convert_goal_desc(&grounded, registry)?);
            }
            if terms.len() == 1 {
                Ok(terms.into_iter().next().unwrap())
            } else {
                Ok(IrTerm::Structure {
                    name: "and".into(),
                    args: terms,
                })
            }
        }
        GoalDesc::Exists(params, inner) => {
            // Ground: disjunction of body for each substitution.
            let subs = compute_substitutions(params, registry)?;
            let mut terms = Vec::new();
            for sub in &subs {
                let grounded = apply_subst_goal(inner, sub);
                terms.push(convert_goal_desc(&grounded, registry)?);
            }
            // or(...) with zero args is vacuously false — the planner will
            // treat it as an unsatisfiable precondition.
            Ok(IrTerm::Structure {
                name: "or".into(),
                args: terms,
            })
        }

        GoalDesc::Or(gds) => {
            let converted: Result<Vec<_>, _> =
                gds.iter().map(|g| convert_goal_desc(g, registry)).collect();
            Ok(IrTerm::Structure {
                name: "or".into(),
                args: converted?,
            })
        }
        GoalDesc::Imply(a, b) => {
            // Rewrite imply(a, b) as or(not(a), b).
            let not_a = IrTerm::Structure {
                name: "not".into(),
                args: vec![convert_goal_desc(a, registry)?],
            };
            let b_term = convert_goal_desc(b, registry)?;
            Ok(IrTerm::Structure {
                name: "or".into(),
                args: vec![not_a, b_term],
            })
        }
        GoalDesc::FComp(comp, lhs, rhs) => {
            let comp_str = match comp {
                Comparator::Eq => "=",
                Comparator::Lt => "<",
                Comparator::Gt => ">",
                Comparator::LtEq => "<=",
                Comparator::GtEq => ">=",
            };
            Ok(IrTerm::Structure {
                name: "fcomp".into(),
                args: vec![
                    IrTerm::Atom(comp_str.into()),
                    convert_fexp(lhs)?,
                    convert_fexp(rhs)?,
                ],
            })
        }
        GoalDesc::Preference(name, inner) => {
            let goal = convert_goal_desc(inner, registry)?;
            let name_term = match name {
                Some(n) => IrTerm::Atom(n.clone()),
                None => IrTerm::Atom("_anon".into()),
            };
            Ok(IrTerm::Structure {
                name: "preference".into(),
                args: vec![name_term, goal],
            })
        }
    }
}

/// Flatten a goal description into a list of IR terms (for precondition / goal context).
///
/// `And(...)` and `Forall(...)` are flattened; a single goal becomes a one-element vec.
pub(crate) fn convert_goal_flat(
    gd: &GoalDesc,
    registry: &ObjectRegistry,
) -> Result<Vec<IrTerm>, PddlIrError> {
    match gd {
        GoalDesc::And(gds) => {
            let mut result = Vec::new();
            for g in gds {
                result.extend(convert_goal_flat(g, registry)?);
            }
            Ok(result)
        }
        GoalDesc::Forall(params, inner) => {
            // Ground and flatten into individual conjuncts.
            let subs = compute_substitutions(params, registry)?;
            let mut result = Vec::new();
            for sub in &subs {
                let grounded = apply_subst_goal(inner, sub);
                result.extend(convert_goal_flat(&grounded, registry)?);
            }
            Ok(result)
        }
        GoalDesc::Empty => Ok(vec![]),
        other => Ok(vec![convert_goal_desc(other, registry)?]),
    }
}

// ── Effect conversion ───────────────────────────────────────────────────────

/// Flatten an effect into a list of IR terms.
pub(crate) fn convert_effect_flat(
    eff: &Effect,
    registry: &ObjectRegistry,
) -> Result<Vec<IrTerm>, PddlIrError> {
    match eff {
        Effect::Add(pred, args) => Ok(vec![IrTerm::Structure {
            name: pred.clone(),
            args: args.iter().map(convert_term).collect(),
        }]),
        Effect::Delete(pred, args) => Ok(vec![IrTerm::Structure {
            name: "not".into(),
            args: vec![IrTerm::Structure {
                name: pred.clone(),
                args: args.iter().map(convert_term).collect(),
            }],
        }]),
        Effect::And(effs) => {
            let mut result = Vec::new();
            for e in effs {
                result.extend(convert_effect_flat(e, registry)?);
            }
            Ok(result)
        }
        Effect::When(cond, eff) => {
            let condition = convert_goal_desc(cond, registry)?;
            let inner_effects = convert_effect_flat(eff, registry)?;
            let effect_term = if inner_effects.len() == 1 {
                inner_effects.into_iter().next().unwrap()
            } else {
                IrTerm::Structure {
                    name: "and".into(),
                    args: inner_effects,
                }
            };
            Ok(vec![IrTerm::Structure {
                name: "when".into(),
                args: vec![condition, effect_term],
            }])
        }
        Effect::Forall(params, inner) => {
            // Ground: expand to flat effects for each substitution.
            let subs = compute_substitutions(params, registry)?;
            let mut result = Vec::new();
            for sub in &subs {
                let grounded = apply_subst_effect(inner, sub);
                result.extend(convert_effect_flat(&grounded, registry)?);
            }
            Ok(result)
        }
        Effect::Assign(fh, fe) => Ok(vec![convert_numeric_effect("assign", fh, fe)?]),
        Effect::Increase(fh, fe) => Ok(vec![convert_numeric_effect("increase", fh, fe)?]),
        Effect::Decrease(fh, fe) => Ok(vec![convert_numeric_effect("decrease", fh, fe)?]),
        Effect::ScaleUp(fh, fe) => Ok(vec![convert_numeric_effect("scale-up", fh, fe)?]),
        Effect::ScaleDown(fh, fe) => Ok(vec![convert_numeric_effect("scale-down", fh, fe)?]),
    }
}

// ── Action conversion ───────────────────────────────────────────────────────

fn convert_action(
    action: &Action,
    registry: &ObjectRegistry,
) -> Result<IrAction, PddlIrError> {
    let parameters: Vec<String> = action
        .parameters
        .iter()
        .flat_map(|tl| tl.items.iter())
        .map(|name| capitalize_var(name))
        .collect();

    let preconditions = match &action.precondition {
        Some(gd) => convert_goal_flat(gd, registry)?,
        None => vec![],
    };

    let effects = match &action.effect {
        Some(eff) => convert_effect_flat(eff, registry)?,
        None => vec![],
    };

    let type_info = extract_parameter_types(&action.parameters);
    let metadata = if type_info.is_empty() {
        None
    } else {
        Some(IrMetadata {
            types: Some(type_info),
            ..IrMetadata::default()
        })
    };

    Ok(IrAction {
        name: action.name.clone(),
        parameters,
        preconditions,
        effects,
        metadata,
    })
}

// ── Durative action conversion ──────────────────────────────────────────────

fn convert_durative_action(
    da: &DurativeAction,
    registry: &ObjectRegistry,
) -> Result<IrAction, PddlIrError> {
    let parameters: Vec<String> = da
        .parameters
        .iter()
        .flat_map(|tl| tl.items.iter())
        .map(|name| capitalize_var(name))
        .collect();

    // Duration constraint → special precondition term(s).
    let mut preconditions = convert_duration_constraint(&da.duration)?;

    // Temporal conditions.
    if let Some(ref cond) = da.condition {
        preconditions.extend(convert_da_gd_flat(cond, registry)?);
    }

    // Temporal effects.
    let effects = match &da.effect {
        Some(eff) => convert_da_effect_flat(eff, registry)?,
        None => vec![],
    };

    let type_info = extract_parameter_types(&da.parameters);
    let metadata = if type_info.is_empty() {
        None
    } else {
        Some(IrMetadata {
            types: Some(type_info),
            ..IrMetadata::default()
        })
    };

    Ok(IrAction {
        name: da.name.clone(),
        parameters,
        preconditions,
        effects,
        metadata,
    })
}

fn convert_duration_constraint(
    dc: &DurationConstraint,
) -> Result<Vec<IrTerm>, PddlIrError> {
    match dc {
        DurationConstraint::Cmp(comp, fe) => {
            let comp_str = match comp {
                Comparator::Eq => "=",
                Comparator::Lt => "<",
                Comparator::Gt => ">",
                Comparator::LtEq => "<=",
                Comparator::GtEq => ">=",
            };
            Ok(vec![IrTerm::Structure {
                name: "duration".into(),
                args: vec![IrTerm::Atom(comp_str.into()), convert_fexp(fe)?],
            }])
        }
        DurationConstraint::And(constraints) => {
            let mut result = Vec::new();
            for c in constraints {
                result.extend(convert_duration_constraint(c)?);
            }
            Ok(result)
        }
    }
}

fn convert_da_gd_flat(
    dagd: &DaGd,
    registry: &ObjectRegistry,
) -> Result<Vec<IrTerm>, PddlIrError> {
    match dagd {
        DaGd::AtStart(gd) => {
            let inner = convert_goal_desc(gd, registry)?;
            Ok(vec![IrTerm::Structure {
                name: "at-start".into(),
                args: vec![inner],
            }])
        }
        DaGd::AtEnd(gd) => {
            let inner = convert_goal_desc(gd, registry)?;
            Ok(vec![IrTerm::Structure {
                name: "at-end".into(),
                args: vec![inner],
            }])
        }
        DaGd::OverAll(gd) => {
            let inner = convert_goal_desc(gd, registry)?;
            Ok(vec![IrTerm::Structure {
                name: "over-all".into(),
                args: vec![inner],
            }])
        }
        DaGd::And(gds) => {
            let mut result = Vec::new();
            for g in gds {
                result.extend(convert_da_gd_flat(g, registry)?);
            }
            Ok(result)
        }
        DaGd::Forall(params, inner) => {
            let subs = compute_substitutions(params, registry)?;
            let mut result = Vec::new();
            for sub in &subs {
                let grounded = apply_subst_da_gd(inner, sub);
                result.extend(convert_da_gd_flat(&grounded, registry)?);
            }
            Ok(result)
        }
        DaGd::Preference(name, inner) => {
            // Wrap the inner DaGd's terms in a preference marker.
            let inner_terms = convert_da_gd_flat(inner, registry)?;
            let name_term = match name {
                Some(n) => IrTerm::Atom(n.clone()),
                None => IrTerm::Atom("_anon".into()),
            };
            let inner_term = if inner_terms.len() == 1 {
                inner_terms.into_iter().next().unwrap()
            } else {
                IrTerm::Structure {
                    name: "and".into(),
                    args: inner_terms,
                }
            };
            Ok(vec![IrTerm::Structure {
                name: "preference".into(),
                args: vec![name_term, inner_term],
            }])
        }
    }
}

fn convert_da_effect_flat(
    daeff: &DaEffect,
    registry: &ObjectRegistry,
) -> Result<Vec<IrTerm>, PddlIrError> {
    match daeff {
        DaEffect::AtStart(eff) => {
            let inner = convert_effect_flat(eff, registry)?;
            Ok(inner
                .into_iter()
                .map(|e| IrTerm::Structure {
                    name: "at-start".into(),
                    args: vec![e],
                })
                .collect())
        }
        DaEffect::AtEnd(eff) => {
            let inner = convert_effect_flat(eff, registry)?;
            Ok(inner
                .into_iter()
                .map(|e| IrTerm::Structure {
                    name: "at-end".into(),
                    args: vec![e],
                })
                .collect())
        }
        DaEffect::And(effs) => {
            let mut result = Vec::new();
            for e in effs {
                result.extend(convert_da_effect_flat(e, registry)?);
            }
            Ok(result)
        }
        DaEffect::Forall(params, inner) => {
            let subs = compute_substitutions(params, registry)?;
            let mut result = Vec::new();
            for sub in &subs {
                let grounded = apply_subst_da_effect(inner, sub);
                result.extend(convert_da_effect_flat(&grounded, registry)?);
            }
            Ok(result)
        }
        DaEffect::When(cond, eff) => {
            let cond_terms = convert_da_gd_flat(cond, registry)?;
            let eff_terms = convert_da_effect_flat(eff, registry)?;
            let cond_term = if cond_terms.len() == 1 {
                cond_terms.into_iter().next().unwrap()
            } else {
                IrTerm::Structure {
                    name: "and".into(),
                    args: cond_terms,
                }
            };
            let eff_term = if eff_terms.len() == 1 {
                eff_terms.into_iter().next().unwrap()
            } else {
                IrTerm::Structure {
                    name: "and".into(),
                    args: eff_terms,
                }
            };
            Ok(vec![IrTerm::Structure {
                name: "when".into(),
                args: vec![cond_term, eff_term],
            }])
        }
        DaEffect::ContinuousIncrease(fh, fe) => Ok(vec![IrTerm::Structure {
            name: "continuous-increase".into(),
            args: vec![convert_fhead(fh), convert_fexp(fe)?],
        }]),
        DaEffect::ContinuousDecrease(fh, fe) => Ok(vec![IrTerm::Structure {
            name: "continuous-decrease".into(),
            args: vec![convert_fhead(fh), convert_fexp(fe)?],
        }]),
    }
}

fn apply_subst_da_gd(dagd: &DaGd, subst: &PddlSubstitution) -> DaGd {
    match dagd {
        DaGd::AtStart(gd) => DaGd::AtStart(apply_subst_goal(gd, subst)),
        DaGd::AtEnd(gd) => DaGd::AtEnd(apply_subst_goal(gd, subst)),
        DaGd::OverAll(gd) => DaGd::OverAll(apply_subst_goal(gd, subst)),
        DaGd::And(gds) => {
            DaGd::And(gds.iter().map(|g| apply_subst_da_gd(g, subst)).collect())
        }
        DaGd::Forall(params, inner) => {
            let filtered = filter_bound_vars(subst, params);
            DaGd::Forall(params.clone(), Box::new(apply_subst_da_gd(inner, &filtered)))
        }
        DaGd::Preference(name, inner) => {
            DaGd::Preference(name.clone(), Box::new(apply_subst_da_gd(inner, subst)))
        }
    }
}

fn apply_subst_da_effect(daeff: &DaEffect, subst: &PddlSubstitution) -> DaEffect {
    match daeff {
        DaEffect::AtStart(eff) => DaEffect::AtStart(apply_subst_effect(eff, subst)),
        DaEffect::AtEnd(eff) => DaEffect::AtEnd(apply_subst_effect(eff, subst)),
        DaEffect::And(effs) => {
            DaEffect::And(effs.iter().map(|e| apply_subst_da_effect(e, subst)).collect())
        }
        DaEffect::Forall(params, inner) => {
            let filtered = filter_bound_vars(subst, params);
            DaEffect::Forall(
                params.clone(),
                Box::new(apply_subst_da_effect(inner, &filtered)),
            )
        }
        DaEffect::When(cond, eff) => DaEffect::When(
            apply_subst_da_gd(cond, subst),
            Box::new(apply_subst_da_effect(eff, subst)),
        ),
        DaEffect::ContinuousIncrease(fh, fe) => {
            DaEffect::ContinuousIncrease(apply_subst_fhead(fh, subst), apply_subst_fexp(fe, subst))
        }
        DaEffect::ContinuousDecrease(fh, fe) => {
            DaEffect::ContinuousDecrease(apply_subst_fhead(fh, subst), apply_subst_fexp(fe, subst))
        }
    }
}

// ── Init conversion ─────────────────────────────────────────────────────────

fn convert_init(inits: &[Init]) -> Result<IrState, PddlIrError> {
    let mut facts = Vec::new();
    for init in inits {
        match init {
            Init::Positive(pred, args) => {
                facts.push(IrTerm::Structure {
                    name: pred.clone(),
                    args: args.iter().map(|a| IrTerm::Atom(a.clone())).collect(),
                });
            }
            Init::Negative(pred, args) => {
                facts.push(IrTerm::Structure {
                    name: "not".into(),
                    args: vec![IrTerm::Structure {
                        name: pred.clone(),
                        args: args.iter().map(|a| IrTerm::Atom(a.clone())).collect(),
                    }],
                });
            }
            Init::FunctionValue(fname, obj_args, val) => {
                // (= (func a b) 5.0) → Structure { "=", [fhead, Float(val)] }
                facts.push(IrTerm::Structure {
                    name: "=".into(),
                    args: vec![
                        IrTerm::Structure {
                            name: fname.clone(),
                            args: obj_args.iter().map(|a| IrTerm::Atom(a.clone())).collect(),
                        },
                        IrTerm::Float(*val),
                    ],
                });
            }
            Init::At(..) => {
                return Err(PddlIrError::UnsupportedFeature {
                    feature: "timed initial literals".into(),
                });
            }
        }
    }
    Ok(IrState::with_facts(facts))
}

/// Flatten the problem goal into a list of IR goal terms.
fn convert_goal(
    goal: &GoalDesc,
    registry: &ObjectRegistry,
) -> Result<Vec<IrTerm>, PddlIrError> {
    convert_goal_flat(goal, registry)
}

// ── Derived predicates ──────────────────────────────────────────────────────

fn convert_derived(
    dp: &DerivedPredicate,
    registry: &ObjectRegistry,
) -> Result<IrClause, PddlIrError> {
    let head_args: Vec<IrTerm> = dp
        .predicate
        .parameters
        .iter()
        .flat_map(|tl| tl.items.iter())
        .map(|name| IrTerm::Var(capitalize_var(name)))
        .collect();
    let head = IrTerm::Structure {
        name: dp.predicate.name.clone(),
        args: head_args,
    };
    let body = convert_goal_flat(&dp.body, registry)?;
    Ok(IrClause {
        head,
        body,
        metadata: None,
    })
}

// ── Numeric fluent helpers ──────────────────────────────────────────────────

/// Convert a PDDL function head to an IR term.
pub(crate) fn convert_fhead(fh: &FHead) -> IrTerm {
    IrTerm::Structure {
        name: fh.name.clone(),
        args: fh.args.iter().map(convert_term).collect(),
    }
}

/// Convert a PDDL function expression to an IR term.
pub(crate) fn convert_fexp(fe: &FExp) -> Result<IrTerm, PddlIrError> {
    match fe {
        FExp::Number(n) => Ok(IrTerm::Float(*n)),
        FExp::FHead(fh) => Ok(convert_fhead(fh)),
        FExp::Negate(inner) => Ok(IrTerm::Structure {
            name: "negate".into(),
            args: vec![convert_fexp(inner)?],
        }),
        FExp::BinaryOp(op, lhs, rhs) => {
            let op_str = match op {
                BinaryOp::Add => "+",
                BinaryOp::Sub => "-",
                BinaryOp::Mul => "*",
                BinaryOp::Div => "/",
            };
            Ok(IrTerm::Structure {
                name: op_str.into(),
                args: vec![convert_fexp(lhs)?, convert_fexp(rhs)?],
            })
        }
        FExp::Duration => Ok(IrTerm::Atom("?duration".into())),
        FExp::Time => Ok(IrTerm::Atom("#t".into())),
        FExp::TotalTime => Ok(IrTerm::Atom("total-time".into())),
        FExp::IsViolated(name) => Ok(IrTerm::Structure {
            name: "is-violated".into(),
            args: vec![IrTerm::Atom(name.clone())],
        }),
    }
}

/// Convert a numeric effect to an IR term.
fn convert_numeric_effect(
    op: &str,
    fh: &FHead,
    fe: &FExp,
) -> Result<IrTerm, PddlIrError> {
    Ok(IrTerm::Structure {
        name: op.into(),
        args: vec![convert_fhead(fh), convert_fexp(fe)?],
    })
}

// ── PDDL+ Process & Event conversion ────────────────────────────────────────

/// Convert a PDDL+ `Process` to an `IrAction` with a `"process"` marker.
///
/// Encoding:
/// - preconditions: `[process-marker, ...preconditions]`
/// - effects: each effect wrapped in `continuous-effect(...)`
fn convert_process(
    proc: &Process,
    registry: &ObjectRegistry,
) -> Result<IrAction, PddlIrError> {
    let parameters: Vec<String> = proc
        .parameters
        .iter()
        .flat_map(|tl| tl.items.iter())
        .map(|name| capitalize_var(name))
        .collect();

    let mut preconditions = vec![IrTerm::Atom("__process".into())];
    preconditions.extend(convert_goal_flat(&proc.precondition, registry)?);

    let mut effects = Vec::new();
    for eff in &proc.effect {
        let flat = convert_effect_flat(eff, registry)?;
        for e in flat {
            effects.push(IrTerm::Structure {
                name: "continuous-effect".into(),
                args: vec![e],
            });
        }
    }

    let type_info = extract_parameter_types(&proc.parameters);
    let metadata = if type_info.is_empty() {
        None
    } else {
        Some(IrMetadata {
            types: Some(type_info),
            ..IrMetadata::default()
        })
    };

    Ok(IrAction {
        name: proc.name.clone(),
        parameters,
        preconditions,
        effects,
        metadata,
    })
}

/// Convert a PDDL+ `Event` to an `IrAction` with an `"event"` marker.
///
/// Encoding:
/// - preconditions: `[event-marker, ...preconditions]`
/// - effects: standard effect encoding (instantaneous)
fn convert_event(
    evt: &Event,
    registry: &ObjectRegistry,
) -> Result<IrAction, PddlIrError> {
    let parameters: Vec<String> = evt
        .parameters
        .iter()
        .flat_map(|tl| tl.items.iter())
        .map(|name| capitalize_var(name))
        .collect();

    let mut preconditions = vec![IrTerm::Atom("__event".into())];
    preconditions.extend(convert_goal_flat(&evt.precondition, registry)?);

    let mut effects = Vec::new();
    for eff in &evt.effect {
        effects.extend(convert_effect_flat(eff, registry)?);
    }

    let type_info = extract_parameter_types(&evt.parameters);
    let metadata = if type_info.is_empty() {
        None
    } else {
        Some(IrMetadata {
            types: Some(type_info),
            ..IrMetadata::default()
        })
    };

    Ok(IrAction {
        name: evt.name.clone(),
        parameters,
        preconditions,
        effects,
        metadata,
    })
}

// ── PDDL 3.0: Constraints, preferences, metrics ────────────────────────────

/// Convert a domain-level trajectory constraint (`ConGd`) to an IR term.
pub(crate) fn convert_con_gd(
    con: &ConGd,
    registry: &ObjectRegistry,
) -> Result<IrTerm, PddlIrError> {
    match con {
        ConGd::And(gds) => {
            let items: Result<Vec<_>, _> = gds.iter().map(|g| convert_con_gd(g, registry)).collect();
            Ok(IrTerm::Structure {
                name: "and".into(),
                args: items?,
            })
        }
        ConGd::Forall(params, inner) => {
            let subs = compute_substitutions(params, registry)?;
            let mut items = Vec::new();
            for sub in &subs {
                let grounded = apply_subst_con_gd(inner, sub);
                items.push(convert_con_gd(&grounded, registry)?);
            }
            if items.len() == 1 {
                Ok(items.into_iter().next().unwrap())
            } else {
                Ok(IrTerm::Structure {
                    name: "and".into(),
                    args: items,
                })
            }
        }
        ConGd::AtEnd(gd) => Ok(IrTerm::Structure {
            name: "at-end".into(),
            args: vec![convert_goal_desc(gd, registry)?],
        }),
        ConGd::Always(gd) => Ok(IrTerm::Structure {
            name: "always".into(),
            args: vec![convert_goal_desc(gd, registry)?],
        }),
        ConGd::Sometime(gd) => Ok(IrTerm::Structure {
            name: "sometime".into(),
            args: vec![convert_goal_desc(gd, registry)?],
        }),
        ConGd::Within(t, gd) => Ok(IrTerm::Structure {
            name: "within".into(),
            args: vec![IrTerm::Float(*t), convert_goal_desc(gd, registry)?],
        }),
        ConGd::AtMostOnce(gd) => Ok(IrTerm::Structure {
            name: "at-most-once".into(),
            args: vec![convert_goal_desc(gd, registry)?],
        }),
        ConGd::SometimeAfter(trigger, target) => Ok(IrTerm::Structure {
            name: "sometime-after".into(),
            args: vec![
                convert_goal_desc(trigger, registry)?,
                convert_goal_desc(target, registry)?,
            ],
        }),
        ConGd::SometimeBefore(trigger, target) => Ok(IrTerm::Structure {
            name: "sometime-before".into(),
            args: vec![
                convert_goal_desc(trigger, registry)?,
                convert_goal_desc(target, registry)?,
            ],
        }),
        ConGd::AlwaysWithin(t, trigger, target) => Ok(IrTerm::Structure {
            name: "always-within".into(),
            args: vec![
                IrTerm::Float(*t),
                convert_goal_desc(trigger, registry)?,
                convert_goal_desc(target, registry)?,
            ],
        }),
        ConGd::HoldDuring(t1, t2, gd) => Ok(IrTerm::Structure {
            name: "hold-during".into(),
            args: vec![
                IrTerm::Float(*t1),
                IrTerm::Float(*t2),
                convert_goal_desc(gd, registry)?,
            ],
        }),
        ConGd::HoldAfter(t, gd) => Ok(IrTerm::Structure {
            name: "hold-after".into(),
            args: vec![IrTerm::Float(*t), convert_goal_desc(gd, registry)?],
        }),
    }
}

/// Convert a problem-level preference/constraint (`PrefConGd`) to IR terms.
pub(crate) fn convert_pref_con_gd(
    pcg: &PrefConGd,
    registry: &ObjectRegistry,
) -> Result<Vec<IrTerm>, PddlIrError> {
    match pcg {
        PrefConGd::And(gds) => {
            let mut result = Vec::new();
            for g in gds {
                result.extend(convert_pref_con_gd(g, registry)?);
            }
            Ok(result)
        }
        PrefConGd::Forall(params, inner) => {
            let subs = compute_substitutions(params, registry)?;
            let mut result = Vec::new();
            for sub in &subs {
                let grounded = apply_subst_pref_con_gd(inner, sub);
                result.extend(convert_pref_con_gd(&grounded, registry)?);
            }
            Ok(result)
        }
        PrefConGd::Preference(name, con) => {
            let name_term = match name {
                Some(n) => IrTerm::Atom(n.clone()),
                None => IrTerm::Atom("_anon".into()),
            };
            let con_term = convert_con_gd(con, registry)?;
            Ok(vec![IrTerm::Structure {
                name: "preference".into(),
                args: vec![name_term, con_term],
            }])
        }
        PrefConGd::Goal(gd) => {
            Ok(vec![convert_goal_desc(gd, registry)?])
        }
    }
}

/// Convert a metric specification to an IR term.
pub(crate) fn convert_metric(metric: &MetricSpec) -> Result<IrTerm, PddlIrError> {
    let opt = match metric.optimization {
        Optimization::Minimize => "minimize",
        Optimization::Maximize => "maximize",
    };
    Ok(IrTerm::Structure {
        name: "metric".into(),
        args: vec![IrTerm::Atom(opt.into()), convert_fexp(&metric.expression)?],
    })
}

fn apply_subst_con_gd(con: &ConGd, subst: &PddlSubstitution) -> ConGd {
    match con {
        ConGd::And(gds) => ConGd::And(gds.iter().map(|g| apply_subst_con_gd(g, subst)).collect()),
        ConGd::Forall(params, inner) => {
            let filtered = filter_bound_vars(subst, params);
            ConGd::Forall(params.clone(), Box::new(apply_subst_con_gd(inner, &filtered)))
        }
        ConGd::AtEnd(gd) => ConGd::AtEnd(apply_subst_goal(gd, subst)),
        ConGd::Always(gd) => ConGd::Always(apply_subst_goal(gd, subst)),
        ConGd::Sometime(gd) => ConGd::Sometime(apply_subst_goal(gd, subst)),
        ConGd::Within(t, gd) => ConGd::Within(*t, apply_subst_goal(gd, subst)),
        ConGd::AtMostOnce(gd) => ConGd::AtMostOnce(apply_subst_goal(gd, subst)),
        ConGd::SometimeAfter(a, b) => ConGd::SometimeAfter(
            apply_subst_goal(a, subst),
            apply_subst_goal(b, subst),
        ),
        ConGd::SometimeBefore(a, b) => ConGd::SometimeBefore(
            apply_subst_goal(a, subst),
            apply_subst_goal(b, subst),
        ),
        ConGd::AlwaysWithin(t, a, b) => ConGd::AlwaysWithin(
            *t,
            apply_subst_goal(a, subst),
            apply_subst_goal(b, subst),
        ),
        ConGd::HoldDuring(t1, t2, gd) => {
            ConGd::HoldDuring(*t1, *t2, apply_subst_goal(gd, subst))
        }
        ConGd::HoldAfter(t, gd) => ConGd::HoldAfter(*t, apply_subst_goal(gd, subst)),
    }
}

fn apply_subst_pref_con_gd(pcg: &PrefConGd, subst: &PddlSubstitution) -> PrefConGd {
    match pcg {
        PrefConGd::And(gds) => {
            PrefConGd::And(gds.iter().map(|g| apply_subst_pref_con_gd(g, subst)).collect())
        }
        PrefConGd::Forall(params, inner) => {
            let filtered = filter_bound_vars(subst, params);
            PrefConGd::Forall(
                params.clone(),
                Box::new(apply_subst_pref_con_gd(inner, &filtered)),
            )
        }
        PrefConGd::Preference(name, con) => {
            PrefConGd::Preference(name.clone(), apply_subst_con_gd(con, subst))
        }
        PrefConGd::Goal(gd) => PrefConGd::Goal(apply_subst_goal(gd, subst)),
    }
}

// ── Helpers ─────────────────────────────────────────────────────────────────

/// PDDL variable name (lowercase, no `?`) → IR variable name (capitalized).
pub(crate) fn capitalize_var(name: &str) -> String {
    let mut chars = name.chars();
    match chars.next() {
        None => String::new(),
        Some(c) => c.to_uppercase().collect::<String>() + chars.as_str(),
    }
}

/// Extract ordered type names from a typed parameter list.
fn extract_parameter_types(params: &[TypedList]) -> Vec<String> {
    let mut types = Vec::new();
    let mut all_untyped = true;
    for tl in params {
        let ty = type_name_str(tl.type_name.as_ref());
        if tl.type_name.is_some() {
            all_untyped = false;
        }
        for _ in &tl.items {
            types.push(ty.clone());
        }
    }
    if all_untyped {
        Vec::new()
    } else {
        types
    }
}

/// Get a type name string from an optional Type reference.
fn type_name_str(ty: Option<&Type>) -> String {
    match ty {
        Some(Type::Simple(s)) => s.clone(),
        Some(Type::Either(names)) => names.join("|"),
        None => "object".into(),
    }
}

// ── Tests ───────────────────────────────────────────────────────────────────

#[cfg(test)]
mod tests {
    use super::*;

    /// Empty registry for tests that don't need grounding.
    fn no_objects() -> ObjectRegistry {
        ObjectRegistry::new()
    }

    #[test]
    fn test_convert_term_name() {
        assert_eq!(
            convert_term(&Term::Name("room1".into())),
            IrTerm::Atom("room1".into())
        );
    }

    #[test]
    fn test_convert_term_variable() {
        assert_eq!(
            convert_term(&Term::Variable("from".into())),
            IrTerm::Var("From".into())
        );
    }

    #[test]
    fn test_capitalize_var() {
        assert_eq!(capitalize_var("x"), "X");
        assert_eq!(capitalize_var("from"), "From");
        assert_eq!(capitalize_var("from-waypoint"), "From-waypoint");
    }

    #[test]
    fn test_convert_goal_atom() {
        let gd = GoalDesc::Atom("at".into(), vec![Term::Name("a".into())]);
        let ir = convert_goal_desc(&gd, &no_objects()).unwrap();
        assert_eq!(
            ir,
            IrTerm::Structure {
                name: "at".into(),
                args: vec![IrTerm::Atom("a".into())],
            }
        );
    }

    #[test]
    fn test_convert_goal_not() {
        let gd = GoalDesc::Not(Box::new(GoalDesc::Atom(
            "clear".into(),
            vec![Term::Variable("x".into())],
        )));
        let ir = convert_goal_desc(&gd, &no_objects()).unwrap();
        assert_eq!(
            ir,
            IrTerm::Structure {
                name: "not".into(),
                args: vec![IrTerm::Structure {
                    name: "clear".into(),
                    args: vec![IrTerm::Var("X".into())],
                }],
            }
        );
    }

    #[test]
    fn test_convert_goal_and_flattens() {
        let gd = GoalDesc::And(vec![
            GoalDesc::Atom("a".into(), vec![]),
            GoalDesc::Atom("b".into(), vec![]),
        ]);
        let flat = convert_goal_flat(&gd, &no_objects()).unwrap();
        assert_eq!(flat.len(), 2);
    }

    #[test]
    fn test_convert_effect_add() {
        let eff =
            Effect::Add("on".into(), vec![Term::Variable("x".into()), Term::Variable("y".into())]);
        let ir = convert_effect_flat(&eff, &no_objects()).unwrap();
        assert_eq!(ir.len(), 1);
        assert_eq!(
            ir[0],
            IrTerm::Structure {
                name: "on".into(),
                args: vec![IrTerm::Var("X".into()), IrTerm::Var("Y".into())],
            }
        );
    }

    #[test]
    fn test_convert_effect_delete() {
        let eff = Effect::Delete("on".into(), vec![Term::Variable("x".into())]);
        let ir = convert_effect_flat(&eff, &no_objects()).unwrap();
        assert_eq!(ir.len(), 1);
        assert_eq!(
            ir[0],
            IrTerm::Structure {
                name: "not".into(),
                args: vec![IrTerm::Structure {
                    name: "on".into(),
                    args: vec![IrTerm::Var("X".into())],
                }],
            }
        );
    }

    #[test]
    fn test_convert_effect_and_flattens() {
        let eff = Effect::And(vec![
            Effect::Add("a".into(), vec![]),
            Effect::And(vec![
                Effect::Add("b".into(), vec![]),
                Effect::Delete("c".into(), vec![]),
            ]),
        ]);
        let ir = convert_effect_flat(&eff, &no_objects()).unwrap();
        assert_eq!(ir.len(), 3);
    }

    #[test]
    fn test_convert_action_strips() {
        let action = Action {
            name: "move".into(),
            parameters: vec![
                TypedList {
                    items: vec!["v".into()],
                    type_name: Some(Type::Simple("vehicle".into())),
                },
                TypedList {
                    items: vec!["from".into(), "to".into()],
                    type_name: Some(Type::Simple("location".into())),
                },
            ],
            precondition: Some(GoalDesc::Atom(
                "at".into(),
                vec![Term::Variable("v".into()), Term::Variable("from".into())],
            )),
            effect: Some(Effect::And(vec![
                Effect::Add(
                    "at".into(),
                    vec![Term::Variable("v".into()), Term::Variable("to".into())],
                ),
                Effect::Delete(
                    "at".into(),
                    vec![Term::Variable("v".into()), Term::Variable("from".into())],
                ),
            ])),
        };

        let ir = convert_action(&action, &no_objects()).unwrap();
        assert_eq!(ir.name, "move");
        assert_eq!(ir.parameters, vec!["V", "From", "To"]);
        assert_eq!(ir.preconditions.len(), 1);
        assert_eq!(ir.effects.len(), 2);
        let types = ir.metadata.as_ref().unwrap().types.as_ref().unwrap();
        assert_eq!(types, &["vehicle", "location", "location"]);
    }

    #[test]
    fn test_convert_action_no_precondition() {
        let action = Action {
            name: "noop".into(),
            parameters: vec![],
            precondition: None,
            effect: None,
        };
        let ir = convert_action(&action, &no_objects()).unwrap();
        assert!(ir.preconditions.is_empty());
        assert!(ir.effects.is_empty());
        assert!(ir.metadata.is_none());
    }

    #[test]
    fn test_convert_init_positive() {
        let inits = vec![Init::Positive("on".into(), vec!["a".into(), "b".into()])];
        let state = convert_init(&inits).unwrap();
        assert_eq!(state.fact_count(), 1);
        assert!(state.contains(&IrTerm::Structure {
            name: "on".into(),
            args: vec![IrTerm::Atom("a".into()), IrTerm::Atom("b".into())],
        }));
    }

    #[test]
    fn test_convert_init_negative() {
        let inits = vec![Init::Negative("on".into(), vec!["a".into()])];
        let state = convert_init(&inits).unwrap();
        assert_eq!(state.fact_count(), 1);
    }

    #[test]
    fn test_convert_goal_desc_to_goals() {
        let goal = GoalDesc::And(vec![
            GoalDesc::Atom("on".into(), vec![Term::Name("a".into()), Term::Name("b".into())]),
            GoalDesc::Atom("clear".into(), vec![Term::Name("a".into())]),
        ]);
        let goals = convert_goal(&goal, &no_objects()).unwrap();
        assert_eq!(goals.len(), 2);
    }

    #[test]
    fn test_convert_derived_predicate() {
        let dp = DerivedPredicate {
            predicate: AtomicFormulaSkeleton {
                name: "reachable".into(),
                parameters: vec![TypedList {
                    items: vec!["x".into()],
                    type_name: None,
                }],
            },
            body: GoalDesc::Atom("connected".into(), vec![Term::Variable("x".into())]),
        };
        let clause = convert_derived(&dp, &no_objects()).unwrap();
        match &clause.head {
            IrTerm::Structure { name, args } => {
                assert_eq!(name, "reachable");
                assert_eq!(args, &[IrTerm::Var("X".into())]);
            }
            _ => panic!("expected Structure"),
        }
        assert_eq!(clause.body.len(), 1);
    }

    #[test]
    fn test_convert_when_effect_single() {
        let eff = Effect::When(
            GoalDesc::Atom("fragile".into(), vec![Term::Variable("x".into())]),
            Box::new(Effect::Add("broken".into(), vec![Term::Variable("x".into())])),
        );
        let ir = convert_effect_flat(&eff, &no_objects()).unwrap();
        assert_eq!(ir.len(), 1);
        assert_eq!(
            ir[0],
            IrTerm::Structure {
                name: "when".into(),
                args: vec![
                    IrTerm::Structure {
                        name: "fragile".into(),
                        args: vec![IrTerm::Var("X".into())],
                    },
                    IrTerm::Structure {
                        name: "broken".into(),
                        args: vec![IrTerm::Var("X".into())],
                    },
                ],
            }
        );
    }

    #[test]
    fn test_convert_when_effect_multiple_inner() {
        let eff = Effect::When(
            GoalDesc::Atom("heavy".into(), vec![]),
            Box::new(Effect::And(vec![
                Effect::Add("damaged".into(), vec![]),
                Effect::Delete("intact".into(), vec![]),
            ])),
        );
        let ir = convert_effect_flat(&eff, &no_objects()).unwrap();
        assert_eq!(ir.len(), 1);
        match &ir[0] {
            IrTerm::Structure { name, args } => {
                assert_eq!(name, "when");
                assert_eq!(args.len(), 2);
                match &args[1] {
                    IrTerm::Structure { name, args } => {
                        assert_eq!(name, "and");
                        assert_eq!(args.len(), 2);
                    }
                    _ => panic!("expected and structure"),
                }
            }
            _ => panic!("expected when structure"),
        }
    }

    #[test]
    fn test_convert_when_effect_with_not_condition() {
        let eff = Effect::When(
            GoalDesc::Not(Box::new(GoalDesc::Atom("locked".into(), vec![]))),
            Box::new(Effect::Add("open".into(), vec![])),
        );
        let ir = convert_effect_flat(&eff, &no_objects()).unwrap();
        assert_eq!(ir.len(), 1);
        match &ir[0] {
            IrTerm::Structure { name, args } if name == "when" => {
                assert_eq!(
                    args[0],
                    IrTerm::Structure {
                        name: "not".into(),
                        args: vec![IrTerm::Structure {
                            name: "locked".into(),
                            args: vec![],
                        }],
                    }
                );
            }
            _ => panic!("expected when structure"),
        }
    }

    #[test]
    fn test_typed_parameters_in_metadata() {
        let action = Action {
            name: "pick".into(),
            parameters: vec![TypedList {
                items: vec!["obj".into()],
                type_name: Some(Type::Simple("block".into())),
            }],
            precondition: None,
            effect: None,
        };
        let ir = convert_action(&action, &no_objects()).unwrap();
        let types = ir.metadata.as_ref().unwrap().types.as_ref().unwrap();
        assert_eq!(types, &["block"]);
    }

    #[test]
    fn test_pddl_to_ir_blocksworld() {
        let domain = Domain {
            name: "blocksworld".into(),
            requirements: vec![Requirement::Strips],
            predicates: vec![],
            actions: vec![Action {
                name: "pick-up".into(),
                parameters: vec![TypedList {
                    items: vec!["x".into()],
                    type_name: None,
                }],
                precondition: Some(GoalDesc::And(vec![
                    GoalDesc::Atom("clear".into(), vec![Term::Variable("x".into())]),
                    GoalDesc::Atom("on-table".into(), vec![Term::Variable("x".into())]),
                    GoalDesc::Atom("arm-empty".into(), vec![]),
                ])),
                effect: Some(Effect::And(vec![
                    Effect::Add("holding".into(), vec![Term::Variable("x".into())]),
                    Effect::Delete("clear".into(), vec![Term::Variable("x".into())]),
                    Effect::Delete("on-table".into(), vec![Term::Variable("x".into())]),
                    Effect::Delete("arm-empty".into(), vec![]),
                ])),
            }],
            ..Domain::default()
        };

        let problem = Problem {
            name: "bw-1".into(),
            domain_name: "blocksworld".into(),
            init: vec![
                Init::Positive("on-table".into(), vec!["a".into()]),
                Init::Positive("clear".into(), vec!["a".into()]),
                Init::Positive("arm-empty".into(), vec![]),
            ],
            goal: GoalDesc::Atom("holding".into(), vec![Term::Name("a".into())]),
            ..Problem::default()
        };

        let (program, state, goals) = pddl_to_ir(&domain, &problem).unwrap();
        assert_eq!(program.actions.len(), 1);
        assert_eq!(program.actions[0].name, "pick-up");
        assert_eq!(state.fact_count(), 3);
        assert_eq!(goals.len(), 1);
    }

    // ── Quantifier grounding tests ──────────────────────────────────────────

    fn pkg_registry() -> ObjectRegistry {
        let mut reg = ObjectRegistry::new();
        reg.insert("package".into(), vec!["pkg1".into(), "pkg2".into()]);
        reg.insert("location".into(), vec!["loc1".into(), "loc2".into()]);
        reg.insert(
            "object".into(),
            vec![
                "pkg1".into(),
                "pkg2".into(),
                "loc1".into(),
                "loc2".into(),
            ],
        );
        reg
    }

    #[test]
    fn test_build_object_registry() {
        let objects = vec![
            TypedList {
                items: vec!["pkg1".into(), "pkg2".into()],
                type_name: Some(Type::Simple("package".into())),
            },
            TypedList {
                items: vec!["loc1".into()],
                type_name: Some(Type::Simple("location".into())),
            },
        ];
        let reg = build_object_registry(&[], &objects);
        assert_eq!(reg["package"], vec!["pkg1", "pkg2"]);
        assert_eq!(reg["location"], vec!["loc1"]);
        assert!(reg["object"].contains(&"pkg1".to_string()));
        assert!(reg["object"].contains(&"loc1".to_string()));
    }

    #[test]
    fn test_compute_substitutions_single_var() {
        let params = vec![TypedList {
            items: vec!["x".into()],
            type_name: Some(Type::Simple("package".into())),
        }];
        let subs = compute_substitutions(&params, &pkg_registry()).unwrap();
        assert_eq!(subs.len(), 2);
        assert_eq!(subs[0]["x"], "pkg1");
        assert_eq!(subs[1]["x"], "pkg2");
    }

    #[test]
    fn test_compute_substitutions_cartesian() {
        let params = vec![
            TypedList {
                items: vec!["x".into()],
                type_name: Some(Type::Simple("package".into())),
            },
            TypedList {
                items: vec!["l".into()],
                type_name: Some(Type::Simple("location".into())),
            },
        ];
        let subs = compute_substitutions(&params, &pkg_registry()).unwrap();
        // 2 packages × 2 locations = 4
        assert_eq!(subs.len(), 4);
    }

    #[test]
    fn test_forall_precondition_grounds_to_conjunction() {
        let reg = pkg_registry();
        // (forall (?x - package) (ready ?x))
        let gd = GoalDesc::Forall(
            vec![TypedList {
                items: vec!["x".into()],
                type_name: Some(Type::Simple("package".into())),
            }],
            Box::new(GoalDesc::Atom("ready".into(), vec![Term::Variable("x".into())])),
        );
        let flat = convert_goal_flat(&gd, &reg).unwrap();
        assert_eq!(flat.len(), 2);
        assert_eq!(
            flat[0],
            IrTerm::Structure {
                name: "ready".into(),
                args: vec![IrTerm::Atom("pkg1".into())],
            }
        );
        assert_eq!(
            flat[1],
            IrTerm::Structure {
                name: "ready".into(),
                args: vec![IrTerm::Atom("pkg2".into())],
            }
        );
    }

    #[test]
    fn test_exists_precondition_grounds_to_disjunction() {
        let reg = pkg_registry();
        // (exists (?x - package) (damaged ?x))
        let gd = GoalDesc::Exists(
            vec![TypedList {
                items: vec!["x".into()],
                type_name: Some(Type::Simple("package".into())),
            }],
            Box::new(GoalDesc::Atom("damaged".into(), vec![Term::Variable("x".into())])),
        );
        let ir = convert_goal_desc(&gd, &reg).unwrap();
        match &ir {
            IrTerm::Structure { name, args } => {
                assert_eq!(name, "or");
                assert_eq!(args.len(), 2);
                assert_eq!(
                    args[0],
                    IrTerm::Structure {
                        name: "damaged".into(),
                        args: vec![IrTerm::Atom("pkg1".into())],
                    }
                );
            }
            _ => panic!("expected or structure"),
        }
    }

    #[test]
    fn test_forall_effect_grounds_to_multiple_effects() {
        let reg = pkg_registry();
        // (forall (?x - package) (delivered ?x))
        let eff = Effect::Forall(
            vec![TypedList {
                items: vec!["x".into()],
                type_name: Some(Type::Simple("package".into())),
            }],
            Box::new(Effect::Add("delivered".into(), vec![Term::Variable("x".into())])),
        );
        let ir = convert_effect_flat(&eff, &reg).unwrap();
        assert_eq!(ir.len(), 2);
        assert_eq!(
            ir[0],
            IrTerm::Structure {
                name: "delivered".into(),
                args: vec![IrTerm::Atom("pkg1".into())],
            }
        );
        assert_eq!(
            ir[1],
            IrTerm::Structure {
                name: "delivered".into(),
                args: vec![IrTerm::Atom("pkg2".into())],
            }
        );
    }

    #[test]
    fn test_forall_effect_with_when() {
        let reg = pkg_registry();
        // (forall (?x - package) (when (fragile ?x) (broken ?x)))
        let eff = Effect::Forall(
            vec![TypedList {
                items: vec!["x".into()],
                type_name: Some(Type::Simple("package".into())),
            }],
            Box::new(Effect::When(
                GoalDesc::Atom("fragile".into(), vec![Term::Variable("x".into())]),
                Box::new(Effect::Add("broken".into(), vec![Term::Variable("x".into())])),
            )),
        );
        let ir = convert_effect_flat(&eff, &reg).unwrap();
        assert_eq!(ir.len(), 2);
        // Each should be when(fragile(pkgN), broken(pkgN))
        for (i, pkg) in ["pkg1", "pkg2"].iter().enumerate() {
            match &ir[i] {
                IrTerm::Structure { name, args } if name == "when" => {
                    assert_eq!(
                        args[0],
                        IrTerm::Structure {
                            name: "fragile".into(),
                            args: vec![IrTerm::Atom(pkg.to_string())],
                        }
                    );
                }
                _ => panic!("expected when structure"),
            }
        }
    }

    #[test]
    fn test_forall_empty_domain_is_vacuously_true() {
        let mut reg = ObjectRegistry::new();
        reg.insert("unicorn".into(), vec![]);
        let gd = GoalDesc::Forall(
            vec![TypedList {
                items: vec!["x".into()],
                type_name: Some(Type::Simple("unicorn".into())),
            }],
            Box::new(GoalDesc::Atom("magical".into(), vec![Term::Variable("x".into())])),
        );
        let flat = convert_goal_flat(&gd, &reg).unwrap();
        assert!(flat.is_empty()); // vacuously true → no preconditions
    }

    #[test]
    fn test_exists_empty_domain_produces_empty_or() {
        let mut reg = ObjectRegistry::new();
        reg.insert("unicorn".into(), vec![]);
        let gd = GoalDesc::Exists(
            vec![TypedList {
                items: vec!["x".into()],
                type_name: Some(Type::Simple("unicorn".into())),
            }],
            Box::new(GoalDesc::Atom("magical".into(), vec![Term::Variable("x".into())])),
        );
        let ir = convert_goal_desc(&gd, &reg).unwrap();
        match &ir {
            IrTerm::Structure { name, args } => {
                assert_eq!(name, "or");
                assert!(args.is_empty()); // or() with no args = false
            }
            _ => panic!("expected or structure"),
        }
    }

    #[test]
    fn test_pddl_to_ir_with_forall_precondition() {
        // ADL domain: action requires all packages ready
        let domain = Domain {
            name: "logistics".into(),
            actions: vec![Action {
                name: "ship-all".into(),
                parameters: vec![],
                precondition: Some(GoalDesc::Forall(
                    vec![TypedList {
                        items: vec!["p".into()],
                        type_name: Some(Type::Simple("package".into())),
                    }],
                    Box::new(GoalDesc::Atom(
                        "ready".into(),
                        vec![Term::Variable("p".into())],
                    )),
                )),
                effect: Some(Effect::Add("shipped".into(), vec![])),
            }],
            ..Domain::default()
        };
        let problem = Problem {
            name: "p1".into(),
            domain_name: "logistics".into(),
            objects: vec![TypedList {
                items: vec!["pkg1".into(), "pkg2".into()],
                type_name: Some(Type::Simple("package".into())),
            }],
            init: vec![
                Init::Positive("ready".into(), vec!["pkg1".into()]),
                Init::Positive("ready".into(), vec!["pkg2".into()]),
            ],
            goal: GoalDesc::Atom("shipped".into(), vec![]),
            ..Problem::default()
        };

        let (program, _state, _goals) = pddl_to_ir(&domain, &problem).unwrap();
        let action = &program.actions[0];
        // forall (?p - package) (ready ?p) → ready(pkg1), ready(pkg2)
        assert_eq!(action.preconditions.len(), 2);
    }

    #[test]
    fn test_pddl_to_ir_with_forall_effect() {
        let domain = Domain {
            name: "logistics".into(),
            actions: vec![Action {
                name: "release-all".into(),
                parameters: vec![],
                precondition: None,
                effect: Some(Effect::Forall(
                    vec![TypedList {
                        items: vec!["p".into()],
                        type_name: Some(Type::Simple("package".into())),
                    }],
                    Box::new(Effect::Add("released".into(), vec![Term::Variable("p".into())])),
                )),
            }],
            ..Domain::default()
        };
        let problem = Problem {
            name: "p1".into(),
            domain_name: "logistics".into(),
            objects: vec![TypedList {
                items: vec!["pkg1".into(), "pkg2".into(), "pkg3".into()],
                type_name: Some(Type::Simple("package".into())),
            }],
            init: vec![],
            goal: GoalDesc::Empty,
            ..Problem::default()
        };

        let (program, _, _) = pddl_to_ir(&domain, &problem).unwrap();
        // forall → 3 effects
        assert_eq!(program.actions[0].effects.len(), 3);
    }

    // ── Or / Imply conversion tests ─────────────────────────────────────────

    #[test]
    fn test_convert_goal_or() {
        let gd = GoalDesc::Or(vec![
            GoalDesc::Atom("path-a".into(), vec![]),
            GoalDesc::Atom("path-b".into(), vec![]),
        ]);
        let ir = convert_goal_desc(&gd, &no_objects()).unwrap();
        assert_eq!(
            ir,
            IrTerm::Structure {
                name: "or".into(),
                args: vec![
                    IrTerm::Structure { name: "path-a".into(), args: vec![] },
                    IrTerm::Structure { name: "path-b".into(), args: vec![] },
                ],
            }
        );
    }

    #[test]
    fn test_convert_goal_or_nested_in_and() {
        // and(p, or(q, r))
        let gd = GoalDesc::And(vec![
            GoalDesc::Atom("p".into(), vec![]),
            GoalDesc::Or(vec![
                GoalDesc::Atom("q".into(), vec![]),
                GoalDesc::Atom("r".into(), vec![]),
            ]),
        ]);
        let flat = convert_goal_flat(&gd, &no_objects()).unwrap();
        // And flattens: p is flat, or(q,r) stays as one term
        assert_eq!(flat.len(), 2);
        assert_eq!(
            flat[1],
            IrTerm::Structure {
                name: "or".into(),
                args: vec![
                    IrTerm::Structure { name: "q".into(), args: vec![] },
                    IrTerm::Structure { name: "r".into(), args: vec![] },
                ],
            }
        );
    }

    #[test]
    fn test_convert_goal_imply() {
        // imply(a, b) → or(not(a), b)
        let gd = GoalDesc::Imply(
            Box::new(GoalDesc::Atom("armed".into(), vec![])),
            Box::new(GoalDesc::Atom("dangerous".into(), vec![])),
        );
        let ir = convert_goal_desc(&gd, &no_objects()).unwrap();
        assert_eq!(
            ir,
            IrTerm::Structure {
                name: "or".into(),
                args: vec![
                    IrTerm::Structure {
                        name: "not".into(),
                        args: vec![IrTerm::Structure {
                            name: "armed".into(),
                            args: vec![],
                        }],
                    },
                    IrTerm::Structure { name: "dangerous".into(), args: vec![] },
                ],
            }
        );
    }

    #[test]
    fn test_convert_goal_imply_with_vars() {
        // imply(fragile(?x), handle-carefully(?x))
        let gd = GoalDesc::Imply(
            Box::new(GoalDesc::Atom(
                "fragile".into(),
                vec![Term::Variable("x".into())],
            )),
            Box::new(GoalDesc::Atom(
                "handle-carefully".into(),
                vec![Term::Variable("x".into())],
            )),
        );
        let ir = convert_goal_desc(&gd, &no_objects()).unwrap();
        match &ir {
            IrTerm::Structure { name, args } => {
                assert_eq!(name, "or");
                assert_eq!(args.len(), 2);
                // First arg: not(fragile(X))
                assert_eq!(
                    args[0],
                    IrTerm::Structure {
                        name: "not".into(),
                        args: vec![IrTerm::Structure {
                            name: "fragile".into(),
                            args: vec![IrTerm::Var("X".into())],
                        }],
                    }
                );
                // Second arg: handle-carefully(X)
                assert_eq!(
                    args[1],
                    IrTerm::Structure {
                        name: "handle-carefully".into(),
                        args: vec![IrTerm::Var("X".into())],
                    }
                );
            }
            _ => panic!("expected or structure"),
        }
    }

    #[test]
    fn test_convert_action_with_or_precondition() {
        let action = Action {
            name: "go".into(),
            parameters: vec![TypedList {
                items: vec!["from".into(), "to".into()],
                type_name: Some(Type::Simple("location".into())),
            }],
            precondition: Some(GoalDesc::And(vec![
                GoalDesc::Atom(
                    "at".into(),
                    vec![Term::Variable("from".into())],
                ),
                GoalDesc::Or(vec![
                    GoalDesc::Atom(
                        "road".into(),
                        vec![Term::Variable("from".into()), Term::Variable("to".into())],
                    ),
                    GoalDesc::Atom(
                        "bridge".into(),
                        vec![Term::Variable("from".into()), Term::Variable("to".into())],
                    ),
                ]),
            ])),
            effect: Some(Effect::And(vec![
                Effect::Add("at".into(), vec![Term::Variable("to".into())]),
                Effect::Delete("at".into(), vec![Term::Variable("from".into())]),
            ])),
        };

        let ir = convert_action(&action, &no_objects()).unwrap();
        assert_eq!(ir.name, "go");
        // And flattens: at(From) + or(road(...), bridge(...))
        assert_eq!(ir.preconditions.len(), 2);
        match &ir.preconditions[1] {
            IrTerm::Structure { name, args } => {
                assert_eq!(name, "or");
                assert_eq!(args.len(), 2);
            }
            _ => panic!("expected or in precondition"),
        }
    }

    // ── Numeric fluent tests ────────────────────────────────────────────────

    #[test]
    fn test_convert_fexp_number() {
        let fe = FExp::Number(42.0);
        assert_eq!(convert_fexp(&fe).unwrap(), IrTerm::Float(42.0));
    }

    #[test]
    fn test_convert_fexp_fhead() {
        let fe = FExp::FHead(FHead {
            name: "fuel".into(),
            args: vec![Term::Variable("v".into())],
        });
        assert_eq!(
            convert_fexp(&fe).unwrap(),
            IrTerm::Structure {
                name: "fuel".into(),
                args: vec![IrTerm::Var("V".into())],
            }
        );
    }

    #[test]
    fn test_convert_fexp_binary_op() {
        let fe = FExp::BinaryOp(
            BinaryOp::Add,
            Box::new(FExp::FHead(FHead {
                name: "fuel".into(),
                args: vec![],
            })),
            Box::new(FExp::Number(10.0)),
        );
        let ir = convert_fexp(&fe).unwrap();
        assert_eq!(
            ir,
            IrTerm::Structure {
                name: "+".into(),
                args: vec![
                    IrTerm::Structure { name: "fuel".into(), args: vec![] },
                    IrTerm::Float(10.0),
                ],
            }
        );
    }

    #[test]
    fn test_convert_fexp_negate() {
        let fe = FExp::Negate(Box::new(FExp::Number(5.0)));
        assert_eq!(
            convert_fexp(&fe).unwrap(),
            IrTerm::Structure {
                name: "negate".into(),
                args: vec![IrTerm::Float(5.0)],
            }
        );
    }

    #[test]
    fn test_convert_goal_fcomp() {
        let gd = GoalDesc::FComp(
            Comparator::GtEq,
            FExp::FHead(FHead { name: "fuel".into(), args: vec![Term::Variable("r".into())] }),
            FExp::Number(10.0),
        );
        let ir = convert_goal_desc(&gd, &no_objects()).unwrap();
        assert_eq!(
            ir,
            IrTerm::Structure {
                name: "fcomp".into(),
                args: vec![
                    IrTerm::Atom(">=".into()),
                    IrTerm::Structure {
                        name: "fuel".into(),
                        args: vec![IrTerm::Var("R".into())],
                    },
                    IrTerm::Float(10.0),
                ],
            }
        );
    }

    #[test]
    fn test_convert_numeric_effect_decrease() {
        let eff = Effect::Decrease(
            FHead { name: "fuel".into(), args: vec![Term::Variable("r".into())] },
            FExp::Number(5.0),
        );
        let ir = convert_effect_flat(&eff, &no_objects()).unwrap();
        assert_eq!(ir.len(), 1);
        assert_eq!(
            ir[0],
            IrTerm::Structure {
                name: "decrease".into(),
                args: vec![
                    IrTerm::Structure {
                        name: "fuel".into(),
                        args: vec![IrTerm::Var("R".into())],
                    },
                    IrTerm::Float(5.0),
                ],
            }
        );
    }

    #[test]
    fn test_convert_numeric_effect_assign() {
        let eff = Effect::Assign(
            FHead { name: "cost".into(), args: vec![] },
            FExp::Number(0.0),
        );
        let ir = convert_effect_flat(&eff, &no_objects()).unwrap();
        assert_eq!(ir.len(), 1);
        assert_eq!(
            ir[0],
            IrTerm::Structure {
                name: "assign".into(),
                args: vec![
                    IrTerm::Structure { name: "cost".into(), args: vec![] },
                    IrTerm::Float(0.0),
                ],
            }
        );
    }

    #[test]
    fn test_convert_init_function_value() {
        let inits = vec![
            Init::Positive("at".into(), vec!["rover1".into(), "base".into()]),
            Init::FunctionValue("fuel".into(), vec!["rover1".into()], 100.0),
        ];
        let state = convert_init(&inits).unwrap();
        assert_eq!(state.fact_count(), 2);
        assert!(state.contains(&IrTerm::Structure {
            name: "=".into(),
            args: vec![
                IrTerm::Structure {
                    name: "fuel".into(),
                    args: vec![IrTerm::Atom("rover1".into())],
                },
                IrTerm::Float(100.0),
            ],
        }));
    }

    #[test]
    fn test_convert_action_with_numeric_fluents() {
        let action = Action {
            name: "drive".into(),
            parameters: vec![TypedList {
                items: vec!["r".into()],
                type_name: Some(Type::Simple("rover".into())),
            }],
            precondition: Some(GoalDesc::FComp(
                Comparator::GtEq,
                FExp::FHead(FHead {
                    name: "fuel".into(),
                    args: vec![Term::Variable("r".into())],
                }),
                FExp::Number(10.0),
            )),
            effect: Some(Effect::Decrease(
                FHead {
                    name: "fuel".into(),
                    args: vec![Term::Variable("r".into())],
                },
                FExp::Number(10.0),
            )),
        };
        let ir = convert_action(&action, &no_objects()).unwrap();
        assert_eq!(ir.preconditions.len(), 1);
        assert_eq!(ir.effects.len(), 1);
        match &ir.preconditions[0] {
            IrTerm::Structure { name, .. } => assert_eq!(name, "fcomp"),
            _ => panic!("expected fcomp"),
        }
        match &ir.effects[0] {
            IrTerm::Structure { name, .. } => assert_eq!(name, "decrease"),
            _ => panic!("expected decrease"),
        }
    }

    // ── Durative action tests ─────────────────────────────────────────────

    #[test]
    fn test_convert_durative_action_basic() {
        let da = DurativeAction {
            name: "fly".into(),
            parameters: vec![TypedList {
                items: vec!["a".into()],
                type_name: Some(Type::Simple("aircraft".into())),
            }],
            duration: DurationConstraint::Cmp(Comparator::Eq, FExp::Number(10.0)),
            condition: Some(DaGd::And(vec![
                DaGd::AtStart(GoalDesc::Atom(
                    "at-airport".into(),
                    vec![Term::Variable("a".into())],
                )),
                DaGd::OverAll(GoalDesc::Atom(
                    "has-fuel".into(),
                    vec![Term::Variable("a".into())],
                )),
            ])),
            effect: Some(DaEffect::And(vec![
                DaEffect::AtStart(Effect::Delete(
                    "at-airport".into(),
                    vec![Term::Variable("a".into())],
                )),
                DaEffect::AtEnd(Effect::Add(
                    "arrived".into(),
                    vec![Term::Variable("a".into())],
                )),
            ])),
        };

        let ir = convert_durative_action(&da, &no_objects()).unwrap();
        assert_eq!(ir.name, "fly");
        assert_eq!(ir.parameters, vec!["A".to_string()]);

        // Should have: duration constraint + 2 temporal conditions = 3 preconditions
        assert_eq!(ir.preconditions.len(), 3);

        // First: duration(=, 10.0)
        match &ir.preconditions[0] {
            IrTerm::Structure { name, .. } => assert_eq!(name, "duration"),
            _ => panic!("expected duration"),
        }

        // Second: at-start(at-airport(A))
        match &ir.preconditions[1] {
            IrTerm::Structure { name, args } => {
                assert_eq!(name, "at-start");
                assert_eq!(args.len(), 1);
            }
            _ => panic!("expected at-start"),
        }

        // Third: over-all(has-fuel(A))
        match &ir.preconditions[2] {
            IrTerm::Structure { name, .. } => assert_eq!(name, "over-all"),
            _ => panic!("expected over-all"),
        }

        // Effects: 2 temporal effects
        assert_eq!(ir.effects.len(), 2);
        match &ir.effects[0] {
            IrTerm::Structure { name, .. } => assert_eq!(name, "at-start"),
            _ => panic!("expected at-start effect"),
        }
        match &ir.effects[1] {
            IrTerm::Structure { name, .. } => assert_eq!(name, "at-end"),
            _ => panic!("expected at-end effect"),
        }
    }

    #[test]
    fn test_convert_durative_action_continuous_effects() {
        let da = DurativeAction {
            name: "move".into(),
            parameters: vec![],
            duration: DurationConstraint::Cmp(Comparator::Eq, FExp::Number(5.0)),
            condition: None,
            effect: Some(DaEffect::And(vec![
                DaEffect::ContinuousIncrease(
                    FHead { name: "distance".into(), args: vec![] },
                    FExp::Number(1.0),
                ),
                DaEffect::ContinuousDecrease(
                    FHead { name: "fuel".into(), args: vec![] },
                    FExp::Number(0.5),
                ),
            ])),
        };

        let ir = convert_durative_action(&da, &no_objects()).unwrap();
        assert_eq!(ir.effects.len(), 2);
        match &ir.effects[0] {
            IrTerm::Structure { name, .. } => assert_eq!(name, "continuous-increase"),
            _ => panic!("expected continuous-increase"),
        }
        match &ir.effects[1] {
            IrTerm::Structure { name, .. } => assert_eq!(name, "continuous-decrease"),
            _ => panic!("expected continuous-decrease"),
        }
    }

    #[test]
    fn test_domain_to_ir_includes_durative_actions() {
        let domain = Domain {
            name: "test".into(),
            durative_actions: vec![DurativeAction {
                name: "fly".into(),
                parameters: vec![],
                duration: DurationConstraint::Cmp(Comparator::Eq, FExp::Number(5.0)),
                condition: Some(DaGd::AtStart(GoalDesc::Atom("ready".into(), vec![]))),
                effect: Some(DaEffect::AtEnd(Effect::Add("done".into(), vec![]))),
            }],
            ..Domain::default()
        };

        let program = domain_to_ir(&domain).unwrap();
        assert_eq!(program.actions.len(), 1);
        assert_eq!(program.actions[0].name, "fly");
        // Should have temporal markers
        assert!(program.actions[0].preconditions.iter().any(
            |p| matches!(p, IrTerm::Structure { name, .. } if name == "duration")
        ));
    }

    // ── PDDL 3.0 tests ───────────────────────────────────────────────────

    #[test]
    fn test_convert_goal_desc_preference() {
        let gd = GoalDesc::Preference(
            Some("p1".into()),
            Box::new(GoalDesc::Atom("clean".into(), vec![])),
        );
        let result = convert_goal_desc(&gd, &no_objects()).unwrap();
        match result {
            IrTerm::Structure { name, args } => {
                assert_eq!(name, "preference");
                assert_eq!(args[0], IrTerm::Atom("p1".into()));
                match &args[1] {
                    IrTerm::Structure { name, .. } => assert_eq!(name, "clean"),
                    _ => panic!("expected structure"),
                }
            }
            _ => panic!("expected structure"),
        }
    }

    #[test]
    fn test_convert_goal_desc_preference_anonymous() {
        let gd = GoalDesc::Preference(
            None,
            Box::new(GoalDesc::Atom("tidy".into(), vec![])),
        );
        let result = convert_goal_desc(&gd, &no_objects()).unwrap();
        match result {
            IrTerm::Structure { name, args } => {
                assert_eq!(name, "preference");
                assert_eq!(args[0], IrTerm::Atom("_anon".into()));
            }
            _ => panic!("expected structure"),
        }
    }

    #[test]
    fn test_convert_con_gd_always() {
        let con = ConGd::Always(GoalDesc::Atom("safe".into(), vec![]));
        let result = convert_con_gd(&con, &no_objects()).unwrap();
        match result {
            IrTerm::Structure { name, args } => {
                assert_eq!(name, "always");
                assert_eq!(args.len(), 1);
            }
            _ => panic!("expected structure"),
        }
    }

    #[test]
    fn test_convert_con_gd_sometime_after() {
        let con = ConGd::SometimeAfter(
            GoalDesc::Atom("alarm".into(), vec![]),
            GoalDesc::Atom("evacuated".into(), vec![]),
        );
        let result = convert_con_gd(&con, &no_objects()).unwrap();
        match result {
            IrTerm::Structure { name, args } => {
                assert_eq!(name, "sometime-after");
                assert_eq!(args.len(), 2);
            }
            _ => panic!("expected structure"),
        }
    }

    #[test]
    fn test_convert_con_gd_within() {
        let con = ConGd::Within(5.0, GoalDesc::Atom("goal".into(), vec![]));
        let result = convert_con_gd(&con, &no_objects()).unwrap();
        match result {
            IrTerm::Structure { name, args } => {
                assert_eq!(name, "within");
                assert_eq!(args[0], IrTerm::Float(5.0));
            }
            _ => panic!("expected structure"),
        }
    }

    #[test]
    fn test_convert_con_gd_at_most_once() {
        let con = ConGd::AtMostOnce(GoalDesc::Atom("toggle".into(), vec![]));
        let result = convert_con_gd(&con, &no_objects()).unwrap();
        match result {
            IrTerm::Structure { name, .. } => assert_eq!(name, "at-most-once"),
            _ => panic!("expected structure"),
        }
    }

    #[test]
    fn test_convert_con_gd_hold_during() {
        let con = ConGd::HoldDuring(
            10.0,
            20.0,
            GoalDesc::Atom("stable".into(), vec![]),
        );
        let result = convert_con_gd(&con, &no_objects()).unwrap();
        match result {
            IrTerm::Structure { name, args } => {
                assert_eq!(name, "hold-during");
                assert_eq!(args.len(), 3);
                assert_eq!(args[0], IrTerm::Float(10.0));
                assert_eq!(args[1], IrTerm::Float(20.0));
            }
            _ => panic!("expected structure"),
        }
    }

    #[test]
    fn test_convert_pref_con_gd() {
        let pcg = PrefConGd::Preference(
            Some("soft1".into()),
            ConGd::Sometime(GoalDesc::Atom("visited".into(), vec![])),
        );
        let result = convert_pref_con_gd(&pcg, &no_objects()).unwrap();
        assert_eq!(result.len(), 1);
        match &result[0] {
            IrTerm::Structure { name, args } => {
                assert_eq!(name, "preference");
                assert_eq!(args[0], IrTerm::Atom("soft1".into()));
                match &args[1] {
                    IrTerm::Structure { name, .. } => assert_eq!(name, "sometime"),
                    _ => panic!("expected sometime"),
                }
            }
            _ => panic!("expected structure"),
        }
    }

    #[test]
    fn test_convert_metric() {
        let metric = MetricSpec {
            optimization: Optimization::Minimize,
            expression: FExp::BinaryOp(
                BinaryOp::Add,
                Box::new(FExp::FHead(FHead {
                    name: "total-cost".into(),
                    args: vec![],
                })),
                Box::new(FExp::BinaryOp(
                    BinaryOp::Mul,
                    Box::new(FExp::Number(10.0)),
                    Box::new(FExp::IsViolated("p1".into())),
                )),
            ),
        };
        let result = convert_metric(&metric).unwrap();
        match result {
            IrTerm::Structure { name, args } => {
                assert_eq!(name, "metric");
                assert_eq!(args[0], IrTerm::Atom("minimize".into()));
                match &args[1] {
                    IrTerm::Structure { name, .. } => assert_eq!(name, "+"),
                    _ => panic!("expected +"),
                }
            }
            _ => panic!("expected structure"),
        }
    }

    #[test]
    fn test_pddl_to_ir_full_with_constraints() {
        let domain = Domain {
            name: "test".into(),
            requirements: vec![Requirement::Strips, Requirement::Preferences],
            actions: vec![Action {
                name: "go".into(),
                parameters: vec![],
                precondition: Some(GoalDesc::Atom("ready".into(), vec![])),
                effect: Some(Effect::Add("done".into(), vec![])),
            }],
            constraints: Some(ConGd::Always(GoalDesc::Atom("safe".into(), vec![]))),
            ..Domain::default()
        };
        let problem = Problem {
            name: "p1".into(),
            domain_name: "test".into(),
            goal: GoalDesc::And(vec![
                GoalDesc::Atom("done".into(), vec![]),
                GoalDesc::Preference(
                    Some("neat".into()),
                    Box::new(GoalDesc::Atom("tidy".into(), vec![])),
                ),
            ]),
            constraints: Some(PrefConGd::Preference(
                Some("visited-all".into()),
                ConGd::Sometime(GoalDesc::Atom("visited".into(), vec![])),
            )),
            metric: Some(MetricSpec {
                optimization: Optimization::Minimize,
                expression: FExp::IsViolated("neat".into()),
            }),
            ..Problem::default()
        };

        let result = pddl_to_ir_full(&domain, &problem).unwrap();
        assert!(!result.goals.is_empty());
        assert!(result.domain_constraints.is_some());
        assert!(!result.problem_constraints.is_empty());
        assert!(result.metric.is_some());

        // Domain constraint: always(safe())
        match result.domain_constraints.unwrap() {
            IrTerm::Structure { name, .. } => assert_eq!(name, "always"),
            _ => panic!("expected always"),
        }

        // Metric: metric(minimize, is-violated(neat))
        match result.metric.unwrap() {
            IrTerm::Structure { name, args } => {
                assert_eq!(name, "metric");
                assert_eq!(args[0], IrTerm::Atom("minimize".into()));
            }
            _ => panic!("expected metric"),
        }
    }

    // ── PDDL+ Process & Event conversion ────────────────────────────────────

    #[test]
    fn test_convert_process_to_ir() {
        let proc = Process {
            name: "gravity".into(),
            parameters: vec![TypedList {
                items: vec!["ball".into()],
                type_name: Some(Type::Simple("object".into())),
            }],
            precondition: GoalDesc::Atom("airborne".into(), vec![Term::Variable("ball".into())]),
            effect: vec![Effect::Increase(
                FHead {
                    name: "velocity".into(),
                    args: vec![Term::Variable("ball".into())],
                },
                FExp::Number(9.81),
            )],
        };

        let registry = HashMap::new();
        let result = convert_process(&proc, &registry).unwrap();

        assert_eq!(result.name, "gravity");
        assert_eq!(result.parameters, vec!["Ball".to_string()]);

        // First precondition should be __process marker.
        assert_eq!(result.preconditions[0], IrTerm::Atom("__process".into()));
        assert_eq!(result.preconditions.len(), 2);

        // Effects should be wrapped in continuous-effect.
        assert_eq!(result.effects.len(), 1);
        match &result.effects[0] {
            IrTerm::Structure { name, .. } => assert_eq!(name, "continuous-effect"),
            _ => panic!("expected continuous-effect wrapper"),
        }
    }

    #[test]
    fn test_convert_event_to_ir() {
        let evt = Event {
            name: "bounce".into(),
            parameters: vec![],
            precondition: GoalDesc::And(vec![
                GoalDesc::Atom("falling".into(), vec![]),
                GoalDesc::FComp(
                    Comparator::LtEq,
                    FExp::FHead(FHead { name: "height".into(), args: vec![] }),
                    FExp::Number(0.0),
                ),
            ]),
            effect: vec![
                Effect::Delete("falling".into(), vec![]),
                Effect::Add("rising".into(), vec![]),
            ],
        };

        let registry = HashMap::new();
        let result = convert_event(&evt, &registry).unwrap();

        assert_eq!(result.name, "bounce");

        // First precondition should be __event marker.
        assert_eq!(result.preconditions[0], IrTerm::Atom("__event".into()));
        // Remaining preconditions: falling() + fcomp.
        assert!(result.preconditions.len() >= 3);

        // Effects should NOT be wrapped in continuous-effect (events are instantaneous).
        for eff in &result.effects {
            if let IrTerm::Structure { name, .. } = eff {
                assert_ne!(name, "continuous-effect", "events should not have continuous-effect wrappers");
            }
        }
    }

    #[test]
    fn test_domain_with_process_and_event() {
        let domain = Domain {
            name: "physics".into(),
            processes: vec![Process {
                name: "fall".into(),
                parameters: vec![],
                precondition: GoalDesc::Atom("airborne".into(), vec![]),
                effect: vec![Effect::Increase(
                    FHead { name: "velocity".into(), args: vec![] },
                    FExp::Number(9.81),
                )],
            }],
            events: vec![Event {
                name: "land".into(),
                parameters: vec![],
                precondition: GoalDesc::Atom("at-ground".into(), vec![]),
                effect: vec![
                    Effect::Delete("airborne".into(), vec![]),
                    Effect::Add("grounded".into(), vec![]),
                ],
            }],
            ..Domain::default()
        };

        let registry = HashMap::new();
        let program = domain_to_ir_inner(&domain, &registry).unwrap();

        // Should have 2 actions: the process and the event.
        assert_eq!(program.actions.len(), 2);

        // Process should have __process marker.
        let proc_action = &program.actions[0];
        assert_eq!(proc_action.preconditions[0], IrTerm::Atom("__process".into()));

        // Event should have __event marker.
        let evt_action = &program.actions[1];
        assert_eq!(evt_action.preconditions[0], IrTerm::Atom("__event".into()));
    }

    // ── Type hierarchy storage ──────────────────────────────────────────────

    #[test]
    fn test_type_hierarchy_stored_in_program() {
        let domain = Domain {
            name: "typed".into(),
            types: vec![
                TypeDecl {
                    names: vec!["city".into(), "location".into()],
                    parent: Some("object".into()),
                },
                TypeDecl {
                    names: vec!["truck".into(), "airplane".into()],
                    parent: Some("vehicle".into()),
                },
                TypeDecl {
                    names: vec!["vehicle".into()],
                    parent: None,
                },
            ],
            ..Domain::default()
        };

        let program = domain_to_ir(&domain).unwrap();

        assert_eq!(program.type_hierarchy.len(), 3);
        assert_eq!(
            program.type_hierarchy[0],
            (vec!["city".into(), "location".into()], Some("object".into()))
        );
        assert_eq!(
            program.type_hierarchy[1],
            (vec!["truck".into(), "airplane".into()], Some("vehicle".into()))
        );
        assert_eq!(
            program.type_hierarchy[2],
            (vec!["vehicle".into()], None::<String>)
        );
    }
}