according to camlp5 sources, the dummy loc should be 0,0 and not -1,-1

[helm.git] / helm / software / components / cic_disambiguation / disambiguate.ml

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))