From 4f26dcf536abc80587365e39b3f5992ac85d68fa Mon Sep 17 00:00:00 2001
From: ploc <ploc@garoche.net>
Date: Thu, 13 Sep 2018 15:36:24 +0200
Subject: [PATCH] Renamed annots into contracts. Preparing for syntax extension
---
TODO.org | 7 +++----
src/corelang.ml | 2 +-
src/corelang.mli | 2 +-
src/lustre_types.ml | 16 ++++++++++++----
src/machine_code_types.ml | 2 +-
src/parser_lustre.mly | 8 ++++----
6 files changed, 22 insertions(+), 15 deletions(-)
diff --git a/TODO.org b/TODO.org
index c697dce2..a70e2762 100644
--- a/TODO.org
+++ b/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
diff --git a/src/corelang.ml b/src/corelang.ml
index b176ef92..1155ee5f 100644
--- a/src/corelang.ml
+++ b/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;
diff --git a/src/corelang.mli b/src/corelang.mli
index 3c61b825..07715ee0 100644
--- a/src/corelang.mli
+++ b/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*)
diff --git a/src/lustre_types.ml b/src/lustre_types.ml
index 306241a5..8ea62446 100644
--- a/src/lustre_types.ml
+++ b/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 *)
diff --git a/src/machine_code_types.ml b/src/machine_code_types.ml
index 692684ab..378af262 100644
--- a/src/machine_code_types.ml
+++ b/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;
}
diff --git a/src/parser_lustre.mly b/src/parser_lustre.mly
index 6e28721e..e9e0f83f 100644
--- a/src/parser_lustre.mly
+++ b/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 -> []) }
--
GitLab