Mercurial > urweb

annotate src/elab_util.sig @ 1591:20f898c29525

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Tweaks to choices of source positions to use in error messages, including for subSgn
author Adam Chlipala <adam@chlipala.net>
date Sat, 05 Nov 2011 13:12:07 -0400
parents c37d8341940a
children 6c00d8af6239
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
adamc@711 67 val existsB : {kind : 'context * Elab.kind' -> bool,
adamc@711 68 con : 'context * Elab.con' -> bool,
adamc@711 69 bind : 'context * binder -> 'context}
adamc@711 70 -> 'context -> Elab.con -> bool
adamc@6 71 val exists : {kind : Elab.kind' -> bool,
adamc@6 72 con : Elab.con' -> bool} -> Elab.con -> bool
adamc@448 73
adamc@623 74 val foldB : {kind : 'context * Elab.kind' * 'state -> 'state,
adamc@448 75 con : 'context * Elab.con' * 'state -> 'state,
adamc@448 76 bind : 'context * binder -> 'context}
adamc@448 77 -> 'context -> 'state -> Elab.con -> 'state
adamc@839 78 val fold : {kind : Elab.kind' * 'state -> 'state,
adamc@839 79 con : Elab.con' * 'state -> 'state}
adamc@839 80 -> 'state -> Elab.con -> 'state
adamc@6 81 end
adamc@6 82
adamc@10 83 structure Exp : sig
adamc@11 84 datatype binder =
adamc@623 85 RelK of string
adamc@623 86 | RelC of string * Elab.kind
adamc@792 87 | NamedC of string * int * Elab.kind * Elab.con option
adamc@11 88 | RelE of string * Elab.con
adamc@11 89 | NamedE of string * Elab.con
adamc@11 90
adamc@623 91 val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB,
adamc@11 92 con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB,
adamc@11 93 exp : ('context, Elab.exp', 'state, 'abort) Search.mapfolderB,
adamc@11 94 bind : 'context * binder -> 'context}
adamc@11 95 -> ('context, Elab.exp, 'state, 'abort) Search.mapfolderB
adamc@10 96 val mapfold : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder,
adamc@10 97 con : (Elab.con', 'state, 'abort) Search.mapfolder,
adamc@10 98 exp : (Elab.exp', 'state, 'abort) Search.mapfolder}
adamc@10 99 -> (Elab.exp, 'state, 'abort) Search.mapfolder
adamc@623 100 val mapB : {kind : 'context -> Elab.kind' -> Elab.kind',
adamc@211 101 con : 'context -> Elab.con' -> Elab.con',
adamc@211 102 exp : 'context -> Elab.exp' -> Elab.exp',
adamc@211 103 bind : 'context * binder -> 'context}
adamc@211 104 -> 'context -> (Elab.exp -> Elab.exp)
adamc@10 105 val exists : {kind : Elab.kind' -> bool,
adamc@10 106 con : Elab.con' -> bool,
adamc@10 107 exp : Elab.exp' -> bool} -> Elab.exp -> bool
adamc@448 108
adamc@623 109 val foldB : {kind : 'context * Elab.kind' * 'state -> 'state,
adamc@448 110 con : 'context * Elab.con' * 'state -> 'state,
adamc@448 111 exp : 'context * Elab.exp' * 'state -> 'state,
adamc@448 112 bind : 'context * binder -> 'context}
adamc@448 113 -> 'context -> 'state -> Elab.exp -> 'state
adamc@10 114 end
adamc@10 115
adamc@34 116 structure Sgn : sig
adamc@34 117 datatype binder =
adamc@623 118 RelK of string
adamc@623 119 | RelC of string * Elab.kind
adamc@792 120 | NamedC of string * int * Elab.kind * Elab.con option
adamc@792 121 | Str of string * int * Elab.sgn
adamc@792 122 | Sgn of string * int * Elab.sgn
adamc@34 123
adamc@623 124 val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB,
adamc@34 125 con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB,
adamc@34 126 sgn_item : ('context, Elab.sgn_item', 'state, 'abort) Search.mapfolderB,
adamc@34 127 sgn : ('context, Elab.sgn', 'state, 'abort) Search.mapfolderB,
adamc@34 128 bind : 'context * binder -> 'context}
adamc@34 129 -> ('context, Elab.sgn, 'state, 'abort) Search.mapfolderB
adamc@34 130
adamc@34 131
adamc@34 132 val mapfold : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder,
adamc@34 133 con : (Elab.con', 'state, 'abort) Search.mapfolder,
adamc@34 134 sgn_item : (Elab.sgn_item', 'state, 'abort) Search.mapfolder,
adamc@34 135 sgn : (Elab.sgn', 'state, 'abort) Search.mapfolder}
adamc@34 136 -> (Elab.sgn, 'state, 'abort) Search.mapfolder
adamc@34 137
adamc@34 138 val map : {kind : Elab.kind' -> Elab.kind',
adamc@34 139 con : Elab.con' -> Elab.con',
adamc@34 140 sgn_item : Elab.sgn_item' -> Elab.sgn_item',
adamc@34 141 sgn : Elab.sgn' -> Elab.sgn'}
adamc@34 142 -> Elab.sgn -> Elab.sgn
adamc@34 143
adamc@792 144 val mapB : {kind : 'context -> Elab.kind' -> Elab.kind',
adamc@792 145 con : 'context -> Elab.con' -> Elab.con',
adamc@792 146 sgn_item : 'context -> Elab.sgn_item' -> Elab.sgn_item',
adamc@792 147 sgn : 'context -> Elab.sgn' -> Elab.sgn',
adamc@792 148 bind : 'context * binder -> 'context}
adamc@792 149 -> 'context -> Elab.sgn -> Elab.sgn
adamc@792 150
adamc@2 151 end
adamc@34 152
adamc@76 153 structure Decl : sig
adamc@76 154 datatype binder =
adamc@623 155 RelK of string
adamc@623 156 | RelC of string * Elab.kind
adamc@792 157 | NamedC of string * int * Elab.kind * Elab.con option
adamc@76 158 | RelE of string * Elab.con
adamc@76 159 | NamedE of string * Elab.con
adam@1345 160 | Str of string * int * Elab.sgn
adam@1345 161 | Sgn of string * int * Elab.sgn
adamc@76 162
adamc@623 163 val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB,
adamc@76 164 con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB,
adamc@76 165 exp : ('context, Elab.exp', 'state, 'abort) Search.mapfolderB,
adamc@76 166 sgn_item : ('context, Elab.sgn_item', 'state, 'abort) Search.mapfolderB,
adamc@76 167 sgn : ('context, Elab.sgn', 'state, 'abort) Search.mapfolderB,
adamc@76 168 str : ('context, Elab.str', 'state, 'abort) Search.mapfolderB,
adamc@76 169 decl : ('context, Elab.decl', 'state, 'abort) Search.mapfolderB,
adamc@76 170 bind : 'context * binder -> 'context}
adamc@76 171 -> ('context, Elab.decl, 'state, 'abort) Search.mapfolderB
adamc@76 172 val mapfold : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder,
adamc@76 173 con : (Elab.con', 'state, 'abort) Search.mapfolder,
adamc@76 174 exp : (Elab.exp', 'state, 'abort) Search.mapfolder,
adamc@76 175 sgn_item : (Elab.sgn_item', 'state, 'abort) Search.mapfolder,
adamc@76 176 sgn : (Elab.sgn', 'state, 'abort) Search.mapfolder,
adamc@76 177 str : (Elab.str', 'state, 'abort) Search.mapfolder,
adamc@76 178 decl : (Elab.decl', 'state, 'abort) Search.mapfolder}
adamc@76 179 -> (Elab.decl, 'state, 'abort) Search.mapfolder
adamc@76 180 val exists : {kind : Elab.kind' -> bool,
adamc@76 181 con : Elab.con' -> bool,
adamc@76 182 exp : Elab.exp' -> bool,
adamc@76 183 sgn_item : Elab.sgn_item' -> bool,
adamc@76 184 sgn : Elab.sgn' -> bool,
adamc@76 185 str : Elab.str' -> bool,
adamc@76 186 decl : Elab.decl' -> bool}
adamc@76 187 -> Elab.decl -> bool
adamc@76 188 val search : {kind : Elab.kind' -> 'a option,
adamc@76 189 con : Elab.con' -> 'a option,
adamc@76 190 exp : Elab.exp' -> 'a option,
adamc@76 191 sgn_item : Elab.sgn_item' -> 'a option,
adamc@76 192 sgn : Elab.sgn' -> 'a option,
adamc@76 193 str : Elab.str' -> 'a option,
adamc@76 194 decl : Elab.decl' -> 'a option}
adamc@76 195 -> Elab.decl -> 'a option
adamc@448 196
adamc@623 197 val foldMapB : {kind : 'context * Elab.kind' * 'state -> Elab.kind' * 'state,
adamc@448 198 con : 'context * Elab.con' * 'state -> Elab.con' * 'state,
adamc@448 199 exp : 'context * Elab.exp' * 'state -> Elab.exp' * 'state,
adamc@448 200 sgn_item : 'context * Elab.sgn_item' * 'state -> Elab.sgn_item' * 'state,
adamc@448 201 sgn : 'context * Elab.sgn' * 'state -> Elab.sgn' * 'state,
adamc@448 202 str : 'context * Elab.str' * 'state -> Elab.str' * 'state,
adamc@448 203 decl : 'context * Elab.decl' * 'state -> Elab.decl' * 'state,
adamc@448 204 bind : 'context * binder -> 'context}
adamc@448 205 -> 'context -> 'state -> Elab.decl -> Elab.decl * 'state
adam@1345 206
adam@1345 207 val map : {kind : Elab.kind' -> Elab.kind',
adam@1345 208 con : Elab.con' -> Elab.con',
adam@1345 209 exp : Elab.exp' -> Elab.exp',
adam@1345 210 sgn_item : Elab.sgn_item' -> Elab.sgn_item',
adam@1345 211 sgn : Elab.sgn' -> Elab.sgn',
adam@1345 212 str : Elab.str' -> Elab.str',
adam@1345 213 decl : Elab.decl' -> Elab.decl'}
adam@1345 214 -> Elab.decl -> Elab.decl
adam@1345 215
adam@1345 216 val mapB : {kind : 'context -> Elab.kind' -> Elab.kind',
adam@1345 217 con : 'context -> Elab.con' -> Elab.con',
adam@1345 218 exp : 'context -> Elab.exp' -> Elab.exp',
adam@1345 219 sgn_item : 'context -> Elab.sgn_item' -> Elab.sgn_item',
adam@1345 220 sgn : 'context -> Elab.sgn' -> Elab.sgn',
adam@1345 221 str : 'context -> Elab.str' -> Elab.str',
adam@1345 222 decl : 'context -> Elab.decl' -> Elab.decl',
adam@1345 223 bind : 'context * binder -> 'context}
adam@1345 224 -> 'context -> Elab.decl -> Elab.decl
adamc@448 225 end
adamc@448 226
adamc@448 227 structure File : sig
adamc@448 228 val maxName : Elab.file -> int
adam@1584 229
adam@1584 230 val findDecl : (Elab.decl -> bool) -> Elab.file -> Elab.decl option
adamc@34 231 end
adamc@76 232
adamc@76 233 end