diff --git a/AUTHORS b/AUTHORS
index 1b9044ada5863c353c901adc65b60a5e3d11059c..e18499053630e4fa2d6217aa0f05fb5f34cc671c 100644
--- a/AUTHORS
+++ b/AUTHORS
@@ -1,2 +1,4 @@
-Pierre-Loïc Garoche - ONERA
-Xavier Thirioux - ENSEEIHT/INPT
+Pierre-Loïc Garoche - ONERA, France
+Xavier Thirioux - ENSEEIHT/INPT, France
+
+Inital Typing/Clocking by Julien Forget - LIFL, France
diff --git a/_tags b/_tags
index 543fa78959ff34769675799cd35d0381ce552c2f..d9173e6cb5dac006ffe678c43b07162b32817ca1 100644
--- a/_tags
+++ b/_tags
@@ -1,5 +1,6 @@
"src": include
"src/backends/C": include
+"src/backends/Horn": include
# OASIS_START
# DO NOT EDIT (digest: df9189c6c6943133cb99a2bb11ba7f05)
# Ignore VCS directories, you can use the same kind of rule outside
diff --git a/doc/lustre_spec.org b/doc/lustre_spec.org
index abbc81b77f39d80749096e2f89ae418bc5ed0acf..1ad28dc1c7e1a86e6b654a2f861f3a12ff95dc5e 100644
--- a/doc/lustre_spec.org
+++ b/doc/lustre_spec.org
@@ -1,4 +1,5 @@
Lustre annotation/specification language
+#+AUTHORS: Pierre-Loic Garoche, Rémi Delmas, Temesghen Kahsai
#+LATEX_HEADER: \usepackage{tikz,listings,stmaryrd,pgfplots,mathrsfs,syntax}
#+LATEX_HEADER: \input{lustre_lst}
diff --git a/src/Print.ml b/src/Print.ml
deleted file mode 100644
index 23d2c7403360a85cb5593725477e5fc898d165e5..0000000000000000000000000000000000000000
--- a/src/Print.ml
+++ /dev/null
@@ -1,90 +0,0 @@
-(*
- * Copyright (c) 2009 CNRS & Université Bordeaux 1.
- *
- * Author(s): Grégoire Sutre <gregoire.sutre@labri.fr>,
- * modified by Julien Forget <julien.forget@lifl.fr>
- *
- * Permission to use, copy, modify, and distribute this software for any
- * purpose with or without fee is hereby granted, provided that the above
- * copyright notice and this permission notice appear in all copies.
- *
- * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
- * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
- * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
- * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
- * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
- * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
- * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
- *)
-
-
-(*
- * Signatures and helper functions for pretty-printing.
- *)
-
-
-module type PRINTABLE_TYPE =
-sig
- type t
- val print : Format.formatter -> t -> unit
-end
-
-
-let string_converter_from_printer printer =
- function data ->
- Format.fprintf Format.str_formatter "@[%a@]" printer data ;
- Format.flush_str_formatter ()
-
-let hashtbl_printer_from_printer beg_f sep_f end_f printer fmt hashtbl =
- let length = Hashtbl.length hashtbl in
- if length > 0 then
- begin
- Format.fprintf fmt beg_f;
- ignore(
- Hashtbl.fold
- (fun k v cpt ->
- if cpt < length then
- begin
- Format.fprintf fmt "@[%a@]" printer (k,v);
- Format.fprintf fmt sep_f;
- cpt+1
- end
- else
- begin
- Format.fprintf fmt "@[%a@]" printer (k,v);
- Format.fprintf fmt end_f;
- cpt+1
- end)
- hashtbl 1)
- end
-
-let list_printer_from_printer beg_f sep_f end_f printer fmt list =
- match list with
- [] -> ()
- | head::tail ->
- Format.fprintf fmt beg_f;
- Format.fprintf fmt "@[%a@]" printer head;
- List.iter
- (function data ->
- begin
- Format.fprintf fmt sep_f;
- Format.fprintf fmt "@[%a@]" printer data
- end)
- tail;
- Format.fprintf fmt end_f
-
-let array_printer_from_printer beg_f sep_f end_f printer fmt array =
- if (Array.length array) > 0 then
- let n = Array.length array
- in
- Format.fprintf fmt beg_f;
- for i = 0 to n - 2 do
- Format.fprintf fmt "@[%a@]" printer (i, array.(i)) ;
- Format.fprintf fmt sep_f
- done ;
- Format.fprintf fmt "@[%a@]" printer (n-1, array.(n-1));
- Format.fprintf fmt end_f
-
-(* Local Variables: *)
-(* compile-command:"make -C .." *)
-(* End: *)
diff --git a/src/Print.mli b/src/Print.mli
deleted file mode 100644
index 81aba959ea93b4ae662baf53491e5f6d7ad4dbf3..0000000000000000000000000000000000000000
--- a/src/Print.mli
+++ /dev/null
@@ -1,131 +0,0 @@
-(* $Id$ *)
-
-(*
- * Copyright (c) 2009 CNRS & Université Bordeaux 1.
- *
- * Author(s): Grégoire Sutre <gregoire.sutre@labri.fr>
- *
- * Permission to use, copy, modify, and distribute this software for any
- * purpose with or without fee is hereby granted, provided that the above
- * copyright notice and this permission notice appear in all copies.
- *
- * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
- * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
- * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
- * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
- * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
- * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
- * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
- *)
-
-
-(**
- Signatures and helper functions for pretty-printing.
-
- This module follows the standard OCaml pretty-printing facility provided in
- the module [Format] of the standard library. In particular, pretty-printing
- commands assume that there is an opened pretty-printing box. This permits
- more flexibility, since the choice of the enclosing pretty-printing box may
- depend on the context.
-
- @see <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Format.html> Format
- *)
-
-
-(** Signature for a type equipped with a pretty-printing function. *)
-module type PRINTABLE_TYPE =
-sig
- (** The type. *)
- type t
-
- (** A pretty-printer for this type. This function prints values of
- type [t] in the current pretty-printing box. *) val print :
- Format.formatter -> t -> unit end
-
-
-(** Transform a pretty-printer into a string converter. *)
-val string_converter_from_printer :
- (Format.formatter -> 'a -> unit) -> 'a -> string
-
-(** [hashtbl_printer_from_printer beg sep endf printer] returns a
- pretty-printer for hashtbls of type [('a,'b) Hashtbl.t], given a three formatters
- [beg], [sep] and [endf], and a pretty-printer [printer] for values of
- type [('a,'b)]. The resulting pretty-printer first prints [beg], then each
- element of its argument list with [sep] between each element, and
- finally prints [endf]. Each element in the hashtbl is printed in a new
- enclosing pretty-printing box. In other words,
- [hashtbl_printer_from_printer sep printer fmt [{k1|->v1; ...; kn|->vn}]] is
- equivalent to [
- begin
- Format.fprintf fmt beg;
- Format.fprintf fmt "@[%a@]" printer (k1,v1) ;
- Format.fprintf fmt sep ;
- ... ;
- Format.fprintf fmt sep ;
- Format.fprintf fmt "@[%a@]" printer (kn,vn);
- Format.fprintf fmt endf;
- end
- ]. Note that the separator [sep] may contain pretty-printing commands. For
- instance [";@ "] could be used as a separator argument to this function.
- *)
-val hashtbl_printer_from_printer :
- (unit, Format.formatter, unit) format ->
- (unit, Format.formatter, unit) format ->
- (unit, Format.formatter, unit) format ->
- (Format.formatter -> ('a*'b) -> unit) ->
- Format.formatter -> ('a,'b) Hashtbl.t -> unit
-
-(** [list_printer_from_printer beg sep endf printer] returns a
- pretty-printer for lists of type ['a list], given three formatters
- [beg], [sep] and [endf], and a pretty-printer [printer] for values of
- type ['a]. The resulting pretty-printer first prints [beg], then each
- element of its argument list with [sep] between each element, and
- finally prints [endf]. Each element in the list is printed in a new
- enclosing pretty-printing box. In other words,
- [list_printer_from_printer beg sep endf printer fmt [a1; ...; aN]] is
- equivalent to [
- begin
- Format.fprintf fmt beg;
- Format.fprintf fmt "@[%a@]" printer a1 ;
- Format.fprintf fmt sep ;
- ... ;
- Format.fprintf fmt sep ;
- Format.fprintf fmt "@[%a@]" printer aN
- Format.fprintf fmt endf;
- end
- ]. Note that the separator [sep] may contain pretty-printing commands. For
- instance [";@ "] could be used as a separator argument to this function.
- *)
-val list_printer_from_printer :
- (unit, Format.formatter, unit) format ->
- (unit, Format.formatter, unit) format ->
- (unit, Format.formatter, unit) format ->
- (Format.formatter -> 'a -> unit) ->
- Format.formatter -> 'a list -> unit
-
-(** [array_printer_from_printer sep printer] returns a pretty-printer
- for arrays of type ['a array], given three formatters [beg], [sep] and
- [endf], and a pretty-printer [printer] for values of type [int * 'a].
- The resulting pretty-printer first prints [beg], then prints each pair
- [(i, a.(i))] of its argument array [a] and prints [sep] between each
- pair and finally prints [endf]. Each pair in the array is printed in
- a new enclosing pretty-printing box. In other words,
- [array_printer_from_printer beg sep end printer fmt [|a1; ...; aN|]] is
- equivalent to [
- begin
- Format.fprintf fmt beg;
- Format.fprintf fmt "@[%a@]" printer (0, a1) ;
- Format.fprintf fmt sep ;
- ... ;
- Format.fprintf fmt sep ;
- Format.fprintf fmt "@[%a@]" printer (N-1, aN)
- Format.fprintf fmt endf;
- end
- ]. Note that the separator [sep] may contain pretty-printing commands.
- For instance [";@ "] could be used as a separator argument to this function.
-*)
-val
- array_printer_from_printer : (unit, Format.formatter, unit) format ->
- (unit, Format.formatter, unit) format -> (unit, Format.formatter,
- unit) format -> (Format.formatter -> (int * 'a) -> unit) ->
- Format.formatter -> 'a array -> unit
diff --git a/src/access.ml b/src/access.ml
index 3432bf9c7fd047389a4e31e99d7bd8dfe6be3e14..3efc7caefb807f21551579cdb702b31af064ecd5 100755
--- a/src/access.ml
+++ b/src/access.ml
@@ -1,24 +1,13 @@
-(* ----------------------------------------------------------------------------
- * SchedMCore - A MultiCore Scheduling Framework
- * Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
- *
- * This file is part of Prelude
- *
- * Prelude is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public License
- * as published by the Free Software Foundation ; either version 2 of
- * the License, or (at your option) any later version.
- *
- * Prelude is distributed in the hope that it will be useful, but
- * WITHOUT ANY WARRANTY ; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this program ; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
- * USA
- *---------------------------------------------------------------------------- *)
+(********************************************************************)
+(* *)
+(* 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. *)
+(* *)
+(********************************************************************)
(** Access checking module. Done after typing. Generates dimension constraints stored in nodes *)
diff --git a/src/backends/C/c_backend.ml b/src/backends/C/c_backend.ml
index 62509da967cd798d6bc4ae62506c7b43fef6ac32..932e8033a0f5529c5cb932548db896a401060ce1 100644
--- a/src/backends/C/c_backend.ml
+++ b/src/backends/C/c_backend.ml
@@ -1,27 +1,13 @@
-(* ----------------------------------------------------------------------------
- * SchedMCore - A MultiCore Scheduling Framework
- * Copyright (C) 2009-2013, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
- * Copyright (C) 2012-2013, INPT, Toulouse, FRANCE
- *
- * This file is part of Prelude
- *
- * Prelude is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public License
- * as published by the Free Software Foundation ; either version 2 of
- * the License, or (at your option) any later version.
- *
- * Prelude is distributed in the hope that it will be useful, but
- * WITHOUT ANY WARRANTY ; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this program ; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
- * USA
- *---------------------------------------------------------------------------- *)
-
-(* This module is used for the lustre to C compiler *)
+(********************************************************************)
+(* *)
+(* 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
(********************************************************************************************)
diff --git a/src/backends/C/c_backend_common.ml b/src/backends/C/c_backend_common.ml
index 22f6860a8889539bb9942f5d9e7c46fb274787db..0299ea40688ec563c58edbcf9a9552d101c54531 100644
--- a/src/backends/C/c_backend_common.ml
+++ b/src/backends/C/c_backend_common.ml
@@ -1,3 +1,14 @@
+(********************************************************************)
+(* *)
+(* 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
diff --git a/src/backends/C/c_backend_header.ml b/src/backends/C/c_backend_header.ml
index 9e1c476d27992bc590f635f8aab42196e36f24cd..1147e9a93d7a2223d01b6f87d5ec827136f76e9b 100644
--- a/src/backends/C/c_backend_header.ml
+++ b/src/backends/C/c_backend_header.ml
@@ -1,3 +1,14 @@
+(********************************************************************)
+(* *)
+(* 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
diff --git a/src/backends/C/c_backend_main.ml b/src/backends/C/c_backend_main.ml
index 6680bdf0b622985ab84b622d1c8fe08f28c285a6..2dde47a13702ff6b08c0ab2618d1f2f17e0e4cd3 100644
--- a/src/backends/C/c_backend_main.ml
+++ b/src/backends/C/c_backend_main.ml
@@ -1,3 +1,14 @@
+(********************************************************************)
+(* *)
+(* 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
open Machine_code
diff --git a/src/backends/C/c_backend_makefile.ml b/src/backends/C/c_backend_makefile.ml
index 7a3fec38212659b394d7495aea86bb58fbf0d9ab..a4882e580effdcae666e4024ff566331b604cbe1 100644
--- a/src/backends/C/c_backend_makefile.ml
+++ b/src/backends/C/c_backend_makefile.ml
@@ -1,3 +1,14 @@
+(********************************************************************)
+(* *)
+(* 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
diff --git a/src/backends/C/c_backend_spec.ml b/src/backends/C/c_backend_spec.ml
index 04534deaa68f47e82a924633cac76631ce391742..e03f535bedde4a336df057a117e062b490efd553 100644
--- a/src/backends/C/c_backend_spec.ml
+++ b/src/backends/C/c_backend_spec.ml
@@ -1,3 +1,14 @@
+(********************************************************************)
+(* *)
+(* 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 Machine_code
diff --git a/src/backends/C/c_backend_src.ml b/src/backends/C/c_backend_src.ml
index d78a4c4623ec827fcdf88517692109a560e6a560..02e213724f5b78b197a9fbf2079a5a8a684d1356 100644
--- a/src/backends/C/c_backend_src.ml
+++ b/src/backends/C/c_backend_src.ml
@@ -1,3 +1,14 @@
+(********************************************************************)
+(* *)
+(* 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
diff --git a/src/horn_backend.ml b/src/backends/Horn/horn_backend.ml
similarity index 81%
rename from src/horn_backend.ml
rename to src/backends/Horn/horn_backend.ml
index a1e3df696e37e54db11086b00ea00246bfa1f110..196df1937e6f860b00f92fe4bb48939151dc85d9 100644
--- a/src/horn_backend.ml
+++ b/src/backends/Horn/horn_backend.ml
@@ -1,3 +1,17 @@
+(********************************************************************)
+(* *)
+(* 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. *)
+(* *)
+(********************************************************************)
+
+(* The compilation presented here is defined in Garoche, Gurfinkel, Kahsai,
+ HCSV'14 *)
+
open Format
open LustreSpec
open Corelang
@@ -18,10 +32,10 @@ let pp_type fmt t =
| Types.Tstatic _
| Types.Tconst _
| Types.Tarrow _
- | _ -> Format.eprintf "internal error: pp_type %a@."
- Types.print_ty t; assert false
+ | _ -> Format.eprintf "internal error: pp_type %a@."
+ Types.print_ty t; assert false
-let pp_decl_var fmt id =
+let pp_decl_var fmt id =
Format.fprintf fmt "(declare-var %s %a)"
id.var_id
pp_type id.var_type
@@ -29,52 +43,52 @@ let pp_decl_var fmt id =
let pp_var fmt id = Format.pp_print_string fmt id.var_id
-let pp_conj pp fmt l =
- match l with
+let pp_conj pp fmt l =
+ match l with
[] -> assert false
| [x] -> pp fmt x
| _ -> fprintf fmt "(and @[<v 0>%a@]@ )" (Utils.fprintf_list ~sep:" " pp) l
+
-
-let concat prefix x = if prefix = "" then x else prefix ^ "." ^ x
+let concat prefix x = if prefix = "" then x else prefix ^ "." ^ x
let rename f = (fun v -> {v with var_id = f v.var_id } )
let rename_machine p = rename (fun n -> concat p n)
let rename_machine_list p = List.map (rename_machine p)
-
+
let rename_current = rename (fun n -> n ^ "_c")
let rename_current_list = List.map rename_current
let rename_next = rename (fun n -> n ^ "_x")
let rename_next_list = List.map rename_next
-let get_machine machines node_name =
- List.find (fun m -> m.mname.node_id = node_name) machines
+let get_machine machines node_name =
+ List.find (fun m -> m.mname.node_id = node_name) machines
let full_memory_vars machines machine =
let rec aux fst prefix m =
(rename_machine_list (if fst then prefix else concat prefix m.mname.node_id) m.mmemory) @
- List.fold_left (fun accu (id, (n, _)) ->
- let name = node_name n in
+ List.fold_left (fun accu (id, (n, _)) ->
+ let name = node_name n in
if name = "_arrow" then accu else
let machine_n = get_machine machines name in
- ( aux false (concat prefix (if fst then id else concat m.mname.node_id id)) machine_n ) @ accu
- ) [] (m.minstances)
+ ( aux false (concat prefix (if fst then id else concat m.mname.node_id id)) machine_n ) @ accu
+ ) [] (m.minstances)
in
aux true machine.mname.node_id machine
-let stateless_vars machines m =
+let stateless_vars machines m =
(rename_machine_list m.mname.node_id m.mstep.step_inputs)@
(rename_machine_list m.mname.node_id m.mstep.step_outputs)
-
-let step_vars machines m =
+
+let step_vars machines m =
(stateless_vars machines m)@
- (rename_current_list (full_memory_vars machines m)) @
- (rename_next_list (full_memory_vars machines m))
-
-let init_vars machines m =
- (stateless_vars machines m) @ (rename_next_list (full_memory_vars machines m))
-
+ (rename_current_list (full_memory_vars machines m)) @
+ (rename_next_list (full_memory_vars machines m))
+
+let init_vars machines m =
+ (stateless_vars machines m) @ (rename_next_list (full_memory_vars machines m))
+
(********************************************************************************************)
(* Instruction Printing functions *)
(********************************************************************************************)
@@ -107,13 +121,13 @@ let rec pp_horn_const fmt c =
let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v =
match v with
| Cst c -> pp_horn_const fmt c
- | Array _
+ | Array _
| Access _ -> assert false (* no arrays *)
| Power (v, n) -> assert false
| LocalVar v -> pp_var fmt (rename_machine self v)
| StateVar v ->
if Types.is_array_type v.var_type
- then assert false
+ then assert false
else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
| Fun (n, vl) -> Format.fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl
@@ -133,10 +147,10 @@ let rec pp_value_suffix self pp_value fmt value =
*)
let pp_assign m self pp_var fmt var_type var_name value =
fprintf fmt "(= %a %a)" (pp_horn_val ~is_lhs:true self pp_var) var_name (pp_value_suffix self pp_var) value
-
-let pp_instance_call
+
+let pp_instance_call
machines ?(init=false) m self fmt i (inputs: value_t list) (outputs: var_decl list) =
- try (* stateful node instance *)
+ try (* stateful node instance *)
begin
let (n,_) = List.assoc i m.minstances in
match node_name n, inputs, outputs with
@@ -145,65 +159,65 @@ let pp_instance_call
pp_assign
m
self
- (pp_horn_var m)
+ (pp_horn_var m)
fmt
o.var_type (LocalVar o) i1
else
pp_assign
m self (pp_horn_var m) fmt
o.var_type (LocalVar o) i2
-
+
end
- | name, _, _ ->
+ | name, _, _ ->
begin
let target_machine = List.find (fun m -> m.mname.node_id = name) machines in
if init then
Format.fprintf fmt "(%a %a%t%a%t%a)"
- pp_machine_init_name (node_name n)
+ pp_machine_init_name (node_name n)
(* inputs *)
- (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
+ (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
inputs
- (Utils.pp_final_char_if_non_empty " " inputs)
+ (Utils.pp_final_char_if_non_empty " " inputs)
(* outputs *)
- (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
+ (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
(List.map (fun v -> LocalVar v) outputs)
(Utils.pp_final_char_if_non_empty " " outputs)
(* memories (next) *)
(Utils.fprintf_list ~sep:" " pp_var) (
- rename_machine_list
- (concat m.mname.node_id i)
+ rename_machine_list
+ (concat m.mname.node_id i)
(rename_next_list (full_memory_vars machines target_machine)
- )
+ )
)
else
Format.fprintf fmt "(%a %a%t%a%t%a)"
- pp_machine_step_name (node_name n)
+ pp_machine_step_name (node_name n)
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs
- (Utils.pp_final_char_if_non_empty " " inputs)
- (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
+ (Utils.pp_final_char_if_non_empty " " inputs)
+ (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
(List.map (fun v -> LocalVar v) outputs)
(Utils.pp_final_char_if_non_empty " " outputs)
(Utils.fprintf_list ~sep:" " pp_var) (
- (rename_machine_list
- (concat m.mname.node_id i)
+ (rename_machine_list
+ (concat m.mname.node_id i)
(rename_current_list (full_memory_vars machines target_machine))
- ) @
- (rename_machine_list
- (concat m.mname.node_id i)
+ ) @
+ (rename_machine_list
+ (concat m.mname.node_id i)
(rename_next_list (full_memory_vars machines target_machine))
- )
+ )
)
-
+
end
end
with Not_found -> ( (* stateless node instance *)
let (n,_) = List.assoc i m.mcalls in
Format.fprintf fmt "(%s %a%t%a)"
(node_name n)
- (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
+ (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
inputs
- (Utils.pp_final_char_if_non_empty " " inputs)
- (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
+ (Utils.pp_final_char_if_non_empty " " inputs)
+ (Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
(List.map (fun v -> LocalVar v) outputs)
)
@@ -225,7 +239,7 @@ let rec pp_conditional machines ?(init=false) (m: machine_t) self fmt c tl el =
(Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init m self)) el
and pp_machine_instr machines ?(init=false) (m: machine_t) self fmt instr =
- match instr with
+ match instr with
| MReset i ->
pp_machine_init m self fmt i
| MLocalAssign (i,v) ->
@@ -236,7 +250,7 @@ and pp_machine_instr machines ?(init=false) (m: machine_t) self fmt instr =
pp_assign
m self (pp_horn_var m) fmt
i.var_type (StateVar i) v
- | MStep ([i0], i, vl) when Basic_library.is_internal_fun i ->
+ | MStep ([i0], i, vl) when Basic_library.is_internal_fun i ->
assert false (* This should not happen anymore *)
| MStep (il, i, vl) ->
pp_instance_call machines ~init:init m self fmt i vl il
@@ -251,44 +265,44 @@ and pp_machine_instr machines ?(init=false) (m: machine_t) self fmt instr =
(**************************************************************)
+
+let is_stateless m = m.minstances = [] && m.mmemory = []
-let is_stateless m = m.minstances = [] && m.mmemory = []
-
-(* Print the machine m:
+(* Print the machine m:
two functions: m_init and m_step
- m_init is a predicate over m memories
- m_step is a predicate over old_memories, inputs, new_memories, outputs
We first declare all variables then the two /rules/.
*)
-let print_machine machines fmt m =
+let print_machine machines fmt m =
let pp_instr init = pp_machine_instr machines ~init:init m in
- if m.mname.node_id = arrow_id then
+ if m.mname.node_id = arrow_id then
(* We don't print arrow function *)
()
- else
- begin
+ else
+ begin
Format.fprintf fmt "; %s@." m.mname.node_id;
(* Printing variables *)
- Utils.fprintf_list ~sep:"@." pp_decl_var fmt
+ Utils.fprintf_list ~sep:"@." pp_decl_var fmt
((step_vars machines m)@
(rename_machine_list m.mname.node_id m.mstep.step_locals));
Format.pp_print_newline fmt ();
-
-
+
+
if is_stateless m then
begin
(* Declaring single predicate *)
Format.fprintf fmt "(declare-rel %a (%a))@."
pp_machine_stateless_name m.mname.node_id
- (Utils.fprintf_list ~sep:" " pp_type)
+ (Utils.fprintf_list ~sep:" " pp_type)
(List.map (fun v -> v.var_type) (stateless_vars machines m));
-
+
(* Rule for single predicate *)
Format.fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a %a)@]@.))@.@."
- (pp_conj (pp_instr
- true (* In this case, the boolean init can be set to true or false.
+ (pp_conj (pp_instr
+ true (* In this case, the boolean init can be set to true or false.
The node is stateless. *)
m.mname.node_id)
)
@@ -296,19 +310,19 @@ let print_machine machines fmt m =
pp_machine_stateless_name m.mname.node_id
(Utils.fprintf_list ~sep:" " pp_var) (stateless_vars machines m);
end
- else
+ else
begin
(* Declaring predicate *)
Format.fprintf fmt "(declare-rel %a (%a))@."
pp_machine_init_name m.mname.node_id
- (Utils.fprintf_list ~sep:" " pp_type)
+ (Utils.fprintf_list ~sep:" " pp_type)
(List.map (fun v -> v.var_type) (init_vars machines m));
-
+
Format.fprintf fmt "(declare-rel %a (%a))@."
pp_machine_step_name m.mname.node_id
- (Utils.fprintf_list ~sep:" " pp_type)
+ (Utils.fprintf_list ~sep:" " pp_type)
(List.map (fun v -> v.var_type) (step_vars machines m));
-
+
Format.pp_print_newline fmt ();
(* Rule for init *)
@@ -328,19 +342,19 @@ let print_machine machines fmt m =
| [] -> ()
| assertsl -> begin
let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id pp_var in
-
+
Format.fprintf fmt "; Asserts@.";
Format.fprintf fmt "(assert @[<v 2>%a@]@ )@.@.@."
(pp_conj pp_val) assertsl;
-
- (** TEME: the following code is the one we described. But it generates a segfault in z3
+
+ (** TEME: the following code is the one we described. But it generates a segfault in z3
Format.fprintf fmt "; Asserts for init@.";
Format.fprintf fmt "@[<v 2>(assert (=> @ (and @[<v 0>%a@]@ (%a %a))@ %a@]@.))@.@.@."
(Utils.fprintf_list ~sep:"@ " (pp_instr true m.mname.node_id)) m.mstep.step_instrs
pp_machine_init_name m.mname.node_id
(Utils.fprintf_list ~sep:" " pp_var) (init_vars machines m)
- (pp_conj pp_val) assertsl;
-
+ (pp_conj pp_val) assertsl;
+
Format.fprintf fmt "; Asserts for step@.";
Format.fprintf fmt "@[<v 2>(assert (=> @ (and @[<v 0>%a@]@ (%a %a))@ %a@]@.))@.@."
(Utils.fprintf_list ~sep:"@ " (pp_instr false m.mname.node_id)) m.mstep.step_instrs
@@ -351,18 +365,18 @@ let print_machine machines fmt m =
*)
end
);
-
+
(*
match m.mspec with
None -> () (* No node spec; we do nothing *)
- | Some {requires = []; ensures = [EnsuresExpr e]; behaviors = []} ->
- (
+ | Some {requires = []; ensures = [EnsuresExpr e]; behaviors = []} ->
+ (
(* For the moment, we only deal with simple case: single ensures, no other parameters *)
()
-
+
)
| _ -> () (* Other cases give nothing *)
-*)
+*)
end
end
@@ -374,20 +388,20 @@ let collecting_semantics machines fmt node machine =
let main_output =
rename_machine_list machine.mname.node_id machine.mstep.step_outputs
in
- let main_output_dummy =
+ let main_output_dummy =
rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
in
- let main_memory_next =
+ let main_memory_next =
(rename_next_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
main_output
in
- let main_memory_current =
+ let main_memory_current =
(rename_current_list (* machine.mname.node_id *) (full_memory_vars machines machine)) @
main_output_dummy
in
(* Special case when the main node is stateless *)
- let init_name, step_name =
+ let init_name, step_name =
if is_stateless machine then
pp_machine_stateless_name, pp_machine_stateless_name
else
@@ -395,9 +409,9 @@ let collecting_semantics machines fmt node machine =
in
Format.fprintf fmt "(declare-rel MAIN (%a))@."
- (Utils.fprintf_list ~sep:" " pp_type)
+ (Utils.fprintf_list ~sep:" " pp_type)
(List.map (fun v -> v.var_type) main_memory_next);
-
+
Format.fprintf fmt "; Initial set@.";
Format.fprintf fmt "(declare-rel INIT_STATE ())@.";
Format.fprintf fmt "(rule INIT_STATE)@.";
@@ -408,18 +422,18 @@ let collecting_semantics machines fmt node machine =
Format.fprintf fmt "; Inductive def@.";
(Utils.fprintf_list ~sep:" " (fun fmt v -> Format.fprintf fmt "%a@." pp_decl_var v)) fmt main_output_dummy;
- Format.fprintf fmt
+ Format.fprintf fmt
"@[<v 2>(rule (=> @ (and @[<v 0>(MAIN %a)@ (@[<v 0>%a %a@])@]@ )@ (MAIN %a)@]@.))@.@."
(Utils.fprintf_list ~sep:" " pp_var) main_memory_current
step_name node
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine)
- (Utils.fprintf_list ~sep:" " pp_var) main_memory_next
+ (Utils.fprintf_list ~sep:" " pp_var) main_memory_next
let check_prop machines fmt node machine =
let main_output =
rename_machine_list machine.mname.node_id machine.mstep.step_outputs
in
- let main_memory_next =
+ let main_memory_next =
(rename_next_list (full_memory_vars machines machine)) @ main_output
in
Format.fprintf fmt "; Property def@.";
@@ -428,7 +442,8 @@ let check_prop machines fmt node machine =
(pp_conj pp_var) main_output
(Utils.fprintf_list ~sep:" " pp_var) main_memory_next
;
- Format.fprintf fmt "(query ERR)@."
+ if !Options.horn_queries then
+ Format.fprintf fmt "(query ERR)@."
let cex_computation machines fmt node machine =
@@ -437,24 +452,24 @@ let cex_computation machines fmt node machine =
let cex_input =
rename_machine_list machine.mname.node_id machine.mstep.step_inputs
in
- let cex_input_dummy =
+ let cex_input_dummy =
rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_inputs
in
let cex_output =
rename_machine_list machine.mname.node_id machine.mstep.step_outputs
in
- let cex_output_dummy =
+ let cex_output_dummy =
rename_machine_list ("dummy" ^ machine.mname.node_id) machine.mstep.step_outputs
in
- let cex_memory_next =
+ let cex_memory_next =
cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output
in
- let cex_memory_current =
+ let cex_memory_current =
cex_input_dummy @ (rename_current_list (full_memory_vars machines machine)) @ cex_output_dummy
in
(* Special case when the cex node is stateless *)
- let init_name, step_name =
+ let init_name, step_name =
if is_stateless machine then
pp_machine_stateless_name, pp_machine_stateless_name
else
@@ -462,9 +477,9 @@ let cex_computation machines fmt node machine =
in
Format.fprintf fmt "(declare-rel CEX (Int %a))@.@."
- (Utils.fprintf_list ~sep:" " pp_type)
+ (Utils.fprintf_list ~sep:" " pp_type)
(List.map (fun v -> v.var_type) cex_memory_next);
-
+
Format.fprintf fmt "; Initial set@.";
Format.fprintf fmt "@[<v 2>(rule (=> @ (and @[<v 0>INIT_STATE@ (@[<v 0>%a %a@])@]@ )@ (CEX 0 %a)@]@.))@.@."
init_name node
@@ -475,12 +490,12 @@ let cex_computation machines fmt node machine =
(* Declare dummy inputs. Outputs should have been declared previously with collecting sem *)
(Utils.fprintf_list ~sep:" " (fun fmt v -> Format.fprintf fmt "%a@." pp_decl_var v)) fmt cex_input_dummy;
Format.fprintf fmt "(declare-var cexcpt Int)@.";
- Format.fprintf fmt
+ Format.fprintf fmt
"@[<v 2>(rule (=> @ (and @[<v 0>(CEX cexcpt %a)@ (@[<v 0>%a %a@])@]@ )@ (CEX (+ 1 cexcpt) %a)@]@.))@.@."
(Utils.fprintf_list ~sep:" " pp_var) cex_memory_current
step_name node
(Utils.fprintf_list ~sep:" " pp_var) (step_vars machines machine)
- (Utils.fprintf_list ~sep:" " pp_var) cex_memory_next
+ (Utils.fprintf_list ~sep:" " pp_var) cex_memory_next
let get_cex machines fmt node machine =
let cex_input =
@@ -489,7 +504,7 @@ let get_cex machines fmt node machine =
let cex_output =
rename_machine_list machine.mname.node_id machine.mstep.step_outputs
in
- let cex_memory_next =
+ let cex_memory_next =
cex_input @ (rename_next_list (full_memory_vars machines machine)) @ cex_output
in
Format.fprintf fmt "; Property def@.";
@@ -498,11 +513,12 @@ let get_cex machines fmt node machine =
(pp_conj pp_var) cex_output
(Utils.fprintf_list ~sep:" " pp_var) cex_memory_next
;
- Format.fprintf fmt "(query CEXTRACE)@."
+ if !Options.horn_queries then
+ Format.fprintf fmt "(query CEXTRACE)@."
-let main_print machines fmt =
-if !Options.main_node <> "" then
+let main_print machines fmt =
+if !Options.main_node <> "" then
begin
let node = !Options.main_node in
let machine = get_machine machines node in
@@ -518,35 +534,35 @@ end
let translate fmt basename prog machines =
List.iter (print_machine machines fmt) (List.rev machines);
-
- main_print machines fmt
+
+ main_print machines fmt
let traces_file fmt basename prog machines =
- Format.fprintf fmt
+ Format.fprintf fmt
"; Horn code traceability generated by %s@.; SVN version number %s@.@."
- (Filename.basename Sys.executable_name)
+ (Filename.basename Sys.executable_name)
Version.number;
(* We extract the annotation dealing with traceability *)
- let machines_traces = List.map (fun m ->
- let traces : (ident * expr) list=
+ let machines_traces = List.map (fun m ->
+ let traces : (ident * expr) list=
let all_annots = List.flatten (List.map (fun ann -> ann.annots) m.mannot) in
- let filtered =
- List.filter (fun (kwds, _) -> kwds = ["horn_backend";"trace"]) all_annots
+ let filtered =
+ List.filter (fun (kwds, _) -> kwds = ["horn_backend";"trace"]) all_annots
in
let content = List.map snd filtered in
(* Elements are supposed to be a pair (tuple): variable, expression *)
- List.map (fun ee ->
- match ee.eexpr_quantifiers, ee.eexpr_qfexpr.expr_desc with
+ List.map (fun ee ->
+ match ee.eexpr_quantifiers, ee.eexpr_qfexpr.expr_desc with
| [], Expr_tuple [v;e] -> (
- match v.expr_desc with
- | Expr_ident vid -> vid, e
+ match v.expr_desc with
+ | Expr_ident vid -> vid, e
| _ -> assert false )
| _ -> assert false)
content
in
-
+
m, traces
) machines
@@ -556,22 +572,22 @@ let traces_file fmt basename prog machines =
let compute_mems m =
let rec aux fst prefix m =
(List.map (fun mem -> (prefix, mem)) m.mmemory) @
- List.fold_left (fun accu (id, (n, _)) ->
- let name = node_name n in
+ List.fold_left (fun accu (id, (n, _)) ->
+ let name = node_name n in
if name = "_arrow" then accu else
let machine_n = get_machine machines name in
- ( aux false ((id,machine_n)::prefix) machine_n )
+ ( aux false ((id,machine_n)::prefix) machine_n )
@ accu
- ) [] m.minstances
+ ) [] m.minstances
in
aux true [] m
in
List.iter (fun m ->
Format.fprintf fmt "; Node %s@." m.mname.node_id;
-
- let memories_old =
- List.map (fun (p, v) ->
+
+ let memories_old =
+ List.map (fun (p, v) ->
let machine = match p with | [] -> m | (_,m')::_ -> m' in
let traces = List.assoc machine machines_traces in
if List.mem_assoc v.var_id traces then
@@ -580,20 +596,20 @@ let traces_file fmt basename prog machines =
else
(* We keep the variable as is: we create an expression v *)
p, mkexpr Location.dummy_loc (Expr_ident v.var_id)
-
- ) (compute_mems m)
+
+ ) (compute_mems m)
in
let memories_next = (* We remove the topest pre in each expression *)
- List.map
- (fun (prefix, ee) ->
- match ee.expr_desc with
- | Expr_pre e -> prefix, e
- | _ -> Format.eprintf
- "Mem Failure: (prefix: %a, eexpr: %a)@.@?"
- (Utils.fprintf_list ~sep:","
- (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id ))
- (List.rev prefix)
- Printers.pp_expr ee;
+ List.map
+ (fun (prefix, ee) ->
+ match ee.expr_desc with
+ | Expr_pre e -> prefix, e
+ | _ -> Format.eprintf
+ "Mem Failure: (prefix: %a, eexpr: %a)@.@?"
+ (Utils.fprintf_list ~sep:","
+ (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id ))
+ (List.rev prefix)
+ Printers.pp_expr ee;
assert false)
memories_old
in
@@ -629,9 +645,9 @@ let traces_file fmt basename prog machines =
(Utils.fprintf_list ~sep:" " pp_var) (m.mstep.step_inputs@m.mstep.step_outputs)
(fun fmt -> match memories_old with [] -> () | _ -> fprintf fmt " ")
(Utils.fprintf_list ~sep:" " (fun fmt (prefix,ee) -> fprintf fmt "%a(%a)" pp_prefix_rev prefix Printers.pp_expr ee)) (memories_old@memories_next);
- Format.pp_print_newline fmt ();
+ Format.pp_print_newline fmt ();
) (List.rev machines);
-
+
(* Local Variables: *)
(* compile-command:"make -C .." *)
diff --git a/src/java_backend.ml b/src/backends/Java/java_backend.ml
similarity index 92%
rename from src/java_backend.ml
rename to src/backends/Java/java_backend.ml
index 01bdd4fd5d109da3bb43d2983b63d9f00dcad8d4..5708cb42ad4b47e8f30d490452d394918d7cde58 100644
--- a/src/java_backend.ml
+++ b/src/backends/Java/java_backend.ml
@@ -1,27 +1,13 @@
-(* ----------------------------------------------------------------------------
- * SchedMCore - A MultiCore Scheduling Framework
- * Copyright (C) 2009-2013, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
- * Copyright (C) 2012-2013, INPT, Toulouse, FRANCE
- *
- * This file is part of Prelude
- *
- * Prelude is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public License
- * as published by the Free Software Foundation ; either version 2 of
- * the License, or (at your option) any later version.
- *
- * Prelude is distributed in the hope that it will be useful, but
- * WITHOUT ANY WARRANTY ; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this program ; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
- * USA
- *---------------------------------------------------------------------------- *)
-
-(* This module is used for the lustre to Java compiler *)
+(********************************************************************)
+(* *)
+(* 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 Utils
diff --git a/src/basic_library.ml b/src/basic_library.ml
index a8b78a6b10707f081cb6c230ff88554dfd8e2fdc..02dde4e6f81c1b16256eb992eafb623a7b775d5f 100644
--- a/src/basic_library.ml
+++ b/src/basic_library.ml
@@ -1,27 +1,15 @@
-(* ----------------------------------------------------------------------------
- * SchedMCore - A MultiCore Scheduling Framework
- * Copyright (C) 2009-2013, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
- * Copyright (C) 2012-2013, INPT, Toulouse, FRANCE
- *
- * This file is part of Prelude
- *
- * Prelude is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public License
- * as published by the Free Software Foundation ; either version 2 of
- * the License, or (at your option) any later version.
- *
- * Prelude is distributed in the hope that it will be useful, but
- * WITHOUT ANY WARRANTY ; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this program ; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
- * USA
- *---------------------------------------------------------------------------- *)
-
-(* This module is used for the lustre to C compiler *)
+(********************************************************************)
+(* *)
+(* The LustreC compiler toolset / The LustreC Development Team *)
+(* Copyright 2012 - -- ONERA - CNRS - INPT - LIFL *)
+(* *)
+(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)
+(* under the terms of the GNU Lesser General Public License *)
+(* version 2.1. *)
+(* *)
+(********************************************************************)
+
+(* Parts of this file come from the Prelude compiler *)
open LustreSpec
open Type_predef
diff --git a/src/causality.ml b/src/causality.ml
index b15b178c696790c5ee534ba54ac8a4b95d21eaf6..489027f4d43ba17da80dd3623d838e2048af1a19 100644
--- a/src/causality.ml
+++ b/src/causality.ml
@@ -1,24 +1,15 @@
-(* ----------------------------------------------------------------------------
- * SchedMCore - A MultiCore Scheduling Framework
- * Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
- *
- * This file is part of Prelude
- *
- * Prelude is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public License
- * as published by the Free Software Foundation ; either version 2 of
- * the License, or (at your option) any later version.
- *
- * Prelude is distributed in the hope that it will be useful, but
- * WITHOUT ANY WARRANTY ; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this program ; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
- * USA
- *---------------------------------------------------------------------------- *)
+(********************************************************************)
+(* *)
+(* The LustreC compiler toolset / The LustreC Development Team *)
+(* Copyright 2012 - -- ONERA - CNRS - INPT - LIFL *)
+(* *)
+(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)
+(* under the terms of the GNU Lesser General Public License *)
+(* version 2.1. *)
+(* *)
+(* This file was originally from the Prelude compiler *)
+(* *)
+(********************************************************************)
(** Simple modular syntactic causality analysis. Can reject correct
diff --git a/src/clock_calculus.ml b/src/clock_calculus.ml
index ef6c22a9ac9136bb4e8cb1347624bc45972715f3..9e2cb8e65443609930b479f16b219c86bc7b03a4 100755
--- a/src/clock_calculus.ml
+++ b/src/clock_calculus.ml
@@ -1,24 +1,16 @@
-(* ----------------------------------------------------------------------------
- * SchedMCore - A MultiCore Scheduling Framework
- * Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
- *
- * This file is part of Prelude
- *
- * Prelude is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public License
- * as published by the Free Software Foundation ; either version 2 of
- * the License, or (at your option) any later version.
- *
- * Prelude is distributed in the hope that it will be useful, but
- * WITHOUT ANY WARRANTY ; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this program ; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
- * USA
- *---------------------------------------------------------------------------- *)
+(********************************************************************)
+(* *)
+(* The LustreC compiler toolset / The LustreC Development Team *)
+(* Copyright 2012 - -- ONERA - CNRS - INPT - LIFL *)
+(* *)
+(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)
+(* under the terms of the GNU Lesser General Public License *)
+(* version 2.1. *)
+(* *)
+(* This file was originally from the Prelude compiler *)
+(* *)
+(********************************************************************)
+
(** Main clock-calculus module. Based on type inference algorithms with
destructive unification. Uses a bit of subtyping for periodic clocks. *)
diff --git a/src/clock_predef.ml b/src/clock_predef.ml
index 3ed7fa9c0b8c04008d483a051cce02c863ae642c..155dba080c949b93bbcc6d3deb51dbf8981ab7f8 100644
--- a/src/clock_predef.ml
+++ b/src/clock_predef.ml
@@ -1,24 +1,15 @@
-(* ----------------------------------------------------------------------------
- * SchedMCore - A MultiCore Scheduling Framework
- * Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
- *
- * This file is part of Prelude
- *
- * Prelude is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public License
- * as published by the Free Software Foundation ; either version 2 of
- * the License, or (at your option) any later version.
- *
- * Prelude is distributed in the hope that it will be useful, but
- * WITHOUT ANY WARRANTY ; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this program ; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
- * USA
- *---------------------------------------------------------------------------- *)
+(********************************************************************)
+(* *)
+(* The LustreC compiler toolset / The LustreC Development Team *)
+(* Copyright 2012 - -- ONERA - CNRS - INPT - LIFL *)
+(* *)
+(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)
+(* under the terms of the GNU Lesser General Public License *)
+(* version 2.1. *)
+(* *)
+(* This file was originally from the Prelude compiler *)
+(* *)
+(********************************************************************)
(** Predefined operator clocks *)
open Clocks
diff --git a/src/clocks.ml b/src/clocks.ml
index 7c0fc38c30e85077906cb98333e83dc95fd4e0be..ca0e0a44e56d795d4705dfea553406ce8e03e12e 100755
--- a/src/clocks.ml
+++ b/src/clocks.ml
@@ -1,24 +1,15 @@
-(* ----------------------------------------------------------------------------
- * SchedMCore - A MultiCore Scheduling Framework
- * Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
- *
- * This file is part of Prelude
- *
- * Prelude is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public License
- * as published by the Free Software Foundation ; either version 2 of
- * the License, or (at your option) any later version.
- *
- * Prelude is distributed in the hope that it will be useful, but
- * WITHOUT ANY WARRANTY ; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this program ; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
- * USA
- *---------------------------------------------------------------------------- *)
+(********************************************************************)
+(* *)
+(* The LustreC compiler toolset / The LustreC Development Team *)
+(* Copyright 2012 - -- ONERA - CNRS - INPT - LIFL *)
+(* *)
+(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)
+(* under the terms of the GNU Lesser General Public License *)
+(* version 2.1. *)
+(* *)
+(* This file was originally from the Prelude compiler *)
+(* *)
+(********************************************************************)
(** Clocks definitions and a few utility functions on clocks. *)
open Utils
diff --git a/src/com_protocol.ml b/src/com_protocol.ml
deleted file mode 100644
index f14b8407375e5e3a61b3c5011f27c57d1ec2a38a..0000000000000000000000000000000000000000
--- a/src/com_protocol.ml
+++ /dev/null
@@ -1,187 +0,0 @@
-(* ----------------------------------------------------------------------------
- * SchedMCore - A MultiCore Scheduling Framework
- * Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
- *
- * This file is part of Prelude
- *
- * Prelude is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public License
- * as published by the Free Software Foundation ; either version 2 of
- * the License, or (at your option) any later version.
- *
- * Prelude is distributed in the hope that it will be useful, but
- * WITHOUT ANY WARRANTY ; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this program ; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
- * USA
- *---------------------------------------------------------------------------- *)
-
-(** Compute the communication protocols of a task graph. *)
-
-open Deadlines
-open Precedence_functions
-open Corelang
-open Task_graph
-open Task_set
-open Format
-
-(* Number of times instance [n] is consumed *)
-let conso_ops ops n =
- (gops ops (n+1)) - (gops ops n)
-
-(* Lifespan of instance [n] *)
-let lifespan ti ops tj n =
- let span_start = abs_release ti n in
- if (conso_ops ops n) =0 then
- (span_start,span_start)
- else
- let first_conso_release = abs_release tj (gops ops n) in
- let span_end = first_conso_release + (conso_ops ops n) * tj.task_period in
- (span_start,span_end)
-
-(* The number of cells of the buffer *)
-let nb_cells ti ops tj =
- let total_length = (pref_size ops) + (periodicity ops) in
- let max_intersects = ref 0 in
- for k = 0 to total_length -1 do
- let (sp_start,sp_end) = lifespan ti ops tj k in
- let sp_size = sp_end - sp_start in
- (* the following is an overapproximation *)
- let approx_intersect =
- int_of_float (ceil ((float_of_int sp_size) /. (float_of_int ti.task_period)))
- in
- if approx_intersect > !max_intersects then
- max_intersects := approx_intersect
- done;
- if contains_init ops then
- !max_intersects + 1
- else
- !max_intersects
-
-(* Pattern that the writer must follow. *)
-let write_pattern ti ops tj =
- let write_pref = Array.make (pref_size ops) true in
- for k = 0 to (pref_size ops) -1 do
- if (conso_ops ops k) >= 1 then
- write_pref.(k) <- true
- else
- write_pref.(k) <- false
- done;
- let write_pat = Array.make (periodicity ops) true in
- for k = 0 to (periodicity ops) -1 do
- if (conso_ops ops (k+(pref_size ops))) >= 1 then
- write_pat.(k) <- true
- else
- write_pat.(k) <- false
- done;
- write_pref,write_pat
-
-(* Pattern that the reader must follow *)
-let read_pattern ti ops tj =
- (* TODO: concat operator ! *)
- let read_pattern_pref = ref [] in
- if (gops ops 0) > 0 then (* First reads the init of the fby/concat *)
- begin
- for k=0 to (gops ops 0)-2 do
- read_pattern_pref := false::!read_pattern_pref
- done;
- read_pattern_pref := true::!read_pattern_pref
- end;
- for k = 0 to (pref_size ops) - 1 do
- let dep_ij_k = (conso_ops ops k) in
- if dep_ij_k >= 1 then
- begin
- for k'=0 to dep_ij_k -2 do
- read_pattern_pref := false::!read_pattern_pref
- done;
- read_pattern_pref := true::!read_pattern_pref
- end
- done;
- let read_pattern_pat = ref [] in
- for k = 0 to (periodicity ops) - 1 do
- let dep_ij_k = (conso_ops ops (k+(pref_size ops))) in
- if dep_ij_k >= 1 then
- begin
- for k'=0 to dep_ij_k -2 do
- read_pattern_pat := false::!read_pattern_pat
- done;
- read_pattern_pat := true::!read_pattern_pat
- end
- done;
- (Array.of_list (List.rev !read_pattern_pref),
- Array.of_list (List.rev !read_pattern_pat))
-
-let vertex_of_vdecl t vdecl =
- match t.task_kind with
- | StdTask -> NodeVar (vdecl.var_id, t.task_id)
- | Sensor | Actuator -> Var vdecl.var_id
-
-(* Returns the initial value of a precedence annotation (if any). Assumes the
- same init value is used for each fby/concat in annots *)
-let rec init_of_annots annots =
- match annots with
- | [] -> None
- | (Gfby cst)::_ -> Some cst
- | (Gconcat cst)::_ -> Some cst
- | _::rest -> init_of_annots rest
-
-(* Computes the communication protocol of a task output *)
-let proto_output g task_set t vout =
- let vertex_out_id = vertex_of_vdecl t vout in
- let vertex_out = Hashtbl.find g.graph vertex_out_id in
- let succs = vertex_out.vertex_succs in
- Hashtbl.fold
- (fun succ_id annot protos ->
- let task_from = task_of_vertex task_set vertex_out_id in
- let task_to = task_of_vertex task_set succ_id in
- let bsize = nb_cells task_from annot task_to in
- let pref,pat = write_pattern task_from annot task_to in
- let init = init_of_annots annot in
- let proto = {wbuf_size = bsize;
- write_pref = pref;
- write_pat = pat;
- wbuf_init = init} in
- let succ_ref = vref_of_vertex_id succ_id in
- (succ_ref,proto)::protos)
- succs []
-
-(* Computes the communication protocol of a task input *)
-let proto_input g task_set t vin =
- let vertex_in_id = vertex_of_vdecl t vin in
- let vertex_in = Hashtbl.find g.graph vertex_in_id in
- let pred = vertex_in.vertex_pred in
- match pred with
- | None -> failwith "internal error"
- | Some (vpred,annot) ->
- let task_from = task_of_vertex task_set vpred in
- let task_to = task_of_vertex task_set vertex_in_id in
- let bsize = nb_cells task_from annot task_to in
- let pref,pat = read_pattern task_from annot task_to in
- let init = init_of_annots annot in
- let proto = {rbuf_size = bsize;
- change_pref = pref;
- change_pat = pat;
- rbuf_init = init} in
- let pred_ref = vref_of_vertex_id vpred in
- pred_ref, proto
-
-(* Computes the communication protocols for each variable of a task *)
-let proto_task g task_set t =
- t.task_inputs <-
- List.map (fun (vdecl,_,_) ->
- let pred, proto = proto_input g task_set t vdecl in
- (vdecl, pred, proto)) t.task_inputs;
- t.task_outputs <-
- List.map (fun (vdecl,_) -> (vdecl,proto_output g task_set t vdecl)) t.task_outputs
-
-(* Computes all the communication protocols of the task set *)
-let proto_prog g task_set =
- Hashtbl.iter (fun _ t -> proto_task g task_set t) task_set
-
-(* Local Variables: *)
-(* compile-command:"make -C .." *)
-(* End: *)
diff --git a/src/corelang.ml b/src/corelang.ml
index 6b8799391c36bf831c0c0b996f51e26416ed81de..bfb54be335a3dac095dd2f09bb6f64eac5cca568 100755
--- a/src/corelang.ml
+++ b/src/corelang.ml
@@ -1,24 +1,14 @@
-(* ----------------------------------------------------------------------------
- * SchedMCore - A MultiCore Scheduling Framework
- * Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
- *
- * This file is part of Prelude
- *
- * Prelude is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public License
- * as published by the Free Software Foundation ; either version 2 of
- * the License, or (at your option) any later version.
- *
- * Prelude is distributed in the hope that it will be useful, but
- * WITHOUT ANY WARRANTY ; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this program ; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
- * USA
- *---------------------------------------------------------------------------- *)
+(********************************************************************)
+(* *)
+(* 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 Dimension
diff --git a/src/corelang.mli b/src/corelang.mli
index 6781317f18da9c339b7d2a71db6e78ee1a841a25..80b9455c749c17a6704a989f05f6efe9a05e83cb 100755
--- a/src/corelang.mli
+++ b/src/corelang.mli
@@ -1,167 +1,17 @@
-(* ----------------------------------------------------------------------------
- * SchedMCore - A MultiCore Scheduling Framework
- * Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
- *
- * This file is part of Prelude
- *
- * Prelude is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public License
- * as published by the Free Software Foundation ; either version 2 of
- * the License, or (at your option) any later version.
- *
- * Prelude is distributed in the hope that it will be useful, but
- * WITHOUT ANY WARRANTY ; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this program ; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
- * USA
- *---------------------------------------------------------------------------- *)
+(********************************************************************)
+(* *)
+(* 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
-(*
-(** The core language and its ast. *)
-type ident = Utils.ident
-type label = Utils.ident
-type rat = Utils.rat
-type tag = Utils.tag
-
-type constant =
- | Const_int of int
- | Const_real of string
- | Const_float of float
- | Const_array of constant list
- | Const_tag of label
- | Const_struct of (label * constant) list
-
-val dummy_type_dec: type_dec
-
-type type_dec = LustreSpec.type_dec
-
-type clock_dec = LustreSpec.clock_dec
-val dummy_clock_dec: clock_dec
-
-type var_decl = LustreSpec.var_decl
-
-type expr =
- {expr_tag: tag; (* Unique identifier *)
- expr_desc: expr_desc;
- mutable expr_type: Types.type_expr;
- mutable expr_clock: Clocks.clock_expr;
- mutable expr_delay: Delay.delay_expr; (* Used for the initialisation check *)
- mutable expr_annot: LustreSpec.expr_annot option; (* Spec *)
- expr_loc: Location.t}
-and expr_desc =
-| Expr_const of constant
-| Expr_ident of ident
-| Expr_tuple of expr list
-| Expr_ite of expr * expr * expr
-| Expr_arrow of expr * expr
-| Expr_fby of expr * expr
-(*
-| Expr_struct of (label * expr) list
-| Expr_field of expr * label
-| Expr_update of expr * (label * expr)
-*)
-| Expr_array of expr list
-| Expr_access of expr * Dimension.dim_expr (* acces(e,i) is the i-th element
- of array epxression e *)
-| Expr_power of expr * Dimension.dim_expr (* power(e,n) is the array of
- size n filled with expression e *)
-| Expr_pre of expr
-| Expr_when of expr * ident * label
-| Expr_merge of ident * (label * expr) list
-| Expr_appl of call_t
-| Expr_uclock of expr * int
-| Expr_dclock of expr * int
-| Expr_phclock of expr * rat
-and call_t = ident * expr * (ident * label) option (* The third part denotes the reseting clock label and value *)
-
-type eq =
- {eq_lhs: ident list;
- eq_rhs: expr;
- eq_loc: Location.t}
-
-type assert_t =
- {
- assert_expr: expr * eq list;
- assert_loc: Location.t
- }
-
-type node_desc =
- {node_id: ident;
- mutable node_type: Types.type_expr;
- mutable node_clock: Clocks.clock_expr;
- node_inputs: var_decl list;
- node_outputs: var_decl list;
- node_locals: var_decl list;
- mutable node_gencalls: expr list;
- mutable node_checks: Dimension.dim_expr list;
- node_asserts: assert_t list;
- node_eqs: eq list;
- mutable node_dec_stateless: bool;
- mutable node_stateless: bool option;
- node_spec: LustreSpec.node_annot option;
- node_annot: LustreSpec.expr_annot option;}
-
-type imported_node_desc =
- {nodei_id: ident;
- mutable nodei_type: Types.type_expr;
- mutable nodei_clock: Clocks.clock_expr;
- nodei_inputs: var_decl list;
- nodei_outputs: var_decl list;
- nodei_stateless: bool;
- nodei_spec: LustreSpec.node_annot option;
- nodei_prototype: string option;
- nodei_in_lib: string option;
-}
-(*
-type imported_fun_desc =
- {fun_id: ident;
- mutable fun_type: Types.type_expr;
- fun_inputs: var_decl list;
- fun_outputs: var_decl list;
- fun_spec: LustreSpec.node_annot option;}
-*)
-type const_desc =
- {const_id: ident;
- const_loc: Location.t;
- const_value: constant;
- mutable const_type: Types.type_expr;
- }
-(* type sensor_desc = *)
-(* {sensor_id: ident; *)
-(* sensor_wcet: int} *)
-
-(* type actuator_desc = *)
-(* {actuator_id: ident; *)
-(* actuator_wcet: int} *)
-
-type top_decl_desc =
- | Node of node_desc
- | Consts of const_desc list
- | ImportedNode of imported_node_desc
- (* | ImportedFun of imported_fun_desc *)
- (* | SensorDecl of sensor_desc *)
- (* | ActuatorDecl of actuator_desc *)
- | Open of bool * string
-
-type top_decl =
- {top_decl_desc: top_decl_desc;
- top_decl_loc: Location.t}
-
-type program = top_decl list
+open LustreSpec
-type error =
- Main_not_found
- | Main_wrong_kind
- | No_main_specified
- | Unbound_symbol of ident
- | Already_bound_symbol of ident
-*)
exception Error of Location.t * error
val dummy_type_dec: type_dec
diff --git a/src/deadline_calculus.ml b/src/deadline_calculus.ml
deleted file mode 100755
index 690365e686936b4dd9bbb428693eeada2f0afe23..0000000000000000000000000000000000000000
--- a/src/deadline_calculus.ml
+++ /dev/null
@@ -1,198 +0,0 @@
-(* ----------------------------------------------------------------------------
- * SchedMCore - A MultiCore Scheduling Framework
- * Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
- *
- * This file is part of Prelude
- *
- * Prelude is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public License
- * as published by the Free Software Foundation ; either version 2 of
- * the License, or (at your option) any later version.
- *
- * Prelude is distributed in the hope that it will be useful, but
- * WITHOUT ANY WARRANTY ; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this program ; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
- * USA
- *---------------------------------------------------------------------------- *)
-
-open Format
-open Corelang
-open Task_graph
-open Task_set
-open Deadlines
-open Precedence_functions
-(** Encodes precedences by adjusting task deadlines. The names of the
- functions below refer to the names in the thesis manuscript *)
-
-(* ----- Core functions *)
-let rec t_ops ops t =
- match ops with
- | [] -> t
- | (Gfby _)::rest ->
- t_ops rest t
- | (Guclock k)::rest ->
- k*(t_ops rest t)
- | (Gdclock k)::rest ->
- (t_ops rest t)/k
- | (Gphclock _)::rest ->
- t_ops rest t
- | Gtail::rest ->
- t_ops rest t
- | (Gconcat _)::rest ->
- t_ops rest t
-
-let rec r_ops ops r t =
- match ops with
- | [] -> r
- | (Gfby _)::rest ->
- r_ops rest r t
- | (Guclock _)::rest ->
- r_ops rest r t
- | (Gdclock _)::rest ->
- r_ops rest r t
- | (Gphclock (a,b))::rest ->
- (r_ops rest r t) - a*(t_ops rest t)/b
- | Gtail::rest ->
- (r_ops rest r t) - (t_ops rest t)
- | (Gconcat _)::rest ->
- (r_ops rest r t) + (t_ops rest t)
-
-let delta_ops ops ti tj rj n =
- (gops ops n)*tj-n*ti+rj-(r_ops ops rj tj)
-
-(* delta_ops(ti,tj,rj) *)
-let delta_word ops ti tj rj =
- let lpref = pref_size ops in
- let lpat = periodicity ops in
- Array.init lpref (fun n -> delta_ops ops ti tj rj n),
- Array.init lpat (fun n -> delta_ops ops ti tj rj (n+lpref))
-
-(* P'(ops) *)
-let rec periodicity' wj ops =
- match ops with
- | [] -> pat_length wj
- | (Guclock k)::rest ->
- let pops = periodicity' wj rest in
- pops/(Utils.gcd k pops)
- | (Gdclock k):: rest ->
- k*(periodicity' wj rest)
- | (Gfby _)::rest ->
- periodicity' wj rest
- | (Gphclock _)::rest | Gtail::rest | (Gconcat _)::rest ->
- periodicity' wj rest
-
-let rec pref_size' wj ops =
- let rec aux ops =
- match ops with
- | [] -> pref_length wj
- | (Guclock k)::rest ->
- let props = aux rest in
- int_of_float (ceil ((float_of_int props) /. (float_of_int k)))
- | (Gdclock k)::rest ->
- let props = aux rest in
- max ((props -1)*k+1) 0
- | Gtail::rest ->
- (aux rest)+1
- | (Gfby _)::rest | (Gconcat _)::rest ->
- let props = aux rest in
- max (props -1) 0
- | (Gphclock _)::rest ->
- aux rest
- in
- max (aux ops) 0
-
-let w_ops wj ops =
- let lpref = pref_size' wj ops in
- let lpat = periodicity' wj ops in
- Array.init lpref (fun n -> nth_ud wj (gops ops n)),
- Array.init lpat (fun n -> nth_ud wj (gops ops n))
-
-(* Update deadlines to encode the precedence [from_v]-[annots]->[to_v]. *)
-let update_dd task_set from_v to_v annots =
- let task_from = task_of_vertex task_set from_v in
- let task_to = task_of_vertex task_set to_v in
- let wi = task_from.task_deadline in
- let ti = task_from.task_period in
- let wj = task_to.task_deadline in
- let tj = task_to.task_period in
- let rj = task_to.task_release in
- let cj = task_to.task_wcet in
- let delta = delta_word annots ti tj rj in
- let wops = w_ops wj annots in
- let cstr = add_int (add_dw delta wops) (-cj) in
- task_from.task_deadline <- min_dw wi cstr
-
-(* ----- Functions for the topological traversal *)
-let count_succs g =
- (* Count successors of tasks, ie count the successors of all the variables
- of the task. *)
- let nb_succs = Hashtbl.create 30 in
- let add_succs v nb =
- let tid = taskid_of_vertex v in
- let nb' =
- try Hashtbl.find nb_succs tid with Not_found -> 0 in
- Hashtbl.replace nb_succs tid (nb'+nb)
- in
- Hashtbl.iter
- (fun vid v ->
- let nb =
- Hashtbl.fold
- (fun succ annot n ->
- if is_delayed_prec annot then n else n+1)
- v.vertex_succs 0 in
- add_succs vid nb)
- g.graph;
- nb_succs
-
-(* Compute the initial set of vertices that have no successors *)
-let no_succs task_set nb_succs =
- Hashtbl.fold
- (fun tid nb acc ->
- if nb = 0 then
- let t = Hashtbl.find task_set tid in
- (inputs_of_task t)@acc
- else
- acc)
- nb_succs []
-
-(* Compute the new set of vertices that have no successors. *)
-let new_no_succs task_set nb_succs no_succs lost_one_succ =
- let tid = taskid_of_vertex lost_one_succ in
- let n = Hashtbl.find nb_succs tid in
- Hashtbl.replace nb_succs tid (n-1);
- if n = 1 then
- no_succs@(inputs_of_task (task_of_vertex task_set lost_one_succ))
- else
- no_succs
-
-let dd_prog g task_set exp_main =
- let nb_succs = count_succs g in
- (* Traversal of the graph as a classic reverse topological sort. *)
- let rec topo_traversal no_succs =
- match no_succs with
- | [] -> ()
- | v::rest ->
- let pred = (Hashtbl.find g.graph v).vertex_pred in
- match pred with
- | None -> topo_traversal rest
- | Some (p, annot) ->
- if not (is_delayed_prec annot) then
- begin
- update_dd task_set p v annot;
- let no_succs' = new_no_succs task_set nb_succs rest p in
- topo_traversal no_succs'
- end
- else
- topo_traversal rest
- in
- let no_succs = no_succs task_set nb_succs in
- topo_traversal no_succs
-
-(* Local Variables: *)
-(* compile-command:"make -C .." *)
-(* End: *)
diff --git a/src/deadlines.ml b/src/deadlines.ml
deleted file mode 100755
index ddaa773816ee0ae4948f863755675bd04fe083ce..0000000000000000000000000000000000000000
--- a/src/deadlines.ml
+++ /dev/null
@@ -1,84 +0,0 @@
-(* ----------------------------------------------------------------------------
- * SchedMCore - A MultiCore Scheduling Framework
- * Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
- *
- * This file is part of Prelude
- *
- * Prelude is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public License
- * as published by the Free Software Foundation ; either version 2 of
- * the License, or (at your option) any later version.
- *
- * Prelude is distributed in the hope that it will be useful, but
- * WITHOUT ANY WARRANTY ; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this program ; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
- * USA
- *---------------------------------------------------------------------------- *)
-
-open Utils
-open Format
-
-type deadline_word = int array * int array
-
-let dword_create ud =
- [||],[|ud|]
-
-let pat_length dw =
- let (dpref, dpat) = dw in
- Array.length dpat
-
-let pref_length dw =
- let (dpref, dpat) = dw in
- Array.length dpref
-
-(* [nth_ud dw n] returns the nth value of dw *)
-let nth_ud dw n =
- let (dpref, dpat) = dw in
- let (lpref, lpat) = Array.length dpref, Array.length dpat in
- if n < lpref then
- dpref.(n)
- else
- let pos = (n-lpref) mod lpat in
- dpat.(pos)
-
-let add_int dw n =
- let (dpref, dpat) = dw in
- (Array.map (fun ud -> ud+n) dpref,Array.map (fun ud -> ud+n) dpat)
-
-let dw_map2 f dw1 dw2 =
- let (dpref1, dpat1), (dpref2, dpat2) = dw1, dw2 in
- let (lpref1, lpref2) = Array.length dpref1, Array.length dpref2 in
- let (lpat1, lpat2) = Array.length dpat1, Array.length dpat2 in
- let lpref = max lpref1 lpref2 in
- let lpat = lcm lpat1 lpat2 in
- let pref,pat = Array.make lpref 0, Array.make lpat 0 in
- for i=0 to lpref-1 do
- pref.(i) <- f (nth_ud dw1 i) (nth_ud dw2 i)
- done;
- for i=0 to lpat-1 do
- pat.(i) <- f (nth_ud dw1 (i+lpref)) (nth_ud dw2 (i+lpref))
- done;
- pref,pat
-
-let add_dw dw1 dw2 =
- dw_map2 (+) dw1 dw2
-
-(* [min_dw dw1 dw2] returns the minimum, point-by-point, of [dw1] and [dw2].
- Can only be used on fully instanciated deadlines. *)
-let min_dw dw1 dw2 =
- dw_map2 (min) dw1 dw2
-
-let print_dw dw =
- let (dpref, dpat) = dw in
- if (Array.length dpref > 0) then
- pp_array dpref print_int "" "." ".";
- pp_array dpat print_int "(" ")" "."
-
-(* Local Variables: *)
-(* compile-command:"make -C .." *)
-(* End: *)
diff --git a/src/delay.ml b/src/delay.ml
index 0f40ba067a9fe2e9c14a7b6cfe5824ebe807131d..306bce0940cad3049ada051192125a1cc6146ede 100755
--- a/src/delay.ml
+++ b/src/delay.ml
@@ -1,24 +1,13 @@
-(* ----------------------------------------------------------------------------
- * SchedMCore - A MultiCore Scheduling Framework
- * Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
- *
- * This file is part of Prelude
- *
- * Prelude is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public License
- * as published by the Free Software Foundation ; either version 2 of
- * the License, or (at your option) any later version.
- *
- * Prelude is distributed in the hope that it will be useful, but
- * WITHOUT ANY WARRANTY ; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this program ; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
- * USA
- *---------------------------------------------------------------------------- *)
+(********************************************************************)
+(* *)
+(* 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. *)
+(* *)
+(********************************************************************)
(** Types definitions and a few utility functions on delay types. *)
(** Delay analysis by type polymorphism instead of constraints *)
diff --git a/src/delay_predef.ml b/src/delay_predef.ml
index 6d58cccc3f1c60d572555a2d2c96d4996b1710d0..9c9051270e39b827d0829620c7d154cb4b3e0430 100755
--- a/src/delay_predef.ml
+++ b/src/delay_predef.ml
@@ -1,24 +1,13 @@
-(* ----------------------------------------------------------------------------
- * SchedMCore - A MultiCore Scheduling Framework
- * Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
- *
- * This file is part of Prelude
- *
- * Prelude is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public License
- * as published by the Free Software Foundation ; either version 2 of
- * the License, or (at your option) any later version.
- *
- * Prelude is distributed in the hope that it will be useful, but
- * WITHOUT ANY WARRANTY ; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this program ; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
- * USA
- *---------------------------------------------------------------------------- *)
+(********************************************************************)
+(* *)
+(* 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. *)
+(* *)
+(********************************************************************)
(** Base types and predefined operator types. *)
open Delay
diff --git a/src/dimension.ml b/src/dimension.ml
index d5d4e6f5209c1102666a2d3654056b92728ed0ee..8c40339f4aed313df1a4ab12d358cdebfca79807 100644
--- a/src/dimension.ml
+++ b/src/dimension.ml
@@ -1,27 +1,13 @@
-(* ----------------------------------------------------------------------------
- * SchedMCore - A MultiCore Scheduling Framework
- * Copyright (C) 2009-2013, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
- * Copyright (C) 2012-2013, INPT, Toulouse, FRANCE
- *
- * This file is part of Prelude
- *
- * Prelude is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public License
- * as published by the Free Software Foundation ; either version 2 of
- * the License, or (at your option) any later version.
- *
- * Prelude is distributed in the hope that it will be useful, but
- * WITHOUT ANY WARRANTY ; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this program ; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
- * USA
- *---------------------------------------------------------------------------- *)
-
-(* This module is used for the lustre to C compiler *)
+(********************************************************************)
+(* *)
+(* 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
diff --git a/src/env.ml b/src/env.ml
index 8e10610ab3a744ac1e7cb3b671e8720b052a4976..31111bb59225979aae7d0254c583a75e8cf8e371 100755
--- a/src/env.ml
+++ b/src/env.ml
@@ -1,24 +1,13 @@
-(* ----------------------------------------------------------------------------
- * SchedMCore - A MultiCore Scheduling Framework
- * Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
- *
- * This file is part of Prelude
- *
- * Prelude is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public License
- * as published by the Free Software Foundation ; either version 2 of
- * the License, or (at your option) any later version.
- *
- * Prelude is distributed in the hope that it will be useful, but
- * WITHOUT ANY WARRANTY ; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this program ; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
- * USA
- *---------------------------------------------------------------------------- *)
+(********************************************************************)
+(* *)
+(* 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. *)
+(* *)
+(********************************************************************)
(** Generic inference environments. Used both for typing and
clock-calculus. *)
diff --git a/src/expand.ml b/src/expand.ml
index fc6c5f4f41ce9c7f9d039f982875cf0a179379d2..bf43fe90b0da2ef81923d95781d947283d14a230 100755
--- a/src/expand.ml
+++ b/src/expand.ml
@@ -1,24 +1,13 @@
-(* ----------------------------------------------------------------------------
- * SchedMCore - A MultiCore Scheduling Framework
- * Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
- *
- * This file is part of Prelude
- *
- * Prelude is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public License
- * as published by the Free Software Foundation ; either version 2 of
- * the License, or (at your option) any later version.
- *
- * Prelude is distributed in the hope that it will be useful, but
- * WITHOUT ANY WARRANTY ; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this program ; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
- * USA
- *---------------------------------------------------------------------------- *)
+(********************************************************************)
+(* *)
+(* 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 Clocks
open Corelang
diff --git a/src/init_calculus.ml b/src/init_calculus.ml
index 636acb63b491eb952e0973cb2c88379a0b0a7be3..7872e0a55302df2ebccf78641f1f81c472c19b7c 100755
--- a/src/init_calculus.ml
+++ b/src/init_calculus.ml
@@ -1,24 +1,13 @@
-(* ----------------------------------------------------------------------------
- * SchedMCore - A MultiCore Scheduling Framework
- * Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
- *
- * This file is part of Prelude
- *
- * Prelude is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public License
- * as published by the Free Software Foundation ; either version 2 of
- * the License, or (at your option) any later version.
- *
- * Prelude is distributed in the hope that it will be useful, but
- * WITHOUT ANY WARRANTY ; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this program ; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
- * USA
- *---------------------------------------------------------------------------- *)
+(********************************************************************)
+(* *)
+(* 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. *)
+(* *)
+(********************************************************************)
(** Main typing module. Classic inference algorithm with destructive
unification. *)
diff --git a/src/init_predef.ml b/src/init_predef.ml
index 3ab5aca2ea9c58d881619f0185235db1735c3913..0bab5149e2220ff089ad6a8d35a5a20a19c09939 100755
--- a/src/init_predef.ml
+++ b/src/init_predef.ml
@@ -1,24 +1,14 @@
-(* ----------------------------------------------------------------------------
- * SchedMCore - A MultiCore Scheduling Framework
- * Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
- *
- * This file is part of Prelude
- *
- * Prelude is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public License
- * as published by the Free Software Foundation ; either version 2 of
- * the License, or (at your option) any later version.
- *
- * Prelude is distributed in the hope that it will be useful, but
- * WITHOUT ANY WARRANTY ; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this program ; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
- * USA
- *---------------------------------------------------------------------------- *)
+(********************************************************************)
+(* *)
+(* 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. *)
+(* *)
+(********************************************************************)
+
(** Base types and predefined operator types. *)
open Init
diff --git a/src/inliner.ml b/src/inliner.ml
index 00bcaf7d235f624bb1fc59ebfd9fe6df723b40c7..e73b5ce2994cea3092e3cd23cc1feeef457c4043 100644
--- a/src/inliner.ml
+++ b/src/inliner.ml
@@ -1,3 +1,14 @@
+(********************************************************************)
+(* *)
+(* 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
diff --git a/src/lexerLustreSpec.mll b/src/lexerLustreSpec.mll
index c59191caf67b52f5f294bb47a3e24c40562ae07d..da4ca6caeab124ec8928ca365b423c35b634e4fc 100644
--- a/src/lexerLustreSpec.mll
+++ b/src/lexerLustreSpec.mll
@@ -1,3 +1,14 @@
+(********************************************************************)
+(* *)
+(* 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 ParserLustreSpec *)
diff --git a/src/lexer_lustre.mll b/src/lexer_lustre.mll
index 549810cd12093f584bee4016f87e370b4fac88c8..02a5255a8ced28229af9b459342cc114521b58da 100755
--- a/src/lexer_lustre.mll
+++ b/src/lexer_lustre.mll
@@ -1,24 +1,13 @@
-(* ----------------------------------------------------------------------------
- * SchedMCore - A MultiCore Scheduling Framework
- * Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
- *
- * This file is part of Prelude
- *
- * Prelude is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public License
- * as published by the Free Software Foundation ; either version 2 of
- * the License, or (at your option) any later version.
- *
- * Prelude is distributed in the hope that it will be useful, but
- * WITHOUT ANY WARRANTY ; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this program ; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
- * USA
- *---------------------------------------------------------------------------- *)
+(********************************************************************)
+(* *)
+(* 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 Parser_lustre
diff --git a/src/lexer_prelude.mll b/src/lexer_prelude.mll
index dc65c3a924e2a0a58357f779d1ac77bf1ac5fab3..ab0b64c42c49f32f9ed53f317e330f939bf39cf7 100755
--- a/src/lexer_prelude.mll
+++ b/src/lexer_prelude.mll
@@ -1,24 +1,13 @@
-(* ----------------------------------------------------------------------------
- * SchedMCore - A MultiCore Scheduling Framework
- * Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
- *
- * This file is part of Prelude
- *
- * Prelude is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public License
- * as published by the Free Software Foundation ; either version 2 of
- * the License, or (at your option) any later version.
- *
- * Prelude is distributed in the hope that it will be useful, but
- * WITHOUT ANY WARRANTY ; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this program ; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
- * USA
- *---------------------------------------------------------------------------- *)
+(********************************************************************)
+(* *)
+(* 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 Parser_prelude
diff --git a/src/liveness.ml b/src/liveness.ml
index 756a9e4ad5b32ab69fb8843976b3666294b32026..88285ccee01f83a271a7ef8f37cc47112f246b29 100755
--- a/src/liveness.ml
+++ b/src/liveness.ml
@@ -1,25 +1,13 @@
-(* ----------------------------------------------------------------------------
- * SchedMCore - A MultiCore Scheduling Framework
- * Copyright (C) 2009-2013, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
- * Copyright (C) 2012-2013, INPT, Toulouse, FRANCE
- *
- * This file is part of Prelude
- *
- * Prelude is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public License
- * as published by the Free Software Foundation ; either version 2 of
- * the License, or (at your option) any later version.
- *
- * Prelude is distributed in the hope that it will be useful, but
- * WITHOUT ANY WARRANTY ; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this program ; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
- * USA
- *---------------------------------------------------------------------------- *)
+(********************************************************************)
+(* *)
+(* 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
diff --git a/src/location.ml b/src/location.ml
index 89b73d99b0e5dc362ec349b5d8f4325ab4d1fc0c..1dc6919aa3c7a2f40884e59ad8e6a5d02859fec0 100755
--- a/src/location.ml
+++ b/src/location.ml
@@ -1,24 +1,13 @@
-(* ----------------------------------------------------------------------------
- * SchedMCore - A MultiCore Scheduling Framework
- * Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
- *
- * This file is part of Prelude
- *
- * Prelude is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public License
- * as published by the Free Software Foundation ; either version 2 of
- * the License, or (at your option) any later version.
- *
- * Prelude is distributed in the hope that it will be useful, but
- * WITHOUT ANY WARRANTY ; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this program ; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
- * USA
- *---------------------------------------------------------------------------- *)
+(********************************************************************)
+(* *)
+(* 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. *)
+(* *)
+(********************************************************************)
type t = { loc_start: Lexing.position; loc_end: Lexing.position }
let dummy_loc = {loc_start=Lexing.dummy_pos; loc_end=Lexing.dummy_pos}
diff --git a/src/log.ml b/src/log.ml
index a5bb5fe8a9c9b09dd9d137de61d97b0f3cbbe8d2..52151f55ff991e75af20f45badfc4962ddc44b4d 100644
--- a/src/log.ml
+++ b/src/log.ml
@@ -1,27 +1,13 @@
-(* ----------------------------------------------------------------------------
- * SchedMCore - A MultiCore Scheduling Framework
- * Copyright (C) 2009-2013, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
- * Copyright (C) 2012-2013, INPT, Toulouse, FRANCE
- *
- * This file is part of Prelude
- *
- * Prelude is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public License
- * as published by the Free Software Foundation ; either version 2 of
- * the License, or (at your option) any later version.
- *
- * Prelude is distributed in the hope that it will be useful, but
- * WITHOUT ANY WARRANTY ; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this program ; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
- * USA
- *---------------------------------------------------------------------------- *)
-
-(* This module is used for the lustre to C compiler *)
+(********************************************************************)
+(* *)
+(* 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. *)
+(* *)
+(********************************************************************)
let report ~level:level p =
if !Options.verbose_level >= level then
diff --git a/src/lustreSpec.ml b/src/lustreSpec.ml
index a5580e1df91454f3724f1b0fc09195576703ab72..275173164b26fe5595744dc02aacdbe5e4d22042 100644
--- a/src/lustreSpec.ml
+++ b/src/lustreSpec.ml
@@ -1,3 +1,14 @@
+(********************************************************************)
+(* *)
+(* 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
type ident = Utils.ident
diff --git a/src/machine_code.ml b/src/machine_code.ml
index 6e6402d709e2790d2b6c16ec0387568e7bb03f17..9d3b6d1c1d41507dca83f0cae4a986316eef35a6 100644
--- a/src/machine_code.ml
+++ b/src/machine_code.ml
@@ -1,28 +1,13 @@
-
-(* ----------------------------------------------------------------------------
- * SchedMCore - A MultiCore Scheduling Framework
- * Copyright (C) 2009-2013, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
- * Copyright (C) 2012-2013, INPT, Toulouse, FRANCE
- *
- * This file is part of Prelude
- *
- * Prelude is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public License
- * as published by the Free Software Foundation ; either version 2 of
- * the License, or (at your option) any later version.
- *
- * Prelude is distributed in the hope that it will be useful, but
- * WITHOUT ANY WARRANTY ; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this program ; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
- * USA
- *---------------------------------------------------------------------------- *)
-
-(* This module is used for the lustre to C compiler *)
+(********************************************************************)
+(* *)
+(* 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
diff --git a/src/main_lustre_compiler.ml b/src/main_lustre_compiler.ml
index 0f7dd113a8a415bfe40b9cca044cd61bb6e76b9c..e5e7f66866043fa01ff54cde3142c9bc13df3d7a 100644
--- a/src/main_lustre_compiler.ml
+++ b/src/main_lustre_compiler.ml
@@ -1,27 +1,13 @@
-(* ----------------------------------------------------------------------------
- * SchedMCore - A MultiCore Scheduling Framework
- * Copyright (C) 2009-2013, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
- * Copyright (C) 2012-2013, INPT, Toulouse, FRANCE
- *
- * This file is part of Prelude
- *
- * Prelude is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public License
- * as published by the Free Software Foundation ; either version 2 of
- * the License, or (at your option) any later version.
- *
- * Prelude is distributed in the hope that it will be useful, but
- * WITHOUT ANY WARRANTY ; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this program ; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
- * USA
- *---------------------------------------------------------------------------- *)
-
-(* This module is used for the lustre to C compiler *)
+(********************************************************************)
+(* *)
+(* 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
diff --git a/src/normalization.ml b/src/normalization.ml
index 8c786a00294226f5cc01c10afe6e4791bc056b34..05f34f4b24e897da1ae4131d46f486ae4f6453a3 100644
--- a/src/normalization.ml
+++ b/src/normalization.ml
@@ -1,33 +1,17 @@
-(* ----------------------------------------------------------------------------
- * SchedMCore - A MultiCore Scheduling Framework
- * Copyright (C) 2009-2013, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
- * Copyright (C) 2012-2013, INPT, Toulouse, FRANCE
- *
- * This file is part of Prelude
- *
- * Prelude is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public License
- * as published by the Free Software Foundation ; either version 2 of
- * the License, or (at your option) any later version.
- *
- * Prelude is distributed in the hope that it will be useful, but
- * WITHOUT ANY WARRANTY ; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this program ; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
- * USA
- *---------------------------------------------------------------------------- *)
-
-(* This module is used for the lustre to C compiler *)
-
+(********************************************************************)
+(* *)
+(* 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 Clocks *)
open Format
let expr_true loc ck =
diff --git a/src/optimize_machine.ml b/src/optimize_machine.ml
index aa923ecddd062c0fc14af46ae8436dd4fe1af189..6ee61f84c5b0e34385915a55f548bed1abdb1028 100644
--- a/src/optimize_machine.ml
+++ b/src/optimize_machine.ml
@@ -1,3 +1,14 @@
+(********************************************************************)
+(* *)
+(* 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
open Machine_code
diff --git a/src/optimize_prog.ml b/src/optimize_prog.ml
index e6dae6ba7f9eaa4a5765f7b3ab5968712b10fb03..b658953e242a97d97cae851e973802a149fa497e 100644
--- a/src/optimize_prog.ml
+++ b/src/optimize_prog.ml
@@ -1,3 +1,14 @@
+(********************************************************************)
+(* *)
+(* 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 Corelang
open LustreSpec
diff --git a/src/options.ml b/src/options.ml
index 72976f727e197821e3097be68b9b9ebbbc2af12e..4e47a0bc3be3cd4a0f6237cbd6596d61644096a0 100755
--- a/src/options.ml
+++ b/src/options.ml
@@ -1,24 +1,13 @@
-(* ----------------------------------------------------------------------------
- * SchedMCore - A MultiCore Scheduling Framework
- * Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
- *
- * This file is part of Prelude
- *
- * Prelude is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public License
- * as published by the Free Software Foundation ; either version 2 of
- * the License, or (at your option) any later version.
- *
- * Prelude is distributed in the hope that it will be useful, but
- * WITHOUT ANY WARRANTY ; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this program ; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
- * USA
- *---------------------------------------------------------------------------- *)
+(********************************************************************)
+(* *)
+(* 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. *)
+(* *)
+(********************************************************************)
let version = "0.1-"^Version.number
let main_node = ref ""
@@ -36,9 +25,10 @@ let verbose_level = ref 1
let global_inline = ref false
let witnesses = ref false
let optimization = ref 2
+
let horntraces = ref false
let horn_cex = ref false
-
+let horn_queries = ref false
let options =
[ "-d", Arg.Set_string dest_dir,
@@ -55,7 +45,8 @@ let options =
"-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C";
"-horn", Arg.Unit (fun () -> output := "horn"), "generates Horn clauses encoding output instead of C";
"-horn-traces", Arg.Unit (fun () -> output := "horn"; horntraces:=true), "produce traceability file for Horn backend. Enable the horn backend.";
- "-horn-cex", Arg.Set horn_cex, "generate cex enumeration. Enable the horn backend (work in progress)";
+ "-horn-cex", Arg.Unit (fun () -> output := "horn"; horn_cex:=true), "generate cex enumeration. Enable the horn backend (work in progress)";
+ "-horn-queries", Arg.Unit (fun () -> output := "horn"; horn_queries:=true), "generate queries in generated Horn file. Enable the horn backend (work in progress)";
"-lustre", Arg.Unit (fun () -> output := "lustre"), "generates Lustre output, performing all active optimizations";
"-inline", Arg.Set global_inline, "inline all node calls (require a main node)";
"-witnesses", Arg.Set witnesses, "enable production of witnesses during compilation";
diff --git a/src/parse.ml b/src/parse.ml
index 108a8757691f652b755ebe97529ee7396227973f..1c13b7e385d2eeeabcf040e062c5401f1a7e04c3 100755
--- a/src/parse.ml
+++ b/src/parse.ml
@@ -1,24 +1,13 @@
-(* ----------------------------------------------------------------------------
- * SchedMCore - A MultiCore Scheduling Framework
- * Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
- *
- * This file is part of Prelude
- *
- * Prelude is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public License
- * as published by the Free Software Foundation ; either version 2 of
- * the License, or (at your option) any later version.
- *
- * Prelude is distributed in the hope that it will be useful, but
- * WITHOUT ANY WARRANTY ; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this program ; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
- * USA
- *---------------------------------------------------------------------------- *)
+(********************************************************************)
+(* *)
+(* 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. *)
+(* *)
+(********************************************************************)
exception Syntax_err of Location.t
diff --git a/src/parserLustreSpec.mly b/src/parserLustreSpec.mly
index 8f37b46bfdad55ff825d5c3a0f40cc9285597cba..17fb13120b88b9b53c0b07784ac8095de20294ac 100644
--- a/src/parserLustreSpec.mly
+++ b/src/parserLustreSpec.mly
@@ -1,4 +1,15 @@
%{
+(********************************************************************)
+(* *)
+(* 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 Corelang
open LustreSpec
diff --git a/src/parser_lustre.mly b/src/parser_lustre.mly
index ecf50464a32ae6d85bd0f1f3c69dbf0fd3a89c01..16750c6374da6ac5e00b331a786a166379305da0 100755
--- a/src/parser_lustre.mly
+++ b/src/parser_lustre.mly
@@ -1,24 +1,13 @@
-/* ----------------------------------------------------------------------------
- * SchedMCore - A MultiCore Scheduling Framework
- * Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
- *
- * This file is part of Prelude
- *
- * Prelude is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public License
- * as published by the Free Software Foundation ; either version 2 of
- * the License, or (at your option) any later version.
- *
- * Prelude is distributed in the hope that it will be useful, but
- * WITHOUT ANY WARRANTY ; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this program ; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
- * USA
- *---------------------------------------------------------------------------- */
+/********************************************************************/
+/* */
+/* 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
diff --git a/src/precedence_functions.ml b/src/precedence_functions.ml
deleted file mode 100644
index ce014a463c22b760bc5373641c661ff5a524fa8e..0000000000000000000000000000000000000000
--- a/src/precedence_functions.ml
+++ /dev/null
@@ -1,101 +0,0 @@
-(* ----------------------------------------------------------------------------
- * SchedMCore - A MultiCore Scheduling Framework
- * Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
- *
- * This file is part of Prelude
- *
- * Prelude is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public License
- * as published by the Free Software Foundation ; either version 2 of
- * the License, or (at your option) any later version.
- *
- * Prelude is distributed in the hope that it will be useful, but
- * WITHOUT ANY WARRANTY ; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this program ; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
- * USA
- *---------------------------------------------------------------------------- *)
-
-open Task_graph
-
-(* Precedences as defined by g_ops(n) (see thesis manuscript) *)
-
-(* g_ops(n) *)
-let rec gops ops n =
- match ops with
- | [] -> n
- | (Gfby _)::rest ->
- gops rest (n+1)
- | (Guclock k)::rest ->
- gops rest (k*n)
- | (Gdclock k)::rest ->
- gops rest (int_of_float (ceil ((float_of_int n)/. (float_of_int k))))
- | (Gphclock _)::rest ->
- gops rest n
- | Gtail::rest ->
- if n = 0 then gops rest 0 else
- gops rest (n-1)
- | (Gconcat _)::rest ->
- gops rest (n+1)
-
-(* pref(ops) *)
-let pref_size ops =
- let rec aux ops =
- match ops with
- | [] -> 0
- | (Guclock k)::rest ->
- let props = aux rest in
- int_of_float (ceil ((float_of_int props) /. (float_of_int k)))
- | (Gdclock k)::rest ->
- let props = aux rest in
- (props -1)*k+1
- | Gtail::rest ->
- (aux rest)+1
- | (Gfby _)::rest | (Gconcat _)::rest ->
- let props = aux rest in
- max (props -1) 0
- | (Gphclock _)::rest ->
- aux rest
- in
- max (aux ops) 0
-
-(* P(ops) *)
-let rec periodicity ops =
- match ops with
- | [] -> 1
- | (Guclock k)::rest ->
- let pops = periodicity rest in
- pops/(Utils.gcd k pops)
- | (Gdclock k)::rest ->
- k*(periodicity rest)
- | (Gfby _)::rest ->
- periodicity rest
- | (Gphclock _)::rest | Gtail::rest | (Gconcat _)::rest ->
- periodicity rest
-
-(* Returns the non-redundant precedence relation as defined in RTAS, ie
- the set of pairs (n,n') such that ti.n->tj.n' (in the first HP) *)
-let prec_relation ops =
- let spref = pref_size ops in
- let spat = periodicity ops in
- let pref = Hashtbl.create spref in
- let pat = Hashtbl.create spat in
- let aux tbl n =
- if gops ops n <> gops ops (n+1) then
- Hashtbl.add tbl n (gops ops n)
- in
- for i=0 to spref-1 do
- aux pref i;
- done;
- for i=0 to spat-1 do
- aux pat i;
- done;
- (pref,pat)
-
-(* Local Variables: *)
-(* compile-command:"make -C .." *)
-(* End: *)
diff --git a/src/printers.ml b/src/printers.ml
index 6849f999e9ab875da6a6a649def08e513eb91f61..676ba4153f286ca38e56af0652370e3571b6c259 100644
--- a/src/printers.ml
+++ b/src/printers.ml
@@ -1,24 +1,14 @@
-(* ----------------------------------------------------------------------------
- * SchedMCore - A MultiCore Scheduling Framework
- * Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
- *
- * This file is part of Prelude
- *
- * Prelude is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public License
- * as published by the Free Software Foundation ; either version 2 of
- * the License, or (at your option) any later version.
- *
- * Prelude is distributed in the hope that it will be useful, but
- * WITHOUT ANY WARRANTY ; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this program ; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
- * USA
- *---------------------------------------------------------------------------- *)
+(********************************************************************)
+(* *)
+(* 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 Corelang
open LustreSpec
open Format
diff --git a/src/scheduling.ml b/src/scheduling.ml
index a87ddd20697e7af7e83c7f4f52a41b0978de0fee..bbd91c6ffa145fad6b107ee29845f0df1fcbccc1 100644
--- a/src/scheduling.ml
+++ b/src/scheduling.ml
@@ -1,27 +1,13 @@
-(* ----------------------------------------------------------------------------
- * SchedMCore - A MultiCore Scheduling Framework
- * Copyright (C) 2009-2013, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
- * Copyright (C) 2012-2013, INPT, Toulouse, FRANCE
- *
- * This file is part of Prelude
- *
- * Prelude is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public License
- * as published by the Free Software Foundation ; either version 2 of
- * the License, or (at your option) any later version.
- *
- * Prelude is distributed in the hope that it will be useful, but
- * WITHOUT ANY WARRANTY ; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this program ; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
- * USA
- *---------------------------------------------------------------------------- *)
-
-(* This module is used for the lustre to C compiler *)
+(********************************************************************)
+(* *)
+(* 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
diff --git a/src/sortProg.ml b/src/sortProg.ml
index 00f16aa15f77ad859aa69c92b3b492588f265559..ea131754dadd57e3f22b5b5c5783a021013486f1 100644
--- a/src/sortProg.ml
+++ b/src/sortProg.ml
@@ -1,3 +1,14 @@
+(********************************************************************)
+(* *)
+(* 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 Graph
open LustreSpec
open Corelang
diff --git a/src/splitting.ml b/src/splitting.ml
index 5d638d2bc98596720594202ebb9b3e4608c75474..e830b614526893b5df3fabf83b73506f885d68af 100644
--- a/src/splitting.ml
+++ b/src/splitting.ml
@@ -1,28 +1,13 @@
-(* ----------------------------------------------------------------------------
- * SchedMCore - A MultiCore Scheduling Framework
- * Copyright (C) 2009-2013, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
- * Copyright (C) 2012-2013, INPT, Toulouse, FRANCE
- *
- * This file is part of Prelude
- *
- * Prelude is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public License
- * as published by the Free Software Foundation ; either version 2 of
- * the License, or (at your option) any later version.
- *
- * Prelude is distributed in the hope that it will be useful, but
- * WITHOUT ANY WARRANTY ; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this program ; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
- * USA
- *---------------------------------------------------------------------------- *)
-
-(* This module is used for the lustre to C compiler *)
-
+(********************************************************************)
+(* *)
+(* 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 Corelang
diff --git a/src/stateless.ml b/src/stateless.ml
index f08d8223124fc5d4d040d32d3e62fe0bb8aca7a3..5fcec93b7e94dfd62aa09ea9275ef83e81305850 100755
--- a/src/stateless.ml
+++ b/src/stateless.ml
@@ -1,24 +1,14 @@
-(* ----------------------------------------------------------------------------
- * SchedMCore - A MultiCore Scheduling Framework
- * Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
- *
- * This file is part of Prelude
- *
- * Prelude is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public License
- * as published by the Free Software Foundation ; either version 2 of
- * the License, or (at your option) any later version.
- *
- * Prelude is distributed in the hope that it will be useful, but
- * WITHOUT ANY WARRANTY ; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this program ; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
- * USA
- *---------------------------------------------------------------------------- *)
+(********************************************************************)
+(* *)
+(* 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
diff --git a/src/type_predef.ml b/src/type_predef.ml
index b60141b32ff7e42c07e45acb7fbf6c049dc64fb1..0690be222ffd8afb77707d1437f84f12290e3ac5 100755
--- a/src/type_predef.ml
+++ b/src/type_predef.ml
@@ -1,24 +1,15 @@
-(* ----------------------------------------------------------------------------
- * SchedMCore - A MultiCore Scheduling Framework
- * Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
- *
- * This file is part of Prelude
- *
- * Prelude is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public License
- * as published by the Free Software Foundation ; either version 2 of
- * the License, or (at your option) any later version.
- *
- * Prelude is distributed in the hope that it will be useful, but
- * WITHOUT ANY WARRANTY ; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this program ; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
- * USA
- *---------------------------------------------------------------------------- *)
+(********************************************************************)
+(* *)
+(* The LustreC compiler toolset / The LustreC Development Team *)
+(* Copyright 2012 - -- ONERA - CNRS - INPT - LIFL *)
+(* *)
+(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)
+(* under the terms of the GNU Lesser General Public License *)
+(* version 2.1. *)
+(* *)
+(* This file was originally from the Prelude compiler *)
+(* *)
+(********************************************************************)
(** Base types and predefined operator types. *)
open Types
diff --git a/src/types.ml b/src/types.ml
index fb32f6a52346fef88c2b7ada74fcc100a2828dea..bc4b82a0ff3f1105ae6bfaec4977ac54b9d9f2b2 100755
--- a/src/types.ml
+++ b/src/types.ml
@@ -1,24 +1,15 @@
-(* ----------------------------------------------------------------------------
- * SchedMCore - A MultiCore Scheduling Framework
- * Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
- *
- * This file is part of Prelude
- *
- * Prelude is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public License
- * as published by the Free Software Foundation ; either version 2 of
- * the License, or (at your option) any later version.
- *
- * Prelude is distributed in the hope that it will be useful, but
- * WITHOUT ANY WARRANTY ; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this program ; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
- * USA
- *---------------------------------------------------------------------------- *)
+(********************************************************************)
+(* *)
+(* The LustreC compiler toolset / The LustreC Development Team *)
+(* Copyright 2012 - -- ONERA - CNRS - INPT - LIFL *)
+(* *)
+(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)
+(* under the terms of the GNU Lesser General Public License *)
+(* version 2.1. *)
+(* *)
+(* This file was originally from the Prelude compiler *)
+(* *)
+(********************************************************************)
(** Types definitions and a few utility functions on types. *)
open Utils
diff --git a/src/typing.ml b/src/typing.ml
index 26e04feb30ecdde5d10827893d7d76502fafb81e..5eb7bfc40bd1c317b36f3006db5bb83cbd0a65ae 100755
--- a/src/typing.ml
+++ b/src/typing.ml
@@ -1,24 +1,15 @@
-(* ----------------------------------------------------------------------------
- * SchedMCore - A MultiCore Scheduling Framework
- * Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
- *
- * This file is part of Prelude
- *
- * Prelude is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public License
- * as published by the Free Software Foundation ; either version 2 of
- * the License, or (at your option) any later version.
- *
- * Prelude is distributed in the hope that it will be useful, but
- * WITHOUT ANY WARRANTY ; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this program ; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
- * USA
- *---------------------------------------------------------------------------- *)
+(********************************************************************)
+(* *)
+(* The LustreC compiler toolset / The LustreC Development Team *)
+(* Copyright 2012 - -- ONERA - CNRS - INPT - LIFL *)
+(* *)
+(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)
+(* under the terms of the GNU Lesser General Public License *)
+(* version 2.1. *)
+(* *)
+(* This file was originally from the Prelude compiler *)
+(* *)
+(********************************************************************)
(** Main typing module. Classic inference algorithm with destructive
unification. *)
diff --git a/src/utils.ml b/src/utils.ml
index 465be7edefdbb641849532c31309052a9b252d67..44df4172e4d73c7592b501b44bd436ab0653399f 100755
--- a/src/utils.ml
+++ b/src/utils.ml
@@ -1,24 +1,14 @@
-(* ----------------------------------------------------------------------------
- * SchedMCore - A MultiCore Scheduling Framework
- * Copyright (C) 2009-2011, ONERA, Toulouse, FRANCE - LIFL, Lille, FRANCE
- *
- * This file is part of Prelude
- *
- * Prelude is free software; you can redistribute it and/or
- * modify it under the terms of the GNU Lesser General Public License
- * as published by the Free Software Foundation ; either version 2 of
- * the License, or (at your option) any later version.
- *
- * Prelude is distributed in the hope that it will be useful, but
- * WITHOUT ANY WARRANTY ; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
- * Lesser General Public License for more details.
- *
- * You should have received a copy of the GNU Lesser General Public
- * License along with this program ; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307
- * USA
- *---------------------------------------------------------------------------- *)
+(********************************************************************)
+(* *)
+(* 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 Graph
type rat = int*int