Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / EAFormula.ml @ 966e1556

History | View | Annotate | Download (2.14 KB)

1
(* This module implements formulas with global box and global diamond (A, E) *)
2

    
3
module CA = CoAlgFormula
4

    
5
type eaformula =
6
  | TRUE
7
  | FALSE
8
  | AP of string (*named atom*)
9
  | NOT of eaformula
10
  | OR of eaformula * eaformula
11
  | AND of eaformula * eaformula
12
  | EQU of eaformula * eaformula
13
  | IMP of eaformula * eaformula
14
  | EX of string * eaformula (* exists, diamond of K *)
15
  | AX of string * eaformula (* forall, box of K *)
16
  | ID of eaformula (* modality of the identity functor *)
17
  | E of eaformula (* global diamond *)
18
  | A of eaformula (* global box *)
19

    
20
let rec exportFormula_buffer sb f =
21
  let prio n lf =
22
    let prionr = function
23
      | EQU _ -> 0
24
      | IMP _ -> 1
25
      | OR _ -> 2
26
      | AND _ -> 3
27
      | _ -> 4
28
    in
29
    if prionr lf < n then begin
30
      Buffer.add_char sb '(';
31
      exportFormula_buffer sb lf;
32
      Buffer.add_char sb ')'
33
    end
34
    else exportFormula_buffer sb lf
35
  in
36
  match f with
37
  | TRUE -> Buffer.add_string sb "True"
38
  | FALSE -> Buffer.add_string sb "False"
39
  | AP s -> Buffer.add_string sb s
40
  | NOT f1 ->
41
      Buffer.add_string sb "~";
42
      prio 4 f1
43
  | OR (f1, f2) ->
44
      prio 2 f1;
45
      Buffer.add_string sb " | ";
46
      prio 2 f2
47
  | AND (f1, f2) ->
48
      prio 3 f1;
49
      Buffer.add_string sb " & ";
50
      prio 3 f2
51
  | EQU (f1, f2) ->
52
      prio 0 f1;
53
      Buffer.add_string sb " <=> ";
54
      prio 0 f2
55
  | IMP (f1, f2) ->
56
      prio 2 f1;
57
      Buffer.add_string sb " => ";
58
      prio 2 f2
59
  | EX (s, f1) ->
60
      Buffer.add_string sb "<";
61
      Buffer.add_string sb s;
62
      Buffer.add_string sb ">"
63
  | AX (s, f1) ->
64
      Buffer.add_string sb "[";
65
      Buffer.add_string sb s;
66
      Buffer.add_string sb "]"
67
  | ID f1 ->
68
      Buffer.add_string sb "0";
69
      prio 4 f1
70
  | E f1 ->
71
      Buffer.add_string sb "E ";
72
      prio 4 f1
73
  | A f1 ->
74
      Buffer.add_string sb "A ";
75
      prio 4 f1
76

    
77
let exportFormula f =
78
  let sb = Buffer.create 128 in
79
  exportFormula_buffer sb f;
80
  Buffer.contents sb
81

    
82
let rec nom2EA f = match f with
83
  | CoAlgFormula.FALSE -> FALSE
84
  | CoAlgFormula.AP a -> AP a
85
  | CoAlgFormula.AND (a, b) -> E (AND (nom2EA a, nom2EA b))
86
  | _ -> TRUE
87
        
88
(* vim: set et sw=2 sts=2 ts=8 : *)