# GCL Parser

A simple parser for the GCL language used in the course _Program Verification_. The parser is written using Happy and Haskell. A Cabal build file is included to build the library.

This parser admits a richer language than the base GCL to also accommodate optional assignments. You can ignore the parts of the parser/syntax that you don't need in your parts of assignments.

#### Prerequisites
To compile the tool, the following package are required:
* array
* containers
* optparse-applicative
* pretty.

#### Compilation
To compile the library, run the command `> cabal build` from your console.

#### Running/testing from interpreter

After building (see above), you can run:

```
> cabal repl
```

This will run `ghci` (Haskell interpreter) and also load the module `GCLParser.Parser`. From there you can load other packages using the usual `:l <modulename>` command.

The file `.ghci` in the project root contains ghci options that will also be turned on. Currently it only contains:

```
-XNamedFieldPuns
```


#### Usage

The module `GCLParser.Parser` exports two functions:

```Haskell
parseGCLstring :: String -> ParseResult Program
parseGCLfile :: FilePath -> IO (ParseResult Program)
```
The first is to parse a GCL program from a string, and the second is to parse from a text file. The parser returns a value of type `ParseResult Program`, which is a synonym for `Either String Program`. Such value takes the form of either `Left e` where `e` is an error message if the parsing fails, or `Right p` if the parsing is successful. In the later case, `p` is a value of type `Program` which is a datatype used to structurally repfresent a GCL program. See the module `GCLParser.GCLDatatype` for its definition.

Note that the module `GCLParser.Parser` is generated by Happy. The source code is `src/GCLParser/Parser.y`, which is a Happy parser definition. So, if you need to change the parser, you should not edit `Parser.hs` manually, but instead edit `Parser.y`.

#### Other tools

##### Pretty printing

The module `GCLParser.PrettyPrint` provides a function to pretty print a value of type `Program`:

```Haskell
ppProgram2String :: Program -> String
```

##### interpreter (running a GCL program)

The module `GCLInterpreter` provides a function to execute a GCL program, given a starting state.

```Haskell
execProgram :: Program -> State -> Either (String,State) State
```

Be mindful that this tool is experimental, and is not made for performance. There is also some incompleteness when interpreting the ∀ and ∃ quantifiers. Obviously, we can't actually check such a quantifier over the whole space of integers, so some practical choice was made. See the module in-code documentation.

##### mutation test

The module `MuGCL` provides a function that generate mutants of a GCL Program.
Given a program P, the function below generates a bunch of so-called
mutants. Each is a program P', which is a copy of P, but where it is changed
in one place (e.g. some expression "i<n" is mutated to "i<=n").

```Haskell
mutateProgram :: Program -> [(MutationType,Program)]
```

You can use this mutants to test the completeness of your verification
tool (it should be able to kill all the mutants, but see also my note in
the documentation of `MuGCL`).

#### Supported GCL syntax

See in `/docs`.

#### Error message

Unfortunately almost none. But if some of you know how to make Happy produces a more friendly error message, do let me know.

#### GCL examples and verification benchmark

See in `/examples`

#### Z3

* [A note on how to install Z3 for your Haskell project.](./docs/aboutInstallingZ3.md)
* Some examples of how to use Z3 from Haskell: in `examples/examplesHaskellZ3`.

#### [Papers for your Related Work section](./docs/papers.md)

#### Credits

Many thanks to Stefan Koppier for providing the initial implementation of the parser.

**Contributors:** Stefan Koppier, Wishnu Prasetya