+(* replaces in a term a term with another one. *)
+(* Lifting are performed as usual. *)
+let replace_lifting_csc nnn ~equality ~what ~with_what ~where =
+ let rec substaux k =
+ let module C = Cic in
+ let module S = CicSubstitution in
+ function
+ t when (equality t what) -> S.lift (k-1) with_what
+ | C.Rel n as t ->
+ if n < k then C.Rel n else C.Rel (n + nnn)
+ | C.Var (uri,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
+ in
+ C.Var (uri,exp_named_subst')
+ | C.Meta (i, l) as t ->
+ let l' =
+ List.map
+ (function
+ None -> None
+ | Some t -> Some (substaux k t)
+ ) l
+ in
+ C.Meta(i,l')
+ | C.Sort _ as t -> t
+ | C.Implicit as t -> t
+ | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
+ | C.Prod (n,s,t) ->
+ C.Prod (n, substaux k s, substaux (k + 1) t)
+ | C.Lambda (n,s,t) ->
+ C.Lambda (n, substaux k s, substaux (k + 1) t)
+ | C.LetIn (n,s,t) ->
+ C.LetIn (n, substaux k s, substaux (k + 1) t)
+ | C.Appl (he::tl) ->
+ (* Invariant: no Appl applied to another Appl *)
+ let tl' = List.map (substaux k) tl in
+ begin
+ match substaux k he with
+ C.Appl l -> C.Appl (l@tl')
+ | _ as he' -> C.Appl (he'::tl')
+ end
+ | C.Appl _ -> assert false
+ | C.Const (uri,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
+ in
+ C.Const (uri,exp_named_subst')
+ | C.MutInd (uri,i,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
+ in
+ C.MutInd (uri,i,exp_named_subst')
+ | C.MutConstruct (uri,i,j,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
+ in
+ C.MutConstruct (uri,i,j,exp_named_subst')
+ | C.MutCase (sp,i,outt,t,pl) ->
+ C.MutCase (sp,i,substaux k outt, substaux k t,
+ List.map (substaux k) pl)
+ | C.Fix (i,fl) ->
+ let len = List.length fl in
+ let substitutedfl =
+ List.map
+ (fun (name,i,ty,bo) ->
+ (name, i, substaux k ty, substaux (k+len) bo))
+ fl
+ in
+ C.Fix (i, substitutedfl)
+ | C.CoFix (i,fl) ->
+ let len = List.length fl in
+ let substitutedfl =
+ List.map
+ (fun (name,ty,bo) ->
+ (name, substaux k ty, substaux (k+len) bo))
+ fl
+ in
+ C.CoFix (i, substitutedfl)
+ in
+let res =
+ substaux 1 where
+in prerr_endline ("@@@@ risultato replace: " ^ (CicPp.ppterm res)); res
+;;
+