{-# OPTIONS --safe --cubical #-}

module OWL2.Data.String where

open import OWL2.Prelude
import Agda.Builtin.Char as BChar
import Agda.Builtin.Char.Properties as BCharProps
import Agda.Builtin.String as BString
import Agda.Builtin.String.Properties as BStringProps
import Cubical.Data.Equality.Conversion as EqConversion
import Cubical.Data.List.Properties as ListProperties
import Cubical.Data.Nat.Properties as NatProperties
open import Cubical.Relation.Nullary.Base using (Discrete; yes; no)

private
  BoolIsTrue : Bool → Type₀
  BoolIsTrue true =
    Unit*
  BoolIsTrue false =
    ⊥

  falseNotTrue : false ≡ true → ⊥
  falseNotTrue equality =
    subst BoolIsTrue (sym equality) tt*

  absurd : ∀ {ℓ} {A : Type ℓ} → ⊥ → A
  absurd ()

charDiscrete : Discrete BChar.Char
charDiscrete left right
  with NatProperties.discreteℕ
        (BChar.primCharToNat left)
        (BChar.primCharToNat right)
... | yes equalCode =
  yes
    (EqConversion.eqToPath
      (BCharProps.primCharToNatInjective
        left
        right
        (EqConversion.pathToEq equalCode)))
... | no unequalCode =
  no (λ equalChar → unequalCode (cong BChar.primCharToNat equalChar))

stringDiscrete : Discrete String
stringDiscrete left right
  with ListProperties.discreteList
        charDiscrete
        (BString.primStringToList left)
        (BString.primStringToList right)
... | yes equalCharacters =
  yes
    (EqConversion.eqToPath
      (BStringProps.primStringToListInjective
        left
        right
        (EqConversion.pathToEq equalCharacters)))
... | no unequalCharacters =
  no (λ equalString → unequalCharacters (cong BString.primStringToList equalString))

stringEquality : String → String → Bool
stringEquality left right with stringDiscrete left right
... | yes equal =
  true
... | no unequal =
  false

stringEqualityTrueFromEqual :
  (left right : String) →
  left ≡ right →
  stringEquality left right ≡ true
stringEqualityTrueFromEqual left right equal with stringDiscrete left right
... | yes equal′ =
  refl
... | no unequal =
  absurd (unequal equal)

stringEqualityTrueToEqual :
  (left right : String) →
  stringEquality left right ≡ true →
  left ≡ right
stringEqualityTrueToEqual left right equality with stringDiscrete left right
... | yes equal =
  equal
... | no unequal =
  absurd (falseNotTrue equality)