diff --git a/src/Unbound.ml b/src/Unbound.ml index ed0cb6b437fe117ade7f04242a96b9d0cc62334a..1025995974146847b56e1cb0b772f9ca6feef103 100644 --- a/src/Unbound.ml +++ b/src/Unbound.ml @@ -1,7 +1,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 *) + | OutsideRec (* updating [current] and visiting [outer] subterms *) + | InsideRecDiscovery (* updating [current] and doing nothing else; embedded subterms not visited *) + | InsideRecVisit (* [current] not updated; [inner] is [current]; embedded subterms visited *) | Repeated type 'env penv = { @@ -29,10 +29,8 @@ type ('p, 't) bind = (('p, 't outer) rebind) abstraction (* = 'p * 't *) (* [Abstraction] allowed only in an expression *) -(* [Rebind], [Rec] forbidden under [Rec] *) -(* [Outer], [Binder] allowed both outside and inside [Rec] *) -(* [Inner] allowed only under [Rec]. *) -(* [Repeated] allowed everywhere *) +(* [Rebind], [Rec] forbidden under [Rec] and [Repeated] *) +(* [Outer], [Inner], [Binder], [Repeated] allowed everywhere *) type 't inner = 't @@ -58,7 +56,7 @@ 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 -> @@ -77,15 +75,11 @@ 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] *) + | Repeated + | InsideRecVisit -> (* The environment should not be extended when in visit mode. It has been extended already during the discovery phase. *) - self#lookup env x1 + self#lookup x1 !(penv.current) method private visit_rebind: 'env 'p1 'p2 'q1 'q2 . ('env penv -> 'p1 -> 'p2) -> @@ -101,7 +95,7 @@ class virtual ['self] libmap = object (self : 'self) let q2 = visit_q penv q1 in p2, q2 | InsideRecDiscovery - | InsideRecVisit _ + | InsideRecVisit | Repeated -> (* [rebind] forbidden under [rec] and [repeated] *) assert false @@ -123,15 +117,11 @@ class virtual ['self] libmap = object (self : 'self) 'env penv -> 't1 inner -> 't2 inner = fun visit_t penv t1 -> match penv.mode with - | OutsideRec -> - (* [inner] allowed only under [rec] *) - assert false | InsideRecDiscovery -> (* An [inner] subterm is NOT visited in discovery mode. *) Obj.magic () - | InsideRecVisit env -> - assert (env == !(penv.current)); - visit_t env t1 + | OutsideRec + | InsideRecVisit | Repeated -> visit_t !(penv.current) t1 @@ -146,12 +136,12 @@ class virtual ['self] libmap = object (self : 'self) let penv = { penv with mode = InsideRecDiscovery } in let _ = visit_p penv p1 in (* [!current] becomes [inner] *) - let penv = { penv with mode = InsideRecVisit !(penv.current) } in + let penv = { penv with mode = InsideRecVisit } in visit_p penv p1 | InsideRecDiscovery - | InsideRecVisit _ + | InsideRecVisit | Repeated -> - (* [rec] not allowed under [rec] or [repeated] *) + (* [rec] forbidden under [rec] or [repeated] *) assert false method private visit_repeated: 'env 'p1 'p2 .