Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556575859606162636465666768697071727374757677787980818283(************************************************************************)(* * The Rocq Prover / The Rocq Development Team *)(* v * Copyright INRIA, CNRS and contributors *)(* <O___,, * (see version control and CREDITS file for authors & dates) *)(* \VV/ **************************************************************)(* // * This file is distributed under the terms of the *)(* * GNU Lesser General Public License Version 2.1 *)(* * (see LICENSE file for the text of the license) *)(************************************************************************)
type 'a t = 'a option array option ref
let return a : 'a t = ref (Some a)
let if_valid (r : 'a t) = match !r with | Some a -> a | None -> invalid_arg "Tried to reuse invalidated NoDupArray."
(** Non-destructive get operator *)let (let+) r f = f (if_valid r)
let destruct_get r = let+ a = r in r := None; a
(** Destructive get operator *)let (let-) r f = f (destruct_get r)
let update r f : 'b t = let- a = r in return (f a)
(** Updating functor operator *)let (let*) = update
let make n = return (Array.make n None)
let get i a = let+ a = a in a.(i)
let is_filled i a = let+ a = a in Option.has_some a.(i)
let add i e a = let* a = a in begin match a.(i) with | None -> a.(i) <- Some e | Some _ -> invalid_arg "Tried to add duplicate in NoDupArray." end; a
let fill_remaining e a = let* a = a in Array.iteri (fun i elt -> begin match elt with | None -> a.(i) <- Some e | Some _ -> () end) a; a
let to_array a = let- a = a in Array.map (function Some e -> e | None -> invalid_arg "Tried to cast non-full NoDupArray.") a
let to_array_opt a = let- a = a in let exception Stop in try Some (Array.map (function Some e -> e | None -> raise Stop) a) with Stop -> None
module Internal = struct
let unsafe_to_array = if_validend