spec/lib/sequence.bend source

spec/lib/sequence.bend on the hub · documented module

import Baseimport ./common.bend as SC# The model of SPARK's formal vectors, over the lists every sequence# specification here uses. SPARKlib spark-containers-formal-vectors.ads# (AdaCore/SPARKlib 46ec319, lines 104-280, package Formal_Model) states each# postcondition with a few predicates on the functional sequence# M.Sequence (spark-containers-functional-vectors.ads):#   M.Length, Element             SC.length, SC.nth#   M.Range_Equal (L, R, F, Lst)   RangeEqual(l, r, f, lst+1)#   M.Range_Shifted (.., Offset)   RangeShifted(l, r, f, lst+1, off)#   M.Equal_Prefix (L, R)          EqualPrefix(l, r)#   M.Equal_Except (L, R, P)       EqualExcept(l, r, p)#   M.Constant_Range (C, F, L, E)  ConstantRange(c, f, lst+1, e)#   M_Elements_Reversed (L, R)     ElementsReversed(l, r)# Two translations: indices start at 0 (Index_Type'First), and every range# is half open [fst, en), so the empty range needs no Index_Type'Base.# The lemmas about these predicates are in proofs/lib/sequence.bend.def RangeEqual(-A: Data, l: List<&2, A>, r: List<&2, A>, fst: Nat, en: Nat) -> Type:  @+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>}def RangeShifted(-A: Data, l: List<&2, A>, r: List<&2, A>, fst: Nat, en: Nat, off: Nat) -> Type:  @+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>}def EqualPrefix(-A: Data, l: List<&2, A>, r: List<&2, A>) -> Type:  {Nat.is_le(SC.length(A, l), SC.length(A, r)) == True{} : Bool} & RangeEqual(A, l, r, 0n, SC.length(A, l))def EqualExcept(-A: Data, l: List<&2, A>, r: List<&2, A>, p: Nat) -> Type:  {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>})def ConstantRange(-A: Data, c: List<&2, A>, fst: Nat, en: Nat, x: A) -> Type:  @+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>}def ElementsReversed(-A: Data, l: List<&2, A>, r: List<&2, A>) -> Type:  {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>})# Last_Element: the element at Last_Index = Length - 1def last_elem(-A: Data, +xs: List<&2, A>) -> Maybe<&2, A>:  SC.nth(A, xs, Nat.sub(SC.length(A, xs), 1n))