From 93a8a0a29f033e02812d341b785f4522a6a17549 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 25 Oct 2007 16:53:12 +0000 Subject: [PATCH] Bug fixed: case analysis where a case had not the expected number of arguments was not detected. --- components/cic_disambiguation/disambiguate.ml | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) 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 -- 2.39.2