-- 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"
Load "lambdaLsubplus"
Load "nat"

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