! enc_inst.eax - extended axioms to map encoded expr to real expr instance
! Encoded expressions are ground expressions that use symbols #.. and &.. to
! represent expression and string variables.  Symbols beginning with one or
! more _ followed by # or & are mapped to symbols with one of the _ removed.

! predicate format:

  (enc_inst <enc_ex> <real_inst> [<var_asnmts>])
 
  ! <enc_ex> -- ground expr with #.. and &.. symbols for expr & str vars
  !     -- _{_}#.., _{_}&.. symbols mapped to symbol with one less _
  ! <real_inst> -- expr with arbitrary exprs/strs substituted for encoded vars
  !                (same expr/string substituted for same encoded var)
  ! <var_asnmts> -- optional list matching encoded vars to exprs/strings
  ! Note that all ground expressions occur as <enc_ex> arguments!

! enc_inst - get real instance of an encoded expression

  (enc_inst %enc %inst)< (enc_inst %enc %inst %asnmts).
    ! -- var assignments only needed to match encoded symbols to real exprs

  (enc_inst %atom %atom %asnmts)< (atom %atom).   ! atom maps to itself

  ! -- At this point in our recursive definition, the encoded expression
  !    is known to not be a sub-expression of an encoded symbol.

  (enc_inst (` ('_' $enc_#sym)) (` ($enc_#sym)) %asnmts)<
    (enc_#sym (` ($enc_#sym)).    ! encoded {_}#.. symbol 
      ! -- leading _ gets removed from _{_}#.. symbol

  (enc_inst (` ('#' $chars) %val %asnmts)<      ! encoded expr var: #..
    (*set char ($chars)),       ! arbitrary chars allowed in symbol after #
         ! ... but probably should exclude ' ', ')', and some special chars
    (key_value %asnmts (` ('#' $chars)) %val).   ! var value is arbitrary expr

  (enc_inst %enc_seq %asnmts)<      ! sequence of encoded elements
    (enc_#sym %enc_seq))~,          ! sequence not an encoded #-symbol {_}#..
         ! -- May, however, be a &-symbol, but at this "expression" level,
         !    such a symbol is treated as data, not as encoded.
    (enc_inst_seq %enc_seq %seq %asnmts),   ! get inst of encoded seq

! enc_inst_seq - get real instance of an encoded sequence

  (enc_inst_seq () () %asnmts).         ! empty sequence

  (enc_inst_seq (%elem $elems) ($elem_inst $elems_inst) %asnmts)<
    (enc_inst_elem %elem ($elem_inst) %asnmts),
    (enc_inst_seq ($elems) ($elems_inst) %asnmts).

! enc_inst_elem - get real instance string of an encoded element within a seq
! (Element is an encoded string variable &.. or an encoded expression (as
! defined above) or an encoded symbol _{_}&.. (also an encoded expression),
! which maps to a symbol with one less leading _.

  (enc_inst_elem (` ('_' $enc_&sym)) ((` ($enc_&sym))) %asnmts)<
    (enc_&sym (` ($enc_&sym))).     ! {_}&.. symbol
      ! -- one of the leading _ gets removed from _{_}&.. symbol

  (enc_inst_elem (` ('&' $chars) ($val) %asnmts)<   ! encoded str var: &..
    (key_value %asnmts (` ('&' $chars)) ($val)).   ! var value is arb string

  (enc_inst_elem %expr (%inst) %asnmts)<
    (enc_&sym %expr)~,                ! expression is not a {_}&.. symbol
    (enc_inst %expr %inst %asnmts).   ! get instance of this encoded expr

! enc_#sym - encoded symbol {_}#..

  (enc_#sym (` ($_ '#' $chars)))<      ! {_}#.. symbol
    (* '_' ($_)),              ! zero or more underscores
    (*set char ($chars)).        ! string of characters

    ! The predicate (char <char>) is defined elsewhere.

! enc_&sym - encoded symbol {_}&..

  (enc_&sym (` ($_ '&' $chars)))<      ! {_}&.. symbol
    (* '_' ($_)),
    (*set char ($chars)).

! * - sequence of zero or more of an expression

  (* % ()).
  (* % (% $))< (* % ($)).

! *set - sequence of zero or more of elements from a set

  (*set %set ())< (%set %).
  (*set %set (% $))< (%set %), (*set %set ($)).

! key_value - utility to get value from sequence of key-value pairs
! (key_value <kvpairs> <key> <value>)

  (key_value ($kvpairs1 (%key %value) $kvpairs2) %key %value)<
    (key_value_missing ($kvpairs1 $kvpairs2) %key).
        ! -- key can only occur once

  (key_value_missing () %key).
  (key_value_missing ((%keyx %value) $kvpairs) %key)<
    (== %keyx %key)~,           ! use ~ here to allow for arbitrary atoms
    (key_value_missing ($kvpairs) %key).