% Parsing first-order formulae
% no use of deterministic
% instead of hypothetical judgements use 
% explicit lists.
%{

Identifiers id
  start with a letter A-Z or a-z
  followed by letters A-Z or a-z or digits 0-9

Terms
  t ::= id        % constant or variable
      | id(id)    % function with arguments

Atomic Propositions

  P ::= id          % propositional constant
      | id(t)       % predicate with arguments

Propositions
  A ::= atom P
      | ~ A              % negation
      | A & A            % conjunction
      | A v A            % disjunction
      | A => A           % implication
      | T                % truth
      | F                % falsehood
      | forall id A      % universal quantification
      | exist id A       % existential quantification
      | (A)              % parentheses to override precedence
  Operator Precedence  ~ > & > v > =>
  & v are left associative
  => is right associative
  forall, exist are prefix operators weaker than =>
  forall and exist bind x, shadowing previous bindings


}%

id  : type.  %name id I.
ids : type.  % sequence
prop: type.  %name prop P.

% identifiers (just define some)
% identifiers for bound vars or propositions
x: id.
y: id.
z: id.
u: id.
v: id.

% identifiers for predicates
p: id -> id.
q: id -> id.
r: id -> id.
s: id -> id.

% propositions together with precedence

atom   : id -> prop.
~      : prop -> prop.                          %prefix 50 ~.
&      : prop -> prop -> prop.                  %infix left 40 &.
v      : prop -> prop -> prop.                  %infix left 30 v.
=>     : prop -> prop -> prop.                  %infix right 20 =>.
forall : (id -> prop) -> prop.                  %prefix 10 forall.
exist  : (id -> prop) -> prop.                  %prefix 10 exist.
true   : prop.
false  : prop.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Define token stream
%

tok:type.  %name tok T.

% tokens reserved for predicates
'p': tok.
'q': tok.
'r': tok.
's': tok.

% tokens reserved for variables or atomic propositions
'x': tok.
'y': tok.
'z': tok.

% tokens for formulas including brackets

'forall' : tok.
'exist'  : tok.
'and'    : tok.
'or'     : tok.
'imp'    : tok.
'not'    : tok.
'openB'  : tok.
'closeB' : tok.
'true'   : tok.
'false'  : tok.

% list of tokens
tokens : type. %name tokens S.
nil: tokens.
; : tok -> tokens -> tokens.  %infix right 10 ;.

% conversions of tokens to identifiers
idconv: tok -> id -> type.
predconv: tok -> (id -> id) -> type.

% explicit context for bvars 
% to only retrieve the first instance 
ctx: type.   
hyp: type.   
bvar: tok -> id -> hyp.
# : hyp -> ctx -> ctx.   %infix right 10 #.
e : ctx.

%  
neq: tok -> tok -> type.
%tabled neq.

nxy: neq 'x' 'y'.
nxz: neq 'x' 'z'.
nyz: neq 'y' 'z'.


nsym: neq T T'
       <- neq T' T.

% returns the first occurrence of (bvar T I) 
% in the context, i.e. later shadows earlier occurrences
% of bound variables
lookup: tok -> ctx -> id -> type.

ls: lookup T ((bvar T I) # C) I.

lf: lookup T ((bvar T' I') # C) I
     <- neq T T'
     <- lookup T C I.


ip : predconv 'p' p.
iq : predconv 'q' q.
ir : predconv 'r' r.
is : predconv 's' s.
ix : idconv 'x' x.
iy : idconv 'y' y.
iz : idconv 'z' z.

parse : tokens -> prop -> type.
fq: ctx -> tokens -> tokens -> prop -> type.
fi: ctx -> tokens -> tokens -> prop -> type.
fa: ctx -> tokens -> tokens -> prop -> type.
fo: ctx -> tokens -> tokens -> prop -> type.
fn: ctx -> tokens -> tokens -> prop -> type.
fatom: ctx -> tokens -> tokens -> prop -> type.


% tabled fi.
%tabled fa.
%tabled fo.

% top-level parsing of tokens F to formula P
pform: parse F P
	<- fq e F nil P.

fall: fq C ('forall' ; I ; F) F' (forall P)
       <- ({x:id} fq ((bvar I x) # C) F F' (P x)).

fex: fq C ('exist' ; I ; F) F' (exist P)
       <- ({x:id} fq ((bvar I x) # C) F F' (P x)).

cq : fq C F F' P <- fi C F F' P.

% implication -- right associative
fimp: fi C F F' (P1 => P2)
       <- fo C F ('imp' ; F1) P1
       <- fi C F1 F' P2.

ci : fi C F F' P <- fo C F F' P.

% disjunction -- left associative
for : fo C F F' (P1 v P2)
	 <- fo C F ('or' ; F1) P1
	 <- fa C F1 F' P2.

co  : fo C F F' P <- fa C F F' P.

% conjunction -- left associative
fand : fa C F F' (P1 & P2)
	 <- fa C F ('and' ; F1) P1
	 <- fn C F1 F' P2.

ca  : fa C F F' P <- fn C F F' P.

% negation
fneg: fn C ('not' ; F) F' (~ P) <- fatom C F F' P.

cn : fn C F F' P <- fatom C F F' P.

% atom
fat : fatom C (X ; F) F (atom X') <- idconv X X'.

brack : fatom C ('openB' ; F) F' P
	    <- fq C F ('closeB' ; F') P.

fprop: fatom C (X ; BV ; F) F  (atom (P V))
	<- predconv X P
	<- lookup BV C V.

ftrue : fatom C ('true' ; F) F true.
ffalse : fatom C ('false' ; F) F false.