-and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
- need_dummy ind arity1 arity2 ugraph =
- let module C = Cic in
- let module U = UriManager in
- let arity1 = CicReduction.whd ~subst context arity1 in
- let rec check_allowed_sort_elimination_aux ugraph context arity2 need_dummy =
- match arity1, CicReduction.whd ~subst context arity2 with
- (C.Prod (_,so1,de1), C.Prod (_,so2,de2)) ->
- let b,ugraph1 =
- CicReduction.are_convertible ~subst ~metasenv context so1 so2 ugraph in
- if b then
- check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
- need_dummy (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2
- ugraph1
- else
- false,ugraph1
- | (C.Sort _, 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
- check_allowed_sort_elimination_aux ugraph1
- ((Some (name,C.Decl so))::context) ta true
- | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true,ugraph
- | (C.Sort C.Prop, C.Sort C.Set)
- | (C.Sort C.Prop, C.Sort C.CProp)
- | (C.Sort C.Prop, C.Sort (C.Type _) ) when need_dummy ->
- (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
- match o with
- C.InductiveDefinition (itl,_,paramsno,_) ->
- let itl_len = List.length itl in
- let (name,_,ty,cl) = List.nth itl i in
- let cl_len = List.length cl in
- if (cl_len = 0 || (itl_len = 1 && cl_len = 1)) then
- let non_informative,ugraph =
- if cl_len = 0 then true,ugraph
- else
- is_non_informative ~logger [Some (C.Name name,C.Decl ty)]
- paramsno (snd (List.nth cl 0)) ugraph
- in
- (* is it a singleton or empty non recursive and non informative
- definition? *)
- non_informative, ugraph
- else
- false,ugraph
- | _ ->
- raise (TypeCheckerFailure
- (lazy ("Unknown mutual inductive definition:" ^
- UriManager.string_of_uri uri)))
- )
- | (C.Sort C.Set, C.Sort C.Prop) when need_dummy -> true , ugraph
- | (C.Sort C.CProp, C.Sort C.Prop) when need_dummy -> true , ugraph
- | (C.Sort C.Set, C.Sort C.Set) when need_dummy -> true , ugraph
- | (C.Sort C.Set, C.Sort C.CProp) when need_dummy -> true , ugraph
- | (C.Sort C.CProp, C.Sort C.Set) when need_dummy -> true , ugraph
- | (C.Sort C.CProp, C.Sort C.CProp) when need_dummy -> true , ugraph
- | ((C.Sort C.Set, C.Sort (C.Type _)) | (C.Sort C.CProp, C.Sort (C.Type _)))
- when need_dummy ->
- (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
- match o with
- C.InductiveDefinition (itl,_,paramsno,_) ->
- let tys =
- List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
- in
- let (_,_,_,cl) = List.nth itl i in
- (List.fold_right
- (fun (_,x) (i,ugraph) ->
- if i then
- is_small ~logger tys paramsno x ugraph
- else
- false,ugraph
- ) cl (true,ugraph))
- | _ ->
- raise (TypeCheckerFailure
- (lazy ("Unknown mutual inductive definition:" ^
- UriManager.string_of_uri uri)))
- )
- | (C.Sort (C.Type _), C.Sort _) when need_dummy -> true , ugraph
- | (_,_) -> false,ugraph
- in
- check_allowed_sort_elimination_aux ugraph context arity2 need_dummy
-