107 lines
2.9 KiB
Text
107 lines
2.9 KiB
Text
|
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)
|
|||
|
|
|
|||
|
|
}
|