spec/lib/sequence.bend
bend-collections-laws-containers@1.0.0.0 · 40 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
3
4# The model of SPARK's formal vectors, over the lists every sequence
5# specification here uses. SPARKlib spark-containers-formal-vectors.ads
6# (AdaCore/SPARKlib 46ec319, lines 104-280, package Formal_Model) states each
7# postcondition with a few predicates on the functional sequence
8# M.Sequence (spark-containers-functional-vectors.ads):
9# M.Length, Element SC.length, SC.nth
10# M.Range_Equal (L, R, F, Lst) RangeEqual(l, r, f, lst+1)
11# M.Range_Shifted (.., Offset) RangeShifted(l, r, f, lst+1, off)
12# M.Equal_Prefix (L, R) EqualPrefix(l, r)
13# M.Equal_Except (L, R, P) EqualExcept(l, r, p)
14# M.Constant_Range (C, F, L, E) ConstantRange(c, f, lst+1, e)
15# M_Elements_Reversed (L, R) ElementsReversed(l, r)
16# Two translations: indices start at 0 (Index_Type'First), and every range
17# is half open [fst, en), so the empty range needs no Index_Type'Base.
18# The lemmas about these predicates are in proofs/lib/sequence.bend.
19
20def RangeEqual(-A: Data, l: List<&2, A>, r: List<&2, A>, fst: Nat, en: Nat) -> Type:
21 @+i: Nat -> @+h1: {Nat.is_le(fst, i) == True{} : Bool} -> @+h2: {Nat.is_lt(i, en) == True{} : Bool} -> {SC.nth(A, l, i) == SC.nth(A, r, i) : Maybe<&2, A>}
22
23def RangeShifted(-A: Data, l: List<&2, A>, r: List<&2, A>, fst: Nat, en: Nat, off: Nat) -> Type:
24 @+i: Nat -> @+h1: {Nat.is_le(fst, i) == True{} : Bool} -> @+h2: {Nat.is_lt(i, en) == True{} : Bool} -> {SC.nth(A, l, i) == SC.nth(A, r, Nat.add(i, off)) : Maybe<&2, A>}
25
26def EqualPrefix(-A: Data, l: List<&2, A>, r: List<&2, A>) -> Type:
27 {Nat.is_le(SC.length(A, l), SC.length(A, r)) == True{} : Bool} & RangeEqual(A, l, r, 0n, SC.length(A, l))
28
29def EqualExcept(-A: Data, l: List<&2, A>, r: List<&2, A>, p: Nat) -> Type:
30 {SC.length(A, l) == SC.length(A, r) : Nat} & (@+i: Nat -> @+h: {Nat.is_eq(p, i) == False{} : Bool} -> {SC.nth(A, l, i) == SC.nth(A, r, i) : Maybe<&2, A>})
31
32def ConstantRange(-A: Data, c: List<&2, A>, fst: Nat, en: Nat, x: A) -> Type:
33 @+i: Nat -> @+h1: {Nat.is_le(fst, i) == True{} : Bool} -> @+h2: {Nat.is_lt(i, en) == True{} : Bool} -> {SC.nth(A, c, i) == Some{x} : Maybe<&2, A>}
34
35def ElementsReversed(-A: Data, l: List<&2, A>, r: List<&2, A>) -> Type:
36 {SC.length(A, l) == SC.length(A, r) : Nat} & (@+i: Nat -> @+h: {Nat.is_lt(i, SC.length(A, l)) == True{} : Bool} -> {SC.nth(A, r, i) == SC.nth(A, l, Nat.sub(Nat.sub(SC.length(A, l), 1n), i)) : Maybe<&2, A>})
37
38# Last_Element: the element at Last_Index = Length - 1
39def last_elem(-A: Data, +xs: List<&2, A>) -> Maybe<&2, A>:
40 SC.nth(A, xs, Nat.sub(SC.length(A, xs), 1n))