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:

Context-Free Syntax

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

• All words that are reserved in Haskell 98 are reserved in P-logic.
• The following additional words are reserved within the P-logic syntax:

  All, Exist, Gfp, Lfp,
  !, ., $, -/, /\, \/, ===, ==>, <==>

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