Module fungi_lang::bitype [−] [src]

Bidirectional type system.

Modules

Stringification for debugging derivation rules

Der	Typing derivation: A context (`ctx`), a direction (`dir`), a classifier (type, sort, etc) and a rule (`rule`).
DerVis	Information for visualizing derivation trees in HFI
Ext	"Extra" typing information carried by the typing judgements
ItemDer	Module item derivation; wraps a `DeclDer` with additional structure
ModuleDer	Module typing derivation
UseAllModuleDer	Module import typing derivation

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 `Decl` is typed by an `ItemRule`
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

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

CtxRec
DeclDer	Module declaration typing derivation
ExpDer
IdxTmDer
NmTmDer
ValDer