Project

General

Profile

Revision a28d1ba7 src/corelang.ml

View differences:

src/corelang.ml
792 792
  Utils.fprintf_list ~sep:"" pp_decl_clock fmt prog
793 793

  
794 794
let pp_error fmt = function
795
    Main_not_found ->
796
      fprintf fmt "Cannot compile node %s: could not find the node definition.@."
795
  | Main_not_found ->
796
      fprintf fmt "cannot compile node %s: could not find the node definition.@."
797 797
	!Options.main_node
798 798
  | Main_wrong_kind ->
799 799
    fprintf fmt
800
      "Name %s does not correspond to a (non-imported) node definition.@." 
800
      "name %s does not correspond to a (non-imported) node definition.@." 
801 801
      !Options.main_node
802 802
  | No_main_specified ->
803
    fprintf fmt "No main node specified@."
803
    fprintf fmt "no main node specified.@."
804 804
  | Unbound_symbol sym ->
805 805
    fprintf fmt
806 806
      "%s is undefined.@."
......
811 811
      sym
812 812
  | Unknown_library sym ->
813 813
    fprintf fmt
814
      "impossible to load library %s.lusic@.Please compile the corresponding interface or source file.@."
814
      "impossible to load library %s.lusic.@.Please compile the corresponding interface or source file.@."
815 815
      sym
816 816
  | Wrong_number sym ->
817 817
    fprintf fmt
818
      "library %s.lusic has a different version number and may crash compiler@.Please recompile the corresponding interface or source file.@."
818
      "library %s.lusic has a different version number and may crash compiler.@.Please recompile the corresponding interface or source file.@."
819 819
      sym
820 820

  
821 821
(* filling node table with internal functions *)
......
1004 1004
and node_has_arrows node =
1005 1005
  List.exists (fun eq -> eq_has_arrows eq) (get_node_eqs node)
1006 1006

  
1007
let mkvar_decl loc ?(orig=false) (id, ty_dec, ck_dec, is_const, value) =
1008
  assert (value = None || is_const);
1009
  { var_id = id;
1010
    var_orig = orig;
1011
    var_dec_type = ty_dec;
1012
    var_dec_clock = ck_dec;
1013
    var_dec_const = is_const;
1014
    var_dec_value = value;
1015
    var_type = Types.new_var ();
1016
    var_clock = Clocks.new_var true;
1017
    var_loc = loc }
1018

  
1019
let mkexpr loc d =
1020
  { expr_tag = Utils.new_tag ();
1021
    expr_desc = d;
1022
    expr_type = Types.new_var ();
1023
    expr_clock = Clocks.new_var true;
1024
    expr_delay = Delay.new_var ();
1025
    expr_annot = None;
1026
    expr_loc = loc }
1027

  
1028
let var_decl_of_const c =
1029
  { var_id = c.const_id;
1030
    var_orig = true;
1031
    var_dec_type = { ty_dec_loc = c.const_loc; ty_dec_desc = Tydec_any };
1032
    var_dec_clock = { ck_dec_loc = c.const_loc; ck_dec_desc = Ckdec_any };
1033
    var_dec_const = true;
1034
    var_dec_value = None;
1035
    var_type = c.const_type;
1036
    var_clock = Clocks.new_var false;
1037
    var_loc = c.const_loc }
1038

  
1039
let mk_new_name used id =
1040
  let rec new_name name cpt =
1041
    if used name
1042
    then new_name (sprintf "_%s_%i" id cpt) (cpt+1)
1043
    else name
1044
  in new_name id 1
1045

  
1046
let mkeq loc (lhs, rhs) =
1047
  { eq_lhs = lhs;
1048
    eq_rhs = rhs;
1049
    eq_loc = loc }
1050

  
1051
let mkassert loc expr =
1052
  { assert_loc = loc;
1053
    assert_expr = expr
1054
  }
1055

  
1056
let mktop_decl loc own itf d =
1057
  { top_decl_desc = d; top_decl_loc = loc; top_decl_owner = own; top_decl_itf = itf }
1058

  
1059
let mkpredef_call loc funname args =
1060
  mkexpr loc (Expr_appl (funname, mkexpr loc (Expr_tuple args), None))
1061

  
1062
let is_clock_dec_type cty =
1063
  match cty with
1064
  | Tydec_clock _ -> true
1065
  | _             -> false
1066

  
1067
let const_of_top top_decl =
1068
  match top_decl.top_decl_desc with
1069
  | Const c -> c
1070
  | _ -> assert false
1071

  
1072
let node_of_top top_decl =
1073
  match top_decl.top_decl_desc with
1074
  | Node nd -> nd
1075
  | _ -> assert false
1076

  
1077
let imported_node_of_top top_decl =
1078
  match top_decl.top_decl_desc with
1079
  | ImportedNode ind -> ind
1080
  | _ -> assert false
1081

  
1082
let typedef_of_top top_decl =
1083
  match top_decl.top_decl_desc with
1084
  | TypeDef tdef -> tdef
1085
  | _ -> assert false
1086

  
1087
let dependency_of_top top_decl =
1088
  match top_decl.top_decl_desc with
1089
  | Open (local, dep) -> (local, dep)
1090
  | _ -> assert false
1091

  
1092
let consts_of_enum_type top_decl =
1093
  match top_decl.top_decl_desc with
1094
  | TypeDef tdef ->
1095
    (match tdef.tydef_desc with
1096
     | Tydec_enum tags -> List.map (fun tag -> let cdecl = { const_id = tag; const_loc = top_decl.top_decl_loc; const_value = Const_tag tag; const_type = Type_predef.type_const tdef.tydef_id } in { top_decl with top_decl_desc = Const cdecl }) tags
1097
     | _               -> [])
1098
  | _ -> assert false
1099

  
1100
(************************************************************)
1101
(*   Eexpr functions *)
1102
(************************************************************)
1103

  
1104
let merge_node_annot ann1 ann2 =
1105
  { requires = ann1.requires @ ann2.requires;
1106
    ensures = ann1.ensures @ ann2.ensures;
1107
    behaviors = ann1.behaviors @ ann2.behaviors;
1108
    spec_loc = ann1.spec_loc
1109
  }
1110

  
1111
let mkeexpr loc expr =
1112
  { eexpr_tag = Utils.new_tag ();
1113
    eexpr_qfexpr = expr;
1114
    eexpr_quantifiers = [];
1115
    eexpr_type = Types.new_var ();
1116
    eexpr_clock = Clocks.new_var true;
1117
    eexpr_normalized = None;
1118
    eexpr_loc = loc }
1119

  
1120
let extend_eexpr q e = { e with eexpr_quantifiers = q@e.eexpr_quantifiers }
1121

  
1122
(*
1123
let mkepredef_call loc funname args =
1124
  mkeexpr loc (EExpr_appl (funname, mkeexpr loc (EExpr_tuple args), None))
1125

  
1126
let mkepredef_unary_call loc funname arg =
1127
  mkeexpr loc (EExpr_appl (funname, arg, None))
1128
*)
1129

  
1130
let merge_expr_annot ann1 ann2 =
1131
  match ann1, ann2 with
1132
    | None, None -> assert false
1133
    | Some _, None -> ann1
1134
    | None, Some _ -> ann2
1135
    | Some ann1, Some ann2 -> Some {
1136
      annots = ann1.annots @ ann2.annots;
1137
      annot_loc = ann1.annot_loc
1138
    }
1139

  
1140
let update_expr_annot node_id e annot =
1141
  List.iter (fun (key, _) -> 
1142
    Annotations.add_expr_ann node_id e.expr_tag key
1143
  ) annot.annots;
1144
  { e with expr_annot = merge_expr_annot e.expr_annot (Some annot) }
1145

  
1146

  
1147
(***********************************************************)
1148
(* Fast access to nodes, by name *)
1149
let (node_table : (ident, top_decl) Hashtbl.t) = Hashtbl.create 30
1150
let consts_table = Hashtbl.create 30
1151

  
1152
let print_node_table fmt () =
1153
  begin
1154
    Format.fprintf fmt "{ /* node table */@.";
1155
    Hashtbl.iter (fun id nd ->
1156
      Format.fprintf fmt "%s |-> %a"
1157
	id
1158
	Printers.pp_short_decl nd
1159
    ) node_table;
1160
    Format.fprintf fmt "}@."
1161
  end
1162

  
1163
let print_consts_table fmt () =
1164
  begin
1165
    Format.fprintf fmt "{ /* consts table */@.";
1166
    Hashtbl.iter (fun id const ->
1167
      Format.fprintf fmt "%s |-> %a"
1168
	id
1169
	Printers.pp_const_decl (const_of_top const)
1170
    ) consts_table;
1171
    Format.fprintf fmt "}@."
1172
  end
1173

  
1174
let node_name td =
1175
    match td.top_decl_desc with 
1176
    | Node nd         -> nd.node_id
1177
    | ImportedNode nd -> nd.nodei_id
1178
    | _ -> assert false
1179

  
1180
let is_generic_node td =
1181
  match td.top_decl_desc with 
1182
  | Node nd         -> List.exists (fun v -> v.var_dec_const) nd.node_inputs
1183
  | ImportedNode nd -> List.exists (fun v -> v.var_dec_const) nd.nodei_inputs
1184
  | _ -> assert false
1185

  
1186
let node_inputs td =
1187
  match td.top_decl_desc with 
1188
  | Node nd         -> nd.node_inputs
1189
  | ImportedNode nd -> nd.nodei_inputs
1190
  | _ -> assert false
1191

  
1192
let node_from_name id =
1193
  try
1194
    Hashtbl.find node_table id
1195
  with Not_found -> (Format.eprintf "Unable to find any node named %s@ @?" id;
1196
		     assert false)
1197

  
1198
let is_imported_node td =
1199
  match td.top_decl_desc with 
1200
  | Node nd         -> false
1201
  | ImportedNode nd -> true
1202
  | _ -> assert false
1203

  
1204

  
1205
(* alias and type definition table *)
1206

  
1207
let mktop = mktop_decl Location.dummy_loc Version.include_path false 
1208

  
1209
let top_int_type = mktop (TypeDef {tydef_id = "int"; tydef_desc = Tydec_int})
1210
let top_bool_type = mktop (TypeDef {tydef_id = "bool"; tydef_desc = Tydec_bool})
1211
let top_float_type = mktop (TypeDef {tydef_id = "float"; tydef_desc = Tydec_float})
1212
let top_real_type = mktop (TypeDef {tydef_id = "real"; tydef_desc = Tydec_real})
1213

  
1214
let type_table =
1215
  Utils.create_hashtable 20 [
1216
    Tydec_int  , top_int_type;
1217
    Tydec_bool , top_bool_type;
1218
    Tydec_float, top_float_type;
1219
    Tydec_real , top_real_type
1220
  ]
1221

  
1222
let print_type_table fmt () =
1223
  begin
1224
    Format.fprintf fmt "{ /* type table */@.";
1225
    Hashtbl.iter (fun tydec tdef ->
1226
      Format.fprintf fmt "%a |-> %a"
1227
	Printers.pp_var_type_dec_desc tydec
1228
	Printers.pp_typedef (typedef_of_top tdef)
1229
    ) type_table;
1230
    Format.fprintf fmt "}@."
1231
  end
1232

  
1233
let rec is_user_type typ =
1234
  match typ with
1235
  | Tydec_int | Tydec_bool | Tydec_real 
1236
  | Tydec_float | Tydec_any | Tydec_const _ -> false
1237
  | Tydec_clock typ' -> is_user_type typ'
1238
  | _ -> true
1239

  
1240
let get_repr_type typ =
1241
  let typ_def = (typedef_of_top (Hashtbl.find type_table typ)).tydef_desc in
1242
  if is_user_type typ_def then typ else typ_def
1243

  
1244
let rec coretype_equal ty1 ty2 =
1245
  let res =
1246
  match ty1, ty2 with
1247
  | Tydec_any           , _
1248
  | _                   , Tydec_any             -> assert false
1249
  | Tydec_const _       , Tydec_const _         -> get_repr_type ty1 = get_repr_type ty2
1250
  | Tydec_const _       , _                     -> let ty1' = (typedef_of_top (Hashtbl.find type_table ty1)).tydef_desc
1251
	       					   in (not (is_user_type ty1')) && coretype_equal ty1' ty2
1252
  | _                   , Tydec_const _         -> coretype_equal ty2 ty1
1253
  | Tydec_int           , Tydec_int
1254
  | Tydec_real          , Tydec_real
1255
  | Tydec_float         , Tydec_float
1256
  | Tydec_bool          , Tydec_bool            -> true
1257
  | Tydec_clock ty1     , Tydec_clock ty2       -> coretype_equal ty1 ty2
1258
  | Tydec_array (d1,ty1), Tydec_array (d2, ty2) -> Dimension.is_eq_dimension d1 d2 && coretype_equal ty1 ty2
1259
  | Tydec_enum tl1      , Tydec_enum tl2        -> List.sort compare tl1 = List.sort compare tl2
1260
  | Tydec_struct fl1    , Tydec_struct fl2      ->
1261
       List.length fl1 = List.length fl2
1262
    && List.for_all2 (fun (f1, t1) (f2, t2) -> f1 = f2 && coretype_equal t1 t2)
1263
      (List.sort (fun (f1,_) (f2,_) -> compare f1 f2) fl1)
1264
      (List.sort (fun (f1,_) (f2,_) -> compare f1 f2) fl2)
1265
  | _                                  -> false
1266
  in ((*Format.eprintf "coretype_equal %a %a = %B@." Printers.pp_var_type_dec_desc ty1 Printers.pp_var_type_dec_desc ty2 res;*) res)
1267

  
1268
let tag_true = "true"
1269
let tag_false = "false"
1270
let tag_default = "default"
1271

  
1272
let const_is_bool c =
1273
 match c with
1274
 | Const_tag t -> t = tag_true || t = tag_false
1275
 | _           -> false
1276

  
1277
(* Computes the negation of a boolean constant *)
1278
let const_negation c =
1279
  assert (const_is_bool c);
1280
  match c with
1281
  | Const_tag t when t = tag_true  -> Const_tag tag_false
1282
  | _                              -> Const_tag tag_true
1283

  
1284
let const_or c1 c2 =
1285
  assert (const_is_bool c1 && const_is_bool c2);
1286
  match c1, c2 with
1287
  | Const_tag t1, _            when t1 = tag_true -> c1
1288
  | _           , Const_tag t2 when t2 = tag_true -> c2
1289
  | _                                             -> Const_tag tag_false
1290

  
1291
let const_and c1 c2 =
1292
  assert (const_is_bool c1 && const_is_bool c2);
1293
  match c1, c2 with
1294
  | Const_tag t1, _            when t1 = tag_false -> c1
1295
  | _           , Const_tag t2 when t2 = tag_false -> c2
1296
  | _                                              -> Const_tag tag_true
1297

  
1298
let const_xor c1 c2 =
1299
  assert (const_is_bool c1 && const_is_bool c2);
1300
   match c1, c2 with
1301
  | Const_tag t1, Const_tag t2 when t1 <> t2  -> Const_tag tag_true
1302
  | _                                         -> Const_tag tag_false
1303

  
1304
let const_impl c1 c2 =
1305
  assert (const_is_bool c1 && const_is_bool c2);
1306
  match c1, c2 with
1307
  | Const_tag t1, _ when t1 = tag_false           -> Const_tag tag_true
1308
  | _           , Const_tag t2 when t2 = tag_true -> Const_tag tag_true
1309
  | _                                             -> Const_tag tag_false
1310

  
1311
(* To guarantee uniqueness of tags in enum types *)
1312
let tag_table =
1313
  Utils.create_hashtable 20 [
1314
   tag_true, top_bool_type;
1315
   tag_false, top_bool_type
1316
  ]
1317

  
1318
(* To guarantee uniqueness of fields in struct types *)
1319
let field_table =
1320
  Utils.create_hashtable 20 [
1321
  ]
1322

  
1323
let get_enum_type_tags cty =
1324
(*Format.eprintf "get_enum_type_tags %a@." Printers.pp_var_type_dec_desc cty;*)
1325
 match cty with
1326
 | Tydec_bool    -> [tag_true; tag_false]
1327
 | Tydec_const _ -> (match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with
1328
                     | Tydec_enum tl -> tl
1329
                     | _             -> assert false)
1330
 | _            -> assert false
1331

  
1332
let get_struct_type_fields cty =
1333
 match cty with
1334
 | Tydec_const _ -> (match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with
1335
                     | Tydec_struct fl -> fl
1336
                     | _               -> assert false)
1337
 | _            -> assert false
1338

  
1339
let const_of_bool b =
1340
 Const_tag (if b then tag_true else tag_false)
1341

  
1342
(* let get_const c = snd (Hashtbl.find consts_table c) *)
1343

  
1344
let ident_of_expr expr =
1345
 match expr.expr_desc with
1346
 | Expr_ident id -> id
1347
 | _             -> assert false
1348

  
1349
(* Generate a new ident expression from a declared variable *)
1350
let expr_of_vdecl v =
1351
  { expr_tag = Utils.new_tag ();
1352
    expr_desc = Expr_ident v.var_id;
1353
    expr_type = v.var_type;
1354
    expr_clock = v.var_clock;
1355
    expr_delay = Delay.new_var ();
1356
    expr_annot = None;
1357
    expr_loc = v.var_loc }
1358

  
1359
(* Caution, returns an untyped and unclocked expression *)
1360
let expr_of_ident id loc =
1361
  {expr_tag = Utils.new_tag ();
1362
   expr_desc = Expr_ident id;
1363
   expr_type = Types.new_var ();
1364
   expr_clock = Clocks.new_var true;
1365
   expr_delay = Delay.new_var ();
1366
   expr_loc = loc;
1367
   expr_annot = None}
1368

  
1369
let is_tuple_expr expr =
1370
 match expr.expr_desc with
1371
  | Expr_tuple _ -> true
1372
  | _            -> false
1373

  
1374
let expr_list_of_expr expr =
1375
  match expr.expr_desc with
1376
  | Expr_tuple elist -> elist
1377
  | _                -> [expr]
1378

  
1379
let expr_of_expr_list loc elist =
1380
 match elist with
1381
 | [t]  -> { t with expr_loc = loc }
1382
 | t::_ ->
1383
    let tlist = List.map (fun e -> e.expr_type) elist in
1384
    let clist = List.map (fun e -> e.expr_clock) elist in
1385
    { t with expr_desc = Expr_tuple elist;
1386
	     expr_type = Type_predef.type_tuple tlist;
1387
	     expr_clock = Clock_predef.ck_tuple clist;
1388
	     expr_tag = Utils.new_tag ();
1389
	     expr_loc = loc }
1390
 | _    -> assert false
1391

  
1392
let call_of_expr expr =
1393
 match expr.expr_desc with
1394
 | Expr_appl (f, args, r) -> (f, expr_list_of_expr args, r)
1395
 | _                      -> assert false
1396

  
1397
(* Conversion from dimension expr to standard expr, for the purpose of printing, typing, etc... *)
1398
let rec expr_of_dimension dim =
1399
 match dim.dim_desc with
1400
 | Dbool b        ->
1401
     mkexpr dim.dim_loc (Expr_const (const_of_bool b))
1402
 | Dint i         ->
1403
     mkexpr dim.dim_loc (Expr_const (Const_int i))
1404
 | Dident id      ->
1405
     mkexpr dim.dim_loc (Expr_ident id)
1406
 | Dite (c, t, e) ->
1407
     mkexpr dim.dim_loc (Expr_ite (expr_of_dimension c, expr_of_dimension t, expr_of_dimension e))
1408
 | Dappl (id, args) ->
1409
     mkexpr dim.dim_loc (Expr_appl (id, expr_of_expr_list dim.dim_loc (List.map expr_of_dimension args), None))
1410
 | Dlink dim'       -> expr_of_dimension dim'
1411
 | Dvar
1412
 | Dunivar          -> (Format.eprintf "internal error: Corelang.expr_of_dimension %a@." Dimension.pp_dimension dim;
1413
			assert false)
1414

  
1415
let dimension_of_const loc const =
1416
 match const with
1417
 | Const_int i                                    -> mkdim_int loc i
1418
 | Const_tag t when t = tag_true || t = tag_false -> mkdim_bool loc (t = tag_true)
1419
 | _                                              -> raise InvalidDimension
1420

  
1421
(* Conversion from standard expr to dimension expr, for the purpose of injecting static call arguments 
1422
   into dimension expressions *)
1423
let rec dimension_of_expr expr =
1424
  match expr.expr_desc with
1425
  | Expr_const c  -> dimension_of_const expr.expr_loc c
1426
  | Expr_ident id -> mkdim_ident expr.expr_loc id
1427
  | Expr_appl (f, args, None) when Basic_library.is_internal_fun f ->
1428
      let k = Types.get_static_value (Env.lookup_value Basic_library.type_env f) in
1429
      if k = None then raise InvalidDimension;
1430
      mkdim_appl expr.expr_loc f (List.map dimension_of_expr (expr_list_of_expr args))
1431
  | Expr_ite (i, t, e)        ->
1432
      mkdim_ite expr.expr_loc (dimension_of_expr i) (dimension_of_expr t) (dimension_of_expr e)
1433
  | _ -> raise InvalidDimension (* not a simple dimension expression *)
1434

  
1435

  
1436
let sort_handlers hl =
1437
 List.sort (fun (t, _) (t', _) -> compare t t') hl
1438

  
1439
let rec is_eq_expr e1 e2 = match e1.expr_desc, e2.expr_desc with
1440
  | Expr_const c1, Expr_const c2 -> c1 = c2
1441
  | Expr_ident i1, Expr_ident i2 -> i1 = i2
1442
  | Expr_array el1, Expr_array el2 
1443
  | Expr_tuple el1, Expr_tuple el2 -> 
1444
    List.length el1 = List.length el2 && List.for_all2 is_eq_expr el1 el2 
1445
  | Expr_arrow (e1, e2), Expr_arrow (e1', e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2'
1446
  | Expr_fby (e1,e2), Expr_fby (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2'
1447
  | Expr_ite (i1, t1, e1), Expr_ite (i2, t2, e2) -> is_eq_expr i1 i2 && is_eq_expr t1 t2 && is_eq_expr e1 e2
1448
  (* | Expr_concat (e1,e2), Expr_concat (e1',e2') -> is_eq_expr e1 e1' && is_eq_expr e2 e2' *)
1449
  (* | Expr_tail e, Expr_tail e' -> is_eq_expr e e' *)
1450
  | Expr_pre e, Expr_pre e' -> is_eq_expr e e'
1451
  | Expr_when (e, i, l), Expr_when (e', i', l') -> l=l' && i=i' && is_eq_expr e e'
1452
  | 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')
1453
  | Expr_appl (i, e, r), Expr_appl (i', e', r') -> i=i' && r=r' && is_eq_expr e e'
1454
  | Expr_power (e1, i1), Expr_power (e2, i2)
1455
  | Expr_access (e1, i1), Expr_access (e2, i2) -> is_eq_expr e1 e2 && is_eq_expr (expr_of_dimension i1) (expr_of_dimension i2)
1456
  | _ -> false
1457

  
1458
let get_node_vars nd =
1459
  nd.node_inputs @ nd.node_locals @ nd.node_outputs
1460

  
1461
let mk_new_node_name nd id =
1462
  let used_vars = get_node_vars nd in
1463
  let used v = List.exists (fun vdecl -> vdecl.var_id = v) used_vars in
1464
  mk_new_name used id
1465

  
1466
let get_var id var_list =
1467
    List.find (fun v -> v.var_id = id) var_list
1468

  
1469
let get_node_var id node =
1470
  get_var id (get_node_vars node)
1471

  
1472
let get_node_eqs =
1473
  let get_eqs stmts =
1474
    List.fold_right
1475
      (fun stmt res ->
1476
	match stmt with
1477
	| Eq eq -> eq :: res
1478
	| Aut _ -> assert false)
1479
      stmts
1480
      [] in
1481
  let table_eqs = Hashtbl.create 23 in
1482
  (fun nd ->
1483
    try
1484
      let (old, res) = Hashtbl.find table_eqs nd.node_id
1485
      in if old == nd.node_stmts then res else raise Not_found
1486
    with Not_found -> 
1487
      let res = get_eqs nd.node_stmts in
1488
      begin
1489
	Hashtbl.replace table_eqs nd.node_id (nd.node_stmts, res);
1490
	res
1491
      end)
1492

  
1493
let get_node_eq id node =
1494
 List.find (fun eq -> List.mem id eq.eq_lhs) (get_node_eqs node)
1495

  
1496
let get_nodes prog = 
1497
  List.fold_left (
1498
    fun nodes decl ->
1499
      match decl.top_decl_desc with
1500
	| Node _ -> decl::nodes
1501
	| Const _ | ImportedNode _ | Open _ | TypeDef _ -> nodes  
1502
  ) [] prog
1503

  
1504
let get_imported_nodes prog = 
1505
  List.fold_left (
1506
    fun nodes decl ->
1507
      match decl.top_decl_desc with
1508
	| ImportedNode _ -> decl::nodes
1509
	| Const _ | Node _ | Open _ | TypeDef _-> nodes  
1510
  ) [] prog
1511

  
1512
let get_consts prog = 
1513
  List.fold_right (
1514
    fun decl consts ->
1515
      match decl.top_decl_desc with
1516
	| Const _ -> decl::consts
1517
	| Node _ | ImportedNode _ | Open _ | TypeDef _ -> consts  
1518
  ) prog []
1519

  
1520
let get_typedefs prog = 
1521
  List.fold_right (
1522
    fun decl types ->
1523
      match decl.top_decl_desc with
1524
	| TypeDef _ -> decl::types
1525
	| Node _ | ImportedNode _ | Open _ | Const _ -> types  
1526
  ) prog []
1527

  
1528
let get_dependencies prog =
1529
  List.fold_right (
1530
    fun decl deps ->
1531
      match decl.top_decl_desc with
1532
	| Open _ -> decl::deps
1533
	| Node _ | ImportedNode _ | TypeDef _ | Const _ -> deps  
1534
  ) prog []
1535

  
1536
let get_node_interface nd =
1537
 {nodei_id = nd.node_id;
1538
  nodei_type = nd.node_type;
1539
  nodei_clock = nd.node_clock;
1540
  nodei_inputs = nd.node_inputs;
1541
  nodei_outputs = nd.node_outputs;
1542
  nodei_stateless = nd.node_dec_stateless;
1543
  nodei_spec = nd.node_spec;
1544
  nodei_prototype = None;
1545
  nodei_in_lib = None;
1546
 }
1547

  
1548
(************************************************************************)
1549
(*        Renaming                                                      *)
1550

  
1551
let rec rename_static rename cty =
1552
 match cty with
1553
 | Tydec_array (d, cty') -> Tydec_array (Dimension.expr_replace_expr rename d, rename_static rename cty')
1554
 | Tydec_clock cty       -> Tydec_clock (rename_static rename cty)
1555
 | Tydec_struct fl       -> Tydec_struct (List.map (fun (f, cty) -> f, rename_static rename cty) fl)
1556
 | _                      -> cty
1557

  
1558
let rec rename_carrier rename cck =
1559
 match cck with
1560
 | Ckdec_bool cl -> Ckdec_bool (List.map (fun (c, l) -> rename c, l) cl)
1561
 | _             -> cck
1562

  
1563
(*Format.eprintf "Types.rename_static %a = %a@." print_ty ty print_ty res; res*)
1564

  
1565
(* applies the renaming function [fvar] to all variables of expression [expr] *)
1566
 let rec expr_replace_var fvar expr =
1567
  { expr with expr_desc = expr_desc_replace_var fvar expr.expr_desc }
1568

  
1569
 and expr_desc_replace_var fvar expr_desc =
1570
   match expr_desc with
1571
   | Expr_const _ -> expr_desc
1572
   | Expr_ident i -> Expr_ident (fvar i)
1573
   | Expr_array el -> Expr_array (List.map (expr_replace_var fvar) el)
1574
   | Expr_access (e1, d) -> Expr_access (expr_replace_var fvar e1, d)
1575
   | Expr_power (e1, d) -> Expr_power (expr_replace_var fvar e1, d)
1576
   | Expr_tuple el -> Expr_tuple (List.map (expr_replace_var fvar) el)
1577
   | Expr_ite (c, t, e) -> Expr_ite (expr_replace_var fvar c, expr_replace_var fvar t, expr_replace_var fvar e)
1578
   | Expr_arrow (e1, e2)-> Expr_arrow (expr_replace_var fvar e1, expr_replace_var fvar e2) 
1579
   | Expr_fby (e1, e2) -> Expr_fby (expr_replace_var fvar e1, expr_replace_var fvar e2)
1580
   | Expr_pre e' -> Expr_pre (expr_replace_var fvar e')
1581
   | Expr_when (e', i, l)-> Expr_when (expr_replace_var fvar e', fvar i, l)
1582
   | Expr_merge (i, hl) -> Expr_merge (fvar i, List.map (fun (t, h) -> (t, expr_replace_var fvar h)) hl)
1583
   | Expr_appl (i, e', i') -> Expr_appl (i, expr_replace_var fvar e', Utils.option_map (expr_replace_var fvar) i')
1584

  
1585
(* Applies the renaming function [fvar] to every rhs
1586
   only when the corresponding lhs satisfies predicate [pvar] *)
1587
 let eq_replace_rhs_var pvar fvar eq =
1588
   let pvar l = List.exists pvar l in
1589
   let rec replace lhs rhs =
1590
     { rhs with expr_desc = replace_desc lhs rhs.expr_desc }
1591
   and replace_desc lhs rhs_desc =
1592
     match lhs with
1593
     | []  -> assert false
1594
     | [_] -> if pvar lhs then expr_desc_replace_var fvar rhs_desc else rhs_desc
1595
     | _   ->
1596
       (match rhs_desc with
1597
       | Expr_tuple tl ->
1598
	 Expr_tuple (List.map2 (fun v e -> replace [v] e) lhs tl)
1599
       | Expr_appl (f, arg, None) when Basic_library.is_internal_fun f ->
1600
	 let args = expr_list_of_expr arg in
1601
	 Expr_appl (f, expr_of_expr_list arg.expr_loc (List.map (replace lhs) args), None)
1602
       | Expr_array _
1603
       | Expr_access _
1604
       | Expr_power _
1605
       | Expr_const _
1606
       | Expr_ident _
1607
       | Expr_appl _   ->
1608
	 if pvar lhs
1609
	 then expr_desc_replace_var fvar rhs_desc
1610
	 else rhs_desc
1611
       | Expr_ite (c, t, e)   -> Expr_ite (replace lhs c, replace lhs t, replace lhs e)
1612
       | Expr_arrow (e1, e2)  -> Expr_arrow (replace lhs e1, replace lhs e2) 
1613
       | Expr_fby (e1, e2)    -> Expr_fby (replace lhs e1, replace lhs e2)
1614
       | Expr_pre e'          -> Expr_pre (replace lhs e')
1615
       | Expr_when (e', i, l) -> let i' = if pvar lhs then fvar i else i
1616
				 in Expr_when (replace lhs e', i', l)
1617
       | Expr_merge (i, hl)   -> let i' = if pvar lhs then fvar i else i
1618
				 in Expr_merge (i', List.map (fun (t, h) -> (t, replace lhs h)) hl)
1619
       )
1620
   in { eq with eq_rhs = replace eq.eq_lhs eq.eq_rhs }
1621

  
1622

  
1623
 let rec rename_expr  f_node f_var f_const expr =
1624
   { expr with expr_desc = rename_expr_desc f_node f_var f_const expr.expr_desc }
1625
 and rename_expr_desc f_node f_var f_const expr_desc =
1626
   let re = rename_expr  f_node f_var f_const in
1627
   match expr_desc with
1628
   | Expr_const _ -> expr_desc
1629
   | Expr_ident i -> Expr_ident (f_var i)
1630
   | Expr_array el -> Expr_array (List.map re el)
1631
   | Expr_access (e1, d) -> Expr_access (re e1, d)
1632
   | Expr_power (e1, d) -> Expr_power (re e1, d)
1633
   | Expr_tuple el -> Expr_tuple (List.map re el)
1634
   | Expr_ite (c, t, e) -> Expr_ite (re c, re t, re e)
1635
   | Expr_arrow (e1, e2)-> Expr_arrow (re e1, re e2) 
1636
   | Expr_fby (e1, e2) -> Expr_fby (re e1, re e2)
1637
   | Expr_pre e' -> Expr_pre (re e')
1638
   | Expr_when (e', i, l)-> Expr_when (re e', f_var i, l)
1639
   | Expr_merge (i, hl) -> 
1640
     Expr_merge (f_var i, List.map (fun (t, h) -> (t, re h)) hl)
1641
   | Expr_appl (i, e', i') -> 
1642
     Expr_appl (f_node i, re e', Utils.option_map re i')
1643
  
1644
 let rename_node_annot f_node f_var f_const expr  =
1645
   expr
1646
 (* TODO assert false *)
1647

  
1648
 let rename_expr_annot f_node f_var f_const annot =
1649
   annot
1650
 (* TODO assert false *)
1651

  
1652
let rename_node f_node f_var f_const nd =
1653
  let rename_var v = { v with var_id = f_var v.var_id } in
1654
  let rename_eq eq = { eq with
1655
      eq_lhs = List.map f_var eq.eq_lhs; 
1656
      eq_rhs = rename_expr f_node f_var f_const eq.eq_rhs
1657
    } 
1658
  in
1659
  let inputs = List.map rename_var nd.node_inputs in
1660
  let outputs = List.map rename_var nd.node_outputs in
1661
  let locals = List.map rename_var nd.node_locals in
1662
  let gen_calls = List.map (rename_expr f_node f_var f_const) nd.node_gencalls in
1663
  let node_checks = List.map (Dimension.expr_replace_var f_var)  nd.node_checks in
1664
  let node_asserts = List.map 
1665
    (fun a -> 
1666
      {a with assert_expr = 
1667
	  let expr = a.assert_expr in
1668
	  rename_expr f_node f_var f_const expr})
1669
    nd.node_asserts
1670
  in
1671
  let node_stmts = List.map (fun eq -> Eq (rename_eq eq)) (get_node_eqs nd) in
1672
  let spec = 
1673
    Utils.option_map 
1674
      (fun s -> rename_node_annot f_node f_var f_const s) 
1675
      nd.node_spec 
1676
  in
1677
  let annot =
1678
    List.map 
1679
      (fun s -> rename_expr_annot f_node f_var f_const s) 
1680
      nd.node_annot
1681
  in
1682
  {
1683
    node_id = f_node nd.node_id;
1684
    node_type = nd.node_type;
1685
    node_clock = nd.node_clock;
1686
    node_inputs = inputs;
1687
    node_outputs = outputs;
1688
    node_locals = locals;
1689
    node_gencalls = gen_calls;
1690
    node_checks = node_checks;
1691
    node_asserts = node_asserts;
1692
    node_stmts = node_stmts;
1693
    node_dec_stateless = nd.node_dec_stateless;
1694
    node_stateless = nd.node_stateless;
1695
    node_spec = spec;
1696
    node_annot = annot;
1697
  }
1698

  
1699

  
1700
let rename_const f_const c =
1701
  { c with const_id = f_const c.const_id }
1702

  
1703
let rename_typedef f_var t =
1704
  match t.tydef_desc with
1705
  | Tydec_enum tags -> { t with tydef_desc = Tydec_enum (List.map f_var tags) }
1706
  | _               -> t
1707

  
1708
let rename_prog f_node f_var f_const prog =
1709
  List.rev (
1710
    List.fold_left (fun accu top ->
1711
      (match top.top_decl_desc with
1712
      | Node nd -> 
1713
	 { top with top_decl_desc = Node (rename_node f_node f_var f_const nd) }
1714
      | Const c -> 
1715
	 { top with top_decl_desc = Const (rename_const f_const c) }
1716
      | TypeDef tdef ->
1717
	 { top with top_decl_desc = TypeDef (rename_typedef f_var tdef) }
1718
      | ImportedNode _
1719
      | Open _       -> top)
1720
      ::accu
1721
) [] prog
1722
		   )
1723

  
1724
(**********************************************************************)
1725
(* Pretty printers *)
1726

  
1727
let pp_decl_type fmt tdecl =
1728
  match tdecl.top_decl_desc with
1729
  | Node nd ->
1730
    fprintf fmt "%s: " nd.node_id;
1731
    Utils.reset_names ();
1732
    fprintf fmt "%a@ " Types.print_ty nd.node_type
1733
  | ImportedNode ind ->
1734
    fprintf fmt "%s: " ind.nodei_id;
1735
    Utils.reset_names ();
1736
    fprintf fmt "%a@ " Types.print_ty ind.nodei_type
1737
  | Const _ | Open _ | TypeDef _ -> ()
1738

  
1739
let pp_prog_type fmt tdecl_list =
1740
  Utils.fprintf_list ~sep:"" pp_decl_type fmt tdecl_list
1741

  
1742
let pp_decl_clock fmt cdecl =
1743
  match cdecl.top_decl_desc with
1744
  | Node nd ->
1745
    fprintf fmt "%s: " nd.node_id;
1746
    Utils.reset_names ();
1747
    fprintf fmt "%a@ " Clocks.print_ck nd.node_clock
1748
  | ImportedNode ind ->
1749
    fprintf fmt "%s: " ind.nodei_id;
1750
    Utils.reset_names ();
1751
    fprintf fmt "%a@ " Clocks.print_ck ind.nodei_clock
1752
  | Const _ | Open _ | TypeDef _ -> ()
1753

  
1754
let pp_prog_clock fmt prog =
1755
  Utils.fprintf_list ~sep:"" pp_decl_clock fmt prog
1756

  
1757
let pp_error fmt = function
1758
    Main_not_found ->
1759
      fprintf fmt "Cannot compile node %s: could not find the node definition.@."
1760
	!Options.main_node
1761
  | Main_wrong_kind ->
1762
    fprintf fmt
1763
      "Name %s does not correspond to a (non-imported) node definition.@." 
1764
      !Options.main_node
1765
  | No_main_specified ->
1766
    fprintf fmt "No main node specified@."
1767
  | Unbound_symbol sym ->
1768
    fprintf fmt
1769
      "%s is undefined.@."
1770
      sym
1771
  | Already_bound_symbol sym -> 
1772
    fprintf fmt
1773
      "%s is already defined.@."
1774
      sym
1775
  | Unknown_library sym ->
1776
    fprintf fmt
1777
      "impossible to load library %s.lusic@.Please compile the corresponding interface or source file.@."
1778
      sym
1779

  
1780
(* filling node table with internal functions *)
1781
let vdecls_of_typ_ck cpt ty =
1782
  let loc = Location.dummy_loc in
1783
  List.map
1784
    (fun _ -> incr cpt;
1785
              let name = sprintf "_var_%d" !cpt in
1786
              mkvar_decl loc (name, mktyp loc Tydec_any, mkclock loc Ckdec_any, false, None))
1787
    (Types.type_list_of_type ty)
1788

  
1789
let mk_internal_node id =
1790
  let spec = None in
1791
  let ty = Env.lookup_value Basic_library.type_env id in
1792
  let ck = Env.lookup_value Basic_library.clock_env id in
1793
  let (tin, tout) = Types.split_arrow ty in
1794
  (*eprintf "internal fun %s: %d -> %d@." id (List.length (Types.type_list_of_type tin)) (List.length (Types.type_list_of_type tout));*)
1795
  let cpt = ref (-1) in
1796
  mktop
1797
    (ImportedNode
1798
       {nodei_id = id;
1799
	nodei_type = ty;
1800
	nodei_clock = ck;
1801
	nodei_inputs = vdecls_of_typ_ck cpt tin;
1802
	nodei_outputs = vdecls_of_typ_ck cpt tout;
1803
	nodei_stateless = Types.get_static_value ty <> None;
1804
	nodei_spec = spec;
1805
	nodei_prototype = None;
1806
       	nodei_in_lib = None;
1807
       })
1808

  
1809
let add_internal_funs () =
1810
  List.iter
1811
    (fun id -> let nd = mk_internal_node id in Hashtbl.add node_table id nd)
1812
    Basic_library.internal_funs
1813

  
1814

  
1815

  
1816
(* Replace any occurence of a var in vars_to_replace by its associated
1817
   expression in defs until e does not contain any such variables *)
1818
let rec substitute_expr vars_to_replace defs e =
1819
  let se = substitute_expr vars_to_replace defs in
1820
  { e with expr_desc = 
1821
      let ed = e.expr_desc in
1822
      match ed with
1823
      | Expr_const _ -> ed
1824
      | Expr_array el -> Expr_array (List.map se el)
1825
      | Expr_access (e1, d) -> Expr_access (se e1, d)
1826
      | Expr_power (e1, d) -> Expr_power (se e1, d)
1827
      | Expr_tuple el -> Expr_tuple (List.map se el)
1828
      | Expr_ite (c, t, e) -> Expr_ite (se c, se t, se e)
1829
      | Expr_arrow (e1, e2)-> Expr_arrow (se e1, se e2) 
1830
      | Expr_fby (e1, e2) -> Expr_fby (se e1, se e2)
1831
      | Expr_pre e' -> Expr_pre (se e')
1832
      | Expr_when (e', i, l)-> Expr_when (se e', i, l)
1833
      | Expr_merge (i, hl) -> Expr_merge (i, List.map (fun (t, h) -> (t, se h)) hl)
1834
      | Expr_appl (i, e', i') -> Expr_appl (i, se e', i')
1835
      | Expr_ident i -> 
1836
	if List.exists (fun v -> v.var_id = i) vars_to_replace then (
1837
	  let eq_i eq = eq.eq_lhs = [i] in
1838
	  if List.exists eq_i defs then
1839
	    let sub = List.find eq_i defs in
1840
	    let sub' = se sub.eq_rhs in
1841
	    sub'.expr_desc
1842
	  else 
1843
	    assert false
1844
	)
1845
	else
1846
	  ed
1847

  
1848
  }
1849
(* FAUT IL RETIRER ?
1850
  
1851
 let rec expr_to_eexpr  expr =
1852
   { eexpr_tag = expr.expr_tag;
1853
     eexpr_desc = expr_desc_to_eexpr_desc expr.expr_desc;
1854
     eexpr_type = expr.expr_type;
1855
     eexpr_clock = expr.expr_clock;
1856
     eexpr_loc = expr.expr_loc
1857
   }
1858
 and expr_desc_to_eexpr_desc expr_desc =
1859
   let conv = expr_to_eexpr in
1860
   match expr_desc with
1861
   | Expr_const c -> EExpr_const (match c with
1862
     | Const_int x -> EConst_int x 
1863
     | Const_real x -> EConst_real x 
1864
     | Const_float x -> EConst_float x 
1865
     | Const_tag x -> EConst_tag x 
1866
     | _ -> assert false
1867

  
1868
   )
1869
   | Expr_ident i -> EExpr_ident i
1870
   | Expr_tuple el -> EExpr_tuple (List.map conv el)
1871

  
1872
   | Expr_arrow (e1, e2)-> EExpr_arrow (conv e1, conv e2) 
1873
   | Expr_fby (e1, e2) -> EExpr_fby (conv e1, conv e2)
1874
   | Expr_pre e' -> EExpr_pre (conv e')
1875
   | Expr_appl (i, e', i') -> 
1876
     EExpr_appl 
1877
       (i, conv e', match i' with None -> None | Some(id, _) -> Some id)
1878

  
1879
   | Expr_when _
1880
   | Expr_merge _ -> assert false
1881
   | Expr_array _ 
1882
   | Expr_access _ 
1883
   | Expr_power _  -> assert false
1884
   | Expr_ite (c, t, e) -> assert false 
1885
   | _ -> assert false
1886

  
1887
     *)
1888
let rec get_expr_calls nodes e =
1889
  get_calls_expr_desc nodes e.expr_desc
1890
and get_calls_expr_desc nodes expr_desc =
1891
  let get_calls = get_expr_calls nodes in
1892
  match expr_desc with
1893
  | Expr_const _ 
1894
   | Expr_ident _ -> Utils.ISet.empty
1895
   | Expr_tuple el
1896
   | Expr_array el -> List.fold_left (fun accu e -> Utils.ISet.union accu (get_calls e)) Utils.ISet.empty el
1897
   | Expr_pre e1 
1898
   | Expr_when (e1, _, _) 
1899
   | Expr_access (e1, _) 
1900
   | Expr_power (e1, _) -> get_calls e1
1901
   | Expr_ite (c, t, e) -> Utils.ISet.union (Utils.ISet.union (get_calls c) (get_calls t)) (get_calls e) 
1902
   | Expr_arrow (e1, e2) 
1903
   | Expr_fby (e1, e2) -> Utils.ISet.union (get_calls e1) (get_calls e2)
1904
   | Expr_merge (_, hl) -> List.fold_left (fun accu (_, h) -> Utils.ISet.union accu (get_calls h)) Utils.ISet.empty  hl
1905
   | Expr_appl (i, e', i') -> 
1906
     if Basic_library.is_internal_fun i then 
1907
       (get_calls e') 
1908
     else
1909
       let calls =  Utils.ISet.add i (get_calls e') in
1910
       let test = (fun n -> match n.top_decl_desc with Node nd -> nd.node_id = i | _ -> false) in
1911
       if List.exists test nodes then
1912
	 match (List.find test nodes).top_decl_desc with
1913
	 | Node nd -> Utils.ISet.union (get_node_calls nodes nd) calls
1914
	 | _ -> assert false
1915
       else 
1916
	 calls
1917

  
1918
and get_eq_calls nodes eq =
1919
  get_expr_calls nodes eq.eq_rhs
1920
and get_node_calls nodes node =
1921
  List.fold_left (fun accu eq -> Utils.ISet.union (get_eq_calls nodes eq) accu) Utils.ISet.empty (get_node_eqs node)
1922

  
1923
let rec get_expr_vars vars e =
1924
  get_expr_desc_vars vars e.expr_desc
1925
and get_expr_desc_vars vars expr_desc =
1926
  match expr_desc with
1927
  | Expr_const _ -> vars
1928
  | Expr_ident x -> Utils.ISet.add x vars
1929
  | Expr_tuple el
1930
  | Expr_array el -> List.fold_left get_expr_vars vars el
1931
  | Expr_pre e1 -> get_expr_vars vars e1
1932
  | Expr_when (e1, c, _) -> get_expr_vars (Utils.ISet.add c vars) e1 
1933
  | Expr_access (e1, d) 
1934
  | Expr_power (e1, d)   -> List.fold_left get_expr_vars vars [e1; expr_of_dimension d]
1935
  | Expr_ite (c, t, e) -> List.fold_left get_expr_vars vars [c; t; e]
1936
  | Expr_arrow (e1, e2) 
1937
  | Expr_fby (e1, e2) -> List.fold_left get_expr_vars vars [e1; e2]
1938
  | Expr_merge (c, hl) -> List.fold_left (fun vars (_, h) -> get_expr_vars vars h) (Utils.ISet.add c vars) hl
1939
  | Expr_appl (_, arg, None)   -> get_expr_vars vars arg
1940
  | Expr_appl (_, arg, Some r) -> List.fold_left get_expr_vars vars [arg; r]
1941

  
1942

  
1943
let rec expr_has_arrows e =
1944
  expr_desc_has_arrows e.expr_desc
1945
and expr_desc_has_arrows expr_desc =
1946
  match expr_desc with
1947
  | Expr_const _ 
1948
  | Expr_ident _ -> false
1949
  | Expr_tuple el
1950
  | Expr_array el -> List.exists expr_has_arrows el
1951
  | Expr_pre e1 
1952
  | Expr_when (e1, _, _) 
1953
  | Expr_access (e1, _) 
1954
  | Expr_power (e1, _) -> expr_has_arrows e1
1955
  | Expr_ite (c, t, e) -> List.exists expr_has_arrows [c; t; e]
1956
  | Expr_arrow (e1, e2) 
1957
  | Expr_fby (e1, e2) -> true
1958
  | Expr_merge (_, hl) -> List.exists (fun (_, h) -> expr_has_arrows h) hl
1959
  | Expr_appl (i, e', i') -> expr_has_arrows e'
1960

  
1961
and eq_has_arrows eq =
1962
  expr_has_arrows eq.eq_rhs
1963
and node_has_arrows node =
1964
  List.exists (fun eq -> eq_has_arrows eq) (get_node_eqs node)
1965 1007

  
1966 1008
let copy_var_decl vdecl =
1967 1009
  mkvar_decl vdecl.var_loc ~orig:vdecl.var_orig (vdecl.var_id, vdecl.var_dec_type, vdecl.var_dec_clock, vdecl.var_dec_const, vdecl.var_dec_value)

Also available in: Unified diff