Renamed annots into contracts. Preparing for syntax extension

TODO.org

@@ -133,17 +133,16 @@ But also some not-so-nice features (ploc's remarks):
 
 ** Development
 *** Done
+- (ploc) retirer le parser Kind2 et revenir à celui de lustrec
 *** To be done
 **** Court terme
-
+- (CG) etendre la syntaxe pour coller à la definition donnée ci-dessus
+  - lexeur/parseur lustreSpec + document latex de grammaire
 - repartir la branche acsl2018 qui contient la normalisation des eexpr
   - le refaire compiler
   - merger avec unstable 
 - transformer cette normalisation pour partager les definitions locales de
   variables dans le noeud de spec, aka contract
-- retirer le parser Kind21 et revenir à celui de lustrec
-- (CG) etendre la syntaxe pour coller à la definition donnée ci-dessus
-  - lexeur/parseur lustreSpec + document latex de grammaire
 
 **** Apres
 - developper dans les backends

src/corelang.ml

@@ -165,7 +165,7 @@ let consts_of_enum_type top_decl =
 (*   Eexpr functions *)
 (************************************************************)
 
-let merge_node_annot ann1 ann2 =
+let merge_contracts ann1 ann2 =
   { requires = ann1.requires @ ann2.requires;
     ensures = ann1.ensures @ ann2.ensures;
     behaviors = ann1.behaviors @ ann2.behaviors;

src/corelang.mli

@@ -156,7 +156,7 @@ val copy_prog: top_decl list -> top_decl list
 
 (** Annotation expression related functions *)
 val mkeexpr: Location.t ->  expr -> eexpr
-val merge_node_annot: node_annot -> node_annot -> node_annot 
+val merge_contracts:  contract_desc -> contract_desc -> contract_desc 
 val extend_eexpr: (quantifier_type * var_decl list) list -> eexpr -> eexpr
 val update_expr_annot: ident -> expr -> expr_annot -> expr
 (* val mkpredef_call: Location.t -> ident -> eexpr list -> eexpr*)

src/lustre_types.ml

@@ -124,7 +124,14 @@ and expr_annot =
  {annots: (string list * eexpr) list;
   annot_loc: Location.t}
 
-type node_annot = {
+type contract_desc = {
+(* TODO: 
+   local variables 
+   rename: assume/guarantee
+           in behavior mode (id, requires/ensures)
+   import contract
+*)
+  
   requires: eexpr list;
   ensures: eexpr list;
   behaviors: (string * eexpr list * eexpr list * Location.t) list;
@@ -173,7 +180,7 @@ type node_desc =
      node_stmts: statement list;
      mutable node_dec_stateless: bool;
      mutable node_stateless: bool option;
-     node_spec: node_annot option;
+     node_spec: contract_desc option;
      node_annot: expr_annot list;
     }
 
@@ -184,7 +191,7 @@ type imported_node_desc =
      nodei_inputs: var_decl list;
      nodei_outputs: var_decl list;
      nodei_stateless: bool;
-     nodei_spec: node_annot option;
+     nodei_spec: contract_desc option;
      (* nodei_annot: expr_annot list; *)
      nodei_prototype: string option;
      nodei_in_lib: string list;
@@ -204,7 +211,8 @@ type top_decl_desc =
 | Open of bool * string (* the boolean set to true denotes a local
 			   lusi vs a lusi installed at system level *)
 | TypeDef of typedef_desc
-
+| Contract of contract_desc
+    
 type top_decl =
     {top_decl_desc: top_decl_desc;      (* description of the symbol *)
      top_decl_owner: Location.filename; (* the module where it is defined *)

src/machine_code_types.ml

@@ -51,6 +51,6 @@ type machine_t = {
   mstatic: var_decl list; (* static inputs only *)
   mconst: instr_t list; (* assignments of node constant locals *)
   mstep: step_t;
-  mspec: node_annot option;
+  mspec: contract_desc option;
   mannot: expr_annot list;
 }

src/parser_lustre.mly

@@ -56,13 +56,13 @@ let rec fby expr n init =
 %token <Num.num * int * string> REAL
 
 %token <string> STRING
-%token AUTOMATON STATE UNTIL UNLESS RESTART RESUME LAST
+%token AUTOMATON STATE UNTIL UNLESS RESTART RESUME 
 %token ASSERT OPEN QUOTE FUNCTION
 %token <string> IDENT
 %token <string> UIDENT
 %token TRUE FALSE
 %token <Lustre_types.expr_annot> ANNOT
-%token <Lustre_types.node_annot> NODESPEC
+%token <Lustre_types.contract_desc> NODESPEC
 %token LBRACKET RBRACKET LCUR RCUR LPAR RPAR SCOL COL COMMA COLCOL 
 %token AMPERAMPER BARBAR NOT POWER
 %token IF THEN ELSE
@@ -113,7 +113,7 @@ let rec fby expr n init =
 %type <Lustre_types.expr_annot> lustre_annot
 
 %start lustre_spec
-%type <Lustre_types.node_annot> lustre_spec
+%type <Lustre_types.contract_desc> lustre_spec
 
 %start signed_const
 %type <Lustre_types.constant> signed_const
@@ -248,7 +248,7 @@ nodespec_list:
 | NODESPEC nodespec_list { 
   (function 
   | None    -> (fun s1 -> Some s1) 
-  | Some s2 -> (fun s1 -> Some (merge_node_annot s1 s2))) $2 $1 }
+  | Some s2 -> (fun s1 -> Some (merge_contracts s1 s2))) $2 $1 }
 
 typ_def_list:
     /* empty */             { (fun itf -> []) }