PrhoLog version 1.0 and later. 


SYNTAX 
============================================
Both for Prholog-full and Prholog-Light.
Exceptions for Prholog-Light are indicated.
Prholog with proximity relations follow the
syntax of Prholog-full.
-------------------------------------------

  Clauses, queries, and meta-queries:

      clause ::= rho-clause | Prolog clause
      query ::= literal_1, ..., literal_n, n >= 0

      meta-query ::= ?(query, Prolog_var)
         % meta-queries are used to actually query Prholog programs. 
         % They should be typed in the Prolog command line.
   

  Rho-clauses:

      rho-clause ::= rho-atom | rho-atom :- query.


  Rho-atoms and literals:

      rho-atom ::= 
          strategy :: (sequence_1) ==> (sequence_2)
        | strategy :: (sequence_1) ==> (sequence_2) where constraint

      rho-literal ::=
          rho-atom
        | strategy :: (sequence_1) =\=> (sequence_2)
        | strategy :: (sequence_1) =\=> (sequence_2) where constraint


  Literals:

      literal ::= rho-literal | Prolog literal


  Strategies:

      strategy ::= rho-term


  Strategy definitions:

      strategy_def ::= 
         strategy_1 := strategy_2
         % Remark. Strategy definitions are just shortcuts for the
         % corresponding clauses:
         %    strategy_1 :: seqvar_1 ==> seqvar_2 :- 
         %        strategy_2 :: seqvar_1 ==> seqvar_2.


  Sequences:

      sequence ::= 
           eps 
         | seqvar_or_term_1, ..., seqvar_or_term_n,   n >= 1.

  
  Seqvar_or_term:

      seqvar_or_term ::= seqvar | rho-term


  Rho-terms:

      rho-term ::= 
           indvar 
         | funvar(sequence) 
         | funsymb(sequence) 
         | ctxvar(rho-term)              % NOT IN PRHOLOG-LIGHT

  
  Contexts:                              % NOT IN PRHOLOG-LIGHT

      context ::= 
           hole 
         | funvar(sequence, context, sequence) 
         | funsymb(sequence, context, sequence)
         | ctxvar(context) 

  
  Variables:

      Individual variables
      indvar ::= 
         Prolog constants that start with i_ (i followed by the underscore).
      Anonymous indiviual variables are written as i_.
      Examples: i_1, i_X, i_ThisIsIndVar.

      Sequence variables
      seqvar ::= 
         Prolog constants that start with s_ (s followed by the underscore).
      Anonymous sequence variables are written as s_.
      Examples: s_1, s_S, s_ThisIsSeqVar.

      Function variables
      funvar ::= 
         Prolog constants that start with f_ (f followed by the underscore).
      Anonymous function variables are written as f_.
      Examples: f_1, f_F, f_ThisIsFunVar.

      Context variables                  % NOT IN PRHOLOG-LIGHT
      ctxvar ::=
         Prolog constants that start with c_ (c followed by the underscore).
      Anonymous context variables are written as c_.
      Examples: c_1, c_C, c_ThisIsCtxVar.

  
  Function symbols:

      funsymb ::= Prolog constants


  Constraints:

      constraint ::= [single_constraint_1,...,single_constraint_n],   n>=0

      single_constraint ::= 
           seqvar in seq_regexp 
         | ctxvar in ctx_regexp           % NOT IN PRHOLOG-LIGHT

      seq_regexp ::= 
           rho-term-without-named-variables 
         | eps 
         | sconc(seq_regexp, seq_regexp)  % seq_regexp concatenation
         | sor(seq_regexp, seq_regexp)    % seq_regexp choice
         | sstar(seq_regexp)              % seq_regexp star


      ctx_regexp ::=                      % NOT IN PRHOLOG-LIGHT
           context-without-named-variables   
         | cconc(seq_regexp, ctx_regexp, seq_regexp)  % ctx_regexp concatenation
         | cor(seq_regexp, ctx_regexp, seq_regexp)    % ctx_regexp choice
         | cstar(ctx_regexp)                          % ctx_regexp star

      
      rho-term-without-named-variables ::=
         rho-term that does not contain individual, sequence, function
         and context variables except, maybe, anonymous versions of them.

      context-without-named-variables ::=  % NOT IN PRHOLOG-LIGHT
         context that does not contain individual, sequence, function
         and context variables except, maybe, anonymous versions of them.


For a meta-query
    ?(query, Prolog_variable)
Prholog either fails, or returns an instantiation of Prolog_variable by a
substitution, defined below.


  Substitutions:
      sibstitution ::= [binding_1,...,binding_n], n>=0.

  Bindings:
      binding ::=
          indvar ---> rho-term
        | seqvar ---> (sequence)
        | funvar ---> funsymb
        | ctxvar ---> context

Bindings do not map indvars, seqvars, and funvars to themselves, 
ctxvars to themselves applied to the hole, i.e., there is no binding
of the form c_Var ---> c_Var(hole)
   

Remark about reserved words:

      constants that end with _rholog_internal should not be used 
      in the programs and queries.