Revision 01c7d5e1 src/corelang.ml
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