* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
(* TODO factorize functions to frequent errors (e.g. "Unknwon mutual inductive
* ...") *)
raise (TypeCheckerFailure (lazy (List.fold_right debug_aux (t::context) "")))
;;
-let debug_print = fun _ -> () ;;
+let debug_print = fun _ -> ();;
let rec split l n =
match (l,n) with
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
;;
let b,ugraph = (CicReduction.are_convertible [] ty_te ty ugraph) in
if not b then
raise (TypeCheckerFailure
- (lazy "the type of the body is not the one expected"))
+ (lazy
+ ("the type of the body is not the one expected:\n" ^
+ CicPp.ppterm ty_te ^ "\nvs\n" ^
+ CicPp.ppterm ty)))
else
ugraph
| C.Constant (_,None,ty,_,_) ->