( load "mon.met" )
;---------------------

( load "int.met" )
;---------------------

( load "ff.met" )
;---------------------

( load "tex.met" )
;---------------------
;N mse.cam - a CAMILA library for multisets
;A J.N. Oliveira (jno@di.uminho.pt)
;D
; This library provides an algebra of multisets, that is, of
; the F(X)=X->NAT data type functor,
; which can be regarded as an X-dimensional semi-vectorial space.
; Multisets are very useful devices in formal specification
; which stand half-way in between the X-set and X-seq abstractions.
;E
;
; mseMax(m,n) is the monoidal extension of NAT max to multisets.
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote mseMax )
        ( quote
          (
            (
              ( FF A NAT )
              ( FF A NAT )
            )
            ( FF A NAT )
          )
        )
      )
    )
  )
)
;---------------------

( def mseMax lambda
  ( m n )
  ( monff m n max )
)
;---------------------
;
; mseCup(m,n) is the multiset union of two multisets (cf. vector addition).
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote mseCup )
        ( quote
          (
            (
              ( FF A NAT )
              ( FF A NAT )
            )
            ( FF A NAT )
          )
        )
      )
    )
  )
)
;---------------------

( def mseCup lambda
  ( m n )
  ( monff m n add )
)
;---------------------
;
; mseDiff(m,n) yields the multiset difference between two multisets.
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote mseDiff )
        ( quote
          (
            (
              ( FF A NAT )
              ( FF A NAT )
            )
            ( FF A NAT )
          )
        )
      )
    )
  )
)
;---------------------

( def mseDiff lambda
  ( m n )
  ( plus
    ( ds m
      ( dom n )
    )
    ( ff1
      ( list a
        ( sub
          ( ap m a )
          ( ap n a )
        )
      )
      ( from a
        ( intersection
          ( dom m )
          ( dom n )
        )
        ( gt
          ( ap m a )
          ( ap n a )
        )
      )
    )
  )
)
;---------------------
;
; mseExMul(m,n) is the multiset external multiplication operation
; (cf. vector spaces).
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote mseExMul )
        ( quote
          (
            (
              ( FF A NAT )
              ( NAT )
            )
            ( FF A NAT )
          )
        )
      )
    )
  )
)
;---------------------

( def mseExMul lambda
  ( m n )
  ( let
    (
      ( f
        ( lambda
          ( x )
          ( mul x n )
        )
      )
    )
    (
      ( lambda
        ( _y_ )
        ( ff1
          ( list _x_
            ( f
              ( ap _y_ _x_ )
            )
          )
          ( from _x_
            ( dom _y_ )
          )
        )
      ) m
    )
  )
)
;---------------------
;
; mseCUP(l) extends mseCup to sequences of multisets.
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote mseCUP )
        ( quote
          (
            (
              ( LIST FF A NAT )
            )
            ( FF A NAT )
          )
        )
      )
    )
  )
)
;---------------------

( def mseCUP lambda
  ( l )
  ( reduce
    ( makeff ) mseCup l
  )
)
;---------------------
;
; mseMul(m,n):A->Nat is the monoidal extension of NAT product to multisets.
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote mseMul )
        ( quote
          (
            (
              ( FF A NAT )
              ( FF A NAT )
            )
            ( FF A Nat )
          )
        )
      )
    )
  )
)
;---------------------

( def mseMul lambda
  ( m n )
  ( monff m n mul )
)
;---------------------
;
; mseSumRan(f) computes de "cardinal" of a multiset f.
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote mseSumRan )
        ( quote
          (
            (
              ( FF A NAT )
            )
            ( NAT )
          )
        )
      )
    )
  )
)
;---------------------

( def mseSumRan lambda
  ( f )
  ( intSUM
    ( seq
      ( ap f x )
      ( from x
        ( dom f )
      )
    )
  )
)
;---------------------
;
; mseWam(ms,p) computes a NAT-multiset weighted average, where
; p may add precision to the computation (see int.cam about the
; limited scope of NAT or INT in CAMILA).
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote mseWam )
        ( quote
          (
            (
              ( FF NAT NAT )
              ( NAT )
            )
            ( NAT )
          )
        )
      )
    )
  )
)
;---------------------

( def mseWam lambda
  ( ms p )
  ( div
    ( intSUM
      ( seq
        ( mul
          ( mul
            ( ap ms n ) n
          )
          ( intPot 10 p )
        )
        ( from n
          ( dom ms )
        )
      )
    )
    ( mseSumRan ms )
  )
)
;---------------------
;
; msePerc(ms:A->NAT):A->NAT
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote msePerc )
        ( quote
          (
            (
              ( FF A NAT )
            )
            ( FF A NAT )
          )
        )
      )
    )
  )
)
;---------------------

( def msePerc lambda
  ( ms )
  ( let
    (
      ( t
        ( mseSumRan ms )
      )
    )
    ( ff1
      ( list x
        ( perc
          ( ap ms x ) t
        )
      )
      ( from x
        ( dom ms )
      )
    )
  )
)
;---------------------
;
; mseUnif(ms,ff) provides for multiset consolidation in which
; ms is the target multiset and ff acts as a classification device.
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote mseUnif )
        ( quote
          (
            (
              ( FF A NAT )
              ( FF A A )
            )
            ( FF A NAT )
          )
        )
      )
    )
  )
)
;---------------------

( def mseUnif lambda
  ( ms ff )
  ( let
    (
      ( f
        ( ffinv ff )
      )
    )
    ( ff1
      ( list x
        ( mseSumRan
          ( dr ms
            ( ap f x )
          )
        )
      )
      ( from x
        ( dom f )
      )
    )
  )
)
;---------------------
;
; mseCupSeq(l,n) computes "seq-functorial" mseCup on pairs of lists of
; msets.
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote mseCupSeq )
        ( quote
          (
            (
              ( LIST FF A NAT )
              ( LIST FF A NAT )
            )
            ( LIST FF A NAT )
          )
        )
      )
    )
  )
)
;---------------------

( def mseCupSeq lambda
  ( l n )
  ( monseq l n mseCup )
)
;---------------------
;
; mseCUPSEQ(l) extends mseCupSeq to sequences of multiset sequences.
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote mseCUPSEQ )
        ( quote
          (
            (
              ( LIST LIST FF A NAT )
            )
            ( LIST FF A NAT )
          )
        )
      )
    )
  )
)
;---------------------

( def mseCUPSEQ lambda
  ( l )
  ( reduce
    ( makeseq ) mseCupSeq l
  )
)
;---------------------
;
; mse2TeXbarenv(ms) builds a LaTeX barenv environment based picture of a
; multiset ms.
;
;
; \unitlength=.27mm recommended
;
;      < TeXCmd("setxaxis",<0,card(dom(ms)),1>)> ^

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote mse2TeXbarenv )
        ( quote
          (
            (
              ( FF A NAT )
            )
            ( TeX )
          )
        )
      )
    )
  )
)
;---------------------

( def mse2TeXbarenv lambda
  ( ms )
  ( append
    ( append
      ( append
        ( append
          ( append
            ( makeseq
              ( TeXCmd "begin"
                ( makeseq "barenv" )
              )
            )
            ( makeseq
              ( TeXCmd "setdepth"
                ( makeseq 14 )
              )
            )
          )
          ( makeseq
            ( TeXCmd "setstretch"
              ( makeseq "5.0" )
            )
          )
        )
        ( makeseq
          ( TeXCmd "setyaxis"
            ( makeseq 0
              ( let
                (
                  ( m
                    ( intMAX
                      ( ran ms )
                    )
                  )
                )
                ( mul
                  ( add
                    ( div m 10 ) 1
                  ) 10
                )
              ) 5
            )
          )
        )
      )
      ( seq
        ( TeXCmd "bar"
          ( makeseq
            ( ap ms x ) 1
            ( Opt x )
          )
        )
        ( from x
          ( dom ms )
        )
      )
    )
    ( makeseq
      ( TeXCmd "end"
        ( makeseq "barenv" )
      )
    )
  )
)
;---------------------