package why3find

  1. Overview
  2. Docs

Source file rangemap.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
(**************************************************************************)
(*                                                                        *)
(*  SPDX-License-Identifier LGPL-2.1                                      *)
(*  Copyright (C)                                                         *)
(*  CEA (Commissariat à l'énergie atomique et aux énergies alternatives)  *)
(*                                                                        *)
(**************************************************************************)

open Range

type 'a t =
  | Empty
  | Range of { range : range ; value : 'a ; inner : 'a t }
  | Node of { range : range ; left : 'a t ; right : 'a t }

let rec dump pp fmt = function
  | Empty -> Format.fprintf fmt "-"
  | Range { range ; value ; inner } ->
    Format.fprintf fmt "@[<hv 2>{ %a@ value: %a@ inner: %a }@]"
      Range.pp_range range pp value (dump pp) inner
  | Node { range ; left ; right } ->
    Format.fprintf fmt "@[<hv 2>{ %a@ left: %a@ right: %a }@]"
      Range.pp_range range (dump pp) left (dump pp) right
[@@ warning "-32"]

let empty = Empty

let compare (a,b) (c,d) =
  let cmp = compare c a in
  if cmp <> 0 then cmp else
    compare b d

let inside p (a,b) = a <<= p && p << b

let subset (a,b) (c,d) = c <<= a && b <<= d

let compare_entry x y =
  match x,y with
  | None, None -> 0
  | Some _, None -> (-1)
  | None, Some _ -> (+1)
  | Some(a,_) , Some (b,_) -> compare a b

let rec find_opt p = function
  | Empty -> None
  | Range { range ; value ; inner } ->
    begin
      match find_opt p inner with
      | Some _ as r -> r
      | None -> if inside p range then Some(range,value) else None
    end
  | Node { range ; left ; right } ->
    if inside p range then
      let l = find_opt p left in
      let r = find_opt p right in
      if compare_entry l r < 0 then l else r
    else None

let find p t = match find_opt p t with None -> raise Not_found | Some e -> e

let singleton rg v = Range { range = rg ; value = v ; inner = Empty }

let range = function
  | Empty -> assert false
  | Range { range } | Node { range } -> range

let (++) u v =
  let a,b = range u in
  let c,d = range v in
  if b <<= c then
    Node { range = a,d ; left = u ; right = v }
  else
  if d <<= a then
    Node { range = c,b ; left = v ; right = u }
  else
    let p = if a <<= c then a else c in
    let q = if b <<= d then d else b in
    Node { range = p,q ; left = u ; right = v }

let union a b =
  match a,b with
  | Empty,c | c,Empty -> c
  | _ -> a ++ b

let rec add rg v = function
  | Empty -> singleton rg v
  | Range r as a ->
    if subset rg r.range then
      if subset r.range rg then
        Range { r with value = v }
      else
        Range { r with inner = add rg v r.inner }
    else
      singleton rg v ++ a
  | Node { range = ra ; left ; right } as a ->
    if subset ra rg then
      Range { range = rg ; value = v ; inner =  a }
    else
    if rg <<< range right then add rg v left ++ right else
    if range left <<< rg then left ++ add rg v right else
      singleton rg v ++ a

let rec iter f = function
  | Empty -> ()
  | Range r ->
    iter f r.inner ;
    f r.range r.value
  | Node { left ; right } -> iter f left ; iter f right