! bool.ax.txt - Boolean functions that yield true/false values
! - also includes non-Bool-fn predicates that use t/f values
! More higher-order operations are defined that involve Booleans.
! We adopt the convention of having '?' at the end of a Boolean function name.
! uses form.ax ho.ax atom.ax char.ax
!/
 t, f, tf - true/false representation values (hidden in this file)
 tfset - the set of true/false values
 tfseq - sequence of the 2 true/false values
 t/f_sel - select from two values based on t/f index
 tffn? - combine complementary relations to make a Boolean function
 tffn: - define Boolean function from complementary relation
 and? - conjuction of t/f values
 or? - disjuction of t/f values
 not? - map `t/`f to `f/`t
 (~ _Bf?) - complement of Boolean function
 in? - test if elem in a sequence or not (given bit-distinguishability)
 =l?, ~=?, <l?, >l?, <=l?, >=? - sequence length Boolean fns
 dig? - test if char expr is a digit
 ltr? - test if char expr is a letter
 (cnsc? _Bf?) - test if consecutive Bf?=true values exist in a sequence
 (Bf?{ _seq _seq') - "filter" seq keeping elems where Bf? is true
 (>{ _xymap) - apply x>y map to x-seq giving y-seq when x-elems in map
!\


!---+----|----+----|----+----|----+----|----+----|----+----|----+----|----+----8


! 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 >=0 true/false values  -- needed? - just use *tfset

  (def tfseq *tfset).

! We need to "declare" t/f atoms:

  (atoms (`t  `f)
         ("t" "f")).


! tf_sel - select from two values based on t/f index
! - Should false value come before true value??  - probably not

  (tf_sel %t (%tval %fval) %tval)< (t %t).
  (tf_sel %f (%tval %fval) %fval)< (f %f).
    ! - Nicer to put selection index as arg0 of this function?
    ! - Note that this is not a Boolean fn since it doesn't return t/f.


! tffn? - combine complementary relations to make a Boolean function
! - a higher-order form used in definitions below
! - This is a Boolean function with parameters.

  ((tffn? %trel %frel) $targs %t)<
    (%trel $targs),       ! "true" rel is valid for "true" args
    (t %t).
  ((tffn? %trel %frel) $fargs %f)<
    (%frel $fargs),      ! "false" ("negative") rel is valid for "false" args
    (f %f).

  ! - It would be an error if (_trel _args_) and (_frel _args_) are ever valid
  !   for the same argument string.
  ! - Ideally, we want _trel and _frel combined to be a total function over
  !   some argument string domain.


! tffn: - define Boolean function from complementary relation
! - a little more compact than using def everwhere!

  (tffn: %Bf? %trel %frel)<
    (def %Bf? (tffn? %trel %frel)).


! and? - conjunction of list of zero-or-more t/f values
! ??? Let and? function just apply to two input args,
!     and?_ can apply to list of 0 or more,
!     and?* can apply to a seq of args.
!     - like cat, join, plus, times, other?

  (and? $targs %t)<
    (t %t),
    (copies %t ($targs)).   ! all args are true
  (and? $tfargs %f)<
    (f %f),
    (tfseq ($tfargs)),
    (in %f ($tfargs)).      ! at least one arg is false

!/ alt defn:
  (and? $tfargs %tf)<
    (tfseq ($tfargs)),
    (~in? %f ($tfargs) %tf).    ! requires in? and ~ h-o op defined below
!\

 ! *** Have 2-arg and?, sequence and*? and multiarg and_?, like cat!
 !     (same for or?)

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

  (or? $fargs %f)<
    (f %f),
    (copies %f ($fargs)).    ! all args are false
  (or? $tfargs %t)<
    (t %t),
    (tfseq ($tfargs)),
    (in %t ($tfargs)).       ! at least one arg is true


! not? - map true/false to false/true  (alt?: ~)

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


! (~ Bf?) - complement of a Boolean function

  ((~ %Bf?) $args %ft)<     ! this is only defined for Boolean fns
    (catsym %Bfsym ? %Bf?),   ! Boolean function name %Bf? ends w ?
    (%Bf? $args %tf),
    (not? %tf %ft).

  (hopre ~).      ! ~ can be prefix for a Boolean function 

  ! *** Note that a leading ~ on a predicate symbol without an ending ? is
  !     often used for a "negative" predicate, which is not a Boolean function!


! in? - test if elem in a sequence or not
! - uses atom-distinguishability

  (tffn: in? in ~in).
  
  ! - Note that we require a name ending in ? to denote a Boolean function
  !   (- a function that yields a t/f result).


! =l?, ~=l?, <l?, >l?, <=l?, >=l? - seq length Boolean fns

  (tffn: =l? =l ~=l).
    ! ~=l? - application of ~ prefix to =l?
  (tffn: <l? <l >=l)).
  (tffn: >l? >l <=l)).
  (tffn: <=l? <=l >l)).
  (tffn: >=l? >=l <l)).

!/ more compact!:
  (*tffn:  ( =l?  <l?  >l?  <=l?  >=l?)    ! Bool fns being defined
           ( =l   <l   >l   <=l   >=l )    ! true relations
           (~=l  >=l  <=l    >l    <l )).  ! false relations
!\

! dig? - test if char expr is a digit
! (recall char expr is a char or a seq of char exprs)

  (tffn: dig? dig ~dig)).


! ltr? - test if char expr is a letter

  (tffn: ltr? ltr ~ltr)).


! (cnsc? Bf?) - consecutive Bf?=true values exist in a sequence
! - Note that cnsc? is a Boolean function on the sequence.
! - Bf? is a parameter of the cnsc? function.

  ((cnsc? %Bf?) %seq %t)<     ! consecutive Bf?=true elements exist in seq
    (t %t),
    ((* %Bf?) %seq %tfseq),    ! apply Bf? to seq elems to get seq of t/f
    (substr (%t %t) %tfseq).   ! two consecutive 'true' values exist
  ((cnsc? %Bf?) %seq %f)<     ! no consecutive Bf?=true elems exist in seq
    (tf %t %f),
    ((* %Bf?) %seq %tfseq),    ! get seq of t/f
    (no_consec %t %f %tfseq).  ! no consecutive t in t/f seq (see form.ax)
    ! - see form.ax 

  (hopre cnsc?).  ! This Bf? name can be combined w its param Bf?: cnsc?Bf? .
                  ! The combined name is a Bool fn on the sequence!


! (Bf?} _seq _seq') - "filter" seq keeping elems where Bf? is true
! - Note that the filter fn itself is not a Boolean function.

  (axs              ! we factor out the shared conditions for these two axioms
    ((%Bf?{ () ()))                    ! empty seq is filtered
    ((%Bf?{ (%tx $seq) (%tx $seq'))    ! keep    "true" seq expr element
    ((%Bf?{ (%fx $seq) ($seq'))        ! discard "false"       "
  )< 
    (catsym %Bf? { %Bf?{),    ! "filter" symbol { appended to Bool fn sym
    (tf %t %f),
    (%Bf? %tx %t),            ! Bool fn is true for a "true" seq expr
    (%Bf? %fx %f),            !        "   falset  "  "false'   "
    ((%Bf?{ ($seq) ($seq')).  ! filter rest of seq


! ((>{ _xymap) - apply map x>y to x-seq giving y-seq when x-elems in map
! (Similar to (*map _x>y _xseq _yseq') (- see 'map' in form.ax) except here
!  we allow for an xseq elem z to not be in the x>y map, in which case no
!  corresponding yelem is added to the resulting yseq.) 

  (axs
    (((>{ %xymap) () ()))
    (((>{ %xymap) (%x $xseq) (%y $yseq)))      ! x in x>y, y added
    (((>{ %xymap) (%z $xseq) ($yseq)))
  )<
    (map %xymap %x %y),        ! x,y in x>y map
    ((*sel1 %xymap %xdomain),  ! 1st elem of x>y map pairs gives xdomain seq
    (~in %z %xdomain),         ! z is not in domain of x>y
    ((>{ ($xseq) ($yseq)).     ! apply to rest of xseq

 ! *** Also create version '>{nil' that gives `nil atom for z value??!


!---+----|----+----|----+----|----+----|----+----|----+----|----+----|----+----8
!/
***** To Be Done:

! =set? - return t/f if two sequence sets are equal
! (order and duplicates do not matter

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

  ! example would be good here - div by 0, avg of nat seqs, including empty seq
!\