summaryrefslogtreecommitdiff
path: root/compiler/Substitute.ml
diff options
context:
space:
mode:
Diffstat (limited to 'compiler/Substitute.ml')
-rw-r--r--compiler/Substitute.ml12
1 files changed, 12 insertions, 0 deletions
diff --git a/compiler/Substitute.ml b/compiler/Substitute.ml
index 415f4d59..8348424c 100644
--- a/compiler/Substitute.ml
+++ b/compiler/Substitute.ml
@@ -456,3 +456,15 @@ let abs_subst_ids (rsubst : T.RegionId.id -> T.RegionId.id)
(bsubst : V.BorrowId.id -> V.BorrowId.id)
(asubst : V.AbstractionId.id -> V.AbstractionId.id) (x : V.abs) : V.abs =
(subst_ids_visitor rsubst rvsubst tsubst ssubst bsubst asubst)#visit_abs x
+
+let typed_avalue_subst_rids (rsubst : T.RegionId.id -> T.RegionId.id)
+ (x : V.typed_avalue) : V.typed_avalue =
+ let asubst _ = raise (Failure "Unreachable") in
+ (subst_ids_visitor rsubst
+ (fun x -> x)
+ (fun x -> x)
+ (fun x -> x)
+ (fun x -> x)
+ asubst)
+ #visit_typed_avalue
+ x