Struct KripkeFormatter 

pub struct KripkeFormatter;

Formatter for Kripke lowered output with explicit world arguments. Modals are already lowered to quantifiers; this formatter just renders the result with world arguments appended to predicates.

Trait Implementations

impl LogicFormatter for KripkeFormatter

fn universal(&self) -> String

fn existential(&self) -> String

fn cardinal(&self, n: u32) -> String

fn at_least(&self, n: u32) -> String

fn at_most(&self, n: u32) -> String

fn and(&self) -> &'static str

fn or(&self) -> &'static str

fn implies(&self) -> &'static str

fn iff(&self) -> &'static str

fn not(&self) -> &'static str

fn necessity(&self) -> &'static str

fn possibility(&self) -> &'static str

fn past(&self) -> &'static str

fn future(&self) -> &'static str

fn progressive(&self) -> &'static str

fn perfect(&self) -> &'static str

fn habitual(&self) -> &'static str

fn iterative(&self) -> &'static str

fn passive(&self) -> &'static str

fn lambda(&self, var: &str, body: &str) -> String

fn counterfactual(&self, antecedent: &str, consequent: &str) -> String

fn superlative(&self, comp: &str, domain: &str, subject: &str) -> String

fn categorical_all(&self) -> &'static str

fn categorical_no(&self) -> &'static str

fn categorical_some(&self) -> &'static str

fn categorical_not(&self) -> &'static str

fn modal(&self, _domain: ModalDomain, _force: f32, body: &str) -> String

fn use_full_names(&self) -> bool

fn include_world_arguments(&self) -> bool

fn quantifier(&self, kind: &QuantifierKind, var: &str, body: &str) -> String

fn binary_op(&self, op: &TokenType, left: &str, right: &str) -> String

fn unary_op(&self, op: &TokenType, operand: &str) -> String

fn identity(&self) -> &'static str

fn wrap_identity(&self) -> bool

fn temporal(&self, op: &TemporalOperator, body: &str) -> String

fn temporal_binary( &self, op: &BinaryTemporalOp, left: &str, right: &str, ) -> String

fn aspectual(&self, op: &AspectOperator, body: &str) -> String

fn voice(&self, op: &VoiceOperator, body: &str) -> String

fn event_quantifier(&self, pred: &str, adverbs: &[String]) -> String

fn sanitize(&self, s: &str) -> String

fn use_simple_events(&self) -> bool

fn preserve_case(&self) -> bool

fn write_comparative<W>( &self, w: &mut W, adjective: &str, subject: &str, object: &str, difference: Option<&str>, ) -> Result<(), Error>

where W: Write,

Hook for customizing how comparatives are rendered. Default implementation uses standard logic notation: tallER(subj, obj) or tallER(subj, obj, diff)

fn write_predicate<W>( &self, w: &mut W, name: &str, args: &[Term<'_>], registry: &mut SymbolRegistry, interner: &Interner, ) -> Result<(), Error>

where W: Write,

Hook for customizing how predicates are rendered. Default implementation uses standard logic notation: Name(Arg1, Arg2)