1. More localization: interpretation errors are now loosely localized.

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

diff --git a/components/cic_disambiguation/disambiguate.ml b/components/cic_disambiguation/disambiguate.ml
index 0b8674c0cf9804b56119107181b6779967468136..020d038ac74ff687dec0a0fd30062a9c358eef85 100644 (file)
--- a/components/cic_disambiguation/disambiguate.ml
+++ b/components/cic_disambiguation/disambiguate.ml
@@ -217,7 +217,7 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
           in
           do_branch' context args
         in
-        let (indtype_uri, indtype_no) =
+        let indtype_uri, indtype_no =
           if create_dummy_ids then
             (UriManager.uri_of_string "cic:/fake_indty.con", 0)
           else
@@ -229,12 +229,12 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
                  raise (Try_again (lazy "The type of the term to be matched
                   is still unknown"))
               | _ ->
-                raise (Invalid_choice (lazy "The type of the term to be matched is not (co)inductive!")))
+                raise (Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!")))
           | None ->
               let fst_constructor =
                 match branches with
                 | ((head, _, _), _) :: _ -> head
-                | [] -> raise (Invalid_choice (lazy "The type of the term to be matched is an inductive type without constructors that cannot be determined"))
+                | [] -> raise (Invalid_choice (Some loc, lazy "The type of the term to be matched is an inductive type without constructors that cannot be determined"))
               in
               (match resolve env (Id fst_constructor) () with
               | Cic.MutConstruct (indtype_uri, indtype_no, _, _) ->
@@ -243,7 +243,45 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
                  raise (Try_again (lazy "The type of the term to be matched
                   is still unknown"))
               | _ ->
-                raise (Invalid_choice (lazy "The type of the term to be matched is not (co)inductive!")))
+                raise (Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!")))
+        in
+        let branches =
+         match fst(CicEnvironment.get_obj CicUniv.empty_ugraph indtype_uri) with
+            Cic.InductiveDefinition (il,_,_,_) ->
+             let _,_,_,cl =
+              try
+               List.nth il indtype_no
+              with _ -> assert false
+             in
+              let rec sort branches cl =
+               match cl with
+                  [] ->
+                   if branches = [] then []
+                   else
+                    raise (Invalid_choice
+                     (Some loc,
+                      lazy
+                       ("Unrecognized constructors: " ^
+                        String.concat " "
+                         (List.map (fun ((head,_,_),_) -> head) branches))))
+                | (name,_)::cltl ->
+                   let rec find_and_remove =
+                    function
+                       [] ->
+                        raise
+                         (Invalid_choice
+                          (Some loc, lazy ("Missing case: " ^ name)))
+                     | ((name',_,_),_) as branch :: tl when name = name' ->
+                        branch,tl
+                     | branch::tl ->
+                        let found,rest = find_and_remove tl in
+                         found, branch::rest
+                   in
+                    let branch,tl = find_and_remove branches in
+                     branch::sort tl cltl
+              in
+               sort branches cl
+          | _ -> assert false
         in
         Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
           (List.map do_branch branches))
@@ -386,7 +424,7 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
                     (try
                       List.assoc s ids_to_uris, aux ~localize loc context term
                      with Not_found ->
-                       raise (Invalid_choice (lazy "The provided explicit named substitution is trying to instantiate a named variable the object is not abstracted on"))))
+                       raise (Invalid_choice (Some loc, lazy "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
@@ -430,10 +468,10 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
 *)
                 t
             | _ ->
-              raise (Invalid_choice (lazy "??? Can this happen?"))
+              raise (Invalid_choice (Some loc, lazy "??? Can this happen?"))
            with 
              CicEnvironment.CircularDependency _ -> 
-               raise (Invalid_choice (lazy "Circular dependency in the environment"))))
+               raise (Invalid_choice (None, lazy "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 ()
@@ -990,7 +1028,7 @@ let foo () =
 in refine_profiler.HExtlib.profile foo ()
         with
         | Try_again msg -> Uncertain (None,msg), ugraph
-        | Invalid_choice msg -> Ko (None,msg), ugraph
+        | Invalid_choice (loc,msg) -> Ko (loc,msg), ugraph
       in
       (* (4) build all possible interpretations *)
       let (@@) (l1,l2,l3) (l1',l2',l3') = l1@l1', l2@l2', l3@l3' in