Skip to content
Snippets Groups Projects
Commit a2d97a3e authored by Pierre Loic Garoche's avatar Pierre Loic Garoche
Browse files

Updated the licence info and header for each file.

Moved backends in separate folders



git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/trunk@313 041b043f-8d7c-46b2-b46e-ef0dd855326e
parent be3dd43f
No related branches found
No related tags found
No related merge requests found
Showing
with 318 additions and 539 deletions
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
"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
......
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}
......
(*
* 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: *)
(* $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
(* ----------------------------------------------------------------------------
* 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 *)
......
(* ----------------------------------------------------------------------------
* 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
(********************************************************************************************)
......
(********************************************************************)
(* *)
(* 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
......
(********************************************************************)
(* *)
(* 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
......
(********************************************************************)
(* *)
(* 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
......
(********************************************************************)
(* *)
(* 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
......
(********************************************************************)
(* *)
(* 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
......
(********************************************************************)
(* *)
(* 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
......
This diff is collapsed.
(* ----------------------------------------------------------------------------
* 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
......
(* ----------------------------------------------------------------------------
* 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
......
(* ----------------------------------------------------------------------------
* 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
......
(* ----------------------------------------------------------------------------
* 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. *)
......
(* ----------------------------------------------------------------------------
* 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
......
(* ----------------------------------------------------------------------------
* 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
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment