Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / EAFormula.ml @ def3763d

History | View | Annotate | Download (8.02 KB)

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

    
3
module CA = CoAlgFormula
4
module StringMap = Map.Make(String)
5

    
6
type nomTbl = string -> CoAlgFormula.sort option
7

    
8
type eaformula =
9
  | TRUE
10
  | FALSE
11
  | AP of string (*named atom*)
12
  | NOT of eaformula
13
  | OR of eaformula * eaformula
14
  | AND of eaformula * eaformula
15
  | EQU of eaformula * eaformula
16
  | IMP of eaformula * eaformula
17
  | EX of string * eaformula (* exists, diamond of K *)
18
  | AX of string * eaformula (* forall, box of K *)
19
  | ID of eaformula (* modality of the identity functor *)
20
  | E_AP of string (* global diamond *)
21
  | A of eaformula (* global box *)
22
  | MU of string * eaformula
23
  | NU of string * eaformula
24
  | AF of eaformula
25
  | EF of eaformula
26
  | AG of eaformula
27
  | EG of eaformula
28

    
29
let rec exportFormula_buffer sb f =
30
  let prio n lf =
31
    let prionr = function
32
      | EQU _ -> 0
33
      | IMP _ -> 1
34
      | OR _ -> 2
35
      | AND _ -> 3
36
      | _ -> 4
37
    in
38
    if prionr lf < n then begin
39
      Buffer.add_char sb '(';
40
      exportFormula_buffer sb lf;
41
      Buffer.add_char sb ')'
42
    end
43
    else exportFormula_buffer sb lf
44
  in
45
  match f with
46
  | TRUE -> Buffer.add_string sb "True"
47
  | FALSE -> Buffer.add_string sb "False"
48
  | AP s -> Buffer.add_string sb s
49
  | NOT f1 ->
50
      Buffer.add_string sb "~";
51
      prio 4 f1
52
  | OR (f1, f2) ->
53
      prio 2 f1;
54
      Buffer.add_string sb " | ";
55
      prio 2 f2
56
  | AND (f1, f2) ->
57
      prio 3 f1;
58
      Buffer.add_string sb " & ";
59
      prio 3 f2
60
  | EQU (f1, f2) ->
61
      prio 0 f1;
62
      Buffer.add_string sb " <=> ";
63
      prio 0 f2
64
  | IMP (f1, f2) ->
65
      prio 2 f1;
66
      Buffer.add_string sb " => ";
67
      prio 2 f2
68
  | EX (s, f1) ->
69
      Buffer.add_string sb "<";
70
      Buffer.add_string sb s;
71
      Buffer.add_string sb ">";
72
      prio 4 f1
73
  | AX (s, f1) ->
74
      Buffer.add_string sb "[";
75
      Buffer.add_string sb s;
76
      Buffer.add_string sb "]";
77
      prio 4 f1
78
  | ID f1 ->
79
      Buffer.add_string sb "0";
80
      prio 4 f1
81
  | MU (s, f1) ->
82
      Buffer.add_string sb "µ";
83
      Buffer.add_string sb s;
84
      Buffer.add_string sb ".";
85
      prio 4 f1
86
  | NU (s, f1) ->
87
      Buffer.add_string sb "ν";
88
      Buffer.add_string sb s;
89
      Buffer.add_string sb ".";
90
      prio 4 f1
91
  | E_AP s ->
92
      Buffer.add_string sb "E";
93
      Buffer.add_string sb "(";
94
      Buffer.add_string sb s;
95
      Buffer.add_string sb ")"
96
  | A f1 ->
97
      Buffer.add_string sb "A";
98
      prio 4 f1
99

    
100
let exportFormula f =
101
  let sb = Buffer.create 128 in
102
  exportFormula_buffer sb f;
103
  Buffer.contents sb
104
       
105
let gensym = Stream.from (fun i -> Some (Printf.sprintf "#gensym%x#" i))
106

    
107
let rename f nomsub noms =
108
  let rec rename_formula1 f = 
109
    let name = Stream.next gensym in
110
    match f with
111
    | CoAlgFormula.FALSE -> CoAlgFormula.FALSE
112
    | CoAlgFormula.TRUE -> CoAlgFormula.TRUE
113
    | CoAlgFormula.AP s ->
114
        if (CoAlgFormula.isNominal s && not (StringMap.mem s !nomsub)) then noms := name :: !noms;
115
        if (CoAlgFormula.isNominal s && not (StringMap.mem s !nomsub)) then nomsub := StringMap.add s name !nomsub;
116
        if (CoAlgFormula.isNominal s) then CoAlgFormula.AP (StringMap.find s !nomsub)
117
        else CoAlgFormula.AP s
118
    | CoAlgFormula.NOT f -> CoAlgFormula.NOT (rename_formula1 f)
119
    | CoAlgFormula.OR (f1, f2) -> CoAlgFormula.OR ((rename_formula1 f1), (rename_formula1 f2))
120
    | CoAlgFormula.AND (f1, f2) -> CoAlgFormula.AND ((rename_formula1 f1), (rename_formula1 f2))
121
    | CoAlgFormula.EQU (f1, f2) -> CoAlgFormula.EQU ((rename_formula1 f1), (rename_formula1 f2))
122
    | CoAlgFormula.IMP (f1, f2) -> CoAlgFormula.IMP ((rename_formula1 f1), (rename_formula1 f2))
123
    | CoAlgFormula.EX (s, f) -> CoAlgFormula.EX (s, (rename_formula1 f))
124
    | CoAlgFormula.AX (s, f) -> CoAlgFormula.AX (s, (rename_formula1 f))
125
    | CoAlgFormula.ID f -> CoAlgFormula.ID (rename_formula1 f)
126
    | CoAlgFormula.MU (s, f) -> CoAlgFormula.MU (s, (rename_formula1 f))
127
    | CoAlgFormula.NU (s, f) -> CoAlgFormula.NU (s, (rename_formula1 f))
128
    | CoAlgFormula.AF f -> CoAlgFormula.AF (rename_formula1 f)
129
    | CoAlgFormula.EF f -> CoAlgFormula.EF (rename_formula1 f)
130
    | CoAlgFormula.AG f -> CoAlgFormula.AG (rename_formula1 f)
131
    | CoAlgFormula.EG f -> CoAlgFormula.EG (rename_formula1 f)
132
  in
133
  rename_formula1 f
134

    
135

    
136
let coalgtoea f = 
137
  let rec nom2EA_formula1 f =
138
    match f with
139
    | CoAlgFormula.FALSE -> FALSE
140
    | CoAlgFormula.TRUE -> TRUE
141
    | CoAlgFormula.AP s -> AP s
142
    | CoAlgFormula.NOT f -> NOT (nom2EA_formula1 f)
143
    | CoAlgFormula.OR (f1, f2) -> OR ((nom2EA_formula1 f1), (nom2EA_formula1 f2))
144
    | CoAlgFormula.AND (f1, f2) -> AND ((nom2EA_formula1 f1), (nom2EA_formula1 f2))
145
    | CoAlgFormula.EQU (f1, f2) -> EQU ((nom2EA_formula1 f1), (nom2EA_formula1 f2))
146
    | CoAlgFormula.IMP (f1, f2) -> IMP ((nom2EA_formula1 f1), (nom2EA_formula1 f2))
147
    | CoAlgFormula.EX (s, f) -> EX (s, (nom2EA_formula1 f))
148
    | CoAlgFormula.AX (s, f) -> AX (s, (nom2EA_formula1 f))
149
    | CoAlgFormula.ID f -> ID (nom2EA_formula1 f)
150
    | CoAlgFormula.MU (s, f) -> MU (s, (nom2EA_formula1 f))
151
    | CoAlgFormula.NU (s, f) -> NU (s, (nom2EA_formula1 f))
152
    | CoAlgFormula.AF f -> AF (nom2EA_formula1 f)
153
    | CoAlgFormula.EF f -> EF (nom2EA_formula1 f)
154
    | CoAlgFormula.AG f -> AG (nom2EA_formula1 f)
155
    | CoAlgFormula.EG f -> EG (nom2EA_formula1 f)
156
  in
157
  nom2EA_formula1 f
158

    
159
let formula2 f noms nomTbl sorts =
160
  let card = Array.length sorts in
161
  let hcF = CoAlgFormula.HcFormula.create true in
162
  let fset = Array.init card (fun _ -> CoAlgFormula.HcFHt.create 128) in
163
  let vset = Array.init card (fun _ -> CoAlgFormula.HcFHt.create 128) in
164
  let atset = CoAlgFormula.HcFHt.create 64 in
165
  let nomset = Hashtbl.create 16 in
166
  let (s, fo) = CoAlgFormula.importSortedFormula (CoAlgFormula.exportFormula f) in
167

    
168
  let hcform = CoAlgFormula.hc_formula hcF f in
169

    
170
  CoAlgMisc.sortTable := Array.copy sorts;
171
  CoAlgMisc.detClosure [] nomTbl hcF fset vset atset nomset s hcform;
172

    
173
  let hashedformulaList = ref [] in
174
  CoAlgFormula.HcFHt.iter (fun k v -> hashedformulaList := k :: (!hashedformulaList)) fset.(0);
175
  
176
  let formulaList = ref [] in
177

    
178
  for i = 0 to (List.length !hashedformulaList) - 1 do
179
    formulaList := (List.nth !hashedformulaList i).fml :: (!formulaList);
180
  done;
181

    
182
  (*TODO ueber alle Klauseln iterieren*)
183
  let ret = ref (List.hd !formulaList) in
184
  for i = 1 to (List.length !formulaList) - 1 do
185
    ret := CoAlgFormula.AND(!ret, (List.nth !formulaList i));
186
  done;
187

    
188
  !ret
189

    
190
let formula3 noms =
191
  let formula = ref (E_AP (List.nth noms 0)) in
192
  for i = 1 to (List.length noms) - 1 do
193
    formula := AND(!formula, E_AP (List.nth noms i))
194
  done;
195
  !formula
196

    
197
(* calculates the translation from formulas with nominals to formulas with E and A*)
198
(* form_new = form1 & form2 & form3 where
199
 * form1 = form [qi -> nomi] 
200
 * form2 = inv (form1)
201
 * form3 = /\ E(qi)
202
 * *)
203
let nom2EA f nomTbl sorts =
204
  (*list of nominals*)
205
  let noms = ref [] in
206
  (*mapping from nominals to new syms*)
207
  let nomsub = ref StringMap.empty in
208

    
209
  print_endline (CoAlgFormula.exportFormula f);
210

    
211
  (*first rename nominals then change type to eaformula*)
212
  let form1help = rename f nomsub noms in
213
  print_string "form1help: ";
214
  print_endline (CoAlgFormula.exportFormula form1help);
215

    
216
  let form1 = coalgtoea form1help in
217
  print_string "form1: ";
218
  print_endline (exportFormula form1);
219

    
220
  (*first calculate flc (and in future the other stuff) then rename nominals then change type to eaformula*)
221
  (*TODO Wont work for this A in translation.. Fix it!*)
222
  let form2help = formula2 f noms nomTbl sorts in
223
  print_string "form2help: ";
224
  print_endline (CoAlgFormula.exportFormula form2help);
225

    
226
  let form22 = rename form2help nomsub noms in
227
  print_string "form22: ";
228
  print_endline (CoAlgFormula.exportFormula form22);
229

    
230
  let form2 = coalgtoea form22 in
231
  print_string "form2: ";
232
  print_endline (exportFormula form2);
233

    
234
  (*conjunction of all new nominalsymbols*)
235
  let form3 = if List.length !noms > 0 then formula3 !noms else TRUE in
236
  print_string "form3: ";
237
  print_endline (exportFormula form3);
238
  
239
  let formula = if List.length !noms > 0 then AND(AND(form1, form2), form3) else form1 in
240
 
241
  formula
242

    
243
(* vim: set et sw=2 sts=2 ts=8 : *)