Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / Nom2fix.ml @ def3763d

History | View | Annotate | Download (4.07 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
  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 : *)