Mercurial > urweb

annotate src/elab_util.sig @ 1698:aaae710417df

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