(fun (metasenv,last,coerc) ->
let pp t =
CicMetaSubst.ppterm_in_context ~metasenv subst t context in
- let subst,metasenv,ugraph =
- fo_unif_subst subst context metasenv last he ugraph in
- debug_print (lazy ("New head: "^ pp coerc));
try
+ let subst,metasenv,ugraph =
+ fo_unif_subst subst context metasenv last he ugraph in
+ debug_print (lazy ("New head: "^ pp coerc));
let tty,ugraph =
- CicTypeChecker.type_of_aux' ~subst metasenv context coerc ugraph in
- debug_print (lazy (" has type: "^ pp tty));
- Some (coerc,tty,subst,metasenv,ugraph)
+ CicTypeChecker.type_of_aux' ~subst metasenv context coerc
+ ugraph
+ in
+ debug_print (lazy (" has type: "^ pp tty));
+ Some (coerc,tty,subst,metasenv,ugraph)
with
| Uncertain _ | RefineFailure _
| HExtlib.Localized (_,Uncertain _)
let ugraph = CicUniv.empty_ugraph in
match obj with
Cic.Constant (name,Some bo,ty,args,attrs) ->
+ (* CSC: ugly code. Here I need to retrieve in advance the loc of bo
+ since type_of_aux' destroys localization information (which are
+ preserved by type_of_aux *)
+ let loc exn' =
+ try
+ Cic.CicHash.find localization_tbl bo
+ with Not_found ->
+ HLog.debug ("!!! NOT LOCALIZED: " ^ CicPp.ppterm bo);
+ raise exn' in
let bo',boty,metasenv,ugraph =
type_of_aux' ~localization_tbl metasenv [] bo ugraph in
let ty',_,metasenv,ugraph =
type_of_aux' ~localization_tbl metasenv [] ty ugraph in
- let subst,metasenv,ugraph = fo_unif_subst [] [] metasenv boty ty' ugraph in
+ let subst,metasenv,ugraph =
+ try
+ fo_unif_subst [] [] metasenv boty ty' ugraph
+ with
+ RefineFailure _
+ | Uncertain _ as exn ->
+ let msg =
+ lazy ("The term " ^
+ CicMetaSubst.ppterm_in_context ~metasenv [] bo' [] ^
+ " has type " ^
+ CicMetaSubst.ppterm_in_context ~metasenv [] boty [] ^
+ " but is here used with type " ^
+ CicMetaSubst.ppterm_in_context ~metasenv [] ty' [])
+ in
+ let exn' =
+ match exn with
+ RefineFailure _ -> RefineFailure msg
+ | Uncertain _ -> Uncertain msg
+ | _ -> assert false
+ in
+ raise (HExtlib.Localized (loc exn',exn'))
+ in
let bo' = CicMetaSubst.apply_subst subst bo' in
let ty' = CicMetaSubst.apply_subst subst ty' in
let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in