i && check_is_really_smaller_arg ~subst context n nn kl x safes p)
pl true
else
+ let pl_and_cl =
+ try
+ List.combine pl cl
+ with
+ Invalid_argument _ ->
+ raise (TypeCheckerFailure "not enough patterns")
+ in
List.fold_right
(fun (p,(_,c)) i ->
let rl' =
in
i &&
check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
- ) (List.combine pl cl) true
+ ) pl_and_cl true
| C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
let (tys,len,isinductive,paramsno,cl) =
let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
i && check_is_really_smaller_arg ~subst context n nn kl x safes p)
pl true
else
+ let pl_and_cl =
+ try
+ List.combine pl cl
+ with
+ Invalid_argument _ ->
+ raise (TypeCheckerFailure "not enough patterns")
+ in
(*CSC: supponiamo come prima che nessun controllo sia necessario*)
(*CSC: sugli argomenti di una applicazione *)
List.fold_right
in
i &&
check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
- ) (List.combine pl cl) true
+ ) pl_and_cl true
| _ ->
List.fold_right
(fun p i ->
i && guarded_by_destructors context n nn kl x safes p)
pl true
else
+ let pl_and_cl =
+ try
+ List.combine pl cl
+ with
+ Invalid_argument _ ->
+ raise (TypeCheckerFailure "not enough patterns")
+ in
guarded_by_destructors context n nn kl x safes outtype &&
(*CSC: manca ??? il controllo sul tipo di term? *)
List.fold_right
in
i &&
guarded_by_destructors context' n' nn' kl x' safes' e
- ) (List.combine pl cl) true
+ ) pl_and_cl true
| C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
let (tys,len,isinductive,paramsno,cl) =
let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
i && guarded_by_destructors context n nn kl x safes p)
pl true
else
+ let pl_and_cl =
+ try
+ List.combine pl cl
+ with
+ Invalid_argument _ ->
+ raise (TypeCheckerFailure "not enough patterns")
+ in
guarded_by_destructors context n nn kl x safes outtype &&
(*CSC: manca ??? il controllo sul tipo di term? *)
List.fold_right
in
i &&
guarded_by_destructors context' n' nn' kl x' safes' e
- ) (List.combine pl cl) true
+ ) pl_and_cl true
| _ ->
guarded_by_destructors context n nn kl x safes outtype &&
guarded_by_destructors context n nn kl x safes term &&
false,ugraph1
else
(match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
- C.Sort C.Prop -> true,ugraph1
- | (C.Sort C.Set | C.Sort C.CProp) ->
- (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
- match o with
- C.InductiveDefinition (itl,_,_,_) ->
- let (_,_,_,cl) = List.nth itl i in
- (* is a singleton definition? *)
- List.length cl = 1,ugraph1
- | _ ->
- raise (TypeCheckerFailure
- ("Unknown mutual inductive definition:" ^
- UriManager.string_of_uri uri))
- )
- | _ -> false,ugraph1
- )
+ C.Sort C.Prop -> true,ugraph1
+ | (C.Sort C.Set | C.Sort C.CProp | C.Sort (C.Type _)) ->
+ (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ match o with
+ C.InductiveDefinition (itl,_,_,_) ->
+ let (_,_,_,cl) = List.nth itl i in
+ (* is a singleton definition or the empty proposition? *)
+ (List.length cl = 1 || List.length cl = 0),ugraph1
+ | _ ->
+ raise (TypeCheckerFailure
+ ("Unknown mutual inductive definition:" ^
+ UriManager.string_of_uri uri)))
+ | _ -> false,ugraph1)
| ((C.Sort C.Set, C.Prod (name,so,ta))
| (C.Sort C.CProp, C.Prod (name,so,ta)))
when not need_dummy ->
if not branches_ok then
raise
(TypeCheckerFailure "Case analysys: wrong branch type");
- let arguments =
+ let arguments' =
if not need_dummy then outtype::arguments@[term]
else outtype::arguments in
let outtype =
- if arguments = [] then outtype
- else CicReduction.head_beta_reduce (C.Appl arguments)
+ if need_dummy && arguments = [] then outtype
+ else CicReduction.head_beta_reduce (C.Appl arguments')
in
outtype,ugraph5
| C.Fix (i,fl) ->