stt,tchou

stt's People

Contributors

Stargazers

Watchers

stt's Issues

Assertion error for a certain type

Parsing the type

type t1 = [ (X, Y) ] 
    where X = [ Int; Y* ] 
    and Y = X | `nil

type t2 = [ X; X ] 
    where X = [ t1*; Y ]
    and Y = X | [ Z*; Bool ] | `nil
    and Z = Int | X | `nil

gives the error

Fatal error: exception File "core/typ.ml", line 244, characters 2-8: Assertion failed

which is, for me, in the function

let descr n =
  assert (n.id >= 0);
  n.descr

A huuuge type

Parsing the type

type t ('a, 'b) = [ X*; Y; X ] 
    where X = 'a | (Y & Z) 
    and Y = ('a, 'b) | `nil 
    and Z = [ 'a; 'b; X* ]

generates a very huge type when applying a substitution in order to compare it to its pretty-printed type (re-parsed)
This is the function doing the variable subsitution in order to do the comparison

open Stt

let alpha_renaming (t : Typ.t)
                   (t' : Typ.t) =
    let vp, vn = Typ.vars t in
    let v = Var.Set.union vp vn in
    let var_map = Var.Set.fold (
      fun v acc -> (v.Var.name, v) :: acc
    ) v []
    in
    let vp', vn' = Typ.vars t' in
    let v' = Var.Set.union vp' vn' in
    let subst = Var.Set.fold (
      fun v acc ->
        let n_var =
          match List.assoc_opt v.Var.name var_map with
          | Some n_var -> n_var
          | None -> v
        in
        Subst.add v (Typ.var n_var) acc
    ) v' @@ Subst.of_list []
    in
    Subst.apply subst t'