Module fungi_lang::bitype
source · Expand description
Bidirectional type system.
Modules
Stringification for debugging derivation rules
Structs
Typing derivation: A context (
ctx), a direction (dir), a classifier (type, sort, etc) and a rule (rule).Information for visualizing derivation trees in HFI
“Extra” typing information carried by the typing judgements
Module item derivation; wraps a
DeclDer with additional structureModule typing derivation
Module import typing derivation
Enums
Typing context
Classifier for declared object in a module
Module declaration typing rule
Bidirectional direction: Synthesis vs Checking
Expression typing rule
Index term sorting rule
Module item typing rule; each
Decl is typed by an ItemRuleName term sorting rule
Primitive application typing rule
Qualifiers for module item names
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.
Typing error
Value typing rule
Traits
Functions
Check a program expression against a given type and effect
check index term against a given sort
check name term against a given sort
check value against a value type
Synthesize a type and effect for a program expression
synthesize sort for index term
Synthesize typing derivations for a list of declarations (e.g., from a module)
Synthesize a typing derivation for a module, given the module AST.
synthesize sort for name term
synthesize sort for value term
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.)