aboutsummaryrefslogtreecommitdiffstats
path: root/checklink/Lens.ml
diff options
context:
space:
mode:
authorFrançois Pottier <francois.pottier@inria.fr>2015-10-23 15:08:33 +0200
committerFrançois Pottier <francois.pottier@inria.fr>2015-10-23 15:08:33 +0200
commit8b817cda643d180d43ab8c84809ca2d55c7dd3df (patch)
tree812fe2f7ec68c03c5f0762f1266f383193bbfe92 /checklink/Lens.ml
parentc46723c0169145d41d1879c236f53314456f1ba1 (diff)
parent1cb3d93ff278ebbd0c6967c5f9401a97f9b618b4 (diff)
downloadcompcert-8b817cda643d180d43ab8c84809ca2d55c7dd3df.tar.gz
compcert-8b817cda643d180d43ab8c84809ca2d55c7dd3df.zip
Merge remote branch 'upstream/master' into clean
Conflicts: Makefile.extr
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