use std::marker::PhantomData;
use std::sync::Arc;
use std::rc::Rc;
use std::cell::{RefMut, RefCell};
use std::sync::{MutexGuard, Mutex};

type B = CopyingBacktracker;
type C = DFSController<<B as Backtracker>::Node>;

pub struct CPLabelChoice {
    pub x: i64,
    pub val: i64,
}

pub trait CPPropagator<K: CPSolverKernel> {
    fn post(&mut self, solver: Arc<K>) -> Result<(),()>;
}

impl<E: CPSearchExplorer> CPHeuristicFactory<E> for FirstFailFactory {
    type H = FirstFailSearch;
}

pub struct Model {
}

unsafe impl Sync for Model {}

pub struct CopyingBacktracker {
}

impl Backtracker for CopyingBacktracker {
    type Node = CPCopyingSearchNode;
}

pub struct CPCopyingSearchNode {
}

pub struct TrailingBacktracker {
}

#[derive(Clone)]
pub struct FirstFailFactory {}

pub trait Solver {
    fn solve(self);
}

impl<H> Solver for CPSequentialSolver<H>
    where H: CPHeuristicFactory<CPWorker<B, C>> + 'static {

    fn solve(mut self) {
    }
}

pub trait CPScheduledPropagation<K>
    where K: CPSolverKernel {
    fn propagate(&mut self, &mut K) -> Result<(),()>;
    fn is_scheduled(&self, solver: &K) -> bool;
    fn notify_scheduled(&mut self, solver: &K);
}

/// A trait defining a backtrackable value
pub trait Backtrackable {
    type B: Backtracker;
    type V: Copy;
    fn new(val: Self::V, backtracker: &mut Self::B) -> Self;
    fn set(&mut self, val: Self::V, backtracker: &mut Self::B);
    fn get(&self) -> Self::V;
}

pub struct CPKernelEvents {
    presolve_begin: Vec<Box<FnMut()>>,
    search_begin: Vec<Box<FnMut()>>,
    search_end: Vec<Box<FnMut()>>,
    fixedpoint: Vec<Box<FnMut()>>,
    fail: Vec<Box<FnMut()>>,
}

pub trait CPSearchExplorer {
    fn domain_size(&self, x: i64) -> usize;
    fn is_domain_bound(&self, x: i64) -> bool;
    fn domain_min(&self, x: i64) -> i64;
    fn domain_max(&self, x: i64) -> i64;
}

pub trait CPLabelingHeuristic<S: CPSearchExplorer> {
    fn next_for(&mut self, x: i64, solver: &mut S) -> Option<CPLabelChoice>;
    fn next(&mut self, solver: &mut S) -> Option<CPLabelChoice>;
}

pub trait CPHeuristicFactory<E: CPSearchExplorer>: Clone + Send + Sync {
    type H: CPLabelingHeuristic<E>;
}

pub struct CustomSearch<S: CPSearchExplorer + CPSolverKernel> {
    p: PhantomData<S>
}

pub trait HeuristicBuilder<E: CPSearchExplorer> {
    type H: CPLabelingHeuristic<E>;

    fn finalize(self) -> Self::H;
}

pub struct FirstFailSearch {}

pub struct CustomSearchFactory<E, F>
    where E: CPSearchExplorer,
          F: 'static + Fn(&mut HeuristicBuilder<E, H=CustomSearch<E>>) {
    build_func: Arc<F>,
    _phantom: PhantomData<E>,
}

impl<E, F> CPHeuristicFactory<E> for CustomSearchFactory<E, F>
    where E: CPSearchExplorer + CPSolverKernel,
          F: 'static + Fn(&mut HeuristicBuilder<E, H=CustomSearch<E>>) {
    type H = CustomSearch<E>;
}

pub struct CPWorker<B, C> where
    B: Backtracker + 'static,
    C: SearchController<B::Node> {

    pub props: PhantomData<C>,
    pub backtracker: B,
    pub events: Mutex<CPKernelEvents>,
}

pub trait Backtracker where Self: Sized {
    type Node: CPSearchNode;
}

pub trait CPSolverKernel {
    type B: Backtracker;
    type C: SearchController<<Self::B as Backtracker>::Node>;
    
    fn backtracker(&self) -> &Self::B;
    fn backtracker_mut(&mut self) -> &mut Self::B;
    fn min(&self, y: i64) -> i64;
    fn max(&self, y: i64) -> i64;
    fn contains(&self, y: i64, val: i64) -> bool;
    fn count(&self, y: i64) -> i64;
    fn is_bound(&self, y: i64) -> bool;
    fn bind(&mut self, y: i64, val: i64) -> Result<(),()>;
    fn remove(&mut self, y: i64, val: i64) -> Result<(),()>;
    fn remove_lt(&mut self, y: i64, val: i64)->Result<(),()>;
    fn remove_gt(&mut self, y: i64, val: i64)->Result<(),()>;
    fn enforce_choice(&mut self, choice: CPLabelChoice) -> Result<(), ()>;
    fn enforce_objective_bounds(&mut self) -> Result<(), ()>;
    fn capture_objective_bounds(&self) -> (Option<i64>, Option<i64>);
    fn schedule(&mut self, propagation: Rc<RefCell<CPScheduledPropagation<Self>>>);
    fn new_scheduled_propagation<F>(&mut self, f: F)
        where F: 'static + FnMut(&mut Self) -> Result<(),()>;
    fn print_domain(&self, y: i64);
}

impl<B, C> CPSolverKernel for CPWorker<B, C>
    where B: Backtracker,
          C: SearchController<B::Node> + 'static {
    type B = B;
    type C = C;
    
    #[inline]
    fn backtracker(&self) -> &B {
        &self.backtracker
    }

    #[inline]
    fn backtracker_mut(&mut self) -> &mut B {
        &mut self.backtracker
    }
    
    #[inline]
    fn min(&self, y: i64) -> i64 {
        0
    }

    #[inline]
    fn max(&self, y: i64) -> i64 {
        0
    }

    #[inline]
    fn contains(&self, y: i64, val: i64) -> bool {
        true
    }

    #[inline]
    fn count(&self, y: i64) -> i64 {
        0
    }

    #[inline]
    fn is_bound(&self, y: i64) -> bool {
        true
    }

    #[inline]
    fn bind(&mut self, y: i64, val: i64) -> Result<(),()> {
        Ok(())
    }

    #[inline]
    fn remove(&mut self, y: i64, val: i64) -> Result<(),()> {
        Ok(())
    }

    #[inline]
    fn remove_lt(&mut self, y: i64, val: i64) -> Result<(),()> {
        Ok(())
    }

    #[inline]
    fn remove_gt(&mut self, y: i64, val: i64) -> Result<(),()> {
        Ok(())
    }

    #[inline]
    fn enforce_choice(&mut self, choice: CPLabelChoice) -> Result<(), ()> {
        Ok(())
    }

    #[inline]
    fn enforce_objective_bounds(&mut self) -> Result<(), ()> {
        Ok(())
    }

    #[inline]
    fn capture_objective_bounds(&self) -> (Option<i64>, Option<i64>) {
        (None, None)
    }
        
    #[inline]
    fn schedule(&mut self, propagation: Rc<RefCell<CPScheduledPropagation<Self>>>) {
    }
    
    fn new_scheduled_propagation<F>(&mut self, f: F)
        where F: 'static + FnMut(&mut Self) -> Result<(),()> {
    }

    fn print_domain(&self, y: i64) {
    }
}

impl<E, F> Clone for CustomSearchFactory<E, F>
    where E: CPSearchExplorer + CPSolverKernel,
          F: 'static + Fn(&mut HeuristicBuilder<E, H=CustomSearch<E>>) {

    fn clone(&self) -> CustomSearchFactory<E, F> {
        CustomSearchFactory {
            build_func: self.build_func.clone(),
            _phantom: PhantomData,
        }
    }
}

pub trait CPSearchNode where Self: Sized {
    fn label_choice(&self) -> Option<CPLabelChoice>;
    fn objective_bounds(&self) -> (Option<i64>, Option<i64>);
    fn restore<K>(self, solver: &mut K) -> Result<(), ()>
        where K: CPSolverKernel,
              K::B: Backtracker<Node=Self>,
              K::C: SearchController<Self>;
}

impl<S> CPLabelingHeuristic<S> for CustomSearch<S>
    where S: CPSearchExplorer + CPSolverKernel {

    fn next_for(&mut self, x: i64, solver: &mut S) -> Option<CPLabelChoice> {
        None
    }
    
    fn next(&mut self, solver: &mut S) -> Option<CPLabelChoice> {
        None
    }
    
}

impl CPSearchNode for CPCopyingSearchNode {

    #[inline]
    fn label_choice(&self) -> Option<CPLabelChoice> {
        None
    }

    #[inline]
    fn objective_bounds(&self) -> (Option<i64>, Option<i64>) {
        (None, None)
    }

    #[inline]
    fn restore<K>(self, solver: &mut K) -> Result<(), ()>
        where K: CPSolverKernel,
              K::B: Backtracker<Node=Self>,
              K::C: SearchController<Self> {
        Ok(())
    }
}

pub trait SearchController<N: CPSearchNode> {
    fn set_root(&mut self, n: N);
    fn push_node(&mut self, n: N);
    fn pop_node(&mut self) -> Option<N>;
    fn node_count(&self) -> usize;
    fn objective_bounds(&self) -> (Option<i64>, Option<i64>);
    fn update_primal_bound(&mut self, bnd: i64);
}

pub trait CPSolver<H> : Solver
    where H: CPHeuristicFactory<Self::E> {    
    type E: CPSearchExplorer;
    
    fn new(model: Arc<Model>) -> Self
        where Self: CPSolver<FirstFailFactory>;
    fn with_heuristic(model: Arc<Model>, heuristic: H) -> Self;
}

pub struct CPSequentialSolver<H>
    where H: CPHeuristicFactory<CPWorker<B, C>> {
    controller: PhantomData<C>,
    heuristic: H,
}

impl<H> CPSolver<H> for CPSequentialSolver<H>
    where H: CPHeuristicFactory<CPWorker<B, C>> + 'static {
    type E = CPWorker<B, C>;

    fn new(model: Arc<Model>) -> Self
        where Self: CPSolver<FirstFailFactory> {
        let heur = FirstFailFactory::new();
        CPSequentialSolver::with_heuristic(model, heur)
    }
    
    fn with_heuristic(model: Arc<Model>, heuristic: H)
                      -> CPSequentialSolver<H> {
        let solver: CPSequentialSolver<H> =
            CPSequentialSolver {
                controller: PhantomData,
                heuristic: heuristic,
            };
        solver
    }
}

impl FirstFailFactory {
    pub fn new() -> FirstFailFactory {
        FirstFailFactory {}
    }
}

impl<S> CPLabelingHeuristic<S> for FirstFailSearch
    where S: CPSearchExplorer {

    fn next_for(&mut self, x: i64, solver: &mut S) -> Option<CPLabelChoice> {
        None
    }
    
    fn next(&mut self, solver: &mut S) -> Option<CPLabelChoice> {
        None
    }
    
}

pub struct DFSController<N: CPSearchNode> {
    stack: Vec<N>,
    objective_bounds: (Option<i64>, Option<i64>),
}

impl<N: CPSearchNode> DFSController<N> {

    pub fn new() -> DFSController<N> {
        DFSController {
            stack: vec![],
            objective_bounds: (None, None),
        }
    }
}

impl<N: CPSearchNode> SearchController<N> for DFSController<N> {

    fn set_root(&mut self, n: N) {
        self.stack.push(n);
    }
    
    #[inline]
    fn push_node(&mut self, n: N) {
        self.stack.push(n);
    }

    #[inline]
    fn pop_node(&mut self) -> Option<N> {
        self.stack.pop()
    }

    #[inline]
    fn node_count(&self) -> usize {
        self.stack.len()
    }

    #[inline]
    fn objective_bounds(&self) -> (Option<i64>, Option<i64>) {
        self.objective_bounds
    }

    #[inline]
    fn update_primal_bound(&mut self, bnd: i64) {
        self.objective_bounds.1 = Some(bnd)
    }
}


pub trait CPSolverWithSearch<E, F> : CPSolver<CustomSearchFactory<E, F>>
    where E: CPSearchExplorer,
          F: 'static + Fn(&mut HeuristicBuilder<E, H=CustomSearch<E>>),
          CustomSearchFactory<E, F>: CPHeuristicFactory<
                                  <Self as CPSolver<CustomSearchFactory<E, F>>>::E> {

    fn with_search(model: Arc<Model>, search: F) -> Self;
}

impl<F> CPSolverWithSearch<CPWorker<B, C>, F>
    for CPSequentialSolver<CustomSearchFactory<CPWorker<B, C>, F>>
    where F: Fn(&mut HeuristicBuilder<CPWorker<B, C>,
                                      H=CustomSearch<CPWorker<B, C>>>) {

    fn with_search(model: Arc<Model>, search: F) -> Self {
        let heur = CustomSearchFactory::new(search);
        <Self as CPSolver<CustomSearchFactory<CPWorker<B, C>, F>>>
            ::with_heuristic(model, heur)
    }
}

impl<E, F> CustomSearchFactory<E, F>
    where E: CPSearchExplorer,
          F: 'static + Fn(&mut HeuristicBuilder<E, H=CustomSearch<E>>) {
    
    pub fn new(f: F) -> CustomSearchFactory<E, F> {
        CustomSearchFactory {
            build_func: Arc::new(f),
            _phantom: PhantomData,
        }
    }
}

// Implement Send
unsafe impl<E, F> Send for CustomSearchFactory<E, F>
    where E: CPSearchExplorer + CPSolverKernel,
          F: 'static + Fn(&mut HeuristicBuilder<E, H=CustomSearch<E>>) {}

// Implement Sync
unsafe impl<E, F> Sync for CustomSearchFactory<E, F>
    where E: CPSearchExplorer + CPSolverKernel,
          F: 'static + Fn(&mut HeuristicBuilder<E, H=CustomSearch<E>>) {}

unsafe impl Send for FirstFailFactory {}
unsafe impl Sync for FirstFailFactory {}

impl<B, C> CPSearchExplorer for CPWorker<B, C>
    where B: Backtracker,
          C: SearchController<B::Node> + 'static {

    #[inline]
    fn domain_size(&self, x: i64) -> usize {
        self.count(x as i64) as usize
    }

    #[inline]
    fn is_domain_bound(&self, x: i64) -> bool {
        self.is_bound(x as i64)
    }
    
    #[inline]
    fn domain_min(&self, x: i64) -> i64 {
        self.min(x as i64)
    }

    #[inline]
    fn domain_max(&self, x: i64) -> i64 {
        self.max(x as i64)
    }
}

// This code is editable and runnable!
fn main() {
    // A simple integer calculator:
    // `+` or `-` means add or subtract by 1
    // `*` or `/` means multiply or divide by 2
    
    let program = "+ + + +";
    let mut accumulator = 0;
    
    for token in program.chars() {
        match token {
            '+' => accumulator += 1,
            '-' => accumulator -= 1,
            '*' => accumulator *= 2,
            '/' => accumulator /= 2,
            _ => { /* ignore everything else */ }
        }
    }
    
    println!("The program \"{}\" calculates the value {}",
             program, accumulator);
}