```-- File: pointDevelop2

-- This file shows how the OOP concept of encapsulation is modelled in system
-- lambda-omega-L-plus. It corresponds with Section 9.2.

Path "../lol"
Path "../lolExtra"
Path "../lolplus"
Load "lambdaLplus"
Load "nat"

-------------------------
-- Step 1: Aggregation --
-------------------------

-- We retain PointRep, pointInt, PointI and pointMet from pointDevelop1

Def PointRep := {|x:Nat|}

Def pointInit := {x=O} : PointRep

Def PointI := \R:*s. {|getX:R->Nat,
setX:R->Nat->R,
bump:R->R|}

Def pointMet := {getX = \st:PointRep. st`x,
setX = \st:PointRep. \n:Nat. {x=n},
bump = \st:PointRep. {x= S st`x}} :
PointI PointRep

---------------------------
-- Step 2: Encapsulation --
---------------------------

Def newPoint := (pack (\X:*s. {| state : X, met : PointI X |}) PointRep
{state = pointInit,
met = pointMet}) :
Sig X:*s. {| state : X, met : PointI X |}

Def Point := Sig X:*s. {| state : X, met : PointI X |}

Check newPoint : Point
-- Result: Yes.

Def Object := \I:*s->*s. Sig X:*s. {| state : X, met : I X |}
Check Object PointI :=: Point
-- Result: Yes.

-- method invocation:

Def point'getX := \p:Point. unpack p (\X:*s.\x:{|state:X,met : PointI X|}.
x`met`getX x`state) :
Point -> Nat

Def point'bump := \p:Point. unpack p (\X:*s.\x:{|state:X,met : PointI X|}.
pack (\X:*s. {| state : X, met : PointI X |})
X {state= x`met`bump x`state,
met = x`met}) :
Point -> Point

Def point'setX :=
\p:Point. \n:Nat. unpack p (\X:*s.\x:{|state:X,met : PointI X|}.
pack (\X:*s. {| state : X, met : PointI X |})
X {state= x`met`setX x`state n,
met = x`met}) :
Point -> Nat -> Point

bdRed point'getX (point'setX newPoint (S O))
-- Result: S O

-- Another implementation
Def PointRep2 := {|x:Nat, bumped : Bool|}

Def pointInit2 := {x=O,bumped=false} : PointRep2

Def pointMet2 := {getX = \st:PointRep2. st`x,
setX = \st:PointRep2. \n:Nat. {x=n,bumped=st`bumped},
bump = \st:PointRep2. {x= S st`x,bumped=true}} :
PointI PointRep2

Def newPoint2 := (pack (\X:*s. {| state : X, met : PointI X |}) PointRep2
{state = pointInit2,
met = pointMet2}) :
Point

-- preparation step 3.

Var Colour : *s
Var red,white, blue : Colour

Def ColPointI := \R:*s. {|getX:R->Nat,
setX:R->Nat->R,
bump:R->R,
getC:R->Colour,
setC:R->Colour->R|}

Def ColPoint := Object ColPointI

Def newColPoint := (pack (\X:*s. {| state : X, met : ColPointI X |}) {||}
{state = {},
met = {getX= \r:{||}.O,
setX= \r:{||}.\n:Nat. r,
bump= \r:{||}.r,
getC= \r:{||}.red,
setC= \r:{||}.\c:Colour.r}}) :
ColPoint

Check newColPoint : Point
-- Result: No.
```