- | C.Rel m -> subst,metasenv,
- (if m <= n then C.Rel m else C.Rel (m+1)),ugraph
- | C.Var (uri,exp_named_subst) ->
- let subst,metasenv,exp_named_subst',ugraph1 =
- aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
- in
- subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
- | C.Meta (i,l) ->
- (* andrea: in general, beta_expand can create badly typed
- terms. This happens quite seldom in practice, UNLESS we
- iterate on the local context. For this reason, we renounce
- to iterate and just lift *)
- let l =
- List.map
- (function
- Some t -> Some (CicSubstitution.lift 1 t)
- | None -> None) l in
- subst, metasenv, C.Meta (i,l), ugraph
- | C.Sort _
- | C.Implicit _ as t -> subst,metasenv,t,ugraph
- | C.Cast (te,ty) ->
- let subst,metasenv,te',ugraph1 =
- aux metasenv subst n context te ugraph in
- let subst,metasenv,ty',ugraph2 =
- aux metasenv subst n context ty ugraph1 in
- (* TASSI: sure this is in serial? *)
- subst,metasenv,(C.Cast (te', ty')),ugraph2
- | C.Prod (nn,s,t) ->
- let subst,metasenv,s',ugraph1 =
- aux metasenv subst n context s ugraph in
- let subst,metasenv,t',ugraph2 =
- aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
- ugraph1
- in
- (* TASSI: sure this is in serial? *)
- subst,metasenv,(C.Prod (nn, s', t')),ugraph2
- | C.Lambda (nn,s,t) ->
- let subst,metasenv,s',ugraph1 =
- aux metasenv subst n context s ugraph in
- let subst,metasenv,t',ugraph2 =
- aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1
- in
- (* TASSI: sure this is in serial? *)
- subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
- | C.LetIn (nn,s,ty,t) ->
- let subst,metasenv,s',ugraph1 =
- aux metasenv subst n context s ugraph in
- let subst,metasenv,ty',ugraph1 =
- aux metasenv subst n context ty ugraph in
- let subst,metasenv,t',ugraph2 =
- aux metasenv subst (n+1) ((Some (nn, C.Def (s,ty)))::context) t
- ugraph1
- in
- (* TASSI: sure this is in serial? *)
- subst,metasenv,(C.LetIn (nn, s', ty', t')),ugraph2
- | C.Appl l ->
- let subst,metasenv,revl',ugraph1 =
- List.fold_left
- (fun (subst,metasenv,appl,ugraph) t ->
- let subst,metasenv,t',ugraph1 =
- aux metasenv subst n context t ugraph in
- subst,metasenv,(t'::appl),ugraph1
- ) (subst,metasenv,[],ugraph) l
- in
- subst,metasenv,(C.Appl (List.rev revl')),ugraph1
- | C.Const (uri,exp_named_subst) ->
- let subst,metasenv,exp_named_subst',ugraph1 =
- aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
- in
- subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1
- | C.MutInd (uri,i,exp_named_subst) ->
- let subst,metasenv,exp_named_subst',ugraph1 =
- aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
- in
- subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1
- | C.MutConstruct (uri,i,j,exp_named_subst) ->
- let subst,metasenv,exp_named_subst',ugraph1 =
- aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
- in
- subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1
- | C.MutCase (sp,i,outt,t,pl) ->
- let subst,metasenv,outt',ugraph1 =
- aux metasenv subst n context outt ugraph in
- let subst,metasenv,t',ugraph2 =
- aux metasenv subst n context t ugraph1 in
- let subst,metasenv,revpl',ugraph3 =
- List.fold_left
- (fun (subst,metasenv,pl,ugraph) t ->
- let subst,metasenv,t',ugraph1 =
- aux metasenv subst n context t ugraph in
- subst,metasenv,(t'::pl),ugraph1
- ) (subst,metasenv,[],ugraph2) pl
- in
- subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3
- (* TASSI: not sure this is serial *)
- | C.Fix (i,fl) ->
-(*CSC: not implemented
- let tylen = List.length fl in
- let substitutedfl =
- List.map
- (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
- fl
- in
- C.Fix (i, substitutedfl)
-*)
- subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph
- | C.CoFix (i,fl) ->
-(*CSC: not implemented
- let tylen = List.length fl in
- let substitutedfl =
- List.map
- (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
- fl
- in
- C.CoFix (i, substitutedfl)