Add the [rc::let] annotation.

ANNOTATIONS.md

@@ -33,6 +33,7 @@ attached to.
 | `constraints`  | One or more | Structures, Loops     | `<constr>`                                 |
 | `ensures`      | One or more | Functions             | `<constr>`                                 |
 | `exists`       | One or more | Functions, Loops      | `<ident> ":" <coq_expr>`                   |
+| `let`          | One or more | Structures            | `<ident> {":" <coq_expr>`} "=" <coq_expr>  |
 | `field`        | Exactly one | Structure members     | `<type_expr>`                              |
 | `global`       | Exactly one | Global variables      | `<type_expr>`                              |
 | `immovable`    | None        | Structures            | N/A                                        |
@@ -190,6 +191,17 @@ a function, this variable can only appear in post-conditions and on the return
 type of the function (see `rc::ensures` and `rc::returns`). On the other hand,
 when used on a loop, the variable is bound in the whole invariant.
 
+## `rc::let`
+
+This annotation may appear on structures and should have at least one argument
+of the following form.
+```
+<ident (as variable name)> {":" <coq_expr (as Coq type)>} "=" <coq_expr>
+```
+It corresponds to a Coq let-binding with an optional type annotation. All such
+bindings are inserted in the type definition under the existentials (specified
+with `rc::exists`).
+
 ## `rc::field`
 
 This annotation only appears on structure members, and it requires exactly one

frontend/coq_pp.ml

@@ -672,6 +672,14 @@ let rec pp_struct_def_np structs guard annot fields ff id =
         in
         List.iter pp_exist annot.st_exists;
       end;
+    (* Printing the let-bindings. *)
+    let pp_let (id, ty, def) =
+      let pp_coq = pp_simple_coq_expr false in
+      match ty with
+      | None    -> pp "let %s := %a in@;" id pp_coq def;
+      | Some ty -> pp "let %s : %a := %a in@;" id pp_coq ty pp_coq def;
+    in
+    List.iter pp_let annot.st_lets;
     (* Opening the "constrained". *)
     pp "@[<v 2>"; (* Open box for struct fields. *)
     if annot.st_constrs <> [] then pp "constrained (";

frontend/rc_annot.ml

@@ -248,6 +248,9 @@ let parser annot_exist : (ident * coq_expr) Earley.grammar =
 let parser annot_constr : constr Earley.grammar =
   | c:constr
 
+let parser annot_let : (ident * coq_expr option * coq_expr) Earley.grammar =
+  | id:ident ty:{":" coq_expr}? "=" def:coq_expr
+
 (** {4 Annotations on tagged unions} *)
 
 type tag_spec = string * (string * coq_expr) list
@@ -322,6 +325,7 @@ type annot =
   | Annot_ptr_type     of (ident * type_expr)
   | Annot_size         of coq_expr
   | Annot_exist        of (ident * coq_expr) list
+  | Annot_lets         of (ident * coq_expr option * coq_expr) list
   | Annot_constraint   of constr list
   | Annot_immovable
   | Annot_tagged_union of coq_expr
@@ -411,6 +415,7 @@ let parse_attr : rc_attr -> annot = fun attr ->
   | "ptr_type"     -> single_arg annot_ptr_type (fun e -> Annot_ptr_type(e))
   | "size"         -> single_arg annot_size (fun e -> Annot_size(e))
   | "exists"       -> many_args annot_exist (fun l -> Annot_exist(l))
+  | "let"          -> many_args annot_let (fun l -> Annot_lets(l))
   | "constraints"  -> many_args annot_constr (fun l -> Annot_constraint(l))
   | "immovable"    -> no_args Annot_immovable
   | "tagged_union" -> single_arg tagged_union (fun e -> Annot_tagged_union(e))
@@ -557,6 +562,7 @@ type basic_struct_annot =
   { st_parameters : (ident * coq_expr) list
   ; st_refined_by : (ident * coq_expr) list
   ; st_exists     : (ident * coq_expr) list
+  ; st_lets       : (ident * coq_expr option * coq_expr) list
   ; st_constrs    : constr list
   ; st_size       : coq_expr option
   ; st_ptr_type   : (ident * type_expr) option
@@ -566,6 +572,7 @@ let default_basic_struct_annot : basic_struct_annot =
   { st_parameters = []
   ; st_refined_by = []
   ; st_exists     = []
+  ; st_lets       = []
   ; st_constrs    = []
   ; st_size       = None
   ; st_ptr_type   = None
@@ -580,6 +587,7 @@ let struct_annot : rc_attr list -> struct_annot = fun attrs ->
   let parameters = ref [] in
   let refined_by = ref [] in
   let exists = ref [] in
+  let lets = ref [] in
   let constrs = ref [] in
   let size = ref None in
   let ptr = ref None in
@@ -602,6 +610,7 @@ let struct_annot : rc_attr list -> struct_annot = fun attrs ->
     | (Annot_parameters(l)  , None   ) -> parameters := !parameters @ l
     | (Annot_refined_by(l)  , None   ) -> refined_by := !refined_by @ l
     | (Annot_exist(l)       , None   ) -> exists := !exists @ l
+    | (Annot_lets(l)        , None   ) -> lets := !lets @ l
     | (Annot_constraint(l)  , None   ) -> constrs := !constrs @ l
     | (Annot_size(s)        , None   ) -> check_and_set size s
     | (Annot_ptr_type(e)    , None   ) -> check_and_set ptr e
@@ -628,6 +637,7 @@ let struct_annot : rc_attr list -> struct_annot = fun attrs ->
     { st_parameters = !parameters
     ; st_refined_by = !refined_by
     ; st_exists     = !exists
+    ; st_lets       = !lets
     ; st_constrs    = !constrs
     ; st_size       = !size
     ; st_ptr_type   = !ptr