Mercurial > urweb

annotate src/core_util.sig @ 1732:4a03aa3251cb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Initial support for reusing elaboration results
author Adam Chlipala <adam@chlipala.net>
date Sun, 29 Apr 2012 13:17:31 -0400
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