1

open Basetypes

2

open ActiveStates

3

open CPS_transformer

4


5

let ff = Format.fprintf

6


7

module LustrePrinter (

8

Vars : sig

9

val state_vars : ActiveStates.Vars.t

10

val global_vars : GlobalVarDef.t list

11


12

end) : TransformerType =

13

struct

14

include TransformerStub

15


16

type name_t = string

17

type t_base = { statements : Lustre_types.statement list; assert_false: bool }

18

type t = name_t > name_t > (ActiveStates.Vars.t * t_base)

19


20


21

let new_loc, reset_loc =

22

let cpt = ref 0 in

23

((fun () > incr cpt; Format.sprintf "loc_%i" !cpt),

24

(fun () > cpt := 0))

25


26

let new_aut, reset_aut =

27

let cpt = ref 0 in

28

((fun () > incr cpt; Format.sprintf "aut_%i" !cpt),

29

(fun () > cpt := 0))

30


31

let pp_path prefix fmt path =

32

Format.fprintf fmt "%s%t"

33

prefix

34

(fun fmt > Utils.fprintf_list ~sep:"_" Format.pp_print_string fmt path)

35


36

let pp_typed_path sin fmt path =

37

Format.fprintf fmt "%a : bool" (pp_path sin) path

38


39

let pp_vars sin fmt vars =

40

Format.fprintf fmt "%t" (fun fmt > Utils.fprintf_list ~sep:", " (pp_path sin) fmt (ActiveStates.Vars.elements vars))

41

let pp_vars_decl sin fmt vars =

42

Format.fprintf fmt "%t" (fun fmt > Utils.fprintf_list ~sep:"; " (pp_typed_path sin) fmt (ActiveStates.Vars.elements vars))

43


44

let var_to_ident prefix p =

45

pp_path prefix Format.str_formatter p;

46

Format.flush_str_formatter ()

47


48

let vars_to_ident_list ?(prefix="") vars =

49

List.map (

50

fun p > var_to_ident prefix p

51

) (ActiveStates.Vars.elements vars)

52


53

let mkvar name typ =

54

let loc = Location.dummy_loc in

55

Corelang.mkvar_decl

56

loc

57

(name, typ, Corelang.mkclock loc Lustre_types.Ckdec_any, false, None, None (*"__no_parent__" *))

58


59

let var_to_vdecl ?(prefix="") var typ = mkvar (var_to_ident prefix var) typ

60

let state_vars_to_vdecl_list ?(prefix="") vars =

61

let bool_type = Corelang.mktyp Location.dummy_loc Lustre_types.Tydec_bool in

62

List.map

63

(fun v > var_to_vdecl ~prefix:prefix v bool_type)

64

(ActiveStates.Vars.elements vars)

65


66

let mk_locals locs =

67

ActiveStates.Vars.fold (fun v accu >

68

(state_vars_to_vdecl_list ~prefix:(List.hd v) Vars.state_vars)@accu

69

) locs []

70

(* TODO: declare global vars *)

71


72

let mkeq = Corelang.mkeq Location.dummy_loc

73

let mkexpr = Corelang.mkexpr Location.dummy_loc

74

let mkpredef_call = Corelang.mkpredef_call Location.dummy_loc

75

let expr_of_bool b = mkexpr (Lustre_types.Expr_const (Corelang.const_of_bool b))

76

let mkstmt_eq lhs_vars ?(prefix_lhs="") rhs =

77

{ statements = [

78

Lustre_types.Eq (

79

mkeq (

80

vars_to_ident_list ~prefix:prefix_lhs lhs_vars, (* lhs *)

81

rhs (* rhs *)

82

)

83

)

84

];

85

assert_false = false

86

}

87

let base_to_assert b =

88

if b.assert_false then

89

[{Lustre_types.assert_expr = expr_of_bool false; assert_loc = Location.dummy_loc}]

90

else

91

[]

92


93


94

let var_to_expr ?(prefix="") p =

95

let id = var_to_ident prefix p in

96

Corelang.expr_of_ident id Location.dummy_loc

97


98

let vars_to_exprl ?(prefix="") vars =

99

List.map

100

(fun p > var_to_expr ~prefix:prefix p)

101

(ActiveStates.Vars.elements vars)

102


103


104

(* Events *)

105

let event_type_decl =

106

Corelang.mktop

107

(

108

Lustre_types.TypeDef {

109

Lustre_types.tydef_id = "event_type";

110

tydef_desc = Lustre_types.Tydec_int

111

}

112

)

113


114

let event_type = {

115

Lustre_types.ty_dec_desc = Lustre_types.Tydec_const "event_type";

116

Lustre_types.ty_dec_loc = Location.dummy_loc;

117

}

118


119

let event_var = mkvar "event" event_type

120


121


122

let const_map : (event_base_t, int) Hashtbl.t = Hashtbl.create 13

123

let get_event_const e =

124

try Hashtbl.find const_map e

125

with Not_found > (

126

let nb = Hashtbl.length const_map in

127

Hashtbl.add const_map e nb;

128

nb

129

)

130


131


132


133

let null sin sout =

134

let expr_list = vars_to_exprl ~prefix:sin Vars.state_vars in

135

ActiveStates.Vars.empty,

136

(

137

(* Nothing happen here: out_vars = in_vars *)

138

let rhs = mkexpr (Lustre_types.Expr_tuple expr_list) in

139

mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs

140

)

141


142

let bot sin sout =

143

let (vars, tr) = null sin sout in

144

(

145

ActiveStates.Vars.empty,

146

{ tr with assert_false = true }

147

)

148


149

let ( >> ) tr1 tr2 sin sout =

150

let l = new_loc () in

151

let (vars1, tr1) = tr1 sin l in

152

let (vars2, tr2) = tr2 l sout in

153

(ActiveStates.Vars.add [l] (ActiveStates.Vars.union vars1 vars2),

154

{

155

statements = tr1.statements @ tr2.statements;

156

assert_false = tr1.assert_false  tr2.assert_false

157

}

158

)

159


160

let pp_name :

161

type c. c call_t > c > unit =

162

fun call >

163

match call with

164

 Ecall > (fun (p, p', f) >

165

Format.fprintf Format.str_formatter "theta%a%a%a_%a"

166

pp_call call

167

(pp_path "_from_") p

168

(pp_path "_to_") p'

169

pp_frontier f)

170

 Dcall > (fun p >

171

Format.fprintf Format.str_formatter "theta%a%a"

172

pp_call call

173

(pp_path "_from_") p)

174

 Xcall > (fun (p, f) >

175

Format.fprintf Format.str_formatter "theta%a%a_%a"

176

pp_call call

177

(pp_path "_from_") p

178

pp_frontier f)

179


180


181

let mkcall' :

182

type c. name_t > name_t > c call_t > c > t_base =

183

fun sin sout call arg >

184

pp_name call arg;

185

let funname = Format.flush_str_formatter () in

186

let args = (Corelang.expr_of_vdecl event_var)::(vars_to_exprl ~prefix:sin Vars.state_vars) in

187

let rhs = mkpredef_call funname args in

188

mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs

189


190

let mkact' action sin sout =

191

match action with

192

 Action.Call (c, a) > mkcall' sin sout c a

193

 Action.Quote a >

194

(* TODO: check. This seems to be innappropriate *)

195

(* let funname = "action_" ^ a.ident in

196

let args = vars_to_exprl ~prefix:sin Vars.state_vars in

197

let rhs = mkpredef_call funname args in

198

mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs

199

*)

200

{

201

statements = a.defs;

202

assert_false = false

203

}

204

 Action.Open p >

205

let vars' = ActiveStates.Vars.remove p Vars.state_vars in

206

(* eq1: sout_p = true *)

207

let eq1 = mkeq ([var_to_ident sout p] , expr_of_bool true) in

208

(* eq2: sout_xx = sin_xx *)

209

let expr_list = vars_to_exprl ~prefix:sin vars' in

210

let rhs = mkexpr (Lustre_types.Expr_tuple expr_list) in

211

let eq2 = mkeq (vars_to_ident_list ~prefix:sout vars', rhs) in

212

{

213

statements = [

214

Lustre_types.Eq (eq1);

215

Lustre_types.Eq (eq2);

216

];

217

assert_false = false

218

}

219


220

 Action.Close p >

221

let vars' = ActiveStates.Vars.remove p Vars.state_vars in

222

(* eq1: sout_p = false *)

223

let eq1 = mkeq ([var_to_ident sout p] , expr_of_bool false) in

224

(* eq2: sout_xx = sin_xx *)

225

let expr_list = vars_to_exprl ~prefix:sin vars' in

226

let rhs = mkexpr (Lustre_types.Expr_tuple expr_list) in

227

let eq2 = mkeq (vars_to_ident_list ~prefix:sout vars', rhs) in

228

{

229

statements = [

230

Lustre_types.Eq (eq1);

231

Lustre_types.Eq (eq2);

232

];

233

assert_false = false

234

}

235


236

 Action.Nil >

237

let expr_list = vars_to_exprl ~prefix:sin Vars.state_vars in

238

let rhs = mkexpr (Lustre_types.Expr_tuple expr_list) in

239

mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs

240


241

let eval_act kenv (action : act_t) =

242

(*Format.printf " action = %a@." Action.pp_act action;*)

243

(fun sin sout > (ActiveStates.Vars.empty,

244

mkact' action sin sout ))

245


246

let rec mkcond' sin condition =

247

(*Format.printf " cond = %a@." Condition.pp_cond condition;*)

248

match condition with

249

 Condition.True > expr_of_bool true

250

 Condition.Active p > var_to_expr ~prefix:sin p

251

 Condition.Event e >

252

mkpredef_call "=" [

253

Corelang.expr_of_vdecl event_var;

254

mkexpr (Lustre_types.Expr_const (Lustre_types.Const_int (get_event_const e)))

255

]

256

 Condition.Neg cond > mkpredef_call "not" [mkcond' sin cond]

257

 Condition.And (cond1, cond2) > mkpredef_call "&&" [mkcond' sin cond1;

258

mkcond' sin cond2]

259

 Condition.Quote c > c.expr (* TODO: shall we prefix with sin ? *)

260


261

let rec eval_cond condition (ok:t) ko sin sout =

262

let open Lustre_types in

263

let loc = Location.dummy_loc in

264

(*Format.printf " cond = %a@." Condition.pp_cond condition;*)

265

let (vars1, tr1) = ok sin sout in

266

let (vars2, tr2) = ko sin sout in

267

let (vars0, tr0) = bot sin sout in

268

let aut = new_aut () in

269

(ActiveStates.Vars.empty,

270

{

271

statements = [

272

let handler_default_mode = (* Default mode : CenterPoint *)

273

let handler_default_mode_unless = [

274

(loc, mkcond' sin condition, true (* restart *), "Cond_" ^ aut);

275

(loc, mkcond' sin (Condition.Neg condition), true (* restart *), "NotCond_" ^ aut);

276

]

277

in

278

Automata.mkhandler

279

loc (* location *)

280

("CenterPoint_" ^ aut) (* state name *)

281

handler_default_mode_unless (* unless *)

282

[] (* until *)

283

[] (* locals *)

284

(tr0.statements, base_to_assert tr0, []) (* stmts, asserts, annots *)

285

in

286

let handler_cond_mode = (* Cond mode *)

287

let handler_cond_mode_until = [

288

(loc, expr_of_bool true, true (* restart *), "CenterPoint_" ^ aut);

289

]

290

in

291

Automata.mkhandler

292

loc (* location *)

293

("Cond_" ^ aut) (* state name *)

294

[] (* unless *)

295

handler_cond_mode_until (* until *)

296

(mk_locals vars1) (* locals *)

297

(tr1.statements, base_to_assert tr1, []) (* stmts, asserts, annots *)

298

in

299

let handler_notcond_mode = (* NotCond mode *)

300

let handler_notcond_mode_until = [

301

(loc, expr_of_bool true, true (* restart *), "CenterPoint_" ^ aut);

302

]

303

in

304

Automata.mkhandler

305

loc (* location *)

306

("NotCond_" ^ aut) (* state name *)

307

[] (* unless *)

308

handler_notcond_mode_until (* until *)

309

(mk_locals vars2) (* locals *)

310

(tr2.statements, base_to_assert tr2, []) (* stmts, asserts, annots *)

311

in

312

let handlers = [ handler_default_mode; handler_cond_mode; handler_notcond_mode ] in

313

Aut (Automata.mkautomata loc aut handlers)

314

];

315

assert_false = false

316

}

317

)

318


319

let mktransformer tr =

320

let (vars, tr) = tr "sin_" "sout_"

321

in tr

322


323

let mkcomponent :

324

type c. c call_t > c > t > Lustre_types.program =

325

fun call args >

326

fun tr >

327

reset_loc ();

328

let (vars', tr') = tr "sin_" "sout_" in

329

pp_name call args;

330

let funname = Format.flush_str_formatter () in

331

let inputs = event_var :: state_vars_to_vdecl_list ~prefix:"sin_" Vars.state_vars in

332

let outputs = state_vars_to_vdecl_list ~prefix:"sout_" Vars.state_vars in

333

let node =

334

Corelang.mktop (

335

Lustre_types.Node {Lustre_types.node_id = funname;

336

node_type = Types.new_var ();

337

node_clock = Clocks.new_var true;

338

node_inputs = inputs;

339

node_outputs = outputs;

340

node_locals = mk_locals vars'; (* TODO: add global vars *)

341

node_gencalls = [];

342

node_checks = [];

343

node_stmts = tr'.statements;

344

node_asserts = base_to_assert tr';

345

node_dec_stateless = false;

346

node_stateless = None;

347

node_spec = None;

348

node_annot = []}

349

)

350

in

351

[node]

352


353


354


355

(* TODO

356

C'est pas evident.

357

Il faut faire les choses suivantes:

358

 rajouter dans un ensemble les variables manipulées localement

359

 on doit comprendre comment les variables globales sont injectées dans le modele final:

360

 le node principal doit uniquement les afficher. Il peut les initialiser avec les valeurs init définies. Puis appeller la fcn thetacallD_from_principal.

361

 elles peuvent/doivent etre dans input et output de ce node thetacallD

362

*)

363


364


365

let mk_main_loop () =

366

(* let loc = Location.dummy_loc in *)

367


368

let call_stmt =

369

(* (%t) > pre (thetaCallD_from_principal (event, %a)) *)

370

let init =

371

let init_state_false =

372

List.map (fun _ > expr_of_bool false) (ActiveStates.Vars.elements Vars.state_vars) in

373

let init_globals =

374

List.map (fun v > v.GlobalVarDef.init_val) Vars.global_vars in

375

mkexpr (Lustre_types.Expr_tuple (init_state_false @ init_globals))

376

in

377

let args = (Corelang.expr_of_vdecl event_var)::

378

(vars_to_exprl ~prefix:"sout_" Vars.state_vars)

379

in

380

let call_expr = mkpredef_call "thetaCallD_from_principal" args in

381

let pre_call_expr = mkexpr (Lustre_types.Expr_pre (call_expr)) in

382

let rhs = mkexpr (Lustre_types.Expr_arrow (init, pre_call_expr)) in

383

mkstmt_eq Vars.state_vars ~prefix_lhs:"sout_" rhs

384

in

385

let inputs = List.map Corelang.copy_var_decl [event_var] in

386

let outputs = state_vars_to_vdecl_list ~prefix:"sout_" Vars.state_vars in

387

(* TODO add the globals as sout_data_x entry values *)

388

let node_principal =

389

Corelang.mktop (

390

Lustre_types.Node {Lustre_types.node_id = "principal_loop";

391

node_type = Types.new_var ();

392

node_clock = Clocks.new_var true;

393

node_inputs = inputs;

394

node_outputs = outputs;

395

node_locals = []; (* TODO: add global vars *)

396

node_gencalls = [];

397

node_checks = [];

398

node_asserts = base_to_assert call_stmt;

399

node_stmts = call_stmt.statements;

400

node_dec_stateless = false;

401

node_stateless = None;

402

node_spec = None;

403

node_annot = []}

404

)

405

in

406

node_principal

407


408


409

let mkprincipal tr =

410

event_type_decl :: mkcomponent Dcall ["principal"] tr @ [mk_main_loop ()]

411


412

end
