use crate::block::BlockIdx;
use crate::stable::StringIdx;
use crate::ty::TyIdx;
use std::collections::BTreeMap;

#[derive(Debug)]
pub struct Clause {
    arguments: BTreeMap<StringIdx, TyIdx>,
    body: BlockIdx,
}

impl Clause {
    pub fn new(arguments: Vec<(StringIdx, TyIdx)>, body: BlockIdx) -> Clause {
        let arguments = arguments.iter().fold(BTreeMap::new(), |mut args, (k, v)| {
            args.insert(k.clone(), v.clone());
            args
        });
        Clause { arguments, body }
    }

    pub fn arguments(&self) -> Vec<(&StringIdx, &TyIdx)> {
        self.arguments.iter().collect()
    }

    pub fn body(&self) -> &BlockIdx {
        &self.body
    }
}

#[derive(Debug, Clone, PartialEq)]
pub struct ClauseIdx(usize);

impl From<usize> for ClauseIdx {
    fn from(i: usize) -> ClauseIdx {
        ClauseIdx(i)
    }
}

impl From<ClauseIdx> for usize {
    fn from(i: ClauseIdx) -> usize {
        i.0
    }
}

impl From<&ClauseIdx> for usize {
    fn from(i: &ClauseIdx) -> usize {
        i.0
    }
}

pub trait Clauseable {
    fn clauses(&self) -> Vec<&Clause>;
    fn has_clauses(&self) -> bool;
    fn push_clause(&mut self, arguments: Vec<(StringIdx, TyIdx)>, block: BlockIdx) -> ClauseIdx;
}