-- File: pointDevelop1 -- This file shows how the OOP concept of aggregation is modelled in system -- lambda-omega-L-plus. It corresponds with Section 9.1. Path "../lol" Path "../lolExtra" Path "../lolplus" Load "lambdaLplus" Load "nat" ------------------------- -- Step 1: Aggregation -- ------------------------- Def PointRep := {|x:Nat|} Def pointInit := {x=O} : PointRep Def getX := \st:PointRep. st`x : PointRep -> Nat Def setX := \st:PointRep. \n:Nat. {x=n} : PointRep -> Nat -> PointRep Def bump := \st:PointRep. {x= S st`x} : PointRep -> PointRep Def pointMet := {getX = \st:PointRep. st`x, setX = \st:PointRep. \n:Nat. {x=n}, bump = \st:PointRep. {x= S st`x}} : {|getX:PointRep->Nat, setX:PointRep->Nat->PointRep, bump:PointRep->PointRep|} Def PointI := \R:*s. {|getX:R->Nat, setX:R->Nat->R, bump:R->R|} -- Result: Yes Def newPoint := {state = pointInit, met = pointMet} : {| state : PointRep, met : PointI PointRep |} Def Point := {| state : PointRep, met : PointI PointRep |} Def point'getX := \p:Point. p`met`getX p`state : Point -> Nat Def point'bump := \p:Point. {state = p`met`bump p`state, met = p`met} : Point -> Point Def point'setX := \p:Point. \n:Nat. {state = p`met`setX p`state n, met = p`met} : Point -> Nat -> Point -- Result: S O