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 
(* compilecommand:"make C .." *) 
729  710 
(* End: *) 
Also available in: Unified diff