$Id: CoreVerifParser.lhs,v 1.1 1998/03/19 07:18:13 leavens Exp $

AUTHOR: Gary T. Leavens

This Haskell module defines the lexical and context free grammar,
and a parser for annotation style proofs for the Hoare Logic
of Dave Schmidt's "Core Language"; see chapter 1 of
"The Structure of Typed Programming Languages" (MIT Press, 1994).

> module CoreVerifParser where
> import ParserFunctions
> import LexerTools
> import CoreLangParser


               MICROSYNTAX (LEXICAL SCANNER)

The microsyntax for the core language is defined by the following
definitions, which use the function "scanning" from the LexerTools module.

> verifScanner :: [Char] -> [Token]
> verifScanner = scanning keywords' symbols' []
> keywords' = keywords
> symbols' = symbols ++ ["{", "}"]


             ADDITIONAL ABSTRACT SYNTAX

The abstract syntax of the verification logic's proof trees is as follows.
A HoareTree is either a rule or an axiom; it may have 0 or more hypotheses.
Each of these contains applications of the consequence rule implicitly;
as the lists of expressions, [e1,e2,...,en] are interpreted as
implicit applications of the consequence rule; that is we interpret
such a list as e1 ==> e2 ==> e3 ... ==> en.
The first list of expressions contains the precondition of the command,
the second contains its the postcondition.

> type H = HoareTree
> data HoareTree = Rule [E] C [E] [H]

A PreHoareTree is a HoareTree without the conclusions

> data PreHoareTree = PreRule C [H]


                   CONCRETE SYNTAX

The concrete syntax and parser for annotation-style proof turns them
into proof trees.
It uses the parser combinators found in the ParserFunctions module.

> annotated_command :: Parser Token HoareTree
> annotated_command =
>               (some_sep_by (p_check ";") annotated_stmt)  `using` groupRight
>  where annotated_stmt =
>               ((predicates $~ stmt) $~ predicates)
>                                `using` (\((ps,PreRule c hs),qs)
>                                                     -> Rule ps c qs hs)
>        stmt :: Parser Token PreHoareTree
>        stmt = (location $~ (p_check ":=" /$~ expr))
>                                `using` (\(l,e) -> PreRule (l `Assign` e) [])
>            $| p_check "skip"   `p_return` (PreRule Skip [])
>            $| ((p_check "while" /$~ expr) $~
>                (p_check "do" /$~ annotated_command) $~/
>                p_check "od")   `using` (\(e, r@(Rule _ c _ _))
>                                                  -> PreRule (While e c) [r])
>            $| ((p_check "if" /$~ expr $~
>                (p_check "then" /$~ annotated_command)) $~
>                (p_check "else" /$~ annotated_command) $~/
>                 p_check "fi")  `using` (\((e, r1@(Rule _ c1 _ _)),
>                                           r2@(Rule _ c2 _ _))
>                                         -> PreRule (If e c1 c2) [r1, r2])
>            $| (p_check "(" /$~ annotated_command $~/ p_check ")")
>                                `using` (\r@(Rule _ c _ _) -> PreRule c [r])

> predicates :: Parser Token [Expression]
> predicates = (some predicate)

> predicate :: Parser Token Expression
> predicate = (p_check "{") /$~ expr $~/ (p_check "}")


The following is used in parsing semicolons.  In essence, it implements
the semicolon rule of the Hoare logic.

> groupRight :: [HoareTree] -> HoareTree
> groupRight [r] = r
> groupRight (Rule ps1 c1 qs1 hs1 : hts) =
>            let remaining@(Rule prest crest qrest hsrest) = groupRight hts
>                c = c1 `Semi` crest
>            in Rule [head ps1] c [last qrest]
>                    [Rule ps1 c1 qs1 hs1, remaining]


             READER (READ INSTANCE)

The read function is an overloaded function that can be used to read in
commands, expressions, or locations from a String.
This allows you to type at the command prompt things like:
     (read "skip" :: Command)
and have an abstract syntax tree for the command returned.

> instance Read HoareTree where
>    readsPrec n input = first_parse_by annotated_command input