reasoninglayer 0.1.2

//! Proof control DTOs (cut, findall, forall, NAF, conditionals, modules).

use std::collections::BTreeMap;

use serde::{Deserialize, Serialize};

use super::namespaces::VisibilityDto;

/// Value for assignment operations (tagged by `type`, lowercase).
#[derive(Debug, Clone, Serialize, Deserialize)]
#[serde(tag = "type", rename_all = "snake_case")]
pub enum AssignValueDto {
    Integer { value: i64 },
    Real { value: f64 },
    String { value: String },
    Boolean { value: bool },
    TermRef { term_id: String },
}

/// Goal payload used by control endpoints. Free-form by design in the TS SDK.
pub type GoalPayload = BTreeMap<String, serde_json::Value>;

#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct BacktrackableAssignRequest {
    pub session_id: String,
    pub term_id: String,
    pub feature_name: String,
    pub new_value: AssignValueDto,
}

#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct BacktrackableAssignResponse {
    pub feature_name: String,
    #[serde(default, skip_serializing_if = "Option::is_none")]
    pub previous_value: Option<AssignValueDto>,
    pub term_id: String,
    pub trail_entry_added: bool,
}

#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct GlobalAssignRequest {
    pub session_id: String,
    pub variable_name: String,
    pub value: AssignValueDto,
}

#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct GlobalAssignResponse {
    #[serde(default, skip_serializing_if = "Option::is_none")]
    pub previous_value: Option<AssignValueDto>,
    pub variable_name: String,
}

#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct CallOnceRequest {
    pub session_id: String,
    pub goal: GoalPayload,
}

#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct CallOnceResponse {
    pub choice_points_cut: u32,
    pub success: bool,
}

#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct CondRequest {
    pub session_id: String,
    pub condition: GoalPayload,
    pub then_goal: GoalPayload,
    pub else_goal: GoalPayload,
}

#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct CondResponse {
    pub branch_executed: String,
    pub condition_succeeded: bool,
    pub success: bool,
}

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

#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct CutResponse {
    pub choice_points_removed: u32,
}

#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct FindallRequest {
    pub session_id: String,
    pub template: String,
    pub goal: GoalPayload,
    #[serde(default, skip_serializing_if = "Option::is_none")]
    pub max_solutions: Option<u32>,
}

#[derive(Debug, Clone, Default, Serialize, Deserialize)]
pub struct FindallResponse {
    pub count: u64,
    #[serde(default)]
    pub solutions: Vec<String>,
}

#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct ForallRequest {
    pub session_id: String,
    pub generator: GoalPayload,
    pub test: GoalPayload,
}

#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct ForallResponse {
    pub result: bool,
    pub solutions_tested: u64,
}

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

#[derive(Debug, Clone, Serialize, Deserialize)]
#[serde(tag = "status", rename_all = "snake_case")]
pub enum GlobalGetResponse {
    Found { value: AssignValueDto },
    NotFound { variable_name: String },
}

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

#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct GlobalIncrementResponse {
    pub new_value: i64,
    pub variable_name: String,
}

#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct ImpliesRequest {
    pub session_id: String,
    pub antecedent: GoalPayload,
    pub consequent: GoalPayload,
}

#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct ImpliesResponse {
    pub antecedent_succeeded: bool,
    #[serde(default, skip_serializing_if = "Option::is_none")]
    pub consequent_succeeded: Option<bool>,
    pub result: bool,
}

#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct ControlNafRequest {
    pub session_id: String,
    pub goal: GoalPayload,
}

#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct NafResponse {
    pub result: bool,
}

#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct UndoRequest {
    pub session_id: String,
    pub goal: GoalPayload,
}

#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct UndoResponse {
    pub trail_position: u64,
    pub undo_id: String,
}

/// Symbol kind in a module.
#[derive(Debug, Clone, Serialize, Deserialize)]
#[serde(tag = "type", rename_all = "snake_case")]
pub enum SymbolKindDto {
    Sort { sort_id: String },
    Function { arity: u32, evaluable: bool },
    Predicate { arity: u32 },
    Constant { value: AssignValueDto },
    Module { module_name: String },
}

#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct SymbolDto {
    #[serde(default, skip_serializing_if = "Option::is_none")]
    pub doc: Option<String>,
    pub kind: SymbolKindDto,
    pub name: String,
    pub visibility: VisibilityDto,
}

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

#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct CreateModuleResponse {
    pub module_name: String,
}

#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct ImportModuleRequest {
    #[serde(default, skip_serializing_if = "Option::is_none")]
    pub alias: Option<String>,
    pub imported_module: String,
    pub importer_module: String,
    pub session_id: String,
}

#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct ImportModuleResponse {
    pub imported_module: String,
}

#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct AddSymbolRequest {
    pub module_name: String,
    pub session_id: String,
    pub symbol: SymbolDto,
}

#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct AddSymbolResponse {
    pub module_name: String,
    pub success: bool,
    pub symbol_name: String,
}

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

#[derive(Debug, Clone, Default, Serialize, Deserialize)]
pub struct ListSymbolsResponse {
    pub module_name: String,
    #[serde(default)]
    pub symbols: Vec<SymbolDto>,
}

#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct ResolveSymbolRequest {
    pub current_module: String,
    pub qualified_name: String,
    pub session_id: String,
}

#[derive(Debug, Clone, Serialize, Deserialize)]
#[serde(tag = "status", rename_all = "snake_case")]
pub enum ResolveSymbolResponse {
    Found {
        module_name: String,
        symbol: SymbolDto,
    },
    NotFound {
        reason: String,
    },
    NotVisible {
        module_name: String,
        symbol_name: String,
    },
}