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 : *) 