118 and expr_assign = |
118 and expr_assign = |
119 AssignFormulaReg of int * formula | |
119 AssignFormulaReg of int * formula | |
120 AssignRelReg of n_ary_index * rel_expr | |
120 AssignRelReg of n_ary_index * rel_expr | |
121 AssignIntReg of int * int_expr |
121 AssignIntReg of int * int_expr |
122 |
122 |
123 type 'a fold_expr_funcs = { |
123 type 'a fold_expr_funcs = |
124 formula_func: formula -> 'a -> 'a, |
124 {formula_func: formula -> 'a -> 'a, |
125 rel_expr_func: rel_expr -> 'a -> 'a, |
125 rel_expr_func: rel_expr -> 'a -> 'a, |
126 int_expr_func: int_expr -> 'a -> 'a |
126 int_expr_func: int_expr -> 'a -> 'a} |
127 } |
|
128 |
127 |
129 val fold_formula : 'a fold_expr_funcs -> formula -> 'a -> 'a |
128 val fold_formula : 'a fold_expr_funcs -> formula -> 'a -> 'a |
130 val fold_rel_expr : 'a fold_expr_funcs -> rel_expr -> 'a -> 'a |
129 val fold_rel_expr : 'a fold_expr_funcs -> rel_expr -> 'a -> 'a |
131 val fold_int_expr : 'a fold_expr_funcs -> int_expr -> 'a -> 'a |
130 val fold_int_expr : 'a fold_expr_funcs -> int_expr -> 'a -> 'a |
132 val fold_decl : 'a fold_expr_funcs -> decl -> 'a -> 'a |
131 val fold_decl : 'a fold_expr_funcs -> decl -> 'a -> 'a |
133 val fold_expr_assign : 'a fold_expr_funcs -> expr_assign -> 'a -> 'a |
132 val fold_expr_assign : 'a fold_expr_funcs -> expr_assign -> 'a -> 'a |
134 |
133 |
135 type 'a fold_tuple_funcs = { |
134 type 'a fold_tuple_funcs = |
136 tuple_func: tuple -> 'a -> 'a, |
135 {tuple_func: tuple -> 'a -> 'a, |
137 tuple_set_func: tuple_set -> 'a -> 'a |
136 tuple_set_func: tuple_set -> 'a -> 'a} |
138 } |
|
139 |
137 |
140 val fold_tuple : 'a fold_tuple_funcs -> tuple -> 'a -> 'a |
138 val fold_tuple : 'a fold_tuple_funcs -> tuple -> 'a -> 'a |
141 val fold_tuple_set : 'a fold_tuple_funcs -> tuple_set -> 'a -> 'a |
139 val fold_tuple_set : 'a fold_tuple_funcs -> tuple_set -> 'a -> 'a |
142 val fold_tuple_assign : 'a fold_tuple_funcs -> tuple_assign -> 'a -> 'a |
140 val fold_tuple_assign : 'a fold_tuple_funcs -> tuple_assign -> 'a -> 'a |
143 val fold_bound : |
141 val fold_bound : |
144 'a fold_expr_funcs -> 'a fold_tuple_funcs -> bound -> 'a -> 'a |
142 'a fold_expr_funcs -> 'a fold_tuple_funcs -> bound -> 'a -> 'a |
145 val fold_int_bound : 'a fold_tuple_funcs -> int_bound -> 'a -> 'a |
143 val fold_int_bound : 'a fold_tuple_funcs -> int_bound -> 'a -> 'a |
146 |
144 |
147 type problem = { |
145 type problem = |
148 comment: string, |
146 {comment: string, |
149 settings: setting list, |
147 settings: setting list, |
150 univ_card: int, |
148 univ_card: int, |
151 tuple_assigns: tuple_assign list, |
149 tuple_assigns: tuple_assign list, |
152 bounds: bound list, |
150 bounds: bound list, |
153 int_bounds: int_bound list, |
151 int_bounds: int_bound list, |
154 expr_assigns: expr_assign list, |
152 expr_assigns: expr_assign list, |
155 formula: formula} |
153 formula: formula} |
156 |
154 |
157 type raw_bound = n_ary_index * int list list |
155 type raw_bound = n_ary_index * int list list |
158 |
156 |
159 datatype outcome = |
157 datatype outcome = |
160 JavaNotInstalled | |
158 JavaNotInstalled | |
289 and expr_assign = |
287 and expr_assign = |
290 AssignFormulaReg of int * formula | |
288 AssignFormulaReg of int * formula | |
291 AssignRelReg of n_ary_index * rel_expr | |
289 AssignRelReg of n_ary_index * rel_expr | |
292 AssignIntReg of int * int_expr |
290 AssignIntReg of int * int_expr |
293 |
291 |
294 type problem = { |
292 type problem = |
295 comment: string, |
293 {comment: string, |
296 settings: setting list, |
294 settings: setting list, |
297 univ_card: int, |
295 univ_card: int, |
298 tuple_assigns: tuple_assign list, |
296 tuple_assigns: tuple_assign list, |
299 bounds: bound list, |
297 bounds: bound list, |
300 int_bounds: int_bound list, |
298 int_bounds: int_bound list, |
301 expr_assigns: expr_assign list, |
299 expr_assigns: expr_assign list, |
302 formula: formula} |
300 formula: formula} |
303 |
301 |
304 type raw_bound = n_ary_index * int list list |
302 type raw_bound = n_ary_index * int list list |
305 |
303 |
306 datatype outcome = |
304 datatype outcome = |
307 JavaNotInstalled | |
305 JavaNotInstalled | |
311 Interrupted of int list option | |
309 Interrupted of int list option | |
312 Error of string * int list |
310 Error of string * int list |
313 |
311 |
314 exception SYNTAX of string * string |
312 exception SYNTAX of string * string |
315 |
313 |
316 type 'a fold_expr_funcs = { |
314 type 'a fold_expr_funcs = |
317 formula_func: formula -> 'a -> 'a, |
315 {formula_func: formula -> 'a -> 'a, |
318 rel_expr_func: rel_expr -> 'a -> 'a, |
316 rel_expr_func: rel_expr -> 'a -> 'a, |
319 int_expr_func: int_expr -> 'a -> 'a |
317 int_expr_func: int_expr -> 'a -> 'a} |
320 } |
|
321 |
318 |
322 (** Auxiliary functions on ML representation of Kodkod problems **) |
319 (** Auxiliary functions on ML representation of Kodkod problems **) |
323 |
320 |
324 fun fold_formula (F : 'a fold_expr_funcs) formula = |
321 fun fold_formula (F : 'a fold_expr_funcs) formula = |
325 case formula of |
322 case formula of |
417 case assign of |
414 case assign of |
418 AssignFormulaReg (x, f) => fold_formula F (FormulaReg x) #> fold_formula F f |
415 AssignFormulaReg (x, f) => fold_formula F (FormulaReg x) #> fold_formula F f |
419 | AssignRelReg (x, r) => fold_rel_expr F (RelReg x) #> fold_rel_expr F r |
416 | AssignRelReg (x, r) => fold_rel_expr F (RelReg x) #> fold_rel_expr F r |
420 | AssignIntReg (x, i) => fold_int_expr F (IntReg x) #> fold_int_expr F i |
417 | AssignIntReg (x, i) => fold_int_expr F (IntReg x) #> fold_int_expr F i |
421 |
418 |
422 type 'a fold_tuple_funcs = { |
419 type 'a fold_tuple_funcs = |
423 tuple_func: tuple -> 'a -> 'a, |
420 {tuple_func: tuple -> 'a -> 'a, |
424 tuple_set_func: tuple_set -> 'a -> 'a |
421 tuple_set_func: tuple_set -> 'a -> 'a} |
425 } |
|
426 |
422 |
427 fun fold_tuple (F : 'a fold_tuple_funcs) = #tuple_func F |
423 fun fold_tuple (F : 'a fold_tuple_funcs) = #tuple_func F |
428 fun fold_tuple_set F tuple_set = |
424 fun fold_tuple_set F tuple_set = |
429 case tuple_set of |
425 case tuple_set of |
430 TupleUnion (ts1, ts2) => fold_tuple_set F ts1 #> fold_tuple_set F ts2 |
426 TupleUnion (ts1, ts2) => fold_tuple_set F ts1 #> fold_tuple_set F ts2 |