Module fungi_lang::bitype
[−]
[src]
Bidirectional type system.
Structs
Der |
Typing derivation: A context ( |
DerVis |
Information for visualizing derivation trees in HFI |
ItemDer |
Module item derivation; wraps a |
ModuleDer |
Module typing derivation |
UseAllModuleDer |
Module import typing derivation |
Enums
Ctx |
Typing context |
DeclClas |
Classifier for declared object in a module |
DeclRule |
Module declaration typing rule |
Dir |
Bidirectional direction: Synthesis vs Checking |
ExpRule |
Expression typing rule |
IdxTmRule |
Index term sorting rule |
ItemRule |
Module item typing rule; each |
NmTmRule |
Name term sorting rule |
PrimAppRule |
Primitive application typing rule |
Qual |
Qualifiers for module item names |
Term |
Type terms; each can be defined by a module declaration, and carried (by identifier name) in the typing context, and used (by identifier name) to construct terms used in typing derivations. |
TypeError |
Typing error |
ValRule |
Value typing rule |
Traits
HasClas |
Functions
check_exp |
Check a type and effect against a program expression |
check_idxtm |
check sort against index term |
check_nmtm |
check sort against name term |
check_val |
check sort against value term |
normal_type |
Normalize types (expand definitions and reduce applications). |
synth_exp |
Synthesize a type and effect for a program expression |
synth_idxtm |
synthesize sort for index term |
synth_items |
Synthesize typing derivations for a list of declarations (e.g., from a module) |
synth_module |
Synthesize a typing derivation for a module, given the module AST. |
synth_nmtm |
synthesize sort for name term |
synth_val |
synthesize sort for value term |
unroll_type |
Unroll a |
Type Definitions
CtxRec | |
DeclDer |
Module declaration typing derivation |
ExpDer | |
IdxTmDer | |
NmTmDer | |
ValDer |