! balanced.ax - axioms for balanced parentheses program
!  -- tests if input string has balanced parentheses
!
! User enters input string with parentheses and other characters.
! Program types "Ok" if parentheses are balanced, else gives error
! message.  An empty input string terminates the program.
!
! example Program expr:
!
!   (Program Balanced
!     ("Enter strings with balanced parentheses ...")
!      "(ab()(3 2 1)x)"
!     ("Ok")
!      "((ABC)))()"
!     ("       ^ extra right parenthesis")
!      "(1(23"
!     ("     ^ missing right parenthesis")
!      ""
!     ("Bye!"))

! Program - defining the balanced parentheses program

   (Program Balanced
     ("Enter strings with balanced parentheses ...")
      ""                      ! immediate termination
     ("Bye!")).
   (Program $history %in %out "" ("Bye!"))<
     (Program $history "" ("Bye!")),
     (interaction %in %out).

! interaction - processing a non-terminating user interaction

   (interaction (% $) "Ok")< (bal_parens (% $)).   ! non-null balanced string
   (interaction %extra ($blanks '^ extra right parenthesis'))<
     (unbal_parens_extra %extra ($blanks)).
   (interaction %missing ($blanks '^ missing right parenthesis'))<
     (unbal_parens_missing %missing),
     (blank_seq ($blanks)),
     (=len %missing ($blanks)).

! bal_parens - character string with balanced parentheses

   (bal_parens ()).               ! empty string has balanced parens
   (bal_parens (%nonparen))<      ! a non-parenthesis char is balanced
     (char %nonparen),
     (not_in %nonparen "()").
   (bal_parens ('(' $bal ')'))< (bal_parens ($bal)).  ! adding paren pair
   (bal_parens ($bal1 $bal2))<        ! concatenating balanced paren strings
     (bal_parens ($bal1)),
     (bal_parens ($bal2)).

! unbal_parens_missing - string with one or more missing right parentheses

   (unbal_parens_missing ($1 '(' $2))< (bal_parens ($1 $2)).
   (unbal_parens_missing ($1 '(' $2))< (unbal_parens_missing ($1 $2)).

! unbal_parens_extra - string with one or more extra right parentheses
! -- blank string gives the position of the first extra right paren

   (unbal_parens_extra ($bal ')' $chars) %blanks)<
     (bal_parens ($bal)),
     (blank_seq %blanks),
     (=len ($bal) %blanks),
     (charstr ($chars)).

! blank_seq - sequence of blank characters

   (blank_seq ()).
   (blank_seq (' ' $blanks))< (blank_seq ($blanks)).

! charstr - string (sequence) of characters

   (charstr ()).
   (charstr (%char $chars))< (char %char), (charstr ($chars)).

! char - definition of characters
! example:  'A'  ==  (`char (`0 `1 `0 `0 `0 `0 `0 `1))  (syntactic shorthand)

   (char (`char %8bitseq))<            ! 8-bit characters
     (bit_seq %8bitseq),
     (=len %8bitseq (* * * *  * * * *)).

! bit_seq - sequence of bit atoms

   (bit_seq ()).
   (bit_seq (%bit $bits))< (bit %bit), (bit_seq ($bits)).

! bit - definition of bit atoms

   (bit `0).
   (bit `1).

! not_in - element not in a sequence

   (not_in %x ()).
   (not_in %x (% $))<
     (/= %x %),
     (not_in %x ($)).

! /= - inequality between (some types of) expressions

   (/= `0 `1).                  ! inequality between distinct bit atoms
   (/= %bit ($))< (bit %bit).   ! inequality between bit atom and sequence
   (/= %1 %2)< (/= %2 %1).      ! inequality is commutative
   (/= () (% $)).               ! inequality between sequences
   (/= (%1 $1) (%2 $2))< (/= %1 %2).
   (/= (%1 $1) (%2 $2))< (/= ($1) ($2)).

! =len - sequences of equal length

   (=len () ()).
   (=len (%1 $1) (%2 $2))< (=len ($1) ($2)).