Source file multimap.ml

(*Generated by Lem from multimap.lem.*)
open Lem_bool 
open Lem_basic_classes 
open Lem_maybe 
open Lem_function 
open Lem_num 
open Lem_list
open Lem_set
open Lem_set_extra
open Lem_assert_extra
open Missing_pervasives
open Lem_string
open Show

(* HMM. Is the right thing instead to implement multiset first? Probably. *)

(* This is a set of pairs
 * augmented with operations implementing a particular kind of 
 * map.
 * 
 * This map differs from the Lem map in the following ways.
 * 
 * 0. The basic idea: it's a multimap, so a single key, supplied as a "query",
 *    can map to many (key, value) results.
 *    But PROBLEM: how do we store them in a tree? We're using OCaml's
 *    Set implementation underneath, and that doesn't allow duplicates.
 * 
 * 1. ANSWER: require keys still be unique, but that the user supplies an 
 *    equivalence relation on them, which
 *    is coarser-grained than the ordering relation
 *    used to order the set. It must be consistent with it, though: 
 *    equivalent keys should appear as a contiguous range in the 
 *    ordering.
 * 
 * 2. This allows many "non-equal" keys, hence present independently
 *    in the set of pairs, to be "equivalent" for the purposes of a 
 *    query.
 * 
 * 3. The coarse-grained equivalence relation can be supplied on a 
 *    per-query basis, meaning that different queries on the same
 *    set can query by finer or coarser criteria (while respecting 
 *    the requirement to be consistent with the ordering).
 * 
 * Although this seems more complicated than writing a map from 
 * k to list (k, v), which would allow us to ditch the finer ordering, 
 * it scales better (no lists) and allows certain range queries which 
 * would be harder to implement under that approach. It also has the 
 * nice property that the inverse multimap is represented as the same
 * set but with the pairs reversed.
 *)

type( 'k, 'v) multimap = ('k * 'v) Pset.set

(* In order for bisection search within a set to work, 
 * we need the equivalence class to tell us whether we're less than or
 * greater than the members of the key's class. 
 * It effectively identifies a set of ranges. *)
type 'k key_equiv = 'k -> 'k -> bool

(*
val hasMapping : forall 'k 'v. key_equiv 'k -> multimap 'k 'v -> bool
let inline hasMapping equiv m =
*)

(*
val mappingCount : forall 'k 'v. key_equiv 'k -> multimap 'k 'v -> natural
val any : forall 'k 'v. ('k -> 'v -> bool) -> multimap 'k 'v -> bool 
val all : forall 'k 'v. ('k -> 'v -> bool) -> multimap 'k 'v -> bool 
*)
(*val findLowestKVWithKEquivTo : forall 'k 'v. 
    Ord 'k, Ord 'v, SetType 'k, SetType 'v =>
        'k 
        -> key_equiv 'k 
        -> multimap 'k 'v 
        -> maybe ('k * 'v) 
        -> maybe ('k * 'v)*)
let rec findLowestKVWithKEquivTo dict_Basic_classes_Ord_k dict_Basic_classes_Ord_v dict_Basic_classes_SetType_k dict_Basic_classes_SetType_v k equiv subSet maybeBest:('k*'v)option= 
     ((match Pset.choose_and_split subSet with
        None -> (* empty subset *) maybeBest
      | Some(lower, ((chosenK: 'k), (chosenV : 'v)), higher) ->
            (* is k equiv to chosen? *)
            if equiv k chosenK
            then
                (* is chosen less than our current best? *)
                let (bestK, bestV) = ((match maybeBest with
                    None -> (chosenK, chosenV)
                    | Some(currentBestK, currentBestV) -> 
                        if pairLess 
  dict_Basic_classes_Ord_v dict_Basic_classes_Ord_k (chosenK, chosenV) (currentBestK, currentBestV)
                            then (chosenK, chosenV)
                            else (currentBestK, currentBestV)
                ))
                in
                (* recurse down lower subSet; best is whichever is lower *)
                findLowestKVWithKEquivTo 
  dict_Basic_classes_Ord_k dict_Basic_classes_Ord_v dict_Basic_classes_SetType_k dict_Basic_classes_SetType_v k equiv lower (Some(bestK, bestV))
            else
                (* k is not equiv to chosen; do we need to look lower or higher? *)
                if  dict_Basic_classes_Ord_k.isLess_method k chosenK
                then
                    (* k is lower, so look lower for equivs-to-k *)
                    findLowestKVWithKEquivTo 
  dict_Basic_classes_Ord_k dict_Basic_classes_Ord_v dict_Basic_classes_SetType_k dict_Basic_classes_SetType_v k equiv lower maybeBest
                else
                    (* k is higher *)
                    findLowestKVWithKEquivTo 
  dict_Basic_classes_Ord_k dict_Basic_classes_Ord_v dict_Basic_classes_SetType_k dict_Basic_classes_SetType_v k equiv higher maybeBest
    ))

(*val testEquiv : natural -> natural -> bool*)
let testEquiv x y:bool=  (if ( Nat_big_num.greater_equal x( (Nat_big_num.of_int 3)) && (Nat_big_num.less x( (Nat_big_num.of_int 5)) && (Nat_big_num.greater_equal y( (Nat_big_num.of_int 3)) && Nat_big_num.less_equal y( (Nat_big_num.of_int 5))))) then true
     else if ( Nat_big_num.less x( (Nat_big_num.of_int 3)) && Nat_big_num.less y( (Nat_big_num.of_int 3))) then true
     else if ( Nat_big_num.greater x( (Nat_big_num.of_int 5)) && Nat_big_num.greater y( (Nat_big_num.of_int 5))) then true
     else false)

         (*
assert lowest_simple: findLowestKVWithKEquivTo 4 testEquiv 
({ (1, 0); (2, 0); (3, 0); (4, 0); (5, 0); (6, 0) } : set (natural * natural)) Nothing = Just (3, 0)
assert lowest_kv: findLowestKVWithKEquivTo 4 testEquiv 
({ (1, 0); (2, 0); (3, 0); (3, 1); (4, 0); (5, 0); (6, 0) } : set (natural * natural)) Nothing = Just (3, 0)
assert lowest_empty: findLowestKVWithKEquivTo 4 testEquiv
({} : set (natural * natural)) Nothing = Nothing
assert lowest_onepast: findLowestKVWithKEquivTo 4 testEquiv
({ (6, 0) } : set (natural * natural)) Nothing = Nothing
assert lowest_oneprev: findLowestKVWithKEquivTo 4 testEquiv 
({ (2, 0) } : set (natural * natural)) Nothing = Nothing
          *)
         
(* Note we can't just use findLowestEquiv with inverted relations, because 
 * chooseAndSplit returns us (lower, chosen, higher) and we need to swap
 * around how we consume that. *)
(*val findHighestKVWithKEquivTo : forall 'k 'v. 
    Ord 'k, Ord 'v, SetType 'k, SetType 'v =>
        'k 
        -> key_equiv 'k 
        -> multimap 'k 'v 
        -> maybe ('k * 'v) 
        -> maybe ('k * 'v)*)
let rec findHighestKVWithKEquivTo dict_Basic_classes_Ord_k dict_Basic_classes_Ord_v dict_Basic_classes_SetType_k dict_Basic_classes_SetType_v k equiv subSet maybeBest:('k*'v)option= 
     ((match Pset.choose_and_split subSet with
        None -> (* empty subset *) maybeBest
      | Some(lower, ((chosenK: 'k), (chosenV : 'v)), higher) ->
            (* is k equiv to chosen? *)
            if equiv k chosenK
            then
                (* is chosen greater than our current best? *)
                let (bestK, bestV) = ((match maybeBest with
                    None -> (chosenK, chosenV)
                    | Some(currentBestK, currentBestV) -> 
                        if pairGreater 
  dict_Basic_classes_Ord_k dict_Basic_classes_Ord_v (chosenK, chosenV) (currentBestK, currentBestV)
                            then (chosenK, chosenV)
                            else (currentBestK, currentBestV)
                ))
                in
                (* recurse down higher-than-chosen subSet; best is whichever is higher *)
                findHighestKVWithKEquivTo 
  dict_Basic_classes_Ord_k dict_Basic_classes_Ord_v dict_Basic_classes_SetType_k dict_Basic_classes_SetType_v k equiv higher (Some(bestK, bestV))
            else
                (* k is not equiv to chosen; do we need to look lower or higher? 
                 * NOTE: the pairs in the set must be lexicographically ordered! *)
                if  dict_Basic_classes_Ord_k.isGreater_method k chosenK
                then
                    (* k is higher than chosen, so look higher for equivs-to-k *)
                    findHighestKVWithKEquivTo 
  dict_Basic_classes_Ord_k dict_Basic_classes_Ord_v dict_Basic_classes_SetType_k dict_Basic_classes_SetType_v k equiv higher maybeBest
                else
                    (* k is lower than chosen, so look lower *)
                    findHighestKVWithKEquivTo 
  dict_Basic_classes_Ord_k dict_Basic_classes_Ord_v dict_Basic_classes_SetType_k dict_Basic_classes_SetType_v k equiv lower maybeBest
    ))

(*
let _ = Missing_pervasives.errln ("choose_and_split {3, 4, 5} is " ^ 
    (match Set_extra.chooseAndSplit ({3;4;5} : set natural)
     with Just (l, m, r) -> (show (toList l, m, toList r))
     | Nothing -> "Nothing" end))
*)

  (*
assert highest_simple: findHighestKVWithKEquivTo 4 testEquiv
({ (1, 0); (2, 0); (3, 0); (4, 0); (5, 0); (6, 0) } : set (natural * natural)) Nothing = Just (5, 0)
assert highest_kv: findHighestKVWithKEquivTo 4 testEquiv
({ (1, 0); (2, 0); (3, 0); (4, 0); (5, 0); (5, 1); (6, 0) } : set (natural * natural)) Nothing = Just (5, 1)
assert highest_empty: findHighestKVWithKEquivTo 4 testEquiv
({} : set (natural * natural)) Nothing = Nothing
assert highest_onepast: findHighestKVWithKEquivTo 4 testEquiv 
({ (6, 0) } : set (natural * natural)) Nothing = Nothing
assert highest_oneprev: findHighestKVWithKEquivTo 4 testEquiv
({ (2, 0) } : set (natural * natural)) Nothing = Nothing
   *)
  
(* get the list of all pairs with key equiv to k. *)
(*val lookupBy : forall 'k 'v. 
    Ord 'k, Ord 'v, SetType 'k, SetType 'v =>
        key_equiv 'k -> 'k -> multimap 'k 'v -> list ('k * 'v)*)
let lookupBy0 dict_Basic_classes_Ord_k dict_Basic_classes_Ord_v dict_Basic_classes_SetType_k dict_Basic_classes_SetType_v equiv k m:('k*'v)list=
     ( 
    (* Find the lowest and highest elements equiv to k. 
     * We do this using chooseAndSplit recursively. *)(match findLowestKVWithKEquivTo 
  dict_Basic_classes_Ord_k dict_Basic_classes_Ord_v dict_Basic_classes_SetType_k dict_Basic_classes_SetType_v k equiv m None with
        None -> []
        | Some lowestEquiv -> 
            let (highestEquiv : ('k * 'v)) =
                ( 
                (* We can't just invert the relation on the set, because
                 * the whole set is ordered *)(match findHighestKVWithKEquivTo 
  dict_Basic_classes_Ord_k dict_Basic_classes_Ord_v dict_Basic_classes_SetType_k dict_Basic_classes_SetType_v k equiv m None with
                    None -> failwith "impossible: lowest equiv but no highest equiv"
                    | Some highestEquiv -> highestEquiv
                ))
        in
        (* FIXME: split is currently needlessly inefficient on OCaml! *)
        let (lowerThanLow, highEnough) = (Lem_set.split 
  (instance_Basic_classes_SetType_tup2_dict dict_Basic_classes_SetType_k
     dict_Basic_classes_SetType_v) (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_k
   dict_Basic_classes_Ord_v) lowestEquiv m)
        in 
        let (wanted, tooHigh) = (Lem_set.split 
  (instance_Basic_classes_SetType_tup2_dict dict_Basic_classes_SetType_k
     dict_Basic_classes_SetType_v) (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_k
   dict_Basic_classes_Ord_v) highestEquiv highEnough)
        in 
        (* NOTE that lowestEquiv is a single element; we want to include 
         * *all those equiv to it*, which may be non-equal. FIXME: use splitMember,
         * although that needs fixing in Lem (plus an optimised OCaml version). *)
        List.rev_append (List.rev (List.rev_append (List.rev (Pset.elements (let x2 =(Pset.from_list (pairCompare  
  dict_Basic_classes_SetType_k.setElemCompare_method  dict_Basic_classes_SetType_v.setElemCompare_method) []) in  Pset.fold
   (fun s x2 ->
    if Lem.orderingEqual 0
         (pairCompare dict_Basic_classes_Ord_k.compare_method
            dict_Basic_classes_Ord_v.compare_method s lowestEquiv) then
      Pset.add s x2 else x2) m x2))) (Pset.elements wanted))) (
            (* don't include the lowest and highest twice, if they're the same *)
            if pairLess 
  dict_Basic_classes_Ord_v dict_Basic_classes_Ord_k lowestEquiv highestEquiv then (Pset.elements (let x2 =(Pset.from_list (pairCompare  
  dict_Basic_classes_SetType_k.setElemCompare_method  dict_Basic_classes_SetType_v.setElemCompare_method) []) in  Pset.fold
   (fun s x2 ->
    if Lem.orderingEqual 0
         (pairCompare dict_Basic_classes_Ord_k.compare_method
            dict_Basic_classes_Ord_v.compare_method s highestEquiv) then
      Pset.add s x2 else x2) m x2)) else []
        )
    ))

(*
let _ = Missing_pervasives.errln
("lookupBy testEquiv 4 { (1, 0); (2, 0); (3, 0); (4, 0); (5, 0); (6, 0) } is : "
^ (show (lookupBy testEquiv 
4 ({ (1, 0); (2, 0); (3, 0); (4, 0); (5, 0); (6, 0) } : set (natural * natural)))))
*)
(*
assert lookup_simple : lookupBy testEquiv 
4 ({ (1, 0); (2, 0); (3, 0); (4, 0); (5, 0); (6, 0) } : set (natural * natural))
= ([(3, 0); (4, 0); (5, 0)] : list (natural * natural))
assert lookup_kv : lookupBy testEquiv 
4 ({ (1, 0); (2, 0); (3, 0); (4, 0); (4, 1); (5, 0); (6, 0) } : set (natural * natural))
= ([(3, 0); (4, 0); (4, 1); (5, 0)] : list (natural * natural))
assert lookup_empty: lookupBy testEquiv
4 ({} : set (natural * natural)) = ([]: list (natural * natural))
assert lookup_singleton: lookupBy testEquiv 
4 ({(5, 0)} : set (natural * natural)) = ([(5, 0)]: list (natural * natural))
assert lookup_onepast: lookupBy testEquiv
4 ({ (6, 0) } : set (natural * natural)) = ([] : list (natural * natural))
assert lookup_oneprev: lookupBy testEquiv 
4 ({ (2, 0) } : set (natural * natural)) = ([] : list (natural * natural))
*)

(* To delete all pairs with key equiv to k, can use deleteBy *)