- (* TASSI: da verificare *)
- | (C.Sort C.Prop, C.Prod (name,so,ta)) when not need_dummy ->
- let b,ugraph1 =
- CicReduction.are_convertible ~subst ~metasenv context so ind ugraph in
- if not b then
- false,ugraph1
- else
- (match CicReduction.whd ~subst ((Some (name,(C.Decl so)))::context) ta with
- 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 ->
- let b,ugraph1 =
- CicReduction.are_convertible ~subst ~metasenv context so ind ugraph in
- if not b then
- false,ugraph1
- else
- (match CicReduction.whd ~subst ((Some (name,(C.Decl so)))::context) ta with
- C.Sort C.Prop
- | C.Sort C.Set -> true,ugraph1
- | C.Sort C.CProp -> true,ugraph1
- | C.Sort (C.Type _) ->
- (* TASSI: da verificare *)
- (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
- match o with
- C.InductiveDefinition (itl,_,paramsno,_) ->
- let (_,_,_,cl) = List.nth itl i in
- let tys =
- List.map
- (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
- in
- (List.fold_right
- (fun (_,x) (i,ugraph) ->
- if i then
- is_small ~logger tys paramsno x ugraph
- else
- false,ugraph
- ) cl (true,ugraph1))
- | _ ->
- raise (TypeCheckerFailure
- ("Unknown mutual inductive definition:" ^
- UriManager.string_of_uri uri))
- )
- | _ -> raise (AssertFailure "19")
- )
- | (C.Sort (C.Type _), C.Prod (_,so,_)) when not need_dummy ->
- (* TASSI: da verificare *)
- CicReduction.are_convertible ~subst ~metasenv context so ind ugraph