diff options
Diffstat (limited to 'lib/ocaml_rts/linksem/src_lem_library')
42 files changed, 0 insertions, 6310 deletions
diff --git a/lib/ocaml_rts/linksem/src_lem_library/bit.ml b/lib/ocaml_rts/linksem/src_lem_library/bit.ml deleted file mode 100644 index bd972008..00000000 --- a/lib/ocaml_rts/linksem/src_lem_library/bit.ml +++ /dev/null @@ -1,19 +0,0 @@ -type bit = Zero | One - -let to_bool b = match b with | Zero -> false | _ -> true -let bn b = match b with | Zero -> One | One -> Zero -let bor b1 b2 = match (b1,b2) with - | Zero,Zero -> Zero - | _ -> One -let xor b1 b2 = match (b1,b2) with - | Zero,Zero -> Zero - | Zero,One | One,Zero -> One - | _ -> Zero -let band b1 b2 = match (b1,b2) with - | One,One -> One - | _ -> Zero - -let add b1 b2 = match (b1,b2) with - | Zero,Zero -> Zero, false - | Zero,One | One,Zero -> One, false - | One,One -> Zero, true diff --git a/lib/ocaml_rts/linksem/src_lem_library/bit.mli b/lib/ocaml_rts/linksem/src_lem_library/bit.mli deleted file mode 100644 index a39c1a09..00000000 --- a/lib/ocaml_rts/linksem/src_lem_library/bit.mli +++ /dev/null @@ -1,8 +0,0 @@ -type bit = Zero | One - -val to_bool : bit -> bool -val bn : bit -> bit -val bor : bit -> bit -> bit -val xor : bit -> bit -> bit -val band : bit -> bit -> bit -val add : bit -> bit -> bit * bool diff --git a/lib/ocaml_rts/linksem/src_lem_library/either.ml b/lib/ocaml_rts/linksem/src_lem_library/either.ml deleted file mode 100644 index ddf1b214..00000000 --- a/lib/ocaml_rts/linksem/src_lem_library/either.ml +++ /dev/null @@ -1,24 +0,0 @@ -type ('a, 'b) either = - | Left of 'a - | Right of 'b - -let either_case fa fb x = match x with - | (Left a) -> fa a - | (Right b) -> fb b - -let eitherEqualBy eql eqr (left: ('a, 'b) either) (right: ('a, 'b) either) = - match (left, right) with - | ((Left l), (Left l')) -> eql l l' - | ((Right r), (Right r')) -> eqr r r' - | _ -> false - -let rec either_partition l = ((match l with - | [] -> ([], []) - | x :: xs -> begin - let (ll, rl) = (either_partition xs) in - (match x with - | (Left l) -> ((l::ll), rl) - | (Right r) -> (ll, (r::rl)) - ) - end -)) diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem.ml b/lib/ocaml_rts/linksem/src_lem_library/lem.ml deleted file mode 100644 index 2ff0090f..00000000 --- a/lib/ocaml_rts/linksem/src_lem_library/lem.ml +++ /dev/null @@ -1,103 +0,0 @@ -(* ========================================================================== *) -(* Tuples *) -(* ========================================================================== *) - - -let pair_equal eq1 eq2 (a1, b1) (a2, b2) = - (eq1 a1 a2) && (eq2 b1 b2) - -let pair_swap (v1, v2) = (v2, v1) - -let curry f v1 v2 = f (v1, v2) - -let uncurry f (v1, v2) = f v1 v2 - -(* ========================================================================== *) -(* Orderings *) -(* ========================================================================== *) - -let orderingIsLess r = (r < 0) -let orderingIsGreater r = (r > 0) -let orderingIsEqual r = (r = 0) - -let ordering_cases (r : int) (lt : 'a) (eq : 'a) (gt : 'a) : 'a = - (if (r < 0) then lt else - if (r = 0) then eq else gt) - -let orderingEqual r1 r2 = - ordering_cases r1 (orderingIsLess r2) (orderingIsEqual r2) (orderingIsGreater r2) - - -(* ========================================================================== *) -(* Lists *) -(* ========================================================================== *) - - -let list_null = function - | [] -> true - | _ -> false - -let rec lexicographic_compare cmp l1 l2 : int = (match (l1,l2) with - | ([], []) -> 0 - | ([], _::_) -> -1 - | (_::_, []) -> 1 - | (x::xs, y::ys) -> begin - ordering_cases (cmp x y) (-1) (lexicographic_compare cmp xs ys) (1) - end -) - -let rec lexicographic_less less less_eq l1 l2 = ((match (l1,l2) with - | ([], []) -> false - | ([], _::_) -> true - | (_::_, []) -> false - | (x::xs, y::ys) -> ((less x y) || ((less_eq x y) && (lexicographic_less less less_eq xs ys))) -)) - -let rec lexicographic_less_eq less less_eq l1 l2 = ((match (l1,l2) with - | ([], []) -> true - | ([], _::_) -> true - | (_::_, []) -> false - | (x::xs, y::ys) -> (less x y || (less_eq x y && lexicographic_less_eq less less_eq xs ys)) -)) - -let rec list_index l n = (match l with - | [] -> None - | x :: xs -> if n = 0 then (Some x) else list_index xs (n - 1) -) - - -(* ========================================================================== *) -(* Options *) -(* ========================================================================== *) - -let is_none = function - | None -> true - | Some _ -> false - -let is_some = function - | None -> false - | Some _ -> true - -let option_case d f mb = (match mb with - | Some a -> f a - | None -> d -) - -let option_default d = function - | Some a -> a - | None -> d - -let option_map f = function - | Some a -> Some (f a) - | None -> None - -let option_bind m f = - match m with - | Some a -> f a - | None -> None - -let option_equal eq o1 o2 = match (o1, o2) with - | (None, None) -> true - | (None, Some _) -> false - | (Some _, None) -> false - | (Some x1, Some x2) -> eq x1 x2 diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_assert_extra.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_assert_extra.ml deleted file mode 100644 index 3b4a1548..00000000 --- a/lib/ocaml_rts/linksem/src_lem_library/lem_assert_extra.ml +++ /dev/null @@ -1,28 +0,0 @@ -(*Generated by Lem from assert_extra.lem.*) - -open Xstring - -(* ------------------------------------ *) -(* failing with a proper error message *) -(* ------------------------------------ *) - -(*val failwith: forall 'a. string -> 'a*) - -(* ------------------------------------ *) -(* failing without an error message *) -(* ------------------------------------ *) - -(*val fail : forall 'a. 'a*) -(*let fail = failwith "fail"*) - -(* ------------------------------------- *) -(* assertions *) -(* ------------------------------------- *) - -(*val ensure : bool -> string -> unit*) -let ensure test msg = -(if test then - () - else - failwith msg) -;; diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_basic_classes.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_basic_classes.ml deleted file mode 100644 index 9f24e5fb..00000000 --- a/lib/ocaml_rts/linksem/src_lem_library/lem_basic_classes.ml +++ /dev/null @@ -1,323 +0,0 @@ -(*Generated by Lem from basic_classes.lem.*) -(******************************************************************************) -(* Basic Type Classes *) -(******************************************************************************) - -open Lem_bool - -(* ========================================================================== *) -(* Equality *) -(* ========================================================================== *) - -(* Lem`s default equality (=) is defined by the following type-class Eq. - This typeclass should define equality on an abstract datatype 'a. It should - always coincide with the default equality of Coq, HOL and Isabelle. - For OCaml, it might be different, since abstract datatypes like sets - might have fancy equalities. *) - -type 'a eq_class= { - isEqual_method : 'a -> 'a -> bool; - isInequal_method : 'a -> 'a -> bool -} - - -(* (=) should for all instances be an equivalence relation - The isEquivalence predicate of relations could be used here. - However, this would lead to a cyclic dependency. *) - -(* TODO: add later, once lemmata can be assigned to classes -lemma eq_equiv: ((forall x. (x = x)) && - (forall x y. (x = y) <-> (y = x)) && - (forall x y z. ((x = y) && (y = z)) --> (x = z))) -*) - -(* Structural equality *) - -(* Sometimes, it is also handy to be able to use structural equality. - This equality is mapped to the build-in equality of backends. This equality - differs significantly for each backend. For example, OCaml can`t check equality - of function types, whereas HOL can. When using structural equality, one should - know what one is doing. The only guarentee is that is behaves like - the native backend equality. - - A lengthy name for structural equality is used to discourage its direct use. - It also ensures that users realise it is unsafe (e.g. OCaml can`t check two functions - for equality *) -(*val unsafe_structural_equality : forall 'a. 'a -> 'a -> bool*) - -(*val unsafe_structural_inequality : forall 'a. 'a -> 'a -> bool*) -let unsafe_structural_inequality x y = (not (x = y)) - -(* The default for equality is the unsafe structural one. It can - (and should) be overriden for concrete types later. *) - -let instance_Basic_classes_Eq_var_dict =({ - - isEqual_method = (=); - - isInequal_method = unsafe_structural_inequality}) - - -(* ========================================================================== *) -(* Orderings *) -(* ========================================================================== *) - -(* The type-class Ord represents total orders (also called linear orders) *) -(*type ordering = LT | EQ | GT*) - -(*let orderingIsLess r = (match r with LT -> true | _ -> false end)*) -(*let orderingIsGreater r = (match r with GT -> true | _ -> false end)*) -(*let orderingIsEqual r = (match r with EQ -> true | _ -> false end)*) - -(*let ordering_cases r lt eq gt = - if orderingIsLess r then lt else - if orderingIsEqual r then eq else gt*) - - -(*val orderingEqual : ordering -> ordering -> bool*) - -let instance_Basic_classes_Eq_Basic_classes_ordering_dict =({ - - isEqual_method = Lem.orderingEqual; - - isInequal_method = (fun x y->not (Lem.orderingEqual x y))}) - -type 'a ord_class= { - compare_method : 'a -> 'a -> int; - isLess_method : 'a -> 'a -> bool; - isLessEqual_method : 'a -> 'a -> bool; - isGreater_method : 'a -> 'a -> bool; - isGreaterEqual_method : 'a -> 'a -> bool -} - - -(* Ocaml provides default, polymorphic compare functions. Let's use them - as the default. However, because used perhaps in a typeclass they must be - defined for all targets. So, explicitly declare them as undefined for - all other targets. If explictly declare undefined, the type-checker won't complain and - an error will only be raised when trying to actually output the function for a certain - target. *) -(*val defaultCompare : forall 'a. 'a -> 'a -> ordering*) -(*val defaultLess : forall 'a. 'a -> 'a -> bool*) -(*val defaultLessEq : forall 'a. 'a -> 'a -> bool*) -(*val defaultGreater : forall 'a. 'a -> 'a -> bool*) -(*val defaultGreaterEq : forall 'a. 'a -> 'a -> bool*) -;; - -let genericCompare (less: 'a -> 'a -> bool) (equal: 'a -> 'a -> bool) (x : 'a) (y : 'a) = -(if less x y then - (-1) - else if equal x y then - 0 - else - 1) - - -(* -(* compare should really be a total order *) -lemma ord_OK_1: ( - (forall x y. (compare x y = EQ) <-> (compare y x = EQ)) && - (forall x y. (compare x y = LT) <-> (compare y x = GT))) - -lemma ord_OK_2: ( - (forall x y z. (x <= y) && (y <= z) --> (x <= z)) && - (forall x y. (x <= y) || (y <= x)) -) -*) - -(* let's derive a compare function from the Ord type-class *) -(*val ordCompare : forall 'a. Eq 'a, Ord 'a => 'a -> 'a -> ordering*) -let ordCompare dict_Basic_classes_Eq_a dict_Basic_classes_Ord_a x y = -(if ( dict_Basic_classes_Ord_a.isLess_method x y) then (-1) else - if ( dict_Basic_classes_Eq_a.isEqual_method x y) then 0 else 1) - -type 'a ordMaxMin_class= { - max_method : 'a -> 'a -> 'a; - min_method : 'a -> 'a -> 'a -} - -(*val minByLessEqual : forall 'a. ('a -> 'a -> bool) -> 'a -> 'a -> 'a*) -let minByLessEqual le x y = (if (le x y) then x else y) - -(*val maxByLessEqual : forall 'a. ('a -> 'a -> bool) -> 'a -> 'a -> 'a*) -let maxByLessEqual le x y = (if (le y x) then x else y) - -(*val defaultMax : forall 'a. Ord 'a => 'a -> 'a -> 'a*) - -(*val defaultMin : forall 'a. Ord 'a => 'a -> 'a -> 'a*) - -let instance_Basic_classes_OrdMaxMin_var_dict dict_Basic_classes_Ord_a =({ - - max_method = max; - - min_method = min}) - - -(* ========================================================================== *) -(* SetTypes *) -(* ========================================================================== *) - -(* Set implementations use often an order on the elements. This allows the OCaml implementation - to use trees for implementing them. At least, one needs to be able to check equality on sets. - One could use the Ord type-class for sets. However, defining a special typeclass is cleaner - and allows more flexibility. One can make e.g. sure, that this type-class is ignored for - backends like HOL or Isabelle, which don't need it. Moreover, one is not forced to also instantiate - the functions "<", "<=" ... *) - -type 'a setType_class= { - setElemCompare_method : 'a -> 'a -> int -} - -let instance_Basic_classes_SetType_var_dict =({ - - setElemCompare_method = compare}) - -(* ========================================================================== *) -(* Instantiations *) -(* ========================================================================== *) - -let instance_Basic_classes_Eq_bool_dict =({ - - isEqual_method = (=); - - isInequal_method = (fun x y->not ((=) x y))}) - -let boolCompare b1 b2 = ((match (b1, b2) with - | (true, true) -> 0 - | (true, false) -> 1 - | (false, true) -> (-1) - | (false, false) -> 0 -)) - -let instance_Basic_classes_SetType_bool_dict =({ - - setElemCompare_method = boolCompare}) - -(* strings *) - -(*val charEqual : char -> char -> bool*) - -let instance_Basic_classes_Eq_char_dict =({ - - isEqual_method = (=); - - isInequal_method = (fun left right->not (left = right))}) - -(*val stringEquality : string -> string -> bool*) - -let instance_Basic_classes_Eq_string_dict =({ - - isEqual_method = (=); - - isInequal_method = (fun l r->not (l = r))}) - -(* pairs *) - -(*val pairEqual : forall 'a 'b. Eq 'a, Eq 'b => ('a * 'b) -> ('a * 'b) -> bool*) -(*let pairEqual (a1, b1) (a2, b2) = ( - dict_Basic_classes_Eq_a.isEqual_method a1 a2) && ( dict_Basic_classes_Eq_b.isEqual_method b1 b2)*) - -(*val pairEqualBy : forall 'a 'b. ('a -> 'a -> bool) -> ('b -> 'b -> bool) -> ('a * 'b) -> ('a * 'b) -> bool*) - -let instance_Basic_classes_Eq_tup2_dict dict_Basic_classes_Eq_a dict_Basic_classes_Eq_b =({ - - isEqual_method = (Lem.pair_equal - dict_Basic_classes_Eq_a.isEqual_method dict_Basic_classes_Eq_b.isEqual_method); - - isInequal_method = (fun x y->not ((Lem.pair_equal - dict_Basic_classes_Eq_a.isEqual_method dict_Basic_classes_Eq_b.isEqual_method x y)))}) - -(*val pairCompare : forall 'a 'b. ('a -> 'a -> ordering) -> ('b -> 'b -> ordering) -> ('a * 'b) -> ('a * 'b) -> ordering*) -let pairCompare cmpa cmpb (a1, b1) (a2, b2) = - (Lem.ordering_cases (cmpa a1 a2) (-1) (cmpb b1 b2) 1) - -let pairLess dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b (x1, x2) (y1, y2) = (( - dict_Basic_classes_Ord_b.isLess_method x1 y1) || (( dict_Basic_classes_Ord_b.isLessEqual_method x1 y1) && ( dict_Basic_classes_Ord_a.isLess_method x2 y2))) -let pairLessEq dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b (x1, x2) (y1, y2) = (( - dict_Basic_classes_Ord_b.isLess_method x1 y1) || (( dict_Basic_classes_Ord_b.isLessEqual_method x1 y1) && ( dict_Basic_classes_Ord_a.isLessEqual_method x2 y2))) - -let pairGreater dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b x12 y12 = (pairLess - dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a y12 x12) -let pairGreaterEq dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b x12 y12 = (pairLessEq - dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a y12 x12) - -let instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b =({ - - compare_method = (pairCompare - dict_Basic_classes_Ord_a.compare_method dict_Basic_classes_Ord_b.compare_method); - - isLess_method = - (pairLess dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a); - - isLessEqual_method = - (pairLessEq dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a); - - isGreater_method = - (pairGreater dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b); - - isGreaterEqual_method = - (pairGreaterEq dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b)}) - -let instance_Basic_classes_SetType_tup2_dict dict_Basic_classes_SetType_a dict_Basic_classes_SetType_b =({ - - setElemCompare_method = (pairCompare - dict_Basic_classes_SetType_a.setElemCompare_method dict_Basic_classes_SetType_b.setElemCompare_method)}) - - -(* triples *) - -(*val tripleEqual : forall 'a 'b 'c. Eq 'a, Eq 'b, Eq 'c => ('a * 'b * 'c) -> ('a * 'b * 'c) -> bool*) -let tripleEqual dict_Basic_classes_Eq_a dict_Basic_classes_Eq_b dict_Basic_classes_Eq_c (x1, x2, x3) (y1, y2, y3) = ( (Lem.pair_equal - dict_Basic_classes_Eq_a.isEqual_method (Lem.pair_equal dict_Basic_classes_Eq_b.isEqual_method dict_Basic_classes_Eq_c.isEqual_method)(x1, (x2, x3)) (y1, (y2, y3)))) - -let instance_Basic_classes_Eq_tup3_dict dict_Basic_classes_Eq_a dict_Basic_classes_Eq_b dict_Basic_classes_Eq_c =({ - - isEqual_method = - (tripleEqual dict_Basic_classes_Eq_a dict_Basic_classes_Eq_b - dict_Basic_classes_Eq_c); - - isInequal_method = (fun x y->not (tripleEqual - dict_Basic_classes_Eq_a dict_Basic_classes_Eq_b dict_Basic_classes_Eq_c x y))}) - -(*val tripleCompare : forall 'a 'b 'c. ('a -> 'a -> ordering) -> ('b -> 'b -> ordering) -> ('c -> 'c -> ordering) -> ('a * 'b * 'c) -> ('a * 'b * 'c) -> ordering*) -let tripleCompare cmpa cmpb cmpc (a1, b1, c1) (a2, b2, c2) = -(pairCompare cmpa (pairCompare cmpb cmpc) (a1, (b1, c1)) (a2, (b2, c2))) - -let tripleLess dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c (x1, x2, x3) (y1, y2, y3) = (pairLess - (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_b - dict_Basic_classes_Ord_c) dict_Basic_classes_Ord_a (x1, (x2, x3)) (y1, (y2, y3))) -let tripleLessEq dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c (x1, x2, x3) (y1, y2, y3) = (pairLessEq - (instance_Basic_classes_Ord_tup2_dict dict_Basic_classes_Ord_b - dict_Basic_classes_Ord_c) dict_Basic_classes_Ord_a (x1, (x2, x3)) (y1, (y2, y3))) - -let tripleGreater dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c x123 y123 = (tripleLess - dict_Basic_classes_Ord_c dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a y123 x123) -let tripleGreaterEq dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c x123 y123 = (tripleLessEq - dict_Basic_classes_Ord_c dict_Basic_classes_Ord_b dict_Basic_classes_Ord_a y123 x123) - -let instance_Basic_classes_Ord_tup3_dict dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b dict_Basic_classes_Ord_c =({ - - compare_method = (tripleCompare - dict_Basic_classes_Ord_a.compare_method dict_Basic_classes_Ord_b.compare_method dict_Basic_classes_Ord_c.compare_method); - - isLess_method = - (tripleLess dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b - dict_Basic_classes_Ord_c); - - isLessEqual_method = - (tripleLessEq dict_Basic_classes_Ord_a dict_Basic_classes_Ord_b - dict_Basic_classes_Ord_c); - - isGreater_method = - (tripleGreater dict_Basic_classes_Ord_c dict_Basic_classes_Ord_b - dict_Basic_classes_Ord_a); - - isGreaterEqual_method = - (tripleGreaterEq dict_Basic_classes_Ord_c dict_Basic_classes_Ord_b - dict_Basic_classes_Ord_a)}) - -let instance_Basic_classes_SetType_tup3_dict dict_Basic_classes_SetType_a dict_Basic_classes_SetType_b dict_Basic_classes_SetType_c =({ - - setElemCompare_method = (tripleCompare - dict_Basic_classes_SetType_a.setElemCompare_method dict_Basic_classes_SetType_b.setElemCompare_method dict_Basic_classes_SetType_c.setElemCompare_method)}) - diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_bool.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_bool.ml deleted file mode 100644 index 9b6eb0f6..00000000 --- a/lib/ocaml_rts/linksem/src_lem_library/lem_bool.ml +++ /dev/null @@ -1,66 +0,0 @@ -(*Generated by Lem from bool.lem.*) - - -(* The type bool is hard-coded, so are true and false *) - -(* ----------------------- *) -(* not *) -(* ----------------------- *) - -(*val not : bool -> bool*) -(*let not b = match b with - | true -> false - | false -> true -end*) - -(* ----------------------- *) -(* and *) -(* ----------------------- *) - -(*val && [and] : bool -> bool -> bool*) -(*let && b1 b2 = match (b1, b2) with - | (true, true) -> true - | _ -> false -end*) - - -(* ----------------------- *) -(* or *) -(* ----------------------- *) - -(*val || [or] : bool -> bool -> bool*) -(*let || b1 b2 = match (b1, b2) with - | (false, false) -> false - | _ -> true -end*) - - -(* ----------------------- *) -(* implication *) -(* ----------------------- *) - -(*val --> [imp] : bool -> bool -> bool*) -(*let --> b1 b2 = match (b1, b2) with - | (true, false) -> false - | _ -> true -end*) - - -(* ----------------------- *) -(* equivalence *) -(* ----------------------- *) - -(*val <-> [equiv] : bool -> bool -> bool*) -(*let <-> b1 b2 = match (b1, b2) with - | (true, true) -> true - | (false, false) -> true - | _ -> false -end*) - - -(* ----------------------- *) -(* xor *) -(* ----------------------- *) - -(*val xor : bool -> bool -> bool*) - diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_either.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_either.ml deleted file mode 100644 index 9f1b4ad8..00000000 --- a/lib/ocaml_rts/linksem/src_lem_library/lem_either.ml +++ /dev/null @@ -1,87 +0,0 @@ -(*Generated by Lem from either.lem.*) - - -open Lem_bool -open Lem_basic_classes -open Lem_list -open Lem_tuple -open Either - -(*type either 'a 'b - = Left of 'a - | Right of 'b*) - - -(* -------------------------------------------------------------------------- *) -(* Equality. *) -(* -------------------------------------------------------------------------- *) - -(*val eitherEqual : forall 'a 'b. Eq 'a, Eq 'b => (either 'a 'b) -> (either 'a 'b) -> bool*) -(*val eitherEqualBy : forall 'a 'b. ('a -> 'a -> bool) -> ('b -> 'b -> bool) -> (either 'a 'b) -> (either 'a 'b) -> bool*) - -(*let eitherEqualBy eql eqr (left: either 'a 'b) (right: either 'a 'b) = - match (left, right) with - | (Left l, Left l') -> eql l l' - | (Right r, Right r') -> eqr r r' - | _ -> false - end*) -(*let eitherEqual = eitherEqualBy - dict_Basic_classes_Eq_a.isEqual_method dict_Basic_classes_Eq_b.isEqual_method*) - -let instance_Basic_classes_Eq_Either_either_dict dict_Basic_classes_Eq_a dict_Basic_classes_Eq_b =({ - - isEqual_method = (Either.eitherEqualBy - dict_Basic_classes_Eq_a.isEqual_method dict_Basic_classes_Eq_b.isEqual_method); - - isInequal_method = (fun x y->not ((Either.eitherEqualBy - dict_Basic_classes_Eq_a.isEqual_method dict_Basic_classes_Eq_b.isEqual_method x y)))}) - -let either_setElemCompare cmpa cmpb x y = -((match (x, y) with - | (Either.Left x', Either.Left y') -> cmpa x' y' - | (Either.Right x', Either.Right y') -> cmpb x' y' - | (Either.Left _, Either.Right _) -> (-1) - | (Either.Right _, Either.Left _) -> 1 - )) - -let instance_Basic_classes_SetType_Either_either_dict dict_Basic_classes_SetType_a dict_Basic_classes_SetType_b =({ - - setElemCompare_method = (fun x y->either_setElemCompare - dict_Basic_classes_SetType_a.setElemCompare_method dict_Basic_classes_SetType_b.setElemCompare_method x y)}) - - -(* -------------------------------------------------------------------------- *) -(* Utility functions. *) -(* -------------------------------------------------------------------------- *) - -(*val isLeft : forall 'a 'b. either 'a 'b -> bool*) - -(*val isRight : forall 'a 'b. either 'a 'b -> bool*) - - -(*val either : forall 'a 'b 'c. ('a -> 'c) -> ('b -> 'c) -> either 'a 'b -> 'c*) -(*let either fa fb x = match x with - | Left a -> fa a - | Right b -> fb b -end*) - - -(*val partitionEither : forall 'a 'b. list (either 'a 'b) -> (list 'a * list 'b)*) -(*let rec partitionEither l = match l with - | [] -> ([], []) - | x :: xs -> begin - let (ll, rl) = partitionEither xs in - match x with - | Left l -> (l::ll, rl) - | Right r -> (ll, r::rl) - end - end -end*) - - -(*val lefts : forall 'a 'b. list (either 'a 'b) -> list 'a*) - - -(*val rights : forall 'a 'b. list (either 'a 'b) -> list 'b*) - - diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_function.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_function.ml deleted file mode 100644 index 677adc4c..00000000 --- a/lib/ocaml_rts/linksem/src_lem_library/lem_function.ml +++ /dev/null @@ -1,53 +0,0 @@ -(*Generated by Lem from function.lem.*) -(******************************************************************************) -(* A library for common operations on functions *) -(******************************************************************************) - -open Lem_bool -open Lem_basic_classes - -(* ----------------------- *) -(* identity function *) -(* ----------------------- *) - -(*val id : forall 'a. 'a -> 'a*) -let id x = x - - -(* ----------------------- *) -(* constant function *) -(* ----------------------- *) - -(*val const : forall 'a 'b. 'a -> 'b -> 'a*) - - -(* ----------------------- *) -(* function composition *) -(* ----------------------- *) - -(*val comb : forall 'a 'b 'c. ('b -> 'c) -> ('a -> 'b) -> ('a -> 'c)*) -let comb f g = (fun x -> f (g x)) - - -(* ----------------------- *) -(* function application *) -(* ----------------------- *) - -(*val $ [apply] : forall 'a 'b. ('a -> 'b) -> ('a -> 'b)*) -(*let $ f = (fun x -> f x)*) - -(* ----------------------- *) -(* flipping argument order *) -(* ----------------------- *) - -(*val flip : forall 'a 'b 'c. ('a -> 'b -> 'c) -> ('b -> 'a -> 'c)*) -let flip f = (fun x y -> f y x) - - -(* currying / uncurrying *) - -(*val curry : forall 'a 'b 'c. (('a * 'b) -> 'c) -> 'a -> 'b -> 'c*) -let curry f = (fun a b -> f (a, b)) - -(*val uncurry : forall 'a 'b 'c. ('a -> 'b -> 'c) -> ('a * 'b -> 'c)*) -let uncurry f (a,b) = (f a b) diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_function_extra.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_function_extra.ml deleted file mode 100644 index 3c9e7854..00000000 --- a/lib/ocaml_rts/linksem/src_lem_library/lem_function_extra.ml +++ /dev/null @@ -1,15 +0,0 @@ -(*Generated by Lem from function_extra.lem.*) - - -open Lem_maybe -open Lem_bool -open Lem_basic_classes -open Lem_num -open Lem_function - -(* ----------------------- *) -(* getting a unique value *) -(* ----------------------- *) - -(*val THE : forall 'a. ('a -> bool) -> maybe 'a*) - diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_list.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_list.ml deleted file mode 100644 index be308d6e..00000000 --- a/lib/ocaml_rts/linksem/src_lem_library/lem_list.ml +++ /dev/null @@ -1,722 +0,0 @@ -(*Generated by Lem from list.lem.*) - - -open Lem_bool -open Lem_maybe -open Lem_basic_classes -open Lem_tuple -open Lem_num - -(* ========================================================================== *) -(* Basic list functions *) -(* ========================================================================== *) - -(* The type of lists as well as list literals like [], [1;2], ... are hardcoded. - Thus, we can directly dive into derived definitions. *) - - -(* ----------------------- *) -(* cons *) -(* ----------------------- *) - -(*val :: : forall 'a. 'a -> list 'a -> list 'a*) - - -(* ----------------------- *) -(* Emptyness check *) -(* ----------------------- *) - -(*val null : forall 'a. list 'a -> bool*) -let list_null l = ((match l with [] -> true | _ -> false )) - -(* ----------------------- *) -(* Length *) -(* ----------------------- *) - -(*val length : forall 'a. list 'a -> nat*) -(*let rec length l = - match l with - | [] -> 0 - | x :: xs -> (Instance_Num_NumAdd_nat.+) (length xs) 1 - end*) - -(* ----------------------- *) -(* Equality *) -(* ----------------------- *) - -(*val listEqual : forall 'a. Eq 'a => list 'a -> list 'a -> bool*) -(*val listEqualBy : forall 'a. ('a -> 'a -> bool) -> list 'a -> list 'a -> bool*) - -let rec listEqualBy eq l1 l2 = ((match (l1,l2) with - | ([], []) -> true - | ([], (_::_)) -> false - | ((_::_), []) -> false - | (x::xs, y :: ys) -> (eq x y && listEqualBy eq xs ys) -)) - -let instance_Basic_classes_Eq_list_dict dict_Basic_classes_Eq_a =({ - - isEqual_method = (listEqualBy - dict_Basic_classes_Eq_a.isEqual_method); - - isInequal_method = (fun l1 l2->not ((listEqualBy - dict_Basic_classes_Eq_a.isEqual_method l1 l2)))}) - - -(* ----------------------- *) -(* compare *) -(* ----------------------- *) - -(*val lexicographicCompare : forall 'a. Ord 'a => list 'a -> list 'a -> ordering*) -(*val lexicographicCompareBy : forall 'a. ('a -> 'a -> ordering) -> list 'a -> list 'a -> ordering*) - -let rec lexicographic_compare cmp l1 l2 = ((match (l1,l2) with - | ([], []) -> 0 - | ([], _::_) -> (-1) - | (_::_, []) -> 1 - | (x::xs, y::ys) -> begin - Lem.ordering_cases (cmp x y) (-1) (lexicographic_compare cmp xs ys) 1 - end -)) - -(*val lexicographicLess : forall 'a. Ord 'a => list 'a -> list 'a -> bool*) -(*val lexicographicLessBy : forall 'a. ('a -> 'a -> bool) -> ('a -> 'a -> bool) -> list 'a -> list 'a -> bool*) -let rec lexicographic_less less less_eq l1 l2 = ((match (l1,l2) with - | ([], []) -> false - | ([], _::_) -> true - | (_::_, []) -> false - | (x::xs, y::ys) -> ((less x y) || ((less_eq x y) && (lexicographic_less less less_eq xs ys))) -)) - -(*val lexicographicLessEq : forall 'a. Ord 'a => list 'a -> list 'a -> bool*) -(*val lexicographicLessEqBy : forall 'a. ('a -> 'a -> bool) -> ('a -> 'a -> bool) -> list 'a -> list 'a -> bool*) -let rec lexicographic_less_eq less less_eq l1 l2 = ((match (l1,l2) with - | ([], []) -> true - | ([], _::_) -> true - | (_::_, []) -> false - | (x::xs, y::ys) -> (less x y || (less_eq x y && lexicographic_less_eq less less_eq xs ys)) -)) - - -let instance_Basic_classes_Ord_list_dict dict_Basic_classes_Ord_a =({ - - compare_method = (lexicographic_compare - dict_Basic_classes_Ord_a.compare_method); - - isLess_method = (lexicographic_less - dict_Basic_classes_Ord_a.isLess_method dict_Basic_classes_Ord_a.isLessEqual_method); - - isLessEqual_method = (lexicographic_less_eq - dict_Basic_classes_Ord_a.isLess_method dict_Basic_classes_Ord_a.isLessEqual_method); - - isGreater_method = (fun x y->(lexicographic_less - dict_Basic_classes_Ord_a.isLess_method dict_Basic_classes_Ord_a.isLessEqual_method y x)); - - isGreaterEqual_method = (fun x y->(lexicographic_less_eq - dict_Basic_classes_Ord_a.isLess_method dict_Basic_classes_Ord_a.isLessEqual_method y x))}) - - -(* ----------------------- *) -(* Append *) -(* ----------------------- *) - -(*val ++ : forall 'a. list 'a -> list 'a -> list 'a*) (* originally append *) -(*let rec ++ xs ys = match xs with - | [] -> ys - | x :: xs' -> x :: (xs' ++ ys) - end*) - -(* ----------------------- *) -(* snoc *) -(* ----------------------- *) - -(*val snoc : forall 'a. 'a -> list 'a -> list 'a*) -let snoc e l = (List.append l [e]) - - -(* ----------------------- *) -(* Map *) -(* ----------------------- *) - -(*val map : forall 'a 'b. ('a -> 'b) -> list 'a -> list 'b*) -(*let rec map f l = match l with - | [] -> [] - | x :: xs -> (f x) :: map f xs -end*) - -(* ----------------------- *) -(* Reverse *) -(* ----------------------- *) - -(* First lets define the function [reverse_append], which is - closely related to reverse. [reverse_append l1 l2] appends the list [l2] to the reverse of [l1]. - This can be implemented more efficienctly than appending and is - used to implement reverse. *) - -(*val reverseAppend : forall 'a. list 'a -> list 'a -> list 'a*) (* originally named rev_append *) -(*let rec reverseAppend l1 l2 = match l1 with - | [] -> l2 - | x :: xs -> reverseAppend xs (x :: l2) - end*) - -(* Reversing a list *) -(*val reverse : forall 'a. list 'a -> list 'a*) (* originally named rev *) -(*let reverse l = reverseAppend l []*) - - -(* ----------------------- *) -(* Reverse Map *) -(* ----------------------- *) - -(*val reverseMap : forall 'a 'b. ('a -> 'b) -> list 'a -> list 'b*) - - - -(* ========================================================================== *) -(* Folding *) -(* ========================================================================== *) - -(* ----------------------- *) -(* fold left *) -(* ----------------------- *) - -(*val foldl : forall 'a 'b. ('a -> 'b -> 'a) -> 'a -> list 'b -> 'a*) (* originally foldl *) - -(*let rec foldl f b l = match l with - | [] -> b - | x :: xs -> foldl f (f b x) xs -end*) - - -(* ----------------------- *) -(* fold right *) -(* ----------------------- *) - -(*val foldr : forall 'a 'b. ('a -> 'b -> 'b) -> 'b -> list 'a -> 'b*) (* originally foldr with different argument order *) -(*let rec foldr f b l = match l with - | [] -> b - | x :: xs -> f x (foldr f b xs) -end*) - - -(* ----------------------- *) -(* concatenating lists *) -(* ----------------------- *) - -(*val concat : forall 'a. list (list 'a) -> list 'a*) (* before also called "flatten" *) -(*let concat = foldr (++) []*) - - -(* -------------------------- *) -(* concatenating with mapping *) -(* -------------------------- *) - -(*val concatMap : forall 'a 'b. ('a -> list 'b) -> list 'a -> list 'b*) - - -(* ------------------------- *) -(* universal qualification *) -(* ------------------------- *) - -(*val all : forall 'a. ('a -> bool) -> list 'a -> bool*) (* originally for_all *) -(*let all P l = foldl (fun r e -> P e && r) true l*) - - - -(* ------------------------- *) -(* existential qualification *) -(* ------------------------- *) - -(*val any : forall 'a. ('a -> bool) -> list 'a -> bool*) (* originally exist *) -(*let any P l = foldl (fun r e -> P e || r) false l*) - - -(* ------------------------- *) -(* dest_init *) -(* ------------------------- *) - -(* get the initial part and the last element of the list in a safe way *) - -(*val dest_init : forall 'a. list 'a -> maybe (list 'a * 'a)*) - -let rec dest_init_aux rev_init last_elem_seen to_process = -((match to_process with - | [] -> (List.rev rev_init, last_elem_seen) - | x::xs -> dest_init_aux (last_elem_seen::rev_init) x xs - )) - -let dest_init l = ((match l with - | [] -> None - | x::xs -> Some (dest_init_aux [] x xs) -)) - - -(* ========================================================================== *) -(* Indexing lists *) -(* ========================================================================== *) - -(* ------------------------- *) -(* index / nth with maybe *) -(* ------------------------- *) - -(*val index : forall 'a. list 'a -> nat -> maybe 'a*) - -let rec list_index l n = ((match l with - | [] -> None - | x :: xs -> if n = 0 then Some x else list_index xs (Nat_num.nat_monus n( 1)) -)) - -(* ------------------------- *) -(* findIndices *) -(* ------------------------- *) - -(* [findIndices P l] returns the indices of all elements of list [l] that satisfy predicate [P]. - Counting starts with 0, the result list is sorted ascendingly *) -(*val findIndices : forall 'a. ('a -> bool) -> list 'a -> list nat*) - -let rec find_indices_aux (i:int) p0 l = -((match l with - | [] -> [] - | x :: xs -> if p0 x then i :: find_indices_aux (i + 1) p0 xs else find_indices_aux (i + 1) p0 xs - )) -let find_indices p0 l = (find_indices_aux( 0) p0 l) - - - -(* ------------------------- *) -(* findIndex *) -(* ------------------------- *) - -(* findIndex returns the first index of a list that satisfies a given predicate. *) -(*val findIndex : forall 'a. ('a -> bool) -> list 'a -> maybe nat*) -let find_index p0 l = ((match find_indices p0 l with - | [] -> None - | x :: _ -> Some x -)) - -(* ------------------------- *) -(* elemIndices *) -(* ------------------------- *) - -(*val elemIndices : forall 'a. Eq 'a => 'a -> list 'a -> list nat*) - -(* ------------------------- *) -(* elemIndex *) -(* ------------------------- *) - -(*val elemIndex : forall 'a. Eq 'a => 'a -> list 'a -> maybe nat*) - - -(* ========================================================================== *) -(* Creating lists *) -(* ========================================================================== *) - -(* ------------------------- *) -(* genlist *) -(* ------------------------- *) - -(* [genlist f n] generates the list [f 0; f 1; ... (f (n-1))] *) -(*val genlist : forall 'a. (nat -> 'a) -> nat -> list 'a*) - - -let rec genlist f n = - ( - if(n = 0) then ([]) else - (let n'0 =(Nat_num.nat_monus n ( 1)) in snoc (f n'0) (genlist f n'0))) - - -(* ------------------------- *) -(* replicate *) -(* ------------------------- *) - -(*val replicate : forall 'a. nat -> 'a -> list 'a*) -let rec replicate n x = - ( - if(n = 0) then ([]) else - (let n'0 =(Nat_num.nat_monus n ( 1)) in x :: replicate n'0 x)) - - -(* ========================================================================== *) -(* Sublists *) -(* ========================================================================== *) - -(* ------------------------- *) -(* splitAt *) -(* ------------------------- *) - -(* [splitAt n xs] returns a tuple (xs1, xs2), with "append xs1 xs2 = xs" and - "length xs1 = n". If there are not enough elements - in [xs], the original list and the empty one are returned. *) -(*val splitAt : forall 'a. nat -> list 'a -> (list 'a * list 'a)*) -let rec split_at n l = - ((match l with - | [] -> ([], []) - | x::xs -> - if n <= 0 then ([], l) else - begin - let (l1, l2) = (split_at (Nat_num.nat_monus n( 1)) xs) in - ((x::l1), l2) - end - )) - - -(* ------------------------- *) -(* take *) -(* ------------------------- *) - -(* take n xs returns the prefix of xs of length n, or xs itself if n > length xs *) -(*val take : forall 'a. nat -> list 'a -> list 'a*) -let take n l = (fst (split_at n l)) - - - -(* ------------------------- *) -(* drop *) -(* ------------------------- *) - -(* [drop n xs] drops the first [n] elements of [xs]. It returns the empty list, if [n] > [length xs]. *) -(*val drop : forall 'a. nat -> list 'a -> list 'a*) -let drop n l = (snd (split_at n l)) - -(* ------------------------- *) -(* dropWhile *) -(* ------------------------- *) - -(* [dropWhile p xs] drops the first elements of [xs] that satisfy [p]. *) -(*val dropWhile : forall 'a. ('a -> bool) -> list 'a -> list 'a*) -let rec dropWhile p l = ((match l with - | [] -> [] - | x::xs -> if p x then dropWhile p xs else l -)) - - -(* ------------------------- *) -(* takeWhile *) -(* ------------------------- *) - -(* [takeWhile p xs] takes the first elements of [xs] that satisfy [p]. *) -(*val takeWhile : forall 'a. ('a -> bool) -> list 'a -> list 'a*) -let rec takeWhile p l = ((match l with - | [] -> [] - | x::xs -> if p x then x::takeWhile p xs else [] -)) - - -(* ------------------------- *) -(* isPrefixOf *) -(* ------------------------- *) - -(*val isPrefixOf : forall 'a. Eq 'a => list 'a -> list 'a -> bool*) -let rec isPrefixOf dict_Basic_classes_Eq_a l1 l2 = ((match (l1, l2) with - | ([], _) -> true - | (_::_, []) -> false - | (x::xs, y::ys) -> ( - dict_Basic_classes_Eq_a.isEqual_method x y) && isPrefixOf dict_Basic_classes_Eq_a xs ys -)) - -(* ------------------------- *) -(* update *) -(* ------------------------- *) -(*val update : forall 'a. list 'a -> nat -> 'a -> list 'a*) -let rec list_update l n e = - ((match l with - | [] -> [] - | x :: xs -> if n = 0 then e :: xs else x :: (list_update xs ( Nat_num.nat_monus n( 1)) e) -)) - - - -(* ========================================================================== *) -(* Searching lists *) -(* ========================================================================== *) - -(* ------------------------- *) -(* Membership test *) -(* ------------------------- *) - -(* The membership test, one of the basic list functions, is actually tricky for - Lem, because it is tricky, which equality to use. From Lem`s point of - perspective, we want to use the equality provided by the equality type - class. - This allows for example to check whether a set is in a list of sets. - - However, in order to use the equality type class, elem essentially becomes - existential quantification over lists. For types, which implement semantic - equality (=) with syntactic equality, this is overly complicated. In - our theorem prover backend, we would end up with overly complicated, harder - to read definitions and some of the automation would be harder to apply. - Moreover, nearly all the old Lem generated code would change and require - (hopefully minor) adaptions of proofs. - - For now, we ignore this problem and just demand, that all instances of - the equality type class do the right thing for the theorem prover backends. -*) - -(*val elem : forall 'a. Eq 'a => 'a -> list 'a -> bool*) -(*val elemBy : forall 'a. ('a -> 'a -> bool) -> 'a -> list 'a -> bool*) - -let elemBy eq e l = (List.exists (eq e) l) -(*let elem = elemBy dict_Basic_classes_Eq_a.isEqual_method*) - -(* ------------------------- *) -(* Find *) -(* ------------------------- *) -(*val find : forall 'a. ('a -> bool) -> list 'a -> maybe 'a*) (* previously not of maybe type *) -let rec list_find_opt p0 l = ((match l with - | [] -> None - | x :: xs -> if p0 x then Some x else list_find_opt p0 xs -)) - - -(* ----------------------------- *) -(* Lookup in an associative list *) -(* ----------------------------- *) -(*val lookup : forall 'a 'b. Eq 'a => 'a -> list ('a * 'b) -> maybe 'b*) -(*val lookupBy : forall 'a 'b. ('a -> 'a -> bool) -> 'a -> list ('a * 'b) -> maybe 'b*) - -(* DPM: eta-expansion for Coq backend type-inference. *) -let lookupBy eq k m = (Lem.option_map (fun x -> snd x) (list_find_opt (fun (k', _) -> eq k k') m)) - -(* ------------------------- *) -(* filter *) -(* ------------------------- *) -(*val filter : forall 'a. ('a -> bool) -> list 'a -> list 'a*) -(*let rec filter P l = match l with - | [] -> [] - | x :: xs -> if (P x) then x :: (filter P xs) else filter P xs - end*) - - -(* ------------------------- *) -(* partition *) -(* ------------------------- *) -(*val partition : forall 'a. ('a -> bool) -> list 'a -> list 'a * list 'a*) -(*let partition P l = (filter P l, filter (fun x -> not (P x)) l)*) - -(*val reversePartition : forall 'a. ('a -> bool) -> list 'a -> list 'a * list 'a*) -let reversePartition p0 l = (List.partition p0 (List.rev l)) - - -(* ------------------------- *) -(* delete first element *) -(* with certain property *) -(* ------------------------- *) - -(*val deleteFirst : forall 'a. ('a -> bool) -> list 'a -> maybe (list 'a)*) -let rec list_delete_first p0 l = ((match l with - | [] -> None - | x :: xs -> if (p0 x) then Some xs else Lem.option_map (fun xs' -> x :: xs') (list_delete_first p0 xs) - )) - - -(*val delete : forall 'a. Eq 'a => 'a -> list 'a -> list 'a*) -(*val deleteBy : forall 'a. ('a -> 'a -> bool) -> 'a -> list 'a -> list 'a*) - -let list_delete eq x l = (Lem.option_default l (list_delete_first (eq x) l)) - - -(* ========================================================================== *) -(* Zipping and unzipping lists *) -(* ========================================================================== *) - -(* ------------------------- *) -(* zip *) -(* ------------------------- *) - -(* zip takes two lists and returns a list of corresponding pairs. If one input list is short, excess elements of the longer list are discarded. *) -(*val zip : forall 'a 'b. list 'a -> list 'b -> list ('a * 'b)*) (* before combine *) -let rec list_combine l1 l2 = ((match (l1, l2) with - | (x :: xs, y :: ys) -> (x, y) :: list_combine xs ys - | _ -> [] -)) - -(* ------------------------- *) -(* unzip *) -(* ------------------------- *) - -(*val unzip: forall 'a 'b. list ('a * 'b) -> (list 'a * list 'b)*) -(*let rec unzip l = match l with - | [] -> ([], []) - | (x, y) :: xys -> let (xs, ys) = unzip xys in (x :: xs, y :: ys) -end*) - - -let instance_Basic_classes_SetType_list_dict dict_Basic_classes_SetType_a =({ - - setElemCompare_method = (lexicographic_compare - dict_Basic_classes_SetType_a.setElemCompare_method)}) - -(* ------------------------- *) -(* distinct elements *) -(* ------------------------- *) - -(*val allDistinct : forall 'a. Eq 'a => list 'a -> bool*) -let rec allDistinct dict_Basic_classes_Eq_a l = - ((match l with - | [] -> true - | (x::l') -> not (List.mem x l') && allDistinct - dict_Basic_classes_Eq_a l' - )) - -(* some more useful functions *) -(*val mapMaybe : forall 'a 'b. ('a -> maybe 'b) -> list 'a -> list 'b*) -let rec mapMaybe f xs = -((match xs with - | [] -> [] - | x::xs -> - (match f x with - | None -> mapMaybe f xs - | Some y -> y :: (mapMaybe f xs) - ) - )) - -(*val mapi : forall 'a 'b. (nat -> 'a -> 'b) -> list 'a -> list 'b*) -let rec mapiAux f (n : int) l = ((match l with - | [] -> [] - | x :: xs -> (f n x) :: mapiAux f (n + 1) xs -)) -let mapi f l = (mapiAux f( 0) l) - -(* ========================================================================== *) -(* Comments (not clean yet, please ignore the rest of the file) *) -(* ========================================================================== *) - -(* ----------------------- *) -(* skipped from Haskell Lib*) -(* ----------------------- - -intersperse :: a -> [a] -> [a] -intercalate :: [a] -> [[a]] -> [a] -transpose :: [[a]] -> [[a]] -subsequences :: [a] -> [[a]] -permutations :: [a] -> [[a]] -foldl` :: (a -> b -> a) -> a -> [b] -> aSource -foldl1` :: (a -> a -> a) -> [a] -> aSource - -and -or -sum -product -maximum -minimum -scanl -scanr -scanl1 -scanr1 -Accumulating maps - -mapAccumL :: (acc -> x -> (acc, y)) -> acc -> [x] -> (acc, [y])Source -mapAccumR :: (acc -> x -> (acc, y)) -> acc -> [x] -> (acc, [y])Source - -iterate :: (a -> a) -> a -> [a] -repeat :: a -> [a] -cycle :: [a] -> [a] -unfoldr - - -takeWhile :: (a -> Bool) -> [a] -> [a]Source -dropWhile :: (a -> Bool) -> [a] -> [a]Source -dropWhileEnd :: (a -> Bool) -> [a] -> [a]Source -span :: (a -> Bool) -> [a] -> ([a], [a])Source -break :: (a -> Bool) -> [a] -> ([a], [a])Source -break p is equivalent to span (not . p). -stripPrefix :: Eq a => [a] -> [a] -> Maybe [a]Source -group :: Eq a => [a] -> [[a]]Source -inits :: [a] -> [[a]]Source -tails :: [a] -> [[a]]Source - - -isPrefixOf :: Eq a => [a] -> [a] -> BoolSource -isSuffixOf :: Eq a => [a] -> [a] -> BoolSource -isInfixOf :: Eq a => [a] -> [a] -> BoolSource - - - -notElem :: Eq a => a -> [a] -> BoolSource - -zip3 :: [a] -> [b] -> [c] -> [(a, b, c)]Source -zip4 :: [a] -> [b] -> [c] -> [d] -> [(a, b, c, d)]Source -zip5 :: [a] -> [b] -> [c] -> [d] -> [e] -> [(a, b, c, d, e)]Source -zip6 :: [a] -> [b] -> [c] -> [d] -> [e] -> [f] -> [(a, b, c, d, e, f)]Source -zip7 :: [a] -> [b] -> [c] -> [d] -> [e] -> [f] -> [g] -> [(a, b, c, d, e, f, g)]Source - -zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]Source -zipWith3 :: (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]Source -zipWith4 :: (a -> b -> c -> d -> e) -> [a] -> [b] -> [c] -> [d] -> [e]Source -zipWith5 :: (a -> b -> c -> d -> e -> f) -> [a] -> [b] -> [c] -> [d] -> [e] -> [f]Source -zipWith6 :: (a -> b -> c -> d -> e -> f -> g) -> [a] -> [b] -> [c] -> [d] -> [e] -> [f] -> [g]Source -zipWith7 :: (a -> b -> c -> d -> e -> f -> g -> h) -> [a] -> [b] -> [c] -> [d] -> [e] -> [f] -> [g] -> [h]Source - - -unzip3 :: [(a, b, c)] -> ([a], [b], [c])Source -unzip4 :: [(a, b, c, d)] -> ([a], [b], [c], [d])Source -unzip5 :: [(a, b, c, d, e)] -> ([a], [b], [c], [d], [e])Source -unzip6 :: [(a, b, c, d, e, f)] -> ([a], [b], [c], [d], [e], [f])Source -unzip7 :: [(a, b, c, d, e, f, g)] -> ([a], [b], [c], [d], [e], [f], [g])Source - - -lines :: String -> [String]Source -words :: String -> [String]Source -unlines :: [String] -> StringSource -unwords :: [String] -> StringSource -nub :: Eq a => [a] -> [a]Source -delete :: Eq a => a -> [a] -> [a]Source - -(\\) :: Eq a => [a] -> [a] -> [a]Source -union :: Eq a => [a] -> [a] -> [a]Source -intersect :: Eq a => [a] -> [a] -> [a]Source -sort :: Ord a => [a] -> [a]Source -insert :: Ord a => a -> [a] -> [a]Source - - -nubBy :: (a -> a -> Bool) -> [a] -> [a]Source -deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]Source -deleteFirstsBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]Source -unionBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]Source -intersectBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]Source -groupBy :: (a -> a -> Bool) -> [a] -> [[a]]Source -sortBy :: (a -> a -> Ordering) -> [a] -> [a]Source -insertBy :: (a -> a -> Ordering) -> a -> [a] -> [a]Source -maximumBy :: (a -> a -> Ordering) -> [a] -> aSource -minimumBy :: (a -> a -> Ordering) -> [a] -> aSource -genericLength :: Num i => [b] -> iSource -genericTake :: Integral i => i -> [a] -> [a]Source -genericDrop :: Integral i => i -> [a] -> [a]Source -genericSplitAt :: Integral i => i -> [b] -> ([b], [b])Source -genericIndex :: Integral a => [b] -> a -> bSource -genericReplicate :: Integral i => i -> a -> [a]Source - - -*) - - -(* ----------------------- *) -(* skipped from Lem Lib *) -(* ----------------------- - - -val for_all2 : forall 'a 'b. ('a -> 'b -> bool) -> list 'a -> list 'b -> bool -val exists2 : forall 'a 'b. ('a -> 'b -> bool) -> list 'a -> list 'b -> bool -val map2 : forall 'a 'b 'c. ('a -> 'b -> 'c) -> list 'a -> list 'b -> list 'c -val rev_map2 : forall 'a 'b 'c. ('a -> 'b -> 'c) -> list 'a -> list 'b -> list 'c -val fold_left2 : forall 'a 'b 'c. ('a -> 'b -> 'c -> 'a) -> 'a -> list 'b -> list 'c -> 'a -val fold_right2 : forall 'a 'b 'c. ('a -> 'b -> 'c -> 'c) -> list 'a -> list 'b -> 'c -> 'c - - -(* now maybe result and called lookup *) -val assoc : forall 'a 'b. 'a -> list ('a * 'b) -> 'b -let inline {ocaml} assoc = Ocaml.List.assoc - - -val mem_assoc : forall 'a 'b. 'a -> list ('a * 'b) -> bool -val remove_assoc : forall 'a 'b. 'a -> list ('a * 'b) -> list ('a * 'b) - - - -val stable_sort : forall 'a. ('a -> 'a -> num) -> list 'a -> list 'a -val fast_sort : forall 'a. ('a -> 'a -> num) -> list 'a -> list 'a - -val merge : forall 'a. ('a -> 'a -> num) -> list 'a -> list 'a -> list 'a -val intersect : forall 'a. list 'a -> list 'a -> list 'a - - -*) diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_list_extra.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_list_extra.ml deleted file mode 100644 index 8769b232..00000000 --- a/lib/ocaml_rts/linksem/src_lem_library/lem_list_extra.ml +++ /dev/null @@ -1,85 +0,0 @@ -(*Generated by Lem from list_extra.lem.*) - - -open Lem_bool -open Lem_maybe -open Lem_basic_classes -open Lem_tuple -open Lem_num -open Lem_list -open Lem_assert_extra - -(* ------------------------- *) -(* head of non-empty list *) -(* ------------------------- *) -(*val head : forall 'a. list 'a -> 'a*) -(*let head l = match l with | x::xs -> x | [] -> failwith "List_extra.head of empty list" end*) - - -(* ------------------------- *) -(* tail of non-empty list *) -(* ------------------------- *) -(*val tail : forall 'a. list 'a -> list 'a*) -(*let tail l = match l with | x::xs -> xs | [] -> failwith "List_extra.tail of empty list" end*) - - -(* ------------------------- *) -(* last *) -(* ------------------------- *) -(*val last : forall 'a. list 'a -> 'a*) -let rec last l = ((match l with | [x] -> x | x1::x2::xs -> last (x2 :: xs) | [] -> failwith "List_extra.last of empty list" )) - - -(* ------------------------- *) -(* init *) -(* ------------------------- *) - -(* All elements of a non-empty list except the last one. *) -(*val init : forall 'a. list 'a -> list 'a*) -let rec init l = ((match l with | [x] -> [] | x1::x2::xs -> x1::(init (x2::xs)) | [] -> failwith "List_extra.init of empty list" )) - - -(* ------------------------- *) -(* foldl1 / foldr1 *) -(* ------------------------- *) - -(* folding functions for non-empty lists, - which don`t take the base case *) -(*val foldl1 : forall 'a. ('a -> 'a -> 'a) -> list 'a -> 'a*) -let foldl1 f x_xs = ((match x_xs with | (x :: xs) -> List.fold_left f x xs | [] -> failwith "List_extra.foldl1 of empty list" )) - -(*val foldr1 : forall 'a. ('a -> 'a -> 'a) -> list 'a -> 'a*) -let foldr1 f x_xs = ((match x_xs with | (x :: xs) -> List.fold_right f xs x | [] -> failwith "List_extra.foldr1 of empty list" )) - - -(* ------------------------- *) -(* nth element *) -(* ------------------------- *) - -(* get the nth element of a list *) -(*val nth : forall 'a. list 'a -> nat -> 'a*) -(*let nth l n = match index l n with Just e -> e | Nothing -> failwith "List_extra.nth" end*) - - -(* ------------------------- *) -(* Find_non_pure *) -(* ------------------------- *) -(*val findNonPure : forall 'a. ('a -> bool) -> list 'a -> 'a*) -let findNonPure p0 l = ((match (list_find_opt p0 l) with - | Some e -> e - | None -> failwith "List_extra.findNonPure" -)) - - -(* ------------------------- *) -(* zip same length *) -(* ------------------------- *) - -(*val zipSameLength : forall 'a 'b. list 'a -> list 'b -> list ('a * 'b)*) -(*let rec zipSameLength l1 l2 = match (l1, l2) with - | (x :: xs, y :: ys) -> (x, y) :: zipSameLength xs ys - | ([], []) -> [] - | _ -> failwith "List_extra.zipSameLength of different length lists" - -end*) - diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_map.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_map.ml deleted file mode 100644 index a1aab076..00000000 --- a/lib/ocaml_rts/linksem/src_lem_library/lem_map.ml +++ /dev/null @@ -1,154 +0,0 @@ -(*Generated by Lem from map.lem.*) - - -open Lem_bool -open Lem_basic_classes -open Lem_function -open Lem_maybe -open Lem_list -open Lem_tuple -open Lem_set -open Lem_num - -(*type map 'k 'v*) - - - -(* -------------------------------------------------------------------------- *) -(* Map equality. *) -(* -------------------------------------------------------------------------- *) - -(*val mapEqual : forall 'k 'v. Eq 'k, Eq 'v => map 'k 'v -> map 'k 'v -> bool*) -(*val mapEqualBy : forall 'k 'v. ('k -> 'k -> bool) -> ('v -> 'v -> bool) -> map 'k 'v -> map 'k 'v -> bool*) - -let instance_Basic_classes_Eq_Map_map_dict dict_Basic_classes_Eq_k dict_Basic_classes_Eq_v =({ - - isEqual_method = (Pmap.equal dict_Basic_classes_Eq_v.isEqual_method); - - isInequal_method = (fun m1 m2->not ((Pmap.equal dict_Basic_classes_Eq_v.isEqual_method m1 m2)))}) - - -(* -------------------------------------------------------------------------- *) -(* Map type class *) -(* -------------------------------------------------------------------------- *) - -type 'a mapKeyType_class= { - mapKeyCompare_method : 'a -> 'a -> int -} - -let instance_Map_MapKeyType_var_dict dict_Basic_classes_SetType_a =({ - - mapKeyCompare_method = dict_Basic_classes_SetType_a.setElemCompare_method}) - - -(* -------------------------------------------------------------------------- *) -(* Empty maps *) -(* -------------------------------------------------------------------------- *) - -(*val empty : forall 'k 'v. MapKeyType 'k => map 'k 'v*) -(*val emptyBy : forall 'k 'v. ('k -> 'k -> ordering) -> map 'k 'v*) - - -(* -------------------------------------------------------------------------- *) -(* Insertion *) -(* -------------------------------------------------------------------------- *) - -(*val insert : forall 'k 'v. MapKeyType 'k => 'k -> 'v -> map 'k 'v -> map 'k 'v*) - - -(* -------------------------------------------------------------------------- *) -(* Singleton *) -(* -------------------------------------------------------------------------- *) - -(*val singleton : forall 'k 'v. MapKeyType 'k => 'k -> 'v -> map 'k 'v*) - - - -(* -------------------------------------------------------------------------- *) -(* Emptyness check *) -(* -------------------------------------------------------------------------- *) - -(*val null : forall 'k 'v. MapKeyType 'k, Eq 'k, Eq 'v => map 'k 'v -> bool*) - - -(* -------------------------------------------------------------------------- *) -(* lookup *) -(* -------------------------------------------------------------------------- *) - -(*val lookupBy : forall 'k 'v. ('k -> 'k -> ordering) -> 'k -> map 'k 'v -> maybe 'v*) - -(*val lookup : forall 'k 'v. MapKeyType 'k => 'k -> map 'k 'v -> maybe 'v*) - -(* -------------------------------------------------------------------------- *) -(* findWithDefault *) -(* -------------------------------------------------------------------------- *) - -(*val findWithDefault : forall 'k 'v. MapKeyType 'k => 'k -> 'v -> map 'k 'v -> 'v*) - -(* -------------------------------------------------------------------------- *) -(* from lists *) -(* -------------------------------------------------------------------------- *) - -(*val fromList : forall 'k 'v. MapKeyType 'k => list ('k * 'v) -> map 'k 'v*) -let fromList dict_Map_MapKeyType_k l = (List.fold_left (fun m (k,v) -> Pmap.add k v m) (Pmap.empty - dict_Map_MapKeyType_k.mapKeyCompare_method) l) - - -(* -------------------------------------------------------------------------- *) -(* to sets / domain / range *) -(* -------------------------------------------------------------------------- *) - -(*val toSet : forall 'k 'v. MapKeyType 'k, SetType 'k, SetType 'v => map 'k 'v -> set ('k * 'v)*) -(*val toSetBy : forall 'k 'v. (('k * 'v) -> ('k * 'v) -> ordering) -> map 'k 'v -> set ('k * 'v)*) - - -(*val domainBy : forall 'k 'v. ('k -> 'k -> ordering) -> map 'k 'v -> set 'k*) -(*val domain : forall 'k 'v. MapKeyType 'k, SetType 'k => map 'k 'v -> set 'k*) - - -(*val range : forall 'k 'v. MapKeyType 'k, SetType 'v => map 'k 'v -> set 'v*) -(*val rangeBy : forall 'k 'v. ('v -> 'v -> ordering) -> map 'k 'v -> set 'v*) - - -(* -------------------------------------------------------------------------- *) -(* member *) -(* -------------------------------------------------------------------------- *) - -(*val member : forall 'k 'v. MapKeyType 'k, SetType 'k, Eq 'k => 'k -> map 'k 'v -> bool*) - -(*val notMember : forall 'k 'v. MapKeyType 'k, SetType 'k, Eq 'k => 'k -> map 'k 'v -> bool*) - -(* -------------------------------------------------------------------------- *) -(* Quantification *) -(* -------------------------------------------------------------------------- *) - -(*val any : forall 'k 'v. MapKeyType 'k, Eq 'v => ('k -> 'v -> bool) -> map 'k 'v -> bool*) -(*val all : forall 'k 'v. MapKeyType 'k, Eq 'v => ('k -> 'v -> bool) -> map 'k 'v -> bool*) - -(*let all P m = (forall k v. (P k v && ((Instance_Basic_classes_Eq_Maybe_maybe.=) (lookup k m) (Just v))))*) - - -(* -------------------------------------------------------------------------- *) -(* Set-like operations. *) -(* -------------------------------------------------------------------------- *) -(*val deleteBy : forall 'k 'v. ('k -> 'k -> ordering) -> 'k -> map 'k 'v -> map 'k 'v*) -(*val delete : forall 'k 'v. MapKeyType 'k => 'k -> map 'k 'v -> map 'k 'v*) -(*val deleteSwap : forall 'k 'v. MapKeyType 'k => map 'k 'v -> 'k -> map 'k 'v*) - -(*val union : forall 'k 'v. MapKeyType 'k => map 'k 'v -> map 'k 'v -> map 'k 'v*) - -(*val unions : forall 'k 'v. MapKeyType 'k => list (map 'k 'v) -> map 'k 'v*) - - -(* -------------------------------------------------------------------------- *) -(* Maps (in the functor sense). *) -(* -------------------------------------------------------------------------- *) - -(*val map : forall 'k 'v 'w. MapKeyType 'k => ('v -> 'w) -> map 'k 'v -> map 'k 'w*) - -(*val mapi : forall 'k 'v 'w. MapKeyType 'k => ('k -> 'v -> 'w) -> map 'k 'v -> map 'k 'w*) - -(* -------------------------------------------------------------------------- *) -(* Cardinality *) -(* -------------------------------------------------------------------------- *) -(*val size : forall 'k 'v. MapKeyType 'k, SetType 'k => map 'k 'v -> nat*) diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_map_extra.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_map_extra.ml deleted file mode 100644 index c27f6b73..00000000 --- a/lib/ocaml_rts/linksem/src_lem_library/lem_map_extra.ml +++ /dev/null @@ -1,41 +0,0 @@ -(*Generated by Lem from map_extra.lem.*) - - -open Lem_bool -open Lem_basic_classes -open Lem_function -open Lem_assert_extra -open Lem_maybe -open Lem_list -open Lem_num -open Lem_set -open Lem_map - -(* -------------------------------------------------------------------------- *) -(* find *) -(* -------------------------------------------------------------------------- *) - -(*val find : forall 'k 'v. MapKeyType 'k => 'k -> map 'k 'v -> 'v*) -(*let find k m = match (lookup k m) with Just x -> x | Nothing -> failwith "Map_extra.find" end*) - - - -(* -------------------------------------------------------------------------- *) -(* from sets / domain / range *) -(* -------------------------------------------------------------------------- *) - - -(*val fromSet : forall 'k 'v. MapKeyType 'k => ('k -> 'v) -> set 'k -> map 'k 'v*) -(*let fromSet f s = Set_helpers.fold (fun k m -> Map.insert k (f k) m) s Map.empty*) - - -(* -------------------------------------------------------------------------- *) -(* fold *) -(* -------------------------------------------------------------------------- *) - -(*val fold : forall 'k 'v 'r. MapKeyType 'k, SetType 'k, SetType 'v => ('k -> 'v -> 'r -> 'r) -> map 'k 'v -> 'r -> 'r*) -(*let fold f m v = Set_helpers.fold (fun (k, v) r -> f k v r) (Map.toSet m) v*) - - -(*val toList: forall 'k 'v. MapKeyType 'k => map 'k 'v -> list ('k * 'v)*) - diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_maybe.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_maybe.ml deleted file mode 100644 index 8f35b88f..00000000 --- a/lib/ocaml_rts/linksem/src_lem_library/lem_maybe.ml +++ /dev/null @@ -1,98 +0,0 @@ -(*Generated by Lem from maybe.lem.*) - - -open Lem_bool -open Lem_basic_classes -open Lem_function - -(* ========================================================================== *) -(* Basic stuff *) -(* ========================================================================== *) - -(*type maybe 'a = - | Nothing - | Just of 'a*) - - -(*val maybeEqual : forall 'a. Eq 'a => maybe 'a -> maybe 'a -> bool*) -(*val maybeEqualBy : forall 'a. ('a -> 'a -> bool) -> maybe 'a -> maybe 'a -> bool*) - -(*let maybeEqualBy eq x y = match (x,y) with - | (Nothing, Nothing) -> true - | (Nothing, Just _) -> false - | (Just _, Nothing) -> false - | (Just x', Just y') -> (eq x' y') -end*) - -let instance_Basic_classes_Eq_Maybe_maybe_dict dict_Basic_classes_Eq_a =({ - - isEqual_method = (Lem.option_equal - dict_Basic_classes_Eq_a.isEqual_method); - - isInequal_method = (fun x y->not ((Lem.option_equal - dict_Basic_classes_Eq_a.isEqual_method x y)))}) - - -let maybeCompare cmp x y = ((match (x,y) with - | (None, None) -> 0 - | (None, Some _) -> (-1) - | (Some _, None) -> 1 - | (Some x', Some y') -> cmp x' y' -)) - -let instance_Basic_classes_SetType_Maybe_maybe_dict dict_Basic_classes_SetType_a =({ - - setElemCompare_method = (maybeCompare - dict_Basic_classes_SetType_a.setElemCompare_method)}) - - -(* ----------------------- *) -(* maybe *) -(* ----------------------- *) - -(*val maybe : forall 'a 'b. 'b -> ('a -> 'b) -> maybe 'a -> 'b*) -(*let maybe d f mb = match mb with - | Just a -> f a - | Nothing -> d -end*) - -(* ----------------------- *) -(* isJust / isNothing *) -(* ----------------------- *) - -(*val isJust : forall 'a. maybe 'a -> bool*) -(*let isJust mb = match mb with - | Just _ -> true - | Nothing -> false -end*) - -(*val isNothing : forall 'a. maybe 'a -> bool*) -(*let isNothing mb = match mb with - | Just _ -> false - | Nothing -> true -end*) - -(* ----------------------- *) -(* fromMaybe *) -(* ----------------------- *) - -(*val fromMaybe : forall 'a. 'a -> maybe 'a -> 'a*) -(*let fromMaybe d mb = match mb with - | Just v -> v - | Nothing -> d -end*) - -(* ----------------------- *) -(* map *) -(* ----------------------- *) - -(*val map : forall 'a 'b. ('a -> 'b) -> maybe 'a -> maybe 'b*) -(*let map f = maybe Nothing (fun v -> Just (f v))*) - - -(* ----------------------- *) -(* bind *) -(* ----------------------- *) - -(*val bind : forall 'a 'b. maybe 'a -> ('a -> maybe 'b) -> maybe 'b*) -(*let bind mb f = maybe Nothing f mb*) diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_maybe_extra.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_maybe_extra.ml deleted file mode 100644 index 7260b642..00000000 --- a/lib/ocaml_rts/linksem/src_lem_library/lem_maybe_extra.ml +++ /dev/null @@ -1,14 +0,0 @@ -(*Generated by Lem from maybe_extra.lem.*) - - -open Lem_basic_classes -open Lem_maybe -open Lem_assert_extra - -(* ----------------------- *) -(* fromJust *) -(* ----------------------- *) - -(*val fromJust : forall 'a. maybe 'a -> 'a*) -let fromJust op = ((match op with | Some v -> v | None -> failwith "fromJust of Nothing" )) - diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_num.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_num.ml deleted file mode 100644 index f2e10846..00000000 --- a/lib/ocaml_rts/linksem/src_lem_library/lem_num.ml +++ /dev/null @@ -1,901 +0,0 @@ -(*Generated by Lem from num.lem.*) - - -open Lem_bool -open Lem_basic_classes - -(*class inline ( Numeral 'a ) - val fromNumeral : numeral -> 'a -end*) - -(* ========================================================================== *) -(* Syntactic type-classes for common operations *) -(* ========================================================================== *) - -(* Typeclasses can be used as a mean to overload constants like "+", "-", etc *) - -type 'a numNegate_class= { - numNegate_method : 'a -> 'a -} - -type 'a numAbs_class= { - abs_method : 'a -> 'a -} - -type 'a numAdd_class= { - numAdd_method : 'a -> 'a -> 'a -} - -type 'a numMinus_class= { - numMinus_method : 'a -> 'a -> 'a -} - -type 'a numMult_class= { - numMult_method : 'a -> 'a -> 'a -} - -type 'a numPow_class= { - numPow_method : 'a -> int -> 'a -} - -type 'a numDivision_class= { - numDivision_method : 'a -> 'a -> 'a -} - -type 'a numIntegerDivision_class= { - div_method : 'a -> 'a -> 'a -} - - -type 'a numRemainder_class= { - mod_method : 'a -> 'a -> 'a -} - -type 'a numSucc_class= { - succ_method : 'a -> 'a -} - -type 'a numPred_class= { - pred_method : 'a -> 'a -} - - -(* ----------------------- *) -(* natural *) -(* ----------------------- *) - -(* unbounded size natural numbers *) -(*type natural*) - - -(* ----------------------- *) -(* int *) -(* ----------------------- *) - -(* bounded size integers with uncertain length *) - -(*type int*) - - -(* ----------------------- *) -(* integer *) -(* ----------------------- *) - -(* unbounded size integers *) - -(*type integer*) - -(* ----------------------- *) -(* bint *) -(* ----------------------- *) - -(* TODO the bounded ints are only partially implemented, use with care. *) - -(* 32 bit integers *) -(*type int32*) - -(* 64 bit integers *) -(*type int64*) - - -(* ----------------------- *) -(* rational *) -(* ----------------------- *) - -(* unbounded size and precision rational numbers *) - -(*type rational*) (* ???: better type for this in HOL? *) - - -(* ----------------------- *) -(* double *) -(* ----------------------- *) - -(* double precision floating point (64 bits) *) - -(*type float64*) (* ???: better type for this in HOL? *) - -(*type float32*) (* ???: better type for this in HOL? *) - - -(* ========================================================================== *) -(* Binding the standard operations for the number types *) -(* ========================================================================== *) - - -(* ----------------------- *) -(* nat *) -(* ----------------------- *) - -(*val natFromNumeral : numeral -> nat*) - -(*val natEq : nat -> nat -> bool*) -let instance_Basic_classes_Eq_nat_dict =({ - - isEqual_method = (=); - - isInequal_method = (fun n1 n2->not (n1 = n2))}) - -(*val natLess : nat -> nat -> bool*) -(*val natLessEqual : nat -> nat -> bool*) -(*val natGreater : nat -> nat -> bool*) -(*val natGreaterEqual : nat -> nat -> bool*) - -(*val natCompare : nat -> nat -> ordering*) - -let instance_Basic_classes_Ord_nat_dict =({ - - compare_method = compare; - - isLess_method = (<); - - isLessEqual_method = (<=); - - isGreater_method = (>); - - isGreaterEqual_method = (>=)}) - -let instance_Basic_classes_SetType_nat_dict =({ - - setElemCompare_method = compare}) - -(*val natAdd : nat -> nat -> nat*) - -let instance_Num_NumAdd_nat_dict =({ - - numAdd_method = (+)}) - -(*val natMinus : nat -> nat -> nat*) - -let instance_Num_NumMinus_nat_dict =({ - - numMinus_method = Nat_num.nat_monus}) - -(*val natSucc : nat -> nat*) -(*let natSucc n = (Instance_Num_NumAdd_nat.+) n 1*) -let instance_Num_NumSucc_nat_dict =({ - - succ_method = succ}) - -(*val natPred : nat -> nat*) -let instance_Num_NumPred_nat_dict =({ - - pred_method = Nat_num.nat_pred}) - -(*val natMult : nat -> nat -> nat*) - -let instance_Num_NumMult_nat_dict =({ - - numMult_method = ( * )}) - -(*val natDiv : nat -> nat -> nat*) - -let instance_Num_NumIntegerDivision_nat_dict =({ - - div_method = (/)}) - -let instance_Num_NumDivision_nat_dict =({ - - numDivision_method = (/)}) - -(*val natMod : nat -> nat -> nat*) - -let instance_Num_NumRemainder_nat_dict =({ - - mod_method = (mod)}) - - -(*val gen_pow_aux : forall 'a. ('a -> 'a -> 'a) -> 'a -> 'a -> nat -> 'a*) -let rec gen_pow_aux (mul : 'a -> 'a -> 'a) (a : 'a) (b : 'a) (e : int) = - ( (* cannot happen, call discipline guarentees e >= 1 *) if(e = 0) then - a else - ( - if(e = 1) then (mul a b) else - (let e'' = (e / 2) in - let a' = (if (e mod 2) = 0 then a else mul a b) in - gen_pow_aux mul a' (mul b b) e''))) - -let gen_pow (one : 'a) (mul : 'a -> 'a -> 'a) (b : 'a) (e : int) : 'a = - (if e < 0 then one else - if (e = 0) then one else gen_pow_aux mul one b e) - -(*val natPow : nat -> nat -> nat*) -let natPow = (gen_pow( 1) ( * )) - -let instance_Num_NumPow_nat_dict =({ - - numPow_method = natPow}) - -(*val natMin : nat -> nat -> nat*) - -(*val natMax : nat -> nat -> nat*) - -let instance_Basic_classes_OrdMaxMin_nat_dict =({ - - max_method = max; - - min_method = min}) - - -(* ----------------------- *) -(* natural *) -(* ----------------------- *) - -(*val naturalFromNumeral : numeral -> natural*) - -(*val naturalEq : natural -> natural -> bool*) -let instance_Basic_classes_Eq_Num_natural_dict =({ - - isEqual_method = Big_int.eq_big_int; - - isInequal_method = (fun n1 n2->not (Big_int.eq_big_int n1 n2))}) - -(*val naturalLess : natural -> natural -> bool*) -(*val naturalLessEqual : natural -> natural -> bool*) -(*val naturalGreater : natural -> natural -> bool*) -(*val naturalGreaterEqual : natural -> natural -> bool*) - -(*val naturalCompare : natural -> natural -> ordering*) - -let instance_Basic_classes_Ord_Num_natural_dict =({ - - compare_method = Big_int.compare_big_int; - - isLess_method = Big_int.lt_big_int; - - isLessEqual_method = Big_int.le_big_int; - - isGreater_method = Big_int.gt_big_int; - - isGreaterEqual_method = Big_int.ge_big_int}) - -let instance_Basic_classes_SetType_Num_natural_dict =({ - - setElemCompare_method = Big_int.compare_big_int}) - -(*val naturalAdd : natural -> natural -> natural*) - -let instance_Num_NumAdd_Num_natural_dict =({ - - numAdd_method = Big_int.add_big_int}) - -(*val naturalMinus : natural -> natural -> natural*) - -let instance_Num_NumMinus_Num_natural_dict =({ - - numMinus_method = Nat_num.natural_monus}) - -(*val naturalSucc : natural -> natural*) -(*let naturalSucc n = (Instance_Num_NumAdd_Num_natural.+) n 1*) -let instance_Num_NumSucc_Num_natural_dict =({ - - succ_method = Big_int.succ_big_int}) - -(*val naturalPred : natural -> natural*) -let instance_Num_NumPred_Num_natural_dict =({ - - pred_method = Nat_num.natural_pred}) - -(*val naturalMult : natural -> natural -> natural*) - -let instance_Num_NumMult_Num_natural_dict =({ - - numMult_method = Big_int.mult_big_int}) - - -(*val naturalPow : natural -> nat -> natural*) - -let instance_Num_NumPow_Num_natural_dict =({ - - numPow_method = Big_int.power_big_int_positive_int}) - -(*val naturalDiv : natural -> natural -> natural*) - -let instance_Num_NumIntegerDivision_Num_natural_dict =({ - - div_method = Big_int.div_big_int}) - -let instance_Num_NumDivision_Num_natural_dict =({ - - numDivision_method = Big_int.div_big_int}) - -(*val naturalMod : natural -> natural -> natural*) - -let instance_Num_NumRemainder_Num_natural_dict =({ - - mod_method = Big_int.mod_big_int}) - -(*val naturalMin : natural -> natural -> natural*) - -(*val naturalMax : natural -> natural -> natural*) - -let instance_Basic_classes_OrdMaxMin_Num_natural_dict =({ - - max_method = Big_int.max_big_int; - - min_method = Big_int.min_big_int}) - - -(* ----------------------- *) -(* int *) -(* ----------------------- *) - -(*val intFromNumeral : numeral -> int*) - -(*val intEq : int -> int -> bool*) -let instance_Basic_classes_Eq_Num_int_dict =({ - - isEqual_method = (=); - - isInequal_method = (fun n1 n2->not (n1 = n2))}) - -(*val intLess : int -> int -> bool*) -(*val intLessEqual : int -> int -> bool*) -(*val intGreater : int -> int -> bool*) -(*val intGreaterEqual : int -> int -> bool*) - -(*val intCompare : int -> int -> ordering*) - -let instance_Basic_classes_Ord_Num_int_dict =({ - - compare_method = compare; - - isLess_method = (<); - - isLessEqual_method = (<=); - - isGreater_method = (>); - - isGreaterEqual_method = (>=)}) - -let instance_Basic_classes_SetType_Num_int_dict =({ - - setElemCompare_method = compare}) - -(*val intNegate : int -> int*) - -let instance_Num_NumNegate_Num_int_dict =({ - - numNegate_method = (fun i->(~- i))}) - -(*val intAbs : int -> int*) (* TODO: check *) - -let instance_Num_NumAbs_Num_int_dict =({ - - abs_method = abs}) - -(*val intAdd : int -> int -> int*) - -let instance_Num_NumAdd_Num_int_dict =({ - - numAdd_method = (+)}) - -(*val intMinus : int -> int -> int*) - -let instance_Num_NumMinus_Num_int_dict =({ - - numMinus_method = (-)}) - -(*val intSucc : int -> int*) -let instance_Num_NumSucc_Num_int_dict =({ - - succ_method = succ}) - -(*val intPred : int -> int*) -let instance_Num_NumPred_Num_int_dict =({ - - pred_method = pred}) - -(*val intMult : int -> int -> int*) - -let instance_Num_NumMult_Num_int_dict =({ - - numMult_method = ( * )}) - - -(*val intPow : int -> nat -> int*) -let intPow = (gen_pow( 1) ( * )) - -let instance_Num_NumPow_Num_int_dict =({ - - numPow_method = intPow}) - -(*val intDiv : int -> int -> int*) - -let instance_Num_NumIntegerDivision_Num_int_dict =({ - - div_method = Nat_num.int_div}) - -let instance_Num_NumDivision_Num_int_dict =({ - - numDivision_method = Nat_num.int_div}) - -(*val intMod : int -> int -> int*) - -let instance_Num_NumRemainder_Num_int_dict =({ - - mod_method = Nat_num.int_mod}) - -(*val intMin : int -> int -> int*) - -(*val intMax : int -> int -> int*) - -let instance_Basic_classes_OrdMaxMin_Num_int_dict =({ - - max_method = max; - - min_method = min}) - -(* ----------------------- *) -(* int32 *) -(* ----------------------- *) -(*val int32FromNumeral : numeral -> int32*) - -(*val int32Eq : int32 -> int32 -> bool*) - -let instance_Basic_classes_Eq_Num_int32_dict =({ - - isEqual_method = (=); - - isInequal_method = (fun n1 n2->not (n1 = n2))}) - -(*val int32Less : int32 -> int32 -> bool*) -(*val int32LessEqual : int32 -> int32 -> bool*) -(*val int32Greater : int32 -> int32 -> bool*) -(*val int32GreaterEqual : int32 -> int32 -> bool*) - -(*val int32Compare : int32 -> int32 -> ordering*) - -let instance_Basic_classes_Ord_Num_int32_dict =({ - - compare_method = Int32.compare; - - isLess_method = (<); - - isLessEqual_method = (<=); - - isGreater_method = (>); - - isGreaterEqual_method = (>=)}) - -let instance_Basic_classes_SetType_Num_int32_dict =({ - - setElemCompare_method = Int32.compare}) - -(*val int32Negate : int32 -> int32*) - -let instance_Num_NumNegate_Num_int32_dict =({ - - numNegate_method = Int32.neg}) - -(*val int32Abs : int32 -> int32*) -(*let int32Abs i = (if (Instance_Basic_classes_Ord_Num_int32.<=) 0 i then i else Instance_Num_NumNegate_Num_int32.~ i)*) - -let instance_Num_NumAbs_Num_int32_dict =({ - - abs_method = Int32.abs}) - - -(*val int32Add : int32 -> int32 -> int32*) - -let instance_Num_NumAdd_Num_int32_dict =({ - - numAdd_method = Int32.add}) - -(*val int32Minus : int32 -> int32 -> int32*) - -let instance_Num_NumMinus_Num_int32_dict =({ - - numMinus_method = Int32.sub}) - -(*val int32Succ : int32 -> int32*) - -let instance_Num_NumSucc_Num_int32_dict =({ - - succ_method = Int32.succ}) - -(*val int32Pred : int32 -> int32*) -let instance_Num_NumPred_Num_int32_dict =({ - - pred_method = Int32.pred}) - -(*val int32Mult : int32 -> int32 -> int32*) - -let instance_Num_NumMult_Num_int32_dict =({ - - numMult_method = Int32.mul}) - - -(*val int32Pow : int32 -> nat -> int32*) -let int32Pow = (gen_pow(Int32.of_int 1) Int32.mul) - -let instance_Num_NumPow_Num_int32_dict =({ - - numPow_method = int32Pow}) - -(*val int32Div : int32 -> int32 -> int32*) - -let instance_Num_NumIntegerDivision_Num_int32_dict =({ - - div_method = Nat_num.int32_div}) - -let instance_Num_NumDivision_Num_int32_dict =({ - - numDivision_method = Nat_num.int32_div}) - -(*val int32Mod : int32 -> int32 -> int32*) - -let instance_Num_NumRemainder_Num_int32_dict =({ - - mod_method = Nat_num.int32_mod}) - -(*val int32Min : int32 -> int32 -> int32*) - -(*val int32Max : int32 -> int32 -> int32*) - -let instance_Basic_classes_OrdMaxMin_Num_int32_dict =({ - - max_method = max; - - min_method = min}) - - - -(* ----------------------- *) -(* int64 *) -(* ----------------------- *) -(*val int64FromNumeral : numeral -> int64*) - -(*val int64Eq : int64 -> int64 -> bool*) - -let instance_Basic_classes_Eq_Num_int64_dict =({ - - isEqual_method = (=); - - isInequal_method = (fun n1 n2->not (n1 = n2))}) - -(*val int64Less : int64 -> int64 -> bool*) -(*val int64LessEqual : int64 -> int64 -> bool*) -(*val int64Greater : int64 -> int64 -> bool*) -(*val int64GreaterEqual : int64 -> int64 -> bool*) - -(*val int64Compare : int64 -> int64 -> ordering*) - -let instance_Basic_classes_Ord_Num_int64_dict =({ - - compare_method = Int64.compare; - - isLess_method = (<); - - isLessEqual_method = (<=); - - isGreater_method = (>); - - isGreaterEqual_method = (>=)}) - -let instance_Basic_classes_SetType_Num_int64_dict =({ - - setElemCompare_method = Int64.compare}) - -(*val int64Negate : int64 -> int64*) - -let instance_Num_NumNegate_Num_int64_dict =({ - - numNegate_method = Int64.neg}) - -(*val int64Abs : int64 -> int64*) -(*let int64Abs i = (if (Instance_Basic_classes_Ord_Num_int64.<=) 0 i then i else Instance_Num_NumNegate_Num_int64.~ i)*) - -let instance_Num_NumAbs_Num_int64_dict =({ - - abs_method = Int64.abs}) - - -(*val int64Add : int64 -> int64 -> int64*) - -let instance_Num_NumAdd_Num_int64_dict =({ - - numAdd_method = Int64.add}) - -(*val int64Minus : int64 -> int64 -> int64*) - -let instance_Num_NumMinus_Num_int64_dict =({ - - numMinus_method = Int64.sub}) - -(*val int64Succ : int64 -> int64*) - -let instance_Num_NumSucc_Num_int64_dict =({ - - succ_method = Int64.succ}) - -(*val int64Pred : int64 -> int64*) -let instance_Num_NumPred_Num_int64_dict =({ - - pred_method = Int64.pred}) - -(*val int64Mult : int64 -> int64 -> int64*) - -let instance_Num_NumMult_Num_int64_dict =({ - - numMult_method = Int64.mul}) - - -(*val int64Pow : int64 -> nat -> int64*) -let int64Pow = (gen_pow(Int64.of_int 1) Int64.mul) - -let instance_Num_NumPow_Num_int64_dict =({ - - numPow_method = int64Pow}) - -(*val int64Div : int64 -> int64 -> int64*) - -let instance_Num_NumIntegerDivision_Num_int64_dict =({ - - div_method = Nat_num.int64_div}) - -let instance_Num_NumDivision_Num_int64_dict =({ - - numDivision_method = Nat_num.int64_div}) - -(*val int64Mod : int64 -> int64 -> int64*) - -let instance_Num_NumRemainder_Num_int64_dict =({ - - mod_method = Nat_num.int64_mod}) - -(*val int64Min : int64 -> int64 -> int64*) - -(*val int64Max : int64 -> int64 -> int64*) - -let instance_Basic_classes_OrdMaxMin_Num_int64_dict =({ - - max_method = max; - - min_method = min}) - - -(* ----------------------- *) -(* integer *) -(* ----------------------- *) - -(*val integerFromNumeral : numeral -> integer*) - -(*val integerEq : integer -> integer -> bool*) -let instance_Basic_classes_Eq_Num_integer_dict =({ - - isEqual_method = Big_int.eq_big_int; - - isInequal_method = (fun n1 n2->not (Big_int.eq_big_int n1 n2))}) - -(*val integerLess : integer -> integer -> bool*) -(*val integerLessEqual : integer -> integer -> bool*) -(*val integerGreater : integer -> integer -> bool*) -(*val integerGreaterEqual : integer -> integer -> bool*) - -(*val integerCompare : integer -> integer -> ordering*) - -let instance_Basic_classes_Ord_Num_integer_dict =({ - - compare_method = Big_int.compare_big_int; - - isLess_method = Big_int.lt_big_int; - - isLessEqual_method = Big_int.le_big_int; - - isGreater_method = Big_int.gt_big_int; - - isGreaterEqual_method = Big_int.ge_big_int}) - -let instance_Basic_classes_SetType_Num_integer_dict =({ - - setElemCompare_method = Big_int.compare_big_int}) - -(*val integerNegate : integer -> integer*) - -let instance_Num_NumNegate_Num_integer_dict =({ - - numNegate_method = Big_int.minus_big_int}) - -(*val integerAbs : integer -> integer*) (* TODO: check *) - -let instance_Num_NumAbs_Num_integer_dict =({ - - abs_method = Big_int.abs_big_int}) - -(*val integerAdd : integer -> integer -> integer*) - -let instance_Num_NumAdd_Num_integer_dict =({ - - numAdd_method = Big_int.add_big_int}) - -(*val integerMinus : integer -> integer -> integer*) - -let instance_Num_NumMinus_Num_integer_dict =({ - - numMinus_method = Big_int.sub_big_int}) - -(*val integerSucc : integer -> integer*) -let instance_Num_NumSucc_Num_integer_dict =({ - - succ_method = Big_int.succ_big_int}) - -(*val integerPred : integer -> integer*) -let instance_Num_NumPred_Num_integer_dict =({ - - pred_method = Big_int.pred_big_int}) - -(*val integerMult : integer -> integer -> integer*) - -let instance_Num_NumMult_Num_integer_dict =({ - - numMult_method = Big_int.mult_big_int}) - - -(*val integerPow : integer -> nat -> integer*) - -let instance_Num_NumPow_Num_integer_dict =({ - - numPow_method = Big_int.power_big_int_positive_int}) - -(*val integerDiv : integer -> integer -> integer*) - -let instance_Num_NumIntegerDivision_Num_integer_dict =({ - - div_method = Big_int.div_big_int}) - -let instance_Num_NumDivision_Num_integer_dict =({ - - numDivision_method = Big_int.div_big_int}) - -(*val integerMod : integer -> integer -> integer*) - -let instance_Num_NumRemainder_Num_integer_dict =({ - - mod_method = Big_int.mod_big_int}) - -(*val integerMin : integer -> integer -> integer*) - -(*val integerMax : integer -> integer -> integer*) - -let instance_Basic_classes_OrdMaxMin_Num_integer_dict =({ - - max_method = Big_int.max_big_int; - - min_method = Big_int.min_big_int}) - - - -(* ========================================================================== *) -(* Translation between number types *) -(* ========================================================================== *) - -(******************) -(* integerFrom... *) -(******************) - -(*val integerFromInt : int -> integer*) - - -(*val integerFromNat : nat -> integer*) - -(*val integerFromNatural : natural -> integer*) - - -(*val integerFromInt32 : int32 -> integer*) - - -(*val integerFromInt64 : int64 -> integer*) - - -(******************) -(* naturalFrom... *) -(******************) - -(*val naturalFromNat : nat -> natural*) - -(*val naturalFromInteger : integer -> natural*) - - -(******************) -(* intFrom ... *) -(******************) - -(*val intFromInteger : integer -> int*) - -(*val intFromNat : nat -> int*) - - -(******************) -(* natFrom ... *) -(******************) - -(*val natFromNatural : natural -> nat*) - -(*val natFromInt : int -> nat*) - - -(******************) -(* int32From ... *) -(******************) - -(*val int32FromNat : nat -> int32*) - -(*val int32FromNatural : natural -> int32*) - -(*val int32FromInteger : integer -> int32*) -(*let int32FromInteger i = ( - let abs_int32 = int32FromNatural (naturalFromInteger i) in - if ((Instance_Basic_classes_Ord_Num_integer.<) i 0) then (Instance_Num_NumNegate_Num_int32.~ abs_int32) else abs_int32 -)*) - -(*val int32FromInt : int -> int32*) -(*let int32FromInt i = int32FromInteger (integerFromInt i)*) - - -(*val int32FromInt64 : int64 -> int32*) -(*let int32FromInt64 i = int32FromInteger (integerFromInt64 i)*) - - - - -(******************) -(* int64From ... *) -(******************) - -(*val int64FromNat : nat -> int64*) - -(*val int64FromNatural : natural -> int64*) - -(*val int64FromInteger : integer -> int64*) -(*let int64FromInteger i = ( - let abs_int64 = int64FromNatural (naturalFromInteger i) in - if ((Instance_Basic_classes_Ord_Num_integer.<) i 0) then (Instance_Num_NumNegate_Num_int64.~ abs_int64) else abs_int64 -)*) - -(*val int64FromInt : int -> int64*) -(*let int64FromInt i = int64FromInteger (integerFromInt i)*) - - -(*val int64FromInt32 : int32 -> int64*) -(*let int64FromInt32 i = int64FromInteger (integerFromInt32 i)*) - - -(******************) -(* what's missing *) -(******************) - -(*val naturalFromInt : int -> natural*) -(*val naturalFromInt32 : int32 -> natural*) -(*val naturalFromInt64 : int64 -> natural*) - - -(*val intFromNatural : natural -> int*) -(*val intFromInt32 : int32 -> int*) -(*val intFromInt64 : int64 -> int*) - -(*val natFromInteger : integer -> nat*) -(*val natFromInt32 : int32 -> nat*) -(*val natFromInt64 : int64 -> nat*) - -(*val string_of_natural : natural -> string*) diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_pervasives.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_pervasives.ml deleted file mode 100644 index 729d9b79..00000000 --- a/lib/ocaml_rts/linksem/src_lem_library/lem_pervasives.ml +++ /dev/null @@ -1,18 +0,0 @@ -(*Generated by Lem from pervasives.lem.*) - - -include Lem_basic_classes -include Lem_bool -include Lem_tuple -include Lem_maybe -include Lem_either -include Lem_function -include Lem_num -include Lem_map -include Lem_set -include Lem_list -include Lem_string -include Lem_word - -(*import Sorting Relation*) - diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_pervasives_extra.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_pervasives_extra.ml deleted file mode 100644 index 121429c6..00000000 --- a/lib/ocaml_rts/linksem/src_lem_library/lem_pervasives_extra.ml +++ /dev/null @@ -1,12 +0,0 @@ -(*Generated by Lem from pervasives_extra.lem.*) - - -include Lem_pervasives -include Lem_function_extra -include Lem_maybe_extra -include Lem_map_extra -include Lem_set_extra -include Lem_set_helpers -include Lem_list_extra -include Lem_string_extra -include Lem_assert_extra diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_relation.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_relation.ml deleted file mode 100644 index f2e8114b..00000000 --- a/lib/ocaml_rts/linksem/src_lem_library/lem_relation.ml +++ /dev/null @@ -1,424 +0,0 @@ -(*Generated by Lem from relation.lem.*) - - -open Lem_bool -open Lem_basic_classes -open Lem_tuple -open Lem_set -open Lem_num - -(* ========================================================================== *) -(* The type of relations *) -(* ========================================================================== *) - -type( 'a, 'b) rel_pred = 'a -> 'b -> bool -type( 'a, 'b) rel_set = ('a * 'b) Pset.set - -(* Binary relations are usually represented as either - sets of pairs (rel_set) or as curried functions (rel_pred). - - The choice depends on taste and the backend. Lem should not take a - decision, but supports both representations. There is an abstract type - pred, which can be converted to both representations. The representation - of pred itself then depends on the backend. However, for the time beeing, - let's implement relations as sets to get them working more quickly. *) - -type( 'a, 'b) rel = ('a, 'b) rel_set - -(*val relToSet : forall 'a 'b. SetType 'a, SetType 'b => rel 'a 'b -> rel_set 'a 'b*) -(*val relFromSet : forall 'a 'b. SetType 'a, SetType 'b => rel_set 'a 'b -> rel 'a 'b*) - -(*val relEq : forall 'a 'b. SetType 'a, SetType 'b => rel 'a 'b -> rel 'a 'b -> bool*) -let relEq dict_Basic_classes_SetType_a dict_Basic_classes_SetType_b r1 r2 = ( Pset.equal r1 r2) - -(*val relToPred : forall 'a 'b. SetType 'a, SetType 'b, Eq 'a, Eq 'b => rel 'a 'b -> rel_pred 'a 'b*) -(*val relFromPred : forall 'a 'b. SetType 'a, SetType 'b, Eq 'a, Eq 'b => set 'a -> set 'b -> rel_pred 'a 'b -> rel 'a 'b*) - -let relToPred dict_Basic_classes_SetType_a dict_Basic_classes_SetType_b dict_Basic_classes_Eq_a dict_Basic_classes_Eq_b r = (fun x y -> Pset.mem(x, y) r) -let relFromPred dict_Basic_classes_SetType_a dict_Basic_classes_SetType_b dict_Basic_classes_Eq_a dict_Basic_classes_Eq_b xs ys p = (Pset.filter (fun (x,y) -> p x y) ((Pset.cross (pairCompare - dict_Basic_classes_SetType_a.setElemCompare_method dict_Basic_classes_SetType_b.setElemCompare_method) xs ys))) - - -(* ========================================================================== *) -(* Basic Operations *) -(* ========================================================================== *) - -(* ----------------------- *) -(* membership test *) -(* ----------------------- *) - -(*val inRel : forall 'a 'b. SetType 'a, SetType 'b, Eq 'a, Eq 'b => 'a -> 'b -> rel 'a 'b -> bool*) - - -(* ----------------------- *) -(* empty relation *) -(* ----------------------- *) - -(*val relEmpty : forall 'a 'b. SetType 'a, SetType 'b => rel 'a 'b*) - -(* ----------------------- *) -(* Insertion *) -(* ----------------------- *) - -(*val relAdd : forall 'a 'b. SetType 'a, SetType 'b => 'a -> 'b -> rel 'a 'b -> rel 'a 'b*) - - -(* ----------------------- *) -(* Identity relation *) -(* ----------------------- *) - -(*val relIdOn : forall 'a. SetType 'a, Eq 'a => set 'a -> rel 'a 'a*) -let relIdOn dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a s = (relFromPred - dict_Basic_classes_SetType_a dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a dict_Basic_classes_Eq_a s s dict_Basic_classes_Eq_a.isEqual_method) - -(*val relId : forall 'a. SetType 'a, Eq 'a => rel 'a 'a*) - -(* ----------------------- *) -(* relation union *) -(* ----------------------- *) - -(*val relUnion : forall 'a 'b. SetType 'a, SetType 'b => rel 'a 'b -> rel 'a 'b -> rel 'a 'b*) - -(* ----------------------- *) -(* relation intersection *) -(* ----------------------- *) - -(*val relIntersection : forall 'a 'b. SetType 'a, SetType 'b, Eq 'a, Eq 'b => rel 'a 'b -> rel 'a 'b -> rel 'a 'b*) - -(* ----------------------- *) -(* Relation Composition *) -(* ----------------------- *) - -(*val relComp : forall 'a 'b 'c. SetType 'a, SetType 'b, SetType 'c, Eq 'a, Eq 'b => rel 'a 'b -> rel 'b 'c -> rel 'a 'c*) -let relComp dict_Basic_classes_SetType_a dict_Basic_classes_SetType_b dict_Basic_classes_SetType_c dict_Basic_classes_Eq_a dict_Basic_classes_Eq_b r1 r2 = (let x2 =(Pset.from_list (pairCompare - dict_Basic_classes_SetType_a.setElemCompare_method dict_Basic_classes_SetType_c.setElemCompare_method) []) in Pset.fold - (fun(e1,e2) x2 -> Pset.fold - (fun(e2',e3) x2 -> - if dict_Basic_classes_Eq_b.isEqual_method e2 e2' then - Pset.add (e1, e3) x2 else x2) (r2) x2) (r1) - x2) - -(* ----------------------- *) -(* restrict *) -(* ----------------------- *) - -(*val relRestrict : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> rel 'a 'a*) -let relRestrict dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s = (let x2 =(Pset.from_list (pairCompare - dict_Basic_classes_SetType_a.setElemCompare_method dict_Basic_classes_SetType_a.setElemCompare_method) []) in Pset.fold - (fun a x2 -> Pset.fold - (fun b x2 -> - if Pset.mem (a, b) r then Pset.add (a, b) x2 else x2) - s x2) s x2) - - -(* ----------------------- *) -(* Converse *) -(* ----------------------- *) - -(*val relConverse : forall 'a 'b. SetType 'a, SetType 'b => rel 'a 'b -> rel 'b 'a*) -let relConverse dict_Basic_classes_SetType_a dict_Basic_classes_SetType_b r = ((Pset.map (pairCompare - dict_Basic_classes_SetType_b.setElemCompare_method dict_Basic_classes_SetType_a.setElemCompare_method) Lem.pair_swap (r))) - - -(* ----------------------- *) -(* domain *) -(* ----------------------- *) - -(*val relDomain : forall 'a 'b. SetType 'a, SetType 'b => rel 'a 'b -> set 'a*) -let relDomain dict_Basic_classes_SetType_a dict_Basic_classes_SetType_b r = (Pset.map - dict_Basic_classes_SetType_a.setElemCompare_method (fun x -> fst x) (r)) - -(* ----------------------- *) -(* range *) -(* ----------------------- *) - -(*val relRange : forall 'a 'b. SetType 'a, SetType 'b => rel 'a 'b -> set 'b*) -let relRange dict_Basic_classes_SetType_a dict_Basic_classes_SetType_b r = (Pset.map - dict_Basic_classes_SetType_b.setElemCompare_method (fun x -> snd x) (r)) - - -(* ----------------------- *) -(* field / definedOn *) -(* *) -(* avoid the keyword field *) -(* ----------------------- *) - -(*val relDefinedOn : forall 'a. SetType 'a => rel 'a 'a -> set 'a*) - -(* ----------------------- *) -(* relOver *) -(* *) -(* avoid the keyword field *) -(* ----------------------- *) - -(*val relOver : forall 'a. SetType 'a => rel 'a 'a -> set 'a -> bool*) -let relOver dict_Basic_classes_SetType_a r s = ( Pset.subset(( Pset.(union)(relDomain - dict_Basic_classes_SetType_a dict_Basic_classes_SetType_a r) (relRange dict_Basic_classes_SetType_a dict_Basic_classes_SetType_a r))) s) - - -(* ----------------------- *) -(* apply a relation *) -(* ----------------------- *) - -(* Given a relation r and a set s, relApply r s applies s to r, i.e. - it returns the set of all value reachable via r from a value in s. - This operation can be seen as a generalisation of function application. *) - -(*val relApply : forall 'a 'b. SetType 'a, SetType 'b, Eq 'a => rel 'a 'b -> set 'a -> set 'b*) -let relApply dict_Basic_classes_SetType_a dict_Basic_classes_SetType_b dict_Basic_classes_Eq_a r s = (let x2 =(Pset.from_list - dict_Basic_classes_SetType_b.setElemCompare_method []) in Pset.fold (fun(x, y) x2 -> if Pset.mem x s then Pset.add y x2 else x2) - (r) x2) - - -(* ========================================================================== *) -(* Properties *) -(* ========================================================================== *) - -(* ----------------------- *) -(* subrel *) -(* ----------------------- *) - -(*val isSubrel : forall 'a 'b. SetType 'a, SetType 'b, Eq 'a, Eq 'b => rel 'a 'b -> rel 'a 'b -> bool*) - -(* ----------------------- *) -(* reflexivity *) -(* ----------------------- *) - -(*val isReflexiveOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*) -let isReflexiveOn dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s = (Pset.for_all - (fun e -> Pset.mem (e, e) r) s) - -(*val isReflexive : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*) - - -(* ----------------------- *) -(* irreflexivity *) -(* ----------------------- *) - -(*val isIrreflexiveOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*) -let isIrreflexiveOn dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s = (Pset.for_all - (fun e -> not ( Pset.mem (e, e) r)) s) - -(*val isIrreflexive : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*) -let isIrreflexive dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r = (Pset.for_all - (fun (e1, e2) -> not ( dict_Basic_classes_Eq_a.isEqual_method e1 e2)) (r)) - - -(* ----------------------- *) -(* symmetry *) -(* ----------------------- *) - -(*val isSymmetricOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*) -let isSymmetricOn dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s = (Pset.for_all - (fun e1 -> Pset.for_all - (fun e2 -> ((not ( Pset.mem (e1, e2) r)) || - ( Pset.mem (e2, e1) r))) s) s) - -(*val isSymmetric : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*) -let isSymmetric dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r = (Pset.for_all - (fun (e1, e2) -> Pset.mem (e2, e1) r) r) - - -(* ----------------------- *) -(* antisymmetry *) -(* ----------------------- *) - -(*val isAntisymmetricOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*) -let isAntisymmetricOn dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s = (Pset.for_all - (fun e1 -> Pset.for_all - (fun e2 -> ((not ( Pset.mem (e1, e2) r)) || - ((not ( Pset.mem (e2, e1) r)) || - ( dict_Basic_classes_Eq_a.isEqual_method - e1 e2)))) s) s) - -(*val isAntisymmetric : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*) -let isAntisymmetric dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r = (Pset.for_all - (fun (e1, e2) -> ((not ( Pset.mem (e2, e1) r)) || - ( dict_Basic_classes_Eq_a.isEqual_method e1 e2))) r) - - -(* ----------------------- *) -(* transitivity *) -(* ----------------------- *) - -(*val isTransitiveOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*) -let isTransitiveOn dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s = (Pset.for_all - (fun e1 -> Pset.for_all - (fun e2 -> Pset.for_all - (fun e3 -> ((not ( Pset.mem (e1, e2) r)) || - ((not ( Pset.mem (e2, e3) r)) || - ( Pset.mem (e1, e3) r)))) - s) s) s) - -(*val isTransitive : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*) -let isTransitive dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r = (Pset.for_all - (fun (e1, e2) -> Pset.for_all (fun e3 -> Pset.mem (e1, e3) r) - (relApply dict_Basic_classes_SetType_a - dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a - r - (Pset.from_list - dict_Basic_classes_SetType_a.setElemCompare_method - [e2]))) r) - -(* ----------------------- *) -(* total *) -(* ----------------------- *) - -(*val isTotalOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*) -let isTotalOn dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s = (Pset.for_all - (fun e1 -> Pset.for_all - (fun e2 -> ( Pset.mem (e1, e2) r) || ( Pset.mem (e2, e1) r)) - s) s) - - -(*val isTotal : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*) - - -(*val isTrichotomousOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*) -let isTrichotomousOn dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s = (Pset.for_all - (fun e1 -> Pset.for_all - (fun e2 -> ( Pset.mem (e1, e2) r) || - (( dict_Basic_classes_Eq_a.isEqual_method e1 e2) - || ( Pset.mem (e2, e1) r))) s) s) - -(*val isTrichotomous : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*) - - -(* ----------------------- *) -(* is_single_valued *) -(* ----------------------- *) - -(*val isSingleValued : forall 'a 'b. SetType 'a, SetType 'b, Eq 'a, Eq 'b => rel 'a 'b -> bool*) -let isSingleValued dict_Basic_classes_SetType_a dict_Basic_classes_SetType_b dict_Basic_classes_Eq_a dict_Basic_classes_Eq_b r = (Pset.for_all - (fun (e1, e2a) -> Pset.for_all - (fun e2b -> dict_Basic_classes_Eq_b.isEqual_method - e2a e2b) - (relApply dict_Basic_classes_SetType_a - dict_Basic_classes_SetType_b dict_Basic_classes_Eq_a - r - (Pset.from_list - dict_Basic_classes_SetType_a.setElemCompare_method - [e1]))) r) - - -(* ----------------------- *) -(* equivalence relation *) -(* ----------------------- *) - -(*val isEquivalenceOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*) -let isEquivalenceOn dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s = (isReflexiveOn - dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s && (isSymmetricOn - dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s && isTransitiveOn - dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s)) - - -(*val isEquivalence : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*) - - -(* ----------------------- *) -(* well founded *) -(* ----------------------- *) - -(*val isWellFounded : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*) - - -(* ========================================================================== *) -(* Orders *) -(* ========================================================================== *) - - -(* ----------------------- *) -(* pre- or quasiorders *) -(* ----------------------- *) - -(*val isPreorderOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*) -let isPreorderOn dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s = (isReflexiveOn - dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s && isTransitiveOn - dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s) - -(*val isPreorder : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*) - - -(* ----------------------- *) -(* partial orders *) -(* ----------------------- *) - -(*val isPartialOrderOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*) -let isPartialOrderOn dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s = (isReflexiveOn - dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s && (isTransitiveOn - dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s && isAntisymmetricOn - dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s)) - - -(*val isStrictPartialOrderOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*) -let isStrictPartialOrderOn dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s = (isIrreflexiveOn - dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s && isTransitiveOn - dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s) - - -(*val isStrictPartialOrder : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*) -let isStrictPartialOrder dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r = (isIrreflexive - dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r && isTransitive dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r) - -(*val isPartialOrder : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*) - -(* ----------------------- *) -(* total / linear orders *) -(* ----------------------- *) - -(*val isTotalOrderOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*) -let isTotalOrderOn dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s = (isPartialOrderOn - dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s && isTotalOn dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s) - -(*val isStrictTotalOrderOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> bool*) -let isStrictTotalOrderOn dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s = (isStrictPartialOrderOn - dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s && isTrichotomousOn - dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s) - -(*val isTotalOrder : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*) - -(*val isStrictTotalOrder : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> bool*) - - - -(* ========================================================================== *) -(* closures *) -(* ========================================================================== *) - -(* ----------------------- *) -(* transitive closure *) -(* ----------------------- *) - -(*val transitiveClosure : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> rel 'a 'a*) -(*val transitiveClosureByEq : forall 'a. ('a -> 'a -> bool) -> rel 'a 'a -> rel 'a 'a*) -(*val transitiveClosureByCmp : forall 'a. ('a * 'a -> 'a * 'a -> ordering) -> rel 'a 'a -> rel 'a 'a*) - - -(* ----------------------- *) -(* transitive closure step *) -(* ----------------------- *) - -(*val transitiveClosureAdd : forall 'a. SetType 'a, Eq 'a => 'a -> 'a -> rel 'a 'a -> rel 'a 'a*) - -let transitiveClosureAdd dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a x y r = - (( Pset.(union)(((Pset.add (x,y) (r)))) ((( Pset.(union)((let x2 =(Pset.from_list (pairCompare - dict_Basic_classes_SetType_a.setElemCompare_method dict_Basic_classes_SetType_a.setElemCompare_method) []) in Pset.fold (fun z x2 -> if Pset.mem (y, z) r then Pset.add (x, z) x2 else x2) - (relRange dict_Basic_classes_SetType_a dict_Basic_classes_SetType_a r) - x2)) ((let x2 =(Pset.from_list (pairCompare - dict_Basic_classes_SetType_a.setElemCompare_method dict_Basic_classes_SetType_a.setElemCompare_method) []) in Pset.fold (fun z x2 -> if Pset.mem (z, x) r then Pset.add (z, y) x2 else x2) - (relDomain dict_Basic_classes_SetType_a dict_Basic_classes_SetType_a r) - x2))))))) - - -(* ========================================================================== *) -(* reflexiv closures *) -(* ========================================================================== *) - -(*val reflexivTransitiveClosureOn : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> set 'a -> rel 'a 'a*) -let reflexivTransitiveClosureOn dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a r s = (Pset.tc (pairCompare - dict_Basic_classes_SetType_a.setElemCompare_method dict_Basic_classes_SetType_a.setElemCompare_method) (( Pset.(union)(r) ((relIdOn - dict_Basic_classes_SetType_a dict_Basic_classes_Eq_a s))))) - - -(*val reflexivTransitiveClosure : forall 'a. SetType 'a, Eq 'a => rel 'a 'a -> rel 'a 'a*) - diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_set.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_set.ml deleted file mode 100644 index 1cd7c3fa..00000000 --- a/lib/ocaml_rts/linksem/src_lem_library/lem_set.ml +++ /dev/null @@ -1,290 +0,0 @@ -(*Generated by Lem from set.lem.*) -(******************************************************************************) -(* A library for sets *) -(* *) -(* It mainly follows the Haskell Set-library *) -(******************************************************************************) - -(* Sets in Lem are a bit tricky. On the one hand, we want efficiently executable sets. - OCaml and Haskell both represent sets by some kind of balancing trees. This means - that sets are finite and an order on the element type is required. - Such sets are constructed by simple, executable operations like inserting or - deleting elements, union, intersection, filtering etc. - - On the other hand, we want to use sets for specifications. This leads often - infinite sets, which are specificied in complicated, perhaps even undecidable - ways. - - The set library in this file, chooses the first approach. It describes - *finite* sets with an underlying order. Infinite sets should in the medium - run be represented by a separate type. Since this would require some significant - changes to Lem, for the moment also infinite sets are represented using this - class. However, a run-time exception might occour when using these sets. - This problem needs adressing in the future. *) - - -(* ========================================================================== *) -(* Header *) -(* ========================================================================== *) - -open Lem_bool -open Lem_basic_classes -open Lem_maybe -open Lem_function -open Lem_num -open Lem_list -open Lem_set_helpers - -(* ----------------------- *) -(* Equality check *) -(* ----------------------- *) - -(*val setEqualBy : forall 'a. ('a -> 'a -> ordering) -> set 'a -> set 'a -> bool*) - -(*val setEqual : forall 'a. SetType 'a => set 'a -> set 'a -> bool*) - -let instance_Basic_classes_Eq_set_dict dict_Basic_classes_SetType_a =({ - - isEqual_method = Pset.equal; - - isInequal_method = (fun s1 s2->not (Pset.equal s1 s2))}) - - - -(* ----------------------- *) -(* compare *) -(* ----------------------- *) - -(*val setCompareBy: forall 'a. ('a -> 'a -> ordering) -> set 'a -> set 'a -> ordering*) - -(*val setCompare : forall 'a. SetType 'a => set 'a -> set 'a -> ordering*) - -let instance_Basic_classes_SetType_set_dict dict_Basic_classes_SetType_a =({ - - setElemCompare_method = Pset.compare}) - - -(* ----------------------- *) -(* Empty set *) -(* ----------------------- *) - -(*val empty : forall 'a. SetType 'a => set 'a*) -(*val emptyBy : forall 'a. ('a -> 'a -> ordering) -> set 'a*) - -(* ----------------------- *) -(* any / all *) -(* ----------------------- *) - -(*val any : forall 'a. SetType 'a => ('a -> bool) -> set 'a -> bool*) - -(*val all : forall 'a. SetType 'a => ('a -> bool) -> set 'a -> bool*) - - -(* ----------------------- *) -(* (IN) *) -(* ----------------------- *) - -(*val IN [member] : forall 'a. SetType 'a => 'a -> set 'a -> bool*) -(*val memberBy : forall 'a. ('a -> 'a -> ordering) -> 'a -> set 'a -> bool*) - -(* ----------------------- *) -(* not (IN) *) -(* ----------------------- *) - -(*val NIN [notMember] : forall 'a. SetType 'a => 'a -> set 'a -> bool*) - - - -(* ----------------------- *) -(* Emptyness check *) -(* ----------------------- *) - -(*val null : forall 'a. SetType 'a => set 'a -> bool*) - - -(* ------------------------ *) -(* singleton *) -(* ------------------------ *) - -(*val singleton : forall 'a. SetType 'a => 'a -> set 'a*) - - -(* ----------------------- *) -(* size *) -(* ----------------------- *) - -(*val size : forall 'a. SetType 'a => set 'a -> nat*) - - -(* ----------------------------*) -(* setting up pattern matching *) -(* --------------------------- *) - -(*val set_case : forall 'a 'b. SetType 'a => set 'a -> 'b -> ('a -> 'b) -> 'b -> 'b*) - - -(* ------------------------ *) -(* union *) -(* ------------------------ *) - -(*val unionBy : forall 'a. ('a -> 'a -> ordering) -> set 'a -> set 'a -> set 'a*) -(*val union : forall 'a. SetType 'a => set 'a -> set 'a -> set 'a*) - -(* ----------------------- *) -(* insert *) -(* ----------------------- *) - -(*val insert : forall 'a. SetType 'a => 'a -> set 'a -> set 'a*) - -(* ----------------------- *) -(* filter *) -(* ----------------------- *) - -(*val filter : forall 'a. SetType 'a => ('a -> bool) -> set 'a -> set 'a*) -(*let filter P s = {e | forall (e IN s) | P e}*) - - -(* ----------------------- *) -(* partition *) -(* ----------------------- *) - -(*val partition : forall 'a. SetType 'a => ('a -> bool) -> set 'a -> set 'a * set 'a*) -let partition dict_Basic_classes_SetType_a p0 s = (Pset.filter p0 s, Pset.filter (fun e -> not (p0 e)) s) - - -(* ----------------------- *) -(* split *) -(* ----------------------- *) - -(*val split : forall 'a. SetType 'a, Ord 'a => 'a -> set 'a -> set 'a * set 'a*) -let split dict_Basic_classes_SetType_a dict_Basic_classes_Ord_a p s = (Pset.filter ( - dict_Basic_classes_Ord_a.isLess_method p) s, Pset.filter (dict_Basic_classes_Ord_a.isGreater_method p) s) - -(*val splitMember : forall 'a. SetType 'a, Ord 'a => 'a -> set 'a -> set 'a * bool * set 'a*) -let splitMember dict_Basic_classes_SetType_a dict_Basic_classes_Ord_a p s = (Pset.filter ( - dict_Basic_classes_Ord_a.isLess_method p) s, Pset.mem p s, Pset.filter ( - dict_Basic_classes_Ord_a.isGreater_method p) s) - - -(* ------------------------ *) -(* subset and proper subset *) -(* ------------------------ *) - -(*val isSubsetOfBy : forall 'a. ('a -> 'a -> ordering) -> set 'a -> set 'a -> bool*) -(*val isProperSubsetOfBy : forall 'a. ('a -> 'a -> ordering) -> set 'a -> set 'a -> bool*) - -(*val isSubsetOf : forall 'a. SetType 'a => set 'a -> set 'a -> bool*) -(*val isProperSubsetOf : forall 'a. SetType 'a => set 'a -> set 'a -> bool*) - - -(* ------------------------ *) -(* delete *) -(* ------------------------ *) - -(*val delete : forall 'a. SetType 'a, Eq 'a => 'a -> set 'a -> set 'a*) -(*val deleteBy : forall 'a. SetType 'a => ('a -> 'a -> bool) -> 'a -> set 'a -> set 'a*) - - -(* ------------------------ *) -(* bigunion *) -(* ------------------------ *) - -(*val bigunion : forall 'a. SetType 'a => set (set 'a) -> set 'a*) -(*val bigunionBy : forall 'a. ('a -> 'a -> ordering) -> set (set 'a) -> set 'a*) - -(*let bigunion bs = {x | forall (s IN bs) (x IN s) | true}*) - - -(* ------------------------ *) -(* difference *) -(* ------------------------ *) - -(*val differenceBy : forall 'a. ('a -> 'a -> ordering) -> set 'a -> set 'a -> set 'a*) -(*val difference : forall 'a. SetType 'a => set 'a -> set 'a -> set 'a*) - -(* ------------------------ *) -(* intersection *) -(* ------------------------ *) - -(*val intersection : forall 'a. SetType 'a => set 'a -> set 'a -> set 'a*) -(*val intersectionBy : forall 'a. ('a -> 'a -> ordering) -> set 'a -> set 'a -> set 'a*) - - -(* ------------------------ *) -(* map *) -(* ------------------------ *) - -(*val map : forall 'a 'b. SetType 'a, SetType 'b => ('a -> 'b) -> set 'a -> set 'b*) (* before image *) -(*let map f s = { f e | forall (e IN s) | true }*) - -(*val mapBy : forall 'a 'b. ('b -> 'b -> ordering) -> ('a -> 'b) -> set 'a -> set 'b*) - - -(* ------------------------ *) -(* bigunionMap *) -(* ------------------------ *) - -(* In order to avoid providing an comparison function for sets of sets, - it might be better to combine bigunion and map sometimes into a single operation. *) - -(*val bigunionMap : forall 'a 'b. SetType 'a, SetType 'b => ('a -> set 'b) -> set 'a -> set 'b*) -(*val bigunionMapBy : forall 'a 'b. ('b -> 'b -> ordering) -> ('a -> set 'b) -> set 'a -> set 'b*) - -(* ------------------------ *) -(* min and max *) -(* ------------------------ *) - -(*val findMin : forall 'a. SetType 'a, Eq 'a => set 'a -> maybe 'a*) -(*val findMax : forall 'a. SetType 'a, Eq 'a => set 'a -> maybe 'a*) - - - -(* ------------------------ *) -(* fromList *) -(* ------------------------ *) - -(*val fromList : forall 'a. SetType 'a => list 'a -> set 'a*) (* before from_list *) -(*val fromListBy : forall 'a. ('a -> 'a -> ordering) -> list 'a -> set 'a*) - - -(* ------------------------ *) -(* Sigma *) -(* ------------------------ *) - -(*val sigma : forall 'a 'b. SetType 'a, SetType 'b => set 'a -> ('a -> set 'b) -> set ('a * 'b)*) -(*val sigmaBy : forall 'a 'b. (('a * 'b) -> ('a * 'b) -> ordering) -> set 'a -> ('a -> set 'b) -> set ('a * 'b)*) - -(*let sigma sa sb = { (a, b) | forall (a IN sa) (b IN sb a) | true }*) - - -(* ------------------------ *) -(* cross product *) -(* ------------------------ *) - -(*val cross : forall 'a 'b. SetType 'a, SetType 'b => set 'a -> set 'b -> set ('a * 'b)*) -(*val crossBy : forall 'a 'b. (('a * 'b) -> ('a * 'b) -> ordering) -> set 'a -> set 'b -> set ('a * 'b)*) - -(*let cross s1 s2 = { (e1, e2) | forall (e1 IN s1) (e2 IN s2) | true }*) - - -(* ------------------------ *) -(* finite *) -(* ------------------------ *) - -(*val finite : forall 'a. SetType 'a => set 'a -> bool*) - - -(* ----------------------------*) -(* fixed point *) -(* --------------------------- *) - -(*val leastFixedPoint : forall 'a. SetType 'a - => nat -> (set 'a -> set 'a) -> set 'a -> set 'a*) -let rec leastFixedPoint dict_Basic_classes_SetType_a bound f x = - ( - if(bound = 0) then x else - (let bound'0 =(Nat_num.nat_monus bound ( 1)) in - let fx = (f x) in - if Pset.subset fx x then x else - leastFixedPoint dict_Basic_classes_SetType_a bound'0 f - ( Pset.(union) fx x))) diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_set_extra.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_set_extra.ml deleted file mode 100644 index 505f2d3e..00000000 --- a/lib/ocaml_rts/linksem/src_lem_library/lem_set_extra.ml +++ /dev/null @@ -1,66 +0,0 @@ -(*Generated by Lem from set_extra.lem.*) -(******************************************************************************) -(* A library for sets *) -(* *) -(* It mainly follows the Haskell Set-library *) -(******************************************************************************) - -(* ========================================================================== *) -(* Header *) -(* ========================================================================== *) - -open Lem_bool -open Lem_basic_classes -open Lem_maybe -open Lem_function -open Lem_num -open Lem_list -open Lem_sorting -open Lem_set - - -(* ----------------------------*) -(* set choose (be careful !) *) -(* --------------------------- *) - -(*val choose : forall 'a. SetType 'a => set 'a -> 'a*) - - -(* ----------------------------*) -(* universal set *) -(* --------------------------- *) - -(*val universal : forall 'a. SetType 'a => set 'a*) - - -(* ----------------------------*) -(* toList *) -(* --------------------------- *) - -(*val toList : forall 'a. SetType 'a => set 'a -> list 'a*) - - -(* ----------------------------*) -(* toOrderedList *) -(* --------------------------- *) - -(* "toOrderedList" returns a sorted list. Therefore the result is (given a suitable order) deterministic. - Therefore, it is much preferred to "toList". However, it still is only defined for finite sets. So, please - use carefully and consider using set-operations instead of translating sets to lists, performing list manipulations - and then transforming back to sets. *) - -(*val toOrderedListBy : forall 'a. ('a -> 'a -> bool) -> set 'a -> list 'a*) - -(*val toOrderedList : forall 'a. SetType 'a, Ord 'a => set 'a -> list 'a*) - -(* ----------------------------*) -(* unbounded fixed point *) -(* --------------------------- *) - -(* Is NOT supported by the coq backend! *) -(*val leastFixedPointUnbounded : forall 'a. SetType 'a => (set 'a -> set 'a) -> set 'a -> set 'a*) -let rec leastFixedPointUnbounded dict_Basic_classes_SetType_a f x = -(let fx = (f x) in - if Pset.subset fx x then x - else leastFixedPointUnbounded - dict_Basic_classes_SetType_a f ( Pset.(union) fx x)) diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_set_helpers.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_set_helpers.ml deleted file mode 100644 index 25aa739f..00000000 --- a/lib/ocaml_rts/linksem/src_lem_library/lem_set_helpers.ml +++ /dev/null @@ -1,38 +0,0 @@ -(*Generated by Lem from set_helpers.lem.*) -(******************************************************************************) -(* Helper functions for sets *) -(******************************************************************************) - -(* Usually there is a something.lem file containing the main definitions and a - something_extra.lem one containing functions that might cause problems for - some backends or are just seldomly used. - - For sets the situation is different. folding is not well defined, since it - is only sensibly defined for finite sets and it the traversel - order is underspecified. *) - -(* ========================================================================== *) -(* Header *) -(* ========================================================================== *) - -open Lem_bool -open Lem_basic_classes -open Lem_maybe -open Lem_function -open Lem_num - -(* ------------------------ *) -(* fold *) -(* ------------------------ *) - -(* fold is suspicious, because if given a function, for which - the order, in which the arguments are given, matters, it's - results are undefined. On the other hand, it is very handy to - define other - non suspicious functions. - - Moreover, fold is central for OCaml, size it is used to - compile set comprehensions *) - -(*val fold : forall 'a 'b. ('a -> 'b -> 'b) -> set 'a -> 'b -> 'b*) - - diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_sorting.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_sorting.ml deleted file mode 100644 index fa16f70c..00000000 --- a/lib/ocaml_rts/linksem/src_lem_library/lem_sorting.ml +++ /dev/null @@ -1,83 +0,0 @@ -(*Generated by Lem from sorting.lem.*) - - -open Lem_bool -open Lem_basic_classes -open Lem_maybe -open Lem_list -open Lem_num - -(* ------------------------- *) -(* permutations *) -(* ------------------------- *) - -(*val isPermutation : forall 'a. Eq 'a => list 'a -> list 'a -> bool*) -(*val isPermutationBy : forall 'a. ('a -> 'a -> bool) -> list 'a -> list 'a -> bool*) - -let rec isPermutationBy eq l1 l2 = ((match l1 with - | [] -> list_null l2 - | (x :: xs) -> begin - (match list_delete_first (eq x) l2 with - | None -> false - | Some ys -> isPermutationBy eq xs ys - ) - end -)) - - - -(* ------------------------- *) -(* isSorted *) -(* ------------------------- *) - -(* isSortedBy R l - checks, whether the list l is sorted by ordering R. - R should represent an order, i.e. it should be transitive. - Different backends defined "isSorted" slightly differently. However, - the definitions coincide for transitive R. Therefore there is the - following restriction: - - WARNING: Use isSorted and isSortedBy only with transitive relations! -*) - -(*val isSorted : forall 'a. Ord 'a => list 'a -> bool*) -(*val isSortedBy : forall 'a. ('a -> 'a -> bool) -> list 'a -> bool*) - -(* DPM: rejigged the definition with a nested match to get past Coq's termination checker. *) -let rec isSortedBy cmp l = ((match l with - | [] -> true - | x1 :: xs -> - (match xs with - | [] -> true - | x2 :: _ -> (cmp x1 x2 && isSortedBy cmp xs) - ) -)) - - -(* ----------------------- *) -(* insertion sort *) -(* ----------------------- *) - -(*val insert : forall 'a. Ord 'a => 'a -> list 'a -> list 'a*) -(*val insertBy : forall 'a. ('a -> 'a -> bool) -> 'a -> list 'a -> list 'a*) - -(*val insertSort: forall 'a. Ord 'a => list 'a -> list 'a*) -(*val insertSortBy: forall 'a. ('a -> 'a -> bool) -> list 'a -> list 'a*) - -let rec insertBy cmp e l = ((match l with - | [] -> [e] - | x :: xs -> if cmp x e then x :: (insertBy cmp e xs) else (e :: (x :: xs)) -)) - -let insertSortBy cmp l = (List.fold_left (fun l e -> insertBy cmp e l) [] l) - - -(* ----------------------- *) -(* general sorting *) -(* ----------------------- *) - -(*val sort: forall 'a. Ord 'a => list 'a -> list 'a*) -(*val sortBy: forall 'a. ('a -> 'a -> bool) -> list 'a -> list 'a*) -(*val sortByOrd: forall 'a. ('a -> 'a -> ordering) -> list 'a -> list 'a*) - - diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_string.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_string.ml deleted file mode 100644 index f193f7dd..00000000 --- a/lib/ocaml_rts/linksem/src_lem_library/lem_string.ml +++ /dev/null @@ -1,53 +0,0 @@ -(*Generated by Lem from string.lem.*) - - -open Lem_bool -open Lem_basic_classes -open Lem_list -open Xstring - -(* ------------------------------------------- *) -(* translations between strings and char lists *) -(* ------------------------------------------- *) - -(*val toCharList : string -> list char*) - -(*val toString : list char -> string*) - - -(* ----------------------- *) -(* generating strings *) -(* ----------------------- *) - -(*val makeString : nat -> char -> string*) -(*let makeString len c = toString (replicate len c)*) - -(* ----------------------- *) -(* length *) -(* ----------------------- *) - -(*val stringLength : string -> nat*) - -(* ----------------------- *) -(* string concatenation *) -(* ----------------------- *) - -(*val ^ [stringAppend] : string -> string -> string*) - - -(* ----------------------------*) -(* setting up pattern matching *) -(* --------------------------- *) - -(*val string_case : forall 'a. string -> 'a -> (char -> string -> 'a) -> 'a*) - -(*let string_case s c_empty c_cons = - match (toCharList s) with - | [] -> c_empty - | c :: cs -> c_cons c (toString cs) - end*) - -(*val empty_string : string*) - -(*val cons_string : char -> string -> string*) - diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_string_extra.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_string_extra.ml deleted file mode 100644 index a3c8fe7b..00000000 --- a/lib/ocaml_rts/linksem/src_lem_library/lem_string_extra.ml +++ /dev/null @@ -1,91 +0,0 @@ -(*Generated by Lem from string_extra.lem.*) -(******************************************************************************) -(* String functions *) -(******************************************************************************) - -open Lem_basic_classes -open Lem_num -open Lem_list -open Lem_string -open Lem_list_extra - - -(******************************************************************************) -(* Character's to numbers *) -(******************************************************************************) - -(*val ord : char -> nat*) - -(*val chr : nat -> char*) - -(******************************************************************************) -(* Converting to strings *) -(******************************************************************************) - -type 'a show_class={ - show_method : 'a -> string -} - -(*val natToStringHelper : nat -> list char -> list char*) -let rec natToStringHelper n acc = -(if n = 0 then - acc - else - natToStringHelper (n / 10) (Char.chr ((n mod 10) + 48) :: acc)) - -(*val natToString : nat -> string*) -let natToString n = (Xstring.implode (natToStringHelper n [])) - -let instance_String_extra_Show_nat_dict =({ - - show_method = natToString}) - -(*val naturalToStringHelper : natural -> list char -> list char*) -let rec naturalToStringHelper n acc = -(if Big_int.eq_big_int n(Big_int.big_int_of_int 0) then - acc - else - naturalToStringHelper ( Big_int.div_big_int n(Big_int.big_int_of_int 10)) (Char.chr (Big_int.int_of_big_int ( Big_int.add_big_int (Big_int.mod_big_int n(Big_int.big_int_of_int 10))(Big_int.big_int_of_int 48))) :: acc)) - -(*val naturalToString : natural -> string*) -let naturalToString n = (Xstring.implode (naturalToStringHelper n [])) - -let instance_String_extra_Show_Num_natural_dict =({ - - show_method = naturalToString}) - - -(******************************************************************************) -(* List-like operations *) -(******************************************************************************) - -(*val nth : string -> nat -> char*) -(*let nth s n = List_extra.nth (toCharList s) n*) - -(*val stringConcat : list string -> string*) -(*let stringConcat s = - List.foldr (^) "" s*) - -(******************************************************************************) -(* String comparison *) -(******************************************************************************) - -(*val stringCompare : string -> string -> ordering*) - -let stringLess x y = (Lem.orderingIsLess (compare x y)) -let stringLessEq x y = (not (Lem.orderingIsGreater (compare x y))) -let stringGreater x y = (stringLess y x) -let stringGreaterEq x y = (stringLessEq y x) - -let instance_Basic_classes_Ord_string_dict =({ - - compare_method = compare; - - isLess_method = stringLess; - - isLessEqual_method = stringLessEq; - - isGreater_method = stringGreater; - - isGreaterEqual_method = stringGreaterEq}) - diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_tuple.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_tuple.ml deleted file mode 100644 index 8b7aec27..00000000 --- a/lib/ocaml_rts/linksem/src_lem_library/lem_tuple.ml +++ /dev/null @@ -1,41 +0,0 @@ -(*Generated by Lem from tuple.lem.*) - - -open Lem_bool -open Lem_basic_classes - -(* ----------------------- *) -(* fst *) -(* ----------------------- *) - -(*val fst : forall 'a 'b. 'a * 'b -> 'a*) -(*let fst (v1, v2) = v1*) - -(* ----------------------- *) -(* snd *) -(* ----------------------- *) - -(*val snd : forall 'a 'b. 'a * 'b -> 'b*) -(*let snd (v1, v2) = v2*) - - -(* ----------------------- *) -(* curry *) -(* ----------------------- *) - -(*val curry : forall 'a 'b 'c. ('a * 'b -> 'c) -> ('a -> 'b -> 'c)*) - -(* ----------------------- *) -(* uncurry *) -(* ----------------------- *) - -(*val uncurry : forall 'a 'b 'c. ('a -> 'b -> 'c) -> ('a * 'b -> 'c)*) - - -(* ----------------------- *) -(* swap *) -(* ----------------------- *) - -(*val swap : forall 'a 'b. ('a * 'b) -> ('b * 'a)*) -(*let swap (v1, v2) = (v2, v1)*) - diff --git a/lib/ocaml_rts/linksem/src_lem_library/lem_word.ml b/lib/ocaml_rts/linksem/src_lem_library/lem_word.ml deleted file mode 100644 index b446f885..00000000 --- a/lib/ocaml_rts/linksem/src_lem_library/lem_word.ml +++ /dev/null @@ -1,731 +0,0 @@ -(*Generated by Lem from word.lem.*) - - -open Lem_bool -open Lem_maybe -open Lem_num -open Lem_basic_classes -open Lem_list - - -(* ========================================================================== *) -(* Define general purpose word, i.e. sequences of bits of arbitrary length *) -(* ========================================================================== *) - -type bitSequence = BitSeq of - int option * (* length of the sequence, Nothing means infinite length *) - bool * bool (* sign of the word, used to fill up after concrete value is exhausted *) - list (* the initial part of the sequence, least significant bit first *) - -(*val bitSeqEq : bitSequence -> bitSequence -> bool*) -let instance_Basic_classes_Eq_Word_bitSequence_dict =({ - - isEqual_method = (=); - - isInequal_method = (fun n1 n2->not (n1 = n2))}) - -(*val boolListFrombitSeq : nat -> bitSequence -> list bool*) - -let rec boolListFrombitSeqAux n s bl = -(if n = 0 then [] else - (match bl with - | [] -> replicate n s - | b :: bl' -> b :: (boolListFrombitSeqAux (Nat_num.nat_monus n( 1)) s bl') - )) - -let boolListFrombitSeq n (BitSeq( _, s, bl)) = (boolListFrombitSeqAux n s bl) - - -(*val bitSeqFromBoolList : list bool -> maybe bitSequence*) -let bitSeqFromBoolList bl = -((match dest_init bl with - | None -> None - | Some (bl', s) -> Some (BitSeq( (Some (List.length bl)), s, bl')) - )) - - -(* cleans up the representation of a bitSequence without changing its semantics *) -(*val cleanBitSeq : bitSequence -> bitSequence*) -let cleanBitSeq (BitSeq( len, s, bl)) = ((match len with - | None -> (BitSeq( len, s, (List.rev (dropWhile ((=) s) (List.rev bl))))) - | Some n -> (BitSeq( len, s, (List.rev (dropWhile ((=) s) (List.rev (Lem_list.take (Nat_num.nat_monus n( 1)) bl)))))) -)) - - -(*val bitSeqTestBit : bitSequence -> nat -> maybe bool*) -let bitSeqTestBit (BitSeq( len, s, bl)) pos = - ((match len with - | None -> if pos < List.length bl then list_index bl pos else Some s - | Some l -> if (pos >= l) then None else - if ((pos = ( Nat_num.nat_monus l( 1))) || (pos >= List.length bl)) then Some s else - list_index bl pos - )) - -(*val bitSeqSetBit : bitSequence -> nat -> bool -> bitSequence*) -let bitSeqSetBit (BitSeq( len, s, bl)) pos v = -(let bl' = (if (pos < List.length bl) then bl else List.append bl (replicate pos s)) in - let bl'' = (Lem_list.list_update bl' pos v) in - let bs' = (BitSeq( len, s, bl'')) in - cleanBitSeq bs') - - -(*val resizeBitSeq : maybe nat -> bitSequence -> bitSequence*) -let resizeBitSeq new_len bs = -(let (BitSeq( len, s, bl)) = (cleanBitSeq bs) in - let shorten_opt = ((match (new_len, len) with - | (None, _) -> None - | (Some l1, None) -> Some l1 - | (Some l1, Some l2) -> if (l1 < l2) then Some l1 else None - )) in - (match shorten_opt with - | None -> BitSeq( new_len, s, bl) - | Some l1 -> ( - let bl' = (Lem_list.take l1 ( List.append bl [s])) in - (match dest_init bl' with - | None -> (BitSeq( len, s, bl)) (* do nothing if size 0 is requested *) - | Some (bl'', s') -> cleanBitSeq (BitSeq( new_len, s', bl'')) - )) - )) - -(*val bitSeqNot : bitSequence -> bitSequence*) -let bitSeqNot (BitSeq( len, s, bl)) = (BitSeq( len, (not s), (List.map not bl))) - -(*val bitSeqBinop : (bool -> bool -> bool) -> bitSequence -> bitSequence -> bitSequence*) - -(*val bitSeqBinopAux : (bool -> bool -> bool) -> bool -> list bool -> bool -> list bool -> list bool*) -let rec bitSeqBinopAux binop s1 bl1 s2 bl2 = -((match (bl1, bl2) with - | ([], []) -> [] - | (b1 :: bl1', []) -> (binop b1 s2) :: bitSeqBinopAux binop s1 bl1' s2 [] - | ([], b2 :: bl2') -> (binop s1 b2) :: bitSeqBinopAux binop s1 [] s2 bl2' - | (b1 :: bl1', b2 :: bl2') -> (binop b1 b2) :: bitSeqBinopAux binop s1 bl1' s2 bl2' - )) - -let bitSeqBinop binop bs1 bs2 = ( - let (BitSeq( len1, s1, bl1)) = (cleanBitSeq bs1) in - let (BitSeq( len2, s2, bl2)) = (cleanBitSeq bs2) in - - let len = ((match (len1, len2) with - | (Some l1, Some l2) -> Some (max l1 l2) - | _ -> None - )) in - let s = (binop s1 s2) in - let bl = (bitSeqBinopAux binop s1 bl1 s2 bl2) in - cleanBitSeq (BitSeq( len, s, bl)) -) - -let bitSeqAnd = (bitSeqBinop (&&)) -let bitSeqOr = (bitSeqBinop (||)) -let bitSeqXor = (bitSeqBinop (fun b1 b2->not (b1 = b2))) - -(*val bitSeqShiftLeft : bitSequence -> nat -> bitSequence*) -let bitSeqShiftLeft (BitSeq( len, s, bl)) n = (cleanBitSeq (BitSeq( len, s, ( List.append(replicate n false) bl)))) - -(*val bitSeqArithmeticShiftRight : bitSequence -> nat -> bitSequence*) -let bitSeqArithmeticShiftRight bs n = - (let (BitSeq( len, s, bl)) = (cleanBitSeq bs) in - cleanBitSeq (BitSeq( len, s, (drop n bl)))) - -(*val bitSeqLogicalShiftRight : bitSequence -> nat -> bitSequence*) -let bitSeqLogicalShiftRight bs n = - (if (n = 0) then cleanBitSeq bs else - let (BitSeq( len, s, bl)) = (cleanBitSeq bs) in - (match len with - | None -> cleanBitSeq (BitSeq( len, s, (drop n bl))) - | Some l -> cleanBitSeq (BitSeq( len, false, ( List.append(drop n bl) (replicate l s)))) - )) - - -(* integerFromBoolList sign bl creates an integer from a list of bits - (least significant bit first) and an explicitly given sign bit. - It uses two's complement encoding. *) -(*val integerFromBoolList : (bool * list bool) -> integer*) - -let rec integerFromBoolListAux (acc : Big_int.big_int) (bl : bool list) = - ((match bl with - | [] -> acc - | (true :: bl') -> integerFromBoolListAux ( Big_int.add_big_int( Big_int.mult_big_int acc(Big_int.big_int_of_int 2))(Big_int.big_int_of_int 1)) bl' - | (false :: bl') -> integerFromBoolListAux ( Big_int.mult_big_int acc(Big_int.big_int_of_int 2)) bl' - )) - -let integerFromBoolList (sign, bl) = - (if sign then - Big_int.minus_big_int( Big_int.add_big_int(integerFromBoolListAux(Big_int.big_int_of_int 0) (List.rev_map not bl))(Big_int.big_int_of_int 1)) - else integerFromBoolListAux(Big_int.big_int_of_int 0) (List.rev bl)) - -(* [boolListFromInteger i] creates a sign bit and a list of booleans from an integer. The len_opt tells it when to stop.*) -(*val boolListFromInteger : integer -> bool * list bool*) - -let rec boolListFromNatural acc (remainder : Big_int.big_int) = -(if ( Big_int.gt_big_int remainder(Big_int.big_int_of_int 0)) then - (boolListFromNatural (( Big_int.eq_big_int( Big_int.mod_big_int remainder(Big_int.big_int_of_int 2))(Big_int.big_int_of_int 1)) :: acc) - ( Big_int.div_big_int remainder(Big_int.big_int_of_int 2))) - else - List.rev acc) - -let boolListFromInteger (i : Big_int.big_int) = - (if ( Big_int.lt_big_int i(Big_int.big_int_of_int 0)) then - (true, List.map not (boolListFromNatural [] (Big_int.abs_big_int (Big_int.minus_big_int( Big_int.add_big_int i(Big_int.big_int_of_int 1)))))) - else - (false, boolListFromNatural [] (Big_int.abs_big_int i))) - - -(* [bitSeqFromInteger len_opt i] encodes [i] as a bitsequence with [len_opt] bits. If there are not enough - bits, truncation happens *) -(*val bitSeqFromInteger : maybe nat -> integer -> bitSequence*) -let bitSeqFromInteger len_opt i = -(let (s, bl) = (boolListFromInteger i) in - resizeBitSeq len_opt (BitSeq( None, s, bl))) - - -(*val integerFromBitSeq : bitSequence -> integer*) -let integerFromBitSeq bs = -(let (BitSeq( len, s, bl)) = (cleanBitSeq bs) in - integerFromBoolList (s, bl)) - - -(* Now we can via translation to integers map arithmetic operations to bitSequences *) - -(*val bitSeqArithUnaryOp : (integer -> integer) -> bitSequence -> bitSequence*) -let bitSeqArithUnaryOp uop bs = -(let (BitSeq( len, _, _)) = bs in - bitSeqFromInteger len (uop (integerFromBitSeq bs))) - -(*val bitSeqArithBinOp : (integer -> integer -> integer) -> bitSequence -> bitSequence -> bitSequence*) -let bitSeqArithBinOp binop bs1 bs2 = -(let (BitSeq( len1, _, _)) = bs1 in - let (BitSeq( len2, _, _)) = bs2 in - let len = ((match (len1, len2) with - | (Some l1, Some l2) -> Some (max l1 l2) - | _ -> None - )) in - bitSeqFromInteger len (binop (integerFromBitSeq bs1) (integerFromBitSeq bs2))) - -(*val bitSeqArithBinTest : forall 'a. (integer -> integer -> 'a) -> bitSequence -> bitSequence -> 'a*) -let bitSeqArithBinTest binop bs1 bs2 = (binop (integerFromBitSeq bs1) (integerFromBitSeq bs2)) - - -(* now instantiate the number interface for bit-sequences *) - -(*val bitSeqFromNumeral : numeral -> bitSequence*) - -(*val bitSeqLess : bitSequence -> bitSequence -> bool*) -let bitSeqLess bs1 bs2 = (bitSeqArithBinTest Big_int.lt_big_int bs1 bs2) - -(*val bitSeqLessEqual : bitSequence -> bitSequence -> bool*) -let bitSeqLessEqual bs1 bs2 = (bitSeqArithBinTest Big_int.le_big_int bs1 bs2) - -(*val bitSeqGreater : bitSequence -> bitSequence -> bool*) -let bitSeqGreater bs1 bs2 = (bitSeqArithBinTest Big_int.gt_big_int bs1 bs2) - -(*val bitSeqGreaterEqual : bitSequence -> bitSequence -> bool*) -let bitSeqGreaterEqual bs1 bs2 = (bitSeqArithBinTest Big_int.ge_big_int bs1 bs2) - -(*val bitSeqCompare : bitSequence -> bitSequence -> ordering*) -let bitSeqCompare bs1 bs2 = (bitSeqArithBinTest Big_int.compare_big_int bs1 bs2) - -let instance_Basic_classes_Ord_Word_bitSequence_dict =({ - - compare_method = bitSeqCompare; - - isLess_method = bitSeqLess; - - isLessEqual_method = bitSeqLessEqual; - - isGreater_method = bitSeqGreater; - - isGreaterEqual_method = bitSeqGreaterEqual}) - -let instance_Basic_classes_SetType_Word_bitSequence_dict =({ - - setElemCompare_method = bitSeqCompare}) - -(* arithmetic negation, don't mix up with bitwise negation *) -(*val bitSeqNegate : bitSequence -> bitSequence*) -let bitSeqNegate bs = (bitSeqArithUnaryOp Big_int.minus_big_int bs) - -let instance_Num_NumNegate_Word_bitSequence_dict =({ - - numNegate_method = bitSeqNegate}) - - -(*val bitSeqAdd : bitSequence -> bitSequence -> bitSequence*) -let bitSeqAdd bs1 bs2 = (bitSeqArithBinOp Big_int.add_big_int bs1 bs2) - -let instance_Num_NumAdd_Word_bitSequence_dict =({ - - numAdd_method = bitSeqAdd}) - -(*val bitSeqMinus : bitSequence -> bitSequence -> bitSequence*) -let bitSeqMinus bs1 bs2 = (bitSeqArithBinOp Big_int.sub_big_int bs1 bs2) - -let instance_Num_NumMinus_Word_bitSequence_dict =({ - - numMinus_method = bitSeqMinus}) - -(*val bitSeqSucc : bitSequence -> bitSequence*) -let bitSeqSucc bs = (bitSeqArithUnaryOp Big_int.succ_big_int bs) - -let instance_Num_NumSucc_Word_bitSequence_dict =({ - - succ_method = bitSeqSucc}) - -(*val bitSeqPred : bitSequence -> bitSequence*) -let bitSeqPred bs = (bitSeqArithUnaryOp Big_int.pred_big_int bs) - -let instance_Num_NumPred_Word_bitSequence_dict =({ - - pred_method = bitSeqPred}) - -(*val bitSeqMult : bitSequence -> bitSequence -> bitSequence*) -let bitSeqMult bs1 bs2 = (bitSeqArithBinOp Big_int.mult_big_int bs1 bs2) - -let instance_Num_NumMult_Word_bitSequence_dict =({ - - numMult_method = bitSeqMult}) - - -(*val bitSeqPow : bitSequence -> nat -> bitSequence*) -let bitSeqPow bs n = (bitSeqArithUnaryOp (fun i -> Big_int.power_big_int_positive_int i n) bs) - -let instance_Num_NumPow_Word_bitSequence_dict =({ - - numPow_method = bitSeqPow}) - -(*val bitSeqDiv : bitSequence -> bitSequence -> bitSequence*) -let bitSeqDiv bs1 bs2 = (bitSeqArithBinOp Big_int.div_big_int bs1 bs2) - -let instance_Num_NumIntegerDivision_Word_bitSequence_dict =({ - - div_method = bitSeqDiv}) - -let instance_Num_NumDivision_Word_bitSequence_dict =({ - - numDivision_method = bitSeqDiv}) - -(*val bitSeqMod : bitSequence -> bitSequence -> bitSequence*) -let bitSeqMod bs1 bs2 = (bitSeqArithBinOp Big_int.mod_big_int bs1 bs2) - -let instance_Num_NumRemainder_Word_bitSequence_dict =({ - - mod_method = bitSeqMod}) - -(*val bitSeqMin : bitSequence -> bitSequence -> bitSequence*) -let bitSeqMin bs1 bs2 = (bitSeqArithBinOp Big_int.min_big_int bs1 bs2) - -(*val bitSeqMax : bitSequence -> bitSequence -> bitSequence*) -let bitSeqMax bs1 bs2 = (bitSeqArithBinOp Big_int.max_big_int bs1 bs2) - -let instance_Basic_classes_OrdMaxMin_Word_bitSequence_dict =({ - - max_method = bitSeqMax; - - min_method = bitSeqMin}) - - - - -(* ========================================================================== *) -(* Interface for bitoperations *) -(* ========================================================================== *) - -type 'a wordNot_class= { - lnot_method : 'a -> 'a -} - -type 'a wordAnd_class= { - land_method : 'a -> 'a -> 'a -} - -type 'a wordOr_class= { - lor_method : 'a -> 'a -> 'a -} - - -type 'a wordXor_class= { - lxor_method : 'a -> 'a -> 'a -} - -type 'a wordLsl_class= { - lsl_method : 'a -> int -> 'a -} - -type 'a wordLsr_class= { - lsr_method : 'a -> int -> 'a -} - -type 'a wordAsr_class= { - asr_method : 'a -> int -> 'a -} - -(* ----------------------- *) -(* bitSequence *) -(* ----------------------- *) - -let instance_Word_WordNot_Word_bitSequence_dict =({ - - lnot_method = bitSeqNot}) - -let instance_Word_WordAnd_Word_bitSequence_dict =({ - - land_method = bitSeqAnd}) - -let instance_Word_WordOr_Word_bitSequence_dict =({ - - lor_method = bitSeqOr}) - -let instance_Word_WordXor_Word_bitSequence_dict =({ - - lxor_method = bitSeqXor}) - -let instance_Word_WordLsl_Word_bitSequence_dict =({ - - lsl_method = bitSeqShiftLeft}) - -let instance_Word_WordLsr_Word_bitSequence_dict =({ - - lsr_method = bitSeqLogicalShiftRight}) - -let instance_Word_WordAsr_Word_bitSequence_dict =({ - - asr_method = bitSeqArithmeticShiftRight}) - - -(* ----------------------- *) -(* int32 *) -(* ----------------------- *) - -(*val int32Lnot : int32 -> int32*) (* XXX: fix *) - -let instance_Word_WordNot_Num_int32_dict =({ - - lnot_method = Int32.lognot}) - - -(*val int32Lor : int32 -> int32 -> int32*) (* XXX: fix *) - -let instance_Word_WordOr_Num_int32_dict =({ - - lor_method = Int32.logor}) - -(*val int32Lxor : int32 -> int32 -> int32*) (* XXX: fix *) - -let instance_Word_WordXor_Num_int32_dict =({ - - lxor_method = Int32.logxor}) - -(*val int32Land : int32 -> int32 -> int32*) (* XXX: fix *) - -let instance_Word_WordAnd_Num_int32_dict =({ - - land_method = Int32.logand}) - -(*val int32Lsl : int32 -> nat -> int32*) (* XXX: fix *) - -let instance_Word_WordLsl_Num_int32_dict =({ - - lsl_method = Int32.shift_left}) - -(*val int32Lsr : int32 -> nat -> int32*) (* XXX: fix *) - -let instance_Word_WordLsr_Num_int32_dict =({ - - lsr_method = Int32.shift_right_logical}) - - -(*val int32Asr : int32 -> nat -> int32*) (* XXX: fix *) - -let instance_Word_WordAsr_Num_int32_dict =({ - - asr_method = Int32.shift_right}) - - -(* ----------------------- *) -(* int64 *) -(* ----------------------- *) - -(*val int64Lnot : int64 -> int64*) (* XXX: fix *) - -let instance_Word_WordNot_Num_int64_dict =({ - - lnot_method = Int64.lognot}) - -(*val int64Lor : int64 -> int64 -> int64*) (* XXX: fix *) - -let instance_Word_WordOr_Num_int64_dict =({ - - lor_method = Int64.logor}) - -(*val int64Lxor : int64 -> int64 -> int64*) (* XXX: fix *) - -let instance_Word_WordXor_Num_int64_dict =({ - - lxor_method = Int64.logxor}) - -(*val int64Land : int64 -> int64 -> int64*) (* XXX: fix *) - -let instance_Word_WordAnd_Num_int64_dict =({ - - land_method = Int64.logand}) - -(*val int64Lsl : int64 -> nat -> int64*) (* XXX: fix *) - -let instance_Word_WordLsl_Num_int64_dict =({ - - lsl_method = Int64.shift_left}) - -(*val int64Lsr : int64 -> nat -> int64*) (* XXX: fix *) - -let instance_Word_WordLsr_Num_int64_dict =({ - - lsr_method = Int64.shift_right_logical}) - -(*val int64Asr : int64 -> nat -> int64*) (* XXX: fix *) - -let instance_Word_WordAsr_Num_int64_dict =({ - - asr_method = Int64.shift_right}) - - -(* ----------------------- *) -(* Words via bit sequences *) -(* ----------------------- *) - -(*val defaultLnot : forall 'a. (bitSequence -> 'a) -> ('a -> bitSequence) -> 'a -> 'a*) -let defaultLnot fromBitSeq toBitSeq x = (fromBitSeq (bitSeqNegate (toBitSeq x))) - -(*val defaultLand : forall 'a. (bitSequence -> 'a) -> ('a -> bitSequence) -> 'a -> 'a -> 'a*) -let defaultLand fromBitSeq toBitSeq x1 x2 = (fromBitSeq (bitSeqAnd (toBitSeq x1) (toBitSeq x2))) - -(*val defaultLor : forall 'a. (bitSequence -> 'a) -> ('a -> bitSequence) -> 'a -> 'a -> 'a*) -let defaultLor fromBitSeq toBitSeq x1 x2 = (fromBitSeq (bitSeqOr (toBitSeq x1) (toBitSeq x2))) - -(*val defaultLxor : forall 'a. (bitSequence -> 'a) -> ('a -> bitSequence) -> 'a -> 'a -> 'a*) -let defaultLxor fromBitSeq toBitSeq x1 x2 = (fromBitSeq (bitSeqXor (toBitSeq x1) (toBitSeq x2))) - -(*val defaultLsl : forall 'a. (bitSequence -> 'a) -> ('a -> bitSequence) -> 'a -> nat -> 'a*) -let defaultLsl fromBitSeq toBitSeq x n = (fromBitSeq (bitSeqShiftLeft (toBitSeq x) n)) - -(*val defaultLsr : forall 'a. (bitSequence -> 'a) -> ('a -> bitSequence) -> 'a -> nat -> 'a*) -let defaultLsr fromBitSeq toBitSeq x n = (fromBitSeq (bitSeqLogicalShiftRight (toBitSeq x) n)) - -(*val defaultAsr : forall 'a. (bitSequence -> 'a) -> ('a -> bitSequence) -> 'a -> nat -> 'a*) -let defaultAsr fromBitSeq toBitSeq x n = (fromBitSeq (bitSeqArithmeticShiftRight (toBitSeq x) n)) - -(* ----------------------- *) -(* integer *) -(* ----------------------- *) - -(*val integerLnot : integer -> integer*) -let integerLnot i = (Big_int.minus_big_int( Big_int.add_big_int i(Big_int.big_int_of_int 1))) - -let instance_Word_WordNot_Num_integer_dict =({ - - lnot_method = integerLnot}) - - -(*val integerLor : integer -> integer -> integer*) -(*let integerLor i1 i2 = defaultLor integerFromBitSeq (bitSeqFromInteger Nothing) i1 i2*) - -let instance_Word_WordOr_Num_integer_dict =({ - - lor_method = Big_int.or_big_int}) - -(*val integerLxor : integer -> integer -> integer*) -(*let integerLxor i1 i2 = defaultLxor integerFromBitSeq (bitSeqFromInteger Nothing) i1 i2*) - -let instance_Word_WordXor_Num_integer_dict =({ - - lxor_method = Big_int.xor_big_int}) - -(*val integerLand : integer -> integer -> integer*) -(*let integerLand i1 i2 = defaultLand integerFromBitSeq (bitSeqFromInteger Nothing) i1 i2*) - -let instance_Word_WordAnd_Num_integer_dict =({ - - land_method = Big_int.and_big_int}) - -(*val integerLsl : integer -> nat -> integer*) -(*let integerLsl i n = defaultLsl integerFromBitSeq (bitSeqFromInteger Nothing) i n*) - -let instance_Word_WordLsl_Num_integer_dict =({ - - lsl_method = Big_int.shift_left_big_int}) - -(*val integerAsr : integer -> nat -> integer*) -(*let integerAsr i n = defaultAsr integerFromBitSeq (bitSeqFromInteger Nothing) i n*) - -let instance_Word_WordLsr_Num_integer_dict =({ - - lsr_method = Big_int.shift_right_big_int}) - -let instance_Word_WordAsr_Num_integer_dict =({ - - asr_method = Big_int.shift_right_big_int}) - - -(* ----------------------- *) -(* int *) -(* ----------------------- *) - -(* sometimes it is convenient to be able to perform bit-operations on ints. - However, since int is not well-defined (it has different size on different systems), - it should be used very carefully and only for operations that don't depend on the - bitwidth of int *) - -(*val intFromBitSeq : bitSequence -> int*) -let intFromBitSeq bs = (Big_int.int_of_big_int (integerFromBitSeq (resizeBitSeq (Some( 31)) bs))) - - -(*val bitSeqFromInt : int -> bitSequence*) -let bitSeqFromInt i = (bitSeqFromInteger (Some( 31)) (Big_int.big_int_of_int i)) - - -(*val intLnot : int -> int*) -(*let intLnot i = Instance_Num_NumNegate_Num_int.~((Instance_Num_NumAdd_Num_int.+) i 1)*) - -let instance_Word_WordNot_Num_int_dict =({ - - lnot_method = lnot}) - -(*val intLor : int -> int -> int*) -(*let intLor i1 i2 = defaultLor intFromBitSeq bitSeqFromInt i1 i2*) - -let instance_Word_WordOr_Num_int_dict =({ - - lor_method = (lor)}) - -(*val intLxor : int -> int -> int*) -(*let intLxor i1 i2 = defaultLxor intFromBitSeq bitSeqFromInt i1 i2*) - -let instance_Word_WordXor_Num_int_dict =({ - - lxor_method = (lxor)}) - -(*val intLand : int -> int -> int*) -(*let intLand i1 i2 = defaultLand intFromBitSeq bitSeqFromInt i1 i2*) - -let instance_Word_WordAnd_Num_int_dict =({ - - land_method = (land)}) - -(*val intLsl : int -> nat -> int*) -(*let intLsl i n = defaultLsl intFromBitSeq bitSeqFromInt i n*) - -let instance_Word_WordLsl_Num_int_dict =({ - - lsl_method = (lsl)}) - -(*val intAsr : int -> nat -> int*) -(*let intAsr i n = defaultAsr intFromBitSeq bitSeqFromInt i n*) - -let instance_Word_WordAsr_Num_int_dict =({ - - asr_method = (asr)}) - - - -(* ----------------------- *) -(* natural *) -(* ----------------------- *) - -(* some operations work also on positive numbers *) - -(*val naturalFromBitSeq : bitSequence -> natural*) -let naturalFromBitSeq bs = (Big_int.abs_big_int (integerFromBitSeq bs)) - -(*val bitSeqFromNatural : maybe nat -> natural -> bitSequence*) -let bitSeqFromNatural len n = (bitSeqFromInteger len ( n)) - -(*val naturalLor : natural -> natural -> natural*) -(*let naturalLor i1 i2 = defaultLor naturalFromBitSeq (bitSeqFromNatural Nothing) i1 i2*) - -let instance_Word_WordOr_Num_natural_dict =({ - - lor_method = Big_int.or_big_int}) - -(*val naturalLxor : natural -> natural -> natural*) -(*let naturalLxor i1 i2 = defaultLxor naturalFromBitSeq (bitSeqFromNatural Nothing) i1 i2*) - -let instance_Word_WordXor_Num_natural_dict =({ - - lxor_method = Big_int.xor_big_int}) - -(*val naturalLand : natural -> natural -> natural*) -(*let naturalLand i1 i2 = defaultLand naturalFromBitSeq (bitSeqFromNatural Nothing) i1 i2*) - -let instance_Word_WordAnd_Num_natural_dict =({ - - land_method = Big_int.and_big_int}) - -(*val naturalLsl : natural -> nat -> natural*) -(*let naturalLsl i n = defaultLsl naturalFromBitSeq (bitSeqFromNatural Nothing) i n*) - -let instance_Word_WordLsl_Num_natural_dict =({ - - lsl_method = Big_int.shift_left_big_int}) - -(*val naturalAsr : natural -> nat -> natural*) -(*let naturalAsr i n = defaultAsr naturalFromBitSeq (bitSeqFromNatural Nothing) i n*) - -let instance_Word_WordLsr_Num_natural_dict =({ - - lsr_method = Big_int.shift_right_big_int}) - -let instance_Word_WordAsr_Num_natural_dict =({ - - asr_method = Big_int.shift_right_big_int}) - - -(* ----------------------- *) -(* nat *) -(* ----------------------- *) - -(* sometimes it is convenient to be able to perform bit-operations on nats. - However, since nat is not well-defined (it has different size on different systems), - it should be used very carefully and only for operations that don't depend on the - bitwidth of nat *) - -(*val natFromBitSeq : bitSequence -> nat*) -let natFromBitSeq bs = (Big_int.int_of_big_int (naturalFromBitSeq (resizeBitSeq (Some( 31)) bs))) - - -(*val bitSeqFromNat : nat -> bitSequence*) -let bitSeqFromNat i = (bitSeqFromNatural (Some( 31)) (Big_int.big_int_of_int i)) - - -(*val natLor : nat -> nat -> nat*) -(*let natLor i1 i2 = defaultLor natFromBitSeq bitSeqFromNat i1 i2*) - -let instance_Word_WordOr_nat_dict =({ - - lor_method = (lor)}) - -(*val natLxor : nat -> nat -> nat*) -(*let natLxor i1 i2 = defaultLxor natFromBitSeq bitSeqFromNat i1 i2*) - -let instance_Word_WordXor_nat_dict =({ - - lxor_method = (lxor)}) - -(*val natLand : nat -> nat -> nat*) -(*let natLand i1 i2 = defaultLand natFromBitSeq bitSeqFromNat i1 i2*) - -let instance_Word_WordAnd_nat_dict =({ - - land_method = (land)}) - -(*val natLsl : nat -> nat -> nat*) -(*let natLsl i n = defaultLsl natFromBitSeq bitSeqFromNat i n*) - -let instance_Word_WordLsl_nat_dict =({ - - lsl_method = (lsl)}) - -(*val natAsr : nat -> nat -> nat*) -(*let natAsr i n = defaultAsr natFromBitSeq bitSeqFromNat i n*) - -let instance_Word_WordAsr_nat_dict =({ - - asr_method = (asr)}) - diff --git a/lib/ocaml_rts/linksem/src_lem_library/nat_big_num.ml b/lib/ocaml_rts/linksem/src_lem_library/nat_big_num.ml deleted file mode 100644 index 2320188c..00000000 --- a/lib/ocaml_rts/linksem/src_lem_library/nat_big_num.ml +++ /dev/null @@ -1,18 +0,0 @@ -module BI = Big_int - -type num = BI.big_int -let (<) = BI.lt_big_int -let (<=) = BI.le_big_int -let (>) = BI.gt_big_int -let (>=) = BI.ge_big_int -let (+) = BI.add_big_int -let (-) x y = - let d = BI.sub_big_int x y in - if d < BI.zero_big_int then - BI.zero_big_int - else - d -let ( * ) = BI.mult_big_int -let (/) = BI.div_big_int -let (mod) = BI.mod_big_int -let string_of_num = BI.string_of_big_int diff --git a/lib/ocaml_rts/linksem/src_lem_library/nat_big_num.mli b/lib/ocaml_rts/linksem/src_lem_library/nat_big_num.mli deleted file mode 100644 index b6f6eb63..00000000 --- a/lib/ocaml_rts/linksem/src_lem_library/nat_big_num.mli +++ /dev/null @@ -1,11 +0,0 @@ -type num -val (<) : num -> num -> bool -val (<=) : num -> num -> bool -val (>) : num -> num -> bool -val (>=) : num -> num -> bool -val (+) : num -> num -> num -val (-) : num -> num -> num -val ( * ) : num -> num -> num -val (/) : num -> num -> num -val (mod) : num -> num -> num -val string_of_num : num -> string diff --git a/lib/ocaml_rts/linksem/src_lem_library/nat_num.ml b/lib/ocaml_rts/linksem/src_lem_library/nat_num.ml deleted file mode 100755 index 50165e6d..00000000 --- a/lib/ocaml_rts/linksem/src_lem_library/nat_num.ml +++ /dev/null @@ -1,43 +0,0 @@ -type nat = int -type natural = Big_int.big_int - -let nat_monus x y = - let d = x - y in - if d < 0 then - 0 - else - d - -let natural_monus x y = - (if Big_int.le_big_int x y then - Big_int.zero_big_int - else - (Big_int.sub_big_int x y)) - -let nat_pred x = nat_monus x 1 -let natural_pred x = natural_monus x Big_int.unit_big_int - -let int_mod i n = - let r = i mod n in - if (r < 0) then r + n else r - -let int_div i n = - let r = i / n in - if (i mod n < 0) then r - 1 else r - -let int32_mod i n = - let r = Int32.rem i n in - if (r < Int32.zero) then Int32.add r n else r - -let int32_div i n = - let r = Int32.div i n in - if (Int32.rem i n < Int32.zero) then Int32.pred r else r - -let int64_mod i n = - let r = Int64.rem i n in - if (r < Int64.zero) then Int64.add r n else r - -let int64_div i n = - let r = Int64.div i n in - if (Int64.rem i n < Int64.zero) then Int64.pred r else r - diff --git a/lib/ocaml_rts/linksem/src_lem_library/nat_num.mli b/lib/ocaml_rts/linksem/src_lem_library/nat_num.mli deleted file mode 100755 index d918b9df..00000000 --- a/lib/ocaml_rts/linksem/src_lem_library/nat_num.mli +++ /dev/null @@ -1,14 +0,0 @@ -type nat = int -type natural = Big_int.big_int - -val natural_monus : natural -> natural -> natural -val natural_pred : natural -> natural - -val nat_pred : nat -> nat -val nat_monus : nat -> nat -> nat -val int_div : int -> int -> int -val int32_div : Int32.t -> Int32.t -> Int32.t -val int64_div : Int64.t -> Int64.t -> Int64.t -val int_mod : int -> int -> int -val int32_mod : Int32.t -> Int32.t -> Int32.t -val int64_mod : Int64.t -> Int64.t -> Int64.t diff --git a/lib/ocaml_rts/linksem/src_lem_library/pmap.ml b/lib/ocaml_rts/linksem/src_lem_library/pmap.ml deleted file mode 100755 index 9e9f607b..00000000 --- a/lib/ocaml_rts/linksem/src_lem_library/pmap.ml +++ /dev/null @@ -1,321 +0,0 @@ -(***********************************************************************) -(* *) -(* Objective Caml *) -(* *) -(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *) -(* *) -(* Copyright 1996 Institut National de Recherche en Informatique et *) -(* en Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU Library General Public License, with *) -(* the special exception on linking described in file ../LICENSE. *) -(* *) -(***********************************************************************) - -(* Modified by Susmit Sarkar 2010-11-30 *) -(* $Id: map.ml 10468 2010-05-25 13:29:43Z frisch $ *) - -(* A map from ordered keys *) - -type ('key,'a) rep = - Empty - | Node of ('key,'a) rep * 'key * 'a * ('key,'a) rep * int - -let height = function - Empty -> 0 - | Node(_,_,_,_,h) -> h - -let create l x d r = - let hl = height l and hr = height r in - Node(l, x, d, r, (if hl >= hr then hl + 1 else hr + 1)) - -let singleton x d = Node(Empty, x, d, Empty, 1) - -let bal l x d r = - let hl = match l with Empty -> 0 | Node(_,_,_,_,h) -> h in - let hr = match r with Empty -> 0 | Node(_,_,_,_,h) -> h in - if hl > hr + 2 then begin - match l with - Empty -> invalid_arg "Map.bal" - | Node(ll, lv, ld, lr, _) -> - if height ll >= height lr then - create ll lv ld (create lr x d r) - else begin - match lr with - Empty -> invalid_arg "Map.bal" - | Node(lrl, lrv, lrd, lrr, _)-> - create (create ll lv ld lrl) lrv lrd (create lrr x d r) - end - end else if hr > hl + 2 then begin - match r with - Empty -> invalid_arg "Map.bal" - | Node(rl, rv, rd, rr, _) -> - if height rr >= height rl then - create (create l x d rl) rv rd rr - else begin - match rl with - Empty -> invalid_arg "Map.bal" - | Node(rll, rlv, rld, rlr, _) -> - create (create l x d rll) rlv rld (create rlr rv rd rr) - end - end else - Node(l, x, d, r, (if hl >= hr then hl + 1 else hr + 1)) - -let empty = Empty - -let is_empty = function Empty -> true | _ -> false - -let rec add cmp x data = function - Empty -> - Node(Empty, x, data, Empty, 1) - | Node(l, v, d, r, h) -> - let c = cmp x v in - if c = 0 then - Node(l, x, data, r, h) - else if c < 0 then - bal (add cmp x data l) v d r - else - bal l v d (add cmp x data r) - -let rec find cmp x = function - Empty -> - raise Not_found - | Node(l, v, d, r, _) -> - let c = cmp x v in - if c = 0 then d - else find cmp x (if c < 0 then l else r) - -let rec mem cmp x = function - Empty -> - false - | Node(l, v, d, r, _) -> - let c = cmp x v in - c = 0 || mem cmp x (if c < 0 then l else r) - -let rec min_binding = function - Empty -> raise Not_found - | Node(Empty, x, d, r, _) -> (x, d) - | Node(l, x, d, r, _) -> min_binding l - -let rec max_binding = function - Empty -> raise Not_found - | Node(l, x, d, Empty, _) -> (x, d) - | Node(l, x, d, r, _) -> max_binding r - -let rec remove_min_binding = function - Empty -> invalid_arg "Map.remove_min_elt" - | Node(Empty, x, d, r, _) -> r - | Node(l, x, d, r, _) -> bal (remove_min_binding l) x d r - -let merge t1 t2 = - match (t1, t2) with - (Empty, t) -> t - | (t, Empty) -> t - | (_, _) -> - let (x, d) = min_binding t2 in - bal t1 x d (remove_min_binding t2) - -let rec remove cmp x = function - Empty -> - Empty - | Node(l, v, d, r, h) -> - let c = cmp x v in - if c = 0 then - merge l r - else if c < 0 then - bal (remove cmp x l) v d r - else - bal l v d (remove cmp x r) - -let rec iter f = function - Empty -> () - | Node(l, v, d, r, _) -> - iter f l; f v d; iter f r - -let rec map f = function - Empty -> - Empty - | Node(l, v, d, r, h) -> - let l' = map f l in - let d' = f d in - let r' = map f r in - Node(l', v, d', r', h) - -let rec mapi f = function - Empty -> - Empty - | Node(l, v, d, r, h) -> - let l' = mapi f l in - let d' = f v d in - let r' = mapi f r in - Node(l', v, d', r', h) - -let rec fold f m accu = - match m with - Empty -> accu - | Node(l, v, d, r, _) -> - fold f r (f v d (fold f l accu)) - -let rec for_all p = function - Empty -> true - | Node(l, v, d, r, _) -> p v d && for_all p l && for_all p r - -let rec exists p = function - Empty -> false - | Node(l, v, d, r, _) -> p v d || exists p l || exists p r - -let filter cmp p s = - let rec filt accu = function - | Empty -> accu - | Node(l, v, d, r, _) -> - filt (filt (if p v d then add cmp v d accu else accu) l) r in - filt Empty s - -let partition cmp p s = - let rec part (t, f as accu) = function - | Empty -> accu - | Node(l, v, d, r, _) -> - part (part (if p v d then (add cmp v d t, f) else (t, add cmp v d f)) l) r in - part (Empty, Empty) s - - (* Same as create and bal, but no assumptions are made on the - relative heights of l and r. *) - -let rec join cmp l v d r = - match (l, r) with - (Empty, _) -> add cmp v d r - | (_, Empty) -> add cmp v d l - | (Node(ll, lv, ld, lr, lh), Node(rl, rv, rd, rr, rh)) -> - if lh > rh + 2 then bal ll lv ld (join cmp lr v d r) else - if rh > lh + 2 then bal (join cmp l v d rl) rv rd rr else - create l v d r - - (* Merge two trees l and r into one. - All elements of l must precede the elements of r. - No assumption on the heights of l and r. *) - -let concat cmp t1 t2 = - match (t1, t2) with - (Empty, t) -> t - | (t, Empty) -> t - | (_, _) -> - let (x, d) = min_binding t2 in - join cmp t1 x d (remove_min_binding t2) - -let concat_or_join cmp t1 v d t2 = - match d with - | Some d -> join cmp t1 v d t2 - | None -> concat cmp t1 t2 - -let rec split cmp x = function - Empty -> - (Empty, None, Empty) - | Node(l, v, d, r, _) -> - let c = cmp x v in - if c = 0 then (l, Some d, r) - else if c < 0 then - let (ll, pres, rl) = split cmp x l in (ll, pres, join cmp rl v d r) - else - let (lr, pres, rr) = split cmp x r in (join cmp l v d lr, pres, rr) - -let rec merge cmp f s1 s2 = - match (s1, s2) with - (Empty, Empty) -> Empty - | (Node (l1, v1, d1, r1, h1), _) when h1 >= height s2 -> - let (l2, d2, r2) = split cmp v1 s2 in - concat_or_join cmp (merge cmp f l1 l2) v1 (f v1 (Some d1) d2) (merge cmp f r1 r2) - | (_, Node (l2, v2, d2, r2, h2)) -> - let (l1, d1, r1) = split cmp v2 s1 in - concat_or_join cmp (merge cmp f l1 l2) v2 (f v2 d1 (Some d2)) (merge cmp f r1 r2) - | _ -> - assert false - -type ('key,'a) enumeration = End | More of 'key * 'a * ('key,'a) rep * ('key,'a) enumeration - -let rec cons_enum m e = - match m with - Empty -> e - | Node(l, v, d, r, _) -> cons_enum l (More(v, d, r, e)) - -let compare cmp_key cmp_a m1 m2 = - let rec compare_aux e1 e2 = - match (e1, e2) with - (End, End) -> 0 - | (End, _) -> -1 - | (_, End) -> 1 - | (More(v1, d1, r1, e1), More(v2, d2, r2, e2)) -> - let c = cmp_key v1 v2 in - if c <> 0 then c else - let c = cmp_a d1 d2 in - if c <> 0 then c else - compare_aux (cons_enum r1 e1) (cons_enum r2 e2) - in compare_aux (cons_enum m1 End) (cons_enum m2 End) - -let equal cmp_key cmp_a m1 m2 = - let rec equal_aux e1 e2 = - match (e1, e2) with - (End, End) -> true - | (End, _) -> false - | (_, End) -> false - | (More(v1, d1, r1, e1), More(v2, d2, r2, e2)) -> - cmp_key v1 v2 = 0 && cmp_a d1 d2 && - equal_aux (cons_enum r1 e1) (cons_enum r2 e2) - in equal_aux (cons_enum m1 End) (cons_enum m2 End) - -let rec cardinal = function - Empty -> 0 - | Node(l, _, _, r, _) -> cardinal l + 1 + cardinal r - -let rec bindings_aux accu = function - Empty -> accu - | Node(l, v, d, r, _) -> bindings_aux ((v, d) :: bindings_aux accu r) l - -let bindings s = - bindings_aux [] s - -let choose = min_binding - - -(* Wrapper functions now *) - -type ('key,'a) map = {cmp:'key -> 'key -> int; m:('key,'a) rep} - -let empty cmp = {cmp = cmp; m = Empty} -let is_empty m = is_empty m.m -let mem k m = mem m.cmp k m.m -let add k a m = {m with m = add m.cmp k a m.m} -let singleton cmp k a = {cmp = cmp; m = singleton k a} -let remove k m = {m with m = remove m.cmp k m.m} -let merge f a b = {cmp = a.cmp; (* does not matter, a and b should have the same comparison function *) - m = merge a.cmp f a.m b.m;} -let union a b = merge (fun k o1 o2 -> - match (o1, o2) with - | (_, Some v) -> Some v - | (Some v, _) -> Some v - | (_, _) -> None) a b - let compare f a b = compare a.cmp f a.m b.m -let equal f a b = equal a.cmp f a.m b.m -let iter f m = iter f m.m -let fold f m b = fold f m.m b -let for_all f m = for_all f m.m -let exist f m = exists f m.m -let filter f m = {m with m = filter m.cmp f m.m} -let partition f m = - let m1,m2 = partition m.cmp f m.m in - ({m with m = m1},{m with m = m2}) -let cardinal m = cardinal m.m -let domain m = Pset.from_list m.cmp (List.map fst (bindings m.m)) -let range cmp m = Pset.from_list cmp (List.map snd (bindings m.m)) -let bindings_list m = bindings m.m -let bindings cmp m = Pset.from_list cmp (bindings m.m) -let min_binding m = min_binding m.m -let max_binding m = max_binding m.m -let choose m = choose m.m -let split k m = - let (m1,opt,m2) = split m.cmp k m.m in - ({m with m = m1},opt,{m with m = m2}) -let find k m = find m.cmp k m.m -let lookup k m = try Some (find k m) with Not_found -> None -let map f m = {m with m = map f m.m} -let mapi f m = {m with m = mapi f m.m} - -let from_set f s = Pset.fold (fun k m -> (add k (f k) m)) s (empty (Pset.get_elem_compare s)) diff --git a/lib/ocaml_rts/linksem/src_lem_library/pmap.mli b/lib/ocaml_rts/linksem/src_lem_library/pmap.mli deleted file mode 100755 index f2016418..00000000 --- a/lib/ocaml_rts/linksem/src_lem_library/pmap.mli +++ /dev/null @@ -1,190 +0,0 @@ -(***********************************************************************) -(* *) -(* Objective Caml *) -(* *) -(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *) -(* *) -(* Copyright 1996 Institut National de Recherche en Informatique et *) -(* en Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU Library General Public License, with *) -(* the special exception on linking described in file ../LICENSE. *) -(* *) -(***********************************************************************) - -(* Modified by Susmit Sarkar 2010-11-30 *) -(* $Id: map.mli 10632 2010-07-24 14:16:58Z garrigue $ *) - -(** Association tables over ordered types. - - This module implements applicative association tables, also known as - finite maps or dictionaries, given a total ordering function - over the keys. - All operations over maps are purely applicative (no side-effects). - The implementation uses balanced binary trees, and therefore searching - and insertion take time logarithmic in the size of the map. -*) - -type ('key,+'a) map - (** The type of maps from type ['key] to type ['a]. *) - -val empty: ('key -> 'key -> int) -> ('key,'a) map - (** The empty map. *) - -val is_empty: ('key,'a) map -> bool - (** Test whether a map is empty or not. *) - -val mem: 'key -> ('key,'a) map -> bool - (** [mem x m] returns [true] if [m] contains a binding for [x], - and [false] otherwise. *) - -val add: 'key -> 'a -> ('key,'a) map -> ('key,'a) map - (** [add x y m] returns a map containing the same bindings as - [m], plus a binding of [x] to [y]. If [x] was already bound - in [m], its previous binding disappears. *) - -val singleton: ('key -> 'key -> int) -> 'key -> 'a -> ('key,'a) map - (** [singleton x y] returns the one-element map that contains a binding [y] - for [x]. - @since 3.12.0 - *) - -val remove: 'key -> ('key,'a) map -> ('key,'a) map - (** [remove x m] returns a map containing the same bindings as - [m], except for [x] which is unbound in the returned map. *) - -val merge: - ('key -> 'a option -> 'b option -> 'c option) -> ('key,'a) map -> ('key,'b) map -> ('key,'c) map - (** [merge f m1 m2] computes a map whose keys is a subset of keys of [m1] - and of [m2]. The presence of each such binding, and the corresponding - value, is determined with the function [f]. - @since 3.12.0 - *) - -val union: ('key,'a) map -> ('key,'a) map -> ('key,'a) map - (** [union m1 m2] computes a map whose keys is a subset of keys of [m1] - and of [m2]. The bindings in m2 take precedence. - @since 3.12.0 - *) - -val compare: ('a -> 'a -> int) -> ('key,'a) map -> ('key,'a) map -> int - (** Total ordering between maps. The first argument is a total ordering - used to compare data associated with equal keys in the two maps. *) - -val equal: ('a -> 'a -> bool) -> ('key,'a) map -> ('key,'a) map -> bool - (** [equal cmp m1 m2] tests whether the maps [m1] and [m2] are - equal, that is, contain equal keys and associate them with - equal data. [cmp] is the equality predicate used to compare - the data associated with the keys. *) - -val iter: ('key -> 'a -> unit) -> ('key,'a) map -> unit - (** [iter f m] applies [f] to all bindings in map [m]. - [f] receives the key as first argument, and the associated value - as second argument. The bindings are passed to [f] in increasing - order with respect to the ordering over the type of the keys. *) - -val fold: ('key -> 'a -> 'b -> 'b) -> ('key,'a) map -> 'b -> 'b - (** [fold f m a] computes [(f kN dN ... (f k1 d1 a)...)], - where [k1 ... kN] are the keys of all bindings in [m] - (in increasing order), and [d1 ... dN] are the associated data. *) - -val for_all: ('key -> 'a -> bool) -> ('key,'a) map -> bool - (** [for_all p m] checks if all the bindings of the map - satisfy the predicate [p]. - @since 3.12.0 - *) - -val exist: ('key -> 'a -> bool) -> ('key,'a) map -> bool - (** [exists p m] checks if at least one binding of the map - satisfy the predicate [p]. - @since 3.12.0 - *) - -val filter: ('key -> 'a -> bool) -> ('key,'a) map -> ('key,'a) map - (** [filter p m] returns the map with all the bindings in [m] - that satisfy predicate [p]. - @since 3.12.0 - *) - -val partition: ('key -> 'a -> bool) -> ('key,'a) map -> ('key,'a) map * ('key,'a) map - (** [partition p m] returns a pair of maps [(m1, m2)], where - [m1] contains all the bindings of [s] that satisfy the - predicate [p], and [m2] is the map with all the bindings of - [s] that do not satisfy [p]. - @since 3.12.0 - *) - -val cardinal: ('key,'a) map -> int - (** Return the number of bindings of a map. - @since 3.12.0 - *) - -val bindings_list: ('key,'a) map -> ('key * 'a) list - (** Return the list of all bindings of the given map. - The returned list is sorted in increasing order with respect - to the ordering [Ord.compare], where [Ord] is the argument - given to {!Map.Make}. - @since 3.12.0 - *) - -val bindings: (('key * 'a) -> ('key * 'a) -> int) -> ('key,'a) map -> ('key * 'a) Pset.set - (** Return a set of all bindings of the given map. *) - -(** [domain m] returns the domain of the map [m], i.e. the - set of keys of this map. *) -val domain : ('key,'a) map -> 'key Pset.set - -(** [range m] returns the range of the map [m], i.e. the - set of all values stored in this map. *) -val range : ('a -> 'a -> int) -> ('key,'a) map -> 'a Pset.set - -val min_binding: ('key,'a) map -> ('key * 'a) - (** Return the smallest binding of the given map - (with respect to the [Ord.compare] ordering), or raise - [Not_found] if the map is empty. - @since 3.12.0 - *) - -val max_binding: ('key,'a) map -> ('key * 'a) - (** Same as {!Map.S.min_binding}, but returns the largest binding - of the given map. - @since 3.12.0 - *) - -val choose: ('key,'a) map -> ('key * 'a) - (** Return one binding of the given map, or raise [Not_found] if - the map is empty. Which binding is chosen is unspecified, - but equal bindings will be chosen for equal maps. - @since 3.12.0 - *) - -val split: 'key -> ('key,'a) map -> ('key,'a) map * 'a option * ('key,'a) map - (** [split x m] returns a triple [(l, data, r)], where - [l] is the map with all the bindings of [m] whose key - is strictly less than [x]; - [r] is the map with all the bindings of [m] whose key - is strictly greater than [x]; - [data] is [None] if [m] contains no binding for [x], - or [Some v] if [m] binds [v] to [x]. - @since 3.12.0 - *) - -val find: 'key -> ('key,'a) map -> 'a - (** [find x m] returns the current binding of [x] in [m], - or raises [Not_found] if no such binding exists. *) - -val lookup: 'key -> ('key,'a) map -> 'a option - (** [lookup x m] returns the current binding of [x] in [m]. In contrast to [find], - it returns [None] instead of raising an exception, if no such binding exists. *) - -val map: ('a -> 'b) -> ('key,'a) map -> ('key,'b) map - (** [map f m] returns a map with same domain as [m], where the - associated value [a] of all bindings of [m] has been - replaced by the result of the application of [f] to [a]. - The bindings are passed to [f] in increasing order - with respect to the ordering over the type of the keys. *) - -val mapi: ('key -> 'a -> 'b) -> ('key,'a) map -> ('key,'b) map - (** Same as {!Map.S.map}, but the function receives as arguments both the - key and the associated value for each binding of the map. *) - -val from_set : ('key -> 'v) -> ('key Pset.set) -> ('key, 'v) map diff --git a/lib/ocaml_rts/linksem/src_lem_library/pset.ml b/lib/ocaml_rts/linksem/src_lem_library/pset.ml deleted file mode 100755 index 35335e88..00000000 --- a/lib/ocaml_rts/linksem/src_lem_library/pset.ml +++ /dev/null @@ -1,522 +0,0 @@ -(***********************************************************************) -(* *) -(* Objective Caml *) -(* *) -(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *) -(* *) -(* Copyright 1996 Institut National de Recherche en Informatique et *) -(* en Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU Library General Public License, with *) -(* the special exception on linking described in file ../LICENSE. *) -(* *) -(***********************************************************************) - -(* Modified by Scott Owens 2010-10-28 *) - -(* $Id: set.ml 6694 2004-11-25 00:06:06Z doligez $ *) - -(* Sets over ordered types *) - -type 'a rep = Empty | Node of 'a rep * 'a * 'a rep * int - -(* Sets are represented by balanced binary trees (the heights of the - children differ by at most 2 *) - -let height = function - Empty -> 0 - | Node(_, _, _, h) -> h - -(* Creates a new node with left son l, value v and right son r. - We must have all elements of l < v < all elements of r. - l and r must be balanced and | height l - height r | <= 2. - Inline expansion of height for better speed. *) - -let create l v r = - let hl = match l with Empty -> 0 | Node(_,_,_,h) -> h in - let hr = match r with Empty -> 0 | Node(_,_,_,h) -> h in - Node(l, v, r, (if hl >= hr then hl + 1 else hr + 1)) - -(* Same as create, but performs one step of rebalancing if necessary. - Assumes l and r balanced and | height l - height r | <= 3. - Inline expansion of create for better speed in the most frequent case - where no rebalancing is required. *) - -let bal l v r = - let hl = match l with Empty -> 0 | Node(_,_,_,h) -> h in - let hr = match r with Empty -> 0 | Node(_,_,_,h) -> h in - if hl > hr + 2 then begin - match l with - Empty -> invalid_arg "Set.bal" - | Node(ll, lv, lr, _) -> - if height ll >= height lr then - create ll lv (create lr v r) - else begin - match lr with - Empty -> invalid_arg "Set.bal" - | Node(lrl, lrv, lrr, _)-> - create (create ll lv lrl) lrv (create lrr v r) - end - end else if hr > hl + 2 then begin - match r with - Empty -> invalid_arg "Set.bal" - | Node(rl, rv, rr, _) -> - if height rr >= height rl then - create (create l v rl) rv rr - else begin - match rl with - Empty -> invalid_arg "Set.bal" - | Node(rll, rlv, rlr, _) -> - create (create l v rll) rlv (create rlr rv rr) - end - end else - Node(l, v, r, (if hl >= hr then hl + 1 else hr + 1)) - -(* Insertion of one element *) - -let rec add cmp x = function - Empty -> Node(Empty, x, Empty, 1) - | Node(l, v, r, _) as t -> - let c = cmp x v in - if c = 0 then t else - if c < 0 then bal (add cmp x l) v r else bal l v (add cmp x r) - -(* Same as create and bal, but no assumptions are made on the - relative heights of l and r. *) - -let rec join cmp l v r = - match (l, r) with - (Empty, _) -> add cmp v r - | (_, Empty) -> add cmp v l - | (Node(ll, lv, lr, lh), Node(rl, rv, rr, rh)) -> - if lh > rh + 2 then bal ll lv (join cmp lr v r) else - if rh > lh + 2 then bal (join cmp l v rl) rv rr else - create l v r - -(* Smallest and greatest element of a set *) - -let rec min_elt = function - Empty -> raise Not_found - | Node(Empty, v, r, _) -> v - | Node(l, v, r, _) -> min_elt l - -let rec max_elt = function - Empty -> raise Not_found - | Node(l, v, Empty, _) -> v - | Node(l, v, r, _) -> max_elt r - -(* Remove the smallest element of the given set *) - -let rec remove_min_elt = function - Empty -> invalid_arg "Set.remove_min_elt" - | Node(Empty, v, r, _) -> r - | Node(l, v, r, _) -> bal (remove_min_elt l) v r - -(* Merge two trees l and r into one. - All elements of l must precede the elements of r. - Assume | height l - height r | <= 2. *) - -let merge t1 t2 = - match (t1, t2) with - (Empty, t) -> t - | (t, Empty) -> t - | (_, _) -> bal t1 (min_elt t2) (remove_min_elt t2) - -(* Merge two trees l and r into one. - All elements of l must precede the elements of r. - No assumption on the heights of l and r. *) - -let concat cmp t1 t2 = - match (t1, t2) with - (Empty, t) -> t - | (t, Empty) -> t - | (_, _) -> join cmp t1 (min_elt t2) (remove_min_elt t2) - -(* Splitting. split x s returns a triple (l, present, r) where - - l is the set of elements of s that are < x - - r is the set of elements of s that are > x - - present is false if s contains no element equal to x, - or true if s contains an element equal to x. *) - -let rec split cmp x = function - Empty -> - (Empty, false, Empty) - | Node(l, v, r, _) -> - let c = cmp x v in - if c = 0 then (l, true, r) - else if c < 0 then - let (ll, pres, rl) = split cmp x l in (ll, pres, join cmp rl v r) - else - let (lr, pres, rr) = split cmp x r in (join cmp l v lr, pres, rr) - -(* Implementation of the set operations *) - -let empty = Empty - -let is_empty = function Empty -> true | _ -> false - -let rec mem cmp x = function - Empty -> false - | Node(l, v, r, _) -> - let c = cmp x v in - c = 0 || mem cmp x (if c < 0 then l else r) - -let singleton x = Node(Empty, x, Empty, 1) - -let rec remove cmp x = function - Empty -> Empty - | Node(l, v, r, _) -> - let c = cmp x v in - if c = 0 then merge l r else - if c < 0 then bal (remove cmp x l) v r else bal l v (remove cmp x r) - -let rec union cmp s1 s2 = - match (s1, s2) with - (Empty, t2) -> t2 - | (t1, Empty) -> t1 - | (Node(l1, v1, r1, h1), Node(l2, v2, r2, h2)) -> - if h1 >= h2 then - if h2 = 1 then add cmp v2 s1 else begin - let (l2, _, r2) = split cmp v1 s2 in - join cmp (union cmp l1 l2) v1 (union cmp r1 r2) - end - else - if h1 = 1 then add cmp v1 s2 else begin - let (l1, _, r1) = split cmp v2 s1 in - join cmp (union cmp l1 l2) v2 (union cmp r1 r2) - end - -let rec inter cmp s1 s2 = - match (s1, s2) with - (Empty, t2) -> Empty - | (t1, Empty) -> Empty - | (Node(l1, v1, r1, _), t2) -> - match split cmp v1 t2 with - (l2, false, r2) -> - concat cmp (inter cmp l1 l2) (inter cmp r1 r2) - | (l2, true, r2) -> - join cmp (inter cmp l1 l2) v1 (inter cmp r1 r2) - -let rec diff cmp s1 s2 = - match (s1, s2) with - (Empty, t2) -> Empty - | (t1, Empty) -> t1 - | (Node(l1, v1, r1, _), t2) -> - match split cmp v1 t2 with - (l2, false, r2) -> - join cmp (diff cmp l1 l2) v1 (diff cmp r1 r2) - | (l2, true, r2) -> - concat cmp (diff cmp l1 l2) (diff cmp r1 r2) - -type 'a enumeration = End | More of 'a * 'a rep * 'a enumeration - -let rec cons_enum s e = - match s with - Empty -> e - | Node(l, v, r, _) -> cons_enum l (More(v, r, e)) - -let rec compare_aux cmp e1 e2 = - match (e1, e2) with - (End, End) -> 0 - | (End, _) -> -1 - | (_, End) -> 1 - | (More(v1, r1, e1), More(v2, r2, e2)) -> - let c = cmp v1 v2 in - if c <> 0 - then c - else compare_aux cmp (cons_enum r1 e1) (cons_enum r2 e2) - -let compare cmp s1 s2 = - compare_aux cmp (cons_enum s1 End) (cons_enum s2 End) - -let equal cmp s1 s2 = - compare cmp s1 s2 = 0 - -let rec subset cmp s1 s2 = - match (s1, s2) with - Empty, _ -> - true - | _, Empty -> - false - | Node (l1, v1, r1, _), (Node (l2, v2, r2, _) as t2) -> - let c = cmp v1 v2 in - if c = 0 then - subset cmp l1 l2 && subset cmp r1 r2 - else if c < 0 then - subset cmp (Node (l1, v1, Empty, 0)) l2 && subset cmp r1 t2 - else - subset cmp (Node (Empty, v1, r1, 0)) r2 && subset cmp l1 t2 - -let rec iter f = function - Empty -> () - | Node(l, v, r, _) -> iter f l; f v; iter f r - -let rec fold f s accu = - match s with - Empty -> accu - | Node(l, v, r, _) -> fold f r (f v (fold f l accu)) - -let map cmp f s = fold (fun e s -> add cmp (f e) s) s empty - -let map_union cmp f s = fold (fun e s -> union cmp (f e) s) s empty - - -let rec for_all p = function - Empty -> true - | Node(l, v, r, _) -> p v && for_all p l && for_all p r - -let rec exists p = function - Empty -> false - | Node(l, v, r, _) -> p v || exists p l || exists p r - -let filter cmp p s = - let rec filt accu = function - | Empty -> accu - | Node(l, v, r, _) -> - filt (filt (if p v then add cmp v accu else accu) l) r in - filt Empty s - -let partition cmp p s = - let rec part (t, f as accu) = function - | Empty -> accu - | Node(l, v, r, _) -> - part (part (if p v then (add cmp v t, f) else (t, add cmp v f)) l) r in - part (Empty, Empty) s - -let rec cardinal = function - Empty -> 0 - | Node(l, v, r, _) -> cardinal l + 1 + cardinal r - -let rec elements_aux accu = function - Empty -> accu - | Node(l, v, r, _) -> elements_aux (v :: elements_aux accu r) l - -let elements s = - elements_aux [] s - -let choose = min_elt - -type 'a set = { cmp : 'a -> 'a -> int; s : 'a rep } - -let empty c = { cmp = c; s = Empty; } - -let is_empty s = is_empty s.s - -let mem x s = mem s.cmp x s.s - -let add x s = { s with s = add s.cmp x s.s } - -let singleton c x = { cmp = c; s = singleton x } - -let remove x s = { s with s = remove s.cmp x s.s } - -let union s1 s2 = { s1 with s = union s1.cmp s1.s s2.s } - -let map_union c f s1 = { cmp = c; s = map_union c (fun x -> (f x).s) s1.s} - -let inter s1 s2 = { s1 with s = inter s1.cmp s1.s s2.s } - -let diff s1 s2 = { s1 with s = diff s1.cmp s1.s s2.s } - -let compare_by cmp s1 s2 = compare cmp s1.s s2.s - -let compare s1 s2 = compare s1.cmp s1.s s2.s - -let equal s1 s2 = equal s1.cmp s1.s s2.s - -let subset s1 s2 = subset s1.cmp s1.s s2.s -let subset_proper s1 s2 = (subset s1 s2) && not (equal s1 s2) - -let iter f s = iter f s.s - -let fold f s a = fold f s.s a - -let map c f s = {cmp = c; s = map c f s.s} - -let for_all p s = for_all p s.s - -let exists p s = exists p s.s - -let filter p s = { s with s = filter s.cmp p s.s } - -let partition p s = - let (r1,r2) = partition s.cmp p s.s in - ({s with s = r1}, {s with s = r2}) - -let cardinal s = cardinal s.s - -let elements s = elements s.s - -let min_elt s = min_elt s.s - -let min_elt_opt s = try Some (min_elt s) with Not_found -> None - -let max_elt s = max_elt s.s - -let max_elt_opt s = try Some (max_elt s) with Not_found -> None - -let choose s = choose s.s - -let set_case s c_emp c_sing c_else = match s.s with - Empty -> c_emp - | Node(Empty, v, Empty, _) -> c_sing v - | _ -> c_else - -let split x s = - let (l,present,r) = split s.cmp x s.s in - ({ s with s = l }, present, { s with s = r }) - -let from_list c l = - List.fold_left (fun s x -> add x s) (empty c) l - -let comprehension1 cmp f p s = - fold (fun x s -> if p x then add (f x) s else s) s (empty cmp) - -let comprehension2 cmp f p s1 s2 = - fold - (fun x1 s -> - fold - (fun x2 s -> - if p x1 x2 then add (f x1 x2) s else s) - s2 - s) - s1 - (empty cmp) - -let comprehension3 cmp f p s1 s2 s3 = - fold - (fun x1 s -> - fold - (fun x2 s -> - fold - (fun x3 s -> - if p x1 x2 x3 then add (f x1 x2 x3) s else s) - s3 - s) - s2 - s) - s1 - (empty cmp) - -let comprehension4 cmp f p s1 s2 s3 s4 = - fold - (fun x1 s -> - fold - (fun x2 s -> - fold - (fun x3 s -> - fold - (fun x4 s -> - if p x1 x2 x3 x4 then add (f x1 x2 x3 x4) s else s) - s4 - s) - s3 - s) - s2 - s) - s1 - (empty cmp) - -let comprehension5 cmp f p s1 s2 s3 s4 s5 = - fold - (fun x1 s -> - fold - (fun x2 s -> - fold - (fun x3 s -> - fold - (fun x4 s -> - fold - (fun x5 s -> - if p x1 x2 x3 x4 x5 then add (f x1 x2 x3 x4 x5) s else s) - s5 - s) - s4 - s) - s3 - s) - s2 - s) - s1 - (empty cmp) - -let comprehension6 cmp f p s1 s2 s3 s4 s5 s6 = - fold - (fun x1 s -> - fold - (fun x2 s -> - fold - (fun x3 s -> - fold - (fun x4 s -> - fold - (fun x5 s -> - fold - (fun x6 s -> - if p x1 x2 x3 x4 x5 x6 then add (f x1 x2 x3 x4 x5 x6) s else s) - s6 - s) - s5 - s) - s4 - s) - s3 - s) - s2 - s) - s1 - (empty cmp) - -let comprehension7 cmp f p s1 s2 s3 s4 s5 s6 s7 = - fold - (fun x1 s -> - fold - (fun x2 s -> - fold - (fun x3 s -> - fold - (fun x4 s -> - fold - (fun x5 s -> - fold - (fun x6 s -> - fold - (fun x7 s -> - if p x1 x2 x3 x4 x5 x6 x7 then add (f x1 x2 x3 x4 x5 x6 x7) s else s) - s7 - s) - s6 - s) - s5 - s) - s4 - s) - s3 - s) - s2 - s) - s1 - (empty cmp) - -let bigunion c xss = - fold union xss (empty c) - -let sigma c xs ys = - fold (fun x xys -> fold (fun y xys -> add (x,y) xys) (ys x) xys) xs (empty c) - -let cross c xs ys = sigma c xs (fun _ -> ys) - -let rec lfp s f = - let s' = f s in - if subset s' s then - s - else - lfp (union s' s) f - -let tc c r = - let one_step r = fold (fun (x,y) xs -> fold (fun (y',z) xs -> - if c (y,y) (y',y') = 0 then add (x,z) xs else xs) r xs) r (empty c) in - lfp r one_step - - -let get_elem_compare s = s.cmp - diff --git a/lib/ocaml_rts/linksem/src_lem_library/pset.mli b/lib/ocaml_rts/linksem/src_lem_library/pset.mli deleted file mode 100755 index 162d5f3b..00000000 --- a/lib/ocaml_rts/linksem/src_lem_library/pset.mli +++ /dev/null @@ -1,174 +0,0 @@ -(***********************************************************************) -(* *) -(* Objective Caml *) -(* *) -(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *) -(* *) -(* Copyright 1996 Institut National de Recherche en Informatique et *) -(* en Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU Library General Public License, with *) -(* the special exception on linking described in file ../LICENSE. *) -(* *) -(***********************************************************************) - -(* Modified by Scott Owens 2010-10-28 *) - -(* $Id: set.mli 6974 2005-07-21 14:52:45Z doligez $ *) - -(** Sets over ordered types. - - This module implements the set data structure, given a total ordering - function over the set elements. All operations over sets - are purely applicative (no side-effects). - The implementation uses balanced binary trees, and is therefore - reasonably efficient: insertion and membership take time - logarithmic in the size of the set, for instance. - *) - -type 'a set -(** The type of sets. *) - -val empty: ('a -> 'a -> int) -> 'a set -(** The empty set. *) - -val is_empty: 'a set -> bool -(** Test whether a set is empty or not. *) - -val from_list: ('a -> 'a -> int) -> 'a list -> 'a set - -val mem: 'a -> 'a set -> bool -(** [mem x s] tests whether [x] belongs to the set [s]. *) - -val add: 'a -> 'a set -> 'a set -(** [add x s] returns a set containing all elements of [s], - plus [x]. If [x] was already in [s], [s] is returned unchanged. *) - -val singleton: ('a -> 'a -> int) -> 'a -> 'a set -(** [singleton x] returns the one-element set containing only [x]. *) - -val remove: 'a -> 'a set -> 'a set -(** [remove x s] returns a set containing all elements of [s], - except [x]. If [x] was not in [s], [s] is returned unchanged. *) - -val union: 'a set -> 'a set -> 'a set -(** Set union. *) - -val inter: 'a set -> 'a set -> 'a set -(** Set intersection. *) - -(** Set difference. *) -val diff: 'a set -> 'a set -> 'a set - -val compare: 'a set -> 'a set -> int -(** Total ordering between sets. Can be used as the ordering function - for doing sets of sets. *) - -val equal: 'a set -> 'a set -> bool -(** [equal s1 s2] tests whether the sets [s1] and [s2] are - equal, that is, contain equal elements. *) - -val subset: 'a set -> 'a set -> bool -(** [subset s1 s2] tests whether the set [s1] is a subset of - the set [s2]. This includes the case where [s1] and [s2] are equal. *) - -val subset_proper : 'a set -> 'a set -> bool -(** [subset_proper s1 s2] tests whether the set [s1] is a proper subset of - the set [s2]. *) - -val iter: ('a -> unit) -> 'a set -> unit -(** [iter f s] applies [f] in turn to all elements of [s]. - The elements of [s] are presented to [f] in increasing order - with respect to the ordering over the type of the elements. *) - -val fold: ('a -> 'b -> 'b) -> 'a set -> 'b -> 'b -(** [fold f s a] computes [(f xN ... (f x2 (f x1 a))...)], - where [x1 ... xN] are the elements of [s], in increasing order. *) - -val map: ('b -> 'b -> int) -> ('a -> 'b) -> 'a set -> 'b set - -val map_union: ('b -> 'b -> int) -> ('a -> 'b set) -> 'a set -> 'b set -(** [map_union cmp f s] does the same as [bigunion cmp (map cmp' f s)]. - Because the set of sets is internally not constructed though the comparison function [cmp'] is - not needed. *) - -val for_all: ('a -> bool) -> 'a set -> bool -(** [for_all p s] checks if all elements of the set - satisfy the predicate [p]. *) - -val exists: ('a -> bool) -> 'a set -> bool -(** [exists p s] checks if at least one element of - the set satisfies the predicate [p]. *) - -val filter: ('a -> bool) -> 'a set -> 'a set -(** [filter p s] returns the set of all elements in [s] - that satisfy predicate [p]. *) - -val partition: ('a -> bool) -> 'a set -> 'a set * 'a set -(** [partition p s] returns a pair of sets [(s1, s2)], where - [s1] is the set of all the elements of [s] that satisfy the - predicate [p], and [s2] is the set of all the elements of - [s] that do not satisfy [p]. *) - -val cardinal: 'a set -> int -(** Return the number of elements of a set. *) - -val elements: 'a set -> 'a list -(** Return the list of all elements of the given set. - The returned list is sorted in increasing order with respect - to the ordering [Ord.compare], where [Ord] is the argument - given to {!Set.Make}. *) - -val min_elt: 'a set -> 'a -(** Return the smallest element of the given set - (with respect to the [Ord.compare] ordering), or raise - [Not_found] if the set is empty. *) - -val max_elt: 'a set -> 'a -(** Same as {!Set.S.min_elt}, but returns the largest element of the - given set. *) - -val min_elt_opt: 'a set -> 'a option -(** an optional version of [min_elt] *) - -val max_elt_opt: 'a set -> 'a option -(** an optional version of [max_elt] *) - -val choose: 'a set -> 'a -(** Return one element of the given set, or raise [Not_found] if - the set is empty. Which element is chosen is unspecified, - but equal elements will be chosen for equal sets. *) - -val set_case: 'a set -> 'b -> ('a -> 'b) -> 'b -> 'b -(** case-split function for sets *) - -val split: 'a -> 'a set -> 'a set * bool * 'a set - (** [split x s] returns a triple [(l, present, r)], where - [l] is the set of elements of [s] that are - strictly less than [x]; - [r] is the set of elements of [s] that are - strictly greater than [x]; - [present] is [false] if [s] contains no element equal to [x], - or [true] if [s] contains an element equal to [x]. *) - -val comprehension1 : ('b -> 'b -> int) -> ('a -> 'b) -> ('a -> bool) -> 'a set -> 'b set -val comprehension2 : ('c -> 'c -> int) -> ('a -> 'b -> 'c) -> ('a -> 'b -> bool) -> 'a set -> 'b set -> 'c set -val comprehension3 : ('d -> 'd -> int) -> ('a -> 'b -> 'c -> 'd) -> ('a -> 'b -> 'c -> bool) -> 'a set -> 'b set -> 'c set -> 'd set -val comprehension4 : ('e -> 'e -> int) -> ('a -> 'b -> 'c -> 'd -> 'e) -> ('a -> 'b -> 'c -> 'd -> bool) -> 'a set -> 'b set -> 'c set -> 'd set -> 'e set -val comprehension5 : ('f -> 'f -> int) -> ('a -> 'b -> 'c -> 'd -> 'e -> 'f) -> ('a -> 'b -> 'c -> 'd -> 'e -> bool) -> 'a set -> 'b set -> 'c set -> 'd set -> 'e set -> 'f set -val comprehension6 : ('g -> 'g -> int) -> ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g) -> ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> bool) -> 'a set -> 'b set -> 'c set -> 'd set -> 'e set -> 'f set -> 'g set -val comprehension7 : ('h -> 'h -> int) -> ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h) -> ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> bool) -> 'a set -> 'b set -> 'c set -> 'd set -> 'e set -> 'f set -> 'g set -> 'h set - -val bigunion : ('a -> 'a -> int) -> 'a set set -> 'a set - -val lfp : 'a set -> ('a set -> 'a set) -> 'a set -val tc : ('a * 'a -> 'a * 'a -> int) -> ('a * 'a) set -> ('a * 'a) set - - -val sigma : ('a * 'b -> 'a * 'b -> int) -> 'a set -> ('a -> 'b set) -> ('a * 'b) set -val cross : ('a * 'b -> 'a * 'b -> int) -> 'a set -> 'b set -> ('a * 'b) set - -val get_elem_compare : 'a set -> ('a -> 'a -> int) - -val compare_by: ('a->'a->int) -> 'a set -> 'a set -> int -(** set comparison parameterised by element comparison (ignoring the comparison functions of the argument sets*) - diff --git a/lib/ocaml_rts/linksem/src_lem_library/pset_using_lists.ml b/lib/ocaml_rts/linksem/src_lem_library/pset_using_lists.ml deleted file mode 100644 index 1fadd8f7..00000000 --- a/lib/ocaml_rts/linksem/src_lem_library/pset_using_lists.ml +++ /dev/null @@ -1,336 +0,0 @@ -(***********************************************************************) -(* *) -(* Objective Caml *) -(* *) -(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *) -(* *) -(* Copyright 1996 Institut National de Recherche en Informatique et *) -(* en Automatique. All rights reserved. This file is distributed *) -(* under the terms of the GNU Library General Public License, with *) -(* the special exception on linking described in file ../LICENSE. *) -(* *) -(***********************************************************************) - -(* Modified by Scott Owens 2010-10-28 *) -(* Modified by Kyndylan Nienhuis 2013-04-.. *) - -(* $Id: set.ml 6694 2004-11-25 00:06:06Z doligez $ *) - -(* Sets over ordered types *) - - - -(* Implementation of the set operations *) - -type 'a rep = 'a list - -exception Not_implemented - -let rec add cmp x list = - x::list - -let empty = [] - -let is_empty = function [] -> true | _ -> false - -let rec mem cmp x = function - [] -> false - | v::l -> - let c = cmp x v in - c = 0 || mem cmp x l - -let singleton x = [x] - -let rec remove cmp x = function - [] -> [] - | v::l -> - let c = cmp x v in - if c = 0 then remove cmp x l else - v::(remove cmp x l) - -let compare cmp s1 s2 = - raise Not_implemented - -let equal cmp s1 s2 = - compare cmp s1 s2 = 0 - -let rec iter f = function - [] -> () - | v::l -> iter f l; f v - -let rec fold f s accu = - match s with - [] -> accu - | v::l -> f v (fold f l accu) - -let map cmp f s = fold (fun e s -> add cmp (f e) s) s empty - -let rec for_all p = function - [] -> true - | v::l -> p v && for_all p l - -let rec exists p = function - [] -> false - | v::l -> p v || exists p l - -let rec subset cmp s1 s2 = - for_all (fun e -> mem cmp e s2) s1 - -let filter cmp p s = - let rec filt accu = function - | [] -> accu - | v::r -> - filt (if p v then add cmp v accu else accu) r in - filt [] s - -let partition cmp p s = - let rec part (l, r as accu) = function - | [] -> accu - | h::t -> - part (if p h then (add cmp h l, r) else (l, add cmp h r)) t in - part ([], []) s - -let rec union cmp s1 s2 = - match s1 with - [] -> s2 - | v::l -> v::(union cmp l s2) - -let rec inter cmp s1 s2 = - filter cmp (fun e -> mem cmp e s2) s1 - -let rec cardinal cmp = function - [] -> 0 - | h::t -> (cardinal cmp (remove cmp h t)) + 1 - -let elements s = - s - -let diff cmp s s = - raise Not_implemented - -let min_elt s = - raise Not_implemented - -let max_elt s = - raise Not_implemented - -let split cmp x s = - raise Not_implemented - -(* It's not determenistic in the sense that s1.choose = s2.choose given that s1 equals s2 *) -let choose = function - [] -> raise Not_found - | h::_ -> h - -type 'a set = { cmp : 'a -> 'a -> int; s : 'a rep } - -let empty c = { cmp = c; s = []; } - -let is_empty s = is_empty s.s - -let mem x s = mem s.cmp x s.s - -let add x s = { s with s = add s.cmp x s.s } - -let singleton c x = { cmp = c; s = singleton x } - -let remove x s = { s with s = remove s.cmp x s.s } - -let union s1 s2 = { s1 with s = union s1.cmp s1.s s2.s } - -let inter s1 s2 = { s1 with s = inter s1.cmp s1.s s2.s } - -let diff s1 s2 = { s1 with s = diff s1.cmp s1.s s2.s } - -let compare s1 s2 = compare s1.cmp s1.s s2.s - -let equal s1 s2 = equal s1.cmp s1.s s2.s - -let subset s1 s2 = subset s1.cmp s1.s s2.s - -let iter f s = iter f s.s - -let fold f s a = fold f s.s a - -let map c f s = {cmp = c; s = map c f s.s} - -let for_all p s = for_all p s.s - -let exists p s = exists p s.s - -let filter p s = { s with s = filter s.cmp p s.s } - -let partition p s = - let (r1,r2) = partition s.cmp p s.s in - ({s with s = r1}, {s with s = r2}) - -let cardinal s = cardinal s.cmp s.s - -let elements s = elements s.s - -let min_elt s = min_elt s.s - -let max_elt s = max_elt s.s - -let choose s = choose s.s - -let split x s = - let (l,present,r) = split s.cmp x s.s in - ({ s with s = l }, present, { s with s = r }) - -let from_list c l = - {cmp = c; s = l} - -let comprehension1 cmp f p s = - fold (fun x s -> if p x then add (f x) s else s) s (empty cmp) - -let comprehension2 cmp f p s1 s2 = - fold - (fun x1 s -> - fold - (fun x2 s -> - if p x1 x2 then add (f x1 x2) s else s) - s2 - s) - s1 - (empty cmp) - -let comprehension3 cmp f p s1 s2 s3 = - fold - (fun x1 s -> - fold - (fun x2 s -> - fold - (fun x3 s -> - if p x1 x2 x3 then add (f x1 x2 x3) s else s) - s3 - s) - s2 - s) - s1 - (empty cmp) - -let comprehension4 cmp f p s1 s2 s3 s4 = - fold - (fun x1 s -> - fold - (fun x2 s -> - fold - (fun x3 s -> - fold - (fun x4 s -> - if p x1 x2 x3 x4 then add (f x1 x2 x3 x4) s else s) - s4 - s) - s3 - s) - s2 - s) - s1 - (empty cmp) - -let comprehension5 cmp f p s1 s2 s3 s4 s5 = - fold - (fun x1 s -> - fold - (fun x2 s -> - fold - (fun x3 s -> - fold - (fun x4 s -> - fold - (fun x5 s -> - if p x1 x2 x3 x4 x5 then add (f x1 x2 x3 x4 x5) s else s) - s5 - s) - s4 - s) - s3 - s) - s2 - s) - s1 - (empty cmp) - -let comprehension6 cmp f p s1 s2 s3 s4 s5 s6 = - fold - (fun x1 s -> - fold - (fun x2 s -> - fold - (fun x3 s -> - fold - (fun x4 s -> - fold - (fun x5 s -> - fold - (fun x6 s -> - if p x1 x2 x3 x4 x5 x6 then add (f x1 x2 x3 x4 x5 x6) s else s) - s6 - s) - s5 - s) - s4 - s) - s3 - s) - s2 - s) - s1 - (empty cmp) - -let comprehension7 cmp f p s1 s2 s3 s4 s5 s6 s7 = - fold - (fun x1 s -> - fold - (fun x2 s -> - fold - (fun x3 s -> - fold - (fun x4 s -> - fold - (fun x5 s -> - fold - (fun x6 s -> - fold - (fun x7 s -> - if p x1 x2 x3 x4 x5 x6 x7 then add (f x1 x2 x3 x4 x5 x6 x7) s else s) - s7 - s) - s6 - s) - s5 - s) - s4 - s) - s3 - s) - s2 - s) - s1 - (empty cmp) - -let bigunion c xss = - fold union xss (empty c) - -let rec lfp s f = - let s' = f s in - if subset s' s then - s - else - lfp (union s' s) f - -let cross c xs ys = - fold (fun x xys -> fold (fun y xys -> add (x,y) xys) ys xys) xs (empty c) - -let rec lfp s f = - let s' = f s in - if subset s' s then - s - else - lfp (union s' s) f - -let tc c r = - let one_step r = fold (fun (x,y) xs -> fold (fun (y',z) xs -> - if y = y' then add (x,z) xs else xs) r xs) r (empty c) in - lfp r one_step diff --git a/lib/ocaml_rts/linksem/src_lem_library/sum.ml b/lib/ocaml_rts/linksem/src_lem_library/sum.ml deleted file mode 100644 index a9ea35ae..00000000 --- a/lib/ocaml_rts/linksem/src_lem_library/sum.ml +++ /dev/null @@ -1,4 +0,0 @@ -type ('a, 'b) sum = - | Inl of ('a) - | Inr of ('b) - diff --git a/lib/ocaml_rts/linksem/src_lem_library/vector.ml b/lib/ocaml_rts/linksem/src_lem_library/vector.ml deleted file mode 100644 index ff9ddb24..00000000 --- a/lib/ocaml_rts/linksem/src_lem_library/vector.ml +++ /dev/null @@ -1,35 +0,0 @@ -open Nat_num - -type 'a vector = Vector of 'a array - -let vconcat (Vector a) (Vector b) = Vector(Array.append a b) - -let vmap f (Vector a) = Vector(Array.map f a) - -let vfold f base (Vector a) = Array.fold_left f base a - -let vzip (Vector a) (Vector b) = - Vector( Array.of_list (List.combine (Array.to_list a) (Array.to_list b))) - -let vmapacc f (Vector a) base = - let rec mapacc vl b = match vl with - | [] -> ([],b) - | v::vl -> let (v',b') = f v b in - let (vl',b'') = mapacc vl b' in - (v'::vl',b'') in - let vls,b = mapacc (Array.to_list a) base in - Vector(Array.of_list vls),b - -let vmapi f (Vector a) = Vector(Array.mapi f a) - -let extend default size (Vector a) = Vector(Array.append (Array.make size default) a) - -let duplicate (Vector a) = Vector(Array.append a (Array.copy a)) - -let vlength (Vector a) = Array.length a - -let vector_access n (Vector a) = a.(n) - -let vector_slice n1 n2 (Vector a) = Vector(Array.sub a n1 n2) - -let make_vector vs l = Vector(Array.of_list vs)
\ No newline at end of file diff --git a/lib/ocaml_rts/linksem/src_lem_library/vector.mli b/lib/ocaml_rts/linksem/src_lem_library/vector.mli deleted file mode 100644 index fbbe11ab..00000000 --- a/lib/ocaml_rts/linksem/src_lem_library/vector.mli +++ /dev/null @@ -1,28 +0,0 @@ -open Nat_num - -type 'a vector = Vector of 'a array - -val vconcat : 'a vector -> 'a vector -> 'a vector - -val vmap : ('a ->'b) -> 'a vector -> 'b vector - -val vfold : ('b -> 'a -> 'b) -> 'b -> 'a vector -> 'b - -val vzip : 'a vector -> 'b vector -> ('a * 'b) vector - -val vmapacc : ('a -> 'c -> ('b * 'c)) -> 'a vector -> 'c -> ('b vector) * 'c - -val vmapi : (nat -> 'a -> 'b) -> 'a vector -> 'b vector - -val extend : 'a -> nat -> 'a vector -> 'a vector - -val duplicate : 'a vector -> 'a vector - -val vlength : 'a vector -> nat - -val vector_access : nat ->'a vector -> 'a - -val vector_slice : nat -> nat ->'a vector -> 'a vector - -val make_vector : 'a list -> nat -> 'a vector - diff --git a/lib/ocaml_rts/linksem/src_lem_library/xstring.ml b/lib/ocaml_rts/linksem/src_lem_library/xstring.ml deleted file mode 100644 index 7a705aeb..00000000 --- a/lib/ocaml_rts/linksem/src_lem_library/xstring.ml +++ /dev/null @@ -1,22 +0,0 @@ -let explode s = - let rec exp i l = - if i < 0 then l else exp (i - 1) (s.[i] :: l) in - exp (String.length s - 1) [];; - -let implode l = - let res = String.create (List.length l) in - let rec imp i = function - | [] -> res - | c :: l -> res.[i] <- c; imp (i + 1) l in - imp 0 l;; - -let string_case s c_empty c_cons = begin - let len = String.length s in - if (len = 0) then c_empty else - c_cons (String.get s 0) (String.sub s 1 (len - 1)) -end;; - -let cons_string c s = begin - let cs = String.make 1 c in - cs ^ s -end;; diff --git a/lib/ocaml_rts/linksem/src_lem_library/xstring.mli b/lib/ocaml_rts/linksem/src_lem_library/xstring.mli deleted file mode 100644 index aa9182d7..00000000 --- a/lib/ocaml_rts/linksem/src_lem_library/xstring.mli +++ /dev/null @@ -1,4 +0,0 @@ -val explode : string -> char list -val implode : char list -> string -val cons_string : char -> string -> string -val string_case : string -> 'a -> (char -> string -> 'a) -> 'a |