Project

General

Profile

Revision def3763d

View differences:

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