diff options
Diffstat (limited to 'lib/ocaml_rts/linksem/multimap.ml')
| -rw-r--r-- | lib/ocaml_rts/linksem/multimap.ml | 215 |
1 files changed, 215 insertions, 0 deletions
diff --git a/lib/ocaml_rts/linksem/multimap.ml b/lib/ocaml_rts/linksem/multimap.ml new file mode 100644 index 00000000..5ba51824 --- /dev/null +++ b/lib/ocaml_rts/linksem/multimap.ml @@ -0,0 +1,215 @@ +(*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) + +(* 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 + )) + +(* 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 [] + ) + )) + + +(* To delete all pairs with key equiv to k, can use deleteBy *) + |