1

%{

2

(********************************************************************)

3

(* *)

4

(* The LustreC compiler toolset / The LustreC Development Team *)

5

(* Copyright 2012   ONERA  CNRS  INPT *)

6

(* *)

7

(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)

8

(* under the terms of the GNU Lesser General Public License *)

9

(* version 2.1. *)

10

(* *)

11

(********************************************************************)

12


13

open Utils

14

open Corelang

15

open LustreSpec

16


17

let mkexpr x = mkexpr (Location.symbol_rloc ()) x

18

let mkpredef_call x = mkpredef_call (Location.symbol_rloc ()) x

19

let mkpredef_unary_call x = mkpredef_unary_call (Location.symbol_rloc ()) x

20


21

let mkeexpr x = mkeexpr (Location.symbol_rloc ()) x

22

(*

23

let mkepredef_call x = mkepredef_call (Location.symbol_rloc ()) x

24

let mkepredef_unary_call x = mkepredef_unary_call (Location.symbol_rloc ()) x

25

*)

26


27

let mktyp x = mktyp (Location.symbol_rloc ()) x

28

let mkvar_decl x = mkvar_decl (Location.symbol_rloc ()) x

29

let mkclock x = mkclock (Location.symbol_rloc ()) x

30


31

%}

32


33


34

%token <int> INT

35

%token <string> REAL

36

%token <float> FLOAT

37

%token <string> STRING

38

%token TRUE FALSE STATELESS ASSERT INCLUDE QUOTE

39

%token <string> IDENT

40

%token LPAR RPAR SCOL COL COMMA COLCOL

41

%token AMPERAMPER BARBAR NOT POWER

42

%token IF THEN ELSE

43

%token UCLOCK DCLOCK PHCLOCK TAIL

44

%token MERGE FBY WHEN WHENNOT EVERY

45

%token NODE LET TEL RETURNS VAR IMPORTED SENSOR ACTUATOR WCET TYPE CONST

46

%token TINT TFLOAT TREAL TBOOL TCLOCK

47

%token RATE DUE

48

%token EQ LT GT LTE GTE NEQ

49

%token AND OR XOR IMPL

50

%token MULT DIV MOD

51

%token MINUS PLUS UMINUS

52

%token PRE ARROW

53

%token EOF

54

%token REQUIRES ENSURES OBSERVER

55

%token INVARIANT BEHAVIOR ASSUMES

56

%token EXISTS FORALL

57


58

%nonassoc prec_exists prec_forall

59

%nonassoc COMMA POWER

60

%left MERGE IF

61

%nonassoc ELSE

62

%right ARROW FBY

63

%left WHEN WHENNOT UCLOCK DCLOCK PHCLOCK

64

%right COLCOL

65

%right IMPL

66

%left OR XOR BARBAR

67

%left AND AMPERAMPER

68

%left NOT

69

%nonassoc EQ LT GT LTE GTE NEQ

70

%left MINUS PLUS

71

%left MULT DIV MOD

72

%left PRE

73

%nonassoc UMINUS

74


75

%start lustre_annot

76

%type <LustreSpec.ident > LustreSpec.expr_annot> lustre_annot

77


78

%start lustre_spec

79

%type <LustreSpec.node_annot> lustre_spec

80


81

%%

82


83

lustre_spec:

84

 contract EOF { $1 }

85


86

contract:

87

requires ensures behaviors { { requires = $1; ensures = $2; behaviors = $3; } }

88


89

requires:

90

{ [] }

91

 REQUIRES qexpr SCOL requires { $2::$4 }

92


93

ensures:

94

{ [] }

95

 ENSURES qexpr SCOL ensures { (EnsuresExpr $2) :: $4 }

96

 OBSERVER IDENT LPAR tuple_qexpr RPAR SCOL ensures { (SpecObserverNode($2,$4)) :: $7 }

97


98

behaviors:

99

{ [] }

100

 BEHAVIOR IDENT COL assumes ensures behaviors { ($2,$4,$5)::$6 }

101


102

assumes:

103

{ [] }

104

 ASSUMES qexpr SCOL assumes { $2::$4 }

105


106

tuple_qexpr:

107

 qexpr COMMA qexpr {[$3;$1]}

108

 tuple_qexpr COMMA qexpr {$3::$1}

109


110


111

tuple_expr:

112

expr COMMA expr {[$3;$1]}

113

 tuple_expr COMMA expr {$3::$1}

114


115

// Same as tuple expr but accepting lists with single element

116

array_expr:

117

expr {[$1]}

118

 expr COMMA array_expr {$1::$3}

119


120

dim_list:

121

dim RBRACKET { fun base > mkexpr (Expr_access (base, $1)) }

122

 dim RBRACKET LBRACKET dim_list { fun base > $4 (mkexpr (Expr_access (base, $1))) }

123


124

expr:

125

/* constants */

126

INT {mkexpr (Expr_const (Const_int $1))}

127

 REAL {mkexpr (Expr_const (Const_real $1))}

128

 FLOAT {mkexpr (Expr_const (Const_float $1))}

129

/* Idents or type enum tags */

130

 IDENT {

131

if Hashtbl.mem tag_table $1

132

then mkexpr (Expr_const (Const_tag $1))

133

else mkexpr (Expr_ident $1)}

134

 LPAR ANNOT expr RPAR

135

{update_expr_annot $3 $2}

136

 LPAR expr RPAR

137

{$2}

138

 LPAR tuple_expr RPAR

139

{mkexpr (Expr_tuple (List.rev $2))}

140


141

/* Array expressions */

142

 LBRACKET array_expr RBRACKET { mkexpr (Expr_array $2) }

143

 expr POWER dim { mkexpr (Expr_power ($1, $3)) }

144

 expr LBRACKET dim_list { $3 $1 }

145


146

/* Temporal operators */

147

 PRE expr

148

{mkexpr (Expr_pre $2)}

149

 expr ARROW expr

150

{mkexpr (Expr_arrow ($1,$3))}

151

 expr FBY expr

152

{(*mkexpr (Expr_fby ($1,$3))*)

153

mkexpr (Expr_arrow ($1, mkexpr (Expr_pre $3)))}

154

 expr WHEN IDENT

155

{mkexpr (Expr_when ($1,$3,tag_true))}

156

 expr WHENNOT IDENT

157

{mkexpr (Expr_when ($1,$3,tag_false))}

158

 expr WHEN IDENT LPAR IDENT RPAR

159

{mkexpr (Expr_when ($1, $5, $3))}

160

 MERGE IDENT handler_expr_list

161

{mkexpr (Expr_merge ($2,$3))}

162


163

/* Applications */

164

 IDENT LPAR expr RPAR

165

{mkexpr (Expr_appl ($1, $3, None))}

166

 IDENT LPAR expr RPAR EVERY IDENT

167

{mkexpr (Expr_appl ($1, $3, Some ($6, tag_true)))}

168

 IDENT LPAR expr RPAR EVERY IDENT LPAR IDENT RPAR

169

{mkexpr (Expr_appl ($1, $3, Some ($8, $6))) }

170

 IDENT LPAR tuple_expr RPAR

171

{mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), None))}

172

 IDENT LPAR tuple_expr RPAR EVERY IDENT

173

{mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($6, tag_true))) }

174

 IDENT LPAR tuple_expr RPAR EVERY IDENT LPAR IDENT RPAR

175

{mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($8, $6))) }

176


177

/* Boolean expr */

178

 expr AND expr

179

{mkpredef_call "&&" [$1;$3]}

180

 expr AMPERAMPER expr

181

{mkpredef_call "&&" [$1;$3]}

182

 expr OR expr

183

{mkpredef_call "" [$1;$3]}

184

 expr BARBAR expr

185

{mkpredef_call "" [$1;$3]}

186

 expr XOR expr

187

{mkpredef_call "xor" [$1;$3]}

188

 NOT expr

189

{mkpredef_unary_call "not" $2}

190

 expr IMPL expr

191

{mkpredef_call "impl" [$1;$3]}

192


193

/* Comparison expr */

194

 expr EQ expr

195

{mkpredef_call "=" [$1;$3]}

196

 expr LT expr

197

{mkpredef_call "<" [$1;$3]}

198

 expr LTE expr

199

{mkpredef_call "<=" [$1;$3]}

200

 expr GT expr

201

{mkpredef_call ">" [$1;$3]}

202

 expr GTE expr

203

{mkpredef_call ">=" [$1;$3]}

204

 expr NEQ expr

205

{mkpredef_call "!=" [$1;$3]}

206


207

/* Arithmetic expr */

208

 expr PLUS expr

209

{mkpredef_call "+" [$1;$3]}

210

 expr MINUS expr

211

{mkpredef_call "" [$1;$3]}

212

 expr MULT expr

213

{mkpredef_call "*" [$1;$3]}

214

 expr DIV expr

215

{mkpredef_call "/" [$1;$3]}

216

 MINUS expr %prec UMINUS

217

{mkpredef_unary_call "uminus" $2}

218

 expr MOD expr

219

{mkpredef_call "mod" [$1;$3]}

220


221

/* If */

222

 IF expr THEN expr ELSE expr

223

{mkexpr (Expr_ite ($2, $4, $6))}

224


225


226

handler_expr_list:

227

{ [] }

228

 handler_expr handler_expr_list { $1 :: $2 }

229


230

handler_expr:

231

LPAR IDENT ARROW expr RPAR { ($2, $4) }

232


233

qexpr:

234

 expr { mkeexpr [] $1 }

235

/* Quantifiers */

236

 EXISTS vdecl SCOL qexpr %prec prec_exists { extend_eepxr (Exists, $2) $4 }

237

 FORALL vdecl SCOL qexpr %prec prec_forall { extend_eepxr (Forall, $2) $4 }

238


239

vdecl:

240

 ident_list COL typ clock

241

{List.map mkvar_decl (List.map (fun id > (id, $3, $4, false)) $1)}

242

 CONST ident_list COL typ clock

243

{List.map mkvar_decl (List.map (fun id > (id, $4, $5, true)) $2)}

244


245


246

ident_list:

247

IDENT {[$1]}

248

 ident_list COMMA IDENT {$3::$1}

249


250


251

typ:

252

{mktyp Tydec_any}

253

 TINT {mktyp Tydec_int}

254

 IDENT {

255

try

256

mktyp (Hashtbl.find Corelang.type_table (Tydec_const $1))

257

with Not_found > raise (Corelang.Error (Location.symbol_rloc(), Corelang.Unbound_symbol ("type " ^ $1)))

258

}

259

 TFLOAT {mktyp Tydec_float}

260

 TREAL {mktyp Tydec_real}

261

 TBOOL {mktyp Tydec_bool}

262

 TCLOCK {mktyp (Tydec_clock Tydec_bool) }

263

 typ POWER INT {mktyp Tydec_any (*(mktyptuple $3 $1)*)}

264

 typ POWER IDENT {mktyp Tydec_any (*(mktyptuple (try

265

match get_const $3 with Const_int i > i with _ > failwith "Const power error") $1)*)}

266


267

clock:

268

{mkclock Ckdec_any}

269

 when_list

270

{mkclock (Ckdec_bool (List.rev $1))}

271


272

when_cond:

273

WHEN IDENT {($2, tag_true)}

274

 WHENNOT IDENT {($2, tag_false)}

275


276

when_list:

277

when_cond {[$1]}

278

 when_list when_cond {$2::$1}

279


280


281

const:

282

 INT {Const_int $1}

283

 REAL {Const_real $1}

284

 FLOAT {Const_float $1}

285

 TRUE {Const_bool true}

286

 FALSE {Const_bool false}

287

 STRING {Const_string $1}

288


289

lustre_annot:

290

lustre_annot_list EOF { fun node_id > $1 }

291


292

lustre_annot_list:

293

{ [] }

294

 kwd COL expr SCOL lustre_annot_list { ($1,$3)::$5 }

295

 IDENT COL expr SCOL lustre_annot_list { ([$1],$3)::$5 }

296

 INVARIANT COL expr SCOL lustre_annot_list{ (["invariant"],$3)::$5 }

297

 OBSERVER COL expr SCOL lustre_annot_list { (["observer"],$3)::$5 }

298


299

kwd:

300

DIV { [] }

301

 DIV IDENT kwd { $2::$3}
