-- ===========================
-- ===========================
--  Specification of Entities
-- ===========================
-- ===========================
-- Bool with equality
mod! EQBOOL {
  pr ( EQL )

  -- error operator
  op noBool : -> Bool
  -- equality
--  op _=_ : Bool Bool -> Bool { assoc comm }

  var B : Bool
--  eq (B = B) = true .
  eq (true = false) = false .
  eq (true = noBool) = false .
  eq (false = noBool) = false .
}

-- TRIV with error operator
mod* TRIV-EQL {
  pr ( EQL )
  [ Elt ]

  -- error operator
  op noElt : -> Elt
}

-- set
mod! SET (X :: TRIV-EQL){
  [ Elt < Set ]

  op empty : -> Set
  op _ _ : Set Set -> Set { assoc comm idem idr: empty }
  op in? : Elt Set -> Bool 
  op add : Elt Set -> Set
  op delete : Elt Set -> Set 
  op get : Elt Set -> Elt

  vars E E' : Elt
  vars S S' : Set
--
  eq (E = empty) = false .
  eq ((E S) = empty) = false .
-- in?
  eq in?(E, empty) = false .
  eq in?(E, E') = (E = E') .
  eq in?(E, (E S)) = true .
  ceq in?(E, (E' S)) = in?(E, S)
      if not(E = E') .
-- add
  eq add(E, empty) = E .
  eq add(E, E) = E .
  ceq add(E, E') = (E E')
      if not(E = E') .
  eq add(E, S) = (E S) .
  ceq add(E, S) = S
      if in?(E, S) .
-- delete
  eq delete(E, empty) = empty .
  eq delete(E, E) = empty .
  ceq delete(E, E') = E'
      if not(E = E') .
  eq delete(E, (E S)) = S .
  ceq delete(E, S) = S 
      if not(in?(E, S)) .
-- get
  eq get(E, empty) = noElt .
  eq get(E, E) = E .
  ceq get(E, E') = noElt
      if not(E = E') .
  eq get(E, (E S)) = E .
  ceq get(E, S) = noElt
      if not(in?(E, S)) .
}
"[
-- test
open SET 
ops e1 e2 e3 : -> Elt .
eq (e1 = e2) = false .
eq (e1 = e3) = false .
eq (e2 = e3) = false .
red (e1 e1 e1) .
red (e1 = e1) .
red (e1 = (e1 e1)) .
--> test for in?
red in?(e1, empty) .
red in?(e1, e1) .
red in?(e1, e2) .
red in?(e1, (e1 e2 e3)) .
red in?(e1, (e2 e3 e1)) .
red in?(e1, (e3 e2 e1)) .
red in?(e1, (e3 e1 e2)) .
red in?(e1, (e2 e1 e3)) .
red in?(e1, (e2 e3)) .
--> test for delete
red delete(e1, empty) .
red delete(e1, e1) .
red delete(e1, e2) .
red delete(e1, (e1 e2 e3)) .
red delete(e1, (e2 e3 e1)) .
red delete(e1, (e3 e2 e1)) .
red delete(e1, (e3 e1 e2)) .
red delete(e1, (e2 e1 e3)) .
red delete(e1, (e2 e3)) .

close

eof
]"

          
mod! LIST (X :: TRIV-EQL){
  pr ( EQL )
  [ List ] 

  op nill : -> List
  op _;_ : Elt List -> List
  op add : Elt List -> List
  op top : List -> Elt
  op bottom : List -> List
  op delete : Elt List -> List
  op in? : Elt List -> Bool

  vars E E' : Elt
  var L : List
  eq ((E ; L) = nill) = false .
  eq (noElt ; nill) = nill .
  eq top(nill) = noElt .
  eq top(E ; L) = E .
  eq bottom(nill) = nill .
  eq bottom(E ; L) = L .
  eq add(E, L) = (E ; L) .
  eq delete(E, nill) = nill .
  eq delete(E, (E' ; L)) = if (E = E') then L
                         else (E' ; delete(E, L)) fi .
  eq in?(E, nill) = false .
  eq in?(E, (E' ; L)) = if (E = E') then true
                      else in?(E, L) fi .
}



-- =================================================
-- Entities related to businesses
-- 
-- Division
-- *************************************************
-- a division is either a department, a client, a partner, 
-- or a supplier.
mod! DIVISION {
  pr ( EQL )
  [ Department < Division ]

  -- departments
  ops sales sales-admin shipping : -> Department
  -- outside of the company
  ops client partner supplier : -> Division
  -- error operator
  op noDivision : -> Division

  var D : Division
  eq (sales = sales-admin) = false .
  eq (sales = shipping) = false .
  eq (sales = client) = false .
  eq (sales = partner) = false .
  eq (sales = supplier) = false .
  eq (sales = noDivision) = false .
  eq (sales-admin = shipping) = false .
  eq (sales-admin = client) = false .
  eq (sales-admin = partner) = false .
  eq (sales-admin = supplier) = false .
  eq (sales-admin = noDivision) = false .
  eq (shipping = client) = false .
  eq (shipping = partner) = false .
  eq (shipping = supplier) = false .
  eq (shipping = noDivision) = false .
  eq (client = partner) = false .
  eq (client = supplier) = false .
  eq (client = noDivision) = false .
  eq (partner = supplier) = false .
  eq (partner = noDivision) = false .
  eq (supplier = noDivision) = false .
}
--
-- set of divisions
mod! DIVISIONSET {
  pr ( SET (X <= view to DIVISION
              { sort Elt -> Division,
                op noElt -> noDivision } )
          * { sort Set -> DivisionSet,
              op empty -> emptyD } )
}

-- *************************************************
--
-- Document
-- *************************************************
-- a document has document ID, document type, 
-- a boolean value, and evidence history.
-- the boolean value shows authenticity of the document.
--
-- document type
-- --------------------------------------
mod* DOCUMENTID {
  pr ( EQL )
  [ DocumentID ]

  -- for carboncopy
  op cc : DocumentID -> DocumentID
  -- error operator
  op noDocumentID : -> DocumentID
  -- 
  op is-cc? : DocumentID -> Bool

  var D : DocumentID
  eq is-cc?(cc(D)) = true .
  eq is-cc?(noDocumentID) = false .
  eq (cc(D) = D) = false .
  eq cc(noDocumentID) = noDocumentID .

}
--
-- set of docuemnt IDs
mod! DOCUMENTIDSET {
  pr ( SET (X <= view to DOCUMENTID
              { sort Elt -> DocumentID,
                op noElt -> noDocumentID } )
          * { sort Set -> DocumentIDSet,
              op empty -> emptyDID } )
}
--
-- list of document IDs
mod! DOCUMENTIDLIST {
  pr ( LIST (X <= view to DOCUMENTID
              { sort Elt -> DocumentID,
                op noElt -> noDocumentID } )
          * { sort List -> DocumentIDList,
              op nill -> nillDID } )
}
--
-- --------------------------------------
--
-- document type
-- --------------------------------------
mod! DOCUMENTTYPE {
  pr ( EQL )
  [ DocumentType ]

  -- orderは注文書，order-reportは受注票，
  -- invoiceは確認用の書類を表す

  ops order report invoice ack 
      receipt request : -> DocumentType
  -- error operator
  op noDocumentType : -> DocumentType
  -- カーボンコピーのドキュメントタイプは
  -- cc : DocumentType -> DocumentType
  -- で表す　
  -- carbon copy
  op cc : DocumentType -> DocumentType { constr }
  -- checking if a document is a carbon copy
  op is-cc? : DocumentType -> Bool

  vars T T1 T2 : DocumentType
  eq cc(noDocumentType) = noDocumentType .
  -- is-cc?
  eq is-cc?(cc(T)) = true .
  eq is-cc?(order) = false .
  eq is-cc?(report) = false .
  eq is-cc?(invoice) = false .
  eq is-cc?(ack) = false .
  eq is-cc?(receipt) = false .
  eq is-cc?(request) = false .
  eq is-cc?(noDocumentType) = false .
  -- equality
  eq (cc(T1) = cc(T2)) = (T1 = T2) .
  eq (order = report) = false .
  eq (order = invoice) = false .
  eq (order = ack) = false .
  eq (order = receipt) = false .
  eq (order = request) = false .
  eq (order = cc(T)) = false .
  eq (order = noDocumentType) = false .
  eq (report = invoice) = false .
  eq (report = ack) = false .
  eq (report = receipt) = false .
  eq (report = request) = false .
  eq (report = cc(T)) = false .
  eq (report = noDocumentType) = false .
  eq (invoice = ack) = false .
  eq (invoice = receipt) = false .
  eq (invoice = request) = false .
  eq (invoice = cc(T)) = false .
  eq (invoice = noDocumentType) = false .
  eq (ack = receipt) = false .
  eq (ack = request) = false .
  eq (ack = cc(T)) = false .
  eq (ack = noDocumentType) = false .
  eq (receipt = request) = false .
  eq (receipt = cc(T)) = false .
  eq (receipt = noDocumentType) = false .
  eq (request = cc(T)) = false .
  eq (request = noDocumentType) = false .
  eq (cc(T) = noDocumentType) = false .
--
}
--
-- set of docuemnt types
mod! DOCUMENTTYPESET {
  pr ( SET (X <= view to DOCUMENTTYPE
              { sort Elt -> DocumentType,
                op noElt -> noDocumentType } )
          * { sort Set -> DocumentTypeSet,
              op empty -> emptyDT } )
}
--
-- pair of document ID and type
mod! DOCUMENTIDANDTYPE {
  pr ( DOCUMENTID + DOCUMENTTYPE )
  [ DocumentID&Type ]

  -- constructor
  op _,_ : DocumentID DocumentType -> DocumentID&Type { constr }
  -- error operator
  op noDocumentID&Type : -> DocumentID&Type
--
  -- getting document ID
  op getDocumentID : DocumentID&Type -> DocumentID
  -- getting document type
  op getDocumentType : DocumentID&Type -> DocumentType

  var D : DocumentID
  var T : DocumentType
  var DT : DocumentID&Type
  eq (DT = noDocumentID&Type) = false .
  eq getDocumentID((D, T)) = D .
  eq getDocumentType((D, T)) = T .
}
--
-- set of DocumentID&Type
mod! DOCUMENTIDANDTYPESET {
  pr ( SET (X <= view to DOCUMENTIDANDTYPE
              { sort Elt -> DocumentID&Type,
                op noElt -> noDocumentID&Type } )
          * { sort Set -> DocumentID&TypeSet,
              op empty -> emptyDIT } )

  op in? : DocumentID DocumentID&TypeSet -> Bool
  op in? : DocumentType DocumentID&TypeSet -> Bool
  op getDocumentID : DocumentType DocumentID&TypeSet
                     -> DocumentID
  op getDocumentType : DocumentID DocumentID&TypeSet
                       -> DocumentType

  var D : DocumentID 
  var T : DocumentType
  var DT : DocumentID&Type
  var S :  DocumentID&TypeSet
  -- in?
  eq in?(D, emptyDIT) = false .
  eq in?(D, DT) = (D = getDocumentID(DT)) .
  ceq in?(D, (DT S)) = true
      if (D = getDocumentID(DT)) .
  ceq in?(D, (DT S)) = in?(D, S)
      if not(D = getDocumentID(DT)) .
  --
  eq in?(T, emptyDIT) = false .
  eq in?(T, DT) = (T = getDocumentType(DT)) .
  ceq in?(T, (DT S)) = true
      if (T = getDocumentType(DT)) .
  ceq in?(T, (DT S)) = in?(T, S)
      if not(T = getDocumentType(DT)) .
--
  -- getDocumentID
  eq getDocumentID(T, emptyDIT) = noDocumentID .
  ceq getDocumentID(T, DT) = getDocumentID(DT)
      if (T = getDocumentType(DT)) .
  ceq getDocumentID(T, DT) = noDocumentID
      if not(T = getDocumentType(DT)) .
  ceq getDocumentID(T, (DT S)) = getDocumentID(DT)
      if (T = getDocumentType(DT)) .
  ceq getDocumentID(T, S) = noDocumentID
      if not(in?(T, S)) .
--
  -- getDocumentType
  eq getDocumentType(D, emptyDIT) = noDocumentType .
  ceq getDocumentType(D, DT) = getDocumentType(DT)
      if (D = getDocumentID(DT)) .
  ceq getDocumentType(D, DT) = noDocumentType
      if not(D = getDocumentID(DT)) .
  ceq getDocumentType(D, (DT S)) = getDocumentType(DT)
      if (D = getDocumentID(DT)) .
  ceq getDocumentType(D, S) = noDocumentType
      if not(in?(D, S)) .
}
--
"[
-- test
open DOCUMENTIDANDTYPESET
ops d1 d2 d3 : -> DocumentID .
ops t1 t2 t3 : -> DocumentType .
eq (d1 = d2) = false .
eq (d1 = d3) = false .
eq (d2 = d3) = false .
eq (t1 = t2) = false .
eq (t1 = t3) = false .
eq (t2 = t3) = false .
red in?(d1, emptyDIT) .
red in?(d1, (d1, t1)) .
red in?(d1, (d2, t2)) .
red in?(d1, ((d1, t1) (d2, t2) (d3, t3))) .
red in?(d1, ((d3, t3) (d2, t2) (d1, t1))) .
red in?(d1, ((d3, t3) (d1, t1) (d2, t2))) .
red in?(d1, ((d3, t3) (d2, t2))) .
red getDocumentType(d1, emptyDIT) .
red getDocumentType(d1, (d1, t1)) .
red getDocumentType(d1, (d2, t2)) .
red getDocumentType(d1, ((d1, t1) (d2, t2) (d3, t3))) .
red getDocumentType(d1, ((d2, t2) (d1, t1) (d3, t3))) .
red getDocumentType(d1, ((d3, t3) (d2, t2) (d1, t1))) .
red getDocumentType(d1, ((d2, t2) (d3, t3))) .
close
eof
]"
--
-- --------------------------------------
--
-- evidence history
-- --------------------------------------
-- evidence
mod! EVIDENCE {
  pr ( EQL + DOCUMENTTYPE + DIVISION )
  [ Evidence ]

  -- evidences which are constructed by "ch"
  -- are used when a document is checked, and
  -- ones by "apv" are used when a document is 
  -- approved.

  -- constructors
  op ch : DocumentType -> Evidence { constr }
  op apv : Division -> Evidence { constr }
  -- error operator
  op noEvidence : -> Evidence

  var D : DocumentType
  var V : Division
  eq (ch(D) = noEvidence) = false .
  eq (apv(V) = noEvidence) = false .
}
--
-- evidence history
-- an evidence history is a set of evidence
mod! EVIDENCEHISTORY {
  pr ( SET (X <= view to EVIDENCE
              { sort Elt -> Evidence,
                op noElt -> noEvidence } )
          * { sort Set -> EvidenceHistory,
              op empty -> emptyE } )
}
--
-- *************************************************
--
-- セッションID
-- *************************************************
mod* SESSIONID {
  pr ( EQL )
  [ SessionID ]

  -- error operator
  op noSessionID : -> SessionID

}
-- *************************************************

eof