use serde::{Deserialize, Serialize};

pub type SessionID = String;
pub type TaskID = String;

#[derive(Serialize, Deserialize)]
#[serde(untagged)]
pub enum ClientCommand {
    UseTheories {
        session_id : SessionID,
        theories : Vec<String>,
        master_dir : Option<String>
    },
    SessionStart {
        session : String,
        include_sessions : Vec<String>
    },
    Echo (String),
    ShutDown
}

#[derive(Debug)]
pub enum SyncAnswer<T,E> {
    Ok (T),
    Error (E),
}

pub enum AsyncAnswer<T, E, N> {
    Finished (T),
    Failed (E),
    Note (N)
}

#[derive(Deserialize, Debug)]
pub struct ClientHello {
    pub isabelle_id : String,
    pub isabelle_version : String
}

#[allow(dead_code)]
#[derive(Deserialize)]
pub struct SessionStartedOk {
    pub session_id : String,
    pub tmp_dir : String,
    pub task : String
}

#[allow(dead_code)]
#[derive(Deserialize)]
pub struct SessionStartedNote {
    pub percentage : u8,
    pub task : TaskID,
    pub message : String,
    pub kind : String,
    pub session : String,
    pub theory : String
}

#[derive(Deserialize, Clone, Debug)]
pub struct SessionStartedFinished {
    pub session_id : SessionID,
    pub tmp_dir : String,
    pub task : TaskID
}



#[derive(Deserialize, Clone, Debug)]
pub struct UseTheoriesFinished {
    pub ok : bool,
    pub errors : Vec<IsabelleError>,
    pub nodes : Vec<IsabelleNode>,
    pub task : TaskID,
}

#[derive(Deserialize, Clone, Debug)]
pub struct IsabelleError {
    pub kind : String,
    pub message : String,
    pub pos : Span
}

#[derive(Deserialize, Clone, Debug)]
pub struct IsabelleNode {
    pub messages : Vec<IsabelleError>,
    pub exports : Vec<()>,
    pub status : Status,
    pub theory_name : String,
    pub node_name : String
}

#[derive(Deserialize, Clone, Debug)]
pub struct Status {
    pub percentage : u8,
    pub unprocessed : u64,
    pub running : u64,
    pub finished : u64,
    pub failed : u64,
    pub total : u64,
    pub consolidated : bool,
    pub canceled : bool,
    pub ok : bool,
    pub warned : u64
}

#[derive(Deserialize,Clone, Debug)]
pub struct Span {
    pub line : u64,
    pub offset : u64,
    pub end_offset : u64,
    pub file : String
}

#[derive(Deserialize)]
pub struct AsyncStartOk {
    pub task : TaskID
}





pub trait Encode {
    fn encode (&self) -> String;
}

impl Encode for ClientCommand {
    fn encode (&self) -> String {
        let ty = match self {
            ClientCommand::UseTheories {..} => "use_theories",
            ClientCommand::SessionStart {..} => "session_start",
            ClientCommand::Echo (..) => "echo",
            ClientCommand::ShutDown => "shutdown"
        };

        let blob = serde_json::to_string(self).unwrap();

        let res = ty.to_owned() + &blob + "\n";
        println!("encoded: {}", res);
        res
    }
}