use derive_more::Display;

// Set layer

#[derive(Clone, PartialEq, Display, Debug)]
pub enum BuiltIn {
    Nat,
    Int,
    Float,
    Str,
    Bool,
}

#[derive(Clone, PartialEq, Display, Debug)]
#[display("{name} : {set}")]
pub struct RecordField {
    pub name: String,
    pub set: Set,
}

#[derive(Clone, PartialEq, Display, Debug)]
#[display("{name} : {set}")]
pub struct VariantField {
    pub name: String,
    pub set: Set,
}

#[derive(Clone, PartialEq, Display, Debug)]
pub enum Set {
    #[display("{_0}")]
    BuiltIn(BuiltIn),

    #[display("record {{ {} }}", _0.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" , "))]
    Record(Vec<RecordField>),

    #[display("variant [ {} ]", _0.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" | "))]
    Variant(Vec<VariantField>),

    #[display("set-of({_0})")]
    ClaimedSet(Instance),

    #[display("{_0}")]
    Var(String),
}

// Signature layer

#[derive(Clone, PartialEq, Display, Debug)]
#[display("({name} : {set})")]
pub struct Param {
    pub name: String,
    pub set: Set,
}

#[derive(Clone, PartialEq, Display, Debug)]
#[display("{name} :: {signature}")]
pub struct SigField {
    pub name: String,
    pub signature: Signature,
}

#[derive(Clone, PartialEq, Display, Debug)]
pub enum Signature {
    #[display("Set")]
    Set,

    #[display("theory {{ {} }}", _0.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" , "))]
    Theory(Vec<SigField>),

    #[display("{} -> {}", params.iter().map(|p| p.to_string()).collect::<Vec<_>>().join(", "), codomain)]
    Ext {
        params: Vec<Param>,
        codomain: Box<Signature>,
    },

    #[display("{_0}")]
    Var(String),
}

// Element layer

#[derive(Clone, PartialEq, Display, Debug)]
pub enum Literal {
    Nat(u64),
    Int(i64),
    Float(f64),
    Str(String),
    Bool(bool),
}

#[derive(Clone, PartialEq, Display, Debug)]
#[display(".{name} = {element}")]
pub struct ElemAssign {
    pub name: String,
    pub element: Element,
}

#[derive(Clone, PartialEq, Display, Debug)]
#[display(".{tag} {bound} => {body}")]
pub struct CaseArm {
    pub tag: String,
    pub bound: String,
    pub body: Element,
}

#[derive(Clone, PartialEq, Display, Debug)]
pub enum Element {
    #[display("{_0}")]
    Literal(Literal),

    #[display("{_0}")]
    Var(String),

    #[display("{{ {} }}", _0.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(" , "))]
    Record(Vec<ElemAssign>),

    #[display("{element} .{field}")]
    Project {
        element: Box<Element>,
        field: String,
    },

    #[display("{field}. {element}")]
    Inject {
        field: String,
        element: Box<Element>,
    },

    #[display("case {} of {{ {} }}", scrutinee, arms.iter().map(|a| a.to_string()).collect::<Vec<_>>().join(" | "))]
    Case {
        scrutinee: Box<Element>,
        arms: Vec<CaseArm>,
    },
}

// Instance layer

#[derive(Clone, PartialEq, Display, Debug)]
#[display(".{name} = {instance}")]
pub struct InstAssign {
    pub name: String,
    pub instance: Instance,
}

#[derive(Clone, PartialEq, Display, Debug)]
pub enum Instance {
    #[display("({_0} :: Set)")]
    SetCoerce(Box<Set>),

    #[display("{_0}")]
    Var(String),

    #[display("{{ {} }}", _0.iter().map(|f| f.to_string()).collect::<Vec<_>>().join(", "))]
    Record(Vec<InstAssign>),

    #[display("for {}, {body}", params.iter().map(|p| p.to_string()).collect::<Vec<_>>().join(""))]
    For {
        params: Vec<Param>,
        body: Box<Instance>,
    },

    #[display("{_0} {_1}")]
    App(Box<Instance>, Box<Element>),

    #[display("{instance} .{field}")]
    Project {
        instance: Box<Instance>,
        field: String,
    },
}

// Declarations

#[derive(Clone, PartialEq, Display, Debug)]
pub enum Decl {
    #[display("let set {name} = {set}")]
    Set { name: String, set: Set },

    #[display("let element {name} : {set} = {element}")]
    Element {
        name: String,
        set: Set,
        element: Element,
    },

    #[display("let signature {name} = {signature}")]
    Signature { name: String, signature: Signature },

    #[display("let instance {name} :: {signature} = {instance}")]
    Instance {
        name: String,
        signature: Signature,
        instance: Instance,
    },
}

#[derive(Display, Debug)]
#[display("{}", _0.iter().map(|d| d.to_string()).collect::<Vec<_>>().join("\n"))]
pub struct Programme(pub Vec<Decl>);