reasoninglayer 1.0.3

//! Execution session DTOs (trail-based proof search, choice points, currying, residuation).

use std::collections::BTreeMap;

use serde::{Deserialize, Serialize};

/// Tagged value carried by execution-session bindings.
#[derive(Debug, Clone, Serialize, Deserialize)]
#[serde(tag = "type", rename_all = "snake_case")]
pub enum ExecutionValueDto {
    Integer { value: i64 },
    Real { value: f64 },
    String { value: String },
    Boolean { value: bool },
    Uninstantiated,
}

#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct FeatureBindingDto {
    pub name: String,
    pub value: ExecutionValueDto,
}

#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct TermBindingDto {
    pub term_id: String,
    pub sort_id: String,
    #[serde(default)]
    pub features: Vec<FeatureBindingDto>,
}

/// Tagged trail-entry record (one entry per undo-able operation).
#[derive(Debug, Clone, Serialize, Deserialize)]
#[serde(tag = "type", rename_all = "snake_case")]
pub enum TrailEntryDto {
    TermBinding {
        term_id: String,
        previous_sort_id: Option<String>,
    },
    VariableBinding {
        variable_id: String,
        bound_to: Option<String>,
    },
    SortNarrowing {
        term_id: String,
        previous_sort_id: String,
    },
    FeatureAddition {
        term_id: String,
        feature_name: String,
    },
    CorefChange {
        term1_id: String,
        term2_id: String,
    },
    RationalBoundsChange {
        term_id: String,
    },
}

/// Tagged proof-search goal.
#[derive(Debug, Clone, Serialize, Deserialize)]
#[serde(tag = "type", rename_all = "snake_case")]
pub enum GoalDto {
    Unify {
        term1_id: String,
        term2_id: String,
        #[serde(default, skip_serializing_if = "Option::is_none")]
        eval_flag: Option<bool>,
    },
    Prove {
        predicate_name: String,
        arguments: Vec<String>,
    },
    Eval {
        function_name: String,
        arguments: Vec<String>,
        result_var: String,
    },
    TypeDisj {
        term_id: String,
        types: Vec<String>,
    },
    Cut,
    IfThenElse {
        condition: Box<GoalDto>,
        then_goal: Box<GoalDto>,
        else_goal: Box<GoalDto>,
    },
}

#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct PositionalArgumentDto {
    pub position: u64,
    pub value: ExecutionValueDto,
}

#[derive(Debug, Clone, Default, Serialize, Deserialize)]
pub struct GoalEvaluationResultDto {
    pub goal_id: u64,
    pub success: bool,
    #[serde(default, skip_serializing_if = "Option::is_none")]
    pub error: Option<String>,
}

// ─── Session lifecycle ──────────────────────────────────────────────────────

#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct CreateExecutionSessionRequest {
    pub tenant_id: String,
    #[serde(default, skip_serializing_if = "Option::is_none")]
    pub name: Option<String>,
}

#[derive(Debug, Clone, Default, Serialize, Deserialize)]
pub struct ExecutionSessionResponse {
    pub session_id: String,
    pub tenant_id: String,
    pub trail_length: u64,
    pub choice_point_count: u64,
    pub bindings_count: u64,
}

// ─── Bindings ───────────────────────────────────────────────────────────────

#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct BindTermRequest {
    pub term_id: String,
    pub sort_id: String,
    #[serde(default)]
    pub features: Vec<FeatureBindingDto>,
}

#[derive(Debug, Clone, Default, Serialize, Deserialize)]
pub struct BindTermResponse {
    pub session_id: String,
    pub tenant_id: String,
    pub trail_length: u64,
    pub choice_point_count: u64,
    pub bindings_count: u64,
    #[serde(default)]
    pub evaluation_results: Vec<GoalEvaluationResultDto>,
}

#[derive(Debug, Clone, Default, Serialize, Deserialize)]
pub struct GetBindingsRequest {
    #[serde(default)]
    pub term_ids: Vec<String>,
}

#[derive(Debug, Clone, Default, Serialize, Deserialize)]
pub struct BindingsResponse {
    #[serde(default)]
    pub bindings: Vec<TermBindingDto>,
}

// ─── Choice points / backtracking ───────────────────────────────────────────

#[derive(Debug, Clone, Default, Serialize, Deserialize)]
pub struct MarkChoicePointRequest {
    #[serde(default, skip_serializing_if = "Option::is_none")]
    pub description: Option<String>,
}

#[derive(Debug, Clone, Default, Serialize, Deserialize)]
pub struct ChoicePointMarkerResponse {
    pub marker_index: u64,
    pub timestamp: u64,
    pub choice_point_count: u64,
}

#[derive(Debug, Clone, Default, Serialize, Deserialize)]
pub struct BacktrackRequest {
    #[serde(default, skip_serializing_if = "Option::is_none")]
    pub marker_index: Option<u64>,
}

#[derive(Debug, Clone, Default, Serialize, Deserialize)]
pub struct BacktrackResponse {
    pub undone_count: u64,
    #[serde(default)]
    pub undone_entries: Vec<TrailEntryDto>,
    pub remaining_trail_length: u64,
    pub remaining_choice_points: u64,
}

// ─── Goal stack ─────────────────────────────────────────────────────────────

#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct PushGoalRequest {
    pub goal: GoalDto,
}

#[derive(Debug, Clone, Default, Serialize, Deserialize)]
pub struct PushGoalResponse {
    pub stack_size: u64,
    pub goal_id: u64,
}

#[derive(Debug, Clone, Default, Serialize, Deserialize)]
pub struct GoalStackEntryDto {
    pub index: u64,
    pub goal: Option<GoalDto>,
}

#[derive(Debug, Clone, Default, Serialize, Deserialize)]
pub struct GoalStackResponse {
    #[serde(default)]
    pub goals: Vec<GoalStackEntryDto>,
    pub size: u64,
}

#[derive(Debug, Clone, Default, Serialize, Deserialize)]
pub struct ExecuteGoalsRequest {
    /// Default 1000.
    #[serde(default, skip_serializing_if = "Option::is_none")]
    pub max_steps: Option<u64>,
}

// ─── Currying ───────────────────────────────────────────────────────────────

#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct CreateCurriedFunctionRequest {
    pub tenant_id: String,
    pub function_name: String,
    pub arity: u64,
    #[serde(default)]
    pub provided_arguments: Vec<PositionalArgumentDto>,
    #[serde(default = "default_true")]
    pub can_curry: bool,
}

fn default_true() -> bool {
    true
}

#[derive(Debug, Clone, Default, Serialize, Deserialize)]
pub struct CurriedFunctionResponse {
    pub curried_id: String,
    pub function_name: String,
    pub original_arity: u64,
    pub provided_count: u64,
    pub remaining_count: u64,
    #[serde(default)]
    pub missing_positions: Vec<u64>,
    pub is_fully_applied: bool,
    pub can_curry: bool,
}

#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct ApplyCurriedRequest {
    pub curried_id: String,
    pub arguments: Vec<PositionalArgumentDto>,
}

#[derive(Debug, Clone, Serialize, Deserialize)]
#[serde(tag = "status", rename_all = "snake_case")]
pub enum ApplyCurriedResponse {
    FullyApplied {
        result: ExecutionValueDto,
        all_arguments: Vec<PositionalArgumentDto>,
    },
    StillCurried {
        curried_id: String,
        remaining_count: u64,
        missing_positions: Vec<u64>,
    },
    CannotCurry {
        reason: String,
    },
}

#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct DetectMissingAttributesRequest {
    pub call_attributes: Vec<String>,
    pub definition_attributes: Vec<String>,
}

#[derive(Debug, Clone, Default, Serialize, Deserialize)]
pub struct CurryingContextResponse {
    pub more_call_attr: bool,
    pub more_def_attr: bool,
    pub should_curry: bool,
    #[serde(default)]
    pub missing_in_call: Vec<String>,
    #[serde(default)]
    pub missing_in_def: Vec<String>,
}

// ─── Lazy evaluation / residuation ──────────────────────────────────────────

#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct LazyEvalRequest {
    pub session_id: String,
    pub term_id: String,
    #[serde(default)]
    pub exclude_features: Vec<String>,
}

#[derive(Debug, Clone, Serialize, Deserialize)]
#[serde(tag = "status", rename_all = "snake_case")]
pub enum LazyEvalResponse {
    Evaluated {
        term_id: String,
    },
    Quoted {
        term_id: String,
    },
    SubtermsNeedEval {
        term_ids: Vec<String>,
    },
    NeedsFunctionEval {
        function_term_id: String,
        #[serde(default, skip_serializing_if = "Option::is_none")]
        function_name: Option<String>,
    },
}

#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct ResiduationGoalDto {
    pub operation_type: String,
    #[serde(default)]
    pub arguments: Vec<String>,
    #[serde(default, skip_serializing_if = "Option::is_none")]
    pub result_target: Option<String>,
}

#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct ResiduateGoalRequest {
    pub session_id: String,
    pub goal: ResiduationGoalDto,
    pub term_id: String,
    #[serde(default, skip_serializing_if = "Option::is_none")]
    pub best_sort: Option<String>,
    #[serde(default, skip_serializing_if = "Option::is_none")]
    pub best_value: Option<ExecutionValueDto>,
}

#[derive(Debug, Clone, Default, Serialize, Deserialize)]
pub struct ResiduateGoalResponse {
    pub residuation_id: String,
    pub suspended_count: u64,
    pub term_id: String,
    #[serde(default, skip_serializing_if = "Option::is_none")]
    pub best_sort: Option<String>,
}

#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct ReleaseResiduationsRequest {
    pub session_id: String,
    pub term_id: String,
}

/// Free-form result; backend's `release_residuations` payload continues to evolve.
pub type ReleaseResiduationsResponse = serde_json::Value;

/// Stats payload for `/execution/stats`.
pub type ExecutionStatsResponse = serde_json::Value;

/// Cleanup payload for `/execution/cleanup`.
pub type ExecutionCleanupResponse = serde_json::Value;

/// Generic JSON response slot used for endpoints that don't yet expose a stable struct.
pub type ExecutionJsonResponse = BTreeMap<String, serde_json::Value>;