! form.ax - utility predicates based on the form 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 funcions/relations
!   that cover all possible 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. ?
! "_term" with leading _ denotes a syntactic category used for documentation
!---+----1----+----2----+----3----+----4----+----5----+----6---+----7----+----8
!/ index:

=> categories:
  sets:
    seq nonnull null sing pair triple evseq odseq
  unary fn (1 input arg gives unique result):
    id head tail last front rev mid roth rotl
  binary relation (that is not a fn in either direction (except ==)):
    == perm rot  - symmetric
    pre suf in rmv substr subseq copies dupstr elcopy elcopy1 - nonsymmetric
    =l <l <=l >l >=l /=l
  binary functions (plus) - 2 input args with unique output:
    join join_ join* append1 prepend cat cat_ cat*
    xdistr xsdistr rdistrx rdistrxs
    asnpre | _ asnsuf | _
  length-index (0..) predicates:
    sel#l pre#l suf#l rot#l rmv#l - binary functions
    find#l findstr#l -  multi-valued bin fn (if >1 occur of searched expr/str)
    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 rmvstr insstr asnstr asnstr= split even|odd 
    no_consec all_subseqs ins_btw ins_<btw ins_btw> ins_<btw> map
  
 Alternate predicate names are sometimes given.
 Argument order may need to be revised!
 Predicate definition grouping and order may need refinement!

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

=== 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)
-- also do asnhead, asntail, asnlast, asnfront - assign (replace) with new
 (rev _seq _revseq) - reverse of a sequence
 (mid _seq _mid_elem) - middle elem of a seq (left of middle if even len)
 (roth (_h _tail_) (_tail_ _h)) - rotate the head element (alt: rot1)
 (rotl (_front_ _l) (_l _front_)) - rotate the last elem (alt: rot1-)
   -- 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)
 (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 (opp arg order?)
 (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
 (dupstr _seq1 _seq2) - 2nd sequence is concatenated copies 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 (plus nonbin 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 _seq _e _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') - concat >=0 input arg seqs into one
   -- cat_ w 0 iargs is same as 'null'; w 1 iarg, instance of 'id'
 (cat* (_seq_) _seq') - concat sequence of sequences into one
 (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
 (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
-- other length-index predicates:
 (find#l _e _seq _pos) - find expr in seq -> [_pos] (nondet if >1 occur)
   -- result _pos is unspecified seq of len _pos (ex: (%0 %1 %2) for _pos = 3)
 (findstr#l _str _seq _pos) - find str in seq -> start [_pos] (nondet)
   -- overlapping matches are distinct solutions!
 (ins#l _pos _seq _e _seq') - insert expr at (before) _seq[_pos]
 (asn#l _pos _seq _e _seq') - assign (replace) expr at _seq[_pos]
 (selstr#l _pos _len _seq _str) - select str w _len starting at [_pos]
   -- note that _len is sequence position numbering from [_pos]
   -- no solution if string length goes beyond end of sequence
      (could let 'selstr#l_' give as much string as possible)
 (rmvstr#l _pos _len _seq _seq') - remove _len-string starting at _seq[_pos]
 (insstr#l _pos _seq _str _seq') - insert string before sequence [_pos]
 (asnstr#l _pos _seq _str _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 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
 (rmv#-l _rpos _seq _seq') - remove elem [_rpos] from sequence
-- other length-index predicates:
 (find#-l _e _seq _pos) - find expr in seq -> [_rpos] (nondet if >1 occur)
   -- result _rpos is unspecified seq of len rpos
 (findstr#-l _str _seq _rpos) - find str in seq -> start [_rpos] (nondet)
   -- overlapping matches are distinct solutions
 (ins#-l _rpos _seq _e _seq') - insert expr at (after) _seq[_rpos]
 (asn#-l _rpos _seq _e _seq') - assign (replace) expr at _seq[_rpos]
 (selstr#-l _rpos _len _seq _str) - select str w _len ending at [_pos]
   -- note that _len is sequence position numbering from [_rpos]
   -- no solution if string length goes beyond front of sequence
      (could let 'selstr#-l_' give as much string as possible)
 (rmvstr#-l _rpos _len _seq _seq') - remove _len-string ending at _seq[_rpos]
 (insstr#-l _rpos _seq _str _seq') - insert string after sequence [_rpos]
 (asnstr#-l _rpos _seq _str _seq') - assign (repl) string ending at [_rpos]
   -- asnstr#-l|, asnstr#-l_ - analogous to asnpre|, asnpre_

 === more relations & functions ===
 (ins _seq _e _seq') - insert expr into seq at arbitrary position
 (asn _seq _e _seq') - assign (replace) expr in seq at arb pos
 (rmvstr _seq _seq') - remove arbitrary string from a sequence
 (insstr _seq _str _seq') - insert string into seq at arb pos
 (asnstr _seq _str _seq') - assign (replace) string in seq at arb pos
   - Replaced string and new string can have different lengths??
     (if replaced string has length 0, this is same as 'insstr')
 (asnstr= _seq _str _seq') - replaced string has same length as new
 (split _seq _half1 _half2) - split sequence into two halves (half1 gets 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
 (elemseq _elems _elemseq) - form arg1 seq from elems in arg0 seq
 (all_subseqs _seq (_subseq_)) - set of all subseqs of a sequence
   - "powerset" of sequence elements
 (ins_btw _seq _e _seq') - insert expr between elems of a seq
   - ins_<btw - also insert before first elem
     ins_btw> -     "       after last    "
     ins_<btw> -    "       before first and after last elems
 (map _map _expr _expr') - apply finite map to an expr (in map's domain)
!\

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


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

! seq - set of sequences

  (seq ($)).

! nonnull - non-null sequences (alt: seq>0)

  (nonnull (% $)).

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

  (null ()).

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

  (sing (%)).

! 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??

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

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

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

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


! ====== unary (single-valued) functions (= binary relations) ======

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

  (id % %).

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

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

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

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

! (last _seq _l) - last element in sequence

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

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

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

! (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 (- minimum odd seq)
  (mid (%0 %1) %0).   ! mid of pair (- minimum even seq with mid)
  (mid (%h $ %l) %m)<   ! adding new head & last --> mid stays the same!
    (mid ($) %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 for ==)

! -- 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 _seq1 _seq2) - sequence 2 is permutation of sequence 1 (& vice-versa)

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

! (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

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

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

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

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

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

!  (rmv _seq _seq') - remove expr from seq at arb position (opp arg order?)

  (rmv ($1 % $2) ($1 $2)).

! (substr _seq1 _seq2) - 1st sequence is substring of 2nd sequence

  (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) ($)).

! (copies _e _seq) - sequence is zero or more copies of expression _e

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

! (dupstr _seq1 _seq2) - 2nd sequence is concatenated copies of 1st seq

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

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

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

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

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

! -- length relations:

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

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

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

! (<=l _s1 _s2) - 1st sequence 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 sequence length greater than 2nd

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

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

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

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

  (/=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'.  Perhaps just use 'append'.

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

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

! (prepend _e _seq _seq') - prepend 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'

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

! (cat* (_seqs_) _seq') - cat sequence of sequences into one (unary fn)
! -- Note that the argument seqs are a partition of the result seq.

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

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

   (generalize cat ()).
!\

! (xdistr _x _seqs _seqs') - distr expr over fronts of seqs - ho: (.- 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')).

! (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
!  -- 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.. indexing)
! - position index defined by a sequence length

  (sel#l %pos ($pre %elem $suf) %elem)<
    (=l %pos ($pre)).    ! sequence prefix has length "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)).

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

  (rmv#l %pos ($pre %elem $suf) ($pre $suf))<
    (=l %pos ($pre)).
  
! -- other length-index predicates:

! (find#l _ex _seq _pos) - find expr in seq -> [_pos]
!   (nondeterministic if more than one occurrence)
! - any position soln possible, or none if _ex not present
! - result _pos is unspecified seq of len _pos (ex: (%0 %1 %2) for _pos = 3)

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

! (findstr#l _str _seq _pos) - find string in seq -> start [_pos]
!   (nondeterministic if more than one occurrence)
! - note that overlapping string matches will give distinct solutions

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

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

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

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

! (selstr#l _pos _len _seq _str) - select string of _len starting at [_pos]
! - note that _len is sequence position numbering from [_pos]
! - 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)).

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

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

! (insstr#l _pos _seq _str _seq') - insert string before sequence [_pos]

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

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

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

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

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

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

!/
! -- 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)
      `< (=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)))  
        ((asn#l %pos ($pre % $suf) %expr ($pre %expr $suf)))
        ((find#l %expr ($pre %expr $seq) %pos))
      `< (=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_ ?]
!\

      
! ====== _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)).

! -- other length-index predicates:
 
! (find#-l _ex _seq _pos) - find expr in seq -> [_rpos] (nondet if >1 occur)

  (find#-l %expr ($pre %expr $suf) %rpos)<
    (=l ($suf) %rpos).
 
! (findstr#-l _str _seq _rpos) - find str in seq -> ends at [_rpos] (nondet)
! - multiple solutions if overlapping matches

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

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

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

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

  (asn#-l %rpos ($pre %olde $suf) %newe ($pre %newe $suf))<
    (=l ($suf) %rpos).

! (selstr#-l _rpos _len _seq _str) - select str w _len ending at [_rpos]
!   -- note that _len is sequence position numbering from [_rpos]
!   -- no solution if string length goes beyond front of sequence
!      (could let 'selstr#-l_' give as much string as possible)

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

! (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 _seq _str _seq') - insert string ending at _seq[_rpos]

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

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

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

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

  (asnstr#-l| %rpos %seq %str %seq')<
    (asnstr#-1 %rpos %seq %str %seq').  ! rpos len + str len <= seq len
  (asnstr#-l| %rpos ($oldstr $suf) ($newstr0 $newstr1) ($newstr1 $suf))<
    (=l ($suf) $rpos),
    (=l ($oldstr) ($newstr1)).

! (asnstr#-l_ _rpos _seq _str _seq') - assign string ending at [_rpos]
! - if rpos len + str len > seq len, seq extended as needed

  (asnstr#-l_ %rpos %seq %str %seq')<   ! pos len + str len <= seq len
    (asnstr#-l %rpos %seq %str %seq').  ! - same as asnstr#-l
  (asnstr#-l_ %rpos ($ostr $suf) ($nstr0 $nstr1) ($nstr0 $nstr1 $suf))<
    (=l ($suf) %rpos),
    (=l ($ostr) ($nstr1)).

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


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

! (ins _seq _e _seq') - insert expr into seq at arbitrary position

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

! (asn _seq _e _seq') - assign (replace) expr in seq at arb pos

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

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

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

! (insstr _seq _str _seq') - insert string into seq at arb pos

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

! (asnstr _seq _str _seq') - assign (replace) string in seq at arb pos
!   - 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 ($pre $oldstr $suf) ($str) ($pre $str $suf)).
 
! (asnstr= _seq _str _seq') - replaced string has same length as new

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

! (split _seq _half0 _half1) - split sequence into two halves (half0 gets mid)
! - 0th half gets 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) - partition 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
! - 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 - (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 followed by no-consec-x str starting w y
!\

! (elemseq _elems _elemseq) - form arg1 seq from elements in arg0 seq
! - _elemseq has >=0 occurrences of elems in _elems (in any order)
! - Note if _elems is singleton (set (_elem) then this is same as
!   (copies %elem %elemseq).

  (elemseq (%) %seq%)<    ! elem seqs for just one elem
    (copies % %seq%).
  (elemseq (% $) %seq)<   ! elem added but no copies added
    (elemseq ($) %seq).
  (elemseq (% $) %seq')<   ! 0th element copy added
    (elemseq (% $) %seq),
    (ins %seq % %seq').    ! insert at random pos 

! (all_subseqs _seq (_subseq_)) - set of all subseqs of a sequence
! - subseq is subset of seq elements with order and duplicates kept
! - a seq of length n will have 2^n subseqs (there may be duplicates)

  (all_subseqs () (())).     ! empty seq has just the empty subseq
  (all_subseqs (% $) ($w% $w/o%))<  ! new head elem is distributed to 
    (all_subseqs ($) ($w/o%)),      !  tail subseqs or not
    (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) ()))
  ...
!\

  ! - alternative ordering of subseqs - increasing length:
  !   (), (a), (b), (c), (a a). (a b), (a c), (b a), (b b), ...
      
! (ins_btw _x _seq _seq') - insert expr between each element of a sequence
! (but not before first element or after last)

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

! (ins_<btw _x _seq _seq') - also insert expr before first element

  (ins_<btw %x ($seq) (%x $seq'))<
    (ins_btw %x ($seq) ($seq')).

    ! - note x would be inserted "before" a null string

! (ins_btw> _x _seq _seq') - also insert expr after last element

  (ins_btw> %x ($seq) ($seq' %x))<
    (ins_btw %x ($seq) ($seq')).

! (ins_<btw> _x _seq _seq') - also insert expr before first and after last

  (ins_<btw> %x ($seq) (%x $seq' %x))<
    (ins_btw %x ($seq) ($seq')).

    ! - note x would be inserted before and after a null string - ??

! (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 ?:

! 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)).


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

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

!\