-and type_of_branch ~subst context argsno need_dummy outtype term constype =
- let module C = Cic in
- let module R = CicReduction in
- match R.whd ~subst context constype with
- C.MutInd (_,_,_) ->
- if need_dummy then
- outtype
- else
- C.Appl [outtype ; term]
- | C.Appl (C.MutInd (_,_,_)::tl) ->
- let (_,arguments) = split tl argsno
- in
- if need_dummy && arguments = [] then
- outtype
- else
- C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
- | C.Prod (name,so,de) ->
- let term' =
- match CicSubstitution.lift 1 term with
- C.Appl l -> C.Appl (l@[C.Rel 1])
- | t -> C.Appl [t ; C.Rel 1]
- in
- C.Prod (name,so,type_of_branch ~subst
- ((Some (name,(C.Decl so)))::context) argsno need_dummy
- (CicSubstitution.lift 1 outtype) term' de)
- | _ -> raise (AssertFailure (lazy "20"))
-
- and returns_a_coinductive ~subst context ty =
- let module C = Cic in
- match CicReduction.whd ~subst context ty with
- C.MutInd (uri,i,_) ->
- (*CSC: definire una funzioncina per questo codice sempre replicato *)
- let obj,_ =
- try
- CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
- with Not_found -> assert false
- in
- (match obj with
- C.InductiveDefinition (itl,_,_,_) ->
- let (_,is_inductive,_,_) = List.nth itl i in
- if is_inductive then None else (Some uri)
- | _ ->
- raise (TypeCheckerFailure
- (lazy ("Unknown mutual inductive definition:" ^
- UriManager.string_of_uri uri)))
- )
- | C.Appl ((C.MutInd (uri,i,_))::_) ->
- (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
- match o with
- C.InductiveDefinition (itl,_,_,_) ->
- let (_,is_inductive,_,_) = List.nth itl i in
- if is_inductive then None else (Some uri)
- | _ ->
- raise (TypeCheckerFailure
- (lazy ("Unknown mutual inductive definition:" ^
- UriManager.string_of_uri uri)))
- )
- | C.Prod (n,so,de) ->
- returns_a_coinductive ~subst ((Some (n,C.Decl so))::context) de
- | _ -> None
-