Modified ocaml backend to use ocamlfind for linksem and lem

Fixed test cases for ocaml backend and interpreter

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