```-- File: pointDevelop3

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

Path "../lol"
Path "../lolExtra"
Path "../lolplus"
Path "../lolsub"

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

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 |}

Def Object := \I:*s->*s. Sig X:*s. {| state : X, met : I X |}

-- 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}}) :
Object ColPointI

-----------------------
-- Step 3: Subtyping --
-----------------------

Check ColPointI <: PointI
-- Result: Yes.

Check Object ColPointI <: Object PointI
-- Result: Yes.

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

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

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

Type point'bump ColPointI newColPoint
-- Result: Object ColPointI

Def colPoint'getC := \I<:ColPointI. \p:Object I.
unpack p (\X:*s.\x:{|state:X,met :I X|}.
x`met`getC x`state) :
@I<:ColPointI. Object I -> Colour

Def colPoint'setC := \I<:ColPointI. \p:Object I.
\col:Colour. unpack p (\X:*s.\x:{|state:X,met : I X|}.
pack (\X:*s. {| state : X, met : I X |})
X {state= x`met`setC x`state col,
met = x`met}) :
@I<:ColPointI. Object I -> Colour -> Object I

```