Mercurial > urweb

annotate src/expl_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 354800878b4d
children
rev   line source
adamc@38 1 (* Copyright (c) 2008, Adam Chlipala
adamc@38 2 * All rights reserved.
adamc@38 3 *
adamc@38 4 * Redistribution and use in source and binary forms, with or without
adamc@38 5 * modification, are permitted provided that the following conditions are met:
adamc@38 6 *
adamc@38 7 * - Redistributions of source code must retain the above copyright notice,
adamc@38 8 * this list of conditions and the following disclaimer.
adamc@38 9 * - Redistributions in binary form must reproduce the above copyright notice,
adamc@38 10 * this list of conditions and the following disclaimer in the documentation
adamc@38 11 * and/or other materials provided with the distribution.
adamc@38 12 * - The names of contributors may not be used to endorse or promote products
adamc@38 13 * derived from this software without specific prior written permission.
adamc@38 14 *
adamc@38 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@38 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@38 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@38 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@38 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adamc@38 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@38 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@38 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@38 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@38 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@38 25 * POSSIBILITY OF SUCH DAMAGE.
adamc@38 26 *)
adamc@38 27
adamc@38 28 signature EXPL_UTIL = sig
adamc@38 29
adamc@38 30 structure Kind : sig
adamc@624 31 val mapfoldB : {kind : ('context, Expl.kind', 'state, 'abort) Search.mapfolderB,
adamc@624 32 bind : 'context * string -> 'context}
adamc@624 33 -> ('context, Expl.kind, 'state, 'abort) Search.mapfolderB
adamc@38 34 val mapfold : (Expl.kind', 'state, 'abort) Search.mapfolder
adamc@38 35 -> (Expl.kind, 'state, 'abort) Search.mapfolder
adamc@38 36 val exists : (Expl.kind' -> bool) -> Expl.kind -> bool
adamc@624 37 val mapB : {kind : 'context -> Expl.kind' -> Expl.kind',
adamc@624 38 bind : 'context * string -> 'context}
adamc@624 39 -> 'context -> (Expl.kind -> Expl.kind)
adamc@38 40 end
adamc@38 41
adamc@38 42 structure Con : sig
adamc@38 43 datatype binder =
adamc@624 44 RelK of string
adamc@624 45 | RelC of string * Expl.kind
adamc@624 46 | NamedC of string * Expl.kind
adamc@38 47
adamc@624 48 val mapfoldB : {kind : ('context, Expl.kind', 'state, 'abort) Search.mapfolderB,
adamc@38 49 con : ('context, Expl.con', 'state, 'abort) Search.mapfolderB,
adamc@38 50 bind : 'context * binder -> 'context}
adamc@38 51 -> ('context, Expl.con, 'state, 'abort) Search.mapfolderB
adamc@38 52 val mapfold : {kind : (Expl.kind', 'state, 'abort) Search.mapfolder,
adamc@38 53 con : (Expl.con', 'state, 'abort) Search.mapfolder}
adamc@38 54 -> (Expl.con, 'state, 'abort) Search.mapfolder
adamc@38 55
adamc@624 56 val mapB : {kind : 'context -> Expl.kind' -> Expl.kind',
adamc@38 57 con : 'context -> Expl.con' -> Expl.con',
adamc@38 58 bind : 'context * binder -> 'context}
adamc@38 59 -> 'context -> (Expl.con -> Expl.con)
adamc@38 60 val map : {kind : Expl.kind' -> Expl.kind',
adamc@38 61 con : Expl.con' -> Expl.con'}
adamc@38 62 -> Expl.con -> Expl.con
adamc@38 63 val exists : {kind : Expl.kind' -> bool,
adamc@38 64 con : Expl.con' -> bool} -> Expl.con -> bool
adamc@38 65 end
adamc@38 66
adamc@38 67 structure Exp : sig
adamc@38 68 datatype binder =
adamc@624 69 RelK of string
adamc@624 70 | RelC of string * Expl.kind
adamc@38 71 | NamedC of string * Expl.kind
adamc@38 72 | RelE of string * Expl.con
adamc@38 73 | NamedE of string * Expl.con
adamc@38 74
adamc@624 75 val mapfoldB : {kind : ('context, Expl.kind', 'state, 'abort) Search.mapfolderB,
adamc@38 76 con : ('context, Expl.con', 'state, 'abort) Search.mapfolderB,
adamc@38 77 exp : ('context, Expl.exp', 'state, 'abort) Search.mapfolderB,
adamc@38 78 bind : 'context * binder -> 'context}
adamc@38 79 -> ('context, Expl.exp, 'state, 'abort) Search.mapfolderB
adamc@38 80 val mapfold : {kind : (Expl.kind', 'state, 'abort) Search.mapfolder,
adamc@38 81 con : (Expl.con', 'state, 'abort) Search.mapfolder,
adamc@38 82 exp : (Expl.exp', 'state, 'abort) Search.mapfolder}
adamc@38 83 -> (Expl.exp, 'state, 'abort) Search.mapfolder
adamc@38 84 val exists : {kind : Expl.kind' -> bool,
adamc@38 85 con : Expl.con' -> bool,
adamc@38 86 exp : Expl.exp' -> bool} -> Expl.exp -> bool
adamc@38 87 end
adamc@38 88
adamc@38 89 structure Sgn : sig
adamc@38 90 datatype binder =
adamc@624 91 RelK of string
adamc@624 92 | RelC of string * Expl.kind
adamc@38 93 | NamedC of string * Expl.kind
adamc@64 94 | Sgn of string * Expl.sgn
adamc@38 95 | Str of string * Expl.sgn
adamc@38 96
adamc@624 97 val mapfoldB : {kind : ('context, Expl.kind', 'state, 'abort) Search.mapfolderB,
adamc@38 98 con : ('context, Expl.con', 'state, 'abort) Search.mapfolderB,
adamc@38 99 sgn_item : ('context, Expl.sgn_item', 'state, 'abort) Search.mapfolderB,
adamc@38 100 sgn : ('context, Expl.sgn', 'state, 'abort) Search.mapfolderB,
adamc@38 101 bind : 'context * binder -> 'context}
adamc@38 102 -> ('context, Expl.sgn, 'state, 'abort) Search.mapfolderB
adamc@38 103
adamc@38 104
adamc@38 105 val mapfold : {kind : (Expl.kind', 'state, 'abort) Search.mapfolder,
adamc@38 106 con : (Expl.con', 'state, 'abort) Search.mapfolder,
adamc@38 107 sgn_item : (Expl.sgn_item', 'state, 'abort) Search.mapfolder,
adamc@38 108 sgn : (Expl.sgn', 'state, 'abort) Search.mapfolder}
adamc@38 109 -> (Expl.sgn, 'state, 'abort) Search.mapfolder
adamc@38 110
adamc@38 111 val map : {kind : Expl.kind' -> Expl.kind',
adamc@38 112 con : Expl.con' -> Expl.con',
adamc@38 113 sgn_item : Expl.sgn_item' -> Expl.sgn_item',
adamc@38 114 sgn : Expl.sgn' -> Expl.sgn'}
adamc@38 115 -> Expl.sgn -> Expl.sgn
adamc@38 116
adamc@38 117 end
adamc@38 118
adamc@38 119 end