eflint_json/

spec.rs

//  SPEC.rs
//    by Lut99
//
//  Created:
//    08 Nov 2023, 16:25:20
//  Last edited:
//    20 Dec 2023, 10:21:09
//  Auto updated?
//    Yes
//
//  Description:
//!   Defines the interface of the JSON Specification for various
//!   versions. The versions are gated using features.
//!
//!   The interfaces are implemented as [`serde`]-structs, which can be
//!   serialized to- and deserialized from specification-compliant JSON.
//

use std::collections::HashMap;
use std::fmt::{Display, Formatter, Result as FResult};
use std::ops::{Deref, DerefMut, RangeInclusive};

#[cfg(feature = "display_eflint")]
use console::Style;
use enum_debug::EnumDebug;
use serde::de::{Deserializer, Error as _, SeqAccess, Visitor};
use serde::ser::{SerializeSeq, Serializer};
use serde::{Deserialize, Serialize};

#[cfg(feature = "display_eflint")]
use crate::display_eflint::{style, DisplayEFlint, Indent};


/***** TESTS *****/
#[cfg(test)]
mod tests {
    use error_trace::ErrorTrace as _;

    use super::*;

    #[test]
    fn test_ping_request() {
        // Create a ping request
        let req: Request = Request::Ping(RequestPing { common: RequestCommon { version: auxillary::Version::v1_0_0(), extensions: HashMap::new() } });

        // Check serialization
        let sreq: String = match serde_json::to_string_pretty(&req) {
            Ok(text) => text,
            Err(err) => panic!("Failed to serialize Ping-request: {}", err.trace()),
        };
        assert_eq!(
            sreq,
            r#"{
  "kind": "ping",
  "version": "1.0.0"
}"#
        );

        // Check de-serializing it
        let req: Request = match serde_json::from_str(&sreq) {
            Ok(text) => text,
            Err(err) => panic!("Failed to deserialize Ping-request: {}", err.trace()),
        };
        assert!(req.is_ping());
        assert_eq!(req.ping().common.version, auxillary::Version::v1_0_0());
        assert_eq!(req.ping().common.extensions, HashMap::new());
    }

    #[test]
    fn test_ping_response() {
        // Create a ping request
        let res: ResponsePing = ResponsePing { common: ResponseCommon { success: true, errors: vec![] } };

        // Check serialization
        let sres: String = match serde_json::to_string_pretty(&res) {
            Ok(text) => text,
            Err(err) => panic!("Failed to serialize Ping-response: {}", err.trace()),
        };
        assert_eq!(
            sres,
            r#"{
  "success": true
}"#
        );

        // Check de-serializing it
        let res: ResponsePing = match serde_json::from_str(&sres) {
            Ok(text) => text,
            Err(err) => panic!("Failed to deserialize Ping-response: {}", err.trace()),
        };
        assert_eq!(res.common.success, true);
        assert!(res.common.errors.is_empty());
    }

    #[test]
    fn test_handshake_request() {
        // Create a ping request
        let req: Request =
            Request::Handshake(RequestHandshake { common: RequestCommon { version: auxillary::Version::v1_0_0(), extensions: HashMap::new() } });

        // Check serialization
        let sreq: String = match serde_json::to_string_pretty(&req) {
            Ok(text) => text,
            Err(err) => panic!("Failed to serialize Handshake-request: {}", err.trace()),
        };
        assert_eq!(
            sreq,
            r#"{
  "kind": "handshake",
  "version": "1.0.0"
}"#
        );

        // Check de-serializing it
        let req: Request = match serde_json::from_str(&sreq) {
            Ok(text) => text,
            Err(err) => panic!("Failed to deserialize Handshake-request: {}", err.trace()),
        };
        assert!(req.is_handshake());
        assert_eq!(req.handshake().common.version, auxillary::Version::v1_0_0());
        assert_eq!(req.handshake().common.extensions, HashMap::new());
    }

    #[test]
    fn test_handshake_response() {
        // Create a ping request
        let res: ResponseHandshake = ResponseHandshake {
            common: ResponseCommon { success: true, errors: vec![] },
            supported_versions: vec![auxillary::Version::v0_1_0(), auxillary::Version::v1_0_0()],
            supported_extensions: None,
            reasoner: None,
            reasoner_version: None,
            shares_updates: None,
            shares_triggers: None,
            shares_violations: None,
        };

        // Check serialization
        let sres: String = match serde_json::to_string_pretty(&res) {
            Ok(text) => text,
            Err(err) => panic!("Failed to serialize Handshake-response: {}", err.trace()),
        };
        assert_eq!(
            sres,
            r#"{
  "success": true,
  "supported_versions": [
    "0.1.0",
    "1.0.0"
  ]
}"#
        );

        // Check de-serializing it
        let res: ResponseHandshake = match serde_json::from_str(&sres) {
            Ok(text) => text,
            Err(err) => panic!("Failed to deserialize Handshake-response: {}", err.trace()),
        };
        assert_eq!(res.common.success, true);
        assert!(res.common.errors.is_empty());
        assert_eq!(res.supported_versions, vec![auxillary::Version::v0_1_0(), auxillary::Version::v1_0_0()]);
        assert_eq!(res.supported_extensions, None);
        assert_eq!(res.reasoner, None);
        assert_eq!(res.reasoner_version, None);
        assert_eq!(res.shares_updates, None);
        assert_eq!(res.shares_triggers, None);
        assert_eq!(res.shares_violations, None);
    }

    #[test]
    fn test_handshake_response_spec() {
        // Create a ping request
        let res: ResponseHandshake = ResponseHandshake {
            common: ResponseCommon { success: true, errors: vec![] },
            supported_versions: vec![auxillary::Version::v2_0_0(), auxillary::Version::v1_0_0()],
            supported_extensions: Some(HashMap::from([
                (
                    auxillary::Version::v2_0_0(),
                    HashMap::from([
                        ("instances".into(), vec![auxillary::Version(1, 0, 0)]),
                        ("sequential".into(), vec![auxillary::Version(1, 0, 0)]),
                    ]),
                ),
                (auxillary::Version::v1_0_0(), HashMap::from([("sequential".into(), vec![auxillary::Version(1, 0, 0)])])),
            ])),
            reasoner: Some(appendix::Reasoner::EFLINT.into()),
            reasoner_version: None,
            shares_updates: Some(true),
            shares_triggers: Some(true),
            shares_violations: Some(false),
        };

        // Check serialization
        let sres: String = match serde_json::to_string_pretty(&res) {
            Ok(text) => text,
            Err(err) => panic!("Failed to serialize Handshake-response: {}", err.trace()),
        };
        let opt1 = r#"{
  "success": true,
  "supported_versions": [
    "2.0.0",
    "1.0.0"
  ],
  "supported_extensions": {
    "2.0.0": {
      "instances": [
        "1.0.0"
      ],
      "sequential": [
        "1.0.0"
      ]
    },
    "1.0.0": {
      "sequential": [
        "1.0.0"
      ]
    }
  },
  "reasoner": "eflint",
  "shares_updates": true,
  "shares_triggers": true,
  "shares_violations": false
}"#;
        let opt2 = r#"{
  "success": true,
  "supported_versions": [
    "2.0.0",
    "1.0.0"
  ],
  "supported_extensions": {
    "1.0.0": {
      "sequential": [
        "1.0.0"
      ]
    },
    "2.0.0": {
      "instances": [
        "1.0.0"
      ],
      "sequential": [
        "1.0.0"
      ]
    }
  },
  "reasoner": "eflint",
  "shares_updates": true,
  "shares_triggers": true,
  "shares_violations": false
}"#;
        if sres != opt1 && sres != opt2 {
            panic!("Serialized ResponseHandshake is incorrect:\n\nGot:\n{sres}\n\nExpected EITHER:\n{opt1}\n\nExpected OR:\n{opt2}\n\n");
        }

        // Check de-serializing it
        let res: ResponseHandshake = match serde_json::from_str(&sres) {
            Ok(text) => text,
            Err(err) => panic!("Failed to deserialize Handshake-response: {}", err.trace()),
        };
        assert_eq!(res.common.success, true);
        assert!(res.common.errors.is_empty());
        assert_eq!(res.supported_versions, vec![auxillary::Version::v2_0_0(), auxillary::Version::v1_0_0()]);
        assert_eq!(
            res.supported_extensions,
            Some(HashMap::from([
                (
                    auxillary::Version::v2_0_0(),
                    HashMap::from([
                        ("instances".into(), vec![auxillary::Version(1, 0, 0)]),
                        ("sequential".into(), vec![auxillary::Version(1, 0, 0)])
                    ])
                ),
                (auxillary::Version::v1_0_0(), HashMap::from([("sequential".into(), vec![auxillary::Version(1, 0, 0)])])),
            ]))
        );
        assert_eq!(res.reasoner, Some(appendix::Reasoner::EFLINT.into()));
        assert_eq!(res.reasoner_version, None);
        assert_eq!(res.shares_updates, Some(true));
        assert_eq!(res.shares_triggers, Some(true));
        assert_eq!(res.shares_violations, Some(false));
    }

    #[test]
    fn test_inspect_request() {
        // Create a ping request
        let req: Request = Request::Inspect(RequestInspect {
            common:  RequestCommon { version: auxillary::Version::v2_0_0(), extensions: HashMap::new() },
            targets: vec![],
        });

        // Check serialization
        let sreq: String = match serde_json::to_string_pretty(&req) {
            Ok(text) => text,
            Err(err) => panic!("Failed to serialize Inspect-request: {}", err.trace()),
        };
        assert_eq!(
            sreq,
            r#"{
  "kind": "inspect",
  "version": "2.0.0"
}"#
        );

        // Check de-serializing it
        let req: Request = match serde_json::from_str(&sreq) {
            Ok(text) => text,
            Err(err) => panic!("Failed to deserialize Inspect-request: {}", err.trace()),
        };
        assert!(req.is_inspect());
        assert_eq!(req.inspect().common.version, auxillary::Version::v2_0_0());
        assert_eq!(req.inspect().common.extensions, HashMap::new());
        assert_eq!(req.inspect().targets, Vec::<String>::new());
    }

    #[test]
    fn test_inspect_response() {
        // Create a ping request
        let res: ResponseInspect = ResponseInspect { common: ResponseCommon { success: true, errors: vec![] }, phrases: vec![] };

        // Check serialization
        let sres: String = match serde_json::to_string_pretty(&res) {
            Ok(text) => text,
            Err(err) => panic!("Failed to serialize Inspect-response: {}", err.trace()),
        };
        assert_eq!(
            sres,
            r#"{
  "success": true,
  "phrases": []
}"#
        );

        // Check de-serializing it
        let res: ResponseInspect = match serde_json::from_str(&sres) {
            Ok(text) => text,
            Err(err) => panic!("Failed to deserialize Inspect-response: {}", err.trace()),
        };
        assert_eq!(res.common.success, true);
        assert!(res.common.errors.is_empty());
        assert!(res.phrases.is_empty());
    }
}





/***** RUST ERRORS *****/
/// Defines Rust errors, which are not part of the spec but generated by it.
pub mod errors {
    use std::error::Error;
    use std::fmt::{Display, Formatter, Result as FResult};

    /// Defines errors occuring when parsing [`Version`](super::auxillary::Version)s from strings.
    #[derive(Debug)]
    pub enum VersionParseError {
        /// Failed to find the first dot in the version.
        FirstDot { raw: String },
        /// Failed to find the second dot in the version.
        SecondDot { raw: String },
        /// Failed to parse the major version number as a number.
        ParseMajor { raw: String, num: String, err: std::num::ParseIntError },
        /// Failed to parse the minor version number as a number.
        ParseMinor { raw: String, num: String, err: std::num::ParseIntError },
        /// Failed to parse the patch version number as a number.
        ParsePatch { raw: String, num: String, err: std::num::ParseIntError },
    }
    impl Display for VersionParseError {
        fn fmt(&self, f: &mut Formatter<'_>) -> FResult {
            use VersionParseError::*;
            match self {
                FirstDot { raw } => write!(f, "Failed to find first version dot in '{raw}' (separating major- and minor version numbers)"),
                SecondDot { raw } => write!(f, "Failed to find second version dot in '{raw}' (separating minor- and patch version numbers)"),
                ParseMajor { raw, num, .. } => write!(f, "Failed to parse major version number '{num}' in '{raw}' as an integer"),
                ParseMinor { raw, num, .. } => write!(f, "Failed to parse minor version number '{num}' in '{raw}' as an integer"),
                ParsePatch { raw, num, .. } => write!(f, "Failed to parse patch version number '{num}' in '{raw}' as an integer"),
            }
        }
    }
    impl Error for VersionParseError {
        fn source(&self) -> Option<&(dyn Error + 'static)> {
            use VersionParseError::*;
            match self {
                FirstDot { .. } | SecondDot { .. } => None,
                ParseMajor { err, .. } | ParseMinor { err, .. } | ParsePatch { err, .. } => Some(err),
            }
        }
    }

    /// Defines errors occuring when parsing [`AtomicType`](super::auxillary::AtomicType)s from strings.
    #[derive(Debug)]
    pub enum AtomicTypeParseError {
        /// An illegal type string was given.
        Unknown { raw: String },
    }
    impl Display for AtomicTypeParseError {
        fn fmt(&self, f: &mut Formatter<'_>) -> FResult {
            use AtomicTypeParseError::*;
            match self {
                Unknown { raw } => write!(f, "Unknown atomic type '{raw}' (expected 'String' or 'Int')"),
            }
        }
    }
    impl Error for AtomicTypeParseError {}

    /// Defines errors occurring when parsing [`NonEmptyVec`](super::auxillary::NonEmptyVec)s from strings.
    #[derive(Debug)]
    pub enum NonEmptyVecParseError<E> {
        /// Failed to deserialize the vector itself
        Vec { err: E },
        /// The vector was empty
        Empty,
    }
    impl<E: Display> Display for NonEmptyVecParseError<E> {
        #[inline]
        fn fmt(&self, f: &mut Formatter<'_>) -> FResult {
            use NonEmptyVecParseError::*;
            match self {
                Vec { .. } => write!(f, "Failed to deserialize vector"),
                Empty => write!(f, "Vector is empty"),
            }
        }
    }
    impl<E: 'static + Error> Error for NonEmptyVecParseError<E> {
        fn source(&self) -> Option<&(dyn Error + 'static)> {
            use NonEmptyVecParseError::*;
            match self {
                Vec { err } => Some(err),
                Empty => None,
            }
        }
    }

    /// Defines errors occuring when parsing [`ExpressionVarRef`](super::ExpressionVarRef)s from strings.
    #[derive(Debug)]
    pub enum ExpressionVarRefParseError {
        /// Got an empty array
        TooFew,
        /// Got too many elements in the array
        TooMany,
    }
    impl Display for ExpressionVarRefParseError {
        fn fmt(&self, f: &mut Formatter<'_>) -> FResult {
            use ExpressionVarRefParseError::*;
            match self {
                TooFew => write!(f, "Got less than 1 element for variable reference list"),
                TooMany => write!(f, "Got more than 1 element for variable reference list"),
            }
        }
    }
    impl Error for ExpressionVarRefParseError {}

    /// Defines errors occuring when parsing [`TriggerKind`](super::auxillary::TriggerKind)s from strings.
    #[derive(Debug)]
    pub enum TriggerKindParseError {
        /// An illegal kind string was given.
        Unknown { raw: String },
    }
    impl Display for TriggerKindParseError {
        fn fmt(&self, f: &mut Formatter<'_>) -> FResult {
            use TriggerKindParseError::*;
            match self {
                Unknown { raw } => write!(f, "Unknown trigger kind '{raw}' (expected 'act' or 'event')"),
            }
        }
    }
    impl Error for TriggerKindParseError {}

    /// Defines errors occuring when parsing [`ViolationKind`](super::auxillary::ViolationKind)s from strings.
    #[derive(Debug)]
    pub enum ViolationKindParseError {
        /// An illegal kind string was given.
        Unknown { raw: String },
    }
    impl Display for ViolationKindParseError {
        fn fmt(&self, f: &mut Formatter<'_>) -> FResult {
            use ViolationKindParseError::*;
            match self {
                Unknown { raw } => write!(f, "Unknown violation kind '{raw}' (expected 'act', 'duty' or 'invariant')"),
            }
        }
    }
    impl Error for ViolationKindParseError {}
}





/***** AUXILLARY *****/
/// Defines practical structs that are extremely convenient and spec-compliant, but not necessary mentioned in it.
pub mod auxillary {
    use std::cmp::Ordering;
    use std::fmt::{Display, Formatter, Result as FResult};
    use std::marker::PhantomData;
    use std::ops::{Deref, DerefMut};
    use std::str::FromStr;

    use enum_debug::EnumDebug;
    use serde::de::{Deserializer, Visitor};
    use serde::ser::Serializer;
    use serde::{Deserialize, Serialize};

    use super::errors::{AtomicTypeParseError, NonEmptyVecParseError, TriggerKindParseError, VersionParseError, ViolationKindParseError};
    #[cfg(feature = "display_eflint")]
    use crate::display_eflint::DisplayEFlint;


    /// Visitor for any type that uses its [`FromStr`]-implementation.
    ///
    /// # Generics
    /// - `T`: The type for which we can use this visitor.
    struct FromStrVisitor<'s, T> {
        /// The thing to print in [`Visitor::expecting()`].
        what: &'s str,
        /// Allows us to capture `T`
        _ty:  PhantomData<T>,
    }
    impl<'s, T> FromStrVisitor<'s, T> {
        /// Constructor for the FromStrVisitor.
        ///
        /// # Arguments
        /// - `what`: What we're [expecting](Visitor::expecting()). Should complete: "This visitor expects to receive ...".
        ///
        /// # Returns
        /// A new instance of Self that can visit for the given type.
        #[inline]
        fn new(what: &'s str) -> Self { Self { what, _ty: PhantomData::default() } }
    }
    impl<'s, 'de, T: FromStr> Visitor<'de> for FromStrVisitor<'s, T>
    where
        T::Err: Display,
    {
        type Value = T;

        #[inline]
        fn expecting(&self, f: &mut Formatter<'_>) -> FResult { write!(f, "{}", self.what) }

        #[inline]
        fn visit_str<E>(self, v: &str) -> Result<Self::Value, E>
        where
            E: serde::de::Error,
        {
            match T::from_str(v) {
                Ok(res) => Ok(res),
                Err(err) => Err(E::custom(err)),
            }
        }
    }



    /// Toplevel enum that parses \*any\* eFLINT JSON request or response.
    #[derive(Clone, Debug, Deserialize, EnumDebug, Serialize)]
    #[serde(untagged)]
    pub enum Message {
        // Requests
        /// It's a [request](super::Request) of some kind.
        Request(super::Request),

        // Responses
        /// It's a [handshake response](super::ResponseHandshake).
        ResponseHandshake(super::ResponseHandshake),
        /// It's a [phrases response](super::ResponsePhrases).
        ResponsePhrases(super::ResponsePhrases),
        /// It's a [inspect response](super::ResponseInspect).
        ResponseInspect(super::ResponseInspect),
        // NOTE: Important ordering, ping only has common fields so needs to be last to avoid it always being parsed.
        /// It's a [ping response](super::ResponsePing).
        ResponsePing(super::ResponsePing),
    }
    #[cfg(feature = "display_eflint")]
    impl DisplayEFlint for Message {
        #[inline]
        fn eflint_fmt(&self, indent: usize, f: &mut Formatter<'_>) -> FResult {
            match self {
                Self::Request(request) => request.eflint_fmt(indent, f),

                Self::ResponseHandshake(handshake) => handshake.eflint_fmt(indent, f),
                Self::ResponsePhrases(phrases) => phrases.eflint_fmt(indent, f),
                Self::ResponseInspect(inspect) => inspect.eflint_fmt(indent, f),
                Self::ResponsePing(ping) => ping.eflint_fmt(indent, f),
            }
        }
    }



    /// Represents a specification-compliant version number.
    #[derive(Clone, Copy, Debug, Eq, Hash, PartialEq)]
    pub struct Version(pub u32, pub u32, pub u32);
    impl Version {
        /// Constructor for version 0.1.0 of the specification.
        ///
        /// # Returns
        /// A new [`Version`] that represents release 0.1.0.
        #[inline]
        pub const fn v0_1_0() -> Self { Self(0, 1, 0) }

        /// Constructor for version 1.0.0 of the specification.
        ///
        /// # Returns
        /// A new [`Version`] that represents release 1.0.0.
        #[inline]
        pub const fn v1_0_0() -> Self { Self(1, 0, 0) }

        /// Constructor for version 2.0.0 of the specification.
        ///
        /// # Returns
        /// A new [`Version`] that represents release 2.0.0.
        #[inline]
        pub const fn v2_0_0() -> Self { Self(2, 0, 0) }

        /// Returns the major version number in this Version.
        ///
        /// # Returns
        /// An [`u32`] representing the major version number.
        #[inline]
        pub fn major(&self) -> u32 { self.0 }

        /// Returns the minor version number in this Version.
        ///
        /// # Returns
        /// An [`u32`] representing the minor version number.
        #[inline]
        pub fn minor(&self) -> u32 { self.1 }

        /// Returns the patch version number in this Version.
        ///
        /// # Returns
        /// An [`u32`] representing the patch version number.
        #[inline]
        pub fn patch(&self) -> u32 { self.2 }
    }
    impl Ord for Version {
        #[inline]
        fn cmp(&self, other: &Self) -> Ordering { self.0.cmp(&other.0).then_with(|| self.1.cmp(&other.1).then_with(|| self.2.cmp(&other.2))) }
    }
    impl PartialOrd for Version {
        #[inline]
        fn partial_cmp(&self, other: &Self) -> Option<Ordering> { Some(self.cmp(other)) }
    }
    impl<'de> Deserialize<'de> for Version {
        fn deserialize<D>(deserializer: D) -> Result<Self, D::Error>
        where
            D: Deserializer<'de>,
        {
            /// Visitor for the [`Version`].
            struct VersionVisitor;
            impl<'de> Visitor<'de> for VersionVisitor {
                type Value = Version;

                #[inline]
                fn expecting(&self, f: &mut Formatter) -> FResult { write!(f, "a semantic version number") }

                fn visit_str<E>(self, v: &str) -> std::result::Result<Self::Value, E>
                where
                    E: serde::de::Error,
                {
                    match Version::from_str(v) {
                        Ok(version) => Ok(version),
                        Err(err) => Err(E::custom(err)),
                    }
                }
            }

            // Visit the string
            deserializer.deserialize_str(VersionVisitor)
        }
    }
    impl Serialize for Version {
        #[inline]
        fn serialize<S>(&self, serializer: S) -> Result<S::Ok, S::Error>
        where
            S: Serializer,
        {
            // Simply serialize as a tuple with dots
            serializer.serialize_str(&format!("{}.{}.{}", self.0, self.1, self.2))
        }
    }
    impl Display for Version {
        #[inline]
        fn fmt(&self, f: &mut Formatter<'_>) -> FResult { write!(f, "{}.{}.{}", self.0, self.1, self.2) }
    }
    impl FromStr for Version {
        type Err = VersionParseError;

        fn from_str(s: &str) -> Result<Self, Self::Err> {
            // Attempt to split into a major, minor and patch version.
            let (major, minor_patch): (&str, &str) = match s.find('.') {
                Some(pos) => (&s[..pos], &s[pos + 1..]),
                None => return Err(VersionParseError::FirstDot { raw: s.into() }),
            };
            let (minor, patch): (&str, &str) = match minor_patch.find('.') {
                Some(pos) => (&minor_patch[..pos], &minor_patch[pos + 1..]),
                None => return Err(VersionParseError::SecondDot { raw: s.into() }),
            };

            // Parse the numbers individually
            let major: u32 = match u32::from_str(major) {
                Ok(major) => major,
                Err(err) => return Err(VersionParseError::ParseMajor { raw: s.into(), num: major.into(), err }),
            };
            let minor: u32 = match u32::from_str(minor) {
                Ok(minor) => minor,
                Err(err) => return Err(VersionParseError::ParseMinor { raw: s.into(), num: minor.into(), err }),
            };
            let patch: u32 = match u32::from_str(patch) {
                Ok(patch) => patch,
                Err(err) => return Err(VersionParseError::ParsePatch { raw: s.into(), num: patch.into(), err }),
            };

            // Alright, done!
            Ok(Self(major, minor, patch))
        }
    }



    /// Groups particular [`Phrase`](super::Phrase)s together into phrase subclasses.
    #[derive(Clone, Copy, Debug, EnumDebug, Eq, Hash, PartialEq)]
    pub enum PhraseSubclass {
        /// Boolean- or instance queries.
        Query,
        /// Postulation, triggers.
        Statement,
        /// Definitions of Facts, Events, Acts, etc.
        Definition,
    }

    /// The possible types that are considered as open-ended domains for [atomic facts](super::PhraseAtomicFact).
    #[derive(Clone, Copy, Debug, EnumDebug, Eq, Hash, PartialEq)]
    pub enum AtomicType {
        /// Open-ended string domain
        String,
        /// Open-ended integer domain
        Integer,
    }
    impl AtomicType {
        /// Creates a new [`AtomicType::String`] (but in such a way we can use it as a serde default).
        ///
        /// # Returns
        /// A new instance of self that is String.
        #[inline]
        pub fn string() -> Self { Self::String }

        /// Creates a new [`AtomicType::Integer`] (but in such a way we can use it as a serde default).
        ///
        /// # Returns
        /// A new instance of self that is Integer.
        #[inline]
        pub fn integer() -> Self { Self::Integer }
    }
    impl Display for AtomicType {
        fn fmt(&self, f: &mut Formatter<'_>) -> FResult {
            match self {
                Self::String => write!(f, "String"),
                Self::Integer => write!(f, "Integer"),
            }
        }
    }
    impl FromStr for AtomicType {
        type Err = AtomicTypeParseError;

        fn from_str(s: &str) -> Result<Self, Self::Err> {
            match s {
                "String" => Ok(Self::String),
                "Int" => Ok(Self::Integer),
                raw => Err(AtomicTypeParseError::Unknown { raw: raw.into() }),
            }
        }
    }
    impl<'de> Deserialize<'de> for AtomicType {
        #[inline]
        fn deserialize<D>(deserializer: D) -> Result<Self, D::Error>
        where
            D: Deserializer<'de>,
        {
            // Simply deserialize using its FromStr
            deserializer.deserialize_str(FromStrVisitor::new("an atomic type identifier"))
        }
    }
    impl Serialize for AtomicType {
        #[inline]
        fn serialize<S>(&self, serializer: S) -> Result<S::Ok, S::Error>
        where
            S: Serializer,
        {
            match self {
                AtomicType::String => serializer.serialize_str("String"),
                AtomicType::Integer => serializer.serialize_str("Int"),
            }
        }
    }

    /// A newtype for a vector that deserializes non-empty only.
    #[derive(Clone, Debug)]
    pub struct NonEmptyVec<T>(pub Vec<T>);
    impl<T> Deref for NonEmptyVec<T> {
        type Target = Vec<T>;

        #[inline]
        fn deref(&self) -> &Self::Target { &self.0 }
    }
    impl<T> DerefMut for NonEmptyVec<T> {
        #[inline]
        fn deref_mut(&mut self) -> &mut Self::Target { &mut self.0 }
    }
    impl<'de, T: Deserialize<'de>> Deserialize<'de> for NonEmptyVec<T> {
        fn deserialize<D>(deserializer: D) -> Result<Self, D::Error>
        where
            D: Deserializer<'de>,
        {
            // Deserialize the vector first
            let data: Vec<T> = match Vec::deserialize(deserializer) {
                Ok(data) => data,
                Err(err) => return Err(<D::Error as serde::de::Error>::custom(NonEmptyVecParseError::Vec { err })),
            };

            // Assert it isn't empty
            if !data.is_empty() { Ok(Self(data)) } else { Err(<D::Error as serde::de::Error>::custom(NonEmptyVecParseError::<D::Error>::Empty)) }
        }
    }
    impl<T: Serialize> Serialize for NonEmptyVec<T> {
        #[inline]
        fn serialize<S>(&self, serializer: S) -> Result<S::Ok, S::Error>
        where
            S: Serializer,
        {
            self.0.serialize(serializer)
        }
    }

    /// Defines the possible types that can be extended.
    #[derive(Clone, Copy, Debug, EnumDebug, Eq, Hash, PartialEq)]
    pub enum ExtendKind {
        /// An eFLINT Fact is being extended.
        Fact,
        /// An eFLINT Event is being extended.
        Event,
        /// An eFLINT Act is being extended.
        Act,
        /// An eFLINT Duty is being extended.
        Duty,
    }



    /// The type of [`Expression`](super::Expression)s, which is either a boolean expression or an instance expression.
    ///
    /// Note that strings and integers are seen as instances.
    #[derive(Clone, Copy, Debug, EnumDebug, Eq, Hash, PartialEq)]
    pub enum ExpressionKind {
        /// Boolean expressions evaluate to true or false.
        Boolean,
        /// Instance expressions evaluate to zero or more instances of a particular type.
        Instance,
    }



    /// Determines what types may be triggered.
    #[derive(Clone, Copy, Debug, EnumDebug, Eq, Hash, PartialEq)]
    pub enum TriggerKind {
        /// An eFLINT Act was triggered.
        Act,
        /// An eFLINT Event was triggered.
        Event,
    }
    impl Display for TriggerKind {
        fn fmt(&self, f: &mut Formatter<'_>) -> FResult {
            match self {
                Self::Act => write!(f, "Act"),
                Self::Event => write!(f, "Event"),
            }
        }
    }
    impl FromStr for TriggerKind {
        type Err = TriggerKindParseError;

        fn from_str(s: &str) -> Result<Self, Self::Err> {
            match s {
                "act" => Ok(Self::Act),
                "event" => Ok(Self::Event),
                raw => Err(TriggerKindParseError::Unknown { raw: raw.into() }),
            }
        }
    }
    impl<'de> Deserialize<'de> for TriggerKind {
        fn deserialize<D>(deserializer: D) -> Result<Self, D::Error>
        where
            D: Deserializer<'de>,
        {
            // Visit using the visitor
            deserializer.deserialize_str(FromStrVisitor::new("a trigger kind identifier"))
        }
    }
    impl Serialize for TriggerKind {
        fn serialize<S>(&self, serializer: S) -> Result<S::Ok, S::Error>
        where
            S: Serializer,
        {
            match self {
                TriggerKind::Act => serializer.serialize_str("act"),
                TriggerKind::Event => serializer.serialize_str("event"),
            }
        }
    }

    /// Determines what types may be violated.
    #[derive(Clone, Copy, Debug, EnumDebug, Eq, Hash, PartialEq)]
    pub enum ViolationKind {
        /// An eFLINT Act was violated.
        Act,
        /// An eFLINT Duty was violated.
        Duty,
        /// An eFLINT Invariant was violated.
        Invariant,
    }
    impl Display for ViolationKind {
        fn fmt(&self, f: &mut Formatter<'_>) -> FResult {
            match self {
                Self::Act => write!(f, "Act"),
                Self::Duty => write!(f, "Duty"),
                Self::Invariant => write!(f, "Invariant"),
            }
        }
    }
    impl FromStr for ViolationKind {
        type Err = ViolationKindParseError;

        fn from_str(s: &str) -> Result<Self, Self::Err> {
            match s {
                "act" => Ok(Self::Act),
                "duty" => Ok(Self::Duty),
                "invariant" => Ok(Self::Invariant),
                raw => Err(ViolationKindParseError::Unknown { raw: raw.into() }),
            }
        }
    }
    impl<'de> Deserialize<'de> for ViolationKind {
        fn deserialize<D>(deserializer: D) -> Result<Self, D::Error>
        where
            D: Deserializer<'de>,
        {
            // Visit using the visitor
            deserializer.deserialize_str(FromStrVisitor::new("a violation kind identifier"))
        }
    }
    impl Serialize for ViolationKind {
        fn serialize<S>(&self, serializer: S) -> Result<S::Ok, S::Error>
        where
            S: Serializer,
        {
            match self {
                ViolationKind::Act => serializer.serialize_str("act"),
                ViolationKind::Duty => serializer.serialize_str("duty"),
                ViolationKind::Invariant => serializer.serialize_str("invariant"),
            }
        }
    }
}





/***** DEFAULT FUNCTIONS *****/
/// Defines the default for the `actor`-field in [`PhraseAct`].
///
/// # Returns
/// A new String that encodes `"author"`.
#[inline]
fn default_phrase_act_actor() -> String { "author".into() }





/***** TOPLEVEL INTERACTION *****/
/// The toplevel request of the JSON specification.
///
/// This comes in three variants:
/// - [`Request::Ping`] to establish if a server is online.
/// - [`Request::Handshake`] to retrieve server metadata, such as supported versions, reasoner used, etc.
/// - [`Request::Phrases`] to send eFLINT phrases to the server and do reasoning.
#[derive(Clone, Debug, Deserialize, EnumDebug, Serialize)]
#[serde(tag = "kind")]
pub enum Request {
    /// The Ping-request can be used to establish if a server is online and reachable.
    #[serde(rename = "ping")]
    Ping(RequestPing),
    /// The Handshake-request can be used to retrieve server metadata, such as supported versions, reasoner used, etc.
    #[serde(rename = "handshake")]
    Handshake(RequestHandshake),
    /// The Phrases-request can be used to do reasoning on the server by sending phrases.
    #[serde(rename = "phrases")]
    Phrases(RequestPhrases),
    /// The Inspect-request can be used to query the server's state.
    #[serde(rename = "inspect")]
    Inspect(RequestInspect),
}
impl Request {
    /// Checks if this request is a [`Request::Ping`].
    ///
    /// # Returns
    /// True if it is, or false if not.
    #[inline]
    pub fn is_ping(&self) -> bool { matches!(self, Self::Ping(_)) }

    /// Returns this Request as if it's a [`Request::Ping`].
    ///
    /// # Returns
    /// A reference to the internal [`RequestPing`] object.
    ///
    /// # Panics
    /// This function may panic if this Request is _not_ a [`Request::Ping`].
    #[inline]
    #[track_caller]
    pub fn ping(&self) -> &RequestPing {
        if let Request::Ping(p) = self {
            p
        } else {
            panic!("Cannot unwrap a {:?} as a Request::Ping", self.variant());
        }
    }

    /// Returns this Request as if it's a [`Request::Ping`].
    ///
    /// # Returns
    /// A mutable reference to the internal [`RequestPing`] object.
    ///
    /// # Panics
    /// This function may panic if this Request is _not_ a [`Request::Ping`].
    #[inline]
    #[track_caller]
    pub fn ping_mut(&mut self) -> &mut RequestPing {
        if let Request::Ping(p) = self {
            p
        } else {
            panic!("Cannot unwrap a {:?} as a Request::Ping", self.variant());
        }
    }

    /// Returns this Request as if it's a [`Request::Ping`].
    ///
    /// # Returns
    /// The internal [`RequestPing`] object.
    ///
    /// # Panics
    /// This function may panic if this Request is _not_ a [`Request::Ping`].
    #[inline]
    #[track_caller]
    pub fn into_ping(self) -> RequestPing {
        if let Request::Ping(p) = self {
            p
        } else {
            panic!("Cannot unwrap a {:?} as a Request::Ping", self.variant());
        }
    }

    /// Checks if this request is a [`Request::Handshake`].
    ///
    /// # Returns
    /// True if it is, or false if not.
    #[inline]
    pub fn is_handshake(&self) -> bool { matches!(self, Self::Handshake(_)) }

    /// Returns this Request as if it's a [`Request::Handshake`].
    ///
    /// # Returns
    /// A reference to the internal [`RequestHandshake`] object.
    ///
    /// # Panics
    /// This function may panic if this Request is _not_ a [`Request::Handshake`].
    #[inline]
    #[track_caller]
    pub fn handshake(&self) -> &RequestHandshake {
        if let Request::Handshake(h) = self {
            h
        } else {
            panic!("Cannot unwrap a {:?} as a Request::Handshake", self.variant());
        }
    }

    /// Returns this Request as if it's a [`Request::Handshake`].
    ///
    /// # Returns
    /// A mutable reference to the internal [`RequestHandshake`] object.
    ///
    /// # Panics
    /// This function may panic if this Request is _not_ a [`Request::Handshake`].
    #[inline]
    #[track_caller]
    pub fn handshake_mut(&mut self) -> &mut RequestHandshake {
        if let Request::Handshake(h) = self {
            h
        } else {
            panic!("Cannot unwrap a {:?} as a Request::Handshake", self.variant());
        }
    }

    /// Returns this Request as if it's a [`Request::Handshake`].
    ///
    /// # Returns
    /// The internal [`RequestHandshake`] object.
    ///
    /// # Panics
    /// This function may panic if this Request is _not_ a [`Request::Handshake`].
    #[inline]
    #[track_caller]
    pub fn into_handshake(self) -> RequestHandshake {
        if let Request::Handshake(h) = self {
            h
        } else {
            panic!("Cannot unwrap a {:?} as a Request::Handshake", self.variant());
        }
    }

    /// Checks if this request is a [`Request::Phrases`].
    ///
    /// # Returns
    /// True if it is, or false if not.
    #[inline]
    pub fn is_phrases(&self) -> bool { matches!(self, Self::Phrases(_)) }

    /// Returns this Request as if it's a [`Request::Phrases`].
    ///
    /// # Returns
    /// A reference to the internal [`RequestPhrases`] object.
    ///
    /// # Panics
    /// This function may panic if this Request is _not_ a [`Request::Phrases`].
    #[inline]
    #[track_caller]
    pub fn phrases(&self) -> &RequestPhrases {
        if let Request::Phrases(p) = self {
            p
        } else {
            panic!("Cannot unwrap a {:?} as a Request::Phrases", self.variant());
        }
    }

    /// Returns this Request as if it's a [`Request::Phrases`].
    ///
    /// # Returns
    /// A mutable reference to the internal [`RequestPhrases`] object.
    ///
    /// # Panics
    /// This function may panic if this Request is _not_ a [`Request::Phrases`].
    #[inline]
    #[track_caller]
    pub fn phrases_mut(&mut self) -> &mut RequestPhrases {
        if let Request::Phrases(p) = self {
            p
        } else {
            panic!("Cannot unwrap a {:?} as a Request::Phrases", self.variant());
        }
    }

    /// Returns this Request as if it's a [`Request::Phrases`].
    ///
    /// # Returns
    /// The internal [`RequestPhrases`] object.
    ///
    /// # Panics
    /// This function may panic if this Request is _not_ a [`Request::Phrases`].
    #[inline]
    #[track_caller]
    pub fn into_phrases(self) -> RequestPhrases {
        if let Request::Phrases(p) = self {
            p
        } else {
            panic!("Cannot unwrap a {:?} as a Request::Phrases", self.variant());
        }
    }

    /// Checks if this request is a [`Request::Inspect`].
    ///
    /// # Returns
    /// True if it is, or false if not.
    #[inline]
    pub fn is_inspect(&self) -> bool { matches!(self, Self::Inspect(_)) }

    /// Returns this Request as if it's a [`Request::Inspect`].
    ///
    /// # Returns
    /// A reference to the internal [`RequestInspect`] object.
    ///
    /// # Panics
    /// This function may panic if this Request is _not_ a [`Request::Inspect`].
    #[inline]
    #[track_caller]
    pub fn inspect(&self) -> &RequestInspect {
        if let Request::Inspect(p) = self {
            p
        } else {
            panic!("Cannot unwrap a {:?} as a Request::Inspect", self.variant());
        }
    }

    /// Returns this Request as if it's a [`Request::Inspect`].
    ///
    /// # Returns
    /// A mutable reference to the internal [`RequestInspect`] object.
    ///
    /// # Panics
    /// This function may panic if this Request is _not_ a [`Request::Inspect`].
    #[inline]
    #[track_caller]
    pub fn inspect_mut(&mut self) -> &mut RequestInspect {
        if let Request::Inspect(p) = self {
            p
        } else {
            panic!("Cannot unwrap a {:?} as a Request::Inspect", self.variant());
        }
    }

    /// Returns this Request as if it's a [`Request::Inspect`].
    ///
    /// # Returns
    /// The internal [`RequestInspect`] object.
    ///
    /// # Panics
    /// This function may panic if this Request is _not_ a [`Request::Inspect`].
    #[inline]
    #[track_caller]
    pub fn into_inspect(self) -> RequestInspect {
        if let Request::Inspect(i) = self {
            i
        } else {
            panic!("Cannot unwrap a {:?} as a Request::Inspect", self.variant());
        }
    }
}
#[cfg(feature = "display_eflint")]
impl DisplayEFlint for Request {
    #[inline]
    fn eflint_fmt(&self, indent: usize, f: &mut Formatter<'_>) -> FResult {
        // Write the contents of the request
        match self {
            Self::Ping(ping) => ping.eflint_fmt(indent, f),
            Self::Handshake(handshake) => handshake.eflint_fmt(indent, f),
            Self::Phrases(phrases) => phrases.eflint_fmt(indent, f),
            Self::Inspect(inspect) => inspect.eflint_fmt(indent, f),
        }
    }
}

/// Determines the common fields for all requests.
///
/// Note that this does not include the `kind`-field, as that's part of the parent [`Request`].
#[derive(Clone, Debug, Deserialize, Serialize)]
pub struct RequestCommon {
    /// The version of the specification to use for this interaction.
    pub version:    auxillary::Version,
    /// An optional map of extensions to the version.
    #[serde(default = "HashMap::new", skip_serializing_if = "HashMap::is_empty")]
    pub extensions: HashMap<String, Option<auxillary::Version>>,
}
#[cfg(feature = "display_eflint")]
impl DisplayEFlint for RequestCommon {
    /// Allows this AST node to be serialized to the given formatter.
    ///
    /// This is used in the [`DisplayEFlint`]-trait. However, this trait itself is not implemented, as this is only implemented for types returning whole lines (thereby being "standalone"), as it were.
    ///
    /// # Arguments
    /// - `indent`: The indentation to print each line with.
    /// - `f`: The [`Formatter`] to write to.
    ///
    /// # Errors
    /// This function errors if we failed to write to the given formatter.
    fn eflint_fmt(&self, indent: usize, f: &mut Formatter<'_>) -> FResult {
        // Write the version as an attribute
        if f.alternate() {
            writeln!(f, "{}{}", Indent(indent), style::ATTRIBUTE.apply_to(format!("#[version = {}]", self.version)))?;
        } else {
            writeln!(f, "{}#[version = {}]", Indent(indent), self.version)?;
        }

        // Write the extensions as attributes
        for (ext, ver) in &self.extensions {
            let ver: String = if let Some(ver) = ver { format!("{ver}") } else { "latest".into() };
            if f.alternate() {
                writeln!(f, "{}{}", Indent(indent), style::ATTRIBUTE.apply_to(format!("#[extension({ext}, {ver})]")))?;
            } else {
                writeln!(f, "{}#[extension({}, {})]", Indent(indent), ext, ver)?;
            }
        }

        // Done
        Ok(())
    }
}

/// Represents a Ping-request.
///
/// The Ping-request can be used to establish if a server is online and reachable.
#[derive(Clone, Debug, Deserialize, Serialize)]
pub struct RequestPing {
    /// The common schema of all requests
    #[serde(flatten)]
    pub common: RequestCommon,
}
#[cfg(feature = "display_eflint")]
impl DisplayEFlint for RequestPing {
    fn eflint_fmt(&self, indent: usize, f: &mut Formatter<'_>) -> FResult {
        let Self { common } = self;

        // Write header
        if f.alternate() {
            writeln!(f, "{}{}", Indent(indent), style::REQUEST_DECORATION.apply_to("Request<Handshake> {"))?;
        } else {
            writeln!(f, "{}Request<Handshake> {{", Indent(indent))?;
        }

        // Write only the common part
        common.eflint_fmt(indent + 4, f)?;

        // Write the footer
        if f.alternate() {
            writeln!(f, "{}{}", Indent(indent), style::REQUEST_DECORATION.apply_to("}"))?;
        } else {
            writeln!(f, "{}}}", Indent(indent))?;
        }

        // Done
        Ok(())
    }
}

/// Represents a Handshake-request.
///
/// The Handshake-request can be used to retrieve server metadata, such as supported versions, reasoner used, etc.
#[derive(Clone, Debug, Deserialize, Serialize)]
pub struct RequestHandshake {
    /// The common schema of all requests
    #[serde(flatten)]
    pub common: RequestCommon,
}
#[cfg(feature = "display_eflint")]
impl DisplayEFlint for RequestHandshake {
    fn eflint_fmt(&self, indent: usize, f: &mut Formatter<'_>) -> FResult {
        let Self { common } = self;

        // Write header
        if f.alternate() {
            writeln!(f, "{}{}", Indent(indent), style::REQUEST_DECORATION.apply_to("Request<Handshake> {"))?;
        } else {
            writeln!(f, "{}Request<Handshake> {{", Indent(indent))?;
        }

        // Write the common part only
        common.eflint_fmt(indent + 4, f)?;

        // Write the footer
        if f.alternate() {
            writeln!(f, "{}{}", Indent(indent), style::REQUEST_DECORATION.apply_to("}"))?;
        } else {
            writeln!(f, "{}}}", Indent(indent))?;
        }

        // Done
        Ok(())
    }
}

/// Represents a Phrases-request.
///
/// The Phrases-request can be used to perform reasoning on the server.
#[derive(Clone, Debug, Deserialize, Serialize)]
pub struct RequestPhrases {
    /// The common schema of all requests
    #[serde(flatten)]
    pub common: RequestCommon,

    /// A list of phrases to send to the server.
    pub phrases: Vec<Phrase>,
    /// Whether to ask for updates or not.
    #[serde(default = "bool::default")]
    pub updates: bool,
}
#[cfg(feature = "display_eflint")]
impl DisplayEFlint for RequestPhrases {
    #[inline]
    fn eflint_fmt(&self, indent: usize, f: &mut Formatter<'_>) -> FResult {
        let Self { common, phrases, updates } = self;

        // Write header
        if f.alternate() {
            writeln!(f, "{}{}", Indent(indent), style::REQUEST_DECORATION.apply_to("Request<Phrases> {"))?;
        } else {
            writeln!(f, "{}Request<Phrases> {{", Indent(indent))?;
        }

        // Write the common part first
        common.eflint_fmt(indent + 4, f)?;
        // Add an attribute for the updates
        if f.alternate() {
            writeln!(f, "{}{}", Indent(indent + 4), style::ATTRIBUTE.apply_to(format!("#[updates = {updates}]")))?;
        } else {
            writeln!(f, "{}#[updates = {}]", Indent(indent + 4), updates)?;
        }
        writeln!(f)?;

        // Write the phrases
        for phrase in phrases {
            phrase.eflint_fmt(indent + 4, f)?;
        }

        // Write the footer
        if f.alternate() {
            writeln!(f, "{}{}", Indent(indent), style::REQUEST_DECORATION.apply_to("}"))?;
        } else {
            writeln!(f, "{}}}", Indent(indent))?;
        }

        // Done!
        Ok(())
    }
}

/// Represents an Inspect-request.
///
/// The Inspect-request can be used to get information about the reasoner state.
#[derive(Clone, Debug, Deserialize, Serialize)]
pub struct RequestInspect {
    /// The common schema of all requests
    #[serde(flatten)]
    pub common: RequestCommon,

    /// A list of targets that can be used to scope the inspect request.
    #[serde(default = "Vec::new", skip_serializing_if = "Vec::is_empty")]
    pub targets: Vec<String>,
}
#[cfg(feature = "display_eflint")]
impl DisplayEFlint for RequestInspect {
    #[inline]
    fn eflint_fmt(&self, indent: usize, f: &mut Formatter<'_>) -> FResult {
        let Self { common, targets } = self;

        // Write header
        if f.alternate() {
            writeln!(f, "{}{}", Indent(indent), style::REQUEST_DECORATION.apply_to("Request<Inspect> {"))?;
        } else {
            writeln!(f, "{}Request<Inspect> {{", Indent(indent))?;
        }

        // Write the common part
        common.eflint_fmt(indent + 4, f)?;
        writeln!(f)?;

        // Write the things we're asking information for as a comma-separated list
        for target in targets {
            if f.alternate() {
                writeln!(f, "{}{}{}", Indent(indent + 4), target, style::PUNCTUATION.apply_to(","))?;
            } else {
                writeln!(f, "{}{},", Indent(indent + 4), target)?;
            }
        }

        // Write the footer
        if f.alternate() {
            writeln!(f, "{}{}", Indent(indent), style::REQUEST_DECORATION.apply_to("}"))?;
        } else {
            writeln!(f, "{}}}", Indent(indent))?;
        }

        // Done!
        Ok(())
    }
}



/// Determines the common fields for all responses.
///
/// Note that this does not include the `kind`-field, as that's part of the parent [`Request`].
#[derive(Clone, Debug, Deserialize, Serialize)]
pub struct ResponseCommon {
    /// Whether the response was received and parsed successfully. Basically, represents whether the request was "syntactically valid" according to the specification.
    pub success: bool,
    /// An optional list of errors that occurred when `success` is false.
    #[serde(default = "Vec::new", skip_serializing_if = "Vec::is_empty")]
    pub errors:  Vec<Error>,
}
#[cfg(feature = "display_eflint")]
impl ResponseCommon {
    /// Allows this AST node to be serialized to the given formatter.
    ///
    /// This is used in the [`DisplayEFlint`]-trait. However, this trait itself is not implemented, as this is only implemented for types returning whole lines (thereby being "standalone"), as it were.
    ///
    /// # Arguments
    /// - `indent`: The indentation to print each line with.
    /// - `f`: The [`Formatter`] to write to.
    ///
    /// # Errors
    /// This function errors if we failed to write to the given formatter.
    #[inline]
    fn eflint_fmt(&self, indent: usize, f: &mut Formatter<'_>) -> FResult {
        let Self { success, errors } = self;

        // Write the success as a key/value pair
        if f.alternate() {
            writeln!(
                f,
                "{}success {} {}",
                Indent(indent),
                style::PUNCTUATION.apply_to(":"),
                if *success { style::SUCCESS.apply_to("true") } else { style::FAILURE.apply_to("false") }
            )?;
        } else {
            writeln!(f, "{}success : {}", Indent(indent), success)?;
        }

        // Write the errors if there are any
        if !errors.is_empty() {
            if f.alternate() {
                writeln!(f, "{}errors  {} {}", Indent(indent), style::PUNCTUATION.apply_to(":"), style::PUNCTUATION.apply_to("["))?;
            } else {
                writeln!(f, "{}errors  : [", Indent(indent))?;
            }
            for err in &self.errors {
                err.eflint_fmt(indent + 4, f)?;
            }
            writeln!(f, "{}{}", Indent(indent), style::PUNCTUATION.apply_to("]"))?;
        }

        // Done
        Ok(())
    }
}

/// Represents the reply to a [Ping-request](RequestPing).
#[derive(Clone, Debug, Deserialize, Serialize)]
pub struct ResponsePing {
    // The common schema of all responses
    #[serde(flatten)]
    pub common: ResponseCommon,
}
#[cfg(feature = "display_eflint")]
impl DisplayEFlint for ResponsePing {
    #[inline]
    fn eflint_fmt(&self, indent: usize, f: &mut Formatter<'_>) -> FResult {
        let Self { common } = self;

        // Just write the common one
        if f.alternate() {
            writeln!(f, "{}{}", Indent(indent), style::REQUEST_DECORATION.apply_to("Response<Ping> {"))?;
        } else {
            writeln!(f, "{}Response<Ping> {{", Indent(indent))?;
        }
        common.eflint_fmt(indent + 4, f)?;
        if f.alternate() {
            writeln!(f, "{}{}", Indent(indent), style::REQUEST_DECORATION.apply_to("}"))?;
        } else {
            writeln!(f, "{}}}", Indent(indent))?;
        }

        // Done
        Ok(())
    }
}

/// Represents the reply to a [Handshake-request](RequestHandshake).
#[derive(Clone, Debug, Deserialize, Serialize)]
pub struct ResponseHandshake {
    // The common schema of all responses
    #[serde(flatten)]
    pub common: ResponseCommon,

    /// A list of the supported versions by the server.
    pub supported_versions: Vec<auxillary::Version>,
    /// A list of the supported extensions by the server.
    ///
    /// The extensions are mapped per supported version, and map to a list of supported versions of that extension.
    #[serde(skip_serializing_if = "Option::is_none")]
    pub supported_extensions: Option<HashMap<auxillary::Version, HashMap<String, Vec<auxillary::Version>>>>,
    /// The reasoner backend used. See [`appendix::Reasoner`] for a list of reasoners that are known at the time of writing.
    #[serde(skip_serializing_if = "Option::is_none")]
    pub reasoner: Option<String>,
    /// The version of the reasoner backend used.
    #[serde(skip_serializing_if = "Option::is_none")]
    pub reasoner_version: Option<auxillary::Version>,
    /// Whether or not this server is, in general, inclined to give you updates for state changes of phrases.
    #[serde(skip_serializing_if = "Option::is_none")]
    pub shares_updates: Option<bool>,
    /// Whether or not this server is, in general, inclined to give you updates on triggered Acts or Events.
    #[serde(skip_serializing_if = "Option::is_none")]
    pub shares_triggers: Option<bool>,
    /// Whether or not this server is, in general, inclined to give you updates on violations.
    #[serde(skip_serializing_if = "Option::is_none")]
    pub shares_violations: Option<bool>,
}
#[cfg(feature = "display_eflint")]
impl DisplayEFlint for ResponseHandshake {
    #[inline]
    fn eflint_fmt(&self, indent: usize, f: &mut Formatter<'_>) -> FResult {
        let Self { common, supported_versions, supported_extensions, reasoner, reasoner_version, shares_updates, shares_triggers, shares_violations } =
            self;

        // Write header
        if f.alternate() {
            writeln!(f, "{}{}", Indent(indent), style::REQUEST_DECORATION.apply_to("Response<Handshake> {"))?;
        } else {
            writeln!(f, "{}Response<Handshake> {{", Indent(indent))?;
        }

        // Write the common one first
        common.eflint_fmt(indent + 4, f)?;

        // Produce some coloured (or not) punctuation first
        let colon: Box<dyn Display> = if f.alternate() { Box::new(style::PUNCTUATION.apply_to(":")) } else { Box::new(":") };
        let lbrace: Box<dyn Display> = if f.alternate() { Box::new(style::PUNCTUATION.apply_to("{")) } else { Box::new("{") };
        let rbrace: Box<dyn Display> = if f.alternate() { Box::new(style::PUNCTUATION.apply_to("}")) } else { Box::new("}") };
        let scomma: String = if f.alternate() { style::PUNCTUATION.apply_to(", ").to_string() } else { ", ".into() };

        // Write the other fields; supported versions...
        writeln!(
            f,
            "{}{} {} {}",
            Indent(indent + 4),
            "supported_versions  ",
            colon,
            supported_versions.iter().map(|ver| format!("v{ver}")).collect::<Vec<String>>().join(&scomma)
        )?;

        // ...supported extensions...
        if let Some(supported_extensions) = supported_extensions {
            writeln!(f, "{}{} {} {}", Indent(indent + 4), "supported_extensions", colon, lbrace)?;
            for (spec_ver, exts) in supported_extensions {
                writeln!(f, "{}v{} {} {}", Indent(indent + 8), spec_ver, colon, lbrace)?;
                for (ext, vers) in exts {
                    writeln!(
                        f,
                        "{}{} {} {}",
                        Indent(indent + 12),
                        ext,
                        colon,
                        vers.iter().map(|ver| format!("v{ver}")).collect::<Vec<String>>().join(&scomma)
                    )?;
                }
                writeln!(f, "{}{}", Indent(indent + 8), rbrace)?;
            }
            writeln!(f, "{}{}", Indent(indent + 4), rbrace)?;
        }

        // ...reasoner data...
        if let Some(reasoner) = reasoner {
            writeln!(f, "{}{} {} {}", Indent(indent + 4), "reasoner            ", colon, reasoner)?;
        }
        if let Some(reasoner_version) = reasoner_version {
            writeln!(f, "{}{} {} {}", Indent(indent + 4), "reasoner_version    ", colon, reasoner_version)?;
        }

        // ...and update sharing
        if let Some(shares_updates) = shares_updates {
            writeln!(f, "{}{} {} {}", Indent(indent + 4), "shares_updates      ", colon, shares_updates)?;
        }
        if let Some(shares_triggers) = shares_triggers {
            writeln!(f, "{}{} {} {}", Indent(indent + 4), "shares_triggers     ", colon, shares_triggers)?;
        }
        if let Some(shares_violations) = shares_violations {
            writeln!(f, "{}{} {} {}", Indent(indent + 4), "shares_violations   ", colon, shares_violations)?;
        }

        // Write footer
        if f.alternate() {
            writeln!(f, "{}{}", Indent(indent), style::REQUEST_DECORATION.apply_to("}"))?;
        } else {
            writeln!(f, "{}}}", Indent(indent))?;
        }

        // Done
        Ok(())
    }
}

/// Represents the reply to a [Phrases-request](RequestPhrases).
#[derive(Clone, Debug, Deserialize, Serialize)]
pub struct ResponsePhrases {
    // The common schema of all responses
    #[serde(flatten)]
    pub common: ResponseCommon,

    /// The results returned by the server that mark effects of submitted phrases.
    pub results: Vec<PhraseResult>,
}
#[cfg(feature = "display_eflint")]
impl DisplayEFlint for ResponsePhrases {
    fn eflint_fmt(&self, indent: usize, f: &mut Formatter<'_>) -> FResult {
        let Self { common, results } = self;

        // Write header
        if f.alternate() {
            writeln!(f, "{}{}", Indent(indent), style::REQUEST_DECORATION.apply_to("Response<Phrases> {"))?;
        } else {
            writeln!(f, "{}Response<Phrases> {{", Indent(indent))?;
        }

        // Write the common one first
        common.eflint_fmt(indent + 4, f)?;
        writeln!(f)?;

        // Write the phrases
        if !results.is_empty() {
            for result in results {
                result.eflint_fmt(indent + 4, f)?;
            }
        } else {
            if f.alternate() {
                writeln!(f, "{}{}", Indent(indent + 4), style::EMPTY_LIST.apply_to("<no effects>"))?;
            } else {
                writeln!(f, "{}<no effects>", Indent(indent + 4))?;
            }
        }

        // Write footer
        if f.alternate() {
            writeln!(f, "{}{}", Indent(indent), style::REQUEST_DECORATION.apply_to("}"))?;
        } else {
            writeln!(f, "{}}}", Indent(indent))?;
        }

        // Done
        Ok(())
    }
}

/// Represents the reply to an [Inspect-request](RequestInspect).
#[derive(Clone, Debug, Deserialize, Serialize)]
pub struct ResponseInspect {
    // The common schema of all responses
    #[serde(flatten)]
    pub common: ResponseCommon,

    /// The phrases the list the reasoner state, or the requested definitions.
    pub phrases: Vec<Phrase>,
}
#[cfg(feature = "display_eflint")]
impl DisplayEFlint for ResponseInspect {
    fn eflint_fmt(&self, indent: usize, f: &mut Formatter<'_>) -> FResult {
        let Self { common, phrases } = self;

        // Write header
        if f.alternate() {
            writeln!(f, "{}{}", Indent(indent), style::REQUEST_DECORATION.apply_to("Response<Inspect> {"))?;
        } else {
            writeln!(f, "{}Response<Inspect> {{", Indent(indent))?;
        }

        // Write the common one first
        common.eflint_fmt(indent + 4, f)?;
        writeln!(f)?;

        // Write the phrases
        for phrase in phrases {
            phrase.eflint_fmt(indent, f)?;
        }

        // Write footer
        if f.alternate() {
            writeln!(f, "{}{}", Indent(indent), style::REQUEST_DECORATION.apply_to("}"))?;
        } else {
            writeln!(f, "{}}}", Indent(indent))?;
        }

        // Done
        Ok(())
    }
}





/***** "TYPES" *****/
/// Represents an error returned by the server.
#[derive(Clone, Debug, Deserialize, Serialize)]
pub struct Error {
    /// A machine-usable identifier for the error that occurred.
    pub id:      String,
    /// A human-readable message detailling what went wrong for them to wrap their organic minds around.
    pub message: String,
}
#[cfg(feature = "display_eflint")]
impl DisplayEFlint for Error {
    #[inline]
    fn eflint_fmt(&self, indent: usize, f: &mut Formatter<'_>) -> FResult {
        if f.alternate() {
            writeln!(f, "{}{} {}", Indent(indent), self.message, style::ERROR_ID.apply_to(format!("<{}>", self.id)))
        } else {
            writeln!(f, "{}{} <{}>", Indent(indent), self.message, self.id)
        }
    }
}



/// Represents an eFLINT statement, essentially.
#[derive(Clone, Debug, Deserialize, EnumDebug, Serialize)]
#[serde(tag = "kind")]
pub enum Phrase {
    /// Defines a boolean query, e.g.,
    /// ```eflint
    /// ? has-voted(Bob, Amy)
    /// ```
    #[serde(rename = "bquery")]
    BooleanQuery(PhraseBooleanQuery),
    /// Defines an instance query, e.g.,
    /// ```eflint
    /// ?- has-voted(voter, Amy)
    /// ```
    #[serde(rename = "iquery")]
    InstanceQuery(PhraseInstanceQuery),

    /// Postulates a certain fact to be true, e.g.,
    /// ```eflint
    /// +citizen(Amy).
    /// ```
    #[serde(rename = "create")]
    Create(PhraseCreate),
    /// Postulates a certain fact to be false, e.g.,
    /// ```eflint
    /// -citizen(Amy).
    /// ```
    #[serde(rename = "terminate")]
    Terminate(PhraseTerminate),
    /// Removes the postulation for a certain fact, falling back to its derived value, e.g.,
    /// ```eflint
    /// ~citizen(Amy).
    /// ```
    #[serde(rename = "obfuscate")]
    Obfuscate(PhraseObfuscate),
    /// Triggers an Event or an Act, e.g.,
    /// ```eflint
    /// vote(Amy, Bob).
    /// ```
    #[serde(rename = "trigger")]
    Trigger(PhraseTrigger),

    /// Defines a Fact that has atomic construction, e.g.,
    /// ```eflint
    /// Fact citizen Identified by String.
    /// ```
    #[serde(rename = "afact")]
    AtomicFact(PhraseAtomicFact),
    /// Defines a Fact that has composite fields, e.g.,
    /// ```eflint
    /// Fact voter Identified by citizen.
    /// ```
    #[serde(rename = "cfact")]
    CompositeFact(PhraseCompositeFact),
    /// Defines a Placeholder to create type aliases, e.g.,
    /// ```eflint
    /// Placeholder civilian For citizen.
    /// ```
    #[serde(rename = "placeholder")]
    Placeholder(PhrasePlaceholder),
    /// Defines a Predicate that can be used to "prepare" queries, e.g.,:
    /// ```eflint
    /// Predicate vote-concluded When Not(Exists citizen : voter(citizen) && !has-voted(citizen)).
    /// ```
    /// This includes invariants, which are checked after every derivation procedure and can trigger violations when becoming false, e.g.,
    /// ```eflint
    /// Invariant at-most-one-winner When Not(Exists winner, winner' : winner != winner').
    /// ```
    #[serde(rename = "predicate")]
    Predicate(PhrasePredicate),
    /// Defines an Event that can be used to automatically postulate facts, e.g.,:
    /// ```eflint
    /// Event fire Obfuscates vote.
    /// ```
    #[serde(rename = "event")]
    Event(PhraseEvent),
    /// Defines an Act that can be used to automatically postulate facts while noting it was instantiated by a particular actor, e.g.:
    /// ```eflint
    /// Act murder
    ///   Actor citizen1
    ///   Related to citizen2
    ///   Terminates citizen2
    /// ```
    #[serde(rename = "act")]
    Act(PhraseAct),
    /// Defines a Duty that can be violated when certain conditions are (not) met, e.g.:
    /// ```eflint
    /// Duty must-vote
    ///   Holder citizen
    ///   Claimant administrator
    ///   Enforced by not-voted.
    /// ```
    #[serde(rename = "duty")]
    Duty(PhraseDuty),
    /// Defines an extension to an existing type, e.g.:
    /// ```eflint
    /// Extend Duty duty-to-vote
    ///   Conditioned by can-vote(voter).
    /// ```
    #[serde(rename = "extend")]
    Extend(PhraseExtend),
}
impl Phrase {
    /// Returns the phrase subclass for this phrase.
    ///
    /// # Returns
    /// A [`PhraseSubclass`](auxillary::PhraseSubclass) describing the class of this data.
    #[inline]
    pub fn subclass(&self) -> auxillary::PhraseSubclass {
        match self {
            Phrase::BooleanQuery(_) => auxillary::PhraseSubclass::Query,
            Phrase::InstanceQuery(_) => auxillary::PhraseSubclass::Query,

            Phrase::Create(_) => auxillary::PhraseSubclass::Statement,
            Phrase::Terminate(_) => auxillary::PhraseSubclass::Statement,
            Phrase::Obfuscate(_) => auxillary::PhraseSubclass::Statement,
            Phrase::Trigger(_) => auxillary::PhraseSubclass::Statement,

            Phrase::AtomicFact(_) => auxillary::PhraseSubclass::Definition,
            Phrase::CompositeFact(_) => auxillary::PhraseSubclass::Definition,
            Phrase::Placeholder(_) => auxillary::PhraseSubclass::Definition,
            Phrase::Predicate(_) => auxillary::PhraseSubclass::Definition,
            Phrase::Event(_) => auxillary::PhraseSubclass::Definition,
            Phrase::Act(_) => auxillary::PhraseSubclass::Definition,
            Phrase::Duty(_) => auxillary::PhraseSubclass::Definition,
            Phrase::Extend(_) => auxillary::PhraseSubclass::Definition,
        }
    }
}
#[cfg(feature = "display_eflint")]
impl DisplayEFlint for Phrase {
    fn eflint_fmt(&self, indent: usize, f: &mut Formatter<'_>) -> FResult {
        // Match to pass
        match self {
            Self::BooleanQuery(bquery) => bquery.eflint_fmt(indent, f),
            Self::InstanceQuery(iquery) => iquery.eflint_fmt(indent, f),

            Self::Create(create) => create.eflint_fmt(indent, f),
            Self::Terminate(term) => term.eflint_fmt(indent, f),
            Self::Obfuscate(obfus) => obfus.eflint_fmt(indent, f),
            Self::Trigger(trigger) => trigger.eflint_fmt(indent, f),

            Self::AtomicFact(afact) => afact.eflint_fmt(indent, f),
            Self::CompositeFact(cfact) => cfact.eflint_fmt(indent, f),
            Self::Placeholder(pholder) => pholder.eflint_fmt(indent, f),
            Self::Predicate(predicate) => predicate.eflint_fmt(indent, f),
            Self::Event(event) => event.eflint_fmt(indent, f),
            Self::Act(act) => act.eflint_fmt(indent, f),
            Self::Duty(duty) => duty.eflint_fmt(indent, f),
            Self::Extend(extend) => extend.eflint_fmt(indent, f),
        }
    }
}

/// Represents a boolean query within eFLINT, e.g.,
/// ```eflint
/// ? has-voted(Bob, Amy)
/// ```
#[derive(Clone, Debug, Deserialize, Serialize)]
pub struct PhraseBooleanQuery {
    /// The boolean expression to evaluate.
    pub expression: Expression,
}
#[cfg(feature = "display_eflint")]
impl DisplayEFlint for PhraseBooleanQuery {
    fn eflint_fmt(&self, indent: usize, f: &mut Formatter<'_>) -> FResult {
        let Self { expression } = self;

        // Write the expression, then a finishing period (it's that simple!)
        if f.alternate() {
            write!(f, "{}{}", Indent(indent), style::KEYWORD.apply_to("?"))?;
        } else {
            write!(f, "{}?", Indent(indent))?;
        }
        expression.eflint_fmt(f)?;
        if f.alternate() { writeln!(f, "{}", style::PUNCTUATION.apply_to(".")) } else { writeln!(f, ".") }
    }
}

/// Represents an instance query within eFLINT, e.g.,
/// ```eflint
/// ?- has-voted(voter, Amy)
/// ```
#[derive(Clone, Debug, Deserialize, Serialize)]
pub struct PhraseInstanceQuery {
    /// The instance expression to evaluate.
    pub expression: Expression,
}
#[cfg(feature = "display_eflint")]
impl DisplayEFlint for PhraseInstanceQuery {
    fn eflint_fmt(&self, indent: usize, f: &mut Formatter<'_>) -> FResult {
        let Self { expression } = self;

        // Write the expression, then a finishing period (it's that simple!)
        if f.alternate() {
            write!(f, "{}{}", Indent(indent), style::KEYWORD.apply_to("?-"))?;
        } else {
            write!(f, "{}?-", Indent(indent))?;
        }
        expression.eflint_fmt(f)?;
        if f.alternate() { writeln!(f, "{}", style::PUNCTUATION.apply_to(".")) } else { writeln!(f, ".") }
    }
}

/// Represents a true-postulation within eFLINT, e.g.,
/// ```eflint
/// +citizen(Amy).
/// ```
#[derive(Clone, Debug, Deserialize, Serialize)]
pub struct PhraseCreate {
    /// The expression that determines the instance to postulate to true. _Probably_ a constructor application, but not necessarily.
    pub operand: Expression,
}
#[cfg(feature = "display_eflint")]
impl DisplayEFlint for PhraseCreate {
    fn eflint_fmt(&self, indent: usize, f: &mut Formatter<'_>) -> FResult {
        let Self { operand } = self;

        // Write the expression, then a finishing period (it's that simple!)
        if f.alternate() {
            write!(f, "{}{}", Indent(indent), style::KEYWORD.apply_to("+"))?;
        } else {
            write!(f, "{}+", Indent(indent))?;
        }
        operand.eflint_fmt(f)?;
        if f.alternate() { writeln!(f, "{}", style::PUNCTUATION.apply_to(".")) } else { writeln!(f, ".") }
    }
}

/// Represents a false-postulation within eFLINT, e.g.,
/// ```eflint
/// -citizen(Amy).
/// ```
#[derive(Clone, Debug, Deserialize, Serialize)]
pub struct PhraseTerminate {
    /// The expression that determines the instance to postulate to false. _Probably_ a constructor application, but not necessarily.
    pub operand: Expression,
}
#[cfg(feature = "display_eflint")]
impl DisplayEFlint for PhraseTerminate {
    fn eflint_fmt(&self, indent: usize, f: &mut Formatter<'_>) -> FResult {
        let Self { operand } = self;

        // Write the expression, then a finishing period (it's that simple!)
        if f.alternate() {
            write!(f, "{}{}", Indent(indent), style::KEYWORD.apply_to("-"))?;
        } else {
            write!(f, "{}-", Indent(indent))?;
        }
        operand.eflint_fmt(f)?;
        if f.alternate() { writeln!(f, "{}", style::PUNCTUATION.apply_to(".")) } else { writeln!(f, ".") }
    }
}

/// Represents the removal of postulation within eFLINT, e.g.,
/// ```eflint
/// ~citizen(Amy).
/// ```
#[derive(Clone, Debug, Deserialize, Serialize)]
pub struct PhraseObfuscate {
    /// The expression that determines the instance to un-postulate. _Probably_ a constructor application, but not necessarily.
    pub operand: Expression,
}
#[cfg(feature = "display_eflint")]
impl DisplayEFlint for PhraseObfuscate {
    fn eflint_fmt(&self, indent: usize, f: &mut Formatter<'_>) -> FResult {
        let Self { operand } = self;

        // Write the expression, then a finishing period (it's that simple!)
        if f.alternate() {
            write!(f, "{}{}", Indent(indent), style::KEYWORD.apply_to("~"))?;
        } else {
            write!(f, "{}~", Indent(indent))?;
        }
        operand.eflint_fmt(f)?;
        if f.alternate() { writeln!(f, "{}", style::PUNCTUATION.apply_to(".")) } else { writeln!(f, ".") }
    }
}

/// Represents the execution of an Event or Act, e.g.,
/// ```eflint
/// vote(Amy, Bob).
/// ```
#[derive(Clone, Debug, Deserialize, Serialize)]
pub struct PhraseTrigger {
    /// The expression that determines the instance to trigger. _Probably_ a constructor application, but not necessarily.
    pub operand: Expression,
}
#[cfg(feature = "display_eflint")]
impl DisplayEFlint for PhraseTrigger {
    fn eflint_fmt(&self, indent: usize, f: &mut Formatter<'_>) -> FResult {
        let Self { operand } = self;

        // Write the expression, then a finishing period (it's that simple!)
        write!(f, "{}", Indent(indent))?;
        operand.eflint_fmt(f)?;
        if f.alternate() { writeln!(f, "{}", style::PUNCTUATION.apply_to(".")) } else { writeln!(f, ".") }
    }
}

/// Represents common fields for all type definition phrases.
#[derive(Clone, Debug, Deserialize, Serialize)]
pub struct TypeDefinitionCommon {
    /// A set of instance expressions that generate automatic instances for some type.
    #[serde(rename = "derived-from", default = "Vec::new", skip_serializing_if = "Vec::is_empty")]
    pub derived_from:   Vec<Expression>,
    /// A set of boolean expressions that filter all possible types in the positive (syntax sugar for Derived from over a type's fields with `When <expr>`).
    #[serde(rename = "holds-when", default = "Vec::new", skip_serializing_if = "Vec::is_empty")]
    pub holds_when:     Vec<Expression>,
    /// A set of boolean expressions that limits what instances may be derived by `Derived from`-rules and `Holds when`-rules, i.e., something is only derived if all `Conditioned by`-rules are true.
    #[serde(rename = "conditioned-by", default = "Vec::new", skip_serializing_if = "Vec::is_empty")]
    pub conditioned_by: Vec<Expression>,
}
#[cfg(feature = "display_eflint")]
impl TypeDefinitionCommon {
    /// Helper function to determine if this TypeDefinitionCommon is "empty" (i.e., all of its clauses are empty).
    ///
    /// # Returns
    /// True if all fields are empty lists, or false otherwise.
    #[inline]
    fn is_empty(&self) -> bool {
        let Self { derived_from, holds_when, conditioned_by } = self;
        derived_from.is_empty() && holds_when.is_empty() && conditioned_by.is_empty()
    }

    /// Allows this AST node to be serialized to the given formatter.
    ///
    /// This is used in the [`DisplayEFlint`]-trait. However, this trait itself is not implemented, as this is only implemented for types returning whole lines (thereby being "standalone"), as it were.
    ///
    /// # Arguments
    /// - `indent`: The indentation to print each line with.
    /// - `add_dot`: Whether to add the end-of-phrase dot at the end of this definition or not.
    /// - `f`: The [`Formatter`] to write to.
    ///
    /// # Errors
    /// This function errors if we failed to write to the given formatter.
    #[inline]
    fn eflint_fmt(&self, indent: usize, add_dot: bool, f: &mut Formatter<'_>) -> FResult {
        let Self { derived_from, holds_when, conditioned_by } = self;

        // Write the three rules in succession
        for (i, rule) in derived_from.iter().enumerate() {
            // Write the 'Violated when'-part
            if f.alternate() {
                write!(f, "{}{} ", Indent(indent), style::KEYWORD.apply_to("Derived from"))?;
            } else {
                write!(f, "{}Derived from ", Indent(indent))?;
            }
            // Write the expression
            rule.eflint_fmt(f)?;
            // Write the dot, if asked
            if add_dot && i == derived_from.len() - 1 && holds_when.is_empty() && conditioned_by.is_empty() {
                if f.alternate() {
                    write!(f, "{}", style::PUNCTUATION.apply_to("."))?;
                } else {
                    write!(f, ".")?;
                }
            }
            // Write the end-of-line
            writeln!(f)?;
        }

        // Do the three creates- terminates- and obfuscates in rapid succession
        for (i, rule) in holds_when.iter().enumerate() {
            // Write the 'Violated when'-part
            if f.alternate() {
                write!(f, "{}{} ", Indent(indent), style::KEYWORD.apply_to("Holds when"))?;
            } else {
                write!(f, "{}Holds when ", Indent(indent))?;
            }
            // Write the expression
            rule.eflint_fmt(f)?;
            // Write the dot, if asked
            if add_dot && i == holds_when.len() - 1 && conditioned_by.is_empty() {
                if f.alternate() {
                    write!(f, "{}", style::PUNCTUATION.apply_to("."))?;
                } else {
                    write!(f, ".")?;
                }
            }
            // Write the end-of-line
            writeln!(f)?;
        }
        for (i, rule) in conditioned_by.iter().enumerate() {
            // Write the 'Violated when'-part
            if f.alternate() {
                write!(f, "{}{} ", Indent(indent), style::KEYWORD.apply_to("Conditioned by"))?;
            } else {
                write!(f, "{}Conditioned by ", Indent(indent))?;
            }
            // Write the expression
            rule.eflint_fmt(f)?;
            // Write the dot, if asked
            if add_dot && i == conditioned_by.len() - 1 {
                if f.alternate() {
                    write!(f, "{}", style::PUNCTUATION.apply_to("."))?;
                } else {
                    write!(f, ".")?;
                }
            }
            // Write the end-of-line
            writeln!(f)?;
        }

        // Alright that's it
        Ok(())
    }
}

/// Represents common fields for all event-like definition phrases.
#[derive(Clone, Debug, Deserialize, Serialize)]
pub struct EventDefinitionCommon {
    /// A list of other Events and Acts that are triggered when this Event or Act triggers.
    ///
    /// These are instance expressions generating the lists.
    #[serde(rename = "syncs-with", default = "Vec::new", skip_serializing_if = "Vec::is_empty")]
    pub syncs_with: Vec<Expression>,
    /// A list of instance expressions generating all the facts that are postulated to true when this Event or Act triggers.
    #[serde(default = "Vec::new", skip_serializing_if = "Vec::is_empty")]
    pub creates:    Vec<Expression>,
    /// A list of instance expressions generating all the facts that are postulated to false when this Event or Act triggers.
    #[serde(default = "Vec::new", skip_serializing_if = "Vec::is_empty")]
    pub terminates: Vec<Expression>,
    /// A list of instance expressions generating all the facts whos postulation is removed when this Event or Act triggers.
    #[serde(default = "Vec::new", skip_serializing_if = "Vec::is_empty")]
    pub obfuscates: Vec<Expression>,
}
#[cfg(feature = "display_eflint")]
impl EventDefinitionCommon {
    /// Helper function to determine if this EventDefinitionCommon is "empty" (i.e., all of its clauses are empty).
    ///
    /// # Returns
    /// True if all fields are empty lists, or false otherwise.
    #[inline]
    fn is_empty(&self) -> bool {
        let Self { syncs_with, creates, terminates, obfuscates } = self;
        syncs_with.is_empty() && creates.is_empty() && terminates.is_empty() && obfuscates.is_empty()
    }

    /// Allows this AST node to be serialized to the given formatter.
    ///
    /// This is used in the [`DisplayEFlint`]-trait. However, this trait itself is not implemented, as this is only implemented for types returning whole lines (thereby being "standalone"), as it were.
    ///
    /// # Arguments
    /// - `indent`: The indentation to print each line with.
    /// - `add_dot`: Whether to add the end-of-phrase dot at the end of this definition or not.
    /// - `f`: The [`Formatter`] to write to.
    ///
    /// # Errors
    /// This function errors if we failed to write to the given formatter.
    #[inline]
    fn eflint_fmt(&self, indent: usize, add_dot: bool, f: &mut Formatter<'_>) -> FResult {
        let Self { syncs_with, creates, terminates, obfuscates } = self;

        // Write the Syncs with-statements appropriately
        for (i, rule) in syncs_with.iter().enumerate() {
            // Write the 'Violated when'-part
            if f.alternate() {
                write!(f, "{}{} ", Indent(indent), style::KEYWORD.apply_to("Syncs with"))?;
            } else {
                write!(f, "{}Syncs with ", Indent(indent))?;
            }
            // Write the expression
            rule.eflint_fmt(f)?;
            // Write the dot, if asked
            if add_dot && i == syncs_with.len() - 1 && creates.is_empty() && terminates.is_empty() && obfuscates.is_empty() {
                if f.alternate() {
                    write!(f, "{}", style::PUNCTUATION.apply_to("."))?;
                } else {
                    write!(f, ".")?;
                }
            }
            // Write the end-of-line
            writeln!(f)?;
        }

        // Do the three creates- terminates- and obfuscates in rapid succession
        for (i, rule) in creates.iter().enumerate() {
            // Write the 'Violated when'-part
            if f.alternate() {
                write!(f, "{}{} ", Indent(indent), style::KEYWORD.apply_to("Creates"))?;
            } else {
                write!(f, "{}Creates ", Indent(indent))?;
            }
            // Write the expression
            rule.eflint_fmt(f)?;
            // Write the dot, if asked
            if add_dot && i == creates.len() - 1 && terminates.is_empty() && obfuscates.is_empty() {
                if f.alternate() {
                    write!(f, "{}", style::PUNCTUATION.apply_to("."))?;
                } else {
                    write!(f, ".")?;
                }
            }
            // Write the end-of-line
            writeln!(f)?;
        }
        for (i, rule) in terminates.iter().enumerate() {
            // Write the 'Violated when'-part
            if f.alternate() {
                write!(f, "{}{} ", Indent(indent), style::KEYWORD.apply_to("Terminates"))?;
            } else {
                write!(f, "{}Terminates ", Indent(indent))?;
            }
            // Write the expression
            rule.eflint_fmt(f)?;
            // Write the dot, if asked
            if add_dot && i == terminates.len() - 1 && obfuscates.is_empty() {
                if f.alternate() {
                    write!(f, "{}", style::PUNCTUATION.apply_to("."))?;
                } else {
                    write!(f, ".")?;
                }
            }
            // Write the end-of-line
            writeln!(f)?;
        }
        for (i, rule) in obfuscates.iter().enumerate() {
            // Write the 'Violated when'-part
            if f.alternate() {
                write!(f, "{}{} ", Indent(indent), style::KEYWORD.apply_to("Obfuscates"))?;
            } else {
                write!(f, "{}Obfuscates ", Indent(indent))?;
            }
            // Write the expression
            rule.eflint_fmt(f)?;
            // Write the dot, if asked
            if add_dot && i == obfuscates.len() - 1 {
                if f.alternate() {
                    write!(f, "{}", style::PUNCTUATION.apply_to("."))?;
                } else {
                    write!(f, ".")?;
                }
            }
            // Write the end-of-line
            writeln!(f)?;
        }

        // Alright that's it
        Ok(())
    }
}

/// Represents common fields for all duty-like definition phrases.
#[derive(Clone, Debug, Deserialize, Serialize)]
pub struct DutyDefinitionCommon {
    /// A list of boolean expressions that will trigger the Duty violated if any of them holds true _while_ the Duty itself holds true.
    #[serde(rename = "violated-when", default = "Vec::new", skip_serializing_if = "Vec::is_empty")]
    pub violated_when: Vec<Expression>,
    /// A list of type identifiers that define a set of types that, when any of them becomes true, violates this Duty.
    ///
    /// Note that this list is quite restrictive. Only types with the same fields (names, types and order!) are allowed.
    ///
    /// To illustrate, `enforced-by` is syntax sugar for a particular `violated-when`:
    /// ```eflint
    /// Duty must-vote
    ///   Holder citizen
    ///   Claimant administrator
    ///   Enforced by not-voted.
    /// ```
    /// is the same as
    /// ```eflint
    /// Duty must-vote
    ///   Holder citizen
    ///   Claimant administrator
    ///   Violated when Enabled(not-voted(citizen, administrator)).
    /// ```
    #[serde(rename = "enforced-by", default = "Vec::new", skip_serializing_if = "Vec::is_empty")]
    pub enforced_by:   Vec<String>,
}
#[cfg(feature = "display_eflint")]
impl DutyDefinitionCommon {
    /// Helper function to determine if this TypeDefinitionCommon is "empty" (i.e., all of its clauses are empty).
    ///
    /// # Returns
    /// True if all fields are empty lists, or false otherwise.
    #[inline]
    fn is_empty(&self) -> bool {
        let Self { violated_when, enforced_by } = self;
        violated_when.is_empty() && enforced_by.is_empty()
    }

    /// Allows this AST node to be serialized to the given formatter.
    ///
    /// This is used in the [`DisplayEFlint`]-trait. However, this trait itself is not implemented, as this is only implemented for types returning whole lines (thereby being "standalone"), as it were.
    ///
    /// # Arguments
    /// - `indent`: The indentation to print each line with.
    /// - `add_dot`: Whether to add the end-of-phrase dot at the end of this definition or not.
    /// - `f`: The [`Formatter`] to write to.
    ///
    /// # Errors
    /// This function errors if we failed to write to the given formatter.
    #[inline]
    fn eflint_fmt(&self, indent: usize, add_dot: bool, f: &mut Formatter<'_>) -> FResult {
        let Self { violated_when, enforced_by } = self;

        // Write the Violated when-statements appropriately
        for (i, rule) in violated_when.iter().enumerate() {
            // Write the 'Violated when'-part
            if f.alternate() {
                write!(f, "{}{} ", Indent(indent), style::KEYWORD.apply_to("Violated when"))?;
            } else {
                write!(f, "{}Violated when ", Indent(indent))?;
            }
            // Write the expression
            rule.eflint_fmt(f)?;
            // Write the dot, if asked
            if add_dot && i == violated_when.len() - 1 && enforced_by.is_empty() {
                if f.alternate() {
                    write!(f, "{}", style::PUNCTUATION.apply_to("."))?;
                } else {
                    write!(f, ".")?;
                }
            }
            // Write the end-of-line
            writeln!(f)?;
        }

        // Do the same for Enforced by
        for (i, name) in enforced_by.iter().enumerate() {
            if f.alternate() {
                write!(f, "{}{} {}", Indent(indent), style::KEYWORD.apply_to("Enforced by"), name)?;
                // Write the dot, if asked
                if add_dot && i == enforced_by.len() - 1 {
                    write!(f, "{}", style::PUNCTUATION.apply_to("."))?;
                }
            } else {
                write!(f, "{}Enforced by {}", Indent(indent), name)?;
                // Write the dot, if asked
                if add_dot && i == enforced_by.len() - 1 {
                    write!(f, ".")?;
                }
            }
            writeln!(f)?;
        }

        // Alright that's it
        Ok(())
    }
}

/// Represents the definition of an atomic Fact, e.g.,
/// ```eflint
/// Fact citizen Identified by String.
/// ```
#[derive(Clone, Debug, Deserialize, Serialize)]
pub struct PhraseAtomicFact {
    /// The common fields for this definition.
    #[serde(flatten)]
    pub definition: TypeDefinitionCommon,

    /// The name of the new Fact.
    pub name:  String,
    /// The type of the new Fact, which must be one of eFLINT's builtin types. Defaults to "String" if omitted.
    #[serde(rename = "type", default = "auxillary::AtomicType::string")]
    pub ty:    auxillary::AtomicType,
    /// If non-empty, then the atomic fact has a closed domain of the given values.
    #[serde(skip_serializing_if = "Option::is_none")]
    pub range: Option<Domain>,
}
#[cfg(feature = "display_eflint")]
impl DisplayEFlint for PhraseAtomicFact {
    fn eflint_fmt(&self, indent: usize, f: &mut Formatter<'_>) -> FResult {
        let Self { definition, name, ty, range } = self;

        // Take highlighting into account
        if f.alternate() {
            write!(
                f,
                "{}{} {} {} ",
                Indent(indent),
                style::DATA.apply_to("Fact"),
                style::BOLD_IDENTIFIER.apply_to(name),
                style::KEYWORD.apply_to("Identified by"),
            )?;
        } else {
            write!(f, "{}Fact {} Identified by ", Indent(indent), name)?;
        }

        // Write the range _or_ type
        if let Some(range) = range {
            range.eflint_fmt(f)?;
        } else {
            write!(f, "{ty}")?;
        }

        // Write the definition fields _or_ an ending period
        if !definition.is_empty() {
            writeln!(f)?;
            definition.eflint_fmt(indent + 4, true, f)?;
        } else {
            if f.alternate() {
                writeln!(f, "{}", style::PUNCTUATION.apply_to("."))?;
            } else {
                writeln!(f, ".")?;
            }
        }

        // Done!
        Ok(())
    }
}

/// Represents the definition of a composite Fact, e.g.,
/// ```eflint
/// Fact voter Identified by citizen.
/// ```
#[derive(Clone, Debug, Deserialize, Serialize)]
pub struct PhraseCompositeFact {
    /// The common fields for this definition.
    #[serde(flatten)]
    pub definition: TypeDefinitionCommon,

    /// The name of the new Fact.
    pub name: String,
    /// The fields of this Fact, given as identifiers for nested types.
    #[serde(rename = "identified-by")]
    pub identified_by: auxillary::NonEmptyVec<String>,
}
#[cfg(feature = "display_eflint")]
impl DisplayEFlint for PhraseCompositeFact {
    fn eflint_fmt(&self, indent: usize, f: &mut Formatter<'_>) -> FResult {
        let Self { definition, name, identified_by } = self;

        // Take highlighting into account
        if f.alternate() {
            write!(
                f,
                "{}{} {} {} {}",
                Indent(indent),
                style::DATA.apply_to("Fact"),
                style::BOLD_IDENTIFIER.apply_to(name),
                style::KEYWORD.apply_to("Identified by"),
                identified_by.join(&style::PUNCTUATION.apply_to(", ").to_string()),
            )?;
        } else {
            write!(f, "{}Fact {} Identified by {}", Indent(indent), name, identified_by.join(", "))?;
        }

        // Write the definition fields _or_ an ending period
        if !definition.is_empty() {
            writeln!(f)?;
            definition.eflint_fmt(indent + 4, true, f)?;
        } else {
            if f.alternate() {
                writeln!(f, "{}", style::PUNCTUATION.apply_to("."))?;
            } else {
                writeln!(f, ".")?;
            }
        }

        // Done!
        Ok(())
    }
}

/// Represents a Placeholder definition for Fact for e.g.,
/// ```eflint
/// Placeholder civilian For citizen.
/// ```
#[derive(Clone, Debug, Deserialize, Serialize)]
pub struct PhrasePlaceholder {
    /// The name of the placeholder itself. Note that multiple can be submitted in one go to do it efficiently, but not all backend reasoners may support that syntax.
    pub name:     Vec<String>,
    /// The identifier of the Fact for which phrase holds.
    #[serde(rename = "for")]
    pub for_fact: String,
}
#[cfg(feature = "display_eflint")]
impl DisplayEFlint for PhrasePlaceholder {
    fn eflint_fmt(&self, indent: usize, f: &mut Formatter<'_>) -> FResult {
        let Self { name, for_fact } = self;

        // Generate one definition for every name
        for name in name {
            // Take highlighting into account
            if f.alternate() {
                writeln!(
                    f,
                    "{}{} {} {} {}{}",
                    Indent(indent),
                    style::DATA.apply_to("Placeholder"),
                    style::BOLD_IDENTIFIER.apply_to(name),
                    style::KEYWORD.apply_to("For"),
                    for_fact,
                    style::PUNCTUATION.apply_to(".")
                )?;
            } else {
                writeln!(f, "{}Placeholder {} For {}.", Indent(indent), name, for_fact)?;
            };
        }

        // Done!
        Ok(())
    }
}

/// Represents a predicate that can be queried but not instantiated, e.g.,
/// ```eflint
/// Predicate vote-concluded When Not(Exists citizen : voter(citizen) && !has-voted(citizen)).
/// ```
/// This includes invariants, which are checked after every derivation procedure and can trigger violations when becoming false, e.g.,
/// ```eflint
/// Invariant at-most-one-winner When Not(Exists winner, winner' : winner != winner').
/// ```
#[derive(Clone, Debug, Deserialize, Serialize)]
pub struct PhrasePredicate {
    /// The name of the predicate.
    pub name: String,
    /// Whether this indicate an invariant or not.
    // #[serde(alias = "is-invariant", default = "bool::default")]
    // pub is_invariant: bool,
    #[serde(rename = "is-invariant", alias = "is_invariant", default = "bool::default")]
    pub is_invariant: bool,
    /// The boolean expression checked by this predicate.
    pub expression: Expression,
}
#[cfg(feature = "display_eflint")]
impl DisplayEFlint for PhrasePredicate {
    fn eflint_fmt(&self, indent: usize, f: &mut Formatter<'_>) -> FResult {
        let Self { name, is_invariant, expression } = self;

        // Write the "header" and the expression
        if f.alternate() {
            // The header
            writeln!(
                f,
                "{}{} {}",
                Indent(indent),
                style::DATA.apply_to(if *is_invariant { "Invariant" } else { "Predicate" }),
                style::BOLD_IDENTIFIER.apply_to(name),
            )?;

            // Expression on next line
            write!(f, "{}{} ", Indent(indent + 4), style::KEYWORD.apply_to("When"))?;
            expression.eflint_fmt(f)?;
            writeln!(f, "{}", style::PUNCTUATION.apply_to("."))?;
        } else {
            // The header
            writeln!(f, "{}{} {}", Indent(indent), if *is_invariant { "Invariant" } else { "Predicate" }, name)?;

            // Expression on next line
            write!(f, "{}When ", Indent(indent + 4))?;
            expression.eflint_fmt(f)?;
            writeln!(f, ".")?;
        };

        // Done!
        Ok(())
    }
}

/// Defines an automatic transition between Facts, e.g.,
/// ```eflint
/// Event fire Obfuscates vote.
/// ```
#[derive(Clone, Debug, Deserialize, Serialize)]
pub struct PhraseEvent {
    /// The common fields for this definition.
    #[serde(flatten)]
    pub definition: TypeDefinitionCommon,
    /// The common fields for event-likes.
    #[serde(flatten)]
    pub event:      EventDefinitionCommon,

    /// The name of the new event type.
    pub name: String,
    /// Any fields for this event, basically.
    #[serde(rename = "related-to", default = "Vec::new", skip_serializing_if = "Vec::is_empty")]
    pub related_to: Vec<String>,
}
#[cfg(feature = "display_eflint")]
impl DisplayEFlint for PhraseEvent {
    fn eflint_fmt(&self, indent: usize, f: &mut Formatter<'_>) -> FResult {
        let Self { definition, event, name, related_to } = self;

        // Write the "header" and its fields
        if f.alternate() {
            write!(f, "{}{} {}", Indent(indent), style::DATA.apply_to("Event"), style::BOLD_IDENTIFIER.apply_to(name))?;
            if !related_to.is_empty() {
                write!(
                    f,
                    "\n{}{} {}",
                    Indent(indent + 4),
                    style::KEYWORD.apply_to("Related to"),
                    related_to.join(&style::PUNCTUATION.apply_to(", ").to_string()),
                )?;
            }
        } else {
            write!(f, "{}Event {}", Indent(indent), name)?;
            if !related_to.is_empty() {
                write!(f, "\n{}Related to {}", Indent(indent + 4), related_to.join(", "))?;
            }
        };

        // Write the definition fields, then the duty fields
        if !definition.is_empty() || !event.is_empty() {
            writeln!(f)?;
            definition.eflint_fmt(indent + 4, event.is_empty(), f)?;
            event.eflint_fmt(indent + 4, true, f)?;
        } else {
            if f.alternate() {
                writeln!(f, "{}", style::PUNCTUATION.apply_to("."))?;
            } else {
                writeln!(f, ".")?;
            }
        }

        // Done!
        Ok(())
    }
}

/// Defines an automatic transition between Facts instantiated by a particular actor, e.g.,
/// ```eflint
/// Act murder
///   Actor citizen1
///   Related to citizen2
///   Terminates citizen2
/// ```
#[derive(Clone, Debug, Deserialize, Serialize)]
pub struct PhraseAct {
    /// The common fields for this definition.
    #[serde(flatten)]
    pub definition: TypeDefinitionCommon,
    /// The common fields for event-likes.
    #[serde(flatten)]
    pub event:      EventDefinitionCommon,

    /// The name of the new act type.
    pub name: String,
    /// The actor that instantiates this event. Given as the identifier of a particular type (as in, this is a field to the parent type). Will default to `author` if ommitted.
    #[serde(default = "default_phrase_act_actor")]
    pub actor: String,
    /// Any fields for this act other than `actor`, basically.
    #[serde(rename = "related-to", default = "Vec::new", skip_serializing_if = "Vec::is_empty")]
    pub related_to: Vec<String>,
}
#[cfg(feature = "display_eflint")]
impl DisplayEFlint for PhraseAct {
    fn eflint_fmt(&self, indent: usize, f: &mut Formatter<'_>) -> FResult {
        let Self { definition, event, name, actor, related_to } = self;

        // Write the "header" and its fields
        if f.alternate() {
            writeln!(f, "{}{} {}", Indent(indent), style::DATA.apply_to("Act"), style::BOLD_IDENTIFIER.apply_to(name))?;
            write!(f, "{}{} {}", Indent(indent + 4), style::KEYWORD.apply_to("Actor"), actor)?;
            if !related_to.is_empty() {
                write!(
                    f,
                    "\n{}{} {}",
                    Indent(indent + 4),
                    style::KEYWORD.apply_to("Related to"),
                    related_to.join(&style::PUNCTUATION.apply_to(", ").to_string())
                )?;
            }
        } else {
            writeln!(f, "{}Act {}", Indent(indent), name)?;
            write!(f, "{}Actor {}", Indent(indent + 4), actor)?;
            if !related_to.is_empty() {
                write!(f, "\n{}Related to {}", Indent(indent + 4), related_to.join(", "))?;
            }
        };

        // Write the definition fields, then the duty fields
        if !definition.is_empty() || !event.is_empty() {
            writeln!(f)?;
            definition.eflint_fmt(indent + 4, event.is_empty(), f)?;
            event.eflint_fmt(indent + 4, true, f)?;
        } else {
            if f.alternate() {
                writeln!(f, "{}", style::PUNCTUATION.apply_to("."))?;
            } else {
                writeln!(f, ".")?;
            }
        }

        // Done!
        Ok(())
    }
}

/// Defines an obligation that two actors have, e.g.,
/// ```eflint
/// Duty must-vote
///   Holder citizen
///   Claimant administrator
///   Enforced by not-voted.
/// ```
#[derive(Clone, Debug, Deserialize, Serialize)]
pub struct PhraseDuty {
    /// The common fields for this definition.
    #[serde(flatten)]
    pub definition: TypeDefinitionCommon,
    /// The common fields for this duty.
    #[serde(flatten)]
    pub duty: DutyDefinitionCommon,

    /// The name of the new duty type.
    pub name: String,
    /// The actor that has to perform the duty. Given as the identifier of a particular type (as in, this is a field to the parent type).
    pub holder: String,
    /// The actor that has power to enforce the `holder` doing the duty. Given as the identifier of a particular type (as in, this is a field to the parent type).
    pub claimant: String,
    /// Any fields for this act other than `holder` and `claimant`, basically.
    #[serde(rename = "related-to", default = "Vec::new", skip_serializing_if = "Vec::is_empty")]
    pub related_to: Vec<String>,
}
#[cfg(feature = "display_eflint")]
impl DisplayEFlint for PhraseDuty {
    fn eflint_fmt(&self, indent: usize, f: &mut Formatter<'_>) -> FResult {
        let Self { definition, duty, name, holder, claimant, related_to } = self;

        // Write the "header" and its fields
        if f.alternate() {
            writeln!(f, "{}{} {}", Indent(indent), style::DATA.apply_to("Duty"), style::BOLD_IDENTIFIER.apply_to(name))?;
            writeln!(f, "{}{} {}", Indent(indent + 4), style::KEYWORD.apply_to("Holder"), holder)?;
            write!(f, "{}{} {}", Indent(indent + 4), style::KEYWORD.apply_to("Claimant"), claimant)?;
            if !related_to.is_empty() {
                write!(
                    f,
                    "\n{}{} {}",
                    Indent(indent + 4),
                    style::KEYWORD.apply_to("Related to"),
                    related_to.join(&style::PUNCTUATION.apply_to(", ").to_string())
                )?;
            }
        } else {
            writeln!(f, "{}Duty {}", Indent(indent), name)?;
            writeln!(f, "{}Holder {}", Indent(indent + 4), holder)?;
            write!(f, "{}Claimant {}", Indent(indent + 4), claimant)?;
            if !related_to.is_empty() {
                write!(f, "\n{}Related to {}", Indent(indent + 4), related_to.join(", "))?;
            }
        };

        // Write the definition fields, then the duty fields
        if !definition.is_empty() || !duty.is_empty() {
            writeln!(f)?;
            definition.eflint_fmt(indent + 4, duty.is_empty(), f)?;
            duty.eflint_fmt(indent + 4, true, f)?;
        } else {
            if f.alternate() {
                writeln!(f, "{}", style::PUNCTUATION.apply_to("."))?;
            } else {
                writeln!(f, ".")?;
            }
        }

        // Done!
        Ok(())
    }
}

/// Defines an extension to an existing type, e.g.,
/// ```eflint
/// Extend Duty duty-to-vote
///   Conditioned by can-vote(voter).
/// ```
#[derive(Clone, Debug, Deserialize, EnumDebug, Serialize)]
#[serde(tag = "parent-kind")]
pub enum PhraseExtend {
    /// Extend a Fact, e.g.,
    /// ```eflint
    /// Extend Fact vote
    ///   Conditioned by citizen.person != candidate.person.
    /// ```
    #[serde(rename = "fact")]
    Fact(PhraseExtendFact),
    /// Extend an Event, e.g.,
    /// ```eflint
    /// Extend Event fire
    ///   Creates ash().
    /// ```
    #[serde(rename = "event")]
    Event(PhraseExtendEvent),
    /// Extend an Act, e.g.,
    /// ```eflint
    /// Extend Act vote
    ///   Terminates (Foreach administrator : duty-to-vote(citizen, administrator)).
    /// ```
    #[serde(rename = "act")]
    Act(PhraseExtendAct),
    /// Extend a Duty, e.g.,
    /// ```eflint
    /// Extend Duty duty-to-vote
    ///   Conditioned by can-vote(voter).
    /// ```
    #[serde(rename = "duty")]
    Duty(PhraseExtendDuty),
}
impl PhraseExtend {
    /// Returns the [`auxillary::ExtendKind`] that describes what this PhraseExtend extends.
    ///
    /// # Returns
    /// An equivalent [`auxillary::ExtendKind`].
    #[inline]
    pub fn kind(&self) -> auxillary::ExtendKind {
        match self {
            Self::Fact(_) => auxillary::ExtendKind::Fact,
            Self::Event(_) => auxillary::ExtendKind::Event,
            Self::Act(_) => auxillary::ExtendKind::Act,
            Self::Duty(_) => auxillary::ExtendKind::Duty,
        }
    }
}
#[cfg(feature = "display_eflint")]
impl DisplayEFlint for PhraseExtend {
    #[inline]
    fn eflint_fmt(&self, indent: usize, f: &mut Formatter<'_>) -> FResult {
        // Match to pass
        match self {
            Self::Fact(fact) => fact.eflint_fmt(indent, f),
            Self::Event(event) => event.eflint_fmt(indent, f),
            Self::Act(act) => act.eflint_fmt(indent, f),
            Self::Duty(duty) => duty.eflint_fmt(indent, f),
        }
    }
}

/// Defines an extension to an existing Fact, e.g.,
/// ```eflint
/// Extend Fact vote
///   Conditioned by citizen.person != candidate.person.
/// ```
#[derive(Clone, Debug, Deserialize, Serialize)]
pub struct PhraseExtendFact {
    /// The name of the thing to extend.
    pub name: String,
    /// Defines the common definition fields that can be extended.
    #[serde(flatten)]
    pub definition: TypeDefinitionCommon,
}
#[cfg(feature = "display_eflint")]
impl DisplayEFlint for PhraseExtendFact {
    #[inline]
    fn eflint_fmt(&self, indent: usize, f: &mut Formatter<'_>) -> FResult {
        let Self { name, definition } = self;

        // Write the "header"
        if f.alternate() {
            write!(
                f,
                "{}{} {} {}",
                Indent(indent),
                style::KEYWORD.apply_to("Extend"),
                style::DATA.apply_to("Fact"),
                style::BOLD_IDENTIFIER.apply_to(name),
            )?;
        } else {
            write!(f, "{}Extend Fact {}", Indent(indent), name,)?;
        };

        // Write the definition fields
        if !definition.is_empty() {
            writeln!(f)?;
            definition.eflint_fmt(indent + 4, true, f)?;
        } else {
            if f.alternate() {
                writeln!(f, "{}", style::PUNCTUATION.apply_to("."))?;
            } else {
                writeln!(f, ".")?;
            }
        }

        // Done!
        Ok(())
    }
}

/// Defines an extension to an existing Event, e.g.,
/// ```eflint
/// Extend Event fire
///   Creates ash().
/// ```
#[derive(Clone, Debug, Deserialize, Serialize)]
pub struct PhraseExtendEvent {
    /// The name of the thing to extend.
    pub name: String,
    /// Defines the common definition fields that can be extended.
    #[serde(flatten)]
    pub definition: TypeDefinitionCommon,
    /// Defines the common event fields that can be extended.
    #[serde(flatten)]
    pub event: EventDefinitionCommon,
}
#[cfg(feature = "display_eflint")]
impl DisplayEFlint for PhraseExtendEvent {
    #[inline]
    fn eflint_fmt(&self, indent: usize, f: &mut Formatter<'_>) -> FResult {
        let Self { name, definition, event } = self;

        // Write the "header"
        if f.alternate() {
            write!(
                f,
                "{}{} {} {}",
                Indent(indent),
                style::KEYWORD.apply_to("Extend"),
                style::DATA.apply_to("Event"),
                style::BOLD_IDENTIFIER.apply_to(name),
            )?;
        } else {
            write!(f, "{}Extend Event {}", Indent(indent), name,)?;
        };

        // Write the definition fields, then the duty fields
        if !definition.is_empty() || !event.is_empty() {
            writeln!(f)?;
            definition.eflint_fmt(indent + 4, event.is_empty(), f)?;
            event.eflint_fmt(indent + 4, true, f)?;
        } else {
            if f.alternate() {
                writeln!(f, "{}", style::PUNCTUATION.apply_to("."))?;
            } else {
                writeln!(f, ".")?;
            }
        }

        // Done!
        Ok(())
    }
}

/// Defines an extension to an existing Act, e.g.,
/// ```eflint
/// Extend Act vote
///   Terminates (Foreach administrator : duty-to-vote(citizen, administrator)).
/// ```
#[derive(Clone, Debug, Deserialize, Serialize)]
pub struct PhraseExtendAct {
    /// The name of the thing to extend.
    pub name: String,
    /// Defines the common definition fields that can be extended.
    #[serde(flatten)]
    pub definition: TypeDefinitionCommon,
    /// Defines the common event fields that can be extended.
    #[serde(flatten)]
    pub event: EventDefinitionCommon,
}
#[cfg(feature = "display_eflint")]
impl DisplayEFlint for PhraseExtendAct {
    #[inline]
    fn eflint_fmt(&self, indent: usize, f: &mut Formatter<'_>) -> FResult {
        let Self { name, definition, event } = self;

        // Write the "header"
        if f.alternate() {
            write!(
                f,
                "{}{} {} {}",
                Indent(indent),
                style::KEYWORD.apply_to("Extend"),
                style::DATA.apply_to("Act"),
                style::BOLD_IDENTIFIER.apply_to(name),
            )?;
        } else {
            write!(f, "{}Extend Act {}", Indent(indent), name,)?;
        };

        // Write the definition fields, then the duty fields
        if !definition.is_empty() || !event.is_empty() {
            writeln!(f)?;
            definition.eflint_fmt(indent + 4, event.is_empty(), f)?;
            event.eflint_fmt(indent + 4, true, f)?;
        } else {
            if f.alternate() {
                writeln!(f, "{}", style::PUNCTUATION.apply_to("."))?;
            } else {
                writeln!(f, ".")?;
            }
        }

        // Done!
        Ok(())
    }
}

/// Defines an extension to an existing Act, e.g.,
/// ```eflint
/// Extend Duty duty-to-vote
///   Conditioned by can-vote(voter).
/// ```
#[derive(Clone, Debug, Deserialize, Serialize)]
pub struct PhraseExtendDuty {
    /// The name of the thing to extend.
    pub name: String,
    /// Defines the common definition fields that can be extended.
    #[serde(flatten)]
    pub definition: TypeDefinitionCommon,
    /// Defines the common duty fields that can be extended.
    #[serde(flatten)]
    pub duty: DutyDefinitionCommon,
}
#[cfg(feature = "display_eflint")]
impl DisplayEFlint for PhraseExtendDuty {
    #[inline]
    fn eflint_fmt(&self, indent: usize, f: &mut Formatter<'_>) -> FResult {
        let Self { name, definition, duty } = self;

        // Write the "header"
        if f.alternate() {
            write!(
                f,
                "{}{} {} {}",
                Indent(indent),
                style::KEYWORD.apply_to("Extend"),
                style::DATA.apply_to("Duty"),
                style::BOLD_IDENTIFIER.apply_to(name),
            )?;
        } else {
            write!(f, "{}Extend Duty {}", Indent(indent), name,)?;
        };

        // Write the definition fields, then the duty fields
        if !definition.is_empty() || !duty.is_empty() {
            writeln!(f)?;
            definition.eflint_fmt(indent + 4, duty.is_empty(), f)?;
            duty.eflint_fmt(indent + 4, true, f)?;
        } else {
            if f.alternate() {
                writeln!(f, "{}", style::PUNCTUATION.apply_to("."))?;
            } else {
                writeln!(f, ".")?;
            }
        }

        // Done!
        Ok(())
    }
}



/// Defines the execution result of a particular [`Phrase`].
///
/// There are three variants:
/// - [Boolean queries](PhraseResult::BooleanQuery) encodes the result to a [boolean query](Phrase::BooleanQuery) (no way!);
#[derive(Clone, Debug, Deserialize, EnumDebug, Serialize)]
#[serde(untagged)]
pub enum PhraseResult {
    /// Encodes the result to a boolean query, i.e., to:
    /// ```eflint
    /// ?citizen(Amy).
    /// query successful  // <-- this
    /// ```
    BooleanQuery(PhraseResultBooleanQuery),
    /// Encodes the result to an instance query, i.e., to:
    /// ```eflint
    /// ?- citizen.
    /// citizen(string("Bob"))  // <-- these
    /// citizen(string("Amy"))  // <-- these
    /// ```
    InstanceQuery(PhraseResultInstanceQuery),
    /// Encodes the result to phrases that induce state changes, i.e., to:
    /// ```eflint
    /// +citizen(Amy).
    /// +citizen(string("Amy"))  // <-- this
    /// ```
    StateChange(PhraseResultStateChange),
}
#[cfg(feature = "display_eflint")]
impl DisplayEFlint for PhraseResult {
    #[inline]
    fn eflint_fmt(&self, indent: usize, f: &mut Formatter<'_>) -> FResult {
        // Match to delegate, wrapped in surrounding structs
        match self {
            Self::BooleanQuery(bquery) => bquery.eflint_fmt(indent, f),
            Self::InstanceQuery(iquery) => iquery.eflint_fmt(indent, f),
            Self::StateChange(schange) => schange.eflint_fmt(indent, f),
        }
    }
}

/// Defines the fields common to all [PhraseResult] variants.
#[derive(Clone, Debug, Deserialize, Serialize)]
pub struct PhraseResultCommon {
    /// Defines if the phrase's execution was a success, or whether there was an error in the backend reasoner.
    pub success: bool,
    /// Defines a list of errors that may have occurred in case `success` is false.
    #[serde(default = "Vec::new", skip_serializing_if = "Vec::is_empty")]
    pub errors:  Vec<Error>,
}
#[cfg(feature = "display_eflint")]
impl PhraseResultCommon {
    /// Allows this AST node to be serialized to the given formatter.
    ///
    /// This is used in the [`DisplayEFlint`]-trait. However, this trait itself is not implemented, as this is only implemented for types returning whole lines (thereby being "standalone"), as it were.
    ///
    /// # Arguments
    /// - `indent`: The indentation to print each line with.
    /// - `f`: The [`Formatter`] to write to.
    ///
    /// # Errors
    /// This function errors if we failed to write to the given formatter.
    #[inline]
    fn eflint_fmt(&self, indent: usize, f: &mut Formatter<'_>) -> FResult {
        let Self { success, errors } = self;

        // Write the success as a key/value pair
        if f.alternate() {
            writeln!(
                f,
                "{}success {} {}",
                Indent(indent),
                style::PUNCTUATION.apply_to(":"),
                if *success { style::SUCCESS.apply_to("true") } else { style::FAILURE.apply_to("false") }
            )?;
        } else {
            writeln!(f, "{}success : {}", Indent(indent), success)?;
        }

        // Write the errors if there are any
        if !errors.is_empty() {
            if f.alternate() {
                writeln!(f, "{}errors  {} {}", Indent(indent), style::PUNCTUATION.apply_to(":"), style::PUNCTUATION.apply_to("["))?;
            } else {
                writeln!(f, "{}errors  : [", Indent(indent))?;
            }
            for err in &self.errors {
                err.eflint_fmt(indent + 4, f)?;
            }
            writeln!(f, "{}{}", Indent(indent), style::PUNCTUATION.apply_to("]"))?;
        }

        // Done
        Ok(())
    }
}

/// Defines the result given by the server when a [boolean query](Phrase::BooleanQuery) is processed.
#[derive(Clone, Debug, Deserialize, Serialize)]
pub struct PhraseResultBooleanQuery {
    /// The common fields of any [`PhraseResult`].
    #[serde(flatten)]
    pub common: PhraseResultCommon,
    /// A boolean flag actually indicating the result of the query itself.
    pub result: bool,
}
#[cfg(feature = "display_eflint")]
impl DisplayEFlint for PhraseResultBooleanQuery {
    #[inline]
    fn eflint_fmt(&self, indent: usize, f: &mut Formatter<'_>) -> FResult {
        let Self { common, result } = self;

        // Write the header
        writeln!(f, "{}PhraseResult<BooleanQuery> {{", Indent(indent))?;

        // Write the common part
        common.eflint_fmt(indent + 4, f)?;

        // Write the result too, with extra emphasis
        if f.alternate() {
            writeln!(
                f,
                "{}{}",
                Indent(indent + 4),
                if *result { style::SUCCESS.apply_to("query succesful") } else { style::FAILURE.apply_to("query failed") }
            )?;
        } else {
            writeln!(f, "{}{}", Indent(indent + 4), if *result { "query succesful" } else { "query failed" })?;
        }

        // Finally, write the footer
        writeln!(f, "{}}}", Indent(indent))?;

        // Done!
        Ok(())
    }
}

/// Defines the result given by the server when an [instance query](Phrase::InstanceQuery) is processed.
#[derive(Clone, Debug, Deserialize, Serialize)]
pub struct PhraseResultInstanceQuery {
    /// The common fields of any [`PhraseResult`].
    #[serde(flatten)]
    pub common: PhraseResultCommon,
    /// The list of instances found, encoded as constructor applications.
    pub result: Vec<ExpressionConstructorApp>,
}
#[cfg(feature = "display_eflint")]
impl DisplayEFlint for PhraseResultInstanceQuery {
    #[inline]
    fn eflint_fmt(&self, indent: usize, f: &mut Formatter<'_>) -> FResult {
        let Self { common, result } = self;

        // Write the header
        writeln!(f, "{}PhraseResult<InstanceQuery> {{", Indent(indent))?;

        // Write the common part
        common.eflint_fmt(indent + 4, f)?;
        writeln!(f)?;

        // Write the list of found instances
        for res in result {
            // Write the constructor app
            write!(f, "{}", Indent(indent + 4))?;
            res.eflint_fmt(f)?;
            if f.alternate() {
                writeln!(f, "{}", style::PUNCTUATION.apply_to(","))?;
            } else {
                writeln!(f, ",")?;
            }
        }

        // Finally, write the footer
        writeln!(f, "{}}}", Indent(indent))?;

        // Done!
        Ok(())
    }
}

/// Defines state changes that are induced after executing a [Phrase].
#[derive(Clone, Debug, Deserialize, Serialize)]
pub struct PhraseResultStateChange {
    /// The common fields of any [`PhraseResult`].
    #[serde(flatten)]
    pub common: PhraseResultCommon,

    /// The list of changes given by the server, encoded as phrases necessary to re-create this state. If omitted, then the server does not want to share this (and is thus different than a [`Some(...)`] with an empty list).
    #[serde(skip_serializing_if = "Option::is_none")]
    pub changes:    Option<Vec<Phrase>>,
    /// Any Acts or Events that have been triggered by the phrase. If omitted, then the server does not want to share this (and is thus different than a [`Some(...)`] with an empty list).
    #[serde(skip_serializing_if = "Option::is_none")]
    pub triggers:   Option<Vec<Trigger>>,
    /// Whether or not the given phrase triggered any violations.
    pub violated:   bool,
    /// Any Acts, Duties or Invariants that have been violated by the phrase. If omitted, then the server does not want to share this (and is thus different than a [`Some(...)`] with an empty list).
    #[serde(skip_serializing_if = "Option::is_none")]
    pub violations: Option<Vec<Violation>>,
}
#[cfg(feature = "display_eflint")]
impl DisplayEFlint for PhraseResultStateChange {
    #[inline]
    fn eflint_fmt(&self, indent: usize, f: &mut Formatter<'_>) -> FResult {
        let Self { common, changes, triggers, violations, violated } = self;

        // Prepare some punctuation
        let colon: Box<dyn Display> = if f.alternate() { Box::new(style::PUNCTUATION.apply_to(":")) } else { Box::new(":") };

        // Write the header
        writeln!(f, "{}PhraseResult<StateChange> {{", Indent(indent))?;

        // Write the common part
        common.eflint_fmt(indent + 4, f)?;
        writeln!(f)?;

        // Do whether a violation has occurred first
        if f.alternate() {
            writeln!(
                f,
                "{}violated   {} {}",
                Indent(indent + 4),
                colon,
                if *violated { style::FAILURE.apply_to("true") } else { style::SUCCESS.apply_to("false") }
            )?;
        } else {
            writeln!(f, "{}violated   : {}", Indent(indent + 4), violated)?;
        }

        // Now write the changes, then the triggers, then the violations
        if let Some(changes) = changes {
            for change in changes {
                change.eflint_fmt(indent + 4, f)?;
            }
        }
        if let Some(triggers) = triggers {
            if !triggers.is_empty() {
                writeln!(f, "{}triggers   {}", Indent(indent + 4), colon)?;
                for trigger in triggers {
                    trigger.eflint_fmt(indent + 6, f)?;
                }
            }
        }
        if let Some(violations) = violations {
            if !violations.is_empty() {
                writeln!(f, "{}violations {}", Indent(indent + 4), colon)?;
                for violation in violations {
                    violation.eflint_fmt(indent + 6, f)?;
                }
            }
        }

        // Finally, write the footer
        writeln!(f, "{}}}", Indent(indent))?;

        // Done!
        Ok(())
    }
}



/// Defines how to specify a closed domain of an atomic eFLINT Fact when we declare it.
///
/// This has two variants:
/// - [Set-syntax](Domain::Set) defines a disjoint set of possible values; and
/// - [Range-syntax](Domain::Range) defines a contious range of values for, say, numbers.
#[derive(Clone, Debug, Deserialize, EnumDebug, Serialize)]
#[serde(untagged)]
pub enum Domain {
    /// A set of disjoint values that the atomic Fact can only ever take:
    /// ```eflint
    /// Fact number Identified by 1, 2, 3.
    /// ```
    Set(DomainSet),
    /// A continious range of values that the atomic Fact can only ever take:
    /// ```eflint
    /// Fact number Identified by 1..3.
    /// ```
    Range(DomainRange),
}
#[cfg(feature = "display_eflint")]
impl Domain {
    /// Allows this AST node to be serialized to the given formatter.
    ///
    /// This is used in the [`DisplayEFlint`]-trait. However, this trait itself is not implemented, as this is only implemented for types returning whole lines (thereby being "standalone"), as it were.
    ///
    /// # Arguments
    /// - `f`: The [`Formatter`] to write to.
    ///
    /// # Errors
    /// This function errors if we failed to write to the given formatter.
    #[inline]
    fn eflint_fmt(&self, f: &mut Formatter<'_>) -> FResult {
        match self {
            Self::Range(range) => range.eflint_fmt(f),
            Self::Set(set) => set.eflint_fmt(f),
        }
    }
}

/// Defines how to give a set of values as a domain for an atomic fact.
#[derive(Clone, Debug, Deserialize, Serialize)]
pub struct DomainSet(pub Vec<Expression>);
impl Deref for DomainSet {
    type Target = Vec<Expression>;

    #[inline]
    fn deref(&self) -> &Self::Target { &self.0 }
}
impl DerefMut for DomainSet {
    #[inline]
    fn deref_mut(&mut self) -> &mut Self::Target { &mut self.0 }
}
impl From<Vec<Expression>> for DomainSet {
    #[inline]
    fn from(value: Vec<Expression>) -> Self { Self(value) }
}
impl From<DomainSet> for Vec<Expression> {
    #[inline]
    fn from(value: DomainSet) -> Self { value.0 }
}
#[cfg(feature = "display_eflint")]
impl DomainSet {
    /// Allows this AST node to be serialized to the given formatter.
    ///
    /// This is used in the [`DisplayEFlint`]-trait. However, this trait itself is not implemented, as this is only implemented for types returning whole lines (thereby being "standalone"), as it were.
    ///
    /// # Arguments
    /// - `f`: The [`Formatter`] to write to.
    ///
    /// # Errors
    /// This function errors if we failed to write to the given formatter.
    fn eflint_fmt(&self, f: &mut Formatter<'_>) -> FResult {
        let Self(set) = self;

        // Write the list manually to allow the serializers to error
        let mut first: bool = true;
        for val in set {
            // Write punctuation
            if first {
                first = false;
            } else {
                if f.alternate() {
                    write!(f, "{}", style::PUNCTUATION.apply_to(", "))?;
                } else {
                    write!(f, ", ")?;
                }
            }

            // Write the value
            val.eflint_fmt(f)?;
        }

        // Done
        Ok(())
    }
}

/// Defines how to give a range of values as a domain for an atomic fact.
#[derive(Clone, Debug, Deserialize, Serialize)]
pub struct DomainRange {
    /// The start value of the range, inclusive.
    pub start: i64,
    /// The end value of the range, inclusive.
    pub end:   i64,
}
impl From<RangeInclusive<i64>> for DomainRange {
    #[inline]
    fn from(value: RangeInclusive<i64>) -> Self { Self { start: *value.start(), end: *value.end() } }
}
impl From<DomainRange> for RangeInclusive<i64> {
    #[inline]
    fn from(value: DomainRange) -> Self { value.start..=value.end }
}
#[cfg(feature = "display_eflint")]
impl DomainRange {
    /// Allows this AST node to be serialized to the given formatter.
    ///
    /// This is used in the [`DisplayEFlint`]-trait. However, this trait itself is not implemented, as this is only implemented for types returning whole lines (thereby being "standalone"), as it were.
    ///
    /// # Arguments
    /// - `f`: The [`Formatter`] to write to.
    ///
    /// # Errors
    /// This function errors if we failed to write to the given formatter.
    #[inline]
    fn eflint_fmt(&self, f: &mut Formatter<'_>) -> FResult {
        let Self { start, end } = self;
        if f.alternate() { write!(f, "{}..{}", style::NUMERIC.apply_to(start), style::NUMERIC.apply_to(end)) } else { write!(f, "{start}..{end}") }
    }
}



/// Defines an eFLINT expression that evaluates to a value.
///
/// There are multiple variants of this:
/// - [Primitives](Expression::Primitive): Constants/Literals;
/// - [Variable references](Expression::VarRef): References to quantified variables;
/// - [Construction applications](Expression::ConstructorApp): Instantiation of a type of some kind;
/// - [Operators](Expression::Operator): Addition, substraction, multiplication, etc.;
/// - [Iterators](Expression::Iterator): Foreach, forall, exists, etc.; and
/// - [Projections](Expression::Projection): Field accessing of some type.
#[derive(Clone, Debug, Deserialize, EnumDebug, Serialize)]
#[serde(untagged)]
pub enum Expression {
    /// eFLINT primitives, i.e., literal values:
    /// ```eflint
    /// "Amy"
    /// 42
    /// 42.0
    /// true
    /// ```
    Primitive(ExpressionPrimitive),

    /// eFLINT variable references:
    /// ```eflint
    /// citizen
    /// // As in second occurance in:
    /// Foreach citizen: citizen
    /// ```
    VarRef(ExpressionVarRef),

    /// Constructor applications, i.e., instantiating facts:
    /// ```eflint
    /// citizen("Amy")
    /// ```
    ConstructorApp(ExpressionConstructorApp),

    /// Operators (addition, multiplication, Holds, Violated, etc):
    /// ```eflint
    /// 1 + 2
    /// Holds("Amy")
    /// ```
    Operator(ExpressionOperator),

    /// Iterators that do inherent quantification.
    ///
    /// Note that this is different from operators like [Count](appendix::EFlintOperator::COUNT), which do not quantify themselves but rather process an already produced instance expression.
    ///
    /// For example:
    /// ```eflint
    /// Foreach citizen : citizen.
    /// Forall citizen : citizen.
    /// Exists citizen : citizen.
    /// ```
    Iterator(ExpressionIterator),

    /// Projection:
    /// ```eflint
    /// citizen.string
    /// ```
    Projection(ExpressionProjection),
}
impl Expression {
    /// Returns the kind of this expression, whether it's a [boolean](auxillary::ExpressionKind::Boolean) or [instance](auxillary::ExpressionKind::Instance) expression.
    ///
    /// # Returns
    /// An [`auxillary::ExpressionKind`] denoting which of the two kinds it is. If [`None`] is returned, then this is not statically determinable (this is the case for Operators and Iterators).
    #[inline]
    pub fn kind(&self) -> Option<auxillary::ExpressionKind> {
        match self {
            Expression::Primitive(primitive) => Some(match primitive {
                ExpressionPrimitive::Boolean(_) => auxillary::ExpressionKind::Boolean,
                ExpressionPrimitive::Integer(_) | ExpressionPrimitive::Float(_) | ExpressionPrimitive::String(_) => {
                    auxillary::ExpressionKind::Instance
                },
            }),
            Expression::VarRef(_) => Some(auxillary::ExpressionKind::Instance),
            Expression::ConstructorApp(_) => Some(auxillary::ExpressionKind::Instance),
            Expression::Operator(_) => None,
            Expression::Iterator(_) => None,
            Expression::Projection(_) => Some(auxillary::ExpressionKind::Instance),
        }
    }
}
#[cfg(feature = "display_eflint")]
impl Expression {
    /// Allows this AST node to be serialized to the given formatter.
    ///
    /// This is used in the [`DisplayEFlint`]-trait. However, this trait itself is not implemented, as this is only implemented for types returning whole lines (thereby being "standalone"), as it were.
    ///
    /// # Arguments
    /// - `f`: The [`Formatter`] to write to.
    ///
    /// # Errors
    /// This function errors if we failed to write to the given formatter.
    #[inline]
    fn eflint_fmt(&self, f: &mut Formatter<'_>) -> FResult {
        match self {
            Self::Primitive(primitive) => primitive.eflint_fmt(f),
            Self::VarRef(var_ref) => var_ref.eflint_fmt(f),
            Self::ConstructorApp(constr_app) => constr_app.eflint_fmt(f),
            Self::Operator(operator) => operator.eflint_fmt(f),
            Self::Iterator(iterator) => iterator.eflint_fmt(f),
            Self::Projection(proj) => proj.eflint_fmt(f),
        }
    }
}

/// Represents a primitive eFLINT type.
///
/// This, too, has multiple variants; one for every literal type ([strings](ExpressionPrimitive::String), [integer](ExpressionPrimitive::Integer), [float](ExpressionPrimitive::Float) and [booleans](ExpressionPrimitive::Boolean)).
///
/// Note that the specification makes no difference between integers and floating-point numbers. As such, any number without fractions are parsed as integers, and numbers with are parsed as floats.
///
/// For example:
/// ```eflint
/// "Amy"
/// 42
/// 42.0
/// true
/// ```
#[derive(Clone, Debug, Deserialize, EnumDebug, Serialize)]
#[serde(untagged)]
pub enum ExpressionPrimitive {
    /// String literals, e.g.:
    /// ```eflint
    /// "Amy"
    /// ```
    String(String),
    /// Integer literals, e.g.:
    /// ```eflint
    /// 42
    /// ```
    Integer(i64),
    /// Floating-point literals, e.g.:
    /// ```eflint
    /// 42.0
    /// ```
    Float(f64),
    /// Boolean literals, e.g.:
    /// ```eflint
    /// true
    /// ```
    Boolean(bool),
}
#[cfg(feature = "display_eflint")]
impl ExpressionPrimitive {
    /// Allows this AST node to be serialized to the given formatter.
    ///
    /// This is used in the [`DisplayEFlint`]-trait. However, this trait itself is not implemented, as this is only implemented for types returning whole lines (thereby being "standalone"), as it were.
    ///
    /// # Arguments
    /// - `f`: The [`Formatter`] to write to.
    ///
    /// # Errors
    /// This function errors if we failed to write to the given formatter.
    #[inline]
    fn eflint_fmt(&self, f: &mut Formatter<'_>) -> FResult {
        // Match on the type
        match self {
            Self::String(s) => {
                if f.alternate() {
                    write!(f, "{}", style::STRING.apply_to(format!("\"{s}\"")))
                } else {
                    write!(f, "\"{s}\"")
                }
            },

            Self::Integer(i) => {
                if f.alternate() {
                    write!(f, "{}", style::NUMERIC.apply_to(i))
                } else {
                    write!(f, "{i}")
                }
            },

            Self::Float(fl) => {
                if f.alternate() {
                    write!(f, "{}", style::NUMERIC.apply_to(fl))
                } else {
                    write!(f, "{fl}")
                }
            },

            Self::Boolean(b) => {
                if f.alternate() {
                    write!(f, "{}", style::NUMERIC.apply_to(b))
                } else {
                    write!(f, "{b}")
                }
            },
        }
    }
}

/// Represents a variable reference in eFLINT.
///
/// Note that this is serialized and deserialized as a _list_ of strings with only one string, to differentiate with a [literal string](ExpressionPrimitive::String).
///
/// For example:
/// ```eflint
/// citizen
/// // As in second occurance in:
/// Foreach citizen: citizen
/// ```
#[derive(Clone, Debug)]
pub struct ExpressionVarRef(pub String);
impl<'de> Deserialize<'de> for ExpressionVarRef {
    fn deserialize<D>(deserializer: D) -> Result<Self, D::Error>
    where
        D: Deserializer<'de>,
    {
        /// Visitor for the ExpressionVarRef
        struct ExpressionVarRefVisitor;
        impl<'de> Visitor<'de> for ExpressionVarRefVisitor {
            type Value = ExpressionVarRef;

            fn expecting(&self, f: &mut Formatter) -> FResult { write!(f, "a variable reference expression (list with a single string)") }

            fn visit_seq<A>(self, mut seq: A) -> Result<Self::Value, A::Error>
            where
                A: SeqAccess<'de>,
            {
                if let Some(value) = seq.next_element::<String>()? {
                    // Assert there is no other
                    if seq.next_element::<String>()?.is_none() {
                        Ok(ExpressionVarRef(value))
                    } else {
                        Err(<A as SeqAccess<'de>>::Error::custom(errors::ExpressionVarRefParseError::TooMany))
                    }
                } else {
                    Err(<A as SeqAccess<'de>>::Error::custom(errors::ExpressionVarRefParseError::TooFew))
                }
            }
        }

        // Parse as an array of strings
        deserializer.deserialize_seq(ExpressionVarRefVisitor)
    }
}
impl Serialize for ExpressionVarRef {
    fn serialize<S>(&self, serializer: S) -> Result<S::Ok, S::Error>
    where
        S: Serializer,
    {
        let mut seq = serializer.serialize_seq(Some(1))?;
        seq.serialize_element(&self.0)?;
        seq.end()
    }
}
impl Deref for ExpressionVarRef {
    type Target = String;

    #[inline]
    fn deref(&self) -> &Self::Target { &self.0 }
}
impl DerefMut for ExpressionVarRef {
    #[inline]
    fn deref_mut(&mut self) -> &mut Self::Target { &mut self.0 }
}
impl From<String> for ExpressionVarRef {
    #[inline]
    fn from(value: String) -> Self { Self(value) }
}
impl From<ExpressionVarRef> for String {
    #[inline]
    fn from(value: ExpressionVarRef) -> Self { value.0 }
}
#[cfg(feature = "display_eflint")]
impl ExpressionVarRef {
    /// Allows this AST node to be serialized to the given formatter.
    ///
    /// This is used in the [`DisplayEFlint`]-trait. However, this trait itself is not implemented, as this is only implemented for types returning whole lines (thereby being "standalone"), as it were.
    ///
    /// # Arguments
    /// - `f`: The [`Formatter`] to write to.
    ///
    /// # Errors
    /// This function errors if we failed to write to the given formatter.
    #[inline]
    fn eflint_fmt(&self, f: &mut Formatter<'_>) -> FResult {
        let Self(identifier) = self;

        // Write the variable identifier
        write!(f, "{identifier}")?;

        // Done
        Ok(())
    }
}

/// Defines a constructor application in eFLINT.
///
/// For example:
/// ```eflint
/// citizen("Amy")
/// ```
#[derive(Clone, Debug, Deserialize, Serialize)]
pub struct ExpressionConstructorApp {
    /// The name of the type we're instantiating.
    pub identifier: String,
    /// The list of operands to instantiate, as a [`ConstructorInput`].
    ///
    /// This because there can be multiple ways of instantiation:
    /// ```eflint
    /// // Array syntax
    /// citizen("Amy")
    /// // Map syntax
    /// citizen(string="Amy")
    /// ```
    #[serde(default = "ConstructorInput::default")]
    pub operands:   ConstructorInput,
}
#[cfg(feature = "display_eflint")]
impl ExpressionConstructorApp {
    /// Allows this AST node to be serialized to the given formatter.
    ///
    /// This is used in the [`DisplayEFlint`]-trait. However, this trait itself is not implemented, as this is only implemented for types returning whole lines (thereby being "standalone"), as it were.
    ///
    /// # Arguments
    /// - `f`: The [`Formatter`] to write to.
    ///
    /// # Errors
    /// This function errors if we failed to write to the given formatter.
    fn eflint_fmt(&self, f: &mut Formatter<'_>) -> FResult {
        let Self { identifier, operands } = self;

        // Write the type identifier
        write!(f, "{identifier}")?;

        // Write the brackets, with the operands in them
        if f.alternate() {
            write!(f, "{}", style::PUNCTUATION.apply_to("("))?;
            operands.eflint_fmt(f)?;
            write!(f, "{}", style::PUNCTUATION.apply_to(")"))?;
        } else {
            write!(f, "(")?;
            operands.eflint_fmt(f)?;
            write!(f, ")")?;
        }

        // Done
        Ok(())
    }
}

/// Defines an operator application in eFLINT.
///
/// For example:
/// ```eflint
/// 1 + 2
/// Holds("Amy")
/// ```
#[derive(Clone, Debug, Deserialize, Serialize)]
pub struct ExpressionOperator {
    /// The operator that we're applying. See [`appendix::EFlintOperator`] for a list of eFLINT operators.
    pub operator: String,
    /// The operands to give to the operator. It depends on the operator itself how many are necessary.
    pub operands: Vec<Expression>,
}
#[cfg(feature = "display_eflint")]
impl ExpressionOperator {
    /// Allows this AST node to be serialized to the given formatter.
    ///
    /// This is used in the [`DisplayEFlint`]-trait. However, this trait itself is not implemented, as this is only implemented for types returning whole lines (thereby being "standalone"), as it were.
    ///
    /// # Arguments
    /// - `f`: The [`Formatter`] to write to.
    ///
    /// # Errors
    /// This function errors if we failed to write to the given formatter.
    fn eflint_fmt(&self, f: &mut Formatter<'_>) -> FResult {
        use appendix::EFlintOperator;

        let Self { operator, operands } = self;

        // Prepare some syntax
        let op_style: Style = if f.alternate() { style::OPERATOR.clone() } else { Style::new() };
        let comma: Box<dyn Display> = if f.alternate() { Box::new(style::PUNCTUATION.apply_to(",")) } else { Box::new(",") };
        let lparen: Box<dyn Display> = if f.alternate() { Box::new(style::PUNCTUATION.apply_to("(")) } else { Box::new("(") };
        let rparen: Box<dyn Display> = if f.alternate() { Box::new(style::PUNCTUATION.apply_to(")")) } else { Box::new(")") };
        let none: Box<dyn Display> = if f.alternate() { Box::new(style::INVALID.apply_to("<NONE>")) } else { Box::new("<NONE>") };

        // We can commit to (known supported) eFLINT operators because we're serializing as eFLINT
        match operator.as_str() {
            EFlintOperator::AND => {
                write!(f, "{lparen}")?;
                if let Some(lhs) = operands.get(0) {
                    lhs.eflint_fmt(f)?;
                } else {
                    write!(f, "{none}")?;
                }
                write!(f, " {} ", op_style.apply_to("&&"))?;
                if let Some(rhs) = operands.get(1) {
                    rhs.eflint_fmt(f)?;
                } else {
                    write!(f, "{none}")?;
                }
                write!(f, "{rparen}")
            },
            EFlintOperator::OR => {
                write!(f, "{lparen}")?;
                if let Some(lhs) = operands.get(0) {
                    lhs.eflint_fmt(f)?;
                } else {
                    write!(f, "{none}")?;
                }
                write!(f, " {} ", op_style.apply_to("||"))?;
                if let Some(rhs) = operands.get(1) {
                    rhs.eflint_fmt(f)?;
                } else {
                    write!(f, "{none}")?;
                }
                write!(f, "{rparen}")
            },
            EFlintOperator::NOT => {
                write!(f, "{}{}", op_style.apply_to("Not"), lparen)?;
                if let Some(expr) = operands.get(0) {
                    expr.eflint_fmt(f)?;
                } else {
                    write!(f, "{none}")?;
                }
                write!(f, "{rparen}")
            },
            EFlintOperator::EQUALS => {
                write!(f, "{lparen}")?;
                if let Some(lhs) = operands.get(0) {
                    lhs.eflint_fmt(f)?;
                } else {
                    write!(f, "{none}")?;
                }
                write!(f, " {} ", op_style.apply_to("=="))?;
                if let Some(rhs) = operands.get(1) {
                    rhs.eflint_fmt(f)?;
                } else {
                    write!(f, "{none}")?;
                }
                write!(f, "{rparen}")
            },
            EFlintOperator::NOT_EQUALS => {
                write!(f, "{lparen}")?;
                if let Some(lhs) = operands.get(0) {
                    lhs.eflint_fmt(f)?;
                } else {
                    write!(f, "{none}")?;
                }
                write!(f, " {} ", op_style.apply_to("!="))?;
                if let Some(rhs) = operands.get(1) {
                    rhs.eflint_fmt(f)?;
                } else {
                    write!(f, "{none}")?;
                }
                write!(f, "{rparen}")
            },
            EFlintOperator::GREATER => {
                write!(f, "{lparen}")?;
                if let Some(lhs) = operands.get(0) {
                    lhs.eflint_fmt(f)?;
                } else {
                    write!(f, "{none}")?;
                }
                write!(f, " {} ", op_style.apply_to(">"))?;
                if let Some(rhs) = operands.get(1) {
                    rhs.eflint_fmt(f)?;
                } else {
                    write!(f, "{none}")?;
                }
                write!(f, "{rparen}")
            },
            EFlintOperator::GREATER_OR_EQUALS => {
                write!(f, "{lparen}")?;
                if let Some(lhs) = operands.get(0) {
                    lhs.eflint_fmt(f)?;
                } else {
                    write!(f, "{none}")?;
                }
                write!(f, " {} ", op_style.apply_to(">="))?;
                if let Some(rhs) = operands.get(1) {
                    rhs.eflint_fmt(f)?;
                } else {
                    write!(f, "{none}")?;
                }
                write!(f, "{rparen}")
            },
            EFlintOperator::LESSER => {
                write!(f, "{lparen}")?;
                if let Some(lhs) = operands.get(0) {
                    lhs.eflint_fmt(f)?;
                } else {
                    write!(f, "{none}")?;
                }
                write!(f, " {} ", op_style.apply_to("<"))?;
                if let Some(rhs) = operands.get(1) {
                    rhs.eflint_fmt(f)?;
                } else {
                    write!(f, "{none}")?;
                }
                write!(f, "{rparen}")
            },
            EFlintOperator::LESSER_OR_EQUALS => {
                write!(f, "{lparen}")?;
                if let Some(lhs) = operands.get(0) {
                    lhs.eflint_fmt(f)?;
                } else {
                    write!(f, "{none}")?;
                }
                write!(f, " {} ", op_style.apply_to("<="))?;
                if let Some(rhs) = operands.get(1) {
                    rhs.eflint_fmt(f)?;
                } else {
                    write!(f, "{none}")?;
                }
                write!(f, "{rparen}")
            },
            EFlintOperator::ADD => {
                write!(f, "{lparen}")?;
                if let Some(lhs) = operands.get(0) {
                    lhs.eflint_fmt(f)?;
                } else {
                    write!(f, "{none}")?;
                }
                write!(f, " {} ", op_style.apply_to("+"))?;
                if let Some(rhs) = operands.get(1) {
                    rhs.eflint_fmt(f)?;
                } else {
                    write!(f, "{none}")?;
                }
                write!(f, "{rparen}")
            },
            EFlintOperator::SUB => {
                write!(f, "{lparen}")?;
                if let Some(lhs) = operands.get(0) {
                    lhs.eflint_fmt(f)?;
                } else {
                    write!(f, "{none}")?;
                }
                write!(f, " {} ", op_style.apply_to("-"))?;
                if let Some(rhs) = operands.get(1) {
                    rhs.eflint_fmt(f)?;
                } else {
                    write!(f, "{none}")?;
                }
                write!(f, "{rparen}")
            },
            EFlintOperator::MUL => {
                write!(f, "{lparen}")?;
                if let Some(lhs) = operands.get(0) {
                    lhs.eflint_fmt(f)?;
                } else {
                    write!(f, "{none}")?;
                }
                write!(f, " {} ", op_style.apply_to("*"))?;
                if let Some(rhs) = operands.get(1) {
                    rhs.eflint_fmt(f)?;
                } else {
                    write!(f, "{none}")?;
                }
                write!(f, "{rparen}")
            },
            EFlintOperator::DIV => {
                write!(f, "{lparen}")?;
                if let Some(lhs) = operands.get(0) {
                    lhs.eflint_fmt(f)?;
                } else {
                    write!(f, "{none}")?;
                }
                write!(f, " {} ", op_style.apply_to("/"))?;
                if let Some(rhs) = operands.get(1) {
                    rhs.eflint_fmt(f)?;
                } else {
                    write!(f, "{none}")?;
                }
                write!(f, "{rparen}")
            },
            EFlintOperator::MOD => {
                write!(f, "{lparen}")?;
                if let Some(lhs) = operands.get(0) {
                    lhs.eflint_fmt(f)?;
                } else {
                    write!(f, "{none}")?;
                }
                write!(f, " {} ", op_style.apply_to("%"))?;
                if let Some(rhs) = operands.get(1) {
                    rhs.eflint_fmt(f)?;
                } else {
                    write!(f, "{none}")?;
                }
                write!(f, "{rparen}")
            },
            EFlintOperator::COUNT => {
                write!(f, "{}{}", op_style.apply_to("Count"), lparen)?;
                if let Some(expr) = operands.get(0) {
                    expr.eflint_fmt(f)?;
                } else {
                    write!(f, "{none}")?;
                }
                write!(f, "{rparen}")
            },
            EFlintOperator::SUM => {
                write!(f, "{}{}", op_style.apply_to("Sum"), lparen)?;
                if let Some(expr) = operands.get(0) {
                    expr.eflint_fmt(f)?;
                } else {
                    write!(f, "{none}")?;
                }
                write!(f, "{rparen}")
            },
            EFlintOperator::MAX => {
                write!(f, "{}{}", op_style.apply_to("Max"), lparen)?;
                if let Some(expr) = operands.get(0) {
                    expr.eflint_fmt(f)?;
                } else {
                    write!(f, "{none}")?;
                }
                write!(f, "{rparen}")
            },
            EFlintOperator::MIN => {
                write!(f, "{}{}", op_style.apply_to("Min"), lparen)?;
                if let Some(expr) = operands.get(0) {
                    expr.eflint_fmt(f)?;
                } else {
                    write!(f, "{none}")?;
                }
                write!(f, "{rparen}")
            },
            EFlintOperator::WHEN => {
                write!(f, "{lparen}")?;
                if let Some(lhs) = operands.get(0) {
                    lhs.eflint_fmt(f)?;
                } else {
                    write!(f, "{none}")?;
                }
                write!(f, " {} ", op_style.apply_to("When"))?;
                if let Some(rhs) = operands.get(1) {
                    rhs.eflint_fmt(f)?;
                } else {
                    write!(f, "{none}")?;
                }
                write!(f, "{rparen}")
            },
            EFlintOperator::HOLDS => {
                write!(f, "{}{}", op_style.apply_to("Holds"), lparen)?;
                if let Some(expr) = operands.get(0) {
                    expr.eflint_fmt(f)?;
                } else {
                    write!(f, "{none}")?;
                }
                write!(f, "{rparen}")
            },
            EFlintOperator::ENABLED => {
                write!(f, "{}{}", op_style.apply_to("Enabled"), lparen)?;
                if let Some(expr) = operands.get(0) {
                    expr.eflint_fmt(f)?;
                } else {
                    write!(f, "{none}")?;
                }
                write!(f, "{rparen}")
            },
            EFlintOperator::VIOLATED => {
                write!(f, "{}{}", op_style.apply_to("Violated"), lparen)?;
                if let Some(expr) = operands.get(0) {
                    expr.eflint_fmt(f)?;
                } else {
                    write!(f, "{none}")?;
                }
                write!(f, "{rparen}")
            },
            other => {
                write!(f, "{}{}", op_style.apply_to(other), lparen)?;
                let mut first: bool = true;
                for operand in operands {
                    // Write any comma in the list
                    if first {
                        first = false;
                    } else {
                        write!(f, "{comma} ")?;
                    }

                    // Write the operand
                    operand.eflint_fmt(f)?;
                }
                write!(f, "{rparen}")
            },
        }
    }
}

/// Defines an iterator expression in eFLINT.
///
/// Note that this is different from operators like [Count](appendix::EFlintOperator::COUNT), which do not quantify themselves but rather process an already produced instance expression.
///
/// For example:
/// ```eflint
/// Foreach citizen : citizen.
/// Forall citizen : citizen.
/// Exists citizen : citizen.
/// ```
#[derive(Clone, Debug, Deserialize, Serialize)]
pub struct ExpressionIterator {
    /// The iterator operator to execute. See [appendix::EFlintIteratorOperator] for a list of known eFLINT operators.
    pub iterator:   String,
    /// The list of variables bound by this iterator. Basically the first occurrence of `citizen` in:
    /// ```eflint
    /// Foreach citizen : citizen.
    /// ```
    pub binds:      Vec<String>,
    /// The expression that is repeated for every quantified combination of bound variables.
    ///
    /// For Foreach, this is an [instance expressions](auxillary::ExpressionKind::Instance). For Exists and Forall, these are [boolean expressions](auxillary::ExpressionKind::Boolean).
    pub expression: Box<Expression>,
}
#[cfg(feature = "display_eflint")]
impl ExpressionIterator {
    /// Allows this AST node to be serialized to the given formatter.
    ///
    /// This is used in the [`DisplayEFlint`]-trait. However, this trait itself is not implemented, as this is only implemented for types returning whole lines (thereby being "standalone"), as it were.
    ///
    /// # Arguments
    /// - `f`: The [`Formatter`] to write to.
    ///
    /// # Errors
    /// This function errors if we failed to write to the given formatter.
    fn eflint_fmt(&self, f: &mut Formatter<'_>) -> FResult {
        use appendix::EFlintIteratorOperator;

        let Self { iterator, binds, expression } = self;

        // Prepare some syntax
        let op_style: Style = if f.alternate() { style::OPERATOR.clone() } else { Style::new() };
        let comma: String = if f.alternate() { style::PUNCTUATION.apply_to(", ").to_string() } else { ", ".into() };
        let colon: Box<dyn Display> = if f.alternate() { Box::new(style::PUNCTUATION.apply_to(":")) } else { Box::new(":") };
        let lparen: Box<dyn Display> = if f.alternate() { Box::new(style::PUNCTUATION.apply_to("(")) } else { Box::new("(") };
        let rparen: Box<dyn Display> = if f.alternate() { Box::new(style::PUNCTUATION.apply_to(")")) } else { Box::new(")") };

        // Write openening parenthesis
        write!(f, "{lparen}")?;

        // We can commit to (known supported) eFLINT iterator operators because we're serializing as eFLINT
        match iterator.as_str() {
            EFlintIteratorOperator::EXISTS => {
                write!(f, "{}", op_style.apply_to("Exists"))?;
            },
            EFlintIteratorOperator::FORALL => {
                write!(f, "{}", op_style.apply_to("Forall"))?;
            },
            EFlintIteratorOperator::FOREACH => {
                write!(f, "{}", op_style.apply_to("Foreach"))?;
            },
            other => {
                write!(f, "{}", op_style.apply_to(other))?;
            },
        }

        // Write the binds & the expression
        write!(f, " {} {} ", binds.join(&comma), colon)?;
        expression.eflint_fmt(f)?;

        // Write closing parenthesis
        write!(f, "{rparen}")
    }
}

/// Defines a type projection in eFLINT.
///
/// For example:
/// ```eflint
/// citizen.string
/// ```
#[derive(Clone, Debug, Deserialize, Serialize)]
pub struct ExpressionProjection {
    /// The identifier of the field to project onto the `operand`.
    ///
    /// Basically `string` in:
    /// ```eflint
    /// citizen.string
    /// ```
    pub parameter: String,
    /// The expression evaluating to the instance on which to project the `parameter`
    ///
    /// Basically `citizen` in:
    /// ```eflint
    /// citizen.string
    /// ```
    pub operand:   Box<Expression>,
}
#[cfg(feature = "display_eflint")]
impl ExpressionProjection {
    /// Allows this AST node to be serialized to the given formatter.
    ///
    /// This is used in the [`DisplayEFlint`]-trait. However, this trait itself is not implemented, as this is only implemented for types returning whole lines (thereby being "standalone"), as it were.
    ///
    /// # Arguments
    /// - `f`: The [`Formatter`] to write to.
    ///
    /// # Errors
    /// This function errors if we failed to write to the given formatter.
    fn eflint_fmt(&self, f: &mut Formatter<'_>) -> FResult {
        let Self { parameter, operand } = self;

        // Write the operand, then the parameter
        operand.eflint_fmt(f)?;
        if f.alternate() {
            write!(f, "{}{}", style::PUNCTUATION.apply_to("."), parameter)?;
        } else {
            write!(f, ".{parameter}")?;
        }

        // Done
        Ok(())
    }
}



/// Defines the input to a [constructor application](Expression::ConstructorApp).
///
/// Basically defines the arguments to a constructor application, e.g.:
/// ```eflint
/// // Array syntax
/// has-voted(Amy, Bob).
///
/// // Map syntax
/// has-voted(citizen1=Amy, citizen2=Bob).
/// ```
#[derive(Clone, Debug, Deserialize, EnumDebug, Serialize)]
#[serde(untagged)]
pub enum ConstructorInput {
    /// It's given as an array of values that must match the input to the instance completely.
    ArraySyntax(Vec<Expression>),
    /// It's given as a map of field names to values that only needs to match the instance partially.
    MapSyntax(HashMap<String, Expression>),
}
impl Default for ConstructorInput {
    #[inline]
    fn default() -> Self { Self::ArraySyntax(vec![]) }
}
#[cfg(feature = "display_eflint")]
impl ConstructorInput {
    /// Allows this AST node to be serialized to the given formatter.
    ///
    /// This is used in the [`DisplayEFlint`]-trait. However, this trait itself is not implemented, as this is only implemented for types returning whole lines (thereby being "standalone"), as it were.
    ///
    /// # Arguments
    /// - `f`: The [`Formatter`] to write to.
    ///
    /// # Errors
    /// This function errors if we failed to write to the given formatter.
    fn eflint_fmt(&self, f: &mut Formatter<'_>) -> FResult {
        // Define some (possibly coloured) punctuation
        let comma: String = if f.alternate() { style::PUNCTUATION.apply_to(", ").to_string() } else { ", ".into() };

        // Match on what kind of input
        match self {
            Self::ArraySyntax(vals) => {
                // Serialize the values separately to allow them to quit
                let mut first: bool = true;
                for val in vals {
                    if first {
                        first = false;
                    } else {
                        write!(f, "{comma}")?;
                    }
                    val.eflint_fmt(f)?
                }

                // Done!
                Ok(())
            },

            Self::MapSyntax(vals) => {
                // Serialize the values separately to allow them to quit
                let mut first: bool = true;
                for (field, val) in vals {
                    // Write any preceding comma
                    if first {
                        first = false;
                    } else {
                        write!(f, "{comma}")?;
                    }

                    // Write it as a pair
                    if f.alternate() {
                        write!(f, "{}{}", style::BOLD_IDENTIFIER.apply_to(field), style::PUNCTUATION.apply_to("="))?;
                    } else {
                        write!(f, "{field}=")?;
                    }
                    val.eflint_fmt(f)?
                }

                // Done!
                Ok(())
            },
        }
    }
}

/// Encodes the trigger of an Event or Act that occurs when running an eFLINT spec.
#[derive(Clone, Debug, Deserialize, Serialize)]
pub struct Trigger {
    /// The kind of thing triggered.
    pub kind:     auxillary::TriggerKind,
    /// The identifier (=name) of the thing that triggered this thing. May be `null` to indicate no parent.
    pub parent:   Option<String>,
    /// The identifier (=name) of the triggered thing.
    pub name:     String,
    /// The operands given to the thing that *got* triggered (not that triggered).
    pub operands: Vec<Expression>,
}
#[cfg(feature = "display_eflint")]
impl DisplayEFlint for Trigger {
    fn eflint_fmt(&self, indent: usize, f: &mut Formatter<'_>) -> FResult {
        // let Self { kind, parent, name, operands } = self;

        // if f.alternate() {
        //     writeln!(
        //         f,
        //         "{}{} {}{} {}{}{}{}{}",
        //         Indent(indent),
        //         style::TRIGGER.apply_to("triggered"),
        //         style::BOLD_IDENTIFIER.apply_to(kind),
        //         style::PUNCTUATION.apply_to(":"),
        //         style::BOLD_IDENTIFIER.apply_to(&self.name),
        //         style::PUNCTUATION.apply_to("("),
        //         operands.iter().map(|expr| todo!()).collect::<Vec<String>>().join(&style::PUNCTUATION.apply_to(",").to_string()),
        //         style::PUNCTUATION.apply_to(")"),
        //         if let Some(parent) = parent { style::TRIGGER_PARENT.apply_to(format!(" <- {parent}")).to_string() } else { String::new() },
        //     )
        // } else {
        //     writeln!(
        //         f,
        //         "{}triggered {}: {}({}){}",
        //         Indent(indent),
        //         kind,
        //         name,
        //         operands.iter().map(|expr| todo!()).collect::<Vec<String>>().join(", "),
        //         if let Some(parent) = parent { format!(" <- {parent}") } else { String::new() }
        //     )
        // }

        let Self { kind, parent, name, operands } = self;

        // Serialize the `violated <type>!`-prefix
        if f.alternate() {
            write!(
                f,
                "{}{} {}{} ",
                Indent(indent),
                style::TRIGGER.apply_to("triggered"),
                style::BOLD_IDENTIFIER.apply_to(kind),
                style::PUNCTUATION.apply_to(":"),
            )?;
        } else {
            write!(f, "{}triggered {}: ", Indent(indent), kind)?;
        }

        // Serialize the rest as a constructor app; so first the ID itself (but bold for prettiness)
        if f.alternate() {
            write!(f, "{}{}", style::BOLD_IDENTIFIER.apply_to(name), style::PUNCTUATION.apply_to("("))?;
        } else {
            write!(f, "{name}(")?;
        }

        // Serialize the operands
        let mut first: bool = true;
        for operand in operands {
            // Write a comma if needed
            if first {
                first = false;
            } else {
                if f.alternate() {
                    write!(f, "{}", style::PUNCTUATION.apply_to(", "))?;
                } else {
                    write!(f, ", ")?;
                }
            }

            // Write the operand
            operand.eflint_fmt(f)?;
        }

        // Write the closing parenthesis
        if f.alternate() {
            write!(f, "{}", style::PUNCTUATION.apply_to(")"))?;
        } else {
            write!(f, ")")?;
        }

        // If there is a parent, write it
        if let Some(parent) = parent {
            if f.alternate() {
                write!(f, "{}", style::TRIGGER_PARENT.apply_to(format!(" <-- {parent}")))?;
            } else {
                write!(f, " <-- {parent}")?;
            }
        }

        // Done
        writeln!(f)
    }
}

/// Encodes a violation that occurs when running an eFLINT spec.
#[derive(Clone, Debug, Deserialize, Serialize)]
pub struct Violation {
    /// The kind of thing violated.
    pub kind: auxillary::ViolationKind,
    /// The identifier (=name) of the violated thing.
    pub identifier: String,
    /// The operands given to the thing that violated.
    pub operands: Vec<Expression>,
}
#[cfg(feature = "display_eflint")]
impl DisplayEFlint for Violation {
    fn eflint_fmt(&self, indent: usize, f: &mut Formatter<'_>) -> FResult {
        let Self { kind, identifier, operands } = self;

        // Serialize the `violated <type>!`-prefix
        if f.alternate() {
            write!(
                f,
                "{}{} {}{}{} ",
                Indent(indent),
                style::VIOLATION.apply_to("violated"),
                style::BOLD_IDENTIFIER.apply_to(kind),
                style::VIOLATION.apply_to("!"),
                style::PUNCTUATION.apply_to(":"),
            )?;
        } else {
            write!(f, "{}violated {}!: ", Indent(indent), kind)?;
        }

        // Serialize the rest as a constructor app; so first the ID itself (but bold for prettiness)
        if f.alternate() {
            write!(f, "{}{}", style::BOLD_IDENTIFIER.apply_to(identifier), style::PUNCTUATION.apply_to("("))?;
        } else {
            write!(f, "{identifier}(")?;
        }

        // Serialize the operands
        let mut first: bool = true;
        for operand in operands {
            // Write a comma if needed
            if first {
                first = false;
            } else {
                if f.alternate() {
                    write!(f, "{}", style::PUNCTUATION.apply_to(", "))?;
                } else {
                    write!(f, ", ")?;
                }
            }

            // Write the operand
            operand.eflint_fmt(f)?;
        }

        // Write the closing parenthesis
        if f.alternate() {
            writeln!(f, "{}", style::PUNCTUATION.apply_to(")"))?;
        } else {
            writeln!(f, ")")?;
        }

        // Done
        Ok(())
    }
}





/***** APPENDIX *****/
pub mod appendix {
    use super::auxillary::ExpressionKind;


    /// Defines identifiers for reasoners.
    ///
    /// Reasoners the specification is aware of:
    /// - [eFLINT](https://gitlab.com/eflint): [`Reasoner::EFLINT`].
    #[derive(Clone, Copy, Debug)]
    pub struct Reasoner;
    impl Reasoner {
        /// Defines the eFLINT reasoner.
        pub const EFLINT: &str = "eflint";

        /// Returns a list of all the reasoners known.
        ///
        /// # Returns
        /// A static slice with all reasoners.
        pub const fn all() -> &'static [&'static str] { &[Self::EFLINT] }
    }

    /// Defines identifiers for eFLINT operators, as well as the number of operands they require.
    ///
    /// Note that iterator operators (FORALL, FOREACH, EXISTS) are defined separately in [`EFlintIteratorOperator`].
    #[derive(Clone, Copy, Debug)]
    pub struct EFlintOperator;
    impl EFlintOperator {
        /// Arithmetic addition on two numeric values.
        pub const ADD: &str = "ADD";
        /// Conjunction on two boolean values.
        pub const AND: &str = "AND";
        /// Counts the number of instances generated by a single instance value.
        pub const COUNT: &str = "COUNT";
        /// Arithmetic division on two numeric values.
        pub const DIV: &str = "DIV";
        /// Takes a single instance value and checks if that instance _can_ be derived by the current rules. Essentially is [`EFlintOperator::HOLDS`] but without considering postulation.
        pub const ENABLED: &str = "ENABLED";
        /// Checks if two values are equal.
        pub const EQUALS: &str = "EQ";
        /// Compares two numeric values to examine if the first is stricly greater than the second.
        pub const GREATER: &str = "GT";
        /// Compares two numeric values to examine if the first is greater than- _or_ equal to the second.
        pub const GREATER_OR_EQUALS: &str = "GE";
        /// Essentially inline boolean query, i.e., takes a single instance value and checks if that instance is true.
        pub const HOLDS: &str = "HOLDS";
        /// Compares two numeric values to examine if the first is stricly smaller than the second.
        pub const LESSER: &str = "LT";
        /// Compares two numeric values to examine if the first is smaller than- _or_ equal to the second.
        pub const LESSER_OR_EQUALS: &str = "LE";
        /// Returns the maximum value from the instances generated by a single instance value.
        pub const MAX: &str = "MAX";
        /// Returns the minimum value from the instances generated by a single instance value.
        pub const MIN: &str = "MIN";
        /// Arithmetic modulo on two numeric values.
        pub const MOD: &str = "MOD";
        /// Arithmetic multiplication on two numeric values.
        pub const MUL: &str = "MUL";
        /// Negation on one boolean value.
        pub const NOT: &str = "NOT";
        /// Checks if two values are _not_ equal (inverse of [`EFlintOperator::EQUALS`]).
        pub const NOT_EQUALS: &str = "NE";
        /// Disjunction on two boolean values.
        pub const OR: &str = "OR";
        /// Arithmetic subtraction on two numeric values.
        pub const SUB: &str = "SUB";
        /// Sums the instances generated by a single instance value together to a numeric value.
        pub const SUM: &str = "SUM";
        /// Takes a single instance value and checks if, if that instantiation were to be added to the knowledge base, it would trigger any violations.
        pub const VIOLATED: &str = "VIOLATED";
        /// Filters an instance expression with a boolean expression to keep only the ones that evaluate to true.
        pub const WHEN: &str = "WHEN";

        /// Returns a list of all the eFLINT operators known.
        ///
        /// # Returns
        /// A static slice with all operators.
        pub const fn all() -> &'static [&'static str] {
            &[
                Self::AND,
                Self::OR,
                Self::NOT,
                Self::EQUALS,
                Self::NOT_EQUALS,
                Self::GREATER,
                Self::GREATER_OR_EQUALS,
                Self::LESSER,
                Self::LESSER_OR_EQUALS,
                Self::ADD,
                Self::SUB,
                Self::MUL,
                Self::DIV,
                Self::MOD,
                Self::COUNT,
                Self::SUM,
                Self::MAX,
                Self::MIN,
                Self::WHEN,
                Self::HOLDS,
                Self::ENABLED,
                Self::VIOLATED,
            ]
        }

        /// Returns a list of all the logic operators in eFLINT.
        ///
        /// # Returns
        /// A static slice with all logic operators.
        pub const fn logical() -> &'static [&'static str] { &[Self::AND, Self::OR, Self::NOT] }

        /// Returns a list of all the comparison operators in eFLINT.
        ///
        /// # Returns
        /// A static slice with all comparison operators.
        pub const fn comparison() -> &'static [&'static str] {
            &[Self::EQUALS, Self::NOT_EQUALS, Self::GREATER, Self::GREATER_OR_EQUALS, Self::LESSER, Self::LESSER_OR_EQUALS]
        }

        /// Returns a list of all the arithmetic operators in eFLINT.
        ///
        /// # Returns
        /// A static slice with all arithmetic operators.
        pub const fn arithmetic() -> &'static [&'static str] { &[Self::ADD, Self::SUB, Self::MUL, Self::DIV, Self::MOD] }

        /// Returns a list of all the iterator operators in eFLINT.
        ///
        /// # Returns
        /// A static slice with all iterator operators.
        pub const fn iterator() -> &'static [&'static str] { &[Self::COUNT, Self::SUM, Self::MAX, Self::MIN] }

        /// Returns a list of all the miscellaneous operators in eFLINT.
        ///
        /// # Returns
        /// A static slice with all miscellaneous operators.
        pub const fn miscellaneous() -> &'static [&'static str] { &[Self::WHEN, Self::HOLDS, Self::ENABLED, Self::VIOLATED] }

        /// Returns the expression kind (boolean or instance) to which the given operator evaluates.
        ///
        /// # Arguments
        /// - `op`: The eFLINT operator to return the expression kind for.
        ///
        /// # Returns
        /// An [`auxillary::ExpressionKind`](ExpressionKind) what denotes which of the two kinds it is.
        ///
        /// # Panics
        /// This function panics if the given string is not one of the eFLINT operators.
        #[inline]
        #[track_caller]
        pub fn kind(op: &str) -> ExpressionKind {
            match op {
                Self::AND => ExpressionKind::Boolean,
                Self::OR => ExpressionKind::Boolean,
                Self::NOT => ExpressionKind::Boolean,
                Self::EQUALS => ExpressionKind::Boolean,
                Self::NOT_EQUALS => ExpressionKind::Boolean,
                Self::GREATER => ExpressionKind::Boolean,
                Self::GREATER_OR_EQUALS => ExpressionKind::Boolean,
                Self::LESSER => ExpressionKind::Boolean,
                Self::LESSER_OR_EQUALS => ExpressionKind::Boolean,
                Self::ADD => ExpressionKind::Instance,
                Self::SUB => ExpressionKind::Instance,
                Self::MUL => ExpressionKind::Instance,
                Self::DIV => ExpressionKind::Instance,
                Self::MOD => ExpressionKind::Instance,
                Self::COUNT => ExpressionKind::Instance,
                Self::SUM => ExpressionKind::Instance,
                Self::MAX => ExpressionKind::Instance,
                Self::MIN => ExpressionKind::Instance,
                Self::WHEN => ExpressionKind::Instance,
                Self::HOLDS => ExpressionKind::Boolean,
                Self::ENABLED => ExpressionKind::Boolean,
                Self::VIOLATED => ExpressionKind::Boolean,
                _ => panic!("Cannot get expression kind for unknown eFLINT operator '{op}'"),
            }
        }

        /// Returns the number of operators required by the given eFLINT operator.
        ///
        /// # Arguments
        /// - `op`: The eFLINT operator to return the number of operators for.
        ///
        /// # Returns
        /// The number of operators.
        ///
        /// # Panics
        /// This function panics if the given string is not one of the eFLINT operators.
        #[inline]
        #[track_caller]
        pub fn n_operators(op: &str) -> usize {
            match op {
                Self::AND => 2,
                Self::OR => 2,
                Self::NOT => 1,
                Self::EQUALS => 2,
                Self::NOT_EQUALS => 2,
                Self::GREATER => 2,
                Self::GREATER_OR_EQUALS => 2,
                Self::LESSER => 2,
                Self::LESSER_OR_EQUALS => 2,
                Self::ADD => 2,
                Self::SUB => 2,
                Self::MUL => 2,
                Self::DIV => 2,
                Self::MOD => 2,
                Self::COUNT => 1,
                Self::SUM => 1,
                Self::MAX => 1,
                Self::MIN => 1,
                Self::WHEN => 2,
                Self::HOLDS => 1,
                Self::ENABLED => 1,
                Self::VIOLATED => 1,
                _ => panic!("Cannot get number of operators for unknown eFLINT operator '{op}'"),
            }
        }
    }

    /// Defines identifiers for eFLINT operators that can (only) be used in [iterator expressions](super::Expression::Iterator).
    ///
    /// Note that these are only Foreach, Forall and Exists. Other operators -like Count and Sum- do not quantify, but rather take a Foreach to do the quantification for them.
    ///
    /// For non-iterator operators, see [`EFlintOperator`].
    #[derive(Clone, Copy, Debug)]
    pub struct EFlintIteratorOperator;
    impl EFlintIteratorOperator {
        /// Takes an instance pattern and checks if at least one of those generated is true.
        pub const EXISTS: &str = "EXISTS";
        /// Takes an instance pattern and checks if all of those generated are true.
        pub const FORALL: &str = "FORALL";
        /// Foreach generates an instance expression based on the given instance pattern.
        pub const FOREACH: &str = "FOREACH";

        /// Returns a list of all the iterator operators in eFLINT.
        ///
        /// # Returns
        /// A static slice with all iterator operators.
        pub const fn all() -> &'static [&'static str] { &[Self::FOREACH, Self::EXISTS, Self::FORALL] }

        pub fn kind(op: &str) -> ExpressionKind {
            match op {
                Self::FOREACH => ExpressionKind::Instance,
                Self::EXISTS => ExpressionKind::Boolean,
                Self::FORALL => ExpressionKind::Boolean,
                _ => panic!("Cannot get expression kind for unknown eFLINT iterator operator '{op}'"),
            }
        }
    }
}