------------------------------------------------------------------------
-- 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 4 _≈?_
_≈?_ : 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 4 _≟_
_≟_ : DecidableEquality String
x ≟ y = map′ ≈⇒≡ ≈-reflexive $ x ≈? y
≡-setoid : Setoid _ _
≡-setoid = PropEq.setoid String
≡-decSetoid : DecSetoid _ _
≡-decSetoid = PropEq.decSetoid _≟_
------------------------------------------------------------------------
-- Properties of _<_
infix 4 _<?_
_<?_ : 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 4 _==_
_==_ : 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 _
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4