! form.ax - utility predicates based on the form of expressions
! Note that there is a preference for short names!
! There may be a case for having versions of basic funcions/relations
! that cover all possible argument permutations, since the same fn/rel
! may be thought of in different ways.
! "_term" with leading _ denotes a syntactic category used for documentation
!/ index:
=> categories:
  unary fn (1 input arg gives unique result):
    id, head, tail, last, trim, rev
  binary relation (that is not a fn in either direction)
    =len, pre, suf, in, substr, copies, dupstr,  
 Argument order may need to be revised!
 Predicate definition order may need refinement!

=== sets ===
 (nonnull (% $)) - non-null sequences
  
=== unary fns / binary relations:
 (== _e _e) - identity relation
 (id _e _e) - identity function (- same as relation!)
 (head _h _seq) - first element in a sequence
 (tail _seq _t) - rest of sequence after head
 (last _seq _l) - last element in a sequence
 (trim _seq _t) - trim last elem from sequence
 (rev _seq _rev) - reverse of a sequence
 (rot (_pre_ _suf_) (_suf_ _pre_)) - "rotate" (swap) prefix/suffix of a seq
 (perm _seq1 _seq2) - sequence 2 is permutation of sequence 1
more tbd:
 (asnpre _pre _seq _seq') - assign (replace) seq prefix with new prefix
   -- asnpre| - if prefix longer than seq, we truncate prefix at seq length
      asnpre_ -                 "          prefix becomes new seq
      asnpre is asnpre| or asnpre_ ??
 (asnsuf _suf _seq _seq') - assign (replace seq suffix with new suffixd
   -- asnsuf|, asnsuf_ - analogous comments to asnpre

=== index functions where index is sequence length (func#l <lenseq> ...)
  -- see natnum.ax and decnum.ax for generalized index functions
  -- note that _pos (0..) is the prefix length before seq elem [_pos]
 (sel#l _pos _seq _elem) - select element at [_pos] in seq (0..)
 (pre#l _pos _seq _pre) - get seq prefix ending before [_pos]
 (suf#l _pos _seq _suf) - get seq suffix starting at [_pos]
 (rot#l _pos _seq _rot) - get seq rotation w suffix starting at _pos
 (asn#l _pos _seq _ex _seq') - assign expr at sequence [_pos]
 (find#l _ex _seq _pos) - find expr in sequnce -> [_pos] (nondet)
more tbd:
 (asnstr#l _pos _seq _str _seq') - assign (repl) string starting at [_pos]
   -- asnstr|, asnstr_ - analogous comments to asnpre|, asnpre_
 (insstr#l _pos _seq _str _seq') - insert string before sequence [_pos]
 (selstr#l _pos _len _seq _str) - select str w _len starting at [_pos]
   -- note that _len is sequence position numbering from [_pos]
   -- What if specified string goes beyond range of sequence??
 
=== _rpos (reverse position) indexes seq elems from the end!:
 (sel#-l _rpos _seq _elem) - select element at [_rpos] in seq (..0)
 (pre#-l _rpos _seq _pre) - get seq prefix ending w [_rpos]
 (suf#-l _rpos _seq _suf) - get seq suffix starting after _rpos
 (rot#-l _rpos _seq _rot) - get seq rotation w prefix ending at _rpos
 (asn#-l _rpos _seq _ex _seq') - assign expr at sequence [_rpos]
 (find#-l _ex _seq _rpos) - find expr in sequence -> [_pos] (nondet)
more tbd:
 ..#-l versions of the more tbd --#l functions!
 
=== more relations & functions:
 (=l _s1 _s2) - two sequences have equal length
 (<l _s1 _s2) - 1st sequence length less that 2nd
 <=l, >l, >=l - more sequence length comparison operations
 (/=l _s1 _s2) - sequence lengths not equal
 (pre _pre _seq) - 1st arg is prefix of sequence
 (suf _seq _suf) - 2nd arg is suffix of sequence
 (in _e _seq) - expression is in a sequence
 (substr _seq1 _seq2) - 1st sequence is substring of 2nd sequence
 (subseq _seq1 _seq2) - 1st seq is 2nd seq w elems removed (order kept)
 (copies _e _seq) - sequence is zero or more copies of an expression
 (dupstr _seq1 _seq2) - 2nd sequence is concatenated copies of 1st seq 
 (split _seq _half1 _half2) - split sequence into two halves
 (even_len _seq) - sequence has even-numbered length
 (odd_len _seq)  -         "     odd-        "
 (even/odd _seq _even _odd) - partition 0.. seq into even, odd elements
 (no_consec _a _b _seqab) - no consecutive a's in seq of a's & b's

=== some simple binary operations/functions (== ternary relations)

 (append1 _seq _x _seq') - append one expression to end of a sequence
 (prepend _x _seq _seq') - prepend expression to front of a sequence
 (insert _seq _x _seq') - insert expr at some (any) point in a sequence
                          ("inverse" of remove function)
 (cat _seq1 _seq2 _seq1+2) - concatenation (catenate?!) function
 (cat_ ..seqs.. _catseq) - generalization of cat to >2 input args (ho.ax?)
 (cat* (..seqs..) _catseq) - concatenation of a sequence of seqs (1-arg)
 (ldistr _x _seqs _seqs') - distribute expr over fronts of multiple seqs
 (distr _elems _seqs _seqs') - distr elements over fronts of seqs
 (all_subseqs _seq (.._subseq..)) - set of all subseqs of a sequence
 (ins_btw _x _seq _seq') - insert expr between elems of a seq
!\

!---+----1----+----2----+----3----+----4----+----5----+----6---+----7----+----8


! ====== sets ======

! nonnull - non-null sequences

! (nonnull (% $)).


! ====== some simple unary functions (- also are binary relations) ======

! == - identity relation

  (== % %).

! id - identity function

  (id % %).

  ! -- Same as == but we think of id as the identity function from argument to
  ! a result, while == is an equivalence relation for 2 identical expressions.

! head - first element in a seence

  (head (% $) %).

! tail - rest of a sequence after its head

  (tail (% $) ($)).

! last - last element in a sequence

  (last ($ %) %). 

! trim - all but the last element of a list
! (better name?:  rtail (reverse tail), body, snip,clip,chop,dock)

  (trim ($ %) ($)).

! rev - reverse a sequence

  (rev () ()).
  (rev (% $) ($rev %))<
    (rev ($) ($rev)).

! rot - "rotate" (swap) prefix/suffix of a sequence
! (rot (_pre_ _suf_) (_suf_ _pre_)) - note that this defines all rotations

  (rot ($pre $suf) ($suf $pre)).

! perm - argument sequences are permutations of each other

  (perm () ()).
  (perm (% $) ($1 % $2))<
    (perm ($) ($1 $2)).


! ====== index functions where index is sequence length (func#l <lenseq> ...)
!  -- see natnum.ax and decnum.ax for generalized index functions
!  -- note that _pos (0..) is the prefix length before seq elem [_pos]

! sel#l - select element at [_pos] in sequence (0.. indexing)
! (sel#l _pos _seq _elem) - position index defined by a sequence length

  (sel#l %pos ($pre %elem $suf) %elem)<
    (=len %pos ($pre)).    ! sequence prefix has length "position"

! pre#l - get sequence prefix ending before [_pos]

  (pre#l %pos ($pre $suf) ($pre))<
    (=len %pos ($pre)).
 
! suf#l - get sequence suffix starting at [_pos]
! (suf#l _pos _seq _suf)

  (suf#l %pos ($pre $suf) ($suf))<
    (=len %pos ($pre)).

! rot#l - get seq rotation with suffix starting at [_pos]
! (rot#l _pos _seq _rot)

  (rot#l %pos ($pre $suf) (%suf $pre))<
    (=len %pos ($pre)).

! asn#l - assign expr at sequence [_pos]
! (asn#l _pos _seq _ex _seq')

  (asn#l %pos ($pre % $suf) %expr ($pre %expr $suf))<
    (=len %pos ($pre)).
 
! find#l - find expr in sequence, giving [_pos] index (nondeterministic)
! (find#l _ex _seq _pos) - any _ex soln possible, or none if _ex not present

  (find#l %expr ($pre %expr $seq) %pos)<
    (len= ($pre) %pos).    ! any seq of prefix len can represent position index

!/
! -- defining these [_pos] predicates using a single higher-order form axiom:
!    (... but higher-order forms have not been defined at this point!)

  (ax (sel#l %pos ($pre %elem $suf) %elem)
      (pre#l %pos ($pre $suf) ($pre))
      (suf#l %pos ($pre $suf) ($suf))
      (rot#l %pos ($pre $suf) (%suf $pre))  
      (asn#l %pos ($pre % $suf) %expr ($pre %expr $suf))
      (find#l %expr ($pre %expr $seq) %pos)
      `< (len= ($pre) %pos).   ! same condition for all these predicates!
!\
      
! ---- _rpos (reverse position) indexes seq elems from the end!
!      (sequence elements are numbered n-1..0 where n is sequence length)

! sel#-l - select element at [_rpos] in sequence (reversed indexing n-1..0)
! (sel#-l _rpos _seq _elem)

  (sel#-l %rpos ($pre %elem $suf) %elem)<
    (=len %rpos ($suf)).
 
! pre#-l - get sequence prefix ending with [_rpos]
! (pre#-l _rpos _seq _pre)

  (pre#-l %rpos ($pre $suf) ($pre))<
    (=len %rpos ($suf)).
 
! suf#-l - get sequence suffix starting after [_rpos]
! (suf#-l _rpos _seq _suf)

  (suf#-1 %rpos ($pre $suf) ($suf))<
    (=len %rpos ($suf)).
  
! rot#-l - get sequence rotation w prefix ending at [_rpos]
! (rot#-l _rpos _seq _rot)

  (rot#-l %rpos ($pre $suf) ($suf $pre))<
    (=len %rpos ($suf)).
 
! asn#-l - assign expr at sequence [_rpos]
! (asn#-l _rpos _seq _ex _seq')

  (asn#-l %rpos ($pre % $suf) %expr ($pre %expr $suf))<
    (=len %rpos ($suf)).

! find#-l - find expr's reversed index in sequence -> [_rpos] (nondeterministic)
! (find#-l _ex _seq _rpos)

  (find#-l %expr ($pre %expr $suf) %rpos)<
    (=len ($suf) %rpos).

! -- above higher-order form could be used for these [_rpos] predicates,
!    assuming it was available.


! ====== more relations and functions ======
!(... in addition to == head tail last trim rev rot)

! =l - two sequences have equal length

  (=l () ()).
  (=l (%1 $1) (%2 $2))<
    (=l ($1) ($2)).
    
! <l - 1st sequence length less that 2nd

  (<l () (% $)).
  (<l (%1 $1) (%2 $2))<
    (<l ($1) ($2)).

! <=l

  (<=l %1 %2)< (=l %1 %2).
  (<=l %1 %2)< (<l %1 %2).
  ! -- or use one_valid if ho.ax is available

! >l

  (>l %2 %1)< (<l %1 %2).

! >=l

  (>=l %2 %1)< (<=l %1 %2).

! /=l - sequences with unequal length

  (/=l %1 %2)< (<l %1 %2).
  (/=l %1 %2)< (>l %1 %2).
  ! -- or use one_valid if ho.ax is available

! pre - 1st arg is prefix of sequence

  (pre ($1) ($1 $2)).

! suf - 2nd arg is suffix of sequence

  (suf ($1 $2) ($2)).

! in - expression is in a sequence

  (in % ($1 % $2)).

   !>>> This is called 'member' in traditional LP.

! substr - string is substring of a sequence

  (substr ($sub) ($1 $sub $2)).

! subseq - 1st sequence is 2nd sequence w >=0 elements removed (order kept)

  (subseq ($) ($)).     ! a sequence is a subseq of itself
  (subseq ($1 $2) ($))<   ! removing element from subseq gives subseq
    (subseq ($1 % $2) ($)).

! copies - sequence is zero or more copies of an expression

  (copies % ()).
  (copies % (% $))< (copies % ($)).

 dupstr - 2nd sequence is concatenated copies of 1st seq

   (dupstr ($) ()).
   (dupstr ($) ($ $dup))< (dupstr ($) ($dup)).

! split - split sequence into two halves
! - 1st half gets middle elem if seq length is odd

  (split ($h1 $h2) ($h1) ($h2))< (=l ($h1) ($h2)).        ! even-len seq
  (split ($h1 %m $h2) ($h1 %m) ($h2))< (=l ($h1) ($h2)).  ! odd-len seq

! even_len - sequence has even-numbered length

  (even_len ()).
  (even_len ($ %0 %1))<
    (even_len ($)).

! odd_len - sequence has odd-numbered length

  (odd_len (%0)).
  (odd_len ($ %1 %0))<
    (odd_len ($)).

! even/odd - partition 0-indexed seq into even/odd elements
! (even/odd _seq _even _odd)

  (even/odd () () ()).
  (even/odd ($ %) ($e %) ($o))<
    (even/odd ($) ($e) ($o)),
    (=l ($e) ($o)).   ! same # even & odd means next elem is even
  (even/odd ($ %) ($e) ($o %))<
    (even/odd ($) ($e) ($o)),
    (>l ($e) ($o)).   ! extra even elem means next elem is odd
!or:
  (even/odd () () ()).
  (even/odd ($ %) ($e %) ($o))<
    (even_len ($)).
  (even/odd ($ %) ($e) ($o %))<
    (odd_len ($)).

! (no_consec _a _b _seqab) - no consecutive a's in seq of a's & b's

  (no_consec %a %b ()).
  (no_consec %a %b (%a)).
  (no_consec %a %b (%b $))< (no_consec %a %b ($)).
  (no_consec %a %b (%a %b $))< (no_consec %a %b (%b $)).


! ====== some simple binary operations/functions(== ternary relations) ======

! append1 - append one value to a sequence

  (append1 ($) % ($ %)).

! prepend - prepend expression to front of a sequence

  (prepend % ($) (% $)).

! insert - insert an expression at some (any) point in a sequence

  (insert % ($1 $2) ($1 % $2)).

  ! - this is the inverse of a "remove" function

! cat - concatenation (catenate?!) function
! https://www.cs.cornell.edu/courses/JavaAndDS/files/catenate.pdf
! (cat _seq1 _seq2 _seq1+_seq2)

  (cat ($1) ($2) ($1 $2)).

   !>>> This is called 'append' in traditional LP,
   !    but we use 'cat' to avoid confusion with 'append1':

! cat_ - generalization of cat to >2 input arguments

  (cat_ %arg1 %arg2 $args ($) ($res $))<     ! adding an argument
    (cat %arg1 %arg2 $args ($res)).

! cat* - concatenation of a sequence of sequences (1-argument case)

  (cat* () ()).
  (cat* (($) $seqs) ($ $res))<
    (cat* ($seqs) ($res)).

!/
  Generalize other binary operators in this manner?  (plus, and, etc.)
  from ho.ax:

   (generalize cat ()).
!\

! ldistr - distribute an element over the front of multiple sequences

  (ldistr % () ()).
  (ldistr % (($) $seqs) ((% $) $seqs'))<
    (ldistr % ($seqs) ($seqs')).

!/ -- or could use higher-order definition:

   (ldistr $args)<
     ((1* fappend) $args).
     
!\ -- But higher-order forms are not available to form.ax definitions!

! distr - distribute a sequence of elements over the fronts of sequences
! (Note that this is same as fappend*, once we define the <rel>* mapping
!  (which needs distr in its definition!).)

  (distr () () ()).
  (distr (%el $els) (($seq) $seqs) ((%el $seq) $seqs'))<
    (distr   ($els)        ($seqs)            ($seqs')).

! turn relation <rel> into <rel>* that applies to sequences of arguments

  ((` ($rel '*')) $nulls)< (zero_or_more () ($nulls)).  ! empty arg sequences
  ((` ($rel '*')) $argseqsx)<         ! non-empty arg sequences
    ((` ($rel '*')) $argseqs),
    ((` ($rel)) $args),               ! relation to be mapped
    (distr ($args) ($argseqs) ($argseqsx)).

! all_subseqs
! all_subsets - set of all subsets of a set (sequence)
! (all_subsets <set> (<subset> ... <subset>))
! -- note that element order is preserved
! -- note that we don't eliminate duplicate subsets (in case some original
!       set elements are the same)
! -- Better name needed to reflect that these are all subsets of elements
!    from the original sequence given in their original order.

  (all_subsets () (())).
  (all_subsets (% $) ($w% $w/o%))<
    (all_subsets ($) ($w/o%)),
    (ldistr % ($w/o%) ($w%)).

!/
  examples:
 
  (all_subsets () (()))        -- just the empty sequence itself

  (all_subsets (a) ((a) ()))

  (all_subsets (a b) ((a b) (a) (b) ()))

  (all_subsets (a b c) ((a b c) (a b) (a c) (a) (b c) (b) (c) ()))

  ...
!\

! insert_between - insert an expression between each element of a sequence
! (We do not insert before first element or after last.)

  (insert_between %x () ()).       ! no insertion here
  (insert_between %x (%) (%)).       ! or here
  (insert_between %x (%' % $) (%' %x $'))<   ! here's where we insert
    (insert_between %x (% $) ($')).

! `' - "constant" or "quote" function

  ((`' %) %ignored %).   ! result comes from the function, argument is ignored