Struct IdrisBackend 

pub struct IdrisBackend {
    pub add_header: bool,
    pub default_total: bool,
    pub auto_implicit: bool,
    pub options: IdrisBackendOptions,
}

The Idris 2 code generation backend.

Converts IdrisModule / individual declarations into .idr source text.

Fields

add_header: bool

Whether to add -- AUTO-GENERATED header.

default_total: bool

Whether to emit %default total at the top of each module.

auto_implicit: bool

Whether to emit %auto_implicit pragmas.

options: IdrisBackendOptions

Configuration options.

Implementations

impl IdrisBackend

pub fn new() -> Self

Create a backend with default settings.

pub fn proof_mode() -> Self

Create a backend optimised for proof-oriented Idris 2 output.

pub fn emit_module(&self, module: &IdrisModule) -> String

Emit a complete IdrisModule as .idr source text.

pub fn emit_decl(&self, decl: &IdrisDecl) -> String

Emit a single declaration.

pub fn emit_function(&self, func: &IdrisFunction) -> String

Emit a single function.

pub fn emit_data(&self, data: &IdrisData) -> String

Emit a single data declaration.

pub fn emit_record(&self, rec: &IdrisRecord) -> String

Emit a single record.

pub fn emit_interface(&self, iface: &IdrisInterface) -> String

Emit a single interface.

pub fn emit_impl(&self, im: &IdrisImpl) -> String

Emit a single implementation.

Trait Implementations

impl Debug for IdrisBackend

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for IdrisBackend

fn default() -> IdrisBackend

Returns the “default value” for a type.