! bool.ax.txt - Boolean functions that use or yield `t/`f (true/false) values
! We also include predicates involving `nil.
----+----|----+----|----+----|----+----|----+----|----+----|----+----|----+----8
!/ uses form.ax, ho.ax, bit.ax ...
t, f, tf - true/false representation values (hidden in this file)
tfset - the set of true/false values
tfseq - a sequence of true/false values
t/f_sel - select from two values based on t/f index
tf_fn - combine complementary binary relations to yield a true/false function
and? - conjuction of t/f values
or? - disjuction of t/f values
not? - map `t/`f to `f/`t
(not? <tffn>) - complement of Boolean function
in? - test if elem in a sequence or not (given bit-distinguishability)
=len?, <len?, <=len? - seq length boolean fns
/=len?, /<len?, /<=len? - more seq length boolean fns
=set? - test if two sequence sets are equal (given bit-distinguishability)

map/nil - map unary function to each element of a seq to get seq of results
!\

! t, f, tf - true/false representation values (hidden in this file!)
! (analogous to bit0, bit1, bits preds - should we just use these for t/f??)

  (t `t).
  (f `f).
    ! - alternative representations:
    !   `true, `false     - longer names
    !   `1, `0            - just use bits for true/false
    !    t, f,  true, false  - ordinary symbols
    
  (tf %t %f)< (t %t), (f %f).

! tfset - the set of true/false values

  (tfset %tf)< (one_valid (t %tf) (f %tf)).

! tfseq - a sequence of true/false values

  (def tfseq (* tfset)).

! tf_sel - select from two values based on t/f index

  (tf_sel (%tval %fval) %t %tval)< (t %t).
  (tf_sel (%tval %fval) %f %fval)< (f %f).

! tf_fn - combine complementary binary relations to yield a true/false function
! - a higher-order form - belongs in ho.ax??

  ((tf_fn %tbr %fbr) %1 %2 %t)<
    (%tbr %1 %2 %t),
    (t %t).
  ((tf_fn %tbr %fbr) %1 %2 %f)<
    (%fbr %1 %2 %f),
    (f %f).

  ! - It would be an error if (<tbr> <1> <2>) and (<fbr> <1> <2>) were both
  !   valid for some arg pair <1> <2>.
  ! - Ideally, we want <tbr> and <fbr> combined to be a total function over
  !   some arg pair domain.

! and? - conjuction of (zero-or-more) t/f values

  (and? $tfargs %t)<
    (t %t),
    (copies %t ($tfargs)).  ! all args are true
  (and? $tfargs %f)<
    (f %f),
    (tfseq ($tfargs)),
    (in %f ($tfargs)).     ! at least one arg is false
  ! - can't use in? here since `t/`f are not bit-distinguishable
    
! or? - disjunction of (zero-or-more) t/f values

  (or? $tfargs %f)<
    (f %f),
    (copies %f ($tfargs)).
  (and? $tfargs %t)<
    (t %t),
    (tfseq ($tfargs)),
    (in %t ($tfargs)).

! not? - map true/false to false/true

  (valid (not? %t %f)
         (not? %f %t))< (tf %t %f).

! (not? <tffn>) - complement of Boolean function

  ((not? %tf_fn) $args %tf)<
    (%tf_fn $args %ft),
    (not? %tf %ft).

! in? - test if elem in a sequence or not (given bit-distinguishability)

  (def in? (tf_fn in /in)).
  
  ! - Note that we adopt the convention that a name ending in ? denotes a
  !   function that yields a boolean result.

! =len?, <len?, <=len? - seq length boolean fns

  (def =len? (tf_fn =len /=len)).
  (def <len? (tf_fn <len >=len)).
  (def <=len? (tf_fn <=len >len)).

! /=len?, /<len?, /<=len? - more seq length boolean fns

  (def /=len? (not? =len?)).
  (def /<len? (not? <len?)).
  (def /<=len? (not? <=len?)).

! =set? - return t/f if two sequence sets are equal
! (order and duplicates do not matter - inequality requires bit disting.)

  (=set? %seq1 %seq2 %t)<
    (t %t),
    (all_in %seq1 %seq2),
    (all_in %seq2 %seq1).
  ! - or use permutation if no duplicates!

  (=set? %set1 %seq2 %f)<
    (f %f),
    (one_valid (some_/in %set1 %set2)
               (some_/in %set2 %set1)).


! map/nil - map a unary function to each elem of a seq to get seq of results
! - A "defined" result for function application will be a sequence value,
!   else the result must be the `nil value, in which case the function
!   result is omitted from the result sequence.

  (map/nil %f () ()).
  (map/nil %f (% $) (%r $r))<
    (%f % %r),
    (seq %r),              ! func has defined value, so we include its result
    (map/nil %fn ($) ($r)).
  (map/nil %f (% $) ($r))<
    (%f % `nil),           ! func value undefined, so result is omitted
    (map/nil %f ($) ($r)).