1	# A reusable finite-sequence witness; range membership yields a bounded index.
2	import Base
3	import ../ordered_matrix.bend as OrderedMatrix
4	import ./ordered_ranges.bend as Ranges
5	import ./natural_addition.bend as Addition
6	import ./word_encoding.bend as WordEncoding
7	import ./storage_shape.bend as Shape
8	import ./nat_order.bend as Order
9	
10	def All(-Element: Data,-Property: Element -> Data,items: List<&2,Element>) -> Data:
11	  match items:
12	    case Nil{}: Unit
13	    case item <> rest: Shape.Both<Property(item),All(Element,Property,rest)>
14	
15	# Construct finite range evidence from a bounded pointwise rule.
16	def range_all(~Context: Data,~Property: @+context: Context -> @+index: Nat -> Data,~size: Context -> Nat,
17	  ~cell: @+context: Context -> @+index: Nat -> @+inside: {Nat.is_lt(index,size(context)) == True{} : Bool} -> Property(context,index),
18	  remaining: Nat,+position: Nat,+context: Context,+room: {Nat.is_le(Nat.add(position,remaining),size(context)) == True{} : Bool}) ->
19	  All(Nat,{index => Property(context,index) : Nat -> Data},Ranges.range(remaining,position)):
20	  match remaining:
21	    case 0n: Unit{}
22	    case 1n+ +rest:
23	      Shape.Both{cell(context,position,Order.room_index(position,rest,size(context),room)),
24	        range_all(~Context,~Property,~size,~cell,rest,1n+position,context,Order.advance_room(position,rest,size(context),room))}
25	
26	def all_concatenated(-Element: Data,-Property: Element -> Data,+left: List<&2,Element>,+right: List<&2,Element>,
27	  left_proof: All(Element,Property,left),right_proof: All(Element,Property,right)) -> All(Element,Property,OrderedMatrix.cat(Element,left,right)):
28	  match left:
29	    case Nil{}: right_proof
30	    case +item <> +rest:
31	      Shape.Both{head,tail} = left_proof
32	      Shape.Both{head,all_concatenated(Element,Property,rest,right,tail,right_proof)}
33	
34	def transform_all(~Element: Data,~Context: Data,~Before: @+context: Context -> @+element: Element -> Data,~After: @+context: Context -> @+element: Element -> Data,
35	  ~transform: @+context: Context -> @+element: Element -> @+evidence: Before(context,element) -> After(context,element),
36	  +items: List<&2,Element>,+context: Context,evidence: All(Element,{element => Before(context,element) : Element -> Data},items)) ->
37	  All(Element,{element => After(context,element) : Element -> Data},items):
38	  match items:
39	    case Nil{}: Unit{}
40	    case +element <> +rest:
41	      Shape.Both{head,tail} = evidence
42	      Shape.Both{transform(context,element,head),transform_all(~Element,~Context,~Before,~After,~transform,rest,context,tail)}
43	
44	def Member(-A: Data,+value: A,values: List<&2,A>) -> Data:
45	  match values:
46	    case Nil{}: Empty
47	    case head <> rest: Either<&2,&2,{value == head : A},Member(A,value,rest)>
48	
49	def all_member(-Element: Data,-Property: Element -> Data,+value: Element,items: List<&2,Element>,
50	  all: All(Element,Property,items),member: Member(Element,value,items)) -> Property(value):
51	  match items:
52	    case []: Empty.absurd(Property(value),member)
53	    case +head <> +rest:
54	      Shape.Both{head_proof,tail_proof} = all
55	      match member:
56	        case Inl{equal}:
57	          %Equal.sym(Element,value,head,equal) : Property(_)
58	          head_proof
59	        case Inr{tail}: all_member(Element,Property,value,rest,tail_proof,tail)
60	
61	def lift_split(-A: Data,+value: A,+head: A,+left: List<&2,A>,+right: List<&2,A>,
62	  choice: Either<&2,&2,Member(A,value,left),Member(A,value,right)>) -> Either<&2,&2,Member(A,value,head <> left),Member(A,value,right)>:
63	  match choice:
64	    case Inl{member}: Inl{Inr{member}}
65	    case Inr{member}: Inr{member}
66	
67	def split_concatenated(-A: Data,+value: A,+left: List<&2,A>,+right: List<&2,A>,member: Member(A,value,OrderedMatrix.cat(A,left,right))) ->
68	  Either<&2,&2,Member(A,value,left),Member(A,value,right)>:
69	  match left:
70	    case Nil{}: Inr{member}
71	    case +head <> +rest:
72	      match member:
73	        case Inl{equal}: Inl{Inl{equal}}
74	        case Inr{tail}: lift_split(A,value,head,rest,right,split_concatenated(A,value,rest,right,tail))
75	
76	def range_member(+count: Nat,+start: Nat,+index: Nat,inside: {Nat.is_lt(index,count) == True{} : Bool}) ->
77	  Member(Nat,Nat.add(start,index),Ranges.range(count,start)):
78	  match count index:
79	    case 0n 0n: Empty.absurd(Member(Nat,Nat.add(start,0n),[]),WordEncoding.false_true(inside))
80	    case 0n 1n+index: Empty.absurd(Member(Nat,Nat.add(start,1n+index),[]),WordEncoding.false_true(inside))
81	    case 1n+rest 0n: Inl{Addition.zero_right(start)}
82	    case 1n+ +rest 1n+ +previous:
83	      Inr{
84	        %Equal.sym(Nat,Nat.add(start,1n+previous),1n+Nat.add(start,previous),Addition.successor_right(start,previous)) : Member(Nat,_,Ranges.range(rest,1n+start))
85	        range_member(rest,1n+start,previous,inside)}
86	
87	type RangeIndex<-count: Nat,-start: Nat,-value: Nat> is Data:
88	  RangeIndex{index: Nat,inside: {Nat.is_lt(index,count) == True{} : Bool},exact: {Nat.add(start,index) == value : Nat}}
89	
90	def lift_range_index(+count: Nat,+start: Nat,+value: Nat,proof: RangeIndex<count,1n+start,value>) -> RangeIndex<1n+count,start,value>:
91	  RangeIndex{+index,inside,exact} = proof
92	  RangeIndex{1n+index,inside,
93	    Equal.trans(Nat,Nat.add(start,1n+index),1n+Nat.add(start,index),value,Addition.successor_right(start,index),exact)}
94	
95	def range_index(+count: Nat,+start: Nat,+value: Nat,member: Member(Nat,value,Ranges.range(count,start))) -> RangeIndex<count,start,value>:
96	  match count:
97	    case 0n: Empty.absurd(RangeIndex<0n,start,value>,member)
98	    case 1n+ +rest:
99	      match member:
100	        case Inl{equal}:
101	          RangeIndex{0n,{==},Equal.trans(Nat,Nat.add(start,0n),start,value,Addition.zero_right(start),Equal.sym(Nat,value,start,equal))}
102	        case Inr{tail}: lift_range_index(rest,start,value,range_index(rest,1n+start,value,tail))