package coq-core
The Coq Proof Assistant -- Core Binaries and Tools
Install
Dune Dependency
Authors
Maintainers
Sources
coq-8.19.2.tar.gz
md5=5d1187d5e44ed0163f76fb12dabf012e
sha512=91bc81530fa4f6498961583ad51eac5001f139881788b88e360a866ad8e2a6e2c5bce86d1a580ab4cd4782bf49d48318767df82471ce33ba3ac143e5569ad33c
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 ('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}}
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>