;N seq.cam - a CAMILA library for the A-seq functor
;A J.N. Oliveira (jno@di.uminho.pt)
;D
; This library adds extra functionality to the CAMILA built-in 
; polymorphic finite sequence data type F(X)=X-seq.
;E
;
; seqInseg(n) is the sequence version of inseg(n).
; Thus elems(seqInseg(n)) == inseg(n).
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote seqInseg )
        ( quote
          (
            (
              ( NAT )
            )
            ( LIST NAT )
          )
        )
      )
    )
  )
)
;---------------------

( def seqInseg lambda
  ( n )
  ( if
    ( equal n 0 )
    ( makeseq )
    ( append
      ( seqInseg
        ( sub n 1 )
      )
      ( makeseq n )
    )
  )
)
;---------------------
;
; seqSubl(l,i,n) selects from l its n-element-long subsequence,
; from the ith position onwards, or as much as possible if l is too
; short.
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote seqSubl )
        ( quote
          (
            (
              ( LIST A )
              ( NAT )
              ( NAT0 )
            )
            ( LIST A )
          )
        )
      )
    )
  )
)
;---------------------

( def seqSubl lambda
  ( l i n )
  ( if
    ( equal n 0 )
    ( makeseq )
    ( if
      ( equal l
        ( makeseq )
      )
      ( makeseq )
      ( let
        (
          ( h
            ( hd l )
          )
          ( t
            ( tl l )
          )
        )
        ( if
          ( equal i 1 )
          ( append
            ( makeseq h )
            ( seqSubl t i
              ( sub n 1 )
            )
          )
          ( seqSubl t
            ( sub i 1 ) n
          )
        )
      )
    )
  )
)
;---------------------
;
; seqAddSep(l,a) inserts a as a separator in l.
; For instance, seqAddSep(<c,d,a>,a) == <c,a,d,a,a>.
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote seqAddSep )
        ( quote
          (
            (
              ( LIST A )
              ( A )
            )
            ( LIST A )
          )
        )
      )
    )
  )
)
;---------------------

( def seqAddSep lambda
  ( l a )
  ( if
    ( equal l
      ( makeseq )
    )
    ( makeseq )
    ( append
      ( makeseq
        ( hd l )
      )
      ( CONC
        ( seq
          ( makeseq a x )
          ( from x
            ( tl l )
          )
        )
      )
    )
  )
)
;---------------------
;
; seq2mset(l) converts l into the multiset of its elements.
; So, order is lost but not multiplicity.
; Thus facts
; dom(seq2mset(l)) == elems(l) and
; mseSumRan(seq2mset(l)) == length(l)
; hold.
;

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

( def seq2mset lambda
  ( l )
  ( ff1
    ( list x
      ( length
        ( seq y
          ( from y l
            ( equal y x )
          )
        )
      )
    )
    ( from x
      ( elems l )
    )
  )
)
;---------------------
;
; seqInv(l) is l in reverse order.
; Thus elems(seqInv(l)) == elems(l) and
; seqInv(seqInv(l)) == l are valid properties of seqInv.
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote seqInv )
        ( quote
          (
            (
              ( LIST A )
            )
            ( LIST A )
          )
        )
      )
    )
  )
)
;---------------------

( def seqInv lambda
  ( l )
  ( if
    ( equal l
      ( makeseq )
    )
    ( makeseq )
    ( append
      ( seqInv
        ( tl l )
      )
      ( makeseq
        ( hd l )
      )
    )
  )
)
;---------------------
;
; seqBlast(l) keeps all elements of l but the last one.
;

( def _ops
  ( plus _ops
    ( makeff
      (
        ( quote seqBlast )
        ( quote
          (
            (
              ( LIST A )
            )
            ( LIST A )
          )
        )
      )
    )
  )
)
;---------------------

( def seqBlast lambda
  ( l )
  ( seqInv
    ( tl
      ( seqInv l )
    )
  )
)
;---------------------
;
; seq2mseSeq(l) converts l into the corresponding sequence of unitary
; multisets, which may be useful in a data-mining context.
;

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

( def seq2mseSeq lambda
  ( l )
  ( seq
    ( makeff
      ( x 1 )
    )
    ( from x l )
  )
)
;---------------------
;
; seq2ff(l) converts sequence l into a finite mapping keeping track
; of the original element positions.
; Thus properties dom(seq2ff(l))==inseg(length(l))
; and seq2ff(l)[i]== l(i) hold.
;

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

( def seq2ff lambda
  ( l )
  ( ff1
    ( list x
      ( nth x l )
    )
    ( from x
      ( inseg
        ( length l )
      )
    )
  )
)
;---------------------
;
; seqSplit(l,n) partitions l into the sequence of its subsequences
; of fixed length n (except possibly the last).
; Therefore, CONC(seqSplit(l,n)) == l holds.
;

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

( def seqSplit lambda
  ( l n )
  ( let
    (
      ( c
        ( length l )
      )
      ( i
        ( div c n )
      )
      ( m
        ( if
          ( equal
            ( rem c n ) 0
          ) i
          ( add i 1 )
        )
      )
    )
    ( seq
      ( seqSubl l
        ( add
          ( mul
            ( sub j 1 ) n
          ) 1
        ) n
      )
      ( from j
        ( seqInseg m )
      )
    )
  )
)
;---------------------