aoc2023/lib/string.quox

107 lines
2.9 KiB
Text
Raw Normal View History

2023-12-06 21:47:23 -05:00
load "bool.quox"
load "list.quox"
load "maybe.quox"
load "either.quox"
namespace char {
postulate0 Char : ★
#[compile-scheme "(lambda (c) c)"]
postulate dup : Char → [ω.Char]
#[compile-scheme "char->integer"]
postulate to- : Char →
#[compile-scheme "integer->char"]
postulate from- : → Char
def space = from- 0x20
def tab = from- 0x09
def newline = from- 0x0a
def test-via- : (ω. → ω. → Bool) → (ω.Char → ω.Char → Bool) =
λ p c d ⇒ p (to- c) (to- d)
def lt = test-via- nat.lt
def eq = test-via- nat.eq
def gt = test-via- nat.gt
def le = test-via- nat.le
def ne = test-via- nat.ne
def ge = test-via- nat.ge
postulate0 eq-iff-nat : (c d : Char) → Iff (c ≡ d : Char) (to- c ≡ to- d : )
def eq? : DecEq Char =
λ c d ⇒
let0 Ty = (c ≡ d : Char) ∷ ★ in
dec.elim (to- c ≡ to- d : ) (λ _ ⇒ Dec Ty)
(λ y ⇒ Yes Ty ((snd (eq-iff-nat c d)) y))
(λ n ⇒ No Ty (λ y ⇒ n ((fst (eq-iff-nat c d)) y)))
(nat.eq? (to- c) (to- d))
def ws? : ω.Char → Bool =
λ c ⇒
case dup c return Bool of { [c] ⇒
bool.or (bool.or (eq c space) (eq c tab)) (eq c newline)
}
def digit? : ω.Char → Bool =
λ c ⇒ case dup c return Bool of { [c] ⇒
bool.and (ge c (from- 0x30)) (le c (from- 0x39))
}
def digit-val : Char → =
λ c ⇒
case dup c return of { [c] ⇒
bool.if (digit? c) (nat.minus (to- c) 0x30) 0
}
}
def0 Char = char.Char
namespace string {
#[compile-scheme "string->list"]
postulate to-scheme-list : String → list.SchemeList Char
def to-list : String → List Char =
λ str ⇒ list.from-scheme Char (to-scheme-list str)
#[compile-scheme "list->string"]
postulate from-scheme-list : list.SchemeList Char → String
def from-list : List Char → String =
λ cs ⇒ from-scheme-list (list.to-scheme Char cs)
def foldl : 0.(A : ★) → A → ω.(A → Char → A) → String → A =
λ A z f str ⇒ list.foldl Char A z f (to-list str)
#[compile-scheme
"(lambda% (fail ok str) (cond [(string->number str) => ok] [else fail]))"]
postulate to-' : 0.(B : ★) → ω.B → ω.( → B) → String → B
def to- : String → Maybe =
to-' (Maybe ) (Nothing ) (Just )
def split : ω.(ω.Char → Bool) → ω.String → List String =
λ p str ⇒
list.map (List Char) String from-list
(list.split Char p (to-list str))
def break : ω.(ω.Char → Bool) → ω.String → String × String =
λ p str ⇒
letω pair = list.break Char p (to-list str) in
(from-list (fst pair), from-list (snd pair))
def reverse : String → String =
λ str ⇒ from-list (list.reverse Char (to-list str))
#[compile-scheme "(lambda% (a b) (if (string=? a b) 'true 'false))"]
postulate eq : ω.String → ω.String → Bool
def null : ω.String → Bool = eq ""
def not-null : ω.String → Bool = λ s ⇒ bool.not (null s)
}