equal
deleted
inserted
replaced
19 datatype ostate = Complete | Incomplete | Inconsistent |
19 datatype ostate = Complete | Incomplete | Inconsistent |
20 type specify_data |
20 type specify_data |
21 type solve_data |
21 type solve_data |
22 datatype ppobj = PblObj of specify_data | PrfObj of solve_data |
22 datatype ppobj = PblObj of specify_data | PrfObj of solve_data |
23 datatype ctree = EmptyPtree | Nd of ppobj * ctree list |
23 datatype ctree = EmptyPtree | Nd of ppobj * ctree list |
|
24 |
|
25 val rep_solve_data: ppobj -> solve_data |
|
26 val rep_specify_data: ppobj -> specify_data |
24 |
27 |
25 (** basic functions **) |
28 (** basic functions **) |
26 val e_ctree : ctree (* TODO: replace by EmptyPtree*) |
29 val e_ctree : ctree (* TODO: replace by EmptyPtree*) |
27 val existpt' : Pos.pos' -> ctree -> bool |
30 val existpt' : Pos.pos' -> ctree -> bool |
28 val is_interpos : Pos.pos' -> bool |
31 val is_interpos : Pos.pos' -> bool |
223 EmptyPtree |
226 EmptyPtree |
224 | Nd of ppobj * (ctree list); |
227 | Nd of ppobj * (ctree list); |
225 val e_ctree = EmptyPtree; |
228 val e_ctree = EmptyPtree; |
226 type state = ctree * pos' |
229 type state = ctree * pos' |
227 val e_state = (EmptyPtree , e_pos') |
230 val e_state = (EmptyPtree , e_pos') |
|
231 |
|
232 fun rep_solve_data (PrfObj solve_data) = solve_data |
|
233 | rep_solve_data _ = raise ERROR "rep_solve_data ONLY for solve_data" |
|
234 fun rep_specify_data (PblObj specify_data) = specify_data |
|
235 | rep_specify_data _ = raise ERROR "rep_solve_data ONLY for solve_data" |
228 |
236 |
229 |
237 |
230 (*** minimal set of functions on Ctree* **) |
238 (*** minimal set of functions on Ctree* **) |
231 |
239 |
232 fun is_pblobj (PblObj _) = true |
240 fun is_pblobj (PblObj _) = true |