arti.ml: minor style cleanups
small but controversial simplification of Sig
Merge pull request #9 from gasche/cleanups

Cleanups
Update arti.ml

Fix a typo in gasche's patch
Fix bugs divers/simplifications
Added the example of RBT. Do no test yet if the property of being a
RBT is satisfied
Typo
RBT example: reduce key value coverage to improve bytecode speed
RBT example: add a well-formedness check
implem: delete trailing whitespace; we're not kidding
RBT example: factorize the color bit
let properties return a counter-example when it exists

This is useful when debugging our implementation code, or testing that
our correctness properties indeed catch bugs. For example, if you
change the 'blacken' code to be always return its input unchanged,
then in the toplevel:

    # open RBT;;
    # let _ = Ty.counter_example rbt_t RBT.is_balanced;;

will return
    - : RBT.t option =
    Some
     (T (R,
       T (R, Empty, 2, T (R, T (R, Empty, 5, T (R, Empty, 8, Empty)),
                             8, Empty)),
       8, Empty))
RBT example: zippers in place, but no properties yet

    # let (|?>) m f = match m with None -> None | Some v -> f v;;
    # let some f v = Some (f v);;
    # open RBT;;
    # empty |> insert 2 |> insert 1 |> insert 3
      |> some zip_open
      |?> move Left |?> move_up |?> move Right
      |?> some zip_close;;

    - : RBT.t option =
    Some (T (R, T (R, Empty, 1, Empty),
             2, T (R, Empty, 3, Empty)))