Mercurial > urweb

comparison src/expl_util.sig @ 38:d16ef24de78b

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