package why3find
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
A Why3 Package Manager
Install
dune-project
Dependency
Authors
Maintainers
Sources
why3find-1.3.0.tar.gz
md5=435da830a513fd91ec5411c91126b763
sha512=fd8b04eb16d569c0dc9e5595a40b174d7858121b080c81d459b2f28fb3af1ebc32ef408859d5c1c5f45c61790625c027c2ecfc3d45e597943543de7212bab8d6
doc/src/why3find.utils/rangemap.ml.html
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
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>