2. debrujin now takes a callback used for localization during refinemente :-|
3. localization of inductive types fixed
i + 1,(name,name,Cic.MutInd (uri,i,[]))::res
) (0,[]) tyl) in
let con_env = DisambiguateTypes.env_of_list name_to_uris env in
i + 1,(name,name,Cic.MutInd (uri,i,[]))::res
) (0,[]) tyl) in
let con_env = DisambiguateTypes.env_of_list name_to_uris env in
- let undebrujin t =
- snd
- (List.fold_right
- (fun (name,_,_,_) (i,t) ->
- (*here the explicit_named_substituion is assumed to be of length 0 *)
- let t' = Cic.MutInd (uri,i,[]) in
- let t = CicSubstitution.subst t' t in
- i - 1,t
- ) tyl (List.length tyl - 1,t)) in
let tyl =
List.map
(fun (name,b,ty,cl) ->
let tyl =
List.map
(fun (name,b,ty,cl) ->
let ty' =
add_params (interpretate_term context con_env None false ty)
in
let ty' =
add_params (interpretate_term context con_env None false ty)
in
raise (TypeCheckerFailure (lazy "Parameters number < left parameters number"))
;;
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 res =
+ match t with
C.Rel n as t when n <= k -> t
| C.Rel _ ->
raise (TypeCheckerFailure (lazy "unbound variable found in constructor type"))
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)
fl
in
C.CoFix (i, liftedfl)
exception TypeCheckerFailure of string Lazy.t
exception AssertFailure of string Lazy.t
exception TypeCheckerFailure of string Lazy.t
exception AssertFailure of string Lazy.t
-val debrujin_constructor : UriManager.uri -> int -> Cic.term -> Cic.term
+(* this function is exported to be used also by the refiner;
+ the callback function (defaul value: ignore) is invoked on each
+ processed subterm; its first argument is the undebrujined term (the
+ input); its second argument the corresponding debrujined term (the
+ output). The callback is used to relocalize the error messages *)
+val debrujin_constructor :
+ ?cb:(Cic.term -> Cic.term -> unit) ->
+ UriManager.uri -> int -> Cic.term -> Cic.term
val typecheck : UriManager.uri -> Cic.obj * CicUniv.universe_graph
val typecheck : UriManager.uri -> Cic.obj * CicUniv.universe_graph
let metasenv,ugraph,cl' =
List.fold_right
(fun (name,ty) (metasenv,ugraph,res) ->
let metasenv,ugraph,cl' =
List.fold_right
(fun (name,ty) (metasenv,ugraph,res) ->
- let ty = CicTypeChecker.debrujin_constructor uri typesno ty in
+ let ty =
+ CicTypeChecker.debrujin_constructor
+ ~cb:(relocalize localization_tbl) uri typesno ty in
let ty',_,metasenv,ugraph =
type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
let ty' = undebrujin uri typesno tys ty' in
let ty',_,metasenv,ugraph =
type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
let ty' = undebrujin uri typesno tys ty' in