use std::{io::{BufRead, BufReader, Write}, process::{ChildStdin, ChildStdout, Command, Stdio}};

use regex::Regex;
use serde::de::DeserializeOwned;
use serde_json::Value;

use crate::{AsyncAnswer, ClientCommand, Encode, SessionStartedFinished, UseTheoriesFinished, decode_async, get_async_task_id, wait_for_client};




pub struct IsabelleSession {
    reader : BufReader<ChildStdout>,
    writer : ChildStdin,
    session_id : Option<String>
}

impl IsabelleSession {
    pub fn start_with_client() -> Self {
        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 mut reader = BufReader::new(child.stdout.take().unwrap());
        let a = wait_for_client(&mut reader);
        println!("client hello: {:?}", a);
        IsabelleSession {
            writer: child.stdin.unwrap(),
            reader,
            session_id: None
        }
    }

    pub  fn start_session(&mut self, session : String, include_sessions : Vec<String>)
        -> Result<SessionStartedFinished, Value>
    {

        self.writer.write(ClientCommand::SessionStart {
            session, include_sessions
        }.encode().as_bytes()).unwrap();
        let task_id = get_async_task_id(&mut self.reader);
        let started = self.await_task::<SessionStartedFinished, Value, Value,_>(&task_id, |_n| {})
        //    .await
            .unwrap();

        match started {
            Ok(ref finished) => self.session_id = Some(finished.session_id.to_owned()),
            Err(_) => ()
        };

        started
    }


    pub fn load_theory(&mut self, theory : String, master_dir : Option<String>)
    -> Result<UseTheoriesFinished, Value> {
        let session_id = self.session_id.as_ref().unwrap();

        self.writer.write(ClientCommand::UseTheories {
            session_id: session_id.clone(),
            theories: vec![ theory ],
            master_dir,
        }.encode().as_bytes()).unwrap();

        let task_id = get_async_task_id(&mut self.reader);

        self.await_task::<UseTheoriesFinished, Value, Value, _>(&task_id, |_| {})
            .unwrap()
    }



    fn await_task<'a,T,E,N,F>(
        &mut self,
        task_id: &str,
        mut prog: F)
    -> Option<Result<T, E>>
    where T: DeserializeOwned,
          E: DeserializeOwned,
          N: DeserializeOwned,
          F: FnMut(N)
    {
        let reader = &mut self.reader;
        for res in reader.lines() {
            match res {
                Err(err) => {
                    eprintln!("error while reading from pipe: {}", err);
                    std::process::exit(1);
                },
                Ok(line) => {
                    let regex = Regex::new(r"^[0-9]+$").unwrap();
                    if regex.is_match(&line) {
                        // TODO: we don't support the long style of messages yet …
                        // the following just assumes that the next blob is json
                        // and does not contain line breaks.
                    } else {
                        // TODO: this shouldn't have to parse the json twice
                        let value : Value = match decode_async(&line).unwrap() {
                            AsyncAnswer::Finished(v) => v,
                            AsyncAnswer::Failed(v) => v,
                            AsyncAnswer::Note(v) => v
                        };
                        match value.get("task") {
                            Some(id) if id == task_id =>
                                Some(match decode_async::<T,E,N>(&line).unwrap() {
                                    AsyncAnswer::Finished(data)
                                        => return Some(Ok(data)),
                                    AsyncAnswer::Failed(failed)
                                        => return Some(Err(failed)),
                                    AsyncAnswer::Note(val) => prog(val)

                                }),
                            _ => return None
                        };
                    }
                }
            }
        }
         unreachable!{}
        None
    }
}