Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / CoAlgFormula.ml @ de84f40d

History | View | Annotate | Download (66.9 KB)

1
(** This module implements coalgebraic formulae
2
    (e.g. parsing, printing, (de-)constructing, ...).
3
    @author Florian Widmann
4
 *)
5

    
6

    
7
module HC = HashConsing
8
module A = AltGenlex
9
module L = List
10
module Str = String
11

    
12

    
13
(** A general exception for all kinds of errors
14
    that can happen in the tableau procedure.
15
    More specific information is given in the argument.
16
 *)
17
exception CoAlgException of string
18

    
19
(** Indicates the sort of a sorted formula
20
 *)
21
type sort = int
22

    
23
type rational = { nominator: int; denominator: int }
24

    
25
let string_of_rational r =
26
    (string_of_int r.nominator)^"/"^(string_of_int r.denominator)
27

    
28
let rational_of_int n d = { nominator = n; denominator = d }
29

    
30
(** Defines (unsorted) coalgebraic formulae.
31
 *)
32
type formula =
33
  | TRUE
34
  | FALSE
35
  | AP of string (* atomic proposition *)
36
  | NOT of formula
37
  | AT of string * formula
38
  | OR of formula * formula
39
  | AND of formula * formula
40
  | EQU of formula * formula
41
  | IMP of formula * formula
42
  | EX of string * formula
43
  | AX of string * formula
44
  | ENFORCES of int list * formula
45
  | ALLOWS   of int list * formula
46
  | MIN of int * string * formula
47
  | MAX of int * string * formula
48
  | MORETHAN of int * string * formula (* diamond of GML *)
49
  | MAXEXCEPT of int * string * formula (* box of GML *)
50
  | ATLEASTPROB of rational * formula (* = {>= 0.5} C  ---> C occurs with *)
51
                                      (*  probability of at least 50% *)
52
  | LESSPROBFAIL of rational * formula (* = [1/2] C = {< 1/2} ¬ C ---> C fails with *)
53
                                        (* probability of less than 50% *)
54
  | CONST of string  (* constant functor with value string *)
55
  | CONSTN of string  (* constant functor with value other than string *)
56
  | ID of formula (* modality of the identity functor *)
57
  | NORM of formula * formula (* default implication *)
58
  | NORMN of formula * formula (* \neg NORM (\neg A, \neg B) *)
59
  | CHC of formula * formula (* Choice is self-dual *)
60
  | FUS of bool * formula
61
  | MU of string * formula
62
  | NU of string * formula
63
  | VAR of string
64
  | AF of formula
65
  | EF of formula
66
  | AG of formula
67
  | EG of formula
68
  | AU of formula * formula
69
  | EU of formula * formula
70

    
71
exception ConversionException of formula
72

    
73

    
74
(** Defines sorted coalgebraic formulae.
75
 *)
76
type sortedFormula = sort * formula
77

    
78

    
79
(** Determines whether a name indicates a nominal.
80
    @param A string s.
81
    @return True iff s contains a prime character.
82
 *)
83
let isNominal s = String.contains s '\''
84

    
85

    
86
(** Determines the size of a formula.
87
    @param f A formula.
88
    @return The size of f.
89
 *)
90
let rec sizeFormula f =
91
  match f with
92
  | TRUE
93
  | FALSE
94
  | AP _ -> 1
95
  | NOT f1
96
  | AT (_, f1) -> succ (sizeFormula f1)
97
  | OR (f1, f2)
98
  | AND (f1, f2)
99
  | EQU (f1, f2)
100
  | IMP (f1, f2) -> succ (sizeFormula f1 + sizeFormula f2)
101
  | EX (_, f1)
102
  | AX (_, f1)
103
  | ENFORCES (_, f1)
104
  | ALLOWS (_, f1) -> succ (sizeFormula f1)
105
  | MIN (_, _, f1)
106
  | MAX (_, _, f1)
107
  | ATLEASTPROB (_, f1)
108
  | LESSPROBFAIL (_, f1)
109
  | MORETHAN (_, _, f1)
110
  | MAXEXCEPT (_, _, f1) -> succ (sizeFormula f1)
111
  | ID (f1) -> succ (sizeFormula f1)
112
  | NORM(f1, f2)
113
  | NORMN(f1, f2) -> succ (sizeFormula f1 + sizeFormula f2)
114
  | CONST _
115
  | CONSTN _ -> 1
116
  | CHC (f1, f2) -> succ (sizeFormula f1 + sizeFormula f2)
117
  | FUS (_, f1) -> succ (sizeFormula f1)
118
  | MU (_, f1)
119
  | NU (_, f1) -> succ (succ (sizeFormula f1))
120
  | VAR _ -> 1
121
  | AF _ | EF _
122
  | AG _ | EG _
123
  | AU _ | EU _ ->
124
            raise (CoAlgException ("sizeFormula: CTL should have been removed at this point"))
125

    
126
(** Determines the size of a sorted formula.
127
    @param f A sorted formula.
128
    @return The size of f.
129
 *)
130
let sizeSortedFormula f = sizeFormula (snd f)
131

    
132

    
133
(* think of func: (formula -> unit) -> formula -> unit as identity.
134
  iterate over all subformulae and collect side effects. *)
135
let rec iter func formula =
136
    func formula;
137
    let proc = iter func in (* proc = "process" *)
138
    match formula with
139
    | TRUE | FALSE | AP _ | VAR _ -> ()
140
    | CONST _
141
    | CONSTN _ -> ()
142
    | NOT a | AT (_,a)
143
    | EX (_,a) | AX (_,a) -> proc a
144
    | OR (a,b) | AND (a,b)
145
    | EQU (a,b) | IMP (a,b) -> (proc a ; proc b)
146
    | ENFORCES (_,a) | ALLOWS   (_,a)
147
    | MIN (_,_,a)    | MAX (_,_,a)
148
    | ATLEASTPROB (_, a) | LESSPROBFAIL (_, a)
149
    | MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> proc a
150
    | ID(a) -> proc a
151
    | NORM(a, b) | NORMN(a, b) -> (proc a; proc b)
152
    | CHC (a,b)  -> (proc a ; proc b)
153
    | FUS (_,a) -> proc a
154
    | MU (_, f) | NU (_, f) -> proc f
155
    | AF f | EF f | AG f | EG f -> proc f
156
    | AU (f1, f2) | EU (f1, f2) -> (proc f1; proc f2)
157

    
158
let rec convert_post func formula = (* run over all subformulas in post order *)
159
  let c = convert_post func in (* some shorthand *)
160
  (* replace parts of the formula *)
161
  let formula = (match formula with
162
  (* 0-ary constructors *)
163
  | TRUE | FALSE | AP _ | VAR _ -> formula
164
  | CONST _
165
  | CONSTN _ -> formula
166
  (* unary *)
167
  | NOT a -> NOT (c a)
168
  | AT (s,a) -> AT (s,c a)
169
  (* binary *)
170
  | OR (a,b) -> OR (c a, c b)
171
  | AND (a,b) -> AND (c a, c b)
172
  | EQU (a,b) -> EQU (c a, c b)
173
  | IMP (a,b) -> IMP (c a, c b)
174
  | EX (s,a) -> EX (s,c a)
175
  | AX (s,a) -> AX (s,c a)
176
  | ENFORCES (s,a) -> ENFORCES (s,c a)
177
  | ALLOWS   (s,a) -> ALLOWS   (s,c a)
178
  | MIN (n,s,a) -> MIN (n,s,c a)
179
  | MAX (n,s,a) -> MAX (n,s,c a)
180
  | ATLEASTPROB (p,a) -> ATLEASTPROB (p, c a)
181
  | LESSPROBFAIL (p,a) -> LESSPROBFAIL (p, c a)
182
  | MORETHAN (n,s,a) -> MORETHAN (n,s,c a)
183
  | MAXEXCEPT (n,s,a) -> MAXEXCEPT (n,s,c a)
184
  | ID(a) -> ID (c a)
185
  | NORM(a, b) -> NORM(c a, c b)
186
  | NORMN(a, b) -> NORMN(c a, c b)
187
  | CHC (a,b) -> CHC (c a, c b)
188
  | FUS (s,a) -> FUS (s, c a)
189
  | MU (n, f1) -> MU (n, c f1)
190
  | NU (n, f1) -> NU (n, c f1)
191
  | AF f1 -> AF (c f1)
192
  | EF f1 -> EF (c f1)
193
  | AG f1 -> AG (c f1)
194
  | EG f1 -> EG (c f1)
195
  | AU (f1, f2) -> AU (c f1, c f2)
196
  | EU (f1, f2) -> AU (c f1, c f2))in
197
  func formula
198

    
199
let convertToK formula = (* tries to convert a formula to a pure K formula *)
200
  let helper formula = match formula with
201
  | ENFORCES _ | ALLOWS _ -> raise (ConversionException formula)
202
  | MORETHAN (0,s,a) | MIN (1,s,a) -> EX (s,a)
203
  | MAX (0,s,a) -> AX (s, NOT a)
204
  | MAXEXCEPT (0,s,a) -> AX (s, a)
205
  | TRUE | FALSE
206
  | EQU _ | IMP _
207
  | AND _ | OR _
208
  | AP _ | NOT _
209
  | AX _ | EX _
210
  | CHC _ | FUS _ -> formula
211
  | _ -> raise (ConversionException formula)
212
  in
213
  convert_post helper formula
214

    
215
let convertToGML formula = (* tries to convert a formula to a pure GML formula *)
216
  let helper formula = match formula with
217
  | ENFORCES _ | ALLOWS _ -> raise (ConversionException formula)
218
  | MORETHAN _ | MIN _ | MAX _ | MAXEXCEPT _ -> formula
219
  | TRUE | FALSE
220
  | EQU _ | IMP _
221
  | AND _ | OR _
222
  | AP _ | NOT _
223
  | CHC _ | FUS _ -> formula
224
  | AX (r,a) -> MAXEXCEPT (0,r,a)
225
  | EX (r,a) -> MORETHAN  (0,r,a)
226
  | _ -> raise (ConversionException formula)
227
  in
228
  convert_post helper formula
229

    
230
let gensym = Stream.from (fun i -> Some (Printf.sprintf "#gensym%x#" i))
231

    
232
let convertToMu formula =
233
  let helper formula =
234
    match formula with
235
    | AF f1 ->
236
       MU ("#AF#", (OR (f1, (AX ("", (VAR "#AF#"))))))
237
    | EF f1 ->
238
       MU ("#EF#", (OR (f1, (EX ("", (VAR "#EF#"))))))
239
    | AG f1 ->
240
       NU ("#AG#", (AND (f1, (AX ("", (VAR "#AG#"))))))
241
    | EG f1 ->
242
       NU ("#EG#", (AND (f1, (EX ("", (VAR "#EG#"))))))
243
    | AU (f1, f2) ->
244
       MU ("#AU#", (OR (f2, (AND (f1, (AX ("", (VAR "#AU#"))))))))
245
    | EU (f1, f2) ->
246
       MU ("#EU#", (OR (f2, (AND (f1, (EX ("", (VAR "#EU#"))))))))
247
    | _ -> formula
248
  in
249
  convert_post helper formula
250

    
251
(** Appends a string representation of a formula to a string buffer.
252
    Parentheses are ommited where possible
253
    where the preference rules are defined as usual.
254
    @param sb A string buffer.
255
    @param f A formula.
256
 *)
257
let rec exportFormula_buffer sb f =
258
  let negate = function
259
    | NOT f -> f
260
    | f -> NOT f
261
  in
262
  let prio n lf =
263
    let prionr = function
264
      | EQU _ -> 0
265
      | IMP _  -> 1
266
      | OR _ -> 2
267
      | AND _ -> 3
268
      | _ -> 4
269
    in
270
    if prionr lf < n then begin
271
      Buffer.add_char sb '(';
272
      exportFormula_buffer sb lf;
273
      Buffer.add_char sb ')'
274
    end
275
    else exportFormula_buffer sb lf
276
  in
277
  match f with
278
  | TRUE -> Buffer.add_string sb "True"
279
  | FALSE -> Buffer.add_string sb "False"
280
  | AP s -> Buffer.add_string sb s
281
  | NOT f1 ->
282
      Buffer.add_string sb "~";
283
      prio 4 f1
284
  | AT (s, f1) ->
285
      Buffer.add_string sb "@ ";
286
      Buffer.add_string sb s;
287
      Buffer.add_string sb " ";
288
      prio 4 f1
289
  | OR (f1, f2) ->
290
      prio 2 f1;
291
      Buffer.add_string sb " | ";
292
      prio 2 f2
293
  | AND (f1, f2) ->
294
      prio 3 f1;
295
      Buffer.add_string sb " & ";
296
      prio 3 f2
297
  | EQU (f1, f2) ->
298
      prio 0 f1;
299
      Buffer.add_string sb " <=> ";
300
      prio 0 f2
301
  | IMP (f1, f2) ->
302
      prio 2 f1;
303
      Buffer.add_string sb " => ";
304
      prio 2 f2
305
  | EX (s, f1) ->
306
      Buffer.add_string sb "<";
307
      Buffer.add_string sb s;
308
      Buffer.add_string sb ">";
309
      prio 4 f1
310
  | AX (s, f1) ->
311
      Buffer.add_string sb "[";
312
      Buffer.add_string sb s;
313
      Buffer.add_string sb "]";
314
      prio 4 f1
315
  | ALLOWS (s, f1) ->
316
      Buffer.add_string sb "<{";
317
      Buffer.add_string sb (
318
          match s with
319
          | [] -> " "
320
          | _ ->(Str.concat " " (L.map string_of_int s))
321
      );
322
      Buffer.add_string sb "}>";
323
      prio 4 f1
324
  | ENFORCES (s, f1) ->
325
      Buffer.add_string sb "[{";
326
      Buffer.add_string sb (
327
          match s with
328
          | [] -> " "
329
          | _ ->(Str.concat " " (L.map string_of_int s))
330
      );
331
      Buffer.add_string sb "}]";
332
      prio 4 f1
333
  | ATLEASTPROB (p, f1) ->
334
      Buffer.add_string sb "{>=";
335
      Buffer.add_string sb (string_of_rational p);
336
      Buffer.add_string sb "}";
337
      prio 4 f1
338
  | LESSPROBFAIL (p, f1) ->
339
      Buffer.add_string sb "{<";
340
      Buffer.add_string sb (string_of_rational p);
341
      Buffer.add_string sb "} ~ ";
342
      prio 4 f1
343
  | MIN (n, s, f1) ->
344
      Buffer.add_string sb "{>=";
345
      Buffer.add_string sb (string_of_int n);
346
      Buffer.add_string sb " ";
347
      Buffer.add_string sb s;
348
      Buffer.add_string sb "}";
349
      prio 4 f1
350
  | MAX (n, s, f1) ->
351
      Buffer.add_string sb "{<=";
352
      Buffer.add_string sb (string_of_int n);
353
      Buffer.add_string sb " ";
354
      Buffer.add_string sb s;
355
      Buffer.add_string sb "}";
356
      prio 4 f1
357
  | MORETHAN (n, s, f1) ->
358
      Buffer.add_string sb "{>";
359
      Buffer.add_string sb (string_of_int n);
360
      Buffer.add_string sb " ";
361
      Buffer.add_string sb s;
362
      Buffer.add_string sb "}";
363
      prio 4 f1
364
  | MAXEXCEPT (n, s, f1) ->
365
      Buffer.add_string sb "{<=";
366
      Buffer.add_string sb (string_of_int n);
367
      Buffer.add_string sb " ~ ";
368
      Buffer.add_string sb s;
369
      Buffer.add_string sb "}";
370
      prio 4 f1 (* actually is prio of ~ and not of <= *)
371
  | ID (f1) ->
372
      Buffer.add_string sb "O";
373
      prio 4 f1
374
  | NORM(f1, f2) ->
375
      Buffer.add_string sb "(";
376
      exportFormula_buffer sb f1;
377
      Buffer.add_string sb " =o ";
378
      exportFormula_buffer sb f2;
379
      Buffer.add_string sb ")"
380
  | NORMN(f1, f2) ->
381
      Buffer.add_string sb "~(";
382
      exportFormula_buffer sb (negate f1);
383
      Buffer.add_string sb " =o ";
384
      exportFormula_buffer sb (negate f2);
385
      Buffer.add_string sb ")"
386
  | CHC (f1, f2) ->
387
      Buffer.add_string sb "(";
388
      exportFormula_buffer sb f1;
389
      Buffer.add_string sb " + ";
390
      exportFormula_buffer sb f2;
391
      Buffer.add_string sb ")"
392
  | CONST s -> Buffer.add_string sb "=";
393
      Buffer.add_string sb s
394
  | CONSTN s -> Buffer.add_string sb "~=";
395
      Buffer.add_string sb s
396
  | FUS (first, f1) ->
397
      Buffer.add_string sb (if first then "[pi1]" else "[pi2]");
398
      prio 4 f1
399
  | MU (s, f1) ->
400
      Buffer.add_string sb "μ";
401
      Buffer.add_string sb s;
402
      Buffer.add_string sb ".";
403
      prio 4 f1
404
  | NU (s, f1) ->
405
      Buffer.add_string sb "ν";
406
      Buffer.add_string sb s;
407
      Buffer.add_string sb ".";
408
      prio 4 f1
409
  | VAR s ->
410
     Buffer.add_string sb s
411
  | AF f1 ->
412
     Buffer.add_string sb "AF ";
413
     prio 4 f1
414
  | EF f1 ->
415
     Buffer.add_string sb "EF ";
416
     prio 4 f1
417
  | AG f1 ->
418
     Buffer.add_string sb "AG ";
419
     prio 4 f1
420
  | EG f1 ->
421
     Buffer.add_string sb "EG ";
422
     prio 4 f1
423
  | AU (f1, f2) ->
424
     Buffer.add_string sb "A (";
425
     prio 4 f1;
426
     Buffer.add_string sb " U ";
427
     prio 4 f2;
428
     Buffer.add_string sb ")"
429
  | EU (f1, f2) ->
430
     Buffer.add_string sb "E (";
431
     prio 4 f1;
432
     Buffer.add_string sb " U ";
433
     prio 4 f2;
434
     Buffer.add_string sb ")"
435

    
436
(** Converts a formula into a string representation.
437
    Parentheses are ommited where possible
438
    where the preference rules are defined as usual.
439
    @param f A formula.
440
    @return A string representing f.
441
 *)
442
let exportFormula f =
443
  let sb = Buffer.create 128 in
444
  exportFormula_buffer sb f;
445
  Buffer.contents sb
446

    
447
let string_of_formula = exportFormula
448

    
449
(** export (CL)-formula suitable for tatl-inputs *)
450
let rec exportTatlFormula_buffer sb f =
451
  let prio n lf =
452
    let prionr = function
453
      | EQU _ -> 0
454
      | IMP _  -> 1
455
      | OR _ -> 2
456
      | AND _ -> 3
457
      | _ -> 4
458
    in
459
    if prionr lf < n then begin
460
      Buffer.add_char sb '(';
461
      exportTatlFormula_buffer sb lf;
462
      Buffer.add_char sb ')'
463
    end
464
    else exportTatlFormula_buffer sb lf
465
  in
466
  match f with
467
  | TRUE -> Buffer.add_string sb "(p \\/ ~p)"
468
  | FALSE -> Buffer.add_string sb "(p /\\ ~p)"
469
  | AP s -> Buffer.add_string sb s
470
  | NOT f1 ->
471
      Buffer.add_string sb "~";
472
      prio 4 f1
473
  | OR (f1, f2) ->
474
      prio 2 f1;
475
      Buffer.add_string sb " \\/ ";
476
      prio 2 f2
477
  | AND (f1, f2) ->
478
      prio 3 f1;
479
      Buffer.add_string sb " /\\ ";
480
      prio 3 f2
481
  | EQU (f1, f2) ->
482
      prio 0 (AND (IMP (f1,f2), IMP (f2,f1)))
483
  | IMP (f1, f2) ->
484
      prio 2 f1;
485
      Buffer.add_string sb " -> ";
486
      prio 2 f2
487
  | ALLOWS (s, f1) ->
488
      Buffer.add_string sb "<<";
489
      Buffer.add_string sb (
490
          match s with
491
          | [] -> " "
492
          | _ ->(Str.concat "," (L.map string_of_int s))
493
      );
494
      Buffer.add_string sb ">>X ";
495
      prio 4 f1
496
  | ENFORCES (s, f1) ->
497
      Buffer.add_string sb "~<<";
498
      Buffer.add_string sb (
499
          match s with
500
          | [] -> " "
501
          | _ ->(Str.concat "," (L.map string_of_int s))
502
      );
503
      Buffer.add_string sb ">>X ~ ";
504
      prio 4 f1
505
  | EX _
506
  | AX _
507
  | MIN _
508
  | MAX _
509
  | MORETHAN _
510
  | MAXEXCEPT _
511
  | AT _
512
  | CONST _
513
  | CONSTN _
514
  | CHC _
515
  | ATLEASTPROB _
516
  | LESSPROBFAIL _
517
  | ID _
518
  | NORM _
519
  | NORMN _
520
  | FUS _
521
  | MU _
522
  | NU _
523
  | VAR _
524
  | AF _
525
  | EF _
526
  | AG _
527
  | EG _
528
  | AU _
529
  | EU _ -> raise (CoAlgException ("export to tatl: Not connectives of CL"))
530

    
531
let exportTatlFormula f =
532
  let sb = Buffer.create 128 in
533
  exportTatlFormula_buffer sb f;
534
  Buffer.contents sb
535

    
536
(** Appends a string representation of a sorted formula to a string buffer.
537
    Parentheses are ommited where possible
538
    where the preference rules are defined as usual.
539
    @param sb A string buffer.
540
    @param (s, f) A sorted formula.
541
 *)
542
let rec exportSortedFormula_buffer sb (s, f) =
543
  Buffer.add_string sb (string_of_int s);
544
  Buffer.add_string sb ": ";
545
  exportFormula_buffer sb f
546

    
547
(** Converts a sorted formula into a string representation.
548
    Parentheses are ommited where possible
549
    where the preference rules are defined as usual.
550
    @param f A sorted formula.
551
    @return A string representing f.
552
 *)
553
let exportSortedFormula f =
554
  let sb = Buffer.create 128 in
555
  exportSortedFormula_buffer sb f;
556
  Buffer.contents sb
557

    
558
(** Converts a (sorted) formula query into a string representation.
559
    @param tbox A list of sorted formulae representing a TBox.
560
    @param f A sorted formula.
561
    @return A string representing tbox |- f.
562
 *)
563
let exportQuery tbox f =
564
  let sb = Buffer.create 1000 in
565
  let rec expFl = function
566
    | [] -> ()
567
    | h::tl ->
568
        exportSortedFormula_buffer sb h;
569
        if tl <> [] then Buffer.add_string sb "; " else ();
570
        expFl tl
571
  in
572
  expFl tbox;
573
  Buffer.add_string sb "  |-  ";
574
  exportSortedFormula_buffer sb f;
575
  Buffer.contents sb
576

    
577
(** Converts a (sorted) formula query into a string representation. Such that
578
    coalg can read it again using importQuery
579
    @param tbox A list of sorted formulae representing a TBox.
580
    @param f A sorted formula.
581
    @return A string representing tbox |- f.
582
 *)
583
let exportQueryParsable tbox (_,f) =
584
  let sb = Buffer.create 1000 in
585
  let rec expFl = function
586
    | [] -> ()
587
    | (_,h)::tl ->
588
        exportFormula_buffer sb h;
589
        if tl <> [] then Buffer.add_string sb "; " else ();
590
        expFl tl
591
  in
592
  expFl tbox;
593
  Buffer.add_string sb "  |-  ";
594
  exportFormula_buffer sb f;
595
  Buffer.contents sb
596

    
597

    
598
(* NB: True and False are the propositional constants. Lower case
599
   true/false are regardes as atomic propositions and we emit a warning
600
*)
601
let lexer = A.make_lexer
602
    [":";";";"|-";"(";")";"=>";"<=>";"|";"&";"~";"@";"True";"False";"true";"false";"<";">";"[";"]";"{<=";"{>=";"}";"+";"[pi1]";"[pi2]"
603
     ;"[{";"}]";"<{";"}>";",";"/";"{<";"=";"=o";"O"
604
     ;"μ";"ν";"."
605
     ;"AX";"EX";"AF";"EF";"AG";"EG";"A";"E";"U"
606
    ]
607

    
608
let mk_exn s = CoAlgException s
609

    
610
(** Process from inside out. cons all variables seen, remove them when
611
    binding fixpoint is found. Fixpoint type may only change if last
612
    (inner) fixpoint didn't include any free variables.
613
 *)
614
let rec verifyMuAltFree formula =
615
  let proc = verifyMuAltFree in
616
  match formula with
617
  | TRUE | FALSE | AP _ -> ("none", [])
618
  | CONST _
619
  | CONSTN _ -> ("none", [])
620
  | AT (_,a) | NOT a
621
  | EX (_,a) | AX (_,a) -> proc a
622
  | OR (a,b) | AND (a,b)
623
  | EQU (a,b) | IMP (a,b) ->
624
     let (atype, afree) = proc a
625
     and (btype, bfree) = proc b in
626
     if (compare atype "μ" == 0 && compare btype "ν" == 0) ||
627
          (compare atype "ν" == 0 && compare btype "μ" == 0) then
628
       raise (CoAlgException ("formula not alternation-free"));
629
     if compare atype "none" == 0 then
630
       (btype, List.flatten [afree; bfree])
631
     else
632
       (atype, List.flatten [afree; bfree])
633
  | ENFORCES (_,a) | ALLOWS   (_,a)
634
  | MIN (_,_,a)    | MAX (_,_,a)
635
  | ATLEASTPROB (_, a) | LESSPROBFAIL (_, a)
636
  | MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> proc a
637
  | ID(a) -> proc a
638
  | NORM(a, b) | NORMN(a, b)
639
  | CHC (a,b)  ->
640
     let (atype, afree) = proc a
641
     and (btype, bfree) = proc b in
642
     if (compare atype "μ" == 0 && compare btype "ν" == 0) ||
643
          (compare atype "ν" == 0 && compare btype "μ" == 0) then
644
       raise (CoAlgException ("formula not alternation-free"));
645
     if compare atype "none" == 0 then
646
       (btype, List.flatten [afree; bfree])
647
     else
648
       (atype, List.flatten [afree; bfree])
649
  | FUS (_,a) -> proc a
650
  | MU (s, f) ->
651
     let (fptype, free) = proc f in
652
     (if (compare fptype "ν" == 0) then
653
        raise (CoAlgException ("formula not alternation-free")));
654
     let predicate x = compare x s != 0 in
655
     let newfree = List.filter predicate free in
656
     if newfree = [] then
657
       ("none", [])
658
     else
659
       ("μ", newfree)
660
  | NU (s, f) ->
661
     let (fptype, free) = proc f in
662
     (if (compare fptype "μ" == 0) then
663
        raise (CoAlgException ("formula not alternation-free")));
664
     let predicate x = compare x s != 0 in
665
     let newfree = List.filter predicate free in
666
     if newfree = [] then
667
       ("none", [])
668
     else
669
       ("ν", newfree)
670
  | VAR s -> ("none", [s])
671
  | AF _  | EF _ | AG _ | EG _ | AU _ | EU _ ->
672
     raise (CoAlgException ("verifyMuAltFree: CTL should have been removed at this point"))
673

    
674

    
675
(** Process from outside in. For every variable bound keep the tuple
676
    (name, negations). For every negation crossed map a +1 over snd on
677
    that list. For every variable met check that the matching
678
    negations is even.
679
 *)
680
let rec verifyMuMonotone negations formula =
681
  let proc = verifyMuMonotone negations in
682
  match formula with
683
  | TRUE | FALSE | AP _ -> ()
684
  | CONST _
685
  | CONSTN _ -> ()
686
  | AT (_,a)
687
  | EX (_,a) | AX (_,a) -> proc a
688
  | OR (a,b) | AND (a,b)
689
  | EQU (a,b) | IMP (a,b) -> (proc a ; proc b)
690
  | ENFORCES (_,a) | ALLOWS   (_,a)
691
  | MIN (_,_,a)    | MAX (_,_,a)
692
  | ATLEASTPROB (_, a) | LESSPROBFAIL (_, a)
693
  | MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> proc a
694
  | ID(a) -> proc a
695
  | NORM(a, b) | NORMN(a, b) -> (proc a; proc b)
696
  | CHC (a,b)  -> (proc a ; proc b)
697
  | FUS (_,a) -> proc a
698
  | MU (s, f)
699
  | NU (s, f) ->
700
     let newNeg = (s, 0) :: negations in
701
     verifyMuMonotone newNeg f
702
  | VAR s ->
703
     let finder (x, _) = compare x s == 0 in
704
     let (_, neg) = List.find finder negations in
705
     if ((neg land 1) != 0) then raise (CoAlgException ("formula not monotone"))
706
  | NOT a ->
707
     let increment (s, n) = (s, n+1) in
708
     let newNeg = List.map increment negations in
709
     verifyMuMonotone newNeg a
710
  | AF _  | EF _ | AG _ | EG _ | AU _ | EU _ ->
711
     raise (CoAlgException ("verifyMuMonotone: CTL should have been removed at this point"))
712

    
713
let rec verifyMuGuarded unguarded formula =
714
  let proc = verifyMuGuarded unguarded in
715
  match formula with
716
  | TRUE | FALSE | AP _ -> ()
717
  | CONST _
718
  | CONSTN _ -> ()
719
  | AT (_,a) | NOT a -> proc a
720
  | EX (_,a) | AX (_,a) -> verifyMuGuarded [] a
721
  | OR (a,b) | AND (a,b)
722
  | EQU (a,b) | IMP (a,b) -> (proc a ; proc b)
723
  | ENFORCES (_,a) | ALLOWS   (_,a)
724
  | MIN (_,_,a)    | MAX (_,_,a)
725
  | ATLEASTPROB (_, a) | LESSPROBFAIL (_, a)
726
  | MORETHAN (_,_,a) | MAXEXCEPT (_,_,a) -> proc a
727
  | ID(a) -> proc a
728
  | NORM(a, b) | NORMN(a, b) -> (proc a; proc b)
729
  | CHC (a,b)  -> (proc a ; proc b)
730
  | FUS (_,a) -> proc a
731
  | MU (s, f)
732
  | NU (s, f) ->
733
     let newUnguard = s :: unguarded in
734
     verifyMuGuarded newUnguard f
735
  | VAR s ->
736
     let finder x = compare x s == 0 in
737
     if List.exists finder unguarded then
738
       raise (CoAlgException ("formula not guarded"))
739
  | AF _  | EF _ | AG _ | EG _ | AU _ | EU _ ->
740
     raise (CoAlgException ("verifyMuGuarded: CTL should have been removed at this point"))
741

    
742
let verifyFormula formula =
743
  verifyMuAltFree formula;
744
  verifyMuMonotone [] formula;
745
  verifyMuGuarded [] formula
746

    
747
(** These functions parse a token stream to obtain a formula.
748
    It is a standard recursive descent procedure.
749
    @param ts A token stream.
750
    @return The resulting (sub-)formula.
751
    @raise CoAlgException if ts does not represent a formula.
752
 *)
753
let rec parse_formula (symtab: 'a list) ts =
754
  let formula = (parse_imp symtab ts) in
755
  let f1 = convertToMu formula in
756
  match Stream.peek ts with
757
  | None -> f1
758
  | Some (A.Kwd "<=>") ->
759
      Stream.junk ts;
760
      let f2 = parse_formula symtab ts in
761
      EQU (f1, f2)
762
  | _ -> f1
763

    
764
(** These functions parse a token stream to obtain a formula.
765
    It is a standard recursive descent procedure.
766
    @param ts A token stream.
767
    @return The resulting (sub-)formula.
768
    @raise CoAlgException if ts does not represent a formula.
769
 *)
770
and parse_imp symtab ts=
771
  let f1 = parse_or symtab ts in
772
  match Stream.peek ts with
773
  | None -> f1
774
  | Some (A.Kwd "=>") ->
775
      Stream.junk ts;
776
      let f2 = parse_imp symtab ts in
777
      IMP (f1, f2)
778
  | _ -> f1
779

    
780
(** These functions parse a token stream to obtain a formula.
781
    It is a standard recursive descent procedure.
782
    @param ts A token stream.
783
    @return The resulting (sub-)formula.
784
    @raise CoAlgException if ts does not represent a formula.
785
 *)
786
and parse_or symtab ts =
787
  let f1 = parse_and symtab ts in
788
  match Stream.peek ts with
789
  | None -> f1
790
  | Some (A.Kwd "|") ->
791
      Stream.junk ts;
792
      let f2 = parse_or symtab ts in
793
      OR (f1, f2)
794
  | _ -> f1
795

    
796
(** These functions parse a token stream to obtain a formula.
797
    It is a standard recursive descent procedure.
798
    @param ts A token stream.
799
    @return The resulting (sub-)formula.
800
    @raise CoAlgException if ts does not represent a formula.
801
 *)
802
and parse_and symtab ts =
803
  let f1 = parse_cimp symtab ts in
804
  match Stream.peek ts with
805
  | None -> f1
806
  | Some (A.Kwd "&") ->
807
      Stream.junk ts;
808
      let f2 = parse_and symtab ts in
809
      AND (f1, f2)
810
  | _ -> f1
811

    
812
(** These functions parse a token stream to obtain a formula.
813
    It is a standard recursive descent procedure.
814
    @param ts A token stream.
815
    @return The resulting (sub-)formula.
816
    @raise CoAlgException if ts does not represent a formula.
817
 *)
818
and parse_cimp symtab ts =
819
  let f1 = parse_rest symtab ts in
820
  match Stream.peek ts with
821
  | None -> f1
822
  | Some (A.Kwd "=o") ->
823
      Stream.junk ts;
824
      let f2 = parse_cimp symtab ts in
825
      NORM (f1, f2)
826
  | _ -> f1
827

    
828
(** These functions parse a token stream to obtain a formula.
829
    It is a standard recursive descent procedure.
830
    @param ts A token stream.
831
    @return The resulting (sub-)formula.
832
    @raise CoAlgException if ts does not represent a formula.
833
 *)
834
and parse_rest symtab ts =
835
  let boxinternals noNo es =
836
    let n =
837
      if noNo then 0
838
      else
839
        match Stream.next ts with
840
        | A.Int n when n >= 0 -> n
841
        | t -> A.printError mk_exn ~t ~ts "<non-negative number> expected: "
842
    in
843
    let (s,denominator) =
844
      match Stream.peek ts with
845
      | Some (A.Ident s1) -> Stream.junk ts; (s1,0)
846
      | Some (A.Kwd c) when c = es -> ("", 0)
847
      | Some (A.Kwd "/") -> begin
848
            Stream.junk ts;
849
            match Stream.next ts with
850
            | A.Int denom when denom > 0 -> ("", denom)
851
            | t -> A.printError mk_exn ~t ~ts "<positive number> (the denominator) expected: "
852
        end
853
      | _ -> A.printError mk_exn ~ts ("role name or \"" ^ es ^ "\" expected: ")
854
    in
855
    if (denominator < n) then begin
856
       let explanation =
857
        ("nominator="^(string_of_int n)^" but denominator="^(string_of_int denominator))
858
       in
859
       A.printError mk_exn ~ts ("Nominator must not be larger than the denominator "
860
                               ^"("^explanation^") at: "
861
                               )
862
    end;
863
    let _ =
864
      match Stream.next ts with
865
      | A.Kwd c when c = es -> ()
866
      | t -> A.printError mk_exn ~t ~ts ("\"" ^ es ^ "\" expected: ")
867
    in
868
    (n, denominator, s)
869
  in
870
  let rec agentlist es =
871
    let allAgents = CoolUtils.cl_get_agents () in
872
    match Stream.next ts with
873
    | A.Int n -> if CoolUtils.TArray.elem n allAgents
874
                 then n::(agentlist es)
875
                 else A.printError mk_exn ~ts ("agent name \"" ^ (string_of_int n) ^ "\" unknonwn, see --agents: ")
876
    | A.Kwd c when c = es -> []
877
    | _ -> A.printError mk_exn ~ts ("agent name or " ^ es ^ "\" expected: ")
878
  in
879
  match Stream.next ts with
880
  | A.Kwd "true" ->
881
    print_endline "*** Warning: \"true\" used as propositional variable.";
882
    AP "true"
883
  | A.Kwd "false" ->
884
    print_endline "*** Warning: \"false\" used as propositional variable.";
885
    AP "false"
886
  | A.Kwd "True" -> TRUE
887
  | A.Kwd "False" -> FALSE
888
  | A.Ident s ->
889
      (try
890
          let finder (x, _) = compare x s == 0 in
891
          let (_, symbol) = List.find finder symtab in
892
          VAR symbol
893
        with Not_found -> AP s)
894
  | A.Kwd "~" ->
895
      let f = parse_rest symtab ts in
896
      NOT f
897
  | A.Kwd "@" ->
898
      let s =
899
        match Stream.next ts with
900
        | A.Ident s when isNominal s -> s
901
        | t -> A.printError mk_exn ~t ~ts ("nominal expected: ")
902
      in
903
      let f = parse_rest symtab ts in
904
      AT (s, f)
905
  | A.Kwd "<" ->
906
      let (_, _, s) = boxinternals true ">" in
907
      let f1 = parse_rest symtab ts in
908
      EX (s, f1)
909
  | A.Kwd "[" ->
910
      let (_, _, s) = boxinternals true "]" in
911
      let f1 = parse_rest symtab ts in
912
      AX (s, f1)
913
  | A.Kwd "[{" ->
914
      let ls = agentlist "}]" in
915
      let f1 = parse_rest symtab ts in
916
      ENFORCES (ls, f1)
917
  | A.Kwd "<{" ->
918
      let ls = agentlist "}>" in
919
      let f1 = parse_rest symtab ts in
920
      ALLOWS (ls, f1)
921
  | A.Kwd "{>=" ->
922
      let (n, denom, s) = boxinternals false "}" in
923
      let f1 = parse_rest symtab ts in
924
      if (denom <> 0)
925
      then ATLEASTPROB (rational_of_int n denom, f1)
926
      else MIN (n, s, f1)
927
  | A.Kwd "{<=" ->
928
      let (n, denom, s) = boxinternals false "}" in
929
      let f1 = parse_rest symtab ts in
930
      if (denom <> 0)
931
      then A.printError mk_exn ~ts "Can not express {<= probability}"
932
      else MAX (n, s, f1)
933
  | A.Kwd "{<" ->
934
      let (n, denom, s) = boxinternals false "}" in
935
      let f1 = parse_rest symtab ts in
936
      if (denom <> 0)
937
      then LESSPROBFAIL (rational_of_int n denom, NOT f1)
938
      else A.printError mk_exn ~ts "The \"Less than\" < is not implemented yet"
939
  | A.Kwd "=" -> begin
940
          match Stream.next ts with
941
          (* | A.Int s *)
942
          | A.Kwd s
943
          | A.Ident s -> CONST s
944
          | _ -> A.printError mk_exn ~ts "constant = expects an identifier afterwards"
945
    end
946
  | A.Kwd "(" -> begin
947
      let f = parse_formula symtab ts in
948
      match Stream.next ts with
949
      | A.Kwd ")" -> f
950
      | A.Kwd "+" -> begin
951
          let f2 = parse_formula symtab ts in
952
          match Stream.next ts with
953
          | A.Kwd ")" -> CHC (f, f2)
954
          | t -> A.printError mk_exn ~t ~ts "\")\" expected: "
955
        end
956
      | t -> A.printError mk_exn ~t ~ts "\")\" or \"+\" expected: "
957
    end
958
  | A.Kwd "O" ->
959
    let f = parse_rest symtab ts in
960
      ID f
961
  | A.Kwd "[pi1]" ->
962
      let f = parse_rest symtab ts in
963
      FUS (true, f)
964
  | A.Kwd "[pi2]" ->
965
      let f = parse_rest symtab ts in
966
      FUS (false, f)
967
  | A.Kwd "μ" ->
968
      let (_, _, s) = boxinternals true "." in
969
      let symbol = Stream.next gensym in
970
      let newtab = (s, symbol) :: symtab in
971
      let f1 = parse_rest newtab ts in
972
      MU (symbol, f1)
973
  | A.Kwd "ν" ->
974
      let (_, _, s) = boxinternals true "." in
975
      let symbol = Stream.next gensym in
976
      let newtab = (s, symbol) :: symtab in
977
      let f1 = parse_rest newtab ts in
978
      NU (symbol, f1)
979
  | A.Kwd "AF" ->
980
      let f = parse_rest symtab ts in
981
      AF f
982
  | A.Kwd "EF" ->
983
      let f = parse_rest symtab ts in
984
      EF f
985
  | A.Kwd "AG" ->
986
      let f = parse_rest symtab ts in
987
      AG f
988
  | A.Kwd "EG" ->
989
      let f = parse_rest symtab ts in
990
      EG f
991
  | A.Kwd "A" ->
992
     assert (Stream.next ts = A.Kwd "(");
993
     let f1 = parse_formula symtab ts in
994
     assert (Stream.next ts = A.Kwd "U");
995
     let f2 = parse_formula symtab ts in
996
     assert (Stream.next ts = A.Kwd ")");
997
     AU (f1, f2)
998
  | A.Kwd "E" ->
999
     assert (Stream.next ts = A.Kwd "(");
1000
     let f1 = parse_formula symtab ts in
1001
     assert (Stream.next ts = A.Kwd "U");
1002
     let f2 = parse_formula symtab ts in
1003
     assert (Stream.next ts = A.Kwd ")");
1004
     EU (f1, f2)
1005
  | A.Kwd "AX" ->
1006
     let f1 = parse_rest symtab ts in
1007
     AX ("", f1)
1008
  | A.Kwd "EX" ->
1009
     let f1 = parse_rest symtab ts in
1010
     EX ("", f1)
1011
  | t -> A.printError mk_exn ~t ~ts
1012
      "\"<\", \"[\", \"{>=\", \"{<=\", \"@\", \"~\", \"(\",
1013
      \"True\", \"False\", \"=\", \"=o\", \"O\" or <ident> expected: "
1014

    
1015
(** Parses a sorted formula.
1016
    @param ts A token stream.
1017
    @return A sorted formula.
1018
    @raise CoAlgException If ts does not represent a sorted formula.
1019
 *)
1020
let parse_sortedFormula ts =
1021
  let nr =
1022
    match Stream.peek ts with
1023
    | Some (A.Int n) ->
1024
        if n >= 0 then begin
1025
          Stream.junk ts;
1026
          let () =
1027
            match Stream.next ts with
1028
            | A.Kwd ":" -> ()
1029
            | t -> A.printError mk_exn ~t ~ts ("\":\" expected: ")
1030
          in
1031
          n
1032
        end else
1033
          A.printError mk_exn ~ts ("<non-negative number> expected: ")
1034
    | _ -> 0
1035
  in
1036
  let f = parse_formula [] ts in
1037
  (nr, f)
1038

    
1039
(** Parses a list of sorted formulae separated by ";".
1040
    @param ts A token stream.
1041
    @param acc The list of sorted formulae parsed so far.
1042
    @return The resulting list of sorted formula.
1043
    @raise CoAlgException if ts does not represent a list of sorted formulae.
1044
 *)
1045
let rec parse_sortedFormulaList ts acc =
1046
  let f1 = parse_sortedFormula ts in
1047
  match Stream.peek ts with
1048
  | Some (A.Kwd ";") ->
1049
      Stream.junk ts;
1050
      parse_sortedFormulaList ts (f1::acc)
1051
  | _ -> List.rev (f1::acc)
1052

    
1053
(** A common wrapper for import functions.
1054
    @param fkt An import function.
1055
    @param s A string.
1056
    @return The object imported from s using fkt.
1057
    @raise CoAlgException If ts is not empty.
1058
 *)
1059
let importWrapper fkt s =
1060
  let ts = lexer s in
1061
  try
1062
    let res = fkt ts in
1063
    let _ =
1064
      match Stream.peek ts with
1065
      | None -> ()
1066
      | Some _ -> A.printError mk_exn ~ts "EOS expected: "
1067
    in
1068
    res
1069
  with Stream.Failure -> A.printError mk_exn ~ts "unexpected EOS"
1070

    
1071
(** Parses a string to obtain a formula.
1072
    @param s A string representing a formula.
1073
    @return The resulting formula.
1074
    @raise CoAlgException if s does not represent a formula.
1075
 *)
1076
let importFormula s = importWrapper (parse_formula []) s
1077

    
1078
(** Parses a string to obtain a sorted formula.
1079
    @param s A string representing a sorted formula.
1080
    @return The sorted formula.
1081
    @raise CoAlgException If s does not represent a sorted formula.
1082
 *)
1083
let importSortedFormula s = importWrapper parse_sortedFormula s
1084

    
1085
(** Parses a string to obtain a (sorted) formula query.
1086
    @param s A string representing a formula query.
1087
    @return A pair (tbox, f) where
1088
    tbox is a list of sorted formulae representing the TBox; and
1089
    f is a sorted formula.
1090
    @raise CoAlgException if s does not represent a formula query.
1091
 *)
1092
let importQuery s =
1093
  let fkt ts =
1094
    match Stream.peek ts with
1095
    | Some (A.Kwd "|-") ->
1096
        Stream.junk ts;
1097
        let f = parse_sortedFormula ts in
1098
        ([], f)
1099
    | _ ->
1100
        let fl = parse_sortedFormulaList ts [] in
1101
        match Stream.peek ts with
1102
        | Some (A.Kwd "|-") ->
1103
            Stream.junk ts;
1104
            let f = parse_sortedFormula ts in
1105
            (fl, f)
1106
        | _ ->
1107
            if List.length fl = 1 then ([], List.hd fl)
1108
            else A.printError mk_exn ~ts "\"|-\" expected: "
1109
  in
1110
  importWrapper fkt s
1111

    
1112

    
1113
(** Converts the negation of a formula to negation normal form
1114
    by "pushing in" the negations "~".
1115
    The symbols "<=>" and "=>" are substituted by their usual definitions.
1116
    @param f A formula.
1117
    @return A formula in negation normal form and not containing "<=>" or "=>"
1118
    that is equivalent to ~f.
1119
 *)
1120
let rec nnfNeg f =
1121
  match f with
1122
  | TRUE -> FALSE
1123
  | FALSE -> TRUE
1124
  | AP _ -> NOT f
1125
  | VAR _ -> f
1126
  | NOT f1 -> nnf f1
1127
  | AT (s, f1) -> AT (s, nnfNeg f1)
1128
  | OR (f1, f2) -> AND (nnfNeg f1, nnfNeg f2)
1129
  | AND (f1, f2) -> OR (nnfNeg f1, nnfNeg f2)
1130
  | EQU (f1, f2) -> OR (AND (nnf f1, nnfNeg f2), AND (nnf f2, nnfNeg f1))
1131
  | IMP (f1, f2) -> AND (nnf f1, nnfNeg f2)
1132
  | EX (s, f1) -> AX (s, nnfNeg f1)
1133
  | AX (s, f1) -> EX (s, nnfNeg f1)
1134
  | ENFORCES (s, f1) -> ALLOWS (s, nnfNeg f1)
1135
  | ALLOWS (s, f1) -> ENFORCES (s, nnfNeg f1)
1136
  | MIN (n, s, f1) -> if n = 0 then FALSE else MAXEXCEPT (n-1, s, nnfNeg f1)
1137
  | MAX (n, s, f1) -> MORETHAN (n, s, nnf f1)
1138
  | MORETHAN (n, s, f1) -> MAXEXCEPT (n, s, nnfNeg f1)
1139
  | MAXEXCEPT (n, s, f1) -> MORETHAN (n, s, nnfNeg f1)
1140
  | ATLEASTPROB (p, f1) -> LESSPROBFAIL (p, nnfNeg f1)
1141
  | LESSPROBFAIL (p, f1) -> ATLEASTPROB (p, nnfNeg f1)
1142
  | CONST s -> CONSTN s
1143
  | CONSTN s -> CONST s
1144
  | ID (f1) -> ID (nnfNeg f1)
1145
  | NORM(f1, f2) -> NORMN(nnfNeg f1, nnfNeg f2)
1146
  | NORMN(f1, f2) -> NORM (nnfNeg f1, nnfNeg f2)
1147
  | CHC (f1, f2) -> CHC (nnfNeg f1, nnfNeg f2)
1148
  | FUS (first, f1) -> FUS (first, nnfNeg f1)
1149
  | MU (s, f1) -> NU(s, nnfNeg f1)
1150
  | NU (s, f1) -> MU(s, nnfNeg f1)
1151
  | AF _
1152
  | EF _
1153
  | AG _
1154
  | EG _
1155
  | AU _
1156
  | EU _ -> raise (CoAlgException ("nnfNeg: CTL should have been removed at this point"))
1157

    
1158
(** Converts a formula to negation normal form
1159
    by "pushing in" the negations "~".
1160
    The symbols "<=>" and "=>" are substituted by their usual definitions.
1161
    @param f A formula.
1162
    @return A formula in negation normal form and not containing "<=>" or "=>"
1163
    that is equivalent to f.
1164
 *)
1165
and nnf f =
1166
  match f with
1167
  | TRUE
1168
  | FALSE
1169
  | AP _
1170
  | NOT (AP _)
1171
  | CONST _
1172
  | CONSTN _
1173
  | VAR _ -> f
1174
  | NOT f1 -> nnfNeg f1
1175
  | AT (s, f1) ->
1176
      let ft1 = nnf f1 in
1177
      if ft1 == f1 then f else AT (s, ft1)
1178
  | OR (f1, f2) ->
1179
      let ft1 = nnf f1 in
1180
      let ft2 = nnf f2 in
1181
      if ft1 == f1 && ft2 == f2 then f else OR (ft1, ft2)
1182
  | AND (f1, f2) ->
1183
      let ft1 = nnf f1 in
1184
      let ft2 = nnf f2 in
1185
      if ft1 == f1 && ft2 == f2 then f else AND (ft1, ft2)
1186
  | EQU (f1, f2) -> AND (OR (nnfNeg f1, nnf f2), OR (nnfNeg f2, nnf f1))
1187
  | IMP (f1, f2) -> OR (nnfNeg f1, nnf f2)
1188
  | EX (s, f1) ->
1189
      let ft = nnf f1 in
1190
      if ft == f1 then f else EX (s, ft)
1191
  | AX (s, f1) ->
1192
      let ft = nnf f1 in
1193
      if ft == f1 then f else AX (s, ft)
1194
  | ENFORCES (s, f1) ->
1195
      let ft = nnf f1 in
1196
      if ft == f1 then f else ENFORCES (s, ft)
1197
  | ALLOWS (s, f1) ->
1198
      let ft = nnf f1 in
1199
      if ft == f1 then f else ALLOWS (s, ft)
1200
  | MIN (n, s, f1) ->
1201
      if n = 0 then TRUE
1202
      else
1203
        let ft = nnf f1 in
1204
        MORETHAN (n-1,s,ft)
1205
  | MAX (n, s, f1) ->
1206
      let ft = nnfNeg f1 in
1207
      MAXEXCEPT (n,s, ft)
1208
  | MORETHAN (n,s,f1) ->
1209
      let ft = nnf f1 in
1210
      if ft = f1 then f else MORETHAN (n,s,ft)
1211
  | MAXEXCEPT (n,s,f1) ->
1212
      let ft = nnf f1 in
1213
      if ft = f1 then f else MAXEXCEPT (n,s,ft)
1214
  | ATLEASTPROB (p, f1) ->
1215
      let ft = nnf f1 in
1216
      if ft == f1 then f else ATLEASTPROB (p, ft)
1217
  | LESSPROBFAIL (p, f1) ->
1218
      let ft = nnf f1 in
1219
      if ft == f1 then f else LESSPROBFAIL (p, ft)
1220
  | ID (f1) ->
1221
    let ft = nnf f1 in
1222
    if ft == f1 then f else ID(ft)
1223
  | NORM (f1, f2) ->
1224
      let ft1 = nnf f1 in
1225
      let ft2 = nnf f2 in
1226
      if ft1 == f1 && ft2 == f2 then f else NORM (ft1, ft2)
1227
  | NORMN (f1, f2) ->
1228
      let ft1 = nnf f1 in
1229
      let ft2 = nnf f2 in
1230
      if ft1 == f1 && ft2 == f2 then f else NORMN (ft1, ft2)
1231
  | CHC (f1, f2) ->
1232
      let ft1 = nnf f1 in
1233
      let ft2 = nnf f2 in
1234
      if ft1 == f1 && ft2 == f2 then f else CHC (ft1, ft2)
1235
  | FUS (first, f1) ->
1236
      let ft = nnf f1 in
1237
      if ft == f1 then f else FUS (first, ft)
1238
  | MU (s, f1) ->
1239
      let ft = nnf f1 in
1240
      if ft == f1 then f else MU (s, ft)
1241
  | NU (s, f1) ->
1242
      let ft = nnf f1 in
1243
      if ft == f1 then f else NU (s, ft)
1244
  | AF _
1245
  | EF _
1246
  | AG _
1247
  | EG _
1248
  | AU _
1249
  | EU _ -> raise (CoAlgException ("nnf: CTL should have been removed at this point"))
1250

    
1251
(** Simplifies a formula.
1252
    @param f A formula which must be in negation normal form.
1253
    @return A formula in negation normal form that is equivalent to f.
1254
    @raise CoAlgException if f is not in negation normal form.
1255
 *)
1256
let rec simplify f =
1257
  match f with
1258
  | TRUE
1259
  | FALSE
1260
  | AP _
1261
  | NOT (AP _)
1262
  | VAR _
1263
  | NOT (VAR _) -> f
1264
  | AT (s, f1) ->
1265
      let ft = simplify f1 in
1266
      begin
1267
        match ft with
1268
        | FALSE -> FALSE
1269
        | TRUE -> TRUE
1270
        | AT _ -> ft
1271
        | AP s1 when s = s1 -> TRUE
1272
        | NOT (AP s1) when s = s1 -> FALSE
1273
        | _ -> if ft == f1 then f else AT (s, ft)
1274
      end
1275
  | OR (f1, f2) ->
1276
      let ft1 = simplify f1 in
1277
      let ft2 = simplify f2 in
1278
      begin
1279
        match ft1, ft2 with
1280
        | TRUE, _ -> TRUE
1281
        | FALSE, _ -> ft2
1282
        | _, TRUE -> TRUE
1283
        | _, FALSE -> ft1
1284
        | _, _ ->
1285
            if (f1 == ft1) && (f2 == ft2) then f
1286
            else OR (ft1, ft2)
1287
      end
1288
  | AND (f1, f2) ->
1289
      let ft1 = simplify f1 in
1290
      let ft2 = simplify f2 in
1291
      begin
1292
        match ft1, ft2 with
1293
        | TRUE, _ -> ft2
1294
        | FALSE, _ -> FALSE
1295
        | _, TRUE -> ft1
1296
        | _, FALSE -> FALSE
1297
        | _, _ ->
1298
            if (f1 == ft1) && (f2 == ft2) then f
1299
            else AND (ft1, ft2)
1300
      end
1301
  | NOT _
1302
  | EQU _
1303
  | IMP _ -> raise (CoAlgException "Formula is not in negation normal form.")
1304
  | EX (s, f1) ->
1305
      let ft = simplify f1 in
1306
      begin
1307
        match ft with
1308
        | FALSE -> FALSE
1309
        | _ -> if ft == f1 then f else EX (s, ft)
1310
      end
1311
  | AX (s, f1) ->
1312
      let ft = simplify f1 in
1313
      begin
1314
        match ft with
1315
        | TRUE -> TRUE
1316
        | _ -> if ft == f1 then f else AX (s, ft)
1317
      end
1318
  | ENFORCES (s, f1) ->
1319
      let ft = simplify f1 in
1320
      begin
1321
        match ft with
1322
        (* Simplification rules are checked with dirks Generic.hs
1323
        let enforce ls = M (C ls)
1324
        let allow   ls = Neg . M (C ls) . Neg
1325
        provable $ F <-> enforce [1,2] F
1326
        *)
1327
        | TRUE -> TRUE
1328
        | FALSE -> FALSE
1329
        | _ -> if ft == f1 then f else ENFORCES (s, ft)
1330
      end
1331
  | ALLOWS (s, f1) ->
1332
      let ft = simplify f1 in
1333
      begin
1334
        match ft with
1335
        (* Simplification rules are checked with dirks Generic.hs
1336
        let enforce ls = M (C ls)
1337
        let allow   ls = Neg . M (C ls) . Neg
1338
        provable $ F <-> enforce [1,2] F
1339
        *)
1340
        | TRUE -> TRUE
1341
        | FALSE -> FALSE
1342
        | _ -> if ft == f1 then f else ALLOWS (s, ft)
1343
      end
1344
  | MIN (n, s, f1) ->
1345
      if n = 0 then TRUE
1346
      else
1347
        let ft = simplify f1 in
1348
        begin
1349
          match ft with
1350
          | FALSE -> FALSE
1351
          | _ -> if ft == f1 then f else MIN (n, s, ft)
1352
        end
1353
  | MORETHAN (n,s,f1) ->
1354
      let ft = simplify f1 in
1355
      if ft == f1 then f else MORETHAN (n,s,ft)
1356
  | MAXEXCEPT (n,s,f1) ->
1357
      let ft = simplify f1 in
1358
      if ft == f1 then f else MAXEXCEPT (n,s,ft)
1359
  | MAX (n, s, f1) ->
1360
      let ft = simplify f1 in
1361
      begin
1362
        match ft with
1363
        | FALSE -> TRUE
1364
        | _ -> if ft == f1 then f else MAX (n, s, ft)
1365
      end
1366
  | LESSPROBFAIL (p,f1) ->
1367
      let ft1 = simplify f1 in
1368
      if (ft1 == f1) then f else LESSPROBFAIL (p,ft1)
1369
  | ATLEASTPROB (p,f1) ->
1370
      let ft1 = simplify f1 in
1371
      if (ft1 == f1) then f else ATLEASTPROB (p,ft1)
1372
  | CONST _
1373
  | CONSTN _ -> f (* no simplifications possible *)
1374
  | ID (f1) ->
1375
    let ft1 = simplify f1 in
1376
    begin
1377
      match ft1 with
1378
        | TRUE -> TRUE
1379
        | FALSE -> FALSE
1380
        | _ -> if (ft1 == f1) then f else ID (ft1)
1381
    end
1382
  (* todo: more simplifications for KLM? *)
1383
  | NORM (f1, f2) ->
1384
      let ft1 = simplify f1 in
1385
      let ft2 = simplify f2 in
1386
      begin
1387
        match ft2 with
1388
          | TRUE -> TRUE
1389
          | _ ->
1390
            if (f1 == ft1) && (f2 == ft2) then f
1391
            else NORM (ft1, ft2)
1392
      end
1393
  | NORMN (f1, f2) ->
1394
      let ft1 = simplify f1 in
1395
      let ft2 = simplify f2 in
1396
      begin
1397
        match ft2 with
1398
          | FALSE -> FALSE
1399
          | _ ->
1400
            if (f1 == ft1) && (f2 == ft2) then f
1401
            else NORMN (ft1, ft2)
1402
      end
1403
  | CHC (f1, f2) ->
1404
      let ft1 = simplify f1 in
1405
      let ft2 = simplify f2 in
1406
      begin
1407
        match ft1, ft2 with
1408
        | TRUE, TRUE -> TRUE
1409
        | FALSE, FALSE -> FALSE
1410
        | _, _ ->
1411
            if (f1 == ft1) && (f2 == ft2) then f
1412
            else CHC (ft1, ft2)
1413
      end
1414
  | FUS (first, f1) ->
1415
      let ft = simplify f1 in
1416
      begin
1417
        match ft with
1418
        | FALSE -> FALSE
1419
        | TRUE -> TRUE
1420
        | _ -> if ft == f1 then f else FUS (first, ft)
1421
      end
1422
  | MU (s, f1) ->
1423
      let ft = simplify f1 in
1424
      begin
1425
        match ft with
1426
        | TRUE -> TRUE
1427
        | _ -> if ft == f1 then f else MU (s, ft)
1428
      end
1429
  | NU (s, f1) ->
1430
      let ft = simplify f1 in
1431
      begin
1432
        match ft with
1433
        | TRUE -> TRUE
1434
        | _ -> if ft == f1 then f else NU (s, ft)
1435
      end
1436
  | AF _
1437
  | EF _
1438
  | AG _
1439
  | EG _
1440
  | AU _
1441
  | EU _ ->
1442
     raise (CoAlgException ("nnf: CTL should have been removed at this point"))
1443

    
1444
(** Destructs an atomic proposition.
1445
    @param f An atomic proposition.
1446
    @return The name of the atomic proposition.
1447
    @raise CoAlgException if f is not an atomic proposition.
1448
 *)
1449
let dest_ap f =
1450
  match f with
1451
  | AP s when not (isNominal s) -> s
1452
  | _ -> raise (CoAlgException "Formula is not an atomic proposition.")
1453

    
1454
(** Destructs a nominal.
1455
    @param f A nominal.
1456
    @return The name of the nominal
1457
    @raise CoAlgException if f is not a nominal.
1458
 *)
1459
let dest_nom f =
1460
  match f with
1461
  | AP s when isNominal s -> s
1462
  | _ -> raise (CoAlgException "Formula is not a nominal.")
1463

    
1464
(** Destructs a negation.
1465
    @param f A negation.
1466
    @return The immediate subformula of the negation.
1467
    @raise CoAlgException if f is not a negation.
1468
 *)
1469
let dest_not f =
1470
  match f with
1471
  | NOT f1 -> f1
1472
  | _ -> raise (CoAlgException "Formula is not a negation.")
1473

    
1474
(** Destructs an @-formula.
1475
    @param f An @-formula.
1476
    @return The name of the nominal and the immediate subformula of the @-formula.
1477
    @raise CoAlgException if f is not an @-formula.
1478
 *)
1479
let dest_at f =
1480
  match f with
1481
  | AT (s, f1) -> (s, f1)
1482
  | _ -> raise (CoAlgException "Formula is not an @-formula.")
1483

    
1484
(** Destructs an or-formula.
1485
    @param f An or-formula.
1486
    @return The two immediate subformulae of the or-formula.
1487
    @raise CoAlgException if f is not an or-formula.
1488
 *)
1489
let dest_or f =
1490
  match f with
1491
  | OR (f1, f2) -> (f1, f2)
1492
  | _ -> raise (CoAlgException "Formula is not an or-formula.")
1493

    
1494
(** Destructs an and-formula.
1495
    @param f An and-formula.
1496
    @return The two immediate subformulae of the and-formula.
1497
    @raise CoAlgException if f is not an and-formula.
1498
 *)
1499
let dest_and f =
1500
  match f with
1501
  | AND (f1, f2) -> (f1, f2)
1502
  | _ -> raise (CoAlgException "Formula is not an and-formula.")
1503

    
1504
(** Destructs an equivalence.
1505
    @param f An equivalence.
1506
    @return The two immediate subformulae of the equivalence.
1507
    @raise CoAlgException if f is not an equivalence.
1508
 *)
1509
let dest_equ f =
1510
  match f with
1511
  | EQU (f1, f2) -> (f1, f2)
1512
  | _ -> raise (CoAlgException "Formula is not an equivalence.")
1513

    
1514
(** Destructs an implication.
1515
    @param f An implication.
1516
    @return The two immediate subformulae of the implication.
1517
    @raise CoAlgException if f is not an implication.
1518
 *)
1519
let dest_imp f =
1520
  match f with
1521
  | IMP (f1, f2) -> (f1, f2)
1522
  | _ -> raise (CoAlgException "Formula is not an implication.")
1523

    
1524
(** Destructs an EX-formula.
1525
    @param f An EX-formula.
1526
    @return The role name and the immediate subformula of the EX-formula.
1527
    @raise CoAlgException if f is not an EX-formula.
1528
 *)
1529
let dest_ex f =
1530
  match f with
1531
  | EX (s, f1) -> (s, f1)
1532
  | _ -> raise (CoAlgException "Formula is not an EX-formula.")
1533

    
1534
(** Destructs an AX-formula.
1535
    @param f An AX-formula.
1536
    @return The role name and the immediate subformula of the AX-formula.
1537
    @raise CoAlgException if f is not an AX-formula.
1538
 *)
1539
let dest_ax f =
1540
  match f with
1541
  | AX (s, f1) -> (s, f1)
1542
  | _ -> raise (CoAlgException "Formula is not an AX-formula.")
1543

    
1544
(** Destructs a MIN-formula.
1545
    @param f A MIN-formula.
1546
    @return The number restriction, role name,
1547
    and the immediate subformula of the MIN-formula.
1548
    @raise CoAlgException if f is not a MIN-formula.
1549
 *)
1550
let dest_min f =
1551
  match f with
1552
  | MIN (n, s, f1) -> (n, s, f1)
1553
  | _ -> raise (CoAlgException "Formula is not a MIN-formula.")
1554

    
1555
(** Destructs a MAX-formula.
1556
    @param f A MAX-formula.
1557
    @return The number restriction, role name,
1558
    and the immediate subformula of the MAX-formula.
1559
    @raise CoAlgException if f is not a MAX-formula.
1560
 *)
1561
let dest_max f =
1562
  match f with
1563
  | MAX (n, s, f1) -> (n, s, f1)
1564
  | _ -> raise (CoAlgException "Formula is not a MAX-formula.")
1565

    
1566
(** Destructs a choice formula.
1567
    @param f A choice formula.
1568
    @return The two immediate subformulae of the choice formula.
1569
    @raise CoAlgException if f is not a choice formula.
1570
 *)
1571
let dest_choice f =
1572
  match f with
1573
  | CHC (f1, f2) -> (f1, f2)
1574
  | _ -> raise (CoAlgException "Formula is not a choice formula.")
1575

    
1576
(** Destructs a fusion formula.
1577
    @param f A fusion formula.
1578
    @return A pair (first, f1) where
1579
    first is true iff f is a first projection; and
1580
    f1 is the immediate subformulae of f.
1581
    @raise CoAlgException if f is not a fusion formula.
1582
 *)
1583
let dest_fusion f =
1584
  match f with
1585
  | FUS (first, f1) -> (first, f1)
1586
  | _ -> raise (CoAlgException "Formula is not a fusion formula.")
1587

    
1588

    
1589
(** Tests whether a formula is the constant True.
1590
    @param f A formula.
1591
    @return True iff f is the constant True.
1592
 *)
1593
let is_true f =
1594
  match f with
1595
  | TRUE -> true
1596
  | _ -> false
1597

    
1598
(** Tests whether a formula is the constant False.
1599
    @param f A formula.
1600
    @return True iff f is the constant False.
1601
 *)
1602
let is_false f =
1603
  match f with
1604
  | FALSE -> true
1605
  | _ -> false
1606

    
1607
(** Tests whether a formula is an atomic proposition.
1608
    @param f A formula.
1609
    @return True iff f is an atomic proposition.
1610
 *)
1611
let is_ap f =
1612
  match f with
1613
  | AP s when not (isNominal s) -> true
1614
  | _ -> false
1615

    
1616
(** Tests whether a formula is a nominal.
1617
    @param f A formula.
1618
    @return True iff f is a nominal.
1619
 *)
1620
let is_nom f =
1621
  match f with
1622
  | AP s when isNominal s -> true
1623
  | _ -> false
1624

    
1625
(** Tests whether a formula is a negation.
1626
    @param f A formula.
1627
    @return True iff f is a negation.
1628
 *)
1629
let is_not f =
1630
  match f with
1631
  | NOT _ -> true
1632
  | _ -> false
1633

    
1634
(** Tests whether a formula is an @-formula.
1635
    @param f A formula.
1636
    @return True iff f is an @-formula.
1637
 *)
1638
let is_at f =
1639
  match f with
1640
  | AT _ -> true
1641
  | _ -> false
1642

    
1643
(** Tests whether a formula is an or-formula.
1644
    @param f A formula.
1645
    @return True iff f is an or-formula.
1646
 *)
1647
let is_or f =
1648
  match f with
1649
  | OR _ -> true
1650
  | _ -> false
1651

    
1652
(** Tests whether a formula is an and-formula.
1653
    @param f A formula.
1654
    @return True iff f is an and-formula.
1655
 *)
1656
let is_and f =
1657
  match f with
1658
  | AND _ -> true
1659
  | _ -> false
1660

    
1661
(** Tests whether a formula is an equivalence.
1662
    @param f A formula.
1663
    @return True iff f is an equivalence.
1664
 *)
1665
let is_equ f =
1666
  match f with
1667
  | EQU _ -> true
1668
  | _ -> false
1669

    
1670
(** Tests whether a formula is an implication.
1671
    @param f A formula.
1672
    @return True iff f is an implication.
1673
 *)
1674
let is_imp f =
1675
  match f with
1676
  | IMP _ -> true
1677
  | _ -> false
1678

    
1679
(** Tests whether a formula is an EX-formula.
1680
    @param f A formula.
1681
    @return True iff f is an EX-formula.
1682
 *)
1683
let is_ex f =
1684
  match f with
1685
  | EX _ -> true
1686
  | _ -> false
1687

    
1688
(** Tests whether a formula is an AX-formula.
1689
    @param f A formula.
1690
    @return True iff f is an AX-formula.
1691
 *)
1692
let is_ax f =
1693
  match f with
1694
  | AX _ -> true
1695
  | _ -> false
1696

    
1697
(** Tests whether a formula is a MIN-formula.
1698
    @param f A formula.
1699
    @return True iff f is a MIN-formula.
1700
 *)
1701
let is_min f =
1702
  match f with
1703
  | MIN _ -> true
1704
  | _ -> false
1705

    
1706
(** Tests whether a formula is a MAX-formula.
1707
    @param f A formula.
1708
    @return True iff f is a MAX-formula.
1709
 *)
1710
let is_max f =
1711
  match f with
1712
  | MAX _ -> true
1713
  | _ -> false
1714

    
1715
(** Tests whether a formula is a choice formula.
1716
    @param f A formula.
1717
    @return True iff f is a choice formula.
1718
 *)
1719
let is_choice f =
1720
  match f with
1721
  | CHC _ -> true
1722
  | _ -> false
1723

    
1724
(** Tests whether a formula is a fusion formula.
1725
    @param f A formula.
1726
    @return True iff f is a fusion formula.
1727
 *)
1728
let is_fusion f =
1729
  match f with
1730
  | FUS _ -> true
1731
  | _ -> false
1732

    
1733

    
1734
(** The constant True.
1735
 *)
1736
let const_true = TRUE
1737

    
1738
(** The constant False.
1739
 *)
1740
let const_false = FALSE
1741

    
1742
(** Constructs an atomic proposition.
1743
    @param s The name of the atomic proposition.
1744
    @return The atomic proposition with name s.
1745
    @raise CoAlgException if s is a nominal name.
1746
 *)
1747
let const_ap s =
1748
  if isNominal s then raise (CoAlgException "The name indicates a nominal.")
1749
  else AP s
1750

    
1751
(** Constructs a nominal.
1752
    @param s The name of the nominal.
1753
    @return A nominal with name s.
1754
    @raise CoAlgException if s is not a nominal name.
1755
 *)
1756
let const_nom s =
1757
  if isNominal s then AP s
1758
  else raise (CoAlgException "The name does not indicate a nominal.")
1759

    
1760
(** Negates a formula.
1761
    @param f A formula.
1762
    @return The negation of f.
1763
 *)
1764
let const_not f = NOT f
1765

    
1766
(** Constructs an @-formula from a name and a formula.
1767
    @param s A nominal name.
1768
    @param f A formula.
1769
    @return The formula AT (s, f).
1770
 *)
1771
let const_at s f = AT (s, f)
1772

    
1773
(** Constructs an or-formula from two formulae.
1774
    @param f1 The first formula (LHS).
1775
    @param f2 The second formula (LHS).
1776
    @return The formula f1 | f2.
1777
 *)
1778
let const_or f1 f2 = OR (f1, f2)
1779

    
1780
(** Constructs an and-formula from two formulae.
1781
    @param f1 The first formula (LHS).
1782
    @param f2 The second formula (LHS).
1783
    @return The formula f1 & f2.
1784
 *)
1785
let const_and f1 f2 = AND (f1, f2)
1786

    
1787
(** Constructs an equivalence from two formulae.
1788
    @param f1 The first formula (LHS).
1789
    @param f2 The second formula (LHS).
1790
    @return The equivalence f1 <=> f2.
1791
 *)
1792
let const_equ f1 f2 = EQU (f1, f2)
1793

    
1794
(** Constructs an implication from two formulae.
1795
    @param f1 The first formula (LHS).
1796
    @param f2 The second formula (LHS).
1797
    @return The implication f1 => f2.
1798
 *)
1799
let const_imp f1 f2 = IMP (f1, f2)
1800

    
1801
(** Constructs an EX-formula from a formula.
1802
    @param s A role name.
1803
    @param f A formula.
1804
    @return The formula EX (s, f).
1805
 *)
1806
let const_ex s f = EX (s, f)
1807

    
1808
(** Constructs an AX-formula from a formula.
1809
    @param s A role name.
1810
    @param f A formula.
1811
    @return The formula AX (s, f).
1812
 *)
1813
let const_ax s f = AX (s, f)
1814

    
1815
(** Constructs a MIN-formula from a formula.
1816
    @param n A non-negative integer.
1817
    @param s A role name.
1818
    @param f A formula.
1819
    @return The formula MIN f.
1820
    @raise CoAlgException Iff n is negative.
1821
 *)
1822
let const_min n s f =
1823
  if n < 0 then raise (CoAlgException "Negative cardinality constraint.")
1824
  else MIN (n, s, f)
1825

    
1826
(** Constructs a MAX-formula from a formula.
1827
    @param n A non-negative integer.
1828
    @param s A role name.
1829
    @param f A formula.
1830
    @return The formula MAX f.
1831
    @raise CoAlgException Iff n is negative.
1832
 *)
1833
let const_max n s f =
1834
  if n < 0 then raise (CoAlgException "Negative cardinality constraint.")
1835
  else MAX (n, s, f)
1836

    
1837
let const_enforces p f =
1838
    ENFORCES (p,f)
1839

    
1840
let const_allows p f =
1841
    ALLOWS (p,f)
1842

    
1843
(** Constructs a choice formula from two formulae.
1844
    @param f1 The first formula (LHS).
1845
    @param f2 The second formula (LHS).
1846
    @return The formula (f1 + f2).
1847
 *)
1848
let const_choice f1 f2 = CHC (f1, f2)
1849

    
1850
(** Constructs a fusion formula.
1851
    @param first True iff the result is a first projection.
1852
    @param f1 A formula.
1853
    @return The formula [pi1] f1 or [pi2] f1 (depending on first).
1854
 *)
1855
let const_fusion first f1 = FUS (first, f1)
1856

    
1857

    
1858
(** Hash-consed formulae, which are in negation normal form,
1859
    such that structural and physical equality coincide.
1860

    
1861
    Also CTL has been replaced by the equivalent μ-Calculus
1862
    constructs
1863
 *)
1864
type hcFormula = (hcFormula_node, formula) HC.hash_consed
1865
and hcFormula_node =
1866
  | HCTRUE
1867
  | HCFALSE
1868
  | HCAP of string
1869
  | HCNOT of string
1870
  | HCAT of string * hcFormula
1871
  | HCOR of hcFormula * hcFormula
1872
  | HCAND of hcFormula * hcFormula
1873
  | HCEX of string * hcFormula
1874
  | HCAX of string * hcFormula
1875
  | HCENFORCES of int list * hcFormula
1876
  | HCALLOWS of int list * hcFormula
1877
  | HCMORETHAN of int * string * hcFormula (* GML Diamond *)
1878
  | HCMAXEXCEPT of int * string * hcFormula (* GML Box *)
1879
  | HCATLEASTPROB of rational * hcFormula
1880
  | HCLESSPROBFAIL of rational * hcFormula
1881
  | HCCONST of string
1882
  | HCCONSTN of string
1883
  | HCID of hcFormula
1884
  | HCNORM of hcFormula * hcFormula
1885
  | HCNORMN of hcFormula * hcFormula
1886
  | HCCHC of hcFormula * hcFormula
1887
  | HCFUS of bool * hcFormula
1888
  | HCMU of string * hcFormula
1889
  | HCNU of string * hcFormula
1890
  | HCVAR of string
1891

    
1892
(** Determines whether two formula nodes are structurally equal.
1893
    @param f1 The first formula node.
1894
    @param f2 The second formula node.
1895
    @return True iff f1 and f2 are structurally equal.
1896
 *)
1897
let equal_hcFormula_node f1 f2 =
1898
  match f1, f2 with
1899
  | HCTRUE, HCTRUE -> true
1900
  | HCFALSE, HCFALSE -> true
1901
  | HCCONST s1, HCCONST s2
1902
  | HCCONSTN s1, HCCONSTN s2
1903
  | HCAP s1, HCAP s2
1904
  | HCNOT s1, HCNOT s2 -> compare s1 s2 = 0
1905
  | HCAT (s1, f1), HCAT (s2, f2) -> compare s1 s2 = 0 && f1 == f2
1906
  | HCOR (f1a, f1b), HCOR (f2a, f2b)
1907
  | HCAND (f1a, f1b), HCAND (f2a, f2b) -> f1a == f2a && f1b == f2b
1908
  | HCEX (s1, f1), HCEX (s2, f2)
1909
  | HCAX (s1, f1), HCAX (s2, f2) -> compare s1 s2 = 0 && f1 == f2
1910
  | HCENFORCES (s1, f1), HCENFORCES (s2, f2)
1911
  | HCALLOWS (s1, f1), HCALLOWS (s2, f2) -> compare s1 s2 = 0 && f1 == f2
1912
  | HCMORETHAN (n1, s1, f1), HCMORETHAN (n2, s2, f2)
1913
  | HCMAXEXCEPT (n1, s1, f1), HCMAXEXCEPT (n2, s2, f2) ->
1914
      n1 = n2 && compare s1 s2 = 0 && f1 == f2
1915
  | HCATLEASTPROB (p1, f1), HCATLEASTPROB (p2,f2) ->
1916
      p1 = p2 && f1 == f2
1917
  | HCLESSPROBFAIL (p1, f1), HCLESSPROBFAIL (p2,f2) ->
1918
      p1 = p2 && f1 == f2
1919
  | HCID f1, HCID f2 -> f1 == f2
1920
  | HCNORM (f1a, f1b), HCNORMN (f2a, f2b) -> f1a == f2a && f1b == f2b
1921
  | HCCHC (f1a, f1b), HCCHC (f2a, f2b) -> f1a == f2a && f1b == f2b
1922
  | HCFUS (first1, f1), HCFUS (first2, f2) -> first1 = first2 && f1 == f2
1923
  | HCMU (name1, f1), HCMU(name2, f2) -> compare name1 name2 = 0 && f1 == f2
1924
  | HCNU (name1, f1), HCNU(name2, f2) -> compare name1 name2 = 0 && f1 == f2
1925
  | HCVAR name1, HCVAR name2 -> compare name1 name2 = 0
1926
(* The rest could be shortened to | _ -> false,
1927
   but then the compiler would not warn if the formula type is extended
1928
   and this function is not updated accordingly.*)
1929
  | HCTRUE, _
1930
  | HCFALSE, _
1931
  | HCAP _, _
1932
  | HCNOT _, _
1933
  | HCAT _, _
1934
  | HCOR _, _
1935
  | HCAND _, _
1936
  | HCEX _, _
1937
  | HCAX _, _
1938
  | HCENFORCES _, _
1939
  | HCALLOWS   _, _
1940
  | HCMORETHAN _, _
1941
  | HCMAXEXCEPT _, _
1942
  | HCATLEASTPROB _, _
1943
  | HCLESSPROBFAIL _, _
1944
  | HCCONST _, _
1945
  | HCCONSTN _, _
1946
  | HCID _, _
1947
  | HCNORM _, _
1948
  | HCNORMN _, _
1949
  | HCCHC _, _
1950
  | HCFUS _, _
1951
  | HCMU _, _
1952
  | HCNU _, _
1953
  | HCVAR _, _ -> false
1954

    
1955
(** Computes the hash value of a formula node.
1956
    @param f A formula node.
1957
    @return The hash value of f.
1958
 *)
1959
let hash_hcFormula_node f =
1960
  let base = 23 in (* should be larger than the no of constructors *)
1961
  match f with
1962
  | HCTRUE -> 0
1963
  | HCFALSE -> 1
1964
  | HCAP s
1965
  | HCNOT s
1966
  | HCVAR s -> base * Hashtbl.hash s + 1
1967
  | HCAT (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 2
1968
  | HCOR (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 5
1969
  | HCAND (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 6
1970
  | HCEX (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 3
1971
  | HCAX (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 4
1972
  | HCMORETHAN (n, s, f1) -> base * (base * (base * (Hashtbl.hash s) + n) + f1.HC.hkey) + 7
1973
  | HCMAXEXCEPT (n, s, f1) -> base * (base * (base * (Hashtbl.hash s) + n) + f1.HC.hkey) + 8
1974
  | HCATLEASTPROB (p,f1) -> base * (base * (base * p.nominator + p.denominator) + f1.HC.hkey) + 9
1975
  | HCLESSPROBFAIL (p,f1) -> base * (base * (base * p.nominator + p.denominator) + f1.HC.hkey) + 10
1976
  | HCCHC (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 11
1977
  | HCFUS (first, f1) -> base * (base * (Hashtbl.hash first) + f1.HC.hkey) + 13
1978
  | HCENFORCES (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 14
1979
  | HCALLOWS   (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 15
1980
  | HCCONST s -> Hashtbl.hash s + 16
1981
  | HCCONSTN s -> Hashtbl.hash s + 17
1982
  | HCNORM (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 18
1983
  | HCNORMN (f1, f2) -> base * (base * f1.HC.hkey + f2.HC.hkey) + 19
1984
  | HCID (f1) -> base * f1.HC.hkey + 20
1985
  | HCMU (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 21
1986
  | HCNU (s, f1) -> base * (base * (Hashtbl.hash s) + f1.HC.hkey) + 22
1987

    
1988
(** Determines the "real" formula of a formula node.
1989
    @param f A formula node.
1990
    @return The formula (in negation normal form) which corresponds to f.
1991
 *)
1992
let toFml_hcFormula_node f =
1993
  match f with
1994
  | HCTRUE -> TRUE
1995
  | HCFALSE -> FALSE
1996
  | HCAP s -> AP s
1997
  | HCVAR s -> VAR s
1998
  | HCNOT s -> NOT (AP s)
1999
  | HCAT (s, f1) -> AT (s, f1.HC.fml)
2000
  | HCOR (f1, f2) -> OR (f1.HC.fml, f2.HC.fml)
2001
  | HCAND (f1, f2) -> AND (f1.HC.fml, f2.HC.fml)
2002
  | HCEX (s, f1) -> EX (s, f1.HC.fml)
2003
  | HCAX (s, f1) -> AX (s, f1.HC.fml)
2004
  | HCENFORCES (s, f1) -> ENFORCES (s, f1.HC.fml)
2005
  | HCALLOWS (s, f1) -> ALLOWS (s, f1.HC.fml)
2006
  | HCMORETHAN (n, s, f1) -> MORETHAN (n, s, f1.HC.fml)
2007
  | HCMAXEXCEPT (n, s, f1) -> MAXEXCEPT (n, s, f1.HC.fml)
2008
  | HCATLEASTPROB (p, f1) -> ATLEASTPROB (p, f1.HC.fml)
2009
  | HCLESSPROBFAIL (p, f1) -> LESSPROBFAIL (p, f1.HC.fml)
2010
  | HCCONST s -> CONST s
2011
  | HCCONSTN s -> CONSTN s
2012
  | HCID (f1) -> ID(f1.HC.fml)
2013
  | HCNORM (f1, f2) -> NORM(f1.HC.fml, f2.HC.fml)
2014
  | HCNORMN (f1, f2) -> NORMN(f1.HC.fml, f2.HC.fml)
2015
  | HCCHC (f1, f2) -> CHC (f1.HC.fml, f2.HC.fml)
2016
  | HCFUS (first, f1) -> FUS (first, f1.HC.fml)
2017
  | HCMU (var, f1) -> MU (var, f1.HC.fml)
2018
  | HCNU (var, f1) -> NU (var, f1.HC.fml)
2019

    
2020
(** Determines the negation (in negation normal form) of a formula node.
2021
    @param f A formula node.
2022
    @return The negation (in negation normal form) of f.
2023
 *)
2024
let negNde_hcFormula_node f =
2025
  match f with
2026
  | HCTRUE -> HCFALSE
2027
  | HCFALSE -> HCTRUE
2028
  | HCAP s -> HCNOT s
2029
  | HCNOT s -> HCAP s
2030
  | HCVAR s -> f
2031
  | HCAT (s, f1) -> HCAT (s, f1.HC.neg)
2032
  | HCOR (f1, f2) -> HCAND (f1.HC.neg, f2.HC.neg)
2033
  | HCAND (f1, f2) -> HCOR (f1.HC.neg, f2.HC.neg)
2034
  | HCEX (s, f2) -> HCAX (s, f2.HC.neg)
2035
  | HCAX (s, f2) -> HCEX (s, f2.HC.neg)
2036
  | HCENFORCES (s, f2) -> HCALLOWS (s, f2.HC.neg)
2037
  | HCALLOWS (s, f2) -> HCENFORCES (s, f2.HC.neg)
2038
  | HCMORETHAN (n, s, f1) -> HCMAXEXCEPT (n, s, f1.HC.neg)
2039
  | HCMAXEXCEPT (n, s, f1) -> HCMORETHAN (n, s, f1.HC.neg)
2040
  | HCATLEASTPROB (p, f1) -> HCLESSPROBFAIL (p, f1.HC.neg)
2041
  | HCLESSPROBFAIL (p, f1) -> HCATLEASTPROB (p, f1.HC.neg)
2042
  | HCCONST s -> HCCONSTN s
2043
  | HCCONSTN s -> HCCONST s
2044
  | HCID (f1) -> HCID(f1.HC.neg)
2045
  | HCNORM (f1, f2) -> HCNORMN(f1.HC.neg, f2.HC.neg)
2046
  | HCNORMN (f1, f2) -> HCNORM(f1.HC.neg, f2.HC.neg)
2047
  | HCCHC (f1, f2) -> HCCHC (f1.HC.neg, f2.HC.neg)
2048
  | HCFUS (first, f1) -> HCFUS (first, f1.HC.neg)
2049
  | HCMU (name, f1) -> HCNU (name, f1.HC.neg)
2050
  | HCNU (name, f1) -> HCMU (name, f1.HC.neg)
2051

    
2052
(** An instantiation of hash-consing for formulae.
2053
 *)
2054
module HcFormula = HC.Make(
2055
  struct
2056
    type nde = hcFormula_node
2057
    type fml = formula
2058
    let equal (n1 : nde) n2 = equal_hcFormula_node n1 n2
2059
    let hash (n : nde) = hash_hcFormula_node n
2060
    let negNde (n : nde) = negNde_hcFormula_node n
2061
    let toFml (n : nde) = toFml_hcFormula_node n
2062
  end
2063
 )
2064

    
2065
(** Converts a formula into its hash-consed version.
2066
    @param hcF A hash-cons table for formulae.
2067
    @param f A formula in negation normal form.
2068
    @return The hash-consed version of f.
2069
    @raise CoAlgException if f is not in negation normal form.
2070
*)
2071
let rec hc_formula hcF f =
2072
  match f with
2073
  | TRUE -> HcFormula.hashcons hcF HCTRUE
2074
  | FALSE -> HcFormula.hashcons hcF HCFALSE
2075
  | AP s -> HcFormula.hashcons hcF (HCAP s)
2076
  | VAR s -> HcFormula.hashcons hcF (HCVAR s)
2077
  | NOT (AP s) -> HcFormula.hashcons hcF (HCNOT s)
2078
  | AT (s, f1) ->
2079
      let tf1 = hc_formula hcF f1 in
2080
      HcFormula.hashcons hcF (HCAT (s, tf1))
2081
  | OR (f1, f2) ->
2082
      let tf1 = hc_formula hcF f1 in
2083
      let tf2 = hc_formula hcF f2 in
2084
      HcFormula.hashcons hcF (HCOR (tf1, tf2))
2085
  | AND (f1, f2) ->
2086
      let tf1 = hc_formula hcF f1 in
2087
      let tf2 = hc_formula hcF f2 in
2088
      HcFormula.hashcons hcF (HCAND (tf1, tf2))
2089
  | NOT _
2090
  | EQU _
2091
  | MIN _
2092
  | MAX _
2093
  | IMP _ -> raise (CoAlgException "Formula is not in negation normal form.")
2094
  | EX (s, f1) ->
2095
      let tf1 = hc_formula hcF f1 in
2096
      HcFormula.hashcons hcF (HCEX (s, tf1))
2097
  | AX (s, f1) ->
2098
      let tf1 = hc_formula hcF f1 in
2099
      HcFormula.hashcons hcF (HCAX (s, tf1))
2100
  | ENFORCES (s, f1) ->
2101
      let tf1 = hc_formula hcF f1 in
2102
      HcFormula.hashcons hcF (HCENFORCES (s, tf1))
2103
  | ALLOWS (s, f1) ->
2104
      let tf1 = hc_formula hcF f1 in
2105
      HcFormula.hashcons hcF (HCALLOWS (s, tf1))
2106
  | MORETHAN  (n, s, f1) ->
2107
      let tf1 = hc_formula hcF f1 in
2108
      HcFormula.hashcons hcF (HCMORETHAN (n, s, tf1))
2109
  | MAXEXCEPT  (n, s, f1) ->
2110
      let tf1 = hc_formula hcF f1 in
2111
      HcFormula.hashcons hcF (HCMAXEXCEPT (n, s, tf1))
2112
  | ATLEASTPROB (p, f1) ->
2113
      HcFormula.hashcons hcF (HCATLEASTPROB (p, hc_formula hcF f1))
2114
  | LESSPROBFAIL (p, f1) ->
2115
      HcFormula.hashcons hcF (HCLESSPROBFAIL (p, hc_formula hcF f1))
2116
  | CONST s ->
2117
      HcFormula.hashcons hcF (HCCONST s)
2118
  | CONSTN s ->
2119
      HcFormula.hashcons hcF (HCCONSTN s)
2120
  | ID f1 ->
2121
    let tf1 = hc_formula hcF f1 in
2122
      HcFormula.hashcons hcF (HCID tf1)
2123
  | NORM (f1, f2) ->
2124
      let tf1 = hc_formula hcF f1 in
2125
      let tf2 = hc_formula hcF f2 in
2126
      HcFormula.hashcons hcF (HCNORM (tf1, tf2))
2127
  | NORMN (f1, f2) ->
2128
      let tf1 = hc_formula hcF f1 in
2129
      let tf2 = hc_formula hcF f2 in
2130
      HcFormula.hashcons hcF (HCNORMN (tf1, tf2))
2131
  | CHC (f1, f2) ->
2132
      let tf1 = hc_formula hcF f1 in
2133
      let tf2 = hc_formula hcF f2 in
2134
      HcFormula.hashcons hcF (HCCHC (tf1, tf2))
2135
  | FUS (first, f1) ->
2136
      let tf1 = hc_formula hcF f1 in
2137
      HcFormula.hashcons hcF (HCFUS (first, tf1))
2138
  | MU (var, f1) ->
2139
     let tf1 = hc_formula hcF f1 in
2140
     HcFormula.hashcons hcF (HCMU (var, tf1))
2141
  | NU (var, f1) ->
2142
     let tf1 = hc_formula hcF f1 in
2143
     HcFormula.hashcons hcF (HCNU (var, tf1))
2144
  | AF _
2145
  | EF _
2146
  | AG _
2147
  | EG _
2148
  | AU _
2149
  | EU _ ->
2150
     raise (CoAlgException ("nnf: CTL should have been removed at this point"))
2151

    
2152
(* Replace the Variable name in f with formula formula
2153
   hc_replace foo φ ψ => ψ[foo |-> φ]
2154
 *)
2155
let rec hc_replace hcF name (formula: hcFormula) (f: hcFormula) =
2156
  let func = hc_replace hcF name formula in
2157
  let gennew = HcFormula.hashcons hcF in
2158
  match f.HC.node with
2159
  | HCTRUE
2160
  | HCFALSE
2161
  | HCAP _
2162
  | HCNOT _
2163
  | HCCONST _
2164
  | HCCONSTN _ -> f
2165
  | HCVAR s ->
2166
     if compare s name == 0
2167
     then formula
2168
     else f
2169
  | HCAT (s, f1) ->
2170
     let nf1 = func f1 in
2171
     if nf1 == f1 then f else gennew (HCAT(s, nf1))
2172
  | HCOR (f1, f2) ->
2173
     let nf1 = func f1 in
2174
     let nf2 = func f2 in
2175
     if nf1 == f1 && nf2 == f2 then f else gennew (HCOR(nf1, nf2))
2176
  | HCAND (f1, f2) ->
2177
     let nf1 = func f1 in
2178
     let nf2 = func f2 in
2179
     if nf1 == f1 && nf2 == f2 then f else gennew (HCAND(nf1, nf2))
2180
  | HCEX (s, f1) ->
2181
     let nf1 = func f1 in
2182
     if nf1 == f1 then f else gennew (HCEX(s, nf1))
2183
  | HCAX (s, f1) ->
2184
     let nf1 = func f1 in
2185
     if nf1 == f1 then f else gennew (HCAX(s, nf1))
2186
  | HCENFORCES (s, f1) ->
2187
     let nf1 = func f1 in
2188
     if nf1 == f1 then f else gennew (HCENFORCES(s, nf1))
2189
  | HCALLOWS (s, f1) ->
2190
     let nf1 = func f1 in
2191
     if nf1 == f1 then f else gennew (HCALLOWS(s, nf1))
2192
  | HCMORETHAN  (n, s, f1) ->
2193
     let nf1 = func f1 in
2194
     if nf1 == f1 then f else gennew (HCMORETHAN(n, s, nf1))
2195
  | HCMAXEXCEPT  (n, s, f1) ->
2196
     let nf1 = func f1 in
2197
     if nf1 == f1 then f else gennew (HCMAXEXCEPT(n, s, nf1))
2198
  | HCATLEASTPROB (p, f1) ->
2199
     let nf1 = func f1 in
2200
     if nf1 == f1 then f else gennew (HCATLEASTPROB(p, nf1))
2201
  | HCLESSPROBFAIL (p, f1) ->
2202
     let nf1 = func f1 in
2203
     if nf1 == f1 then f else gennew (HCLESSPROBFAIL(p, nf1))
2204
  | HCID f1 ->
2205
     let nf1 = func f1 in
2206
     if nf1 == f1 then f else gennew (HCID(nf1))
2207
  | HCNORM (f1, f2) ->
2208
     let nf1 = func f1 in
2209
     let nf2 = func f2 in
2210
     if nf1 == f1 && nf2 == f2 then f else gennew (HCNORM(nf1, nf2))
2211
  | HCNORMN (f1, f2) ->
2212
     let nf1 = func f1 in
2213
     let nf2 = func f2 in
2214
     if nf1 == f1 && nf2 == f2 then f else gennew (HCNORMN(nf1, nf2))
2215
  | HCCHC (f1, f2) ->
2216
     let nf1 = func f1 in
2217
     let nf2 = func f2 in
2218
     if nf1 == f1 && nf2 == f2 then f else gennew (HCCHC(nf1, nf2))
2219
  | HCFUS (first, f1) ->
2220
     let nf1 = func f1 in
2221
     if nf1 == f1 then f else gennew (HCFUS(first, nf1))
2222
  | HCMU (var, f1) ->
2223
     if compare var name != 0 then
2224
       let nf1 = func f1 in
2225
       if nf1 == f1 then f else gennew (HCMU(var, nf1))
2226
     else
2227
       f
2228
  | HCNU (var, f1) ->
2229
     if compare var name != 0 then
2230
       let nf1 = func f1 in
2231
       if nf1 == f1 then f else gennew (HCNU(var, nf1))
2232
     else
2233
       f
2234

    
2235
let rec hc_freeIn variable (f: hcFormula) =
2236
  match f.HC.node with
2237
  | HCTRUE
2238
  | HCFALSE
2239
  | HCAP _
2240
  | HCNOT _
2241
  | HCCONST _
2242
  | HCCONSTN _ -> false
2243
  | HCVAR s ->
2244
     if compare variable s == 0
2245
     then true
2246
     else false
2247
  | HCAT (s, f1) ->
2248
     hc_freeIn variable f1
2249
  | HCOR (f1, f2)
2250
  | HCAND (f1, f2) ->
2251
     hc_freeIn variable f1 || hc_freeIn variable f2
2252
  | HCEX (_, f1)
2253
  | HCAX (_, f1)
2254
  | HCENFORCES (_, f1)
2255
  | HCALLOWS (_, f1)
2256
  | HCMORETHAN  (_, _, f1)
2257
  | HCMAXEXCEPT  (_, _, f1)
2258
  | HCATLEASTPROB (_, f1)
2259
  | HCLESSPROBFAIL (_, f1)
2260
  | HCID f1 ->
2261
     hc_freeIn variable f1
2262
  | HCNORM (f1, f2)
2263
  | HCNORMN (f1, f2)
2264
  | HCCHC (f1, f2) ->
2265
     hc_freeIn variable f1 || hc_freeIn variable f2
2266
  | HCFUS (first, f1) ->
2267
     hc_freeIn variable f1
2268
  | HCMU (var, f1)
2269
  | HCNU (var, f1) ->
2270
     (* Do we need to exclude bound variables here? *)
2271
     hc_freeIn variable f1
2272

    
2273

    
2274
(** An instantiation of a hash table (of the standard library)
2275
    for hash-consed formulae. The test for equality
2276
    and computing the hash value is done in constant time.
2277
 *)
2278
module HcFHt = Hashtbl.Make(
2279
  struct
2280
    type t = hcFormula
2281
    let equal (f1 : t) f2 = f1.HC.tag = f2.HC.tag
2282
    let hash (f : t) = f.HC.tag
2283
  end
2284
 )