Initial public import
[afterthought.git] / aft_minterms.ml
1 (* aft_minterms.ml -- 
2  *      1. Converts afterthought programs (pattern matches) first to INF
3  *      (If-then-else normal form) and then Disjunctive Normal Form (DNF).
4  *      2. Optimizes in DNF to produce a hybrid form in which leaf-nodes are 
5  *      DNF expressions, and non-leaf nodes are singleton (decision) variables.
6  *)
7
8 open Xpath_syntax
9 open Xpath_ext
10 open Aft_types
11 open Globals
12 open Array
13 open Python_dict
14
15 type aft_symtab = (path_expr, int) Hashtbl.t
16 type aft_syms = path_expr array
17 type aft_minterm = (path_expr,int) Hashtbl.t * (int list) list
18
19 exception EvalAxisNotSupported
20 exception Aft_error
21
22 let aft_true = Filter(Number_literal(1.0)) 
23 let aft_false = Filter(Number_literal(0.0))
24
25 let one_or_term t =
26   if (t=[]) then [-1] else t
27
28 let zero_or_term t =
29   if (t=[]) then [[-2]] else t
30
31 let aft_to_minterms aft_rep =
32   let minterm_hash:aft_symtab = Hashtbl.create 128 in
33   let syms:aft_syms = Array.create 128 (Expr(Number_literal(1.0))) in
34   let hash_index = ref 0 in
35   let rec aft_to_minterms' prefix cur_term (aft_rep: access_spec) = 
36     match aft_rep with
37       | Filter(Number_literal(x))->
38           if (x = 0.0) then
39             cur_term
40           else
41           if (x=1.0) then ((one_or_term prefix)::cur_term)
42           else begin
43             print "Reached leaf %f" x;raise Aft_error
44           end
45       | INF(m, True(right), False(left)) -> 
46           let term = try Hashtbl.find minterm_hash m with
47             | Not_found ->
48                 Hashtbl.add minterm_hash m !hash_index;
49                 Array.set syms !hash_index m;
50               hash_index := !hash_index + 1;
51               !hash_index-1
52           in
53           let minterm2' = (term+255)::prefix in
54           let minterm2 = term::prefix in
55             let right_function = aft_to_minterms' minterm2 cur_term right in
56                 aft_to_minterms' minterm2' right_function left
57       | _ -> 
58             cur_term
59   in
60   let minterm_list = zero_or_term (aft_to_minterms' [] [] aft_rep) in
61     (minterm_list, syms, !hash_index)
62
63 let rec eval xpath_path =
64   match xpath_path with 
65     | Expr(expr) ->
66         0
67     | Pipe(e1,e2) ->  
68         let v = eval e1 in
69           if (-1=v) then eval e2 else v
70     | Slash(e1,e2) ->
71         let v = eval e1 in
72           if (-1=v) then eval e2 else v
73     | Condition(e,expr) ->
74         eval e
75     | Root ->
76         -1
77     | Axis(_,e)->
78         eval e
79     | Name(s)->
80         let c = String.get s 0 in
81         let ic = int_of_char c in
82           if (ic > 64 && ic < 91) then 1 else 0
83     | _ -> raise EvalAxisNotSupported
84
85 let optimize_minterms m_syms n =
86   let rec gen_lst n suffix = if (n==(-1)) then suffix else gen_lst (n-1) (n::suffix) in
87   let lst = gen_lst (n-1) [] in
88   let cmp_func a1 a2 = 
89     let term1 = Array.get m_syms a1 in
90     let term2 = Array.get m_syms a2 in
91       if ((eval term1) > (eval term2)) then 1 else 0
92   in
93     List.stable_sort cmp_func lst
94
95 let rec print_minterms lst =
96   match lst with
97     | car::cdr -> List.iter (print "%d ") car;print ";";print_minterms cdr
98     | [] -> print "\n"
99
100 let rec const_to_aft m_list = 
101   match m_list with
102     | [] -> aft_false
103     | [singleton]::cdr -> if (singleton=(-1) (*true*) ) then aft_true else const_to_aft cdr
104     | []::cdr -> const_to_aft cdr
105     | x -> print "Did not reduce to constant expression:\n";print_minterms x;raise Aft_error
106
107 let linear x fx =
108   (fx=x || fx=(x+255))
109
110 let var_delete var term = 
111   let rec var_delete' var prefix term = 
112     match term with 
113       | car::[] ->
114           if (linear var car) then
115             if (prefix = []) then [-1] else prefix
116           else
117             car::prefix
118       | car::cdr ->
119           if (linear car var) then
120             var_delete' var prefix cdr
121           else
122             var_delete' var (car::prefix) cdr
123       | [] -> []
124   in
125     var_delete' var [] term
126
127
128 let filter_by_member fn lst =
129     List.filter (fun x->not (List.exists fn x)) lst
130
131 let reduce var terms neg_check = 
132   let nl = filter_by_member neg_check terms in
133     List.map (var_delete var) nl
134
135 let reduce_true var terms =
136     reduce var terms (fun x->x=(var+255))
137
138 let reduce_false var terms =
139   let res = reduce var terms (fun x->var=x) in
140     res
141   
142 let var_to_aft syms term =
143   Array.get syms term
144
145 let rec mature minterms =
146   match minterms with
147     | [[]] -> true
148     | [] -> true
149     | [singleton]::cdr -> if (singleton<0) then mature cdr else false
150     | _ -> false
151
152 let minterms_to_filter minterms =
153   try
154     const_to_aft minterms
155   with Aft_error ->
156     print "Immature expression:";print_minterms minterms;raise Aft_error
157
158 let rec minterms_to_aft m_list m_syms order n_terms =
159   if (mature(m_list)) 
160   then 
161       minterms_to_filter m_list
162   else
163     begin
164       match order with
165         | [] ->
166             const_to_aft m_list
167         | car::cdr ->
168             let right = reduce_true car m_list in
169             let left = reduce_false car m_list in
170             let right_aft = minterms_to_aft right m_syms cdr (n_terms-1) in
171             let left_aft = minterms_to_aft left m_syms cdr (n_terms-1) in
172               (INF((var_to_aft m_syms car),True(right_aft),False(left_aft)))
173     end
174
175 let rec aft_to_il l_inp = 
176   let rec aft_to_il' (aft_rep: access_spec) = 
177     let rec pattern_match_to_il  (pat_match: clause list) =
178         match pat_match with
179             Clause(m, aspec)::cdr -> 
180               let left_function = pattern_match_to_il cdr in
181               let right_function = aft_to_il' aspec in
182                 INF(m,True(right_function),False(left_function))
183             | [] -> 
184                 Filter(Number_literal(0.0))
185     in
186     match aft_rep with
187       | PatternMatch(cl_list) -> 
188           pattern_match_to_il cl_list
189       | other -> other
190   in
191     aft_to_il' l_inp
192
193 let tab n =
194   String.make n '\t'
195
196 let pretty_print l =
197   let rec pretty_print' l tablevel =
198       match l with 
199         | Filter(Number_literal(x)) -> tabprint tablevel "%f\n" x
200         | Filter(_) -> print "[filter]"
201         | INF(path, True(l'), False(l'')) ->
202             let spath = pretty_print_xpath_path path in
203               begin
204                   tabprint tablevel "%s ->\n{" spath;
205                   pretty_print' l' (tablevel + 1);
206                   tabprint tablevel "}\n";
207                   tabprint tablevel "| {";
208                   pretty_print' l'' (tablevel + 1);
209                   tabprint tablevel "}\n"
210               end
211         | PatternMatch(_) -> print "Expression not reduced";raise Aft_error
212   in
213     pretty_print' l 0