From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 25 Oct 2007 16:53:12 +0000 (+0000)
Subject: Bug fixed: case analysis where a case had not the expected number of arguments
X-Git-Tag: 0.4.95@7852~100
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=93a8a0a29f033e02812d341b785f4522a6a17549;p=helm.git

Bug fixed: case analysis where a case had not the expected number of arguments
was not detected.
---

diff --git a/components/cic_disambiguation/disambiguate.ml b/components/cic_disambiguation/disambiguate.ml
index 020d038ac..6dd82cc28 100644
--- a/components/cic_disambiguation/disambiguate.ml
+++ b/components/cic_disambiguation/disambiguate.ml
@@ -253,6 +253,11 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
                List.nth il indtype_no
               with _ -> assert false
              in
+              let rec count_prod t =
+                match CicReduction.whd [] t with
+                    Cic.Prod (_, _, t) -> 1 + (count_prod t)
+                  | _ -> 0 
+              in 
               let rec sort branches cl =
                match cl with
                   [] ->
@@ -264,7 +269,7 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
                        ("Unrecognized constructors: " ^
                         String.concat " "
                          (List.map (fun ((head,_,_),_) -> head) branches))))
-                | (name,_)::cltl ->
+                | (name,ty)::cltl ->
                    let rec find_and_remove =
                     function
                        [] ->
@@ -278,7 +283,14 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
                          found, branch::rest
                    in
                     let branch,tl = find_and_remove branches in
-                     branch::sort tl cltl
+                    let (_,_,args),_ = branch in
+                     if List.length args = count_prod ty then
+                      branch::sort tl cltl
+                     else
+                      raise
+                       (Invalid_choice
+                        (Some loc,
+                          lazy ("Wrong number of arguments for " ^ name)))
               in
                sort branches cl
           | _ -> assert false