| C.Rel m when m <= k || m > nn+k -> ()
| C.Rel m ->
(try match List.nth context (m-1-k) with
- | _,C.Def (bo,_) -> aux (n-m) () bo
+ | _,C.Def (bo,_) -> aux 0 () (S.lift status (m-k) bo)
| _ -> ()
with Failure _ -> assert false)
| C.Meta (_,(_,(C.Irl 0 | C.Ctx []))) -> (* closed meta *) ()
match List.nth context (n - 1) with
| (_,C.Decl ty) -> S.lift status n ty
| (_,C.Def (_,ty)) -> S.lift status n ty
- with Failure _ ->
+ with Failure _ | Invalid_argument _ ->
raise (TypeCheckerFailure (lazy ("unbound variable " ^ string_of_int n
^" under: " ^ status#ppcontext ~metasenv ~subst context))))
| C.Sort s ->
if R.are_convertible status ~metasenv ~subst context ty_arg s then
aux (S.subst status ~avoid_beta_redexes:true arg t) tl
else
+ let indent s = " " ^ (Str.global_replace (Str.regexp "\n") "\n " s) in
raise
(TypeCheckerFailure
(lazy (Printf.sprintf
- ("Appl: wrong application of %s: the argument %s has type"^^
+ ("Appl: wrong application of\n%s\nThe argument\n%s\nhas type"^^
"\n%s\nbut it should have type \n%s\nContext:\n%s\n")
- (status#ppterm ~subst ~metasenv ~context he)
- (status#ppterm ~subst ~metasenv ~context arg)
- (status#ppterm ~subst ~metasenv ~context ty_arg)
- (status#ppterm ~subst ~metasenv ~context s)
+ (indent (status#ppterm ~subst ~metasenv ~context he))
+ (indent (status#ppterm ~subst ~metasenv ~context arg))
+ (indent (status#ppterm ~subst ~metasenv ~context ty_arg))
+ (indent (status#ppterm ~subst ~metasenv ~context s))
(status#ppcontext ~subst ~metasenv context))))
| _ ->
raise
| C.Sort C.Prop ->
false::(aux context new_ty tl)
| C.Sort _
- | C.Meta _ -> true::(aux context new_ty tl)
+ | C.Meta _ -> true::(aux context new_ty tl)
| _ -> raise (TypeCheckerFailure (lazy (Printf.sprintf
"Prod: the type %s of the source of %s is not a sort"
(status#ppterm ~subst ~metasenv ~context sort)
(guarded_by_constructors status ~subst ~metasenv types bo r_uri r_len len)
then
raise (TypeCheckerFailure
- (lazy "CoFix: not guarded by constructors"))
+ (lazy ("CoFix: not guarded by constructors: " ^ status#ppobj (uri,height,metasenv,subst,kind))))
) fl dfl
;;