diff --git a/src/automata.ml b/src/automata.ml
new file mode 100755
index 0000000000000000000000000000000000000000..c412e82a925561277ad2244e211e6482d7966230
--- /dev/null
+++ b/src/automata.ml
@@ -0,0 +1,94 @@
+(********************************************************************)
+(* *)
+(* The LustreC compiler toolset / The LustreC Development Team *)
+(* Copyright 2012 - -- ONERA - CNRS - INPT *)
+(* *)
+(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)
+(* under the terms of the GNU Lesser General Public License *)
+(* version 2.1. *)
+(* *)
+(********************************************************************)
+
+open LustreSpec
+open Corelang
+
+let mkbool loc b =
+ mkexpr loc (Expr_const (const_of_bool b))
+
+let mkident loc id =
+ mkexpr loc (Expr_ident id)
+
+let init (loc, restart, st) =
+ mkexpr loc (Expr_tuple [mkbool loc restart; mkident loc st])
+
+let add_branch expr (loc, restart, st) cont =
+ mkexpr loc (Expr_ite (expr, init (loc, restart, st), cont))
+
+let mkhandler loc st unless until locals eqs =
+ {hand_state = st;
+ hand_unless = unless;
+ hand_until = until;
+ hand_locals = locals;
+ hand_eqs = eqs;
+ hand_loc = loc}
+
+let mkautomata loc id handlers =
+ {aut_id = id;
+ aut_handlers = handlers;
+ aut_loc = loc}
+
+let pp_restart fmt restart =
+ Format.fprintf fmt "%s" (if restart then "restart" else "resume")
+
+let pp_unless fmt (expr, restart, st) =
+ Format.fprintf fmt "unless %a %a %s"
+ Printers.pp_expr expr
+ pp_restart restart
+ st
+
+let pp_until fmt (expr, restart, st) =
+ Format.fprintf fmt "until %a %a %s"
+ Printers.pp_expr expr
+ pp_restart restart
+ st
+
+let pp_handler fmt handler =
+ Format.fprintf fmt "state %s -> %a %a let %a tel %a"
+ handler.hand_state
+ (Utils.fprintf_list ~sep:"@ " pp_unless) handler.hand_unless
+ (fun fmt locals ->
+ match locals with [] -> () | _ ->
+ Format.fprintf fmt "@[<v 4>var %a@]@ "
+ (Utils.fprintf_list ~sep:"@ "
+ (fun fmt v -> Format.fprintf fmt "%a;" Printers.pp_node_var v))
+ locals)
+ handler.hand_locals
+ Printers.pp_node_eqs handler.hand_eqs
+ (Utils.fprintf_list ~sep:"@ " pp_until) handler.hand_until
+
+let pp_automata fmt aut =
+ Format.fprintf fmt "automaton %s %a"
+ aut.aut_id
+ (Utils.fprintf_list ~sep:"@ " pp_handler) aut.aut_handlers
+
+(*
+let rec extract_node expr top_decls =
+ match expr.expr_desc with
+ | Expr_const _
+ | Expr_ident _
+ | Expr_tuple _
+ | 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
+*)
+
+(* Local Variables: *)
+(* compile-command:"make -C .." *)
+(* End: *)
diff --git a/src/backends/C/c_backend.ml b/src/backends/C/c_backend.ml
index 932e8033a0f5529c5cb932548db896a401060ce1..832066200be7290f0a454be7a6690d7ce3f3ca70 100644
--- a/src/backends/C/c_backend.ml
+++ b/src/backends/C/c_backend.ml
@@ -13,7 +13,7 @@ open Format
(********************************************************************************************)
(* Translation function *)
(********************************************************************************************)
-
+(* USELESS
let makefile_opt print basename dependencies makefile_fmt machines =
(* If a main node is identified, generate a main target for it *)
match !Options.main_node with
@@ -23,7 +23,7 @@ let makefile_opt print basename dependencies makefile_fmt machines =
| None -> Format.eprintf "Unable to find a main node named %s@.@?" main_node; ()
| Some _ -> print basename !Options.main_node dependencies makefile_fmt
)
-
+*)
let gen_files funs basename prog machines dependencies header_file source_lib_file source_main_file makefile_file machines =
let header_out = open_out header_file in
@@ -33,11 +33,14 @@ let gen_files funs basename prog machines dependencies header_file source_lib_fi
let print_header, print_lib_c, print_main_c, print_makefile = funs in
(* Generating H file *)
- print_header header_fmt basename prog machines;
+ print_header header_fmt basename prog machines dependencies;
(* Generating Lib C file *)
print_lib_c source_lib_fmt basename prog machines dependencies;
+ close_out header_out;
+ close_out source_lib_out;
+
match !Options.main_node with
| "" -> () (* No main node: we do not genenrate main nor makefile *)
| main_node -> (
@@ -53,11 +56,13 @@ let gen_files funs basename prog machines dependencies header_file source_lib_fi
print_main_c source_main_fmt m basename prog machines dependencies;
(* Generating Makefile *)
- print_makefile basename main_node dependencies makefile_fmt
+ print_makefile basename main_node dependencies makefile_fmt;
+
+ close_out source_main_out;
+ close_out makefile_out
+
end
)
-
-
let translate_to_c header source_lib source_main makefile basename prog machines dependencies =
@@ -73,7 +78,7 @@ let translate_to_c header source_lib source_main makefile basename prog machines
let module SourceMain = C_backend_main.Main (SourceMainMod) in
let module Makefile = C_backend_makefile.Main (MakefileMod) in
- let funs = Header.print_header, Source.print_lib_c, SourceMain.print_main_c, Makefile.print_makefile in
+ let funs = Header.print_alloc_header, Source.print_lib_c, SourceMain.print_main_c, Makefile.print_makefile in
gen_files funs basename prog machines dependencies header source_lib source_main makefile machines
end
@@ -89,7 +94,7 @@ let translate_to_c header source_lib source_main makefile basename prog machines
let module SourceMain = C_backend_main.Main (SourceMainMod) in
let module Makefile = C_backend_makefile.Main (MakefileMod) in
- let funs = Header.print_header, Source.print_lib_c, SourceMain.print_main_c, Makefile.print_makefile in
+ let funs = Header.print_alloc_header, Source.print_lib_c, SourceMain.print_main_c, Makefile.print_makefile in
gen_files funs basename prog machines dependencies header source_lib source_main makefile machines
end
diff --git a/src/backends/C/c_backend_common.ml b/src/backends/C/c_backend_common.ml
index 0299ea40688ec563c58edbcf9a9552d101c54531..cced6a9831272da62a94a4f06adfbe2749b562b6 100644
--- a/src/backends/C/c_backend_common.ml
+++ b/src/backends/C/c_backend_common.ml
@@ -21,8 +21,7 @@ let print_version fmt =
(Filename.basename Sys.executable_name)
Version.number
(if !Options.ansi then "ANSI C90" else "C99")
-
-
+
(* Generation of a non-clashing name for the self memory variable (for step and reset functions) *)
let mk_self m =
mk_new_name (m.mstep.step_inputs@m.mstep.step_outputs@m.mstep.step_locals@m.mmemory) "self"
@@ -235,6 +234,43 @@ let pp_c_checks self fmt m =
fmt
m.mstep.step_checks
+(********************************************************************************************)
+(* Struct Printing functions *)
+(********************************************************************************************)
+
+let pp_registers_struct fmt m =
+ if m.mmemory <> []
+ then
+ fprintf fmt "@[%a {@[%a; @]}@] _reg; "
+ pp_machine_regtype_name m.mname.node_id
+ (Utils.fprintf_list ~sep:"; " pp_c_decl_struct_var) m.mmemory
+ else
+ ()
+
+let print_machine_struct fmt m =
+ if fst (get_stateless_status m) then
+ begin
+ end
+ else
+ begin
+ (* Define struct *)
+ fprintf fmt "@[%a {@[%a%a%t@]};@]@."
+ pp_machine_memtype_name m.mname.node_id
+ pp_registers_struct m
+ (Utils.fprintf_list ~sep:"; " pp_c_decl_instance_var) m.minstances
+ (Utils.pp_final_char_if_non_empty "; " m.minstances)
+ end
+
+let print_machine_struct_from_header fmt inode =
+ if inode.nodei_stateless then
+ begin
+ end
+ else
+ begin
+ (* Declare struct *)
+ fprintf fmt "@[%a;@]@."
+ pp_machine_memtype_name inode.nodei_id
+ end
(********************************************************************************************)
(* Prototype Printing functions *)
@@ -271,9 +307,20 @@ let print_step_prototype self fmt (name, inputs, outputs) =
pp_machine_memtype_name name
self
-let print_import_prototype fmt (s, _, _) =
+let print_import_prototype fmt (_, s, _) =
fprintf fmt "#include \"%s.h\"@," s
+let print_import_alloc_prototype fmt (_, s, _) =
+ fprintf fmt "#include \"%s_alloc.h\"@," s
+
+let print_extern_alloc_prototypes fmt (_,_, header) =
+ List.iter (fun decl -> match decl.top_decl_desc with
+ | ImportedNode ind when not ind.nodei_stateless ->
+ let static = List.filter (fun v -> v.var_dec_const) ind.nodei_inputs
+ in fprintf fmt "extern %a;@." print_alloc_prototype (ind.nodei_id, static)
+ | _ -> ()
+ ) header
+
(* Local Variables: *)
(* compile-command:"make -C ../../.." *)
(* End: *)
diff --git a/src/backends/C/c_backend_header.ml b/src/backends/C/c_backend_header.ml
index 1147e9a93d7a2223d01b6f87d5ec827136f76e9b..3a7d50d1d1a2ab7365c8ca25234d137de556b514 100644
--- a/src/backends/C/c_backend_header.ml
+++ b/src/backends/C/c_backend_header.ml
@@ -36,30 +36,6 @@ struct
let print_import_standard fmt =
fprintf fmt "#include \"%s/include/lustrec/arrow.h\"@.@." Version.prefix
-
-let pp_registers_struct fmt m =
- if m.mmemory <> []
- then
- fprintf fmt "@[%a {@[%a; @]}@] _reg; "
- pp_machine_regtype_name m.mname.node_id
- (Utils.fprintf_list ~sep:"; " pp_c_decl_struct_var) m.mmemory
- else
- ()
-
-let print_machine_struct fmt m =
- if fst (get_stateless_status m) then
- begin
- end
- else
- begin
- (* Define struct *)
- fprintf fmt "@[%a {@[%a%a%t@]};@]@."
- pp_machine_memtype_name m.mname.node_id
- pp_registers_struct m
- (Utils.fprintf_list ~sep:"; " pp_c_decl_instance_var) m.minstances
- (Utils.pp_final_char_if_non_empty "; " m.minstances)
- end
-
let print_static_declare_instance attr fmt (i, (m, static)) =
fprintf fmt "%a(%s, %a%t%s)"
pp_machine_static_declare_name (node_name m)
@@ -161,15 +137,54 @@ let print_machine_decl fmt m =
(m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
end
+let print_machine_alloc_decl fmt m =
+ Mod.print_machine_decl_prefix fmt m;
+ if fst (get_stateless_status m) then
+ begin
+ end
+ else
+ begin
+ if !Options.static_mem
+ then
+ begin
+ (* Static allocation *)
+ fprintf fmt "%a@.%a@.%a@."
+ print_static_declare_macro m
+ print_static_link_macro m
+ print_static_alloc_macro m
+ end
+ else
+ begin
+ (* Dynamic allocation *)
+ fprintf fmt "extern %a;@."
+ print_alloc_prototype (m.mname.node_id, m.mstatic)
+ end
+ end
+
+let print_machine_decl_from_header fmt inode =
+ (*Mod.print_machine_decl_prefix fmt m;*)
+ if inode.nodei_stateless then
+ begin
+ fprintf fmt "extern %a;@.@."
+ print_stateless_prototype
+ (inode.nodei_id, inode.nodei_inputs, inode.nodei_outputs)
+ end
+ else
+ begin
+ let static_inputs = List.filter (fun v -> v.var_dec_const) inode.nodei_inputs in
+ let self = mk_new_name (inode.nodei_inputs@inode.nodei_outputs) "self" in
+ fprintf fmt "extern %a;@.@."
+ (print_reset_prototype self) (inode.nodei_id, static_inputs);
+
+ fprintf fmt "extern %a;@.@."
+ (print_step_prototype self)
+ (inode.nodei_id, inode.nodei_inputs, inode.nodei_outputs)
+ end
+
let print_const_decl fmt cdecl =
fprintf fmt "extern %a;@."
(pp_c_type cdecl.const_id) cdecl.const_type
-(********************************************************************************************)
-(* Struct/TypeDef Printing functions *)
-(********************************************************************************************)
-
-
let rec pp_c_struct_type_field filename cpt fmt (label, tdesc) =
fprintf fmt "%a;" (pp_c_type_decl filename cpt label) tdesc
and pp_c_type_decl filename cpt var fmt tdecl =
@@ -195,49 +210,143 @@ and pp_c_type_decl filename cpt var fmt tdecl =
let print_type_definitions fmt filename =
let cpt_type = ref 0 in
- Hashtbl.iter (fun typ def ->
- match typ with
- | Tydec_const var ->
- fprintf fmt "typedef %a;@.@."
- (pp_c_type_decl filename cpt_type var) def
- | _ -> ()) type_table
+ Hashtbl.iter (fun typ decl ->
+ match typ with
+ | Tydec_const var ->
+ (match decl.top_decl_desc with
+ | TypeDef tdef ->
+ fprintf fmt "typedef %a;@.@."
+ (pp_c_type_decl filename cpt_type var) tdef.tydef_desc
+ | _ -> assert false)
+ | _ -> ()) type_table
+
+let reset_type_definitions, print_type_definition_from_header =
+ let cpt_type =ref 0 in
+ ((fun () -> cpt_type := 0),
+ (fun fmt typ filename ->
+ fprintf fmt "typedef %a;@.@."
+ (pp_c_type_decl filename cpt_type typ.tydef_id) typ.tydef_desc))
(********************************************************************************************)
(* MAIN Header Printing functions *)
(********************************************************************************************)
-let print_header header_fmt basename prog machines =
+let print_header header_fmt basename prog machines dependencies =
(* Include once: start *)
let baseNAME = String.uppercase basename in
let baseNAME = Str.global_replace (Str.regexp "\\.\\|\\ ") "_" baseNAME in
- (* Print the svn version number and the supported C standard (C90 or C99) *)
- print_version header_fmt;
- fprintf header_fmt "#ifndef _%s@.#define _%s@." baseNAME baseNAME;
- pp_print_newline header_fmt ();
- fprintf header_fmt "/* Imports standard library */@.";
- (* imports standard library definitions (arrow) *)
- print_import_standard header_fmt;
- pp_print_newline header_fmt ();
- fprintf header_fmt "/* Types definitions */@.";
- (* Print the type definitions from the type table *)
- print_type_definitions header_fmt basename;
- pp_print_newline header_fmt ();
- (* Print the global constant declarations. *)
- fprintf header_fmt "/* Global constant (declarations, definitions are in C file) */@.";
- List.iter (fun c -> print_const_decl header_fmt c) (get_consts prog);
- pp_print_newline header_fmt ();
- (* Print the struct declarations of all machines. *)
- fprintf header_fmt "/* Struct declarations */@.";
- List.iter (print_machine_struct header_fmt) machines;
- pp_print_newline header_fmt ();
- (* Print the prototypes of all machines *)
- fprintf header_fmt "/* Nodes declarations */@.";
- List.iter (print_machine_decl header_fmt) machines;
- pp_print_newline header_fmt ();
- (* Include once: end *)
- fprintf header_fmt "#endif@.";
- pp_print_newline header_fmt ()
-end
+ begin
+ (* Print the svn version number and the supported C standard (C90 or C99) *)
+ print_version header_fmt;
+ fprintf header_fmt "#ifndef _%s@.#define _%s@." baseNAME baseNAME;
+ pp_print_newline header_fmt ();
+ fprintf header_fmt "/* Imports standard library */@.";
+ (* imports standard library definitions (arrow) *)
+ print_import_standard header_fmt;
+ pp_print_newline header_fmt ();
+ (* imports dependencies *)
+ fprintf header_fmt "/* Import Dependencies */@.";
+ fprintf header_fmt "@[<v>";
+ List.iter (print_import_prototype header_fmt) dependencies;
+ fprintf header_fmt "@]@.";
+ fprintf header_fmt "/* Types definitions */@.";
+ (* Print the type definitions from the type table *)
+ print_type_definitions header_fmt basename;
+ pp_print_newline header_fmt ();
+ (* Print the global constant declarations. *)
+ fprintf header_fmt "/* Global constant (declarations, definitions are in C file) */@.";
+ List.iter (fun c -> print_const_decl header_fmt (const_of_top c)) (get_consts prog);
+ pp_print_newline header_fmt ();
+ (* Print the struct declarations of all machines. *)
+ fprintf header_fmt "/* Struct declarations */@.";
+ List.iter (print_machine_struct header_fmt) machines;
+ pp_print_newline header_fmt ();
+ (* Print the prototypes of all machines *)
+ fprintf header_fmt "/* Nodes declarations */@.";
+ List.iter (print_machine_decl header_fmt) machines;
+ pp_print_newline header_fmt ();
+ (* Include once: end *)
+ fprintf header_fmt "#endif@.";
+ pp_print_newline header_fmt ()
+ end
+
+let print_alloc_header header_fmt basename prog machines dependencies =
+ (* Include once: start *)
+ let baseNAME = String.uppercase basename in
+ let baseNAME = Str.global_replace (Str.regexp "\\.\\|\\ ") "_" baseNAME in
+ begin
+ (* Print the svn version number and the supported C standard (C90 or C99) *)
+ print_version header_fmt;
+ fprintf header_fmt "#ifndef _%s_alloc@.#define _%s_alloc@." baseNAME baseNAME;
+ pp_print_newline header_fmt ();
+ (* Import the header *)
+ fprintf header_fmt "/* Import header from %s */@." basename;
+ fprintf header_fmt "@[<v>";
+ print_import_prototype header_fmt (true, basename, []);
+ fprintf header_fmt "@]@.";
+ fprintf header_fmt "/* Import dependencies */@.";
+ fprintf header_fmt "@[<v>";
+ List.iter (print_import_alloc_prototype header_fmt) dependencies;
+ fprintf header_fmt "@]@.";
+ (* Print the struct definitions of all machines. *)
+ fprintf header_fmt "/* Struct definitions */@.";
+ List.iter (print_machine_struct header_fmt) machines;
+ pp_print_newline header_fmt ();
+ (* Print the prototypes of all machines *)
+ fprintf header_fmt "/* Node allocation function/macro prototypes */@.";
+ List.iter (print_machine_alloc_decl header_fmt) machines;
+ pp_print_newline header_fmt ();
+ (* Include once: end *)
+ fprintf header_fmt "#endif@.";
+ pp_print_newline header_fmt ()
+ end
+let print_header_from_header header_fmt basename header =
+ (* Include once: start *)
+ let baseNAME = String.uppercase basename in
+ let baseNAME = Str.global_replace (Str.regexp "\\.\\|\\ ") "_" baseNAME in
+ let types = get_typedefs header in
+ let consts = get_consts header in
+ let nodes = get_imported_nodes header in
+ let dependencies = get_dependencies header in
+ begin
+ (* Print the svn version number and the supported C standard (C90 or C99) *)
+ print_version header_fmt;
+ fprintf header_fmt "#ifndef _%s@.#define _%s@." baseNAME baseNAME;
+ pp_print_newline header_fmt ();
+ fprintf header_fmt "/* Imports standard library */@.";
+ (* imports standard library definitions (arrow) *)
+ print_import_standard header_fmt;
+ pp_print_newline header_fmt ();
+ (* imports dependencies *)
+ fprintf header_fmt "/* Import dependencies */@.";
+ fprintf header_fmt "@[<v>";
+ List.iter
+ (fun dep -> let (local, s) = dependency_of_top dep in print_import_prototype header_fmt (local, s, []))
+ dependencies;
+ fprintf header_fmt "@]@.";
+ fprintf header_fmt "/* Types definitions */@.";
+ (* Print the type definitions from the type table *)
+ reset_type_definitions ();
+ List.iter (fun typ -> print_type_definition_from_header header_fmt (typedef_of_top typ) basename) types;
+ pp_print_newline header_fmt ();
+ (* Print the global constant declarations. *)
+ fprintf header_fmt "/* Global constant (declarations, definitions are in C file) */@.";
+ List.iter (fun c -> print_const_decl header_fmt (const_of_top c)) consts;
+ pp_print_newline header_fmt ();
+ (* Print the struct declarations of all machines. *)
+ fprintf header_fmt "/* Struct declarations */@.";
+ List.iter (fun node -> print_machine_struct_from_header header_fmt (imported_node_of_top node)) nodes;
+ pp_print_newline header_fmt ();
+ (* Print the prototypes of all machines *)
+ fprintf header_fmt "/* Nodes declarations */@.";
+ List.iter (fun node -> print_machine_decl_from_header header_fmt (imported_node_of_top node)) nodes;
+ pp_print_newline header_fmt ();
+ (* Include once: end *)
+ fprintf header_fmt "#endif@.";
+ pp_print_newline header_fmt ()
+ end
+
+end
(* Local Variables: *)
(* compile-command:"make -C ../../.." *)
(* End: *)
diff --git a/src/backends/C/c_backend_main.ml b/src/backends/C/c_backend_main.ml
index 2dde47a13702ff6b08c0ab2618d1f2f17e0e4cd3..66790707e89f27025f47c6922f8fa7a856317068 100644
--- a/src/backends/C/c_backend_main.ml
+++ b/src/backends/C/c_backend_main.ml
@@ -112,7 +112,10 @@ let print_main_header fmt =
let print_main_c main_fmt main_machine basename prog machines dependencies =
print_main_header main_fmt;
- fprintf main_fmt "#include <stdlib.h>@.#include <assert.h>@.#include \"%s\"@.@." (basename^".h");
+ fprintf main_fmt "#include <stdlib.h>@.#include <assert.h>@.";
+ print_import_alloc_prototype main_fmt (true, basename, []);
+ pp_print_newline main_fmt ();
+
(* Print the svn version number and the supported C standard (C90 or C99) *)
print_version main_fmt;
print_main_fun machines main_machine main_fmt
diff --git a/src/backends/C/c_backend_makefile.ml b/src/backends/C/c_backend_makefile.ml
index a4882e580effdcae666e4024ff566331b604cbe1..c0d6f76ad6bc77fc1c99e2b62291559554ca7e8e 100644
--- a/src/backends/C/c_backend_makefile.ml
+++ b/src/backends/C/c_backend_makefile.ml
@@ -17,7 +17,7 @@ let header_has_code header =
List.exists
(fun top ->
match top.top_decl_desc with
- | Consts _ -> true
+ | Const _ -> true
| ImportedNode nd -> nd.nodei_in_lib = None
| _ -> false
)
@@ -46,13 +46,13 @@ let fprintf_dependencies fmt dep =
fprintf fmt "\t${GCC} -I${INC} -c %s@." s)
(("${INC}/io_frontend.c"):: (* IO functions when a main function is computed *)
(List.map
- (fun (s, local, _) ->
+ (fun (local, s, _) ->
(if local then s else Version.prefix ^ "/include/lustrec/" ^ s) ^ ".c")
compiled_dep))
module type MODIFIERS_MKF =
sig
- val other_targets: Format.formatter -> string -> string -> (string * bool * top_decl list) list -> unit
+ val other_targets: Format.formatter -> string -> string -> (bool * string * top_decl list) list -> unit
end
module EmptyMod =
@@ -77,7 +77,7 @@ let print_makefile basename nodename dependencies fmt =
fprintf fmt "\t${GCC} -I${INC} -I. -c %s_main.c@." basename;
fprintf_dependencies fmt dependencies;
fprintf fmt "\t${GCC} -o %s_%s io_frontend.o %a %s.o %s_main.o %a@." basename nodename
- (Utils.fprintf_list ~sep:" " (fun fmt (s, _, _) -> Format.fprintf fmt "%s.o" s)) (compiled_dependencies dependencies)
+ (Utils.fprintf_list ~sep:" " (fun fmt (_, s, _) -> Format.fprintf fmt "%s.o" s)) (compiled_dependencies dependencies)
basename (* library .o *)
basename (* main function . o *)
(Utils.fprintf_list ~sep:" " (fun fmt lib -> fprintf fmt "-l%s" lib)) (lib_dependencies dependencies)
diff --git a/src/backends/C/c_backend_spec.ml b/src/backends/C/c_backend_spec.ml
index e03f535bedde4a336df057a117e062b490efd553..52881a526539f1bd324bc3fba02be13e845398be 100644
--- a/src/backends/C/c_backend_spec.ml
+++ b/src/backends/C/c_backend_spec.ml
@@ -158,7 +158,7 @@ let makefile_targets fmt basename nodename dependencies =
C_backend_makefile.fprintf_dependencies fmt dependencies;
fprintf fmt "\t${GCC} -Wno-attributes -o %s_main_eacsl io_frontend.o %a %s %s_main_eacsl.o %a@."
basename
- (Utils.fprintf_list ~sep:" " (fun fmt (s, _, _) -> Format.fprintf fmt "%s.o" s))
+ (Utils.fprintf_list ~sep:" " (fun fmt (_, s, _) -> Format.fprintf fmt "%s.o" s))
(C_backend_makefile.compiled_dependencies dependencies)
("${FRAMACEACSL}/e_acsl.c "
^ "${FRAMACEACSL}/memory_model/e_acsl_bittree.c "
diff --git a/src/backends/C/c_backend_src.ml b/src/backends/C/c_backend_src.ml
index 02e213724f5b78b197a9fbf2079a5a8a684d1356..6857a54965a542e83426e29df32abea7e9593110 100644
--- a/src/backends/C/c_backend_src.ml
+++ b/src/backends/C/c_backend_src.ml
@@ -259,7 +259,7 @@ let print_alloc_code fmt m =
let print_stateless_code dependencies fmt m =
let self = "__ERROR__" in
- if not (!Options.ansi && is_generic_node { top_decl_desc = Node m.mname; top_decl_loc = Location.dummy_loc })
+ if not (!Options.ansi && is_generic_node { top_decl_desc = Node m.mname; top_decl_loc = Location.dummy_loc; top_decl_owner = ""; top_decl_itf = false })
then
(* C99 code *)
fprintf fmt "@[<v 2>%a {@,%a%t@,%a%a%t%t@]@,}@.@."
@@ -296,7 +296,7 @@ let print_reset_code dependencies fmt m self =
(Utils.pp_newline_if_non_empty m.minit)
let print_step_code dependencies fmt m self =
- if not (!Options.ansi && is_generic_node { top_decl_desc = Node m.mname; top_decl_loc = Location.dummy_loc })
+ if not (!Options.ansi && is_generic_node { top_decl_desc = Node m.mname; top_decl_loc = Location.dummy_loc; top_decl_owner = ""; top_decl_itf = false })
then
(* C99 code *)
let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
@@ -345,11 +345,11 @@ let print_machine dependencies fmt m =
begin
(* Alloc function, only if non static mode *)
if (not !Options.static_mem) then
- (
+ begin
fprintf fmt "@[<v 2>%a {@,%a@]@,}@.@."
print_alloc_prototype (m.mname.node_id, m.mstatic)
print_alloc_code m;
- );
+ end;
let self = mk_self m in
(* Reset function *)
print_reset_code dependencies fmt m self;
@@ -360,17 +360,41 @@ let print_machine dependencies fmt m =
let print_lib_c source_fmt basename prog machines dependencies =
- fprintf source_fmt "#include <stdlib.h>@.#include <assert.h>@.#include \"%s\"@.@." (basename^".h");
+ fprintf source_fmt "#include <assert.h>@.";
+ if not !Options.static_mem then
+ begin
+ fprintf source_fmt "#include <stdlib.h>@.";
+ end;
+ print_import_prototype source_fmt (true, basename, []);
+ pp_print_newline source_fmt ();
(* Print the svn version number and the supported C standard (C90 or C99) *)
print_version source_fmt;
(* Print the prototype of imported nodes *)
- fprintf source_fmt "/* Imported nodes declarations */@.";
+ fprintf source_fmt "/* Import dependencies */@.";
fprintf source_fmt "@[<v>";
List.iter (print_import_prototype source_fmt) dependencies;
fprintf source_fmt "@]@.";
(* Print consts *)
fprintf source_fmt "/* Global constants (definitions) */@.";
- List.iter (fun c -> print_const_def source_fmt c) (get_consts prog);
+ fprintf source_fmt "@[<v>";
+ List.iter (fun c -> print_const_def source_fmt (const_of_top c)) (get_consts prog);
+ fprintf source_fmt "@]@.";
+ if not !Options.static_mem then
+ begin
+ fprintf source_fmt "/* External allocation function prototypes */@.";
+ fprintf source_fmt "@[<v>";
+ List.iter (print_extern_alloc_prototypes source_fmt) dependencies;
+ fprintf source_fmt "@]@.";
+ fprintf source_fmt "/* Node allocation function prototypes */@.";
+ fprintf source_fmt "@[<v>";
+ List.iter (fun m -> fprintf source_fmt "%a;@." print_alloc_prototype (m.mname.node_id, m.mstatic)) machines;
+ fprintf source_fmt "@]@.";
+ end;
+ (* Print the struct definitions of all machines. *)
+ fprintf source_fmt "/* Struct definitions */@.";
+ fprintf source_fmt "@[<v>";
+ List.iter (print_machine_struct source_fmt) machines;
+ fprintf source_fmt "@]@.";
pp_print_newline source_fmt ();
(* Print nodes one by one (in the previous order) *)
List.iter (print_machine dependencies source_fmt) machines;
diff --git a/src/basic_library.ml b/src/basic_library.ml
index 02dde4e6f81c1b16256eb992eafb623a7b775d5f..080e4c4e61d8ce73f7c7e711350fc67b54fb6e2b 100644
--- a/src/basic_library.ml
+++ b/src/basic_library.ml
@@ -27,7 +27,9 @@ let type_env =
(fun env (op, op_type) -> TE.add_value env op op_type)
TE.initial
[
- "+", (static_op type_bin_poly_op);
+ "true", (static_op type_bool);
+ "false", (static_op type_bool);
+ "+", (static_op type_bin_poly_op);
"uminus", (static_op type_unary_poly_op);
"-", (static_op type_bin_poly_op);
"*", (static_op type_bin_poly_op);
@@ -51,9 +53,12 @@ module CE = Env
let clock_env =
let init_env = CE.initial in
+ let env' =
+ List.fold_right (fun op env -> CE.add_value env op ck_nullary_univ)
+ ["true"; "false"] init_env in
let env' =
List.fold_right (fun op env -> CE.add_value env op ck_unary_univ)
- ["uminus"; "not"] init_env in
+ ["uminus"; "not"] env' in
let env' =
List.fold_right (fun op env -> CE.add_value env op ck_bin_univ)
["+"; "-"; "*"; "/"; "mod"; "&&"; "||"; "xor"; "equi"; "impl"; "<"; "<="; ">"; ">="; "!="; "="] env' in
@@ -63,9 +68,12 @@ module DE = Env
let delay_env =
let init_env = DE.initial in
- let env' =
+ let env' =
+ List.fold_right (fun op env -> DE.add_value env op delay_nullary_poly_op)
+ ["true"; "false"] init_env in
+ let env' =
List.fold_right (fun op env -> DE.add_value env op delay_unary_poly_op)
- ["uminus"; "not"] init_env in
+ ["uminus"; "not"] env' in
let env' =
List.fold_right (fun op env -> DE.add_value env op delay_binary_poly_op)
["+"; "-"; "*"; "/"; "mod"; "&&"; "||"; "xor"; "equi"; "impl"; "<"; "<="; ">"; ">="; "!="; "="] env' in
diff --git a/src/clock_calculus.ml b/src/clock_calculus.ml
index 45e129b8ea132752b030c32685878f5caff61298..42556941af442772c112855714a2734680739665 100755
--- a/src/clock_calculus.ml
+++ b/src/clock_calculus.ml
@@ -832,25 +832,27 @@ let clock_imported_node env loc nd =
nd.nodei_clock <- ck_node;
Env.add_value env nd.nodei_id ck_node
-let clock_top_consts env clist =
- List.fold_left (fun env cdecl ->
- let ck = new_var false in
- try_generalize ck cdecl.const_loc;
- Env.add_value env cdecl.const_id ck) env clist
+let clock_top_const env cdecl=
+ let ck = new_var false in
+ try_generalize ck cdecl.const_loc;
+ Env.add_value env cdecl.const_id ck
-let clock_top_decl env decl =
+let clock_top_consts env clist =
+ List.fold_left clock_top_const env clist
+
+let rec clock_top_decl env decl =
match decl.top_decl_desc with
| Node nd ->
clock_node env decl.top_decl_loc nd
| ImportedNode nd ->
clock_imported_node env decl.top_decl_loc nd
- | Consts clist ->
- clock_top_consts env clist
- | Open _
- | Type _ -> env
+ | Const c ->
+ clock_top_const env c
+ | TypeDef _ -> List.fold_left clock_top_decl env (consts_of_enum_type decl)
+ | Open _ -> env
let clock_prog env decls =
- List.fold_left (fun e decl -> clock_top_decl e decl) env decls
+ List.fold_left clock_top_decl env decls
(* Once the Lustre program is fully clocked,
we must get back to the original description of clocks,
@@ -878,9 +880,9 @@ let uneval_top_generics decl =
uneval_node_generics (nd.node_inputs @ nd.node_locals @ nd.node_outputs)
| ImportedNode nd ->
uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
- | Consts _
+ | Const _
| Open _
- | Type _ -> ()
+ | TypeDef _ -> ()
let uneval_prog_generics prog =
List.iter uneval_top_generics prog
diff --git a/src/clock_predef.ml b/src/clock_predef.ml
index 155dba080c949b93bbcc6d3deb51dbf8981ab7f8..7c1a0a5d790ad3f06d94e955fbeaa6482f4909b1 100644
--- a/src/clock_predef.ml
+++ b/src/clock_predef.ml
@@ -22,6 +22,10 @@ let ck_ite =
let univ = new_univar () in
new_ck (Carrow (new_ck (Ctuple [univ;univ;univ]) true, univ)) true
+let ck_nullary_univ =
+ let univ = new_univar () in
+ univ
+
let ck_unary_univ =
let univ = new_univar () in
new_ck (Carrow (univ, univ)) true
diff --git a/src/compiler_common.ml b/src/compiler_common.ml
new file mode 100644
index 0000000000000000000000000000000000000000..5318993d63cbf7b0d17ca2484c80c364d7ca70ea
--- /dev/null
+++ b/src/compiler_common.ml
@@ -0,0 +1,214 @@
+(********************************************************************)
+(* *)
+(* The LustreC compiler toolset / The LustreC Development Team *)
+(* Copyright 2012 - -- ONERA - CNRS - INPT *)
+(* *)
+(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)
+(* under the terms of the GNU Lesser General Public License *)
+(* version 2.1. *)
+(* *)
+(********************************************************************)
+
+open Utils
+open Format
+open LustreSpec
+open Corelang
+
+let create_dest_dir () =
+ begin
+ if not (Sys.file_exists !Options.dest_dir) then
+ begin
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. creating destination directory@,");
+ Unix.mkdir !Options.dest_dir (Unix.stat ".").Unix.st_perm
+ end;
+ if (Unix.stat !Options.dest_dir).Unix.st_kind <> Unix.S_DIR then
+ begin
+ eprintf "Failure: destination %s is not a directory.@.@." !Options.dest_dir;
+ exit 1
+ end
+ end
+
+(* Loading Lusi file and filling type tables with parsed
+ functions/nodes *)
+let parse_header own filename =
+ Location.set_input filename;
+ let h_in = open_in filename in
+ let lexbuf = Lexing.from_channel h_in in
+ Location.init lexbuf filename;
+ (* Parsing *)
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. parsing header file %s@ " filename);
+ try
+ let header = Parse.header Parser_lustre.header Lexer_lustre.token lexbuf in
+ ignore (Modules.load_header ISet.empty header);
+ close_in h_in;
+ header
+ with
+ | (Lexer_lustre.Error err) | (Parse.Syntax_err err) as exc ->
+ Parse.report_error err;
+ raise exc
+ | Corelang.Error (loc, err) as exc -> (
+ eprintf "Parsing error: %a%a@."
+ Corelang.pp_error err
+ Location.pp_loc loc;
+ raise exc
+ )
+
+let parse_source source_name =
+ (* Loading the input file *)
+ Location.set_input source_name;
+ let s_in = open_in source_name in
+ let lexbuf = Lexing.from_channel s_in in
+ Location.init lexbuf source_name;
+
+ (* Parsing *)
+ Log.report ~level:1
+ (fun fmt -> fprintf fmt ".. parsing source file %s@," source_name);
+ try
+ let prog = Parse.prog Parser_lustre.prog Lexer_lustre.token lexbuf in
+ ignore (Modules.load_program ISet.empty prog);
+ close_in s_in;
+ prog
+ with
+ | (Lexer_lustre.Error err) | (Parse.Syntax_err err) as exc ->
+ Parse.report_error err;
+ raise exc
+ | Corelang.Error (loc, err) as exc ->
+ eprintf "Parsing error %a%a@."
+ Corelang.pp_error err
+ Location.pp_loc loc;
+ raise exc
+
+let check_stateless_decls decls =
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. checking stateless/stateful status@ ");
+ try
+ Stateless.check_prog decls
+ with (Stateless.Error (loc, err)) as exc ->
+ eprintf "Stateless status error %a%a@."
+ Stateless.pp_error err
+ Location.pp_loc loc;
+ raise exc
+
+let type_decls env decls =
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. typing@ ");
+ let new_env =
+ begin
+ try
+ Typing.type_prog env decls
+ with (Types.Error (loc,err)) as exc ->
+ eprintf "Typing error %a%a@."
+ Types.pp_error err
+ Location.pp_loc loc;
+ raise exc
+ end
+ in
+ if !Options.print_types then
+ Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2> %a@]@ " Corelang.pp_prog_type decls);
+ new_env
+
+let clock_decls env decls =
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. clock calculus@ ");
+ let new_env =
+ begin
+ try
+ Clock_calculus.clock_prog env decls
+ with (Clocks.Error (loc,err)) as exc ->
+ eprintf "Clock calculus error %a%a@." Clocks.pp_error err Location.pp_loc loc;
+ raise exc
+ end
+ in
+ if !Options.print_clocks then
+ Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2> %a@]@ " Corelang.pp_prog_clock decls);
+ new_env
+
+let check_top_decls header =
+ let new_tenv = type_decls Basic_library.type_env header in (* Typing *)
+ let new_cenv = clock_decls Basic_library.clock_env header in (* Clock calculus *)
+ header, new_tenv, new_cenv
+
+let get_envs_from_const const_decl (ty_env, ck_env) =
+ (Env.add_value ty_env const_decl.const_id const_decl.const_type,
+ Env.add_value ck_env const_decl.const_id (Clocks.new_var true))
+
+let get_envs_from_consts const_decls (ty_env, ck_env) =
+ List.fold_right get_envs_from_const const_decls (ty_env, ck_env)
+
+let rec get_envs_from_top_decl (ty_env, ck_env) top_decl =
+ match top_decl.top_decl_desc with
+ | Node nd -> (Env.add_value ty_env nd.node_id nd.node_type,
+ Env.add_value ck_env nd.node_id nd.node_clock)
+ | ImportedNode ind -> (Env.add_value ty_env ind.nodei_id ind.nodei_type,
+ Env.add_value ck_env ind.nodei_id ind.nodei_clock)
+ | Const c -> get_envs_from_const c (ty_env, ck_env)
+ | TypeDef _ -> List.fold_left get_envs_from_top_decl (ty_env, ck_env) (consts_of_enum_type top_decl)
+ | Open _ -> (ty_env, ck_env)
+
+(* get type and clock environments from a header *)
+let get_envs_from_top_decls header =
+ List.fold_left get_envs_from_top_decl (Env.initial, Env.initial) header
+
+(*
+ List.fold_right
+ (fun top_decl (ty_env, ck_env) ->
+ match top_decl.top_decl_desc with
+ | Node nd -> (Env.add_value ty_env nd.node_id nd.node_type,
+ Env.add_value ck_env nd.node_id nd.node_clock)
+ | ImportedNode ind -> (Env.add_value ty_env ind.nodei_id ind.nodei_type,
+ Env.add_value ck_env ind.nodei_id ind.nodei_clock)
+ | Const c -> get_envs_from_const c (ty_env, ck_env)
+ | TypeDef _ -> List.fold_left (fun envs top -> consts_of_enum_type top_decl
+ | Open _ -> (ty_env, ck_env))
+ header
+ (Env.initial, Env.initial)
+ *)
+
+let check_compatibility (prog, computed_types_env, computed_clocks_env) (header, declared_types_env, declared_clocks_env) =
+ try
+ (* checking defined types are compatible with declared types*)
+ Typing.check_typedef_compat header;
+
+ (* checking type compatibility with computed types*)
+ Typing.check_env_compat header declared_types_env computed_types_env;
+
+ (* checking clocks compatibility with computed clocks*)
+ Clock_calculus.check_env_compat header declared_clocks_env computed_clocks_env;
+
+ (* checking stateless status compatibility *)
+ Stateless.check_compat header
+ with
+ | (Types.Error (loc,err)) as exc ->
+ eprintf "Type mismatch between computed type and declared type in lustre interface file: %a@."
+ Types.pp_error err;
+ raise exc
+ | Clocks.Error (loc, err) as exc ->
+ eprintf "Clock mismatch between computed clock and declared clock in lustre interface file: %a@."
+ Clocks.pp_error err;
+ raise exc
+ | Stateless.Error (loc, err) as exc ->
+ eprintf "Stateless status mismatch between defined status and declared status in lustre interface file: %a@."
+ Stateless.pp_error err;
+ raise exc
+
+
+
+let import_dependencies prog =
+ Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. extracting dependencies@,");
+ let dependencies = Corelang.get_dependencies prog in
+ let deps =
+ List.fold_left
+ (fun (compilation_dep, type_env, clock_env) dep ->
+ let (local, s) = Corelang.dependency_of_top dep in
+ let basename = Modules.name_dependency (local, s) in
+ Log.report ~level:1 (fun fmt -> Format.fprintf fmt "@[<v 0>Library %s@," basename);
+ let lusic = Modules.import_dependency dep.top_decl_loc (local, s) in
+ Log.report ~level:1 (fun fmt -> Format.fprintf fmt "@]@ ");
+ let (lusi_type_env, lusi_clock_env) = get_envs_from_top_decls lusic.Lusic.contents in
+ (local, s, lusic.Lusic.contents)::compilation_dep,
+ Env.overwrite type_env lusi_type_env,
+ Env.overwrite clock_env lusi_clock_env)
+ ([], Basic_library.type_env, Basic_library.clock_env)
+ dependencies in
+ begin
+ Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ ");
+ deps
+ end
+
diff --git a/src/corelang.ml b/src/corelang.ml
index f8f0ebb65d52ea4230a263cbb337021ecad04845..16f4e3405b91b03f8fab6e07cd9d95631dbe2f89 100755
--- a/src/corelang.ml
+++ b/src/corelang.ml
@@ -28,8 +28,6 @@ module VSet = Set.Make(VDeclModule)
let dummy_type_dec = {ty_dec_desc=Tydec_any; ty_dec_loc=Location.dummy_loc}
-
-
let dummy_clock_dec = {ck_dec_desc=Ckdec_any; ck_dec_loc=Location.dummy_loc}
@@ -87,12 +85,46 @@ let mkassert loc expr =
assert_expr = expr
}
-let mktop_decl loc d =
- { top_decl_desc = d; top_decl_loc = loc }
+let mktop_decl loc own itf d =
+ { top_decl_desc = d; top_decl_loc = loc; top_decl_owner = own; top_decl_itf = itf }
let mkpredef_call loc funname args =
mkexpr loc (Expr_appl (funname, mkexpr loc (Expr_tuple args), None))
+
+let const_of_top top_decl =
+ match top_decl.top_decl_desc with
+ | Const c -> c
+ | _ -> assert false
+
+let node_of_top top_decl =
+ match top_decl.top_decl_desc with
+ | Node nd -> nd
+ | _ -> assert false
+
+let imported_node_of_top top_decl =
+ match top_decl.top_decl_desc with
+ | ImportedNode ind -> ind
+ | _ -> assert false
+
+let typedef_of_top top_decl =
+ match top_decl.top_decl_desc with
+ | TypeDef tdef -> tdef
+ | _ -> assert false
+
+let dependency_of_top top_decl =
+ match top_decl.top_decl_desc with
+ | Open (local, dep) -> (local, dep)
+ | _ -> assert false
+
+let consts_of_enum_type top_decl =
+ match top_decl.top_decl_desc with
+ | TypeDef tdef ->
+ (match tdef.tydef_desc with
+ | Tydec_enum tags -> List.map (fun tag -> let cdecl = { const_id = tag; const_loc = top_decl.top_decl_loc; const_value = Const_tag tag; const_type = Type_predef.type_const tdef.tydef_id } in { top_decl with top_decl_desc = Const cdecl }) tags
+ | _ -> [])
+ | _ -> assert false
+
(************************************************************)
(* Eexpr functions *)
(************************************************************)
@@ -142,6 +174,28 @@ let update_expr_annot e annot =
let (node_table : (ident, top_decl) Hashtbl.t) = Hashtbl.create 30
let consts_table = Hashtbl.create 30
+let print_node_table fmt () =
+ begin
+ Format.fprintf fmt "{ /* node table */@.";
+ Hashtbl.iter (fun id nd ->
+ Format.fprintf fmt "%s |-> %a"
+ id
+ Printers.pp_short_decl nd
+ ) node_table;
+ Format.fprintf fmt "}@."
+ end
+
+let print_consts_table fmt () =
+ begin
+ Format.fprintf fmt "{ /* consts table */@.";
+ Hashtbl.iter (fun id const ->
+ Format.fprintf fmt "%s |-> %a"
+ id
+ Printers.pp_const_decl (const_of_top const)
+ ) consts_table;
+ Format.fprintf fmt "}@."
+ end
+
let node_name td =
match td.top_decl_desc with
| Node nd -> nd.node_id
@@ -174,14 +228,31 @@ let is_imported_node td =
(* alias and type definition table *)
+
+let top_int_type = mktop_decl Location.dummy_loc Version.prefix false (TypeDef {tydef_id = "int"; tydef_desc = Tydec_int})
+let top_bool_type = mktop_decl Location.dummy_loc Version.prefix false (TypeDef {tydef_id = "bool"; tydef_desc = Tydec_bool})
+let top_float_type = mktop_decl Location.dummy_loc Version.prefix false (TypeDef {tydef_id = "float"; tydef_desc = Tydec_float})
+let top_real_type = mktop_decl Location.dummy_loc Version.prefix false (TypeDef {tydef_id = "real"; tydef_desc = Tydec_real})
+
let type_table =
Utils.create_hashtable 20 [
- Tydec_int , Tydec_int;
- Tydec_bool , Tydec_bool;
- Tydec_float, Tydec_float;
- Tydec_real , Tydec_real
+ Tydec_int , top_int_type;
+ Tydec_bool , top_bool_type;
+ Tydec_float, top_float_type;
+ Tydec_real , top_real_type
]
+let print_type_table fmt () =
+ begin
+ Format.fprintf fmt "{ /* type table */@.";
+ Hashtbl.iter (fun tydec tdef ->
+ Format.fprintf fmt "%a |-> %a"
+ Printers.pp_var_type_dec_desc tydec
+ Printers.pp_typedef (typedef_of_top tdef)
+ ) type_table;
+ Format.fprintf fmt "}@."
+ end
+
let rec is_user_type typ =
match typ with
| Tydec_int | Tydec_bool | Tydec_real
@@ -190,16 +261,16 @@ let rec is_user_type typ =
| _ -> true
let get_repr_type typ =
- let typ_def = Hashtbl.find type_table typ in
+ let typ_def = (typedef_of_top (Hashtbl.find type_table typ)).tydef_desc in
if is_user_type typ_def then typ else typ_def
let rec coretype_equal ty1 ty2 =
- (*let res =*)
+ let res =
match ty1, ty2 with
| Tydec_any , _
| _ , Tydec_any -> assert false
| Tydec_const _ , Tydec_const _ -> get_repr_type ty1 = get_repr_type ty2
- | Tydec_const _ , _ -> let ty1' = Hashtbl.find type_table ty1
+ | Tydec_const _ , _ -> let ty1' = (typedef_of_top (Hashtbl.find type_table ty1)).tydef_desc
in (not (is_user_type ty1')) && coretype_equal ty1' ty2
| _ , Tydec_const _ -> coretype_equal ty2 ty1
| Tydec_int , Tydec_int
@@ -215,7 +286,7 @@ let rec coretype_equal ty1 ty2 =
(List.sort (fun (f1,_) (f2,_) -> compare f1 f2) fl1)
(List.sort (fun (f1,_) (f2,_) -> compare f1 f2) fl2)
| _ -> false
- (*in (Format.eprintf "coretype_equal %a %a = %B@." Printers.pp_var_type_dec_desc ty1 Printers.pp_var_type_dec_desc ty2 res; res)*)
+ in ((*Format.eprintf "coretype_equal %a %a = %B@." Printers.pp_var_type_dec_desc ty1 Printers.pp_var_type_dec_desc ty2 res;*) res)
let tag_true = "true"
let tag_false = "false"
@@ -262,8 +333,8 @@ let const_impl c1 c2 =
(* To guarantee uniqueness of tags in enum types *)
let tag_table =
Utils.create_hashtable 20 [
- tag_true, Tydec_bool;
- tag_false, Tydec_bool
+ tag_true, top_bool_type;
+ tag_false, top_bool_type
]
(* To guarantee uniqueness of fields in struct types *)
@@ -272,16 +343,17 @@ let field_table =
]
let get_enum_type_tags cty =
+(*Format.eprintf "get_enum_type_tags %a@." Printers.pp_var_type_dec_desc cty;*)
match cty with
| Tydec_bool -> [tag_true; tag_false]
- | Tydec_const _ -> (match Hashtbl.find type_table cty with
+ | Tydec_const _ -> (match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with
| Tydec_enum tl -> tl
| _ -> assert false)
| _ -> assert false
let get_struct_type_fields cty =
match cty with
- | Tydec_const _ -> (match Hashtbl.find type_table cty with
+ | Tydec_const _ -> (match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with
| Tydec_struct fl -> fl
| _ -> assert false)
| _ -> assert false
@@ -403,25 +475,41 @@ let get_nodes prog =
List.fold_left (
fun nodes decl ->
match decl.top_decl_desc with
- | Node nd -> nd::nodes
- | Consts _ | ImportedNode _ | Open _ | Type _ -> nodes
+ | Node _ -> decl::nodes
+ | Const _ | ImportedNode _ | Open _ | TypeDef _ -> nodes
) [] prog
-let get_consts prog =
+let get_imported_nodes prog =
List.fold_left (
- fun consts decl ->
+ fun nodes decl ->
match decl.top_decl_desc with
- | Consts clist -> clist@consts
- | Node _ | ImportedNode _ | Open _ | Type _ -> consts
+ | ImportedNode _ -> decl::nodes
+ | Const _ | Node _ | Open _ | TypeDef _-> nodes
) [] prog
-let get_types prog =
- List.fold_left (
- fun types decl ->
+let get_consts prog =
+ List.fold_right (
+ fun decl consts ->
match decl.top_decl_desc with
- | Type typ -> typ::types
- | Node _ | ImportedNode _ | Open _ | Consts _ -> types
- ) [] prog
+ | Const _ -> decl::consts
+ | Node _ | ImportedNode _ | Open _ | TypeDef _ -> consts
+ ) prog []
+
+let get_typedefs prog =
+ List.fold_right (
+ fun decl types ->
+ match decl.top_decl_desc with
+ | TypeDef _ -> decl::types
+ | Node _ | ImportedNode _ | Open _ | Const _ -> types
+ ) prog []
+
+let get_dependencies prog =
+ List.fold_right (
+ fun decl deps ->
+ match decl.top_decl_desc with
+ | Open _ -> decl::deps
+ | Node _ | ImportedNode _ | TypeDef _ | Const _ -> deps
+ ) prog []
let get_node_interface nd =
{nodei_id = nd.node_id;
@@ -582,11 +670,11 @@ let rename_prog f_node f_var f_const prog =
(match top.top_decl_desc with
| Node nd ->
{ top with top_decl_desc = Node (rename_node f_node f_var f_const nd) }
- | Consts c ->
- { top with top_decl_desc = Consts (List.map (rename_const f_const) c) }
+ | Const c ->
+ { top with top_decl_desc = Const (rename_const f_const c) }
| ImportedNode _
| Open _
- | Type _ -> top)
+ | TypeDef _ -> top)
::accu
) [] prog
)
@@ -604,7 +692,7 @@ let pp_decl_type fmt tdecl =
fprintf fmt "%s: " ind.nodei_id;
Utils.reset_names ();
fprintf fmt "%a@ " Types.print_ty ind.nodei_type
- | Consts _ | Open _ | Type _ -> ()
+ | Const _ | Open _ | TypeDef _ -> ()
let pp_prog_type fmt tdecl_list =
Utils.fprintf_list ~sep:"" pp_decl_type fmt tdecl_list
@@ -619,7 +707,7 @@ let pp_decl_clock fmt cdecl =
fprintf fmt "%s: " ind.nodei_id;
Utils.reset_names ();
fprintf fmt "%a@ " Clocks.print_ck ind.nodei_clock
- | Consts _ | Open _ | Type _ -> ()
+ | Const _ | Open _ | TypeDef _ -> ()
let pp_prog_clock fmt prog =
Utils.fprintf_list ~sep:"" pp_decl_clock fmt prog
@@ -642,6 +730,10 @@ let pp_error fmt = function
fprintf fmt
"%s is already defined.@."
sym
+ | Unknown_library sym ->
+ fprintf fmt
+ "impossible to load library %s.@."
+ sym
(* filling node table with internal functions *)
let vdecls_of_typ_ck cpt ty =
@@ -659,7 +751,7 @@ let mk_internal_node id =
let (tin, tout) = Types.split_arrow ty in
(*eprintf "internal fun %s: %d -> %d@." id (List.length (Types.type_list_of_type tin)) (List.length (Types.type_list_of_type tout));*)
let cpt = ref (-1) in
- mktop_decl Location.dummy_loc
+ mktop_decl Location.dummy_loc Version.prefix false
(ImportedNode
{nodei_id = id;
nodei_type = ty;
diff --git a/src/corelang.mli b/src/corelang.mli
index f1f1989198337373c9d13627ef18baf623661d66..1dbf06b67b5d57a8b2b8b589a95733cfe5f6980b 100755
--- a/src/corelang.mli
+++ b/src/corelang.mli
@@ -24,32 +24,37 @@ val var_decl_of_const: 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
-val mktop_decl: Location.t -> top_decl_desc -> top_decl
+val mktop_decl: Location.t -> ident -> bool -> top_decl_desc -> top_decl
val mkpredef_call: Location.t -> ident -> expr list -> expr
val mk_new_name: var_decl list -> ident -> ident
val node_table : (ident, top_decl) Hashtbl.t
+val print_node_table: Format.formatter -> unit -> unit
val node_name: top_decl -> ident
val node_inputs: top_decl -> var_decl list
val node_from_name: ident -> top_decl
val is_generic_node: top_decl -> bool
val is_imported_node: top_decl -> bool
-val consts_table: (ident, const_desc) Hashtbl.t
-val type_table: (type_dec_desc, type_dec_desc) Hashtbl.t
+val consts_table: (ident, top_decl) Hashtbl.t
+val print_consts_table: Format.formatter -> unit -> unit
+val type_table: (type_dec_desc, top_decl) Hashtbl.t
+val print_type_table: Format.formatter -> unit -> unit
val get_repr_type: type_dec_desc -> type_dec_desc
val is_user_type: type_dec_desc -> bool
val coretype_equal: type_dec_desc -> type_dec_desc -> bool
val tag_true: label
val tag_false: label
-val tag_table: (label, type_dec_desc) Hashtbl.t
-val field_table: (label, type_dec_desc) Hashtbl.t
+val tag_table: (label, top_decl) Hashtbl.t
+val field_table: (label, top_decl) Hashtbl.t
val get_enum_type_tags: type_dec_desc -> label list
val get_struct_type_fields: type_dec_desc -> (label * type_dec_desc) list
+val consts_of_enum_type: top_decl -> top_decl list
+
val const_of_bool: bool -> constant
val const_is_bool: constant -> bool
val const_negation: constant -> constant
@@ -90,8 +95,17 @@ val pp_prog_type : Format.formatter -> program -> unit
val pp_prog_clock : Format.formatter -> program -> unit
-val get_nodes : program -> node_desc list
- val get_consts : program -> const_desc list
+val const_of_top: top_decl -> const_desc
+val node_of_top: top_decl -> node_desc
+val imported_node_of_top: top_decl -> imported_node_desc
+val typedef_of_top: top_decl -> typedef_desc
+val dependency_of_top: top_decl -> (bool * ident)
+
+val get_nodes : program -> top_decl list
+val get_imported_nodes : program -> top_decl list
+val get_consts : program -> top_decl list
+val get_typedefs: program -> top_decl list
+val get_dependencies : program -> top_decl list
(* val prog_unfold_consts: program -> program *)
val expr_replace_var: (ident -> ident) -> expr -> expr
diff --git a/src/delay_predef.ml b/src/delay_predef.ml
index 9c9051270e39b827d0829620c7d154cb4b3e0430..c03017f39f355f7a3e0070b003049077096a4c5c 100755
--- a/src/delay_predef.ml
+++ b/src/delay_predef.ml
@@ -17,6 +17,10 @@ let delay_zero () = new_univar ()
let delay_un =
new_delay Dundef
+let delay_nullary_poly_op =
+ let univ = new_univar () in
+ univ
+
let delay_unary_poly_op =
let univ = new_univar () in
new_delay (Darrow (univ, univ))
diff --git a/src/inliner.ml b/src/inliner.ml
index e73b5ce2994cea3092e3cd23cc1feeef457c4043..08640119d1e70d59855cd43be20ec2507dafa64c 100644
--- a/src/inliner.ml
+++ b/src/inliner.ml
@@ -279,7 +279,7 @@ let witness filename main_name orig inlined type_env clock_env =
node_annot = [];
}
in
- let main = [{ top_decl_desc = Node main_node; top_decl_loc = loc }] in
+ let main = [{ top_decl_desc = Node main_node; top_decl_loc = loc; top_decl_owner = filename; top_decl_itf = false }] in
let new_prog = others@nodes_origs@nodes_inlined@main in
let _ = Typing.type_prog type_env new_prog in
let _ = Clock_calculus.clock_prog clock_env new_prog in
diff --git a/src/lexer_lustre.mll b/src/lexer_lustre.mll
index 02a5255a8ced28229af9b459342cc114521b58da..6fa09b53675bcf7fb9888084e80b7496ab849656 100755
--- a/src/lexer_lustre.mll
+++ b/src/lexer_lustre.mll
@@ -53,6 +53,8 @@ let keyword_table =
"clock", TCLOCK;
"not", NOT;
"tail", TAIL;
+ "true", TRUE;
+ "false", FALSE;
"and", AND;
"or", OR;
"xor", XOR;
@@ -114,12 +116,18 @@ rule token = parse
| "tel." {TEL}
| "tel;" {TEL}
| "#open" { OPEN }
-| ['_' 'a'-'z' 'A'-'Z'] [ '_' 'a'-'z' 'A'-'Z' '0'-'9']*
+| ['_' 'a'-'z'] [ '_' 'a'-'z' 'A'-'Z' '0'-'9']*
{let s = Lexing.lexeme lexbuf in
try
Hashtbl.find keyword_table s
with Not_found ->
IDENT s}
+| ['A'-'Z'] [ '_' 'a'-'z' 'A'-'Z' '0'-'9']*
+ {let s = Lexing.lexeme lexbuf in
+ try
+ Hashtbl.find keyword_table s
+ with Not_found ->
+ UIDENT s}
| "->" {ARROW}
| "=>" {IMPL}
| "<=" {LTE}
diff --git a/src/liveness.ml b/src/liveness.ml
index 9fc1dc8da52cbf95ddac2ab6cbbe5b9b7d8bca82..6fae8414f2263c97305cb38d2363b82c8a1441f1 100755
--- a/src/liveness.ml
+++ b/src/liveness.ml
@@ -65,11 +65,6 @@ let compute_unused_variables n g =
(ISet.union outputs mems)
(ISet.union inputs mems)
-(* checks whether a variable is aliasable,
- depending on its (address) type *)
-let is_aliasable var =
- Types.is_address_type var.var_type
-
(* computes the set of potentially reusable variables.
We don't reuse input variables, due to possible aliasing *)
let node_reusable_variables node =
diff --git a/src/location.ml b/src/location.ml
index 1dc6919aa3c7a2f40884e59ad8e6a5d02859fec0..31f25234eff0dff31a9706f36cff1b004a90ef79 100755
--- a/src/location.ml
+++ b/src/location.ml
@@ -10,9 +10,17 @@
(********************************************************************)
type t = { loc_start: Lexing.position; loc_end: Lexing.position }
+
+type filename = string
+
let dummy_loc = {loc_start=Lexing.dummy_pos; loc_end=Lexing.dummy_pos}
-let input_name = ref ""
+let set_input, get_input, get_module =
+ let input_name : filename ref = ref "__UNINITIALIZED__" in
+ let module_name : filename ref = ref "__UNINITIALIZED__" in
+ (fun name -> input_name := name; module_name := Filename.chop_extension name),
+ (fun () -> !input_name),
+ (fun () -> !module_name)
let curr lexbuf = {
loc_start = lexbuf.Lexing.lex_start_p;
diff --git a/src/lusic.ml b/src/lusic.ml
new file mode 100644
index 0000000000000000000000000000000000000000..951081adbee95ccd053d6c1ecdb259e295953e07
--- /dev/null
+++ b/src/lusic.ml
@@ -0,0 +1,76 @@
+
+(********************************************************************)
+(* *)
+(* The LustreC compiler toolset / The LustreC Development Team *)
+(* Copyright 2012 - -- ONERA - CNRS - INPT *)
+(* *)
+(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)
+(* under the terms of the GNU Lesser General Public License *)
+(* version 2.1. *)
+(* *)
+(********************************************************************)
+
+open Format
+open LustreSpec
+open Corelang
+
+(********************************************************************************************)
+(* Lusic to/from Header Printing functions *)
+(********************************************************************************************)
+
+type lusic =
+{ from_lusi : bool;
+ contents : top_decl list;
+}
+
+module HeaderMod = C_backend_header.EmptyMod
+module Header = C_backend_header.Main (HeaderMod)
+
+(* extracts a header from a program representing module own *)
+let extract_header own prog =
+ List.fold_right
+ (fun decl header ->
+ if decl.top_decl_itf || decl.top_decl_owner <> own then header else
+ match decl.top_decl_desc with
+ | Node nd -> { decl with top_decl_desc = ImportedNode (Corelang.get_node_interface nd) } :: header
+ | ImportedNode _ -> header
+ | Const _
+ | TypeDef _
+ | Open _ -> decl :: header)
+ prog []
+
+(* encode and write a header in a file *)
+let write_lusic lusi (header : top_decl list) basename extension =
+ let basename' = !Options.dest_dir ^ "/" ^ basename in
+ let target_name = basename' ^ extension in
+ let outchan = open_out_bin target_name in
+ begin
+ Marshal.to_channel outchan {from_lusi = lusi; contents = header} [];
+ close_out outchan
+ end
+
+(* read and decode a header from a file *)
+let read_lusic basename extension =
+ let basename' = !Options.dest_dir ^ "/" ^ basename in
+ let source_name = basename' ^ extension in
+ let inchan = open_in_bin source_name in
+ let lusic = (Marshal.from_channel inchan : lusic) in
+ begin
+ close_in inchan;
+ lusic
+ end
+
+let print_lusic_to_h basename extension =
+ let basename' = !Options.dest_dir ^ "/" ^ basename in
+ let lusic = read_lusic basename extension in
+ let header_name = basename' ^ ".h" in
+ let h_out = open_out header_name in
+ let h_fmt = formatter_of_out_channel h_out in
+ begin
+ Typing.uneval_prog_generics lusic.contents;
+ Clock_calculus.uneval_prog_generics lusic.contents;
+ Header.print_header_from_header h_fmt basename lusic.contents;
+ close_out h_out
+ end
+
+
diff --git a/src/lustreSpec.ml b/src/lustreSpec.ml
index b2497c3e12e1aebeeb9ff220dd0fa9bba4cb8761..67058e71014833109f9b1bbb2d30fed98292452b 100644
--- a/src/lustreSpec.ml
+++ b/src/lustreSpec.ml
@@ -32,10 +32,12 @@ and type_dec_desc =
| Tydec_struct of (ident * type_dec_desc) list
| Tydec_array of Dimension.dim_expr * type_dec_desc
-type type_def =
- {
- ty_def_id: ident;
- ty_def_desc: type_dec_desc}
+type typedec_desc =
+ {tydec_id: ident}
+
+type typedef_desc =
+ {tydef_id: ident;
+ tydef_desc: type_dec_desc}
type clock_dec =
{ck_dec_desc: clock_dec_desc;
@@ -99,12 +101,18 @@ and expr_desc =
| Expr_when of expr * ident * label
| Expr_merge of ident * (label * expr) list
| Expr_appl of call_t
- and call_t = ident * expr * (ident * label) option
+
+and call_t = ident * expr * (ident * label) option
(* The third part denotes the reseting clock label and value *)
-and
+
+and eq =
+ {eq_lhs: ident list;
+ eq_rhs: expr;
+ eq_loc: Location.t}
+
(* The tag of an expression is a unique identifier used to distinguish
different instances of the same node *)
- eexpr =
+and eexpr =
{eexpr_tag: tag;
eexpr_qfexpr: expr;
eexpr_quantifiers: (quantifier_type * var_decl list) list;
@@ -113,16 +121,9 @@ and
mutable eexpr_normalized: (var_decl * eq list * var_decl list) option;
eexpr_loc: Location.t}
-and expr_annot = {
- annots: (string list * eexpr) list;
- annot_loc: Location.t
-}
-and
- eq =
- {eq_lhs: ident list;
- eq_rhs: expr;
- eq_loc: Location.t}
-
+and expr_annot =
+ {annots: (string list * eexpr) list;
+ annot_loc: Location.t}
type node_annot = {
requires: eexpr list;
@@ -136,6 +137,23 @@ type assert_t =
assert_loc: Location.t;
}
+type automata_desc =
+ {aut_id : ident;
+ aut_handlers: handler_desc list;
+ aut_loc: Location.t}
+
+and handler_desc =
+ {hand_state: ident;
+ hand_unless: (expr * bool * ident) list;
+ hand_until: (expr * bool * ident) list;
+ hand_locals: var_decl list;
+ hand_eqs: eq list;
+ hand_loc: Location.t}
+
+type statement =
+| Eq of eq
+| Aut of automata_desc
+
type node_desc =
{node_id: ident;
mutable node_type: Types.type_expr;
@@ -174,15 +192,17 @@ type const_desc =
type top_decl_desc =
| Node of node_desc
-| Consts of const_desc list
+| Const of const_desc
| ImportedNode of imported_node_desc
| Open of bool * string (* the boolean set to true denotes a local
lusi vs a lusi installed at system level *)
-| Type of type_def
+| TypeDef of typedef_desc
type top_decl =
- {top_decl_desc: top_decl_desc;
- top_decl_loc: Location.t}
+ {top_decl_desc: top_decl_desc; (* description of the symbol *)
+ top_decl_owner: Location.filename; (* the module where it is defined *)
+ top_decl_itf: bool; (* header or source file ? *)
+ top_decl_loc: Location.t} (* the location where it is defined *)
type program = top_decl list
@@ -192,7 +212,7 @@ type error =
| No_main_specified
| Unbound_symbol of ident
| Already_bound_symbol of ident
-
+ | Unknown_library of ident
(* Local Variables: *)
(* compile-command:"make -C .." *)
diff --git a/src/machine_code.ml b/src/machine_code.ml
index 0e24b49c778322b459cb87b843d570293c49aca5..2b4b4ab4c0d840284622b6194b9c24a79da9e5ed 100644
--- a/src/machine_code.ml
+++ b/src/machine_code.ml
@@ -165,6 +165,8 @@ let arrow_desc =
let arrow_top_decl =
{
top_decl_desc = Node arrow_desc;
+ top_decl_owner = Version.prefix;
+ top_decl_itf = false;
top_decl_loc = Location.dummy_loc
}
@@ -224,8 +226,12 @@ let translate_ident node (m, si, j, d, s) id =
if ISet.exists (fun v -> v.var_id = id) m
then StateVar var_id
else LocalVar var_id
- with Not_found -> (* id is a constant *)
- LocalVar (Corelang.var_decl_of_const (Hashtbl.find Corelang.consts_table id))
+ with Not_found ->
+ try (* id is a constant *)
+ LocalVar (Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id)))
+ with Not_found ->
+ (* id is a tag *)
+ Cst (Const_tag id)
let rec control_on_clock node ((m, si, j, d, s) as args) ck inst =
match (Clocks.repr ck).cdesc with
@@ -446,27 +452,6 @@ let translate_eqs node args eqs =
let translate_decl nd sch =
(*Log.report ~level:1 (fun fmt -> Printers.pp_node fmt nd);*)
-(*
- let eqs_rev, remainder =
- List.fold_left
- (fun (accu, node_eqs_remainder) v ->
- if List.exists (fun eq -> List.mem v eq.eq_lhs) accu
- then
- (accu, node_eqs_remainder)
- else
- (*if List.exists (fun vdecl -> vdecl.var_id = v) nd.node_locals
- || List.exists (fun vdecl -> vdecl.var_id = v) nd.node_outputs
- then*)
- let eq_v, remainder = find_eq v node_eqs_remainder in
- eq_v::accu, remainder
- (* else it is a constant value, checked during typing phase
- else
- accu, node_eqs_remainder *)
- )
- ([], split_eqs)
- sch
- in
- *)
let sorted_eqs = sort_equations_from_schedule nd sch in
let init_args = ISet.empty, [], Utils.IMap.empty, List.fold_right (fun l -> ISet.add l) nd.node_locals ISet.empty, [] in
@@ -506,7 +491,8 @@ let translate_decl nd sch =
let translate_prog decls node_schs =
let nodes = get_nodes decls in
List.map
- (fun node ->
+ (fun decl ->
+ let node = node_of_top decl in
let sch = (Utils.IMap.find node.node_id node_schs).Scheduling.schedule in
translate_decl node sch
) nodes
diff --git a/src/main_lustre_compiler.ml b/src/main_lustre_compiler.ml
index e8d491c86d2542839f3f8571a476e167ec70c7e6..9e18d620e7da4b4c1623cd5f24050f6ac7a8df75 100644
--- a/src/main_lustre_compiler.ml
+++ b/src/main_lustre_compiler.ml
@@ -1,445 +1,313 @@
-(********************************************************************)
-(* *)
-(* The LustreC compiler toolset / The LustreC Development Team *)
-(* Copyright 2012 - -- ONERA - CNRS - INPT *)
-(* *)
-(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)
-(* under the terms of the GNU Lesser General Public License *)
-(* version 2.1. *)
-(* *)
-(********************************************************************)
-
-open Format
-open Log
-
-open LustreSpec
-
-let usage = "Usage: lustrec [options] <source-file>"
-
-let extensions = [".ec"; ".lus"; ".lusi"]
-
-let check_stateless_decls decls =
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. checking stateless/stateful status@ ");
- try
- Stateless.check_prog decls
- with (Stateless.Error (loc, err)) as exc ->
- eprintf "Stateless status error %a%a@."
- Stateless.pp_error err
- Location.pp_loc loc;
- raise exc
-
-let type_decls env decls =
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. typing@ ");
- let new_env =
- begin
- try
- Typing.type_prog env decls
- with (Types.Error (loc,err)) as exc ->
- eprintf "Typing error %a%a@."
- Types.pp_error err
- Location.pp_loc loc;
- raise exc
- end
- in
- if !Options.print_types then
- Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2> %a@]@ " Corelang.pp_prog_type decls);
- new_env
-
-let clock_decls env decls =
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. clock calculus@ ");
- let new_env =
- begin
- try
- Clock_calculus.clock_prog env decls
- with (Clocks.Error (loc,err)) as exc ->
- eprintf "Clock calculus error %a%a@." Clocks.pp_error err Location.pp_loc loc;
- raise exc
- end
- in
- if !Options.print_clocks then
- Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2> %a@]@ " Corelang.pp_prog_clock decls);
- new_env
-
-(* Loading Lusi file and filling type tables with parsed
- functions/nodes *)
-let load_lusi own filename =
- Location.input_name := filename;
- let lexbuf = Lexing.from_channel (open_in filename) in
- Location.init lexbuf filename;
- (* Parsing *)
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. parsing header file %s@ " filename);
- try
- Parse.header own Parser_lustre.header Lexer_lustre.token lexbuf
- with
- | (Lexer_lustre.Error err) | (Parse.Syntax_err err) as exc ->
- Parse.report_error err;
- raise exc
- | Corelang.Error (loc, err) as exc -> (
- eprintf "Parsing error: %a%a@."
- Corelang.pp_error err
- Location.pp_loc loc;
- raise exc
- )
-
-
-let check_lusi header =
- let new_tenv = type_decls Basic_library.type_env header in (* Typing *)
- let new_cenv = clock_decls Basic_library.clock_env header in (* Clock calculus *)
- header, new_tenv, new_cenv
-
-let load_n_check_lusi source_name lusi_name prog computed_types_env computed_clocks_env=
- try
- let _ = open_in lusi_name in
- let header = load_lusi true lusi_name in
- let _, declared_types_env, declared_clocks_env = check_lusi header in
-
- (* checking defined types are compatible with declared types*)
- Typing.check_typedef_compat header;
-
- (* checking type compatibility with computed types*)
- Typing.check_env_compat header declared_types_env computed_types_env;
- Typing.uneval_prog_generics prog;
-
- (* checking clocks compatibility with computed clocks*)
- Clock_calculus.check_env_compat header declared_clocks_env computed_clocks_env;
- Clock_calculus.uneval_prog_generics prog;
-
- (* checking stateless status compatibility *)
- Stateless.check_compat header
-
- with Sys_error _ -> (
- (* Printing lusi file is necessary *)
- Log.report ~level:1
- (fun fmt ->
- fprintf fmt
- ".. generating lustre interface file %s@," lusi_name);
- let lusi_out = open_out lusi_name in
- let lusi_fmt = formatter_of_out_channel lusi_out in
- Typing.uneval_prog_generics prog;
- Clock_calculus.uneval_prog_generics prog;
- Printers.pp_lusi_header lusi_fmt source_name prog
- )
- | (Types.Error (loc,err)) as exc ->
- eprintf "Type mismatch between computed type and declared type in lustre interface file: %a@."
- Types.pp_error err;
- raise exc
- | Clocks.Error (loc, err) as exc ->
- eprintf "Clock mismatch between computed clock and declared clock in lustre interface file: %a@."
- Clocks.pp_error err;
- raise exc
- | Stateless.Error (loc, err) as exc ->
- eprintf "Stateless status mismatch between defined status and declared status in lustre interface file: %a@."
- Stateless.pp_error err;
- raise exc
-
-let extract_interface prog =
- List.fold_right
- (fun decl header ->
- match decl.top_decl_desc with
- | Node nd -> { decl with top_decl_desc = ImportedNode (Corelang.get_node_interface nd) } :: header
- | ImportedNode _ -> header
- | Consts _
- | Type _
- | Open _ -> decl :: header)
- prog []
-
-let write_compiled_header (header : top_decl list) basename extension =
- let target_name = basename^extension in
- let outchan = open_out_bin target_name in
- begin
- Marshal.to_channel outchan header [];
- close_out outchan
- end
-
-let read_compiled_header basename extension =
- let source_name = basename^extension in
- let inchan = open_in_bin source_name in
- let header = (Marshal.from_channel inchan : top_decl list) in
- begin
- close_in inchan;
- header
- end
-
-let compile_header basename extension =
- let header_name = basename^extension in
- let header = load_lusi true header_name in
- begin
- ignore (check_lusi header);
- write_compiled_header header basename (extension^"c")
- end
-
-let compile_prog basename extension =
- ()
-
-let rec compile basename extension =
-
- (* Loading the input file *)
- let source_name = basename^extension in
- Location.input_name := source_name;
- let lexbuf = Lexing.from_channel (open_in source_name) in
- Location.init lexbuf source_name;
-
- (* Parsing *)
- Log.report ~level:1
- (fun fmt -> fprintf fmt "@[<v>.. parsing file %s@," source_name);
- let prog =
- try
- Parse.prog Parser_lustre.prog Lexer_lustre.token lexbuf
- with
- | (Lexer_lustre.Error err) | (Parse.Syntax_err err) as exc ->
- Parse.report_error err;
- raise exc
- | Corelang.Error (loc, err) as exc ->
- eprintf "Parsing error %a%a@."
- Corelang.pp_error err
- Location.pp_loc loc;
- raise exc
- in
-
- (* Extracting dependencies *)
- Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. extracting dependencies@,");
- let dependencies =
- List.fold_right
- (fun d accu -> match d.top_decl_desc with
- | Open (local, s) -> (s, local)::accu
- | _ -> accu)
- prog []
- in
- let dependencies, type_env, clock_env =
- List.fold_left (fun (compilation_dep, type_env, clock_env) (s, local) ->
- try
- let basename = (if local then s else Version.prefix ^ "/include/lustrec/" ^ s ) ^ ".lusi" in
- Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 0>Library %s@," basename);
- let comp_dep, lusi_type_env, lusi_clock_env = check_lusi (load_lusi false basename) in
- Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ ");
-
- (s, local, comp_dep)::compilation_dep,
- Env.overwrite type_env lusi_type_env,
- Env.overwrite clock_env lusi_clock_env
- with Sys_error msg -> (
- eprintf "Failure: impossible to load library %s.@.%s@." s msg;
- exit 1
- )
- ) ([], Basic_library.type_env, Basic_library.clock_env) dependencies
- in
- Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ ");
-
- (* Sorting nodes *)
- let prog = SortProg.sort prog in
-
- (* Typing *)
- let computed_types_env = type_decls type_env prog in
-
- (* Clock calculus *)
- let computed_clocks_env = clock_decls clock_env prog in
-
- (* Checking stateless/stateful status *)
- check_stateless_decls prog;
-
- (* Perform global inlining *)
- let prog =
- if !Options.global_inline &&
- (match !Options.main_node with | "" -> false | _ -> true) then
- Inliner.global_inline basename prog type_env clock_env
- else
- prog
- in
-
- (* Delay calculus *)
- (*
- if(!Options.delay_calculus)
- then
- begin
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. initialisation analysis@?");
- try
- Delay_calculus.delay_prog Basic_library.delay_env prog
- with (Delay.Error (loc,err)) as exc ->
- Location.print loc;
- eprintf "%a" Delay.pp_error err;
- Utils.track_exception ();
- raise exc
- end;
- *)
- (*
- eprintf "Causality analysis@.@?";
- (* Causality analysis *)
- begin
- try
- Causality.check_causal_prog prog
- with (Causality.Cycle v) as exc ->
- Causality.pp_error err_formatter v;
- raise exc
- end;
- *)
-
- (* Compatibility with Lusi *)
- (* Checking the existence of a lusi (Lustre Interface file) *)
- let lusi_name = basename ^ ".lusi" in
- load_n_check_lusi source_name lusi_name prog computed_types_env computed_clocks_env;
-
- (* Computes and stores generic calls for each node,
- only useful for ANSI C90 compliant generic node compilation *)
- if !Options.ansi then Causality.NodeDep.compute_generic_calls prog;
- (*Hashtbl.iter (fun id td -> match td.Corelang.top_decl_desc with Corelang.Node nd -> Format.eprintf "%s calls %a" id Causality.NodeDep.pp_generic_calls nd | _ -> ()) Corelang.node_table;*)
-
- (* Normalization phase *)
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. normalization@,");
- (* Special treatment of arrows in lustre backend. We want to keep them *)
- if !Options.output = "lustre" then
- Normalization.unfold_arrow_active := false;
- let prog = Normalization.normalize_prog prog in
- Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
-
- (* Checking array accesses *)
- if !Options.check then
- begin
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. array access checks@,");
- Access.check_prog prog;
- end;
-
- (* 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 ".. scheduling@,");
- let prog, node_schs = Scheduling.schedule_prog prog in
- Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %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:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
-
- (* Optimization of prog:
- - Unfold consts
- - eliminate trivial expressions
- *)
- let prog =
- if !Options.optimization >= 2 then
- Optimize_prog.prog_unfold_consts prog
- else
- prog
- in
-
- (* 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
-
- (* Optimize machine code *)
- let machine_code =
- if !Options.optimization >= 3 && !Options.output <> "horn" then
- begin
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization@,");
- Optimize_machine.machines_reuse_variables machine_code node_schs
- end
- else
- machine_code
- in
- let machine_code =
- if !Options.optimization >= 3 && !Options.output <> "horn" then
- begin
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization@,");
- Optimize_machine.machines_fusion machine_code
- end
- else
- machine_code
- in
- Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@,"
- (Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine)
- machine_code);
-
- (* Creating destination directory if needed *)
- if not (Sys.file_exists !Options.dest_dir) then (
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. creating destination directory@,");
- Unix.mkdir !Options.dest_dir (Unix.stat ".").Unix.st_perm
- );
- if (Unix.stat !Options.dest_dir).Unix.st_kind <> Unix.S_DIR then (
- eprintf "Failure: destination %s is not a directory.@.@." !Options.dest_dir;
- exit 1
- );
- (* Printing code *)
- let basename = Filename.basename basename in
- let destname = !Options.dest_dir ^ "/" ^ basename in
- let _ = match !Options.output with
- "C" ->
- begin
- let header_file = destname ^ ".h" in (* Could be changed *)
- let source_lib_file = destname ^ ".c" in (* Could be changed *)
- let source_main_file = destname ^ "_main.c" in (* Could be changed *)
- let makefile_file = destname ^ ".makefile" in (* Could be changed *)
- (* let spec_file_opt = if !Options.c_spec then *)
- (* ( *)
- (* let spec_file = basename ^ "_spec.c" in *)
- (* Log.report ~level:1 (fun fmt -> fprintf fmt ".. opening files %s, %s and %s@," header_file source_file spec_file); *)
- (* Some spec_file *)
- (* ) else ( *)
- (* Log.report ~level:1 (fun fmt -> fprintf fmt ".. opening files %s and %s@," header_file source_file); *)
- (* None *)
- (* ) *)
- (* in *)
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,");
- C_backend.translate_to_c
- header_file source_lib_file source_main_file makefile_file
- basename prog machine_code dependencies
- end
- | "java" ->
- begin
- failwith "Sorry, but not yet supported !"
- (*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 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
- Horn_backend.translate fmt basename prog machine_code;
- (* Tracability file if option is activated *)
- if !Options.horntraces then (
- let traces_file = destname ^ ".traces" in (* Could be changed *)
- let traces_out = open_out traces_file in
- let fmt = formatter_of_out_channel traces_out in
- Horn_backend.traces_file fmt basename prog machine_code
- )
- end
- | "lustre" ->
- begin
- 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;
-(* Lustre_backend.translate fmt basename normalized_prog machine_code *)
- ()
- end
-
- | _ -> assert false
- in
- begin
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.");
- (* We stop the process here *)
- exit 0
- end
-
-let anonymous filename =
- let ok_ext, ext = List.fold_left (fun (ok, ext) ext' -> if not ok && Filename.check_suffix filename ext' then true, ext' else ok, ext) (false, "") extensions in
- if ok_ext then
- let basename = Filename.chop_suffix filename ext in
- compile basename ext
- else
- raise (Arg.Bad ("Can only compile *.lusi, *.lus or *.ec files"))
-
-let _ =
- Corelang.add_internal_funs ();
- try
- Printexc.record_backtrace true;
- Arg.parse Options.options anonymous usage
- with
- | Parse.Syntax_err _ | Lexer_lustre.Error _
- | Types.Error (_,_) | Clocks.Error (_,_)
- | Corelang.Error _ (*| Task_set.Error _*)
- | Causality.Cycle _ -> exit 1
- | exc -> (Utils.track_exception (); raise exc)
-
-(* Local Variables: *)
-(* compile-command:"make -C .." *)
-(* End: *)
+(********************************************************************)
+(* *)
+(* The LustreC compiler toolset / The LustreC Development Team *)
+(* Copyright 2012 - -- ONERA - CNRS - INPT *)
+(* *)
+(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)
+(* under the terms of the GNU Lesser General Public License *)
+(* version 2.1. *)
+(* *)
+(********************************************************************)
+
+open Format
+open Log
+
+open LustreSpec
+open Compiler_common
+
+let usage = "Usage: lustrec [options] <source-file>"
+
+let extensions = [".ec"; ".lus"; ".lusi"]
+
+(* print a .lusi header file from a source prog *)
+let print_lusi prog basename extension =
+ let header = Lusic.extract_header basename prog in
+ let header_name = basename ^ extension in
+ let h_out = open_out header_name in
+ let h_fmt = formatter_of_out_channel h_out in
+ begin
+ Printers.pp_lusi_header h_fmt basename header;
+ close_out h_out
+ end
+
+(* compile a .lusi header file *)
+let compile_header basename extension =
+ let header_name = basename ^ extension in
+ let lusic_ext = extension ^ "c" in
+ begin
+ Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v>");
+ let header = parse_header true header_name in
+ ignore (check_top_decls header);
+ create_dest_dir ();
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %sc@," header_name);
+ Lusic.write_lusic true header basename lusic_ext;
+ Lusic.print_lusic_to_h basename lusic_ext;
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.")
+ end
+
+(* check whether a source file has a compiled header,
+ if not, generate the compiled header *)
+let compile_source_to_header prog computed_types_env computed_clocks_env basename extension =
+ let basename' = !Options.dest_dir ^ "/" ^ basename in
+ let lusic_ext = extension ^ "c" in
+ let header_name = basename' ^ lusic_ext in
+ begin
+ if not (Sys.file_exists header_name) then
+ begin
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name);
+ Lusic.write_lusic false (Lusic.extract_header basename prog) basename lusic_ext;
+ Lusic.print_lusic_to_h basename lusic_ext
+ end
+ else
+ let lusic = Lusic.read_lusic basename lusic_ext in
+ if not lusic.Lusic.from_lusi then
+ begin
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name);
+ Lusic.write_lusic false (Lusic.extract_header basename prog) basename lusic_ext;
+(*List.iter (fun top_decl -> Format.eprintf "lusic: %a@." Printers.pp_decl top_decl) lusic.Lusic.contents;*)
+ Lusic.print_lusic_to_h basename lusic_ext
+ end
+ else
+ begin
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. loading compiled header file %s@," header_name);
+ let header = lusic.Lusic.contents in
+ let (declared_types_env, declared_clocks_env) = get_envs_from_top_decls header in
+ check_compatibility
+ (prog, computed_types_env, computed_clocks_env)
+ (header, declared_types_env, declared_clocks_env)
+ end
+ end
+
+(* compile a .lus source file *)
+let rec compile_source basename extension =
+ let source_name = basename ^ extension in
+
+ Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v>");
+
+ let prog = parse_source source_name in
+
+ (* Extracting dependencies *)
+ let dependencies, type_env, clock_env = import_dependencies prog in
+
+ (* Sorting nodes *)
+ let prog = SortProg.sort prog in
+
+ (* Typing *)
+ let computed_types_env = type_decls type_env prog in
+
+ (* Clock calculus *)
+ let computed_clocks_env = clock_decls clock_env prog in
+
+ (* Checking stateless/stateful status *)
+ check_stateless_decls prog;
+
+ (* Generating a .lusi header file only *)
+ if !Options.lusi then
+ begin
+ let lusi_ext = extension ^ "i" in
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating interface file %s@," (basename ^ lusi_ext));
+ print_lusi prog basename lusi_ext;
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.");
+ exit 0
+ end;
+
+ (* Perform global inlining *)
+ let prog =
+ if !Options.global_inline &&
+ (match !Options.main_node with | "" -> false | _ -> true) then
+ Inliner.global_inline basename prog type_env clock_env
+ else
+ prog
+ in
+
+ (* Delay calculus *)
+ (*
+ if(!Options.delay_calculus)
+ then
+ begin
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. initialisation analysis@?");
+ try
+ Delay_calculus.delay_prog Basic_library.delay_env prog
+ with (Delay.Error (loc,err)) as exc ->
+ Location.print loc;
+ eprintf "%a" Delay.pp_error err;
+ Utils.track_exception ();
+ raise exc
+ end;
+ *)
+ (*
+ eprintf "Causality analysis@.@?";
+ (* Causality analysis *)
+ begin
+ try
+ Causality.check_causal_prog prog
+ with (Causality.Cycle v) as exc ->
+ Causality.pp_error err_formatter v;
+ raise exc
+ end;
+ *)
+
+ (* Creating destination directory if needed *)
+ create_dest_dir ();
+
+ (* Compatibility with Lusi *)
+ (* Checking the existence of a lusi (Lustre Interface file) *)
+ let extension = ".lusi" in
+ compile_source_to_header prog computed_types_env computed_clocks_env basename extension;
+
+ Typing.uneval_prog_generics prog;
+ Clock_calculus.uneval_prog_generics prog;
+
+ (* Computes and stores generic calls for each node,
+ only useful for ANSI C90 compliant generic node compilation *)
+ if !Options.ansi then Causality.NodeDep.compute_generic_calls prog;
+ (*Hashtbl.iter (fun id td -> match td.Corelang.top_decl_desc with Corelang.Node nd -> Format.eprintf "%s calls %a" id Causality.NodeDep.pp_generic_calls nd | _ -> ()) Corelang.node_table;*)
+
+ (* Normalization phase *)
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. normalization@,");
+ (* Special treatment of arrows in lustre backend. We want to keep them *)
+ if !Options.output = "lustre" then
+ Normalization.unfold_arrow_active := false;
+ let prog = Normalization.normalize_prog prog in
+ Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
+
+ (* Checking array accesses *)
+ if !Options.check then
+ begin
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. array access checks@,");
+ Access.check_prog prog;
+ end;
+
+ (* 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 ".. scheduling@,");
+ let prog, node_schs = Scheduling.schedule_prog prog in
+ Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %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:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
+
+ (* Optimization of prog:
+ - Unfold consts
+ - eliminate trivial expressions
+ *)
+ let prog =
+ if !Options.optimization >= 2 then
+ Optimize_prog.prog_unfold_consts prog
+ else
+ prog
+ in
+
+ (* 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
+
+ (* Optimize machine code *)
+ let machine_code =
+ if !Options.optimization >= 3 && !Options.output <> "horn" then
+ begin
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization@,");
+ Optimize_machine.machines_reuse_variables machine_code node_schs
+ end
+ else
+ machine_code
+ in
+ let machine_code =
+ if !Options.optimization >= 3 && !Options.output <> "horn" then
+ begin
+ Optimize_machine.machines_fusion machine_code
+ end
+ else
+ machine_code
+ in
+ Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@,"
+ (Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine)
+ machine_code);
+
+ (* Printing code *)
+ let basename = Filename.basename basename in
+ let destname = !Options.dest_dir ^ "/" ^ basename in
+ let _ = match !Options.output with
+ "C" ->
+ begin
+ let alloc_header_file = destname ^ "_alloc.h" in (* Could be changed *)
+ let source_lib_file = destname ^ ".c" in (* Could be changed *)
+ let source_main_file = destname ^ "_main.c" in (* Could be changed *)
+ let makefile_file = destname ^ ".makefile" in (* Could be changed *)
+ 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
+ failwith "Sorry, but not yet supported !"
+ (*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 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
+ Horn_backend.translate fmt basename prog machine_code;
+ (* Tracability file if option is activated *)
+ if !Options.horntraces then (
+ let traces_file = destname ^ ".traces" in (* Could be changed *)
+ let traces_out = open_out traces_file in
+ let fmt = formatter_of_out_channel traces_out in
+ Horn_backend.traces_file fmt basename prog machine_code
+ )
+ end
+ | "lustre" ->
+ begin
+ 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;
+(* Lustre_backend.translate fmt basename normalized_prog machine_code *)
+ ()
+ end
+
+ | _ -> assert false
+ in
+ begin
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.");
+ (* We stop the process here *)
+ exit 0
+ end
+
+let compile basename extension =
+ match extension with
+ | ".lusi" -> compile_header basename extension
+ | ".lus" -> compile_source basename extension
+ | _ -> assert false
+
+let anonymous filename =
+ let ok_ext, ext = List.fold_left (fun (ok, ext) ext' -> if not ok && Filename.check_suffix filename ext' then true, ext' else ok, ext) (false, "") extensions in
+ if ok_ext then
+ let basename = Filename.chop_suffix filename ext in
+ compile basename ext
+ else
+ raise (Arg.Bad ("Can only compile *.lusi, *.lus or *.ec files"))
+
+let _ =
+ Corelang.add_internal_funs ();
+ try
+ Printexc.record_backtrace true;
+ Arg.parse Options.options anonymous usage
+ with
+ | Parse.Syntax_err _ | Lexer_lustre.Error _
+ | Types.Error (_,_) | Clocks.Error (_,_)
+ | Corelang.Error _ (*| Task_set.Error _*)
+ | Causality.Cycle _ -> exit 1
+ | Sys_error msg -> (eprintf "Failure: %s@." msg)
+ | exc -> (Utils.track_exception (); raise exc)
+
+(* Local Variables: *)
+(* compile-command:"make -C .." *)
+(* End: *)
diff --git a/src/modules.ml b/src/modules.ml
new file mode 100644
index 0000000000000000000000000000000000000000..7bfbc61db1e0dbb8ec06de9bf20f7375545d1d9a
--- /dev/null
+++ b/src/modules.ml
@@ -0,0 +1,159 @@
+(********************************************************************)
+(* *)
+(* The LustreC compiler toolset / The LustreC Development Team *)
+(* Copyright 2012 - -- ONERA - CNRS - INPT *)
+(* *)
+(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)
+(* under the terms of the GNU Lesser General Public License *)
+(* version 2.1. *)
+(* *)
+(********************************************************************)
+
+open Utils
+open LustreSpec
+open Corelang
+
+let add_symbol loc msg hashtbl name value =
+ if Hashtbl.mem hashtbl name
+ then raise (Error (loc, Already_bound_symbol msg))
+ else Hashtbl.add hashtbl name value
+
+let check_symbol loc msg hashtbl name =
+ if not (Hashtbl.mem hashtbl name)
+ then raise (Error (loc, Unbound_symbol msg))
+ else ()
+
+let add_imported_node name value =
+(*Format.eprintf "add_imported_node %s %a (owner=%s)@." name Printers.pp_imported_node (imported_node_of_top value) value.top_decl_owner;*)
+ try
+ let value' = Hashtbl.find node_table name in
+ let owner' = value'.top_decl_owner in
+ let itf' = value'.top_decl_itf in
+ let owner = value.top_decl_owner in
+ let itf = value.top_decl_itf in
+ match value'.top_decl_desc, value.top_decl_desc with
+ | Node _ , ImportedNode _ when owner = owner' && itf' && (not itf) -> Hashtbl.add node_table name value
+ | ImportedNode _, ImportedNode _ -> raise (Error (value.top_decl_loc, Already_bound_symbol ("node " ^ name)))
+ | _ -> assert false
+ with
+ Not_found -> Hashtbl.add node_table name value
+
+let add_node name value =
+(*Format.eprintf "add_node %s %a (owner=%s)@." name Printers.pp_imported_node (get_node_interface (node_of_top value)) value.top_decl_owner;*)
+ try
+ let value' = Hashtbl.find node_table name in
+ let owner' = value'.top_decl_owner in
+ let itf' = value'.top_decl_itf in
+ let owner = value.top_decl_owner in
+ let itf = value.top_decl_itf in
+ match value'.top_decl_desc, value.top_decl_desc with
+ | ImportedNode _, Node _ when owner = owner' && itf' && (not itf) -> ()
+ | Node _ , Node _ -> raise (Error (value.top_decl_loc, Already_bound_symbol ("node " ^ name)))
+ | _ -> assert false
+ with
+ Not_found -> Hashtbl.add node_table name value
+
+
+let add_tag loc name typ =
+ if Hashtbl.mem tag_table name then
+ raise (Error (loc, Already_bound_symbol ("enum tag " ^ name)))
+ else Hashtbl.add tag_table name typ
+
+let add_field loc name typ =
+ if Hashtbl.mem field_table name then
+ raise (Error (loc, Already_bound_symbol ("struct field " ^ name)))
+ else Hashtbl.add field_table name typ
+
+let import_typedef name tydef =
+ let loc = tydef.top_decl_loc in
+ let rec import ty =
+ match ty with
+ | Tydec_enum tl ->
+ List.iter (fun tag -> add_tag loc tag tydef) tl
+ | Tydec_struct fl ->
+ List.iter (fun (field, ty) -> add_field loc field tydef; import ty) fl
+ | Tydec_clock ty -> import ty
+ | Tydec_const c ->
+ if not (Hashtbl.mem type_table (Tydec_const c))
+ then raise (Error (loc, Unbound_symbol ("type " ^ c)))
+ else ()
+ | Tydec_array (c, ty) -> import ty
+ | _ -> ()
+ in import ((typedef_of_top tydef).tydef_desc)
+
+let add_type itf name value =
+(*Format.eprintf "add_type %B %s %a (owner=%s)@." itf name Printers.pp_typedef (typedef_of_top value) value.top_decl_owner;*)
+ try
+ let value' = Hashtbl.find type_table (Tydec_const name) in
+ let owner' = value'.top_decl_owner in
+ let itf' = value'.top_decl_itf in
+ let owner = value.top_decl_owner in
+ let itf = value.top_decl_itf in
+ match value'.top_decl_desc, value.top_decl_desc with
+ | TypeDef ty', TypeDef ty when coretype_equal ty'.tydef_desc ty.tydef_desc && owner' = owner && itf' && (not itf) -> ()
+ | TypeDef ty', TypeDef ty -> raise (Error (value.top_decl_loc, Already_bound_symbol ("type " ^ name)))
+ | _ -> assert false
+ with Not_found -> (import_typedef name value; Hashtbl.add type_table (Tydec_const name) value)
+
+let check_type loc name =
+ if not (Hashtbl.mem type_table (Tydec_const name))
+ then raise (Error (loc, Unbound_symbol ("type " ^ name)))
+ else ()
+
+let add_const itf name value =
+ try
+ let value' = Hashtbl.find consts_table name in
+ let owner' = value'.top_decl_owner in
+ let itf' = value'.top_decl_itf in
+ let owner = value.top_decl_owner in
+ let itf = value.top_decl_itf in
+ match value'.top_decl_desc, value.top_decl_desc with
+ | Const c', Const c when c.const_value = c'.const_value && owner' = owner && itf' && (not itf) -> ()
+ | Const c', Const c -> raise (Error (value.top_decl_loc, Already_bound_symbol ("const " ^ name)))
+ | _ -> assert false
+ with Not_found -> Hashtbl.add consts_table name value
+
+let name_dependency (local, dep) =
+ (if local then "" else Version.prefix ^ "/include/lustrec/") ^ dep
+
+let import_dependency loc (local, dep) =
+ let basename = name_dependency (local, dep) in
+ let extension = ".lusic" in
+ try
+ Lusic.read_lusic basename extension
+ with Sys_error msg ->
+ raise (Error (loc, Unknown_library basename))
+(*
+ begin
+ Format.eprintf "Failure: impossible to load library %s.@.%s@." basename msg;
+ exit 1
+ end
+*)
+
+let rec load_header imported header =
+ List.fold_left (fun imp decl ->
+ match decl.top_decl_desc with
+ | Node nd -> assert false
+ | ImportedNode ind -> (add_imported_node ind.nodei_id decl; imp)
+ | Const c -> (add_const true c.const_id decl; imp)
+ | TypeDef tdef -> (add_type true tdef.tydef_id decl; imp)
+ | Open (local, dep) ->
+ let basename = name_dependency (local, dep) in
+ if ISet.mem basename imported then imp else
+ let lusic = import_dependency decl.top_decl_loc (local, dep)
+ in load_header (ISet.add basename imported) lusic.Lusic.contents
+ ) imported header
+
+let rec load_program imported program =
+ List.fold_left (fun imp decl ->
+ match decl.top_decl_desc with
+ | Node nd -> (add_node nd.node_id decl; imp)
+ | ImportedNode ind -> assert false
+ | Const c -> (add_const false c.const_id decl; imp)
+ | TypeDef tdef -> (add_type false tdef.tydef_id decl; imp)
+ | Open (local, dep) ->
+ let basename = name_dependency (local, dep) in
+ if ISet.mem basename imported then imp else
+ let lusic = import_dependency decl.top_decl_loc (local, dep)
+ in load_header (ISet.add basename imported) lusic.Lusic.contents
+ ) imported program
diff --git a/src/normalization.ml b/src/normalization.ml
index 4d189e3271b04bcadb45cbf1ed3a16aa43885f21..5aafac4da12a380b00de7d1d5da5c865aff70d06 100644
--- a/src/normalization.ml
+++ b/src/normalization.ml
@@ -401,7 +401,7 @@ let normalize_decl decl =
match decl.top_decl_desc with
| Node nd ->
{decl with top_decl_desc = Node (normalize_node nd)}
- | Open _ | ImportedNode _ | Consts _ | Type _ -> decl
+ | Open _ | ImportedNode _ | Const _ | TypeDef _ -> decl
let normalize_prog decls =
List.map normalize_decl decls
diff --git a/src/optimize_prog.ml b/src/optimize_prog.ml
index b658953e242a97d97cae851e973802a149fa497e..3ee977109ce125d35ee01e3cb491e8fd827e7308 100644
--- a/src/optimize_prog.ml
+++ b/src/optimize_prog.ml
@@ -49,7 +49,7 @@ let node_unfold_consts consts node =
{ node with node_eqs = List.map (eq_unfold_consts consts) node.node_eqs }
let prog_unfold_consts prog =
- let consts = get_consts prog in
+ let consts = List.map const_of_top (get_consts prog) in
List.map (
fun decl -> match decl.top_decl_desc with
| Node nd -> {decl with top_decl_desc = Node (node_unfold_consts consts nd)}
diff --git a/src/parse.ml b/src/parse.ml
index 23b38c554dc7a27796e2d86fcc8251f211fee0c4..0bd7e961720a77974906bca2d534e7a57f9dc659 100755
--- a/src/parse.ml
+++ b/src/parse.ml
@@ -15,89 +15,13 @@ open Format
open LustreSpec
open Corelang
-let add_symbol loc msg hashtbl name value =
- if Hashtbl.mem hashtbl name
- then raise (Error (loc, Already_bound_symbol msg))
- else Hashtbl.add hashtbl name value
-
-let check_symbol loc msg hashtbl name =
- if not (Hashtbl.mem hashtbl name)
- then raise (Error (loc, Unbound_symbol msg))
- else ()
-
-let add_node own name value =
- try
- match (Hashtbl.find node_table name).top_decl_desc, value.top_decl_desc with
- | Node _ , ImportedNode _ when own -> ()
- | ImportedNode _, _ -> Hashtbl.add node_table name value
- | Node _ , _ -> raise (Error (value.top_decl_loc, Already_bound_symbol ("node " ^ name)))
- | _ -> assert false
- with
- Not_found -> Hashtbl.add node_table name value
-
-
-let add_tag loc own name typ =
- if Hashtbl.mem tag_table name && (not own) then
- raise (Error (loc, Unbound_symbol ("enum tag " ^ name)))
- else Hashtbl.add tag_table name typ
-
-let add_field loc own name typ =
- if Hashtbl.mem field_table name && (not own) then
- raise (Error (loc, Unbound_symbol ("struct field " ^ name)))
- else Hashtbl.add field_table name typ
-
-let rec check_type_def loc own name ty =
- match ty with
- | Tydec_enum tl ->
- begin
- List.iter (fun tag -> add_tag loc own tag (Tydec_const name)) tl;
- ty
- end
- | Tydec_struct fl ->
- begin
- List.iter (fun (field, _) -> add_field loc own field (Tydec_const name)) fl;
- Tydec_struct (List.map (fun (f, ty) -> (f, check_type_def loc own name ty)) fl)
- end
- | Tydec_clock ty -> Tydec_clock (check_type_def loc own name ty)
- | Tydec_const c ->
- if not (Hashtbl.mem type_table (Tydec_const c))
- then raise (Error (loc, Unbound_symbol ("type " ^ c)))
- else get_repr_type ty
- | Tydec_array (c, ty) -> Tydec_array (c, check_type_def loc own name ty)
- | _ -> ty
-
-let add_type own name value =
-(*Format.eprintf "add_type %B %s@." own name;*)
- match value.top_decl_desc with
- | Type ty ->
- let loc = value.top_decl_loc in
- if Hashtbl.mem type_table (Tydec_const name) && (not own)
- then raise (Error (loc, Already_bound_symbol ("type " ^ name)))
- else Hashtbl.add type_table (Tydec_const name) (check_type_def loc own name ty.ty_def_desc)
- | _ -> assert false
-
-let check_type loc name =
- if not (Hashtbl.mem type_table (Tydec_const name))
- then raise (Error (loc, Unbound_symbol ("type " ^ name)))
- else ()
-
let report_error loc =
Location.print loc;
print_string "Syntax error\n"
-(*
-let wrap own parsing_fun token_fun lexbuf =
- try
- let ast = parsing_fun token_fun lexbuf own in
- Parsing.clear_parser ();
- ast
- with
- | Parsing.Parse_error ->
- let loc = Location.curr lexbuf in
- raise (Syntax_err loc)
- *)
-let header own parsing_fun token_fun lexbuf =
+
+let header parsing_fun token_fun lexbuf =
try
- let ast = parsing_fun token_fun lexbuf own in
+ let ast = parsing_fun token_fun lexbuf in
Parsing.clear_parser ();
ast
with
diff --git a/src/parser_lustre.mly b/src/parser_lustre.mly
index 3ec06fe423ecbd26455aacc79f917a382b91f48e..fd9f83b7f6d6d395a659b0e0fd8e1ced99d4253a 100755
--- a/src/parser_lustre.mly
+++ b/src/parser_lustre.mly
@@ -1,564 +1,595 @@
-/********************************************************************/
-/* */
-/* The LustreC compiler toolset / The LustreC Development Team */
-/* Copyright 2012 - -- ONERA - CNRS - INPT */
-/* */
-/* LustreC is free software, distributed WITHOUT ANY WARRANTY */
-/* under the terms of the GNU Lesser General Public License */
-/* version 2.1. */
-/* */
-/********************************************************************/
-
-%{
-open Utils
-open LustreSpec
-open Corelang
-open Dimension
-open Parse
-
-let get_loc () = Location.symbol_rloc ()
-let mktyp x = mktyp (get_loc ()) x
-let mkclock x = mkclock (get_loc ()) x
-let mkvar_decl x = mkvar_decl (get_loc ()) x
-let mkexpr x = mkexpr (get_loc ()) x
-let mkeexpr x = mkeexpr (get_loc ()) x
-let mkeq x = mkeq (get_loc ()) x
-let mkassert x = mkassert (get_loc ()) x
-let mktop_decl x = mktop_decl (get_loc ()) x
-let mkpredef_call x = mkpredef_call (get_loc ()) x
-(*let mkpredef_unary_call x = mkpredef_unary_call (get_loc ()) x*)
-
-let mkdim_int i = mkdim_int (get_loc ()) i
-let mkdim_bool b = mkdim_bool (get_loc ()) b
-let mkdim_ident id = mkdim_ident (get_loc ()) id
-let mkdim_appl f args = mkdim_appl (get_loc ()) f args
-let mkdim_ite i t e = mkdim_ite (get_loc ()) i t e
-
-let mkannots annots = { annots = annots; annot_loc = get_loc () }
-
-%}
-
-%token <int> INT
-%token <string> REAL
-%token <float> FLOAT
-%token <string> STRING
-%token AUTOMATON STATE UNTIL UNLESS RESTART RESUME LAST
-%token STATELESS ASSERT OPEN QUOTE FUNCTION
-%token <string> IDENT
-%token <LustreSpec.expr_annot> ANNOT
-%token <LustreSpec.node_annot> NODESPEC
-%token LBRACKET RBRACKET LCUR RCUR LPAR RPAR SCOL COL COMMA COLCOL
-%token AMPERAMPER BARBAR NOT POWER
-%token IF THEN ELSE
-%token UCLOCK DCLOCK PHCLOCK TAIL
-%token MERGE FBY WHEN WHENNOT EVERY
-%token NODE LET TEL RETURNS VAR IMPORTED SENSOR ACTUATOR WCET TYPE CONST
-%token STRUCT ENUM
-%token TINT TFLOAT TREAL TBOOL TCLOCK
-%token RATE DUE
-%token EQ LT GT LTE GTE NEQ
-%token AND OR XOR IMPL
-%token MULT DIV MOD
-%token MINUS PLUS UMINUS
-%token PRE ARROW
-%token REQUIRES ENSURES OBSERVER
-%token INVARIANT BEHAVIOR ASSUMES
-%token EXISTS FORALL
-%token PROTOTYPE LIB
-%token EOF
-
-%nonassoc prec_exists prec_forall
-%nonassoc COMMA
-%left MERGE IF
-%nonassoc ELSE
-%right ARROW FBY
-%left WHEN WHENNOT UCLOCK DCLOCK PHCLOCK
-%right COLCOL
-%right IMPL
-%left OR XOR BARBAR
-%left AND AMPERAMPER
-%left NOT
-%nonassoc INT
-%nonassoc EQ LT GT LTE GTE NEQ
-%left MINUS PLUS
-%left MULT DIV MOD
-%left UMINUS
-%left POWER
-%left PRE LAST
-%nonassoc RBRACKET
-%nonassoc LBRACKET
-
-%start prog
-%type <LustreSpec.top_decl list> prog
-
-%start header
-%type <bool -> LustreSpec.top_decl list> header
-
-%start lustre_annot
-%type <LustreSpec.expr_annot> lustre_annot
-
-%start lustre_spec
-%type <LustreSpec.node_annot> lustre_spec
-
-%%
-
-prog:
- open_list typ_def_prog top_decl_list EOF { $1 @ $2 @ (List.rev $3) }
-
-typ_def_prog:
- typ_def_list { $1 true }
-
-header:
- open_list typ_def_list top_decl_header_list EOF { (fun own -> ($1 @ let typs = $2 own in typs @ (List.rev ($3 own)))) }
-
-open_list:
- { [] }
-| open_lusi open_list { $1 :: $2 }
-
-open_lusi:
-| OPEN QUOTE IDENT QUOTE { mktop_decl (Open (true, $3))}
-| OPEN LT IDENT GT { mktop_decl (Open (false, $3)) }
-
-top_decl_list:
- {[]}
-| top_decl_list top_decl {$2::$1}
-
-
-top_decl_header_list:
- {(fun own -> []) }
-| top_decl_header_list top_decl_header {(fun own -> let h1 = $1 own in ($2 own)::h1) }
-
-state_annot:
- FUNCTION { true }
-| NODE { false }
-
-top_decl_header:
-| CONST cdecl_list { let top = mktop_decl (Consts (List.rev $2)) in fun _ -> top }
-| nodespec_list state_annot IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR prototype_opt in_lib_opt SCOL
- {let nd = mktop_decl (ImportedNode
- {nodei_id = $3;
- nodei_type = Types.new_var ();
- nodei_clock = Clocks.new_var true;
- nodei_inputs = List.rev $5;
- nodei_outputs = List.rev $10;
- nodei_stateless = $2;
- nodei_spec = $1;
- nodei_prototype = $13;
- nodei_in_lib = $14;})
- in
- (fun own -> add_node own $3 nd; nd) }
-
-prototype_opt:
- { None }
-| PROTOTYPE IDENT { Some $2}
-
-in_lib_opt:
-{ None }
-| LIB IDENT {Some $2}
-
-top_decl:
-| CONST cdecl_list { mktop_decl (Consts (List.rev $2)) }
-| nodespec_list state_annot IDENT LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt locals LET eq_list TEL
- {let eqs, asserts, annots = $16 in
- let nd = mktop_decl (Node
- {node_id = $3;
- node_type = Types.new_var ();
- node_clock = Clocks.new_var true;
- node_inputs = List.rev $5;
- node_outputs = List.rev $10;
- node_locals = List.rev $14;
- node_gencalls = [];
- node_checks = [];
- node_asserts = asserts;
- node_eqs = eqs;
- node_dec_stateless = $2;
- node_stateless = None;
- node_spec = $1;
- node_annot = annots})
- in
- add_node true $3 nd; nd}
-
-nodespec_list:
- { None }
-| NODESPEC nodespec_list {
- (function
- | None -> (fun s1 -> Some s1)
- | Some s2 -> (fun s1 -> Some (merge_node_annot s1 s2))) $2 $1 }
-
-typ_def_list:
- /* empty */ { (fun own -> []) }
-| typ_def SCOL typ_def_list { (fun own -> let ty1 = ($1 own) in ty1 :: ($3 own)) }
-
-typ_def:
- TYPE IDENT EQ typ_def_rhs { let typ = mktop_decl (Type { ty_def_id = $2;
- ty_def_desc = $4
- })
- in (fun own -> add_type own $2 typ; typ) }
-
-typ_def_rhs:
- typeconst { $1 }
-| ENUM LCUR tag_list RCUR { Tydec_enum (List.rev $3) }
-| STRUCT LCUR field_list RCUR { Tydec_struct (List.rev $3) }
-
-array_typ_decl:
- { fun typ -> typ }
- | POWER dim array_typ_decl { fun typ -> $3 (Tydec_array ($2, typ)) }
-
-typeconst:
- TINT array_typ_decl { $2 Tydec_int }
-| TBOOL array_typ_decl { $2 Tydec_bool }
-| TREAL array_typ_decl { $2 Tydec_real }
-| TFLOAT array_typ_decl { $2 Tydec_float }
-| IDENT array_typ_decl { $2 (Tydec_const $1) }
-| TBOOL TCLOCK { Tydec_clock Tydec_bool }
-| IDENT TCLOCK { Tydec_clock (Tydec_const $1) }
-
-tag_list:
- IDENT { $1 :: [] }
-| tag_list COMMA IDENT { $3 :: $1 }
-
-field_list: { [] }
-| field_list IDENT COL typeconst SCOL { ($2, $4) :: $1 }
-
-eq_list:
- { [], [], [] }
-| eq eq_list {let eql, assertl, annotl = $2 in ($1::eql), assertl, annotl}
-| assert_ eq_list {let eql, assertl, annotl = $2 in eql, ($1::assertl), annotl}
-| ANNOT eq_list {let eql, assertl, annotl = $2 in eql, assertl, $1::annotl}
-| automaton eq_list {let eql, assertl, annotl = $2 in ($1::eql), assertl, annotl}
-
-automaton:
- AUTOMATON IDENT handler_list { failwith "not implemented" }
-
-handler_list:
- { [] }
-| handler handler_list { $1::$2 }
-
-handler:
- STATE IDENT ARROW unless_list locals LET eq_list TEL until_list { () }
-
-unless_list:
- { [] }
-| unless unless_list { $1::$2 }
-
-until_list:
- { [] }
-| until until_list { $1::$2 }
-
-unless:
- UNLESS expr RESTART IDENT { }
-| UNLESS expr RESUME IDENT { }
-
-until:
- UNTIL expr RESTART IDENT { }
-| UNTIL expr RESUME IDENT { }
-
-assert_:
-| ASSERT expr SCOL {mkassert ($2)}
-
-eq:
- ident_list EQ expr SCOL {mkeq (List.rev $1,$3)}
-| LPAR ident_list RPAR EQ expr SCOL {mkeq (List.rev $2,$5)}
-
-lustre_spec:
-| contract EOF { $1 }
-
-contract:
-requires ensures behaviors { { requires = $1; ensures = $2; behaviors = $3; spec_loc = get_loc () } }
-
-requires:
-{ [] }
-| REQUIRES qexpr SCOL requires { $2::$4 }
-
-ensures:
-{ [] }
-| ENSURES qexpr SCOL ensures { $2 :: $4 }
-| OBSERVER IDENT LPAR tuple_expr RPAR SCOL ensures {
- mkeexpr (mkexpr ((Expr_appl ($2, mkexpr (Expr_tuple $4), None)))) :: $7
-}
-
-behaviors:
-{ [] }
-| BEHAVIOR IDENT COL assumes ensures behaviors { ($2,$4,$5,get_loc ())::$6 }
-
-assumes:
-{ [] }
-| ASSUMES qexpr SCOL assumes { $2::$4 }
-
-/* WARNING: UNUSED RULES */
-tuple_qexpr:
-| qexpr COMMA qexpr {[$3;$1]}
-| tuple_qexpr COMMA qexpr {$3::$1}
-
-qexpr:
-| expr { mkeexpr $1 }
- /* Quantifiers */
-| EXISTS vdecl SCOL qexpr %prec prec_exists { extend_eexpr [Exists, $2] $4 }
-| FORALL vdecl SCOL qexpr %prec prec_forall { extend_eexpr [Forall, $2] $4 }
-
-
-tuple_expr:
- expr COMMA expr {[$3;$1]}
-| tuple_expr COMMA expr {$3::$1}
-
-// Same as tuple expr but accepting lists with single element
-array_expr:
- expr {[$1]}
-| expr COMMA array_expr {$1::$3}
-
-dim_list:
- dim RBRACKET { fun base -> mkexpr (Expr_access (base, $1)) }
-| dim RBRACKET LBRACKET dim_list { fun base -> $4 (mkexpr (Expr_access (base, $1))) }
-
-expr:
-/* constants */
- INT {mkexpr (Expr_const (Const_int $1))}
-| REAL {mkexpr (Expr_const (Const_real $1))}
-| FLOAT {mkexpr (Expr_const (Const_float $1))}
-/* Idents or type enum tags */
-| IDENT {
- if Hashtbl.mem tag_table $1
- then mkexpr (Expr_const (Const_tag $1))
- else mkexpr (Expr_ident $1)}
-| LPAR ANNOT expr RPAR
- {update_expr_annot $3 $2}
-| LPAR expr RPAR
- {$2}
-| LPAR tuple_expr RPAR
- {mkexpr (Expr_tuple (List.rev $2))}
-
-/* Array expressions */
-| LBRACKET array_expr RBRACKET { mkexpr (Expr_array $2) }
-| expr POWER dim { mkexpr (Expr_power ($1, $3)) }
-| expr LBRACKET dim_list { $3 $1 }
-
-/* Temporal operators */
-| PRE expr
- {mkexpr (Expr_pre $2)}
-| expr ARROW expr
- {mkexpr (Expr_arrow ($1,$3))}
-| expr FBY expr
- {(*mkexpr (Expr_fby ($1,$3))*)
- mkexpr (Expr_arrow ($1, mkexpr (Expr_pre $3)))}
-| expr WHEN IDENT
- {mkexpr (Expr_when ($1,$3,tag_true))}
-| expr WHENNOT IDENT
- {mkexpr (Expr_when ($1,$3,tag_false))}
-| expr WHEN IDENT LPAR IDENT RPAR
- {mkexpr (Expr_when ($1, $5, $3))}
-| MERGE IDENT handler_expr_list
- {mkexpr (Expr_merge ($2,$3))}
-
-/* Applications */
-| IDENT LPAR expr RPAR
- {mkexpr (Expr_appl ($1, $3, None))}
-| IDENT LPAR expr RPAR EVERY IDENT
- {mkexpr (Expr_appl ($1, $3, Some ($6, tag_true)))}
-| IDENT LPAR expr RPAR EVERY IDENT LPAR IDENT RPAR
- {mkexpr (Expr_appl ($1, $3, Some ($8, $6))) }
-| IDENT LPAR tuple_expr RPAR
- {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), None))}
-| IDENT LPAR tuple_expr RPAR EVERY IDENT
- {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($6, tag_true))) }
-| IDENT LPAR tuple_expr RPAR EVERY IDENT LPAR IDENT RPAR
- {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($8, $6))) }
-
-/* Boolean expr */
-| expr AND expr
- {mkpredef_call "&&" [$1;$3]}
-| expr AMPERAMPER expr
- {mkpredef_call "&&" [$1;$3]}
-| expr OR expr
- {mkpredef_call "||" [$1;$3]}
-| expr BARBAR expr
- {mkpredef_call "||" [$1;$3]}
-| expr XOR expr
- {mkpredef_call "xor" [$1;$3]}
-| NOT expr
- {mkpredef_call "not" [$2]}
-| expr IMPL expr
- {mkpredef_call "impl" [$1;$3]}
-
-/* Comparison expr */
-| expr EQ expr
- {mkpredef_call "=" [$1;$3]}
-| expr LT expr
- {mkpredef_call "<" [$1;$3]}
-| expr LTE expr
- {mkpredef_call "<=" [$1;$3]}
-| expr GT expr
- {mkpredef_call ">" [$1;$3]}
-| expr GTE expr
- {mkpredef_call ">=" [$1;$3]}
-| expr NEQ expr
- {mkpredef_call "!=" [$1;$3]}
-
-/* Arithmetic expr */
-| expr PLUS expr
- {mkpredef_call "+" [$1;$3]}
-| expr MINUS expr
- {mkpredef_call "-" [$1;$3]}
-| expr MULT expr
- {mkpredef_call "*" [$1;$3]}
-| expr DIV expr
- {mkpredef_call "/" [$1;$3]}
-| MINUS expr %prec UMINUS
- {mkpredef_call "uminus" [$2]}
-| expr MOD expr
- {mkpredef_call "mod" [$1;$3]}
-
-/* If */
-| IF expr THEN expr ELSE expr
- {mkexpr (Expr_ite ($2, $4, $6))}
-
-handler_expr_list:
- { [] }
-| handler_expr handler_expr_list { $1 :: $2 }
-
-handler_expr:
- LPAR IDENT ARROW expr RPAR { ($2, $4) }
-
-signed_const_array:
-| signed_const { [$1] }
-| signed_const COMMA signed_const_array { $1 :: $3 }
-
-signed_const_struct:
-| IDENT EQ signed_const { [ ($1, $3) ] }
-| IDENT EQ signed_const COMMA signed_const_struct { ($1, $3) :: $5 }
-
-signed_const:
- INT {Const_int $1}
-| REAL {Const_real $1}
-| FLOAT {Const_float $1}
-| IDENT {Const_tag $1}
-| MINUS INT {Const_int (-1 * $2)}
-| MINUS REAL {Const_real ("-" ^ $2)}
-| MINUS FLOAT {Const_float (-1. *. $2)}
-| LCUR signed_const_struct RCUR { Const_struct $2 }
-| LBRACKET signed_const_array RBRACKET { Const_array $2 }
-
-dim:
- INT { mkdim_int $1 }
-| LPAR dim RPAR { $2 }
-| IDENT { mkdim_ident $1 }
-| dim AND dim
- {mkdim_appl "&&" [$1;$3]}
-| dim AMPERAMPER dim
- {mkdim_appl "&&" [$1;$3]}
-| dim OR dim
- {mkdim_appl "||" [$1;$3]}
-| dim BARBAR dim
- {mkdim_appl "||" [$1;$3]}
-| dim XOR dim
- {mkdim_appl "xor" [$1;$3]}
-| NOT dim
- {mkdim_appl "not" [$2]}
-| dim IMPL dim
- {mkdim_appl "impl" [$1;$3]}
-
-/* Comparison dim */
-| dim EQ dim
- {mkdim_appl "=" [$1;$3]}
-| dim LT dim
- {mkdim_appl "<" [$1;$3]}
-| dim LTE dim
- {mkdim_appl "<=" [$1;$3]}
-| dim GT dim
- {mkdim_appl ">" [$1;$3]}
-| dim GTE dim
- {mkdim_appl ">=" [$1;$3]}
-| dim NEQ dim
- {mkdim_appl "!=" [$1;$3]}
-
-/* Arithmetic dim */
-| dim PLUS dim
- {mkdim_appl "+" [$1;$3]}
-| dim MINUS dim
- {mkdim_appl "-" [$1;$3]}
-| dim MULT dim
- {mkdim_appl "*" [$1;$3]}
-| dim DIV dim
- {mkdim_appl "/" [$1;$3]}
-| MINUS dim %prec UMINUS
- {mkdim_appl "uminus" [$2]}
-| dim MOD dim
- {mkdim_appl "mod" [$1;$3]}
-/* If */
-| IF dim THEN dim ELSE dim
- {mkdim_ite $2 $4 $6}
-
-locals:
- {[]}
-| VAR vdecl_list SCOL {$2}
-
-vdecl_list:
- vdecl {$1}
-| vdecl_list SCOL vdecl {$3 @ $1}
-
-vdecl:
-/* Useless no ?*/ ident_list
- {List.map mkvar_decl
- (List.map (fun id -> (id, mktyp Tydec_any, mkclock Ckdec_any, false)) $1)}
-
-| ident_list COL typeconst clock
- {List.map mkvar_decl (List.map (fun id -> (id, mktyp $3, $4, false)) $1)}
-| CONST ident_list COL typeconst /* static parameters don't have clocks */
- {List.map mkvar_decl (List.map (fun id -> (id, mktyp $4, mkclock Ckdec_any, true)) $2)}
-
-cdecl_list:
- cdecl SCOL { [$1] }
-| cdecl_list cdecl SCOL { $2::$1 }
-
-cdecl:
- IDENT EQ signed_const {
- let c = {
- const_id = $1;
- const_loc = Location.symbol_rloc ();
- const_type = Types.new_var ();
- const_value = $3;
- } in
- Hashtbl.add consts_table $1 c; c
- }
-
-clock:
- {mkclock Ckdec_any}
-| when_list
- {mkclock (Ckdec_bool (List.rev $1))}
-
-when_cond:
- WHEN IDENT {($2, tag_true)}
-| WHENNOT IDENT {($2, tag_false)}
-| WHEN IDENT LPAR IDENT RPAR {($4, $2)}
-
-when_list:
- when_cond {[$1]}
-| when_list when_cond {$2::$1}
-
-ident_list:
- IDENT {[$1]}
-| ident_list COMMA IDENT {$3::$1}
-
-SCOL_opt:
- SCOL {} | {}
-
-
-lustre_annot:
-lustre_annot_list EOF { { annots = $1; annot_loc = get_loc () } }
-
-lustre_annot_list:
- { [] }
-| kwd COL qexpr SCOL lustre_annot_list { ($1,$3)::$5 }
-| IDENT COL qexpr SCOL lustre_annot_list { ([$1],$3)::$5 }
-| INVARIANT COL qexpr SCOL lustre_annot_list{ (["invariant"],$3)::$5 }
-| OBSERVER COL qexpr SCOL lustre_annot_list { (["observer"],$3)::$5 }
-
-kwd:
-DIV { [] }
-| DIV IDENT kwd { $2::$3}
-
-%%
-(* Local Variables: *)
-(* compile-command:"make -C .." *)
-(* End: *)
-
-
+/********************************************************************/
+/* */
+/* The LustreC compiler toolset / The LustreC Development Team */
+/* Copyright 2012 - -- ONERA - CNRS - INPT */
+/* */
+/* LustreC is free software, distributed WITHOUT ANY WARRANTY */
+/* under the terms of the GNU Lesser General Public License */
+/* version 2.1. */
+/* */
+/********************************************************************/
+
+%{
+open Utils
+open LustreSpec
+open Corelang
+open Dimension
+open Parse
+
+let get_loc () = Location.symbol_rloc ()
+
+let mktyp x = mktyp (get_loc ()) x
+let mkclock x = mkclock (get_loc ()) x
+let mkvar_decl x = mkvar_decl (get_loc ()) x
+let mkexpr x = mkexpr (get_loc ()) x
+let mkeexpr x = mkeexpr (get_loc ()) x
+let mkeq x = mkeq (get_loc ()) x
+let mkassert x = mkassert (get_loc ()) x
+let mktop_decl itf x = mktop_decl (get_loc ()) (Location.get_module ()) itf x
+let mkpredef_call x = mkpredef_call (get_loc ()) x
+(*let mkpredef_unary_call x = mkpredef_unary_call (get_loc ()) x*)
+
+let mkdim_int i = mkdim_int (get_loc ()) i
+let mkdim_bool b = mkdim_bool (get_loc ()) b
+let mkdim_ident id = mkdim_ident (get_loc ()) id
+let mkdim_appl f args = mkdim_appl (get_loc ()) f args
+let mkdim_ite i t e = mkdim_ite (get_loc ()) i t e
+
+let mkannots annots = { annots = annots; annot_loc = get_loc () }
+
+%}
+
+%token <int> INT
+%token <string> REAL
+%token <float> FLOAT
+%token <string> STRING
+%token AUTOMATON STATE UNTIL UNLESS RESTART RESUME LAST
+%token STATELESS ASSERT OPEN QUOTE FUNCTION
+%token <string> IDENT
+%token <string> UIDENT
+%token TRUE FALSE
+%token <LustreSpec.expr_annot> ANNOT
+%token <LustreSpec.node_annot> NODESPEC
+%token LBRACKET RBRACKET LCUR RCUR LPAR RPAR SCOL COL COMMA COLCOL
+%token AMPERAMPER BARBAR NOT POWER
+%token IF THEN ELSE
+%token UCLOCK DCLOCK PHCLOCK TAIL
+%token MERGE FBY WHEN WHENNOT EVERY
+%token NODE LET TEL RETURNS VAR IMPORTED SENSOR ACTUATOR WCET TYPE CONST
+%token STRUCT ENUM
+%token TINT TFLOAT TREAL TBOOL TCLOCK
+%token RATE DUE
+%token EQ LT GT LTE GTE NEQ
+%token AND OR XOR IMPL
+%token MULT DIV MOD
+%token MINUS PLUS UMINUS
+%token PRE ARROW
+%token REQUIRES ENSURES OBSERVER
+%token INVARIANT BEHAVIOR ASSUMES
+%token EXISTS FORALL
+%token PROTOTYPE LIB
+%token EOF
+
+%nonassoc prec_exists prec_forall
+%nonassoc COMMA
+%left MERGE IF
+%nonassoc ELSE
+%right ARROW FBY
+%left WHEN WHENNOT UCLOCK DCLOCK PHCLOCK
+%right COLCOL
+%right IMPL
+%left OR XOR BARBAR
+%left AND AMPERAMPER
+%left NOT
+%nonassoc INT
+%nonassoc EQ LT GT LTE GTE NEQ
+%left MINUS PLUS
+%left MULT DIV MOD
+%left UMINUS
+%left POWER
+%left PRE LAST
+%nonassoc RBRACKET
+%nonassoc LBRACKET
+
+%start prog
+%type <LustreSpec.top_decl list> prog
+
+%start header
+%type <LustreSpec.top_decl list> header
+
+%start lustre_annot
+%type <LustreSpec.expr_annot> lustre_annot
+
+%start lustre_spec
+%type <LustreSpec.node_annot> lustre_spec
+
+%%
+
+module_ident:
+ UIDENT { $1 }
+| IDENT { $1 }
+
+tag_ident:
+ UIDENT { $1 }
+| TRUE { tag_true }
+| FALSE { tag_false }
+
+node_ident:
+ UIDENT { $1 }
+| IDENT { $1 }
+
+vdecl_ident:
+ UIDENT { $1 }
+| IDENT { $1 }
+
+const_ident:
+ UIDENT { $1 }
+| IDENT { $1 }
+
+type_ident:
+ IDENT { $1 }
+
+prog:
+ open_list typ_def_prog top_decl_list EOF { $1 @ $2 @ (List.rev $3) }
+
+typ_def_prog:
+ typ_def_list { $1 false }
+
+header:
+ open_list typ_def_header top_decl_header_list EOF { $1 @ $2 @ (List.rev $3) }
+
+typ_def_header:
+ typ_def_list { $1 true }
+
+open_list:
+ { [] }
+| open_lusi open_list { $1 :: $2 }
+
+open_lusi:
+| OPEN QUOTE module_ident QUOTE { mktop_decl false (Open (true, $3))}
+| OPEN LT module_ident GT { mktop_decl false (Open (false, $3)) }
+
+top_decl_list:
+ {[]}
+| top_decl_list top_decl {$2@$1}
+
+
+top_decl_header_list:
+ { [] }
+| top_decl_header_list top_decl_header { $2@$1 }
+
+state_annot:
+ FUNCTION { true }
+| NODE { false }
+
+top_decl_header:
+| CONST cdecl_list { List.rev ($2 true) }
+| nodespec_list state_annot node_ident LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR prototype_opt in_lib_opt SCOL
+ {let nd = mktop_decl true (ImportedNode
+ {nodei_id = $3;
+ nodei_type = Types.new_var ();
+ nodei_clock = Clocks.new_var true;
+ nodei_inputs = List.rev $5;
+ nodei_outputs = List.rev $10;
+ nodei_stateless = $2;
+ nodei_spec = $1;
+ nodei_prototype = $13;
+ nodei_in_lib = $14;})
+ in
+ (*add_imported_node $3 nd;*) [nd] }
+
+prototype_opt:
+ { None }
+| PROTOTYPE node_ident { Some $2}
+
+in_lib_opt:
+{ None }
+| LIB module_ident {Some $2}
+
+top_decl:
+| CONST cdecl_list { List.rev ($2 false) }
+| nodespec_list state_annot node_ident LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt locals LET eq_list TEL
+ {let eqs, asserts, annots = $16 in
+ let nd = mktop_decl false (Node
+ {node_id = $3;
+ node_type = Types.new_var ();
+ node_clock = Clocks.new_var true;
+ node_inputs = List.rev $5;
+ node_outputs = List.rev $10;
+ node_locals = List.rev $14;
+ node_gencalls = [];
+ node_checks = [];
+ node_asserts = asserts;
+ node_eqs = eqs;
+ node_dec_stateless = $2;
+ node_stateless = None;
+ node_spec = $1;
+ node_annot = annots})
+ in
+ (*add_node $3 nd;*) [nd] }
+
+nodespec_list:
+ { None }
+| NODESPEC nodespec_list {
+ (function
+ | None -> (fun s1 -> Some s1)
+ | Some s2 -> (fun s1 -> Some (merge_node_annot s1 s2))) $2 $1 }
+
+typ_def_list:
+ /* empty */ { (fun itf -> []) }
+| typ_def SCOL typ_def_list { (fun itf -> let ty1 = ($1 itf) in ty1 :: ($3 itf)) }
+
+typ_def:
+ TYPE type_ident EQ typ_def_rhs { (fun itf ->
+ let typ = mktop_decl itf (TypeDef { tydef_id = $2;
+ tydef_desc = $4
+ })
+ in (*add_type itf $2 typ;*) typ) }
+
+typ_def_rhs:
+ typeconst { $1 }
+| ENUM LCUR tag_list RCUR { Tydec_enum (List.rev $3) }
+| STRUCT LCUR field_list RCUR { Tydec_struct (List.rev $3) }
+
+array_typ_decl:
+ { fun typ -> typ }
+ | POWER dim array_typ_decl { fun typ -> $3 (Tydec_array ($2, typ)) }
+
+typeconst:
+ TINT array_typ_decl { $2 Tydec_int }
+| TBOOL array_typ_decl { $2 Tydec_bool }
+| TREAL array_typ_decl { $2 Tydec_real }
+| TFLOAT array_typ_decl { $2 Tydec_float }
+| type_ident array_typ_decl { $2 (Tydec_const $1) }
+| TBOOL TCLOCK { Tydec_clock Tydec_bool }
+| IDENT TCLOCK { Tydec_clock (Tydec_const $1) }
+
+tag_list:
+ UIDENT { $1 :: [] }
+| tag_list COMMA UIDENT { $3 :: $1 }
+
+field_list: { [] }
+| field_list IDENT COL typeconst SCOL { ($2, $4) :: $1 }
+
+eq_list:
+ { [], [], [] }
+| eq eq_list {let eql, assertl, annotl = $2 in ($1::eql), assertl, annotl}
+| assert_ eq_list {let eql, assertl, annotl = $2 in eql, ($1::assertl), annotl}
+| ANNOT eq_list {let eql, assertl, annotl = $2 in eql, assertl, $1::annotl}
+| automaton eq_list {let eql, assertl, annotl = $2 in ($1::eql), assertl, annotl}
+
+automaton:
+ AUTOMATON type_ident handler_list { failwith "not implemented" }
+
+handler_list:
+ { [] }
+| handler handler_list { $1::$2 }
+
+handler:
+ STATE UIDENT ARROW unless_list locals LET eq_list TEL until_list { () }
+
+unless_list:
+ { Automata.init }
+| unless unless_list { let (expr1, case1) = $1 in (fun case -> Automata.add_branch expr1 case1 ($2 case)) }
+
+until_list:
+ { Automata.init }
+| until until_list { let (expr1, case1) = $1 in (fun case -> Automata.add_branch expr1 case1 ($2 case)) }
+
+unless:
+ UNLESS expr RESTART UIDENT { ($2, (get_loc (), true, $4)) }
+| UNLESS expr RESUME UIDENT { ($2, (get_loc (), false, $4)) }
+
+until:
+ UNTIL expr RESTART UIDENT { ($2, (get_loc (), true, $4)) }
+| UNTIL expr RESUME UIDENT { ($2, (get_loc (), false, $4)) }
+
+assert_:
+| ASSERT expr SCOL {mkassert ($2)}
+
+eq:
+ ident_list EQ expr SCOL {mkeq (List.rev $1,$3)}
+| LPAR ident_list RPAR EQ expr SCOL {mkeq (List.rev $2,$5)}
+
+lustre_spec:
+| contract EOF { $1 }
+
+contract:
+requires ensures behaviors { { requires = $1; ensures = $2; behaviors = $3; spec_loc = get_loc () } }
+
+requires:
+{ [] }
+| REQUIRES qexpr SCOL requires { $2::$4 }
+
+ensures:
+{ [] }
+| ENSURES qexpr SCOL ensures { $2 :: $4 }
+| OBSERVER node_ident LPAR tuple_expr RPAR SCOL ensures {
+ mkeexpr (mkexpr ((Expr_appl ($2, mkexpr (Expr_tuple $4), None)))) :: $7
+}
+
+behaviors:
+{ [] }
+| BEHAVIOR IDENT COL assumes ensures behaviors { ($2,$4,$5,get_loc ())::$6 }
+
+assumes:
+{ [] }
+| ASSUMES qexpr SCOL assumes { $2::$4 }
+
+/* WARNING: UNUSED RULES */
+tuple_qexpr:
+| qexpr COMMA qexpr {[$3;$1]}
+| tuple_qexpr COMMA qexpr {$3::$1}
+
+qexpr:
+| expr { mkeexpr $1 }
+ /* Quantifiers */
+| EXISTS vdecl SCOL qexpr %prec prec_exists { extend_eexpr [Exists, $2] $4 }
+| FORALL vdecl SCOL qexpr %prec prec_forall { extend_eexpr [Forall, $2] $4 }
+
+
+tuple_expr:
+ expr COMMA expr {[$3;$1]}
+| tuple_expr COMMA expr {$3::$1}
+
+// Same as tuple expr but accepting lists with single element
+array_expr:
+ expr {[$1]}
+| expr COMMA array_expr {$1::$3}
+
+dim_list:
+ dim RBRACKET { fun base -> mkexpr (Expr_access (base, $1)) }
+| dim RBRACKET LBRACKET dim_list { fun base -> $4 (mkexpr (Expr_access (base, $1))) }
+
+expr:
+/* constants */
+ INT {mkexpr (Expr_const (Const_int $1))}
+| REAL {mkexpr (Expr_const (Const_real $1))}
+| FLOAT {mkexpr (Expr_const (Const_float $1))}
+/* Idents or type enum tags */
+| IDENT { mkexpr (Expr_ident $1) }
+| tag_ident { mkexpr (Expr_ident $1) (*(Expr_const (Const_tag $1))*) }
+| LPAR ANNOT expr RPAR
+ {update_expr_annot $3 $2}
+| LPAR expr RPAR
+ {$2}
+| LPAR tuple_expr RPAR
+ {mkexpr (Expr_tuple (List.rev $2))}
+
+/* Array expressions */
+| LBRACKET array_expr RBRACKET { mkexpr (Expr_array $2) }
+| expr POWER dim { mkexpr (Expr_power ($1, $3)) }
+| expr LBRACKET dim_list { $3 $1 }
+
+/* Temporal operators */
+| PRE expr
+ {mkexpr (Expr_pre $2)}
+| expr ARROW expr
+ {mkexpr (Expr_arrow ($1,$3))}
+| expr FBY expr
+ {(*mkexpr (Expr_fby ($1,$3))*)
+ mkexpr (Expr_arrow ($1, mkexpr (Expr_pre $3)))}
+| expr WHEN vdecl_ident
+ {mkexpr (Expr_when ($1,$3,tag_true))}
+| expr WHENNOT vdecl_ident
+ {mkexpr (Expr_when ($1,$3,tag_false))}
+| expr WHEN tag_ident LPAR vdecl_ident RPAR
+ {mkexpr (Expr_when ($1, $5, $3))}
+| MERGE vdecl_ident handler_expr_list
+ {mkexpr (Expr_merge ($2,$3))}
+
+/* Applications */
+| node_ident LPAR expr RPAR
+ {mkexpr (Expr_appl ($1, $3, None))}
+| node_ident LPAR expr RPAR EVERY vdecl_ident
+ {mkexpr (Expr_appl ($1, $3, Some ($6, tag_true)))}
+| node_ident LPAR expr RPAR EVERY tag_ident LPAR vdecl_ident RPAR
+ {mkexpr (Expr_appl ($1, $3, Some ($8, $6))) }
+| node_ident LPAR tuple_expr RPAR
+ {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), None))}
+| node_ident LPAR tuple_expr RPAR EVERY vdecl_ident
+ {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($6, tag_true))) }
+| node_ident LPAR tuple_expr RPAR EVERY tag_ident LPAR vdecl_ident RPAR
+ {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($8, $6))) }
+
+/* Boolean expr */
+| expr AND expr
+ {mkpredef_call "&&" [$1;$3]}
+| expr AMPERAMPER expr
+ {mkpredef_call "&&" [$1;$3]}
+| expr OR expr
+ {mkpredef_call "||" [$1;$3]}
+| expr BARBAR expr
+ {mkpredef_call "||" [$1;$3]}
+| expr XOR expr
+ {mkpredef_call "xor" [$1;$3]}
+| NOT expr
+ {mkpredef_call "not" [$2]}
+| expr IMPL expr
+ {mkpredef_call "impl" [$1;$3]}
+
+/* Comparison expr */
+| expr EQ expr
+ {mkpredef_call "=" [$1;$3]}
+| expr LT expr
+ {mkpredef_call "<" [$1;$3]}
+| expr LTE expr
+ {mkpredef_call "<=" [$1;$3]}
+| expr GT expr
+ {mkpredef_call ">" [$1;$3]}
+| expr GTE expr
+ {mkpredef_call ">=" [$1;$3]}
+| expr NEQ expr
+ {mkpredef_call "!=" [$1;$3]}
+
+/* Arithmetic expr */
+| expr PLUS expr
+ {mkpredef_call "+" [$1;$3]}
+| expr MINUS expr
+ {mkpredef_call "-" [$1;$3]}
+| expr MULT expr
+ {mkpredef_call "*" [$1;$3]}
+| expr DIV expr
+ {mkpredef_call "/" [$1;$3]}
+| MINUS expr %prec UMINUS
+ {mkpredef_call "uminus" [$2]}
+| expr MOD expr
+ {mkpredef_call "mod" [$1;$3]}
+
+/* If */
+| IF expr THEN expr ELSE expr
+ {mkexpr (Expr_ite ($2, $4, $6))}
+
+handler_expr_list:
+ { [] }
+| handler_expr handler_expr_list { $1 :: $2 }
+
+handler_expr:
+ LPAR tag_ident ARROW expr RPAR { ($2, $4) }
+
+signed_const_array:
+| signed_const { [$1] }
+| signed_const COMMA signed_const_array { $1 :: $3 }
+
+signed_const_struct:
+| IDENT EQ signed_const { [ ($1, $3) ] }
+| IDENT EQ signed_const COMMA signed_const_struct { ($1, $3) :: $5 }
+
+signed_const:
+ INT {Const_int $1}
+| REAL {Const_real $1}
+| FLOAT {Const_float $1}
+| tag_ident {Const_tag $1}
+| MINUS INT {Const_int (-1 * $2)}
+| MINUS REAL {Const_real ("-" ^ $2)}
+| MINUS FLOAT {Const_float (-1. *. $2)}
+| LCUR signed_const_struct RCUR { Const_struct $2 }
+| LBRACKET signed_const_array RBRACKET { Const_array $2 }
+
+dim:
+ INT { mkdim_int $1 }
+| LPAR dim RPAR { $2 }
+| UIDENT { mkdim_ident $1 }
+| IDENT { mkdim_ident $1 }
+| dim AND dim
+ {mkdim_appl "&&" [$1;$3]}
+| dim AMPERAMPER dim
+ {mkdim_appl "&&" [$1;$3]}
+| dim OR dim
+ {mkdim_appl "||" [$1;$3]}
+| dim BARBAR dim
+ {mkdim_appl "||" [$1;$3]}
+| dim XOR dim
+ {mkdim_appl "xor" [$1;$3]}
+| NOT dim
+ {mkdim_appl "not" [$2]}
+| dim IMPL dim
+ {mkdim_appl "impl" [$1;$3]}
+
+/* Comparison dim */
+| dim EQ dim
+ {mkdim_appl "=" [$1;$3]}
+| dim LT dim
+ {mkdim_appl "<" [$1;$3]}
+| dim LTE dim
+ {mkdim_appl "<=" [$1;$3]}
+| dim GT dim
+ {mkdim_appl ">" [$1;$3]}
+| dim GTE dim
+ {mkdim_appl ">=" [$1;$3]}
+| dim NEQ dim
+ {mkdim_appl "!=" [$1;$3]}
+
+/* Arithmetic dim */
+| dim PLUS dim
+ {mkdim_appl "+" [$1;$3]}
+| dim MINUS dim
+ {mkdim_appl "-" [$1;$3]}
+| dim MULT dim
+ {mkdim_appl "*" [$1;$3]}
+| dim DIV dim
+ {mkdim_appl "/" [$1;$3]}
+| MINUS dim %prec UMINUS
+ {mkdim_appl "uminus" [$2]}
+| dim MOD dim
+ {mkdim_appl "mod" [$1;$3]}
+/* If */
+| IF dim THEN dim ELSE dim
+ {mkdim_ite $2 $4 $6}
+
+locals:
+ {[]}
+| VAR vdecl_list SCOL {$2}
+
+vdecl_list:
+ vdecl {$1}
+| vdecl_list SCOL vdecl {$3 @ $1}
+
+vdecl:
+/* Useless no ?*/ ident_list
+ {List.map mkvar_decl
+ (List.map (fun id -> (id, mktyp Tydec_any, mkclock Ckdec_any, false)) $1)}
+
+| ident_list COL typeconst clock
+ {List.map mkvar_decl (List.map (fun id -> (id, mktyp $3, $4, false)) $1)}
+| CONST ident_list COL typeconst /* static parameters don't have clocks */
+ {List.map mkvar_decl (List.map (fun id -> (id, mktyp $4, mkclock Ckdec_any, true)) $2)}
+
+cdecl_list:
+ cdecl SCOL { (fun itf -> [$1 itf]) }
+| cdecl cdecl_list SCOL { (fun itf -> let c1 = ($1 itf) in c1::($2 itf)) }
+
+cdecl:
+ const_ident EQ signed_const {
+ (fun itf ->
+ let c = mktop_decl itf (Const {
+ const_id = $1;
+ const_loc = Location.symbol_rloc ();
+ const_type = Types.new_var ();
+ const_value = $3})
+ in
+ (*add_const itf $1 c;*) c)
+ }
+
+clock:
+ {mkclock Ckdec_any}
+| when_list
+ {mkclock (Ckdec_bool (List.rev $1))}
+
+when_cond:
+ WHEN IDENT {($2, tag_true)}
+| WHENNOT IDENT {($2, tag_false)}
+| WHEN tag_ident LPAR IDENT RPAR {($4, $2)}
+
+when_list:
+ when_cond {[$1]}
+| when_list when_cond {$2::$1}
+
+ident_list:
+ vdecl_ident {[$1]}
+| ident_list COMMA vdecl_ident {$3::$1}
+
+SCOL_opt:
+ SCOL {} | {}
+
+
+lustre_annot:
+lustre_annot_list EOF { { annots = $1; annot_loc = get_loc () } }
+
+lustre_annot_list:
+ { [] }
+| kwd COL qexpr SCOL lustre_annot_list { ($1,$3)::$5 }
+| IDENT COL qexpr SCOL lustre_annot_list { ([$1],$3)::$5 }
+| INVARIANT COL qexpr SCOL lustre_annot_list{ (["invariant"],$3)::$5 }
+| OBSERVER COL qexpr SCOL lustre_annot_list { (["observer"],$3)::$5 }
+
+kwd:
+DIV { [] }
+| DIV IDENT kwd { $2::$3}
+
+%%
+(* Local Variables: *)
+(* compile-command:"make -C .." *)
+(* End: *)
+
+
diff --git a/src/printers.ml b/src/printers.ml
index 22d457acf1705e76d910449f9da1960fad259a2c..504dd06a7dc31d1a64c917a49e2e32e78142e168 100644
--- a/src/printers.ml
+++ b/src/printers.ml
@@ -40,65 +40,6 @@ let pp_quantifiers fmt (q, vars) =
| Forall -> fprintf fmt "forall %a" (fprintf_list ~sep:"; " pp_var) vars
| Exists -> fprintf fmt "exists %a" (fprintf_list ~sep:"; " pp_var) vars
-(*
-let pp_econst fmt c =
- match c with
- | EConst_int i -> pp_print_int fmt i
- | EConst_real r -> pp_print_string fmt r
- | EConst_float r -> pp_print_float fmt r
- | EConst_tag t -> pp_print_string fmt t
- | EConst_string s -> pp_print_string fmt ("\"" ^ s ^ "\"")
-
-
-let rec pp_eexpr fmt eexpr =
- match eexpr.eexpr_desc with
- | EExpr_const c -> pp_econst fmt c
- | EExpr_ident id -> pp_print_string fmt id
- | EExpr_tuple el -> fprintf_list ~sep:"," pp_eexpr fmt el
- | EExpr_arrow (e1, e2) -> fprintf fmt "%a -> %a" pp_eexpr e1 pp_eexpr e2
- | EExpr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_eexpr e1 pp_eexpr e2
- (* | EExpr_concat (e1, e2) -> fprintf fmt "%a::%a" pp_eexpr e1 pp_eexpr e2 *)
- (* | EExpr_tail e -> fprintf fmt "tail %a" pp_eexpr e *)
- | EExpr_pre e -> fprintf fmt "pre %a" pp_eexpr e
- | EExpr_when (e, id) -> fprintf fmt "%a when %s" pp_eexpr e id
- | EExpr_merge (id, e1, e2) ->
- fprintf fmt "merge (%s, %a, %a)" id pp_eexpr e1 pp_eexpr e2
- | EExpr_appl (id, e, r) -> pp_eapp fmt id e r
- | EExpr_forall (vars, e) -> fprintf fmt "forall %a; %a" pp_node_args vars pp_eexpr e
- | EExpr_exists (vars, e) -> fprintf fmt "exists %a; %a" pp_node_args vars pp_eexpr e
-
-
- (* | EExpr_whennot _ *)
- (* | EExpr_uclock _ *)
- (* | EExpr_dclock _ *)
- (* | EExpr_phclock _ -> assert false *)
-and pp_eapp fmt id e r =
- match r with
- | None ->
- (match id, e.eexpr_desc with
- | "+", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_eexpr e1 pp_eexpr e2
- | "uminus", _ -> fprintf fmt "(- %a)" pp_eexpr e
- | "-", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_eexpr e1 pp_eexpr e2
- | "*", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_eexpr e1 pp_eexpr e2
- | "/", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_eexpr e1 pp_eexpr e2
- | "mod", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_eexpr e1 pp_eexpr e2
- | "&&", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a && %a)" pp_eexpr e1 pp_eexpr e2
- | "||", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a || %a)" pp_eexpr e1 pp_eexpr e2
- | "xor", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ^^ %a)" pp_eexpr e1 pp_eexpr e2
- | "impl", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ==> %a)" pp_eexpr e1 pp_eexpr e2
- | "<", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a < %a)" pp_eexpr e1 pp_eexpr e2
- | "<=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a <= %a)" pp_eexpr e1 pp_eexpr e2
- | ">", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a > %a)" pp_eexpr e1 pp_eexpr e2
- | ">=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a >= %a)" pp_eexpr e1 pp_eexpr e2
- | "!=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_eexpr e1 pp_eexpr e2
- | "=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a == %a)" pp_eexpr e1 pp_eexpr e2
- | "not", _ -> fprintf fmt "(! %a)" pp_eexpr e
- | "ite", EExpr_tuple([e1;e2;e3]) -> fprintf fmt "(if %a then %a else %a)" pp_eexpr e1 pp_eexpr e2 pp_eexpr e3
- | _ -> fprintf fmt "%s (%a)" id pp_eexpr e)
- | Some x -> fprintf fmt "%s (%a) every %s" id pp_eexpr e x
-*)
-
-
let rec pp_struct_const_field fmt (label, c) =
fprintf fmt "%a = %a;" pp_print_string label pp_const c
and pp_const fmt c =
@@ -211,8 +152,11 @@ and pp_var_type_dec_desc fmt tdesc =
let pp_var_type_dec fmt ty =
pp_var_type_dec_desc fmt ty.ty_dec_desc
-let pp_type_def fmt ty =
- fprintf fmt "type %s = %a;@ " ty.ty_def_id pp_var_type_dec_desc ty.ty_def_desc
+let pp_typedef fmt ty =
+ fprintf fmt "type %s = %a;@ " ty.tydef_id pp_var_type_dec_desc ty.tydef_desc
+
+let pp_typedec fmt ty =
+ fprintf fmt "type %s;@ " ty.tydec_id
(* let rec pp_var_type fmt ty = *)
(* fprintf fmt "%a" (match ty.tdesc with *)
@@ -279,26 +223,26 @@ fprintf fmt "@[<v 0>%a%t%s %s (%a) returns (%a)@.%a%alet@.@[<h 2> @ @[<v>%a@ %
(*fprintf fmt "@ /* Scheduling: %a */ @ " (fprintf_list ~sep:", " pp_print_string) (Scheduling.schedule_node nd)*)
let pp_imported_node fmt ind =
- fprintf fmt "@[<v>%s %s (%a) returns (%a) %t@]"
+ fprintf fmt "@[<v>%s %s (%a) returns (%a)@]"
(if ind.nodei_stateless then "function" else "node")
ind.nodei_id
pp_node_args ind.nodei_inputs
pp_node_args ind.nodei_outputs
- (fun fmt -> if ind.nodei_stateless then Format.fprintf fmt "stateless")
-let pp_const_list fmt clist =
- fprintf_list ~sep:"@ " (fun fmt cdecl ->
- fprintf fmt "%s = %a;"
- cdecl.const_id pp_const cdecl.const_value) fmt clist
+let pp_const_decl fmt cdecl =
+ fprintf fmt "%s = %a;" cdecl.const_id pp_const cdecl.const_value
+
+let pp_const_decl_list fmt clist =
+ fprintf_list ~sep:"@ " pp_const_decl fmt clist
let pp_decl fmt decl =
match decl.top_decl_desc with
| Node nd -> fprintf fmt "%a@ " pp_node nd
| ImportedNode ind ->
fprintf fmt "imported %a;@ " pp_imported_node ind
- | Consts clist -> (fprintf fmt "const %a@ " pp_const_list clist)
- | Open (local, s) -> if local then fprintf fmt "open \"%s\"@ " s else fprintf fmt "open <%s>@ " s
- | Type tdef -> fprintf fmt "%a@ " pp_type_def tdef
+ | Const c -> fprintf fmt "const %a@ " pp_const_decl c
+ | Open (local, s) -> if local then fprintf fmt "#open \"%s\"@ " s else fprintf fmt "#open <%s>@ " s
+ | TypeDef tdef -> fprintf fmt "%a@ " pp_typedef tdef
let pp_prog fmt prog =
fprintf_list ~sep:"@ " pp_decl fmt prog
@@ -307,26 +251,20 @@ let pp_short_decl fmt decl =
match decl.top_decl_desc with
| Node nd -> fprintf fmt "node %s@ " nd.node_id
| ImportedNode ind -> fprintf fmt "imported node %s" ind.nodei_id
- | Consts clist -> (fprintf fmt "const %a@ " pp_const_list clist)
- | Open (local, s) -> if local then fprintf fmt "open \"%s\"@ " s else fprintf fmt "open <%s>@ " s
- | Type tdef -> fprintf fmt "type %s;@ " tdef.ty_def_id
+ | Const c -> fprintf fmt "const %a@ " pp_const_decl c
+ | Open (local, s) -> if local then fprintf fmt "#open \"%s\"@ " s else fprintf fmt "#open <%s>@ " s
+ | TypeDef tdef -> fprintf fmt "type %s;@ " tdef.tydef_id
let pp_lusi fmt decl =
match decl.top_decl_desc with
- | Node nd ->
- fprintf fmt
- "@[<v>%s %s (%a) returns (%a);@ @]@ "
- (if nd.node_dec_stateless then "function" else "node")
- nd.node_id
- pp_node_args nd.node_inputs
- pp_node_args nd.node_outputs
-| Consts clist -> (fprintf fmt "const %a@ " pp_const_list clist)
-| Open (local, s) -> if local then fprintf fmt "open \"%s\"@ " s else fprintf fmt "open <%s>@ " s
-| Type tdef -> fprintf fmt "%a@ " pp_type_def tdef
-| ImportedNode _ -> ()
-
-let pp_lusi_header fmt filename prog =
- fprintf fmt "(* Generated Lustre Interface file from %s *)@." filename;
+ | ImportedNode ind -> fprintf fmt "%a;@ " pp_imported_node ind
+ | Const c -> fprintf fmt "const %a@ " pp_const_decl c
+ | Open (local, s) -> if local then fprintf fmt "#open \"%s\"@ " s else fprintf fmt "#open <%s>@ " s
+ | TypeDef tdef -> fprintf fmt "%a@ " pp_typedef tdef
+ | Node _ -> assert false
+
+let pp_lusi_header fmt basename prog =
+ fprintf fmt "(* Generated Lustre Interface file from %s.lus *)@." basename;
fprintf fmt "(* by Lustre-C compiler version %s, %a *)@." Version.number pp_date (Unix.gmtime (Unix.time ()));
fprintf fmt "(* Feel free to mask some of the definitions by removing them from this file. *)@.@.";
List.iter (fprintf fmt "%a@." pp_lusi) prog
diff --git a/src/types.ml b/src/types.ml
index 1cf1a5e31e6052bf0f6a2cdfc47f1953dacd380a..04d17a74c92ab151fff36a40c5f4900499e69c12 100755
--- a/src/types.ml
+++ b/src/types.ml
@@ -163,7 +163,7 @@ let pp_error fmt = function
(Utils.fprintf_list ~sep:"," pp_print_string)
(fst (Utils.list_of_imap vmap))
| Declared_but_undefined id ->
- fprintf fmt "Node %s is declared but not defined@." id
+ fprintf fmt "%s is declared but not defined@." id
| Type_clash (ty1,ty2) ->
Utils.reset_names ();
fprintf fmt "Expected type %a, got type %a@." print_ty ty1 print_ty ty2
diff --git a/src/typing.ml b/src/typing.ml
index 5c45975dea789c7b2e424f316a1f44ca0b93bde3..718f1d2c8237cc058d41d80e2b0fdb78fc76da20 100755
--- a/src/typing.ml
+++ b/src/typing.ml
@@ -130,11 +130,17 @@ let rec coretype_type ty =
| Tstatic (_, t) -> coretype_type t
| _ -> assert false
-let get_type_definition tname =
+let get_coretype_definition tname =
try
- type_coretype (fun d -> ()) (Hashtbl.find type_table (Tydec_const tname))
+ let top = Hashtbl.find type_table (Tydec_const tname) in
+ match top.top_decl_desc with
+ | TypeDef tdef -> tdef.tydef_desc
+ | _ -> assert false
with Not_found -> raise (Error (Location.dummy_loc, Unbound_type tname))
+let get_type_definition tname =
+ type_coretype (fun d -> ()) (get_coretype_definition tname)
+
(* Equality on ground types only *)
(* Should be used between local variables which must have a ground type *)
let rec eq_ground t1 t2 =
@@ -240,7 +246,8 @@ let try_unify ?(sub=false) ?(semi=false) ty1 ty2 loc =
let rec type_struct_const_field loc (label, c) =
if Hashtbl.mem field_table label
- then let tydec = Hashtbl.find field_table label in
+ 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
@@ -260,7 +267,13 @@ and type_const loc c =
Type_predef.type_array d ty
| Const_tag t ->
if Hashtbl.mem tag_table t
- then type_coretype (fun d -> ()) (Hashtbl.find tag_table t)
+ then
+ let tydef = typedef_of_top (Hashtbl.find tag_table t) in
+ let tydec =
+ if is_user_type tydef.tydef_desc
+ then Tydec_const tydef.tydef_id
+ else tydef.tydef_desc in
+ type_coretype (fun d -> ()) tydec
else raise (Error (loc, Unbound_value ("enum tag " ^ t)))
| Const_struct fl ->
let ty_struct = new_var () in
@@ -642,19 +655,21 @@ let type_imported_node env nd loc =
nd.nodei_type <- ty_node;
new_env
+let type_top_const env cdecl =
+ let ty = type_const cdecl.const_loc cdecl.const_value in
+ let d =
+ 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 new_env = Env.add_value env cdecl.const_id ty in
+ cdecl.const_type <- ty;
+ new_env
+
let type_top_consts env clist =
- List.fold_left (fun env cdecl ->
- let ty = type_const cdecl.const_loc cdecl.const_value in
- let d =
- 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 new_env = Env.add_value env cdecl.const_id ty in
- cdecl.const_type <- ty;
- new_env) env clist
-
-let type_top_decl env decl =
+ List.fold_left type_top_const env clist
+
+let rec type_top_decl env decl =
match decl.top_decl_desc with
| Node nd -> (
try
@@ -668,9 +683,9 @@ let type_top_decl env decl =
)
| ImportedNode nd ->
type_imported_node env nd decl.top_decl_loc
- | Consts clist ->
- type_top_consts env clist
- | Type _
+ | Const c ->
+ type_top_const env c
+ | TypeDef _ -> List.fold_left type_top_decl env (consts_of_enum_type decl)
| Open _ -> env
let type_prog env decls =
@@ -702,39 +717,53 @@ let uneval_top_generics decl =
uneval_node_generics (nd.node_inputs @ nd.node_outputs)
| ImportedNode nd ->
uneval_node_generics (nd.nodei_inputs @ nd.nodei_outputs)
- | Consts _
- | Type _
+ | Const _
+ | TypeDef _
| Open _ -> ()
let uneval_prog_generics prog =
List.iter uneval_top_generics prog
-let rec get_imported_node decls id =
+let rec get_imported_symbol decls id =
match decls with
| [] -> assert false
| decl::q ->
(match decl.top_decl_desc with
- | ImportedNode nd when id = nd.nodei_id -> decl
- | _ -> get_imported_node q id)
+ | ImportedNode nd when id = nd.nodei_id && decl.top_decl_itf -> decl
+ | Const c when id = c.const_id && decl.top_decl_itf -> decl
+ | TypeDef _ -> get_imported_symbol (consts_of_enum_type decl @ q) id
+ | _ -> get_imported_symbol q id)
let check_env_compat header declared computed =
uneval_prog_generics header;
- Env.iter declared (fun k decl_type_k ->
- let computed_t = instantiate (ref []) (ref [])
- (try Env.lookup_value computed k
- with Not_found ->
- let loc = (get_imported_node header k).top_decl_loc in
- raise (Error (loc, Declared_but_undefined k))) in
+ Env.iter declared (fun k decl_type_k ->
+ let loc = (get_imported_symbol header k).top_decl_loc in
+ let computed_t =
+ instantiate (ref []) (ref [])
+ (try Env.lookup_value computed k
+ with Not_found -> raise (Error (loc, Declared_but_undefined k))) in
(*Types.print_ty Format.std_formatter decl_type_k;
- Types.print_ty Format.std_formatter computed_t;*)
- try_unify ~sub:true ~semi:true decl_type_k computed_t Location.dummy_loc
- )
+ Types.print_ty Format.std_formatter computed_t;*)
+ try_unify ~sub:true ~semi:true decl_type_k computed_t loc
+ )
+
let check_typedef_top decl =
+(*Format.eprintf "check_typedef %a@." Printers.pp_short_decl decl;*)
+(*Printers.pp_var_type_dec_desc (typedef_of_top decl).tydef_id*)
+(*Format.eprintf "%a" Corelang.print_type_table ();*)
match decl.top_decl_desc with
- | Type ty ->
-Format.eprintf "check_typedef %a %a@." Printers.pp_var_type_dec_desc ty.ty_def_desc Printers.pp_var_type_dec_desc (Hashtbl.find type_table (Tydec_const ty.ty_def_id));
- if coretype_equal ty.ty_def_desc (Hashtbl.find type_table (Tydec_const ty.ty_def_id)) then ()
- else raise (Error (decl.top_decl_loc, Type_mismatch ty.ty_def_id))
+ | TypeDef ty ->
+ let owner = decl.top_decl_owner in
+ let itf = decl.top_decl_itf in
+ let decl' =
+ try Hashtbl.find type_table (Tydec_const (typedef_of_top decl).tydef_id)
+ with Not_found -> raise (Error (decl.top_decl_loc, Declared_but_undefined ("type "^ ty.tydef_id))) in
+ let owner' = decl'.top_decl_owner in
+ let itf' = decl'.top_decl_itf in
+ (match decl'.top_decl_desc with
+ | Const _ | Node _ | ImportedNode _ -> assert false
+ | TypeDef ty' when coretype_equal ty'.tydef_desc ty.tydef_desc && owner' = owner && itf && (not itf') -> ()
+ | _ -> raise (Error (decl.top_decl_loc, Type_mismatch ty.tydef_id)))
| _ -> ()
let check_typedef_compat header =