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

2. Interpretation of pattern matching highly improved:
   a) missing branches are now detected
   b) additional branches are now detected
   c) permutated branches are handled correctly

   Still to do:
   d) check that every constructor is given as parameters exactly the
      number of expected arguments

diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml
index 0b8674c0cf9804b56119107181b6779967468136..020d038ac74ff687dec0a0fd30062a9c358eef85 100644 (file)
--- a/helm/software/components/cic_disambiguation/disambiguate.ml
+++ b/helm/software/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

diff --git a/helm/software/components/cic_disambiguation/disambiguateChoices.ml b/helm/software/components/cic_disambiguation/disambiguateChoices.ml
index 64d2cf8e0343155736784a6c67d9370fc9ab8343..c3fa7efb2805cf953cf9cee4545f69c416984ca5 100644 (file)
--- a/helm/software/components/cic_disambiguation/disambiguateChoices.ml
+++ b/helm/software/components/cic_disambiguation/disambiguateChoices.ml
@@ -62,7 +62,7 @@ let mk_choice (dsc, args, appl_pattern) =
         try
          combine_with_rest names cic_args
         with Invalid_argument _ ->
-         raise (Invalid_choice (lazy ("The notation " ^ dsc ^ " expects more arguments")))
+         raise (Invalid_choice (None, lazy ("The notation " ^ dsc ^ " expects more arguments")))
     in
      let combined =
       TermAcicContent.instantiate_appl_pattern env' appl_pattern

diff --git a/helm/software/components/cic_disambiguation/disambiguateTypes.ml b/helm/software/components/cic_disambiguation/disambiguateTypes.ml
index 150482fbf503df28236aae0c1753d949dd99f135..1eade4ca09850d1b6d6636d5b3bb8e203142e5ee 100644 (file)
--- a/helm/software/components/cic_disambiguation/disambiguateTypes.ml
+++ b/helm/software/components/cic_disambiguation/disambiguateTypes.ml
@@ -40,7 +40,7 @@ type domain_item =
   | Symbol of string * int     (* literal, instance num *)
   | Num of int                 (* instance num *)
 
-exception Invalid_choice of string Lazy.t
+exception Invalid_choice of Stdpp.location option * string Lazy.t
 
 module OrderedDomain =
   struct

diff --git a/helm/software/components/cic_disambiguation/disambiguateTypes.mli b/helm/software/components/cic_disambiguation/disambiguateTypes.mli
index 96105670108e7d24a184c6042838bfd8659611c6..00fe4114cdcde61ca5e5bde2e299bcda3c846985 100644 (file)
--- a/helm/software/components/cic_disambiguation/disambiguateTypes.mli
+++ b/helm/software/components/cic_disambiguation/disambiguateTypes.mli
@@ -41,7 +41,7 @@ end
 
   (** to be raised when a choice is invalid due to some given parameter (e.g.
    * wrong number of Cic.term arguments received) *)
-exception Invalid_choice of string Lazy.t
+exception Invalid_choice of Stdpp.location option * string Lazy.t
 
 type codomain_item =
   string *  (* description *)

diff --git a/helm/software/components/cic_disambiguation/number_notation.ml b/helm/software/components/cic_disambiguation/number_notation.ml
index 781deb90e210629c60c26cd75ca192f790c90191..78135d9bef9abcf129b2c19a0d52ee3ace492aef 100644 (file)
--- a/helm/software/components/cic_disambiguation/number_notation.ml
+++ b/helm/software/components/cic_disambiguation/number_notation.ml
@@ -40,7 +40,7 @@ let _ =
       (fun _ num _ ->
         let num = int_of_string num in
         if num = 0 then
-          raise (DisambiguateTypes.Invalid_choice (lazy "0 is not a valid positive number"))
+          raise (DisambiguateTypes.Invalid_choice (None, lazy "0 is not a valid positive number"))
         else
           HelmLibraryObjects.build_bin_pos num));
   DisambiguateChoices.add_num_choice