products/Sources/formale Sprachen/Coq/clib/  image not shown  

Quellcode-Bibliothek

hier können Sie eine Nachricht absetzen

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: int.ml   Sprache: SML

Original von: Coq©
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

type t = int

external equal : int -> int -> bool = "%eq"

external compare : int -> int -> int = "caml_int_compare"

let hash i = i land 0x3FFFFFFF

module Self =
struct
  type t = int
  let compare = compare
end

module Set = Set.Make(Self)
module Map =
struct
  include CMap.Make(Self)

  type 'a map = 'a CMap.Make(Self).t

  type 'a _map =
  | MEmpty
  | MNode of 'a map * int * 'a * 'a map * int

  let map_prj : 'a map -> 'a _map = Obj.magic

  let rec find i s = match map_prj s with
  | MEmpty -> raise Not_found
  | MNode (l, k, v, r, h) ->
    if i < k then find i l
    else if i = k then v
    else find i r

  let rec find_opt i s = match map_prj s with
  | MEmpty -> None
  | MNode (l, k, v, r, h) ->
    if i < k then find_opt i l
    else if i = k then Some v
    else find_opt i r
end

module List = struct
  let mem = List.memq
  let assoc = List.assq
  let mem_assoc = List.mem_assq
  let remove_assoc = List.remove_assq
end

let min (i : int) j = if i < j then i else j

(** Utility function *)
let rec next from upto =
  if from < upto then next (2 * from + 1) upto
  else from


module PArray =
struct

  type 'a t = 'a data ref
  and 'a data =
  | Root of 'a option array
  | DSet of int * 'a option * 'a t

  let empty n = ref (Root (Array.make n None))

  let rec rerootk t k = match !t with
  | Root _ -> k ()
  | DSet (i, v, t') ->
    let next () = match !t' with
    | Root a as n ->
      let v' = Array.unsafe_get a i in
      let () = Array.unsafe_set a i v in
      let () = t := n in
      let () = t' := DSet (i, v', t) in
      k ()
    | DSet _ -> assert false
    in
    rerootk t' next

  let reroot t = rerootk t (fun () -> ())

  let get t i =
  let () = assert (0 <= i) in
  match !t with
  | Root a ->
    if Array.length a <= i then None
    else Array.unsafe_get a i
  | DSet _ ->
    let () = reroot t in
    match !t with
    | Root a ->
      if Array.length a <= i then None
      else Array.unsafe_get a i
    | DSet _ -> assert false

  let set t i v =
    let () = assert (0 <= i) in
    let () = reroot t in
    match !t with
    | DSet _ -> assert false
    | Root a as n ->
      let len = Array.length a in
      if i < len then
        let old = Array.unsafe_get a i in
        if old == v then t
        else
          let () = Array.unsafe_set a i v in
          let res = ref n in
          let () = t := DSet (i, old, res) in
          res
      else match v with
      | None -> t (* Nothing to do! *)
      | Some _ -> (* we must resize *)
        let nlen = next len (succ i) in
        let nlen = min nlen Sys.max_array_length in
        let () = assert (i < nlen) in
        let a' = Array.make nlen None in
        let () = Array.blit a 0 a' 0 len in
        let () = Array.unsafe_set a' i v in
        let res = ref (Root a') in
        let () = t := DSet (i, None, res) in
        res

end

module PMap =
struct

  type key = int

  (** Invariants:

    1. an empty map is always [Empty].
    2. the set of the [Map] constructor remembers the present keys.
  *)
  type 'a t = Empty | Map of Set.t * 'a PArray.t

  let empty = Empty

  let is_empty = function
  | Empty -> true
  | Map _ -> false

  let singleton k x =
    let len = next 19 (k + 1) in
    let len = min Sys.max_array_length len in
    let v = PArray.empty len in
    let v = PArray.set v k (Some x) in
    let s = Set.singleton k in
    Map (s, v)

  let add k x = function
  | Empty -> singleton k x
  | Map (s, v) ->
    let s = match PArray.get v k with
    | None -> Set.add k s
    | Some _ -> s
    in
    let v = PArray.set v k (Some x) in
    Map (s, v)

  let remove k = function
  | Empty -> Empty
  | Map (s, v) ->
    let s = Set.remove k s in
    if Set.is_empty s then Empty
    else
      let v = PArray.set v k None in
      Map (s, v)

  let mem k = function
  | Empty -> false
  | Map (_, v) ->
    match PArray.get v k with
    | None -> false
    | Some _ -> true

  let find k = function
  | Empty -> raise Not_found
  | Map (_, v) ->
    match PArray.get v k with
    | None -> raise Not_found
    | Some x -> x

  let iter f = function
  | Empty -> ()
  | Map (s, v) ->
    let iter k = match PArray.get v k with
    | None -> ()
    | Some x -> f k x
    in
    Set.iter iter s

  let fold f m accu = match m with
  | Empty -> accu
  | Map (s, v) ->
    let fold k accu = match PArray.get v k with
    | None -> accu
    | Some x -> f k x accu
    in
    Set.fold fold s accu

  let exists f m = match m with
  | Empty -> false
  | Map (s, v) ->
    let exists k = match PArray.get v k with
    | None -> false
    | Some x -> f k x
    in
    Set.exists exists s

  let for_all f m = match m with
  | Empty -> true
  | Map (s, v) ->
    let for_all k = match PArray.get v k with
    | None -> true
    | Some x -> f k x
    in
    Set.for_all for_all s

  let cast = function
  | Empty -> Map.empty
  | Map (s, v) ->
    let bind k = match PArray.get v k with
    | None -> assert false
    | Some x -> x
    in
    Map.bind bind s

  let domain = function
  | Empty -> Set.empty
  | Map (s, _) -> s

end

¤ Dauer der Verarbeitung: 0.3 Sekunden  (vorverarbeitet)  ¤



Kontakt
Drucken
Kontakt
sprechenden Kalenders

in der Quellcodebibliothek suchen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff