summaryrefslogtreecommitdiff
path: root/Binaries
diff options
context:
space:
mode:
authorGravatar Unknown <namin@idea>2013-06-26 17:48:12 -0700
committerGravatar Unknown <namin@idea>2013-06-26 17:48:12 -0700
commit927a76b4b1461ac549bc12f24c7bf73f610bd4e4 (patch)
treef92d6c14e6d0ad1e17401a8dd1a822530d37eab2 /Binaries
parent23ad17c104cc8814c2b94a608386c0535f6d0f2f (diff)
Changed ranking function for Seq, so that it's compatible with data types.
Diffstat (limited to 'Binaries')
-rw-r--r--Binaries/DafnyPrelude.bpl14
1 files changed, 14 insertions, 0 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index dd0a6671..5d0b647f 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -388,6 +388,20 @@ axiom (forall<T> s: Seq T, v: T, n: int ::
{ Seq#Drop(Seq#Build(s, v), n) }
0 <= n && n <= Seq#Length(s) ==> Seq#Drop(Seq#Build(s, v), n) == Seq#Build(Seq#Drop(s, n), v) );
+function Seq#Rank<T>(Seq T): int;
+axiom (forall s: Seq BoxType, i: int ::
+ { DtRank($Unbox(Seq#Index(s, i)): DatatypeType) }
+ 0 <= i && i < Seq#Length(s) ==> DtRank($Unbox(Seq#Index(s, i)): DatatypeType) < Seq#Rank(s) );
+axiom (forall<T> s: Seq T, i: int ::
+ { Seq#Rank(Seq#Drop(s, i)) }
+ 0 < i && i <= Seq#Length(s) ==> Seq#Rank(Seq#Drop(s, i)) < Seq#Rank(s) );
+axiom (forall<T> s: Seq T, i: int ::
+ { Seq#Rank(Seq#Take(s, i)) }
+ 0 <= i && i < Seq#Length(s) ==> Seq#Rank(Seq#Take(s, i)) < Seq#Rank(s) );
+axiom (forall<T> s: Seq T, i: int, j: int ::
+ { Seq#Rank(Seq#Append(Seq#Take(s, i), Seq#Drop(s, j))) }
+ 0 <= i && i < j && j <= Seq#Length(s) ==> Seq#Rank(Seq#Append(Seq#Take(s, i), Seq#Drop(s, j))) < Seq#Rank(s) );
+
// Additional axioms about common things
axiom Seq#Take(Seq#Empty(): Seq BoxType, 0) == Seq#Empty(); // [][..0] == []
axiom Seq#Drop(Seq#Empty(): Seq BoxType, 0) == Seq#Empty(); // [][0..] == []