From 63ecb7a225670d24d662669c246eba5d7408c2aa Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Pottier?= <francois.pottier@inria.fr>
Date: Mon, 20 Feb 2017 10:30:14 +0100
Subject: [PATCH] Added [repeated].

---
 src/Unbound.ml | 31 ++++++++++++++++++++++++++-----
 1 file changed, 26 insertions(+), 5 deletions(-)

diff --git a/src/Unbound.ml b/src/Unbound.ml
index 4944f2e..ed0cb6b 100644
--- a/src/Unbound.ml
+++ b/src/Unbound.ml
@@ -2,6 +2,7 @@ type 'env mode =
   | OutsideRec
   | InsideRecDiscovery     (* updating [current] and doing nothing else; embedded subterms not visited *)
   | InsideRecVisit of 'env (* [inner] component now known; embedded subterms visited *)
+  | Repeated
 
 type 'env penv = {
     current: 'env ref; (* threaded left to right *)
@@ -21,6 +22,9 @@ type 't outer =
 type ('p, 't) rebind =
   'p * 't
 
+type 'p repeated =
+  'p
+
 type ('p, 't) bind =
   (('p, 't outer) rebind) abstraction (* = 'p * 't *)
 
@@ -28,6 +32,7 @@ type ('p, 't) bind =
 (* [Rebind], [Rec] forbidden under [Rec] *)
 (* [Outer], [Binder] allowed both outside and inside [Rec] *)
 (* [Inner] allowed only under [Rec]. *)
+(* [Repeated] allowed everywhere *)
 
 type 't inner =
   't
@@ -53,7 +58,8 @@ class virtual ['self] libmap = object (self : 'self)
   = fun visit_t penv t1 ->
       match penv.mode with
       | OutsideRec
-      | InsideRecVisit _ ->
+      | InsideRecVisit _
+      | Repeated ->
           visit_t penv.outer t1
       | InsideRecDiscovery ->
           (* An [outer] subterm is NOT visited in discovery mode. *)
@@ -71,6 +77,10 @@ class virtual ['self] libmap = object (self : 'self)
           let x2, env = self#extend x1 env in
           current := env;
           x2
+      | Repeated ->
+          let current = penv.current in
+          let env = !current in
+          self#lookup x1 env
       | InsideRecVisit env ->
           assert (env == !(penv.current)); (* TEMPORARY if always true, then we do not need to carry [env] *)
           (* The environment should not be extended when in visit mode.
@@ -91,8 +101,9 @@ class virtual ['self] libmap = object (self : 'self)
           let q2 = visit_q penv q1 in
           p2, q2
       | InsideRecDiscovery
-      | InsideRecVisit _ ->
-          (* [rebind] forbidden under [rec] *)
+      | InsideRecVisit _
+      | Repeated ->
+          (* [rebind] forbidden under [rec] and [repeated] *)
           assert false
 
   (* could in principle be generated, if [visitors] supported dealing with
@@ -121,6 +132,8 @@ class virtual ['self] libmap = object (self : 'self)
       | InsideRecVisit env ->
           assert (env == !(penv.current));
           visit_t env t1
+      | Repeated ->
+          visit_t !(penv.current) t1
 
   method private visit_recursive: 'env 'p1 'p2 .
     ('env penv -> 'p1 -> 'p2) ->
@@ -136,10 +149,18 @@ class virtual ['self] libmap = object (self : 'self)
           let penv = { penv with mode = InsideRecVisit !(penv.current) } in
           visit_p penv p1
       | InsideRecDiscovery
-      | InsideRecVisit _ ->
-          (* [rec] not allowed under [rec] *)
+      | InsideRecVisit _
+      | Repeated ->
+          (* [rec] not allowed under [rec] or [repeated] *)
           assert false
 
+  method private visit_repeated: 'env 'p1 'p2 .
+    ('env penv -> 'p1 -> 'p2) ->
+    'env penv -> 'p1 repeated -> 'p2 repeated
+  = fun visit_p penv p1 ->
+      let penv = { penv with mode = Repeated } in
+      visit_p penv p1
+
 end
 
 type ('bn, 'fn) tele =
-- 
GitLab