cannam@95
|
1 (*
|
cannam@95
|
2 * Copyright (c) 1997-1999 Massachusetts Institute of Technology
|
cannam@95
|
3 * Copyright (c) 2003, 2007-11 Matteo Frigo
|
cannam@95
|
4 * Copyright (c) 2003, 2007-11 Massachusetts Institute of Technology
|
cannam@95
|
5 *
|
cannam@95
|
6 * This program is free software; you can redistribute it and/or modify
|
cannam@95
|
7 * it under the terms of the GNU General Public License as published by
|
cannam@95
|
8 * the Free Software Foundation; either version 2 of the License, or
|
cannam@95
|
9 * (at your option) any later version.
|
cannam@95
|
10 *
|
cannam@95
|
11 * This program is distributed in the hope that it will be useful,
|
cannam@95
|
12 * but WITHOUT ANY WARRANTY; without even the implied warranty of
|
cannam@95
|
13 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
|
cannam@95
|
14 * GNU General Public License for more details.
|
cannam@95
|
15 *
|
cannam@95
|
16 * You should have received a copy of the GNU General Public License
|
cannam@95
|
17 * along with this program; if not, write to the Free Software
|
cannam@95
|
18 * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA
|
cannam@95
|
19 *
|
cannam@95
|
20 *)
|
cannam@95
|
21
|
cannam@95
|
22 (* Here, we define the data type encapsulating a symbolic arithmetic
|
cannam@95
|
23 expression, and provide some routines for manipulating it. *)
|
cannam@95
|
24
|
cannam@95
|
25 (* I will regret this hack : *)
|
cannam@95
|
26 (* NEWS: I did *)
|
cannam@95
|
27 type transcendent = I | MULTI_A | MULTI_B | CONJ
|
cannam@95
|
28
|
cannam@95
|
29 type expr =
|
cannam@95
|
30 | Num of Number.number
|
cannam@95
|
31 | NaN of transcendent
|
cannam@95
|
32 | Plus of expr list
|
cannam@95
|
33 | Times of expr * expr
|
cannam@95
|
34 | CTimes of expr * expr
|
cannam@95
|
35 | CTimesJ of expr * expr (* CTimesJ (a, b) = conj(a) * b *)
|
cannam@95
|
36 | Uminus of expr
|
cannam@95
|
37 | Load of Variable.variable
|
cannam@95
|
38 | Store of Variable.variable * expr
|
cannam@95
|
39
|
cannam@95
|
40 type assignment = Assign of Variable.variable * expr
|
cannam@95
|
41
|
cannam@95
|
42 (* various hash functions *)
|
cannam@95
|
43 let hash_float x =
|
cannam@95
|
44 let (mantissa, exponent) = frexp x
|
cannam@95
|
45 in truncate (float_of_int(exponent) *. 1234.567 +. mantissa *. 10000.0)
|
cannam@95
|
46
|
cannam@95
|
47 let sum_list l = List.fold_right (+) l 0
|
cannam@95
|
48
|
cannam@95
|
49 let transcendent_to_float = function
|
cannam@95
|
50 | I -> 2.718281828459045235360287471 (* any transcendent number will do *)
|
cannam@95
|
51 | MULTI_A -> 0.6931471805599453094172321214
|
cannam@95
|
52 | MULTI_B -> -0.3665129205816643270124391582
|
cannam@95
|
53 | CONJ -> 0.6019072301972345747375400015
|
cannam@95
|
54
|
cannam@95
|
55 let rec hash = function
|
cannam@95
|
56 | Num x -> hash_float (Number.to_float x)
|
cannam@95
|
57 | NaN x -> hash_float (transcendent_to_float x)
|
cannam@95
|
58 | Load v -> 1 + 1237 * Variable.hash v
|
cannam@95
|
59 | Store (v, x) -> 2 * Variable.hash v - 2345 * hash x
|
cannam@95
|
60 | Plus l -> 5 + 23451 * sum_list (List.map Hashtbl.hash l)
|
cannam@95
|
61 | Times (a, b) -> 41 + 31415 * (Hashtbl.hash a + Hashtbl.hash b)
|
cannam@95
|
62 | CTimes (a, b) -> 49 + 3245 * (Hashtbl.hash a + Hashtbl.hash b)
|
cannam@95
|
63 | CTimesJ (a, b) -> 31 + 3471 * (Hashtbl.hash a + Hashtbl.hash b)
|
cannam@95
|
64 | Uminus x -> 42 + 12345 * (hash x)
|
cannam@95
|
65
|
cannam@95
|
66 (* find all variables *)
|
cannam@95
|
67 let rec find_vars x =
|
cannam@95
|
68 match x with
|
cannam@95
|
69 | Load y -> [y]
|
cannam@95
|
70 | Plus l -> List.flatten (List.map find_vars l)
|
cannam@95
|
71 | Times (a, b) -> (find_vars a) @ (find_vars b)
|
cannam@95
|
72 | CTimes (a, b) -> (find_vars a) @ (find_vars b)
|
cannam@95
|
73 | CTimesJ (a, b) -> (find_vars a) @ (find_vars b)
|
cannam@95
|
74 | Uminus a -> find_vars a
|
cannam@95
|
75 | _ -> []
|
cannam@95
|
76
|
cannam@95
|
77
|
cannam@95
|
78 (* TRUE if expression is a constant *)
|
cannam@95
|
79 let is_constant = function
|
cannam@95
|
80 | Num _ -> true
|
cannam@95
|
81 | NaN _ -> true
|
cannam@95
|
82 | Load v -> Variable.is_constant v
|
cannam@95
|
83 | _ -> false
|
cannam@95
|
84
|
cannam@95
|
85 let is_known_constant = function
|
cannam@95
|
86 | Num _ -> true
|
cannam@95
|
87 | NaN _ -> true
|
cannam@95
|
88 | _ -> false
|
cannam@95
|
89
|
cannam@95
|
90 (* expr to string, used for debugging *)
|
cannam@95
|
91 let rec foldr_string_concat l =
|
cannam@95
|
92 match l with
|
cannam@95
|
93 [] -> ""
|
cannam@95
|
94 | [a] -> a
|
cannam@95
|
95 | a :: b -> a ^ " " ^ (foldr_string_concat b)
|
cannam@95
|
96
|
cannam@95
|
97 let string_of_transcendent = function
|
cannam@95
|
98 | I -> "I"
|
cannam@95
|
99 | MULTI_A -> "MULTI_A"
|
cannam@95
|
100 | MULTI_B -> "MULTI_B"
|
cannam@95
|
101 | CONJ -> "CONJ"
|
cannam@95
|
102
|
cannam@95
|
103 let rec to_string = function
|
cannam@95
|
104 | Load v -> Variable.unparse v
|
cannam@95
|
105 | Num n -> string_of_float (Number.to_float n)
|
cannam@95
|
106 | NaN n -> string_of_transcendent n
|
cannam@95
|
107 | Plus x -> "(+ " ^ (foldr_string_concat (List.map to_string x)) ^ ")"
|
cannam@95
|
108 | Times (a, b) -> "(* " ^ (to_string a) ^ " " ^ (to_string b) ^ ")"
|
cannam@95
|
109 | CTimes (a, b) -> "(c* " ^ (to_string a) ^ " " ^ (to_string b) ^ ")"
|
cannam@95
|
110 | CTimesJ (a, b) -> "(cj* " ^ (to_string a) ^ " " ^ (to_string b) ^ ")"
|
cannam@95
|
111 | Uminus a -> "(- " ^ (to_string a) ^ ")"
|
cannam@95
|
112 | Store (v, a) -> "(:= " ^ (Variable.unparse v) ^ " " ^
|
cannam@95
|
113 (to_string a) ^ ")"
|
cannam@95
|
114
|
cannam@95
|
115 let rec to_string_a d x =
|
cannam@95
|
116 if (d = 0) then "..." else match x with
|
cannam@95
|
117 | Load v -> Variable.unparse v
|
cannam@95
|
118 | Num n -> Number.to_konst n
|
cannam@95
|
119 | NaN n -> string_of_transcendent n
|
cannam@95
|
120 | Plus x -> "(+ " ^ (foldr_string_concat (List.map (to_string_a (d - 1)) x)) ^ ")"
|
cannam@95
|
121 | Times (a, b) -> "(* " ^ (to_string_a (d - 1) a) ^ " " ^ (to_string_a (d - 1) b) ^ ")"
|
cannam@95
|
122 | CTimes (a, b) -> "(c* " ^ (to_string_a (d - 1) a) ^ " " ^ (to_string_a (d - 1) b) ^ ")"
|
cannam@95
|
123 | CTimesJ (a, b) -> "(cj* " ^ (to_string_a (d - 1) a) ^ " " ^ (to_string_a (d - 1) b) ^ ")"
|
cannam@95
|
124 | Uminus a -> "(- " ^ (to_string_a (d-1) a) ^ ")"
|
cannam@95
|
125 | Store (v, a) -> "(:= " ^ (Variable.unparse v) ^ " " ^
|
cannam@95
|
126 (to_string_a (d-1) a) ^ ")"
|
cannam@95
|
127
|
cannam@95
|
128 let to_string = to_string_a 10
|
cannam@95
|
129
|
cannam@95
|
130 let assignment_to_string = function
|
cannam@95
|
131 | Assign (v, a) -> "(:= " ^ (Variable.unparse v) ^ " " ^ (to_string a) ^ ")"
|
cannam@95
|
132
|
cannam@95
|
133 let dump print = List.iter (fun x -> print ((assignment_to_string x) ^ "\n"))
|
cannam@95
|
134
|
cannam@95
|
135 (* find all constants in a given expression *)
|
cannam@95
|
136 let rec expr_to_constants = function
|
cannam@95
|
137 | Num n -> [n]
|
cannam@95
|
138 | Plus a -> List.flatten (List.map expr_to_constants a)
|
cannam@95
|
139 | Times (a, b) -> (expr_to_constants a) @ (expr_to_constants b)
|
cannam@95
|
140 | CTimes (a, b) -> (expr_to_constants a) @ (expr_to_constants b)
|
cannam@95
|
141 | CTimesJ (a, b) -> (expr_to_constants a) @ (expr_to_constants b)
|
cannam@95
|
142 | Uminus a -> expr_to_constants a
|
cannam@95
|
143 | _ -> []
|
cannam@95
|
144
|
cannam@95
|
145
|
cannam@95
|
146 let add_float_key_value list_so_far k =
|
cannam@95
|
147 if List.exists (fun k2 -> Number.equal k k2) list_so_far then
|
cannam@95
|
148 list_so_far
|
cannam@95
|
149 else
|
cannam@95
|
150 k :: list_so_far
|
cannam@95
|
151
|
cannam@95
|
152 let unique_constants = List.fold_left add_float_key_value []
|