module BString where

open import Data.Function
open import Data.Nat
open import Data.List as 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 ∘ String.toList

BString = BList Char

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

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

VString = Vec Char

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

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

trim : Char → String → String
trim c = String.fromList ∘ List.reverse ∘ dropWhile (_==_ c) ∘ List.reverse ∘ String.toList