Struct ExplicitMonadic 

pub struct ExplicitMonadic;

Monadic Phase

This module defines a phase that makes the monadic encoding explicit by introducing calls to hax primitives (pure and lift) when necessary.

Details

In backends with a monadic encoding (Lean for instance), rust computations that can crash are wrapped in an error Monad (say RustM): a function fn f(x:u32) -> u32 will be extracted to something like def f (x:u32) : RustM u32. There are two challenges in this encoding :

1. Some expressions cannot panic (literals, consts, constructors for enums, etc) and should be wrapped in the monad¹. This phase inserts explicit calls to pure to that aim.

2. Language constructs (if-then-else, match, etc.) and rust functions still expect rust values as input, not monadic ones. This phase inserts explicit calls to lift to materialize the sub-expressions that return a monadic result where a value is expected. The Lean backend turns them into explicit lifts (← ..), which implicitly introduces a monadic bind

This phase expects all function and closure bodies to be monadic computations by default.

---

1. While implicit coercions can sometime be enough, they can also badly interact with inference, typically when dealing with branches (like if-then-else) where some branches are pure and some are not. ↩

Trait Implementations

impl Debug for ExplicitMonadic

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

Formats the value using the given formatter.

impl Default for ExplicitMonadic

fn default() -> ExplicitMonadic

Returns the “default value” for a type.

impl Phase for ExplicitMonadic

fn apply(&self, items: &mut Vec<Item>)

Apply the phase on items. A phase may transform an item into zero, one or more items.