use regex::Regex;
use serde::{Deserialize, Serialize, de::DeserializeOwned};
use serde_json::{Result, Value};

use std::{io::{BufRead, BufReader, BufWriter, Write}, path::PathBuf, process::{ChildStdout, Command, Stdio}};

use isabelle_unicode::PrettyUnicode;

use structopt::StructOpt;

type SessionID = String;
type TaskID = String;

#[derive(Serialize, Deserialize)]
#[serde(untagged)]
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)]
enum SyncAnswer<T,E> {
    Ok (T),
    Error (E),
}

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

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

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

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

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



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

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

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

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

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

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

fn decode_sync<'a, T> (msg: &'a str) -> Option<SyncAnswer<T, String>>
where T: Deserialize<'a> {
    let regex = Regex::new(r"^[a-zA-Z]+\b").unwrap();
    let mat = regex.find(msg)?;
    let ty = &msg[..mat.end()];
    let rest = &msg[mat.end()..];

    match ty {
        "OK" => Some(SyncAnswer::Ok(serde_json::from_str(&rest).ok()?)),
        "ERROR" => Some(SyncAnswer::Error(rest.to_owned())),
        _ => None
    }
}

fn decode_async<'a,T,E,N> (msg: &'a str) -> Option<AsyncAnswer<T,E,N>>
where T: Deserialize<'a>, N: Deserialize<'a>, E: Deserialize<'a> {
    let regex = Regex::new(r"^[a-zA-Z]+\b").unwrap();
    let mat = regex.find(msg)?;
    let ty = &msg[..mat.end()];
    let rest = &msg[mat.end()..];

    match ty {
        "NOTE" => Some(AsyncAnswer::Note(serde_json::from_str(&rest).ok()?)),
        "FINISHED" => Some(AsyncAnswer::Finished(serde_json::from_str(&rest).ok()?)),
        "FAILED" => Some(AsyncAnswer::Failed(serde_json::from_str(&rest).ok()?)),
        _ => None
    }
}



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";
        res
    }
}

fn wait_for_client(pipe: &mut BufReader<ChildStdout>) -> Option<ClientHello> {
    for res in pipe.lines() {
        match res {
            Err(_) => (),
            Ok(line) => {
                let hello : Option<SyncAnswer<ClientHello, _>> = decode_sync(&line);
                if let Some(SyncAnswer::Ok(data)) = hello {
                    return Some(data);
                }
            }
        }
    }
    None
}


fn wait_for_async_task<'a,T,E,N,F>
    (reader: &mut BufReader<ChildStdout>, task: &str, mut prog: F) -> Option<T>
where T: DeserializeOwned, E: DeserializeOwned, N: DeserializeOwned,
F: FnMut(N)
{
    for res in reader.lines() {
        match res {
            Err(_) => (),
            Ok(line) => {
                let regex = Regex::new(r"^[0-9]+$").unwrap();
                if regex.is_match(&line) {

                } else {
                    match decode_async::<T,E,N>(&line)? {
                        AsyncAnswer::Finished(data)
                            => return Some(data),
                        AsyncAnswer::Failed(_failed)
                            => panic!("building session failed"),
                        AsyncAnswer::Note(val) => prog(val)
                    }
                }
            }
        }
    };
    None
}

fn get_async_task_id (reader: &mut BufReader<ChildStdout>) -> TaskID {
    let mut res = String::new();
    reader.read_line(&mut res).unwrap();
    match decode_sync(&res).unwrap() {
        SyncAnswer::Ok(AsyncStartOk { task }) => task,
        SyncAnswer::Error(_) => panic!("failed to start async task!")
    }
}

#[derive(StructOpt)]
#[structopt(name = "isabelle-proto-POC", about="proof of concept for communicating with an Isabelle server")]
struct Options {
    theory : String,
    #[structopt(name="directory", default_value=Box::leak(Box::new(std::env::current_dir().unwrap().into_os_string().into_string().unwrap())))]
    directory : String
}

fn main() {
    let options = Options::from_args();
    println!("will check: {} in {}", options.theory, options.directory);

    let mut child = Command::new("isabelle")
        .arg("client")
        .stdin(Stdio::piped())
        .stdout(Stdio::piped())
        .stderr(Stdio::piped())
        .spawn()
        .expect("failed to run isabelle client!");

    let stdin = child.stdin.as_mut().unwrap();
    let stdout = child.stdout.take().unwrap();

    let mut reader = BufReader::new(stdout);

    let _ = wait_for_client(&mut reader);
    // TODO: display version information?

    let mut len : usize = 0;

    let session_id = match std::env::var("ISABAT_SESSION_ID") {
        Ok(id) => id,
        Err(_) => {

            // client should be ready, start a session
            stdin.write(ClientCommand::SessionStart{
                session: "HOL".to_string(),
                include_sessions: vec![],
            }.encode().as_bytes()).unwrap();

            let task = get_async_task_id(&mut reader);

            let started = wait_for_async_task::<SessionStartedFinished, Value, Value,_>(&mut reader, &task, |note| {
                if let Some(Value::String(msg)) = note.get("message") {
                    len = msg.len();
                    print!("{}\r", msg);
                    std::io::stdout().flush().unwrap();
                }
            }).unwrap();

            started.session_id
        }
    };


    // HOL should be loaded now, include a theory file

    stdin.write(ClientCommand::UseTheories {
        session_id,
        theories: vec![ options.theory ],
        master_dir: Some(options.directory),
    }.encode().as_bytes()).unwrap();

    let task = get_async_task_id(&mut reader);
    let result = wait_for_async_task::<UseTheoriesFinished, Value, Value, _>(&mut reader, &task, |note| {
        if let Some(Value::String(msg)) = note.get("message") {
            let white = len.checked_sub(msg.len()).unwrap_or(0);
            len = msg.len();
            print!("{}{}\r", msg, str::repeat(" ", white));
            std::io::stdout().flush().unwrap();
        }
    }).unwrap();
    println!("{}", str::repeat(" ", len));

    // built a theory! Let's display errors

    result
        .errors
        .iter()
        .for_each(|err| {
            println!("Isabelle Error:");
            println!("{}", err.message.to_pretty_unicode().unwrap())
        });
}