model.bend source
model.bend on the hub · documented module
import Base# Independent sequence model. No implementation imports or array operations.type Op is Data: Push{x: U32} Pop{} Get{i: U32} Set{i: U32, x: U32} Swap{i: U32, x: U32} Reserve{minimum: U32} Slice{start: U32, end: U32}type Observation is Data: Ok{} Value{x: U32} Values{xs: List<&2,U32>} BadIndex{} IsEmpty{} AtLimit{} BadRange{}type State is Data: Sequence{items: List<&2,U32>, max: U32}def length(xs: List<&2,U32>) -> U32: U32.from_nat(List.length(&2,U32,xs))def append(xs: List<&2,U32>, value: U32) -> List<&2,U32>: match xs: case Nil{}: Con{value,Nil{}} case Con{x,tail}: Con{x,append(tail,value)}def get(xs: List<&2,U32>, i: Nat) -> Observation: match xs: case Nil{}: BadIndex{} case Con{x,tail}: match i: case 0n: Value{x} case 1n+p: get(tail,p)def set(xs: List<&2,U32>, i: Nat, value: U32) -> List<&2,U32>: match xs: case Nil{}: Nil{} case Con{x,tail}: match i: case 0n: Con{value,tail} case 1n+p: Con{x,set(tail,p,value)}def pop_tail(x: U32, pair: List<&2,U32> & Observation) -> List<&2,U32> & Observation: (xs,result) = pair (Con{x,xs},result)def pop(xs: List<&2,U32>) -> List<&2,U32> & Observation: match xs: case Nil{}: (Nil{},IsEmpty{}) case Con{x,tail}: match tail: case Nil{}: (Nil{},Value{x}) case Con{y,rest}: pop_tail(x,pop(Con{y,rest}))def popped(max: U32, pair: List<&2,U32> & Observation) -> State & Observation: (xs,result) = pair (Sequence{xs,max},result)def push_if(+xs: List<&2,U32>, +max: U32, x: U32, valid: Bool) -> State & Observation: match valid: case False{}: (Sequence{xs,max},AtLimit{}) case True{}: (Sequence{append(xs,x),max},Ok{})def set_if(+xs: List<&2,U32>, max: U32, i: U32, x: U32, valid: Bool) -> State & Observation: match valid: case False{}: (Sequence{xs,max},BadIndex{}) case True{}: (Sequence{set(xs,U32.to_nat(i),x),max},Ok{})def swap_if(+xs: List<&2,U32>, max: U32, +i: U32, x: U32, valid: Bool) -> State & Observation: match valid: case False{}: (Sequence{xs,max},BadIndex{}) case True{}: (Sequence{set(xs,U32.to_nat(i),x),max},get(xs,U32.to_nat(i)))def reserve_if(xs: List<&2,U32>, max: U32, valid: Bool) -> State & Observation: match valid: case False{}: (Sequence{xs,max},AtLimit{}) case True{}: (Sequence{xs,max},Ok{})def slice_if(+xs: List<&2,U32>, max: U32, +start: U32, end: U32, valid: Bool) -> State & Observation: match valid: case False{}: (Sequence{xs,max},BadRange{}) case True{}: (Sequence{xs,max},Values{List.take(&2,U32,List.drop(&2,U32,xs,U32.to_nat(start)),U32.to_nat(U32.sub(end,start)))})def step(state: State, op: Op) -> State & Observation: match state: case Sequence{+xs,+max}: match op: case Push{x}: push_if(xs,max,x,U32.is_lt(length(xs),max)) case Pop{}: popped(max,pop(xs)) case Get{i}: (Sequence{xs,max},get(xs,U32.to_nat(i))) case Set{+i,x}: set_if(xs,max,i,x,U32.is_lt(i,length(xs))) case Swap{+i,x}: swap_if(xs,max,i,x,U32.is_lt(i,length(xs))) case Reserve{minimum}: reserve_if(xs,max,U32.is_le(minimum,max)) case Slice{+start,+end}: slice_if(xs,max,start,end,Bool.and(U32.is_le(start,end),U32.is_le(end,length(xs))))def list_eq(xs: List<&2,U32>, ys: List<&2,U32>) -> Bool: match xs: case Nil{}: match ys: case Nil{}: True{} case Con{h,t}: False{} case Con{x,xt}: match ys: case Nil{}: False{} case Con{y,yt}: Bool.and(U32.is_eq(x,y),list_eq(xt,yt))def obs_eq(x: Observation, y: Observation) -> Bool: match x: case Ok{}: match y: case Ok{}: True{} case _: False{} case Value{a}: match y: case Value{b}: U32.is_eq(a,b) case _: False{} case Values{a}: match y: case Values{b}: list_eq(a,b) case _: False{} case BadIndex{}: match y: case BadIndex{}: True{} case _: False{} case IsEmpty{}: match y: case IsEmpty{}: True{} case _: False{} case AtLimit{}: match y: case AtLimit{}: True{} case _: False{} case BadRange{}: match y: case BadRange{}: True{} case _: False{}