+ let rec analyse_branch context ty te =
+ match CicReduction.whd context ty with
+ C.Meta _ -> raise (Impossible 34)
+ | C.Rel _
+ | C.Var _
+ | C.Sort _ ->
+ does_not_occur context n nn te
+ | C.Implicit
+ | C.Cast _ -> raise (Impossible 24) (* due to type-checking *)
+ | C.Prod (name,so,de) ->
+ analyse_branch ((Some (name,(C.Decl so)))::context) de te
+ | C.Lambda _
+ | C.LetIn _ -> raise (Impossible 25) (* due to type-checking *)
+ | C.Appl ((C.MutInd (uri,_,_))::tl) as ty
+ when uri == coInductiveTypeURI ->
+ guarded_by_constructors context n nn true te [] coInductiveTypeURI
+ | C.Appl ((C.MutInd (uri,_,_))::tl) as ty ->
+ guarded_by_constructors context n nn true te tl coInductiveTypeURI
+ | C.Appl _ ->
+ does_not_occur context n nn te
+ | C.Const _ -> raise (Impossible 26)
+ | C.MutInd (uri,_,_) when uri == coInductiveTypeURI ->
+ guarded_by_constructors context n nn true te [] coInductiveTypeURI
+ | C.MutInd _ ->
+ does_not_occur context n nn te
+ | C.MutConstruct _ -> raise (Impossible 27)
+ (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
+ (*CSC: in head position. *)
+ | C.MutCase _
+ | C.Fix _
+ | C.CoFix _ -> raise (Impossible 28) (* due to type-checking *)
+ in
+ let rec analyse_instantiated_type context ty l =
+ match CicReduction.whd context ty with
+ C.Rel _
+ | C.Var _
+ | C.Meta _
+ | C.Sort _
+ | C.Implicit
+ | C.Cast _ -> raise (Impossible 29) (* due to type-checking *)
+ | C.Prod (name,so,de) ->
+ begin
+ match l with
+ [] -> true
+ | he::tl ->
+ analyse_branch context so he &&
+ analyse_instantiated_type ((Some (name,(C.Decl so)))::context)
+ de tl
+ end
+ | C.Lambda _
+ | C.LetIn _ -> raise (Impossible 30) (* due to type-checking *)
+ | C.Appl _ ->
+ List.fold_left
+ (fun i x -> i && does_not_occur context n nn x) true l
+ | C.Const _ -> raise (Impossible 31)
+ | C.MutInd _ ->
+ List.fold_left
+ (fun i x -> i && does_not_occur context n nn x) true l
+ | C.MutConstruct _ -> raise (Impossible 32)
+ (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
+ (*CSC: in head position. *)
+ | C.MutCase _
+ | C.Fix _
+ | C.CoFix _ -> raise (Impossible 33) (* due to type-checking *)
+ in
+ let rec instantiate_type args consty =
+ function
+ [] -> true
+ | tlhe::tltl as l ->
+ let consty' = CicReduction.whd context consty in
+ match args with
+ he::tl ->
+ begin
+ match consty' with
+ C.Prod (_,_,de) ->
+ let instantiated_de = CicSubstitution.subst he de in
+ (*CSC: siamo sicuri che non sia troppo forte? *)
+ does_not_occur context n nn tlhe &
+ instantiate_type tl instantiated_de tltl
+ | _ ->
+ (*CSC:We do not consider backbones with a MutCase, a *)
+ (*CSC:FixPoint, a CoFixPoint and so on in head position.*)
+ raise (Impossible 23)
+ end
+ | [] -> analyse_instantiated_type context consty' l
+ (* These are all the other cases *)
+ in
+ instantiate_type args consty tl