Levenshtein distance (basic definitions)

Joomy.agda

module Joomy where

open import Level using (Level)

open import Data.List.Base
  as List
  using ()
  renaming (List to [>_]; [] to [>]; _∷_ to _:>_)

open import Data.Nat.Base using (ℕ; _+_; _≤_)

variable
  a : Level
  A : Set a
  x y : A
  xs ys : [> A ]

data [<_] (A : Set a) : Set a where
  [<]  : [< A ]
  _<:_ : [< A ] → A → [< A ]

variable
  sx sy : [< A ]

_<>>_ : [< A ] → [> A ] → [> A ]
[<] <>> xs = xs
(sx <: x) <>> xs = sx <>> (x :> xs)

infix 1 _||_
data Split {A : Set a} : (xs : [> A ]) → Set a where
  _||_ : (seen : [< A ]) (todo : [> A ]) → Split (seen <>> todo)

variable
  spl spr : Split xs

variable
  k l m : ℕ

data Diff {A : Set a} : {xs ys : [> A ]} → Split xs → Split ys → ℕ → Set a where
  done : Diff (sx || [>]) (sy || [>]) 0
  delL : Diff (sx <: x || xs) (sy || ys) k →
         Diff (sx || x :> xs) (sy || ys) (1 + k)
  delR : Diff (sx || xs) (sy <: y || ys) k →
         Diff (sx || xs) (sy || y :> ys) (1 + k)
  same : Diff (sx <: x || xs) (sy <: x || ys) k →
         Diff (sx || x :> xs) (sy || x :> ys) k
  swap : Diff (sx <: x || xs) (sy <: y || ys) k →
         Diff (sx || x :> xs) (sy || y :> ys) (1 + k)

record Dist {A : Set a} {xs ys : [> A ]} (spl : Split xs) (spr : Split ys) (cost : ℕ) : Set a where
  constructor _,_
  field
    diff : Diff spl spr cost
    mini : ∀ cost' → Diff spl spr cost' → cost ≤ cost'