! ho.ax.txt - specification axioms for higher-order forms
! uses: form.ax
! -- more form.ax-type definitions are in this file, using the h-o forms
! -- more higher-order definitions are in bit.ax, char.ax, bool.ax
!/
  Many higher-order forms support a functional programming paradigm where
  function valid expresssions have >=0 input argument exprs and a single
  unique result expr:

    (_func _iargs_ _result)      - function valid expr format
      ! - "multi-valued functions" would not be used for this fp paradigm 

  A the functions used here have a fixed number of input arguments.  Note that
  a function with zero input arguments would be a "constant" function.
  Functions often operate on a "stack" of expressions, where a
  function takes its input arguments from the "front" of the stack
  (i.e., the "top") and replaces them with the result expression.
  Functions are typically "composed" where functions operate on the
  stack one after another.

  For example, a Program that reads >=0 input text files and writes a single
  output text file is defined from a function composition by the 'Prog:'
  higher-order form below.

  A function can be a symbol fsym or an expression (fsym _params_) where
  parameters are a string of "data" expressions that "instance"the function.

/ move this to form.ax:
Predicate (functions & relations) primitive symbols start with lower-case
letters and special characters '< > = ~'.  Characters after the first can
include decimal digits and special characters '_ * ? .'.  (See form.ax.)
\

 *** See char.ax for more higher-order definitions (once decimal
     numbers and other char/symbol utilities have been defined.
     Also see bool.ax for Boolean-related higher-order utilities.

index:

===== h-o forms for valid exprs and axioms =====
 (val _e_) - exprs in list all become valid exprs when used as conclu expr
 (val _ve_) - exprs in list must already be valid exprs (used as cond)
 (val1 _e_ _ve _e_) - at least one expression in list must be valid (cond)
 (ax _conclu _cond_) - define axiom using list of expressions (used as conclu)
 (axs _(_conc _cond_)_) - define set of axioms from a list
 (axs* (_ax_)) - define set of axioms from a single expression

===== higher-order forms for predicates (functions & relations) ===== 
 (def _pname _expr) - define a name for a predicate expression
 (Prog: _fcomp_) - define text-file "Program" from a function composition
 (: _fname _fcomp_) - define name for a function composition
   - note: def assigns name to an expr; ':' assigns name to a string
 ((: _fc_) _stk _stk') - l-to-r fn/oper composition on arg stack in seq
 ((_ _p1) _vals_) - list of 1-arg-predicate values (such as set values)
 ((* _p) _argseqs_) - apply pred to tuples formed from argument sequences
 ((/ _b) _arg0 _arg1s _ress) - do binrel/fn on pairs of arg0-arg1s [->results]
 ((\ _b) _arg0s _arg1 _ress) -                "         arg0s-arg1 [->  "    ]
   - Actually these h-o forms are generalized for any # args.
   - note: / is one-many, \ is many-one arg0-1 pairing
   - (\ (/ bin)) on (a0..an) (b0..bm) argseqs -> ((a0b0..a0bm)..(anb0..anbm))
   - (/ (\ bin)) on (a0..an) (b0..bm) argseqs -> ((a0b0..anb0)..(a0bj..anbm)) 
   - thus composition of these operators can apply bin rel/fn to all arg pairs
   - / \ operators take a bin rel/fn and produce a bin rel/fn
 ((. _f) (_iargs_) _res) - fn input args are in a seq (-> (. f) unary!)
 ((& _f) _iargs_ (_iargs_ res)) - f input args included in seq with fn result
x ((@r _p) _rargs_) - reverse the arguments for a predicate

===== higher-order operators for function composition stack =====
 (^ _x) - insert x at front of stack for func composition
z ((_f ^) ...) - move arg0 into the function parameter position, then apply
   - this is now a suffix defined in char.ax
? (param _p_) - define parameterized versions of preds where arg0 is param
    ! ins_ ins._ ins_. ins._.  - these form.ax fns get parameterized below
 del - delete (pop) arg0 from front of stack
 dup - duplicate arg0 at the front of the stack
 swap - swap args 0,1 at the front of the stack

!/ mostly old, but some may be interesting ...
=== h-o forms for binary relations/functions =====
 ((bun _b) _args_) - apply bin rel/fn to a pair of args (make rel/fn unary)
 heads - head elements of sequences in a sequence
 ((rev <binrel>) <arg1> <arg2>) - reverse args for a binary relation
 head_fn - unary function to get head of a sequence
 >len, >=len - reversed seq length comparison
 ((.* _binrel) _arg1 _arg2s) - rel aplies to 1st arg and each arg2 elem
 ((*. _br) _arg1s _arg2) -        "       to each arg1 elem and arg2
 ((.* _binfn) _arg1 _arg2s _ress) - apply fn to 1st arg and each arg2 elem
 ((*. _bf) _arg1s _arg2 _ress) -         "   to each arg1 elem and arg2
 ((** _br) _arg1s _arg2s) - apply rel to each arg1/arg2 elem pair
 ((^. _br) _arg1s _arg2) - rel valid for at least one arg1 elem wrt arg2
 ((^* _br) _arg1s _arg2s) - for each arg2 elem, at least 1 arg1 elem has rel
 ((seq _br) _seq) - for adjacent seq elems we have _ei _br _ei+1
 ((seq* _br) _seq) - br applies between each ordered pair ei,ej from seq
!\ ... mostly old
!\

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



======= h-o forms for valid exprs and axioms =======


! val (used as conclu) - generate multiple valid exprs from single conclu expr
! (alt: valid val: val!)  - asserts/defines that exprs in list are valid
! (Note that an exclamation point can be part of a symbol after first char.)

  % < (val $0 % $1).   ! all exprs in 'val' list are made valid

!/ exmpl: given axiom
     (val _exA _exB _exC)< _conds_.
!\ if all _conditions_ are valid, then exprs _e`xA,B,C will all be valid

! val (used as cond) - a (val ..) expr is valid if all its exprs are valid
! (alt: all_valid val?)  -- tests that all exprs in its list are valid

  (val).
  (val % $)< % , (val $).
     ! -- all exprs in 'val' list must be valid for 'val' expr to be valid

!/ ex: given axiom
     _exX < (val _ex0 _ex1 _ex2).
!\ if exprs _ex0,1,2 are all valid exprs, then expr _exX will be valid

! val1 - a (val1 ..) expr is valid if at least 1 of its exprs is valid

  (val1 $a %ve $b)< %ve .

!/ ex:
  (val1 (pair (%)) (pair ()) (pair (u v)))  is a valid expr
!\

! *** Axiom language makes it easy to represent axioms as data! ***

! ax - represent an axiom in a single expression
! (ax <conclu> <cond1> .. <condn>)

  %conc < (ax %conc $conds), (val $conds).

! axs - represent a (sub)set of axioms as a list of axiom expressions

  (ax $axiom)< (axs $a ($axiom) $b).

!/ Note that we can factor out shared conditions for multiple axioms.  This:
     (axs _axioms_)< cond0, .., condk).
   is equivalent to writing each of the axioms separately with the conds0-k
!\ added.

! axs* - represent set of axioms in a single expression:

  (axs $axioms)< (axs* ($axioms)).



===== higher-order forms for predicates & functions =====


! (def _pname _expr) - define a symbol name for a predicate expression

  (%pname $args)<
    (def %pname %expr),
    (%expr $args).           ! pname's args same as expr's args


! (Prog: _fcomp_) - defines Program function for text files -- text file i/o
! - generates 'Program' valid exprs from a function composition
!   (Program _iargs_ _res) - Program function expression definition
! - Program maps >=0 input text files to a single output result text file

  (Program $args %res)<        ! Program maps >=0 input text files to 1 output 
    (Prog: $fc),               ! program is defined as a function composition
    ((: $fc) ($args) (%res)).  ! fn comp maps inp file seq to seq w 1 outp file

! -- Functions have >=0 input argument exprs and 1 unique result output expr:
!       (_func _iargs_ _res)
!    Note that for the function expressions that define programs, we
!    always know the number of input arguments.  That is, it is fixed
!    for a given function.


! (: _fname _fcomp_) - defn of new function name for a function composition
! - Note that 'def' operator would require _fcomp_ to be enclosed in parens.

  (%fname $iargs %res)<    ! the defined fn maps >=0 inp args to single result
    (: %fname $fcomp),
    ((: $fcomp) ($iargs) (%res)).   ! fn comp must eval inp stk to 1-arg stk

! Note: 'def' assigns name to an expr; ':' assigns name to a string.


! ((: _fc_) (_args_) (_args'_)) - fn comp maps inp stk to outp stk in a seq
! - A function composition incrementally applies fns to front of stack
!   gradually "consuming" stack arguments until a single result arg remains.
! - A fn comp can also include operations that manipulate the stack.
! - Note that : is a unary function that maps an input stack to an output
!   stack, both in sequences where the "top" of the stack is at the front.
! - The parameters of the : function are the functions/operations that are
!   composed.

  ((:) ($args) ($args)).   ! empty composition is the identity fn on arg seqs
      ! (The remaining stack args at the completion of a function composition
      ! are copied to the output stack sequence.)

  ((: %f $fc) ($iargsf $args) ($args'))<   ! apply next function of compositn
    (%f $iargsf %resf),                    ! func maps input args to result
    ((: $fc) (%resf $args) ($args')).      ! we replace input args w result,
                  ! ... then apply rest of fn compos to get (: ...) result

!/ Note that the "constant function" pushes its parameter expr ...
  ((: (^ %x) $fc) ($args) ($args'))<       ! push expr x onto front of stack
    ((: $fc) (%x $args) ($args')).
!\ ... onto front of stack.  (This follows from preceding axiom.)

  ((: del $fc) (%arg0 $args) ($args'))<    ! delete (pop) arg0 from stack
    ((: $fc) ($args) ($args')).

  ((: dup $fc) (%arg0 $args) ($args'))<    ! duplicate arg0 onto front of stack
    ((: $fc) (%arg0 %arg0 $args) ($args')).

  ((: swap $fc) (%arg0 %arg1 $args) ($args'))<   ! swap args 0,1 on stack  
    ((: $fc) (%arg1 %arg0 $args) ($args')).

 ! See char.ax for d (decimal digit num) suffix for del and dup to replace
 ! arg 0 with arg d and for swap to replace arg 1 with arg d.



! ======= Higher-Order Forms =======
!/
  Higher-order forms are operators that apply to predicates to make new
  predicates.  (By "predicates" we mean functions (that produce a result
  from arguments) and relations (that are valid for some arguments).
  Higher-order operators are typically symbols that have the predicate
  symbol as a parameter:

    ((_hosym _psym) _args_

  Sometimes the predicate itself may be a symbol with its own parameters:

    ((_hosym (_psym _params_)) _args_)

  In char.ax for conciseness and readability we define a catenation of the
  higher-order symbol (often just 1 character) with the predicate symbol
  to produce new predicate symbol:

    (_hosympsym _args_)
    ((_hosympsym _params_) _args_)
       ! - this saves 3 characters!

    ! *** see char.ax! ***
!\


! ((_ _p1) _args_) - for 1-arg predicate (typ set), define list of set elems

  ((_ %pred1))< (%pred1 %val);
  ((_ %pred1) %val $vals)< (%pred1 %val), ((_ %pred1) $vals).

!/ Example valid exprs:
  ((_ pair) (a b) (() 3))
!\ 
!/ some old comments:

 **** Or should this h-o form _ be a suffix???

 **** Also do case of a constant expr repeated in a seq or a flat list!!!
     *** Need nesting of these operations! - seq of seqs of const exprs!
         (same expr or different exprs!?)
     -- Probably sacrifice conciseness for nesting power!!
          -- Or maybe we can have both!!!
!\


! ((* _p) _argseqs_) - map pred to arg tuples from arg seqs

  ((* %pred) $nulls)<            ! - note that %pred may be (_psym _params)
    (copies () ($nulls)),        ! ($nulls) is a sequence of ()
        ! - could use  ((/ ==) () ($nulls))  here, with / defined below 
    (%pred $args),
    (=l ($args) ($nulls)).       ! nice if # nulls matches # pred args
  !? (=nulls ($args) ($nulls))    -- useful utility??  (alt: seqsn=)
  !      (nulls (.. () ..))   - seq of null seqs  (alt: seqsn seqs0)
        
  ((* %pred) $argseqs')<
    (%pred $args),
    ((* %pred) $argseqs),
    (distr ($args) ($argseqs) ($argseqs')).

  ! *** Note that distr is a * map of the prepend function!
  !     (But that would mean we need distr in order to define distr!
  !     Or need * to define *!
  !     So for now we will use the form.ax definition.)

  ! - This is also used to map a function to sequences of input arguments,
  !   yielding a sequence of results.

  ! - Note that the * mapping applies a predicate to sequences of arguments,
  !   but not to sequences of parameters.  The arguments are all operated on
  !   by the same "parameterized predicate".


! ((/ _pred) _arg0 _argseqs) - apply pred to single arg0 and remaining argseqs
! - a one-many relation between arg0 and args>0
!/ This will normally be applied to a binary relation between one arg0 and
   multiple arg1s,
     ((/ >l) (* * * *) (() (a) (a b c)))
   or binary function where one arg0 and multiple arg1s give multiple results:
!\   ((/ join) a (x y z) ((a x) (a y) (a z)))

  ((/ %pred) %arg0 $nulls)<
    (copies () ($nulls)),
    (%pred %arg0 $args),
    (=l ($args) ($nulls)).

  ((/ %pred) %arg0 $argseqs')<
    (%pred %arg0 $args),
    ((/ %pred) %arg0 $argseqs),
    (distr ($args) ($argseqs) ($argseqs')).


! ((\ _pred) _arg0s _arg1 _arg>1s_) - apply pred to one arg1, other args seqs
! - a one-many relation between arg1 and the other args, which are sequences
! - usually used for binary relations:  ((\ in) (b c e) (a b c d e f))
!       and for binary functions:  ((\ prepend) (g h) (u v) ((g u v) (h u v)))

  ((\ %pred) () %arg1 $nulls)<
    (copies () ($nulls)),
    (%pred %arg0 %arg1 $args>1),
    (=l ($args>1) ($nulls)).
  
  ((\ %pred) %arg0seq' %arg1 $arg>1seqs')<
    (%pred %arg0 %arg1 $args>1),
    ((\ %pred) %arg0seq %arg1 $arg>1seqs),
    (distr (%arg0 $args>1) (%arg0seq $arg>1seqs) (%argseq' $arg>1seqs')).

!/
  Merging / and \ higher-order forms on binary rel/fn pred arg sequences: 
    \ / bp on (a0..ai) (b0..bj) argseqs -> ((a0b0..a0bj)..(aib0..aibj))
    / \ bp on (a0..ai) (b0..bj) argseqs -> ((a0b0..aib0)..(a0bj..aibj)) 
    - Composition of these h-o ops apply bin pred to all arg combinations!
    - / \ operators take a bin rel/fn and produce a bin rel/fn

  join function examples:
          (join    a     x        (a x))
       ((/ join)   a    (x y z)  ((a x) (a y) (a z)))
    ((\ (/ join)) (a b) (x y z) (((a x) (a y) (a z))
                                 ((b x) (b y) (b z))))

       ((\ join)  (a b)  x       ((a x) (b x)))
    ((/ (\ join)) (a b) (x y z) (((a x) (b x))
                                 ((a y) (b y))
                                 ((a z) (b z))))
!\


! ((. _f) (_iargs_) _res) - f input args are in a seq (-> (. f) unary!)
! - Only makes sense for functions (which give a result), not relations.

  ((. %f) ($iargs) %res)<    ! - this makes function unary (i.e., 1 arg)
    (%f $iargs %res).        !   (or makes a relation binary!)


! ((& _f) _iargs_ (_iargs_ res)) - f input args are included in seq w f result
! - Only meaningful for functions (because they give a result).

  ((& %f) $iargs ($iargs %res))<
    (%f $iargs %res).


!/ -- possibly useful, but postpone for now:
! ((@r _p) _rargs_) - predicate's arguments are reversed
!  - useful for defining some binary relations

  ((@r %pred) $rargs)<     ! reverse order for predicate arguments
    (%pred $args),
    (rev ($args) ($rargs)).
!\

!/ -- deal with this later: 
! param - define parameterized version of specified preds with arg0 as param

  ((%p %arg0) $args)<
    (param %p),          ! predicate p can use arg0 as a parameter
    (%p %arg0 $args).

  (param %p)<     ! generalize param for list of preds
    (param $p),
    (in %p ($p)).

! create parameterized versions of some 0form.ax functions:

  (param ins_ ins._ ins_. ins._.).
    ! - The expression being inserted becomes part of the function!
!\



!/ OLD - maybe a few useful things here ...

!---+----1----+----2----+----3----+----4----+----5----+----6---+----7----+----8
! =========== higher-order forms for binary relations & functions ===========

! ((bun _b) _args_) - apply bin rel/fn to a pair of args (make rel/fn unary)

  ((bun %br) (%arg1 %arg2))<   ! binary relation becomes unary
    (%br %arg1 %arg2).

  ((bun %bf) (%iarg1 %iarg2) %res)<  ! binary fn (binop) becomes unary
    (%bf %iarg1 %iarg2 %res).

! heads - head elements of sequences in a sequence
! (1st arg is head elements of 2nd arg sequences)

  (def heads (* head)).

! ((rev _binrel) _arg1 _arg2_) - reverse arg order for binary relation

  ((rev %binrel) %arg1 %arg2)<
    (%binrel %arg2 %arg1).
    
!/ examples:
  ((rev in) (a b) b)
  ((rev head) (a b c) a)
  ((rev last) c (a b c))
  ((rev tail) (b c) (a b c))
!\

! ((rev _binfn) _arg1 _arg2 _res) - reverse arg order for binary function

  ((rev %binfn) %arg1 %arg2 %res)<
    (%binfn %arg2 %arg1 %res).

!/ examples:
  ((rev append1) c (a b) (a b c))
!\

! head_fn - unary function to get head of a sequence
! (This turns the head binary relation into a unary function.)

  (def head_fn (rev head)).

! >len, >=len - reversed arg 1, arg 2 sequence length comparison

  (def >len (rev <len)).
  (def >=len (rev <=len)).

! ((.* _binrel) _arg1 _arg2s) - rel applies to 1st arg and each arg2 elem

  ((.* %binrel) %arg1 ()).
  ((.* %binrel) %arg1 (%arg2 $arg2s))<
    (%binrel %arg1 %arg2),
    ((.* %binrel) %arg1 ($arg2s)).

!/ examples:
  ((.* in) x ((a x b) (c d x))   - arg1 elem in every arg2 seq
  ((.* head) a ((a b c) (a x)))   - same head elem in each arg2 seq
!\

! ((*. _br) _arg1s _arg2) - rel applies to each arg1 elem and arg2

  ((*. %binrel) () %arg2).
  ((*. %binrel) (%arg1 $arg1s) %arg2)<
    (%binrel %arg1 %arg2),
    ((*. %binrel) ($arg1s) %arg2).

!/ example:
  ((*. in) (x y z) (a x b z c y)) - each arg1 elem in arg2 seq - all_in,subset
!\

! ((.* _binfn) _arg1 _arg2s _ress) - apply fn to 1st arg and each arg2 elem

  ((.* %binfn) %arg1 () ()).
  ((.* %binfn) %arg1 (%arg2 $arg2s) (%res $ress)<   ! return seq of results
    (%binfn %arg1 %arg2 %res),    ! bin fn maps two input args to a result
    ((.* %binfn) %arg1 ($arg2s) ($ress).

!/ example:
  ((.* append1) (a b) (x y) ((a b x) (a b y)))
!\

! ((*. _bf) _arg1s _arg2 _ress) - apply fn to each arg1 elem and arg2

  ((*. %bf) () %arg2 ()).
  ((*. %bf) (%arg1 $arg1s) %arg2 (%res $ress))<   ! return seq of results
    (%bf %arg1 %arg2 %res
    ((*. %bf) ($arg1s) %arg2 ($ress).

!/ examples:
  ((*. prepend) (1 2) (u v) ((1 u v) (2 u v)))
!\

! ((** _br) _arg1s _arg2s) - rel applies to each arg1/arg2 elem pair
! ((*br _br) ? - covered by 'map' above
   ??? - probably easily defined from other h-o forms!
  
  ((** %br) () %arg2s).
  ((** %br) (%1 $1) %arg2s)<
    ((.* %br) %1 %arg2s),
    ((** %br) ($1) %arg2s). 

!/ example:
  ((** in) (b d) ((a b c d) (x d b y)))
!\

! ((^. _br) _arg1s _arg2) - rel valid for at least one arg1 elem wrt arg2

  ((^. %br) %arg1s %arg2)<
    (in %1 %arg1s),
    (%br %1 %arg2).

!/ examples:
  ((^. in) (a b c d) (x c y))
!\

! ((^* _br) _arg1s _arg2s) - for each arg2 elem, at least 1 arg1 elem has rel
!                            (not necessarily the same arg1 elem)

  ((^* %br) ($1a %1 $1b) ())< 
    (%br %1 %2).            ! binary relation must have a domain?
  (  (^* %br) %arg1s (%2 $2))<
    ((^. %br) %arg1s %2),
    ((^* %br) %arg1s ($2)).
    
!/ examples: 
  ((^* in) (c y) ((x y z) (a b c)))
!\

  ! *** Another possibly useful h-o <binrel> variation would be where
  !     at least one arg 1 elem has rel to each arg2 elem.
  !        ((^. (.* <binrel>)) <arg1> <arg2>)   -- wrong?!?  -- fix!!!

! ((.^ _br) _arg1 _arg2s) - rel valid for arg1 wrt at least one arg2

  ((.^ %br) %arg1 %arg2s)<
    (in %2 %arg2s),
    (%br %arg1 %2).

!/ examples:
  ((.^ head) a ((u v) (a b c)))   - 'a' is head of one arg2 elem seq
!\

! ((*^ _br) _arg1s _arg2s) - for each arg1 there is an arg2 elem
!                            (not necessarily the same arg2 elem)

  ((*^ %br) () ($2a %2 $2b))<
    (%br %1 %2).             ! binary relation must have a domain
  (  (*^ %br) (%1 $1) %arg2s)<
    ((.^ %br) %1 %arg2s)
    ((*^ %br) ($1) %arg2s).

! binary relation folds into a sequence of elements ...
! (note that relation does not need to be reflexive)
! ((seq _br) _seq) - for each adjacent seq elems we have <ei> <br> <ei+1>

  ((seq %br) ())<
    (%br %1 %2).         ! binary relation must be defined
  ((seq %br) (%2))<
    (%br %1 %2).         ! singleton element must be right elem of a bin rel
  ((seq %br) (%1 %2 $))<
    (%br %1 %2),
    ((seq %br) (%2 $)).
  
! ((seq* _br) _seq) - br applies between each ordered pair ei,ej from seq

  ((seq* %br) ())<
    (%br %1 %2).
  ((seq* %br) (% $))<
    ((.* %br) % ($))<
    ((seq* %br) ($)).


! ================ old: =================


! constr - apply sequence of functions to same argument giving seq of results

  ((constr) %arg ()).
  ((constr %f $f) %arg (%res $res))<
    (%f %arg %res),
    ((constr $f) %arg ($res)).

! filter - apply boolean pred to each element of sequence, keeping true values
! ((filter <pred>) <seq> <seq'>) - <seq'> is subset of <seq> where <pred> is `t
! (<pred> <expr> <`t/`f>) - true/false predicate on an expression

  ((filter %pred) () ()).
  ((filter %pred) (%elem $elems) (%elem $elems'))<
    (%pred %elem `t),
    ((filter %pred) ($elems) ($elems')).
  ((filter %pred) (%elem $elems) ($elems'))<
    (%pred %elem `f),
    ((filter %pred) ($elems) ($elems')).

   ! -- use higher-order form for the shared condition?

!/ old:

  (filter %pred () ()).
  (filter %pred (%elem $elems) (%elem $elems'))<
    (%pred %elem `t),
    (filter %pred ($elems) ($elems')).
  (filter %pred (%elem $elems) ($elems'))<
    (%pred %elem `f),
    (filter %pred ($elems) ($elems')).

! or ...

  (filter ($pred) () ()).             ! pred may include "constant" args
  (filter ($pred) (%elem $elems) (%elem $elems'))<
    ($pred %elem `t),
    (filter ($pred) ($elems) ($elems')).
  (filter ($pred) (%elem $elems) ($elems'))<
    ($pred %elem `f),
    (filter ($pred) ($elems) ($elems')).

   ! -- $pred may represent boolean function plus some "constant" parameters

! -- Is there another string-vs-expr var notation that is nicer here???
!\

! repeat - repeat 0 or more function applications

  ((repeat %f) % %).             ! 0 evaluations is identity function
  ((repeat %f) %arg %result')<   ! n+1 evaluations
    ((repeat %f) %arg %result),    ! n evaluations
    (%f %result %result').         ! one more evaluation

! partial - turn multi-argument function into a single argument function
!   by including the initial arguments as part of the function
! ("partial evaluation")

  ((partial %f $initial_args) %last_arg %res)<
    (%f $initial_args %last_arg %res).

! min - get element from sequence with minimum function result value
! - function result is a natural number

  ((min %fnat) (%elem) %elem).     ! if just one value, that's the min
  ((min %fnat) (% $) %)<           ! first element is new minimum
    (%fnat % %n0),
    ((min %fnat) ($) %min),
    (%fnat %min %n1),
    (<=num %n0 %n1).
  ((min %fnat) (% $) %min)<        ! first element is not new minimum
    (%fnat % %n0),
    ((min %fnat) ($) %min),
    (%fnat %min %n1),
    (<=num %n1 %n0).
  ! -- Note that definition is ambiguous if new element value same as min.
  !    Thus the function nondeterministically picks any minimum element.

 ! -- use higher-order form for the common conditions:

   (ax (((min %fnat) (% $) %) (<=num %n0 %n1))
       (((min %fnat) (% $) %min) (<=num %n1 %n0))
    `< (%fnat % n0)
       ((min %fnat) ($) %min)
       (%fnat %min %n1)
   ).

! define_func - define a name for a (single-argument) function expression

  (%name %arg %res)<
    (define_func %name %fn_expr),
    (%fn_expr %arg %res).

!/


! generalize - generalize certain associative binary operators with an identity
! -- We generalize operator to >2 arguments and to a sequence of >=0 args.

  (%binop %arg1 %arg2 $args %arg' %result')<     ! >2 arguments
    (generalize %binop %id),
    (%binop %arg1 %arg2 $args %result),          ! >=2 arguments
    (%binop %result %arg' %result').             ! adding an argument

  (%binop () %id)<                     ! empty argument sequence
    (generalize %binop %id).
  (%binop ($args %arg) %result')<      ! adding arg to sequence
    (generalize %binop %id),
    (%binop ($args) %result),
    (%binop %result %arg %result').

! move these to their original function definitions?:

  (generalize concat ()).
  (generalize plus 0).
  (generalize times (s 0)).
  (generalize and `t).
  (generalize or `f).


! Binary operator and binary relation higher-order forms:


! .* - apply first arg to sequence of second args to get sequence of results
! ((.* <binop> <arg1> <arg2-seq> <result-seq>)

  ((.* %binop) %arg1 () ()).
  ((.* %binop) %arg1 (%arg2 $args2) (%res $res))<
    (%binop %arg1 %arg2 %res),
    ((.* %binop) %arg1 ($args2) ($res)).

! - also apply to binary relation:

  ((.* %binrel) %arg1 ()).
  ((.* %binrel) %arg1 (%arg2 $args2))<
    (%binrel %arg1 %arg2),
    (.* %binrel) %arg1 ($args2)).

! *. - apply sequence of first args to second arg to get sequence of results
! ((*. <binop>) <arg1-seq> <arg2> <result-seq>)

  ((*. %binop) () %arg2 ()).
  ((*. %binop) (%arg1 $args1) %arg2 (%res $res))<
    (%binop %arg1 %arg2 %res),
    ((*. %binop) ($args1) %arg2 ($res)).

! - also apply to binary relation:

  ((*. %binrel) () %arg2).
  ((*. %binrel) (%arg1 $args1) %arg2)<
    (%binrel %arg1 %arg2),
    ((*. %binrel) ($args1) %arg2).

! _ - concatenate the (sequences) of a fn result sequence into a single sequence
! ((_ <fn>) <arg1> ... <argn> <result-seq>)
!    -- number of function input args is arbitrary but last elem must be result

  ((_ %fn) $args %result*)<
    (%fn $args %result),          ! get function result
    (concat %result %result*).    ! concatenate result subsequences

! .*_ - apply .* to binary operator and concatenate the results
! ((.*_ <binop>) <arg1> <arg2-seq> <concatenated results>)

  ((.*_ %binop) %arg1 %arg2s %concatenated_results)<
    ((_ (.* %binop) %arg1 %arg2s %concatenated_results).

    ! ??? This is probably not needed!

! **_ - binary operator cartesian product in flat sequence
! ((**_ <binop>) <a> <b>
!      (<a0xb0> <a0xb1> .. <a0xbn> <a1xb0> .. <a1xbn> ... <amxb0> .. <amxbn>))
!   -- note that the 2nd argument cycles faster

  ((**_ %binop) %args1 %args2 %results)<
    ((_ (*. (.* %binop))) %args1 %args2 %results).
 
! filter.* - filter second arg sequence for a Boolean binary operator
! ((filter.* <boolbinOp>) <arg1> <arg2s> <t-args2s>)

  ((filter.* %binop) %arg1 () ()).
  ((filter.* %binop) %arg1 (%arg2 $arg2s) ($arg2s'))<
    (%binop %arg1 %arg2 `f),        ! result is false - arg2 not included
    ((filter.* %binop) %arg1 ($arg2s) ($arg2s')).
  ((filter.* %binop) %arg1 (%arg2 $arg2s) (%arg2 $arg2s'))<
    (%binop %arg1 %arg2 `t),        ! result is true - arg2 is included
    ((filter.* %binop) %arg1 ($arg2s) ($arg2s')).


! finite_set - define a finite set in a single expression

  (%set %elem)< (finite_set %set ($1 %elem $2)).

 ! example:
 !   (finite_set day (Sun Mon Tue Wed Thu Fri Sat)).


! eval - Lisp-like expression evaluation (from paper)

  (eval (quote %expr) %expr).      ! value is unevaluated expression
  (eval %dec_sym %value)<          ! value of decimal number symbol
    (dec_sym %dec_sym %value).
  (eval (%fn $args) %result)<      ! evaluate function on arguments
    (eval* ($args) ($results)),    ! evaluate argument expressions
    (%fn $results %result).        ! evaluate function on argument results
       ! -- this works for functions that yield a single result at end of list

!\ ... OLD