module Data.String where
open import Data.List as List using (List)
open import Data.Vec as Vec using (Vec)
open import Data.Colist as Colist using (Colist)
open import Data.Char using (Char)
open import Data.Bool using (Bool; true; false)
open import Data.Function
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as PropEq using (_≡_)
open import Relation.Binary.PropositionalEquality.TrustMe
postulate
String : Set
{-# BUILTIN STRING String #-}
{-# COMPILED_TYPE String String #-}
Costring : Set
Costring = Colist Char
private
primitive
primStringAppend : String → String → String
primStringToList : String → List Char
primStringFromList : List Char → String
primStringEquality : String → String → Bool
infixr 5 _++_
_++_ : String → String → String
_++_ = primStringAppend
toList : String → List Char
toList = primStringToList
fromList : List Char → String
fromList = primStringFromList
toVec : (s : String) → Vec Char (List.length (toList s))
toVec s = Vec.fromList (toList s)
toCostring : String → Costring
toCostring = Colist.fromList ∘ toList
infix 4 _==_
_==_ : String → String → Bool
_==_ = primStringEquality
_≟_ : Decidable {A = String} _≡_
s₁ ≟ s₂ with s₁ == s₂
... | true = yes trustMe
... | false = no whatever
where postulate whatever : _
setoid : Setoid _ _
setoid = PropEq.setoid String
decSetoid : DecSetoid _ _
decSetoid = PropEq.decSetoid _≟_