Class Make.base

inherit Gen.base
inherit span_helper
method private catch_exn : (Hax_engine.Prelude.string -> PPrint.document) -> (Hax_engine.Prelude.unit -> PPrint.document) -> PPrint.document
method private catch_exn' : (Hax_engine.Diagnostics.Context.t -> Hax_engine.Diagnostics.kind -> PPrint.document) -> (Hax_engine.Prelude.unit -> PPrint.document) -> PPrint.document

Printer settings

method virtual printer_name : Hax_engine.Prelude.string

Mark a path as unreachable

val concrete_ident_view : (module Hax_engine.Concrete_ident.VIEW_API)

The concrete ident view to be used

Utility functions

method assertion_failure : 'any. Hax_engine.Prelude.string -> 'any

An assertion failed

method unreachable : 'any. Hax_engine.Prelude.unit -> 'any

Mark a path as unreachable

method local_ident : Hax_engine.Ast.local_ident -> PPrint.document

Printers for special types

method concrete_ident : local:Hax_engine.Prelude.bool -> Hax_engine.Concrete_ident.view -> PPrint.document

concrete_ident ~local id prints a name without path if local is true, otherwise it prints the full path, separated by `module_path_separator`.

method quote : contents: Hax_engine__Ast.Make(F).quote_content Hax_engine__Generated_generic_printer_base.LazyDoc.lazy_doc Hax_engine.Prelude.list -> witness:F.quote -> PPrint.document
method quote_content_Verbatim : Hax_engine.Prelude.string -> PPrint.document
method quote_content_Expr : Hax_engine__Ast.Make(F).expr Hax_engine__Generated_generic_printer_base.LazyDoc.lazy_doc -> PPrint.document
method quote_content_Pattern : Hax_engine__Ast.Make(F).pat Hax_engine__Generated_generic_printer_base.LazyDoc.lazy_doc -> PPrint.document
method quote_content_Typ : {ty}34 Hax_engine__Generated_generic_printer_base.LazyDoc.lazy_doc -> PPrint.document

Specialized printers for expr

method virtual expr'_App_constant : super:{expr}47 -> constant:Hax_engine.Ast.concrete_ident LazyDoc.lazy_doc -> generics:{generic_value}35 LazyDoc.lazy_doc Hax_engine.Prelude.list -> PPrint.document

expr'_App_constant ~super ~constant ~generics prints the constant e with generics generics. super is the unspecialized expr.

method virtual expr'_App_application : super:{expr}47 -> f:{expr}47 LazyDoc.lazy_doc -> args:{expr}47 LazyDoc.lazy_doc Hax_engine.Prelude.list -> generics:{generic_value}35 LazyDoc.lazy_doc Hax_engine.Prelude.list -> PPrint.document

expr'_App_application ~super ~f ~args ~generics prints the function application e<...generics>(...args). super is the unspecialized expr.

method virtual expr'_App_tuple_projection : super:{expr}47 -> size:Hax_engine.Prelude.int -> nth:Hax_engine.Prelude.int -> e:{expr}47 LazyDoc.lazy_doc -> PPrint.document

expr'_App_tuple_projection ~super ~size ~nth ~e prints the projection of the nth component of the tuple e of size size. super is the unspecialized expr.

method virtual expr'_App_field_projection : super:{expr}47 -> field:Hax_engine.Ast.concrete_ident LazyDoc.lazy_doc -> e:{expr}47 LazyDoc.lazy_doc -> PPrint.document

expr'_App_field_projection ~super ~field ~e prints the projection of the field field in the expression e. super is the unspecialized expr.

method virtual expr'_Construct_inductive : super:{expr}47 -> constructor:Hax_engine.Ast.concrete_ident LazyDoc.lazy_doc -> is_record:Hax_engine.Prelude.bool -> is_struct:Hax_engine.Prelude.bool -> fields: (Hax_engine.Ast.global_ident LazyDoc.lazy_doc * {expr}47 LazyDoc.lazy_doc) Hax_engine.Prelude.list -> base: ({expr}47 LazyDoc.lazy_doc * F.construct_base) LazyDoc.lazy_doc Hax_engine.Prelude.option -> PPrint.document

expr'_Construct_inductive ~super ~is_record ~is_struct ~constructor ~base ~fields prints the construction of an inductive with base base and fields fields. super is the unspecialized expr. TODO doc is_record is_struct

method virtual expr'_Construct_tuple : super:{expr}47 -> components:{expr}47 LazyDoc.lazy_doc Hax_engine.Prelude.list -> PPrint.document
method virtual expr'_GlobalVar_concrete : super:{expr}47 -> Hax_engine.Ast.concrete_ident LazyDoc.lazy_doc -> PPrint.document
method virtual expr'_GlobalVar_primitive : super:{expr}47 -> Hax_engine.Ast.primitive_ident -> PPrint.document

Specialized printers for pat

method virtual pat'_PConstruct_inductive : super:{pat}43 -> constructor:Hax_engine.Ast.concrete_ident LazyDoc.lazy_doc -> is_record:Hax_engine.Prelude.bool -> is_struct:Hax_engine.Prelude.bool -> fields: (Hax_engine.Ast.global_ident LazyDoc.lazy_doc * {pat}43 LazyDoc.lazy_doc) Hax_engine.Prelude.list -> PPrint.document
method virtual pat'_PConstruct_tuple : super:{pat}43 -> components:{pat}43 LazyDoc.lazy_doc Hax_engine.Prelude.list -> PPrint.document

Specialized printers for lhs

method virtual lhs_LhsFieldAccessor_field : e:{lhs}53 LazyDoc.lazy_doc -> typ:{ty}34 LazyDoc.lazy_doc -> field:Hax_engine.Ast.concrete_ident LazyDoc.lazy_doc -> witness:F.nontrivial_lhs -> PPrint.document
method virtual lhs_LhsFieldAccessor_tuple : e:{lhs}53 LazyDoc.lazy_doc -> typ:{ty}34 LazyDoc.lazy_doc -> nth:Hax_engine.Prelude.int -> size:Hax_engine.Prelude.int -> witness:F.nontrivial_lhs -> PPrint.document

Specialized printers for ty

method virtual ty_TApp_tuple : types:{ty}34 Hax_engine.Prelude.list -> PPrint.document

ty_TApp_tuple ~types prints a tuple type with compounds types types.

method virtual ty_TApp_application : typ: Hax_engine.Ast.concrete_ident LazyDoc.lazy_doc -> generics:{generic_value}35 LazyDoc.lazy_doc Hax_engine.Prelude.list -> PPrint.document

ty_TApp_application ~typ ~generics prints the type typ<...generics>.

Specialized printers for item

method virtual item'_Type_struct : super:{item}335 -> name:Hax_engine.Ast.concrete_ident LazyDoc.lazy_doc -> generics:{generics}332 LazyDoc.lazy_doc -> tuple_struct:Hax_engine.Prelude.bool -> arguments: (Hax_engine.Ast.concrete_ident LazyDoc.lazy_doc * {ty}34 LazyDoc.lazy_doc * Hax_engine.Ast.attr Hax_engine.Prelude.list LazyDoc.lazy_doc) Hax_engine.Prelude.list -> PPrint.document

item'_Type_struct ~super ~name ~generics ~tuple_struct ~arguments prints the struct definition struct name<generics> arguments. `tuple_struct` says whether we are dealing with a tuple struct (e.g. struct Foo(T1, T2)) or a named struct (e.g. struct Foo {field: T1, other: T2})?

method virtual item'_Type_enum : super:{item}335 -> name:Hax_engine.Ast.concrete_ident LazyDoc.lazy_doc -> generics:{generics}332 LazyDoc.lazy_doc -> variants:{variant}333 LazyDoc.lazy_doc Hax_engine.Prelude.list -> PPrint.document

item'_Type_enum ~super ~name ~generics ~variants prints the enum type enum name<generics> { ... }.

item'_Enum_Variant prints a variant of an enum.

Printers for common nodes

method virtual common_array : PPrint.document Hax_engine.Prelude.list -> PPrint.document

common_array values is a default for printing array-like nodes: array patterns, array expressions.

Default printers

*

method module_path_separator : Hax_engine.Prelude.String.t

module_path_separator is the default separator for paths. `::` by default

method pat'_PArray : super:Hax_engine__Ast.Make(F).pat -> args: Hax_engine__Ast.Make(F).pat Hax_engine__Generated_generic_printer_base.LazyDoc.lazy_doc Hax_engine.Prelude.list -> PPrint.document
method expr'_Array : super:Hax_engine__Ast.Make(F).expr -> Hax_engine__Ast.Make(F).expr Hax_engine__Generated_generic_printer_base.LazyDoc.lazy_doc Hax_engine.Prelude.list -> PPrint.document
method pat'_POr : super:Hax_engine__Ast.Make(F).pat -> subpats: Hax_engine__Ast.Make(F).pat Hax_engine__Generated_generic_printer_base.LazyDoc.lazy_doc Hax_engine.Prelude.list -> PPrint.document