1

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

2

(* *)

3

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

4

(* Copyright 2012   ONERA  CNRS  INPT *)

5

(* *)

6

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

7

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

8

(* version 2.1. *)

9

(* *)

10

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

11


12

open Lustre_types

13

open Machine_code_types

14

open Machine_code_common

15

open Spec_types

16

open Spec_common

17

open Corelang

18

open Clocks

19

open Causality

20

open Utils

21


22

exception NormalizationError

23


24

(* Questions:

25


26

 where are used the mconst. They contain initialization of constant in

27

nodes. But they do not seem to be used by c_backend *)

28


29

(* translate_<foo> : vars > context > <foo> > machine code/expression *)

30

(* the context contains m : state aka memory variables *)

31

(* si : initialization instructions *)

32

(* j : node aka machine instances *)

33

(* d : local variables *)

34

(* s : step instructions *)

35


36

(* Machine processing requires knowledge about variables and local variables.

37

Local could be memories while other could not. *)

38

type machine_env = { is_local : string > bool; get_var : string > var_decl }

39


40

let build_env inputs locals outputs =

41

let all = List.sort_uniq VDeclModule.compare (locals @ inputs @ outputs) in

42

{

43

is_local = (fun id > List.exists (fun v > v.var_id = id) locals);

44

get_var =

45

(fun id >

46

try List.find (fun v > v.var_id = id) all

47

with Not_found >

48

(* Format.eprintf "Impossible to find variable %s in set %a@.@?" * id

49

* VSet.pp all; *)

50

raise Not_found);

51

}

52


53

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

54

(* Basic functions to translate to machine values, instructions *)

55

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

56


57

let translate_ident env id =

58

(* Format.eprintf "trnaslating ident: %s@." id; *)

59

(* id is a var that shall be visible here , ie. in vars *)

60

try

61

let var_id = env.get_var id in

62

vdecl_to_val var_id

63

with Not_found > (

64

(* id is a constant *)

65

try

66

let vdecl =

67

Corelang.var_decl_of_const

68

(const_of_top (Hashtbl.find Corelang.consts_table id))

69

in

70

vdecl_to_val vdecl

71

with Not_found > (

72

(* id is a tag, getting its type in the list of declared enums *)

73

try id_to_tag id

74

with Not_found >

75

Format.eprintf "internal error: Machine_code.translate_ident %s@.@?" id;

76

assert false))

77


78

(* specialize predefined (polymorphic) operators wrt their instances, so that

79

the C semantics is preserved *)

80

let specialize_to_c expr =

81

match expr.expr_desc with

82

 Expr_appl (id, e, r) >

83

if

84

List.exists

85

(fun e > Types.is_bool_type e.expr_type)

86

(expr_list_of_expr e)

87

then

88

let id = match id with "=" > "equi"  "!=" > "xor"  _ > id in

89

{ expr with expr_desc = Expr_appl (id, e, r) }

90

else expr

91

 _ >

92

expr

93


94

let specialize_op expr =

95

match !Options.output with Options.OutC > specialize_to_c expr  _ > expr

96


97

let rec translate_expr env expr =

98

let expr = specialize_op expr in

99

let translate_expr = translate_expr env in

100

let value_desc =

101

match expr.expr_desc with

102

 Expr_const v >

103

Cst v

104

 Expr_ident x >

105

(translate_ident env x).value_desc

106

 Expr_array el >

107

Array (List.map translate_expr el)

108

 Expr_access (t, i) >

109

Access (translate_expr t, translate_expr (expr_of_dimension i))

110

 Expr_power (e, n) >

111

Power (translate_expr e, translate_expr (expr_of_dimension n))

112

 Expr_when (e1, _, _) >

113

(translate_expr e1).value_desc

114

 Expr_appl (id, e, _) when Basic_library.is_expr_internal_fun expr >

115

let nd = node_from_name id in

116

Fun (node_name nd, List.map translate_expr (expr_list_of_expr e))

117

 Expr_ite (g, t, e) when Backends.is_functional () >

118

(* special treatment depending on the active backend. For functional ones,

119

like horn backend, ite are preserved in expression. While they are

120

removed for C or Java backends. *)

121

Fun ("ite", [ translate_expr g; translate_expr t; translate_expr e ])

122

 _ >

123

Format.eprintf

124

"Normalization error for backend %t: %a@."

125

Options.pp_output

126

Printers.pp_expr

127

expr;

128

raise NormalizationError

129

in

130

mk_val value_desc expr.expr_type

131


132

let translate_guard env expr =

133

match expr.expr_desc with

134

 Expr_ident x >

135

translate_ident env x

136

 _ >

137

Format.eprintf "internal error: translate_guard %a@." Printers.pp_expr expr;

138

assert false

139


140

let rec translate_act env (y, expr) =

141

let translate_act = translate_act env in

142

let translate_guard = translate_guard env in

143

let translate_expr = translate_expr env in

144

let lustre_eq = Corelang.mkeq Location.dummy ([ y.var_id ], expr) in

145

match expr.expr_desc with

146

 Expr_ite (c, t, e) >

147

let c = translate_guard c in

148

let t, spec_t = translate_act (y, t) in

149

let e, spec_e = translate_act (y, e) in

150

mk_conditional ~lustre_eq c [ t ] [ e ], mk_conditional_tr c spec_t spec_e

151

 Expr_merge (x, hl) >

152

let var_x = env.get_var x in

153

let hl, spec_hl =

154

List.(

155

split

156

(map

157

(fun (t, h) >

158

let h, spec_h = translate_act (y, h) in

159

(t, [ h ]), (t, spec_h))

160

hl))

161

in

162

mk_branch' ~lustre_eq var_x hl, mk_branch_tr var_x spec_hl

163

 _ >

164

let e = translate_expr expr in

165

mk_assign ~lustre_eq y e, mk_assign_tr y e

166


167

let get_memory env mems eq =

168

match eq.eq_lhs, eq.eq_rhs.expr_desc with

169

 ([ x ], Expr_pre _  [ x ], Expr_fby _) when env.is_local x >

170

let var_x = env.get_var x in

171

VSet.add var_x mems

172

 _ >

173

mems

174


175

let get_memories env = List.fold_left (get_memory env) VSet.empty

176


177

(* Datastructure updated while visiting equations *)

178

type machine_ctx = {

179

(* memories *)

180

m : ISet.t;

181

(* Reset instructions *)

182

si : instr_t list;

183

(* Instances *)

184

j : (Lustre_types.top_decl * Dimension.t list) IMap.t;

185

(* Step instructions *)

186

s : instr_t list;

187

(* Memory pack spec *)

188

mp : mc_formula_t list;

189

(* Transition spec *)

190

t :

191

(var_decl list

192

(* vars *)

193

* ISet.t (* memory footprint *)

194

* ident IMap.t

195

(* memory instances footprint *)

196

* mc_formula_t)

197

(* formula *)

198

list;

199

}

200


201

let ctx_init =

202

{ m = ISet.empty; si = []; j = IMap.empty; s = []; mp = []; t = [] }

203


204

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

205

(* Main function to translate equations into this machine context we are

206

building *)

207

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

208


209

let mk_control v l inst = mkinstr (MBranch (vdecl_to_val v, [ l, [ inst ] ]))

210


211

let control_on_clock env ck inst =

212

let rec aux ((fspec, inst) as acc) ck =

213

match (Clocks.repr ck).cdesc with

214

 Con (ck, cr, l) >

215

let id = Clocks.const_of_carrier cr in

216

let v = env.get_var id in

217

aux

218

( (fun spec > Imply (Equal (Var v, Tag (l, v.var_type)), fspec spec)),

219

mk_control v l inst )

220

ck

221

 _ >

222

acc

223

in

224

let fspec, inst = aux ((fun spec > spec), inst) ck in

225

fspec, inst

226


227

let reset_instance env i r c =

228

match r with

229

 Some r >

230

let r = translate_guard env r in

231

let _, inst =

232

control_on_clock

233

env

234

c

235

(mk_conditional r [ mkinstr (MSetReset i) ] [ mkinstr (MNoReset i) ])

236

in

237

Some r, [ inst ]

238

 None >

239

None, []

240


241

let translate_eq env ctx nd inputs locals outputs i eq =

242

let stateless = fst (get_stateless_status_node nd) in

243

let id = nd.node_id in

244

let translate_expr = translate_expr env in

245

let translate_act = translate_act env in

246

let locals_pi = Lustre_live.inter_live_i_with id (i  1) locals in

247

let outputs_pi = Lustre_live.inter_live_i_with id (i  1) outputs in

248

let locals_i = Lustre_live.inter_live_i_with id i locals in

249

let outputs_i = Lustre_live.inter_live_i_with id i outputs in

250

let pred_mp ctx a = And [ mk_memory_pack ~i:(i  1) id; a ] :: ctx.mp in

251

let pred_t ctx a =

252

( inputs @ locals_i @ outputs_i,

253

ctx.m,

254

IMap.map (fun (td, _) > node_name td) ctx.j,

255

Exists

256

( Lustre_live.existential_vars id i eq (locals @ outputs),

257

And

258

[

259

mk_transition

260

~i:(i  1)

261

stateless

262

id

263

(vdecls_to_vals (inputs @ locals_pi @ outputs_pi));

264

a;

265

] ) )

266

:: ctx.t

267

in

268

let control_on_clock ck inst spec_mp spec_t ctx =

269

let fspec, inst = control_on_clock env ck inst in

270

{

271

ctx with

272

s =

273

{

274

inst with

275

instr_spec =

276

(if fst (get_stateless_status_node nd) then []

277

else [ mk_memory_pack ~i id ])

278

@ [

279

mk_transition

280

~i

281

stateless

282

id

283

(vdecls_to_vals (inputs @ locals_i @ outputs_i));

284

];

285

}

286

:: ctx.s;

287

mp = pred_mp ctx spec_mp;

288

t = pred_t ctx (fspec spec_t);

289

}

290

in

291

let reset_instance = reset_instance env in

292

let mkinstr' = mkinstr ~lustre_eq:eq in

293

let ctl ?(ck = eq.eq_rhs.expr_clock) instr =

294

control_on_clock ck (mkinstr' instr)

295

in

296


297

(* Format.eprintf "translate_eq %a with clock %a@." Printers.pp_node_eq eq

298

Clocks.print_ck eq.eq_rhs.expr_clock; *)

299

match eq.eq_lhs, eq.eq_rhs.expr_desc with

300

 [ x ], Expr_arrow (e1, e2) >

301

let var_x = env.get_var x in

302

let td = Arrow.arrow_top_decl () in

303

let inst = new_instance td eq.eq_rhs.expr_tag in

304

let c1 = translate_expr e1 in

305

let c2 = translate_expr e2 in

306

assert (c1.value_desc = Cst (Const_tag "true"));

307

assert (c2.value_desc = Cst (Const_tag "false"));

308

let ctx =

309

ctl

310

(MStep ([ var_x ], inst, [ c1; c2 ]))

311

(mk_memory_pack ~inst (node_name td))

312

(mk_transition ~inst false (node_name td) [ vdecl_to_val var_x ])

313

{ ctx with j = IMap.add inst (td, []) ctx.j }

314

in

315

{ ctx with si = mkinstr (MSetReset inst) :: ctx.si }

316

 [ x ], Expr_pre e when env.is_local x >

317

let var_x = env.get_var x in

318

let e = translate_expr e in

319

ctl

320

(MStateAssign (var_x, e))

321

(mk_state_variable_pack var_x)

322

(mk_state_assign_tr var_x e)

323

{ ctx with m = ISet.add x ctx.m }

324

 [ x ], Expr_fby (e1, e2) when env.is_local x >

325

let var_x = env.get_var x in

326

let e2 = translate_expr e2 in

327

let ctx =

328

ctl

329

(MStateAssign (var_x, e2))

330

(mk_state_variable_pack var_x)

331

(mk_state_assign_tr var_x e2)

332

{ ctx with m = ISet.add x ctx.m }

333

in

334

{

335

ctx with

336

si = mkinstr' (MStateAssign (var_x, translate_expr e1)) :: ctx.si;

337

}

338

 p, Expr_appl (f, arg, r)

339

when not (Basic_library.is_expr_internal_fun eq.eq_rhs) >

340

let var_p = List.map env.get_var p in

341

let el = expr_list_of_expr arg in

342

let vl = List.map translate_expr el in

343

let node_f = node_from_name f in

344

let call_f = node_f, NodeDep.filter_static_inputs (node_inputs node_f) el in

345

let i = new_instance node_f eq.eq_rhs.expr_tag in

346

let env_cks =

347

List.fold_right

348

(fun arg cks > arg.expr_clock :: cks)

349

el

350

[ eq.eq_rhs.expr_clock ]

351

in

352

let call_ck =

353

Clock_calculus.compute_root_clock (Clock_predef.ck_tuple env_cks)

354

in

355

let r, reset_inst = reset_instance i r call_ck in

356

let stateless = Stateless.check_node node_f in

357

let inst = if stateless then None else Some i in

358

let mp =

359

if stateless then True else mk_memory_pack ?inst (node_name node_f)

360

in

361

let ctx =

362

ctl

363

~ck:call_ck

364

(MStep (var_p, i, vl))

365

mp

366

(mk_transition

367

?r

368

?inst

369

stateless

370

(node_name node_f)

371

(vl @ vdecls_to_vals var_p))

372

{

373

ctx with

374

j = IMap.add i call_f ctx.j;

375

s = (if stateless then [] else reset_inst) @ ctx.s;

376

}

377

in

378

(*Clocks.new_var true in Clock_calculus.unify_imported_clock (Some call_ck)

379

eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc; Format.eprintf "call %a: %a:

380

%a@," Printers.pp_expr eq.eq_rhs Clocks.print_ck (Clock_predef.ck_tuple

381

env_cks) Clocks.print_ck call_ck;*)

382

{

383

ctx with

384

si = (if stateless then ctx.si else mkinstr (MSetReset i) :: ctx.si);

385

}

386

 [ x ], _ > (

387

try

388

let var_x = env.get_var x in

389

let instr, spec = translate_act (var_x, eq.eq_rhs) in

390

control_on_clock eq.eq_rhs.expr_clock instr True spec ctx

391

with Not_found >

392

Format.eprintf "ERROR: node %s, eq %a@." id Printers.pp_node_eq eq;

393

raise Not_found)

394

 _ >

395

Format.eprintf

396

"internal error: Machine_code.translate_eq %a@?"

397

Printers.pp_node_eq

398

eq;

399

assert false

400


401

let constant_equations locals =

402

List.fold_left

403

(fun eqs vdecl >

404

if vdecl.var_dec_const then

405

{

406

eq_lhs = [ vdecl.var_id ];

407

eq_rhs = desome vdecl.var_dec_value;

408

eq_loc = vdecl.var_loc;

409

}

410

:: eqs

411

else eqs)

412

[]

413

locals

414


415

let translate_eqs env ctx nd inputs locals outputs eqs =

416

List.fold_left

417

(fun (ctx, i) eq >

418

let ctx = translate_eq env ctx nd inputs locals outputs i eq in

419

ctx, i + 1)

420

(ctx, 1)

421

eqs

422

> fst

423


424

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

425

(* Processing nodes *)

426

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

427


428

let process_asserts nd =

429

let exprl = List.map (fun assert_ > assert_.assert_expr) nd.node_asserts in

430

if Backends.is_functional () then [], [], exprl

431

else

432

(* Each assert(e) is associated to a fresh variable v and declared as v=e;

433

assert (v); *)

434

let _, vars, eql, assertl =

435

List.fold_left

436

(fun (i, vars, eqlist, assertlist) expr >

437

let loc = expr.expr_loc in

438

let var_id = nd.node_id ^ "_assert_" ^ string_of_int i in

439

let assert_var =

440

mkvar_decl

441

loc

442

~orig:false

443

(* fresh var *)

444

( var_id,

445

mktyp loc Tydec_bool,

446

mkclock loc Ckdec_any,

447

false,

448

(* not a constant *)

449

None,

450

(* no default value *)

451

Some nd.node_id )

452

in

453

assert_var.var_type < Type_predef.type_bool

454

(* Types.new_ty (Types.Tbool) *);

455

let eq = mkeq loc ([ var_id ], expr) in

456

( i + 1,

457

assert_var :: vars,

458

eq :: eqlist,

459

{ expr with expr_desc = Expr_ident var_id } :: assertlist ))

460

(1, [], [], [])

461

exprl

462

in

463

vars, eql, assertl

464


465

let translate_core env nd sorted_eqs inputs locals outputs =

466

let constant_eqs = constant_equations locals in

467


468

(* Compute constants' instructions *)

469

let ctx0 = translate_eqs env ctx_init nd inputs locals outputs constant_eqs in

470

assert (ctx0.si = []);

471

assert (IMap.is_empty ctx0.j);

472


473

(* Compute ctx for all eqs *)

474

let ctx = translate_eqs env ctx_init nd inputs locals outputs sorted_eqs in

475


476

ctx, ctx0.s

477


478

let zero = mk_val (Cst (Const_int 0)) Type_predef.type_int

479


480

let memory_pack_0 nd =

481

{

482

mpname = nd;

483

mpindex = Some 0;

484

mpformula =

485

And [ StateVarPack ResetFlag; Equal (Memory ResetFlag, Val zero) ];

486

}

487


488

let memory_pack_toplevel nd i =

489

{

490

mpname = nd;

491

mpindex = None;

492

mpformula =

493

Ternary

494

(Memory ResetFlag, StateVarPack ResetFlag, mk_memory_pack ~i nd.node_id);

495

}

496


497

let transition_0 nd =

498

{

499

tname = nd;

500

tindex = Some 0;

501

tvars = nd.node_inputs;

502

tformula =

503

(if fst (get_stateless_status_node nd) then True

504

else StateVarPack ResetFlag);

505

tmem_footprint = ISet.empty;

506

tinst_footprint = IMap.empty;

507

}

508


509

let transition_toplevel nd i =

510

let stateless = fst (get_stateless_status_node nd) in

511

let tr =

512

mk_transition

513

stateless

514

nd.node_id

515

~i

516

(vdecls_to_vals (nd.node_inputs @ nd.node_outputs))

517

in

518

{

519

tname = nd;

520

tindex = None;

521

tvars = nd.node_inputs @ nd.node_outputs;

522

tformula =

523

(if fst (get_stateless_status_node nd) then tr

524

else ExistsMem (nd.node_id, Predicate (ResetCleared nd.node_id), tr));

525

tmem_footprint = ISet.empty;

526

tinst_footprint = IMap.empty;

527

}

528


529

let translate_eexpr env e =

530

try

531

List.fold_right

532

(fun (qt, xs) f >

533

match qt with

534

 Lustre_types.Exists >

535

Exists (xs, f)

536

 Lustre_types.Forall >

537

Forall (xs, f))

538

e.eexpr_quantifiers

539

(Value (translate_expr env e.eexpr_qfexpr))

540

with NormalizationError >

541

Format.eprintf "Normalization error: %a@." Printers.pp_eexpr e;

542

raise NormalizationError

543


544

let translate_contract env c =

545

{

546

mc_pre = And (List.map (translate_eexpr env) c.Lustre_types.assume);

547

mc_post = And (List.map (translate_eexpr env) c.Lustre_types.guarantees);

548

mc_proof = c.proof;

549

}

550


551

let translate_spec env = function

552

 Contract c >

553

Contract (translate_contract env c)

554

 NodeSpec s >

555

NodeSpec s

556


557

let translate_decl nd sch =

558

let stateless = fst (get_stateless_status_node nd) in

559

(* Format.eprintf "Translating node %s@." nd.node_id; *)

560

(* Extracting eqs, variables .. *)

561

let eqs, auts = get_node_eqs nd in

562

assert (auts = []);

563


564

(* Automata should be expanded by now *)

565


566

(* In case of non functional backend (eg. C), additional local variables have

567

to be declared for each assert *)

568

let new_locals, assert_instrs, nd_node_asserts = process_asserts nd in

569


570

(* Build the env: variables visible in the current scope *)

571

let locals = nd.node_locals @ new_locals in

572

(* let locals = VSet.of_list locals_list in *)

573

(* let inout_vars = nd.node_inputs @ nd.node_outputs in *)

574

let env = build_env nd.node_inputs locals nd.node_outputs in

575


576

(* Format.eprintf "Node content is %a@." Printers.pp_node nd; *)

577


578

(* Computing main content *)

579

(* Format.eprintf "ok1@.@?"; *)

580

let schedule = sch.Scheduling_type.schedule in

581

(* Format.eprintf "ok2@.@?"; *)

582

let sorted_eqs, unused =

583

Scheduling.sort_equations_from_schedule eqs schedule

584

in

585


586

(* Format.eprintf "ok3@.locals=%a@.inout:%a@?"

587

* VSet.pp locals

588

* VSet.pp inout_vars

589

* ; *)

590

let equations = assert_instrs @ sorted_eqs in

591

let mems = get_memories env equations in

592

(* Removing computed memories from locals. We also removed unused

593

variables. *)

594

let locals =

595

List.filter

596

(fun v > (not (VSet.mem v mems)) && not (List.mem v.var_id unused))

597

locals

598

in

599

(* Compute live sets for spec *)

600

Lustre_live.set_live_of nd.node_id nd.node_outputs locals equations;

601


602

(* Translate equations *)

603

let ctx, ctx0_s =

604

translate_core env nd equations nd.node_inputs locals nd.node_outputs

605

in

606


607

(* Format.eprintf "ok4@.@?"; *)

608


609

(* Build the machine *)

610

let mmap = IMap.bindings ctx.j in

611

let mmemory_packs =

612

memory_pack_0 nd

613

:: List.mapi

614

(fun i f > { mpname = nd; mpindex = Some (i + 1); mpformula = red f })

615

(List.rev ctx.mp)

616

@ [ memory_pack_toplevel nd (List.length ctx.mp) ]

617

in

618

let mtransitions =

619

transition_0 nd

620

:: List.mapi

621

(fun i (tvars, tmem_footprint, tinst_footprint, f) >

622

{

623

tname = nd;

624

tindex = Some (i + 1);

625

tvars;

626

tformula = red f;

627

tmem_footprint;

628

tinst_footprint;

629

})

630

(List.rev ctx.t)

631

@ [ transition_toplevel nd (List.length ctx.t) ]

632

in

633

let clear_reset =

634

mkinstr

635

~instr_spec:

636

((if fst (get_stateless_status_node nd) then []

637

else [ mk_memory_pack ~i:0 nd.node_id ])

638

@ [

639

mk_transition

640

~i:0

641

stateless

642

nd.node_id

643

(vdecls_to_vals nd.node_inputs);

644

])

645

MClearReset

646

in

647

let mnode_spec = Utils.option_map (translate_spec env) nd.node_spec in

648

{

649

mname = nd;

650

mmemory = VSet.elements mems;

651

mcalls = mmap;

652

minstances =

653

List.filter (fun (_, (n, _)) > not (Stateless.check_node n)) mmap;

654

minit = List.rev ctx.si;

655

mconst = List.rev ctx0_s;

656

mstatic = List.filter (fun v > v.var_dec_const) nd.node_inputs;

657

mstep =

658

{

659

step_inputs = nd.node_inputs;

660

step_outputs = nd.node_outputs;

661

step_locals = locals;

662

step_checks =

663

List.map

664

(fun d >

665

d.Dimension.dim_loc, translate_expr env (expr_of_dimension d))

666

nd.node_checks;

667

step_instrs =

668

clear_reset

669

::

670

(* special treatment depending on the active backend. For horn

671

backend, common branches are not merged while they are in C or Java

672

backends. *)

673

(if !Backends.join_guards then join_guards_list (List.rev ctx.s)

674

else List.rev ctx.s);

675

step_asserts = List.map (translate_expr env) nd_node_asserts;

676

};

677

(* Processing spec: there is no processing performed here. Contract have

678

been processed already. Either one of the other machine is a cocospec

679

node, or the current one is a cocospec node. Contract do not contain any

680

statement or import. *)

681

mspec = { mnode_spec; mtransitions; mmemory_packs };

682

mannot = nd.node_annot;

683

msch = Some sch;

684

mis_contract = nd.node_iscontract;

685

}

686


687

(** takes the global declarations and the scheduling associated to each node *)

688

let translate_prog decls node_schs =

689

let nodes = get_nodes decls in

690

let machines =

691

List.map

692

(fun decl >

693

let node = node_of_top decl in

694

let sch = IMap.find node.node_id node_schs in

695

translate_decl node sch)

696

nodes

697

in

698

machines

699


700

(* Local Variables: *)

701

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

702

(* End: *)
