From 66359a5eba92be4c94342e67c7a65529db3a9864 Mon Sep 17 00:00:00 2001
From: ploc <ploc@garoche.net>
Date: Wed, 31 Jan 2018 07:27:26 +0100
Subject: [PATCH] [general] large modification: added machine types, a second
typing phase dealing with machine types (eg uint8) typing was
transformed as a functor and parametrized by basic types (int/real/bool)
it can also be applied multiple times on the same program
---
src/_tags.in | 3 +-
src/automata.ml | 16 +-
src/backends/C/c_backend_common.ml | 121 +++--
src/backends/C/c_backend_header.ml | 14 +-
src/backends/C/c_backend_main.ml | 21 +-
src/backends/C/c_backend_mauve.ml | 18 +-
src/backends/C/c_backend_src.ml | 8 +-
src/backends/EMF/EMF_backend.ml | 34 +-
src/backends/EMF/EMF_common.ml | 114 +++--
src/backends/Horn/horn_backend_common.ml | 6 +-
src/backends/Horn/horn_backend_printers.ml | 7 +-
src/compiler_common.ml | 17 +-
src/compiler_stages.ml | 111 ++++-
src/corelang.ml | 12 +-
src/corelang.mli | 13 +-
src/env.ml | 1 +
src/features/machine_types/machine_types.ml | 479 ++++++++++++++++++++
src/global.ml | 2 +
src/inliner.ml | 12 +-
src/lexerLustreSpec.mll | 4 +-
src/lustreSpec.ml | 4 +-
src/machine_code.ml | 8 +-
src/main_lustre_compiler.ml | 98 +---
src/normalization.ml | 45 +-
src/optimize_machine.ml | 2 +-
src/parserLustreSpec.mly | 5 +-
src/parser_lustre.mly | 16 +-
src/pathConditions.ml | 48 +-
src/printers.ml | 10 +-
src/type_predef.ml | 110 +++--
src/types.ml | 326 ++++++++++---
src/typing.ml | 223 +++++----
32 files changed, 1430 insertions(+), 478 deletions(-)
create mode 100644 src/features/machine_types/machine_types.ml
diff --git a/src/_tags.in b/src/_tags.in
index f8fa582f..7e6e8b8d 100644
--- a/src/_tags.in
+++ b/src/_tags.in
@@ -9,6 +9,7 @@ true: bin_annot, color(always)
"plugins/salsa": include
"plugins/scopes": include
"plugins/mpfr": include
+"features/machine_types": include
"tools/stateflow": include
"tools/stateflow/common": include
"tools/stateflow/semantics": include
@@ -46,4 +47,4 @@ true: bin_annot, color(always)
# Local Variables:
# mode: conf
-# End:
\ No newline at end of file
+# End:
diff --git a/src/automata.ml b/src/automata.ml
index 2d579a1c..890651ca 100755
--- a/src/automata.ml
+++ b/src/automata.ml
@@ -114,7 +114,7 @@ let rec handler_write writes handler =
let node_vars_of_idents node iset =
List.fold_right (fun v res -> if ISet.mem v.var_id iset then v :: res else res) (get_node_vars node) []
-let mkautomata_state used typedef loc id =
+let mkautomata_state nodeid used typedef loc id =
let tydec_bool = { ty_dec_desc = Tydec_bool; ty_dec_loc = loc } in
let tydec_state id = { ty_dec_desc = Tydec_const id; ty_dec_loc = loc } in
let ckdec_any = { ck_dec_desc = Ckdec_any; ck_dec_loc = loc } in
@@ -125,12 +125,12 @@ let mkautomata_state used typedef loc id =
let actual_r = mk_new_name used (id ^ "__restart_act") in
let actual_s = mk_new_name used (id ^ "__state_act") in
{
- incoming_r' = mkvar_decl loc (incoming_r', tydec_bool, ckdec_any, false, None);
- incoming_s' = mkvar_decl loc (incoming_s', tydec_state typedef.tydef_id, ckdec_any, false, None);
- incoming_r = mkvar_decl loc (incoming_r, tydec_bool, ckdec_any, false, None);
- incoming_s = mkvar_decl loc (incoming_s, tydec_state typedef.tydef_id, ckdec_any, false, None);
- actual_r = mkvar_decl loc (actual_r , tydec_bool, ckdec_any, false, None);
- actual_s = mkvar_decl loc (actual_s , tydec_state typedef.tydef_id, ckdec_any, false, None)
+ incoming_r' = mkvar_decl loc (incoming_r', tydec_bool, ckdec_any, false, None, Some nodeid);
+ incoming_s' = mkvar_decl loc (incoming_s', tydec_state typedef.tydef_id, ckdec_any, false, None, Some nodeid);
+ incoming_r = mkvar_decl loc (incoming_r, tydec_bool, ckdec_any, false, None, Some nodeid);
+ incoming_s = mkvar_decl loc (incoming_s, tydec_state typedef.tydef_id, ckdec_any, false, None, Some nodeid);
+ actual_r = mkvar_decl loc (actual_r , tydec_bool, ckdec_any, false, None, Some nodeid);
+ actual_s = mkvar_decl loc (actual_s , tydec_state typedef.tydef_id, ckdec_any, false, None, Some nodeid)
}
let vars_of_aut_state aut_state =
@@ -225,7 +225,7 @@ let typedef_of_automata aut =
let expand_automata nused used owner typedef node aut =
let initial = (List.hd aut.aut_handlers).hand_state in
- let aut_state = mkautomata_state used typedef aut.aut_loc aut.aut_id in
+ let aut_state = mkautomata_state node.node_id used typedef aut.aut_loc aut.aut_id in
let unodes = List.map (fun h -> node_of_unless nused used node aut.aut_id aut_state h) aut.aut_handlers in
let aunodes = List.map (fun h -> node_of_assign_until nused used node aut.aut_id aut_state h) aut.aut_handlers in
let all_outputs = List.fold_left (fun all (outputs, _, _) -> ISet.union outputs all) ISet.empty aunodes in
diff --git a/src/backends/C/c_backend_common.ml b/src/backends/C/c_backend_common.ml
index 6edd2aa3..21e54e7a 100644
--- a/src/backends/C/c_backend_common.ml
+++ b/src/backends/C/c_backend_common.ml
@@ -61,6 +61,7 @@ let mk_call_var_decl loc id =
var_dec_clock = mkclock Location.dummy_loc Ckdec_any;
var_dec_const = false;
var_dec_value = None;
+ var_parent_nodeid = None;
var_type = Type_predef.type_arrow (Types.new_var ()) (Types.new_var ());
var_clock = Clocks.new_var true;
var_loc = loc }
@@ -124,34 +125,41 @@ let rec pp_c_dimension fmt dim =
| Dimension.Dunivar -> fprintf fmt "'%s" (Utils.name_of_dimension dim.Dimension.dim_id)
let is_basic_c_type t =
- match (Types.repr t).Types.tdesc with
- | Types.Tbool | Types.Treal | Types.Tint -> true
- | _ -> false
-
-let pp_c_basic_type_desc t_dsec =
- match t_dsec with
- | Types.Tbool when !Options.cpp -> "bool"
- | Types.Tbool -> "_Bool"
- | Types.Tint -> !Options.int_type
- | Types.Treal when !Options.mpfr -> Mpfr.mpfr_t
- | Types.Treal -> !Options.real_type
- | _ -> assert false (* Not a basic C type. Do not handle arrays or pointers *)
+ Types.is_int_type t || Types.is_real_type t || Types.is_bool_type t
+
+let pp_c_basic_type_desc t_desc =
+ if Types.is_bool_type t_desc then
+ if !Options.cpp then "bool" else "_Bool"
+ else if Types.is_int_type t_desc then !Options.int_type
+ else if Types.is_real_type t_desc then
+ if !Options.mpfr then Mpfr.mpfr_t else !Options.real_type
+ else
+ assert false (* Not a basic C type. Do not handle arrays or pointers *)
-let pp_basic_c_type fmt t = fprintf fmt "%s" (pp_c_basic_type_desc (Types.repr t).Types.tdesc)
+let pp_basic_c_type ?(var_opt=None) fmt t =
+ match var_opt with
+ | Some v when Machine_types.is_exportable v ->
+ Machine_types.pp_c_var_type fmt v
+ | _ ->
+ fprintf fmt "%s" (pp_c_basic_type_desc t)
-let pp_c_type var fmt t =
+let pp_c_type ?(var_opt=None) var_id fmt t =
let rec aux t pp_suffix =
- match (Types.repr t).Types.tdesc with
- | Types.Tclock t' -> aux t' pp_suffix
- | Types.Tbool | Types.Tint | Types.Treal
- -> fprintf fmt "%a %s%a" pp_basic_c_type t var pp_suffix ()
- | Types.Tarray (d, t') ->
- let pp_suffix' fmt () = fprintf fmt "%a[%a]" pp_suffix () pp_c_dimension d in
- aux t' pp_suffix'
- | Types.Tstatic (_, t') -> fprintf fmt "const "; aux t' pp_suffix
- | Types.Tconst ty -> fprintf fmt "%s %s" ty var
- | Types.Tarrow (_, _) -> fprintf fmt "void (*%s)()" var
- | _ -> eprintf "internal error: C_backend_common.pp_c_type %a@." Types.print_ty t; assert false
+ if is_basic_c_type t then
+ fprintf fmt "%a %s%a"
+ (pp_basic_c_type ~var_opt) t
+ var_id
+ pp_suffix ()
+ else
+ match (Types.repr t).Types.tdesc with
+ | Types.Tclock t' -> aux t' pp_suffix
+ | Types.Tarray (d, t') ->
+ let pp_suffix' fmt () = fprintf fmt "%a[%a]" pp_suffix () pp_c_dimension d in
+ aux t' pp_suffix'
+ | Types.Tstatic (_, t') -> fprintf fmt "const "; aux t' pp_suffix
+ | Types.Tconst ty -> fprintf fmt "%s %s" ty var_id
+ | Types.Tarrow (_, _) -> fprintf fmt "void (*%s)()" var_id
+ | _ -> eprintf "internal error: C_backend_common.pp_c_type %a@." Types.print_ty t; assert false
in aux t (fun fmt () -> ())
(*
let rec pp_c_initialize fmt t =
@@ -241,8 +249,8 @@ let pp_c_var_write m fmt id =
*)
let pp_c_decl_input_var fmt id =
if !Options.ansi && Types.is_address_type id.var_type
- then pp_c_type (sprintf "(*%s)" id.var_id) fmt (Types.array_base_type id.var_type)
- else pp_c_type id.var_id fmt id.var_type
+ then pp_c_type ~var_opt:(Some id) (sprintf "(*%s)" id.var_id) fmt (Types.array_base_type id.var_type)
+ else pp_c_type ~var_opt:(Some id) id.var_id fmt id.var_type
(* Declaration of an output variable:
- if its type is scalar, then pass its address
@@ -252,8 +260,8 @@ let pp_c_decl_input_var fmt id =
*)
let pp_c_decl_output_var fmt id =
if (not !Options.ansi) && Types.is_address_type id.var_type
- then pp_c_type id.var_id fmt id.var_type
- else pp_c_type (sprintf "(*%s)" id.var_id) fmt (Types.array_base_type id.var_type)
+ then pp_c_type ~var_opt:(Some id) id.var_id fmt id.var_type
+ else pp_c_type ~var_opt:(Some id) (sprintf "(*%s)" id.var_id) fmt (Types.array_base_type id.var_type)
(* Declaration of a local/mem variable:
- if it's an array/matrix/etc, its size(s) should be
@@ -264,11 +272,11 @@ let pp_c_decl_local_var m fmt id =
if id.var_dec_const
then
Format.fprintf fmt "%a = %a"
- (pp_c_type id.var_id) id.var_type
+ (pp_c_type ~var_opt:(Some id) id.var_id) id.var_type
(pp_c_val "" (pp_c_var_read m)) (get_const_assign m id)
else
Format.fprintf fmt "%a"
- (pp_c_type id.var_id) id.var_type
+ (pp_c_type ~var_opt:(Some id) id.var_id) id.var_type
let pp_c_decl_array_mem self fmt id =
fprintf fmt "%a = (%a) (%s->_reg.%s)"
@@ -409,7 +417,7 @@ let print_stateless_C_prototype fmt (name, inputs, outputs) =
| _ -> assert false
in
fprintf fmt "%a %s (@[<v>@[%a@]@,@])"
- pp_basic_c_type output.var_type
+ (pp_basic_c_type ~var_opt:None) output.var_type
name
(Utils.fprintf_list ~sep:",@ " pp_c_decl_input_var) inputs
@@ -650,16 +658,49 @@ let pp_instance_call m self fmt i (inputs: value_t list) (outputs: var_decl list
aux [] fmt (List.hd inputs).value_type
end
-
-(*** Common functions for main ***)
+ (*** Common functions for main ***)
let print_put_var fmt file_suffix name var_type var_id =
- match (Types.unclock_type var_type).Types.tdesc with
- | Types.Tint -> fprintf fmt "_put_int(f_out%s, \"%s\", %s)" file_suffix name var_id
- | Types.Tbool -> fprintf fmt "_put_bool(f_out%s, \"%s\", %s)" file_suffix name var_id
- | Types.Treal when !Options.mpfr -> fprintf fmt "_put_double(f_out%s, \"%s\", mpfr_get_d(%s, %s), %i)" file_suffix name var_id (Mpfr.mpfr_rnd ()) !Options.print_prec_double
- | Types.Treal -> fprintf fmt "_put_double(f_out%s, \"%s\", %s, %i)" file_suffix name var_id !Options.print_prec_double
- | _ -> Format.eprintf "Impossible to print the _put_xx for type %a@.@?" Types.print_ty var_type; assert false
+ let unclocked_t = Types.unclock_type var_type in
+ if Types.is_int_type unclocked_t then
+ fprintf fmt "_put_int(f_out%s, \"%s\", %s)" file_suffix name var_id
+ else if Types.is_bool_type unclocked_t then
+ fprintf fmt "_put_bool(f_out%s, \"%s\", %s)" file_suffix name var_id
+ else if Types.is_real_type unclocked_t then
+ if !Options.mpfr then
+ fprintf fmt "_put_double(f_out%s, \"%s\", mpfr_get_d(%s, %s), %i)" file_suffix name var_id (Mpfr.mpfr_rnd ()) !Options.print_prec_double
+ else
+ fprintf fmt "_put_double(f_out%s, \"%s\", %s, %i)" file_suffix name var_id !Options.print_prec_double
+ else
+ (Format.eprintf "Impossible to print the _put_xx for type %a@.@?" Types.print_ty var_type; assert false)
+
+
+let print_get_inputs fmt m =
+ let pi fmt (id, v', v) =
+
+ let unclocked_t = Types.unclock_type v.var_type in
+ if Types.is_int_type unclocked_t then
+ fprintf fmt "%s = _get_int(f_in%i, \"%s\")" v.var_id id v'.var_id
+ else if Types.is_bool_type unclocked_t then
+ fprintf fmt "%s = _get_bool(f_in%i, \"%s\")" v.var_id id v'.var_id
+ else if Types.is_real_type unclocked_t then
+ if !Options.mpfr then
+ fprintf fmt "mpfr_set_d(%s, _get_double(f_in%i, \"%s\"), %i)" v.var_id id v'.var_id (Mpfr.mpfr_prec ())
+ else
+ fprintf fmt "%s = _get_double(f_in%i, \"%s\")" v.var_id id v'.var_id
+ else
+ begin
+ Global.main_node := !Options.main_node;
+ Format.eprintf "Code generation error: %a%a@."
+ Error.pp_error_msg Error.Main_wrong_kind
+ Location.pp_loc v'.var_loc;
+ raise (Error (v'.var_loc, Error.Main_wrong_kind))
+ end
+ in
+ Utils.List.iteri2 (fun idx v' v ->
+ fprintf fmt "@ %a;" pi ((idx+1), v', v);
+ ) m.mname.node_inputs m.mstep.step_inputs
+
(* Local Variables: *)
(* compile-command:"make -C ../../.." *)
diff --git a/src/backends/C/c_backend_header.ml b/src/backends/C/c_backend_header.ml
index 6fda2576..0ce6fbcb 100644
--- a/src/backends/C/c_backend_header.ml
+++ b/src/backends/C/c_backend_header.ml
@@ -35,15 +35,19 @@ struct
let print_import_standard fmt =
begin
+ (* if Machine_types.has_machine_type () then *)
+ (* begin *)
+ fprintf fmt "#include <stdint.h>@.";
+ (* end; *)
if !Options.mpfr then
begin
fprintf fmt "#include <mpfr.h>@."
end;
- if !Options.cpp then
- fprintf fmt "#include \"%s/arrow.hpp\"@.@." arrow_top_decl.top_decl_owner
- else
- fprintf fmt "#include \"%s/arrow.h\"@.@." arrow_top_decl.top_decl_owner
-
+ if !Options.cpp then
+ fprintf fmt "#include \"%s/arrow.hpp\"@.@." arrow_top_decl.top_decl_owner
+ else
+ fprintf fmt "#include \"%s/arrow.h\"@.@." arrow_top_decl.top_decl_owner
+
end
let rec print_static_val pp_var fmt v =
diff --git a/src/backends/C/c_backend_main.ml b/src/backends/C/c_backend_main.ml
index 04997137..4d149ee2 100644
--- a/src/backends/C/c_backend_main.ml
+++ b/src/backends/C/c_backend_main.ml
@@ -31,32 +31,13 @@ struct
(* Main related functions *)
(********************************************************************************************)
-let print_get_inputs fmt m =
- let pi fmt (id, v', v) =
- match (Types.unclock_type v.var_type).Types.tdesc with
- | Types.Tint -> fprintf fmt "%s = _get_int(f_in%i, \"%s\")" v.var_id id v'.var_id
- | Types.Tbool -> fprintf fmt "%s = _get_bool(f_in%i, \"%s\")" v.var_id id v'.var_id
- | Types.Treal when !Options.mpfr -> fprintf fmt "mpfr_set_d(%s, _get_double(f_in%i, \"%s\"), %i)" v.var_id id v'.var_id (Mpfr.mpfr_prec ())
- | Types.Treal -> fprintf fmt "%s = _get_double(f_in%i, \"%s\")" v.var_id id v'.var_id
- | _ ->
- begin
- Global.main_node := !Options.main_node;
- Format.eprintf "Code generation error: %a%a@."
- Error.pp_error_msg Error.Main_wrong_kind
- Location.pp_loc v'.var_loc;
- raise (Error (v'.var_loc, Error.Main_wrong_kind))
- end
- in
- List.iteri2 (fun idx v' v ->
- fprintf fmt "@ %a;" pi ((idx+1), v', v);
- ) m.mname.node_inputs m.mstep.step_inputs
let print_put_outputs fmt m =
let po fmt (id, o', o) =
let suff = string_of_int id in
print_put_var fmt suff o'.var_id o.var_type o.var_id
in
- Utils.List.iteri2 (fun idx v' v -> fprintf fmt "@ %a;" po ((idx+1), v', v)) m.mname.node_outputs m.mstep.step_outputs
+ List.iteri2 (fun idx v' v -> fprintf fmt "@ %a;" po ((idx+1), v', v)) m.mname.node_outputs m.mstep.step_outputs
let print_main_inout_declaration basename fmt m =
let mname = m.mname.node_id in
diff --git a/src/backends/C/c_backend_mauve.ml b/src/backends/C/c_backend_mauve.ml
index 0cb928ce..bd9c091b 100644
--- a/src/backends/C/c_backend_mauve.ml
+++ b/src/backends/C/c_backend_mauve.ml
@@ -43,12 +43,10 @@ let print_mauve_header fmt mauve_machine basename prog machines _ (*dependencies
let mauve_default_value v =
(* let v_name = v.var_id in *)
- let v_type = (Types.repr v.var_type).Types.tdesc in
- match v_type with
- | Types.Tbool -> "false"
- | Types.Tint -> "0"
- | Types.Treal -> "0.0"
- | _ -> assert false
+ if Types.is_bool_type v.var_type then "false"
+ else if Types.is_int_type v.var_type then "0"
+ else if Types.is_real_type v.var_type then "0.0"
+ else assert false
let print_mauve_default fmt mauve_machine v =
let v_name: string = v.var_id in
@@ -80,7 +78,7 @@ let print_mauve_shell fmt mauve_machine basename prog machines _ (*dependencies*
List.iter
(fun v ->
let v_name = v.var_id in
- let v_type = pp_c_basic_type_desc (Types.repr v.var_type).Types.tdesc in
+ let v_type = pp_c_basic_type_desc v.var_type in
fprintf fmt "\tReadPort<%s> & port_%s = mk_readPort<%s>(\"%s\", " v_type v_name v_type v_name;
print_mauve_default fmt mauve_machine v;
fprintf fmt ");@.";
@@ -90,7 +88,7 @@ let print_mauve_shell fmt mauve_machine basename prog machines _ (*dependencies*
List.iter
(fun v ->
let v_name = v.var_id in
- let v_type = pp_c_basic_type_desc (Types.repr v.var_type).Types.tdesc in
+ let v_type = pp_c_basic_type_desc v.var_type in
fprintf fmt "\tWritePort<%s> & port_%s = mk_writePort<%s>(\"%s\");@." v_type v_name v_type v_name;
) mauve_machine.mstep.step_outputs;
@@ -134,13 +132,13 @@ let print_mauve_core fmt mauve_machine basename prog machines _ (*dependencies*)
List.iter
(fun v ->
let v_name = v.var_id in
- let v_type = pp_c_basic_type_desc (Types.repr v.var_type).Types.tdesc in
+ let v_type = pp_c_basic_type_desc v.var_type in
fprintf fmt "\t\t%s %s = port_%s.read();@." v_type v_name v_name;
) mauve_machine.mstep.step_inputs;
List.iter
(fun v ->
let v_name = v.var_id in
- let v_type = pp_c_basic_type_desc (Types.repr v.var_type).Types.tdesc in
+ let v_type = pp_c_basic_type_desc v.var_type in
fprintf fmt "\t\t%s %s;@." v_type v_name;
) mauve_machine.mstep.step_outputs;
print_mauve_step fmt node_name mauve_machine;
diff --git a/src/backends/C/c_backend_src.ml b/src/backends/C/c_backend_src.ml
index b60ef8f2..50ab74fb 100644
--- a/src/backends/C/c_backend_src.ml
+++ b/src/backends/C/c_backend_src.ml
@@ -608,7 +608,7 @@ let print_global_init_code fmt basename prog dependencies =
let constants = List.map const_of_top (get_consts prog) in
fprintf fmt "@[<v 2>%a {@,static %s init = 0;@,@[<v 2>if (!init) { @,init = 1;@,%a%t%a@]@,}@,return;@]@,}@.@."
print_global_init_prototype baseNAME
- (pp_c_basic_type_desc Types.Tbool)
+ (pp_c_basic_type_desc Type_predef.type_bool)
(* constants *)
(Utils.fprintf_list ~sep:"@," (pp_const_initialize (pp_c_var_read Machine_code.empty_machine))) constants
(Utils.pp_final_char_if_non_empty "@," dependencies)
@@ -620,7 +620,7 @@ let print_global_clear_code fmt basename prog dependencies =
let constants = List.map const_of_top (get_consts prog) in
fprintf fmt "@[<v 2>%a {@,static %s clear = 0;@,@[<v 2>if (!clear) { @,clear = 1;@,%a%t%a@]@,}@,return;@]@,}@.@."
print_global_clear_prototype baseNAME
- (pp_c_basic_type_desc Types.Tbool)
+ (pp_c_basic_type_desc Type_predef.type_bool)
(* constants *)
(Utils.fprintf_list ~sep:"@," (pp_const_clear (pp_c_var_read Machine_code.empty_machine))) constants
(Utils.pp_final_char_if_non_empty "@," dependencies)
@@ -666,6 +666,10 @@ let print_machine dependencies fmt m =
let print_import_standard source_fmt =
begin
fprintf source_fmt "#include <assert.h>@.";
+ if Machine_types.has_machine_type () then
+ begin
+ fprintf source_fmt "#include <stdint.h>@."
+ end;
if not !Options.static_mem then
begin
fprintf source_fmt "#include <stdlib.h>@.";
diff --git a/src/backends/EMF/EMF_backend.ml b/src/backends/EMF/EMF_backend.ml
index 283ee0f6..06d647e8 100644
--- a/src/backends/EMF/EMF_backend.ml
+++ b/src/backends/EMF/EMF_backend.ml
@@ -197,6 +197,7 @@ and branch_instr_vars m i =
(reset_name f,
Corelang.mktyp loc Tydec_bool, Corelang.mkclock loc Ckdec_any,
false,
+ None,
None)
in
VSet.add reset_var args_vars
@@ -365,23 +366,40 @@ let rec pp_emf_instr m fmt i =
fprintf fmt "%a" pp_content i;
fprintf fmt "@]@]@ }"
and pp_emf_instrs m fmt instrs = fprintf_list ~sep:",@ " (pp_emf_instr m) fmt instrs
-
+
+let pp_emf_annot cpt fmt (key, ee) =
+ let _ =
+ fprintf fmt "\"ann%i\": { @[<hov 0>\"key\": [%a],@ \"eexpr\": %a@] }"
+ !cpt
+ (fprintf_list ~sep:"," (fun fmt s -> fprintf fmt "\"%s\"" s)) key
+ pp_emf_eexpr ee
+ in
+ incr cpt
+
+let pp_emf_annots cpt fmt annots = fprintf_list ~sep:",@ " (pp_emf_annot cpt) fmt annots.annots
+let pp_emf_annots_list cpt fmt annots_list = fprintf_list ~sep:",@ " (pp_emf_annots cpt) fmt annots_list
let pp_machine fmt m =
let instrs = (*merge_branches*) m.mstep.step_instrs in
try
fprintf fmt "@[<v 2>\"%a\": {@ "
print_protect (fun fmt -> pp_print_string fmt m.mname.node_id);
- fprintf fmt "\"kind\": %t,@ \"inputs\": [%a],@ \"outputs\": [%a],@ \"locals\": [%a],@ "
+ fprintf fmt "\"kind\": %t,@ "
(fun fmt -> if not ( snd (get_stateless_status m) )
then fprintf fmt "\"stateful\""
- else fprintf fmt "\"stateless\"")
- pp_emf_vars_decl m.mstep.step_inputs
- pp_emf_vars_decl m.mstep.step_outputs
- pp_emf_vars_decl m.mstep.step_locals
- ;
+ else fprintf fmt "\"stateless\"");
+ fprintf fmt "\"inputs\": [%a],@ "
+ pp_emf_vars_decl m.mstep.step_inputs;
+ fprintf fmt "\"outputs\": [%a],@ "
+ pp_emf_vars_decl m.mstep.step_outputs;
+ fprintf fmt "\"locals\": [%a],@ "
+ pp_emf_vars_decl m.mstep.step_locals;
+ fprintf fmt "\"mems\": [%a],@ "
+ pp_emf_vars_decl m.mmemory;
+
fprintf fmt "\"original_name\": \"%s\",@ " m.mname.node_id;
- fprintf fmt "\"instrs\": {@[<v 0> %a@]@ }"
+ fprintf fmt "\"instrs\": {@[<v 0> %a@]@ },@ "
(pp_emf_instrs m) instrs;
+ fprintf fmt "\"annots\": {@[<v 0> %a@]@ }" (pp_emf_annots_list (ref 0)) m.mannot;
fprintf fmt "@]@ }"
with Unhandled msg -> (
eprintf "[Error] @[<v 0>EMF backend@ Issues while translating node %s@ "
diff --git a/src/backends/EMF/EMF_common.ml b/src/backends/EMF/EMF_common.ml
index 2f0be110..43c2b614 100644
--- a/src/backends/EMF/EMF_common.ml
+++ b/src/backends/EMF/EMF_common.ml
@@ -86,7 +86,7 @@ fprintf fmt "uint16"
-let pp_cst_type c infered_typ fmt =
+let pp_cst_type fmt c (*infered_typ*) =
match c with
| Const_tag t ->
let typ = (Corelang.typedef_of_top (Hashtbl.find Corelang.tag_table t)) in
@@ -94,19 +94,17 @@ let pp_cst_type c infered_typ fmt =
fprintf fmt "bool"
else
pp_tag_type fmt typ
- | Const_int _ -> fprintf fmt "%s" !Options.int_type
- | Const_real _ -> fprintf fmt "%s" !Options.real_type
- | _ -> Format.eprintf "cst: %a@." Printers.pp_const c; assert false
+ | Const_int _ -> fprintf fmt "int" (*!Options.int_type*)
+ | Const_real _ -> fprintf fmt "real" (*!Options.real_type*)
+ | Const_string _ -> fprintf fmt "string"
+ | _ -> eprintf "cst: %a@." Printers.pp_const c; assert false
let rec pp_infered_type fmt t =
let open Types in
+ if is_bool_type t then fprintf fmt "bool" else
+ if is_int_type t then fprintf fmt "int" else (* !Options.int_type *)
+ if is_real_type t then fprintf fmt "real" else (* !Options.real_type *)
match t.tdesc with
- | Tint ->
- fprintf fmt "%s" !Options.int_type
- | Treal ->
- fprintf fmt "%s" !Options.real_type
- | Tbool ->
- fprintf fmt "bool"
| Tclock t ->
pp_infered_type fmt t
| Tstatic (_, t) ->
@@ -119,11 +117,12 @@ let rec pp_infered_type fmt t =
pp_tag_type fmt typ
| Tlink ty ->
pp_infered_type fmt ty
- | _ -> Format.eprintf "unhandled type: %a@." Types.print_node_ty t; assert false
+ | _ -> eprintf "unhandled type: %a@." Types.print_node_ty t; assert false
+
let rec pp_concrete_type dec_t infered_t fmt =
match dec_t with
- | Tydec_int -> fprintf fmt "%s" !Options.int_type
- | Tydec_real -> fprintf fmt "%s" !Options.real_type
+ | Tydec_int -> fprintf fmt "int" (* !Options.int_type *)
+ | Tydec_real -> fprintf fmt "real" (* !Options.real_type *)
(* TODO we could add more concrete types here if they were available in
dec_t *)
| Tydec_bool -> fprintf fmt "bool"
@@ -134,20 +133,25 @@ let rec pp_concrete_type dec_t infered_t fmt =
pp_tag_type fmt typ
)
| Tydec_any -> pp_infered_type fmt infered_t
- | _ -> Format.eprintf
+ | _ -> eprintf
"unhandled construct in type printing for EMF backend: %a@."
Printers.pp_var_type_dec_desc dec_t; raise (Failure "var")
-let pp_cst_type fmt v =
+(*let pp_cst_type fmt v =
match v.value_desc with
| Cst c-> pp_cst_type c v.value_type fmt (* constants do not have declared type (yet) *)
| _ -> assert false
-
+*)
+
let pp_var_type fmt v =
try
- pp_concrete_type v.var_dec_type.ty_dec_desc v.var_type fmt
- with Failure _ -> Format.eprintf "failed var: %a@." Printers.pp_var v; assert false
+ if Machine_types.is_specified v then
+ Machine_types.pp_var_type fmt v
+ else
+ pp_concrete_type v.var_dec_type.ty_dec_desc v.var_type fmt
+ with Failure _ -> eprintf "failed var: %a@." Printers.pp_var v; assert false
+
(******** Other print functions *)
let pp_emf_var_decl fmt v =
@@ -171,16 +175,16 @@ let pp_tag_id fmt t =
else
let const_list = match typ.tydef_desc with Tydec_enum tl -> tl | _ -> assert false in
fprintf fmt "%i" (get_idx t const_list)
-
-let pp_emf_cst_or_var fmt v =
- match v.value_desc with
- | Cst ((Const_tag t) as c)->
+
+let pp_emf_cst fmt c =
+ match c with
+ | Const_tag t->
let typ = (Corelang.typedef_of_top (Hashtbl.find Corelang.tag_table t)) in
if typ.tydef_id = "bool" then (
fprintf fmt "{@[\"type\": \"constant\",@ ";
fprintf fmt"\"value\": \"%a\",@ "
Printers.pp_const c;
- fprintf fmt "\"datatype\": \"%a\"@ " pp_cst_type v;
+ fprintf fmt "\"datatype\": \"%a\"@ " pp_cst_type c;
fprintf fmt "@]}"
)
else (
@@ -188,15 +192,25 @@ let pp_emf_cst_or_var fmt v =
pp_tag_id t;
fprintf fmt "\"origin_type\": \"%s\",@ \"origin_value\": \"%s\",@ "
typ.tydef_id t;
- fprintf fmt "\"datatype\": \"%a\"@ " pp_cst_type v;
+ fprintf fmt "\"datatype\": \"%a\"@ " pp_cst_type c;
fprintf fmt "@]}"
)
- | Cst c -> (
+ | Const_string s ->
+ fprintf fmt "{@[\"type\": \"constant\",@ \"value\": \"%s\",@ " s;
+ fprintf fmt "\"datatype\": \"%a\"@ " pp_cst_type c;
+ fprintf fmt "@]}"
+
+ | _ -> (
fprintf fmt "{@[\"type\": \"constant\",@ \"value\": \"%a\",@ "
Printers.pp_const c;
- fprintf fmt "\"datatype\": \"%a\"@ " pp_cst_type v;
+ fprintf fmt "\"datatype\": \"%a\"@ " pp_cst_type c;
fprintf fmt "@]}"
)
+
+
+let pp_emf_cst_or_var fmt v =
+ match v.value_desc with
+ | Cst c -> pp_emf_cst fmt c
| LocalVar v
| StateVar v -> (
fprintf fmt "{@[\"type\": \"variable\",@ \"value\": \"%a\",@ "
@@ -205,13 +219,59 @@ let pp_emf_cst_or_var fmt v =
fprintf fmt "\"datatype\": \"%a\"@ " pp_var_type v;
fprintf fmt "@]}"
)
- | _ -> Format.eprintf "Not of cst or var: %a@." Machine_code.pp_val v ; assert false (* Invalid argument *)
+ | _ -> eprintf "Not of cst or var: %a@." Machine_code.pp_val v ; assert false (* Invalid argument *)
let pp_emf_cst_or_var_list =
Utils.fprintf_list ~sep:",@ " pp_emf_cst_or_var
+(* Printer lustre expr and eexpr *)
+
+let rec pp_emf_expr fmt e =
+ match e.expr_desc with
+ | Expr_const c -> pp_emf_cst fmt c
+ | Expr_ident id ->
+ fprintf fmt "{@[\"type\": \"variable\",@ \"value\": \"%a\",@ "
+ print_protect (fun fmt -> pp_print_string fmt id);
+ fprintf fmt "\"datatype\": \"%t\"@ "
+ (pp_concrete_type
+ Tydec_any (* don't know much about that time since it was not
+ declared. That may not work with clock constants *)
+ e.expr_type
+ );
+ fprintf fmt "@]}"
+
+ | Expr_tuple el ->
+ fprintf fmt "[@[<hov 0>%a@ @]]"
+ (Utils.fprintf_list ~sep:",@ " pp_emf_expr) el
+ | _ -> (
+ Log.report ~level:2
+ (fun fmt ->
+ fprintf fmt "Warning: unhandled expression %a in annotation.@ "
+ Printers.pp_expr e;
+ fprintf fmt "Will not be produced in the experted JSON EMF"
+ );
+ fprintf fmt "\"unhandled construct, complain to Ploc\""
+ )
+(* Remaining constructs *)
+(* | Expr_ite of expr * expr * expr *)
+(* | Expr_arrow of expr * expr *)
+(* | Expr_fby of expr * expr *)
+(* | Expr_array of expr list *)
+(* | Expr_access of expr * Dimension.dim_expr *)
+(* | Expr_power of expr * Dimension.dim_expr *)
+(* | Expr_pre of expr *)
+(* | Expr_when of expr * ident * label *)
+(* | Expr_merge of ident * (label * expr) list *)
+(* | Expr_appl of call_t *)
+
+let pp_emf_eexpr fmt ee =
+ fprintf fmt "{@[<hov 0>\"quantifiers\": \"%a\",@ \"qfexpr\": @[%a@]@] }"
+ (Utils.fprintf_list ~sep:"; " Printers.pp_quantifiers) ee.eexpr_quantifiers
+ pp_emf_expr ee.eexpr_qfexpr
+
+
(* Local Variables: *)
(* compile-command: "make -C ../.." *)
(* End: *)
diff --git a/src/backends/Horn/horn_backend_common.ml b/src/backends/Horn/horn_backend_common.ml
index d00d0e1b..f1638544 100644
--- a/src/backends/Horn/horn_backend_common.ml
+++ b/src/backends/Horn/horn_backend_common.ml
@@ -19,10 +19,10 @@ let pp_machine_step_name fmt id = fprintf fmt "%s_step" id
let pp_machine_stateless_name fmt id = fprintf fmt "%s_fun" id
let rec pp_type fmt t =
+ if Types.is_bool_type t then fprintf fmt "Bool" else
+ if Types.is_int_type t then fprintf fmt "Int" else
+ if Types.is_real_type t then fprintf fmt "Real" else
match (Types.repr t).Types.tdesc with
- | Types.Tbool -> fprintf fmt "Bool"
- | Types.Tint -> fprintf fmt "Int"
- | Types.Treal -> fprintf fmt "Real"
| Types.Tconst ty -> pp_print_string fmt ty
| Types.Tclock t -> pp_type fmt t
| Types.Tarray(dim,ty) -> fprintf fmt "(Array Int "; pp_type fmt ty; fprintf fmt ")"
diff --git a/src/backends/Horn/horn_backend_printers.ml b/src/backends/Horn/horn_backend_printers.ml
index 529a033f..bcffe130 100644
--- a/src/backends/Horn/horn_backend_printers.ml
+++ b/src/backends/Horn/horn_backend_printers.ml
@@ -96,10 +96,11 @@ let rec get_type v =
for the type integer (arrays).
*)
let rec pp_default_val fmt t =
+ let t = Types.dynamic_type t in
+ if Types.is_bool_type t then fprintf fmt "true" else
+ if Types.is_int_type t then fprintf fmt "0" else
+ if Types.is_real_type t then fprintf fmt "0" else
match (Types.dynamic_type t).Types.tdesc with
- | Types.Tint -> fprintf fmt "0"
- | Types.Treal -> fprintf fmt "0"
- | Types.Tbool -> fprintf fmt "true"
| Types.Tarray(dim, l) -> (* TODO PL: this strange code has to be (heavily) checked *)
let valt = Types.array_element_type t in
fprintf fmt "((as const (Array Int %a)) %a)"
diff --git a/src/compiler_common.ml b/src/compiler_common.ml
index 4eeb238c..351f8229 100644
--- a/src/compiler_common.ml
+++ b/src/compiler_common.ml
@@ -262,4 +262,19 @@ let track_exception () =
else ()
-
+let update_vdecl_parents_prog prog =
+ let update_vdecl_parents parent v =
+ v.var_parent_nodeid <- Some parent
+ in
+ List.iter (
+ fun top -> match top.top_decl_desc with
+ | Node nd ->
+ List.iter
+ (update_vdecl_parents nd.node_id)
+ (nd.node_inputs @ nd.node_outputs @ nd.node_locals )
+ | ImportedNode ind ->
+ List.iter
+ (update_vdecl_parents ind.nodei_id)
+ (ind.nodei_inputs @ ind.nodei_outputs )
+ | _ -> ()
+ ) prog
diff --git a/src/compiler_stages.ml b/src/compiler_stages.ml
index 78c407b7..35b2d45c 100644
--- a/src/compiler_stages.ml
+++ b/src/compiler_stages.ml
@@ -48,6 +48,9 @@ let compile_source_to_header prog computed_types_env computed_clocks_env dirname
(* From prog to prog *)
let stage1 prog dirname basename =
+ (* Updating parent node information for variables *)
+ Compiler_common.update_vdecl_parents_prog prog;
+
(* Removing automata *)
let prog = expand_automata prog in
Log.report ~level:4 (fun fmt -> fprintf fmt ".. after automata expansion:@, @[<v 2>@,%a@]@ " Printers.pp_prog prog);
@@ -83,6 +86,10 @@ let stage1 prog dirname basename =
(* Clock calculus *)
let computed_clocks_env = clock_decls clock_env prog in
+ (* Registering and checking machine types *)
+ Machine_types.load prog;
+
+
(* Generating a .lusi header file only *)
if !Options.lusi then
(* We stop here the processing and produce the current prog. It will be
@@ -131,6 +138,7 @@ let stage1 prog dirname basename =
Typing.uneval_prog_generics prog;
Clock_calculus.uneval_prog_generics prog;
+
if !Options.global_inline && !Options.main_node <> "" && !Options.witnesses then
begin
let orig = Corelang.copy_prog orig in
@@ -160,7 +168,11 @@ let stage1 prog dirname basename =
else
prog
in
-
+
+
+ (* (\* Registering and checking machine types *\) *)
+ (* Machine_types.load prog; *)
+
(* Normalization phase *)
Log.report ~level:1 (fun fmt -> fprintf fmt ".. normalization@,");
let prog = Normalization.normalize_prog ~backend:!Options.output prog in
@@ -187,6 +199,103 @@ let stage1 prog dirname basename =
Access.check_prog prog;
end;
+
let prog = SortProg.sort_nodes_locals prog in
prog, dependencies
+
+
+ (* from source to machine code, with optimization *)
+let stage2 prog =
+ (* Computation of node equation scheduling. It also breaks dependency cycles
+ and warns about unused input or memory variables *)
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. @[<v 2>scheduling@ ");
+ let prog, node_schs =
+ try
+ Scheduling.schedule_prog prog
+ with Causality.Error _ -> (* Error is not kept. It is recomputed in a more
+ systemtic way in AlgebraicLoop module *)
+ AlgebraicLoop.analyze prog
+ in
+ Log.report ~level:1 (fun fmt -> fprintf fmt "%a" Scheduling.pp_warning_unused node_schs);
+ Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_schedule node_schs);
+ Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_fanin_table node_schs);
+ Log.report ~level:5 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_dep_graph node_schs);
+ Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
+ Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ ");
+
+ (* TODO Salsa optimize prog:
+ - emits warning for programs with pre inside expressions
+ - make sure each node arguments and memory is bounded by a local annotation
+ - introduce fresh local variables for each real pure subexpression
+ *)
+ (* DFS with modular code generation *)
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines generation@,");
+ let machine_code = Machine_code.translate_prog prog node_schs in
+
+ Log.report ~level:3 (fun fmt -> fprintf fmt ".. generated machines (unoptimized):@ %a@ "Machine_code.pp_machines machine_code);
+
+ (* Optimize machine code *)
+ Optimize_machine.optimize prog node_schs machine_code
+
+
+(* printing code *)
+let stage3 prog machine_code dependencies basename =
+ let basename = Filename.basename basename in
+ match !Options.output with
+ "C" ->
+ begin
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,");
+ C_backend.translate_to_c
+ (* alloc_header_file source_lib_file source_main_file makefile_file *)
+ basename prog machine_code dependencies
+ end
+ | "java" ->
+ begin
+ (Format.eprintf "internal error: sorry, but not yet supported !"; assert false)
+ (*let source_file = basename ^ ".java" in
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. opening file %s@,@?" source_file);
+ let source_out = open_out source_file in
+ let source_fmt = formatter_of_out_channel source_out in
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. java code generation@,@?");
+ Java_backend.translate_to_java source_fmt basename normalized_prog machine_code;*)
+ end
+ | "horn" ->
+ begin
+ let destname = !Options.dest_dir ^ "/" ^ basename in
+ let source_file = destname ^ ".smt2" in (* Could be changed *)
+ let source_out = open_out source_file in
+ let fmt = formatter_of_out_channel source_out in
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. hornification@,");
+ Horn_backend.translate fmt basename prog (Machine_code.arrow_machine::machine_code);
+ (* Tracability file if option is activated *)
+ if !Options.traces then (
+ let traces_file = destname ^ ".traces.xml" in (* Could be changed *)
+ let traces_out = open_out traces_file in
+ let fmt = formatter_of_out_channel traces_out in
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. tracing info@,");
+ Horn_backend_traces.traces_file fmt basename prog machine_code;
+ )
+ end
+ | "lustre" ->
+ begin
+ let destname = !Options.dest_dir ^ "/" ^ basename in
+ let source_file = destname ^ ".lustrec.lus" in (* Could be changed *)
+ let source_out = open_out source_file in
+ let fmt = formatter_of_out_channel source_out in
+ Printers.pp_prog fmt prog;
+ Format.fprintf fmt "@.@?";
+ (* Lustre_backend.translate fmt basename normalized_prog machine_code *)
+ ()
+ end
+ | "emf" ->
+ begin
+ let destname = !Options.dest_dir ^ "/" ^ basename in
+ let source_file = destname ^ ".emf" in (* Could be changed *)
+ let source_out = open_out source_file in
+ let fmt = formatter_of_out_channel source_out in
+ EMF_backend.translate fmt basename prog machine_code;
+ ()
+ end
+
+ | _ -> assert false
diff --git a/src/corelang.ml b/src/corelang.ml
index 8446d910..3573a1cc 100755
--- a/src/corelang.ml
+++ b/src/corelang.ml
@@ -41,7 +41,7 @@ let mktyp loc d =
let mkclock loc d =
{ ck_dec_desc = d; ck_dec_loc = loc }
-let mkvar_decl loc ?(orig=false) (id, ty_dec, ck_dec, is_const, value) =
+let mkvar_decl loc ?(orig=false) (id, ty_dec, ck_dec, is_const, value, parentid) =
assert (value = None || is_const);
{ var_id = id;
var_orig = orig;
@@ -49,6 +49,7 @@ let mkvar_decl loc ?(orig=false) (id, ty_dec, ck_dec, is_const, value) =
var_dec_clock = ck_dec;
var_dec_const = is_const;
var_dec_value = value;
+ var_parent_nodeid = parentid;
var_type = Types.new_var ();
var_clock = Clocks.new_var true;
var_loc = loc }
@@ -62,13 +63,14 @@ let mkexpr loc d =
expr_annot = None;
expr_loc = loc }
-let var_decl_of_const c =
+let var_decl_of_const ?(parentid=None) c =
{ var_id = c.const_id;
var_orig = true;
var_dec_type = { ty_dec_loc = c.const_loc; ty_dec_desc = Tydec_any };
var_dec_clock = { ck_dec_loc = c.const_loc; ck_dec_desc = Ckdec_any };
var_dec_const = true;
var_dec_value = None;
+ var_parent_nodeid = parentid;
var_type = c.const_type;
var_clock = Clocks.new_var false;
var_loc = c.const_loc }
@@ -626,6 +628,7 @@ let get_node_interface nd =
nodei_outputs = nd.node_outputs;
nodei_stateless = nd.node_dec_stateless;
nodei_spec = nd.node_spec;
+ (* nodei_annot = nd.node_annot; *)
nodei_prototype = None;
nodei_in_lib = [];
}
@@ -901,7 +904,7 @@ let vdecls_of_typ_ck cpt ty =
List.map
(fun _ -> incr cpt;
let name = sprintf "_var_%d" !cpt in
- mkvar_decl loc (name, mktyp loc Tydec_any, mkclock loc Ckdec_any, false, None))
+ mkvar_decl loc (name, mktyp loc Tydec_any, mkclock loc Ckdec_any, false, None, None))
(Types.type_list_of_type ty)
let mk_internal_node id =
@@ -920,6 +923,7 @@ let mk_internal_node id =
nodei_outputs = vdecls_of_typ_ck cpt tout;
nodei_stateless = Types.get_static_value ty <> None;
nodei_spec = spec;
+ (* nodei_annot = []; *)
nodei_prototype = None;
nodei_in_lib = [];
})
@@ -1104,7 +1108,7 @@ and node_has_arrows node =
let copy_var_decl vdecl =
- 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)
+ 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, vdecl.var_parent_nodeid)
let copy_const cdecl =
{ cdecl with const_type = Types.new_var () }
diff --git a/src/corelang.mli b/src/corelang.mli
index 17726b40..da1f8161 100755
--- a/src/corelang.mli
+++ b/src/corelang.mli
@@ -20,9 +20,16 @@ val dummy_clock_dec: clock_dec
val mktyp: Location.t -> type_dec_desc -> type_dec
val mkclock: Location.t -> clock_dec_desc -> clock_dec
-val mkvar_decl: Location.t -> ?orig:bool -> ident * type_dec * clock_dec * bool (* is const *) * expr option (* value *) -> var_decl
-
-val var_decl_of_const: const_desc -> var_decl
+val mkvar_decl: Location.t -> ?orig:bool ->
+ ident *
+ type_dec *
+ clock_dec *
+ bool (* is const *) *
+ expr option (* value *) *
+ string option (* parent id *)
+ -> var_decl
+
+val var_decl_of_const: ?parentid:LustreSpec.ident option -> const_desc -> var_decl
val mkexpr: Location.t -> expr_desc -> expr
val mkeq: Location.t -> ident list * expr -> eq
val mkassert: Location.t -> expr -> assert_t
diff --git a/src/env.ml b/src/env.ml
index 9fc32db2..38c03808 100755
--- a/src/env.ml
+++ b/src/env.ml
@@ -27,6 +27,7 @@ let exists_value env ident =
IMap.mem ident env
let iter env f = IMap.iter f env
+let fold = IMap.fold
(* Merges x and y. In case of conflicting definitions,
overwrites definitions in x by definitions in y *)
diff --git a/src/features/machine_types/machine_types.ml b/src/features/machine_types/machine_types.ml
new file mode 100644
index 00000000..8d67293f
--- /dev/null
+++ b/src/features/machine_types/machine_types.ml
@@ -0,0 +1,479 @@
+(* Extension du deal with machine types annotation
+
+ In each node, node local annotations can specify the actual type of the
+ implementation uintXX, intXX, floatXX ...
+
+ The module provide utility functions to query the model:
+ - get_var_machine_type varid nodeid returns the string denoting the actual type
+
+ The actual type is used at different stages of the coompilation
+ - early stage: limited typing, ie validity of operation are checked
+ - a first version ensures that the actual type is a subtype of the declared/infered ones
+ eg uint8 is a valid subtype of int
+ - a future implementation could ensures that operations are valid
+ - each standard or unspecified operation should be homogeneous :
+ op: real -> real -> real is valid for any same subtype t of real: op: t -> t -> t
+ - specific nodes that explicitely defined subtypes could be used to perform casts
+ eg. a int2uint8 (i: int) returns (j: int) with annotations specifying i as int and j as uint8
+ - C backend: any print of a typed variable should rely on the actual machine type when provided
+ - EMF backend: idem
+ - Horn backend: an option could enforce the bounds provided by the machine
+ type or implement the cycling behavior for integer subtypes
+ - Salsa plugin: the information should be propagated to the plugin.
+ One can also imagine that results of the analysis could specify or
+ substitute a type by a subtype. Eg. the analysis detects that a float32 is enough for variable z and
+ the annotation is added to the node.
+
+
+A posisble behavior could be
+- an option to ensure type checking
+- dedicated conversion functions that, in C, would generate cast or calls to simple identity functions (to be inlined)
+
+
+
+TODO
+EMF: rajouter les memoires dans les caracteristiques du node
+ gerer les types plus finement:
+ propager les types machines aux variables fraiches creees par la normalisation
+
+*)
+open LustreSpec
+
+let keyword = ["machine_types"]
+
+module MT =
+struct
+
+ type int_typ =
+ | Tint8_t
+ | Tint16_t
+ | Tint32_t
+ | Tint64_t
+ | Tuint8_t
+ | Tuint16_t
+ | Tuint32_t
+ | Tuint64_t
+
+ let pp_int fmt t =
+ match t with
+ | Tint8_t -> Format.fprintf fmt "int8"
+ | Tint16_t -> Format.fprintf fmt "int16"
+ | Tint32_t -> Format.fprintf fmt "int32"
+ | Tint64_t -> Format.fprintf fmt "int64"
+ | Tuint8_t -> Format.fprintf fmt "uint8"
+ | Tuint16_t -> Format.fprintf fmt "uint16"
+ | Tuint32_t -> Format.fprintf fmt "uint32"
+ | Tuint64_t -> Format.fprintf fmt "uint64"
+
+ let pp_c_int fmt t =
+ match t with
+ | Tint8_t -> Format.fprintf fmt "int8_t"
+ | Tint16_t -> Format.fprintf fmt "int16_t"
+ | Tint32_t -> Format.fprintf fmt "int32_t"
+ | Tint64_t -> Format.fprintf fmt "int64_t"
+ | Tuint8_t -> Format.fprintf fmt "uint8_t"
+ | Tuint16_t -> Format.fprintf fmt "uint16_t"
+ | Tuint32_t -> Format.fprintf fmt "uint32_t"
+ | Tuint64_t -> Format.fprintf fmt "uint64_t"
+
+ type t =
+ | MTint of int_typ option
+ | MTreal of string option
+ | MTbool
+ | MTstring
+
+ open Format
+ let pp fmt t =
+ match t with
+ | MTint None ->
+ fprintf fmt "int"
+ | MTint (Some s) ->
+ fprintf fmt "%a" pp_int s
+ | MTreal None ->
+ fprintf fmt "real"
+ | MTreal (Some s) ->
+ fprintf fmt "%s" s
+ | MTbool ->
+ fprintf fmt "bool"
+ | MTstring ->
+ fprintf fmt "string"
+
+ let pp_c fmt t =
+ match t with
+ | MTint (Some s) ->
+ fprintf fmt "%a" pp_c_int s
+ | MTreal (Some s) ->
+ fprintf fmt "%s" s
+ | MTint None
+ | MTreal None
+ | MTbool
+ | MTstring -> assert false
+
+
+ let is_scalar_type t =
+ match t with
+ | MTbool
+ | MTint _
+ | MTreal _ -> true
+ | _ -> false
+
+
+ let is_numeric_type t =
+ match t with
+ | MTint _
+ | MTreal _ -> true
+ | _ -> false
+
+ let is_int_type t = match t with MTint _ -> true | _ -> false
+ let is_real_type t = match t with MTreal _ -> true | _ -> false
+ let is_bool_type t = t = MTbool
+
+ let is_dimension_type t =
+ match t with
+ | MTint _
+ | MTbool -> true
+ | _ -> false
+
+ let type_int_builder = MTint None
+ let type_real_builder = MTreal None
+ let type_bool_builder = MTbool
+ let type_string_builder = MTstring
+
+ let unify _ _ = ()
+ let is_unifiable b1 b2 =
+ match b1, b2 with
+ | MTint _ , MTint _
+ | MTreal _, MTreal _
+ | MTstring, MTstring
+ | MTbool, MTbool -> true
+ | _ -> false
+
+ let is_exportable b =
+ match b with
+ | MTstring
+ | MTbool
+ | MTreal None
+ | MTint None -> false
+ | _ -> true
+end
+
+module MTypes = Types.Make (MT)
+
+let type_uint8 = MTypes.new_ty (MTypes.Tbasic (MT.MTint (Some MT.Tuint8_t)))
+let type_uint16 = MTypes.new_ty (MTypes.Tbasic (MT.MTint (Some MT.Tuint16_t)))
+let type_uint32 = MTypes.new_ty (MTypes.Tbasic (MT.MTint (Some MT.Tuint32_t)))
+let type_uint64 = MTypes.new_ty (MTypes.Tbasic (MT.MTint (Some MT.Tuint64_t)))
+let type_int8 = MTypes.new_ty (MTypes.Tbasic (MT.MTint (Some MT.Tint8_t)))
+let type_int16 = MTypes.new_ty (MTypes.Tbasic (MT.MTint (Some MT.Tint16_t)))
+let type_int32 = MTypes.new_ty (MTypes.Tbasic (MT.MTint (Some MT.Tint32_t)))
+let type_int64 = MTypes.new_ty (MTypes.Tbasic (MT.MTint (Some MT.Tint64_t)))
+
+
+module ConvTypes =
+ struct
+ type type_expr = MTypes.type_expr
+
+ let map_type_basic f_basic =
+ let rec map_type_basic e =
+ { MTypes.tid = e.Types.tid;
+ MTypes.tdesc = map_type_basic_desc (Types.type_desc e)
+ }
+ and map_type_basic_desc td =
+ let mape = map_type_basic in
+ match td with
+ | Types.Tbasic b -> f_basic b
+ | Types.Tconst c -> MTypes.Tconst c
+ | Types.Tenum e -> MTypes.Tenum e
+ | Types.Tvar -> MTypes.Tvar
+ | Types.Tunivar -> MTypes.Tunivar
+
+ | Types.Tclock te -> MTypes.Tclock (mape te)
+ | Types.Tarrow (te1, te2) -> MTypes.Tarrow (mape te1, mape te2)
+ | Types.Ttuple tel -> MTypes.Ttuple (List.map mape tel)
+ | Types.Tstruct id_te_l -> MTypes.Tstruct (List.map (fun (id, te) -> id, mape te) id_te_l)
+ | Types.Tarray (de, te) -> MTypes.Tarray (de, mape te)
+ | Types.Tstatic (de, te) -> MTypes.Tstatic (de, mape te)
+ | Types.Tlink te -> MTypes.Tlink (mape te)
+ in
+ map_type_basic
+
+ let import main_typ =
+ let import_basic b =
+ if Types.BasicT.is_int_type b then MTypes.type_int else
+ if Types.BasicT.is_real_type b then MTypes.type_real else
+ if Types.BasicT.is_bool_type b then MTypes.type_bool else
+ (Format.eprintf "importing %a with issues!@.@?" Types.print_ty main_typ; assert false)
+ in
+ map_type_basic import_basic main_typ
+
+
+ let map_mtype_basic f_basic =
+ let rec map_mtype_basic e =
+ { Types.tid = e.MTypes.tid;
+ Types.tdesc = map_mtype_basic_desc (MTypes.type_desc e)
+ }
+ and map_mtype_basic_desc td =
+ let mape = map_mtype_basic in
+ match td with
+ | MTypes.Tbasic b ->
+ (* Format.eprintf "supposely basic mtype: %a@." MTypes.BasicT.pp b; *)
+ f_basic b
+ | MTypes.Tconst c -> Types.Tconst c
+ | MTypes.Tenum e -> Types.Tenum e
+ | MTypes.Tvar -> Types.Tvar
+ | MTypes.Tunivar -> Types.Tunivar
+
+ | MTypes.Tclock te -> Types.Tclock (mape te)
+ | MTypes.Tarrow (te1, te2) -> Types.Tarrow (mape te1, mape te2)
+ | MTypes.Ttuple tel -> Types.Ttuple (List.map mape tel)
+ | MTypes.Tstruct id_te_l -> Types.Tstruct (List.map (fun (id, te) -> id, mape te) id_te_l)
+ | MTypes.Tarray (de, te) -> Types.Tarray (de, mape te)
+ | MTypes.Tstatic (de, te) -> Types.Tstatic (de, mape te)
+ | MTypes.Tlink te -> Types.Tlink (mape te)
+ in
+ map_mtype_basic
+
+ let export machine_type =
+ let export_basic b =
+ if MTypes.BasicT.is_int_type b then Types.type_int else
+ if MTypes.BasicT.is_real_type b then Types.type_real else
+ if MTypes.BasicT.is_bool_type b then Types.type_bool else
+ (
+ Format.eprintf "unhandled basic mtype is %a. Issues while dealing with basic type %a@.@?" MTypes.print_ty machine_type MTypes.BasicT.pp b;
+ assert false
+ )
+ in
+ map_mtype_basic export_basic machine_type
+
+ end
+
+module Typing = Typing.Make (MTypes) (ConvTypes)
+
+(* Associate to each (node_id, var_id) its machine type *)
+let machine_type_table : (var_decl, MTypes.type_expr) Hashtbl.t = Hashtbl.create 13
+
+(* Store the node signatures, with machine types when available *)
+let typing_env = ref Env.initial
+
+let is_specified v =
+ (* Format.eprintf "looking for var %a@." Printers.pp_var v; *)
+ Hashtbl.mem machine_type_table v
+
+let pp_table fmt =
+ Format.fprintf fmt "@[<v 0>[";
+ Hashtbl.iter
+ (fun v typ -> Format.fprintf fmt "%a -> %a,@ " Printers.pp_var v MTypes.print_ty typ )
+ machine_type_table;
+ Format.fprintf fmt "@]"
+
+
+let get_specified_type v =
+ (* Format.eprintf "Looking for variable %a in table [%t]@.@?" *)
+ (* Printers.pp_var v *)
+ (* pp_table; *)
+ Hashtbl.find machine_type_table v
+
+let is_exportable v =
+ is_specified v && (
+ let typ = get_specified_type v in
+ match (MTypes.dynamic_type typ).MTypes.tdesc with
+ | MTypes.Tbasic b -> MT.is_exportable b
+ | _ -> assert false (* TODO deal with other constructs *)
+ )
+(* could depend on the actual computed type *)
+
+let type_name typ =
+ MTypes.print_ty Format.str_formatter typ;
+ Format.flush_str_formatter ()
+
+let pp_var_type fmt v =
+ let typ = get_specified_type v in
+ MTypes.print_ty fmt typ
+
+let pp_c_var_type fmt v =
+ let typ = get_specified_type v in
+ MTypes.print_ty_param MT.pp_c fmt typ
+
+(************** Checking types ******************)
+
+let erroneous_annotation loc =
+ Format.eprintf "Invalid annotation for machine_type at loc %a@."
+ Location.pp_loc loc;
+ assert false
+
+
+let valid_subtype subtype typ =
+ let mismatch subtyp typ =
+ Format.eprintf "Subtype mismatch %a vs %a@." MTypes.print_ty subtyp Types.print_ty typ; false
+ in
+ match (MTypes.dynamic_type subtype).MTypes.tdesc with
+
+ | MTypes.Tbasic MT.MTint _ -> Types.is_int_type typ
+ | MTypes.Tbasic MT.MTreal _ -> Types.is_real_type typ
+ | MTypes.Tbasic MT.MTbool -> Types.is_bool_type typ
+ | _ -> mismatch subtype typ
+
+let type_of_name name =
+ match name with
+ | "uint8" -> type_uint8
+ | "uint16" -> type_uint16
+ | "uint32" -> type_uint32
+ | "uint64" -> type_uint64
+ | "int8" -> type_int8
+ | "int16" -> type_int16
+ | "int32" -> type_int32
+ | "int64" -> type_int64
+ | _ -> assert false (* unknown custom machine type *)
+
+let register_var var typ =
+ (* let typ = type_of_name type_name in *)
+ if valid_subtype typ var.var_type then (
+ Hashtbl.add machine_type_table var typ
+ )
+ else
+ erroneous_annotation var.var_loc
+
+(* let register_var_opt var type_name_opt = *)
+(* match type_name_opt with *)
+(* | None -> () *)
+(* | Some type_name -> register_var var type_name *)
+
+(************** Registering annotations ******************)
+
+
+let register_node node_id vars annots =
+ List.fold_left (fun accu annot ->
+ let annl = annot.annots in
+ List.fold_left (fun accu (kwd, value) ->
+ if kwd = keyword then
+ let expr = value.eexpr_qfexpr in
+ match Corelang.expr_list_of_expr expr with
+ | [var_id; type_name] -> (
+ match var_id.expr_desc, type_name.expr_desc with
+ | Expr_ident var_id, Expr_const (Const_string type_name) ->
+ let var = List.find (fun v -> v.var_id = var_id) vars in
+ Log.report ~level:2 (fun fmt ->
+ Format.fprintf fmt "Recorded type %s for variable %a (parent node is %s)@ "
+ type_name
+ Printers.pp_var var
+ (match var.var_parent_nodeid with Some id -> id | None -> "unknown")
+ );
+ let typ = type_of_name type_name in
+ register_var var typ;
+ var::accu
+ | _ -> erroneous_annotation expr.expr_loc
+ )
+ | _ -> erroneous_annotation expr.expr_loc
+ else
+ accu
+ ) accu annl
+ ) [] annots
+
+
+let check_node nd vars =
+(* TODO check that all access to vars are valid *)
+ ()
+
+let type_of_vlist vars =
+ let tyl = List.map (fun v -> if is_specified v then get_specified_type v else
+ ConvTypes.import v.var_type
+ ) vars in
+ MTypes.type_of_type_list tyl
+
+
+let load prog =
+ let init_env =
+ Env.fold (fun id typ env ->
+ Env.add_value env id (ConvTypes.import typ)
+ )
+ Basic_library.type_env Env.initial in
+ let env =
+ List.fold_left (fun type_env top ->
+ match top.top_decl_desc with
+ | Node nd ->
+ (* Format.eprintf "Registeing node %s@." nd.node_id; *)
+ let vars = nd.node_inputs @ nd.node_outputs @ nd.node_locals in
+ let constrained_vars = register_node nd.node_id vars nd.node_annot in
+ check_node nd constrained_vars;
+
+ (* Computing the node type *)
+ let ty_ins = type_of_vlist nd.node_inputs in
+ let ty_outs = type_of_vlist nd.node_outputs in
+ let ty_node = MTypes.new_ty (MTypes.Tarrow (ty_ins,ty_outs)) in
+ Typing.generalize ty_node;
+ let env = Env.add_value type_env nd.node_id ty_node in
+ (* Format.eprintf "Env: %a" (Env.pp_env MTypes.print_ty) env; *)
+ env
+
+ | _ -> type_env
+ (* | ImportedNode ind -> *)
+ (* let vars = ind.nodei_inputs @ ind.nodei_outputs in *)
+ (* register_node ind.nodei_id vars ind.nodei_annot *)
+(* | _ -> () TODO: shall we load something for Open statements? *)
+ ) init_env prog
+ in
+ typing_env := env
+
+let type_expr nd expr =
+ let init_env = !typing_env in
+ (* Format.eprintf "Init env: %a@." (Env.pp_env MTypes.print_ty) init_env; *)
+ let init_vars = nd.node_inputs @ nd.node_outputs @ nd.node_locals in
+ (* Rebuilding the variables environment from accumulated knowledge *)
+ let env,vars = (* First, we add non specified variables *)
+ List.fold_left (fun (env, vars) v ->
+ if not (is_specified v) then
+ let env = Env.add_value env v.var_id (ConvTypes.import v.var_type) in
+ env, v::vars
+ else
+ env, vars
+ ) (init_env, []) init_vars
+ in
+
+ (* Then declared ones *)
+ let env, vars =
+ Hashtbl.fold (fun vdecl machine_type (env, vds) ->
+ if vdecl.var_parent_nodeid = Some nd.node_id then (
+ (* Format.eprintf "Adding variable %a to the environement@." Printers.pp_var vdecl; *)
+ let env = Env.add_value env vdecl.var_id machine_type in
+ env, vdecl::vds
+ )
+ else
+ env, vds
+ ) machine_type_table (env, vars)
+ in
+
+
+ (* Format.eprintf "env with local vars: %a@." (Env.pp_env MTypes.print_ty) env; *)
+ (* Format.eprintf "expr = %a@." Printers.pp_expr expr; *)
+ (* let res = *)
+ Typing.type_expr
+ (env,vars)
+ false (* not in main node *)
+ false (* no a constant *)
+ expr
+ (* in *)
+ (* Format.eprintf "typing ok = %a@." MTypes.print_ty res; *)
+ (* res *)
+
+(* Typing the expression (vars = expr) in node
+
+*)
+let type_def node vars expr =
+ (* Format.eprintf "Typing def %a = %a@.@." *)
+ (* (Utils.fprintf_list ~sep:", " Printers.pp_var) vars *)
+ (* Printers.pp_expr expr *)
+ (* ; *)
+ let typ = type_expr node expr in
+ (* Format.eprintf "Type is %a. Saving stuff@.@." MTypes.print_ty typ; *)
+ let typ = MTypes.type_list_of_type typ in
+ List.iter2 register_var vars typ
+
+let has_machine_type () =
+ let annl = Annotations.get_expr_annotations keyword in
+ Format.eprintf "has _mchine _type annotations: %i@." (List.length annl);
+ List.length annl > 0
+
+(* Local Variables: *)
+(* compile-command:"make -C ../.." *)
+(* End: *)
+
diff --git a/src/global.ml b/src/global.ml
index 892f630c..638dda6f 100644
--- a/src/global.ml
+++ b/src/global.ml
@@ -1,3 +1,5 @@
+module Types = Types.Main
+
let type_env : (Types.type_expr Env.t) ref = ref Env.initial
let clock_env : (Clocks.clock_expr Env.t) ref = ref Env.initial
let basename = ref ""
diff --git a/src/inliner.ml b/src/inliner.ml
index 33935a03..235c3bd7 100644
--- a/src/inliner.ml
+++ b/src/inliner.ml
@@ -137,7 +137,9 @@ let inline_call node loc uid args reset locals caller =
{ v.var_dec_type with ty_dec_desc = Corelang.rename_static rename_static v.var_dec_type.ty_dec_desc },
{ v.var_dec_clock with ck_dec_desc = Corelang.rename_carrier rename_carrier v.var_dec_clock.ck_dec_desc },
v.var_dec_const,
- Utils.option_map (rename_expr (fun x -> x) rename) v.var_dec_value) in
+ Utils.option_map (rename_expr (fun x -> x) rename) v.var_dec_value,
+ v.var_parent_nodeid (* we keep the original parent name *)
+ ) in
begin
(*
(try
@@ -358,7 +360,9 @@ let witness filename main_name orig inlined type_env clock_env =
{ty_dec_desc=Tydec_bool; ty_dec_loc=loc},
{ck_dec_desc=Ckdec_any; ck_dec_loc=loc},
false,
- None)
+ None,
+ None
+ )
) (Utils.enumerate nb_outputs)
in
@@ -369,7 +373,9 @@ let witness filename main_name orig inlined type_env clock_env =
{ty_dec_desc=Tydec_bool; ty_dec_loc=loc},
{ck_dec_desc=Ckdec_any; ck_dec_loc=loc},
false,
- None)
+ None,
+ None
+ )
in
let main_ok_expr =
let mkv x = mkexpr loc (Expr_ident x) in
diff --git a/src/lexerLustreSpec.mll b/src/lexerLustreSpec.mll
index 8027d3e8..81150fc0 100644
--- a/src/lexerLustreSpec.mll
+++ b/src/lexerLustreSpec.mll
@@ -154,9 +154,9 @@ and string_parse = parse
try
Parser_lustre.lustre_annot(* ParserLustreSpec.lustre_annot *) token lexbuf
with Parsing.Parse_error as _e -> (
- Format.eprintf "Lexing error at position %a:@.unexpected token %s@.@?"
+ Format.eprintf "Lexing error at position %a:@.unexpected token %s when parsing annotation %s@.@?"
(fun fmt p -> Format.fprintf fmt "%s l%i c%i" p.Lexing.pos_fname p.Lexing.pos_lnum p.Lexing.pos_cnum) lexbuf.Lexing.lex_curr_p
- (Lexing.lexeme lexbuf);
+ (Lexing.lexeme lexbuf) s;
raise (Error (Location.curr lexbuf)))
diff --git a/src/lustreSpec.ml b/src/lustreSpec.ml
index 82888e0f..e6f5ab2d 100644
--- a/src/lustreSpec.ml
+++ b/src/lustreSpec.ml
@@ -8,7 +8,7 @@
(* version 2.1. *)
(* *)
(********************************************************************)
-
+
type ident = Utils.ident
type rat = Utils.rat
type tag = Utils.tag
@@ -63,6 +63,7 @@ type var_decl =
var_dec_clock: clock_dec;
var_dec_const: bool;
var_dec_value: expr option;
+ mutable var_parent_nodeid: ident option;
mutable var_type: Types.type_expr;
mutable var_clock: Clocks.clock_expr;
var_loc: Location.t}
@@ -184,6 +185,7 @@ type imported_node_desc =
nodei_outputs: var_decl list;
nodei_stateless: bool;
nodei_spec: node_annot option;
+ (* nodei_annot: expr_annot list; *)
nodei_prototype: string option;
nodei_in_lib: string list;
}
diff --git a/src/machine_code.ml b/src/machine_code.ml
index 7288d6ac..e583dec7 100644
--- a/src/machine_code.ml
+++ b/src/machine_code.ml
@@ -178,6 +178,7 @@ let dummy_var_decl name typ =
var_dec_clock = dummy_clock_dec;
var_dec_const = false;
var_dec_value = None;
+ var_parent_nodeid = None;
var_type = typ;
var_clock = Clocks.new_ck Clocks.Cvar true;
var_loc = Location.dummy_loc
@@ -218,7 +219,7 @@ let mk_val v t = { value_desc = v;
let arrow_machine =
let state = "_first" in
- let var_state = dummy_var_decl state (Types.new_ty Types.Tbool) in
+ let var_state = dummy_var_decl state Type_predef.type_bool(* (Types.new_ty Types.Tbool) *) in
let var_input1 = List.nth arrow_desc.node_inputs 0 in
let var_input2 = List.nth arrow_desc.node_inputs 1 in
let var_output = List.nth arrow_desc.node_outputs 0 in
@@ -622,10 +623,11 @@ let translate_decl nd sch =
mktyp loc Tydec_bool,
mkclock loc Ckdec_any,
false, (* not a constant *)
- None (* no default value *)
+ None, (* no default value *)
+ Some nd.node_id
)
in
- assert_var.var_type <- Types.new_ty (Types.Tbool);
+ assert_var.var_type <- Type_predef.type_bool (* Types.new_ty (Types.Tbool) *);
let eq = mkeq loc ([var_id], expr) in
(i+1, assert_var::vars, eq::eqlist, {expr with expr_desc = Expr_ident var_id}::assertlist)
) (1, [], [], []) exprl
diff --git a/src/main_lustre_compiler.ml b/src/main_lustre_compiler.ml
index 8932d19c..51af25f9 100644
--- a/src/main_lustre_compiler.ml
+++ b/src/main_lustre_compiler.ml
@@ -55,100 +55,6 @@ let compile_header dirname basename extension =
-(* from source to machine code, with optimization *)
-let stage2 prog =
- (* Computation of node equation scheduling. It also breaks dependency cycles
- and warns about unused input or memory variables *)
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. @[<v 2>scheduling@ ");
- let prog, node_schs =
- try
- Scheduling.schedule_prog prog
- with Causality.Error _ -> (* Error is not kept. It is recomputed in a more
- systemtic way in AlgebraicLoop module *)
- AlgebraicLoop.analyze prog
- in
- Log.report ~level:1 (fun fmt -> fprintf fmt "%a" Scheduling.pp_warning_unused node_schs);
- Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_schedule node_schs);
- Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_fanin_table node_schs);
- Log.report ~level:5 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_dep_graph node_schs);
- Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
- Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ ");
-
- (* TODO Salsa optimize prog:
- - emits warning for programs with pre inside expressions
- - make sure each node arguments and memory is bounded by a local annotation
- - introduce fresh local variables for each real pure subexpression
- *)
- (* DFS with modular code generation *)
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines generation@,");
- let machine_code = Machine_code.translate_prog prog node_schs in
-
- Log.report ~level:3 (fun fmt -> fprintf fmt ".. generated machines (unoptimized):@ %a@ "Machine_code.pp_machines machine_code);
-
- (* Optimize machine code *)
- Optimize_machine.optimize prog node_schs machine_code
-
-
-(* printing code *)
-let stage3 prog machine_code dependencies basename =
- let basename = Filename.basename basename in
- match !Options.output with
- "C" ->
- begin
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,");
- C_backend.translate_to_c
- (* alloc_header_file source_lib_file source_main_file makefile_file *)
- basename prog machine_code dependencies
- end
- | "java" ->
- begin
- (Format.eprintf "internal error: sorry, but not yet supported !"; assert false)
- (*let source_file = basename ^ ".java" in
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. opening file %s@,@?" source_file);
- let source_out = open_out source_file in
- let source_fmt = formatter_of_out_channel source_out in
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. java code generation@,@?");
- Java_backend.translate_to_java source_fmt basename normalized_prog machine_code;*)
- end
- | "horn" ->
- begin
- let destname = !Options.dest_dir ^ "/" ^ basename in
- let source_file = destname ^ ".smt2" in (* Could be changed *)
- let source_out = open_out source_file in
- let fmt = formatter_of_out_channel source_out in
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. hornification@,");
- Horn_backend.translate fmt basename prog (Machine_code.arrow_machine::machine_code);
- (* Tracability file if option is activated *)
- if !Options.traces then (
- let traces_file = destname ^ ".traces.xml" in (* Could be changed *)
- let traces_out = open_out traces_file in
- let fmt = formatter_of_out_channel traces_out in
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. tracing info@,");
- Horn_backend_traces.traces_file fmt basename prog machine_code;
- )
- end
- | "lustre" ->
- begin
- let destname = !Options.dest_dir ^ "/" ^ basename in
- let source_file = destname ^ ".lustrec.lus" in (* Could be changed *)
- let source_out = open_out source_file in
- let fmt = formatter_of_out_channel source_out in
- Printers.pp_prog fmt prog;
- Format.fprintf fmt "@.@?";
- (* Lustre_backend.translate fmt basename normalized_prog machine_code *)
- ()
- end
- | "emf" ->
- begin
- let destname = !Options.dest_dir ^ "/" ^ basename in
- let source_file = destname ^ ".emf" in (* Could be changed *)
- let source_out = open_out source_file in
- let fmt = formatter_of_out_channel source_out in
- EMF_backend.translate fmt basename prog machine_code;
- ()
- end
-
- | _ -> assert false
(* compile a .lus source file *)
let rec compile_source dirname basename extension =
@@ -188,7 +94,7 @@ let rec compile_source dirname basename extension =
Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. Phase 2 : Machines generation@,");
let machine_code =
- stage2 prog
+ Compiler_stages.stage2 prog
in
Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ ");
@@ -207,7 +113,7 @@ let rec compile_source dirname basename extension =
let machine_code = Plugins.refine_machine_code prog machine_code in
- stage3 prog machine_code dependencies basename;
+ Compiler_stages.stage3 prog machine_code dependencies basename;
begin
Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.");
(* We stop the process here *)
diff --git a/src/normalization.ml b/src/normalization.ml
index ca24d8c8..42fed931 100644
--- a/src/normalization.ml
+++ b/src/normalization.ml
@@ -90,6 +90,7 @@ let mk_fresh_var node loc ty ck =
var_dec_clock = dummy_clock_dec;
var_dec_const = false;
var_dec_value = None;
+ var_parent_nodeid = Some node.node_id;
var_type = ty;
var_clock = ck;
var_loc = loc
@@ -167,7 +168,10 @@ let mk_expr_alias_opt opt node (defs, vars) expr =
(Clocks.clock_list_of_clock expr.expr_clock) in
let new_def =
mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
- in (new_def::defs, new_aliases@vars), replace_expr new_aliases expr
+ in
+ (* Typing and Registering machine type *)
+ let _ = Machine_types.type_def node new_aliases expr in
+ (new_def::defs, new_aliases@vars), replace_expr new_aliases expr
else
(defs, vars), expr
@@ -420,19 +424,23 @@ let normalize_node node =
) (vars, [], []) node.node_asserts in
let new_locals = List.filter not_is_orig_var vars in (* we filter out inout
vars and initial locals ones *)
- let new_locals = node.node_locals @ new_locals in (* we add again, at the
+
+ let all_locals = node.node_locals @ new_locals in (* we add again, at the
beginning of the list the
local declared ones *)
(*Format.eprintf "New locals: %a@.@?" (fprintf_list ~sep:", " Printers.pp_var) new_locals;*)
+
+ (* Updating annotations: traceability and machine types for fresh variables *)
+
+ (* Compute traceability info:
+ - gather newly bound variables
+ - compute the associated expression without aliases
+ *)
let new_annots =
if !Options.traces then
begin
- (* Compute traceability info:
- - gather newly bound variables
- - compute the associated expression without aliases
- *)
- let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals) ) new_locals in
+ let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals) ) all_locals in
let norm_traceability = {
annots = List.map (fun v ->
let eq =
@@ -446,6 +454,7 @@ let normalize_node node =
in
let expr = substitute_expr diff_vars (defs@assert_defs) eq.eq_rhs in
let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in
+ Annotations.add_expr_ann node.node_id pair.eexpr_tag ["traceability"];
(["traceability"], pair)
) diff_vars;
annot_loc = Location.dummy_loc
@@ -457,9 +466,29 @@ let normalize_node node =
node.node_annot
in
+ let new_annots =
+ List.fold_left (fun annots v ->
+ if Machine_types.is_exportable v then
+ let typ = Machine_types.get_specified_type v in
+ let typ_name = Machine_types.type_name typ in
+
+ let loc = v.var_loc in
+ let typ_as_string =
+ mkexpr
+ loc
+ (Expr_const
+ (Const_string typ_name))
+ in
+ let pair = expr_to_eexpr (expr_of_expr_list loc [expr_of_vdecl v; typ_as_string]) in
+ Annotations.add_expr_ann node.node_id pair.eexpr_tag Machine_types.keyword;
+ {annots = [Machine_types.keyword, pair]; annot_loc = loc}::annots
+ else
+ annots
+ ) new_annots new_locals
+ in
let node =
{ node with
- node_locals = new_locals;
+ node_locals = all_locals;
node_stmts = List.map (fun eq -> Eq eq) (defs @ assert_defs);
node_asserts = asserts;
node_annot = new_annots;
diff --git a/src/optimize_machine.ml b/src/optimize_machine.ml
index 71a668c8..61808b7f 100644
--- a/src/optimize_machine.ml
+++ b/src/optimize_machine.ml
@@ -261,7 +261,7 @@ let machine_unfold fanin elim machine =
let instr_of_const top_const =
let const = const_of_top top_const in
- let vdecl = mkvar_decl Location.dummy_loc (const.const_id, mktyp Location.dummy_loc Tydec_any, mkclock Location.dummy_loc Ckdec_any, true, None) in
+ let vdecl = mkvar_decl Location.dummy_loc (const.const_id, mktyp Location.dummy_loc Tydec_any, mkclock Location.dummy_loc Ckdec_any, true, None, None) in
let vdecl = { vdecl with var_type = const.const_type }
in mkinstr (MLocalAssign (vdecl, mk_val (Cst const.const_value) vdecl.var_type))
diff --git a/src/parserLustreSpec.mly b/src/parserLustreSpec.mly
index 37349acc..e3645401 100644
--- a/src/parserLustreSpec.mly
+++ b/src/parserLustreSpec.mly
@@ -123,9 +123,12 @@ dim_list:
expr:
/* constants */
- INT {mkexpr (Expr_const (Const_int $1))}
+| INT {mkexpr (Expr_const (Const_int $1))}
| REAL {mkexpr (Expr_const (Const_real $1))}
| FLOAT {mkexpr (Expr_const (Const_float $1))}
+| TRUE {mkexpr (Expr_const (Const_bool true))}
+| FALSE {mkexpr (Expr_const (Const_bool false))}
+| STRING {mkexpr (Expr_const (Const_string $1))}
/* Idents or type enum tags */
| IDENT {
if Hashtbl.mem tag_table $1
diff --git a/src/parser_lustre.mly b/src/parser_lustre.mly
index 8038a393..bf5ba82f 100755
--- a/src/parser_lustre.mly
+++ b/src/parser_lustre.mly
@@ -382,6 +382,8 @@ expr:
/* constants */
INT {mkexpr (Expr_const (Const_int $1))}
| REAL {let c,e,s = $1 in mkexpr (Expr_const (Const_real (c,e,s)))}
+| STRING {mkexpr (Expr_const (Const_string $1))}
+
/* | FLOAT {mkexpr (Expr_const (Const_float $1))}*/
/* Idents or type enum tags */
| IDENT { mkexpr (Expr_ident $1) }
@@ -579,11 +581,11 @@ vdecl_list:
vdecl:
ident_list COL typeconst clock
- { List.map (fun (id, loc) -> mkvar_decl (id, mktyp $3, $4, false, None) loc) $1 }
+ { List.map (fun (id, loc) -> mkvar_decl (id, mktyp $3, $4, false, None, None) loc) $1 }
| CONST ident_list /* static parameters don't have clocks */
- { List.map (fun (id, loc) -> mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, true, None) loc) $2 }
+ { List.map (fun (id, loc) -> mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, true, None, None) loc) $2 }
| CONST ident_list COL typeconst /* static parameters don't have clocks */
- { List.map (fun (id, loc) -> mkvar_decl (id, mktyp $4, mkclock Ckdec_any, true, None) loc) $2 }
+ { List.map (fun (id, loc) -> mkvar_decl (id, mktyp $4, mkclock Ckdec_any, true, None, None) loc) $2 }
local_vdecl_list:
local_vdecl {$1}
@@ -591,13 +593,13 @@ local_vdecl_list:
local_vdecl:
/* Useless no ?*/ ident_list
- { List.map (fun (id, loc) -> mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, false, None) loc) $1 }
+ { List.map (fun (id, loc) -> mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, false, None, None) loc) $1 }
| ident_list COL typeconst clock
- { List.map (fun (id, loc) -> mkvar_decl (id, mktyp $3, $4, false, None) loc) $1 }
+ { List.map (fun (id, loc) -> mkvar_decl (id, mktyp $3, $4, false, None, None) loc) $1 }
| CONST vdecl_ident EQ expr /* static parameters don't have clocks */
- { let (id, loc) = $2 in [ mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, true, Some $4) loc] }
+ { let (id, loc) = $2 in [ mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, true, Some $4, None) loc] }
| CONST vdecl_ident COL typeconst EQ expr /* static parameters don't have clocks */
- { let (id, loc) = $2 in [ mkvar_decl (id, mktyp $4, mkclock Ckdec_any, true, Some $6) loc] }
+ { let (id, loc) = $2 in [ mkvar_decl (id, mktyp $4, mkclock Ckdec_any, true, Some $6, None) loc] }
cdecl_list:
cdecl SCOL { (fun itf -> [$1 itf]) }
diff --git a/src/pathConditions.ml b/src/pathConditions.ml
index 49882401..98d4475c 100644
--- a/src/pathConditions.ml
+++ b/src/pathConditions.ml
@@ -100,7 +100,7 @@ let rec compute_neg_expr cpt_pre (expr: LustreSpec.expr) =
let vl, neg = neg_list l in
vl, combine (fun l' -> {expr with expr_desc = Expr_tuple l'}) neg l
- | Expr_ite (i,t,e) when (Types.repr t.expr_type).Types.tdesc = Types.Tbool -> (
+ | Expr_ite (i,t,e) when (Types.is_bool_type t.expr_type) -> (
let list = [i; t; e] in
let vl, neg = neg_list list in
vl, combine (fun l ->
@@ -141,7 +141,7 @@ let rec compute_neg_expr cpt_pre (expr: LustreSpec.expr) =
(fun (v, negv) -> (v, { expr with expr_desc = Expr_appl (op_name, negv, r) } ))
args'
- | Expr_ident _ when (Types.repr expr.expr_type).Types.tdesc = Types.Tbool ->
+ | Expr_ident _ when (Types.is_bool_type expr.expr_type) ->
[], [(expr, cpt_pre), mkpredef_call expr.expr_loc "not" [expr]]
| _ -> [] (* empty vars *) , []
and gen_mcdc_cond_var v expr =
@@ -199,18 +199,18 @@ let rec mcdc_expr cpt_pre expr =
| _ -> []
let mcdc_var_def v expr =
- match (Types.repr expr.expr_type).Types.tdesc with
- | Types.Tbool ->
+ if Types.is_bool_type expr.expr_type then
let vl = gen_mcdc_cond_var v expr in
vl
- | _ -> let vl = mcdc_expr 0 expr in
- vl
-
+ else
+ let vl = mcdc_expr 0 expr in
+ vl
+
let mcdc_node_eq eq =
let vl =
- match eq.eq_lhs, (Types.repr eq.eq_rhs.expr_type).Types.tdesc, eq.eq_rhs.expr_desc with
- | [lhs], Types.Tbool, _ -> gen_mcdc_cond_var lhs eq.eq_rhs
- | _::_, Types.Ttuple tl, Expr_tuple rhs ->
+ match eq.eq_lhs, Types.is_bool_type eq.eq_rhs.expr_type, (Types.repr eq.eq_rhs.expr_type).Types.tdesc, eq.eq_rhs.expr_desc with
+ | [lhs], true, _, _ -> gen_mcdc_cond_var lhs eq.eq_rhs
+ | _::_, false, Types.Ttuple tl, Expr_tuple rhs ->
(* We iterate trough pairs, but accumulate variables aside. The resulting
expression shall remain a tuple defintion *)
let vl = List.fold_right2 (fun lhs rhs accu ->
@@ -248,17 +248,29 @@ let mcdc_top_decl td =
Format.fprintf Format.str_formatter "__cov_%i_%i" i nb_total;
let cov_id = Format.flush_str_formatter () in
let cov_var = mkvar_decl loc
- (cov_id, mktyp loc Tydec_bool, mkclock loc Ckdec_any, false, None) in
+ (cov_id, mktyp loc Tydec_bool, mkclock loc Ckdec_any, false, None, None) in
let cov_def = Eq (mkeq loc ([cov_id], cov_expr)) in
- cov_var, cov_def
+ cov_var, cov_def, cov_expr
) fresh_cov_defs
in
- let fresh_vars, fresh_eqs = List.split fresh_cov_vars in
- let fresh_annots =
+ let fresh_vars, fresh_eqs =
+ List.fold_right
+ (fun (v,eq,_) (accuv, accueq)-> v::accuv, eq::accueq )
+ fresh_cov_vars
+ ([], [])
+ in
+ let fresh_annots = (* We produce two sets of annotations: PROPERTY ones for
+ kind2, and regular ones to keep track of the nature
+ of the annotations. *)
List.map
- (fun v -> {annots = [["PROPERTY"], expr_to_eexpr (expr_of_vdecl v)]; annot_loc = td.top_decl_loc})
- fresh_vars in
- Format.printf "We have %i coverage criteria for node %s@." nb_total nd.node_id;
+ (fun v -> let ee = expr_to_eexpr (expr_of_vdecl v) in
+ {annots = [["PROPERTY"], ee;
+ ["coverage";"mcdc"], ee
+ ];
+ annot_loc = v.var_loc})
+ fresh_vars
+ in
+ Format.printf "%i coverage criteria generated for node %s@ " nb_total nd.node_id;
(* And add them as annotations --%PROPERTY: var TODO *)
{td with top_decl_desc = Node {nd with
node_locals = nd.node_locals@fresh_vars;
@@ -284,6 +296,8 @@ let mcdc prog =
| _ -> assert false);
List.map mcdc_top_decl prog
+
+
(* Local Variables: *)
(* compile-command:"make -C .." *)
(* End: *)
diff --git a/src/printers.ml b/src/printers.ml
index 09164157..da0a5157 100644
--- a/src/printers.ml
+++ b/src/printers.ml
@@ -80,6 +80,12 @@ and pp_const fmt c =
| Const_string s -> pp_print_string fmt ("\"" ^ s ^ "\"")
+let pp_annot_key fmt kwds =
+ match kwds with
+ | [] -> assert false
+ | [x] -> Format.pp_print_string fmt x
+ | _ -> Format.fprintf fmt "/%a/" (fprintf_list ~sep:"/" Format.pp_print_string) kwds
+
let rec pp_expr fmt expr =
(match expr.expr_annot with
| None -> fprintf fmt "%t"
@@ -164,8 +170,8 @@ and pp_s_function fmt expr_ann =
and pp_expr_annot fmt expr_ann =
let pp_annot fmt (kwds, ee) =
- Format.fprintf fmt "(*! %t: %a; *)"
- (fun fmt -> match kwds with | [] -> assert false | [x] -> Format.pp_print_string fmt x | _ -> Format.fprintf fmt "/%a/" (fprintf_list ~sep:"/" Format.pp_print_string) kwds)
+ Format.fprintf fmt "(*! %a: %a; *)"
+ pp_annot_key kwds
pp_eexpr ee
in
fprintf_list ~sep:"@ " pp_annot fmt expr_ann.annots
diff --git a/src/type_predef.ml b/src/type_predef.ml
index e9c1cfb2..48fd3f06 100755
--- a/src/type_predef.ml
+++ b/src/type_predef.ml
@@ -12,63 +12,83 @@
(********************************************************************)
(** Base types and predefined operator types. *)
-open Types
-let type_int = new_ty Tint
-let type_real = new_ty Treal
-let type_bool = new_ty Tbool
-let type_clock ty = new_ty (Tclock ty)
-let type_const tname = new_ty (Tconst tname)
-let type_enum taglist = new_ty (Tenum taglist)
-let type_struct fieldlist = new_ty (Tstruct fieldlist)
-let type_tuple tl = new_ty (Ttuple tl)
-let type_arrow ty1 ty2 = new_ty (Tarrow (ty1, ty2))
-let type_array d ty = new_ty (Tarray (d, ty))
-let type_static d ty = new_ty (Tstatic (d, ty))
+
+module Make (T: Types.S) =
+struct
+ (* module T = Types.Make (BT) *)
+ module BT = T.BasicT
+ include T
+
+ let type_int = new_ty type_int
+ let type_real = new_ty type_real
+ let type_bool = new_ty type_bool
+ let type_string = new_ty type_string
+ let type_clock ty = new_ty (Tclock ty)
+ let type_const tname = new_ty (Tconst tname)
+ let type_enum taglist = new_ty (Tenum taglist)
+ let type_struct fieldlist = new_ty (Tstruct fieldlist)
+ let type_tuple tl = new_ty (Ttuple tl)
+ let type_arrow ty1 ty2 = new_ty (Tarrow (ty1, ty2))
+ let type_array d ty = new_ty (Tarray (d, ty))
+ let type_static d ty = new_ty (Tstatic (d, ty))
+
+ let type_unary_bool_op =
+ new_ty (Tarrow (type_bool, type_bool))
-let type_unary_bool_op =
- new_ty (Tarrow (type_bool, type_bool))
+ let type_unary_poly_op =
+ let univ = new_univar () in
+ type_arrow univ univ
-let type_unary_poly_op =
- let univ = new_univar () in
- type_arrow univ univ
+ let type_bin_int_op =
+ type_arrow (type_tuple [type_int;type_int]) type_int
-let type_bin_int_op =
- type_arrow (type_tuple [type_int;type_int]) type_int
+ let type_bin_bool_op =
+ type_arrow (type_tuple [type_bool;type_bool]) type_bool
-let type_bin_bool_op =
- type_arrow (type_tuple [type_bool;type_bool]) type_bool
+ let type_ite_op =
+ let univ = new_univar () in
+ type_arrow (type_tuple [type_bool;univ;univ]) univ
-let type_ite_op =
- let univ = new_univar () in
- type_arrow (type_tuple [type_bool;univ;univ]) univ
+ let type_bin_poly_op =
+ let univ = new_univar () in
+ type_arrow (type_tuple [univ;univ]) univ
-let type_bin_poly_op =
- let univ = new_univar () in
- type_arrow (type_tuple [univ;univ]) univ
+ let type_bin_comp_op =
+ let univ = new_univar () in
+ new_ty (Tarrow (new_ty (Ttuple [univ;univ]), type_bool))
-let type_bin_comp_op =
- let univ = new_univar () in
- new_ty (Tarrow (new_ty (Ttuple [univ;univ]), type_bool))
+ let type_univ_bool_univ =
+ let univ = new_univar () in
+ type_arrow (type_tuple [univ;type_bool]) univ
-let type_univ_bool_univ =
- let univ = new_univar () in
- type_arrow (type_tuple [univ;type_bool]) univ
+ let type_bool_univ3 =
+ let univ = new_univar () in
+ type_arrow (type_tuple [type_bool;univ;univ]) univ
-let type_bool_univ3 =
- let univ = new_univar () in
- type_arrow (type_tuple [type_bool;univ;univ]) univ
+ let type_access =
+ let d = Dimension.mkdim Location.dummy_loc Dimension.Dunivar in
+ let d' = Dimension.mkdim Location.dummy_loc Dimension.Dunivar in
+ let univ = new_univar () in
+ type_arrow (type_tuple [type_array d univ; type_static d' type_int]) univ
-let type_access =
- let d = Dimension.mkdim Location.dummy_loc Dimension.Dunivar in
- let d' = Dimension.mkdim Location.dummy_loc Dimension.Dunivar in
- let univ = new_univar () in
- type_arrow (type_tuple [type_array d univ; type_static d' type_int]) univ
+ let type_power =
+ let d = Dimension.mkdim Location.dummy_loc Dimension.Dunivar in
+ let univ = new_univar () in
+ type_arrow (type_tuple [univ; type_static d type_int]) (type_array d univ)
+end
-let type_power =
- let d = Dimension.mkdim Location.dummy_loc Dimension.Dunivar in
- let univ = new_univar () in
- type_arrow (type_tuple [univ; type_static d type_int]) (type_array d univ)
+
+(* module BaseBuilder = *)
+(* struct *)
+(* let type_int_builder = Tbasic Basic.Tint *)
+(* let type_real_builder = Tbasic Basic.Treal *)
+(* let type_bool_builder = Tbasic Basic.Tbool *)
+(* let type_string_builder = Tbasic Basic.Tstring *)
+(* end *)
+
+module Main = Make (Types.Main)
+include Main
(* Local Variables: *)
(* compile-command:"make -C .." *)
diff --git a/src/types.ml b/src/types.ml
index b7f0374a..ffec4b02 100755
--- a/src/types.ml
+++ b/src/types.ml
@@ -15,70 +15,164 @@
open Utils
open Dimension
-type type_expr =
+module type BASIC_TYPES =
+sig
+ type t
+ val pp: Format.formatter -> t -> unit
+ val pp_c: Format.formatter -> t -> unit
+ val is_scalar_type: t -> bool
+ val is_numeric_type: t -> bool
+ val is_int_type: t -> bool
+ val is_real_type: t -> bool
+ val is_bool_type: t -> bool
+ val is_dimension_type: t -> bool
+ val type_int_builder: t
+ val type_real_builder: t
+ val type_bool_builder: t
+ val type_string_builder: t
+ val unify: t -> t -> unit
+ val is_unifiable: t -> t -> bool
+end
+
+module Basic =
+struct
+ type t =
+ | Tstring
+ | Tint
+ | Treal
+ | Tbool
+ | Trat (* Actually unused for now. Only place where it can appear is
+ in a clock declaration *)
+
+ let type_string_builder = Tstring
+ let type_int_builder = Tint
+ let type_real_builder = Treal
+ let type_bool_builder = Tbool
+
+ open Format
+ let pp fmt t =
+ match t with
+ | Tint ->
+ fprintf fmt "int"
+ | Treal ->
+ fprintf fmt "real"
+ | Tstring ->
+ fprintf fmt "string"
+ | Tbool ->
+ fprintf fmt "bool"
+ | Trat ->
+ fprintf fmt "rat"
+
+ let pp_c = pp
+
+ let is_scalar_type t =
+ match t with
+ | Tbool
+ | Tint
+ | Treal -> true
+ | _ -> false
+
+
+ let is_numeric_type t =
+ match t with
+ | Tint
+ | Treal -> true
+ | _ -> false
+
+ let is_int_type t = t = Tint
+ let is_real_type t = t = Treal
+ let is_bool_type t = t = Tbool
+
+ let is_dimension_type t =
+ match t with
+ | Tint
+ | Tbool -> true
+ | _ -> false
+
+ let is_unifiable b1 b2 = b1 == b2
+ let unify _ _ = ()
+end
+
+
+
+module Make(BasicT : BASIC_TYPES) =
+struct
+
+ module BasicT = BasicT
+ type basic_type = BasicT.t
+ type type_expr =
{mutable tdesc: type_desc;
tid: int}
-
-and type_desc =
- | Tconst of ident (* type constant *)
- | Tint
- | Treal
- | Tbool
- | Trat (* Actually unused for now. Only place where it can appear is
- in a clock declaration *)
- | Tclock of type_expr (* A type expression explicitely tagged as carrying a clock *)
- | Tarrow of type_expr * type_expr
- | Ttuple of type_expr list
- | Tenum of ident list
- | Tstruct of (ident * type_expr) list
- | Tarray of dim_expr * type_expr
- | Tstatic of dim_expr * type_expr (* a type carried by a dimension expression *)
- | Tlink of type_expr (* During unification, make links instead of substitutions *)
- | Tvar (* Monomorphic type variable *)
- | Tunivar (* Polymorphic type variable *)
-
-type error =
- Unbound_value of ident
- | Already_bound of ident
- | Already_defined of ident
- | Undefined_var of ISet.t
- | Declared_but_undefined of ident
- | Unbound_type of ident
- | Not_a_dimension
- | Not_a_constant
- | Assigned_constant of ident
- | WrongArity of int * int
- | WrongMorphism of int * int
- | Type_mismatch of ident
- | Type_clash of type_expr * type_expr
- | Poly_imported_node of ident
+ and type_desc =
+ | Tconst of ident (* type constant *)
+ | Tbasic of basic_type
+ | Tclock of type_expr (* A type expression explicitely tagged as carrying a clock *)
+ | Tarrow of type_expr * type_expr
+ | Ttuple of type_expr list
+ | Tenum of ident list
+ | Tstruct of (ident * type_expr) list
+ | Tarray of dim_expr * type_expr
+ | Tstatic of dim_expr * type_expr (* a type carried by a dimension expression *)
+ | Tlink of type_expr (* During unification, make links instead of substitutions *)
+ | Tvar (* Monomorphic type variable *)
+ | Tunivar (* Polymorphic type variable *)
+
+ (* {mutable tdesc: type_desc; *)
+ (* tid: int} *)
+
+ (* and type_desc = *)
+ (* | Tconst of ident (\* type constant *\) *)
+ (* | Tbasic of BasicT.t *)
+ (* | Tclock of type_expr (\* A type expression explicitely tagged as carrying a clock *\) *)
+ (* | Tarrow of type_expr * type_expr *)
+ (* | Ttuple of type_expr list *)
+ (* | Tenum of ident list *)
+ (* | Tstruct of (ident * type_expr) list *)
+ (* | Tarray of dim_expr * type_expr *)
+ (* | Tstatic of dim_expr * type_expr (\* a type carried by a dimension expression *\) *)
+ (* | Tlink of type_expr (\* During unification, make links instead of substitutions *\) *)
+ (* | Tvar (\* Monomorphic type variable *\) *)
+ (* | Tunivar (\* Polymorphic type variable *\) *)
+
+ type error =
+ Unbound_value of ident
+ | Already_bound of ident
+ | Already_defined of ident
+ | Undefined_var of ISet.t
+ | Declared_but_undefined of ident
+ | Unbound_type of ident
+ | Not_a_dimension
+ | Not_a_constant
+ | Assigned_constant of ident
+ | WrongArity of int * int
+ | WrongMorphism of int * int
+ | Type_mismatch of ident
+ | Type_clash of type_expr * type_expr
+ | Poly_imported_node of ident
exception Unify of type_expr * type_expr
exception Error of Location.t * error
+let mk_basic t = Tbasic t
+
+
(* Pretty-print*)
open Format
-let rec print_struct_ty_field fmt (label, ty) =
- fprintf fmt "%a : %a" pp_print_string label print_ty ty
-and print_ty fmt ty =
+let rec print_struct_ty_field pp_basic fmt (label, ty) =
+ fprintf fmt "%a : %a" pp_print_string label (print_ty_param pp_basic) ty
+and print_ty_param pp_basic fmt ty =
+ let print_ty = print_ty_param pp_basic in
match ty.tdesc with
| Tvar ->
fprintf fmt "_%s" (name_of_type ty.tid)
- | Tint ->
- fprintf fmt "int"
- | Treal ->
- fprintf fmt "real"
- | Tbool ->
- fprintf fmt "bool"
+ | Tbasic t -> pp_basic fmt t
| Tclock t ->
fprintf fmt "%a clock" print_ty t
| Tstatic (d, t) ->
fprintf fmt "(%a:%a)" Dimension.pp_dimension d print_ty t
| Tconst t ->
fprintf fmt "%s" t
- | Trat ->
- fprintf fmt "rat"
| Tarrow (ty1,ty2) ->
fprintf fmt "%a -> %a" print_ty ty1 print_ty ty2
| Ttuple tylist ->
@@ -89,7 +183,7 @@ and print_ty fmt ty =
(Utils.fprintf_list ~sep:", " pp_print_string) taglist
| Tstruct fieldlist ->
fprintf fmt "struct {%a }"
- (Utils.fprintf_list ~sep:"; " print_struct_ty_field) fieldlist
+ (Utils.fprintf_list ~sep:"; " (print_struct_ty_field pp_basic)) fieldlist
| Tarray (e, ty) ->
fprintf fmt "%a^%a" print_ty ty Dimension.pp_dimension e
| Tlink ty ->
@@ -97,28 +191,24 @@ and print_ty fmt ty =
| Tunivar ->
fprintf fmt "'%s" (name_of_type ty.tid)
+let print_ty = print_ty_param BasicT.pp
+
+
let rec print_node_struct_ty_field fmt (label, ty) =
fprintf fmt "%a : %a" pp_print_string label print_node_ty ty
and print_node_ty fmt ty =
match ty.tdesc with
| Tvar -> begin
-(*Format.eprintf "DEBUG:Types.print_node@.";*)
+ (*Format.eprintf "DEBUG:Types.print_node@.";*)
fprintf fmt "_%s" (name_of_type ty.tid)
-end
- | Tint ->
- fprintf fmt "int"
- | Treal ->
- fprintf fmt "real"
- | Tbool ->
- fprintf fmt "bool"
+ end
+ | Tbasic t -> BasicT.pp fmt t
| Tclock t ->
fprintf fmt "%a clock" print_node_ty t
| Tstatic (_, t) ->
fprintf fmt "%a" print_node_ty t
| Tconst t ->
fprintf fmt "%s" t
- | Trat ->
- fprintf fmt "rat"
| Tarrow (ty1,ty2) ->
fprintf fmt "%a -> %a" print_node_ty ty1 print_node_ty ty2
| Ttuple tylist ->
@@ -201,31 +291,39 @@ let get_field_type ty label =
| Tstruct fl -> (try Some (List.assoc label fl) with Not_found -> None)
| _ -> None
+let rec is_static_type ty =
+ match (repr ty).tdesc with
+ | Tstatic (_, ty) -> true
+ | _ -> false
+
let rec is_scalar_type ty =
match (repr ty).tdesc with
| Tstatic (_, ty) -> is_scalar_type ty
- | Tbool
- | Tint
- | Treal -> true
+ | Tbasic t -> BasicT.is_scalar_type t
| _ -> false
let rec is_numeric_type ty =
match (repr ty).tdesc with
| Tstatic (_, ty) -> is_numeric_type ty
- | Tint
- | Treal -> true
+ | Tbasic t -> BasicT.is_numeric_type t
| _ -> false
-
+
let rec is_real_type ty =
match (repr ty).tdesc with
| Tstatic (_, ty) -> is_real_type ty
- | Treal -> true
+ | Tbasic t -> BasicT.is_real_type t
+ | _ -> false
+
+let rec is_int_type ty =
+ match (repr ty).tdesc with
+ | Tstatic (_, ty) -> is_int_type ty
+ | Tbasic t -> BasicT.is_int_type t
| _ -> false
let rec is_bool_type ty =
match (repr ty).tdesc with
| Tstatic (_, ty) -> is_bool_type ty
- | Tbool -> true
+ | Tbasic t -> BasicT.is_bool_type t
| _ -> false
let get_clock_base_type ty =
@@ -241,8 +339,7 @@ let unclock_type ty =
let rec is_dimension_type ty =
match (repr ty).tdesc with
- | Tint
- | Tbool -> true
+ | Tbasic t -> BasicT.is_dimension_type t
| Tclock ty'
| Tstatic (_, ty') -> is_dimension_type ty'
| _ -> false
@@ -341,7 +438,7 @@ let rec type_list_of_type ty =
(** [is_polymorphic ty] returns true if [ty] is polymorphic. *)
let rec is_polymorphic ty =
match ty.tdesc with
- | Tenum _ | Tvar | Tint | Treal | Tbool | Trat | Tconst _ -> false
+ | Tenum _ | Tvar | Tbasic _ | Tconst _ -> false
| Tclock ty -> is_polymorphic ty
| Tarrow (ty1,ty2) -> (is_polymorphic ty1) || (is_polymorphic ty2)
| Ttuple tl -> List.exists (fun t -> is_polymorphic t) tl
@@ -355,7 +452,100 @@ let rec is_polymorphic ty =
let mktyptuple nb typ =
let array = Array.make nb typ in
Ttuple (Array.to_list array)
+
+let type_desc t = t.tdesc
+
+
+
+let type_int = mk_basic BasicT.type_int_builder
+let type_real = mk_basic BasicT.type_real_builder
+let type_bool = mk_basic BasicT.type_bool_builder
+let type_string = mk_basic BasicT.type_string_builder
+end
+
+
+module type S =
+sig
+ module BasicT: BASIC_TYPES
+ type basic_type = BasicT.t
+ type type_expr =
+ {mutable tdesc: type_desc;
+ tid: int}
+ and type_desc =
+ | Tconst of ident (* type constant *)
+ | Tbasic of basic_type
+ | Tclock of type_expr (* A type expression explicitely tagged as carrying a clock *)
+ | Tarrow of type_expr * type_expr
+ | Ttuple of type_expr list
+ | Tenum of ident list
+ | Tstruct of (ident * type_expr) list
+ | Tarray of dim_expr * type_expr
+ | Tstatic of dim_expr * type_expr (* a type carried by a dimension expression *)
+ | Tlink of type_expr (* During unification, make links instead of substitutions *)
+ | Tvar (* Monomorphic type variable *)
+ | Tunivar (* Polymorphic type variable *)
+
+ type error =
+ Unbound_value of ident
+ | Already_bound of ident
+ | Already_defined of ident
+ | Undefined_var of ISet.t
+ | Declared_but_undefined of ident
+ | Unbound_type of ident
+ | Not_a_dimension
+ | Not_a_constant
+ | Assigned_constant of ident
+ | WrongArity of int * int
+ | WrongMorphism of int * int
+ | Type_mismatch of ident
+ | Type_clash of type_expr * type_expr
+ | Poly_imported_node of ident
+
+ exception Unify of type_expr * type_expr
+ exception Error of Location.t * error
+
+ val is_real_type: type_expr -> bool
+ val is_int_type: type_expr -> bool
+ val is_bool_type: type_expr -> bool
+ val is_static_type: type_expr -> bool
+ val is_array_type: type_expr -> bool
+ val is_dimension_type: type_expr -> bool
+ val is_address_type: type_expr -> bool
+ val is_generic_type: type_expr -> bool
+ val print_ty: Format.formatter -> type_expr -> unit
+ val repr: type_expr -> type_expr
+ val dynamic_type: type_expr -> type_expr
+ val type_desc: type_expr -> type_desc
+ val new_var: unit -> type_expr
+ val new_univar: unit -> type_expr
+ val new_ty: type_desc -> type_expr
+ val type_int: type_desc
+ val type_real: type_desc
+ val type_bool: type_desc
+ val type_string: type_desc
+ val array_element_type: type_expr -> type_expr
+ val type_list_of_type: type_expr -> type_expr list
+ val print_node_ty: Format.formatter -> type_expr -> unit
+ val get_clock_base_type: type_expr -> type_expr option
+ val get_static_value: type_expr -> Dimension.dim_expr option
+ val is_tuple_type: type_expr -> bool
+ val type_of_type_list: type_expr list -> type_expr
+ val split_arrow: type_expr -> type_expr * type_expr
+ val unclock_type: type_expr -> type_expr
+ val bottom: type_expr
+ val map_tuple_type: (type_expr -> type_expr) -> type_expr -> type_expr
+ val array_base_type: type_expr -> type_expr
+ val array_type_dimension: type_expr -> Dimension.dim_expr
+ val pp_error: Format.formatter -> error -> unit
+ val struct_field_type: type_expr -> ident -> type_expr
+ val array_type_multi_dimension: type_expr -> Dimension.dim_expr list
+end (* with type type_expr = BasicT.t type_expr_gen *)
+
+module type Sbasic = S with type BasicT.t = Basic.t
+
+module Main : Sbasic = Make (Basic)
+include Main
(* Local Variables: *)
diff --git a/src/typing.ml b/src/typing.ml
index 0aed94cb..471643c2 100755
--- a/src/typing.ml
+++ b/src/typing.ml
@@ -24,9 +24,31 @@ open Utils
overwritten, yet this makes notations far lighter.*)
open LustreSpec
open Corelang
-open Types
+(* open Types *)
open Format
+
+module type EXPR_TYPE_HUB =
+sig
+ type type_expr
+ val import: Types.Main.type_expr -> type_expr
+ val export: type_expr -> Types.Main.type_expr
+end
+
+module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.type_expr) =
+struct
+
+ module TP = Type_predef.Make (T)
+ include TP
+
+let basic_coretype_type t =
+ if is_real_type t then Tydec_real else
+ if is_int_type t then Tydec_int else
+ if is_bool_type t then Tydec_bool else
+ assert false
+
+
+
let pp_typing_env fmt env =
Env.pp_env print_ty fmt env
@@ -34,7 +56,7 @@ let pp_typing_env fmt env =
type [ty]. False otherwise. *)
let rec occurs tvar ty =
let ty = repr ty in
- match ty.tdesc with
+ match type_desc ty with
| Tvar -> ty=tvar
| Tarrow (t1, t2) ->
(occurs tvar t1) || (occurs tvar t2)
@@ -46,12 +68,12 @@ let rec occurs tvar ty =
| Tstatic (_, t)
| Tclock t
| Tlink t -> occurs tvar t
- | Tenum _ | Tconst _ | Tunivar | Tint | Treal | Tbool | Trat -> false
+ | Tenum _ | Tconst _ | Tunivar | Tbasic _ -> false
(** Promote monomorphic type variables to polymorphic type variables. *)
(* Generalize by side-effects *)
let rec generalize ty =
- match ty.tdesc with
+ match type_desc ty with
| Tvar ->
(* No scopes, always generalize *)
ty.tdesc <- Tunivar
@@ -66,13 +88,13 @@ let rec generalize ty =
| Tclock t
| Tlink t ->
generalize t
- | Tenum _ | Tconst _ | Tunivar | Tint | Treal | Tbool | Trat -> ()
+ | Tenum _ | Tconst _ | Tunivar | Tbasic _ -> ()
(** Downgrade polymorphic type variables to monomorphic type variables *)
let rec instantiate inst_vars inst_dim_vars ty =
let ty = repr ty in
match ty.tdesc with
- | Tenum _ | Tconst _ | Tvar | Tint | Treal | Tbool | Trat -> ty
+ | Tenum _ | Tconst _ | Tvar | Tbasic _ -> ty
| Tarrow (t1,t2) ->
{ty with tdesc =
Tarrow ((instantiate inst_vars inst_dim_vars t1), (instantiate inst_vars inst_dim_vars t2))}
@@ -101,28 +123,26 @@ let rec instantiate inst_vars inst_dim_vars ty =
let rec type_coretype type_dim cty =
match (*get_repr_type*) cty with
| Tydec_any -> new_var ()
- | Tydec_int -> Type_predef.type_int
- | Tydec_real -> Type_predef.type_real
+ | Tydec_int -> type_int
+ | Tydec_real -> (* Type_predef. *)type_real
(* | Tydec_float -> Type_predef.type_real *)
- | Tydec_bool -> Type_predef.type_bool
- | Tydec_clock ty -> Type_predef.type_clock (type_coretype type_dim ty)
- | Tydec_const c -> Type_predef.type_const c
- | Tydec_enum tl -> Type_predef.type_enum tl
- | Tydec_struct fl -> Type_predef.type_struct (List.map (fun (f, ty) -> (f, type_coretype type_dim ty)) fl)
+ | Tydec_bool -> (* Type_predef. *)type_bool
+ | Tydec_clock ty -> (* Type_predef. *)type_clock (type_coretype type_dim ty)
+ | Tydec_const c -> (* Type_predef. *)type_const c
+ | Tydec_enum tl -> (* Type_predef. *)type_enum tl
+ | Tydec_struct fl -> (* Type_predef. *)type_struct (List.map (fun (f, ty) -> (f, type_coretype type_dim ty)) fl)
| Tydec_array (d, ty) ->
begin
let d = Dimension.copy (ref []) d in
type_dim d;
- Type_predef.type_array d (type_coretype type_dim ty)
+ (* Type_predef. *)type_array d (type_coretype type_dim ty)
end
(* [coretype_type] is the reciprocal of [type_typecore] *)
let rec coretype_type ty =
match (repr ty).tdesc with
| Tvar -> Tydec_any
- | Tint -> Tydec_int
- | Treal -> Tydec_real
- | Tbool -> Tydec_bool
+ | Tbasic _ -> basic_coretype_type ty
| Tconst c -> Tydec_const c
| Tclock t -> Tydec_clock (coretype_type t)
| Tenum tl -> Tydec_enum tl
@@ -149,7 +169,7 @@ let rec eq_ground t1 t2 =
let t2 = repr t2 in
t1==t2 ||
match t1.tdesc, t2.tdesc with
- | Tint, Tint | Tbool, Tbool | Trat, Trat | Treal, Treal -> true
+ | Tbasic t1, Tbasic t2 when t1 == t2 -> true
| Tenum tl, Tenum tl' when tl == tl' -> true
| Ttuple tl, Ttuple tl' when List.length tl = List.length tl' -> List.for_all2 eq_ground tl tl'
| Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' -> List.for_all2 (fun (_, t) (_, t') -> eq_ground t t') fl fl'
@@ -211,7 +231,7 @@ let unify ?(sub=false) ?(semi=false) t1 t2 =
| Tclock _, Tstatic _
| Tstatic _, Tclock _ -> raise (Unify (t1, t2))
| Tclock t1', Tclock t2' -> unif t1' t2'
- | Tint, Tint | Tbool, Tbool | Trat, Trat | Treal, Treal
+ | Tbasic t1, Tbasic t2 when t1 == t2 -> ()
| Tunivar, _ | _, Tunivar -> ()
| (Tconst t, _) ->
let def_t = get_type_definition t in
@@ -232,6 +252,10 @@ let unify ?(sub=false) ?(semi=false) t1 t2 =
Dimension.eval Basic_library.eval_env eval_const e2;
Dimension.unify ~semi:semi e1 e2;
end
+ (* Special cases for machine_types. Rules to unify static types infered
+ for numerical constants with non static ones for variables with
+ possible machine types *)
+ | Tbasic bt1, Tbasic bt2 when BasicT.is_unifiable bt1 bt2 -> BasicT.unify bt1 bt2
| _,_ -> raise (Unify (t1, t2))
in unif t1 t2
@@ -245,27 +269,27 @@ let try_unify ?(sub=false) ?(semi=false) ty1 ty2 loc =
| Dimension.Unify _ ->
raise (Error (loc, Type_clash (ty1,ty2)))
-let rec type_struct_const_field loc (label, c) =
+let rec type_struct_const_field ?(is_annot=false) loc (label, c) =
if Hashtbl.mem field_table label
then let tydef = Hashtbl.find field_table label in
let tydec = (typedef_of_top tydef).tydef_desc in
let tydec_struct = get_struct_type_fields tydec in
let ty_label = type_coretype (fun d -> ()) (List.assoc label tydec_struct) in
begin
- try_unify ty_label (type_const loc c) loc;
+ try_unify ty_label (type_const ~is_annot loc c) loc;
type_coretype (fun d -> ()) tydec
end
else raise (Error (loc, Unbound_value ("struct field " ^ label)))
-and type_const loc c =
+and type_const ?(is_annot=false) loc c =
match c with
- | Const_int _ -> Type_predef.type_int
- | Const_real _ -> Type_predef.type_real
+ | Const_int _ -> (* Type_predef. *)type_int
+ | Const_real _ -> (* Type_predef. *)type_real
(* | Const_float _ -> Type_predef.type_real *)
| Const_array ca -> let d = Dimension.mkdim_int loc (List.length ca) in
let ty = new_var () in
- List.iter (fun e -> try_unify ty (type_const loc e) loc) ca;
- Type_predef.type_array d ty
+ List.iter (fun e -> try_unify ty (type_const ~is_annot loc e) loc) ca;
+ (* Type_predef. *)type_array d ty
| Const_tag t ->
if Hashtbl.mem tag_table t
then
@@ -284,7 +308,7 @@ and type_const loc c =
(fun acc (l, c) ->
if List.mem l acc
then raise (Error (loc, Already_bound ("struct field " ^ l)))
- else try_unify ty_struct (type_struct_const_field loc (l, c)) loc; l::acc)
+ else try_unify ty_struct (type_struct_const_field ~is_annot loc (l, c)) loc; l::acc)
[] fl in
try
let total = List.map fst (get_struct_type_fields (coretype_type ty_struct)) in
@@ -295,7 +319,7 @@ and type_const loc c =
with Not_found ->
ty_struct
end
- | Const_string _ -> assert false (* string should only appear in annotations *)
+ | Const_string _ -> if is_annot then (* Type_predef. *)type_string else assert false (* string should only appear in annotations *)
(* The following typing functions take as parameter an environment [env]
and whether the element being typed is expected to be constant [const].
@@ -318,10 +342,10 @@ let rec type_add_const env const arg targ =
if is_dimension_type targ
then dimension_of_expr arg
else Dimension.mkdim_var () in
- let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in
+ let eval_const id = (* Types. *)get_static_value (Env.lookup_value (fst env) id) in
Dimension.eval Basic_library.eval_env eval_const d;
- let real_static_type = Type_predef.type_static d (Types.dynamic_type targ) in
- (match Types.get_static_value targ with
+ let real_static_type = (* Type_predef. *)type_static d ((* Types. *)dynamic_type targ) in
+ (match (* Types. *)get_static_value targ with
| None -> ()
| Some d' -> try_unify targ real_static_type arg.expr_loc);
real_static_type
@@ -331,7 +355,7 @@ let rec type_add_const env const arg targ =
used during node applications and assignments *)
and type_subtyping_arg env in_main ?(sub=true) const real_arg formal_type =
let loc = real_arg.expr_loc in
- let const = const || (Types.get_static_value formal_type <> None) in
+ let const = const || ((* Types. *)get_static_value formal_type <> None) in
let real_type = type_add_const env const real_arg (type_expr env in_main const real_arg) in
(*Format.eprintf "subtyping const %B real %a:%a vs formal %a@." const Printers.pp_expr real_arg Types.print_ty real_type Types.print_ty formal_type;*)
try_unify ~sub:sub formal_type real_type loc
@@ -348,26 +372,38 @@ and type_appl env in_main loc const f args =
then
try
let targs = Utils.transpose_list (List.map type_list_of_type targs) in
- Types.type_of_type_list (List.map (type_simple_call env in_main loc const f) targs)
- with
+ (* Types. *)type_of_type_list (List.map (type_simple_call env in_main loc const f) targs)
+ with
Utils.TransposeError (l, l') -> raise (Error (loc, WrongMorphism (l, l')))
- else
+
+ else (
type_dependent_call env in_main loc const f (List.combine args targs)
+ )
(* type a call with possible dependent types. [targs] is here a list of (argument, type) pairs. *)
and type_dependent_call env in_main loc const f targs =
-(*Format.eprintf "Typing.type_dependent_call %s@." f;*)
+(* Format.eprintf "Typing.type_dependent_call %s@." f; *)
let tins, touts = new_var (), new_var () in
- let tfun = Type_predef.type_arrow tins touts in
+ (* Format.eprintf "tin=%a, tout=%a@." print_ty tins print_ty touts; *)
+ let tfun = (* Type_predef. *)type_arrow tins touts in
+ (* Format.eprintf "fun=%a@." print_ty tfun; *)
type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;
+ (* Format.eprintf "type subtyping@."; *)
let tins = type_list_of_type tins in
if List.length targs <> List.length tins then
raise (Error (loc, WrongArity (List.length tins, List.length targs)))
else
begin
- List.iter2 (fun (a,t) ti ->
- let t' = type_add_const env (const || Types.get_static_value ti <> None) a t
- in try_unify ~sub:true ti t' a.expr_loc) targs tins;
+ List.iter2 (
+ fun (a,t) ti ->
+ let t' = type_add_const env (const || (* Types. *)get_static_value ti <> None) a t in
+ (* Format.eprintf "uniying ti=%a t'=%a touts=%a@." print_ty ti print_ty t' print_ty touts; *)
+ try_unify ~sub:true ti t' a.expr_loc;
+ (* Format.eprintf "unified ti=%a t'=%a touts=%a@." print_ty ti print_ty t' print_ty touts; *)
+
+ )
+ targs
+ tins;
touts
end
@@ -376,7 +412,7 @@ and type_dependent_call env in_main loc const f targs =
[targs] is here a list of arguments' types. *)
and type_simple_call env in_main loc const f targs =
let tins, touts = new_var (), new_var () in
- let tfun = Type_predef.type_arrow tins touts in
+ let tfun = (* Type_predef. *)type_arrow tins touts in
type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;
(*Format.eprintf "try unify %a %a@." Types.print_ty tins Types.print_ty (type_of_type_list targs);*)
try_unify ~sub:true tins (type_of_type_list targs) loc;
@@ -384,60 +420,60 @@ and type_simple_call env in_main loc const f targs =
(** [type_expr env in_main expr] types expression [expr] in environment
[env], expecting it to be [const] or not. *)
-and type_expr env in_main const expr =
+and type_expr ?(is_annot=false) env in_main const expr =
let resulting_ty =
match expr.expr_desc with
| Expr_const c ->
- let ty = type_const expr.expr_loc c in
- let ty = Type_predef.type_static (Dimension.mkdim_var ()) ty in
- expr.expr_type <- ty;
+ let ty = type_const ~is_annot expr.expr_loc c in
+ let ty = (* Type_predef. *)type_static (Dimension.mkdim_var ()) ty in
+ expr.expr_type <- Expr_type_hub.export ty;
ty
| Expr_ident v ->
let tyv =
try
Env.lookup_value (fst env) v
with Not_found ->
- Format.eprintf "Failure in typing expr %a@." Printers.pp_expr expr;
+ Format.eprintf "Failure in typing expr %a. Not in typing environement@." Printers.pp_expr expr;
raise (Error (expr.expr_loc, Unbound_value ("identifier " ^ v)))
in
let ty = instantiate (ref []) (ref []) tyv in
let ty' =
if const
- then Type_predef.type_static (Dimension.mkdim_var ()) (new_var ())
+ then (* Type_predef. *)type_static (Dimension.mkdim_var ()) (new_var ())
else new_var () in
try_unify ty ty' expr.expr_loc;
- expr.expr_type <- ty;
+ expr.expr_type <- Expr_type_hub.export ty;
ty
| Expr_array elist ->
let ty_elt = new_var () in
List.iter (fun e -> try_unify ty_elt (type_appl env in_main expr.expr_loc const "uminus" [e]) e.expr_loc) elist;
let d = Dimension.mkdim_int expr.expr_loc (List.length elist) in
- let ty = Type_predef.type_array d ty_elt in
- expr.expr_type <- ty;
+ let ty = (* Type_predef. *)type_array d ty_elt in
+ expr.expr_type <- Expr_type_hub.export ty;
ty
| Expr_access (e1, d) ->
- type_subtyping_arg env in_main false (* not necessary a constant *) (expr_of_dimension d) Type_predef.type_int;
+ type_subtyping_arg env in_main false (* not necessary a constant *) (expr_of_dimension d) (* Type_predef. *)type_int;
let ty_elt = new_var () in
let d = Dimension.mkdim_var () in
- type_subtyping_arg env in_main const e1 (Type_predef.type_array d ty_elt);
- expr.expr_type <- ty_elt;
+ type_subtyping_arg env in_main const e1 ((* Type_predef. *)type_array d ty_elt);
+ expr.expr_type <- Expr_type_hub.export ty_elt;
ty_elt
| Expr_power (e1, d) ->
- let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in
- type_subtyping_arg env in_main true (expr_of_dimension d) Type_predef.type_int;
+ let eval_const id = (* Types. *)get_static_value (Env.lookup_value (fst env) id) in
+ type_subtyping_arg env in_main true (expr_of_dimension d) (* Type_predef. *)type_int;
Dimension.eval Basic_library.eval_env eval_const d;
let ty_elt = type_appl env in_main expr.expr_loc const "uminus" [e1] in
- let ty = Type_predef.type_array d ty_elt in
- expr.expr_type <- ty;
+ let ty = (* Type_predef. *)type_array d ty_elt in
+ expr.expr_type <- Expr_type_hub.export ty;
ty
| Expr_tuple elist ->
- let ty = new_ty (Ttuple (List.map (type_expr env in_main const) elist)) in
- expr.expr_type <- ty;
+ let ty = new_ty (Ttuple (List.map (type_expr ~is_annot env in_main const) elist)) in
+ expr.expr_type <- Expr_type_hub.export ty;
ty
| Expr_ite (c, t, e) ->
- type_subtyping_arg env in_main const c Type_predef.type_bool;
+ type_subtyping_arg env in_main const c (* Type_predef. *)type_bool;
let ty = type_appl env in_main expr.expr_loc const "+" [t; e] in
- expr.expr_type <- ty;
+ expr.expr_type <- Expr_type_hub.export ty;
ty
| Expr_appl (id, args, r) ->
(* application of non internal function is not legal in a constant
@@ -446,54 +482,55 @@ and type_expr env in_main const expr =
| None -> ()
| Some c ->
check_constant expr.expr_loc const false;
- type_subtyping_arg env in_main const c Type_predef.type_bool);
+ type_subtyping_arg env in_main const c (* Type_predef. *)type_bool);
let args_list = expr_list_of_expr args in
+ let targs = new_ty (Ttuple (List.map (fun a -> Expr_type_hub.import a.expr_type) args_list)) in
+ args.expr_type <- Expr_type_hub.export targs;
let touts = type_appl env in_main expr.expr_loc const id args_list in
- args.expr_type <- new_ty (Ttuple (List.map (fun a -> a.expr_type) args_list));
- expr.expr_type <- touts;
+ expr.expr_type <- Expr_type_hub.export touts;
touts
| Expr_fby (e1,e2)
| Expr_arrow (e1,e2) ->
(* fby/arrow is not legal in a constant expression *)
check_constant expr.expr_loc const false;
let ty = type_appl env in_main expr.expr_loc const "+" [e1; e2] in
- expr.expr_type <- ty;
+ expr.expr_type <- Expr_type_hub.export ty;
ty
| Expr_pre e ->
(* pre is not legal in a constant expression *)
check_constant expr.expr_loc const false;
let ty = type_appl env in_main expr.expr_loc const "uminus" [e] in
- expr.expr_type <- ty;
+ expr.expr_type <- Expr_type_hub.export ty;
ty
| Expr_when (e1,c,l) ->
(* when is not legal in a constant expression *)
check_constant expr.expr_loc const false;
- let typ_l = Type_predef.type_clock (type_const expr.expr_loc (Const_tag l)) in
+ let typ_l = (* Type_predef. *)type_clock (type_const ~is_annot expr.expr_loc (Const_tag l)) in
let expr_c = expr_of_ident c expr.expr_loc in
type_subtyping_arg env in_main ~sub:false const expr_c typ_l;
let ty = type_appl env in_main expr.expr_loc const "uminus" [e1] in
- expr.expr_type <- ty;
+ expr.expr_type <- Expr_type_hub.export ty;
ty
| Expr_merge (c,hl) ->
(* merge is not legal in a constant expression *)
check_constant expr.expr_loc const false;
let typ_in, typ_out = type_branches env in_main expr.expr_loc const hl in
let expr_c = expr_of_ident c expr.expr_loc in
- let typ_l = Type_predef.type_clock typ_in in
+ let typ_l = (* Type_predef. *)type_clock typ_in in
type_subtyping_arg env in_main ~sub:false const expr_c typ_l;
- expr.expr_type <- typ_out;
+ expr.expr_type <- Expr_type_hub.export typ_out;
typ_out
in
- Log.report ~level:3 (fun fmt -> Format.fprintf fmt "Type of expr %a: %a@." Printers.pp_expr expr Types.print_ty resulting_ty);
+ Log.report ~level:3 (fun fmt -> Format.fprintf fmt "Type of expr %a: %a@." Printers.pp_expr expr (* Types. *)print_ty resulting_ty);
resulting_ty
-and type_branches env in_main loc const hl =
+and type_branches ?(is_annot=false) env in_main loc const hl =
let typ_in = new_var () in
let typ_out = new_var () in
try
let used_labels =
List.fold_left (fun accu (t, h) ->
- unify typ_in (type_const loc (Const_tag t));
+ unify typ_in (type_const ~is_annot loc (Const_tag t));
type_subtyping_arg env in_main const h typ_out;
if List.mem t accu
then raise (Error (loc, Already_bound t))
@@ -548,7 +585,7 @@ let type_coreclock env ck id loc =
(fun expr (x, l) ->
{expr_tag = new_tag ();
expr_desc= Expr_when (expr,x,l);
- expr_type = new_var ();
+ expr_type = Types.Main.new_var ();
expr_clock = Clocks.new_var true;
expr_delay = Delay.new_var ();
expr_loc=loc;
@@ -571,22 +608,22 @@ let rec check_type_declaration loc cty =
let type_var_decl vd_env env vdecl =
(*Format.eprintf "Typing.type_var_decl START %a:%a@." Printers.pp_var vdecl Printers.print_dec_ty vdecl.var_dec_type.ty_dec_desc;*)
check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc;
- let eval_const id = Types.get_static_value (Env.lookup_value env id) in
+ let eval_const id = (* Types. *)get_static_value (Env.lookup_value env id) in
let type_dim d =
begin
- type_subtyping_arg (env, vd_env) false true (expr_of_dimension d) Type_predef.type_int;
+ type_subtyping_arg (env, vd_env) false true (expr_of_dimension d) (* Type_predef. *)type_int;
Dimension.eval Basic_library.eval_env eval_const d;
end in
let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in
let ty_static =
if vdecl.var_dec_const
- then Type_predef.type_static (Dimension.mkdim_var ()) ty
+ then (* Type_predef. *)type_static (Dimension.mkdim_var ()) ty
else ty in
(match vdecl.var_dec_value with
| None -> ()
| Some v -> type_subtyping_arg (env, vd_env) false ~sub:false true v ty_static);
- try_unify ty_static vdecl.var_type vdecl.var_loc;
+ try_unify ty_static (Expr_type_hub.import vdecl.var_type) vdecl.var_loc;
let new_env = Env.add_value env vdecl.var_id ty_static in
type_coreclock (new_env,vd_env) vdecl.var_dec_clock vdecl.var_id vdecl.var_loc;
(*Format.eprintf "END %a@." Types.print_ty ty_static;*)
@@ -596,7 +633,7 @@ let type_var_decl_list vd_env env l =
List.fold_left (type_var_decl vd_env) env l
let type_of_vlist vars =
- let tyl = List.map (fun v -> v.var_type) vars in
+ let tyl = List.map (fun v -> Expr_type_hub.import v.var_type) vars in
type_of_type_list tyl
let add_vdecl vd_env vdecl =
@@ -631,8 +668,12 @@ let type_node env nd loc =
(* Typing asserts *)
List.iter (fun assert_ ->
let assert_expr = assert_.assert_expr in
- type_subtyping_arg (new_env, vd_env) is_main false assert_expr Type_predef.type_bool
+ type_subtyping_arg (new_env, vd_env) is_main false assert_expr (* Type_predef. *)type_bool
) nd.node_asserts;
+ (* Typing annots *)
+ List.iter (fun annot ->
+ List.iter (fun (_, eexpr) -> ignore (type_expr ~is_annot:true (new_env, vd_env) false false eexpr.eexpr_qfexpr)) annot.annots
+ ) nd.node_annot;
(* check that table is empty *)
let local_consts = List.fold_left (fun res vdecl -> if vdecl.var_dec_const then ISet.add vdecl.var_id res else res) ISet.empty nd.node_locals in
@@ -644,7 +685,7 @@ let type_node env nd loc =
let ty_node = new_ty (Tarrow (ty_ins,ty_outs)) in
generalize ty_node;
(* TODO ? Check that no node in the hierarchy remains polymorphic ? *)
- nd.node_type <- ty_node;
+ nd.node_type <- Expr_type_hub.export ty_node;
Env.add_value env nd.node_id ty_node
let type_imported_node env nd loc =
@@ -661,7 +702,7 @@ let type_imported_node env nd loc =
raise (Error (loc, Poly_imported_node nd.nodei_id));
*)
let new_env = Env.add_value env nd.nodei_id ty_node in
- nd.nodei_type <- ty_node;
+ nd.nodei_type <- Expr_type_hub.export ty_node;
new_env
let type_top_const env cdecl =
@@ -670,9 +711,9 @@ let type_top_const env cdecl =
if is_dimension_type ty
then dimension_of_const cdecl.const_loc cdecl.const_value
else Dimension.mkdim_var () in
- let ty = Type_predef.type_static d ty in
+ let ty = (* Type_predef. *)type_static d ty in
let new_env = Env.add_value env cdecl.const_id ty in
- cdecl.const_type <- ty;
+ cdecl.const_type <- Expr_type_hub.export ty;
new_env
let type_top_consts env clist =
@@ -700,10 +741,10 @@ let rec type_top_decl env decl =
let get_type_of_call decl =
match decl.top_decl_desc with
| Node nd ->
- let (in_typ, out_typ) = split_arrow nd.node_type in
+ let (in_typ, out_typ) = split_arrow (Expr_type_hub.import nd.node_type) in
type_list_of_type in_typ, type_list_of_type out_typ
| ImportedNode nd ->
- let (in_typ, out_typ) = split_arrow nd.nodei_type in
+ let (in_typ, out_typ) = split_arrow (Expr_type_hub.import nd.nodei_type) in
type_list_of_type in_typ, type_list_of_type out_typ
| _ -> assert false
@@ -723,8 +764,8 @@ with Failure _ as exc -> raise exc
let uneval_vdecl_generics vdecl =
if vdecl.var_dec_const
then
- match get_static_value vdecl.var_type with
- | None -> (Format.eprintf "internal error: %a@." Types.print_ty vdecl.var_type; assert false)
+ match get_static_value (Expr_type_hub.import vdecl.var_type) with
+ | None -> (Format.eprintf "internal error: %a@." (* Types. *)print_ty (Expr_type_hub.import vdecl.var_type); assert false)
| Some d -> Dimension.uneval vdecl.var_id d
let uneval_node_generics vdecls =
@@ -788,7 +829,13 @@ let check_typedef_top decl =
let check_typedef_compat header =
List.iter check_typedef_top header
+end
+include Make(Types.Main) (struct
+ type type_expr = Types.Main.type_expr
+ let import x = x
+ let export x = x
+end)
(* Local Variables: *)
(* compile-command:"make -C .." *)
(* End: *)
--
GitLab