- C.Rel m when List.mem m safes || m = x ->
- let (lefts_and_tys,len,isinductive,paramsno,cl) =
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
- match o with
- C.InductiveDefinition (tl,_,paramsno,_) ->
- let tys =
- List.map
- (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) tl
- in
- let (_,isinductive,_,cl) = List.nth tl i in
- let cl' =
- List.map
- (fun (id,ty) ->
- (id, snd (split_prods ~subst tys paramsno ty))) cl in
- let lefts =
- match tl with
- [] -> assert false
- | (_,_,ty,_)::_ ->
- fst (split_prods ~subst [] paramsno ty)
- in
- (lefts@tys,List.length tl,isinductive,paramsno,cl')
- | _ ->
- raise (TypeCheckerFailure
- (lazy ("Unknown mutual inductive definition:" ^
- UriManager.string_of_uri uri)))
- in
- if not isinductive then
- List.fold_right
- (fun p i ->
- 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 (lazy "not enough patterns"))
- in
- List.fold_right
- (fun (p,(_,c)) i ->
- let rl' =
- let debrujinedte = debrujin_constructor uri len c in
- recursive_args lefts_and_tys 0 len debrujinedte
- in
- let (e,safes',n',nn',x',context') =
- get_new_safes ~subst context p c rl' safes n nn x
- in
- i &&
- check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
- ) pl_and_cl true
- | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
- let (lefts_and_tys,len,isinductive,paramsno,cl) =
- let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
- match o with
- C.InductiveDefinition (tl,_,paramsno,_) ->
- let (_,isinductive,_,cl) = List.nth tl i in
- let tys =
- List.map (fun (n,_,ty,_) ->
- Some(Cic.Name n,(Cic.Decl ty))) tl
- in
- let cl' =
- List.map
- (fun (id,ty) ->
- (id, snd (split_prods ~subst tys paramsno ty))) cl in
- let lefts =
- match tl with
- [] -> assert false
- | (_,_,ty,_)::_ ->
- fst (split_prods ~subst [] paramsno ty)
- in
- (lefts@tys,List.length tl,isinductive,paramsno,cl')
- | _ ->
- raise (TypeCheckerFailure
- (lazy ("Unknown mutual inductive definition:" ^
- UriManager.string_of_uri uri)))
- in
- if not isinductive then
- List.fold_right
- (fun p i ->
- 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 (lazy "not enough patterns"))
- in
- (*CSC: supponiamo come prima che nessun controllo sia necessario*)
- (*CSC: sugli argomenti di una applicazione *)
- List.fold_right
- (fun (p,(_,c)) i ->
- let rl' =
- let debrujinedte = debrujin_constructor uri len c in
- recursive_args lefts_and_tys 0 len debrujinedte
- in
- let (e, safes',n',nn',x',context') =
- get_new_safes ~subst context p c rl' safes n nn x
- in
- i &&
- check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
- ) pl_and_cl true
+ | C.Rel m | C.Appl ((C.Rel m)::_) when List.mem m safes || m = x ->
+ let tys,_ =
+ specialize_inductive_type ~logger ~subst ~metasenv context term
+ in
+ let tys_ctx,_ =
+ List.fold_left
+ (fun (types,len) (n,_,ty,_) ->
+ Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+ len+1)
+ ([],0) tys
+ in
+ let _,isinductive,_,cl = List.nth tys i in
+ if not isinductive then
+ List.for_all
+ (check_is_really_smaller_arg rec_uri rec_uri_len
+ ~logger ~metasenv ~subst context n nn kl x safes)
+ pl
+ else
+ List.for_all2
+ (fun p (_,c) ->
+ let rec_params =
+ let c =
+ debrujin_constructor ~check_exp_named_subst:false
+ rec_uri rec_uri_len context c in
+ let len_ctx = List.length context in
+ recursive_args (context@tys_ctx) len_ctx (len_ctx+rec_uri_len) c
+ in
+ let (e, safes',n',nn',x',context') =
+ get_new_safes ~subst context p rec_params safes n nn x
+ in
+ check_is_really_smaller_arg rec_uri rec_uri_len
+ ~logger ~metasenv ~subst context' n' nn' kl x' safes' e
+ ) pl cl