Module fungi_lang::bitype
[−]
[src]
Bidirectional type system.
Modules
debug |
Stringification for debugging derivation rules |
Structs
Der |
Typing derivation: A context ( |
DerVis |
Information for visualizing derivation trees in HFI |
Ext |
"Extra" typing information carried by the typing judgements |
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 |
find_defs_for_idxtm_var | |
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 |
Type Definitions
CtxRec | |
DeclDer |
Module declaration typing derivation |
ExpDer | |
IdxTmDer | |
NmTmDer | |
ValDer |