1. useless code (undebrujin) removed from disambiguate.ml

2. debrujin now takes a callback used for localization during refinemente :-|
3. localization of inductive types fixed

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index f1d53de52f217171b267800774ceea9959f0293d..2ab3b37060cd66829a9696e4206b099a20687ae3 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -445,15 +445,6 @@ let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl =
           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) ->
@@ -464,7 +455,7 @@ let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl =
              let ty' =
               add_params (interpretate_term context con_env None false ty)
              in
-              name,undebrujin ty'
+              name,ty'
            ) cl
          in
           name,b,ty',cl'

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
index 239bd44155dc08261221c0c13d60042db04af85a..5da471a6eb8b934a2239c9994d640925213f91f3 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml
@@ -52,10 +52,11 @@ let rec split l n =
       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"))
@@ -114,6 +115,9 @@ let debrujin_constructor uri number_of_types =
           fl
        in
         C.CoFix (i, liftedfl)
+  in
+   cb t res;
+   res
  in
   aux 0
 ;;

diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.mli b/helm/ocaml/cic_proof_checking/cicTypeChecker.mli
index 28f134e07ce925cbfd506bcd4e1d974d0d8da708..e9419171e906140ea1c9685ff56e7deba12858d9 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicTypeChecker.mli
+++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.mli
@@ -27,7 +27,14 @@
 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
 

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 20be9363bbbc385ad82d972ad51b1769635bc4b1..95e6c7ba6d213ef308592031b32e4e550666d29a 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -1331,7 +1331,9 @@ let typecheck metasenv uri obj ~localization_tbl =
          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