aboutsummaryrefslogtreecommitdiffstats
path: root/checklink/Lens.ml
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2015-10-12 11:48:36 +0200
committerXavier Leroy <xavier.leroy@inria.fr>2015-10-12 11:48:36 +0200
commit3ab947ce345e9d18ddcda57d8f88b2a9b8f5d267 (patch)
tree41afaa730849b6f9e8116ddc3068044928997d8c /checklink/Lens.ml
parentef0f69dc1caeab169dcefca4d8b89f4d9e756bb5 (diff)
downloadcompcert-3ab947ce345e9d18ddcda57d8f88b2a9b8f5d267.tar.gz
compcert-3ab947ce345e9d18ddcda57d8f88b2a9b8f5d267.zip
Removal of cchecklink, superseded by AbsInt's Valex tool.
Diffstat (limited to 'checklink/Lens.ml')
-rw-r--r--checklink/Lens.ml32
1 files changed, 0 insertions, 32 deletions
diff --git a/checklink/Lens.ml b/checklink/Lens.ml
deleted file mode 100644
index 43359334..00000000
--- a/checklink/Lens.ml
+++ /dev/null
@@ -1,32 +0,0 @@
-type ('a, 'b) t = {
- get: 'a -> 'b;
- set: 'b -> 'a -> 'a;
-}
-
-let ( |- ) f g x = g (f x)
-
-let modify l f a =
- let oldval = l.get a in
- let newval = f oldval in
- l.set newval a
-
-let compose l1 l2 = {
- get = l2.get |- l1.get;
- set = l1.set |- modify l2
-}
-
-let _get a l = l.get a
-
-let _set v a l = l.set v a
-
-let _modify f l = modify l f
-
-let (|.) = _get
-
-let (^=) l v = fun a -> _set v a l
-
-let (^%=) l f = _modify f l
-
-let (|--) l1 l2 = compose l2 l1
-
-let (--|) = compose