Project

General

Profile

Revision 01c7d5e1

View differences:

src/access.ml
71 71
  | Expr_when (e1,_,_) -> check_expr checks e1
72 72
 
73 73
  | Expr_merge (_,hl) -> List.fold_left (fun checks (l, h) -> check_expr checks h) checks hl
74
  | _ -> assert false
75 74
  in (*Format.eprintf "typing %B %a at %a = %a@." const Printers.pp_expr expr Location.pp_loc expr.expr_loc Types.print_ty res;*) res
76 75

  
77 76
let rec check_var_decl_type loc checks ty =
......
90 89
let check_node nd =
91 90
  let checks = CSet.empty in
92 91
  let checks =
93
    List.fold_left check_var_decl checks (node_vars nd) in
92
    List.fold_left check_var_decl checks (get_node_vars nd) in
94 93
  let checks =
95 94
    List.fold_left (fun checks eq -> check_expr checks eq.eq_rhs) checks nd.node_eqs in
96 95
  nd.node_checks <- CSet.elements checks
src/backends/C/c_backend_common.ml
192 192
    | Const_tag t     -> pp_c_tag fmt t
193 193
    | Const_array ca  -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " pp_c_const) ca
194 194
    | Const_struct fl -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " (fun fmt (f, c) -> pp_c_const fmt c)) fl
195
    | Const_string _ -> assert false (* string occurs in annotations not in C *)
195 196

  
196 197
(* Prints a value expression [v], with internal function calls only.
197 198
   [pp_var] is a printer for variables (typically [pp_c_var_read]),
src/backends/C/c_backend_makefile.ml
1 1
open Format
2
open LustreSpec
2 3
open Corelang
3 4

  
4 5
let header_has_code header =
......
40 41

  
41 42
module type MODIFIERS_MKF =
42 43
sig
43
  val other_targets: Format.formatter -> string -> string -> (string * bool * Corelang.top_decl list) list -> unit
44
  val other_targets: Format.formatter -> string -> string -> (string * bool * top_decl list) list -> unit
44 45
end
45 46

  
46 47
module EmptyMod =
src/backends/C/c_backend_spec.ml
2 2
open LustreSpec
3 3
open Machine_code
4 4
open C_backend_common
5
open Utils
5 6

  
6 7
(**************************************************************************)
7 8
(*     Printing spec for c *)
8 9

  
9 10
(**************************************************************************)
11
(* OLD STUFF ???
12

  
10 13

  
11 14
let pp_acsl_type var fmt t =
12 15
  let rec aux t pp_suffix =
......
121 124
    pp_acsl_spec m.mstep.step_outputs fmt spec
122 125
  )
123 126

  
127
  *)
128

  
124 129
(**************************************************************************)
125 130
(*                              MAKEFILE                                  *)
126 131
(**************************************************************************)
src/causality.ml
249 249
	mashup_appl_dependencies f e g
250 250
    | Expr_appl (f, e, Some (r, _)) ->
251 251
      mashup_appl_dependencies f e (add_var lhs_is_mem lhs r g)
252
    | Expr_uclock  (e, _)
253
    | Expr_dclock  (e, _)
254
    | Expr_phclock (e, _) -> add_dep lhs_is_mem lhs e g 
255 252
  in
256 253
  let g =
257 254
    List.fold_left
......
294 291
      | Expr_arrow (e1,e2) -> ESet.union (get_expr_calls prednode e1) (get_expr_calls prednode e2)
295 292
      | Expr_ite   (c, t, e) -> ESet.union (get_expr_calls prednode c) (ESet.union (get_expr_calls prednode t) (get_expr_calls prednode e))
296 293
      | Expr_pre e 
297
      | Expr_when (e,_,_)
298
      | Expr_uclock (e,_) 
299
      | Expr_dclock (e,_) 
300
      | Expr_phclock (e,_) -> get_expr_calls prednode e
294
      | Expr_when (e,_,_) -> get_expr_calls prednode e
301 295
      | Expr_appl (id,e, _) ->
302 296
	if not (Basic_library.is_internal_fun id) && prednode id
303 297
	then ESet.add expr (get_expr_calls prednode e)
......
357 351
  module Cycles = Graph.Components.Make (IdentDepGraph)
358 352

  
359 353
  let mk_copy_var n id =
360
    mk_new_name (node_vars n) id
354
    mk_new_name (get_node_vars n) id
361 355

  
362 356
  let mk_copy_eq n var =
363
    let var_decl = node_var var n in
357
    let var_decl = get_node_var var n in
364 358
    let cp_var = mk_copy_var n var in
365 359
    let expr =
366 360
      { expr_tag = Utils.new_tag ();
src/clock_calculus.ml
685 685
      List.iter (fun (t, h) -> clock_subtyping_arg env h (new_ck (Con (cvar,cr,t)) true)) hl;
686 686
      expr.expr_clock <- cvar;
687 687
      cvar
688
  | Expr_uclock (e,k) ->
689
      let pck = clock_expr env e in
690
      if not (can_be_pck pck) then
691
        raise (Error (e.expr_loc, Not_pck));
692
      if k = 0 then
693
        raise (Error (expr.expr_loc, Factor_zero));
694
      (try
695
        subsume pck (CSet_pck (k,(0,1)))
696
      with Subsume (ck,cset) ->
697
        raise (Error (e.expr_loc, Clock_set_mismatch (ck,CSet_pck (k,(0,1))))));
698
      let ck = new_ck (Pck_up (pck,k)) true in
699
      expr.expr_clock <- ck;
700
      ck
701
  | Expr_dclock (e,k) ->
702
      let pck = clock_expr env e in
703
      if not (can_be_pck pck) then
704
        raise (Error (e.expr_loc, Not_pck));
705
      if k = 0 then
706
        raise (Error (expr.expr_loc, Factor_zero));
707
      (try
708
        subsume pck (CSet_pck (1,(0,1)))
709
      with Subsume (ck,cset) ->
710
        raise (Error (e.expr_loc, Clock_set_mismatch (ck,CSet_pck (1,(0,1))))));
711
      let ck = new_ck (Pck_down (pck,k)) true in
712
      expr.expr_clock <- ck;
713
      ck
714
  | Expr_phclock (e,(a,b)) ->
715
      let pck = clock_expr env e in
716
      if not (can_be_pck pck) then
717
        raise (Error (e.expr_loc, Not_pck));
718
      let (a,b) = simplify_rat (a,b) in
719
      (try
720
        subsume pck (CSet_pck (b,(0,1)))
721
      with Subsume (ck,cset) ->
722
        raise (Error (e.expr_loc, Clock_set_mismatch (ck,CSet_pck (b,(0,1))))));
723
      let ck = new_ck (Pck_phase (pck,(a,b))) true in
724
      expr.expr_clock <- ck;
725
      ck
726 688
  in
727 689
  Log.report ~level:4 (fun fmt -> Format.fprintf fmt "Clock of expr %a: %a@." Printers.pp_expr expr Clocks.print_ck resulting_ck);
728 690
  resulting_ck
src/corelang.ml
23 23
open LustreSpec
24 24
open Dimension
25 25

  
26
(** The core language and its ast. Every element of the ast contains its
27
    location in the program text. The type and clock of an ast element
28
    is mutable (and initialized to dummy values). This avoids to have to
29
    duplicate ast structures (e.g. ast, typed_ast, clocked_ast). *)
30

  
31
type ident = Utils.ident
32
type label = Utils.ident
33
type rat = Utils.rat
34
type tag = Utils.tag
35

  
36
type constant =
37
  | Const_int of int
38
  | Const_real of string
39
  | Const_float of float
40
  | Const_array of constant list
41
  | Const_tag of label
42
  | Const_struct of (label * constant) list
43

  
44
type type_dec = LustreSpec.type_dec
45

  
46
let dummy_type_dec = {ty_dec_desc=Tydec_any; ty_dec_loc=Location.dummy_loc}
47

  
48

  
49
type clock_dec = LustreSpec.clock_dec
50

  
51
let dummy_clock_dec = {ck_dec_desc=Ckdec_any; ck_dec_loc=Location.dummy_loc}
52

  
53
type var_decl = LustreSpec.var_decl
54

  
55
(* The tag of an expression is a unique identifier used to distinguish
56
   different instances of the same node *)
57
type expr =
58
    {expr_tag: tag;
59
     expr_desc: expr_desc;
60
     mutable expr_type: Types.type_expr;
61
     mutable expr_clock: Clocks.clock_expr;
62
     mutable expr_delay: Delay.delay_expr;
63
     mutable expr_annot: LustreSpec.expr_annot option;
64
     expr_loc: Location.t}
65

  
66
and expr_desc =
67
  | Expr_const of constant
68
  | Expr_ident of ident
69
  | Expr_tuple of expr list
70
  | Expr_ite   of expr * expr * expr
71
  | Expr_arrow of expr * expr
72
  | Expr_fby of expr * expr
73
  | Expr_array of expr list
74
  | Expr_access of expr * Dimension.dim_expr
75
  | Expr_power of expr * Dimension.dim_expr
76
  | Expr_pre of expr
77
  | Expr_when of expr * ident * label
78
  | Expr_merge of ident * (label * expr) list
79
  | Expr_appl of call_t
80
  | Expr_uclock of expr * int
81
  | Expr_dclock of expr * int
82
  | Expr_phclock of expr * rat
83
 and call_t = ident * expr * (ident * label) option (* The third part denotes the reseting clock label and value *)
84

  
85
type eq =
86
    {eq_lhs: ident list;
87
     eq_rhs: expr;
88
     eq_loc: Location.t}
89

  
90
type assert_t = 
91
    {
92
      assert_expr: expr;
93
      assert_loc: Location.t
94
    } 
95

  
96
type node_desc =
97
    {node_id: ident;
98
     mutable node_type: Types.type_expr;
99
     mutable node_clock: Clocks.clock_expr;
100
     node_inputs: var_decl list;
101
     node_outputs: var_decl list;
102
     node_locals: var_decl list;
103
     mutable node_gencalls: expr list;
104
     mutable node_checks: Dimension.dim_expr list;
105
     node_asserts: assert_t list; 
106
     node_eqs: eq list;
107
     mutable node_dec_stateless: bool;
108
     mutable node_stateless: bool option;
109
     node_spec: LustreSpec.node_annot option;
110
     node_annot: LustreSpec.expr_annot option;
111
    }
112

  
113
type imported_node_desc =
114
    {nodei_id: ident;
115
     mutable nodei_type: Types.type_expr;
116
     mutable nodei_clock: Clocks.clock_expr;
117
     nodei_inputs: var_decl list;
118
     nodei_outputs: var_decl list;
119
     nodei_stateless: bool;
120
     nodei_spec: LustreSpec.node_annot option;
121
     nodei_prototype: string option;
122
     nodei_in_lib: string option;
123
    }
124

  
125
type const_desc = 
126
    {const_id: ident; 
127
     const_loc: Location.t; 
128
     const_value: constant;      
129
     mutable const_type: Types.type_expr;
130
    }
131

  
132
type top_decl_desc =
133
| Node of node_desc
134
| Consts of const_desc list
135
| ImportedNode of imported_node_desc
136
| Open of bool * string (* the boolean set to true denotes a local 
137
			   lusi vs a lusi installed at system level *)
138

  
139
type top_decl =
140
    {top_decl_desc: top_decl_desc;
141
     top_decl_loc: Location.t}
142

  
143
type program = top_decl list
144

  
145
type error =
146
    Main_not_found
147
  | Main_wrong_kind
148
  | No_main_specified
149
  | Unbound_symbol of ident
150
  | Already_bound_symbol of ident
151 26

  
152 27
exception Error of Location.t * error
153 28

  
......
163 38

  
164 39
module VSet = Set.Make(VDeclModule)
165 40

  
41
let dummy_type_dec = {ty_dec_desc=Tydec_any; ty_dec_loc=Location.dummy_loc}
42

  
43

  
44

  
45
let dummy_clock_dec = {ck_dec_desc=Ckdec_any; ck_dec_loc=Location.dummy_loc}
46

  
47

  
48

  
166 49
(************************************************************)
167 50
(* *)
168 51

  
......
206 89
    else name
207 90
  in new_name id 1
208 91

  
209
let update_expr_annot e annot =
210
  { e with expr_annot = LustreSpec.merge_expr_annot e.expr_annot (Some annot) }
211

  
212 92
let mkeq loc (lhs, rhs) =
213 93
  { eq_lhs = lhs;
214 94
    eq_rhs = rhs;
......
225 105
let mkpredef_call loc funname args =
226 106
  mkexpr loc (Expr_appl (funname, mkexpr loc (Expr_tuple args), None))
227 107

  
108
(************************************************************)
109
(*   Eexpr functions *)
110
(************************************************************)
111

  
112
let merge_node_annot ann1 ann2 =
113
  { requires = ann1.requires @ ann2.requires;
114
    ensures = ann1.ensures @ ann2.ensures;
115
    behaviors = ann1.behaviors @ ann2.behaviors;
116
    spec_loc = ann1.spec_loc
117
  }
118

  
119
let mkeexpr loc expr =
120
  { eexpr_tag = Utils.new_tag ();
121
    eexpr_qfexpr = expr;
122
    eexpr_quantifiers = [];
123
    eexpr_type = Types.new_var ();
124
    eexpr_clock = Clocks.new_var true;
125
    eexpr_normalized = None;
126
    eexpr_loc = loc }
127

  
128
let extend_eexpr q e = { e with eexpr_quantifiers = q@e.eexpr_quantifiers }
129

  
130
(*
131
let mkepredef_call loc funname args =
132
  mkeexpr loc (EExpr_appl (funname, mkeexpr loc (EExpr_tuple args), None))
133

  
134
let mkepredef_unary_call loc funname arg =
135
  mkeexpr loc (EExpr_appl (funname, arg, None))
136
*)
137

  
138
let merge_expr_annot ann1 ann2 =
139
  match ann1, ann2 with
140
    | None, None -> assert false
141
    | Some _, None -> ann1
142
    | None, Some _ -> ann2
143
    | Some ann1, Some ann2 -> Some {
144
      annots = ann1.annots @ ann2.annots;
145
      annot_loc = ann1.annot_loc
146
    }
147

  
148
let update_expr_annot e annot =
149
  { e with expr_annot = merge_expr_annot e.expr_annot (Some annot) }
150

  
151

  
228 152
(***********************************************************)
229 153
(* Fast access to nodes, by name *)
230 154
let (node_table : (ident, top_decl) Hashtbl.t) = Hashtbl.create 30
......
449 373
  | Expr_when (e, i, l), Expr_when (e', i', l') -> l=l' && i=i' && is_eq_expr e e'
450 374
  | Expr_merge(i, hl), Expr_merge(i', hl') -> i=i' && List.for_all2 (fun (t, h) (t', h') -> t=t' && is_eq_expr h h') (sort_handlers hl) (sort_handlers hl')
451 375
  | Expr_appl (i, e, r), Expr_appl (i', e', r') -> i=i' && r=r' && is_eq_expr e e'
452
  | Expr_uclock(e, i), Expr_uclock(e', i') -> i=i' && is_eq_expr e e'
453
  | Expr_dclock(e, i), Expr_dclock(e', i') -> i=i' && is_eq_expr e e'
454
  | Expr_phclock(e, r), Expr_phclock(e', r') -> r=r' && is_eq_expr e e'
455 376
  | Expr_power (e1, i1), Expr_power (e2, i2)
456 377
  | Expr_access (e1, i1), Expr_access (e2, i2) -> is_eq_expr e1 e2 && is_eq_expr (expr_of_dimension i1) (expr_of_dimension i2)
457 378
  | _ -> false
458 379

  
459
let node_vars nd =
380
let get_node_vars nd =
460 381
  nd.node_inputs @ nd.node_locals @ nd.node_outputs
461 382

  
462
let node_var id node =
463
 List.find (fun v -> v.var_id = id) (node_vars node)
383
let get_var id var_list =
384
 List.find (fun v -> v.var_id = id) var_list
464 385

  
465
let node_eq id node =
386
let get_node_var id node = get_var id (get_node_vars node)
387

  
388
let get_node_eq id node =
466 389
 List.find (fun eq -> List.mem id eq.eq_lhs) node.node_eqs
467 390

  
468 391
let get_nodes prog = 
......
505 428
   | Expr_when (e', i, l)-> Expr_when (expr_replace_var fvar e', fvar i, l)
506 429
   | Expr_merge (i, hl) -> Expr_merge (fvar i, List.map (fun (t, h) -> (t, expr_replace_var fvar h)) hl)
507 430
   | Expr_appl (i, e', i') -> Expr_appl (i, expr_replace_var fvar e', Utils.option_map (fun (x, l) -> fvar x, l) i')
508
   | _ -> assert false
509 431

  
510 432
(* Applies the renaming function [fvar] to every rhs
511 433
   only when the corresponding lhs satisfies predicate [pvar] *)
......
541 463
				 in Expr_when (replace lhs e', i', l)
542 464
       | Expr_merge (i, hl)   -> let i' = if pvar lhs then fvar i else i
543 465
				 in Expr_merge (i', List.map (fun (t, h) -> (t, replace lhs h)) hl)
544
       | _                    -> assert false)
466
       )
545 467
   in { eq with eq_rhs = replace eq.eq_lhs eq.eq_rhs }
546 468

  
547 469

  
......
565 487
     Expr_merge (f_var i, List.map (fun (t, h) -> (t, re h)) hl)
566 488
   | Expr_appl (i, e', i') -> 
567 489
     Expr_appl (f_node i, re e', Utils.option_map (fun (x, l) -> f_var x, l) i')
568
   | _ -> assert false
569

  
490
  
570 491
 let rename_node_annot f_node f_var f_const expr  =
571 492
   expr
572 493
 (* TODO assert false *)
......
599 520
      nd.node_spec 
600 521
  in
601 522
  let annot =
602
    Utils.option_map
523
    List.map 
603 524
      (fun s -> rename_expr_annot f_node f_var f_const s) 
604 525
      nd.node_annot
605 526
  in
......
724 645
    (fun id -> let nd = mk_internal_node id in Hashtbl.add node_table id nd)
725 646
    Basic_library.internal_funs
726 647

  
648

  
649
let rec get_expr_calls nodes e =
650
  get_calls_expr_desc nodes e.expr_desc
651
and get_calls_expr_desc nodes expr_desc =
652
  let get_calls = get_expr_calls nodes in
653
  match expr_desc with
654
  | Expr_const _ 
655
   | Expr_ident _ -> Utils.ISet.empty
656
   | Expr_tuple el
657
   | Expr_array el -> List.fold_left (fun accu e -> Utils.ISet.union accu (get_calls e)) Utils.ISet.empty el
658
   | Expr_pre e1 
659
   | Expr_when (e1, _, _) 
660
   | Expr_access (e1, _) 
661
   | Expr_power (e1, _) -> get_calls e1
662
   | Expr_ite (c, t, e) -> Utils.ISet.union (Utils.ISet.union (get_calls c) (get_calls t)) (get_calls e) 
663
   | Expr_arrow (e1, e2) 
664
   | Expr_fby (e1, e2) -> Utils.ISet.union (get_calls e1) (get_calls e2)
665
   | Expr_merge (_, hl) -> List.fold_left (fun accu (_, h) -> Utils.ISet.union accu (get_calls h)) Utils.ISet.empty  hl
666
   | Expr_appl (i, e', i') -> 
667
     if Basic_library.is_internal_fun i then 
668
       (get_calls e') 
669
     else
670
       let calls =  Utils.ISet.add i (get_calls e') in
671
       let test = (fun n -> match n.top_decl_desc with Node nd -> nd.node_id = i | _ -> false) in
672
       if List.exists test nodes then
673
	 match (List.find test nodes).top_decl_desc with
674
	 | Node nd -> Utils.ISet.union (get_node_calls nodes nd) calls
675
	 | _ -> assert false
676
       else 
677
	 calls
678

  
679
and get_eq_calls nodes eq =
680
  get_expr_calls nodes eq.eq_rhs
681
and get_node_calls nodes node =
682
  List.fold_left (fun accu eq -> Utils.ISet.union (get_eq_calls nodes eq) accu) Utils.ISet.empty node.node_eqs
683

  
684

  
685
let rec expr_has_arrows e =
686
  expr_desc_has_arrows e.expr_desc
687
and expr_desc_has_arrows expr_desc =
688
  match expr_desc with
689
  | Expr_const _ 
690
  | Expr_ident _ -> false
691
  | Expr_tuple el
692
  | Expr_array el -> List.exists expr_has_arrows el
693
  | Expr_pre e1 
694
  | Expr_when (e1, _, _) 
695
  | Expr_access (e1, _) 
696
  | Expr_power (e1, _) -> expr_has_arrows e1
697
  | Expr_ite (c, t, e) -> List.exists expr_has_arrows [c; t; e]
698
  | Expr_arrow (e1, e2) 
699
  | Expr_fby (e1, e2) -> true
700
  | Expr_merge (_, hl) -> List.exists (fun (_, h) -> expr_has_arrows h) hl
701
  | Expr_appl (i, e', i') -> expr_has_arrows e'
702

  
703
and eq_has_arrows eq =
704
  expr_has_arrows eq.eq_rhs
705
and node_has_arrows node =
706
  List.exists (fun eq -> eq_has_arrows eq) node.node_eqs
707

  
727 708
(* Local Variables: *)
728 709
(* compile-command:"make -C .." *)
729 710
(* End: *)
src/corelang.mli
21 21
 *---------------------------------------------------------------------------- *)
22 22

  
23 23
open LustreSpec
24

  
24
(*
25 25
(** The core language and its ast. *)
26 26
type ident = Utils.ident
27 27
type label = Utils.ident
......
161 161
  | No_main_specified
162 162
  | Unbound_symbol of ident
163 163
  | Already_bound_symbol of ident
164

  
164
*)
165 165
exception Error of Location.t * error
166 166

  
167
val dummy_type_dec: type_dec
168
val dummy_clock_dec: clock_dec
169

  
167 170
val mktyp: Location.t -> type_dec_desc -> type_dec
168 171
val mkclock: Location.t -> clock_dec_desc -> clock_dec
169 172
val mkvar_decl: Location.t -> ident * type_dec * clock_dec * bool (* is const *) -> var_decl
......
204 207
val const_xor: constant -> constant -> constant
205 208
val const_impl: constant -> constant -> constant
206 209

  
207
val node_vars: node_desc -> var_decl list
208
val node_var: ident -> node_desc -> var_decl
209
val node_eq: ident -> node_desc -> eq
210
val get_node_vars: node_desc -> var_decl list
211
val get_node_var: ident -> node_desc -> var_decl
212
val get_node_eq: ident -> node_desc -> eq
210 213

  
211 214
(* val get_const: ident -> constant *)
212 215

  
......
248 251
val update_expr_annot: expr -> LustreSpec.expr_annot -> expr
249 252

  
250 253

  
254
(** Annotation expression related functions *)
255
val mkeexpr: Location.t ->  expr -> eexpr
256
val merge_node_annot: node_annot -> node_annot -> node_annot 
257
val extend_eexpr: (quantifier_type * var_decl list) list -> eexpr -> eexpr
258
val update_expr_annot: expr -> expr_annot -> expr
259
(* val mkpredef_call: Location.t -> ident -> eexpr list -> eexpr*)
260

  
251 261
(* Local Variables: *)
252 262
(* compile-command:"make -C .." *)
253 263
(* End: *)
src/horn_backend.ml
313 313
	 (Utils.fprintf_list ~sep:"@ " (pp_instr false m.mname.node_id)) m.mstep.step_instrs
314 314
	 pp_machine_step_name m.mname.node_id
315 315
	 (Utils.fprintf_list ~sep:" " pp_var) (step_vars machines m);
316

  
316
(*
317 317
       match m.mspec with
318 318
	 None -> () (* No node spec; we do nothing *)
319 319
       | Some {requires = []; ensures = [EnsuresExpr e]; behaviors = []} -> 
......
323 323
	     
324 324
	 )
325 325
       | _ -> () (* Other cases give nothing *)
326
*)      
326 327
     end
327 328
    end
328 329

  
src/inliner.ml
134 134
    let el, l', eqs' = inline_tuple (List.map snd branches) in
135 135
    let branches' = List.map2 (fun (label, _) v -> label, v) branches el in
136 136
    { expr with expr_desc = Expr_merge (id, branches') }, l', eqs'
137
  | Expr_uclock _
138
  | Expr_dclock _
139
  | Expr_phclock _ -> assert false 
140 137
and inline_node nd nodes = 
141 138
  let new_locals, eqs = 
142 139
    List.fold_left (fun (locals, eqs) eq ->
......
244 241
    node_stateless = None;
245 242
    node_spec = Some 
246 243
      {requires = []; 
247
       ensures = [EnsuresExpr (mkeexpr loc (EExpr_ident ok_ident))];
248
       behaviors = []
244
       ensures = [mkeexpr loc (mkexpr loc (Expr_ident ok_ident))];
245
       behaviors = [];
246
       spec_loc = loc
249 247
      };
250
    node_annot = None;
248
    node_annot = [];
251 249
  }
252 250
  in
253 251
  let main = [{ top_decl_desc = Node main_node; top_decl_loc = loc }] in
src/lexerLustreSpec.mll
1 1
{
2 2

  
3
  open ParserLustreSpec
3
  (* open ParserLustreSpec *)
4
  open Parser_lustre
4 5
  open Utils
5 6

  
6 7
  let str_buf = Buffer.create 1024
......
11 12
   used to handle all the possible keywords. *)
12 13
let keyword_table =
13 14
  create_hashtable 20 [
14
  "true", TRUE;
15
  "false", FALSE;
15
  (* "true", TRUE; *)
16
  (* "false", FALSE; *)
16 17
  "stateless", STATELESS;
17 18
  "if", IF;
18 19
  "then", THEN;
......
44 45
  "pre", PRE;
45 46
  "div", DIV;
46 47
  "const", CONST;
47
  "include", INCLUDE;
48
  (* "include", INCLUDE; *)
48 49
  "assert", ASSERT;
49 50
  "ensures", ENSURES;
50 51
  "requires", REQUIRES;
......
136 137
  let annot s =
137 138
    let lb = Lexing.from_string s in
138 139
   try
139
     ParserLustreSpec.lustre_annot token lb
140
     Parser_lustre.lustre_annot(* ParserLustreSpec.lustre_annot *) token lb
140 141
   with Parsing.Parse_error as _e -> (
141 142
     Format.eprintf "Lexing error at position %a:@.unexpected token %s@.@?"
142 143
       (fun fmt p -> Format.fprintf fmt "%s l%i c%i" p.Lexing.pos_fname p.Lexing.pos_lnum p.Lexing.pos_cnum) lb.Lexing.lex_curr_p
......
146 147

  
147 148
  let spec s =
148 149
    let lb = Lexing.from_string s in
149
    ParserLustreSpec.lustre_spec token lb
150
    Parser_lustre.lustre_spec (*ParserLustreSpec.lustre_spec*) token lb
150 151

  
151 152
}
src/liveness.ml
186 186

  
187 187
let find_compatible_local node var dead =
188 188
 (*Format.eprintf "find_compatible_local %s %s %a@." node.node_id var pp_iset dead;*)
189
  let typ = (Corelang.node_var var node).var_type in
190
  let eq_var = node_eq var node in
189
  let typ = (get_node_var var node).var_type in
190
  let eq_var = get_node_eq var node in
191 191
  let aliasable_inputs =
192 192
    match NodeDep.get_callee eq_var.eq_rhs with
193 193
    | None           -> []
src/lustreSpec.ml
1 1
open Format
2 2

  
3

  
4
let merge_expr_annot ann1 ann2 =
5
  match ann1, ann2 with
6
    | None, None -> assert false
7
    | Some _, None -> ann1
8
    | None, Some _ -> ann2
9
    | Some ann1, Some ann2 -> Some (ann1@ann2)
10

  
11

  
12 3
type ident = Utils.ident
4
type label = Utils.ident
13 5
type rat = Utils.rat
14 6
type tag = Utils.tag
15 7

  
16
type constant =
17
  | EConst_int of int
18
  | EConst_real of string
19
  | EConst_float of float
20
  | EConst_bool of bool
21
  | EConst_string of string
22

  
23 8
type type_dec =
24 9
    {ty_dec_desc: type_dec_desc;
25 10
     ty_dec_loc: Location.t}
......
54 39
     mutable var_clock: Clocks.clock_expr;
55 40
     var_loc: Location.t}
56 41

  
42
(** The core language and its ast. Every element of the ast contains its
43
    location in the program text. The type and clock of an ast element
44
    is mutable (and initialized to dummy values). This avoids to have to
45
    duplicate ast structures (e.g. ast, typed_ast, clocked_ast). *)
46

  
47

  
48
type constant =
49
  | Const_int of int
50
  | Const_real of string
51
  | Const_float of float
52
  | Const_array of constant list
53
  | Const_tag of label
54
  | Const_string of string (* used only for annotations *)
55
  | Const_struct of (label * constant) list
56

  
57
type quantifier_type = Exists | Forall
58

  
59

  
60

  
57 61
(* The tag of an expression is a unique identifier used to distinguish
58 62
   different instances of the same node *)
59
type eexpr =
63
type expr =
64
    {expr_tag: tag;
65
     expr_desc: expr_desc;
66
     mutable expr_type: Types.type_expr;
67
     mutable expr_clock: Clocks.clock_expr;
68
     mutable expr_delay: Delay.delay_expr;
69
     mutable expr_annot: expr_annot option;
70
     expr_loc: Location.t}
71

  
72
and expr_desc =
73
  | Expr_const of constant
74
  | Expr_ident of ident
75
  | Expr_tuple of expr list
76
  | Expr_ite   of expr * expr * expr
77
  | Expr_arrow of expr * expr
78
  | Expr_fby of expr * expr
79
  | Expr_array of expr list
80
  | Expr_access of expr * Dimension.dim_expr
81
  | Expr_power of expr * Dimension.dim_expr
82
  | Expr_pre of expr
83
  | Expr_when of expr * ident * label
84
  | Expr_merge of ident * (label * expr) list
85
  | Expr_appl of call_t
86
 and call_t = ident * expr * (ident * label) option 
87
     (* The third part denotes the reseting clock label and value *)
88
and 
89
  (* The tag of an expression is a unique identifier used to distinguish
90
     different instances of the same node *)
91
  eexpr =
60 92
    {eexpr_tag: tag;
61
     eexpr_desc: eexpr_desc;
93
     eexpr_qfexpr: expr;
94
     eexpr_quantifiers: (quantifier_type * var_decl list) list;
62 95
     mutable eexpr_type: Types.type_expr;
63 96
     mutable eexpr_clock: Clocks.clock_expr;
97
     mutable eexpr_normalized: (var_decl * eq list * var_decl list) option;
64 98
     eexpr_loc: Location.t}
65 99

  
66
and eexpr_desc =
67
  | EExpr_const of constant
68
  | EExpr_ident of ident
69
  | EExpr_tuple of eexpr list
70
  | EExpr_arrow of eexpr * eexpr
71
  | EExpr_fby of eexpr * eexpr
72
  (* | EExpr_concat of eexpr * eexpr *)
73
  (* | EExpr_tail of eexpr *)
74
  | EExpr_pre of eexpr
75
  | EExpr_when of eexpr * ident
76
  (* | EExpr_whennot of eexpr * ident *)
77
  | EExpr_merge of ident * eexpr * eexpr
78
  | EExpr_appl of ident * eexpr * ident option
79
  (* | EExpr_uclock of eexpr * int *)
80
  (* | EExpr_dclock of eexpr * int *)
81
  (* | EExpr_phclock of eexpr * rat *)
82
  | EExpr_exists of var_decl list * eexpr
83
  | EExpr_forall of var_decl list * eexpr
84

  
85
type ensures_t = EnsuresExpr of eexpr | SpecObserverNode of (string * eexpr list)
100
and expr_annot = {
101
  annots: (string list * eexpr) list;
102
  annot_loc: Location.t
103
}
104
and 
105
 eq =
106
    {eq_lhs: ident list;
107
     eq_rhs: expr;
108
     eq_loc: Location.t}
109

  
86 110

  
87 111
type node_annot = {
88 112
  requires: eexpr list;
89
  ensures: ensures_t list;
90
  behaviors: (string * eexpr list * ensures_t list) list
113
  ensures: eexpr list;
114
  behaviors: (string * eexpr list * eexpr list * Location.t) list;
115
  spec_loc: Location.t;
91 116
}
117
type assert_t = 
118
    {
119
      assert_expr: expr;
120
      assert_loc: Location.t
121
    } 
122

  
123
type node_desc =
124
    {node_id: ident;
125
     mutable node_type: Types.type_expr;
126
     mutable node_clock: Clocks.clock_expr;
127
     node_inputs: var_decl list;
128
     node_outputs: var_decl list;
129
     node_locals: var_decl list;
130
     mutable node_gencalls: expr list;
131
     mutable node_checks: Dimension.dim_expr list;
132
     node_asserts: assert_t list; 
133
     node_eqs: eq list;
134
     mutable node_dec_stateless: bool;
135
     mutable node_stateless: bool option;
136
     node_spec: node_annot option;
137
     node_annot: expr_annot list;
138
    }
139

  
140
type imported_node_desc =
141
    {nodei_id: ident;
142
     mutable nodei_type: Types.type_expr;
143
     mutable nodei_clock: Clocks.clock_expr;
144
     nodei_inputs: var_decl list;
145
     nodei_outputs: var_decl list;
146
     nodei_stateless: bool;
147
     nodei_spec: node_annot option;
148
     nodei_prototype: string option;
149
     nodei_in_lib: string option;
150
    }
151

  
152
type const_desc = 
153
    {const_id: ident; 
154
     const_loc: Location.t; 
155
     const_value: constant;      
156
     mutable const_type: Types.type_expr;
157
    }
158

  
159
type top_decl_desc =
160
| Node of node_desc
161
| Consts of const_desc list
162
| ImportedNode of imported_node_desc
163
| Open of bool * string (* the boolean set to true denotes a local 
164
			   lusi vs a lusi installed at system level *)
165

  
166
type top_decl =
167
    {top_decl_desc: top_decl_desc;
168
     top_decl_loc: Location.t}
169

  
170
type program = top_decl list
171

  
172
type error =
173
    Main_not_found
174
  | Main_wrong_kind
175
  | No_main_specified
176
  | Unbound_symbol of ident
177
  | Already_bound_symbol of ident
92 178

  
93 179

  
94
type expr_annot = (string list * eexpr) list 
95

  
96
let merge_node_annot ann1 ann2 =
97
  { requires = ann1.requires @ ann2.requires;
98
    ensures = ann1.ensures @ ann2.ensures;
99
    behaviors = ann1.behaviors @ ann2.behaviors;
100
  }
101

  
102
let mkeexpr loc d =
103
  { eexpr_tag = Utils.new_tag ();
104
    eexpr_desc = d;
105
    eexpr_type = Types.new_var ();
106
    eexpr_clock = Clocks.new_var true;
107
    eexpr_loc = loc }
108

  
109
let mkepredef_call loc funname args =
110
  mkeexpr loc (EExpr_appl (funname, mkeexpr loc (EExpr_tuple args), None))
111

  
112
let mkepredef_unary_call loc funname arg =
113
  mkeexpr loc (EExpr_appl (funname, arg, None))
114 180

  
115 181
(* Local Variables: *)
116 182
(* compile-command:"make -C .." *)
src/machine_code.ml
99 99
  mstatic: var_decl list; (* static inputs only *)
100 100
  mstep: step_t;
101 101
  mspec: node_annot option;
102
  mannot: expr_annot option;
102
  mannot: expr_annot list;
103 103
}
104 104

  
105 105
let pp_step fmt s =
......
170 170
    node_dec_stateless = false;
171 171
    node_stateless = Some false;
172 172
    node_spec = None;
173
    node_annot = None;  }
173
    node_annot = [];  }
174 174

  
175 175
let arrow_top_decl =
176 176
  {
......
202 202
                                 [MLocalAssign(var_output, LocalVar var_input2)] ]
203 203
    };
204 204
    mspec = None;
205
    mannot = None;
205
    mannot = [];
206 206
  }
207 207

  
208 208
let new_instance =
......
229 229
(*                       s : step instructions           *)
230 230
let translate_ident node (m, si, j, d, s) id =
231 231
  try (* id is a node var *)
232
    let var_id = node_var id node in
232
    let var_id = get_node_var id node in
233 233
    if ISet.exists (fun v -> v.var_id = id) m
234 234
    then StateVar var_id
235 235
    else LocalVar var_id
......
351 351
  (*Format.eprintf "translate_eq %a with clock %a@." Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock;*)
352 352
  match eq.eq_lhs, eq.eq_rhs.expr_desc with
353 353
  | [x], Expr_arrow (e1, e2)                     ->
354
    let var_x = node_var x node in
354
    let var_x = get_node_var x node in
355 355
    let o = new_instance node arrow_top_decl eq.eq_rhs.expr_tag in
356 356
    let c1 = translate_expr node args e1 in
357 357
    let c2 = translate_expr node args e2 in
......
360 360
     Utils.IMap.add o (arrow_top_decl, []) j,
361 361
     d,
362 362
     (control_on_clock node args eq.eq_rhs.expr_clock (MStep ([var_x], o, [c1;c2]))) :: s)
363
  | [x], Expr_pre e1 when ISet.mem (node_var x node) d     ->
364
    let var_x = node_var x node in
363
  | [x], Expr_pre e1 when ISet.mem (get_node_var x node) d     ->
364
    let var_x = get_node_var x node in
365 365
    (ISet.add var_x m,
366 366
     si,
367 367
     j,
368 368
     d,
369 369
     control_on_clock node args eq.eq_rhs.expr_clock (MStateAssign (var_x, translate_expr node args e1)) :: s)
370
  | [x], Expr_fby (e1, e2) when ISet.mem (node_var x node) d ->
371
    let var_x = node_var x node in
370
  | [x], Expr_fby (e1, e2) when ISet.mem (get_node_var x node) d ->
371
    let var_x = get_node_var x node in
372 372
    (ISet.add var_x m,
373 373
     MStateAssign (var_x, translate_expr node args e1) :: si,
374 374
     j,
......
376 376
     control_on_clock node args eq.eq_rhs.expr_clock (MStateAssign (var_x, translate_expr node args e2)) :: s)
377 377

  
378 378
  | p  , Expr_appl (f, arg, r) when not (Basic_library.is_internal_fun f) ->
379
    let var_p = List.map (fun v -> node_var v node) p in
379
    let var_p = List.map (fun v -> get_node_var v node) p in
380 380
    let el =
381 381
      match arg.expr_desc with
382 382
      | Expr_tuple el -> el
......
402 402
  | [x], Expr_ite   (c, t, e) 
403 403
    when (match !Options.output with | "horn" -> true | "C" | "java" | _ -> false)
404 404
      -> 
405
    let var_x = node_var x node in
405
    let var_x = get_node_var x node in
406 406
    (m, 
407 407
     si, 
408 408
     j, 
......
412 412
    )
413 413
      
414 414
  | [x], _                                       -> (
415
    let var_x = node_var x node in
415
    let var_x = get_node_var x node in
416 416
    (m, si, j, d, 
417 417
     control_on_clock 
418 418
       node
src/main_lustre_compiler.ml
26 26
open Format
27 27
open Log
28 28

  
29
open LustreSpec
30

  
29 31
let usage = "Usage: lustrec [options] <source-file>"
30 32

  
31 33
let extensions = [".ec"; ".lus"; ".lusi"]
......
170 172
  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. extracting dependencies@,");
171 173
  let dependencies = 
172 174
    List.fold_right 
173
      (fun d accu -> match d.Corelang.top_decl_desc with 
174
      | Corelang.Open (local, s) -> (s, local)::accu 
175
      (fun d accu -> match d.top_decl_desc with 
176
      | Open (local, s) -> (s, local)::accu 
175 177
      | _ -> accu) 
176 178
      prog [] 
177 179
  in
src/normalization.ml
74 74

  
75 75
(* Generate a new local [node] variable *)
76 76
let mk_fresh_var node loc ty ck =
77
  let vars = node_vars node in
77
  let vars = get_node_vars node in
78 78
  let rec aux () =
79 79
  incr cpt_fresh;
80 80
  let s = Printf.sprintf "__%s_%d" node.node_id !cpt_fresh in
......
240 240
    let defvars, norm_hl = normalize_branches node offsets defvars hl in
241 241
    let norm_expr = mk_norm_expr offsets expr (Expr_merge (c, norm_hl)) in
242 242
    mk_expr_alias_opt alias node defvars norm_expr
243
  | Expr_uclock _
244
  | Expr_dclock _ 
245
  | Expr_phclock _ -> assert false (* Not handled yet *)
243
  
246 244
(* Creates a conditional with a merge construct, which is more lazy *)
247 245
(*
248 246
let norm_conditional_as_merge alias node norm_expr offsets defvars expr =
src/optimize_prog.ml
1 1
open Corelang
2
open LustreSpec
2 3

  
3 4
(* Consts unfoooolding *)
4 5
let is_const i consts = 
......
28 29
  | Expr_pre e' -> Expr_pre (unfold e')
29 30
  | Expr_when (e', i, l)-> Expr_when (unfold e', i, l)
30 31
  | Expr_merge (i, hl) -> Expr_merge (i, List.map (fun (t, h) -> (t, unfold h)) hl)
31
  | Expr_appl (i, e', i') -> Expr_appl (i, unfold e', i')
32
  | Expr_uclock (e', i) -> Expr_uclock (unfold e', i) 
33
  | Expr_dclock (e', i) -> Expr_dclock (unfold e', i)
34
  | Expr_phclock _ -> e  
32
  | Expr_appl (i, e', i') -> Expr_appl (i, unfold e', i')  
35 33

  
36 34
let eq_unfold_consts consts eq =
37 35
  { eq with eq_rhs = expr_unfold_consts consts eq.eq_rhs }
......
74 72
    | Expr_when (e', i, l)-> distrib ((i, l)::stack) e'
75 73
    | Expr_merge (i, hl) -> { expr with expr_desc = Expr_merge (i, List.map (fun (t, h) -> (t, distrib stack h)) hl) }
76 74
    | Expr_appl (id, e', i') -> { expr with expr_desc = Expr_appl (id, distrib stack e', i')}
77
    | _ -> assert false
78 75
  in distrib [] expr
79 76

  
80 77
let eq_distribute_when eq =
src/parserLustreSpec.mly
3 3
  open Corelang
4 4
  open LustreSpec
5 5
  
6
  let mkexpr x = mkexpr (Location.symbol_rloc ()) x
7
  let mkpredef_call x = mkpredef_call (Location.symbol_rloc ()) x
8
  let mkpredef_unary_call x = mkpredef_unary_call (Location.symbol_rloc ()) x
9

  
6 10
  let mkeexpr x = mkeexpr (Location.symbol_rloc ()) x
11
  (*
7 12
  let mkepredef_call x = mkepredef_call (Location.symbol_rloc ()) x
8 13
  let mkepredef_unary_call x = mkepredef_unary_call (Location.symbol_rloc ()) x
9
  
14
  *)
15

  
10 16
  let mktyp x = mktyp (Location.symbol_rloc ()) x
11 17
  let mkvar_decl x = mkvar_decl (Location.symbol_rloc ()) x
12 18
  let mkclock x = mkclock (Location.symbol_rloc ()) x
......
71 77
 
72 78
requires:
73 79
{ [] }
74
| REQUIRES expr SCOL requires { $2::$4 }
80
| REQUIRES qexpr SCOL requires { $2::$4 }
75 81

  
76 82
ensures:
77 83
{ [] }
78
| ENSURES expr SCOL ensures { (EnsuresExpr $2) :: $4 }
79
| OBSERVER IDENT LPAR tuple_expr RPAR SCOL ensures { (SpecObserverNode($2,$4)) :: $7 }
84
| ENSURES qexpr SCOL ensures { (EnsuresExpr $2) :: $4 }
85
| OBSERVER IDENT LPAR tuple_qexpr RPAR SCOL ensures { (SpecObserverNode($2,$4)) :: $7 }
80 86

  
81 87
behaviors:
82 88
{ [] }
......
84 90

  
85 91
assumes:
86 92
{ [] }
87
| ASSUMES expr SCOL assumes { $2::$4 } 
93
| ASSUMES qexpr SCOL assumes { $2::$4 } 
94

  
95
tuple_qexpr:
96
| qexpr COMMA qexpr {[$3;$1]}
97
| tuple_qexpr COMMA qexpr {$3::$1}
98

  
88 99

  
89 100
tuple_expr:
90
| expr COMMA expr {[$3;$1]}
101
    expr COMMA expr {[$3;$1]}
91 102
| tuple_expr COMMA expr {$3::$1}
92 103

  
104
// Same as tuple expr but accepting lists with single element
105
array_expr:
106
  expr {[$1]}
107
| expr COMMA array_expr {$1::$3}
108

  
109
dim_list:
110
  dim RBRACKET { fun base -> mkexpr (Expr_access (base, $1)) }
111
| dim RBRACKET LBRACKET dim_list { fun base -> $4 (mkexpr (Expr_access (base, $1))) }
112

  
93 113
expr:
94
| const {mkeexpr (EExpr_const $1)} 
95
| IDENT 
96
    {mkeexpr (EExpr_ident $1)}
114
/* constants */
115
  INT {mkexpr (Expr_const (Const_int $1))}
116
| REAL {mkexpr (Expr_const (Const_real $1))}
117
| FLOAT {mkexpr (Expr_const (Const_float $1))}
118
/* Idents or type enum tags */
119
| IDENT {
120
  if Hashtbl.mem tag_table $1
121
  then mkexpr (Expr_const (Const_tag $1))
122
  else mkexpr (Expr_ident $1)}
123
| LPAR ANNOT expr RPAR
124
    {update_expr_annot $3 $2}
97 125
| LPAR expr RPAR
98 126
    {$2}
99 127
| LPAR tuple_expr RPAR
100
    {mkeexpr (EExpr_tuple (List.rev $2))}
128
    {mkexpr (Expr_tuple (List.rev $2))}
129

  
130
/* Array expressions */
131
| LBRACKET array_expr RBRACKET { mkexpr (Expr_array $2) }
132
| expr POWER dim { mkexpr (Expr_power ($1, $3)) }
133
| expr LBRACKET dim_list { $3 $1 }
134

  
135
/* Temporal operators */
136
| PRE expr 
137
    {mkexpr (Expr_pre $2)}
101 138
| expr ARROW expr 
102
    {mkeexpr (EExpr_arrow ($1,$3))}
139
    {mkexpr (Expr_arrow ($1,$3))}
103 140
| expr FBY expr 
104
    {mkeexpr (EExpr_fby ($1,$3))}
141
    {(*mkexpr (Expr_fby ($1,$3))*)
142
      mkexpr (Expr_arrow ($1, mkexpr (Expr_pre $3)))}
105 143
| expr WHEN IDENT 
106
    {mkeexpr (EExpr_when ($1,$3))}
107
| MERGE LPAR IDENT COMMA expr COMMA expr RPAR
108
    {mkeexpr (EExpr_merge ($3,$5,$7))}
144
    {mkexpr (Expr_when ($1,$3,tag_true))}
145
| expr WHENNOT IDENT
146
    {mkexpr (Expr_when ($1,$3,tag_false))}
147
| expr WHEN IDENT LPAR IDENT RPAR
148
    {mkexpr (Expr_when ($1, $5, $3))}
149
| MERGE IDENT handler_expr_list
150
    {mkexpr (Expr_merge ($2,$3))}
151

  
152
/* Applications */
109 153
| IDENT LPAR expr RPAR
110
    {mkeexpr (EExpr_appl ($1, $3, None))}
154
    {mkexpr (Expr_appl ($1, $3, None))}
111 155
| IDENT LPAR expr RPAR EVERY IDENT
112
    {mkeexpr (EExpr_appl ($1, $3, Some $6))}
156
    {mkexpr (Expr_appl ($1, $3, Some ($6, tag_true)))}
157
| IDENT LPAR expr RPAR EVERY IDENT LPAR IDENT RPAR
158
    {mkexpr (Expr_appl ($1, $3, Some ($8, $6))) }
113 159
| IDENT LPAR tuple_expr RPAR
114
    {mkeexpr (EExpr_appl ($1, mkeexpr (EExpr_tuple (List.rev $3)), None))}
160
    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), None))}
115 161
| IDENT LPAR tuple_expr RPAR EVERY IDENT
116
    {mkeexpr (EExpr_appl ($1, mkeexpr (EExpr_tuple (List.rev $3)), Some $6)) }
162
    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($6, tag_true))) }
163
| IDENT LPAR tuple_expr RPAR EVERY IDENT LPAR IDENT RPAR
164
    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($8, $6))) }
117 165

  
118 166
/* Boolean expr */
119 167
| expr AND expr 
120
    {mkepredef_call "&&" [$1;$3]}
168
    {mkpredef_call "&&" [$1;$3]}
121 169
| expr AMPERAMPER expr 
122
    {mkepredef_call "&&" [$1;$3]}
170
    {mkpredef_call "&&" [$1;$3]}
123 171
| expr OR expr 
124
    {mkepredef_call "||" [$1;$3]}
172
    {mkpredef_call "||" [$1;$3]}
125 173
| expr BARBAR expr 
126
    {mkepredef_call "||" [$1;$3]}
174
    {mkpredef_call "||" [$1;$3]}
127 175
| expr XOR expr 
128
    {mkepredef_call "xor" [$1;$3]}
176
    {mkpredef_call "xor" [$1;$3]}
129 177
| NOT expr 
130
    {mkepredef_unary_call "not" $2}
178
    {mkpredef_unary_call "not" $2}
131 179
| expr IMPL expr 
132
    {mkepredef_call "impl" [$1;$3]}
180
    {mkpredef_call "impl" [$1;$3]}
133 181

  
134 182
/* Comparison expr */
135 183
| expr EQ expr 
136
    {mkepredef_call "=" [$1;$3]}
184
    {mkpredef_call "=" [$1;$3]}
137 185
| expr LT expr 
138
    {mkepredef_call "<" [$1;$3]}
186
    {mkpredef_call "<" [$1;$3]}
139 187
| expr LTE expr 
140
    {mkepredef_call "<=" [$1;$3]}
188
    {mkpredef_call "<=" [$1;$3]}
141 189
| expr GT expr 
142
    {mkepredef_call ">" [$1;$3]}
190
    {mkpredef_call ">" [$1;$3]}
143 191
| expr GTE  expr 
144
    {mkepredef_call ">=" [$1;$3]}
192
    {mkpredef_call ">=" [$1;$3]}
145 193
| expr NEQ expr 
146
    {mkepredef_call "!=" [$1;$3]}
194
    {mkpredef_call "!=" [$1;$3]}
147 195

  
148 196
/* Arithmetic expr */
149 197
| expr PLUS expr 
150
    {mkepredef_call "+" [$1;$3]}
198
    {mkpredef_call "+" [$1;$3]}
151 199
| expr MINUS expr 
152
    {mkepredef_call "-" [$1;$3]}
200
    {mkpredef_call "-" [$1;$3]}
153 201
| expr MULT expr 
154
    {mkepredef_call "*" [$1;$3]}
202
    {mkpredef_call "*" [$1;$3]}
155 203
| expr DIV expr 
156
    {mkepredef_call "/" [$1;$3]}
204
    {mkpredef_call "/" [$1;$3]}
157 205
| MINUS expr %prec UMINUS
158
    {mkepredef_unary_call "uminus" $2}
206
  {mkpredef_unary_call "uminus" $2}
159 207
| expr MOD expr 
160
    {mkepredef_call "mod" [$1;$3]}
161

  
162
/* Temp op */
163
| PRE expr 
164
    {mkeexpr (EExpr_pre $2)}
208
    {mkpredef_call "mod" [$1;$3]}
165 209

  
166 210
/* If */
167 211
| IF expr THEN expr ELSE expr
168
    {mkepredef_call "ite" [$2;$4;$6]}
212
    {mkexpr (Expr_ite ($2, $4, $6))}
213

  
214

  
215
handler_expr_list:
216
   { [] }
217
| handler_expr handler_expr_list { $1 :: $2 }
218

  
219
handler_expr:
220
 LPAR IDENT ARROW expr RPAR { ($2, $4) }
169 221

  
170
/* Quantifiers */
171
| EXISTS vdecl SCOL expr %prec prec_exists {mkeexpr (EExpr_exists ($2, $4))} 
172
| FORALL vdecl SCOL expr %prec prec_forall {mkeexpr (EExpr_forall ($2, $4))}
222
qexpr:
223
| expr { mkeexpr [] $1 }
224
  /* Quantifiers */
225
| EXISTS vdecl SCOL qexpr %prec prec_exists { extend_eepxr (Exists, $2) $4 } 
226
| FORALL vdecl SCOL qexpr %prec prec_forall { extend_eepxr (Forall, $2) $4 }
173 227

  
174 228
vdecl:
175 229
| ident_list COL typ clock 
......
214 268

  
215 269

  
216 270
const:
217
| INT {EConst_int $1}
218
| REAL {EConst_real $1}
219
| FLOAT {EConst_float $1}
220
| TRUE {EConst_bool true}
221
| FALSE {EConst_bool false}
222
| STRING {EConst_string $1}
271
| INT {Const_int $1}
272
| REAL {Const_real $1}
273
| FLOAT {Const_float $1}
274
| TRUE {Const_bool true}
275
| FALSE {Const_bool false}
276
| STRING {Const_string $1}
223 277

  
224 278
lustre_annot:
225 279
lustre_annot_list EOF { $1 }
src/parser_lustre.mly
26 26
open Dimension
27 27
open Utils
28 28

  
29
let mktyp x = mktyp (Location.symbol_rloc ()) x
30
let mkclock x = mkclock (Location.symbol_rloc ()) x
31
let mkvar_decl x = mkvar_decl (Location.symbol_rloc ()) x
32
let mkexpr x = mkexpr (Location.symbol_rloc ()) x
33
let mkeq x = mkeq (Location.symbol_rloc ()) x
34
let mkassert x = mkassert (Location.symbol_rloc ()) x
35
let mktop_decl x = mktop_decl (Location.symbol_rloc ()) x
36
let mkpredef_call x = mkpredef_call (Location.symbol_rloc ()) x
37

  
38
let mkdim_int i = mkdim_int (Location.symbol_rloc ()) i
39
let mkdim_bool b = mkdim_bool (Location.symbol_rloc ()) b
40
let mkdim_ident id = mkdim_ident (Location.symbol_rloc ()) id
41
let mkdim_appl f args = mkdim_appl (Location.symbol_rloc ()) f args
42
let mkdim_ite i t e = mkdim_ite (Location.symbol_rloc ()) i t e
29
let get_loc () = Location.symbol_rloc ()
30
let mktyp x = mktyp (get_loc ()) x
31
let mkclock x = mkclock (get_loc ()) x
32
let mkvar_decl x = mkvar_decl (get_loc ()) x
33
let mkexpr x = mkexpr (get_loc ()) x
34
let mkeexpr x = mkeexpr (get_loc ()) x 
35
let mkeq x = mkeq (get_loc ()) x
36
let mkassert x = mkassert (get_loc ()) x
37
let mktop_decl x = mktop_decl (get_loc ()) x
38
let mkpredef_call x = mkpredef_call (get_loc ()) x
39
(*let mkpredef_unary_call x = mkpredef_unary_call (get_loc ()) x*)
40

  
41
let mkdim_int i = mkdim_int (get_loc ()) i
42
let mkdim_bool b = mkdim_bool (get_loc ()) b
43
let mkdim_ident id = mkdim_ident (get_loc ()) id
44
let mkdim_appl f args = mkdim_appl (get_loc ()) f args
45
let mkdim_ite i t e = mkdim_ite (get_loc ()) i t e
46

  
47
let mkannots annots = { annots = annots; annot_loc = get_loc () }
43 48

  
44 49
let add_node loc own msg hashtbl name value =
45 50
  try
46 51
    match (Hashtbl.find hashtbl name).top_decl_desc, value.top_decl_desc with
47 52
    | Node _        , ImportedNode _ when own   -> ()
48 53
    | ImportedNode _, _                         -> Hashtbl.add hashtbl name value
49
    | Node _        , _                         -> raise (Corelang.Error (loc, Corelang.Already_bound_symbol msg))
54
    | Node _        , _                         -> raise (Error (loc, Already_bound_symbol msg))
50 55
    | _                                         -> assert false
51 56
  with
52 57
    Not_found                                   -> Hashtbl.add hashtbl name value
......
54 59

  
55 60
let add_symbol loc msg hashtbl name value =
56 61
 if Hashtbl.mem hashtbl name
57
 then raise (Corelang.Error (loc, Corelang.Already_bound_symbol msg))
62
 then raise (Error (loc, Already_bound_symbol msg))
58 63
 else Hashtbl.add hashtbl name value
59 64

  
60 65
let check_symbol loc msg hashtbl name =
61 66
 if not (Hashtbl.mem hashtbl name)
62
 then raise (Corelang.Error (loc, Corelang.Unbound_symbol msg))
67
 then raise (Error (loc, Unbound_symbol msg))
63 68
 else ()
64 69

  
70
let check_node_symbol msg name value =
71
 if Hashtbl.mem node_table name
72
 then () (* TODO: should we check the types here ? *)
73
 else Hashtbl.add node_table name value
74

  
65 75
%}
66 76

  
67 77
%token <int> INT
68 78
%token <string> REAL
69 79
%token <float> FLOAT
80
%token <string> STRING
70 81
%token AUTOMATON STATE UNTIL UNLESS RESTART RESUME LAST
71 82
%token STATELESS ASSERT OPEN QUOTE FUNCTION
72 83
%token <string> IDENT
......
86 97
%token MULT DIV MOD
87 98
%token MINUS PLUS UMINUS
88 99
%token PRE ARROW
100
%token REQUIRES ENSURES OBSERVER
101
%token INVARIANT BEHAVIOR ASSUMES
102
%token EXISTS FORALL
89 103
%token PROTOTYPE LIB
90 104
%token EOF
91 105

  
106
%nonassoc prec_exists prec_forall
92 107
%nonassoc COMMA
93 108
%left MERGE IF
94 109
%nonassoc ELSE
......
110 125
%nonassoc LBRACKET
111 126

  
112 127
%start prog
113
%type <Corelang.top_decl list> prog
128
%type <LustreSpec.top_decl list> prog
129

  
114 130
%start header
115
%type <bool -> Corelang.top_decl list> header
131
%type <bool -> LustreSpec.top_decl list> header
132

  
133
%start lustre_annot
134
%type <LustreSpec.expr_annot> lustre_annot
135

  
136
%start lustre_spec
137
%type <LustreSpec.node_annot> lustre_spec
116 138

  
117 139
%%
118 140

  
......
157 179
			     nodei_prototype = $13;
158 180
			     nodei_in_lib = $14;})
159 181
    in
160
    (let loc = Location.symbol_rloc () in 
161
     fun own -> add_node loc own ("node " ^ $3) node_table $3 nd; nd) }
182
     check_node_symbol ("node " ^ $3) $3 nd; 
183
     let loc = get_loc () in
184
     (fun own -> add_node loc own ("node " ^ $3) node_table $3 nd; nd) }
162 185

  
163 186
prototype_opt:
164 187
 { None }
......
186 209
			     node_dec_stateless = $2;
187 210
			     node_stateless = None;
188 211
			     node_spec = $1;
189
			     node_annot = match annots with [] -> None | _ -> Some annots})
212
			     node_annot = annots})
190 213
     in
191 214
     let loc = Location.symbol_rloc () in
192 215
     add_node loc true ("node " ^ $3) node_table $3 nd; nd}
193 216

  
194 217
nodespec_list:
195 218
 { None }
196
| NODESPEC nodespec_list { (function None -> (fun s1 -> Some s1) | Some s2 -> (fun s1 -> Some (LustreSpec.merge_node_annot s1 s2))) $2 $1 }
219
| NODESPEC nodespec_list { 
220
  (function 
221
  | None    -> (fun s1 -> Some s1) 
222
  | Some s2 -> (fun s1 -> Some (merge_node_annot s1 s2))) $2 $1 }
197 223

  
198 224
typ_def_list:
199 225
    /* empty */ {}
......
203 229
  TYPE IDENT EQ typeconst {
204 230
    try
205 231
      let loc = Location.symbol_rloc () in
206
      add_symbol loc ("type " ^ $2) type_table (Tydec_const $2) (Corelang.get_repr_type $4)
232
      add_symbol loc ("type " ^ $2) type_table (Tydec_const $2) (get_repr_type $4)
207 233
    with Not_found-> assert false }
208 234
| TYPE IDENT EQ ENUM LCUR tag_list RCUR { Hashtbl.add type_table (Tydec_const $2) (Tydec_enum ($6 (Tydec_const $2))) }
209 235
| TYPE IDENT EQ STRUCT LCUR field_list RCUR { Hashtbl.add type_table (Tydec_const $2) (Tydec_struct ($6 (Tydec_const $2))) }
......
245 271
  { [], [], [] }
246 272
| eq eq_list {let eql, assertl, annotl = $2 in ($1::eql), assertl, annotl}
247 273
| assert_ eq_list {let eql, assertl, annotl = $2 in eql, ($1::assertl), annotl}
248
| ANNOT eq_list {let eql, assertl, annotl = $2 in eql, assertl, $1@annotl}
274
| ANNOT eq_list {let eql, assertl, annotl = $2 in eql, assertl, $1::annotl}
249 275
| automaton eq_list {let eql, assertl, annotl = $2 in ($1::eql), assertl, annotl}
250 276

  
251 277
automaton:
......
281 307
       ident_list      EQ expr SCOL {mkeq (List.rev $1,$3)}
282 308
| LPAR ident_list RPAR EQ expr SCOL {mkeq (List.rev $2,$5)}
283 309

  
310
lustre_spec:
311
| contract EOF { $1 }
312

  
313
contract:
314
requires ensures behaviors { { requires = $1; ensures = $2; behaviors = $3; spec_loc = get_loc () } }
315
 
316
requires:
317
{ [] }
... This diff was truncated because it exceeds the maximum size that can be displayed.

Also available in: Unified diff