From de4ad53ebc47d1628d2b5fe6f3eb5c0b4ff4c496 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Mon, 10 May 2021 13:28:08 -0700 Subject: [PATCH] [sledge] Add Random access list module Reviewed By: ngorogiannis Differential Revision: D27996962 fbshipit-source-id: ad07bafd3 --- sledge/nonstdlib/NS.ml | 1 + sledge/nonstdlib/NS.mli | 1 + sledge/nonstdlib/ral.ml | 14 ++++++++++++++ sledge/nonstdlib/ral.mli | 18 ++++++++++++++++++ 4 files changed, 34 insertions(+) create mode 100644 sledge/nonstdlib/ral.ml create mode 100644 sledge/nonstdlib/ral.mli diff --git a/sledge/nonstdlib/NS.ml b/sledge/nonstdlib/NS.ml index 54acea421..27a89798f 100644 --- a/sledge/nonstdlib/NS.ml +++ b/sledge/nonstdlib/NS.ml @@ -45,6 +45,7 @@ module Multiset = Multiset module Option = Option include Option.Import module Q = Q_ext +module RAL = Ral module Set = NSSet module Sign = Sign module String = String diff --git a/sledge/nonstdlib/NS.mli b/sledge/nonstdlib/NS.mli index bb207eadf..2c2115102 100644 --- a/sledge/nonstdlib/NS.mli +++ b/sledge/nonstdlib/NS.mli @@ -155,6 +155,7 @@ type ('a, 'b) zero_one_many2 = Zero2 | One2 of 'a * 'b | Many2 module Pair = Containers.Pair module List = List +module RAL = Ral module Array = Array module IArray = IArray include module type of IArray.Import diff --git a/sledge/nonstdlib/ral.ml b/sledge/nonstdlib/ral.ml new file mode 100644 index 000000000..bf9754b1b --- /dev/null +++ b/sledge/nonstdlib/ral.ml @@ -0,0 +1,14 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! NS0 +include CCRAL + +let pp ?pre ?suf sep pp_elt fs ral = + List.pp ?pre ?suf sep pp_elt fs (to_list ral) + +let fold l s ~f = fold ~f:(fun s x -> f x s) ~x:s l diff --git a/sledge/nonstdlib/ral.mli b/sledge/nonstdlib/ral.mli new file mode 100644 index 000000000..39b741f98 --- /dev/null +++ b/sledge/nonstdlib/ral.mli @@ -0,0 +1,18 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! NS0 +include module type of CCRAL + +val pp : + ?pre:(unit, unit) fmt + -> ?suf:(unit, unit) fmt + -> (unit, unit) fmt + -> 'a pp + -> 'a t pp + +val fold : 'a t -> 's -> f:('a -> 's -> 's) -> 's