# Gidl

![TravisCI](https://travis-ci.org/GaloisInc/gidl.svg)

Gidl (for Galois Interface Description Language) is a simple IDL for
describing structured types and RPC-style interfaces.

## Overview

[Jump right to an example of gidl.](https://github.com/galoisinc/gidl/tree/master/tests/example.gidl)

### Types

Gidl has a type language which permits the user to define types using
the following primitives:
- Atomic types:
    - Signed integers of 8, 16, 32, 64 bit width
    - Unsigned integers of 8, 16, 32, 64 bit width
    - IEEE 754 single and double precision floating point numbers
    - Boolean values
- User-defined Enum types:
    - Pairs of names and values, where names and values must have
      a one-to-one correspondence
    - User specified representation width (8, 16, 32, or 64 bits)
- User-defined Newtypes:
    - Wraps an existing atomic or enum type with a new type
- User-defined Structures:
    - Set of named fields. Corresponds to a record or a C struct.
    - Fields may be of any other user-defined type

### Interfaces

Gidl interfaces are composed of the following primitives:
- Streams, which are sent from server to client whenever the server wants.
  (We expect to refine this and allow clients to control stream rate.)
- Attributes, which are read and written according to requests by the client.
  Attributes have a user defined read/writable permissions.

Interfaces can be composed by subtyping.
(We expect interface composition may change in the future.)

Protocol drift is detected by identifying each stream and attribute message
on the wire by a hash of its name, its type, and all child types. Therefore

## IDL format

The gidl IDL uses a s-expression based format. The IDL format currently is
documented in `tests/example.gidl`

## Backends

Gidl currently has backends for:
  - Haskell backend: translates types to algebraic datatypes, creates `cereal`
    instances for serialization.
  - Haskell-RPC backend: all of the features of the Haskell backend, and also
    creates an HTTP server that exposes a JSON RPC-style interface for gidl
    interfaces.
  - [Ivory][] backend: translates types to Ivory types, creates `ivory-serialize`
    instances for serialization.
  - [Tower][] backend: all of the features of the Ivory backend, and also
    creates datatypes of tower channels for interface streams and attributes,
    and a tower monitor which implements a server for a given interface.

[Ivory]: http://github.com/GaloisInc/ivory
[Tower]: http://github.com/GaloisInc/tower

## Prerequisites

Gidl requires the GHC 7.8 haskell compiler, and a modern Cabal (>= 1.18).

It also requires the [`s-cargot`][s-cargot] package, which is not yet available
through hackage. In the parent directory, run

```
git clone https://github.com/aisamanra/s-cargot
```

[s-cargot]: https://github.com/aisamanra/s-cargot

In order to build the code generated by the the Ivory and Tower backends, we 
require the [Ivory][], [Tower][], and [ivory-tower-stm32][] repositories. These
should also be found, by default, in the parent directory.

[ivory-tower-stm32]: http://github.com/GaloisInc/ivory-tower-stm32

```
git clone https://github.com/galoisinc/ivory
git clone https://github.com/galoisinc/tower
git clone https://github.com/galoisinc/ivory-tower-stm32
```

## Build and Test

Use the `create-sandbox` target in the Makefile to create a local cabal
sandbox and install all dependencies.

The default target builds the gidl library. You can then use `cabal run gidl --
<OPTIONS>` to run the code generator. Use the `--help` option to get usage
information.

Use the `test` target in the Makefile to generate and test each backend
implementation. The `tests/example.gidl` file is used as the input language.
You may then browse generated code for each implementation, which is generated
and built in subdirectories of the `tests` directory.

## Editor Modes

#### vim
There is a vim-mode available at [`pchickey/vim-gidl`](https://github.com/pchickey/vim-gidl).

If you use the vundle package manager, add the line `Package 'pchickey/vim-gidl'`
to your `.vimrc`, then run `:BundleInstall`.

If you use the Pathogen package manager, clone the `vim-gidl` repo into your
`~/.vim/bundle` directory.

#### emacs
There is an emacs-mode available at [`aisamanra/gidl-mode`](https://github.com/aisamanra/gidl-mode)
and through an elisp archive at [`http://gelpa.gdritter.com`](http://gelpa.gdritter.com).

If an emacs user uses the emacs package manager, they can just add a line to
their `.emacs` and then install it either interactively with `M-x package-list`
or automatically with `(use-package gidl-mode :ensure t)`

## About

Gidl was created at [Galois][] by Pat Hickey, with help from Getty Ritter and
Trevor Elliott, as part of the [SMACCMPilot project][].

Gidl was inspired in part by John Van Enk's excellent [Cauterize][] tools. Look
for gidl to switch to using cauterize as the type language in the future!

Gidl is still experimental - anything may change at any time. Please get in
touch if you're interested in using or working on gidl.

[Galois]: https://galois.com
[SMACCMPilot project]: https://smaccmpilot.org
[Cauterize]: https://github.com/cauterize-tools/cauterize