typesprobe.dl

typedef UUID = u128
typedef type_t = Free { id: UUID } | Resolved { id: UUID, params: Vec<type_t> }
input relation TypeEquality(type_a: type_t, type_b: type_t)

output relation Resolution(free_var_id: UUID, typ: type_t)

////////////////////
// direct relations/
////////////////////
Resolution(free_var_id, typ) :-
  TypeEquality(Free{free_var_id}, typ @ Resolved{_, _}).

// reverse
Resolution(free_var_id, typ) :-
  TypeEquality(typ @ Resolved{_, _}, Free{free_var_id}).


///////////////////////
// recursive relations/
///////////////////////
Resolution(head_free_id, typ) :-
  TypeEquality(Free{head_free_id}, Free{tail_free_id}),
  Resolution(tail_free_id, typ @ Resolved{_, _}).

// reverse
Resolution(tail_free_id, typ) :-
  TypeEquality(Free{head_free_id}, Free{tail_free_id}),
  Resolution(head_free_id, typ @ Resolved{_, _}).


/////////////////////////
// relating inner params/
/////////////////////////
Resolution(free_var_id, typ) :-
  TypeEquality(typ_a @ Resolved { id_a , a_types }, typ_b @ Resolved { id_b, b_types}),
  id_a == id_b, 
  var flat = FlatMap(inner_matches(typ_a, typ_b)),
  var free_var_id = flat.0,
  var typ = flat.1.

    
function inner_matches(type_a: type_t, type_b: type_t): Vec<(UUID, type_t)> {
  var res = vec_empty();
  match ((type_a, type_b)) {
    (Resolved{id_a, params_a}, Resolved{id_b, params_b}) -> {
      if (id_a != id_b) {
        return res
      };

      for (zipped in params_a.zip(params_b)) {
        var param_a = zipped.0;
        var param_b = zipped.1;

        match ((param_a, param_b)) {
          (Free{free_id}, param_b) -> {
            res.push((free_id, param_b));
          },
          (param_b, Free{free_id}) -> {
            res.push((free_id, param_a));
          },
          (Resolved{resolved_a, inner_params_a}, Resolved{resolved_b, inner_params_b}) -> {
            if (resolved_a == resolved_b) {
              for (inner_zipped in inner_params_a.zip(inner_params_b)) {
                var inner_param_a = inner_zipped.0;
                var inner_param_b = inner_zipped.1;
                for (inner_match in inner_matches(inner_param_a, inner_param_b)) {
                  res.push(inner_match);
                }
              }
            }
          }
        }
      }
    },
    _ -> ()
  };
  res
}