Replace bindings by declare blocks

[treiher]

Context and Problem Statement

In #701 the introduction of declare blocks is proposed. Declare blocks provide a similar functionality as the already existing bindings. It could be beneficial to replace bindings by declare blocks.

Example

Without binding or declare block

      state X is
         [...]
         Hash : Opaque;
         Query : P::Query
      begin
         [...]
         Hash := Hash = Get_Hash (Transcript_Hash).Data;
         Query = P::Query'(Tag => P::Hash, Length => Hash'Size, Data => Hash);
         Channel'Write (P::Message'(Tag => P::Request, Length => Query'Size, Payload => Query));

With binding

      state X is
         [...]
      begin
         [...]
         Channel'Write (P::Message'(Tag => P::Request, Length => Query'Size, Payload => Query)
                           where Query = P::Query'(Tag => P::Hash, Length => Hash'Size, Data => Hash)
                              where Hash = Get_Hash (Transcript_Hash).Data);

With declare block

      state X is
         [...]
      begin
         [...]
         declare
            Hash : Opaque = Get_Hash (Transcript_Hash).Data;
            Query : P::Query := P::Query'(Tag => P::Hash, Length => Hash'Size, Data => Hash);
         begin
            Channel'Write (P::Message'(Tag => P::Request, Length => Query'Size, Payload => Query));
         end;

Considered Options

O1 Replace bindings by declare blocks

+ Keep DSL smaller by preventing two ways to do essentially the same thing + Declare blocks are probably easier readable than bindings as type of variable is stated explicitly + Less implementation and maintenance effort (validation and code generation easier to implement for declare blocks than bindings as no type inference is needed)

O2 Keep bindings as well as declare blocks

+ Bindings are easier to write (as bindings are less verbose than declare blocks)

Decision Outcome

O1