thealmarty

MVP unification implementation plan

The implementation of unification (inference) following this document can be split into a few smaller, separate tasks/PRs for smoother transition and easier testing.

Stage 1: Type checker enhancement

At the time of writing, the first stage of the totality checker MVP is finished. But the second and third stages, namely type checking data type and function declarations are required before unification can be implemented.

At the end of this stage, conversion/type checking for constructors is implemented.

thealmarty

onePlusOne : 1+1=2
onePlusOne = Refl

thealmarty

#include <stdio.h>

void insertion(int v[], int size) {
  // invariant: the elements of v before index i are sorted
  for(int i = 1; i < size; ++i) {
    int value = v[i];
    int j = i;
    // invariant: the elements of v between j and i are sorted and > value
    for(;j > 0 && v[j-1] > value; --j) {
      v[j] = v[j-1];

thealmarty

#include <iostream>
#include <vector>

void insertion_sort(std::vector<int> & v) {
  // invariant: the first i elements of v are sorted
  for(size_t i = 1; i < v.size(); ++i) {
    int value = v[i];
    size_t j = i-1;
    // invariant: elements of v from j+1 to i inclusive are sorted and >= value
    for(; j >= 0 && v[j] > value; --j) {