open import Relation.Binary
open import Relation.Binary.PropositionalEquality as PropEq
open import Data.Nat hiding (_≟_)

module Stoughton.Var where

  record Enum (𝒱 : Set) : Set where
    field
      _≟_ : Decidable {A = 𝒱} _≡_ 
      encode : 𝒱 → ℕ 
      decode : ℕ → 𝒱
      inverse : ∀ x → encode (decode x) ≡ x

  module Nat where

    Enumℕ : Enum ℕ
    Enumℕ = record
      { _≟_ = Data.Nat._≟_
      ; encode = λ x → x
      ; decode = λ x → x
      ; inverse = λ _ → refl
      }

  module ASCIIStr where

    open import Data.String as String hiding (_≟_; length; _<_)
    open import Data.List as List
    open import Data.List.Properties
    open import Data.Digit
    open import Data.Fin as Fin hiding (_≟_)
    open import Data.Product hiding (map)
    open import Data.Nat.Properties hiding (_≟_)
    open import Agda.Builtin.FromString
    open import Data.Unit hiding (_≟_)
    open import Data.Char hiding (_≟_; _<_)
    open import Function using (_∘_)
    open import Relation.Binary.PropositionalEquality as PropEq
    open import Relation.Binary
    open import Data.List.Relation.Unary.All
    open import Data.Char as Char hiding (_≟_)
    open import Data.Bool hiding (_≟_)

    ASCIIStr : Set
    ASCIIStr = List (Digit )

    head-and : ∀ {x xs} → T (and (x ∷ xs)) → T x
    head-and {true} Txs = tt
    head-and {false} ()

    tail-and : ∀ {x xs} → T (and (x ∷ xs)) → T (and xs)
    tail-and {true} Txs = Txs
    tail-and {false} ()

    ≤ᵇ⇒suc< : ∀ {m n} → T (m ≤ᵇ n) → m Data.Nat.< suc n 
    ≤ᵇ⇒suc< {m} {n} i = s≤s (≤ᵇ⇒≤ m n i)

    instance
      IsStringASCII : IsString ASCIIStr
      IsStringASCII .IsString.Constraint s = T (and (List.map (λ c → Char.toℕ c ≤ᵇ ) (String.toList s)))
      IsStringASCII .IsString.fromString s {{constr}} = aux (String.toList s) constr
        where      
        aux : (xs : List Char) → T (and (List.map (λ c → Char.toℕ c ≤ᵇ ) xs)) → ASCIIStr
        aux [] _ = []
        aux (c ∷ cs) h = Fin.fromℕ< {Char.toℕ c}
          (≤ᵇ⇒suc< (head-and {Char.toℕ c ≤ᵇ } {List.map (λ c → Char.toℕ c ≤ᵇ ) cs} h)) ∷ aux cs (tail-and {Char.toℕ c ≤ᵇ } {List.map (λ c → Char.toℕ c ≤ᵇ ) cs} h)

    private
      example : ASCIIStr
      example = "Hello world!"

      --bad : ASCIIStr
      --bad = "I'm bad\256"

    encode : ASCIIStr → ℕ
    encode = fromDigits

    decode : ℕ → ASCIIStr
    decode = proj₁ ∘ toDigits 

    encode∘decode : ∀ n → encode (decode n) ≡ n
    encode∘decode = proj₂ ∘ toDigits 

    _≟_ : Decidable {A = ASCIIStr} _≡_
    _≟_ = ≡-dec Fin._≟_

    ASCIIStrEnum : Enum ASCIIStr
    ASCIIStrEnum = record
      { _≟_ = _≟_
      ; encode = encode
      ; decode = decode
      ; inverse = encode∘decode
      }