module CO4_DATATYPES is

-------------------------------------------------------------------------------

type BaseId is
   range 0..6 of Nat
   with ==, <>, <
end type

-------------------------------------------------------------------------------

type Id is
   First,
   Next (precedent: Id)
   with ==, <>
end type

-------------------------------------------------------------------------------

type Atom is
   white, black, square
   with ==, <>, <
end type

function comp (a1, a2: Atom): Bool is
   case a1, a2 in
      black, white -> return false
   |  white, black -> return false
   |  any, any -> return true
   end case
end function

-------------------------------------------------------------------------------

type Knowledge is
   set of Atom
   with ==, <>, remove, member
end type

function IsIn (a: Atom, K: Knowledge): Bool is
   return member (a, K)
end function

-------------------------------------------------------------------------------

type Change is
   Assert (a: Atom),
   Retract (a: Atom)
   with ==, <>, get
end type

function atom (c: Change): Atom is
   return c.a
end function

function + (k: Knowledge, c: Change): Knowledge is
   case c
   var a: Atom in
      Assert (a)  -> return Insert (a, k)
   |  Retract (a) -> return Remove (a, k)
   end case
end function

-------------------------------------------------------------------------------

type Proposal is
   list of Change
   with ==, <>, append, union
end type

function + (p: Proposal, c: Change): Proposal is
   return append (c, p)
end function

function * (p1, p2: Proposal): Proposal is
   return union (p1, p2)
end function

function + (k: Knowledge, p: Proposal): Knowledge is
   case p
   var p1: Proposal, c: Change in
     nil          -> return k
   | cons (c, p1) -> return (k + c) + p1
   end case
end function

function query (k: Knowledge, a: Atom): Bool is
   case k
   var a1: Atom, k1: Knowledge in
      nil           -> return true
   |  cons (a1, k1) -> return comp (a1, a) and query (k1, a)
   end case
end function

function isconsistent (k: Knowledge): Bool is
   case k
   var a: Atom, k1: Knowledge in
      nil          -> return true
   |  cons (a, k1) -> return query (k1, a) and isconsistent (k1)
   end case
end function

function query (k: Knowledge, p: Proposal): Bool is
   return isconsistent (k + p)
end function

function Assert (k: Knowledge): Proposal is
   case k
   var a: Atom, k1: Knowledge in
      nil          -> return nil
   |  cons (a, k1) -> return cons (Assert (a), Assert (remove (a, k1)))
   end case
end function

-------------------------------------------------------------------------------

type Request is
   reqregister (b: BaseId),
   reqevaluate (p: Proposal),
   reqachieve (p: Proposal),
   reqforward (r: Request),
   reqchallenge (p: Proposal),
   reqtell (p: Proposal)
   with ==, <>, get
end type

function Is_reqregister (r: Request): Bool is
   case r in
      reqregister (any BaseId) -> return true
   |  any -> return false
  end case
end function

function Is_reqevaluate (r: Request): Bool is
   case r in
      reqevaluate (any Proposal) -> return true
   |  any -> return false
   end case
end function

function Is_reqachieve (r: Request): Bool is
   case r in
      reqachieve (any Proposal) -> return true
   |  any -> return false
   end case
end function

function Is_reqforward (r: Request): Bool is
   case r in
      reqforward (any Request) -> return true
   |  any -> return false
   end case
end function

function Is_reqchallenge (r: Request): Bool is
   case r in
      reqchallenge (any Proposal) -> return true
   |  any -> return false
   end case
end function

function Is_reqtell (r: Request): Bool is
   case r in
      reqtell (any Proposal) -> return true
   |  any -> return false
   end case
end function

function content (r: Request): BaseId is
   return r.b
   -- i.e., if r is reqregister (b) then return b else raise UNEXPECTED
end function

function content (r: Request): Proposal is
   return r.p
   -- i.e., if r is reqevaluate (p) or reqachieve (p) or reqchallenge (p) or
   -- reqtell (p) then return p else raise UNEXPECTED
end function

function content (r: Request): Request is
   return r.r
   -- i.e., if r is reqforward (r) then return r else raise UNEXPECTED
end function

-------------------------------------------------------------------------------

type Answer is
   acceptx, -- "acceptx" rather than "accept", which was a LOTOS keyword
   reject,
   challenge (id: Id, p: Proposal)
   with ==, <>, get
end type

function Is_acceptx (a: Answer): Bool is
   return a == acceptx
end function

function Is_reject (a: Answer): Bool is
   return a == reject
end function

function Is_challenge (a: Answer): Bool is
   case a in
      challenge (any Id, any Proposal) -> return true
   |  any -> return false
   end case
end function

function replywith (a: Answer): Id is
   return a.id
   -- i.e., if a is challenge (id, p) then return id else raise UNEXPECTED
end function

function content (a: Answer): Proposal is
   return a.p
   -- i.e., if a is challenge (id, p) then return p else raise UNEXPECTED
end function

function answer (b: Bool): Answer is
   if b then
      return acceptx
   else
      return reject
   end if
end function

-------------------------------------------------------------------------------

type message is
   register (id: Id, b: BaseId),
   evaluate (id: Id, p: Proposal),
   achieve (id: Id, p: Proposal),
   forward (id: Id, r: Request),
   deny (id: Id),
   reply (id: Id, a: Answer),
   askall (id: Id, r: Request),
   error (id: Id),
   notify (id: Id, a: Answer),
   poolnotify (id: Id, a: Answer),
   pooldeny (id: Id),
   tell (p: Proposal)
   with ==, <>, get
end type

function Is_register (m: Message): Bool is
   case m in
      register (any Id, any BaseId) -> return true
   |  any -> return false
   end case
end function

function Is_evaluate (m: Message): Bool is
   case m in
      evaluate (any Id, any Proposal) -> return true
   |  any -> return false
   end case
end function

function Is_achieve (m: Message): Bool is
   case m in
      achieve (any Id, any Proposal) -> return true
   |  any -> return false
   end case
end function

function Is_forward (m: Message): Bool is
   case m in
      forward (any Id, any Request) -> return true
   |  any -> return false
   end case
end function

function Is_deny (m: Message): Bool is
   case m in
      deny (any Id) -> return true
   |  any -> return false
   end case
end function

function Is_reply (m: Message): Bool is
   case m in
      reply (any Id, any Answer) -> return true
   |  any -> return false
   end case
end function

function Is_askall (m: Message): Bool is
   case m in
      askall (any Id, any Request) -> return true
   |  any -> return false
   end case
end function

function Is_error (m: Message): Bool is
   case m in
      error (any Id) -> return true
   |  any -> return false
   end case
end function

function Is_notify (m: Message): Bool is
   case m in
      notify (any Id, any Answer) -> return true
   |  any -> return false
   end case
end function

function Is_poolnotify (m: Message): Bool is
   case m in
      poolnotify (any Id, any Answer) -> return true
   |  any -> return false
   end case
end function

function Is_pooldeny (m: Message): Bool is
   case m in
      pooldeny (any Id) -> return true
   |  any -> return false
   end case
end function

function Is_tell (m: Message): Bool is
   case m in
      tell (any Proposal) -> return true
   |  any -> return false
   end case
end function

function replywith (m: Message): Id is
   case m
   var id: Id in
      register (id, any BaseId)
   |  evaluate (id, any Proposal)
   |  achieve (id, any Proposal)
   |  forward (id, any Request)
   |  askall (id, any Request) -> return id
   |  any -> raise UNEXPECTED
   end case
end function

function inreplyto (m: Message): Id is
   case m
   var id: Id in
      deny (id)
   |  reply (id, any Answer)
   |  error (id)
   |  notify (id, any Answer)
   |  poolnotify (id, any Answer)
   |  pooldeny (id) -> return id
   |  any -> raise UNEXPECTED
   end case
end function

function content (m: Message): BaseId is
   return m.b
   -- i.e., if m is register (id, b) then return b else raise UNEXPECTED
end function

function content (m: Message): Proposal is
   return m.p
   -- i.e., if m is evaluate (id, p) or achieve (id, p) or tell (p) then
   -- return p else raise UNEXPECTED
end function

function content (m: Message): Request is
   return m.r
   -- i.e., if m is forward (id, r) or askall (id, r) then return r else
   -- raise UNEXPECTED
end function

function content (m: Message): Answer is
   return m.a
   -- i.e., if m is reply (id, a) or notify (id, a) or poolnotify (id, a)
   -- then return a else raise UNEXPECTED
end function

-------------------------------------------------------------------------------

type UserAction is
   doregister, doevaluate, doachieve, doforward, dodeny, doaccept, doreject,
   dochallenge
   with ==, <>
end type

-------------------------------------------------------------------------------

type SignalVal is
   sigregistered, sigstored, signotinA, signotinP, signotinC, signotconsistent
   with ==, <>
end type

-------------------------------------------------------------------------------

type SubmittedEntry is
   submitted (id: Id, r: Request)
   with ==, <>, get
end type

function id (s: SubmittedEntry): Id is
   return s.id
end function

function req (s: SubmittedEntry): Request is
   return s.r
end function

-------------------------------------------------------------------------------

type SubmittedTbl is
   nil,
   cons (s: SubmittedEntry, t: SubmittedTbl)
   with ==, <>
end type

function Insert (s: SubmittedEntry, t: SubmittedTbl): SubmittedTbl is
   case t
   var s2: SubmittedEntry, t2: SubmittedTbl in
      nil -> return cons (s, nil)
   |  cons (s2, t2) ->
         if id (s2) == id (s) then
            return cons (s, t2)
         else
            return cons (s2, Insert (s, t2))
         end if
   end case
end function

function Remove (id: Id, t: SubmittedTbl): SubmittedTbl is
   case t
   var s: SubmittedEntry, t2: SubmittedTbl in
      nil -> return nil
   |  cons (s, t2) ->
         if id (s) == id then
            return t2
         else
            return cons (s, Remove (id, t2))
         end if
   end case
end function

function Get (id: Id, t: SubmittedTbl): SubmittedEntry is
   case t
   var s: SubmittedEntry, t2: SubmittedTbl in
      nil -> raise UNEXPECTED
   |  cons (s, t2) ->
          if id (s) == id then
             return s
          else
             return Get (id, t2)
          end if
   end case
end function

function IsIn (id: Id, t: SubmittedTbl): Bool is
   case t
   var s: SubmittedEntry, t2: SubmittedTbl in
      nil -> return false
   |  cons (s, t2) ->
      if id (s) == id then
         return true
      else
         return IsIn (id, t2)
      end if
   end case
end function

-------------------------------------------------------------------------------

type GrpSubmittedEntry is
   submitted (id: Id, r: Request, b: BaseId, id2: Id)
   with ==, <>, get
end type

function id (s: GrpSubmittedEntry): Id is
   return s.id
end function

function req (s: GrpSubmittedEntry): Request is
   return s.r
end function

function sender (s: GrpSubmittedEntry): BaseId is
   return s.b
end function

function senderid (s: GrpSubmittedEntry): Id is
   return s.id2
end function

-------------------------------------------------------------------------------

type GrpSubmittedTbl is
   nil,
   cons (s: GrpSubmittedEntry, t: GrpSubmittedTbl)
   with ==, <>
end type

function Insert (s: GrpSubmittedEntry, t: GrpSubmittedTbl): GrpSubmittedTbl is
   case t
   var s2: GrpSubmittedEntry, t2: GrpSubmittedTbl in
      nil -> return cons (s, nil)
   |  cons (s2, t2) ->
         if id (s2) == id (s) then
            return cons (s,t2)
         else
            return cons (s2, Insert (s, t2))
         end if
   end case
end function

function Remove (id: Id, t: GrpSubmittedTbl): GrpSubmittedTbl is
   case t
   var s: GrpSubmittedEntry, t2: GrpSubmittedTbl in
      nil -> return nil
   |  cons (s, t2) ->
         if id == id (s) then
            return t2
         else
            return cons (s, Remove (id, t2))
         end if
   end case
end function

function Get (id: Id, t: GrpSubmittedTbl): GrpSubmittedEntry is
   case t
   var s: GrpSubmittedEntry, t2: GrpSubmittedTbl in
      nil -> raise UNEXPECTED
   |  cons (s, t2) ->
         if id == id (s) then
            return s
         else
            return Get (id, t2)
         end if
   end case
end function

function IsIn (id: Id, t: GrpSubmittedTbl): Bool is
   case t
   var s: GrpSubmittedEntry, t2: GrpSubmittedTbl in
      nil -> return false
   |  cons (s, t2) ->
         if id == id (s) then
            return true
         else
            return IsIn (id, t2)
         end if
   end case
end function

-------------------------------------------------------------------------------

type Status is
   new, accepted, rejected, challenged
   with ==, <>
end type

-------------------------------------------------------------------------------

type PendingEntry is
   pending (id: Id, r: Request, s: Status)
   with ==, <>, get, set
end type

function id (s: PendingEntry): Id is
   return s.id
end function

function req (s: PendingEntry): Request is
   return s.r
end function

function status (s: PendingEntry): Status is
   return s.s
end function

function Set_status (st: Status, s: PendingEntry): PendingEntry is
   return s.{s -> st}
end function

-------------------------------------------------------------------------------

type PendingTbl is
   nil,
   cons (s: PendingEntry, t: PendingTbl)
   with ==, <>
end type

function Insert (s: PendingEntry, t: PendingTbl): PendingTbl is
   case t
   var s2: PendingEntry, t2: PendingTbl in
      nil -> return cons (s, nil)
   |  cons (s2, t2) ->
         if id (s2) == id (s) then
            return cons (s,t2)
         else
            return cons (s2, Insert (s, t2))
         end if
   end case
end function

function Remove (id: Id, t: PendingTbl): PendingTbl is
   case t
   var s: PendingEntry, t2: PendingTbl in
      nil -> return nil
   |  cons (s, t2) ->
         if id (s) == id then
            return t2
         else
            return cons (s, Remove (id, t2))
         end if
   end case
end function

function Get (id: Id, t: PendingTbl): PendingEntry is
   case t
   var s: PendingEntry, t2: PendingTbl in
      nil -> raise UNEXPECTED
   |  cons (s, t2) ->
         if id (s) == id then
            return s
         else
            return Get (id, t2)
         end if
   end case
end function

function IsIn (id: Id, t: PendingTbl): Bool is
   case t
   var s: PendingEntry, t2: PendingTbl in
      nil -> return false
   |  cons (s, t2) ->
         if id (s) == id then
            return true
         else
            return IsIn (id, t2)
         end if
   end case
end function

-------------------------------------------------------------------------------

type SubscriberSet is
   set of BaseId
   with ==, <>, remove, member, card, head, subset
end type

function IsIn (a: BaseId, K: SubscriberSet): Bool is
   return member (a, K)
end function

function Includes (K1,K2: SubscriberSet): Bool is
   return subset (K2, K1)
end function

function pick (K: SubscriberSet): BaseId is
    return head (K) -- raises UNEXPECTED if K == {}
end function

-------------------------------------------------------------------------------

type CfcEntry is
   cfc (id: Id, b: BaseId, id2: Id, req: Request, val: Nat)
   with ==, <>, get, set
end type

function id (c: CfcEntry): Id is
   return c.id
end function

function sender (c: CfcEntry): BaseId is
   return c.b
end function

function senderid (c: CfcEntry): Id is
   return c.id2
end function

function req (c: CfcEntry): Request is
   return c.req
end function

function count (c: CfcEntry): Nat is
   return c.val
end function

function Set_count (count: Nat, c: CfcEntry): CfcEntry is
   return c.{val -> count}
end function

-------------------------------------------------------------------------------

type CfcTbl is
   nil,
   cons (s: CfcEntry, t: CfcTbl)
   with ==, <>, get
end type

function Insert (s: CfcEntry, t: CfcTbl): CfcTbl is
   case t
   var s2: CfcEntry, t2: CfcTbl in
      nil -> return cons (s, nil)
   |  cons (s2, t2) ->
         if id (s2) == id (s) then
            return cons (s,t2)
         else
            return cons (s2, Insert (s, t2))
         end if
   end case
end function

function Remove (id: Id, t: CfcTbl): CfcTbl is
   case t
   var s: CfcEntry, t2: CfcTbl in
      nil -> return nil
   |  cons (s, t2) ->
         if id == id (s) then
            return t2
         else
            return cons (s, Remove (id, t2))
         end if
   end case
end function

function Get (id: Id, t: CfcTbl): CfcEntry is
   case t
   var s: CfcEntry, t2: CfcTbl in
      nil -> raise UNEXPECTED
   |  cons (s, t2) ->
         if id == id (s) then
            return s
         else
            return Get (id, t2)
         end if
   end case
end function

function IsIn (id: Id, t: CfcTbl): Bool is
   case t
   var s: CfcEntry, t2: CfcTbl in
      nil -> return false
   |  cons (s, t2) ->
         if id == id (s) then
            return true
         else
            return IsIn (id, t2)
         end if
   end case
end function

function Test (s: CfcEntry, t: CfcTbl): Bool is
   case t
   var s2: CfcEntry, t2: CfcTbl in
      nil -> return false
   |  cons (s2, t2) ->
         if s2 == s then
            return true
         elsif id (s) == id (s2) then
            return false
         else
            return Test (s, t2)
         end if
   end case
end function

function Includes (t1, t2: CfcTbl): Bool is
   case t2
   var s: CfcEntry, t3: CfcTbl in
      nil -> return true
   |  cons (s, t3) -> return Test (s, t1) and Includes (t1, t3)
   end case
end function

function pick (t: CfcTbl): CfcEntry is
   return t.s -- raises UNEXPECTED if t == {}
end function

function searchrequest (b: BaseId, id: Id, t: CfcTbl): Bool is
   case t
   var s: CfcEntry, t2: CfcTbl in
      nil -> return false
   |  cons (s, t2) ->
         if (sender (s) == b) and (senderid (s) == id) then
            return true
         else
            return searchrequest (b, id, t2)
         end if
   end case
end function

function getrequest (b: BaseId, id: Id, t: CfcTbl): CfcEntry is
   case t
   var s: CfcEntry, t2: CfcTbl in
      nil -> raise UNEXPECTED
   |  cons (s, t2) ->
         if (sender (s) == b) and (senderid (s) == id) then
            return s
         else
            return getrequest (b, id, t2)
         end if
   end case
end function

function incallcount (t: CfcTbl): CfcTbl is
   case t
   var s: CfcEntry, t2: CfcTbl in
      nil -> return nil
   |  cons (s, t2) ->
         return insert (set_count (succ (count (s)), s), incallcount (t2))
   end case
end function

-------------------------------------------------------------------------------

type ParentBase is
   Some (b: BaseId),
   None
   with ==, <>, get
end type

function isSome (p: ParentBase): Bool is
   return p <> None
end function

function isNone (p: ParentBase): Bool is
   return p == None
end function

function the (p: ParentBase): BaseId is
   return p.b  -- raises UNEXPECTED if p == {}
end function

-------------------------------------------------------------------------------

type Packet is
   packet (b1: BaseId, b2: BaseId, m: Message)
   with ==, <>, get
end type

function sender (p: Packet): BaseId is
   return p.b1
end function

function receiver (p: Packet): BaseId is
   return p.b2
end function

function message (p: Packet): Message is
   return p.m
end function

-------------------------------------------------------------------------------

type PacketQueue is
   list of Packet
   with ==, <>, append, head, tail
end type

function + (q: PacketQueue, p: Packet): PacketQueue is
   return append (p, q)
end function

function First (q: PacketQueue): Packet is
   return head (q)  -- raises UNEXPECTED if q == {}
end function

function ButFirst (q: PacketQueue): PacketQueue is
   return tail (q)  -- raises UNEXPECTED if q == {}
end function

-------------------------------------------------------------------------------

end module