BuiltinIteration.ml1 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(******************************************************************************) (* *) (* Monolith *) (* *) (* François Pottier *) (* *) (* Copyright Inria. All rights reserved. This file is distributed under the *) (* terms of the GNU Lesser General Public License as published by the Free *) (* Software Foundation, either version 3 of the License, or (at your *) (* option) any later version, as described in the file LICENSE. *) (* *) (******************************************************************************) open Spec open Support (* This file offers ready-made functions that help deal with iteration functions. *) type ('a, 'c) iter = ('a, 'c) Iteration.iter let iter spec = map_into Iteration.elements_of_iter Iteration.ElementsOfIter.code spec type ('a, 's, 'c) foldr = ('a, 's, 'c) Iteration.foldr let foldr spec = map_into Iteration.elements_of_foldr Iteration.ElementsOfFoldr.code spec type ('a, 's, 'c) foldl = ('a, 's, 'c) Iteration.foldl let foldl spec = map_into Iteration.elements_of_foldl Iteration.ElementsOfFoldl.code spec type ('a, 'b, 'c) iteri = ('a, 'b, 'c) Iteration.iteri let iteri spec = map_into Iteration.elements_of_iteri Iteration.ElementsOfIteri.code spec type ('a, 'b, 's, 'c) foldri = ('a, 'b, 's, 'c) Iteration.foldri let foldri spec = map_into Iteration.elements_of_foldri Iteration.ElementsOfFoldri.code spec type ('a, 'b, 's, 'c) foldli = ('a, 'b, 's, 'c) Iteration.foldli let foldli spec = map_into Iteration.elements_of_foldli Iteration.ElementsOfFoldli.code spec