Struct EmitState 

pub struct EmitState<'p> {
    pub program: &'p Program,
    pub language: Language,
    pub ident: fn(&str) -> String,
    pub mappings: Vec<Mapping>,
    pub theorems: Vec<TheoremRecord>,
    /* private fields */
}

Fields

program: &'p Program

language: Language

ident: fn(&str) -> String

mappings: Vec<Mapping>

theorems: Vec<TheoremRecord>

Implementations

impl<'p> EmitState<'p>

pub fn new( program: &'p Program, language: Language, ident: fn(&str) -> String, reserved: &[&str], options: EmitOptions, ) -> Self

pub fn local_reserved(&self) -> BTreeSet<String>

Names a local binder may not take: a local named like a module, a top-level function or a constructor would shadow it in the target.

pub fn local_name(&self, full_name: &str) -> &str

The target name of a declaration within its module.

Panics

When full_name is not a declaration of the program.

pub fn module_path(&self, full_name: &str) -> &[String]

The target module path of a declaration.

Panics

When full_name is not a declaration of the program.

pub fn module_name(&self, source_path: &[String]) -> Option<&str>

The target name of a source module.

pub fn reference(&self, full_name: &str, separator: &str) -> String

Fully qualified reference from the top level.

pub fn ctor_local(&self, data_name: &str, ctor: &str) -> &str

The target name of a constructor within its namespace.

Panics

When the constructor is not declared.

pub fn ctor_ref(&self, data_name: &str, ctor: &str, separator: &str) -> String

Fully qualified constructor reference from the top level.

pub fn map(&mut self, entry: &Decl, target: &str)

Records where a declaration (and a data type’s constructors) went.

pub fn assume(&mut self, assumption: AssumptionText, detail: Option<&str>)

pub fn machine_integer(&mut self, ty: &Type, representation: &str)

A machine integer of a pure target: its unbounded representation, with Rust’s aborts threaded as values (output).

pub fn array_read(&mut self)

An array read: in bounds it is the element, outside it JavaScript’s undefined, which the targets do not model.

pub fn encode(&mut self, id: &str, statement: &str)

pub fn theorem( &mut self, full_name: &str, name: &str, closed_goal: bool, bounded: bool, )

Records a theorem; bounded theorems are checked by the source kernel and tested on bounded inputs in the target.

pub fn assertion_theorem(&mut self, name: &str, effect: &Effect)

pub fn assertion_theorem_with( &mut self, name: &str, effect: &Effect, discharge: Option<&str>, )

An assertion with how it is discharged, such as runtime-assertion.

pub fn assumption_list(&self) -> Vec<Assumption>

pub fn encoding_list(&self) -> Vec<Encoding>

pub fn finish(&self, text: String, entry: Option<String>) -> Emitted

The emitted result with this state’s contract.