Project

General

Profile

Download (48.9 KB) Statistics
| Branch: | Tag: | Revision:
1
(* This file is part of the Kind 2 model checker.
2

    
3
   Copyright (c) 2015 by the Board of Trustees of the University of Iowa
4

    
5
   Licensed under the Apache License, Version 2.0 (the "License"); you
6
   may not use this file except in compliance with the License.  You
7
   may obtain a copy of the License at
8

    
9
   http://www.apache.org/licenses/LICENSE-2.0 
10

    
11
   Unless required by applicable law or agreed to in writing, software
12
   distributed under the License is distributed on an "AS IS" BASIS,
13
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or
14
   implied. See the License for the specific language governing
15
   permissions and limitations under the License. 
16

    
17
*)
18

    
19
open KindLib
20
module Log = KindLog
21
               
22
module SI = Set.Make (KindIdent)
23

    
24
exception Parser_error
25

    
26

    
27
let error_at_position pos msg =
28
  match Log.get_log_format () with
29
  | Log.F_pt ->
30
    Log.log L_error "Parser error at %a: %s" KindLib.pp_print_position pos msg
31
  | Log.F_xml -> Log.parse_log_xml L_error pos msg
32
  | Log.F_json -> Log.parse_log_json L_error pos msg
33
  | Log.F_relay -> ()
34

    
35

    
36
let warn_at_position pos msg = 
37
  match Log.get_log_format () with
38
  | Log.F_pt ->
39
    Log.log L_warn "Parser warning at %a: %s" KindLib.pp_print_position pos msg
40
  | Log.F_xml -> Log.parse_log_xml L_warn pos msg
41
  | Log.F_json -> Log.parse_log_json L_warn pos msg
42
  | Log.F_relay -> ()
43

    
44

    
45
(* ********************************************************************** *)
46
(* Type declarations                                                      *)
47
(* ********************************************************************** *)
48

    
49

    
50
(* An identifier *)
51
type ident = string
52

    
53
type index = string
54

    
55
let pp_print_ident = Format.pp_print_string
56

    
57
let pp_print_index = Format.pp_print_string
58

    
59

    
60
(* A clock expression *)
61
type clock_expr =
62
  | ClockTrue
63
  | ClockPos of ident
64
  | ClockNeg of ident
65
  | ClockConstr of ident * ident
66

    
67

    
68
(* A Lustre expression *)
69
type expr =
70

    
71
  (* Identifier *)
72
  | Ident of position * ident
73
  | ModeRef of position * ident list
74
  | RecordProject of position * expr * index
75
  | TupleProject of position * expr * expr
76

    
77
  (* Update of an indexed expression *)
78
  | StructUpdate of position * expr * label_or_index list * expr
79

    
80
  (* Values *)
81
  | True of position
82
  | False of position
83
  | Num of position * string
84
  | Dec of position * string
85

    
86
  (* Conversions *)
87
  | ToInt of position * expr
88
  | ToReal of position * expr
89

    
90
  (* List of expressions *)
91
  | ExprList of position * expr list 
92

    
93
  (* Tuple expression *)
94
  | TupleExpr of position * expr list 
95

    
96
  (* Array expression *)
97
  | ArrayExpr of position * expr list 
98

    
99
  (* Array expression *)
100
  | ArrayConstr of position * expr * expr 
101

    
102
  (* Slice of array *)
103
  | ArraySlice of position * expr * (expr * expr) 
104

    
105
  (* Array concatenation *)
106
  | ArrayConcat of position * expr * expr
107

    
108
  (* Record expression *)
109
  | RecordExpr of position * ident * (ident * expr) list
110

    
111
  (* Boolean operators *)
112
  | Not of position * expr 
113
  | And of position * expr * expr 
114
  | Or of position * expr * expr
115
  | Xor of position * expr * expr 
116
  | Impl of position * expr * expr 
117
  | Forall of position * typed_ident list * expr
118
  | Exists of position * typed_ident list * expr
119
  | OneHot of position * expr list
120

    
121
  (* Arithmetic operators *)
122
  | Uminus of position * expr 
123
  | Mod of position * expr * expr
124
  | Minus of position * expr * expr
125
  | Plus of position * expr * expr
126
  | Div of position * expr * expr
127
  | Times of position * expr * expr
128
  | IntDiv of position * expr * expr
129

    
130
  (* If operator *)
131
  | Ite of position * expr * expr * expr 
132

    
133
  (* With operator for recursive definitions *)
134
  | With of position * expr * expr * expr 
135

    
136
  (* Relations *)
137
  | Eq of position * expr * expr 
138
  | Neq of position * expr * expr
139
  | Lte of position * expr * expr
140
  | Lt of position * expr * expr
141
  | Gte of position * expr * expr
142
  | Gt of position * expr * expr
143

    
144
  (* Clock operators *)
145
  | When of position * expr * clock_expr
146
  | Current of position * expr
147
  | Condact of position * expr * expr * ident * expr list * expr list
148
  | Activate of position * ident * expr * expr * expr list
149
  | Merge of position * ident * (ident * expr) list
150
  | RestartEvery of position * ident * expr list * expr
151
      
152
  (* Temporal operators *)
153
  | Pre of position * expr
154
  | Last of position * ident
155
  | Fby of position * expr * int * expr 
156
  | Arrow of position * expr * expr 
157

    
158
  (* A node call *)
159
  | Call of position * ident * expr list 
160

    
161
  (* A node call setting static parameters *)
162
  | CallParam of position * ident * lustre_type list * expr list 
163

    
164

    
165
(* A built-in type *)
166
and lustre_type =
167
  | Bool of position
168
  | Int of position
169
  | IntRange of position * expr * expr
170
  | Real of position
171
  | UserType of position * ident
172
  | TupleType of position * lustre_type list
173
  | RecordType of position * typed_ident list
174
  | ArrayType of position * (lustre_type * expr)
175
  | EnumType of position * ident option * ident list
176

    
177

    
178
(* A declaration of an unclocked type *)
179
and typed_ident = KindLib.position * ident * lustre_type
180

    
181
(* A record field or an array or tuple index *)
182
and label_or_index = 
183
  | Label of KindLib.position * index
184
  | Index of KindLib.position * expr
185

    
186
(* A declaration of a type *)
187
type type_decl = 
188
  | AliasType of position * ident * lustre_type  
189
  | FreeType of position * ident
190

    
191
(* A declaration of a clocked type *)
192
type clocked_typed_decl = 
193
  position * ident * lustre_type * clock_expr
194

    
195

    
196
(* A declaration of a clocked type *)
197
type const_clocked_typed_decl = 
198
  position * ident * lustre_type * clock_expr * bool
199

    
200

    
201
(* A declaration of a constant *)
202
type const_decl = 
203
  | FreeConst of position * ident * lustre_type
204
  | UntypedConst of position * ident * expr 
205
  | TypedConst of position * ident * expr * lustre_type
206

    
207
(*
208
(* A variable declaration *)
209
type var_decl = position * ident * lustre_type * clock_expr
210
*)
211

    
212
(* A static parameter of a node *)
213
type node_param =
214
  | TypeParam of ident
215

    
216

    
217
(* A local declaration in a node *)
218
type node_local_decl =
219
  | NodeConstDecl of position * const_decl 
220
  | NodeVarDecl of position * clocked_typed_decl
221

    
222

    
223
(* Structural assignment in left-hand side of equation *)
224
type struct_item =
225
  | SingleIdent of position * ident
226
  | TupleStructItem of position * struct_item list
227
  | TupleSelection of position * ident * expr
228
  | FieldSelection of position * ident * ident
229
  | ArraySliceStructItem of position * ident * (expr * expr) list
230
  | ArrayDef of position * ident * ident list
231

    
232

    
233
(* The left-hand side of an equation *)
234
type eq_lhs =
235
  | StructDef of position * struct_item list
236

    
237
type transition_to =
238
  | TransRestart of position * (position * ident)
239
  | TransResume of position * (position * ident)
240

    
241
type transition_branch =
242
  | Target of transition_to
243
  | TransIf of position * expr *
244
               transition_branch * transition_branch option
245
  
246
type automaton_transition = position * transition_branch
247

    
248
type auto_returns = Given of ident list | Inferred
249

    
250
(* An equation or assertion in the node body *)
251
type node_equation =
252
  | Assert of position * expr
253
  | Equation of position * eq_lhs * expr 
254
  | Automaton of position * ident option * state list * auto_returns
255

    
256

    
257
and state =
258
  | State of position * ident * bool *
259
             node_local_decl list *
260
             node_equation list *
261
             automaton_transition option *
262
             automaton_transition option
263

    
264

    
265
(* An item in a node declaration *)
266
type node_item =
267
  | Body of node_equation
268
  | AnnotMain of bool
269
  | AnnotProperty of position * string option * expr
270

    
271

    
272
(* A contract ghost constant. *)
273
type contract_ghost_const = const_decl
274

    
275
(* A contract ghost variable. *)
276
type contract_ghost_var = const_decl
277

    
278
(* A contract assume. *)
279
type contract_assume = position * string option * expr
280

    
281
(* A contract guarantee. *)
282
type contract_guarantee = position * string option * expr
283

    
284
(* A contract requirement. *)
285
type contract_require = position * string option * expr
286

    
287
(* A contract ensure. *)
288
type contract_ensure = position * string option * expr
289

    
290
(* A contract mode. *)
291
type contract_mode =
292
  position * ident * (contract_require list) * (contract_ensure list)
293

    
294
(* A contract call. *)
295
type contract_call = position * ident * expr list * expr list
296

    
297
(* Equations that can appear in a contract node. *)
298
type contract_node_equation =
299
  | GhostConst of contract_ghost_const
300
  | GhostVar of contract_ghost_var
301
  | Assume of contract_assume
302
  | Guarantee of contract_guarantee
303
  | Mode of contract_mode
304
  | ContractCall of contract_call
305

    
306
(* A contract is some ghost consts / var, and assumes guarantees and modes. *)
307
type contract = contract_node_equation list
308

    
309

    
310
(* A node or function declaration
311

    
312
Boolean flag indicates whether node / function is extern. *)
313
type node_decl =
314
  ident
315
  * bool
316
  * node_param list
317
  * const_clocked_typed_decl list
318
  * clocked_typed_decl list
319
  * node_local_decl list
320
  * node_item list
321
  * contract option
322

    
323
(* A contract node declaration. Almost the same as a [node_decl] but
324
   with a different type for equations, and no contract
325
   specification. *)
326
type contract_node_decl =
327
  ident
328
  * node_param list
329
  * const_clocked_typed_decl list
330
  * clocked_typed_decl list
331
  * contract
332

    
333

    
334
(* An instance of a parameterized node *)
335
type node_param_inst = ident * ident * lustre_type list
336
  
337
(* A declaration as parsed *)
338
type declaration = 
339
  | TypeDecl of position * type_decl
340
  | ConstDecl of position * const_decl
341
  | NodeDecl of position * node_decl
342
  | FuncDecl of position * node_decl
343
  | ContractNodeDecl of position * contract_node_decl
344
  | NodeParamInst of position * node_param_inst
345

    
346

    
347
(* A Lustre program *)
348
type t = declaration list
349

    
350

    
351
(* ********************************************************************** *)
352
(* Pretty-printing functions                                              *)
353
(* ********************************************************************** *)
354

    
355

    
356
(* Pretty-print a clock expression *)
357
let pp_print_clock_expr ppf = function
358
  | ClockTrue -> ()
359
  | ClockPos s -> Format.fprintf ppf "@ when %a" pp_print_ident s
360
  | ClockNeg s -> Format.fprintf ppf "@ when not %a" pp_print_ident s
361
  | ClockConstr (s, c) ->
362
    Format.fprintf ppf "@ when %a(%a)" pp_print_ident c pp_print_ident s
363

    
364

    
365
(* Pretty-print a Lustre expression *)
366
let rec pp_print_expr ppf = 
367

    
368
  let ppos ppf p =
369
    (if false then Format.fprintf else Format.ifprintf)
370
      ppf
371
      "%a" 
372
      pp_print_position p
373
  in
374

    
375
  (* Pretty-print a string *)
376
  let ps p = Format.fprintf ppf "%a%s" ppos p in 
377

    
378
  (* Pretty-print a unary operator *)
379
  let p1 p s e = 
380
    Format.fprintf ppf "@[<hv 2>%a(%s %a)@]" 
381
      ppos p 
382
      s 
383
      pp_print_expr e 
384
  in 
385

    
386
  (* Pretty-print a binary infix operator *)
387
  let p2 p s e1 e2 = 
388
    Format.fprintf ppf
389
      "@[<hv 2>%a(%a %s@ %a)@]" 
390
      ppos p 
391
      pp_print_expr e1 
392
      s 
393
      pp_print_expr e2 
394
  in 
395

    
396
  (* Pretty-print a ternary infix operator *)
397
  let p3 p s1 s2 s3 e1 e2 e3 = 
398
    Format.fprintf ppf
399
      "@[<hv 2>%a(%s@ %a@;<1 -1>%s@ %a@;<1 -1>%s@ %a)@]" 
400
      ppos p 
401
      s1 
402
      pp_print_expr e1 
403
      s2
404
      pp_print_expr e2 
405
      s3 
406
      pp_print_expr e3 
407
  in 
408
  
409
  (* Pretty-print a comma-separated list of expressions *)
410
  let rec pl ppf = function 
411
    | [] -> ()
412
    | [e] -> Format.fprintf ppf "%a" pp_print_expr e
413
    | e :: tl -> Format.fprintf ppf "%a,@ %a" pl [e] pl tl
414
  in
415

    
416
  (* Pretty-print a variadic prefix operator *)
417
  let pnp p s l = 
418
    Format.fprintf ppf
419
      "@[<hv 2>%a%s@,@[<hv 1>(%a)@]@]" 
420
      ppos p 
421
      s
422
      pl l
423
  in
424

    
425
  function
426
    
427
    | Ident (p, id) -> Format.fprintf ppf "%a%a" ppos p pp_print_ident id
428

    
429
    | ModeRef (p, ids) ->
430
      Format.fprintf ppf "%a::%a" ppos p (
431
        pp_print_list pp_print_ident "::"
432
      ) ids
433
 
434
    | ExprList (p, l) -> Format.fprintf ppf "%a@[<hv 1>(%a)@]" ppos p pl l
435

    
436
    | TupleExpr (p, l) -> Format.fprintf ppf "%a@[<hv 1>{%a}@]" ppos p pl l
437

    
438
    | ArrayExpr (p, l) -> Format.fprintf ppf "%a@[<hv 1>[%a]@]" ppos p pl l
439

    
440
    | StructUpdate (p, e1, i, e2) -> 
441

    
442
      Format.fprintf ppf
443
        "@[<hv 1>(%a@ with@ @[<hv>%a@] =@ %a)@]"
444
        pp_print_expr e1
445
        (pp_print_list pp_print_label_or_index "") i
446
        pp_print_expr e2
447

    
448

    
449
    | ArrayConstr (p, e1, e2) -> 
450

    
451
      Format.fprintf ppf 
452
        "%a@[<hv 1>(%a^%a)@]" 
453
        ppos p 
454
        pp_print_expr e1 
455
        pp_print_expr e2
456

    
457
    | ArraySlice (p, e, l) -> 
458

    
459
      Format.fprintf ppf 
460
        "%a@[<hv 1>%a@[<hv 1>[%a]@]@]" 
461
        ppos p 
462
        pp_print_expr e
463
        pp_print_array_slice l 
464

    
465
    | ArrayConcat (p, e1, e2) -> 
466

    
467
      Format.fprintf ppf 
468
        "%a@[<hv 1>%a|%a@]" 
469
        ppos p 
470
        pp_print_expr e1
471
        pp_print_expr e2 
472

    
473
    | RecordProject (p, e, f) -> 
474

    
475
      Format.fprintf ppf 
476
        "%a%a.%a" 
477
        ppos p 
478
        pp_print_expr e 
479
        pp_print_index f
480

    
481
    | RecordExpr (p, t, l) -> 
482

    
483
      Format.fprintf ppf 
484
        "%a@[<hv 1>%a {%a}@]" 
485
        ppos p 
486
        pp_print_ident t
487
        (pp_print_list pp_print_field_assign ";@ ") l
488

    
489
    | TupleProject (p, e, f) -> 
490

    
491
      Format.fprintf ppf "%a%a.%%%a" ppos p pp_print_expr e pp_print_expr f
492

    
493
    | True p -> ps p "true"
494
    | False p -> ps p "false"
495

    
496
    | Num (p, n) -> ps p n
497
    | Dec (p, d) -> ps p d
498

    
499
    | ToInt (p, e) -> p1 p "int" e
500
    | ToReal (p, e) -> p1 p "real" e
501

    
502
    | Not (p, e) -> p1 p "not" e
503
    | And (p, e1, e2) -> p2 p "and" e1 e2
504
    | Or (p, e1, e2) -> p2 p "or" e1 e2
505
    | Xor (p, e1, e2) -> p2 p "xor" e1 e2
506
    | Impl (p, e1, e2) -> p2 p "=>" e1 e2
507
    | OneHot (p, e) -> pnp p "#" e
508
    | Forall (pos, vars, e) -> 
509
      Format.fprintf ppf "@[<hv 2>forall@ @[<hv 1>(%a)@]@ %a@]" 
510
        (pp_print_list pp_print_typed_decl ";@ ") vars
511
        pp_print_expr e
512
    | Exists (pos, vars, e) -> 
513
      Format.fprintf ppf "@[<hv 2>exists@ @[<hv 1>(%a)@]@ %a@]" 
514
        (pp_print_list pp_print_typed_decl ";@ ") vars
515
        pp_print_expr e
516

    
517
    | Uminus (p, e) -> p1 p "-" e
518
    | Mod (p, e1, e2) -> p2 p "mod" e1 e2 
519
    | Minus (p, e1, e2) -> p2 p "-" e1 e2
520
    | Plus (p, e1, e2) -> p2 p "+" e1 e2
521
    | Div (p, e1, e2) -> p2 p "/" e1 e2
522
    | Times (p, e1, e2) -> p2 p "*" e1 e2
523
    | IntDiv (p, e1, e2) -> p2 p "div" e1 e2
524

    
525
    | Ite (p, e1, e2, e3) -> p3 p "if" "then" "else" e1 e2 e3
526

    
527
    | With (p, e1, e2, e3) -> p3 p "with" "then" "else" e1 e2 e3
528

    
529
    | Eq (p, e1, e2) -> p2 p "=" e1 e2
530
    | Neq (p, e1, e2) -> p2 p "<>" e1 e2
531
    | Lte (p, e1, e2) -> p2 p "<=" e1 e2
532
    | Lt (p, e1, e2) -> p2 p "<" e1 e2
533
    | Gte (p, e1, e2) -> p2 p ">=" e1 e2
534
    | Gt (p, e1, e2) -> p2 p ">" e1 e2
535

    
536
    | When (p, e1, e2) ->
537
      Format.fprintf ppf "%a %a when %a"
538
        ppos p
539
        pp_print_expr e1
540
        pp_print_clock_expr e2
541

    
542
    | Current (p, e) -> p1 p "current" e
543
    | Condact (p, e1, er, n, e2, e3) -> 
544
  
545
      Format.fprintf ppf 
546
        "%acondact(%a,restart %a,%a(%a),%a)" 
547
        ppos p
548
        pp_print_expr e1
549
        pp_print_expr er
550
        pp_print_ident n
551
        (pp_print_list pp_print_expr ",@ ") e2
552
        (pp_print_list pp_print_expr ",@ ") e3
553

    
554
    | Activate (p, i, c, r, l) ->
555

    
556
      Format.fprintf ppf
557
        "(activate (restart %a every %a) every %a) (%a)"
558
        pp_print_ident i
559
        pp_print_expr r
560
        pp_print_expr c
561
        (pp_print_list pp_print_expr ",@ ") l 
562
        
563
    | Merge (p, c, l) ->
564

    
565
      Format.fprintf ppf
566
        "merge(%a,@ %a)"
567
        pp_print_ident c
568
        (pp_print_list (fun fmt (c,e) ->
569
             Format.fprintf fmt "%a -> %a"
570
               pp_print_ident c
571
               pp_print_expr e) ",@ ") l 
572

    
573
    | RestartEvery (p, i, l, c) ->
574
      Format.fprintf ppf
575
        "(restart %a every %a)(%a)"
576
        pp_print_ident i
577
        pp_print_expr c
578
        (pp_print_list pp_print_expr ",@ ") l 
579

    
580
    | Pre (p, e) -> p1 p "pre" e
581
    | Last (p, id) ->
582
      Format.fprintf ppf "last %a%a" ppos p pp_print_ident id
583
    | Fby (p, e1, i, e2) -> 
584

    
585
      Format.fprintf ppf 
586
        "%afby(p, %a,@ %d,@ %a)" 
587
        ppos p 
588
        pp_print_expr e1 
589
        i 
590
        pp_print_expr e2
591

    
592
    | Arrow (p, e1, e2) -> p2 p "->" e1 e2
593

    
594
    | Call (p, id, l) ->
595

    
596
      Format.fprintf ppf 
597
        "%a%a(%a)" 
598
        ppos p
599
        pp_print_ident id
600
        (pp_print_list pp_print_expr ",@ ") l
601

    
602
    | CallParam (p, id, t, l) -> 
603

    
604
      Format.fprintf ppf 
605
        "%a%a<<%a>>(%a)" 
606
        ppos p
607
        pp_print_ident id
608
        (pp_print_list pp_print_lustre_type "@ ") t
609
        (pp_print_list pp_print_expr ",@ ") l
610
        
611

    
612
(* Pretty-print an array slice *)
613
and pp_print_array_slice ppf (l, u) =
614
  if l = u then
615
    Format.fprintf ppf "%a" pp_print_expr l
616
  else
617
    Format.fprintf ppf "%a..%a" pp_print_expr l pp_print_expr u
618

    
619
and pp_print_field_assign ppf (i, e) = 
620

    
621
  Format.fprintf ppf 
622
    "@[<hv 2>%a =@ %a@]"
623
    pp_print_index i
624
    pp_print_expr e
625

    
626

    
627
(* Pretty-print a Lustre type *)
628
and pp_print_lustre_type ppf = function
629

    
630
  | Bool pos -> Format.fprintf ppf "bool"
631

    
632
  | Int pos -> Format.fprintf ppf "int"
633

    
634
  | IntRange (pos, l, u) -> 
635

    
636
    Format.fprintf ppf 
637
      "subrange [%a,%a] of int" 
638
      pp_print_expr l
639
      pp_print_expr u
640

    
641
  | Real pos -> Format.fprintf ppf "real"
642

    
643
  | UserType (pos, s) -> 
644

    
645
    Format.fprintf ppf "%a" pp_print_ident s
646

    
647
  | TupleType (pos, l) -> 
648

    
649
    Format.fprintf ppf 
650
      "@[<hv 1>[%a]@]" 
651
      (pp_print_list pp_print_lustre_type ",@ ") l
652

    
653
  | RecordType (pos, l) -> 
654

    
655
    Format.fprintf ppf 
656
      "struct @[<hv 2>{ %a }@]" 
657
      (pp_print_list pp_print_typed_ident ";@ ") l
658

    
659
  | ArrayType (pos, (t, e)) -> 
660

    
661
    Format.fprintf ppf 
662
      "(%a^%a)" 
663
      pp_print_lustre_type t 
664
      pp_print_expr e
665

    
666
  | EnumType (pos, _, l) -> 
667

    
668
    Format.fprintf ppf 
669
      "enum @[<hv 2>{ %a }@]" 
670
      (pp_print_list Format.pp_print_string ",@ ") l
671

    
672

    
673
(* Pretty-print a typed identifier *)
674
and pp_print_typed_ident ppf (p, s, t) = 
675
  Format.fprintf ppf 
676
    "@[<hov 2>%s:@ %a@]" 
677
    s 
678
    pp_print_lustre_type t
679

    
680

    
681
(* Pretty-print a typed identifier *)
682
and pp_print_typed_decl ppf (p, s, t) = 
683
  Format.fprintf ppf 
684
    "@[<hov 2>%s:@ %a@]" 
685
    s 
686
    pp_print_lustre_type t
687

    
688

    
689
(* Pretty-print a typed identifier with a clock *)
690
and pp_print_clocked_typed_ident ppf (pos, s, t, c) = 
691
  Format.fprintf ppf 
692
    "@[<hov 2>%a:@ %a%a@]" 
693
    pp_print_ident s 
694
    pp_print_lustre_type t 
695
    pp_print_clock_expr c
696

    
697

    
698
(* Pretty-print a typed identifier with a clock, possibly constant *)
699
and pp_print_const_clocked_typed_ident ppf (pos, s, t, c, o) = 
700
  Format.fprintf ppf "@[<hov 2>%t%a:@ %a%a@]" 
701
    (function ppf -> if o then Format.fprintf ppf "const ")
702
    pp_print_ident s 
703
    pp_print_lustre_type t 
704
    pp_print_clock_expr c
705

    
706

    
707
and pp_print_label_or_index ppf = function 
708

    
709
  | Label (pos, i) -> pp_print_index ppf i
710
  | Index (pos, e) -> pp_print_expr ppf e
711

    
712
(* Pretty-print a type declaration *)
713
let pp_print_type_decl ppf = function
714

    
715
  | AliasType (pos, s, t) -> 
716
    
717
    Format.fprintf ppf 
718
      "@[<hv 2>%a =@ %a@]" 
719
      pp_print_ident s 
720
      pp_print_lustre_type t
721

    
722
  | FreeType (pos, t) -> 
723

    
724
    Format.fprintf ppf "%a" pp_print_ident t 
725

    
726

    
727
(* Pretty-print a variable declaration *)
728
let pp_print_var_decl ppf = function 
729

    
730
  | (pos, s, t, c) -> 
731

    
732
    Format.fprintf ppf 
733
      "@[<hov 2>%a:@ %a%a;@]" 
734
      pp_print_ident s 
735
      pp_print_lustre_type t
736
      pp_print_clock_expr c
737

    
738

    
739
(* Pretty-print a constant declaration *)
740
let pp_print_const_decl ppf = function
741

    
742
  | FreeConst (pos, s, t) -> 
743

    
744
    Format.fprintf ppf 
745
      "@[<hov 2>const %a:@ %a;@]" 
746
      pp_print_ident s 
747
      pp_print_lustre_type t
748

    
749
  | UntypedConst (pos, s, e) -> 
750

    
751
    Format.fprintf ppf 
752
      "@[<hov 2>const %a =@ %a;@]" 
753
      pp_print_ident s 
754
      pp_print_expr e
755

    
756
  | TypedConst (pos, s, e, t) -> 
757

    
758
    Format.fprintf ppf 
759
      "@[<hov 2>const %a:@ %a =@ %a;@]" 
760
      pp_print_ident s 
761
      pp_print_lustre_type t
762
      pp_print_expr e
763

    
764

    
765
(* Pretty-print a single static node parameter *)
766
let pp_print_node_param ppf = function
767

    
768
  | TypeParam t ->
769
    Format.fprintf ppf "type %a" pp_print_ident t
770

    
771

    
772
(* Pretty-print a list of static node parameters *)
773
let pp_print_node_param_list ppf = function
774

    
775
  | [] -> ()
776

    
777
  | l ->
778
    
779
    Format.fprintf ppf
780
      "@[<hv 2><<%a>>@]"
781
      (pp_print_list pp_print_node_param ";@ ") l
782

    
783

    
784
(* Pretty-print a node-local variable declaration, skip others *)
785
let pp_print_node_local_decl_var ppf = function
786

    
787
  | NodeVarDecl (pos, v) -> pp_print_var_decl ppf v
788

    
789
  | _ -> ()
790

    
791

    
792
(* Pretty-print a node-local constant declaration, skip others *)
793
let pp_print_node_local_decl_const ppf = function
794

    
795
  | NodeConstDecl (pos, c) -> pp_print_const_decl ppf c
796

    
797
  | _ -> ()
798

    
799

    
800
(* Pretty-print a node-local declaration *)
801
let pp_print_node_local_decl ppf l = 
802

    
803
  let c, v = 
804
    List.partition (function NodeConstDecl _ -> true | _ -> false) l 
805
  in
806

    
807
  if c = [] then () else 
808

    
809
    Format.fprintf ppf 
810
      "%a@ " 
811
      (pp_print_list pp_print_node_local_decl_const "@;<1 -2>") c;
812

    
813
  if v = [] then () else 
814

    
815
    Format.fprintf ppf
816
      "@[<hv 2>var@ %a@]@ "
817
      (pp_print_list pp_print_node_local_decl_var "@ ") v 
818

    
819

    
820
let pp_print_array_def_index ppf ident =
821

    
822
  Format.fprintf ppf
823
    "[%a]"
824
    pp_print_ident ident
825

    
826

    
827
let rec pp_print_struct_item ppf = function
828

    
829
  | SingleIdent (pos, s) -> Format.fprintf ppf "%a" pp_print_ident s
830

    
831
  | TupleStructItem (pos, l) -> 
832

    
833
    Format.fprintf ppf 
834
      "@[<hv 1>[%a]@]" 
835
      (pp_print_list pp_print_struct_item ",@ ") l
836

    
837
  | TupleSelection (pos, e, i) -> 
838

    
839
    Format.fprintf ppf
840
      "%a[%a]"
841
      pp_print_ident e
842
      pp_print_expr i
843

    
844
  | FieldSelection (pos, e, i) -> 
845

    
846
    Format.fprintf ppf
847
      "%a.%a"
848
      pp_print_ident e
849
      pp_print_ident i
850

    
851
  | ArraySliceStructItem (pos, e, i) -> 
852

    
853
    Format.fprintf ppf
854
      "%a@[<hv 1>[%a]@]" 
855
      pp_print_ident e
856
      (pp_print_list pp_print_array_slice ",@ ") i
857
                            
858
  | ArrayDef (pos, i, l) ->
859

    
860
    Format.fprintf ppf
861
      "%a%a"
862
      pp_print_ident i
863
      (pp_print_list pp_print_array_def_index "") l
864

    
865

    
866
let pp_print_eq_lhs ppf = function
867

    
868
  | StructDef (pos, [l]) ->
869
    pp_print_struct_item ppf l
870
      
871
  | StructDef (pos, l) ->
872
    Format.fprintf ppf "(%a)"
873
      (pp_print_list pp_print_struct_item ",") l
874
  
875

    
876
let rec pp_print_body ppf = function
877

    
878
  | Assert (pos, e) -> 
879

    
880
    Format.fprintf ppf "assert %a;" pp_print_expr e
881

    
882
  | Equation (pos, lhs, e) -> 
883
    
884
    Format.fprintf ppf 
885
      "@[<hv 2>%a =@ %a;@]" 
886
      pp_print_eq_lhs lhs
887
      pp_print_expr e
888

    
889
  | Automaton (_, name, states, returns) ->
890
    pp_print_automaton ppf name states returns
891

    
892

    
893
(* Pretty-print a node equation *)
894
and pp_print_node_item ppf = function
895
  
896
  | Body b -> pp_print_body ppf b
897

    
898
  | AnnotMain true -> Format.fprintf ppf "--%%MAIN;"
899

    
900
  | AnnotMain false -> Format.fprintf ppf "--!MAIN : false;"
901

    
902
  | AnnotProperty (pos, None, e) ->
903
    Format.fprintf ppf "--%%PROPERTY %a;" pp_print_expr e 
904

    
905
  | AnnotProperty (pos, Some name, e) ->
906
    Format.fprintf ppf "--%%PROPERTY \"%s\" %a;" name pp_print_expr e 
907

    
908

    
909
and pp_print_automaton ppf name states returns =
910
  Format.fprintf ppf "@[<hv 2>automaton %s@.%a@]returns %a;"
911
    (match name with Some n -> n | None -> "")
912
    pp_print_states states
913
    pp_print_auto_returns returns
914

    
915

    
916
and pp_print_auto_returns ppf = function
917
  | Given l -> pp_print_list pp_print_ident "," ppf l
918
  | Inferred -> Format.fprintf ppf ".."
919

    
920
and pp_print_states ppf =
921
  pp_print_list pp_print_state "@." ppf
922

    
923

    
924
and pp_print_state ppf =
925
  function State (_, name, init, locals, eqs, unless, until) ->
926
    Format.fprintf ppf "state %s@.@[<hv 2>%a%a@[<hv 2>let@.%a@]@.tel@]@.%a" name
927
      (pp_print_auto_trans "unless") unless
928
      pp_print_node_local_decl locals
929
      (pp_print_list pp_print_body "@ ") eqs
930
      (pp_print_auto_trans "until") until
931

    
932
and pp_print_auto_trans kind ppf = function
933
  | None -> ()
934
  | Some (_, br) ->
935
    Format.fprintf ppf "%s %a;@." kind pp_print_transition_branch br
936

    
937
and pp_print_transition_branch ppf = function
938
  | Target (TransRestart (_, (_, t))) -> Format.fprintf ppf "restart %s" t
939
  | Target (TransResume (_, (_, t))) -> Format.fprintf ppf "resume %s" t
940
  | TransIf (_, e, br, None) ->
941
    Format.fprintf ppf "if@ %a@ %a"
942
      pp_print_expr e
943
      pp_print_transition_branch br
944
  | TransIf (_, e, br, Some br2) ->
945
    Format.fprintf ppf "if@ %a@ %a@ else@ %a@ end"
946
      pp_print_expr e
947
      pp_print_transition_branch br
948
      pp_print_transition_branch br2
949

    
950

    
951
let pp_print_contract_ghost_const ppf = function 
952

    
953
  | FreeConst (pos, s, t) -> 
954

    
955
    Format.fprintf ppf 
956
      "@[<hv 3>const %a:@ %a;@]" 
957
      pp_print_ident s 
958
      pp_print_lustre_type t
959

    
960
  | UntypedConst (pos, s, e) -> 
961

    
962
    Format.fprintf ppf 
963
      "@[<hv 3>const %a =@ %a;@]" 
964
      pp_print_ident s 
965
      pp_print_expr e
966

    
967
  | TypedConst (pos, s, e, t) -> 
968

    
969
    Format.fprintf ppf 
970
      "@[<hv 3>const %a:@ %a =@ %a;@]" 
971
      pp_print_ident s 
972
      pp_print_lustre_type t
973
      pp_print_expr e
974

    
975
    
976
let pp_print_contract_ghost_var ppf = function 
977

    
978
  | FreeConst (pos, s, t) -> 
979

    
980
    Format.fprintf ppf 
981
      "@[<hv 3>var %a:@ %a;@]" 
982
      pp_print_ident s 
983
      pp_print_lustre_type t
984

    
985
  | UntypedConst (pos, s, e) -> 
986

    
987
    Format.fprintf ppf 
988
      "@[<hv 3>var %a =@ %a;@]" 
989
      pp_print_ident s 
990
      pp_print_expr e
991

    
992
  | TypedConst (pos, s, e, t) -> 
993

    
994
    Format.fprintf ppf 
995
      "@[<hv 3>var %a:@ %a =@ %a;@]" 
996
      pp_print_ident s 
997
      pp_print_lustre_type t
998
      pp_print_expr e
999

    
1000
    
1001
let pp_print_contract_assume ppf (_, n, e) =
1002
  Format.fprintf
1003
    ppf
1004
    "@[<hv 3>assume%s@ %a;@]"
1005
    (match n with None -> "" | Some s -> " \""^s^"\"")
1006
    pp_print_expr e
1007

    
1008
let pp_print_contract_guarantee ppf (_, n, e) =
1009
  Format.fprintf
1010
    ppf
1011
    "@[<hv 3>guarantee%s@ %a;@]"
1012
    (match n with None -> "" | Some s -> " \""^s^"\"")
1013
    pp_print_expr e
1014

    
1015
    
1016
let pp_print_contract_require ppf (_, n, e) =
1017
  Format.fprintf
1018
    ppf
1019
    "@[<hv 3>require%s@ %a;@]"
1020
    (match n with None -> "" | Some s -> " \""^s^"\"")
1021
    pp_print_expr e
1022

    
1023
let pp_print_contract_ensure ppf (_, n, e) =
1024
  Format.fprintf
1025
    ppf
1026
    "@[<hv 3>ensure%s@ %a;@]"
1027
    (match n with None -> "" | Some s -> " \""^s^"\"")
1028
    pp_print_expr e
1029

    
1030
let cond_new_line b fmt () =
1031
  if b then Format.fprintf fmt "@ " else Format.fprintf fmt ""
1032

    
1033
let pp_print_contract_mode ppf (_, id, reqs, enss) =
1034
  Format.fprintf
1035
    ppf
1036
    "@[<hv 2>mode %a (%a%a%a%a@]%a) ;"
1037
    pp_print_ident id
1038
    (cond_new_line (reqs <> [])) ()
1039
    (pp_print_list pp_print_contract_require "@ ") reqs
1040
    (cond_new_line (enss <> [])) ()
1041
    (pp_print_list pp_print_contract_ensure "@ ") enss
1042
    (cond_new_line ((reqs,enss) <> ([],[]))) ()
1043

    
1044
let pp_print_contract_call fmt (_, id, in_params, out_params) =
1045
  Format.fprintf
1046
    fmt "@[<hov 2>import %a (@,%a@,) (@,%a@,) ;@]"
1047
    pp_print_ident id
1048
    (pp_print_list pp_print_expr ", ") in_params
1049
    (pp_print_list pp_print_expr ", ") out_params
1050

    
1051
let all_empty = List.for_all (fun l -> l = [])
1052

    
1053
let pp_print_contract_item fmt = function
1054
  | GhostConst c -> pp_print_contract_ghost_const fmt c
1055
  | GhostVar v -> pp_print_contract_ghost_var fmt v
1056
  | Assume a -> pp_print_contract_assume fmt a
1057
  | Guarantee g -> pp_print_contract_guarantee fmt g
1058
  | Mode m -> pp_print_contract_mode fmt m
1059
  | ContractCall call -> pp_print_contract_call fmt call
1060

    
1061

    
1062
let pp_print_contract fmt contract =
1063
  Format.fprintf fmt "@[<v>%a@]"
1064
    (pp_print_list pp_print_contract_item "@ ") contract
1065

    
1066

    
1067
let pp_print_contract_spec ppf = function
1068
| None -> ()
1069
| Some contract ->
1070
  Format.fprintf 
1071
    ppf
1072
    "@[<v 2>(*@contract@ %a@]@ *)@ "
1073
    pp_print_contract contract
1074

    
1075

    
1076
(* Pretty-prints a contract node. *)
1077
let pp_print_contract_node ppf (
1078
  id, _, i, o, contract
1079
) =
1080
  Format.fprintf ppf "@[<v>\
1081
      contract %s (@   \
1082
        @[<v>%a@]@ \
1083
      ) returns (@   \
1084
        @[<v>%a@]@ \
1085
      ) ;@ \
1086
      spec@   \
1087
        %a@ \
1088
      ceps\
1089
      @]
1090
    @]"
1091
    id
1092
    (pp_print_list pp_print_const_clocked_typed_ident ";@ ") i
1093
    (pp_print_list pp_print_clocked_typed_ident ";@ ") o
1094
    pp_print_contract contract 
1095

    
1096

    
1097
let pp_print_node_or_fun_decl is_fun ppf (
1098
  pos, (n, ext, p, i, o, l, e, r)
1099
) =
1100

    
1101
    Format.fprintf ppf
1102
      "@[<hv>@[<hv 2>%s%s %a%t@ \
1103
       @[<hv 1>(%a)@]@;<1 -2>\
1104
       returns@ @[<hv 1>(%a)@];@]@ \
1105
       %a@ \
1106
       %a@ \
1107
       @[<v 2>let@ \
1108
       %a@;<1 -2>\
1109
       tel;@]@]"
1110
      (if ext then "extern " else "")
1111
      (if is_fun then "function" else "node")
1112
      pp_print_ident n 
1113
      (function ppf -> pp_print_node_param_list ppf p)
1114
      (pp_print_list pp_print_const_clocked_typed_ident ";@ ") i
1115
      (pp_print_list pp_print_clocked_typed_ident ";@ ") o
1116
      pp_print_contract_spec
1117
      r
1118
      pp_print_node_local_decl l
1119
      (pp_print_list pp_print_node_item "@ ") e
1120

    
1121

    
1122
(* Pretty-print a declaration *)
1123
let pp_print_declaration ppf = function
1124

    
1125
  | TypeDecl (pos, t) -> 
1126

    
1127
    Format.fprintf ppf "type %a;" pp_print_type_decl t
1128

    
1129
  | ConstDecl (pos, c) -> pp_print_const_decl ppf c
1130

    
1131
  | NodeDecl (pos, decl) ->
1132
    pp_print_node_or_fun_decl false ppf (pos, decl)
1133

    
1134
  | FuncDecl (pos, decl) ->
1135
    pp_print_node_or_fun_decl true ppf (pos, decl)
1136

    
1137
  | ContractNodeDecl (pos, (n,p,i,o,e)) ->
1138

    
1139
     Format.fprintf
1140
       ppf
1141
       "@[<hv>@[<hv 2>contract %a%t@ \
1142
        @[<hv 1>(%a)@]@;<1 -2>\
1143
        returns@ @[<hv 1>(%a)@];@]@ \
1144
        @[<hv 2>let@ \
1145
        %a@;<1 -2>\
1146
        tel;@]@]"
1147
       pp_print_ident n
1148
       (function ppf -> pp_print_node_param_list ppf p)
1149
       (pp_print_list pp_print_const_clocked_typed_ident ";@ ") i
1150
       (pp_print_list pp_print_clocked_typed_ident ";@ ") o
1151
       pp_print_contract e
1152

    
1153
  | NodeParamInst (pos, (n, s, p)) -> 
1154

    
1155
    Format.fprintf ppf
1156
      "@[<hv>@[<hv 2>node %a =@ %a@[<hv 2><<%a>>@];@]" 
1157
      pp_print_ident n 
1158
      pp_print_ident n 
1159
      (pp_print_list pp_print_lustre_type "@ ") p
1160

    
1161

    
1162
let pp_print_program ppf p =
1163

    
1164
  Format.fprintf ppf
1165
    "@[<v>%a@]" 
1166
    (pp_print_list pp_print_declaration "@ ") 
1167
    p
1168

    
1169

    
1170

    
1171

    
1172
(***********)
1173
(* Helpers *)
1174
(***********)
1175

    
1176
let pos_of_expr = function
1177
  | Ident (pos , _) | ModeRef (pos , _ ) | RecordProject (pos , _ , _)
1178
  | TupleProject (pos , _ , _) | StructUpdate (pos , _ , _ , _) | True pos
1179
  | False pos | Num (pos , _) | Dec (pos , _) | ToInt (pos , _)
1180
  | ToReal (pos , _) | ExprList (pos , _ ) | TupleExpr (pos , _ )
1181
  | ArrayExpr (pos , _ ) | ArrayConstr (pos , _ , _ )
1182
  | ArraySlice (pos , _ , _) | ArrayConcat (pos , _ , _)
1183
  | RecordExpr (pos , _ , _) | Not (pos , _) | And (pos , _ , _)
1184
  | Or (pos , _ , _) | Xor (pos , _ , _) | Impl (pos , _ , _)
1185
  | OneHot (pos , _ ) | Uminus (pos , _) | Mod (pos , _ , _)
1186
  | Minus (pos , _ , _) | Plus (pos , _ , _) | Div (pos , _ , _)
1187
  | Times (pos , _ , _) | IntDiv (pos , _ , _) | Ite (pos , _ , _ , _)
1188
  | With (pos , _ , _ , _) | Eq (pos , _ , _) | Neq (pos , _ , _)
1189
  | Lte (pos , _ , _) | Lt (pos , _ , _) | Gte (pos , _ , _) | Gt (pos , _ , _)
1190
  | Forall (pos, _, _) | Exists (pos, _, _)
1191
  | When (pos , _ , _) | Current (pos , _) | Condact (pos , _ , _ , _ , _, _)
1192
  | Activate (pos , _ , _ , _ , _) | Merge (pos , _ , _ ) | Pre (pos , _)
1193
  | Last (pos , _) | RestartEvery (pos, _, _, _)
1194
  | Fby (pos , _ , _ , _) | Arrow (pos , _ , _) | Call (pos , _ , _ )
1195
  | CallParam (pos , _ , _ , _ )
1196
    -> pos
1197

    
1198

    
1199
let rec has_unguarded_pre ung = function
1200
  | True _ | False _ | Num _ | Dec _ | Ident _ | ModeRef _ -> false
1201
    
1202
  | RecordProject (_, e, _) | ToInt (_, e) | ToReal (_, e)
1203
  | Not (_, e) | Uminus (_, e) | Current (_, e) | When (_, e, _)
1204
  | Forall (_, _, e) | Exists (_, _, e) -> has_unguarded_pre ung e
1205

    
1206
  | TupleProject (_, e1, e2) | And (_, e1, e2) | Or (_, e1, e2)
1207
  | Xor (_, e1, e2) | Impl (_, e1, e2) | ArrayConstr (_, e1, e2) 
1208
  | Mod (_, e1, e2) | Minus (_, e1, e2) | Plus (_, e1, e2) | Div (_, e1, e2)
1209
  | Times (_, e1, e2) | IntDiv (_, e1, e2) | Eq (_, e1, e2) | Neq (_, e1, e2)
1210
  | Lte (_, e1, e2) | Lt (_, e1, e2) | Gte (_, e1, e2) | Gt (_, e1, e2)
1211
  | ArrayConcat (_, e1, e2) ->
1212
    let u1 = has_unguarded_pre ung e1 in
1213
    let u2 = has_unguarded_pre ung e2 in
1214

    
1215
    u1 || u2
1216

    
1217
  | Ite (_, e1, e2, e3) | With (_, e1, e2, e3)
1218
  | ArraySlice (_, e1, (e2, e3)) ->
1219
    let u1 = has_unguarded_pre ung e1 in
1220
    let u2 = has_unguarded_pre ung e2 in
1221
    let u3 = has_unguarded_pre ung e3 in
1222
    u1 || u2 || u3
1223
  
1224
  | ExprList (_, l) | TupleExpr (_, l) | ArrayExpr (_, l)
1225
  | OneHot (_, l) | Call (_, _, l) | CallParam (_, _, _, l) ->
1226
    let us = List.map (has_unguarded_pre ung) l in
1227
    List.exists KindLib.identity us
1228

    
1229
  | Merge (_, _, l) ->
1230
    let us = List.map (has_unguarded_pre ung) (List.map snd l) in
1231
    List.exists KindLib.identity us
1232

    
1233
  | RestartEvery (_, _, l, e) ->
1234
    let us = List.map (has_unguarded_pre ung) (e :: l) in
1235
    List.exists KindLib.identity us
1236

    
1237
  | Activate (_, _, e, r, l)  ->
1238
    let us = List.map (has_unguarded_pre ung) (e :: r :: l) in
1239
    List.exists KindLib.identity us
1240

    
1241
  | Condact (_, e, r, _, l1, l2) ->
1242
    let us = List.map (has_unguarded_pre ung) (e :: r :: l1 @ l2) in
1243
    List.exists KindLib.identity us
1244

    
1245
  | RecordExpr (_, _, ie) ->
1246
    let us = List.map (fun (_, e) -> has_unguarded_pre ung e) ie in
1247
    List.exists KindLib.identity us
1248

    
1249
  | StructUpdate (_, e1, li, e2) ->
1250
    let u1 = has_unguarded_pre ung e1 in
1251
    let us = List.map (function
1252
        | Label _ -> false
1253
        | Index (_, e) -> has_unguarded_pre ung e
1254
      ) li in
1255
    let u2 = has_unguarded_pre ung e2 in
1256
    u1 || u2 || List.exists KindLib.identity us
1257

    
1258
  | Fby (_, e1, _, e2) ->
1259
    let u1, u2 = has_unguarded_pre ung e1, has_unguarded_pre ung e2 in
1260
    u1 || u2
1261

    
1262
  | Pre (pos, e) as p ->
1263
    if ung then begin
1264
      (* Fail only if in strict mode *)
1265
      let err_or_warn = warn_at_position in
1266

    
1267
      err_or_warn pos
1268
        (Format.asprintf "@[<hov 2>Unguarded pre in expression@ %a@]"
1269
           pp_print_expr p)
1270
    end;
1271

    
1272
    let u = has_unguarded_pre true e in
1273
    ung || u
1274

    
1275
  | Last _ -> false
1276

    
1277
  (* TODO: Only report unguarded lasts contained in automaton states
1278
     that are activable at the initial state *)
1279
(*
1280
  | Last (pos, _) as p ->
1281
    if ung then begin
1282
      (* Fail only if in strict mode *)
1283
      let err_or_warn =
1284
        if Flags.lus_strict () then error_at_position else warn_at_position in
1285

    
1286
      err_or_warn pos
1287
        (Format.asprintf "@[<hov 2>Unguarded pre in expression@ %a@]"
1288
           pp_print_expr p)
1289
    end;
1290
    ung
1291
*)
1292
    
1293
  | Arrow (_, e1, e2) ->
1294
    let u1 = has_unguarded_pre ung e1 in
1295
    let u2 = has_unguarded_pre false e1 in
1296
    u1 || u2
1297

    
1298
let has_unguarded_pre e =
1299
  let u = has_unguarded_pre true e in
1300
  u
1301

    
1302
(** If second argument is `Some _`, returns that. Otherwise runs `f`. *)
1303
let unwrap_or f = function
1304
| None -> f ()
1305
| res -> res
1306

    
1307
(** If input list contains `Some _`, returns that. Otherwise returns `None`. *)
1308
let some_of_list = List.fold_left (
1309
  function
1310
  | None -> KindLib.identity
1311
  | res -> (fun _ -> res)
1312
) None
1313

    
1314
(** Checks whether an expression has a `pre` or a `->`. *)
1315
let rec has_pre_or_arrow = function
1316
  | True _ | False _ | Num _ | Dec _ | Ident _ | ModeRef _ -> None
1317
    
1318
  | RecordProject (_, e, _) | ToInt (_, e) | ToReal (_, e)
1319
  | Not (_, e) | Uminus (_, e) | Current (_, e) | When (_, e, _)
1320
  | Forall (_, _, e) | Exists (_, _, e) ->
1321
    has_pre_or_arrow e
1322

    
1323
  | TupleProject (_, e1, e2) | And (_, e1, e2) | Or (_, e1, e2)
1324
  | Xor (_, e1, e2) | Impl (_, e1, e2) | ArrayConstr (_, e1, e2) 
1325
  | Mod (_, e1, e2) | Minus (_, e1, e2) | Plus (_, e1, e2) | Div (_, e1, e2)
1326
  | Times (_, e1, e2) | IntDiv (_, e1, e2) | Eq (_, e1, e2) | Neq (_, e1, e2)
1327
  | Lte (_, e1, e2) | Lt (_, e1, e2) | Gte (_, e1, e2) | Gt (_, e1, e2)
1328
  | ArrayConcat (_, e1, e2) -> (
1329
    match has_pre_or_arrow e1 with
1330
    | None -> has_pre_or_arrow e2
1331
    | res -> res
1332
  )
1333

    
1334
  | Ite (_, e1, e2, e3) | With (_, e1, e2, e3)
1335
  | ArraySlice (_, e1, (e2, e3)) ->
1336
    has_pre_or_arrow e1
1337
    |> unwrap_or (
1338
      fun _ ->
1339
        has_pre_or_arrow e2
1340
        |> unwrap_or (
1341
          fun _ -> has_pre_or_arrow e3
1342
        )
1343
    )
1344
  
1345
  | ExprList (_, l) | TupleExpr (_, l) | ArrayExpr (_, l)
1346
  | OneHot (_, l) | Call (_, _, l) | CallParam (_, _, _, l) ->
1347
    List.map has_pre_or_arrow l
1348
    |> some_of_list
1349

    
1350
  | Merge (_, _, l) ->
1351
    List.map has_pre_or_arrow (List.map snd l)
1352
    |> some_of_list
1353

    
1354
  | RestartEvery (_, _, l, e) ->
1355
    List.map has_pre_or_arrow (e :: l)
1356
    |> some_of_list
1357

    
1358
  | Activate (_, _, e, r, l) ->
1359
    List.map has_pre_or_arrow (e :: r :: l)
1360
    |> some_of_list
1361

    
1362
  | Condact (_, e, r, _, l1, l2) ->
1363
    List.map has_pre_or_arrow (e :: r :: l1 @ l2)
1364
    |> some_of_list
1365

    
1366
  | RecordExpr (_, _, ie) ->
1367
    List.map (fun (_, e) -> has_pre_or_arrow e) ie
1368
    |> some_of_list
1369

    
1370
  | StructUpdate (_, e1, li, e2) ->
1371
    has_pre_or_arrow e1
1372
    |> unwrap_or (
1373
      fun _ ->
1374
        has_pre_or_arrow e2
1375
        |> unwrap_or (
1376
          fun _ ->
1377
            List.map (function
1378
              | Label _ -> None
1379
              | Index (_, e) -> has_pre_or_arrow e
1380
            ) li
1381
            |> some_of_list
1382
        )
1383
    )
1384

    
1385
  | Fby (_, e1, _, e2) ->
1386
    has_pre_or_arrow e1
1387
    |> unwrap_or (fun _ -> has_pre_or_arrow e2)
1388

    
1389
  | Pre (pos, _) | Last (pos, _) -> Some pos
1390

    
1391
  | Arrow (pos, e1, e2) -> Some pos
1392

    
1393

    
1394
(** Returns identifiers under a last operator *)
1395
let rec lasts_of_expr acc = function
1396
  | True _ | False _ | Num _ | Dec _ | Ident _ | ModeRef _ -> acc
1397
    
1398
  | RecordProject (_, e, _) | ToInt (_, e) | ToReal (_, e)
1399
  | Not (_, e) | Uminus (_, e) | Current (_, e) | When (_, e, _)
1400
  | Forall (_, _, e) | Exists (_, _, e) ->
1401
    lasts_of_expr acc e
1402

    
1403
  | TupleProject (_, e1, e2) | And (_, e1, e2) | Or (_, e1, e2)
1404
  | Xor (_, e1, e2) | Impl (_, e1, e2) | ArrayConstr (_, e1, e2) 
1405
  | Mod (_, e1, e2) | Minus (_, e1, e2) | Plus (_, e1, e2) | Div (_, e1, e2)
1406
  | Times (_, e1, e2) | IntDiv (_, e1, e2) | Eq (_, e1, e2) | Neq (_, e1, e2)
1407
  | Lte (_, e1, e2) | Lt (_, e1, e2) | Gte (_, e1, e2) | Gt (_, e1, e2)
1408
  | ArrayConcat (_, e1, e2) ->
1409
    lasts_of_expr (lasts_of_expr acc e1) e2
1410

    
1411
  | Ite (_, e1, e2, e3) | With (_, e1, e2, e3)
1412
  | ArraySlice (_, e1, (e2, e3)) ->
1413
    lasts_of_expr (lasts_of_expr (lasts_of_expr acc e1) e2) e3
1414
  
1415
  | ExprList (_, l) | TupleExpr (_, l) | ArrayExpr (_, l)
1416
  | OneHot (_, l) | Call (_, _, l) | CallParam (_, _, _, l) ->
1417
    List.fold_left lasts_of_expr acc l
1418

    
1419
  | Merge (_, _, l) ->
1420
    List.fold_left (fun acc (_, e) -> lasts_of_expr acc e) acc l
1421

    
1422
  | RestartEvery (_, _, l, e) ->
1423
    List.fold_left lasts_of_expr acc (e :: l)
1424

    
1425
  | Activate (_, _, e, r, l) ->
1426
    List.fold_left lasts_of_expr acc (e :: r :: l)
1427

    
1428
  | Condact (_, e, r, _, l1, l2) ->
1429
    List.fold_left lasts_of_expr acc (e :: r :: l1 @ l2)
1430

    
1431
  | RecordExpr (_, _, ie) ->
1432
    List.fold_left (fun acc (_, e) -> lasts_of_expr acc e) acc ie
1433

    
1434
  | StructUpdate (_, e1, li, e2) ->
1435
    let acc = lasts_of_expr (lasts_of_expr acc e1) e2 in
1436
    List.fold_left (fun acc -> function
1437
        | Label _ -> acc
1438
        | Index (_, e) -> lasts_of_expr acc e
1439
      ) acc li
1440
    
1441
  | Fby (_, e1, _, e2) ->
1442
    lasts_of_expr (lasts_of_expr acc e1) e2
1443

    
1444
  | Pre (pos, e) -> lasts_of_expr acc e
1445
                      
1446
  | Last (pos, i) -> SI.add i acc
1447

    
1448
  | Arrow (pos, e1, e2) ->
1449
    lasts_of_expr (lasts_of_expr acc e1) e2
1450

    
1451

    
1452
let rec replace_lasts allowed prefix acc ee = match ee with
1453
  | True _ | False _ | Num _ | Dec _ | Ident _ | ModeRef _ ->
1454
    ee, acc
1455
    
1456
  | RecordProject (pos, e, i) ->
1457
    let e', acc' = replace_lasts allowed prefix acc e in
1458
    if e == e' then ee, acc
1459
    else RecordProject (pos, e', i), acc'
1460
         
1461
  | ToInt (pos, e) ->
1462
    let e', acc' = replace_lasts allowed prefix acc e in
1463
    if e == e' then ee, acc
1464
    else ToInt (pos, e'), acc'
1465
                      
1466
  | ToReal (pos, e) ->
1467
    let e', acc' = replace_lasts allowed prefix acc e in
1468
    if e == e' then ee, acc
1469
    else ToReal (pos, e'), acc'
1470

    
1471
  | Not (pos, e) ->
1472
    let e', acc' = replace_lasts allowed prefix acc e in
1473
    if e == e' then ee, acc
1474
    else Not (pos, e'), acc'
1475

    
1476
  | Uminus (pos, e) ->
1477
    let e', acc' = replace_lasts allowed prefix acc e in
1478
    if e == e' then ee, acc
1479
    else Uminus (pos, e'), acc'
1480

    
1481
  | Current (pos, e) ->
1482
    let e', acc' = replace_lasts allowed prefix acc e in
1483
    if e == e' then ee, acc
1484
    else Current (pos, e'), acc'
1485

    
1486
  | When (pos, e, c) ->
1487
    let e', acc' = replace_lasts allowed prefix acc e in
1488
    if e == e' then ee, acc
1489
    else When (pos, e', c), acc'
1490

    
1491
  | Forall (pos, vs, e) ->
1492
    let e', acc' = replace_lasts allowed prefix acc e in
1493
    if e == e' then ee, acc
1494
    else Forall (pos, vs, e'), acc'
1495

    
1496
  | Exists (pos, vs, e) ->
1497
    let e', acc' = replace_lasts allowed prefix acc e in
1498
    if e == e' then ee, acc
1499
    else Exists (pos, vs, e'), acc'
1500

    
1501
  | TupleProject (pos, e1, e2)
1502
  | And (pos, e1, e2) | Or (pos, e1, e2) | Xor (pos, e1, e2)
1503
  | Impl (pos, e1, e2) | ArrayConstr (pos, e1, e2) | Mod (pos, e1, e2)
1504
  | Minus (pos, e1, e2) | Plus (pos, e1, e2) | Div (pos, e1, e2)
1505
  | Times (pos, e1, e2) | IntDiv (pos, e1, e2) | Eq (pos, e1, e2)
1506
  | Neq (pos, e1, e2) | Lte (pos, e1, e2) | Lt (pos, e1, e2)
1507
  | Gte (pos, e1, e2) | Gt (pos, e1, e2) | ArrayConcat (pos, e1, e2) ->
1508
    let e1', acc' = replace_lasts allowed prefix acc e1 in
1509
    let e2', acc' = replace_lasts allowed prefix acc' e2 in
1510
    if e1 == e1' && e2 == e2' then ee, acc
1511
    else (match ee with
1512
        | TupleProject (pos, e1, e2) -> TupleProject (pos, e1', e2')
1513
        | And (pos, e1, e2) -> And (pos, e1', e2')
1514
        | Or (pos, e1, e2) -> Or (pos, e1', e2')
1515
        | Xor (pos, e1, e2) -> Xor (pos, e1', e2')
1516
        | Impl (pos, e1, e2) -> Impl (pos, e1', e2')
1517
        | ArrayConstr (pos, e1, e2)  -> ArrayConstr (pos, e1', e2') 
1518
        | Mod (pos, e1, e2) -> Mod (pos, e1', e2')
1519
        | Minus (pos, e1, e2) -> Minus (pos, e1', e2')
1520
        | Plus (pos, e1, e2) -> Plus (pos, e1', e2')
1521
        | Div (pos, e1, e2) -> Div (pos, e1', e2')
1522
        | Times (pos, e1, e2) -> Times (pos, e1', e2')
1523
        | IntDiv (pos, e1, e2) -> IntDiv (pos, e1', e2')
1524
        | Eq (pos, e1, e2) -> Eq (pos, e1', e2')
1525
        | Neq (pos, e1, e2) -> Neq (pos, e1', e2')
1526
        | Lte (pos, e1, e2) -> Lte (pos, e1', e2')
1527
        | Lt (pos, e1, e2) -> Lt (pos, e1', e2')
1528
        | Gte (pos, e1, e2) -> Gte (pos, e1', e2')
1529
        | Gt (pos, e1, e2) -> Gt (pos, e1', e2')
1530
        | ArrayConcat (pos, e1, e2) -> ArrayConcat (pos, e1', e2')
1531
        | _ -> assert false
1532
      ), acc'
1533

    
1534
  | Ite (_, e1, e2, e3) | With (_, e1, e2, e3)
1535
  | ArraySlice (_, e1, (e2, e3)) ->
1536
    let e1', acc' = replace_lasts allowed prefix acc e1 in
1537
    let e2', acc' = replace_lasts allowed prefix acc' e2 in
1538
    let e3', acc' = replace_lasts allowed prefix acc' e3 in
1539
    if e1 == e1' && e2 == e2' && e3 == e3' then ee, acc
1540
    else (match ee with
1541
        | Ite (pos, e1, e2, e3) -> Ite (pos, e1', e2', e3')
1542
        | With (pos, e1, e2, e3) -> With (pos, e1', e2', e3')
1543
        | ArraySlice (pos, e1, (e2, e3)) -> ArraySlice (pos, e1', (e2', e3'))
1544
        | _ -> assert false
1545
      ), acc'
1546
  
1547
  | ExprList (_, l) | TupleExpr (_, l) | ArrayExpr (_, l)
1548
  | OneHot (_, l) | Call (_, _, l) | CallParam (_, _, _, l) ->
1549
    let l', acc' =
1550
      List.fold_left (fun (l, acc) e ->
1551
          let e, acc = replace_lasts allowed prefix acc e in
1552
          e :: l, acc
1553
        ) ([], acc) l in
1554
    let l' = List.rev l' in
1555
    if try List.for_all2 (==) l l' with _ -> false then ee, acc
1556
    else (match ee with
1557
        | ExprList (pos, l) -> ExprList (pos, l')
1558
        | TupleExpr (pos, l) -> TupleExpr (pos, l')
1559
        | ArrayExpr (pos, l) -> ArrayExpr (pos, l')
1560
        | OneHot (pos, l) -> OneHot (pos, l')
1561
        | Call (pos, n, l) -> Call (pos, n, l')
1562
        | CallParam (pos, n, t, l) -> CallParam (pos, n, t, l')
1563
        | _ -> assert false
1564
      ), acc'
1565
      
1566

    
1567
  | Merge (pos, c, l) ->
1568
    let l', acc' =
1569
      List.fold_left (fun (l, acc) (c, e) ->
1570
          let e, acc = replace_lasts allowed prefix acc e in
1571
          (c, e) :: l, acc
1572
        ) ([], acc) l in
1573
    let l' = List.rev l' in
1574
    if try List.for_all2 (fun (_, x) (_, x') -> x == x') l l' with _ -> false
1575
    then ee, acc
1576
    else Merge (pos, c, l'), acc'
1577

    
1578
  | RestartEvery (pos, n, l, e) ->
1579
    let l', acc' =
1580
      List.fold_left (fun (l, acc) e ->
1581
          let e, acc = replace_lasts allowed prefix acc e in
1582
          e :: l, acc
1583
        ) ([], acc) l in
1584
    let l' = List.rev l' in
1585
    let e', acc' = replace_lasts allowed prefix acc' e in
1586
    if try e == e' && List.for_all2 (==) l l'  with _ -> false then ee, acc
1587
    else RestartEvery (pos, n, l', e'), acc
1588

    
1589
  | Activate (pos, n, e, r, l) ->
1590
    let l', acc' =
1591
      List.fold_left (fun (l, acc) e ->
1592
          let e, acc = replace_lasts allowed prefix acc e in
1593
          e :: l, acc
1594
        ) ([], acc) l in
1595
    let l' = List.rev l' in
1596
    let e', acc' = replace_lasts allowed prefix acc' e in
1597
    let r', acc' = replace_lasts allowed prefix acc' r in
1598
    if try e == e' && r == r' &&
1599
           List.for_all2 (==) l l'  with _ -> false then ee, acc
1600
    else Activate (pos, n, e', r', l'), acc'
1601

    
1602
  | Condact (pos, e, r, n, l1, l2) ->
1603
    let l1', acc' =
1604
      List.fold_left (fun (l, acc) e ->
1605
          let e, acc = replace_lasts allowed prefix acc e in
1606
          e :: l, acc
1607
        ) ([], acc) l1 in
1608
    let l1' = List.rev l1 in
1609
    let l2', acc' =
1610
      List.fold_left (fun (l, acc) e ->
1611
          let e, acc = replace_lasts allowed prefix acc e in
1612
          e :: l, acc
1613
        ) ([], acc') l2 in
1614
    let l2' = List.rev l2 in
1615
    let e', acc' = replace_lasts allowed prefix acc' e in
1616
    let r', acc' = replace_lasts allowed prefix acc' r in
1617
    if try e == e' && r == r' &&
1618
           List.for_all2 (==) l1 l1' &&
1619
           List.for_all2 (==) l2 l2'
1620
      with _ -> false then ee, acc
1621
    else Condact (pos, e', r', n, l1', l2'), acc'
1622

    
1623
  | RecordExpr (pos, n, ie) ->
1624
    let ie', acc' =
1625
      List.fold_left (fun (ie, acc) (i, e) ->
1626
          let e, acc = replace_lasts allowed prefix acc e in
1627
          (i, e) :: ie, acc
1628
        ) ([], acc) ie in
1629
    let ie' = List.rev ie' in
1630
    if try List.for_all2 (fun (_, e) (_, e') -> e == e') ie ie' with _ -> false
1631
    then ee, acc
1632
    else RecordExpr (pos, n, ie'), acc'
1633

    
1634
  | StructUpdate (pos, e1, li, e2) ->
1635
    let li', acc' =
1636
      List.fold_left (fun (li, acc) -> function
1637
          | Label _ as s -> s :: li, acc
1638
          | Index (i, e) as s ->
1639
            let e', acc' = replace_lasts allowed prefix acc e in
1640
            if e == e' then s :: li, acc
1641
            else Index (i, e') :: li, acc
1642
        ) ([], acc) li in
1643
    let li' = List.rev li' in
1644
    let e1', acc' = replace_lasts allowed prefix acc' e1 in
1645
    let e2', acc' = replace_lasts allowed prefix acc' e2 in
1646
    if try e1 == e1' && e2 == e2' &&
1647
           List.for_all2 (fun ei ei' -> match ei, ei' with
1648
               | Label _, Label _ -> true
1649
               | Index (_, e), Index (_, e') -> e == e'
1650
               | _ -> false
1651
             ) li li'
1652
      with _ -> false then ee, acc
1653
    else StructUpdate (pos, e1', li', e2'), acc'
1654
        
1655
  | Fby (pos, e1, i, e2) ->
1656
    let e1', acc' = replace_lasts allowed prefix acc e1 in
1657
    let e2', acc' = replace_lasts allowed prefix acc' e2 in
1658
    if e1 == e1' && e2 == e2' then ee, acc
1659
    else Fby (pos, e1', i, e2'), acc'
1660
    
1661
  | Pre (pos, e) ->
1662
    let e', acc' = replace_lasts allowed prefix acc e in
1663
    if e == e' then ee, acc else Pre (pos, e'), acc'
1664
                      
1665
  | Last (pos, i) ->
1666
    if not (List.mem i allowed) then
1667
      error_at_position pos
1668
        "Only visible variables in the node are allowed under last";
1669
    let acc = SI.add i acc in
1670
    Ident (pos, prefix ^ ".last." ^ i), acc
1671

    
1672
  | Arrow (pos, e1, e2) ->
1673
    let e1', acc' = replace_lasts allowed prefix acc e1 in
1674
    let e2', acc' = replace_lasts allowed prefix acc' e2 in
1675
    if e1 == e1' && e2 == e2' then ee, acc
1676
    else Arrow (pos, e1', e2'), acc'
1677

    
1678

    
1679

    
1680
(** Checks whether a struct item has a `pre` or a `->`. *)
1681
let rec struct_item_has_pre_or_arrow = function
1682
| SingleIdent _ | FieldSelection _ | ArrayDef _ -> None
1683
| TupleStructItem (_, l) ->
1684
  List.map struct_item_has_pre_or_arrow l
1685
  |> some_of_list
1686
| ArraySliceStructItem (_, _, l) ->
1687
  List.map (
1688
    fun (e1, e2) ->
1689
      has_pre_or_arrow e1
1690
      |> unwrap_or (fun _ -> has_pre_or_arrow e2)
1691
  ) l
1692
  |> some_of_list
1693
| TupleSelection (_, _, e) -> has_pre_or_arrow e
1694

    
1695

    
1696
(** Checks whether a constant declaration has a `pre` or a `->`. *)
1697
let const_decl_has_pre_or_arrow = function
1698
| FreeConst _ -> None
1699
| UntypedConst (_, _, e) -> has_pre_or_arrow e
1700
| TypedConst (_, _, e, _) -> has_pre_or_arrow e
1701

    
1702

    
1703

    
1704
(** Checks whether a node local declaration has a `pre` or a `->`. *)
1705
let node_local_decl_has_pre_or_arrow = function
1706
| NodeConstDecl (_, decl) -> const_decl_has_pre_or_arrow decl
1707
| NodeVarDecl _ -> None
1708

    
1709

    
1710
(** Checks whether an equation lhs has a `pre` or a `->`. *)
1711
let eq_lhs_has_pre_or_arrow = function
1712
| StructDef (_, l) ->
1713
  List.map struct_item_has_pre_or_arrow l
1714
  |> some_of_list
1715

    
1716
(** Checks whether a node equation has a `pre` or a `->`. *)
1717
let node_item_has_pre_or_arrow = function
1718
| Body (Assert (_, e)) -> has_pre_or_arrow e
1719
| Body (Equation (_, lhs, e)) ->
1720
  eq_lhs_has_pre_or_arrow lhs
1721
  |> unwrap_or (fun _ -> has_pre_or_arrow e)
1722
| AnnotMain _ -> None
1723
| AnnotProperty (_, _, e) -> has_pre_or_arrow e
1724
| Body (Automaton _) -> assert false
1725

    
1726
(** Checks whether a contract node equation has a `pre` or a `->`.
1727

    
1728
Does not (cannot) check contract calls recursively, checks only inputs and
1729
outputs. *)
1730
let contract_node_equation_has_pre_or_arrow = function
1731
| GhostConst decl
1732
| GhostVar decl -> const_decl_has_pre_or_arrow decl
1733
| Assume (_, _, e)
1734
| Guarantee (_, _, e) -> has_pre_or_arrow e
1735
| Mode (_, _, reqs, enss) ->
1736
  List.map (fun (_, _, e) -> has_pre_or_arrow e) reqs
1737
  |> some_of_list
1738
  |> unwrap_or (
1739
    fun _ ->
1740
      List.map (fun (_, _, e) -> has_pre_or_arrow e) enss
1741
      |> some_of_list
1742
  )
1743
| ContractCall (_, _, ins, outs) ->
1744
  List.map has_pre_or_arrow ins
1745
  |> some_of_list
1746
  |> unwrap_or (
1747
    fun _ ->
1748
      List.map has_pre_or_arrow outs
1749
      |> some_of_list
1750
  )
1751

    
1752
(** Checks whether a contract has a `pre` or a `->`.
1753

    
1754
Does not (cannot) check contract calls recursively, checks only inputs and
1755
outputs. *)
1756
let contract_has_pre_or_arrow l =
1757
  List.map contract_node_equation_has_pre_or_arrow l
1758
  |> some_of_list
1759

    
1760

    
1761
(* 
1762
   Local Variables:
1763
   compile-command: "make -k -C .."
1764
   indent-tabs-mode: nil
1765
   End: 
1766
*)
1767

    
(7-7/12)