[Kernel] remove unused files and licenses

.Makefile.lint

@@ -181,7 +181,6 @@ ML_LINT_KO+=src/libraries/utils/hptset.ml
 ML_LINT_KO+=src/libraries/utils/hptset.mli
 ML_LINT_KO+=src/libraries/utils/indexer.ml
 ML_LINT_KO+=src/libraries/utils/indexer.mli
-ML_LINT_KO+=src/libraries/utils/leftistheap.mli
 ML_LINT_KO+=src/libraries/utils/pretty_utils.ml
 ML_LINT_KO+=src/libraries/utils/pretty_utils.mli
 ML_LINT_KO+=src/libraries/utils/qstack.ml

Makefile

@@ -461,7 +461,6 @@ LIB_CMO =\
 	src/libraries/utils/rgmap \
 	src/libraries/utils/bitvector \
 	src/libraries/utils/qstack \
-	src/libraries/utils/leftistheap \
 	src/libraries/stdlib/integer \
 	src/libraries/utils/json \
 	src/libraries/utils/markdown \

headers/close-source/JCF_LGPL

-
-Copyright (C) Jean-Christophe Filliatre
-
-This software is free software; you can redistribute it and/or
-modify it under the terms of the GNU Library General Public
-License version 2.1, with the special exception on linking
-described in file LICENSE.
-
-This software 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.
-

headers/header_spec.txt

@@ -102,10 +102,8 @@ headers/open-source/UNMODIFIED_WHY3: .ignore
 headers/updates-headers.sh: CEA_PROPRIETARY
 lib/plugins/PLUGINS.README: .ignore
 licenses/CDDL-1.0: .ignore
-licenses/GPLv3: .ignore
 licenses/LGPLv2: .ignore
 licenses/LGPLv2.1: .ignore
-licenses/LGPLv3: .ignore
 licenses/Q_MODIFIED_LICENSE: .ignore
 man/frama-c.1: CEA_LGPL
 opam/descr: .ignore
@@ -670,8 +668,6 @@ src/libraries/utils/hptset.ml: CEA_LGPL
 src/libraries/utils/hptset.mli: CEA_LGPL
 src/libraries/utils/indexer.ml: CEA_LGPL
 src/libraries/utils/indexer.mli: CEA_LGPL
-src/libraries/utils/leftistheap.ml: JCF_LGPL
-src/libraries/utils/leftistheap.mli: JCF_LGPL
 src/libraries/utils/markdown.ml: CEA_LGPL
 src/libraries/utils/markdown.mli: CEA_LGPL
 src/libraries/utils/pretty_utils.ml: CEA_LGPL

headers/open-source/JCF_LGPL

-
-Copyright (C) Jean-Christophe Filliatre
-
-This software is free software; you can redistribute it and/or
-modify it under the terms of the GNU Library General Public
-License version 2.1, with the special exception on linking
-described in file LICENSE.
-
-This software 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.
-
-File modified by CEA (Commissariat à l'énergie atomique et aux
-                      énergies alternatives).
-

licenses/LGPLv3

-		   GNU LESSER GENERAL PUBLIC LICENSE
-                       Version 3, 29 June 2007
-
- Copyright (C) 2007 Free Software Foundation, Inc. <http://fsf.org/>
- Everyone is permitted to copy and distribute verbatim copies
- of this license document, but changing it is not allowed.
-
-
-  This version of the GNU Lesser General Public License incorporates
-the terms and conditions of version 3 of the GNU General Public
-License, supplemented by the additional permissions listed below.
-
-  0. Additional Definitions. 
-
-  As used herein, "this License" refers to version 3 of the GNU Lesser
-General Public License, and the "GNU GPL" refers to version 3 of the GNU
-General Public License.
-
-  "The Library" refers to a covered work governed by this License,
-other than an Application or a Combined Work as defined below.
-
-  An "Application" is any work that makes use of an interface provided
-by the Library, but which is not otherwise based on the Library.
-Defining a subclass of a class defined by the Library is deemed a mode
-of using an interface provided by the Library.
-
-  A "Combined Work" is a work produced by combining or linking an
-Application with the Library.  The particular version of the Library
-with which the Combined Work was made is also called the "Linked
-Version".
-
-  The "Minimal Corresponding Source" for a Combined Work means the
-Corresponding Source for the Combined Work, excluding any source code
-for portions of the Combined Work that, considered in isolation, are
-based on the Application, and not on the Linked Version.
-
-  The "Corresponding Application Code" for a Combined Work means the
-object code and/or source code for the Application, including any data
-and utility programs needed for reproducing the Combined Work from the
-Application, but excluding the System Libraries of the Combined Work.
-
-  1. Exception to Section 3 of the GNU GPL.
-
-  You may convey a covered work under sections 3 and 4 of this License
-without being bound by section 3 of the GNU GPL.
-
-  2. Conveying Modified Versions.
-
-  If you modify a copy of the Library, and, in your modifications, a
-facility refers to a function or data to be supplied by an Application
-that uses the facility (other than as an argument passed when the
-facility is invoked), then you may convey a copy of the modified
-version:
-
-   a) under this License, provided that you make a good faith effort to
-   ensure that, in the event an Application does not supply the
-   function or data, the facility still operates, and performs
-   whatever part of its purpose remains meaningful, or
-
-   b) under the GNU GPL, with none of the additional permissions of
-   this License applicable to that copy.
-
-  3. Object Code Incorporating Material from Library Header Files.
-
-  The object code form of an Application may incorporate material from
-a header file that is part of the Library.  You may convey such object
-code under terms of your choice, provided that, if the incorporated
-material is not limited to numerical parameters, data structure
-layouts and accessors, or small macros, inline functions and templates
-(ten or fewer lines in length), you do both of the following:
-
-   a) Give prominent notice with each copy of the object code that the
-   Library is used in it and that the Library and its use are
-   covered by this License.
-
-   b) Accompany the object code with a copy of the GNU GPL and this license
-   document.
-
-  4. Combined Works.
-
-  You may convey a Combined Work under terms of your choice that,
-taken together, effectively do not restrict modification of the
-portions of the Library contained in the Combined Work and reverse
-engineering for debugging such modifications, if you also do each of
-the following:
-
-   a) Give prominent notice with each copy of the Combined Work that
-   the Library is used in it and that the Library and its use are
-   covered by this License.
-
-   b) Accompany the Combined Work with a copy of the GNU GPL and this license
-   document.
-
-   c) For a Combined Work that displays copyright notices during
-   execution, include the copyright notice for the Library among
-   these notices, as well as a reference directing the user to the
-   copies of the GNU GPL and this license document.
-
-   d) Do one of the following:
-
-       0) Convey the Minimal Corresponding Source under the terms of this
-       License, and the Corresponding Application Code in a form
-       suitable for, and under terms that permit, the user to
-       recombine or relink the Application with a modified version of
-       the Linked Version to produce a modified Combined Work, in the
-       manner specified by section 6 of the GNU GPL for conveying
-       Corresponding Source.
-
-       1) Use a suitable shared library mechanism for linking with the
-       Library.  A suitable mechanism is one that (a) uses at run time
-       a copy of the Library already present on the user's computer
-       system, and (b) will operate properly with a modified version
-       of the Library that is interface-compatible with the Linked
-       Version. 
-
-   e) Provide Installation Information, but only if you would otherwise
-   be required to provide such information under section 6 of the
-   GNU GPL, and only to the extent that such information is
-   necessary to install and execute a modified version of the
-   Combined Work produced by recombining or relinking the
-   Application with a modified version of the Linked Version. (If
-   you use option 4d0, the Installation Information must accompany
-   the Minimal Corresponding Source and Corresponding Application
-   Code. If you use option 4d1, you must provide the Installation
-   Information in the manner specified by section 6 of the GNU GPL
-   for conveying Corresponding Source.)
-
-  5. Combined Libraries.
-
-  You may place library facilities that are a work based on the
-Library side by side in a single library together with other library
-facilities that are not Applications and are not covered by this
-License, and convey such a combined library under terms of your
-choice, if you do both of the following:
-
-   a) Accompany the combined library with a copy of the same work based
-   on the Library, uncombined with any other library facilities,
-   conveyed under the terms of this License.
-
-   b) Give prominent notice with the combined library that part of it
-   is a work based on the Library, and explaining where to find the
-   accompanying uncombined form of the same work.
-
-  6. Revised Versions of the GNU Lesser General Public License.
-
-  The Free Software Foundation may publish revised and/or new versions
-of the GNU Lesser General Public License from time to time. Such new
-versions will be similar in spirit to the present version, but may
-differ in detail to address new problems or concerns.
-
-  Each version is given a distinguishing version number. If the
-Library as you received it specifies that a certain numbered version
-of the GNU Lesser General Public License "or any later version"
-applies to it, you have the option of following the terms and
-conditions either of that published version or of any later version
-published by the Free Software Foundation. If the Library as you
-received it does not specify a version number of the GNU Lesser
-General Public License, you may choose any version of the GNU Lesser
-General Public License ever published by the Free Software Foundation.
-
-  If the Library as you received it specifies that a proxy can decide
-whether future versions of the GNU Lesser General Public License shall
-apply, that proxy's public statement of acceptance of any version is
-permanent authorization for you to choose that version for the
-Library.

src/libraries/utils/leftistheap.ml

-(**************************************************************************)
-(*                                                                        *)
-(*  Copyright (C) Jean-Christophe Filliatre                               *)
-(*                                                                        *)
-(*  This software is free software; you can redistribute it and/or        *)
-(*  modify it under the terms of the GNU Library General Public           *)
-(*  License version 2.1, with the special exception on linking            *)
-(*  described in file LICENSE.                                            *)
-(*                                                                        *)
-(*  This software 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.                  *)
-(*                                                                        *)
-(*  File modified by CEA (Commissariat à l'énergie atomique et aux        *)
-(*                        énergies alternatives).                         *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* Leftist heaps.
-
-   See for instance Chris Okasaki's "Purely Functional Data Structures" *)
-
-
-exception Empty
-
-module Make(X: Set.OrderedType) :
-sig
-  type t
-  val empty : t
-  val is_empty : t -> bool
-  val insert : X.t -> t -> t
-  val min : t -> X.t
-  val extract_min : t -> X.t * t
-  val merge : t -> t -> t
-  val fold: (X.t -> 'a -> 'a) -> t -> 'a -> 'a
-  val elements: t -> X.t list
-  val of_list: X.t list -> t
-end
-=
-struct
-
-  type t = E | T of int * X.t * t * t
-
-  let rank = function E -> 0 | T (r,_,_,_) -> r
-
-  let make x a b =
-    let ra = rank a and rb = rank b in
-    if ra >= rb then T (rb + 1, x, a, b) else T (ra + 1, x, b, a)
-
-  let empty = E
-
-  let is_empty = function E -> true | T _ -> false
-
-  let rec merge h1 h2 = match h1,h2 with
-    | E, h | h, E ->
-      h
-    | T (_,x,a1,b1), T (_,y,a2,b2) ->
-      if X.compare x y <= 0
-      then make x a1 (merge b1 h2)
-      else make y a2 (merge h1 b2)
-
-  let insert x h = merge (T (1, x, E, E)) h
-
-  let min = function E -> raise Empty | T (_,x,_,_) -> x
-
-  let extract_min = function
-    | E -> raise Empty
-    | T (_,x,a,b) -> x, merge a b
-
-  (* Added by CEA *)
-
-  let rec fold f h acc = match h with
-    | E -> acc
-    | T (_, x, h1, h2) -> fold f h2 (f x (fold f h1 acc))
-
-  let elements h = fold (fun e l -> e :: l) h []
-
-  (* can probably be improved *)
-  let of_list l = List.fold_left (fun h x -> insert x h) E  l
-
-end

src/libraries/utils/leftistheap.mli

-(**************************************************************************)
-(*                                                                        *)
-(*  Copyright (C) Jean-Christophe Filliatre                               *)
-(*                                                                        *)
-(*  This software is free software; you can redistribute it and/or        *)
-(*  modify it under the terms of the GNU Library General Public           *)
-(*  License version 2.1, with the special exception on linking            *)
-(*  described in file LICENSE.                                            *)
-(*                                                                        *)
-(*  This software 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.                  *)
-(*                                                                        *)
-(*  File modified by CEA (Commissariat à l'énergie atomique et aux        *)
-(*                        énergies alternatives).                         *)
-(*                                                                        *)
-(**************************************************************************)
-
-(** Leftist heaps.
-
-    See for instance Chris Okasaki's "Purely Functional Data Structures" *)
-
-exception Empty
-
-module Make(X: Set.OrderedType) :
-sig
-  type t
-
-  val empty: t
-
-  val is_empty: t -> bool
-    (** runs in O(1) *)
-
-  val insert: X.t -> t -> t
-    (** runs in O(log n) *)
-
-  val min: t -> X.t
-    (** runs in O(1) *)
-
-  val extract_min: t -> X.t * t
-    (** runs in O(log n) *)
-
-  val merge: t -> t -> t
-    (** runs in O(log max(n1, n2)) *)
-
-
-  (* Added by CEA *)
-
-  val fold: (X.t -> 'a -> 'a) -> t -> 'a -> 'a
-    (** elements are presented in an arbitrary order *)
-
-  val elements: t -> X.t list
-    (** the returned list is not sorted *)
-
-  val of_list: X.t list -> t
-end