package why3find

  1. Overview
  2. Docs
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/ropes.ml.html

Source file ropes.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
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
(**************************************************************************)
(*                                                                        *)
(*  SPDX-License-Identifier LGPL-2.1                                      *)
(*  Copyright (C)                                                         *)
(*  CEA (Commissariat à l'énergie atomique et aux énergies alternatives)  *)
(*                                                                        *)
(**************************************************************************)

type t =
  | Empty
  | Line of string
  | Cat of { lines : int ; left : t ; right : t }

(* -------------------------------------------------------------------------- *)
(* --- Accessors                                                          --- *)
(* -------------------------------------------------------------------------- *)

let lines = function Empty -> 0 | Line _ -> 1 | Cat { lines } -> lines

let rec line_at l = function
  | Empty -> invalid_arg "Ropes.line_at"
  | Line s -> if l <> 0 then invalid_arg "Ropes.line_at" ; s
  | Cat { left ; right } ->
    let n = lines left in
    if l < n then line_at l left else line_at (l-n) right

let char_at (p:Range.pos) a = String.get (line_at p.line a) p.col

let eof a =
  let rec last line = function
    | Empty -> Range.at ~line ()
    | Line s -> Range.at ~line ~col:(String.length s) ()
    | Cat { left ; right } -> last (line + lines left) right
  in last 0 a

(* -------------------------------------------------------------------------- *)
(* --- Balancing                                                          --- *)
(* -------------------------------------------------------------------------- *)

let make a b = Cat { lines = lines a + lines b ; left = a ; right = b }

let rec concat a b =
  match a,b with
  | Empty,c | c,Empty -> c
  | Cat { left ; right } , _ when lines a > lines b ->
    make left (concat right b)
  | _ , Cat { left ; right } when lines a < lines b ->
    make (concat a left) right
  | _ -> make a b

let (++) = concat

(* -------------------------------------------------------------------------- *)
(* --- Iterators                                                          --- *)
(* -------------------------------------------------------------------------- *)

let rec fold_left f w = function
  | Empty -> w
  | Line s -> f w s
  | Cat { left ; right } -> fold_left f (fold_left f w left) right

let rec fold_right f a w =
  match a with
  | Empty -> w
  | Line s -> f s w
  | Cat { left ; right } -> fold_right f left (fold_right f right w)

let iter f a = fold_left (fun () s -> f s) () a
let iteri f a = ignore @@ fold_left (fun k s -> f k s ; succ k) 0 a

let length = fold_left (fun n s -> n + 1 + String.length s) 0

(* -------------------------------------------------------------------------- *)
(* --- Printers                                                           --- *)
(* -------------------------------------------------------------------------- *)

let bline b s = Buffer.add_string b s ; Buffer.add_char b '\n' ; b
let blines = fold_left bline

let to_buffer b s = ignore @@ blines b s

let to_channel out s =
  ignore @@
  fold_left (fun o s -> output_string o s ; output_char o '\n' ; o) out s

let to_string = function
  | Empty -> ""
  | Line n -> n ^ "\n"
  | a -> Buffer.contents @@ blines (Buffer.create 0) a

let pretty fmt s =
  ignore @@
  fold_left
    (fun fmt s ->
       Format.pp_print_string fmt s ;
       Format.pp_print_newline fmt () ;
       fmt)
    fmt s

(* -------------------------------------------------------------------------- *)
(* --- Constructors                                                       --- *)
(* -------------------------------------------------------------------------- *)
let empty = Empty
let trim =
  let rec trimk l r = function
    | Empty -> Empty
    | Line "" -> Empty
    | Line _ as a -> a
    | Cat { left ; right } ->
      (if l then trimk true false left else left) ++
      (if r then trimk false true right else right)
  in trimk true true

let split s =
  List.fold_left (fun w s -> w ++ Line s) Empty (String.split_on_char '\n' s)

let rec endline = function
  | (Empty | Line _) as a -> a
  | Cat { left ; right = Line "" } -> left
  | Cat { left ; right } -> make left (endline right)

let of_string s =
  if String.length s = 0 then Empty else endline @@ split s

let prefix_string c s =
  if c <= 0 then "" else
    let n = String.length s in
    if c < n then String.sub s 0 c else s

let suffix_string c s =
  if c <= 0 then s else
    let n = String.length s in
    if c < n then String.sub s c (n-c) else ""

let prefix (p:Range.pos) a =
  let rec wprefix acc l = function
    | Empty -> acc, ""
    | Line s -> acc, if l = 0 then s else ""
    | Cat { left ; right } ->
      let n = lines left in
      if l < n then wprefix acc l left else wprefix (acc ++ left) (l-n) right
  in let w,s =  wprefix Empty p.line a in w , prefix_string p.col s

let suffix (p:Range.pos) a =
  let rec wsuffix l a acc =
    match a with
    | Empty -> "", acc
    | Line s -> (if l = 0 then s else ""), acc
    | Cat { left ; right } ->
      let n = lines left in
      if l < n then wsuffix l left (right ++ acc) else wsuffix (l-n) right acc
  in let s,w =  wsuffix p.line a Empty in suffix_string p.col s, w

let update (p,q) s a =
  if Range.(<<=) p q then
    begin
      let l,u = prefix p a in
      let v,r = suffix q a in
      l ++ split (u ^ s ^ v) ++ r
    end
  else a

let substring ((p,q):Range.range) a =
  let l1 = p.line in
  let l2 = q.line in
  if l1 > l2 then "" else
  if l1 < l2 then
    let wq = Range.at ~line:(l2-l1-1) ~col:q.col () in
    let u,w = suffix p a in
    let w,v = prefix wq w in
    let b = Buffer.create 0 in
    ignore (bline b u) ;
    ignore (blines b w) ;
    Buffer.add_string b v ;
    Buffer.contents b ;
  else
    let u = line_at l1 a in
    let p = max p.col 0 in
    let q = min q.col (String.length u) in
    if p < q then String.sub u p (q-p) else ""