/[svn]/misc/bool.ml
ViewVC logotype

Diff of /misc/bool.ml

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 274 by abate, Tue Jul 10 17:21:20 2007 UTC revision 275 by abate, Tue Jul 10 17:21:31 2007 UTC
# Line 51  Line 51 
51      match (a,b) with      match (a,b) with
52        | Split (h1,x1, p1,i1,n1), Split (h2,x2, p2,i2,n2) ->        | Split (h1,x1, p1,i1,n1), Split (h2,x2, p2,i2,n2) ->
53            (h1 == h2) &&            (h1 == h2) &&
54            (X.equal x1 x2) && (equal p1 p2) & (equal i1 i2) &&            (equal p1 p2) && (equal i1 i2) &&
55            (equal n1 n2)            (equal n1 n2) && (X.equal x1 x2)
56        | _ -> false        | _ -> false
57    
58    (* Idea: add a mutable "unique" identifier and set it to
59       the minimum of the two when egality ... *)
60    
61    
62    let rec compare a b =    let rec compare a b =
63      if (a == b) then 0      if (a == b) then 0
64      else match (a,b) with      else match (a,b) with
# Line 133  Line 137 
137      | True -> (pos,neg) :: accu      | True -> (pos,neg) :: accu
138      | False -> accu      | False -> accu
139      | Split (_,x, p,i,n) ->      | Split (_,x, p,i,n) ->
140            (*OPT: can avoid creating this list cell when pos or neg =False *)
141          let accu = get accu (x::pos) neg p in          let accu = get accu (x::pos) neg p in
142          let accu = get accu pos (x::neg) n in          let accu = get accu pos (x::neg) n in
143          let accu = get accu pos neg i in          let accu = get accu pos neg i in
# Line 175  Line 180 
180     - no ``subsumption'     - no ``subsumption'
181  *)  *)
182    
183      let rec simplify a b =
184        if equal a b then False
185        else match (a,b) with
186          | False,_ | _, True -> False
187          | a, False -> a
188          | True, _ -> True
189          | Split (_,x1,p1,i1,n1), Split (_,x2,p2,i2,n2) ->
190              let c = X.compare x1 x2 in
191              if c = 0 then
192                let p1' = simplify (simplify p1 i2) p2
193                and i1' = simplify i1 i2
194                and n1' = simplify (simplify n1 i2) n2 in
195                if (p1 != p1') || (n1 != n1') || (i1 != i1')
196                then split x1 p1' i1' n1'
197                else a
198              else if c > 0 then
199                simplify a i2
200              else
201                let p1' = simplify p1 b
202                and i1' = simplify i1 b
203                and n1' = simplify n1 b in
204                if (p1 != p1') || (n1 != n1') || (i1 != i1')
205                then split x1 p1' i1' n1'
206                else a
207    (*
208    let rec simplify a l =    let rec simplify a l =
209      if (a = False) then False else simpl_aux1 a [] l      if (a = False) then False else simpl_aux1 a [] l
210    and simpl_aux1 a accu = function    and simpl_aux1 a accu = function
# Line 209  Line 239 
239            simpl_aux2 x p i n (b :: ap) (b :: ai) (b :: an) l            simpl_aux2 x p i n (b :: ap) (b :: ai) (b :: an) l
240          else          else
241            simpl_aux2 x p i n (p2 :: i2 :: ap) (i2 :: ai) (n2 :: i2 :: an) l            simpl_aux2 x p i n (p2 :: i2 :: ap) (i2 :: ai) (n2 :: i2 :: an) l
242    *)
243    
244    let split x p i n =    let split x p i n =
245      split x (simplify p [i]) i (simplify n [i])      split x (simplify p i) i (simplify n i)
246    
247    let rec ( ++ ) a b =    let rec ( ++ ) a b =
248  (*    if equal a b then a *)  (*    if equal a b then a *)
Legend:
Removed from v.274  
changed lines
  Added in v.275
CVS Admin">CVS Admin
 ViewVC Help
Powered by ViewVC 1.1.5