-- ========================================================================
--                           PNAT*, QUEUE, SET 
-- ========================================================================

-- ========================================================================
-- a comment starts with '-- ' or '** ' and ends at the end of line
--
-- a convention for commenting:
--   '-- ' is used before the commented CafeOBJ text
--   '** ' is used after the commented CafeOBJ text
-- ========================================================================

-- ========================================================================
require pnat

-- ========================================================================
-- enhancing Peano Style Natural Numbers with multiplication function
mod! PNAT* {pr(PNAT)
  -- associative and commutative _*_ (times)
  op _*_ : Nat Nat -> Nat {assoc comm} .
  eq 0 * Y:Nat = 0 .
  eq (s X:Nat) * Y:Nat = Y + (X * Y) . 
}

-- ========================================================================
-- mod* TRIV {[Elt]} is a bulit-in module
-- generic (or parameterized) queue (first in first out storage)
mod! QUEUE (X :: TRIV) {
** (X :: TRIV) declares the parameter module X should be an instance
** of the module TRIV
-- elements and their queues, Elt comes from (X :: TRIV)
[Elt.X < Qu]
** an element in Elt is an element in Qu
-- declaration of a constructor constant
op empQ : -> Qu {constr}   ** empty queue
-- assoicative queue constructors with id: empQ
op _&_ : Qu Qu -> Qu {constr assoc id: empQ} 
-- equality _=_ over the sort Qu
-- _=_ is defined for each sort in the built-in module EQL
-- and EQL is imported to each module automatically
eq (empQ = (E:Elt & Q:Qu)) = false .
ceq ((E1:Elt & Q1:Qu) = (E2:Elt & Q2:Qu)) = ((E1 = E2) and (Q1 = Q2))
    if not((Q1 = empQ) and (Q2 = empQ)) .
}
** head and tail operations on queues are not defined here
** they are defined in module AID-QUEUE-a in the file qlock-prop.cafe
** the module QUEUE just defines generic sequences

-- ========================================================================
-- generic sets
mod! SET(X :: TRIV) { [Elt.X < Set]
-- empty set
op empty : -> Set {constr}
-- assicative and commutative set constructor with identity
op _ _ : Set Set -> Set {constr assoc comm id: empty}
-- '_ _' is idempotent with respect to the sort Elt
eq E:Elt E S:Set = E S .
}

-- ========================================================================
provide qlock-natQuSet

-- ========================================================================
eof