library: renamed array.ArraySorted -> array.IntArraySorted

array.ArraySorted is now generic, with type and order relation parameters
parent bfd6164d
* marks an incompatible change
library
* renamed array.ArraySorted -> array.IntArraySorted
array.ArraySorted is now generic, with type and order relation parameters
provers
* fixed Coq printer (former Coq proofs may have to be updated, by removing
non-emptiness constraints from polymorphic type applications)
......
......@@ -17,7 +17,7 @@ module Algo64
use import ref.Ref
use import array.Array
use import array.ArrayPermut
use import array.ArraySorted
use import array.IntArraySorted
(* Algorithm 63 *)
......
......@@ -19,7 +19,7 @@ module Spec
use import int.Int
use export array.Array
use export array.ArraySorted
use export array.IntArraySorted
(* values of the array are in the range 0..k-1 *)
constant k: int
......
......@@ -15,11 +15,7 @@ module Elt
clone relations.TotalPreOrder with type t = elt, predicate rel = le
predicate sorted_sub (a: array elt) (l u: int) =
forall i1 i2 : int. l <= i1 <= i2 < u -> le a[i1] a[i2]
predicate sorted (a: array elt) =
forall i1 i2 : int. 0 <= i1 <= i2 < length a -> le a[i1] a[i2]
clone export array.ArraySorted with type elt = elt, predicate le = le
end
......
This source diff could not be displayed because it is too large. You can view the blob instead.
......@@ -6,7 +6,7 @@ module InsertionSort
use import int.Int
use import ref.Ref
use import array.Array
use import array.ArraySorted
use import array.IntArraySorted
use import array.ArrayPermut
use import array.ArrayEq
......
......@@ -12,7 +12,7 @@ module InsertionSortNaive
use import ref.Ref
use import ref.Refint
use import array.Array
use import array.ArraySorted
use import array.IntArraySorted
use import array.ArrayPermut
let sort (a:array int)
......
......@@ -8,7 +8,7 @@ module Quicksort
use import int.Int
use import ref.Ref
use import array.Array
use import array.ArraySorted
use import array.IntArraySorted
use import array.ArraySwap
use import array.ArrayPermut
use import array.ArrayEq
......@@ -78,7 +78,7 @@ end
module QuicksortWithShuffle
use import array.Array
use import array.ArraySorted
use import array.IntArraySorted
use import array.ArrayPermut
use import Shuffle
use import Quicksort
......@@ -97,7 +97,7 @@ module Quicksort3way
use import int.Int
use import ref.Refint
use import array.Array
use import array.ArraySorted
use import array.IntArraySorted
use import array.ArraySwap
use import array.ArrayPermut
use import array.ArrayEq
......
......@@ -6,7 +6,7 @@ module SelectionSort
use import int.Int
use import ref.Ref
use import array.Array
use import array.ArraySorted
use import array.IntArraySorted
use import array.ArraySwap
use import array.ArrayPermut
use import array.ArrayEq
......
......@@ -9,7 +9,7 @@ use import bag_of_integers.Bag_integers
use import ref.Ref
use import array.Array
use import array.ArraySorted
use import array.IntArraySorted
use import abstract_heap.AbstractHeap
lemma Min_of_sorted:
......
......@@ -111,7 +111,7 @@ end
(** {2 Sorted Arrays} *)
module ArraySorted
module IntArraySorted
use import int.Int
use import Array
......@@ -119,9 +119,32 @@ module ArraySorted
predicate sorted_sub (a : array int) (l u : int) =
M.sorted_sub a.elts l u
(** [sorted_sub a l u] is true whenever the array segment [a(l..u-1)]
is sorted w.r.t order relation [le] *)
predicate sorted (a : array int) =
M.sorted_sub a.elts 0 a.length
(** [sorted a] is true whenever the array [a] is sorted w.r.t [le] *)
end
module ArraySorted
use import int.Int
use import Array
type elt
predicate le elt elt
predicate sorted_sub (a: array elt) (l u: int) =
forall i1 i2 : int. l <= i1 <= i2 < u -> le a[i1] a[i2]
(** [sorted_sub a l u] is true whenever the array segment [a(l..u-1)]
is sorted w.r.t order relation [le] *)
predicate sorted (a: array elt) =
forall i1 i2 : int. 0 <= i1 <= i2 < length a -> le a[i1] a[i2]
(** [sorted a] is true whenever the array [a] is sorted w.r.t [le] *)
end
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment