1(* ========================================================================= *)
2(* RANDOM FINITE MODELS                                                      *)
3(* Copyright (c) 2003 Joe Hurd, distributed under the BSD License            *)
4(* ========================================================================= *)
5
6signature Model =
7sig
8
9(* ------------------------------------------------------------------------- *)
10(* Model size.                                                               *)
11(* ------------------------------------------------------------------------- *)
12
13type size = {size : int}
14
15(* ------------------------------------------------------------------------- *)
16(* A model of size N has integer elements 0...N-1.                           *)
17(* ------------------------------------------------------------------------- *)
18
19type element = int
20
21val zeroElement : element
22
23val incrementElement : size -> element -> element option
24
25(* ------------------------------------------------------------------------- *)
26(* The parts of the model that are fixed.                                    *)
27(* ------------------------------------------------------------------------- *)
28
29type fixedFunction = size -> element list -> element option
30
31type fixedRelation = size -> element list -> bool option
32
33datatype fixed =
34    Fixed of
35      {functions : fixedFunction NameArityMap.map,
36       relations : fixedRelation NameArityMap.map}
37
38val emptyFixed : fixed
39
40val unionFixed : fixed -> fixed -> fixed
41
42val getFunctionFixed : fixed -> NameArity.nameArity -> fixedFunction
43
44val getRelationFixed : fixed -> NameArity.nameArity -> fixedRelation
45
46val insertFunctionFixed : fixed -> NameArity.nameArity * fixedFunction -> fixed
47
48val insertRelationFixed : fixed -> NameArity.nameArity * fixedRelation -> fixed
49
50val unionListFixed : fixed list -> fixed
51
52val basicFixed : fixed  (* interprets equality and hasType *)
53
54(* ------------------------------------------------------------------------- *)
55(* Renaming fixed model parts.                                               *)
56(* ------------------------------------------------------------------------- *)
57
58type fixedMap =
59     {functionMap : Name.name NameArityMap.map,
60      relationMap : Name.name NameArityMap.map}
61
62val mapFixed : fixedMap -> fixed -> fixed
63
64val ppFixedMap : fixedMap Print.pp
65
66(* ------------------------------------------------------------------------- *)
67(* Standard fixed model parts.                                               *)
68(* ------------------------------------------------------------------------- *)
69
70(* Projections *)
71
72val projectionMin : int
73
74val projectionMax : int
75
76val projectionName : int -> Name.name
77
78val projectionFixed : fixed
79
80(* Arithmetic *)
81
82val numeralMin : int
83
84val numeralMax : int
85
86val numeralName : int -> Name.name
87
88val addName : Name.name
89
90val divName : Name.name
91
92val dividesName : Name.name
93
94val evenName : Name.name
95
96val expName : Name.name
97
98val geName : Name.name
99
100val gtName : Name.name
101
102val isZeroName : Name.name
103
104val leName : Name.name
105
106val ltName : Name.name
107
108val modName : Name.name
109
110val multName : Name.name
111
112val negName : Name.name
113
114val oddName : Name.name
115
116val preName : Name.name
117
118val subName : Name.name
119
120val sucName : Name.name
121
122val modularFixed : fixed
123
124val overflowFixed : fixed
125
126(* Sets *)
127
128val cardName : Name.name
129
130val complementName : Name.name
131
132val differenceName : Name.name
133
134val emptyName : Name.name
135
136val memberName : Name.name
137
138val insertName : Name.name
139
140val intersectName : Name.name
141
142val singletonName : Name.name
143
144val subsetName : Name.name
145
146val symmetricDifferenceName : Name.name
147
148val unionName : Name.name
149
150val universeName : Name.name
151
152val setFixed : fixed
153
154(* Lists *)
155
156val appendName : Name.name
157
158val consName : Name.name
159
160val lengthName : Name.name
161
162val nilName : Name.name
163
164val nullName : Name.name
165
166val tailName : Name.name
167
168val listFixed : fixed
169
170(* ------------------------------------------------------------------------- *)
171(* Valuations.                                                               *)
172(* ------------------------------------------------------------------------- *)
173
174type valuation
175
176val emptyValuation : valuation
177
178val zeroValuation : NameSet.set -> valuation
179
180val constantValuation : element -> NameSet.set -> valuation
181
182val peekValuation : valuation -> Name.name -> element option
183
184val getValuation : valuation -> Name.name -> element
185
186val insertValuation : valuation -> Name.name * element -> valuation
187
188val randomValuation : {size : int} -> NameSet.set -> valuation
189
190val incrementValuation :
191    {size : int} -> NameSet.set -> valuation -> valuation option
192
193val foldValuation :
194    {size : int} -> NameSet.set -> (valuation * 'a -> 'a) -> 'a -> 'a
195
196(* ------------------------------------------------------------------------- *)
197(* A type of random finite models.                                           *)
198(* ------------------------------------------------------------------------- *)
199
200type parameters = {size : int, fixed : fixed}
201
202type model
203
204val default : parameters
205
206val new : parameters -> model
207
208val size : model -> int
209
210(* ------------------------------------------------------------------------- *)
211(* Interpreting terms and formulas in the model.                             *)
212(* ------------------------------------------------------------------------- *)
213
214val interpretFunction : model -> Term.functionName * element list -> element
215
216val interpretRelation : model -> Atom.relationName * element list -> bool
217
218val interpretTerm : model -> valuation -> Term.term -> element
219
220val interpretAtom : model -> valuation -> Atom.atom -> bool
221
222val interpretFormula : model -> valuation -> Formula.formula -> bool
223
224val interpretLiteral : model -> valuation -> Literal.literal -> bool
225
226val interpretClause : model -> valuation -> Thm.clause -> bool
227
228(* ------------------------------------------------------------------------- *)
229(* Check whether random groundings of a formula are true in the model.       *)
230(* Note: if it's cheaper, a systematic check will be performed instead.      *)
231(* ------------------------------------------------------------------------- *)
232
233val check :
234    (model -> valuation -> 'a -> bool) -> {maxChecks : int option} -> model ->
235    NameSet.set -> 'a -> {T : int, F : int}
236
237val checkAtom :
238    {maxChecks : int option} -> model -> Atom.atom -> {T : int, F : int}
239
240val checkFormula :
241    {maxChecks : int option} -> model -> Formula.formula -> {T : int, F : int}
242
243val checkLiteral :
244    {maxChecks : int option} -> model -> Literal.literal -> {T : int, F : int}
245
246val checkClause :
247    {maxChecks : int option} -> model -> Thm.clause -> {T : int, F : int}
248
249(* ------------------------------------------------------------------------- *)
250(* Updating the model.                                                       *)
251(* ------------------------------------------------------------------------- *)
252
253val updateFunction :
254    model -> (Term.functionName * element list) * element -> unit
255
256val updateRelation :
257    model -> (Atom.relationName * element list) * bool -> unit
258
259(* ------------------------------------------------------------------------- *)
260(* Choosing a random perturbation to make a formula true in the model.       *)
261(* ------------------------------------------------------------------------- *)
262
263val perturbTerm : model -> valuation -> Term.term * element list -> unit
264
265val perturbAtom : model -> valuation -> Atom.atom * bool -> unit
266
267val perturbLiteral : model -> valuation -> Literal.literal -> unit
268
269val perturbClause : model -> valuation -> Thm.clause -> unit
270
271(* ------------------------------------------------------------------------- *)
272(* Pretty printing.                                                          *)
273(* ------------------------------------------------------------------------- *)
274
275val pp : model Print.pp
276
277end
278