package coq-core

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

Source file stream.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
(**************************************************************************)
(*                                                                        *)
(*                                 OCaml                                  *)
(*                                                                        *)
(*         Daniel de Rauglaudre, projet Cristal, INRIA Rocquencourt       *)
(*                                                                        *)
(*   Copyright 1997 Institut National de Recherche en Informatique et     *)
(*     en Automatique.                                                    *)
(*                                                                        *)
(*   All rights reserved.  This file is distributed under the terms of    *)
(*   the GNU Lesser General Public License version 2.1, with the          *)
(*   special exception on linking described in the file LICENSE.          *)
(*                                                                        *)
(**************************************************************************)

type ('e,'a) t = { mutable count : int; mutable data : ('e,'a) data }
and ('e,'a) data =
    Sempty
  | Scons of 'a * ('e,'a) data
  | Sgen of ('e,'a) gen
  | Sbuffio : buffio -> (unit,char) data
and ('e,'a) gen = { mutable curr : 'a option option; func : 'e -> 'a option }
and buffio =
  { ic : in_channel; buff : bytes; mutable len : int; mutable ind : int }

exception Failure

let count { count } = count

let fill_buff b =
  b.len <- input b.ic b.buff 0 (Bytes.length b.buff); b.ind <- 0

let peek : type e v. e -> (e,v) t -> v option = fun e s ->
 (* consult the first item of s *)
 match s.data with
   Sempty -> None
 | Scons (a, _) -> Some a
 | Sgen {curr = Some a} -> a
 | Sgen g -> let x = g.func e in g.curr <- Some x; x
 | Sbuffio b ->
     if b.ind >= b.len then fill_buff b;
     if b.len == 0 then begin s.data <- Sempty; None end
     else Some (Bytes.unsafe_get b.buff b.ind)


let rec junk : type e v. e -> (e,v) t -> unit = fun e s ->
  match s.data with
    Scons (_, d) -> s.count <- (succ s.count); s.data <- d
  | Sgen ({curr = Some _} as g) -> s.count <- (succ s.count); g.curr <- None
  | Sbuffio b ->
      if b.ind >= b.len then fill_buff b;
      if b.len == 0 then s.data <- Sempty
      else (s.count <- (succ s.count); b.ind <- succ b.ind)
  | Sempty -> ()
  | Sgen { curr = None } ->
      match peek e s with
        None -> ()
      | Some _ -> junk e s

let rec nget e n s =
  if n <= 0 then [], s.data, 0
  else
    match peek e s with
      Some a ->
        junk e s;
        let (al, d, k) = nget e (pred n) s in a :: al, Scons (a, d), succ k
    | None -> [], s.data, 0


let npeek e n s =
  let (al, d, len) = nget e n s in
  s.count <- (s.count - len);
  s.data <- d;
  al

let nth e n st =
  try List.nth (npeek e (n+1) st) n
  with Stdlib.Failure _ -> raise Failure

let rec njunk e n st =
  if n <> 0 then (junk e st; njunk e (n-1) st)

let next e s =
  match peek e s with
    Some a -> junk e s; a
  | None -> raise Failure


let is_empty e s =
  match peek e s with
  | Some _ -> false
  | None -> true


(* Stream building functions *)

let from ?(offset=0) f = {count = offset; data = Sgen {curr = None; func = f}}

(* NB we need the thunk for value restriction *)
let empty () = {count = 0; data = Sempty}

let of_string ?(offset=0) s =
  let count = ref 0 in
  from ~offset (fun () ->
    let c = !count in
    if c < String.length s
    then (incr count; Some s.[c])
    else None)


let of_channel ic =
  {count = 0;
        data = Sbuffio {ic = ic; buff = Bytes.create 4096; len = 0; ind = 0}}
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