raise (TypeCheckerFailure (lazy "Parameters number < left parameters number"))
;;
-let debrujin_constructor uri number_of_types =
- let rec aux k =
+let debrujin_constructor ?(cb=fun _ _ -> ()) uri number_of_types =
+ let rec aux k t =
let module C = Cic in
- function
+ let res =
+ match t with
C.Rel n as t when n <= k -> t
| C.Rel _ ->
raise (TypeCheckerFailure (lazy "unbound variable found in constructor type"))
fl
in
C.CoFix (i, liftedfl)
+ in
+ cb t res;
+ res
in
aux 0
;;