(*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 *)