------------------------------------------------------------------------
-- The Agda standard library
--
-- Properties of operations on strings
------------------------------------------------------------------------

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

module Data.String.Properties where

open import Data.Bool.Base using (Bool)
import Data.Char.Properties as Char
import Data.List.Relation.Binary.Pointwise as Pointwise
import Data.List.Relation.Binary.Lex.Strict as StrictLex
open import Data.String.Base
open import Function.Base using (_∘_; _$_)
open import Relation.Nullary.Decidable using (yes; no)
open import Relation.Nullary.Decidable using (map′; isYes)
open import Relation.Binary.Core using (_⇒_)
open import Relation.Binary.Bundles
  using (Setoid; DecSetoid; StrictPartialOrder; StrictTotalOrder
        ; DecTotalOrder; DecPoset)
open import Relation.Binary.Structures
  using (IsEquivalence; IsDecEquivalence; IsStrictPartialOrder
        ; IsStrictTotalOrder; IsDecPartialOrder; IsDecTotalOrder)
open import Relation.Binary.Definitions
  using (Reflexive; Symmetric; Transitive; Substitutive; Decidable
        ; DecidableEquality)
open import Relation.Binary.PropositionalEquality.Core
import Relation.Binary.Construct.On as On
import Relation.Binary.PropositionalEquality.Properties as PropEq

------------------------------------------------------------------------
-- Primitive properties

open import Agda.Builtin.String.Properties public
  renaming ( primStringToListInjective to toList-injective)

------------------------------------------------------------------------
-- Properties of _≈_

≈⇒≡ : _≈_ ⇒ _≡_
≈⇒≡ = toList-injective _ _
    ∘ Pointwise.Pointwise-≡⇒≡

≈-reflexive : _≡_ ⇒ _≈_
≈-reflexive = Pointwise.≡⇒Pointwise-≡
            ∘ cong toList

≈-refl : Reflexive _≈_
≈-refl {x} = ≈-reflexive {x} {x} refl

≈-sym : Symmetric _≈_
≈-sym = Pointwise.symmetric sym

≈-trans : Transitive _≈_
≈-trans = Pointwise.transitive trans

≈-subst : ∀ {ℓ} → Substitutive _≈_ ℓ
≈-subst P x≈y p = subst P (≈⇒≡ x≈y) p

infix  _≈?_
_≈?_ : Decidable _≈_
x ≈? y = Pointwise.decidable Char._≟_ (toList x) (toList y)

≈-isEquivalence : IsEquivalence _≈_
≈-isEquivalence = record
  { refl  = λ {i} → ≈-refl {i}
  ; sym   = λ {i j} → ≈-sym {i} {j}
  ; trans = λ {i j k} → ≈-trans {i} {j} {k}
  }

≈-setoid : Setoid _ _
≈-setoid = record
  { isEquivalence = ≈-isEquivalence
  }

≈-isDecEquivalence : IsDecEquivalence _≈_
≈-isDecEquivalence = record
  { isEquivalence = ≈-isEquivalence
  ; _≟_           = _≈?_
  }

≈-decSetoid : DecSetoid _ _
≈-decSetoid = record
  { isDecEquivalence = ≈-isDecEquivalence
  }

------------------------------------------------------------------------
-- Properties of _≡_

infix  _≟_

_≟_ : DecidableEquality String
x ≟ y = map′ ≈⇒≡ ≈-reflexive $ x ≈? y

≡-setoid : Setoid _ _
≡-setoid = PropEq.setoid String

≡-decSetoid : DecSetoid _ _
≡-decSetoid = PropEq.decSetoid _≟_

------------------------------------------------------------------------
-- Properties of _<_

infix  _<?_
_<?_ : Decidable _<_
x <? y = StrictLex.<-decidable Char._≟_ Char._<?_ (toList x) (toList y)

<-isStrictPartialOrder-≈ : IsStrictPartialOrder _≈_ _<_
<-isStrictPartialOrder-≈ =
  On.isStrictPartialOrder
    toList
    (StrictLex.<-isStrictPartialOrder Char.<-isStrictPartialOrder)

<-isStrictTotalOrder-≈ : IsStrictTotalOrder _≈_ _<_
<-isStrictTotalOrder-≈ =
  On.isStrictTotalOrder
    toList
    (StrictLex.<-isStrictTotalOrder Char.<-isStrictTotalOrder)

<-strictPartialOrder-≈ : StrictPartialOrder _ _ _
<-strictPartialOrder-≈ =
  On.strictPartialOrder
    (StrictLex.<-strictPartialOrder Char.<-strictPartialOrder)
    toList

<-strictTotalOrder-≈ : StrictTotalOrder _ _ _
<-strictTotalOrder-≈ =
  On.strictTotalOrder
    (StrictLex.<-strictTotalOrder Char.<-strictTotalOrder)
    toList

≤-isDecPartialOrder-≈ : IsDecPartialOrder _≈_ _≤_
≤-isDecPartialOrder-≈ =
  On.isDecPartialOrder
    toList
    (StrictLex.≤-isDecPartialOrder Char.<-isStrictTotalOrder)

≤-isDecTotalOrder-≈ : IsDecTotalOrder _≈_ _≤_
≤-isDecTotalOrder-≈ =
  On.isDecTotalOrder
    toList
    (StrictLex.≤-isDecTotalOrder Char.<-isStrictTotalOrder)

≤-decTotalOrder-≈ :  DecTotalOrder _ _ _
≤-decTotalOrder-≈ =
  On.decTotalOrder
    (StrictLex.≤-decTotalOrder Char.<-strictTotalOrder)
    toList

≤-decPoset-≈ : DecPoset _ _ _
≤-decPoset-≈ =
  On.decPoset
    (StrictLex.≤-decPoset Char.<-strictTotalOrder)
    toList

------------------------------------------------------------------------
-- Alternative Boolean equality test.
--
-- Why is the definition _==_ = primStringEquality not used? One
-- reason is that the present definition can sometimes improve type
-- inference, at least with the version of Agda that is current at the
-- time of writing: see unit-test below.

infix  _==_
_==_ : String → String → Bool
s₁ == s₂ = isYes (s₁ ≟ s₂)

private

  -- The following unit test does not type-check (at the time of
  -- writing) if _==_ is replaced by primStringEquality.

  data P : (String → Bool) → Set where
    p : (c : String) → P (_==_ c)

  unit-test : P (_==_ "")
  unit-test = p _