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 program expression against a given type and effect
check_idxtm	check index term against a given sort
check_nmtm	check name term against a given sort
check_val	check value against a value type
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
term_of_idxtm	Depending on the sort, construct either a name term or index term from the given index term derivation. (The `subst` module uses this "term family" distinction to guide how it searches for free variables in terms.)

CtxRec
DeclDer	Module declaration typing derivation
ExpDer
IdxTmDer
NmTmDer
ValDer