-(* funzione generale di rilocazione dei riferimenti locali *)
-
-let relocate_term map t =
- let rec map_xnss k xnss =
- let imap (uri, t) = uri, map_term k t in
- List.map imap xnss
- and map_mss k mss =
- let imap = function
- | None -> None
- | Some t -> Some (map_term k t)
- in
- List.map imap mss
- and map_fs len k fs =
- let imap (name, i, ty, bo) = name, i, map_term k ty, map_term (k + len) bo in
- List.map imap fs
- and map_cfs len k cfs =
- let imap (name, ty, bo) = name, map_term k ty, map_term (k + len) bo in
- List.map imap cfs
- and map_term k = function
- | C.Rel m -> if m < k then C.Rel m else C.Rel (map (m - k))
- | C.Sort _ as t -> t
- | C.Implicit _ as t -> t
- | C.Var (uri, xnss) -> C.Var (uri, map_xnss k xnss)
- | C.Const (uri, xnss) -> C.Const (uri, map_xnss k xnss)
- | C.MutInd (uri, tyno, xnss) -> C.MutInd (uri, tyno, map_xnss k xnss)
- | C.MutConstruct (uri, tyno, consno, xnss) ->
- C.MutConstruct (uri, tyno, consno, map_xnss k xnss)
- | C.Meta (i, mss) -> C.Meta(i, map_mss k mss)
- | C.Cast (te, ty) -> C.Cast (map_term k te, map_term k ty)
- | C.Appl ts -> C.Appl (List.map (map_term k) ts)
- | C.MutCase (sp, i, outty, t, pl) ->
- C.MutCase (sp, i, map_term k outty, map_term k t, List.map (map_term k) pl)
- | C.Prod (n, s, t) -> C.Prod (n, map_term k s, map_term (succ k) t)
- | C.Lambda (n, s, t) -> C.Lambda (n, map_term k s, map_term (succ k) t)
- | C.LetIn (n, s, t) -> C.LetIn (n, map_term k s, map_term (succ k) t)
- | C.Fix (i, fs) -> C.Fix (i, map_fs (List.length fs) k fs)
- | C.CoFix (i, cfs) -> C.CoFix (i, map_cfs (List.length cfs) k cfs)
- in
- map_term 0 t
-
-let id n = n
-
-let after continuation aftermap beforemap =
- continuation ~map:(fun n -> aftermap (beforemap n))
-
-let after2 continuation aftermap beforemap ~map =
- continuation ~map:(fun n -> map (aftermap (beforemap n)))
-