+ raise (Invalid_choice (Some loc, lazy "The type of the term to be matched is not (co)inductive!")))
+ in
+ let branches =
+ if create_dummy_ids then
+ List.map
+ (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 \"_\""))
+ ) branches
+ else
+ match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph indtype_uri) with
+ Cic.InductiveDefinition (il,_,leftsno,_) ->
+ let _,_,_,cl =
+ try
+ 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
+ [] ->
+ let rec analyze unused unrecognized useless =
+ function
+ [] ->
+ if unrecognized != [] then
+ raise (Invalid_choice
+ (Some loc,
+ lazy
+ ("Unrecognized constructors: " ^
+ String.concat " " unrecognized)))
+ else if useless > 0 then
+ raise (Invalid_choice
+ (Some loc,
+ lazy
+ ("The last " ^ string_of_int useless ^
+ "case" ^ if useless > 1 then "s are" else " is" ^
+ " unused")))
+ else
+ []
+ | (Ast.Wildcard,_)::tl when not unused ->
+ analyze true unrecognized useless tl
+ | (Ast.Pattern (head,_,_),_)::tl when not unused ->
+ analyze unused (head::unrecognized) useless tl
+ | _::tl -> analyze unused unrecognized (useless + 1) tl
+ in
+ analyze false [] 0 branches
+ | (name,ty)::cltl ->
+ let rec find_and_remove =
+ function
+ [] ->
+ raise
+ (Invalid_choice
+ (Some loc, lazy ("Missing case: " ^ name)))
+ | ((Ast.Wildcard, _) as branch :: _) as branches ->
+ branch, branches
+ | (Ast.Pattern (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
+ match branch with
+ Ast.Pattern (name,y,args),term ->
+ if List.length args = count_prod ty - leftsno then
+ ((name,y,args),term)::sort tl cltl
+ else
+ raise
+ (Invalid_choice
+ (Some loc,
+ lazy ("Wrong number of arguments for " ^ name)))
+ | Ast.Wildcard,term ->
+ let rec mk_lambdas =
+ function
+ 0 -> term
+ | n ->
+ CicNotationPt.Binder
+ (`Lambda, (CicNotationPt.Ident ("_", None), None),
+ mk_lambdas (n - 1))
+ in
+ (("wildcard",None,[]),
+ mk_lambdas (count_prod ty - leftsno)) :: sort tl cltl
+ in
+ sort branches cl
+ | _ -> assert false