package wax-lib
Install
dune-project
Dependency
Authors
Maintainers
Sources
sha256=41b580846af8d41bdf6c3f005f62e38feda3e60fe2e9e4aa440db34ce515a153
sha512=4b3a181fcc7d743194a8647260870fb5190770066a197bcc48104c2b77fd40c643228b795c2bcd6b29a120820e969eb42a37a9bcec98b3f608d13f152d9f6579
doc/wax-lib.wax/Wax_lang/Infer/index.html
Module Wax_lang.InferSource
The inferred-type lattice used while type checking, the mutable cells (Cell) that carry it, and the shared printers/type aliases built on top.
Output printers wrapping Output so they take a Format.formatter directly (rather than a Wax_utils.Printer.t), for use in diagnostics.
A mutable cell carrying a value, backed by union-find: merge unifies two cells so they share one value, and get resolves a cell to that value.
type inferred_valtype = {typ : Ast.valtype;internal : Internal.valtype;anon_comptype : Ast.comptype option;(*For a synthesized reference type with no source name — a string's byte array, an inline function-type cast target — the referenced composite type, which diagnostics render inline (e.g.
*)[mut i8]) instead of the meaningless synthetic<..>name kept intyp.Noneotherwise.
}type inferred_type = | Unknown(*The genuinely polymorphic type of a value taken off the stack of unreachable or branch-terminated code. No error has been reported for it: an instruction that needs its operand's concrete type to be compiled reports one when it meets an
*)Unknownoperand.| Error(*The recovery type of a value whose own typing already failed. An error has already been reported, so
*)Errorpropagates silently — treated likeUnknownbut raising no further error.| UnknownRef(*A non-null reference of unknown heap type — the Wax counterpart of the Wasm
*)(ref bot). Produced when a reference is recovered from an otherwise-polymorphic value (null!/br_on_nullon anUnknownoperand or a barenull). Behaves likeUnknowneverywhere except thatsubtypeknows it is a reference: a subtype of every reference type but of no numeric or vector type.| Null(*A bare
*)nullliteral: a null reference whose heap type is not yet fixed. Narrowed to a concrete reference type by context; with none it takes the bottom of the relevant hierarchy.| Number(*Any numeric literal: narrows to i32, i64, f32 or f64, defaulting to i32. The bottom of the flexible-literal lattice.
*)| Int8(*A packed narrow read — a
*)load8or ani8struct/array field — which yields an i32 value tracked as 8-bit wide so a following widening cast (as i64_s/i64_u) fuses into the read. Defaults to i32.| Int16(*A packed narrow read — a
*)load16or ani16field — asInt8but 16-bit. Defaults to i32.| Int(*An integer literal committed to the integer family (e.g. by a bitwise or shift operator): narrows to i32 or i64, defaulting to i32. It can no longer become a float by inference — only an explicit
*)ascast, which emits a conversion, does that.| LargeInt(*A numeric literal too large for i32: narrows to i64, f32 or f64 (never i32), defaulting to i64. Despite the name it is float-capable and so belongs to the
*)numberfamily, notInt— it isNumberwith i32 excluded by magnitude. Lets a decompiled out-of-range constant keep its width instead of overflowing, and renders aslarge number.| Float(*A floating-point literal: narrows to f32 or f64, defaulting to f64.
*)| Valtype of inferred_valtype| Collecting of collecting(*Transient state of a fresh cell used as the result / branch-target type of a block whose result is being inferred. A value checked against it is recorded into
*)collectedrather than unified, then joined byval_lubonce the body is typed. The cell never escapes inference, so other uses treat it likeUnknown.
and collecting = {mutable collected : (Ast.location option * inferred_type Cell.t) list;(*Each value reaching the block's exit, paired with the location it was produced at (when known) so a join failure can point at the offending exits.
*)mutable exacts : (Ast.location option * inferred_type Cell.t) list;(*Snapshots of the natural types of values delivered by
*)br_if(and other pass-through branches). Such a value continues on the stack and is typed as the block result, so — unlike an ordinary exit, which need only be a subtype — its type must beexactly the result. Recorded before the delivery pins the live cell; used to decide the keep-bool (drop the annotation only if every exact matches it) and to reject an inferred block whose result would differ from an exact.declared : inferred_type Cell.t option;(*The single result type the block already carries while being inferred — a Wasm->Wax annotation under test, or
*)Nonewhen omitted.mutable needed : bool;(*Set when
*)declaredis relied upon in a way the join cannot re-derive, forcing the annotation to be kept.
}Render an inferred type into a styled printer, so it shares a diagnostic message's colour theme and width (an unresolved one prints as any). This is what the typer's Message typ combinator is built on.
Render an inferred type as plain (uncoloured) text — for the editor's hover string and the stack/debug printers. Diagnostics use output_inferred_type_styled instead.
Whether a cell resolves to Unknown, Error or UnknownRef — the common "no concrete type known" test.
The numeric value types, and shared cells holding them. A concrete base type is never re-resolved during inference, so a base-type cell's value never changes and a single shared cell per type can stand in for a fresh one.
valtype_cell v wraps a fully resolved value type in a fresh cell.