! ho.ax - specification axioms for higher-order forms
! (Many of these are FP-style higher-order functional forms.)
! uses: form.ax
!/
   fp function format in AL:

      (f <arg> <result>)    -- always 1-argument function

   functional forms are used to combine functions into larger functions.
!\


! comp - composition of (single-argument) functions in right-to-left order

  ((comp) %arg %arg).          ! empty function list is identity function
  ((comp %f $f) %arg %res')<
    ((comp $f) %arg %res),
    (%f %res %ref').

! map (apply-to-all) - map a function to each element of a sequence
! (just one argument in this case -- gives sequence of results)
! ((map <f>) <seq> <seq'>) - where (<f> <elem> <elem'>) for each element

  ((map %f) () ()).
  ((map %f) (%elem $elems) (%elem' $elems'))<
    (%f %elem %elem'),
    ((map %f) ($elems) ($elems')).

!/ old:

  (map %f () ()).
  (map %f (%elem $elems) (%elem' $elems'))<
    (%f %elem %elem'),
    (map %f ($elems) ($elems')).

! or ...

  (map ($f) () ()).                 ! function may include "constant" args
  (map ($f) (%elem $elems) (%elem' $elems'))<
    ($f %elem %elem'),
    (map ($f) ($elems) ($elems')).
!\

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

! 1 - turn binary op into single arg function with operands in a 2-elem seq
! ((1 <binop>) (<arg1> <arg2>) <result>)

  ((1 %binop) (%arg1 %arg2) %result)<
    (%binop %arg1 %arg2 %result). 

! - also turn binary relation into single arg relation:

  ((1 %binrel) (%arg1 %arg2))<
    (%binrel %arg1 %arg2).

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

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

! - also apply to binary relation:

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

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

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

! - also apply to binary relation:

  ((*1 %binrel) () %arg2).
  ((*1 %binrel) (%arg1 $args1) %arg2)<
    (%binrel %arg1 %arg2),
    ((*1 %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

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

  ((1*_ %binop) %arg1 %arg2s %concatenated_results)<
    ((_ (1* %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)<
    ((_ (*1 (1* %binop))) %args1 %args2 %results).
 
! filter1* - filter second arg sequence for a Boolean binary operator
! ((filter1* <boolbinOp>) <arg1> <arg2s> <t-args2s>)

  ((filter1* %binop) %arg1 () ()).
  ((filter1* %binop) %arg1 (%arg2 $arg2s) ($arg2s'))<
    (%binop %arg1 %arg2 `f),        ! result is false - arg2 not included
    ((filter1* %binop) %arg1 ($arg2s) ($arg2s')).
  ((filter1* %binop) %arg1 (%arg2 $arg2s) (%arg2 $arg2s'))<
    (%binop %arg1 %arg2 `t),        ! result is true - arg2 is included
    ((filter1* %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)).

! valid - generating multiple valid expressions from a single expression

  % < (valid $1 % $2).

! all_valid - combine valid expressions into single expression

  (all_valid).
  (all_valid % $)< % , (all_valid $).
     ! -- all expressions in list are valid

! one_valid - assert that at least one expression in list is valid

  (one_valid $1 % $2)< % .
     ! -- (at least) one expression in list is valid

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

  %conclu < (axiom %conclu $conds), (all_valid $conds).

! axiom_set - generate a set of axioms from a single expression

  (axiom $axiom)< (axiom_set $1 ($axiom) $2).

! ax - define multiple axioms with shared conditions
! (ax (<conc> <cond> .. <cond>) .. (<conc> <cond> .. <cond>)
!     `< <cond> .. <cond>)      -- shared conditions

  (axiom %conclu $conds $shared_conds))<
    (ax $ax1 (%conclu $conds) $ax2 `< $shared_conds).
    ! -- no shared condition can be an `< atom  

! 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