package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.17.0.tar.gz
sha512=2f77bcb5211018b5d46320fd39fd34450eeb654aca44551b28bb50a2364398c4b34587630b6558db867ecfb63b246fd3e29dc2375f99967ff62bc002db9c3250
doc/src/coq-core.gramlib/stream.ml.html
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 'a t = { mutable count : int; mutable data : 'a data } and 'a data = Sempty | Scons of 'a * 'a data | Sgen of 'a gen | Sbuffio : buffio -> char data and 'a gen = { mutable curr : 'a option option; func : unit -> 'a option } and buffio = { ic : in_channel; buff : bytes; mutable len : int; mutable ind : int } exception Failure exception Error of string 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 v. v t -> v option = fun 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 () 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 v. v t -> unit = fun 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) | _ -> match peek s with None -> () | Some _ -> junk s let rec nget n s = if n <= 0 then [], s.data, 0 else match peek s with Some a -> junk s; let (al, d, k) = nget (pred n) s in a :: al, Scons (a, d), succ k | None -> [], s.data, 0 let npeek n s = let (al, d, len) = nget n s in s.count <- (s.count - len); s.data <- d; al let nth n st = try List.nth (npeek (n+1) st) n with Stdlib.Failure _ -> raise Failure let rec njunk n st = if n <> 0 then (junk st; njunk (n-1) st) let next s = match peek s with Some a -> junk s; a | None -> raise Failure let is_empty s = match peek 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}}
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>