Add "with" syntax

Add with syntax on AST, parsetrees, parsers and printers

compiler/heptagon/hept_printer.ml

@@ -255,11 +255,13 @@ let rec print_type_def ff { t_name = name; t_desc = tdesc } =
   fprintf ff "@[<2>type %a%a@]@." print_qualname name print_type_desc tdesc
 
 let print_contract ff { c_block = b;
-                        c_assume = e_a; c_enforce = e_g; } =
-  fprintf ff "@[<v2>contract@\n%a@ assume %a;@ enforce %a@]"
+                        c_assume = e_a; c_enforce = e_g;
+			c_controllables = c} =
+  fprintf ff "@[<v2>contract@\n%a@ assume %a@ enforce %a@ with (%a)@]"
     print_block b
     print_exp e_a
     print_exp e_g
+    print_vd_tuple c
 
 let print_node ff
     { n_name = n; n_input = ni;

compiler/heptagon/heptagon.ml

@@ -131,6 +131,7 @@ and type_dec_desc =
 type contract = {
   c_assume  : exp;
   c_enforce : exp;
+  c_controllables : var_dec list;
   c_block   : block }
 
 type node_dec = {

compiler/heptagon/parsing/hept_parser.mly

@@ -220,10 +220,11 @@ node_params:
 
 contract:
   | /* empty */ {None}
-  | CONTRACT b=block(LET) TEL? opt_assume enforce
+  | CONTRACT b=block(LET) TEL? opt_assume opt_enforce opt_with
       { Some{ c_block = b;
               c_assume = $4;
-              c_enforce = $5 } }
+              c_enforce = $5;
+	      c_controllables = $6 } }
 ;
 
 opt_assume:
@@ -231,10 +232,16 @@ opt_assume:
   | ASSUME exp { $2 }
 ;
 
-enforce:
+opt_enforce:
+  | /* empty */ { mk_constructor_exp ptrue (Loc($startpos,$endpos)) }
   | ENFORCE exp { $2 }
 ;
 
+opt_with:
+  | /* empty */ { [] }
+  | WITH LPAREN params RPAREN { $3 }
+;
+
 loc_vars:
   | /* empty */    { [] }
   | VAR loc_params { $2 }

compiler/heptagon/parsing/hept_parsetree.ml

@@ -153,6 +153,7 @@ and type_desc =
 type contract =
   { c_assume  : exp;
     c_enforce : exp;
+    c_controllables : var_dec list;
     c_block   : block }
 
 type node_dec =

compiler/minils/minils.ml

@@ -99,6 +99,7 @@ type var_dec = {
 type contract = {
   c_assume : exp;
   c_enforce : exp;
+  c_controllables : var_dec list;
   c_local : var_dec list;
   c_eq : eq list }
 
@@ -107,6 +108,8 @@ type node_dec = {
   n_input  : var_dec list;
   n_output : var_dec list;
   n_contract : contract option;
+  (* GD: inglorious hack for controller call *)
+  mutable n_controller_call : var_ident list * var_ident list;
   n_local  : var_dec list;
   n_equs   : eq list;
   n_loc    : location;

compiler/minils/mls_printer.ml

@@ -188,12 +188,14 @@ let rec print_type_dec ff { t_name = name; t_desc = tdesc } =
 
 
 let print_contract ff { c_local = l; c_eq = eqs;
-                        c_assume = e_a; c_enforce = e_g; } =
-  fprintf ff "@[<v2>contract@\n%a%a@ assume %a;@ enforce %a@]"
+                        c_assume = e_a; c_enforce = e_g;
+			c_controllables = c;} =
+  fprintf ff "@[<v2>contract@\n%a%a@ assume %a@ enforce %a@ with (%a)@]"
     print_local_vars l
     print_eqs eqs
     print_exp e_a
     print_exp e_g
+    print_vd_tuple c
 
 
 let print_node ff { n_name = n; n_input = ni; n_output = no;

compiler/minils/parsing/mls_lexer.mll

@@ -19,6 +19,10 @@ List.iter (fun (str,tok) -> Hashtbl.add keyword_table str tok) [
  "var", VAR;
  "let", LET;
  "tel", TEL;
+ "contract", CONTRACT;
+ "assume", ASSUME;
+ "enforce", ENFORCE;
+ "with", WITH;
  "fby", FBY;
  "when", WHEN;
  "merge", MERGE;

compiler/minils/parsing/mls_parser.mly

@@ -116,10 +116,44 @@ type_dec:
 node_decs: ns=list(node_dec) {ns}
 node_dec:
   NODE n=qualname p=params(n_param) LPAREN args=args RPAREN
-  RETURNS LPAREN out=args RPAREN vars=loc_vars eqs=equs
-      { mk_node p args out vars eqs ~loc:(Loc ($startpos,$endpos)) n }
+  RETURNS LPAREN out=args RPAREN
+  contract=contract vars=loc_vars eqs=equs
+      { mk_node p args out vars eqs 
+	  ~loc:(Loc ($startpos,$endpos))
+	  ~contract:contract
+	  n }
 
 
+contract:
+  | /* empty */ {None}
+  | CONTRACT
+    locvars=loc_vars
+    eqs=opt_equs
+    assume=opt_assume 
+    enforce=opt_enforce 
+    withvar=opt_with
+      { Some{ c_local=locvars;
+	      c_equs=eqs;
+              c_assume = assume;
+              c_enforce = enforce;
+	      c_controllables = withvar } }
+;
+
+opt_assume:
+  | /* empty */ { mk_constructor_exp ptrue (Loc($startpos,$endpos)) }
+  | ASSUME exp { $2 }
+;
+
+opt_enforce:
+  | /* empty */ { mk_constructor_exp ptrue (Loc($startpos,$endpos)) }
+  | ENFORCE exp { $2 }
+;
+
+opt_with:
+  | /* empty */ { [] }
+  | WITH LPAREN params RPAREN { $3 }
+;
+
 args_t: SEMICOL p=args {p}
 args:
   | /* empty */ { [] }
@@ -147,6 +181,10 @@ var:
   | ns=snlist(COMMA, NAME) COLON t=type_ident c=clock_annot
       { List.map (fun n -> mk_var_dec n t c (Loc ($startpos,$endpos))) ns }
 
+opt_equs: 
+  | /* empty */ { [] }
+  | LET e=slist(SEMICOL, equ) TEL { e }
+
 equs: LET e=slist(SEMICOL, equ) TEL { e }
 equ: p=pat EQUAL e=exp { mk_equation p e (Loc ($startpos,$endpos)) }
 

compiler/minils/parsing/mls_parsetree.ml

@@ -52,11 +52,18 @@ and var_dec = {
   v_clock : ck;
   v_loc   : location }
 
+type contract =
+  { c_assume  : exp;
+    c_enforce : exp;
+    c_controllables : var_dec list;
+    c_local   : var_dec list;
+    c_equs    : eq list }
+
 type node_dec = {
   n_name     : qualname;
   n_input    : var_dec list;
   n_output   : var_dec list;
-  n_contract : Minils.contract option;
+  n_contract : contract option;
   n_local    : var_dec list;
   n_equs     : eq list;
   n_loc      : location;