Adding new bitvector literals and enum/struct Notations for constr

[maxkurze1]

I've been wasting some time creating / adapting some Koika notations to make the language a bit more usable.

(Examples shown here can be found and executed in Parsing.v)

Features

New bitvector literals

The default bitvector literals (|size 'd deciaml| and Ob~1~0~...) seemed a bit inconsistent and tedious to me. Additionally, they did not support hex and the first one is only accessible from within Koika.

The new proposed literals are usable from Koika as well as from normal Coq. They support 4 bases hex, decimal, octal and binary.

Their syntax looks like this | prefix? "literal" postfix? size? |.
Either the prefix or the postfix must be present to declare which base is used.

Prefixes := 0b 0o 0d 0x
Postfixes := :b :o :d :h

The size is also optional. If it is inferred, it will be derived from the length of the literal for binary, octal and hex, as for these bases the length directly corresponds with the bit vector length. For decimal, however, the bit vector length is the minimum necessary to encode the given value.

Examples:

Definition num_test_b_1 : [| |"01101":b|       =koika= Ob~0~1~1~0~1 |] := eq_refl.
Definition num_test_b_2 : [| |0b"00011"|       =koika= Ob~0~0~0~1~1 |] := eq_refl.
Definition num_test_b_3 : [| |"11":b5|         =koika= Ob~0~0~0~1~1 |] := eq_refl.
Definition num_test_b_4 : [| |0b"10"5|         =koika= Ob~0~0~0~1~0 |] := eq_refl.
Definition num_test_b_5 : [| |0b"10010110"3|   =koika= Ob~1~1~0     |] := eq_refl.
Fail Definition num_test_b_6  := {{ |0b"102"|  }} : ua.
Fail Definition num_test_b_7  := {{ |0b"10f"6| }} : ua.
Fail Definition num_test_b_8  := {{ |"f0":b5|  }} : ua.
Fail Definition num_test_b_9  := {{ |"f0":b|   }} : ua.
Fail Definition num_test_b_10 := {{ |"":b|     }} : ua.

Definition num_test_o_1 : [| |"330":o|   =koika= Ob~0~1~1~0~1~1~0~0~0     |] := eq_refl.
Definition num_test_o_2 : [| |"070":o9|  =koika= Ob~0~0~0~1~1~1~0~0~0     |] := eq_refl.
Definition num_test_o_3 : [| |0o"000"|   =koika= Ob~0~0~0~0~0~0~0~0~0     |] := eq_refl.
Definition num_test_o_4 : [| |0o"750"11| =koika= Ob~0~0~1~1~1~1~0~1~0~0~0 |] := eq_refl.
Definition num_test_o_5 : [| |0o"751"3|  =koika= Ob~0~0~1                 |] := eq_refl.
Fail Definition num_test_o_6  := {{ |0o"108"|   }} : ua.
Fail Definition num_test_o_7  := {{ |0o"080"10| }} : ua.
Fail Definition num_test_o_8  := {{ |"f00":o10| }} : ua.
Fail Definition num_test_o_9  := {{ |"00f":o5|  }} : ua.
Fail Definition num_test_o_10 := {{ |"":o|      }} : ua.

Definition num_test_d_1 : [| |"33":d|    =koika= Ob~1~0~0~0~0~1           |] := eq_refl.
Definition num_test_d_2 : [| |"33":d9|   =koika= Ob~0~0~0~1~0~0~0~0~1     |] := eq_refl.
Definition num_test_d_3 : [| |"070":d9|  =koika= Ob~0~0~1~0~0~0~1~1~0     |] := eq_refl.
Definition num_test_d_4 : [| |0d"070"|   =koika= Ob~1~0~0~0~1~1~0         |] := eq_refl.
Definition num_test_d_5 : [| |0d"198"11| =koika= Ob~0~0~0~1~1~0~0~0~1~1~0 |] := eq_refl.
Definition num_test_d_6 : [| |0d"15"3|   =koika= Ob~1~1~1                 |] := eq_refl.
Fail Definition num_test_d_7  := {{ |0d"1a0"|   }} : ua.
Fail Definition num_test_d_8  := {{ |0d"0z0"10| }} : ua.
Fail Definition num_test_d_9  := {{ |"f00":d10| }} : ua.
Fail Definition num_test_d_10 := {{ |"00f":d5|  }} : ua.
Fail Definition num_test_d_11 := {{ |"":d|      }} : ua.

Definition num_test_h_1 : [| |"fa":h|    =koika= Ob~1~1~1~1~1~0~1~0         |] := eq_refl.
Definition num_test_h_2 : [| |"bb":h9|   =koika= Ob~0~1~0~1~1~1~0~1~1       |] := eq_refl.
Definition num_test_h_3 : [| |"014":h|   =koika= Ob~0~0~0~0~0~0~0~1~0~1~0~0 |] := eq_refl.
Definition num_test_h_4 : [| |0x"070"|   =koika= Ob~0~0~0~0~0~1~1~1~0~0~0~0 |] := eq_refl.
Definition num_test_h_5 : [| |0x"198"11| =koika= Ob~0~0~1~1~0~0~1~1~0~0~0   |] := eq_refl.
Definition num_test_h_6 : [| |0x"1d"3|   =koika= Ob~1~0~1                   |] := eq_refl.
Fail Definition num_test_h_7  := {{ |0x"1h0"|   }} : ua.
Fail Definition num_test_h_8  := {{ |0x"0z0"10| }} : ua.
Fail Definition num_test_h_9  := {{ |"g00":h10| }} : ua.
Fail Definition num_test_h_10 := {{ |"00k":h5|  }} : ua.
Fail Definition num_test_h_11 := {{ |"":h|      }} : ua.

Definition num_test_constr_1 := |"0110":b|     : bits _.
Definition num_test_constr_2 := |0b"0110"|     : bits _.
Definition num_test_constr_3 := |"c0ffee":h|   : bits _.
Definition num_test_constr_4 := |0x"deadbeef"| : bits _.

Enum literals in Coq

To access enum values by their name, I am proposing a new notation for Coq (enum e_name < FIELD >). Unfortunately, I wasn't able to exactly match the enum notation which already exists inside Koika, which is using curly braces instead of angle brackets.

Definition numbers_e := {|
  enum_name        := "some_enum_name";
  enum_members     :=                          [ "ONE"; "TWO"; "THREE"; "IDK" ];
  enum_bitpatterns := vect_map (Bits.of_nat 3) [ 1    ; 2    ; 3      ; 7     ]
|}%vect.

(* Accessing enum constants *)
Definition enum_test_1 := enum numbers_e < ONE >.
Definition enum_test_2 := enum numbers_e < TWO >.
Definition enum_test_3 :  enum numbers_e < ONE >   = |"001":b| := eq_refl.
Definition enum_test_4 :  enum numbers_e < TWO >   = |"010":b| := eq_refl.
Definition enum_test_5 :  enum numbers_e < THREE > = |"011":b| := eq_refl.
Definition enum_test_6 :  enum numbers_e < IDK >   = |"111":b| := eq_refl.

Struct literals in Coq

Just like Koikas enums, structs did not have a syntax to construct them in Coq. They had to be built like this: (Bits.of_N 3 1, (Bits.of_N 5 2, (... , tt))). Which made it hard to mentally associate the field's position with its purpose.

The new syntax looks similar to the Koika syntax, again with the adaption of using angle brackets.

Example:

Definition numbers_s := {|
  struct_name:= "some_s";
  struct_fields :=
  [ ("one"  , bits_t 3);
    ("two"  , bits_t 3);
    ("three", bits_t 3);
    ("four" , bits_t 3);
    ("five" , enum_t numbers_e) ]
|}.
Definition struct_test_1 := struct numbers_s < >.
Definition struct_test_2 :  struct numbers_s < > = value_of_bits Bits.zero := eq_refl.
Definition struct_test_3 := struct numbers_s < one := |"010":b| >.
Definition struct_test_4 :  struct numbers_s < one := |"010":b| ; two := |"111":b| > = (Ob~0~1~0, (Ob~1~1~1, (Ob~0~0~0, (Ob~0~0~0, (Ob~0~0~0, tt))))) := eq_refl.
Definition struct_test_5 :  struct numbers_s < five := enum numbers_e < IDK > >      = (Ob~0~0~0, (Ob~0~0~0, (Ob~0~0~0, (Ob~0~0~0, (Ob~1~1~1, tt))))) := eq_refl.
Fail Definition struct_test_6 := (struct numbers_s < five := enum numbers_e < WRONG > >).
Fail Definition struct_test_7 := (struct numbers_s < one := Bits.of_N 9 3 >).
Fail Definition struct_test_8 := (struct numbers_s < wrong := Bits.of_N 3 3 >).

Adapting match

The old match syntax didn't accept sequences on the branches, they always had to be wrapped in parentheses. I don't see the need for keeping the branch level lower than the level of sequences. Consequently, I lifted the level to declutter the syntax a bit.

As the branch is completely enclosed within the arrow (=>) and the bar (|) of the next guard, there should be no problem.

So the following match could now be written without parentheses.

match ... with
| guard1.. => 
  (
  pass;
  pass
  )
| guard2.. =>
  ...
return default: pass
end.

A new if

The default if always expects an else-branch (which is often left empty with else pass). Therefore, I see the need for an if statement that can be used without else. For the time being, I added one called if' .. then .., but it doesn't fit very nice with the syntax.

Future ideas for if

In the future, I would really like to have some kind of if in combination with an early return to write code with less nesting. Currently, with the if-statement that always needs the if- and the else-branch, code has to be nested very deep in certain situation.