aoc2023/lib/string.quox

106 lines
2.9 KiB
Text
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

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)
}