From cd8062bb6dbbc4564c4d35e3bc1557b030568902 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 9 Dec 2005 15:53:18 +0000
Subject: [PATCH] 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

---
 helm/ocaml/cic_disambiguation/disambiguate.ml    | 11 +----------
 helm/ocaml/cic_proof_checking/cicTypeChecker.ml  | 10 +++++++---
 helm/ocaml/cic_proof_checking/cicTypeChecker.mli |  9 ++++++++-
 helm/ocaml/cic_unification/cicRefine.ml          |  4 +++-
 4 files changed, 19 insertions(+), 15 deletions(-)

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index f1d53de52..2ab3b3706 100644
--- 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 239bd4415..5da471a6e 100644
--- 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 28f134e07..e9419171e 100644
--- 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 20be9363b..95e6c7ba6 100644
--- 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
-- 
2.39.2