Revision ca7ff3f7
Added by LĂ©lio Brun over 1 year ago
src/corelang.mli  

9  9 
(* *) 
10  10 
(********************************************************************) 
11  11  
12  
13  12 
open Lustre_types 
14  13  
15 
module VDeclModule: sig 

14 
module VDeclModule : sig


16  15 
type t 
17 
val compare: t > t > int 

18 
end with type t = Lustre_types.var_decl 

19  16  
20 
module VSet: sig 

17 
val compare : t > t > int 

18 
end 

19 
with type t = Lustre_types.var_decl 

20  
21 
module VSet : sig 

21  22 
include Set.S 
22 
val pp: Format.formatter > t > unit 

23 
val get: ident > t > elt 

24 
end with type elt = Lustre_types.var_decl 

25 


26 
val dummy_type_dec: type_dec 

27 
val dummy_clock_dec: clock_dec 

28  
29 
val mktyp: Location.t > type_dec_desc > type_dec 

30 
val mkclock: Location.t > clock_dec_desc > clock_dec 

31 
val mkvar_decl: Location.t > ?orig:bool > 

32 
ident * 

33 
type_dec * 

34 
clock_dec * 

35 
bool (* is const *) * 

36 
expr option (* value *) * 

37 
string option (* parent id *) 

38 
> var_decl 

39  
40 
val dummy_var_decl: ident > Types.type_expr > var_decl 

41  
42 
val var_decl_of_const: ?parentid:ident option > const_desc > var_decl 

43 
val mkexpr: Location.t > expr_desc > expr 

44 
val mkeq: Location.t > ident list * expr > eq 

45 
val mkassert: Location.t > expr > assert_t 

46 
val mktop_decl: Location.t > ident > bool > top_decl_desc > top_decl 

47 
val mkpredef_call: Location.t > ident > expr list > expr 

48 
val mk_new_name: (ident > bool) > ident > ident 

49 
val mk_new_node_name: node_desc > ident > ident 

50 
val mktop: top_decl_desc > top_decl 

23  
24 
val pp : Format.formatter > t > unit 

25  
26 
val get : ident > t > elt 

27 
end 

28 
with type elt = Lustre_types.var_decl 

29  
30 
val dummy_type_dec : type_dec 

31  
32 
val dummy_clock_dec : clock_dec 

33  
34 
val mktyp : Location.t > type_dec_desc > type_dec 

35  
36 
val mkclock : Location.t > clock_dec_desc > clock_dec 

37  
38 
val mkvar_decl : 

39 
Location.t > 

40 
?orig:bool > 

41 
ident 

42 
* type_dec 

43 
* clock_dec 

44 
* bool (* is const *) 

45 
* expr option 

46 
(* value *) 

47 
* string option 

48 
(* parent id *) > 

49 
var_decl 

50  
51 
val dummy_var_decl : ident > Types.type_expr > var_decl 

52  
53 
val var_decl_of_const : ?parentid:ident option > const_desc > var_decl 

54  
55 
val mkexpr : Location.t > expr_desc > expr 

56  
57 
val mkeq : Location.t > ident list * expr > eq 

58  
59 
val mkassert : Location.t > expr > assert_t 

60  
61 
val mktop_decl : Location.t > ident > bool > top_decl_desc > top_decl 

62  
63 
val mkpredef_call : Location.t > ident > expr list > expr 

64  
65 
val mk_new_name : (ident > bool) > ident > ident 

66  
67 
val mk_new_node_name : node_desc > ident > ident 

68  
69 
val mktop : top_decl_desc > top_decl 

51  70  
52  71 
(* constructor for machine types *) 
53 
val mkinstr: (* ?lustre_expr:expr > *)?lustre_eq: eq > ?instr_spec: Machine_code_types.value_t Spec_types.formula_t list > Machine_code_types.instr_t_desc > Machine_code_types.instr_t 

54 
val get_instr_desc: Machine_code_types.instr_t > Machine_code_types.instr_t_desc 

55 
val update_instr_desc: Machine_code_types.instr_t > Machine_code_types.instr_t_desc > Machine_code_types.instr_t 

56 


72 
val mkinstr : 

73 
?lustre_eq:(* ?lustre_expr:expr > *) 

74 
eq > 

75 
?instr_spec:Machine_code_types.value_t Spec_types.formula_t list > 

76 
Machine_code_types.instr_t_desc > 

77 
Machine_code_types.instr_t 

78  
79 
val get_instr_desc : 

80 
Machine_code_types.instr_t > Machine_code_types.instr_t_desc 

81  
82 
val update_instr_desc : 

83 
Machine_code_types.instr_t > 

84 
Machine_code_types.instr_t_desc > 

85 
Machine_code_types.instr_t 

86  
57  87 
(*val node_table : (ident, top_decl) Hashtbl.t*) 
58 
val print_node_table: Format.formatter > unit > unit 

59 
val node_name: top_decl > ident 

60 
val node_inputs: top_decl > var_decl list 

61 
val node_from_name: ident > top_decl 

62 
val update_node: ident > top_decl > unit 

63 
val is_generic_node: top_decl > bool 

64 
val is_imported_node: top_decl > bool 

65 
val is_contract: top_decl > bool 

66 
val is_node_contract: node_desc > bool 

67 
val get_node_contract: node_desc > contract_desc 

68 


69 
val consts_table: (ident, top_decl) Hashtbl.t 

70 
val print_consts_table: Format.formatter > unit > unit 

71 
val type_table: (type_dec_desc, top_decl) Hashtbl.t 

72 
val print_type_table: Format.formatter > unit > unit 

73 
val is_clock_dec_type: type_dec_desc > bool 

74 
val get_repr_type: type_dec_desc > type_dec_desc 

75 
val is_user_type: type_dec_desc > bool 

76 
val coretype_equal: type_dec_desc > type_dec_desc > bool 

77 
val tag_default: label 

78 
val tag_table: (label, top_decl) Hashtbl.t 

79 
val field_table: (label, top_decl) Hashtbl.t 

80  
81 
val get_enum_type_tags: type_dec_desc > label list 

82  
83 
val get_struct_type_fields: type_dec_desc > (label * type_dec_desc) list 

84  
85 
val consts_of_enum_type: top_decl > top_decl list 

86  
87 
val const_of_bool: bool > constant 

88 
val const_is_bool: constant > bool 

89 
val const_negation: constant > constant 

90 
val const_or: constant > constant > constant 

91 
val const_and: constant > constant > constant 

92 
val const_xor: constant > constant > constant 

93 
val const_impl: constant > constant > constant 

94  
95 
val get_var: ident > var_decl list > var_decl 

96 
val get_node_vars: node_desc > var_decl list 

97 
val get_node_var: ident > node_desc > var_decl 

98 
val get_node_eqs: node_desc > eq list * automata_desc list 

99 
val get_node_eq: ident > node_desc > eq 

100 
val get_node_interface: node_desc > imported_node_desc 

88 
val print_node_table : Format.formatter > unit > unit 

89  
90 
val node_name : top_decl > ident 

91  
92 
val node_inputs : top_decl > var_decl list 

93  
94 
val node_from_name : ident > top_decl 

95  
96 
val update_node : ident > top_decl > unit 

97  
98 
val is_generic_node : top_decl > bool 

99  
100 
val is_imported_node : top_decl > bool 

101  
102 
val is_contract : top_decl > bool 

103  
104 
val is_node_contract : node_desc > bool 

105  
106 
val get_node_contract : node_desc > contract_desc 

107  
108 
val consts_table : (ident, top_decl) Hashtbl.t 

109  
110 
val print_consts_table : Format.formatter > unit > unit 

111  
112 
val type_table : (type_dec_desc, top_decl) Hashtbl.t 

113  
114 
val print_type_table : Format.formatter > unit > unit 

115  
116 
val is_clock_dec_type : type_dec_desc > bool 

117  
118 
val get_repr_type : type_dec_desc > type_dec_desc 

119  
120 
val is_user_type : type_dec_desc > bool 

121  
122 
val coretype_equal : type_dec_desc > type_dec_desc > bool 

123  
124 
val tag_default : label 

125  
126 
val tag_table : (label, top_decl) Hashtbl.t 

127  
128 
val field_table : (label, top_decl) Hashtbl.t 

129  
130 
val get_enum_type_tags : type_dec_desc > label list 

131  
132 
val get_struct_type_fields : type_dec_desc > (label * type_dec_desc) list 

133  
134 
val consts_of_enum_type : top_decl > top_decl list 

135  
136 
val const_of_bool : bool > constant 

137  
138 
val const_is_bool : constant > bool 

139  
140 
val const_negation : constant > constant 

141  
142 
val const_or : constant > constant > constant 

143  
144 
val const_and : constant > constant > constant 

145  
146 
val const_xor : constant > constant > constant 

147  
148 
val const_impl : constant > constant > constant 

149  
150 
val get_var : ident > var_decl list > var_decl 

151  
152 
val get_node_vars : node_desc > var_decl list 

153  
154 
val get_node_var : ident > node_desc > var_decl 

155  
156 
val get_node_eqs : node_desc > eq list * automata_desc list 

157  
158 
val get_node_eq : ident > node_desc > eq 

159  
160 
val get_node_interface : node_desc > imported_node_desc 

101  161  
102  162 
(* val get_const: ident > constant *) 
103  163  
104  164 
val sort_handlers : (label * 'a) list > (label * 'a) list 
105  165  
106 
val is_eq_expr: expr > expr > bool 

166 
val is_eq_expr : expr > expr > bool


107  167  
108 
(* val pp_error : Format.formatter > error > unit *)


168 
(* val pp_error : Format.formatter > error > unit *) 

109  169  
110  170 
(* Caution, returns an untyped, unclocked, etc, expression *) 
111  171 
val is_tuple_expr : expr > bool 
172  
112  173 
val ident_of_expr : expr > ident 
174  
113  175 
val expr_of_vdecl : var_decl > expr 
176  
114  177 
val expr_of_ident : ident > Location.t > expr 
178  
115  179 
val expr_list_of_expr : expr > expr list 
180  
116  181 
val expr_of_expr_list : Location.t > expr list > expr 
117 
val call_of_expr: expr > (ident * expr list * expr option) 

118 
val expr_of_dimension: Dimension.dim_expr > expr 

119 
val dimension_of_expr: expr > Dimension.dim_expr 

120 
val dimension_of_const: Location.t > constant > Dimension.dim_expr 

121 
val expr_to_eexpr: expr > eexpr 

122 
(* REMOVED, pushed in utils.ml val new_tag : unit > tag *) 

123  182  
124 
val add_internal_funs: unit > unit 

183 
val call_of_expr : expr > ident * expr list * expr option 

184  
185 
val expr_of_dimension : Dimension.dim_expr > expr 

186  
187 
val dimension_of_expr : expr > Dimension.dim_expr 

188  
189 
val dimension_of_const : Location.t > constant > Dimension.dim_expr 

190  
191 
val expr_to_eexpr : expr > eexpr 

192 
(* REMOVED, pushed in utils.ml val new_tag : unit > tag *) 

193  
194 
val add_internal_funs : unit > unit 

125  195  
126  196 
val pp_prog_type : Format.formatter > program_t > unit 
127  197  
128  198 
val pp_prog_clock : Format.formatter > program_t > unit 
129  199  
130 
val const_of_top: top_decl > const_desc 

131 
val node_of_top: top_decl > node_desc 

132 
val imported_node_of_top: top_decl > imported_node_desc 

133 
val typedef_of_top: top_decl > typedef_desc 

134 
val dependency_of_top: top_decl > (bool * ident) 

200 
val const_of_top : top_decl > const_desc 

201  
202 
val node_of_top : top_decl > node_desc 

203  
204 
val imported_node_of_top : top_decl > imported_node_desc 

205  
206 
val typedef_of_top : top_decl > typedef_desc 

207  
208 
val dependency_of_top : top_decl > bool * ident 

135  209  
136  210 
val get_nodes : program_t > top_decl list 
211  
137  212 
val get_imported_nodes : program_t > top_decl list 
213  
138  214 
val get_consts : program_t > top_decl list 
139 
val get_typedefs: program_t > top_decl list 

215  
216 
val get_typedefs : program_t > top_decl list 

217  
140  218 
val get_dependencies : program_t > top_decl list 
141  219 
(* val prog_unfold_consts: program_t > program_t *) 
142  220  
143 
(** Returns the node named ident in the provided program. Raise Not_found *) 

144  221 
val get_node : ident > program_t > node_desc 
222 
(** Returns the node named ident in the provided program. Raise Not_found *) 

223  
224 
val rename_static : 

225 
(ident > Dimension.dim_expr) > type_dec_desc > type_dec_desc 

145  226  
146 


147 
val rename_static: (ident > Dimension.dim_expr) > type_dec_desc > type_dec_desc 

148 
val rename_carrier: (ident > ident) > clock_dec_desc > clock_dec_desc 

227 
val rename_carrier : (ident > ident) > clock_dec_desc > clock_dec_desc 

149  228  
150 
val get_expr_vars: expr > Utils.ISet.t 

229 
val get_expr_vars : expr > Utils.ISet.t


151  230 
(*val expr_replace_var: (ident > ident) > expr > expr*) 
152  231  
153 
val eq_replace_rhs_var: (ident > bool) > (ident > ident) > eq > eq 

232 
val eq_replace_rhs_var : (ident > bool) > (ident > ident) > eq > eq


154  233  
155 
(** val rename_expr f_node f_var expr *) 

156  234 
val rename_expr : (ident > ident) > (ident > ident) > expr > expr 
235 
(** val rename_expr f_node f_var expr *) 

157  236  
158 
(** val rename_eq f_node f_var eq *) 

159  237 
val rename_eq : (ident > ident) > (ident > ident) > eq > eq 
238 
(** val rename_eq f_node f_var eq *) 

160  239  
240 
val rename_aut : 

241 
(ident > ident) > (ident > ident) > automata_desc > automata_desc 

161  242 
(** val rename_aut f_node f_var aut *) 
162 
val rename_aut : (ident > ident) > (ident > ident) > automata_desc > automata_desc 

163  243  
244 
val rename_prog : 

245 
(ident > ident) > 

246 
(ident > ident) > 

247 
(ident > ident) > 

248 
program_t > 

249 
program_t 

164  250 
(** rename_prog f_node f_var f_const prog *) 
165 
val rename_prog: (ident > ident) > (ident > ident) > (ident > ident) > program_t > program_t 

166 
val rename_node: (ident > ident) > (ident > ident) > node_desc > node_desc 

167  251  
168 
val substitute_expr: var_decl list > eq list > expr > expr 

252 
val rename_node : (ident > ident) > (ident > ident) > node_desc > node_desc 

253  
254 
val substitute_expr : var_decl list > eq list > expr > expr 

255  
256 
val copy_var_decl : var_decl > var_decl 

257  
258 
val copy_const : const_desc > const_desc 

169  259  
170 
val copy_var_decl: var_decl > var_decl 

171 
val copy_const: const_desc > const_desc 

172 
val copy_node: node_desc > node_desc 

173 
val copy_top: top_decl > top_decl 

174 
val copy_prog: top_decl list > top_decl list 

260 
val copy_node : node_desc > node_desc 

175  261  
262 
val copy_top : top_decl > top_decl 

263  
264 
val copy_prog : top_decl list > top_decl list 

265  
266 
val mkeexpr : Location.t > expr > eexpr 

176  267 
(** Annotation expression related functions *) 
177 
val mkeexpr: Location.t > expr > eexpr 

178 
val empty_contract: contract_desc 

179 
val mk_contract_var: ident > bool > type_dec option > expr > Location.t > contract_desc 

180 
val mk_contract_guarantees: string option > eexpr > contract_desc 

181 
val mk_contract_assume: string option > eexpr > contract_desc 

182 
val mk_contract_mode: ident > eexpr list > eexpr list > Location.t > contract_desc 

183 
val mk_contract_import: ident > expr > expr > Location.t > contract_desc 

184 
val merge_contracts: contract_desc > contract_desc > contract_desc 

185 
val extend_eexpr: (quantifier_type * var_decl list) list > eexpr > eexpr 

186 
val update_expr_annot: ident > expr > expr_annot > expr 

268  
269 
val empty_contract : contract_desc 

270  
271 
val mk_contract_var : 

272 
ident > bool > type_dec option > expr > Location.t > contract_desc 

273  
274 
val mk_contract_guarantees : string option > eexpr > contract_desc 

275  
276 
val mk_contract_assume : string option > eexpr > contract_desc 

277  
278 
val mk_contract_mode : 

279 
ident > eexpr list > eexpr list > Location.t > contract_desc 

280  
281 
val mk_contract_import : ident > expr > expr > Location.t > contract_desc 

282  
283 
val merge_contracts : contract_desc > contract_desc > contract_desc 

284  
285 
val extend_eexpr : (quantifier_type * var_decl list) list > eexpr > eexpr 

286  
287 
val update_expr_annot : ident > expr > expr_annot > expr 

187  288 
(* val mkpredef_call: Location.t > ident > eexpr list > eexpr*) 
188  289  
189 
val expr_contains_expr: tag > expr > bool 

290 
val expr_contains_expr : tag > expr > bool 

291  
292 
val reset_cpt_fresh : unit > unit 

190  293  
191 
val reset_cpt_fresh: unit > unit 

192 


193 
(* mk_fresh_var parentid to be registered as parent_nodeid, vars is the list of existing vars in that context *) 

194 
val mk_fresh_var: (ident * var_decl list) > Location.t > Types.type_expr > Clocks.clock_expr > var_decl 

294 
(* mk_fresh_var parentid to be registered as parent_nodeid, vars is the list of 

295 
existing vars in that context *) 

296 
val mk_fresh_var : 

297 
ident * var_decl list > 

298 
Location.t > 

299 
Types.type_expr > 

300 
Clocks.clock_expr > 

301 
var_decl 

195  302  
196 
val find_eq: ident list > eq list > eq * eq list 

303 
val find_eq : ident list > eq list > eq * eq list


197  304  
198 
val get_expr_calls: top_decl list > expr > Utils.ISet.t 

305 
val get_expr_calls : top_decl list > expr > Utils.ISet.t


199  306  
200  307 
(* val eq_has_arrows: eq > bool *) 
201  308  
202 
val push_negations: ?neg:bool > expr > expr 

309 
val push_negations : ?neg:bool > expr > expr


203  310  
204 
val add_pre_expr: ident list > expr > expr 

311 
val add_pre_expr : ident list > expr > expr


205  312  
206 
val mk_eq: Location.t > expr > expr > expr


313 
val mk_eq : Location.t > expr > expr > expr


207  314  
208  315 
(* Simple transformations: eg computation over constants *) 
209 
val partial_eval: expr > expr 

316 
val partial_eval : expr > expr


210  317  
211 
(* Local Variables: *)


318 
(* Local Variables: *) 

212  319 
(* compilecommand:"make C .." *) 
213  320 
(* End: *) 
Also available in: Unified diff
reformatting