Mercurial > urweb

annotate src/core_util.sig @ 1327:1cc67fdac4d3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
New argument to transactional free functions, to specify whether we are about to retry
author Adam Chlipala <adam@chlipala.net>
date Sat, 04 Dec 2010 11:15:20 -0500
parents 338be96f8533
children
rev   line source
adamc@16 1 (* Copyright (c) 2008, Adam Chlipala
adamc@16 2 * All rights reserved.
adamc@16 3 *
adamc@16 4 * Redistribution and use in source and binary forms, with or without
adamc@16 5 * modification, are permitted provided that the following conditions are met:
adamc@16 6 *
adamc@16 7 * - Redistributions of source code must retain the above copyright notice,
adamc@16 8 * this list of conditions and the following disclaimer.
adamc@16 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@16 10 * this list of conditions and the following disclaimer in the documentation
adamc@16 11 * and/or other materials provided with the distribution.
adamc@16 12 * - The names of contributors may not be used to endorse or promote products
adamc@16 13 * derived from this software without specific prior written permission.
adamc@16 14 *
adamc@16 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@16 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@16 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@16 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@16 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@16 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@16 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@16 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@16 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@16 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@16 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@16 26 *)
adamc@16 27
adamc@16 28 signature CORE_UTIL = sig
adamc@16 29
adamc@16 30 structure Kind : sig
adamc@193 31 val compare : Core.kind * Core.kind -> order
adamc@193 32
adamc@626 33 val mapfoldB : {kind : ('context, Core.kind', 'state, 'abort) Search.mapfolderB,
adamc@626 34 bind : 'context * string -> 'context}
adamc@626 35 -> ('context, Core.kind, 'state, 'abort) Search.mapfolderB
adamc@16 36 val mapfold : (Core.kind', 'state, 'abort) Search.mapfolder
adamc@16 37 -> (Core.kind, 'state, 'abort) Search.mapfolder
adamc@16 38 val map : (Core.kind' -> Core.kind') -> Core.kind -> Core.kind
adamc@16 39 val exists : (Core.kind' -> bool) -> Core.kind -> bool
adamc@626 40 val mapB : {kind : 'context -> Core.kind' -> Core.kind',
adamc@626 41 bind : 'context * string -> 'context}
adamc@626 42 -> 'context -> (Core.kind -> Core.kind)
adamc@16 43 end
adamc@16 44
adamc@16 45 structure Con : sig
adamc@193 46 val compare : Core.con * Core.con -> order
adamc@193 47
adamc@16 48 datatype binder =
adamc@626 49 RelK of string
adamc@626 50 | RelC of string * Core.kind
adamc@626 51 | NamedC of string * int * Core.kind * Core.con option
adamc@16 52
adamc@626 53 val mapfoldB : {kind : ('context, Core.kind', 'state, 'abort) Search.mapfolderB,
adamc@16 54 con : ('context, Core.con', 'state, 'abort) Search.mapfolderB,
adamc@16 55 bind : 'context * binder -> 'context}
adamc@16 56 -> ('context, Core.con, 'state, 'abort) Search.mapfolderB
adamc@16 57 val mapfold : {kind : (Core.kind', 'state, 'abort) Search.mapfolder,
adamc@16 58 con : (Core.con', 'state, 'abort) Search.mapfolder}
adamc@16 59 -> (Core.con, 'state, 'abort) Search.mapfolder
adamc@16 60
adamc@16 61 val map : {kind : Core.kind' -> Core.kind',
adamc@16 62 con : Core.con' -> Core.con'}
adamc@16 63 -> Core.con -> Core.con
adamc@16 64
adamc@626 65 val mapB : {kind : 'context -> Core.kind' -> Core.kind',
adamc@16 66 con : 'context -> Core.con' -> Core.con',
adamc@16 67 bind : 'context * binder -> 'context}
adamc@16 68 -> 'context -> (Core.con -> Core.con)
adamc@23 69
adamc@23 70 val fold : {kind : Core.kind' * 'state -> 'state,
adamc@680 71 con : Core.con' * 'state -> 'state}
adamc@680 72 -> 'state -> Core.con -> 'state
adamc@680 73
adamc@16 74 val exists : {kind : Core.kind' -> bool,
adamc@16 75 con : Core.con' -> bool} -> Core.con -> bool
adamc@1185 76
adamc@1185 77 val existsB : {kind : 'context * Core.kind' -> bool,
adamc@1185 78 con : 'context * Core.con' -> bool,
adamc@1185 79 bind : 'context * binder -> 'context}
adamc@1185 80 -> 'context -> Core.con -> bool
adamc@680 81
adamc@193 82 val foldMap : {kind : Core.kind' * 'state -> Core.kind' * 'state,
adamc@193 83 con : Core.con' * 'state -> Core.con' * 'state}
adamc@193 84 -> 'state -> Core.con -> Core.con * 'state
adamc@16 85 end
adamc@16 86
adamc@16 87 structure Exp : sig
adamc@479 88 val compare : Core.exp * Core.exp -> order
adamc@479 89
adamc@16 90 datatype binder =
adamc@626 91 RelK of string
adamc@626 92 | RelC of string * Core.kind
adamc@20 93 | NamedC of string * int * Core.kind * Core.con option
adamc@16 94 | RelE of string * Core.con
adamc@109 95 | NamedE of string * int * Core.con * Core.exp option * string
adamc@16 96
adamc@626 97 val mapfoldB : {kind : ('context, Core.kind', 'state, 'abort) Search.mapfolderB,
adamc@16 98 con : ('context, Core.con', 'state, 'abort) Search.mapfolderB,
adamc@16 99 exp : ('context, Core.exp', 'state, 'abort) Search.mapfolderB,
adamc@16 100 bind : 'context * binder -> 'context}
adamc@16 101 -> ('context, Core.exp, 'state, 'abort) Search.mapfolderB
adamc@16 102 val mapfold : {kind : (Core.kind', 'state, 'abort) Search.mapfolder,
adamc@16 103 con : (Core.con', 'state, 'abort) Search.mapfolder,
adamc@16 104 exp : (Core.exp', 'state, 'abort) Search.mapfolder}
adamc@16 105 -> (Core.exp, 'state, 'abort) Search.mapfolder
adamc@16 106
adamc@16 107 val map : {kind : Core.kind' -> Core.kind',
adamc@16 108 con : Core.con' -> Core.con',
adamc@16 109 exp : Core.exp' -> Core.exp'}
adamc@16 110 -> Core.exp -> Core.exp
adamc@626 111 val mapB : {kind : 'context -> Core.kind' -> Core.kind',
adamc@21 112 con : 'context -> Core.con' -> Core.con',
adamc@21 113 exp : 'context -> Core.exp' -> Core.exp',
adamc@21 114 bind : 'context * binder -> 'context}
adamc@21 115 -> 'context -> (Core.exp -> Core.exp)
adamc@23 116
adamc@23 117 val fold : {kind : Core.kind' * 'state -> 'state,
adamc@23 118 con : Core.con' * 'state -> 'state,
adamc@23 119 exp : Core.exp' * 'state -> 'state}
adamc@23 120 -> 'state -> Core.exp -> 'state
adamc@484 121
adamc@626 122 val foldB : {kind : 'context * Core.kind' * 'state -> 'state,
adamc@484 123 con : 'context * Core.con' * 'state -> 'state,
adamc@484 124 exp : 'context * Core.exp' * 'state -> 'state,
adamc@484 125 bind : 'context * binder -> 'context}
adamc@484 126 -> 'context -> 'state -> Core.exp -> 'state
adamc@23 127
adamc@16 128 val exists : {kind : Core.kind' -> bool,
adamc@16 129 con : Core.con' -> bool,
adamc@16 130 exp : Core.exp' -> bool} -> Core.exp -> bool
adamc@443 131
adamc@626 132 val existsB : {kind : 'context * Core.kind' -> bool,
adamc@479 133 con : 'context * Core.con' -> bool,
adamc@479 134 exp : 'context * Core.exp' -> bool,
adamc@479 135 bind : 'context * binder -> 'context}
adamc@479 136 -> 'context -> Core.exp -> bool
adamc@479 137
adamc@443 138 val foldMap : {kind : Core.kind' * 'state -> Core.kind' * 'state,
adamc@443 139 con : Core.con' * 'state -> Core.con' * 'state,
adamc@443 140 exp : Core.exp' * 'state -> Core.exp' * 'state}
adamc@443 141 -> 'state -> Core.exp -> Core.exp * 'state
adamc@626 142 val foldMapB : {kind : 'context * Core.kind' * 'state -> Core.kind' * 'state,
adamc@488 143 con : 'context * Core.con' * 'state -> Core.con' * 'state,
adamc@488 144 exp : 'context * Core.exp' * 'state -> Core.exp' * 'state,
adamc@488 145 bind : 'context * binder -> 'context}
adamc@488 146 -> 'context -> 'state -> Core.exp -> Core.exp * 'state
adamc@16 147 end
adamc@16 148
adamc@20 149 structure Decl : sig
adamc@20 150 datatype binder = datatype Exp.binder
adamc@20 151
adamc@626 152 val mapfoldB : {kind : ('context, Core.kind', 'state, 'abort) Search.mapfolderB,
adamc@20 153 con : ('context, Core.con', 'state, 'abort) Search.mapfolderB,
adamc@20 154 exp : ('context, Core.exp', 'state, 'abort) Search.mapfolderB,
adamc@20 155 decl : ('context, Core.decl', 'state, 'abort) Search.mapfolderB,
adamc@20 156 bind : 'context * binder -> 'context}
adamc@20 157 -> ('context, Core.decl, 'state, 'abort) Search.mapfolderB
adamc@23 158 val mapfold : {kind : (Core.kind', 'state, 'abort) Search.mapfolder,
adamc@23 159 con : (Core.con', 'state, 'abort) Search.mapfolder,
adamc@23 160 exp : (Core.exp', 'state, 'abort) Search.mapfolder,
adamc@23 161 decl : (Core.decl', 'state, 'abort) Search.mapfolder}
adamc@23 162 -> (Core.decl, 'state, 'abort) Search.mapfolder
adamc@23 163
adamc@23 164 val fold : {kind : Core.kind' * 'state -> 'state,
adamc@23 165 con : Core.con' * 'state -> 'state,
adamc@23 166 exp : Core.exp' * 'state -> 'state,
adamc@23 167 decl : Core.decl' * 'state -> 'state}
adamc@23 168 -> 'state -> Core.decl -> 'state
adamc@110 169
adamc@110 170 val foldMap : {kind : Core.kind' * 'state -> Core.kind' * 'state,
adamc@110 171 con : Core.con' * 'state -> Core.con' * 'state,
adamc@110 172 exp : Core.exp' * 'state -> Core.exp' * 'state,
adamc@110 173 decl : Core.decl' * 'state -> Core.decl' * 'state}
adamc@110 174 -> 'state -> Core.decl -> Core.decl * 'state
adamc@626 175 val foldMapB : {kind : 'context * Core.kind' * 'state -> Core.kind' * 'state,
adamc@484 176 con : 'context * Core.con' * 'state -> Core.con' * 'state,
adamc@484 177 exp : 'context * Core.exp' * 'state -> Core.exp' * 'state,
adamc@484 178 decl : 'context * Core.decl' * 'state -> Core.decl' * 'state,
adamc@484 179 bind : 'context * binder -> 'context}
adamc@484 180 -> 'context -> 'state -> Core.decl -> Core.decl * 'state
adamc@522 181
adamc@522 182 val exists : {kind : Core.kind' -> bool,
adamc@522 183 con : Core.con' -> bool,
adamc@522 184 exp : Core.exp' -> bool,
adamc@522 185 decl : Core.decl' -> bool} -> Core.decl -> bool
adamc@16 186 end
adamc@20 187
adamc@20 188 structure File : sig
adamc@179 189 val maxName : Core.file -> int
adamc@179 190
adamc@20 191 datatype binder = datatype Exp.binder
adamc@20 192
adamc@626 193 val mapfoldB : {kind : ('context, Core.kind', 'state, 'abort) Search.mapfolderB,
adamc@20 194 con : ('context, Core.con', 'state, 'abort) Search.mapfolderB,
adamc@20 195 exp : ('context, Core.exp', 'state, 'abort) Search.mapfolderB,
adamc@20 196 decl : ('context, Core.decl', 'state, 'abort) Search.mapfolderB,
adamc@20 197 bind : 'context * binder -> 'context}
adamc@20 198 -> ('context, Core.file, 'state, 'abort) Search.mapfolderB
adamc@20 199
adamc@23 200 val mapfold : {kind : (Core.kind', 'state, 'abort) Search.mapfolder,
adamc@23 201 con : (Core.con', 'state, 'abort) Search.mapfolder,
adamc@23 202 exp : (Core.exp', 'state, 'abort) Search.mapfolder,
adamc@23 203 decl : (Core.decl', 'state, 'abort) Search.mapfolder}
adamc@23 204 -> (Core.file, 'state, 'abort) Search.mapfolder
adamc@23 205
adamc@626 206 val mapB : {kind : 'context -> Core.kind' -> Core.kind',
adamc@20 207 con : 'context -> Core.con' -> Core.con',
adamc@20 208 exp : 'context -> Core.exp' -> Core.exp',
adamc@20 209 decl : 'context -> Core.decl' -> Core.decl',
adamc@20 210 bind : 'context * binder -> 'context}
adamc@20 211 -> 'context -> Core.file -> Core.file
adamc@23 212
adamc@482 213 val map : {kind : Core.kind' -> Core.kind',
adamc@482 214 con : Core.con' -> Core.con',
adamc@482 215 exp : Core.exp' -> Core.exp',
adamc@482 216 decl : Core.decl' -> Core.decl'}
adamc@482 217 -> Core.file -> Core.file
adamc@482 218
adamc@23 219 val fold : {kind : Core.kind' * 'state -> 'state,
adamc@23 220 con : Core.con' * 'state -> 'state,
adamc@23 221 exp : Core.exp' * 'state -> 'state,
adamc@23 222 decl : Core.decl' * 'state -> 'state}
adamc@23 223 -> 'state -> Core.file -> 'state
adamc@110 224
adamc@110 225 val foldMap : {kind : Core.kind' * 'state -> Core.kind' * 'state,
adamc@110 226 con : Core.con' * 'state -> Core.con' * 'state,
adamc@110 227 exp : Core.exp' * 'state -> Core.exp' * 'state,
adamc@110 228 decl : Core.decl' * 'state -> Core.decl' * 'state}
adamc@110 229 -> 'state -> Core.file -> Core.file * 'state
adamc@20 230 end
adamc@20 231
adamc@20 232 end