Experimental localization of errors during refinement and disambiguation.

diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml
index 0f4dc67db6b9fafc977d414b3f7e85f5a79b729e..d46f9a1bfbefd5b059623adabfa65dbab046cfbd 100644 (file)
--- a/helm/matita/matitaDisambiguator.ml
+++ b/helm/matita/matitaDisambiguator.ml
@@ -28,7 +28,8 @@ open Printf
 open MatitaTypes
 
 exception Ambiguous_input
-exception DisambiguationError of string Lazy.t list list
+exception DisambiguationError of
+ (Token.flocation option * string Lazy.t) list list
 
 type choose_uris_callback =
   id:string -> UriManager.uri list -> UriManager.uri list

diff --git a/helm/matita/matitaDisambiguator.mli b/helm/matita/matitaDisambiguator.mli
index 7e207e12fd7970f742daed95357c959d784dbb5e..64cd5563b1d691d6035b54c03f03607f35b976fb 100644 (file)
--- a/helm/matita/matitaDisambiguator.mli
+++ b/helm/matita/matitaDisambiguator.mli
@@ -28,7 +28,8 @@ open MatitaTypes
 (** raised when ambiguous input is found but not expected (e.g. in the batch
   * compiler) *)
 exception Ambiguous_input
-exception DisambiguationError of string Lazy.t list list
+exception DisambiguationError of
+ (Token.flocation option * string Lazy.t) list list
 
 type choose_uris_callback = id:string -> UriManager.uri list -> UriManager.uri list
 type choose_interp_callback = (string * string) list list -> int list

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index b62dd23deabd9ecd24375cb0ced9153fed7c6510..72b252140b3a9400383f718fdd3dccfb2dabeefa 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -253,7 +253,7 @@ let disambiguate_tactic status goal tactic =
               with
               | Cic.MutInd (uri, tyno, _) ->
                   (GrafiteAst.Type (uri, tyno) :: types)
-              | _ -> raise (MatitaDisambiguator.DisambiguationError [[lazy "Decompose works only on inductive types"]]))
+              | _ -> raise (MatitaDisambiguator.DisambiguationError [[None,lazy "Decompose works only on inductive types"]]))
         in
         let types = List.fold_left disambiguate [] types in
         GrafiteAst.Decompose (loc, types, what, names)

diff --git a/helm/matita/matitaExcPp.ml b/helm/matita/matitaExcPp.ml
index 2d0f60c9e6e4ec7fc749a99aee76e661918606d7..38951713eab19127332836aa3d6f84aed11b2205 100644 (file)
--- a/helm/matita/matitaExcPp.ml
+++ b/helm/matita/matitaExcPp.ml
@@ -69,10 +69,22 @@ let rec to_string =
           aux (n+1) tl ^
            "***** Errors obtained during phase " ^ string_of_int n ^": *****\n"^
             String.concat "\n\n"
-             (List.map (fun msg -> "*Error: " ^ Lazy.force msg) phase) ^
-            "\n\n\n"
+             (List.map (fun (floc,msg) ->
+               let loc_descr =
+                match floc with
+                   None -> ""
+                 | Some floc ->
+                    let (x, y) = HExtlib.loc_of_floc floc in
+                     sprintf " at %d-%d" x y
+               in
+                "*Error" ^ loc_descr ^ ": " ^ Lazy.force msg) phase) ^
+            "\n\n\n" in
+     let loc =
+      match errorll with
+         ((Some _ as loc,_)::_)::_ -> loc
+       | _ -> None
      in
-      None,
+      loc,
        "********** DISAMBIGUATION ERRORS: **********\n" ^
         aux 1 errorll
   | exn -> None, "Uncaught exception: " ^ Printexc.to_string exn

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 41025ee3a84e4e427827092331466365cee4c7d9..ce26f935131f418f26963c4e8121ba7948a74e15 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -28,7 +28,8 @@ open Printf
 open DisambiguateTypes
 open UriManager
 
-exception NoWellTypedInterpretation of string Lazy.t list
+exception NoWellTypedInterpretation of
+ (Token.flocation option * string Lazy.t) list
 exception PathNotWellFormed
 
   (** raised when an environment is not enough informative to decide *)
@@ -55,40 +56,56 @@ let descr_of_domain_item = function
 
 type 'a test_result =
   | Ok of 'a * Cic.metasenv
-  | Ko of string Lazy.t
-  | Uncertain of string Lazy.t
+  | Ko of Token.flocation option * string Lazy.t
+  | Uncertain of Token.flocation option * string Lazy.t
 
-let refine_term metasenv context uri term ugraph =
+let refine_term metasenv context uri term ugraph ~localization_tbl =
 (*   if benchmark then incr actual_refinements; *)
   assert (uri=None);
     debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term)));
     try
       let term', _, metasenv',ugraph1 = 
-       CicRefine.type_of_aux' metasenv context term ugraph in
+       CicRefine.type_of_aux' metasenv context term ugraph ~localization_tbl in
        (Ok (term', metasenv')),ugraph1
     with
-      | CicRefine.Uncertain msg ->
-          debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ;
-          Uncertain (msg (*lazy ("Uncertain trying to refine: " ^ CicMetaSubst.ppterm_in_context [] term context ^ "\n" ^ Lazy.force msg)*)),ugraph
-      | CicRefine.RefineFailure msg ->
-          debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
-            (CicPp.ppterm term) (Lazy.force msg)));
-          Ko (msg (*lazy ("Error trying to refine: " ^ CicMetaSubst.ppterm_in_context [] term context ^ "\n" ^ Lazy.force msg)*)),ugraph
+     exn ->
+      let rec process_exn loc =
+       function
+          HExtlib.Localized (loc,exn) -> process_exn (Some loc) exn
+        | CicRefine.Uncertain msg ->
+            debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ;
+            Uncertain (loc,msg),ugraph
+        | CicRefine.RefineFailure msg ->
+            debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
+              (CicPp.ppterm term) (Lazy.force msg)));
+            Ko (loc,msg),ugraph
+       | exn -> raise exn
+      in
+       process_exn None exn
 
-let refine_obj metasenv context uri obj ugraph =
+let refine_obj metasenv context uri obj ugraph ~localization_tbl =
  assert (context = []);
    debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppobj obj))) ;
    try
-     let obj', metasenv,ugraph = CicRefine.typecheck metasenv uri obj in
+     let obj', metasenv,ugraph =
+      CicRefine.typecheck metasenv uri obj ~localization_tbl
+     in
        (Ok (obj', metasenv)),ugraph
    with
-     | CicRefine.Uncertain msg ->
-         debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppobj obj)) ;
-         Uncertain (msg (*lazy ("Uncertain trying to refine: " ^ CicPp.ppobj obj ^ "\n" ^ Lazy.force msg)*)),ugraph
-     | CicRefine.RefineFailure msg ->
-         debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
-           (CicPp.ppobj obj) (Lazy.force msg))) ;
-         Ko (msg (*lazy ("Error trying to refine: " ^ CicPp.ppobj obj ^ "\n" ^ Lazy.force msg)*)),ugraph
+     exn ->
+      let rec process_exn loc =
+       function
+          HExtlib.Localized (loc,exn) -> process_exn (Some loc) exn
+        | CicRefine.Uncertain msg ->
+            debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppobj obj)) ;
+            Uncertain (loc,msg),ugraph
+        | CicRefine.RefineFailure msg ->
+            debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
+              (CicPp.ppobj obj) (Lazy.force msg))) ;
+            Ko (loc,msg),ugraph
+       | exn -> raise exn
+      in
+       process_exn None exn
 
 let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () =
   try
@@ -106,11 +123,15 @@ let find_in_context name (context: Cic.name list) =
   in
   aux 1 context
 
-let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast =
+let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast
+     ~localization_tbl
+=
   assert (uri = None);
   let rec aux loc (context: Cic.name list) = function
     | CicNotationPt.AttributedTerm (`Loc loc, term) ->
-        aux loc context term
+        let res = aux loc context term in
+         Cic.CicHash.add localization_tbl res loc;
+         res
     | CicNotationPt.AttributedTerm (_, term) -> aux loc context term
     | CicNotationPt.Appl (CicNotationPt.Symbol (symb, i) :: args) ->
         let cic_args = List.map (aux loc context) args in
@@ -352,16 +373,19 @@ let interpretate_term ~(context: Cic.name list) ~env ~uri ~is_path ast =
     | None -> Cic.Implicit annotation
     | Some term -> aux loc context term
   in
-  match ast with
-  | CicNotationPt.AttributedTerm (`Loc loc, term) -> aux loc context term
-  | term -> aux dummy_floc context term
+   aux dummy_floc context ast
 
 let interpretate_path ~context path =
- interpretate_term ~context ~env:Environment.empty ~uri:None ~is_path:true path
+ let localization_tbl = Cic.CicHash.create 23 in
+  (* here we are throwing away useful localization informations!!! *)
+  fst (
+   interpretate_term ~context ~env:Environment.empty ~uri:None ~is_path:true
+    path ~localization_tbl, localization_tbl)
 
-let interpretate_obj ~context ~env ~uri ~is_path obj =
+let interpretate_obj ~context ~env ~uri ~is_path obj ~localization_tbl =
  assert (context = []);
  assert (is_path = false);
+ let interpretate_term = interpretate_term ~localization_tbl in
  match obj with
   | CicNotationPt.Inductive (params,tyl) ->
      let uri = match uri with Some uri -> uri | None -> assert false in
@@ -808,17 +832,20 @@ let refine_profiler = HExtlib.profile "disambiguate_thing.refine_thing"
             aliases todo_dom 
         in
         try
+          let localization_tbl = Cic.CicHash.create 503 in
           let cic_thing =
             interpretate_thing ~context:disambiguate_context ~env:filled_env
-             ~uri ~is_path:false thing
+             ~uri ~is_path:false thing ~localization_tbl
           in
 let foo () =
-          let k,ugraph1 = refine_thing metasenv context uri cic_thing ugraph in
+          let k,ugraph1 =
+           refine_thing metasenv context uri cic_thing ugraph ~localization_tbl
+          in
             (k , ugraph1 )
 in refine_profiler.HExtlib.profile foo ()
         with
-        | Try_again msg -> Uncertain msg, ugraph
-        | Invalid_choice msg -> Ko msg, ugraph
+        | Try_again msg -> Uncertain (None,msg), ugraph
+        | Invalid_choice msg -> Ko (None,msg), ugraph
       in
       (* (4) build all possible interpretations *)
       let (@@) (l1,l2) (l1',l2') = l1@l1', l2@l2' in
@@ -829,7 +856,7 @@ in refine_profiler.HExtlib.profile foo ()
             (match test_env aliases [] base_univ with
             | Ok (thing, metasenv),new_univ -> 
                [ aliases, diff, metasenv, thing, new_univ ], []
-            | Ko msg,_ | Uncertain msg,_ -> [],[msg])
+            | Ko (loc,msg),_ | Uncertain (loc,msg),_ -> [],[loc,msg])
         | item :: remaining_dom ->
             debug_print (lazy (sprintf "CHOOSED ITEM: %s"
              (string_of_domain_item item)));
@@ -838,7 +865,8 @@ in refine_profiler.HExtlib.profile foo ()
                 None -> lookup_choices item
               | Some choices -> choices in
             match choices with
-               [] -> [], [lazy ("No choices for " ^ string_of_domain_item item)]
+               [] ->
+                [], [None,lazy ("No choices for " ^ string_of_domain_item item)]
              | [codomain_item] ->
                  (* just one choice. We perform a one-step look-up and
                     if the next set of choices is also a singleton we
@@ -865,13 +893,13 @@ in refine_profiler.HExtlib.profile foo ()
                         | _ ->
                            aux new_env new_diff lookup_in_todo_dom
                             remaining_dom new_univ)
-                    | Uncertain msg,new_univ ->
+                    | Uncertain (loc,msg),new_univ ->
                         (match remaining_dom with
-                        | [] -> [], [msg]
+                        | [] -> [], [loc,msg]
                         | _ ->
                            aux new_env new_diff lookup_in_todo_dom
                             remaining_dom new_univ)
-                    | Ko msg,_ -> [], [msg])
+                    | Ko (loc,msg),_ -> [], [loc,msg])
              | _::_ ->
                let rec filter univ = function 
                 | [] -> [],[]
@@ -886,13 +914,13 @@ in refine_profiler.HExtlib.profile foo ()
                         | _ -> aux new_env new_diff None remaining_dom new_univ
                         ) @@ 
                           filter univ tl
-                    | Uncertain msg,new_univ ->
+                    | Uncertain (loc,msg),new_univ ->
                         (match remaining_dom with
-                        | [] -> [],[msg]
+                        | [] -> [],[loc,msg]
                         | _ -> aux new_env new_diff None remaining_dom new_univ
                         ) @@ 
                           filter univ tl
-                    | Ko msg,_ -> ([],[msg]) @@ filter univ tl)
+                    | Ko (loc,msg),_ -> ([],[loc,msg]) @@ filter univ tl)
                in
                 filter base_univ choices
       in

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.mli b/helm/ocaml/cic_disambiguation/disambiguate.mli
index f0ca92db00dc69d18addf9e84d66f9adf49a04cf..fc88b6cf84d54320fb092cb9a3f67763a1585897 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.mli
+++ b/helm/ocaml/cic_disambiguation/disambiguate.mli
@@ -25,7 +25,8 @@
 
 (** {2 Disambiguation interface} *)
 
-exception NoWellTypedInterpretation of string Lazy.t list
+exception NoWellTypedInterpretation of
+ (Token.flocation option * string Lazy.t) list
 exception PathNotWellFormed
 
 val interpretate_path :

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index d3a297d43e88b517cec0e9caf4eef32e322896d9..ccf662f185967f799faacbcb4fabf914adc005db 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -43,11 +43,25 @@ in profiler.HExtlib.profile foo ()
     | (CicUnification.Uncertain msg) -> raise (Uncertain msg)
 ;;
 
-let enrich f =
- function
-    RefineFailure msg -> raise (RefineFailure (f msg))
-  | Uncertain msg -> raise (Uncertain (f msg))
-  | _ -> assert false
+let enrich loc f exn =
+ let exn' =
+  match exn with
+     RefineFailure msg -> RefineFailure (f msg)
+   | Uncertain msg -> Uncertain (f msg)
+   | _ -> assert false
+ in
+  match loc with
+     None -> raise exn'
+   | Some loc -> raise (HExtlib.Localized (loc,exn'))
+
+let relocalize localization_tbl oldt newt =
+ try
+  let infos = Cic.CicHash.find localization_tbl oldt in
+   Cic.CicHash.remove localization_tbl oldt;
+   Cic.CicHash.add localization_tbl newt infos;
+ with
+  Not_found -> ()
+;;
                        
 let rec split l n =
  match (l,n) with
@@ -56,128 +70,20 @@ let rec split l n =
   | (_,_) -> raise (AssertFailure (lazy "split: list too short"))
 ;;
 
-let exp_impl metasenv subst context term =
-  let rec aux metasenv context = function
-    | (Cic.Rel _) as t -> metasenv, t
-    | (Cic.Sort _) as t -> metasenv, t
-    | Cic.Const (uri, subst) ->
-        let metasenv', subst' = do_subst metasenv context subst in
-        metasenv', Cic.Const (uri, subst')
-    | Cic.Var (uri, subst) ->
-        let metasenv', subst' = do_subst metasenv context subst in
-        metasenv', Cic.Var (uri, subst')
-    | Cic.MutInd (uri, i, subst) ->
-        let metasenv', subst' = do_subst metasenv context subst in
-        metasenv', Cic.MutInd (uri, i, subst')
-    | Cic.MutConstruct (uri, i, j, subst) ->
-        let metasenv', subst' = do_subst metasenv context subst in
-        metasenv', Cic.MutConstruct (uri, i, j, subst')
-    | Cic.Meta (n,l) -> 
-        let metasenv', l' = do_local_context metasenv context l in
-        metasenv', Cic.Meta (n, l')
-    | Cic.Implicit (Some `Type) ->
+let exp_impl metasenv subst context =
+ function
+  | Some `Type ->
         let (metasenv', idx) = CicMkImplicit.mk_implicit_type metasenv subst context in
         let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
         metasenv', Cic.Meta (idx, irl)
-    | Cic.Implicit (Some `Closed) ->
+  | Some `Closed ->
         let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst [] in
         metasenv', Cic.Meta (idx, [])
-    | Cic.Implicit None ->
+  | None ->
         let (metasenv', idx) = CicMkImplicit.mk_implicit metasenv subst context in
         let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
         metasenv', Cic.Meta (idx, irl)
-    | Cic.Implicit _ -> assert false
-    | Cic.Cast (te, ty) ->
-        let metasenv', ty' = aux metasenv context ty in
-        let metasenv'', te' = aux metasenv' context te in
-        metasenv'', Cic.Cast (te', ty')
-    | Cic.Prod (name, s, t) ->
-        let metasenv', s' = aux metasenv context s in
-        metasenv', Cic.Prod (name, s', t)
-    | Cic.Lambda (name, s, t) ->
-        let metasenv', s' = aux metasenv context s in
-        metasenv', Cic.Lambda (name, s', t)
-    | Cic.LetIn (name, s, t) ->
-        let metasenv', s' = aux metasenv context s in
-        metasenv', Cic.LetIn (name, s', t)
-    | Cic.Appl l when List.length l > 1 ->
-        let metasenv', l' =
-          List.fold_right
-            (fun term (metasenv, terms) ->
-              let new_metasenv, term = aux metasenv context term in
-              new_metasenv, term :: terms)
-            l (metasenv, [])
-        in
-        metasenv', Cic.Appl l'
-    | Cic.Appl _ -> assert false
-    | Cic.MutCase (uri, i, outtype, term, patterns) ->
-        let metasenv', l' =
-          List.fold_right
-            (fun term (metasenv, terms) ->
-              let new_metasenv, term = aux metasenv context term in
-              new_metasenv, term :: terms)
-            (outtype :: term :: patterns) (metasenv, [])
-        in
-        let outtype', term', patterns' =
-          match l' with
-          | outtype' :: term' :: patterns' -> outtype', term', patterns'
-          | _ -> assert false
-        in
-        metasenv', Cic.MutCase (uri, i, outtype', term', patterns')
-    | Cic.Fix (i, funs) ->
-        let metasenv', types =
-          List.fold_right
-            (fun (name, _, typ, _) (metasenv, types) ->
-              let new_metasenv, new_type = aux metasenv context typ in
-              (new_metasenv, (name, new_type) :: types))
-            funs (metasenv, [])
-        in
-        let rec combine = function
-          | ((name, index, _, body) :: funs_tl),
-            ((_, typ) :: typ_tl) ->
-              (name, index, typ, body) :: combine (funs_tl, typ_tl)
-          | [], [] -> []
-          | _ -> assert false
-        in
-        let funs' = combine (funs, types) in
-        metasenv', Cic.Fix (i, funs')
-    | Cic.CoFix (i, funs) ->
-        let metasenv', types =
-          List.fold_right
-            (fun (name, typ, _) (metasenv, types) ->
-              let new_metasenv, new_type = aux metasenv context typ in
-              (new_metasenv, (name, new_type) :: types))
-            funs (metasenv, [])
-        in
-        let rec combine = function
-          | ((name, _, body) :: funs_tl),
-            ((_, typ) :: typ_tl) ->
-              (name, typ, body) :: combine (funs_tl, typ_tl)
-          | [], [] -> []
-          | _ -> assert false
-        in
-        let funs' = combine (funs, types) in
-        metasenv', Cic.CoFix (i, funs')
-  and do_subst metasenv context subst =
-    List.fold_right
-      (fun (uri, term) (metasenv, substs) ->
-        let metasenv', term' = aux metasenv context term in
-        (metasenv', (uri, term') :: substs))
-      subst (metasenv, [])
-  and do_local_context metasenv context local_context =
-    List.fold_right
-      (fun term (metasenv, local_context) ->
-        let metasenv', term' =
-          match term with
-          | None -> metasenv, None
-          | Some term ->
-              let metasenv', term' = aux metasenv context term in
-              metasenv', Some term'
-        in
-        metasenv', term' :: local_context)
-      local_context (metasenv, [])
-  in
-  aux metasenv context term
+  | _ -> assert false
 ;;
 
 let rec type_of_constant uri ugraph =
@@ -294,8 +200,9 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt
              | _ -> raise (AssertFailure (lazy "Wrong number of arguments")))
       | _ -> raise (AssertFailure (lazy "Prod or MutInd expected"))
 
-and type_of_aux' metasenv context t ugraph =
-  let metasenv, t = exp_impl metasenv [] context t in
+and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
+     ugraph
+=
   let rec type_of_aux subst metasenv context t ugraph =
     let module C = Cic in
     let module S = CicSubstitution in
@@ -358,7 +265,9 @@ and type_of_aux' metasenv context t ugraph =
               t,(C.Sort (C.Type tno')),subst,metasenv,ugraph1
         | C.Sort _ -> 
             t,C.Sort (C.Type (CicUniv.fresh())),subst,metasenv,ugraph
-        | C.Implicit _ -> raise (AssertFailure (lazy "21"))
+        | C.Implicit infos ->
+           let metasenv',t' = exp_impl metasenv subst context infos in
+            type_of_aux subst metasenv' context t' ugraph
         | C.Cast (te,ty) ->
             let ty',_,subst',metasenv',ugraph1 =
               type_of_aux subst metasenv context ty ugraph 
@@ -416,7 +325,6 @@ and type_of_aux' metasenv context t ugraph =
               s' sort1 subst' context metasenv' ugraph1
             in
             let context_for_t = ((Some (name,(C.Decl s')))::context) in
-            let metasenv',t = exp_impl metasenv' subst' context_for_t t in
             let t',sort2,subst'',metasenv'',ugraph2 =
               type_of_aux subst' metasenv' 
                 context_for_t t ugraph1
@@ -452,7 +360,6 @@ and type_of_aux' metasenv context t ugraph =
                       "Not well-typed lambda-abstraction: the source %s should be a type; instead it is a term of type %s" (CicPp.ppterm s) (CicPp.ppterm sort1))))
             in
             let context_for_t = ((Some (n,(C.Decl s')))::context) in 
-            let metasenv',t = exp_impl metasenv' subst' context_for_t t in
             let t',type2,subst'',metasenv'',ugraph2 =
               type_of_aux subst' metasenv' context_for_t t ugraph1
             in
@@ -464,7 +371,6 @@ and type_of_aux' metasenv context t ugraph =
               type_of_aux subst metasenv context s ugraph
             in
            let context_for_t = ((Some (n,(C.Def (s',Some ty))))::context) in
-            let metasenv',t = exp_impl metasenv' subst' context_for_t t in
            
             let t',inferredty,subst'',metasenv'',ugraph2 =
               type_of_aux subst' metasenv' 
@@ -486,20 +392,13 @@ and type_of_aux' metasenv context t ugraph =
                    let x',ty,subst',metasenv',ugraph1 =
                      type_of_aux subst metasenv context x ugraph
                    in
-                     (x', ty)::res,subst',metasenv',ugraph1
+                    relocalize localization_tbl x x';
+                    (x', ty)::res,subst',metasenv',ugraph1
                 ) tl ([],subst',metasenv',ugraph1)
             in
             let tl',applty,subst''',metasenv''',ugraph3 =
-             try
               eat_prods true subst'' metasenv'' context 
                 hetype tlbody_and_type ugraph2
-             with
-              exn ->
-               enrich
-                (fun msg ->
-                  lazy ("The application " ^
-                   CicMetaSubst.ppterm_in_context subst'' t context ^
-                  " is not well typed:\n" ^ Lazy.force msg)) exn
             in
               C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3
         | C.Appl _ -> raise (RefineFailure (lazy "Appl: no arguments"))
@@ -819,7 +718,6 @@ and type_of_aux' metasenv context t ugraph =
             let fl_bo',subst,metasenv,ugraph2 =
               List.fold_left
                 (fun (fl,subst,metasenv,ugraph) ((name,x,_,bo),ty) ->
-                   let metasenv, bo = exp_impl metasenv subst context' bo in
                    let bo',ty_of_bo,subst,metasenv,ugraph1 =
                      type_of_aux subst metasenv context' bo ugraph
                    in
@@ -861,7 +759,6 @@ and type_of_aux' metasenv context t ugraph =
             let fl_bo',subst,metasenv,ugraph2 =
               List.fold_left
                 (fun (fl,subst,metasenv,ugraph) ((name,_,bo),ty) ->
-                   let metasenv, bo = exp_impl metasenv subst context' bo in
                    let bo',ty_of_bo,subst,metasenv,ugraph1 =
                      type_of_aux subst metasenv context' bo ugraph
                    in
@@ -1125,7 +1022,9 @@ and type_of_aux' metasenv context t ugraph =
                             CicMetaSubst.ppterm_in_context subst s context
                              (* "\nReason: " ^ Lazy.force e*))
                           in
-                           enrich msg exn
+                           enrich 
+                            (try Some (Cic.CicHash.find localization_tbl hete) with Not_found -> prerr_endline ("!!! NOT LOCALIZED: " ^ CicPp.ppterm hete); None)
+                            msg exn
                        | CoercGraph.NotMetaClosed -> 
                            raise (Uncertain (lazy "Coercions on meta"))
                        | CoercGraph.SomeCoercion c -> 
@@ -1192,9 +1091,9 @@ and type_of_aux' metasenv context t ugraph =
     (cleaned_t,cleaned_ty,cleaned_metasenv,ugraph1) 
 ;;
 
-let type_of_aux' metasenv context term ugraph =
+let type_of_aux' ?localization_tbl metasenv context term ugraph =
   try 
-    type_of_aux' metasenv context term ugraph
+    type_of_aux' ?localization_tbl metasenv context term ugraph
   with 
     CicUniv.UniverseInconsistency msg -> raise (RefineFailure (lazy msg))
 
@@ -1273,25 +1172,31 @@ let are_all_occurrences_positive metasenv ugraph uri tys leftno =
   in
   metasenv,ugraph,substituted_tys
     
-let typecheck metasenv uri obj =
+let typecheck metasenv uri obj ~localization_tbl =
  let ugraph = CicUniv.empty_ugraph in
  match obj with
     Cic.Constant (name,Some bo,ty,args,attrs) ->
-     let bo',boty,metasenv,ugraph = type_of_aux' metasenv [] bo ugraph in
-     let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph 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 bo' = CicMetaSubst.apply_subst subst bo' in
      let ty' = CicMetaSubst.apply_subst subst ty' in
      let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
       Cic.Constant (name,Some bo',ty',args,attrs),metasenv,ugraph
   | Cic.Constant (name,None,ty,args,attrs) ->
-     let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
+     let ty',_,metasenv,ugraph =
+      type_of_aux' ~localization_tbl metasenv [] ty ugraph
+     in
       Cic.Constant (name,None,ty',args,attrs),metasenv,ugraph
   | Cic.CurrentProof (name,metasenv',bo,ty,args,attrs) ->
      assert (metasenv' = metasenv);
      (* Here we do not check the metasenv for correctness *)
-     let bo',boty,metasenv,ugraph = type_of_aux' metasenv [] bo ugraph in
-     let ty',sort,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
+     let bo',boty,metasenv,ugraph =
+      type_of_aux' ~localization_tbl metasenv [] bo ugraph in
+     let ty',sort,metasenv,ugraph =
+      type_of_aux' ~localization_tbl metasenv [] ty ugraph in
      begin
       match sort with
          Cic.Sort _
@@ -1316,7 +1221,9 @@ let typecheck metasenv uri obj =
      let metasenv,ugraph,tys =
       List.fold_right
        (fun (name,b,ty,cl) (metasenv,ugraph,res) ->
-         let ty',_,metasenv,ugraph = type_of_aux' metasenv [] ty ugraph in
+         let ty',_,metasenv,ugraph =
+          type_of_aux' ~localization_tbl metasenv [] ty ugraph
+         in
           metasenv,ugraph,(name,b,ty',cl)::res
        ) tys (metasenv,ugraph,[]) in
      let con_context =
@@ -1330,7 +1237,7 @@ let typecheck metasenv uri obj =
            (fun (name,ty) (metasenv,ugraph,res) ->
              let ty = CicTypeChecker.debrujin_constructor uri typesno ty in
              let ty',_,metasenv,ugraph =
-              type_of_aux' metasenv con_context ty ugraph in
+              type_of_aux' ~localization_tbl metasenv con_context ty ugraph in
              let ty' = undebrujin uri typesno tys ty' in
               metasenv,ugraph,(name,ty')::res
            ) cl (metasenv,ugraph,[])
@@ -1364,8 +1271,9 @@ let type_of_aux' metasenv context term =
 
 let profiler2 = HExtlib.profile "CicRefine"
 
-let type_of_aux' metasenv context term ugraph =
- profiler2.HExtlib.profile (type_of_aux' metasenv context term) ugraph
+let type_of_aux' ?localization_tbl metasenv context term ugraph =
+ profiler2.HExtlib.profile
+  (type_of_aux' ?localization_tbl metasenv context term) ugraph
 
-let typecheck metasenv uri obj =
- profiler2.HExtlib.profile (typecheck metasenv uri) obj
+let typecheck ~localization_tbl metasenv uri obj =
+ profiler2.HExtlib.profile (typecheck ~localization_tbl metasenv uri) obj

diff --git a/helm/ocaml/cic_unification/cicRefine.mli b/helm/ocaml/cic_unification/cicRefine.mli
index ef089cabf1a433023d01749a884b7808ef3018e4..97417f7f673612163e2bc718264a023792557ea7 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.mli
+++ b/helm/ocaml/cic_unification/cicRefine.mli
@@ -31,13 +31,15 @@ exception AssertFailure of string Lazy.t;;
 (* refines [term] and returns the refined form of [term],  *)
 (* its type, the new metasenv and universe graph.          *)
 val type_of_aux':
- Cic.metasenv -> Cic.context -> Cic.term -> CicUniv.universe_graph ->
-  Cic.term * Cic.term * Cic.metasenv * CicUniv.universe_graph
+ ?localization_tbl:Token.flocation Cic.CicHash.t ->
+  Cic.metasenv -> Cic.context -> Cic.term -> CicUniv.universe_graph ->
+   Cic.term * Cic.term * Cic.metasenv * CicUniv.universe_graph
 
 (* typecheck metasenv uri obj graph                     *)
 (* refines [obj] and returns the refined form of [obj], *)
 (* the new metasenv and universe graph.                 *)
 (* the [uri] is required only for inductive definitions *)
 val typecheck : 
- Cic.metasenv -> UriManager.uri option -> Cic.obj ->
-  Cic.obj * Cic.metasenv * CicUniv.universe_graph
+ localization_tbl:Token.flocation Cic.CicHash.t ->
+  Cic.metasenv -> UriManager.uri option -> Cic.obj ->
+   Cic.obj * Cic.metasenv * CicUniv.universe_graph