diff options
Diffstat (limited to 'lib/ocaml_rts/linksem/multimap.ml')
| -rw-r--r-- | lib/ocaml_rts/linksem/multimap.ml | 215 |
1 files changed, 0 insertions, 215 deletions
diff --git a/lib/ocaml_rts/linksem/multimap.ml b/lib/ocaml_rts/linksem/multimap.ml deleted file mode 100644 index 5ba51824..00000000 --- a/lib/ocaml_rts/linksem/multimap.ml +++ /dev/null @@ -1,215 +0,0 @@ -(*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 *) - |