package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file pool.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
(**************************************************************************)
(*                                                                        *)
(*  This file is part of WP plug-in of Frama-C.                           *)
(*                                                                        *)
(*  Copyright (C) 2007-2024                                               *)
(*    CEA (Commissariat a l'energie atomique et aux energies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  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, version 2.1.                                              *)
(*                                                                        *)
(*  It 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.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

(* -------------------------------------------------------------------------- *)
(* ---     Fresh Variable Management                                      --- *)
(* -------------------------------------------------------------------------- *)

module type Type =
sig
  type t
  val dummy : t
  val equal : t -> t -> bool
  val compare : t -> t -> int
end

module Make(T : Type) =
struct

  type var = {
    vid : int ;
    vbase : string ;
    vrank : int ;
    vtau : T.t ;
  }

  let hash_var x = Hcons.hash_pair x.vrank (Hashtbl.hash x.vbase)

  let pretty fmt x = Format.fprintf fmt "%s_%d" x.vbase x.vrank

  (* HASHCONSING *)

  module W = Weak.Make
      (struct
        type t = var
        let hash = hash_var
        let equal x y =
          x.vbase = y.vbase && x.vrank = y.vrank && T.equal x.vtau y.vtau
      end)

  let kid = ref 0
  let hmap = W.create 32993 (* 3-th Leyland Prime number *)

  let insert base rank tau =
    let x0 = {
      vid = 0 ;
      vbase = base ;
      vrank = rank ;
      vtau = tau ;
    } in
    try W.find hmap x0
    with Not_found ->
      let k = let i = !kid in (assert (i <> -1) ; incr kid ; i) in
      let x = { x0 with vid = k } in W.add hmap x ; x

  let dummy = insert "" 0 T.dummy

  let hash x = x.vid
  let equal = (==)
  let compare x y =
    let cmp = String.compare x.vbase y.vbase in
    if cmp <> 0 then cmp else
      let cmp = Stdlib.compare x.vrank y.vrank in
      if cmp <> 0 then cmp else
        T.compare x.vtau y.vtau

  (* POOL *)

  type pool = (string,int ref) Hashtbl.t
  let create ?copy () = match copy with
    | None -> Hashtbl.create 131
    | Some pool -> Hashtbl.copy pool

  let counter pool base =
    try Hashtbl.find pool base
    with Not_found ->
      let c = ref 0 in Hashtbl.add pool base c ; c

  let add pool x =
    let c = counter pool x.vbase in
    if !c <= x.vrank then c := succ x.vrank

  let next pool base =
    let c = counter pool base in
    let k = !c in incr c ; k

  let fresh pool base tau =
    let rank = next pool base in
    insert base rank tau

  let alpha pool x = fresh pool x.vbase x.vtau

end
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct