Mercurial > urweb

annotate src/elab_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 c7b9a33c26c8
children 9e0fa4f6ac93
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
adamc@76 160 | Str of string * Elab.sgn
adamc@76 161 | Sgn of string * 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
adamc@448 206 end
adamc@448 207
adamc@448 208 structure File : sig
adamc@448 209 val maxName : Elab.file -> int
adamc@34 210 end
adamc@76 211
adamc@76 212 end