Source

ocaml-lib / setset.ml


type ('a,'b) t = Add of (('a * ('a,'b) t * ('a,'b) t) * 'b option) | Empty of 'b option

let yss_vopt : ('a,'b) t -> ('a,'b) t * 'b option =
  function
  | Empty vopt -> Empty None, vopt
  | Add (y,vopt) -> Add (y,None), vopt

let empty : ('a,'b) t = Empty None

let rec singleton : 'a LSet.t -> 'b -> ('a,'b) t =
  fun xs v ->
    match xs with
    | [] -> Empty (Some v)
    | x::xs -> Add ((x,singleton xs v,empty), None)

(*
let rec add : ('b -> 'b -> 'b) -> 'a LSet.t -> 'b -> ('a,'b) t -> ('a,'b) t =
  fun u xs v yss ->
    match xs, yss with
    | _, Empty vopt ->
       singleton xs v
    | [], Add (y, vopt) ->
       Add (y, Some v)
    | x::xs1, Add ((y,yss1,yss2), vopt) ->
       let c = compare x y in
       if c = 0 then Add ((y,add u xs1 v yss1,yss2), vopt)
       else if c < 0 then
         let yss', vopt' = yss_vopt yss in
         Add ((x,singleton xs1 v,yss'), vopt')
       else
         let yss2', vopt' = yss_vopt (add u xs v yss2) in
         Add ((y,yss1,yss2'), add_vopt u vopt vopt')
and add_vopt u vopt1 vopt2 =
  match vopt1, vopt2 with
  | None, _ -> vopt2
  | _, None -> vopt1
  | Some v1, Some v2 -> Some (u v1 v2)
*)

let rec find : ('a,'b) t -> 'a LSet.t -> 'b (* raise Not_found *) =
  fun yss xs ->
    match xs, yss with
    | [], Empty vopt -> find_vopt vopt
    | [], Add (y, vopt) -> find_vopt vopt
    | x::xs1, Empty vopt -> raise Not_found
    | x::xs1, Add ((y,yss1,yss2), vopt) ->
        let c = compare x y in
        if c = 0 then find yss1 xs1
        else if c < 0 then raise Not_found
        else (* c > 0 *) find yss2 xs
and find_vopt = function
  | None -> raise Not_found
  | Some v -> v

let mem : ('a,'b) t -> 'a LSet.t -> bool =
  fun yss xs ->
    try ignore (find yss xs); true
    with Not_found -> true

let rec exists_contained : ('a,'b) t -> 'a LSet.t -> ('a LSet.t -> 'b -> bool) -> bool =
  fun yss xs p -> exists_contained2 yss xs p []
and exists_contained2 yss xs p ys =
  match xs, yss with
  | _, Empty vopt
  | [], Add (_, vopt) -> exists_contained_vopt p ys vopt
  | x::xs1, Add ((y,yss1,yss2), vopt) ->
      let c = compare x y in
      if c = 0 then
        (exists_contained_vopt p ys vopt) or
        (exists_contained2 yss2 xs1 p ys) or
        (exists_contained2 yss1 xs1 p (ys@[y]))
      else if c < 0 then exists_contained2 yss xs1 p ys
      else (* c > 0 *)
        (exists_contained_vopt p ys vopt) or
        (exists_contained2 yss2 xs p ys)
and exists_contained_vopt p ys vopt =
  match vopt with
  | None -> false
  | Some v -> p ys v

let rec union : ('b -> 'b -> 'b) -> ('a,'b) t -> ('a,'b) t -> ('a,'b) t =
  fun u yss1 yss2 ->
    match yss1, yss2 with
    | Empty vopt1, Empty vopt2 -> Empty (union_vopt u vopt1 vopt2)
    | Empty vopt1, Add (y2, vopt2) -> Add (y2, union_vopt u vopt1 vopt2)
    | Add (y1, vopt1), Empty vopt2 -> Add (y1, union_vopt u vopt1 vopt2)
    | Add ((y1,yss11,yss21), vopt1), Add ((y2,yss12,yss22), vopt2) ->
        let c = compare y1 y2 in
        if c = 0 then
          let yss', vopt' = yss_vopt (union u yss21 yss22) in
          Add ((y1,union u yss11 yss12,yss'), union_vopt u (union_vopt u vopt1 vopt2) vopt')
        else if c < 0 then
          let yss', vopt' = yss_vopt (union u yss21 yss2) in
          Add ((y1,yss11,yss'), union_vopt u vopt1 vopt')
        else (* c > 0 *)
          let yss', vopt' = yss_vopt (union u yss1 yss22) in
          Add ((y2,yss12,yss'), union_vopt u vopt2 vopt')
and union_vopt u vopt1 vopt2 =
  match vopt1, vopt2 with
  | None, vopt2 -> vopt2
  | vopt1, None -> vopt1
  | Some v1, Some v2 -> Some (u v1 v2)

let add : ('b -> 'b -> 'b) -> 'a LSet.t -> 'b -> ('a,'b) t -> ('a,'b) t =
  fun u xs v yss ->
    union u (singleton xs v) yss

(* max_subtract yss1 yss2 = {ys1 in yss1 | not exists ys2 in yss2: ys1 included in ys2} *)
(* Assumption: Max yss1 = yss1 *)
let rec max_subtract : ('a,'b) t -> ('a,'b) t -> ('a,'b) t =
  fun yss1 yss2 ->
    match yss1, yss2 with
    | Empty vopt1, Empty vopt2 -> Empty (max_subtract_vopt vopt1 vopt2)
    | Empty vopt1, Add (y2,vopt2) -> Empty None
    | Add (y1,vopt1), Empty vopt2 -> Add (y1, None)
    | Add ((y1,yss11,yss21), vopt1), Add ((y2,yss12,yss22), vopt2) ->
        let c = compare y1 y2 in
        if c = 0 then
          match max_subtract yss11 yss12, max_subtract (max_subtract yss21 yss22) yss12 with
          | Empty None, Empty None -> Empty None
          | yss1', yss2' -> Add ((y1,yss1',yss2'), None)
        else if c < 0 then Add ((y1,yss11,max_subtract yss21 yss2), None)
        else (* c > 0 *) max_subtract (max_subtract yss1 yss22) yss12
and max_subtract_vopt vopt1 vopt2 =
  match vopt1, vopt2 with
  | Some v1, None -> Some v1
  | _, _ -> None

(* max_union yss1 yss2 = Max (Union yss1 yss2) *)
(* Assumption: Max yss1 = yss1, Max yss2 = yss2 *)
let rec max_union : ('b -> 'b -> 'b) -> ('a,'b) t -> ('a,'b) t -> ('a,'b) t =
  fun u yss1 yss2 ->
    match yss1, yss2 with
    | Empty vopt1, Empty vopt2 -> Empty (max_union_vopt u vopt1 vopt2)
    | Empty vopt1, Add (y2, vopt2) -> Add (y2, None)
    | Add (y1, vopt1), Empty vopt2 -> Add (y1, None)
    | Add ((y1,yss11,yss21), vopt1), Add ((y2,yss12,yss22), vopt2) ->
        let c = compare y1 y2 in
        if c = 0 then
          let yss', vopt' = yss_vopt (max_union u (max_subtract yss21 yss12) (max_subtract yss22 yss11)) in
          Add ((y1,max_union u yss11 yss12,yss'), vopt')
        else if c < 0 then
          let yss', vopt' = yss_vopt (max_union u yss21 (max_subtract yss2 yss11)) in
          Add ((y1,yss11,yss'), vopt')
        else (* c > 0 *)
          let yss', vopt' = yss_vopt (max_union u (max_subtract yss1 yss12) yss22) in
          Add ((y2,yss12,yss'), vopt')
and max_union_vopt u vopt1 vopt2 =
  match vopt1, vopt2 with
  | None, vopt2 -> vopt2
  | vopt1, None -> vopt1
  | Some v1, Some v2 -> Some (u v1 v2)

let max_add : ('b -> 'b -> 'b) -> 'a LSet.t -> 'b -> ('a,'b) t -> ('a,'b) t =
  fun u xs v yss ->
    max_union u (singleton xs v) yss

let rec from_list : ('b -> 'b -> 'b) -> ('a LSet.t * 'b) list -> ('a,'b) t =
  fun u -> function
  | [] -> empty
  | (x,v)::l -> add u x v (from_list u l)

let rec fold : ('a LSet.t -> 'b -> 'c -> 'c) -> ('a,'b) t -> 'c -> 'c =
  fun f yss e -> fold2 f yss e []
and fold2 f yss e ys =
  match yss with
  | Empty vopt -> 
      fold_vopt f vopt e ys
  | Add ((y,yss1,yss2),vopt) ->
      let e1 = fold2 f yss1 e (ys@[y]) in
      let e2 = fold2 f yss2 e1 ys in
      fold_vopt f vopt e2 ys
and fold_vopt f vopt e ys =
  match vopt with
  | None -> e
  | Some v -> f ys v e

let rec mapfilter : ('a LSet.t -> 'b -> 'c option) -> ('a,'b) t -> ('a,'c) t =
  fun f yss -> mapfilter2 f yss []
and mapfilter2 f yss ys =
  match yss with
  | Empty vopt -> Empty (mapfilter_vopt f vopt ys)
  | Add ((y,yss1,yss2), vopt) ->
      let vopt' = mapfilter_vopt f vopt ys in
      match mapfilter2 f yss1 (ys@[y]), mapfilter2 f yss2 ys with
      | Empty None, Empty None -> Empty vopt'
      | yss1', yss2' -> Add ((y,yss1',yss2'), vopt')
and mapfilter_vopt f vopt ys =
  match vopt with
  | None -> None
  | Some v -> f ys v



let rec map_inter : ('a LSet.t -> 'b -> 'a LSet.t -> 'b option) -> ('b -> 'b -> 'b) -> ('a,'b) t -> 'a LSet.t -> ('a,'b) t =
  fun f u yss xs -> map_inter2 f u yss xs [] []
and map_inter2 f u yss xs ys ys' =
  match xs, yss with
  | _, Empty vopt -> Empty (map_inter_vopt f vopt ys ys')
  | [], Add ((y,yss1,yss2), vopt) ->
     let yss1' = map_inter2 f u yss1 xs (ys@[y]) ys' in
     let yss2' = map_inter2 f u yss2 xs ys ys' in
     let vopt' = map_inter_vopt f vopt ys ys' in
     union u (Empty vopt') (union u yss1' yss2')
  | x::xs1, Add ((y,yss1,yss2), vopt) ->
     let c = compare x y in
     if c = 0 then
       let yss1' = map_inter2 f u yss1 xs1 (ys@[y]) (ys'@[y]) in
       let yss2', vopt'' = yss_vopt (map_inter2 f u yss2 xs1 ys ys') in
       let vopt' = map_inter_vopt f vopt ys ys' in
       Add ((y,yss1',yss2'), union_vopt u vopt' vopt'')
     else if c < 0 then map_inter2 f u yss xs1 ys ys'
     else (* c > 0 *)
       let yss1' = map_inter2 f u yss1 xs (ys@[y]) ys' in
       let yss2' = map_inter2 f u yss2 xs ys ys' in
       let vopt' = map_inter_vopt f vopt ys ys' in
       union u (Empty vopt') (union u yss1' yss2')
and map_inter_vopt f vopt ys ys' =
  match vopt with
  | None -> None
  | Some v -> f ys v ys'

let rec fold_inter : ('a LSet.t -> 'b -> 'a LSet.t -> 'c -> 'c) -> ('a,'b) t -> 'a LSet.t -> 'c -> 'c =
  fun f yss xs e -> fold_inter2 f yss xs e [] []
and fold_inter2 f yss xs e ys ys' =
  match xs, yss with
  | _, Empty vopt -> fold_inter_vopt f vopt e ys ys'
  | [], Add ((y,yss1,yss2), vopt) ->
     let e1 = fold_inter2 f yss1 xs e (ys@[y]) ys' in
     let e2 = fold_inter2 f yss2 xs e1 ys ys' in
     fold_inter_vopt f vopt e2 ys ys'
  | x::xs1, Add ((y,yss1,yss2), vopt) ->
     let c = compare x y in
     if c = 0 then
       let e1 = fold_inter2 f yss1 xs1 e (ys@[y]) (ys'@[y]) in
       let e2 = fold_inter2 f yss2 xs1 e1 ys ys' in
       fold_inter_vopt f vopt e2 ys ys'
     else if c < 0 then fold_inter2 f yss xs1 e ys ys'
     else (* c > 0 *)
       let e1 = fold_inter2 f yss1 xs e (ys@[y]) ys' in
       let e2 = fold_inter2 f yss2 xs e1 ys ys' in
       fold_inter_vopt f vopt e2 ys ys'
and fold_inter_vopt f vopt e ys ys' =
  match vopt with
  | None -> e
  | Some v -> f ys v ys' e