one more lazy/loc

[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 9d42899c6895fffeeb3366f210c7dd6a3fbbe2f4..47e9c182189efb83e9b8be3518ed448dff80553f 100644 (file)
--- a/helm/software/components/cic_disambiguation/disambiguate.ml
+++ b/helm/software/components/cic_disambiguation/disambiguate.ml
@@ -232,13 +232,13 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
                  raise (Try_again (lazy "The type of the term to be matched
                   is still unknown"))
               | _ ->
-                raise (Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!")))
+                raise (Invalid_choice (lazy (loc,"The type of the term to be matched is not (co)inductive!"))))
           | None ->
               let rec fst_constructor =
                 function
                    (Ast.Pattern (head, _, _), _) :: _ -> head
                  | (Ast.Wildcard, _) :: tl -> fst_constructor tl
-                 | [] -> raise (Invalid_choice (Some loc, lazy "The type of the term to be matched cannot be determined because it is an inductive type without constructors or because all patterns use wildcards"))
+                 | [] -> raise (Invalid_choice (lazy (loc,"The type of the term to be matched cannot be determined because it is an inductive type without constructors or because all patterns use wildcards")))
               in
               (match resolve env (Id (fst_constructor branches)) () with
               | Cic.MutConstruct (indtype_uri, indtype_no, _, _) ->
@@ -247,7 +247,7 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
                  raise (Try_again (lazy "The type of the term to be matched
                   is still unknown"))
               | _ ->
-                raise (Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!")))
+                raise (Invalid_choice (lazy (loc,"The type of the term to be matched is not (co)inductive!"))))
         in
         let branches =
          if create_dummy_ids then
@@ -255,7 +255,7 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
            (function
                Ast.Wildcard,term -> ("wildcard",None,[]), term
              | Ast.Pattern _,_ ->
-                raise (Invalid_choice (Some loc, lazy "Syntax error: the left hand side of a branch patterns must be \"_\""))
+                raise (Invalid_choice (lazy (loc, "Syntax error: the left hand side of a branch patterns must be \"_\"")))
            ) branches
          else
          match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph indtype_uri) with
@@ -278,17 +278,15 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
                        [] ->
                         if unrecognized != [] then
                          raise (Invalid_choice
-                          (Some loc,
-                           lazy
+                          (lazy (loc,
                             ("Unrecognized constructors: " ^
-                             String.concat " " unrecognized)))
+                             String.concat " " unrecognized))))
                         else if useless > 0 then
                          raise (Invalid_choice
-                          (Some loc,
-                           lazy
+                           (lazy (loc,
                             ("The last " ^ string_of_int useless ^
                              "case" ^ if useless > 1 then "s are" else " is" ^
-                             " unused")))
+                             " unused"))))
                         else
                          []
                      | (Ast.Wildcard,_)::tl when not unused ->
@@ -304,7 +302,7 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
                        [] ->
                         raise
                          (Invalid_choice
-                          (Some loc, lazy ("Missing case: " ^ name)))
+                          (lazy (loc, ("Missing case: " ^ name))))
                      | ((Ast.Wildcard, _) as branch :: _) as branches ->
                          branch, branches
                      | (Ast.Pattern (name',_,_),_) as branch :: tl
@@ -322,8 +320,8 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
                         else
                          raise
                           (Invalid_choice
-                           (Some loc,
-                             lazy ("Wrong number of arguments for " ^ name)))
+                            (lazy (loc,"Wrong number of arguments for " ^
+                            name)))
                      | Ast.Wildcard,term ->
                         let rec mk_lambdas =
                          function
@@ -482,7 +480,7 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
                     (try
                       List.assoc s ids_to_uris, aux ~localize loc context term
                      with Not_found ->
-                       raise (Invalid_choice (Some loc, lazy "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on"))))
+                       raise (Invalid_choice (lazy (loc, "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on")))))
                   subst
             | None -> List.map (fun uri -> uri, Cic.Implicit None) uris)
           in
@@ -526,10 +524,10 @@ let interpretate_term ?(create_dummy_ids=false) ~context ~env ~uri ~is_path ast
 *)
                 t
             | _ ->
-              raise (Invalid_choice (Some loc, lazy "??? Can this happen?"))
+              raise (Invalid_choice (lazy (loc, "??? Can this happen?")))
            with 
              CicEnvironment.CircularDependency _ -> 
-               raise (Invalid_choice (None, lazy "Circular dependency in the environment"))))
+               raise (Invalid_choice (lazy (loc,"Circular dependency in the environment")))))
     | CicNotationPt.Implicit -> Cic.Implicit None
     | CicNotationPt.UserInput -> Cic.Implicit (Some `Hole)
     | CicNotationPt.Num (num, i) -> resolve env (Num i) ~num ()
@@ -1147,8 +1145,7 @@ let foo () =
 in refine_profiler.HExtlib.profile foo ()
         with
         | 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))
+        | Invalid_choice loc_msg -> Ko loc_msg
       in
       (* (4) build all possible interpretations *)
       let (@@) (l1,l2,l3) (l1',l2',l3') = l1@l1', l2@l2', l3@l3' in