Revision def3763d
src/coalg/coalg.ml  

7  7 
module CM = CoAlgMisc 
8  8 
module CF = CoAlgFormula 
9  9 
module EA = EAFormula 
10 
module NF = Nom2fix 

10  11  
11  12 
module FE = FunctorParsing 
12  13  
...  ...  
177  178 
let input = read_line () in 
178  179 
if not (GenAndComp.isEmptyString input) then 
179  180 
let f = CoAlgFormula.importFormula input in 
180 
let g = EAFormula.nom2EA f nomTable sorts in 

181 
let str = EAFormula.exportFormula g in 

181 
(*let g = EAFormula.nom2EA f nomTable sorts in*) 

182 
(*let str = EAFormula.exportFormula g in*) 

183 
let g = Nom2fix.translate f nomTable sorts in 

184 
let str = CoAlgFormula.exportFormula g in 

182  185 
incr counter; 
183  186 
print_string("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n"); 
184  187 
flush stdout; 
src/lib/EAFormula.ml  

78  78 
 ID f1 > 
79  79 
Buffer.add_string sb "0"; 
80  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 

81  91 
 E_AP s > 
82  92 
Buffer.add_string sb "E"; 
83  93 
Buffer.add_string sb "("; 
...  ...  
196  206 
(*mapping from nominals to new syms*) 
197  207 
let nomsub = ref StringMap.empty in 
198  208  
209 
print_endline (CoAlgFormula.exportFormula f); 

210  
199  211 
(*first rename nominals then change type to eaformula*) 
200  212 
let form1help = rename f nomsub noms in 
213 
print_string "form1help: "; 

214 
print_endline (CoAlgFormula.exportFormula form1help); 

215  
201  216 
let form1 = coalgtoea form1help in 
217 
print_string "form1: "; 

218 
print_endline (exportFormula form1); 

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

224 
print_endline (CoAlgFormula.exportFormula form2help); 

225  
206  226 
let form22 = rename form2help nomsub noms in 
227 
print_string "form22: "; 

228 
print_endline (CoAlgFormula.exportFormula form22); 

229  
207  230 
let form2 = coalgtoea form22 in 
208 


231 
print_string "form2: "; 

232 
print_endline (exportFormula form2); 

233  
209  234 
(*conjunction of all new nominalsymbols*) 
210  235 
let form3 = if List.length !noms > 0 then formula3 !noms else TRUE in 
236 
print_string "form3: "; 

237 
print_endline (exportFormula form3); 

211  238 

212  239 
let formula = if List.length !noms > 0 then AND(AND(form1, form2), form3) else form1 in 
213  240 

src/lib/Nom2fix.ml  

1 
module CA = CoAlgFormula 

2 
module StringMap = Map.Make(String) 

3  
4 
type nomTbl = string > CoAlgFormula.sort option 

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

6  
7  
8 
let rename f nomsub noms = 

9 
let rec rename_formula1 f = 

10 
let name = Stream.next gensym in 

11 
match f with 

12 
 CoAlgFormula.FALSE > CoAlgFormula.FALSE 

13 
 CoAlgFormula.TRUE > CoAlgFormula.TRUE 

14 
 CoAlgFormula.AP s > 

15 
if (CoAlgFormula.isNominal s && not (StringMap.mem s !nomsub)) then noms := name :: !noms; 

16 
if (CoAlgFormula.isNominal s && not (StringMap.mem s !nomsub)) then nomsub := StringMap.add s name !nomsub; 

17 
if (CoAlgFormula.isNominal s) then CoAlgFormula.AP (StringMap.find s !nomsub) 

18 
else CoAlgFormula.AP s 

19 
 CoAlgFormula.NOT f > CoAlgFormula.NOT (rename_formula1 f) 

20 
 CoAlgFormula.OR (f1, f2) > CoAlgFormula.OR ((rename_formula1 f1), (rename_formula1 f2)) 

21 
 CoAlgFormula.AND (f1, f2) > CoAlgFormula.AND ((rename_formula1 f1), (rename_formula1 f2)) 

22 
 CoAlgFormula.EQU (f1, f2) > CoAlgFormula.EQU ((rename_formula1 f1), (rename_formula1 f2)) 

23 
 CoAlgFormula.IMP (f1, f2) > CoAlgFormula.IMP ((rename_formula1 f1), (rename_formula1 f2)) 

24 
 CoAlgFormula.EX (s, f) > CoAlgFormula.EX (s, (rename_formula1 f)) 

25 
 CoAlgFormula.AX (s, f) > CoAlgFormula.AX (s, (rename_formula1 f)) 

26 
 CoAlgFormula.ID f > CoAlgFormula.ID (rename_formula1 f) 

27 
 CoAlgFormula.MU (s, f) > CoAlgFormula.MU (s, (rename_formula1 f)) 

28 
 CoAlgFormula.NU (s, f) > CoAlgFormula.NU (s, (rename_formula1 f)) 

29 
 CoAlgFormula.AF f > CoAlgFormula.AF (rename_formula1 f) 

30 
 CoAlgFormula.EF f > CoAlgFormula.EF (rename_formula1 f) 

31 
 CoAlgFormula.AG f > CoAlgFormula.AG (rename_formula1 f) 

32 
 CoAlgFormula.EG f > CoAlgFormula.EG (rename_formula1 f) 

33 
in 

34 
rename_formula1 f 

35  
36 
(*calculates inner term of inv for one subformula*) 

37 
let calcforsub subf noms = 

38 
let ret = ref CoAlgFormula.TRUE in 

39 
for i = 0 to (List.length !noms)  1 do 

40 
let aktnom = CoAlgFormula.AP(List.nth !noms i) in 

41 
ret := CoAlgFormula.IMP(CoAlgFormula.EF(CoAlgFormula.AND(subf, aktnom)),CoAlgFormula.AG(CoAlgFormula.IMP(aktnom, subf))); 

42 
done; 

43  
44 
!ret 

45  
46 
let calcinv f noms nomTbl sorts = 

47 
(*calc flc*) 

48 
let card = Array.length sorts in 

49 
let hcF = CoAlgFormula.HcFormula.create true in 

50 
let fset = Array.init card (fun _ > CoAlgFormula.HcFHt.create 128) in 

51 
let vset = Array.init card (fun _ > CoAlgFormula.HcFHt.create 128) in 

52 
let atset = CoAlgFormula.HcFHt.create 64 in 

53 
let nomset = Hashtbl.create 16 in 

54 
let (s, fo) = CoAlgFormula.importSortedFormula (CoAlgFormula.exportFormula f) in 

55  
56 
let hcform = CoAlgFormula.hc_formula hcF f in 

57  
58 
CoAlgMisc.sortTable := Array.copy sorts; 

59 
CoAlgMisc.detClosure [] nomTbl hcF fset vset atset nomset s hcform; 

60  
61 
let hashedformulaList = ref [] in 

62 
CoAlgFormula.HcFHt.iter (fun k v > hashedformulaList := k :: (!hashedformulaList)) fset.(0); 

63 


64 
let formulaList = ref [] in 

65  
66 
for i = 0 to (List.length !hashedformulaList)  1 do 

67 
formulaList := (List.nth !hashedformulaList i).fml :: (!formulaList); 

68 
done; 

69 
(*end calc flc*) 

70  
71  
72 
(*TODO ueber alle Klauseln iterieren*) 

73 
let ret = ref (calcforsub (List.hd !formulaList) noms) in 

74 
for i = 1 to (List.length !formulaList)  1 do 

75 
let sub = calcforsub (List.nth !formulaList i) noms in 

76 
ret := CoAlgFormula.AND(!ret, sub); 

77 
done; 

78  
79 
!ret 

80  
81 
let translate f nomTbl sorts = 

82 
(*list of nominals*) 

83 
let noms = ref [] in 

84 
(*mapping from nominals to new syms*) 

85 
let nomsub = ref StringMap.empty in 

86  
87 
print_endline (CA.exportFormula f); 

88  
89 
(*first rename nominals then change type to eaformula*) 

90 
let ren = rename f nomsub noms in 

91 
print_string "rename: "; 

92 
print_endline (CA.exportFormula ren); 

93  
94 
(*first calculate flc then rename nominals*) 

95 
let invhelp = calcinv f noms nomTbl sorts in 

96 
print_string "invhelp: "; 

97 
print_endline (CoAlgFormula.exportFormula invhelp); 

98  
99 
let inv = rename invhelp nomsub noms in 

100 
print_string "inv: "; 

101 
print_endline (CoAlgFormula.exportFormula inv); 

102  
103 
let formula = if List.length !noms > 0 then CoAlgFormula.AND(ren, inv) else ren in 

104 


105 
formula 

106  
107 
(* vim: set et sw=2 sts=2 ts=8 : *) 
src/lib/Nom2fix.mli  

1 
module CA = CoAlgFormula 

2  
3 
type nomTbl = string > CoAlgFormula.sort option 

4  
5 
val rename : CoAlgFormula.formula > string Map.Make(String).t ref > string list ref > CoAlgFormula.formula 

6 
val calcforsub: CoAlgFormula.formula > string list ref > CoAlgFormula.formula 

7 
val calcinv : CoAlgFormula.formula > string list ref > (string > int option) > CoAlgReasoner.sortTable > CoAlgFormula.formula 

8 
val translate : CoAlgFormula.formula > (string > int option) > CoAlgReasoner.sortTable > CoAlgFormula.formula 

9  
10 
(* vim: set et sw=2 sts=2 ts=8 : *) 
Also available in: Unified diff