From fac69ac2fa6173e68dffd3eef2bbbc84a68f16c5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?C=C3=A9dric=20Pasteur?= Date: Fri, 16 Jul 2010 16:08:14 +0200 Subject: [PATCH] Remove controllables from parser --- compiler/heptagon/parsing/hept_parser.mly | 10 ++-------- compiler/heptagon/parsing/hept_parsetree.ml | 1 - 2 files changed, 2 insertions(+), 9 deletions(-) diff --git a/compiler/heptagon/parsing/hept_parser.mly b/compiler/heptagon/parsing/hept_parser.mly index 713c139..140e113 100644 --- a/compiler/heptagon/parsing/hept_parser.mly +++ b/compiler/heptagon/parsing/hept_parser.mly @@ -206,12 +206,11 @@ node_params: contract: | /* empty */ {None} - | CONTRACT loc_vars opt_equs opt_assume enforce opt_with + | CONTRACT loc_vars opt_equs opt_assume enforce {Some{c_local = $2; c_eq = $3; c_assume = $4; - c_enforce = $5; - c_controllables = $6 }} + c_enforce = $5 }} ; opt_equs: @@ -228,11 +227,6 @@ enforce: | ENFORCE exp { $2 } ; -opt_with: - | /* empty */ { [] } - | WITH LPAREN params RPAREN { $3 } -; - loc_vars: | /* empty */ { [] } | VAR loc_params { $2 } diff --git a/compiler/heptagon/parsing/hept_parsetree.ml b/compiler/heptagon/parsing/hept_parsetree.ml index 6fecee9..b92404a 100644 --- a/compiler/heptagon/parsing/hept_parsetree.ml +++ b/compiler/heptagon/parsing/hept_parsetree.ml @@ -115,7 +115,6 @@ and type_desc = type contract = { c_assume : exp; c_enforce : exp; - c_controllables : var_dec list; c_local : var_dec list; c_eq : eq list; }