**************
*** This first group of modules defines a Calendar
*** *abstractly*. We will add futher modules to make
*** it *concrete* below.
**************

***
*** The basic calendar read/write operations and
*** various status-checking and reporting operations
*** and constants
***
fmod CALENDAR is

    *** Calendars are functions from timeslots to activities
    sorts TimeSlot? TimeSlot Activity Calendar .
    
    *** TimeSlot is a subsort of TimeSlot? and activities can
    *** only be associated with TimeSlot.
    
    subsort TimeSlot < TimeSlot? .

    *** Read a Calendar entry
    op _(_) : Calendar TimeSlot -> Activity .

    *** Write a Calendar entry
    op _(_/_) : Calendar TimeSlot Activity -> Calendar .

    *** Representation of an unused TimeSlot
    op empty : ->  Activity .


    *** The Calendar si *strictly* ordered
    op _<_ : TimeSlot? TimeSlot? -> Bool .

    *** Error codes that can be returned
    ops busy emptySlot : -> Calendar .

    vars s t : TimeSlot .
    var t' : TimeSlot? .
    var a : Activity .
    var c : Calendar .

    *** Define reading and writing - much like
    *** arrays and memory
    eq c(t / a)(t) = a .
    ceq c(t / a)(s) = c(s) if s =/= t .

    *** This must clearly be true.
    eq t' < t' = false .

endfm


*** Add an entry to the diary. Outcomes are either:
*** 1. the new Calender; 2. a badTime error (timeslot
*** outside those permitted); or 3. a busy error
*** (the timeslot is already in use)

fmod ADD-ENTRY is
    protecting CALENDAR .

    op addEntry : Calendar TimeSlot Activity -> Calendar .

    var c : Calendar .
    var t : TimeSlot .
    var a : Activity .

    eq addEntry(c,t,a) =
        if (c(t) =/= empty) then
            busy
        else
            c(t / a)
        fi .
endfm

*** Delete an entry from a Calendar
fmod DEL-ENTRY is
    protecting CALENDAR .

    op delEntry : Calendar TimeSlot -> Calendar .

    var c : Calendar .
    var t : TimeSlot .

    eq delEntry(c,t) =
        if (c(t) == empty) then
            emptySlot
        else
            c(t / empty)
        fi .
endfm

*** Replace an entry in (or add an entry to) a Calendar
fmod REPLACE-ENTRY is
    protecting CALENDAR .

    op replaceEntry : Calendar TimeSlot Activity -> Calendar .

    var c : Calendar .
    var a : Activity .
    var t : TimeSlot .

    eq replaceEntry(c,t,a) = c(t / a) .
endfm

*** Lookup an entry in a Calendar
fmod LOOKUP is
    protecting CALENDAR .

    op lookup : Calendar TimeSlot -> Activity .

    var c : Calendar .
    var t : TimeSlot .

    eq lookup(c,t) = c(t) .

endfm

*** Bring it all together in an "abstract calender"
fmod ABS-CALENDAR is
    protecting CALENDAR .
    protecting ADD-ENTRY .
    protecting DEL-ENTRY .
    protecting REPLACE-ENTRY .
    protecting LOOKUP .
endfm

**************
*** Now we will add some more modules to make the diary
*** *concrete* - we need to do this if we are to
*** execute operations on it.
**************

*** This module says what we mean by a timeslot,
*** and defines the operators previously left unspecified
***
*** There are some obvious problems with our timeslots:
*** they do not cover more than a single week, and have
*** no concept of date. However, they are sufficient for
*** the example.
fmod TIME-SLOTS is
    protecting INT .

    *** We are going to modify CALENDAR, so including
    *** instead of protecting
    including ABS-CALENDAR .

    sorts Day .

    ops mon tue wed thur fri sat sun : -> Day .
    
    *** We divide the day into hours and days - hour:day
    op _:_ : Int Day -> TimeSlot? .
    
    *** (It's actually a bit tacky to just leave hours as
    *** integers, but simpler.)

    op _<_ : Day Day -> Bool .

    var i : Int .
    vars h h1 h2 : Int .
    vars d d1 d2 : Day .

    *** When is one TimeSlot less than another?
    eq (h1 : d1) < (h2 : d2) =
        if ((d1 < d2) or (d1 == d2) and (h1 < h2)) then
            true
        else
            false
        fi .

    *** A [slightly arbitrary] ordering on days
    eq sun < d = if (d =/= sun) then true else false fi .
    eq mon < d = if (d =/= mon) then sun < d
                 else false fi .
    eq tue < d = if (d =/= tue) then mon < d
                 else false fi .
    eq wed < d = if (d =/= wed) then tue < d
                 else false fi .
    eq thur < d = if (d =/= thur) then wed < d
                 else false fi .
    eq fri < d = if (d =/= fri) then thur < d
                 else false fi .
    eq sat < d = false .

    *** We are going to allow times
    *** from 9 : mon to 16 : fri
    *** in the diary
    cmb (h : d) : TimeSlot if
        (h > 8) and (h < 17) and
           (d =/= sat) and (d =/= sun) .
endfm

*** This module just defines some constants
*** representing activities - it is even less sophisticated
*** than TIME-SLOTS
fmod ACTIVITIES is
    protecting ABS-CALENDAR .

    ops staffMeeting interview bossVisiting
        leavingParty : -> Activity .
endfm

*** This module brings everything together, and defines
*** an initially empty diary
fmod CONCRETE-CALENDAR is
    protecting TIME-SLOTS .
    protecting ACTIVITIES .
    
    op initCal : -> Calendar .

    var h : Int .
    var d : Day .
    
    eq initCal(h : d) = empty .
endfm

*** A sample reduction: empty the diary, then add a staff meeting
*** at 9.00 on tuesday; then lookup what is going on at 9.00 on
*** tuesday - should be a staff meeting
red lookup(addEntry(initCal,(9 : tue), staffMeeting),
(9 : tue)) .

*** Another: empty the diary, then add a staff meeting
*** at 9.00 on tuesday; then lookup what is going on at 9.00 on
*** monday - should be empty
red lookup(addEntry(initCal,(9 : tue), staffMeeting),
(9 : mon)) .