Mercurial > urweb

annotate src/elab_util.sig @ 1856:3683d1a8c1c8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add Sigcheck phase to avoid issues with signatures in global initializers
author Adam Chlipala <adam@chlipala.net>
date Sat, 15 Jun 2013 08:18:47 -0400
parents d28adceef22a
children 1091227f535a
rev   line source
adam@1732 1 (* Copyright (c) 2008-2010, 2012, 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
adam@1795 115 val existsB : {kind : 'context * Elab.kind' -> bool,
adam@1795 116 con : 'context * Elab.con' -> bool,
adam@1795 117 exp : 'context * Elab.exp' -> bool,
adam@1795 118 bind : 'context * binder -> 'context}
adam@1795 119 -> 'context -> Elab.exp -> bool
adamc@448 120
adamc@623 121 val foldB : {kind : 'context * Elab.kind' * 'state -> 'state,
adamc@448 122 con : 'context * Elab.con' * 'state -> 'state,
adamc@448 123 exp : 'context * Elab.exp' * 'state -> 'state,
adamc@448 124 bind : 'context * binder -> 'context}
adamc@448 125 -> 'context -> 'state -> Elab.exp -> 'state
adamc@10 126 end
adamc@10 127
adamc@34 128 structure Sgn : sig
adamc@34 129 datatype binder =
adamc@623 130 RelK of string
adamc@623 131 | RelC of string * Elab.kind
adamc@792 132 | NamedC of string * int * Elab.kind * Elab.con option
adamc@792 133 | Str of string * int * Elab.sgn
adamc@792 134 | Sgn of string * int * Elab.sgn
adamc@34 135
adamc@623 136 val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB,
adamc@34 137 con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB,
adamc@34 138 sgn_item : ('context, Elab.sgn_item', 'state, 'abort) Search.mapfolderB,
adamc@34 139 sgn : ('context, Elab.sgn', 'state, 'abort) Search.mapfolderB,
adamc@34 140 bind : 'context * binder -> 'context}
adamc@34 141 -> ('context, Elab.sgn, 'state, 'abort) Search.mapfolderB
adamc@34 142
adamc@34 143
adamc@34 144 val mapfold : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder,
adamc@34 145 con : (Elab.con', 'state, 'abort) Search.mapfolder,
adamc@34 146 sgn_item : (Elab.sgn_item', 'state, 'abort) Search.mapfolder,
adamc@34 147 sgn : (Elab.sgn', 'state, 'abort) Search.mapfolder}
adamc@34 148 -> (Elab.sgn, 'state, 'abort) Search.mapfolder
adamc@34 149
adamc@34 150 val map : {kind : Elab.kind' -> Elab.kind',
adamc@34 151 con : Elab.con' -> Elab.con',
adamc@34 152 sgn_item : Elab.sgn_item' -> Elab.sgn_item',
adamc@34 153 sgn : Elab.sgn' -> Elab.sgn'}
adamc@34 154 -> Elab.sgn -> Elab.sgn
adamc@34 155
adamc@792 156 val mapB : {kind : 'context -> Elab.kind' -> Elab.kind',
adamc@792 157 con : 'context -> Elab.con' -> Elab.con',
adamc@792 158 sgn_item : 'context -> Elab.sgn_item' -> Elab.sgn_item',
adamc@792 159 sgn : 'context -> Elab.sgn' -> Elab.sgn',
adamc@792 160 bind : 'context * binder -> 'context}
adamc@792 161 -> 'context -> Elab.sgn -> Elab.sgn
adamc@792 162
adamc@2 163 end
adamc@34 164
adamc@76 165 structure Decl : sig
adamc@76 166 datatype binder =
adamc@623 167 RelK of string
adamc@623 168 | RelC of string * Elab.kind
adamc@792 169 | NamedC of string * int * Elab.kind * Elab.con option
adamc@76 170 | RelE of string * Elab.con
adamc@76 171 | NamedE of string * Elab.con
adam@1345 172 | Str of string * int * Elab.sgn
adam@1345 173 | Sgn of string * int * Elab.sgn
adamc@76 174
adamc@623 175 val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB,
adamc@76 176 con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB,
adamc@76 177 exp : ('context, Elab.exp', 'state, 'abort) Search.mapfolderB,
adamc@76 178 sgn_item : ('context, Elab.sgn_item', 'state, 'abort) Search.mapfolderB,
adamc@76 179 sgn : ('context, Elab.sgn', 'state, 'abort) Search.mapfolderB,
adamc@76 180 str : ('context, Elab.str', 'state, 'abort) Search.mapfolderB,
adamc@76 181 decl : ('context, Elab.decl', 'state, 'abort) Search.mapfolderB,
adamc@76 182 bind : 'context * binder -> 'context}
adamc@76 183 -> ('context, Elab.decl, 'state, 'abort) Search.mapfolderB
adamc@76 184 val mapfold : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder,
adamc@76 185 con : (Elab.con', 'state, 'abort) Search.mapfolder,
adamc@76 186 exp : (Elab.exp', 'state, 'abort) Search.mapfolder,
adamc@76 187 sgn_item : (Elab.sgn_item', 'state, 'abort) Search.mapfolder,
adamc@76 188 sgn : (Elab.sgn', 'state, 'abort) Search.mapfolder,
adamc@76 189 str : (Elab.str', 'state, 'abort) Search.mapfolder,
adamc@76 190 decl : (Elab.decl', 'state, 'abort) Search.mapfolder}
adamc@76 191 -> (Elab.decl, 'state, 'abort) Search.mapfolder
adamc@76 192 val exists : {kind : Elab.kind' -> bool,
adamc@76 193 con : Elab.con' -> bool,
adamc@76 194 exp : Elab.exp' -> bool,
adamc@76 195 sgn_item : Elab.sgn_item' -> bool,
adamc@76 196 sgn : Elab.sgn' -> bool,
adamc@76 197 str : Elab.str' -> bool,
adamc@76 198 decl : Elab.decl' -> bool}
adamc@76 199 -> Elab.decl -> bool
adamc@76 200 val search : {kind : Elab.kind' -> 'a option,
adamc@76 201 con : Elab.con' -> 'a option,
adamc@76 202 exp : Elab.exp' -> 'a option,
adamc@76 203 sgn_item : Elab.sgn_item' -> 'a option,
adamc@76 204 sgn : Elab.sgn' -> 'a option,
adamc@76 205 str : Elab.str' -> 'a option,
adamc@76 206 decl : Elab.decl' -> 'a option}
adamc@76 207 -> Elab.decl -> 'a option
adamc@448 208
adamc@623 209 val foldMapB : {kind : 'context * Elab.kind' * 'state -> Elab.kind' * 'state,
adamc@448 210 con : 'context * Elab.con' * 'state -> Elab.con' * 'state,
adamc@448 211 exp : 'context * Elab.exp' * 'state -> Elab.exp' * 'state,
adamc@448 212 sgn_item : 'context * Elab.sgn_item' * 'state -> Elab.sgn_item' * 'state,
adamc@448 213 sgn : 'context * Elab.sgn' * 'state -> Elab.sgn' * 'state,
adamc@448 214 str : 'context * Elab.str' * 'state -> Elab.str' * 'state,
adamc@448 215 decl : 'context * Elab.decl' * 'state -> Elab.decl' * 'state,
adamc@448 216 bind : 'context * binder -> 'context}
adamc@448 217 -> 'context -> 'state -> Elab.decl -> Elab.decl * 'state
adam@1345 218
adam@1345 219 val map : {kind : Elab.kind' -> Elab.kind',
adam@1345 220 con : Elab.con' -> Elab.con',
adam@1345 221 exp : Elab.exp' -> Elab.exp',
adam@1345 222 sgn_item : Elab.sgn_item' -> Elab.sgn_item',
adam@1345 223 sgn : Elab.sgn' -> Elab.sgn',
adam@1345 224 str : Elab.str' -> Elab.str',
adam@1345 225 decl : Elab.decl' -> Elab.decl'}
adam@1345 226 -> Elab.decl -> Elab.decl
adam@1345 227
adam@1345 228 val mapB : {kind : 'context -> Elab.kind' -> Elab.kind',
adam@1345 229 con : 'context -> Elab.con' -> Elab.con',
adam@1345 230 exp : 'context -> Elab.exp' -> Elab.exp',
adam@1345 231 sgn_item : 'context -> Elab.sgn_item' -> Elab.sgn_item',
adam@1345 232 sgn : 'context -> Elab.sgn' -> Elab.sgn',
adam@1345 233 str : 'context -> Elab.str' -> Elab.str',
adam@1345 234 decl : 'context -> Elab.decl' -> Elab.decl',
adam@1345 235 bind : 'context * binder -> 'context}
adam@1345 236 -> 'context -> Elab.decl -> Elab.decl
adam@1732 237
adam@1732 238 val fold : {kind : Elab.kind' * 'state -> 'state,
adam@1732 239 con : Elab.con' * 'state -> 'state,
adam@1732 240 exp : Elab.exp' * 'state -> 'state,
adam@1732 241 sgn_item : Elab.sgn_item' * 'state -> 'state,
adam@1732 242 sgn : Elab.sgn' * 'state -> 'state,
adam@1732 243 str : Elab.str' * 'state -> 'state,
adam@1732 244 decl : Elab.decl' * 'state -> 'state}
adam@1732 245 -> 'state -> Elab.decl -> 'state
adamc@448 246 end
adamc@448 247
adamc@448 248 structure File : sig
adamc@448 249 val maxName : Elab.file -> int
adam@1584 250
adam@1584 251 val findDecl : (Elab.decl -> bool) -> Elab.file -> Elab.decl option
adamc@34 252 end
adamc@76 253
adamc@76 254 end