loc * lazy string -> (loc * string) lazy

diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml
index 45186669d09d482f7a55ebf5da9a73ed7ac1b0b8..9d42899c6895fffeeb3366f210c7dd6a3fbbe2f4 100644 (file)
--- a/helm/software/components/cic_disambiguation/disambiguate.ml
+++ b/helm/software/components/cic_disambiguation/disambiguate.ml
@@ -37,7 +37,7 @@ exception NoWellTypedInterpretation of
  int *
  ((Stdpp.location list * string * string) list *
   (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
-  Stdpp.location option * string Lazy.t * bool) list
+  (Stdpp.location * string) Lazy.t * bool) list
 exception PathNotWellFormed
 
   (** raised when an environment is not enough informative to decide *)
@@ -105,8 +105,8 @@ let descr_of_domain_item = function
 
 type ('term,'metasenv,'subst,'graph) test_result =
   | Ok of 'term * 'metasenv * 'subst * 'graph
-  | Ko of Stdpp.location option * string Lazy.t
-  | Uncertain of Stdpp.location option * string Lazy.t
+  | Ko of (Stdpp.location * string) Lazy.t
+  | Uncertain of (Stdpp.location * string) Lazy.t
 
 let refine_term metasenv subst context uri term ugraph ~localization_tbl =
 (*   if benchmark then incr actual_refinements; *)
@@ -120,17 +120,17 @@ let refine_term metasenv subst context uri term ugraph ~localization_tbl =
      exn ->
       let rec process_exn loc =
        function
-          HExtlib.Localized (loc,exn) -> process_exn (Some loc) exn
+          HExtlib.Localized (loc,exn) -> process_exn loc exn
         | CicRefine.Uncertain msg ->
             debug_print (lazy ("UNCERTAIN!!! [" ^ (Lazy.force msg) ^ "] " ^ CicPp.ppterm term)) ;
-            Uncertain (loc,msg)
+            Uncertain (lazy (loc,Lazy.force msg))
         | CicRefine.RefineFailure msg ->
             debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
               (CicPp.ppterm term) (Lazy.force msg)));
-            Ko (loc,msg)
+            Ko (lazy (loc,Lazy.force msg))
        | exn -> raise exn
       in
-       process_exn None exn
+       process_exn Stdpp.dummy_loc exn
 
 let refine_obj metasenv subst context uri obj ugraph ~localization_tbl =
    assert (context = []);
@@ -146,18 +146,18 @@ let refine_obj metasenv subst context uri obj ugraph ~localization_tbl =
      exn ->
       let rec process_exn loc =
        function
-          HExtlib.Localized (loc,exn) -> process_exn (Some loc) exn
+          HExtlib.Localized (loc,exn) -> process_exn loc exn
         | CicRefine.Uncertain msg ->
             debug_print (lazy ("UNCERTAIN!!! [" ^ 
               (Lazy.force msg) ^ "] " ^ CicPp.ppobj obj)) ;
-            Uncertain (loc,msg)
+            Uncertain (lazy (loc,Lazy.force msg))
         | CicRefine.RefineFailure msg ->
             debug_print (lazy (sprintf "PRUNED!!!\nterm%s\nmessage:%s"
               (CicPp.ppobj obj) (Lazy.force msg))) ;
-            Ko (loc,msg)
+            Ko (lazy (loc,Lazy.force msg))
        | exn -> raise exn
       in
-       process_exn None exn
+       process_exn Stdpp.dummy_loc exn
 
 let resolve (env: codomain_item Environment.t) (item: domain_item) ?(num = "") ?(args = []) () =
   try
@@ -1146,8 +1146,9 @@ let foo () =
             k
 in refine_profiler.HExtlib.profile foo ()
         with
-        | Try_again msg -> Uncertain (None,msg)
-        | Invalid_choice (loc,msg) -> Ko (loc,msg)
+        | Try_again msg -> Uncertain (lazy (Stdpp.dummy_loc,Lazy.force msg))
+        | Invalid_choice (None,msg) -> Ko(lazy (Stdpp.dummy_loc,Lazy.force msg))
+        | Invalid_choice (Some loc,msg) -> Ko (lazy (loc,Lazy.force msg))
       in
       (* (4) build all possible interpretations *)
       let (@@) (l1,l2,l3) (l1',l2',l3') = l1@l1', l2@l2', l3@l3' in
@@ -1161,9 +1162,9 @@ in refine_profiler.HExtlib.profile foo ()
             (match test_env aliases rem_dom base_univ with
             | Ok (thing, metasenv,subst,new_univ) -> 
                [ aliases, diff, metasenv, subst, thing, new_univ ], [], []
-            | Ko (loc,msg) -> [],[],[aliases,diff,loc,msg,true]
-            | Uncertain (loc,msg) ->
-               [],[aliases,diff,loc,msg],[])
+            | Ko loc_msg -> [],[],[aliases,diff,loc_msg,true]
+            | Uncertain loc_msg ->
+               [],[aliases,diff,loc_msg],[])
         | Node (locs,item,inner_dom) :: remaining_dom ->
             debug_print (lazy (sprintf "CHOOSED ITEM: %s"
              (string_of_domain_item item)));
@@ -1174,8 +1175,9 @@ in refine_profiler.HExtlib.profile foo ()
             match choices with
                [] ->
                 [], [],
-                 [aliases, diff, Some (List.hd locs),
-                  lazy ("No choices for " ^ string_of_domain_item item),
+                 [aliases, diff, 
+                  (lazy (List.hd locs,
+                    "No choices for " ^ string_of_domain_item item)),
                   true]
 (*
              | [codomain_item] ->
@@ -1215,8 +1217,8 @@ in refine_profiler.HExtlib.profile foo ()
              | _::_ ->
                  let mark_not_significant failures =
                    List.map
-                    (fun (env, diff, loc, msg, _b) ->
-                      env, diff, loc, msg, false)
+                    (fun (env, diff, loc_msg, _b) ->
+                      env, diff, loc_msg, false)
                     failures in
                  let classify_errors ((ok_l,uncertain_l,error_l) as outcome) =
                   if ok_l <> [] || uncertain_l <> [] then
@@ -1245,18 +1247,18 @@ in refine_profiler.HExtlib.profile foo ()
                           ) 
                         in
                          res @@ filter tl
-                    | Uncertain (loc,msg) ->
+                    | Uncertain loc_msg ->
                         let res =
                           (match inner_dom with
-                          | [] -> [],[new_env,new_diff,loc,msg],[]
+                          | [] -> [],[new_env,new_diff,loc_msg],[]
                           | _ ->
                              aux new_env new_diff None inner_dom
                               (remaining_dom@rem_dom) 
                           )
                         in
                          res @@ filter tl
-                    | Ko (loc,msg) ->
-                        let res = [],[],[new_env,new_diff,loc,msg,true] in
+                    | Ko loc_msg ->
+                        let res = [],[],[new_env,new_diff,loc_msg,true] in
                          res @@ filter tl)
                in
                 let ok_l,uncertain_l,error_l =
@@ -1269,7 +1271,7 @@ in refine_profiler.HExtlib.profile foo ()
                    ) ok_l ([],[],error_l)
                 in
                  List.fold_right
-                  (fun (env,diff,_,_) res ->
+                  (fun (env,diff,_) res ->
                     aux env diff None remaining_dom rem_dom @@ res
                   ) uncertain_l res_after_ok_l
       in
@@ -1278,19 +1280,19 @@ in refine_profiler.HExtlib.profile foo ()
         | Ok _
         | Uncertain _ ->
            aux aliases diff lookup_in_todo_dom todo_dom [] 
-        | Ko (loc,msg) -> [],[],[aliases,diff,loc,msg,true] in
+        | Ko (loc_msg) -> [],[],[aliases,diff,loc_msg,true] in
       try
         let res =
          match aux' aliases [] None todo_dom with
          | [],uncertain,errors ->
             let errors =
              List.map
-              (fun (env,diff,loc,msg) -> (env,diff,loc,msg,true)
+              (fun (env,diff,loc_msg) -> (env,diff,loc_msg,true)
               ) uncertain @ errors
             in
             let errors =
              List.map
-              (fun (env,diff,loc,msg,significant) ->
+              (fun (env,diff,loc_msg,significant) ->
                 let env' =
                  filter_map_domain
                    (fun locs domain_item ->
@@ -1303,7 +1305,7 @@ in refine_profiler.HExtlib.profile foo ()
                       Not_found -> None)
                    thing_dom
                 in
-                 env',diff,loc,msg,significant
+                 env',diff,loc_msg,significant
               ) errors
             in
              raise (NoWellTypedInterpretation (0,errors))

diff --git a/helm/software/components/cic_disambiguation/disambiguate.mli b/helm/software/components/cic_disambiguation/disambiguate.mli
index b21c2bbe0f2480b996a44e3bef3379fc5a9c0cae..bb4c726403d8db3ee08c242e274985bf01954c19 100644 (file)
--- a/helm/software/components/cic_disambiguation/disambiguate.mli
+++ b/helm/software/components/cic_disambiguation/disambiguate.mli
@@ -37,7 +37,7 @@ exception NoWellTypedInterpretation of
  int *
  ((Stdpp.location list * string * string) list *
   (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
-  Stdpp.location option * string Lazy.t * bool) list
+  (Stdpp.location * string) Lazy.t * bool) list
 exception PathNotWellFormed
 
 val interpretate_path :
@@ -51,8 +51,8 @@ and domain_tree =
 
 type ('term,'metasenv,'subst,'graph) test_result =
   | Ok of 'term * 'metasenv * 'subst * 'graph
-  | Ko of Stdpp.location option * string Lazy.t
-  | Uncertain of Stdpp.location option * string Lazy.t
+  | Ko of (Stdpp.location * string) Lazy.t
+  | Uncertain of (Stdpp.location * string) Lazy.t
 
 exception Try_again of string Lazy.t
 

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguator.ml b/helm/software/components/grafite_parser/grafiteDisambiguator.ml
index 46b8397badfd9059d202c379a805727f7d34050e..5d803e979025596a354179395a8487eaa1e31482 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguator.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguator.ml
@@ -37,7 +37,7 @@ exception DisambiguationError of
  int *
  ((Stdpp.location list * string * string) list *
   (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
-  Stdpp.location option * string Lazy.t * bool) list list
+  (Stdpp.location * string) Lazy.t * bool) list list
   (** parameters are: option name, error message *)
 exception Unbound_identifier of string
 

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguator.mli b/helm/software/components/grafite_parser/grafiteDisambiguator.mli
index 88940c2c3818bd40cd30c5e707295ceae1e79bfb..d6ff0be4cb522c00c35ca80479b192fc7dbb8519 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguator.mli
+++ b/helm/software/components/grafite_parser/grafiteDisambiguator.mli
@@ -31,7 +31,7 @@ exception DisambiguationError of
  int *
  ((Stdpp.location list * string * string) list *
   (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
-  Stdpp.location option * string Lazy.t * bool) list list
+  (Stdpp.location * string) Lazy.t * bool) list list
   (** parameters are: option name, error message *)
 
 (** initially false; for debugging only (???) *)

diff --git a/helm/software/components/ng_disambiguation/nDisambiguate.ml b/helm/software/components/ng_disambiguation/nDisambiguate.ml
index 40ed34b5fa52af6b76d7c1ca04d799ff66065157..2aa87372467b49568f41f1f192f922b526f5b552 100644 (file)
--- a/helm/software/components/ng_disambiguation/nDisambiguate.ml
+++ b/helm/software/components/ng_disambiguation/nDisambiguate.ml
@@ -34,27 +34,27 @@ module Ast = CicNotationPt
 
 let debug_print _ = ();;
 
-let refine_term metasenv subst context uri term ugraph ~localization_tbl =
+let refine_term metasenv subst context uri term _ ~localization_tbl =
   assert (uri=None);
   debug_print (lazy (sprintf "TEST_INTERPRETATION: %s" 
     (NCicPp.ppterm ~metasenv ~subst ~context term)));
   try
     let localise t = 
-      try NCic.NCicHash.find localization_tbl t
+      try NCicUntrusted.NCicHash.find localization_tbl t
       with Not_found -> assert false
     in
-    let metasenv, subst, term, ty = 
-      NCicRefine.typeof metasenv subst context term None ~localise 
+    let metasenv, subst, term, _ = 
+      NCicRefiner.typeof metasenv subst context term None ~localise 
     in
      Disambiguate.Ok (term, metasenv, subst, ())
   with
-  | NCicRefine.Uncertain (loc, msg) ->
-      debug_print (lazy ("UNCERTAIN: [" ^ Lazy.force msg ^ "] " ^ 
+  | NCicRefiner.Uncertain (msg) ->
+      debug_print (lazy ("UNCERTAIN: [" ^ snd (Lazy.force msg) ^ "] " ^ 
         NCicPp.ppterm ~metasenv ~subst ~context term)) ;
-      Disambiguate.Uncertain (loc,msg,())
-  | NCicRefine.RefineFailure (loc,msg) ->
+      Disambiguate.Uncertain (loc,msg)
+  | NCicRefiner.RefineFailure (msg) ->
       debug_print (lazy (sprintf "PRUNED:\nterm%s\nmessage:%s"
-        (NCicPp.ppterm ~metasenv ~subst ~context term) (Lazy.force msg)));
+        (NCicPp.ppterm ~metasenv ~subst ~context term) (snd(Lazy.force msg))));
       Disambiguate.Ko (loc,msg,())
 ;;
 
@@ -458,12 +458,9 @@ let interpretate_term
 let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
      ~localization_tbl
 =
-  assert false 
-(*
   let context = List.map (function None -> NCic.Anonymous | Some (n,_) -> n) context in
   interpretate_term ~create_dummy_ids ~context ~env ~uri ~is_path ast
 ~localization_tbl
-*)
 ;;
 
 let domain_of_term ~context = 

diff --git a/helm/software/components/ng_kernel/nCicUntrusted.mli b/helm/software/components/ng_kernel/nCicUntrusted.mli
index f752c01dc9a668c23cdd0b3b715b4c68081d993a..b195760cb343d4ff97a0e8f04bed129995ea984a 100644 (file)
--- a/helm/software/components/ng_kernel/nCicUntrusted.mli
+++ b/helm/software/components/ng_kernel/nCicUntrusted.mli
@@ -17,5 +17,5 @@ val map_term_fold_a:
 
 val metas_of_term : NCic.substitution -> NCic.context -> NCic.term -> int list
 
-module NCicHash : Hashtbl.S
+module NCicHash : Hashtbl.S with type key = NCic.term
 

diff --git a/helm/software/components/ng_refiner/nCicRefiner.mli b/helm/software/components/ng_refiner/nCicRefiner.mli
index 5d845eb1fe1526d2e713df641c566498a48439be..9b10e3448cc05cbe52286639678525cc7d28e703 100644 (file)
--- a/helm/software/components/ng_refiner/nCicRefiner.mli
+++ b/helm/software/components/ng_refiner/nCicRefiner.mli
@@ -11,8 +11,8 @@
 
 (* $Id$ *)
 
-exception RefineFailure of Stdpp.location * (string Lazy.t);;
-exception Uncertain of Stdpp.location * (string Lazy.t);;
+exception RefineFailure of (Stdpp.location * string) Lazy.t;;
+exception Uncertain of (Stdpp.location * string) Lazy.t;;
 exception AssertFailure of string Lazy.t;;
 
 val typeof :

diff --git a/helm/software/matita/matitaExcPp.ml b/helm/software/matita/matitaExcPp.ml
index 076a5d763e6fccd1cb4fe0ae4055eca99399e713..17cc7c9422f8444ef3f4f2068118ac4e094a392a 100644 (file)
--- a/helm/software/matita/matitaExcPp.ml
+++ b/helm/software/matita/matitaExcPp.ml
@@ -33,8 +33,9 @@ let compact_disambiguation_errors all_passes errorll =
     (List.map
       (fun (pass,l) ->
         List.map
-         (fun (env,diff,offset,msg,significant) ->
-           offset, [[pass], [[pass], env, diff], msg, significant]) l
+         (fun (env,diff,offset_msg,significant) ->
+           let offset, msg = Lazy.force offset_msg in
+           offset, [[pass], [[pass], env, diff], lazy msg, significant]) l
       ) errorll) in
   (* Here we are doing a stable sort and list_uniq returns the latter
      "equal" element. I.e. we are showing the error corresponding to the
@@ -152,13 +153,16 @@ let rec to_string =
   | GrafiteDisambiguator.DisambiguationError (offset,errorll) ->
      let loc =
       match errorll with
-         ((_,_,Some floc,_,_)::_)::_ ->
-          let (x, y) = HExtlib.loc_of_floc floc in
-          let x = x + offset in
-          let y = y + offset in
-          let floc = HExtlib.floc_of_loc (x,y) in
-           Some floc
-       | _ -> None in
+        | ((_,_,loc_msg,_)::_)::_ ->
+          let floc, _ = Lazy.force loc_msg in
+          if floc = Stdpp.dummy_loc then None else
+            let (x, y) = HExtlib.loc_of_floc floc in
+            let x = x + offset in
+            let y = y + offset in
+            let floc = HExtlib.floc_of_loc (x,y) in
+             Some floc
+        | _ -> assert false
+     in
      let annotated_errorll =
       List.rev
        (snd
@@ -182,11 +186,10 @@ let rec to_string =
           let msg =
             (List.map (fun (passes,_,_,floc,msg,significant) ->
               let loc_descr =
-               match floc with
-                  None -> ""
-                | Some floc ->
-                   let (x, y) = HExtlib.loc_of_floc floc in
-                    sprintf " at %d-%d" (x+offset) (y+offset)
+                if floc = HExtlib.dummy_floc then "" 
+                else 
+                  let (x, y) = HExtlib.loc_of_floc floc in
+                  sprintf " at %d-%d" (x+offset) (y+offset)
               in
                "*" ^ (if not significant then "(Spurious?) " else "")
                ^ "Error" ^ loc_descr ^ ": " ^ Lazy.force msg,

diff --git a/helm/software/matita/matitaExcPp.mli b/helm/software/matita/matitaExcPp.mli
index 419b04c7332bb2ca09f16cb5bb863c07c5b46f12..77a5a3ce90d05e2c19dffc866a43ba3fd670921b 100644 (file)
--- a/helm/software/matita/matitaExcPp.mli
+++ b/helm/software/matita/matitaExcPp.mli
@@ -27,7 +27,11 @@ val compact_disambiguation_errors :
   bool ->
   (int * ((Stdpp.location list * string * string) list *
    (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
-   Stdpp.location option * string Lazy.t * bool) list) list ->
-  (Stdpp.location option * (int list * (int list * (Stdpp.location list * string * string) list * (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list) list * string Lazy.t * bool) list) list
+   (Stdpp.location * string) Lazy.t * bool) list) list ->
+  (Stdpp.location * 
+    (int list * 
+     (int list * (Stdpp.location list * string * string) list * 
+     (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list) list * 
+    string Lazy.t * bool) list) list
 
 val to_string: exn -> Stdpp.location option * string

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index 8bc226ed4a4bdbbbf33292d7afaa3a4f75c6f406..ac34052c134d5e3da486aa18c29ca8e5fde8c20e 100644 (file)
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -220,7 +220,7 @@ let rec interactive_error_interp ~all_passes
   assert (List.flatten errorll <> []);
   let errorll' =
    let remove_non_significant =
-     List.filter (fun (_env,_diff,_loc,_msg,significant) -> significant) in
+     List.filter (fun (_env,_diff,_loc_msg,significant) -> significant) in
    let annotated_errorll () =
     List.rev
      (snd
@@ -264,7 +264,7 @@ let rec interactive_error_interp ~all_passes
         let _,env,diff = List.hd envs_and_diffs in
          notify_exn
           (GrafiteDisambiguator.DisambiguationError
-            (offset,[[env,diff,loffset,msg,significant]]));
+            (offset,[[env,diff,lazy (loffset,Lazy.force msg),significant]]));
     | _::_ ->
        let dialog = new disambiguationErrors () in
        dialog#check_widgets ();
@@ -299,7 +299,7 @@ let rec interactive_error_interp ~all_passes
              ~stop:source_buffer#end_iter;
            notify_exn
             (GrafiteDisambiguator.DisambiguationError
-              (offset,[[env,diff,loffset,msg,significant]]))
+              (offset,[[env,diff,lazy(loffset,Lazy.force msg),significant]]))
            ));
        let return _ =
          dialog#disambiguationErrors#destroy ();