! form.ax - utility predicates (& functions) based on the forms of expressions
!/
  Note that there is a preference for short names!
  The predicates presented are mostly of a "functional style".
  There may be a case for having versions of basic functions/relations
    that cover multiple argument permutations, since the same fn/rel
    may be thought of in different ways.
  Some higher-order forms probably should be defined first so that they can
    be used in the definition of these utilities. ?
    (But see ho.ax where higher-order forms are used to generalize these
    predicates/functions.)
  "_type" with leading _ denotes an expression of some "type".
  "_type_" w leading & trailing _ denotes str of exprs of that type in seq.
 
  A "predicate" is a valid expression sequence with a predicate name (or
  possibly expression) as the first (or "zeroth" element) and the remaining
  expressions are argumens.  The predicate asserts a "true statement" about
  the "tuple" of arguments.  A "function" is a predicate where all but the
  last arguments are the inputs to the function and the last argument is
  the unique "result" of the function (although sometimes we may have a
  "multi-valued function" that can have multiple results for a tuple of
  input arguments).  A "relation" is a predicate that is not a function
  -- just a tuple of arguments that is a "true" about those arguments.
 
  Predicates (both functions and relations) are often a sequence with
  a predicate symbol and a sequence of arguments:
     (psym _args_)           - predicate has >=0 arguments
     (fsym _iargs_ _result)  - fn has >0 input args and a "result argument"
                         (usually the result expr is unique, but maybe not) 
     - pred & fn symbols are usually syntax-extension symbols, but it
       might be interesting to have atoms or char strings or other
       "constant" (i.e., no variables) expressions!
  Sometimes a predicate (function or relation) instead of being specified
  by a symbol can be an expression consisting of a predicate symbol and
  >0 parameters (ever 0 parameters?):
     ((psym _params_) _args_)
     ((fsym _params_) _iargs_ _res)
  Parameters (usually there is just one) are usually constant "data" exprs
  that "instance" the predicate or function.  (Parameters could be made
  arguments, but sometimes it seems more reasonable to "package" them
  with the predicate/function itself.

 Predicate (function & relation) primitive symbols start with lower-case
 letters or special characters '< > = ~'.  Characters after the first can
 include decimal digits and special characters '_ * ? .'.  Note that
 "negative" predicates often start with ~, but a function symbol with an
 ending ? is a Boolean function returning true/false, in which case, an
 initial ~ is a (bool.ax) higher-order form that complements the Boolean
 function.


!---+----1----+----2----+----3----+----4----+----5----+----6---+----7----+----8
!/ index:

=> categories:
  0-arg preds - valid expr "flags"
  1-arg predicates - sets, named symbolic constants, 0-inp-arg fns:
    seq nonnull null single pair triple evenl oddl, named constants, const fn
  unary fns (1 input arg gives unique result):
    id head tail last front rev mid midr roth rotl
  binary relations (that are not a fn in either direction (except ==)):
    == perm rot  - symmetric
    pre suf in rmv substr subseq copies strdup elcopy elcopy1  - nonsymmetric
    =l <l <=l >l >=l ~=l  - seq length comparisons
  binary functions (mostly) - mostly 2 input args with unique output:
    join join_ join* append1 prepend cat cat_ cat*
    xdistr xsdistr rdistrx rdistrxs
    asnhead asnlast asntail asnfront
    asnpre | _ asnsuf | _
  length-index (0..) predicates:
    sel#l pre#l suf#l rot#l rmv#l - binary functions
    ins#l asn#l selstr#l _ rmvstr#l insstr#l asnstr#l | _ - >2 iarg fs
  reverse-length-index (..0) predicates:
    _pred#-l - for all forward-index predicates
  more relations/functions:
    ins asn insstr asnstr asnstr= split even|odd 
    no_consec all_subseqs ins_ ins._ ins_. ins._. map

 Alternate predicate names, (alt: ...) or (? ...), are sometimes given.
 Argument order variations may interesting!
 Predicate definition grouping and order may need refinement!
 (A question mark '?' indicates something uncertain to be reconsidered later.
  Two or more question marks ?..? indicate something particularly vexing!)
 A z before a pred denotes that it is probably obsolete -- may be removed.
 An x before a pred denotes something interesing that needs to be reconsidered.
 tbd means "to be done" or "to be decided" - also something       " 
 A comment block marked "old" often encloses "obsolete" or tbd defns.

=== 0-arg preds ===
 - valid expr "flags"

=== 1-arg predicates ===
 name - named symbolic constant
 ^ - constant function
sets:
 (seq ($)) - set of sequences
 (nonnull (% $)) - non-null sequences (alt: seq>0)
 (null ()) - constant empty seq expr (alt: nullseq, seq0)
 (single (%)) - singleton sequences (? seq1 - use future decnum.ax?)
 (pair (%0 %1)) - sequences that are pairs (? seq2)
 (triple (%0 %1 %2)) - sequences that are triples (? trpl, tpl, trp, seq3)
 - other lengths?
 (evenl _eseq) - seq w even-numbered length (? evseq, even_len, elen)
 (oddl  _oseq) -     "  odd-        "          odseq, odd_len, olen)
 - random-value set-elem "functions"

=== unary (single-valued) fns (= binary relations) ===
 (id _e _e) - identity function (- same as == relation)
 (head _seq _h) - first element of a sequence
 (tail _seq _t) - tail of sequence (rest of sequence after head)
 (last _seq _l) - last element of sequence
 (front _seq _f) - front of sequence (before last element)
z -- also do asnhead, asntail, asnlast, asnfront - assign (replace) with arb?? 
 (rev _seq _revseq) - reverse of a sequence
 (mid _seq _mid_elem) - middle elem of a seq (left of middle if even len)
 (midr _seq _midr_elem) -          "          right         "
 (roth (_h _tail_) (_tail_ _h)) - rotate the head element (alt: rot1)
 (rotl (_front_ _l) (_l _front_)) - rotate the last elem (alt: rot-1)
   -- roth and rotl are each other's inverse

=== binary relations (can be treated as multi-valued unary functions) ===
-- symmetric - arg order doesn't matter:
 (== _e _e) - identity relation (- same as id function)
 (perm _seq1 _seq2) - sequence 2 is permutation of sequence 1 (& vice-versa)
   -- same as =l relation!
 (rot (_pre_ _suf_) (_suf_ _pre_)) - "rotate" (swap prefix/suffix of) a seq
-- non-symmetric - opposite arg order may be interesting:
 (pre _pre _seq) - 1st arg is prefix of sequence
 (suf _seq _suf) - 2nd arg is suffix   "
 (in _e _seq) - expression is in a sequence (alt: member)
? (rmv _seq _seq-) - remove expr from seq at arbitrary position (vs ins?)
 (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 expression _e
 (strdup _seq1 _seq2) - 2nd seq is concatenated duplicates of 1st seq
 (elcopy _seq1 _seq2) - seq2 is >=0 copies of each seq1 elem (in order)
 (elcopy1 _seq1 _seq2) -    "   >=1 copies             "
-- length relations:
 (=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

=== binary operations/functions (& nonbinary: join_ cat_ join* cat*) ===
 (join _e0 _e1 (_e0 _e1)) - join two exprs into a pair (?bind,fuse,pair,merge)
 (join_ _e_ (_e_)) - generalize join to >=0 input arg exprs
   -- note that join_ with zero input args is same as 'null' pred
 (join* (_e_) (_e_)) - join seq of input exprs (-- instance of 'id' fn!)
 (append1 _e _seq _seq') - append 1 expr to end of seq
 (prepend _e _seq _seq') - prepend (1) expr to front of seq
 (cat _seq0 _seq1 (seq0+seq1)) - [con]catenate two sequences into one
 (cat_ _seq_ _seq') - cat >=0 input arg seqs into one
   -- cat_ w 0 iargs is same as 'null'; w 1 iarg, instance of 'id'
 (cat* (_seq_) _seq') - cat sequence of sequences into one
z (xdistr _x _seqs _seqs') - distr expr over fronts of seqs - ho: (/prepend)
 (distr _xs _seqs _seqs') - distr exprs over fronts of seqs - ho: *prepend
   -- we need `distr` in order to define the higher-order pred *!
z (rdistrx _seqs _x _seqs') - right-distr expr over ends of seqs - (/append1)
z (rdistr _seqs _xs _seqs') - right-distr exprs over ends of seqs - *append1
 -- also do asnhead, asntail, asnlast, asnfront - assign (replace) with new
 (asnhead _h' _seq _seq') - expr _h' becomes new head of (nonnull) _seq
 (asnlast _l' _seq _seq') -   "  _l'      "      last         " 
 (asntail  _tail'  _seq _seq') - _tail' becomes new tail of (nonnull) _seq
 (asnfront _front' _seq _seq') - _front'      "     front         "
 (asnpre _pre _seq _seq') - assign (replace) seq prefix with new prefix
   -- asnpre  - if prefix longer than seq, no valid expr generated
      asnpre| -                 "          we truncate prefix at seq length
      asnpre_ -                 "          prefix becomes new seq
 (asnsuf _seq _suf _seq') - assign (replace) seq suffix with new suffix
   -- asnsuf, asnsuf|, asnsuf_ - analogous to asnpre if _suf >l _seq

=== index funcs/preds where position index is seq length (pred#l <lenseq> _)
  -- note that ending char is lowercase 'L', not digit '1'
  -- see natnum.ax and char.ax for alternative index functions
  -- note that _pos (0..) is the prefix length before seq elem [_pos]
-- binary functions:
 (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
 (rmv#l _pos _seq _seq') - remove elem [_pos] from sequence
-- 3-argument functions:
 (ins#l _pos _ex _seq _seq') - insert expr at (before) _seq[_pos]
 (asn#l _pos _ex _seq _seq') - assign (replace) expr at _seq[_pos]
-- string position functions:
 (asnpre#l _pos _str _seq _seq') - assign (repl) prefix before [_pos]
 (asnsuf#l _pos _str _seq _seq') -       "       suffix from [_pos]
 (selstr#l _pos _len _seq _str) - select str w _len starting at [_pos]
 (rmvstr#l _pos _len _seq _seq') - remove _len-string starting at _seq[_pos]
 (insstr#l _pos _str _seq _seq') - insert string before sequence [_pos]
 (asnstr#l _pos _str _seq _seq') - assign (repl) string starting at [_pos]
  -- asnstr#l|, asnstr#l_ - analogous to asnpre|, asnpre_
 
=== _rpos (reverse position) len-indexes seq elems from the end (.. 2 1 0)!:
-- binary functions:
 (sel#-l _rpos _seq _elem) - select element at [_rpos] in seq (..0)
 (pre#-l _rpos _seq _pre) - get seq prefix ending with [_rpos]
 (suf#-l _rpos _seq _suf) - get seq suffix starting after [_rpos]
 (rot#-l _rpos _seq _rot) - get seq rotation w prefix ending w _rpos
 (rmv#-l _rpos _seq _seq') - remove elem [_rpos] from sequence
-- 3-argument functions:
 (ins#-l _rpos _ex _seq _seq') - insert expr after _seq[_rpos]
 (asn#-l _rpos _ex _seq _seq') - assign (replace) expr at _seq[_rpos]
-- string position functions:
***/// to be done!:
 (asnpre#-l _rpos _str _seq _seq') - assign (repl) prefix ending w [_pos]
 (asnsuf#-l _rpos _str _seq _seq') -       "       suffix after [_pos]
***\\\
 (selstr#-l _rpos _len _seq _str) - select str w _len ending with [_rpos]
 (rmvstr#-l _rpos _len _seq _seq') - remove _len-string ending w _seq[_rpos]
 (insstr#-l _rpos _str _seq _seq') - insert string after sequence [_rpos]
 (asnstr#-l _rpos _str _seq _seq') - assign (repl) string ending at [_rpos]
   -- asnstr#-l|, asnstr#-l_ - analogous to asnpre|, asnpre_

 === more relations & functions ===
 (ins _e _seq _seq') - insert expr into seq at arbitrary position
 (asn _e _seq _seq') - assign (replace) expr in seq at arb pos
 (insstr _str _seq _seq') - insert string into seq at arb pos
 (asnstr _str _seq _seq') - assign (replace) string in seq at arb pos
 (asnstr= _str _seq _seq') - replaced string has same length as new
 (split _seq _half0 _half1) - split seq into halves (half0 gets odd mid)
 (even|odd _seq _eseq _oseq) - partition seq (0..) into even, odd elements
 (no_consec _x _notx _seqxnotx) - no consecutive x in seq of (distinct) x,notx
z (elemseq _elems _elemseq) - form arg1 seq from elems in arg0 seq
z (all_subseqs _seq (_subseq_)) - set of all subseqs of a sequence
 (ins_ _seq _e _seq') - insert expr between elems of a seq
   - ins._ - also insert before seq
     ins_. -     "       after seq
     ins._. -    "       before first and last elems (or once for null seq)
 (map _map _expr _expr') - apply finite map to an expr (in map's domain)
!\


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



! ========= 0-arg predicates =========
! -- Note that if there are no args in  (_pred)  expr, we can omit the
!    enclosing sequence and just write  _pred .

! --- valid expr "flags" --- 

! "flag" - sometimes it would be good to define a pred symbol as valid
! - It might represent a fact or condition about the set of axioms.
!/ examples:

  (Tested)  - valid if a set of axioms has been tested
or:
  Tested    - no reason to enclose the 0-arg pred name in parens!

  (`Error "Inconsistent Boolean function!:" %Bf?) <   ! defn of an error flag!
      ! - Note, no enclosing parens here either for this pred expr w params.
    (tf %t %f),            ! true/false values
    (%Bf? $iargs %t),
    (%Bf? $iargs %f).
    ! - Boolean fn gives both true & false for same input args!  (see Bool.ax)
!\



! ========= 1-arg predicates =========


! --- named symbolic constants ---

! "name" - named-symbolic-constant - can be useful to give a constant a name
!                           (which is available to the entire set of axioms)
! - Name could be syntax-extension symbol, atom, or maybe even a char string.

  (_name _x).      ! const expr _x is arg of "pred" symbol _name
                    ! (It's not a parameter of a pred expr.)  
!/ ex:
  (due-date 05-15-26).   ! const expr 05-15-26 is arg of "pred" due-date
                         ! (It's not a parameter of the due-date psym.)
!\


! --- constant function ---

! ^ - constant-function - function w 0 input args returns a constant expr
!   - constant expr value _x is a parameter of the (^ _x) fn expr

  ((^ %x) %x).       ! function w fn expr (^ %x) has result value %x
                     ! (alt names: const, quote)


! --- sets ---

! seq - set of sequences

  (seq ($)).

! nonnull - non-null sequences (alt: seq>0 - see char.ax)

  (nonnull (% $)).

! null - null sequence constant expr (alt: nullseq, seq0)

  (null ()).

! single - singleton sequences (alt: sing, singseq, seq1 - see char.ax)

  (single (%)).

! pair - sequences that are pairs (alt: seq2)

  (pair (%0 %1)).

! triple - sequences that are triples (alt: trpl, tpl, trp, seq3)

  (triple (%0 %1 %2)).

! - other lengths?

! (evenl _evseq) - seq w even-num'd len (alt: seqev evseq eseq even_len elen)

  (evenl ()).                         ! zero-length sequence is even
  (evenl ($e %1 %2))< (evenl ($e)).   ! adding 2 elems to even-len seq

! (oddl _oseq) - seq w odd-num'd len (alt: seqodd odseq oseq odd_len olen)

  (oddl (%)).                        ! length-one sequence is odd
  (oddl ($o %1 %2))< (oddl ($o)).    ! adding 2 elems to odd-len seq


! --- random-value set-elem "functions"! ---

! *** Each "set" pred can be interpreted as a 0-input-arg function that
!     nondeterministically returns an arbirary set element value!

  (_setname %arbsetval).   ! "result" of set "function" is one of its values

!/ example:

  (pair %pair)     - fn `pair` returns an arbitrary pair!
                   - This would be a "multi-valued" function!
!\



! ========= unary (single-valued) functions (= binary relations) =========
! Recall a function has >=0 (input) argument exprs and one unique result expr.
! Most of these can be treated as binary relations between the single input
! argument and the result. 

! (id _e _e) - identity function (- same as '==' relation!)  (alt: i)
!  - We have both predicates since sometimes its nice to think of it as a
!    a function and other times as a relation.

  (id % %).

! (head _seq _h) - first (head) element in a sequence  (alt: h)

  (head (%h $t) %h).

! (tail _seq _t) - rest (tail) of sequence after head  (alt: t)

  (tail (%h $t) ($t)).

! (last _seq _l) - last element in sequence  (alt: l)

  (last ($f %l) %l). 

! (front _seq _f) - all but last element of sequence  (alt: f)
! (better name?:  rtail (reverse tail), body, trim,snip,clip,chop,dock)

  (front ($f %l) ($f)).

!?? -- also do asnhead, asntail, asnlast, asnfront - assign (replace) with arb
! (asn... seq seq') - head, tail, last, or front is replaced w arbitrary expr
! -- Probably not very useful!   -- a "multi-valued function"!?
! -- One can always have a head,tail,last,front arg and leave it a var!


! (rev _seq _revseq) - reverse a sequence

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

! (mid _seq _mid_elem) - middle elem of a seq (left of middle if even len)

                  ! no mid for null-len seq
  (mid (%0) %0).    ! mid of singleton seq is the single expr
  (mid (%0 %1) %0).   ! mid of pair is left expr
  (mid (%h $ %l) %m)<   ! adding new head & last --> mid stays the same!
    (mid ($) %m).

! (midr _seq _mid_elem) - middle elem of a seq (right of middle if even len)

                   ! no midr for null-len seq
  (midr (%0) %0).    ! midr of singleton seq is the single expr
  (midr (%0 %1) %0).   ! midr of pair is right expr
  (midr (%h $ %l) %m)<   ! adding new head & last --> midr stays the same!
    (midr ($) %m).

! (roth (_h _tail_) (_tail_ _h)) - rotate the head element (alt: rot1)

  (roth (%h $tail) ($tail %h)).
 
! (rotl (_front_ _l) (_l _front_)) - rotate the last elem (alt: rot-1)

  (rotl ($front %l) (%l $front)).

  ! -- roth and rotl are each other's inverse



! ========= binary relations (like multi-valued unary functions) =========
!                        (or single-valued fn in the case of ==)

! --- symmetric - arg order doesn't matter:

! (== _e _e) - identity relation (- same as 'id' function)

  (== % %).

  ! -- Same as 'id' but we think of id as a unary function from argument to
  !    a result, while == is a binary relation for 2 identical expressions.

!/ if ho.ax avail:
   (def == id).
!\

! (perm _seq0 _seq1) - sequence 1 is permutation of sequence 0 (& vice-versa)

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

  !/ alt def:
    (perm () ()).
    (perm ($a % $b) ($c % $d))<
      (perm ($a $b) ($c $d)).
  !\  - may be interest?

! (rot (_pre_ _suf_) (_suf_ _pre_)) - "rotate" (swap prefix/suffix of) a seq

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

! --- non-symmetric - opposite arg order may be interesting:

! (pre _pre _seq) - 1st arg is prefix of sequence  (arg order?)

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

! (suf _seq _suf) - 2nd arg is suffix of sequence  (arg order?)

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

! (in _e _seq) - expression is in sequence (alt: member)

  (in % ($a % $b)).

!z (rmv _seq _seq-) - nondetermi. remove an expr from seq at arb position
! (Opposite argument order would be a nondeterministic insert.)

 !z (rmv ($a % $b) ($a $b)).    ! probably not needed

!? (ins ($a $b) ($a % $b)).     ! - Would "insert" arg order be nicer?
! -- already using ins for (ins _e _seq _seq')

! rmv & ins probably aren't very useful anyway!
! Just ignore _e arg in 'ins' below!

! (substr _seq1 _seq2) - 1st sequence is substring of 2nd sequence
! - an extension of 'in'

  (substr ($str) ($1 $str $2)).

! (subseq _seq1 _seq2) - 1st seq is 2nd seq w >=0 elems removed (order kept)

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

  !/ alt def:
    (subseq ($) ($)).
    (subseq %seq1' %seq2)<
      (subseq %seq1 %seq2),
      (rmv %seq1 %seq1').
  !\  - interesting?  - it better "hides" the internal sequence details

! (copies _e _seq) - seq is >=0 copies of const expr _e  (alt: dup cp)
! -- Don't need this since ((/ ==) _e _seq) is equivalent (see ho.ax)!
!    But it may be nice to have as a primitive pred w/o using h-o.
!    Also, we need 'copies' to define some h-o forms.

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

! (strdup _seq1 _seq2) - 2nd seq is catenated duplicates of 1st seq
! (alt: dupstr cpstr *str *$ ?)

  (strdup ($) ()).
  (strdup ($) ($ $dup))< (strdup ($) ($dup)).

! (elcopy _seq1 _seq2) - seq2 is >=0 copies of each seq1 elem (in order)
! (alt: elcp)

  (elcopy () ()).
  (elcopy ($ %) ($c $%c))<
    (elcopy ($) ($c)),
    (copies % ($%c)).

! (elcopy1 _seq1 _seq2) - seq2 is >=1 copies of each seq1 elem (in order)
! (alt: elcp1)

  (elcopy1 () ()).
  (elcopy1 ($ %) ($c1 % $%c))<
    (elcopy1 ($) ($c1)),
    (copies % ($%c)).

! -- length relations:

! (=l _s1 _s2) - two sequences have equal length  (symmetric)

  (=l () ()).
  (=l (%1 $1) (%2 $2))<
    (=l ($1) ($2)).
    
! (<l _s1 _s2) - 1st seq length less than 2nd seq

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

! (<=l _s1 _s2) - 1st seq length less than or equal 2nd

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

! (>l _s1 _s2) - 1st seq length greater than 2nd

  (>l %2 %1)< (<l %1 %2).
  ! -- or use (rev <l) if ho.ax available

! (>=l _s1 _s2) - 1st seq length greater than or equal 2nd

  (>=l %2 %1)< (<=l %1 %2).
  ! -- or use (rev <=l)

! (~=l _s1 _s2) - sequences with unequal length  (symmetric)

  (~=l %1 %2)< (<l %1 %2).
  (~=l %1 %2)< (>l %1 %2).
  ! -- or use 1val if ho.ax available



! ========= binary operations/functions =========
!      (plus nonbinary join_ cat_ join* cat*)

! (join _e0 _e1 (_e0 _e1)) - join two exprs into pair (?bind,fuse,pair,merge) 

  (join %0 %1 (%0 %1)).  
 
! (join_ _e_ (_e_)) - generalize join to >=0 input arg exprs
! -- note that join_ with zero input args is same as 'null' pred

  (join_ $ ($)).

! (join* (_e_) (_e_)) - join seq of input exprs (- instance of 'id' fn)
!   - Does this serve any purpose?

  (join* ($) ($)). 

! (append1 _seq _e _seq') - append 1 expr to end of seq  (? append)
!   - Note that 'append' in traditional LP is same as my 'cat',
!     Thus I call this function 'append1'.  Or perhaps just use 'append'?

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

 ! alt arg order??:
 !  (append1 % ($) ($ %)).   ! - it may be nicer to put appended expr first!

! - A nice generalization:
!   (append1_ ($) $e ($ $e)).   ! append multiple exprs

 !or:  (append1_ $e ($) ($ $e)).   ! alt arg order?

! (prepend _e _seq _seq') - prepend (1) expr to front of seq  (? prepend1)

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

! - Nice generalization:
!   (prepend $e ($) ($e $)).

! (cat _s0 _s1 (s0+s1)) - [con]catenate two sequences into one (? concat)
! see https://www.cs.cornell.edu/courses/JavaAndDS/files/catenate.pdf

  (cat ($0) ($1) ($0 $1)).

! (cat_ _seq_ _seq') - cat >=0 input arg seqs into one
! -- cat_ w 0 iargs is same as 'null'; w 1 iarg, instance of 'id'
! -- Note that the argument seqs are a partition of the result seq.

  (cat_ ()).
  (cat_ ($) $seqs ($ $cat)))<
    (cat_ $seqs ($cat)).

! (cat* (_seqs_) _seq') - cat sequence of sequences into one seq  (unary fn)

  (cat* ($seqs) %cat)<
    (cat_ $seqs %cat).

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

   (generalize cat ()).
!\

! (distr _exprs _seqs _seqs') - distribute exprs over fronts of seqs (? distr*)
! - Same as ho *prepend, but we need distr in order to define ho * operator!

  (distr () () ()).
  (distr (%e $e) (($seq) $seqs) ((%e $seq) ($seqs')))<
    (distr ($e) ($seqs) ($seqs')).

  /* use ho for:
     (distr1 _expr _seqs _seqs') - distr 1 expr over fronts of seqs
     (rdistr* _seqs _exprs _seqs') - "right distr" exprs over ends of seqs
     (rdistr1 _seqs _expr _seqs') -        "      1 expr          "
      == /prepend, *append1, \append1  - but need to decide on arg order!!
  */


!/ old...
 (xdistr _x _seqs _seqs') - distr expr over fronts of seqs - ho: (/prepend)
 (distr _xs _seqs _seqs') - distr exprs over fronts of seqs - ho: *prepend
   -- we need these primitives in order to define the higher-order preds!
 (rdistrx _seqs _x _seqs') - right-distr expr over ends of seqs - (-. append1)
 (rdistr _seqs _xs _seqs') - right-distr exprs over ends of seqs - *append1

! (distr1 _x _seqs _seqs') - distribute 1 expr over fronts of seqs
! - same as h-o / op applied to prepend, 
! -- note that xdistr is needed to define .-
! -- alt: 1distr, distr1

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

! (distr _xs _seqs _seqs') - distr exprs over fronts of seqs - ho: *prepend
! -- We need these primitives in order to define the higher-order preds!

  (distr () () ()).
  (distr (% $e) (($) $seqs) ((% $) ($seqs')))< 
    (distr ($e) ($seqs) ($seqs')).

! (rdistrx _seqs _x _seqs') - right-distr expr over ends of seqs (-. append1)
! -- alt: 1rdistr, rdistr1

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

! (rdistr _seqs _xs _seqs') - right-distr exprs over ends of seqs - *append1

  (rdistr () () ()).
  (rdistr ($seqs ($)) ($e %) ($seqs' ($ %)))<
    (rdistr ($seqs) ($e) ($seqs')).
!\ ...old



! (asnhead _e _seq _seq') - expr _e becomes new head elem of (nonnull) _seq

  (asnhead %h' (%h $tail) (%h' $tail)).

! (asnlast _e _seq _seq') - expr _e becomes new last elem of (nonnull) _seq

  (asnlast %l' ($front %l) ($front %l').

! (asntail _tail' _seq _seq') - _tail' becomes new tail of (nonnull) _seq

  (asntail %tail (%h $tail) (%h $tail')).

! (asnfront _front' _seq _seq') - _front' becomes new front of (nonnull) seq

  (asnfront %front' ($front %l) ($front' %l)).

! (asnpre _pre _seq _seq') - assign (replace) seq prefix with new prefix
! - prefix can't be longer than sequence (else no valid expr generated!)
! - arg order?

  (asnpre ($newpre) ($oldpre $suf) ($newpre $suf))<
    (=l ($newpre) ($oldpre)).     ! new prefix replaces old prefix of same len

! (asnpre| _pre _seq _seq') - assign seq prefix w new prefix
! - if _pre longer than _seq, we truncate prefix at seq len

  (asnpre| %newpre %seq %seq')<
    (asnpre %newpre %seq %seq').  ! new prefix len <= seq len, replace prefix
  (asnpre| ($newpre0 $newpre1) ($seq) ($newpre0))<
    (=l ($newpre0) ($seq)).      ! new pre >l _seq, _seq' := truncated new pre

! (asnpre_ _pre _seq _seq') - assign seq prefix w new prefix
! - if _pre longer than _seq, sequence is replaced with prefix

  (asnpre_ %newpre %seq %seq')<
    (asnpre %newpre %seq %seq').   ! new prefix len <= seq len, replace prefix
  (asnpre_ ($newpre) ($seq) ($newpre)<
    (>l ($newpre) ($seq)).        ! new prefix len > seq len, _seq' := new pre
   
! (asnsuf _seq _suf _seq') - assign (replace) seq suffix with new suffix
! - suffix can't be longer than sequence (else no valid expr generated!)
! - arg order?

  (asnsuf ($pre $oldsuf) ($newsuf) ($pre $newsuf))<
    (=l ($oldsuf) ($newsuf)).   ! new suffix replaces old suffix of same len

! (asnsuf| _seq _suf _seq') - assign seq suffix w new suffix
! - if _suf longer than _seq, we "front-truncate" suffix at seq len
! *** Or should be truncate at end of sequence??? ***

  (asnsuf| %seq %newsuf %seq')<
    (asnsuf %seq %newsuf %seq').  ! new suffix len <= seq len, replace suffix
  (asnsuf| ($seq) ($newsuf0 $newsuf1) ($newsuf1)<
    (=l ($newsuf1) ($seq)).    ! new suf >l _seq, _seq' := front-truncd newsuf

! (asnsuf_ _seq _suf _seq') - assign seq suffix w new suffix
! - if _suf longer than _seq, sequence is replaced with new suffix

  (asnsuf_ %seq %newsuf %seq')<
    (asnsuf %seq %newsuf %seq').   ! new suffix len <= seq len, replace suffix
  (asnsuf_ ($seq) ($newsuf) ($newsuf)<
    (>l ($newsuf) ($seq)).        ! new suffix len > seq len, _seq' := new suf

 

! ========= index predicates where index is seq len =========
!                      (pred#l <lenseq> ...)
!  -- Note that ending char 'l' is lowercase 'L', not digit '1'.
!  -- See natnum.ax and char.ax for alternative indexes.
!  -- The _pos expression is an arbitrary sequence whose length represents
!     the natural number index of an element position in the sequence.
!  -- Note that _pos (0..) is the prefix length before seq elem [_pos].
!     (That is, 0-based indexing.)
!  -- These predicates are undefined if _pos length is > sequence length. 

! -- binary functions:

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

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

!/
   Note that using function (sel#l ...) as a condition expression with
   instantiated _seq & _elem nondeterministically "finds" an occurrence
   of _elem in _seq, if it exists, and returns its position (which is an
   unspecified sequence of length corresponding to the _elem position.
!\ 

! (pre#l _pos _seq _pre) - get sequence prefix ending before [_pos]

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

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

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

  (rot#l %pos ($pre $suf) ($suf $pre))<
    (=l %pos ($pre)).             ! prefix has length _pos

! (rmv#l _pos _seq _seq') - remove elem [_pos] from sequence

  (rmv#l %pos ($pre %elem $suf) ($pre $suf))<
    (=l %pos ($pre)).
  
! -- 3-argument functions:

! (ins#l _pos _ex _seq _seq') - insert expr at (before) _seq[_pos]

  (ins#l %pos %ex ($pre $suf) ($pre %ex $suf))<
    (=l %pos ($pre)).
  
! (asn#l _pos _ex _seq _seq') - assign (replace) expr at _seq[_pos]

  (asn#l %pos %ex ($pre %oldex $suf) ($pre %ex $suf))<
    (=l %pos ($pre)).

!/
! -- 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))
      (rmv#l %pos ($pre %elem $suf) ($pre $suf))
      (ins#l %pos %ex ($pre $suf) ($pre %ex $suf))
      (asn#l %pos %ex ($pre %oldex $suf) ($pre %ex $suf))
      `< (=l %pos ($pre)).   ! shared condition for all these predicates!
!\

!/ example - pred#l form predicates
  (axs< ((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)))
        ((rmv#l %pos ($pre %elem $suf) ($pre $suf)))
        ((ins#l %pos %ex ($pre $suf) ($pre %ex $suf)))
        ((asn#l %pos %ex ($pre %oldex $suf) ($pre %ex $suf)))
      `< (=l %pos ($pre))).   ! shared cond for all these predicates!

  - also do findstr# ins#l asn#l selstr#l rmvstr#l insstr#l asnstr#l
            [asnstr#l| asnstr#l_ ?]
!\

! -- string position predicates:
!    (_len param is arbitrary sequence whose length denotes the length of
!     the string of interest.)

! (asnpre#l _pos _str _seq _seq') - assign (repl) prefix before [_pos]

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

! (asnsuf#l _pos _str _seq _seq') - assign (repl) suffix from [_pos]

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

! (selstr#l _pos _len _seq _str) - select string of length _len at [_pos]
! - note that last string element has sequence position [_pos + _len]
! - no solution if string length goes beyond end of sequence
!   (or could let selstr#l_ give as much string as possible?)

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

!/
   Setting _str and _seq in selstr#l, leaving _len unspecified allows us
   to get the position _pos of string, if it occurs in sequence.
!\

! (rmvstr#l _pos _len _seq _seq') - remove string of length _len at [_pos]

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

! (insstr#l _pos _str _seq _seq') - insert string starting at [_pos]

  (insstr#l %pos ($str) ($pre $suf) ($pre $str $suf))<
    (=l %pos ($pre)).
 
! (asnstr#l _pos _str _seq _seq') - assign (repl) string starting at [_pos]
! - no valid expr generated if pos len + str len > seq len

  (asnstr#l %pos ($tr) ($pre $oldstr $suf) ($str) ($pre $str $suf))<
    (=1 %pos ($pre)),
    (=l ($oldstr) ($str)).

! (asnstr#l| _pos _str _seq _seq') - assign (repl) string at [_pos]
! - if pos len + str len > seq len, str truncated as needed

  (asnstr#l| %pos %str %seq %seq')<   ! pos len + str len <= seq len
    (asnstr#l %pos %str %seq %seq').  ! - same as asnstr#l
  (asnstr#l| %pos ($str0 $str1) ($pre $oldstr) ($pre $str0))<
    (=1 %pos ($pre)),
    (=l ($oldstr) ($str0)).  ! pos + new str >=l seq - truncate new str

! (asnstr#l_ _pos _str _seq _seq') - assign (repl) string at [_pos]
! - if pos len + str len > seq len, seq' is extended to hold it

  (asnstr#l_ %pos %str %seq %seq')<   ! pos len + str len <= seq len
    (asnstr#l %pos %str %seq %seq').  ! - same as asnstr#l
  (asnstr#l_ %pos ($pre $oldstr) ($str0 $str1) ($pre $str0 $str1))<
    (=1 %pos ($pre)),
    (=l ($oldstr) ($str0)).  ! pos + new str >=l seq - extend sequence

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

   tbd...
!\


      
! ====== _rpos (reverse position) indexes seq elems from the end! ======
!        (sequence elements are numbered n-1..0 where n is sequence length)

!-- binary functions:

! (sel#-l _rpos _seq _elem) - select elem at [_rpos] in seq (rev'd idx n-1..0)

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

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

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

  (rot#-l %rpos ($pre $suf) ($suf $pre))<
    (=l %rpos ($suf)).

! (rmv#-l _rpos _seq _seq') - remove elem [_rpos] from sequence

  (rmv#-l %rpos ($pre %elem $suf) ($pre $suf))<
    (=l %rpos ($suf)).

! -- 3-argument functions:

! (ins#-l _rpos _ex _seq _seq') - insert expr at (after) _seq[_rpos]

  (ins#-l %rpos %ex ($pre $suf) ($pre %ex $suf))<
    (=l ($suf) %rpos).

! (asn#-l _rpos _ex _seq _seq') - assign (replace) expr at _seq[_rpos]

  (asn#-l %rpos %ex ($pre %oldex $suf) ($pre %ex $suf))<
    (=l ($suf) %rpos).

! -- string right-position predicates:

! (selstr#-l _rpos _len _seq _str) - select str w _len ending at [_rpos]
!   - note that str elems go from seq r-pos [_rpos+_len-1] to [_rpos]
!   - no solution if string length goes beyond front of sequence
!     (or could let selstr#-l_ give as much string as possible?)

  (selstr#-l %rpos %len ($pre $str $suf) ($str))<
    (=l ($suf) %rpos),
    (=l ($str) %len).

  ! -- Can use selstr#-1 to nondeterministically  "find" a string in a seq.

! (rmvstr#-l _rpos _len _seq _seq') - remove _len-string ending at _seq[_rpos]

  (rmvstr#-l %rpos %len ($pre $str $suf) ($pre $suf))<
    (=l ($suf) %rpos),
    (=l ($str) %len).

! (insstr#-l _rpos _str _seq _seq') - insert string ending at _seq[_rpos]

  (insstr#-l %rpos ($str) ($pre $suf) ($pre $str $suf))<
    (=l ($suf) %rpos).

! (asnstr#-l _rpos _str _seq _seq') - assign (repl) string ending at [_rpos]
! - no valid generated expr if rpos len + str len > seq len

  (asnstr#-l %rpos ($str) ($pre $oldstr $suf) ($pre $str $suf))<
    (=l ($suf) %rpos),
    (=l ($oldstr) ($str)).

! (asnstr#-l| _rposi _str _seq _seq') - assign string ending at [_rpos]
! - if rpos len + str len > seq len, string front-truncate at seq len

  (asnstr#-l| %rpos %str %seq %seq')<   ! rpos len + str len <= seq len
    (asnstr#-1 %rpos %str %seq %seq').  ! - same as asnstr#-l 
  (asnstr#-l| %rpos ($str0 %str1) ($oldstr $suf) ($str1 $suf))<  !" >= seq len
    (=l ($suf) $rpos),
    (=l ($oldstr) ($str1)).  ! rpos + new str >=l seq - truncate new str
      
! (asnstr#-l_ _rpos _str _seq _seq') - assign string ending at [_rpos]
! - if rpos len + str len > seq len, seq extended as needed

  (asnstr#-l_ %rpos %str %seq %seq')<   ! rpos len + str len <= seq len
    (asnstr#-l %rpos %str %seq %seq').  ! - same as asnstr#-l
  (asnstr#-l_ %rpos ($str0 $str1) ($ostr $suf) ($str0 $str1 $suf))<
    (=l ($suf) %rpos),
    (=l ($ostr) ($str1)).  ! rpos + new str >=l seq - extend seq

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



! ========= more relations and functions =========

! (ins _e _seq _seq') - insert expr into seq at arbitrary position
! alt arg order:  (ins _seq _e _seq')  - is this sometimes nice??

  (ins %e ($pre $suf) ($pre %e $suf)).

  ! (rmv _seq seq') - remove an arbitray expr in _seq, giving _seq'
  !  -- don't need this -- just use ins, letting _e be an unused var:
  !    (rmv %seq %seq')< (ins %e %seq' %seq).
  ! ??? What's a good term for a var with a single occurrence in a clause?

  ! -- Can also use ins to nondeterministically remove a single occurrence
  !    of a specified expr.

! (asn _e _seq _seq') - assign (replace) expr in seq at arbitrary position

  (asn %e ($pre %olde $suf) ($pre %e $suf)).


 === more relations & functions ===

!/ old ...
! (rmvstr _seq _seq') - remove arbitrary string from a sequence
! -- Move to earlier "binary relation" category, near 'rmv'?

  (rmvstr ($pre $str $suf) ($pre $suf)).

 ?? Is 'rmvstr' needed? -- could just use 'insstr'!
!\

! (insstr _str _seq _seq') - insert string into seq at arbitrary position
! alt arg order:  (insstr _seq _str _seq')  - sometimes nice??

  (insstr ($str) ($pre $suf) ($pre $str $suf)). 

  ! Can define 'rmvstr' from 'insstr' as follows:
  !   (rmvstr %seq %seq') < (instr %str %seq' %seq).

! (asnstr _str _seq _seq') - assign (replace) string in seq at arb pos
! alt order: (asnstr _seq _str _seq')  ?
!   - Replaced string and new string can have different lengths.
!     (If replaced string has length 0, this is same as 'insstr'.
!      If new string has length 0, this is same as 'rmvstr'.)

  (asnstr ($str) ($pre $oldstr $suf) ($pre $str $suf)).
 
  ! Can define 'rmvstr' from 'asnstr' as follows:
  !   (rmvstr %seq %seq')< (asnstr () %seq %seq').

! (asnstr= _str _seq _seq') - replaced string has same length as new

  (asnstr= ($str) ($pre $oldstr $suf) ($pre $str $suf))<
    (=l ($oldstr) ($str)).

! (split _seq _half0 _half1) -split seq into halves (0th gets odd mid)
! - _half0gets middle elem if seq length is odd

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

! (even|odd _seq _eseq _oseq) - distribute seq (0..) into even, odd elements 

  (even|odd () () ()).
  (even|odd ($seq %) ($e %) %o)<
    (even|odd ($seq) ($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

! (no_consec _x _y _seqxy) - no consecutive x in seq of distinct x, y elems
! - we don't need an inequality relation here!

  (no_consec %x %y ()).    ! empty seq has no consecutive x
  (no_consec %x %y (%x)).    ! single x seq has no consec x
  (no_consec %x %y (%y $))< (no_consec %x %y ($)).  ! can add y at front
  (no_consec %x %y (%x %y $))< (no_consec %x %y (%y $)). ! can add x to y-seq

!/ examples of (no_consec x y _no_consec_x) :  _no_consec = (), (y),
  (y _no-consec-x), where y is at front of a _no-consec-x str,
  (x _y-no-consec-x), where x is followed by a no-consec-x str starting w y
!\


!/ -- Everything to the end is OLD! -- But a few things may be of interest!!

!/ not needed! -- use  ((\ in) _elemseq _elems)  (see ho.ax)
! (elemseq _elems _elemseq) - form arg1 seq from elements in arg0 seq
! - _elemseq has >=0 occurrences of elements in _elems (in any order)
! - Note if _elems is a singleton set (_elem) then this is same as
!   (copies %elem %elemseq).

  (elemseq %elems ()).           ! no elems in seq
  (elemseq %elems (%el $els))<   ! adding elem to elems seq
    (elemseq %elems ($els)),
    (in %el %elems).               ! added elem is in set of elemens
!\

!/ move to ho.ax - use (/ prepend) instead of xdistr
! (all_subseqs _seq _allsubseqs) - seq of all subseqs of a seq
! - Recall that a subsequence of a sequence is itself or is obtained by
!   removing an element from a subsequence.
!   from that sequence or from one of its subsequences (thus always keeping
!   original element order).
! - A seq of length n will have 2^n subseqs.
! - Note that if _seq has distinct elements (and thus is a set), then
!   _allsubseqs is the powerset of that set (since each subseq has distinct
!   elements and is thus a set).

  (all_subseqs () (())).            ! empty seq has just the empty subseq
  (all_subseqs (% $) ($w% $w/o%))<  ! new head elem is both distributed to 
    (all_subseqs ($) ($w/o%)),      !  tail's subseqs and not distributed
    (xdistr % ($w/o%) ($w%)).

!/ examples:
    (all_subseqs () (()))        -- just the empty sequence itself
    (all_subseqs (c) ((c) ()))
    (all_subseqs (b c) ((b c) (b) (c) ()))
    (all_subseqs (a b c) ((a b c) (a b) (a c) (a) (b c) (b) (c) ()))
    ...
    ! How useful is this??!
!\

  ! Interesting variation tbd: Get subseqs in increasing (or decreasing) order.
  ! There may be other interesting collections one can define!
!\

! (ins_ _x _seq _seq^) - insert expr between elements of a sequence
! (but not before first element or after last)

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

! (ins._ _x _seq _seq^) - also insert expr before sequence

  (ins._ %x %seq (%x $seq^))<
    (ins_ %x %seq ($seq^)).

    ! - Note that _x would be inserted "before" a null sequence.

! (ins_. _x _seq _seq^) - also insert expr after sequence

  (ins_. %x %seq ($seq^ %x))<
    (ins_ %x seq ($seq^)).

    ! - Note that _x would be inserted "after" a null sequence.

! (ins._. _x _seq _seq^) - also insert expr before first and after last elem

  (ins._. %x () (%x)).        ! only insert expr once for a null sequence!
                  ! -- Or should we have 2 insertions for a null sequence??
  (ins._. %x %seq1 (%x $seq1^ %x))<
    (nonnull %seq1),                    ! seq1 has at least 1 elem
    (ins_ %x %seq1 ($seq1^)).

! (map _map _expr _expr') - apply finite map to an expr (in map's domain)

  (map %map %expr %expr')<
    (in (%expr %expr') %map).


    
!/ old - something for ho.ax ?:

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

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

!\
!\ -- End of OLD! --