;N mon.cam - basic CAMILA monoidal constructions
;A J.N. Oliveira (jno@di.uminho.pt)
;D
; This small library provides two basic monoidal constructs which prove
; useful many specification contexts.
; The basic idea is to scale up monoidal computations in a compositional
; and functorial way.
;E
;
; monff(m,n,f) is a higher-order function extending a binary monoidal
; operation f to the F(X)=A->X functor.
; monff(m,n,f) is itself a monoidal operator.
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote monff )
        ( quote
          (
            (
              ( FF A B )
              ( FF A B )
              ( FF BxB B )
            )
            ( FF A B )
          )
        )
      )
    )
  )
)
;---------------------

( def monff lambda
  ( m n f )
  ( plus
    ( plus m n )
    ( ff1
      ( list a
        ( f
          ( ap m a )
          ( ap n a )
        )
      )
      ( from a
        ( intersection
          ( dom m )
          ( dom n )
        )
      )
    )
  )
)
;---------------------
;
; monseq(m,n,f) is a higher-order function extending a binary monoidal
; operation f to the F(X)=X-seq functor.
; monseq(m,n,f) is itself a monoidal operator.
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote monseq )
        ( quote
          (
            (
              ( LIST B )
              ( LIST B )
              ( FF BxB B )
            )
            ( LIST B )
          )
        )
      )
    )
  )
)
;---------------------

( def monseq lambda
  ( l r f )
  ( if
    ( equal l
      ( makeseq )
    )
    ( makeseq )
    ( if
      ( equal r
        ( makeseq )
      ) l
      ( append
        ( makeseq
          ( f
            ( head l )
            ( head r )
          )
        )
        ( monseq
          ( tail l )
          ( tail r ) f
        )
      )
    )
  )
)
;---------------------