Project

General

Profile

Revision 0038002e src/corelang.ml

View differences:

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: *)

Also available in: Unified diff