package coq-core

  1. Overview
  2. Docs
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.