1

%{

2

open Utils

3

open Corelang

4

open LustreSpec

5


6

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

7

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

8

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

9


10

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

11

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

12

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

13


14

%}

15


16


17

%token <int> INT

18

%token <string> REAL

19

%token <float> FLOAT

20

%token <string> STRING

21

%token TRUE FALSE STATELESS ASSERT INCLUDE QUOTE

22

%token <string> IDENT

23

%token LPAR RPAR SCOL COL COMMA COLCOL

24

%token AMPERAMPER BARBAR NOT POWER

25

%token IF THEN ELSE

26

%token UCLOCK DCLOCK PHCLOCK TAIL

27

%token MERGE FBY WHEN WHENNOT EVERY

28

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

29

%token TINT TFLOAT TREAL TBOOL TCLOCK

30

%token RATE DUE

31

%token EQ LT GT LTE GTE NEQ

32

%token AND OR XOR IMPL

33

%token MULT DIV MOD

34

%token MINUS PLUS UMINUS

35

%token PRE ARROW

36

%token EOF

37

%token REQUIRES ENSURES OBSERVER

38

%token INVARIANT BEHAVIOR ASSUMES

39

%token EXISTS FORALL

40


41

%nonassoc prec_exists prec_forall

42

%nonassoc COMMA POWER

43

%left MERGE IF

44

%nonassoc ELSE

45

%right ARROW FBY

46

%left WHEN WHENNOT UCLOCK DCLOCK PHCLOCK

47

%right COLCOL

48

%right IMPL

49

%left OR XOR BARBAR

50

%left AND AMPERAMPER

51

%left NOT

52

%nonassoc EQ LT GT LTE GTE NEQ

53

%left MINUS PLUS

54

%left MULT DIV MOD

55

%left PRE

56

%nonassoc UMINUS

57


58

%start lustre_annot

59

%type <LustreSpec.expr_annot> lustre_annot

60


61

%start lustre_spec

62

%type <LustreSpec.node_annot> lustre_spec

63


64

%%

65


66

lustre_spec:

67

 contract EOF { $1 }

68


69

contract:

70

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

71


72

requires:

73

{ [] }

74

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

75


76

ensures:

77

{ [] }

78

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

79

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

80


81

behaviors:

82

{ [] }

83

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

84


85

assumes:

86

{ [] }

87

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

88


89

tuple_expr:

90

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

91

 tuple_expr COMMA expr {$3::$1}

92


93

expr:

94

 const {mkeexpr (EExpr_const $1)}

95

 IDENT

96

{mkeexpr (EExpr_ident $1)}

97

 LPAR expr RPAR

98

{$2}

99

 LPAR tuple_expr RPAR

100

{mkeexpr (EExpr_tuple (List.rev $2))}

101

 expr ARROW expr

102

{mkeexpr (EExpr_arrow ($1,$3))}

103

 expr FBY expr

104

{mkeexpr (EExpr_fby ($1,$3))}

105

 expr WHEN IDENT

106

{mkeexpr (EExpr_when ($1,$3))}

107

 MERGE LPAR IDENT COMMA expr COMMA expr RPAR

108

{mkeexpr (EExpr_merge ($3,$5,$7))}

109

 IDENT LPAR expr RPAR

110

{mkeexpr (EExpr_appl ($1, $3, None))}

111

 IDENT LPAR expr RPAR EVERY IDENT

112

{mkeexpr (EExpr_appl ($1, $3, Some $6))}

113

 IDENT LPAR tuple_expr RPAR

114

{mkeexpr (EExpr_appl ($1, mkeexpr (EExpr_tuple (List.rev $3)), None))}

115

 IDENT LPAR tuple_expr RPAR EVERY IDENT

116

{mkeexpr (EExpr_appl ($1, mkeexpr (EExpr_tuple (List.rev $3)), Some $6)) }

117


118

/* Boolean expr */

119

 expr AND expr

120

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

121

 expr AMPERAMPER expr

122

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

123

 expr OR expr

124

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

125

 expr BARBAR expr

126

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

127

 expr XOR expr

128

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

129

 NOT expr

130

{mkepredef_unary_call "not" $2}

131

 expr IMPL expr

132

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

133


134

/* Comparison expr */

135

 expr EQ expr

136

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

137

 expr LT expr

138

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

139

 expr LTE expr

140

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

141

 expr GT expr

142

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

143

 expr GTE expr

144

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

145

 expr NEQ expr

146

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

147


148

/* Arithmetic expr */

149

 expr PLUS expr

150

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

151

 expr MINUS expr

152

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

153

 expr MULT expr

154

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

155

 expr DIV expr

156

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

157

 MINUS expr %prec UMINUS

158

{mkepredef_unary_call "uminus" $2}

159

 expr MOD expr

160

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

161


162

/* Temp op */

163

 PRE expr

164

{mkeexpr (EExpr_pre $2)}

165


166

/* If */

167

 IF expr THEN expr ELSE expr

168

{mkepredef_call "ite" [$2;$4;$6]}

169


170

/* Quantifiers */

171

 EXISTS vdecl SCOL expr %prec prec_exists {mkeexpr (EExpr_exists ($2, $4))}

172

 FORALL vdecl SCOL expr %prec prec_forall {mkeexpr (EExpr_forall ($2, $4))}

173


174

vdecl:

175

 ident_list COL typ clock

176

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

177

 CONST ident_list COL typ clock

178

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

179


180


181

ident_list:

182

IDENT {[$1]}

183

 ident_list COMMA IDENT {$3::$1}

184


185


186

typ:

187

{mktyp Tydec_any}

188

 TINT {mktyp Tydec_int}

189

 IDENT {

190

try

191

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

192

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

193

}

194

 TFLOAT {mktyp Tydec_float}

195

 TREAL {mktyp Tydec_real}

196

 TBOOL {mktyp Tydec_bool}

197

 TCLOCK {mktyp (Tydec_clock Tydec_bool) }

198

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

199

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

200

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

201


202

clock:

203

{mkclock Ckdec_any}

204

 when_list

205

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

206


207

when_cond:

208

WHEN IDENT {($2, tag_true)}

209

 WHENNOT IDENT {($2, tag_false)}

210


211

when_list:

212

when_cond {[$1]}

213

 when_list when_cond {$2::$1}

214


215


216

const:

217

 INT {EConst_int $1}

218

 REAL {EConst_real $1}

219

 FLOAT {EConst_float $1}

220

 TRUE {EConst_bool true}

221

 FALSE {EConst_bool false}

222

 STRING {EConst_string $1}

223


224

lustre_annot:

225

lustre_annot_list EOF { $1 }

226


227

lustre_annot_list:

228

{ [] }

229

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

230

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

231

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

232

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

233


234

kwd:

235

DIV { [] }

236

 DIV IDENT kwd { $2::$3}
