math_sequence.bend source

math_sequence.bend on the hub · documented module

# Element- and length-indexed sequence model. Random get is O(index);# runtime dense storage is Array<Element>, not this sequential observation.import Baselaw Values:  for -Element: Data  for length: Nat  Datatype Elements<-Element: Data,-length: Nat> is Data:  Elements{head: Element,tail: Values(Element,length)}def Values(Element,length):  match length:    case 0n: Unit    case 1n+rest: Elements<Element,rest>law Index:  for length: Nat  Datatype Position<-length: Nat> is Data:  First{}  Next{index: Index(length)}def Index(length):  match length:    case 0n: Empty    case 1n+rest: Position<rest>def index_value(length: Nat,index: Index(length)) -> Nat:  match length:    case 0n:      match index:    case 1n+rest:      match index:        case First{}: 0n        case Next{index}: 1n+index_value(rest,index)def tabulate(~Element: Data,~Context: Data,~sample: Context -> Nat -> Element,length: Nat,+offset: Nat,+context: Context) -> Values(Element,length):  match length:    case 0n: Unit{}    case 1n+rest:      Elements{sample(context,offset),tabulate(~Element,~Context,~sample,rest,1n+offset,context)}def get(-Element: Data,length: Nat,index: Index(length),vector: Values(Element,length)) -> Element:  match length:    case 0n:      match index:    case 1n+rest:      match index:        case First{}:          Elements{head,tail} = vector          head        case Next{index}:          Elements{head,tail} = vector          get(Element,rest,index,tail)def replicate(-Element: Data,length: Nat,+value: Element) -> Values(Element,length):  match length:    case 0n: Unit{}    case 1n+rest: Elements{value,replicate(Element,rest,value)}def zip_map(~Element: Data,~Context: Data,~combine: Context -> Element -> Element -> Element,  length: Nat,+context: Context,left: Values(Element,length),right: Values(Element,length)) -> Values(Element,length):  match length:    case 0n: Unit{}    case 1n+rest:      Elements{left_head,left_tail} = left      Elements{right_head,right_tail} = right      Elements{combine(context,left_head,right_head),zip_map(~Element,~Context,~combine,rest,context,left_tail,right_tail)}