module BString where

open import Function
open import Data.Nat
open import List
open import Data.Bool renaming (T to isTrue)
open import Data.Vec
open import Data.Char
import Data.String as String
open String using (String)
open import Relation.Nullary

data BList (A : Set) : ℕ → Set where
  []  : {n : ℕ} → BList A n
  _∷_ : {n : ℕ} → A → BList A n → BList A (suc n)

forgetV : {A : Set}{n : ℕ} → Vec A n → List A
forgetV []        = []
forgetV (x ∷ xs) = x ∷ forgetV xs

forgetB : {A : Set}{n : ℕ} → BList A n → List A
forgetB []        = []
forgetB (x ∷ xs) = x ∷ forgetB xs

_=<_ : ℕ → ℕ → Bool
zero  =< _     = true
suc n =< zero  = false
suc n =< suc m = n =< m

vec : ∀ {n A} → A → Vec A n
vec {zero} _ = []
vec {suc n} x = x ∷ vec x

bList : {n : ℕ}{A : Set}(xs : List A){p : isTrue (length xs =< n)} →
        BList A n
bList [] = []
bList {zero}  (x ∷ xs) {}
bList {suc n} (x ∷ xs) {p} = x ∷ bList xs {p} 

vList : {n : ℕ}{A : Set}(xs : List A){p : isTrue (length xs =< n)} →
        A → Vec A n
vList [] z = vec z
vList {zero}  (x ∷ xs) {} _
vList {suc n} (x ∷ xs) {p} z = x ∷ vList xs {p} z

strLen : String → ℕ
strLen = length ∘ stringToList

BString = BList Char

bString : ∀ {n} s {p : isTrue (strLen s =< n)} → BString n
bString s {p} = bList (stringToList s) {p}

unBString : ∀ {n} → BString n → String
unBString = stringFromList ∘ forgetB

VString = Vec Char

vString : ∀ {n} s {p : isTrue (strLen s =< n)} → VString n
vString s {p} = vList (stringToList s) {p} ' '

unVString : ∀ {n} → VString n → String
unVString = stringFromList ∘ forgetV

trim : Char → String → String
trim c = stringFromList ∘ List.reverse ∘ dropWhile (_==_ c) ∘ List.reverse ∘ stringToList