1	import Base
2	import ./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	
20	def 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	
23	def 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	
26	def 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	
29	def 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	
32	def 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	
35	def 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
39	def last_elem(-A: Data, +xs: List<&2, A>) -> Maybe<&2, A>:
40	  SC.nth(A, xs, Nat.sub(SC.length(A, xs), 1n))