Skip to content

9-add-a-basic-type-checker

belazy requested to merge 9-add-a-basic-type-checker into main

This merge request implements a basic type-checker for Proost.

Here's a short description of the implementation:

  • add normal_form()and whnf(), which respectively allow you to get the normal form and weak-head normal form of a term.
  • Implement an untyped conversion checker. It checks whether two given terms are convertible (read, definitionally equal).
  • Implement a type-checker based on bidirectional type-checking : the checker checks the type of lambda-abstractions, and infers the types of every other term in a bidirectional manner (read, mutually recursive).

/!\ This merge request only implements type-checking of terms in an empty environment (as in, it doesn't make use of other definitions in the environment), though it won't be too hard to add the feature at a later date.

This merge requests needs an extensive review, as well as many more tests. I am planning on making more tests in my spare-time.

Closes #9 (closed)

Edited by belazy

Merge request reports