cool / src / lib / Nom2fix.ml @ 946e8213
History  View  Annotate  Download (4.04 KB)
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 
 CoAlgFormula.VAR s > CoAlgFormula.VAR s 
34 
in 
35 
rename_formula1 f 
36  
37 
(*calculates inner term of inv for one subformula*) 
38 
let calcforsub subf noms = 
39 
let ret = ref CoAlgFormula.TRUE in 
40 
for i = 0 to (List.length !noms)  1 do 
41 
let aktnom = CoAlgFormula.AP(List.nth !noms i) in 
42 
ret := CoAlgFormula.IMP(CoAlgFormula.EF(CoAlgFormula.AND(subf, aktnom)),CoAlgFormula.AG(CoAlgFormula.IMP(aktnom, subf))); 
43 
done; 
44  
45 
!ret 
46  
47 
let calcinv f noms nomTbl sorts s = 
48 
(*calc flc*) 
49 
let card = Array.length sorts in 
50 
let hcF = CoAlgFormula.HcFormula.create true in 
51 
let fset = Array.init card (fun _ > CoAlgFormula.HcFHt.create 128) in 
52 
let vset = Array.init card (fun _ > CoAlgFormula.HcFHt.create 128) in 
53 
let atset = CoAlgFormula.HcFHt.create 64 in 
54 
let nomset = Hashtbl.create 16 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  
62 
let hashedformulaList = ref [] in 
63 
CoAlgFormula.HcFHt.iter (fun k v > hashedformulaList := k :: (!hashedformulaList)) fset.(0); 
64 

65 
let formulaList = ref [] in 
66  
67 
for i = 0 to (List.length !hashedformulaList)  1 do 
68 
formulaList := (List.nth !hashedformulaList i).fml :: (!formulaList); 
69 
done; 
70 
(*end calc flc*) 
71  
72 
let ret = ref (calcforsub (List.hd !formulaList) noms) in 
73 
for i = 1 to (List.length !formulaList)  1 do 
74 
let sub = calcforsub (List.nth !formulaList i) noms in 
75 
ret := CoAlgFormula.AND(!ret, sub); 
76 
done; 
77  
78 
!ret 
79  
80 
let translate fu nomTbl sorts s = 
81 
let f = (CA.nnf fu) in 
82  
83 
(*list of nominals*) 
84 
let noms = ref [] in 
85 
(*mapping from nominals to new syms*) 
86 
let nomsub = ref StringMap.empty in 
87  
88 
(*first rename nominals then change type to eaformula*) 
89 
let ren = rename f nomsub noms in 
90 
print_string "using Formula: "; 
91 
print_endline (CA.exportFormula ren); 
92  
93 
(*first calculate flc then rename nominals*) 
94 
let invhelp = calcinv f noms nomTbl sorts s in 
95 
(*print_string "invhelp: "; 
96 
print_endline (CoAlgFormula.exportFormula invhelp);*) 
97  
98 
let inv = rename invhelp nomsub noms in 
99 
(*print_string "inv: "; 
100 
print_endline (CoAlgFormula.exportFormula inv);*) 
101  
102 
let formula = if List.length !noms > 0 then CoAlgFormula.AND(ren, inv) else ren in 
103 
let ret = CA.convertToMu formula in 
104 

105 
ret 
106  
107 
(* vim: set et sw=2 sts=2 ts=8 : *) 