model.bend source

model.bend on the hub · documented module

import Baseimport ./types.bend as T# Independent sequential specification: no Vec, main, binary search, or line index.def get(text: String, pos: Nat) -> Result<T.Error,Char>:  match text pos:    case SNil{} 0n: Fail{T.Bounds{}}    case SNil{} 1n+p: Fail{T.Bounds{}}    case SCon{c,t} 0n: Done{c}    case SCon{c,t} 1n+p: get(t,p)def advance(line: U32, col: U32, lf: Bool) -> T.Location:  match lf:    case False{}: T.Location{line,(col + 1 : U32)}    case True{}: T.Location{(line + 1 : U32),0}def locate_go(text: String, pos: Nat, loc: T.Location) -> Result<T.Error,T.Location>:  match text pos loc:    case SNil{} 0n T.Location{l,c}: Done{T.Location{l,c}}    case SNil{} 1n+p T.Location{l,c}: Fail{T.Bounds{}}    case SCon{h,t} 0n T.Location{l,c}: Done{T.Location{l,c}}    case SCon{h,t} 1n+p T.Location{l,c}: locate_go(t,p,advance(l,c,Char.is_eq(h,'\n')))def locate(text: String, pos: U32) -> Result<T.Error,T.Location>:  locate_go(text,U32.to_nat(pos),T.Location{0,0})def slice(text: String, start: Nat, size: Nat) -> String:  String.take(String.drop(text,start),size)# Reverse lookup enumerates positions from a freshly scanned string. It cannot# reproduce the implementation's line-index arithmetic by accident.def location_eq(a: T.Location, b: T.Location) -> Bool:  match a b:    case T.Location{l,c} T.Location{l2,c2}: Bool.and(U32.is_eq(l,l2),U32.is_eq(c,c2))def choose_offset(pos: U32, later: Result<T.Error,U32>, same: Bool) -> Result<T.Error,U32>:  match same:    case True{}: Done{pos}    case False{}: laterdef next(loc: T.Location, c: Char) -> T.Location:  match loc:    case T.Location{l,col}: advance(l,col,Char.is_eq(c,'\n'))def offset_go(text: String, +wanted: T.Location, +loc: T.Location, +pos: U32) -> Result<T.Error,U32>:  match text:    case SNil{}: choose_offset(pos,Fail{T.Bounds{}},location_eq(wanted,loc))    case SCon{h,t}:      choose_offset(pos,offset_go(t,wanted,next(loc,h),(pos + 1 : U32)),location_eq(wanted,loc))def offset(text: String, loc: T.Location) -> Result<T.Error,U32>:  offset_go(text,loc,T.Location{0,0},0)def line_count(text: String) -> U32:  match text:    case SNil{}: 1    case SCon{h,t}: (line_count(t) + Bool.to_u32(Char.is_eq(h,'\n')) : U32)