Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / EAFormula.ml @ e3cf4ca2

History | View | Annotate | Download (7.28 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
  | E_AP s ->
82
      Buffer.add_string sb "E";
83
      Buffer.add_string sb "(";
84
      Buffer.add_string sb s;
85
      Buffer.add_string sb ")"
86
  | A f1 ->
87
      Buffer.add_string sb "A";
88
      prio 4 f1
89

    
90
let exportFormula f =
91
  let sb = Buffer.create 128 in
92
  exportFormula_buffer sb f;
93
  Buffer.contents sb
94
       
95
let gensym = Stream.from (fun i -> Some (Printf.sprintf "#gensym%x#" i))
96

    
97
let rename f nomsub noms =
98
  let rec rename_formula1 f = 
99
    let name = Stream.next gensym in
100
    match f with
101
    | CoAlgFormula.FALSE -> CoAlgFormula.FALSE
102
    | CoAlgFormula.TRUE -> CoAlgFormula.TRUE
103
    | CoAlgFormula.AP s ->
104
        if (CoAlgFormula.isNominal s && not (StringMap.mem s !nomsub)) then noms := name :: !noms;
105
        if (CoAlgFormula.isNominal s && not (StringMap.mem s !nomsub)) then nomsub := StringMap.add s name !nomsub;
106
        if (CoAlgFormula.isNominal s) then CoAlgFormula.AP (StringMap.find s !nomsub)
107
        else CoAlgFormula.AP s
108
    | CoAlgFormula.NOT f -> CoAlgFormula.NOT (rename_formula1 f)
109
    | CoAlgFormula.OR (f1, f2) -> CoAlgFormula.OR ((rename_formula1 f1), (rename_formula1 f2))
110
    | CoAlgFormula.AND (f1, f2) -> CoAlgFormula.AND ((rename_formula1 f1), (rename_formula1 f2))
111
    | CoAlgFormula.EQU (f1, f2) -> CoAlgFormula.EQU ((rename_formula1 f1), (rename_formula1 f2))
112
    | CoAlgFormula.IMP (f1, f2) -> CoAlgFormula.IMP ((rename_formula1 f1), (rename_formula1 f2))
113
    | CoAlgFormula.EX (s, f) -> CoAlgFormula.EX (s, (rename_formula1 f))
114
    | CoAlgFormula.AX (s, f) -> CoAlgFormula.AX (s, (rename_formula1 f))
115
    | CoAlgFormula.ID f -> CoAlgFormula.ID (rename_formula1 f)
116
    | CoAlgFormula.MU (s, f) -> CoAlgFormula.MU (s, (rename_formula1 f))
117
    | CoAlgFormula.NU (s, f) -> CoAlgFormula.NU (s, (rename_formula1 f))
118
    | CoAlgFormula.AF f -> CoAlgFormula.AF (rename_formula1 f)
119
    | CoAlgFormula.EF f -> CoAlgFormula.EF (rename_formula1 f)
120
    | CoAlgFormula.AG f -> CoAlgFormula.AG (rename_formula1 f)
121
    | CoAlgFormula.EG f -> CoAlgFormula.EG (rename_formula1 f)
122
  in
123
  rename_formula1 f
124

    
125

    
126
let coalgtoea f = 
127
  let rec nom2EA_formula1 f =
128
    match f with
129
    | CoAlgFormula.FALSE -> FALSE
130
    | CoAlgFormula.TRUE -> TRUE
131
    | CoAlgFormula.AP s -> AP s
132
    | CoAlgFormula.NOT f -> NOT (nom2EA_formula1 f)
133
    | CoAlgFormula.OR (f1, f2) -> OR ((nom2EA_formula1 f1), (nom2EA_formula1 f2))
134
    | CoAlgFormula.AND (f1, f2) -> AND ((nom2EA_formula1 f1), (nom2EA_formula1 f2))
135
    | CoAlgFormula.EQU (f1, f2) -> EQU ((nom2EA_formula1 f1), (nom2EA_formula1 f2))
136
    | CoAlgFormula.IMP (f1, f2) -> IMP ((nom2EA_formula1 f1), (nom2EA_formula1 f2))
137
    | CoAlgFormula.EX (s, f) -> EX (s, (nom2EA_formula1 f))
138
    | CoAlgFormula.AX (s, f) -> AX (s, (nom2EA_formula1 f))
139
    | CoAlgFormula.ID f -> ID (nom2EA_formula1 f)
140
    | CoAlgFormula.MU (s, f) -> MU (s, (nom2EA_formula1 f))
141
    | CoAlgFormula.NU (s, f) -> NU (s, (nom2EA_formula1 f))
142
    | CoAlgFormula.AF f -> AF (nom2EA_formula1 f)
143
    | CoAlgFormula.EF f -> EF (nom2EA_formula1 f)
144
    | CoAlgFormula.AG f -> AG (nom2EA_formula1 f)
145
    | CoAlgFormula.EG f -> EG (nom2EA_formula1 f)
146
  in
147
  nom2EA_formula1 f
148

    
149
let formula2 f noms nomTbl sorts =
150
  let card = Array.length sorts in
151
  let hcF = CoAlgFormula.HcFormula.create true in
152
  let fset = Array.init card (fun _ -> CoAlgFormula.HcFHt.create 128) in
153
  let vset = Array.init card (fun _ -> CoAlgFormula.HcFHt.create 128) in
154
  let atset = CoAlgFormula.HcFHt.create 64 in
155
  let nomset = Hashtbl.create 16 in
156
  let (s, fo) = CoAlgFormula.importSortedFormula (CoAlgFormula.exportFormula f) in
157

    
158
  let hcform = CoAlgFormula.hc_formula hcF f in
159

    
160
  CoAlgMisc.sortTable := Array.copy sorts;
161
  CoAlgMisc.detClosure [] nomTbl hcF fset vset atset nomset s hcform;
162

    
163
  let hashedformulaList = ref [] in
164
  CoAlgFormula.HcFHt.iter (fun k v -> hashedformulaList := k :: (!hashedformulaList)) fset.(0);
165
  
166
  let formulaList = ref [] in
167

    
168
  for i = 0 to (List.length !hashedformulaList) - 1 do
169
    formulaList := (List.nth !hashedformulaList i).fml :: (!formulaList);
170
  done;
171

    
172
  (*TODO ueber alle Klauseln iterieren*)
173
  let ret = ref (List.hd !formulaList) in
174
  for i = 1 to (List.length !formulaList) - 1 do
175
    ret := CoAlgFormula.AND(!ret, (List.nth !formulaList i));
176
  done;
177

    
178
  !ret
179

    
180
let formula3 noms =
181
  let formula = ref (E_AP (List.nth noms 0)) in
182
  for i = 1 to (List.length noms) - 1 do
183
    formula := AND(!formula, E_AP (List.nth noms i))
184
  done;
185
  !formula
186

    
187
(* calculates the translation from formulas with nominals to formulas with E and A*)
188
(* form_new = form1 & form2 & form3 where
189
 * form1 = form [qi -> nomi] 
190
 * form2 = inv (form1)
191
 * form3 = /\ E(qi)
192
 * *)
193
let nom2EA f nomTbl sorts =
194
  (*list of nominals*)
195
  let noms = ref [] in
196
  (*mapping from nominals to new syms*)
197
  let nomsub = ref StringMap.empty in
198

    
199
  (*first rename nominals then change type to eaformula*)
200
  let form1help = rename f nomsub noms in
201
  let form1 = coalgtoea form1help in
202

    
203
  (*first calculate flc (and in future the other stuff) then rename nominals then change type to eaformula*)
204
  (*TODO Wont work for this A in translation.. Fix it!*)
205
  let form2help = formula2 f noms nomTbl sorts in
206
  let form22 = rename form2help nomsub noms in
207
  let form2 = coalgtoea form22 in
208
  
209
  (*conjunction of all new nominalsymbols*)
210
  let form3 = if List.length !noms > 0 then formula3 !noms else TRUE in
211
  
212
  let formula = if List.length !noms > 0 then AND(AND(form1, form2), form3) else form1 in
213
 
214
  formula
215

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