Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / lib / Nom2fix.ml @ 2da28579

History | View | Annotate | Download (4.08 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 =
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
  let (s, fo) = CoAlgFormula.importSortedFormula (CoAlgFormula.exportFormula f) in
56

    
57
  let hcform = CoAlgFormula.hc_formula hcF f in
58

    
59
  CoAlgMisc.sortTable := Array.copy sorts;
60
  CoAlgMisc.detClosure [] nomTbl hcF fset vset atset nomset s hcform;
61

    
62

    
63
  let hashedformulaList = ref [] in
64
  CoAlgFormula.HcFHt.iter (fun k v -> hashedformulaList := k :: (!hashedformulaList)) fset.(0);
65
  
66
  let formulaList = ref [] in
67

    
68
  for i = 0 to (List.length !hashedformulaList) - 1 do
69
    formulaList := (List.nth !hashedformulaList i).fml :: (!formulaList);
70
  done;
71
  (*end calc flc*)
72

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