Struct TypeInferenceSystem 

pub struct TypeInferenceSystem;

A bidirectional type inference system for STLC. Implements the “Check” and “Synth” modes of bidirectional typing.

Implementations

impl TypeInferenceSystem

pub fn new() -> Self

Create a new type inference system.

pub fn synthesize(&self, ctx: &Context, term: &Term) -> Option<SimpleType>

Synthesis mode: try to infer the type of term in context ctx. Returns Some(ty) if successful.

pub fn check(&self, ctx: &Context, term: &Term, ty: &SimpleType) -> bool

Checking mode: verify that term has type ty in context ctx.

pub fn infer_with_annotation( &self, ctx: &Context, term: &Term, hint: Option<&SimpleType>, ) -> Option<SimpleType>

Attempt to reconstruct the type of an annotated term. A term is “annotated” if it is an application with a synthesizable function.

Trait Implementations

impl Default for TypeInferenceSystem

fn default() -> Self

Returns the “default value” for a type.