P-logic syntax, as implemented by PFE

Extracted from parse2/Parser/PropParser.y on 2004-09-01.

Notational Conventions

As in the Haskell 98 syntax reference:

NotationMeaning
[pattern] optional
{pattern} zero or more repetitions
(pattern) grouping
pat1|pat2 choice
assert terminal syntax

Context-Free Syntax

P-logic is added to Haskell 98 by extending the declaration syntax with property assertions and predicate definitions, as defined by the nonterminals assertion and property below, respectively.
assertion : assert [conid =] prop

property  : property conid {var|con} = formula

prop    : pqcon {predarg}
        | (All | Exist) var [:: ctype] . prop
        | -/ prop
        | prop propop prop
        | pexp === pexp
        | pexp ::: formula
        | ( prop )

propop : /\ | \/ | ==> | <==>

pexp    : { exp }
        | qvar
        | pqcon
	| literal		

formula : aformula
        | formula -> formula
        | formula qconop formula
        | -/ formula		
        | formula propop formula		
        | Lfp conid . formula
        | Gfp conid . formula
        | pqcon {predarg}

predarg : { exp }
        | qvar
	| literal		
        | aformula

aformula
        : pqcon
        | [ ]
	| ! aexp1
        | $ aformula
        | ( formulas )
        | {| typedpats | prop |}

typedpats : typedpat { , typedpat }

typedpat : pat [:: ctype]

formulas : formula { , formula }

pqconid	: CONID | QCONID | tupcon

pqcon   : pqconid
	| ( gconsym )

Reserverd keywords

In Haskell
Two new keywords are reserved: assert and property. Apart from this, all valid Haskell 98 syntax remains valid in the extended language.
In P-logic

Comments

There is a special comment syntax that can be used to mark assertions and other code that should be considered by the Programatica tools, but ignored by Haskell compilers:

{-P:
...
-)

This syntax is seen as a comment by regular Haskell tools, but treated as if the {-P: and -} characters were spaces by the Programatica tools.

Precedences

Precedences, from lowest to highest
AssociativityOperator
rightGfp, Lfp, All, Exist
right->, qconop
left<==>
right==>
left/\, \/, -/, ===
left:::