Struct LeanPrinter 

pub struct LeanPrinter { /* private fields */ }

The Lean printer

Implementations

impl LeanPrinter

pub fn is_hax_core_models_extraction_mode(&self) -> bool

Checks if we are extracting core models to be able to use different namespeacing when referring to core.

pub fn render_id(&self, id: &GlobalId) -> String

Render a global id using the Rendering strategy of the Lean printer. Works for both concrete and projector ids. TODO: https://github.com/cryspen/hax/issues/1660

pub fn render_last(&self, id: &GlobalId) -> String

Renders the last, most local part of an id. Used for named arguments of constructors.

pub fn render_with_injection(&self, id: &GlobalId, injection: &String) -> String

Inject an identifier in before-last position while rendering TODO: use DefIdInner::kind for this instead (https://github.com/cryspen/hax/issues/1877)

impl LeanPrinter

pub fn arguments<A: 'static + Clone, D>( &self, fields: &[(GlobalId, D)], is_record: &bool, ) -> DocBuilder<A>

where D: ToDocument<Self, A>,

Prints arguments a variant or constructor of struct, using named or unamed arguments based on the is_record flag. Used for both expressions and patterns

Trait Implementations

impl Clone for LeanPrinter

fn clone(&self) -> LeanPrinter

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Default for LeanPrinter

fn default() -> LeanPrinter

Returns the “default value” for a type.

impl HasContextualSpan for LeanPrinter

fn span(&self) -> Option<Span>

Returns the span currently associated with the printer, if any.

fn with_span(&self, span: Span) -> Self

Clone the printer, adding a span hint. Useful for errors.

impl HasLinkedItemGraph for LeanPrinter

fn linked_item_graph(&self) -> &LinkedItemGraph

Get a reference of the LinkedItemGraph.

fn with_linked_item_graph(self, graph: Rc<LinkedItemGraph>) -> Self

Set a LinkedItemGraph.

impl<A: 'static + Clone> PrettyAst<A> for LeanPrinter

fn todo_document(&self, message: &str, issue_id: Option<u32>) -> DocBuilder<A>

Produce a non-panicking placeholder document. In general, prefer the use of the helper macro [todo_document!].

const NAME: &'static str = "Lean"

A name for this instance of PrettyAst. Useful for diagnostics and debugging.

fn module(&self, module: &Module) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn global_id(&self, global_id: &GlobalId) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn generics(&self, generics: &Generics) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn generic_constraint(&self, _: &GenericConstraint) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn generic_param(&self, generic_param: &GenericParam) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn generic_value(&self, generic_value: &GenericValue) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn expr(&self, _: &Expr) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn arm(&self, arm: &Arm) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn pat(&self, pat: &Pat) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn ty(&self, ty: &Ty) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn literal(&self, literal: &Literal) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn local_id(&self, local_id: &LocalId) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn spanned_ty(&self, spanned_ty: &SpannedTy) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn primitive_ty(&self, primitive_ty: &PrimitiveTy) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn int_kind(&self, int_kind: &IntKind) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn float_kind(&self, float_kind: &FloatKind) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn quote_content(&self, quote_content: &QuoteContent) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn quote(&self, quote: &Quote) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn param(&self, param: &Param) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn item(&self, item: &Item) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn impl_item(&self, _: &ImplItem) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn impl_ident(&self, _: &ImplIdent) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn trait_goal(&self, _: &TraitGoal) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn variant(&self, _: &Variant) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn symbol(&self, symbol: &Symbol) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn metadata(&self, _: &Metadata) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn lhs(&self, _lhs: &Lhs) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn safety_kind(&self, _safety_kind: &SafetyKind) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn binding_mode(&self, _binding_mode: &BindingMode) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn region(&self, _region: &Region) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn dyn_trait_goal(&self, _dyn_trait_goal: &DynTraitGoal) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn attribute(&self, _: &Attribute) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn borrow_kind(&self, _borrow_kind: &BorrowKind) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn guard(&self, _guard: &Guard) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn projection_predicate( &self, projection_predicate: &ProjectionPredicate, ) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn error_node(&self, _error_node: &ErrorNode) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn impl_expr(&self, _impl_expr: &ImplExpr) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn emit_diagnostic(&self, kind: Kind)

Emit a diagnostic with proper context and span.

fn unimplemented_method( &self, method: &str, ast: FragmentRef<'_>, ) -> DocBuilder<A>

Produce a structured error document for an unimplemented method.

fn trait_item(&self, trait_item: &TraitItem) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn generic_param_kind( &self, generic_param_kind: &GenericParamKind, ) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn item_kind(&self, item_kind: &ItemKind) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn resugared_expr_kind( &self, resugared_expr_kind: &ResugaredExprKind, ) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn resugared_ty_kind( &self, resugared_ty_kind: &ResugaredTyKind, ) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn resugared_pat_kind( &self, resugared_pat_kind: &ResugaredPatKind, ) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn resugared_impl_item_kind( &self, resugared_impl_item_kind: &ResugaredImplItemKind, ) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn resugared_trait_item_kind( &self, resugared_trait_item_kind: &ResugaredTraitItemKind, ) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

fn resugared_item_kind( &self, resugared_item_kind: &ResugaredItemKind, ) -> DocBuilder<A>

👎Deprecated:

Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

Define how the printer formats a value of this AST type. Do not call this method directly. Use ToDocument::to_document instead, so annotations/spans are preserved correctly.

impl Printer for LeanPrinter

const NAME: &'static str = _

The name of the printer

impl RenderView for LeanPrinter

fn reserved_keywords() -> &'static HashSet<String>

List of reserved keywords that will be escaped when rendering

fn should_escape(id: &str) -> bool

Check if a string needs escaping

fn separator(&self) -> &str

Returns the string used to join rendered atoms (defaults to "::").

fn relativize_module_path<'a>( &self, module_path: &'a [PathSegment], ) -> &'a [PathSegment]

Allows backends to adjust a module path before rendering, e.g., to shorten it according to currenly open namespaces.

fn render_path_segment(&self, chunk: &PathSegment) -> Vec<String>

Renders a single PathSegment into a vector of display atoms.

fn is_reserved_keyword(id: &str) -> bool

Check if a string is a reserved keyword that needs escaping

fn escape(id: &str) -> String

Escape a string if it needs escaping according to Self::should_escape

fn render_unnamed_path_segment_payload( &self, unnamed: UnnamedPathSegmentPayload, ) -> Symbol

Converts an unnamed path segment payload into a printable Symbol.

fn render_path_segment_payload(&self, payload: PathSegmentPayload) -> Symbol

Converts a full PathSegmentPayload (named or unnamed) into a printable Symbol.

fn render_suffix(&self, suffix: &ReservedSuffix) -> String

Renders the optional suffix

fn module(&self, view: &View) -> Vec<String>

Renders just the module path (crate + modules) of a View, as a list of atoms.

fn render(&self, view: &View) -> Rendered

Renders a View into a structured Rendered value, splitting output into module and path parts.

fn rendered_to_strings( &self, rendered: Rendered, ) -> impl Iterator<Item = String>

Lazy render a view as an iterator of strings.

fn rendered_to_string(&self, rendered: Rendered) -> String

Joins the atoms contained in a Rendered into a single string using separator.

fn render_string(&self, view: &View) -> String

Convenience: renders a View straight to a single String.

fn render_strings(&self, view: &View) -> impl Iterator<Item = String>

Convenience: renders a View straight to a iterator of Strings.

impl<A: 'static + Clone> ToDocument<LeanPrinter, A> for Vec<Param>

Render parameters, adding a line after each parameter

fn to_document(&self, printer: &LeanPrinter) -> DocBuilder<A>

Produce a document using the provided printer reference.

impl<A: 'static + Clone> ToDocument<LeanPrinter, A> for (Vec<GenericParam>, &TraitItem)

fn to_document(&self, printer: &LeanPrinter) -> DocBuilder<A>

Produce a document using the provided printer reference.