1

open Basetypes

2

open CPS_transformer

3


4

let ff = Format.fprintf

5


6

module LustrePrinter (Vars : sig

7

val state_vars : ActiveStates.Vars.t

8


9

val global_vars : GlobalVarDef.t list

10

end) : TransformerType = struct

11

include TransformerStub

12


13

type name_t = string

14


15

type t_base = {

16

statements : Lustre_types.statement list;

17

assert_false : bool;

18

}

19


20

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

21


22

let new_loc, reset_loc =

23

let cpt = ref 0 in

24

( (fun () >

25

incr cpt;

26

Format.sprintf "loc_%i" !cpt),

27

fun () > cpt := 0 )

28


29

let new_aut, _reset_aut =

30

let cpt = ref 0 in

31

( (fun () >

32

incr cpt;

33

Format.sprintf "aut_%i" !cpt),

34

fun () > cpt := 0 )

35


36

let pp_path prefix fmt path =

37

Format.fprintf fmt "%s%t" prefix (fun fmt >

38

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

39


40

(* let pp_typed_path sin fmt path =

41

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

42


43

(* let pp_vars sin fmt vars =

44

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

45

(* let pp_vars_decl sin fmt vars =

46

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

47


48

let var_to_ident prefix p =

49

pp_path prefix Format.str_formatter p;

50

Format.flush_str_formatter ()

51


52

let vars_to_ident_list ?(prefix = "") vars =

53

List.map (fun p > var_to_ident prefix p) (ActiveStates.Vars.elements vars)

54


55

let mkvar name typ =

56

let loc = Location.dummy_loc in

57

Corelang.mkvar_decl loc

58

( name,

59

typ,

60

Corelang.mkclock loc Lustre_types.Ckdec_any,

61

false,

62

None,

63

None (*"__no_parent__" *) )

64


65

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

66


67

let state_vars_to_vdecl_list ?(prefix = "") vars =

68

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

69

List.map

70

(fun v > var_to_vdecl ~prefix v bool_type)

71

(ActiveStates.Vars.elements vars)

72


73

let mk_locals locs =

74

ActiveStates.Vars.fold

75

(fun v accu >

76

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

77

locs []

78

(* TODO: declare global vars *)

79


80

let mkeq = Corelang.mkeq Location.dummy_loc

81


82

let mkexpr = Corelang.mkexpr Location.dummy_loc

83


84

let mkpredef_call = Corelang.mkpredef_call Location.dummy_loc

85


86

let expr_of_bool b =

87

mkexpr (Lustre_types.Expr_const (Corelang.const_of_bool b))

88


89

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

90

{

91

statements =

92

[

93

Lustre_types.Eq

94

(mkeq

95

( vars_to_ident_list ~prefix:prefix_lhs lhs_vars,

96

(* lhs *)

97

rhs (* rhs *) ));

98

];

99

assert_false = false;

100

}

101


102

let base_to_assert b =

103

if b.assert_false then

104

[

105

{

106

Lustre_types.assert_expr = expr_of_bool false;

107

assert_loc = Location.dummy_loc;

108

};

109

]

110

else []

111


112

let var_to_expr ?(prefix = "") p =

113

let id = var_to_ident prefix p in

114

Corelang.expr_of_ident id Location.dummy_loc

115


116

let vars_to_exprl ?(prefix = "") vars =

117

List.map (fun p > var_to_expr ~prefix p) (ActiveStates.Vars.elements vars)

118


119

(* Events *)

120

let event_type_decl =

121

Corelang.mktop

122

(Lustre_types.TypeDef

123

{

124

Lustre_types.tydef_id = "event_type";

125

tydef_desc = Lustre_types.Tydec_int;

126

})

127


128

let event_type =

129

{

130

Lustre_types.ty_dec_desc = Lustre_types.Tydec_const "event_type";

131

Lustre_types.ty_dec_loc = Location.dummy_loc;

132

}

133


134

let event_var = mkvar "event" event_type

135


136

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

137


138

let get_event_const e =

139

try Hashtbl.find const_map e

140

with Not_found >

141

let nb = Hashtbl.length const_map in

142

Hashtbl.add const_map e nb;

143

nb

144


145

let null sin sout =

146

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

147

( ActiveStates.Vars.empty,

148

(* Nothing happen here: out_vars = in_vars *)

149

let rhs = mkexpr (Lustre_types.Expr_tuple expr_list) in

150

mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs )

151


152

let bot sin sout =

153

let _, tr = null sin sout in

154

ActiveStates.Vars.empty, { tr with assert_false = true }

155


156

let ( >> ) tr1 tr2 sin sout =

157

let l = new_loc () in

158

let vars1, tr1 = tr1 sin l in

159

let vars2, tr2 = tr2 l sout in

160

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

161

{

162

statements = tr1.statements @ tr2.statements;

163

assert_false = tr1.assert_false  tr2.assert_false;

164

} )

165


166

let pp_name : type c. c call_t > c > unit =

167

fun call >

168

match call with

169

 Ecall >

170

fun (p, p', f) >

171

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

172

(pp_path "_from_") p (pp_path "_to_") p' pp_frontier f

173

 Dcall >

174

fun p >

175

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

176

(pp_path "_from_") p

177

 Xcall >

178

fun (p, f) >

179

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

180

(pp_path "_from_") p pp_frontier f

181


182

let mkcall' : 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 =

187

Corelang.expr_of_vdecl event_var

188

:: vars_to_exprl ~prefix:sin Vars.state_vars

189

in

190

let rhs = mkpredef_call funname args in

191

mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs

192


193

let mkact' action sin sout =

194

match action with

195

 Action.Call (c, a) >

196

mkcall' sin sout c a

197

 Action.Quote a >

198

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

199

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

200

~prefix:sin Vars.state_vars in let rhs = mkpredef_call funname args in

201

mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs *)

202

{ statements = a.defs; assert_false = false }

203

 Action.Open p >

204

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

205

(* eq1: sout_p = true *)

206

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

207

(* eq2: sout_xx = sin_xx *)

208

let expr_list = vars_to_exprl ~prefix:sin vars' in

209

let rhs = mkexpr (Lustre_types.Expr_tuple expr_list) in

210

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

211

{

212

statements = [ Lustre_types.Eq eq1; Lustre_types.Eq eq2 ];

213

assert_false = false;

214

}

215

 Action.Close p >

216

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

217

(* eq1: sout_p = false *)

218

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

219

(* eq2: sout_xx = sin_xx *)

220

let expr_list = vars_to_exprl ~prefix:sin vars' in

221

let rhs = mkexpr (Lustre_types.Expr_tuple expr_list) in

222

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

223

{

224

statements = [ Lustre_types.Eq eq1; Lustre_types.Eq eq2 ];

225

assert_false = false;

226

}

227

 Action.Nil >

228

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

229

let rhs = mkexpr (Lustre_types.Expr_tuple expr_list) in

230

mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs

231


232

let eval_act _kenv (action : act_t)

233

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

234

sin sout =

235

ActiveStates.Vars.empty, mkact' action sin sout

236


237

let rec mkcond' sin condition =

238

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

239

match condition with

240

 Condition.True >

241

expr_of_bool true

242

 Condition.Active p >

243

var_to_expr ~prefix:sin p

244

 Condition.Event e >

245

mkpredef_call "="

246

[

247

Corelang.expr_of_vdecl event_var;

248

mkexpr

249

(Lustre_types.Expr_const

250

(Lustre_types.Const_int (get_event_const e)));

251

]

252

 Condition.Neg cond >

253

mkpredef_call "not" [ mkcond' sin cond ]

254

 Condition.And (cond1, cond2) >

255

mkpredef_call "&&" [ mkcond' sin cond1; mkcond' sin cond2 ]

256

 Condition.Quote c >

257

c.expr

258

(* TODO: shall we prefix with sin ? *)

259


260

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

261

let open Lustre_types in

262

let loc = Location.dummy_loc in

263

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

264

let vars1, tr1 = ok sin sout in

265

let vars2, tr2 = ko sin sout in

266

let _, tr0 = bot sin sout in

267

let aut = new_aut () in

268

( ActiveStates.Vars.empty,

269

{

270

statements =

271

[

272

(let handler_default_mode =

273

(* Default mode : CenterPoint *)

274

let handler_default_mode_unless =

275

[

276

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

277

( loc,

278

mkcond' sin (Condition.Neg condition),

279

true (* restart *),

280

"NotCond_" ^ aut );

281

]

282

in

283

Automata.mkhandler loc

284

(* location *)

285

("CenterPoint_" ^ aut)

286

(* state name *)

287

handler_default_mode_unless (* unless *) [] (* until *) []

288

(* locals *)

289

(tr0.statements, base_to_assert tr0, [])

290

(* stmts, asserts, annots *)

291

in

292

let handler_cond_mode =

293

(* Cond mode *)

294

let handler_cond_mode_until =

295

[

296

( loc,

297

expr_of_bool true,

298

true (* restart *),

299

"CenterPoint_" ^ aut );

300

]

301

in

302

Automata.mkhandler loc

303

(* location *)

304

("Cond_" ^ aut)

305

(* state name *)

306

[] (* unless *) handler_cond_mode_until

307

(* until *)

308

(mk_locals vars1)

309

(* locals *)

310

(tr1.statements, base_to_assert tr1, [])

311

(* stmts, asserts, annots *)

312

in

313

let handler_notcond_mode =

314

(* NotCond mode *)

315

let handler_notcond_mode_until =

316

[

317

( loc,

318

expr_of_bool true,

319

true (* restart *),

320

"CenterPoint_" ^ aut );

321

]

322

in

323

Automata.mkhandler loc

324

(* location *)

325

("NotCond_" ^ aut)

326

(* state name *)

327

[] (* unless *) handler_notcond_mode_until

328

(* until *)

329

(mk_locals vars2)

330

(* locals *)

331

(tr2.statements, base_to_assert tr2, [])

332

(* stmts, asserts, annots *)

333

in

334

let handlers =

335

[ handler_default_mode; handler_cond_mode; handler_notcond_mode ]

336

in

337

Aut (Automata.mkautomata loc aut handlers));

338

];

339

assert_false = false;

340

} )

341


342

(* let mktransformer tr =

343

* let _, tr = tr "sin_" "sout_"

344

* in tr *)

345


346

let mkcomponent : type c. c call_t > c > t > Lustre_types.program_t =

347

fun call args tr >

348

reset_loc ();

349

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

350

pp_name call args;

351

let funname = Format.flush_str_formatter () in

352

let inputs =

353

event_var :: state_vars_to_vdecl_list ~prefix:"sin_" Vars.state_vars

354

in

355

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

356

let node =

357

Corelang.mktop

358

(Lustre_types.Node

359

{

360

Lustre_types.node_id = funname;

361

node_type = Types.new_var ();

362

node_clock = Clocks.new_var true;

363

node_inputs = inputs;

364

node_outputs = outputs;

365

node_locals = mk_locals vars';

366

(* TODO: add global vars *)

367

node_gencalls = [];

368

node_checks = [];

369

node_stmts = tr'.statements;

370

node_asserts = base_to_assert tr';

371

node_dec_stateless = false;

372

node_stateless = None;

373

node_spec = None;

374

node_annot = [];

375

node_iscontract = false;

376

})

377

in

378

[ node ]

379


380

(* TODO C'est pas evident. Il faut faire les choses suivantes:  rajouter dans

381

un ensemble les variables manipulées localement  on doit comprendre

382

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

383

node principal doit uniquement les afficher. Il peut les initialiser avec

384

les valeurs init définies. Puis appeller la fcn thetacallD_from_principal.

385

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

386


387

let mk_main_loop () =

388

(* let loc = Location.dummy_loc in *)

389

let call_stmt =

390

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

391

let init =

392

let init_state_false =

393

List.map

394

(fun _ > expr_of_bool false)

395

(ActiveStates.Vars.elements Vars.state_vars)

396

in

397

let init_globals =

398

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

399

in

400

mkexpr (Lustre_types.Expr_tuple (init_state_false @ init_globals))

401

in

402

let args =

403

Corelang.expr_of_vdecl event_var

404

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

405

in

406

let call_expr = mkpredef_call "thetaCallD_from_principal" args in

407

let pre_call_expr = mkexpr (Lustre_types.Expr_pre call_expr) in

408

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

409

mkstmt_eq Vars.state_vars ~prefix_lhs:"sout_" rhs

410

in

411

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

412

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

413

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

414

let node_principal =

415

Corelang.mktop

416

(Lustre_types.Node

417

{

418

Lustre_types.node_id = "principal_loop";

419

node_type = Types.new_var ();

420

node_clock = Clocks.new_var true;

421

node_inputs = inputs;

422

node_outputs = outputs;

423

node_locals = [];

424

(* TODO: add global vars *)

425

node_gencalls = [];

426

node_checks = [];

427

node_asserts = base_to_assert call_stmt;

428

node_stmts = call_stmt.statements;

429

node_dec_stateless = false;

430

node_stateless = None;

431

node_spec = None;

432

node_annot = [];

433

node_iscontract = false;

434

})

435

in

436

node_principal

437


438

let mkprincipal tr =

439

event_type_decl :: mkcomponent Dcall [ "principal" ] tr

440

@ [ mk_main_loop () ]

441

end

442


443

(* Local Variables: *)

444

(* compilecommand:"make C ../../../.." *)

445

(* End: *)
