module Revise.Reflection where

Import list

open import Data.Nat using (ℕ; _+_; suc; zero; _≤_; s≤s; z≤n; _≟_)
open import Data.Vec using (Vec; []; _∷_; tail; head)
open import Data.Empty using (⊥)
open import Data.Unit using (⊤; tt)
open import Data.Product using (Σ; _×_; _,_; proj₁; proj₂)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Function renaming (_∘_ to _∘f_)
open import Relation.Nullary using (Dec; yes; no)
open import Relation.Binary.Core using (Decidable)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; trans; cong)

Syntax for existential quantification

ex : {A : Set} → (A → Set) → Set
ex = Σ _

syntax ex (λ y → x) = y ∣ x

Permutation relation _∼_

module _ {A : Set} where

  private V = Vec A

  infix  _~_
  infixl  _∘_

  data _~_ : ∀ {n} → V n → V n → Set where
    zero  : [] ~ []
    suc   : ∀ {n a} {xs ys : V n}   → xs ~ ys → a ∷ xs ~ a ∷ ys
    _∘_   : ∀ {n} {xs ys zs : V n}  → xs ~ ys → ys ~ zs → xs ~ zs
    exch  : ∀ {n a b} {xs : V n}    → a ∷ b ∷ xs ~ b ∷ a ∷ xs

Reflexivity and symmertry of _∼_

  ~-refl : ∀ {n} {xs : V n} → xs ~ xs
  ~-refl {xs = []} = zero
  ~-refl {xs = _ ∷ []} = suc zero
  ~-refl {xs = _ ∷ _ ∷ xs} = exch ∘ exch

  ~-sym : ∀ {n} {xs ys : V n} → xs ~ ys → ys ~ xs
  ~-sym zero = zero
  ~-sym (suc e) = suc (~-sym e)
  ~-sym (e ∘ e₁) = ~-sym e₁ ∘ ~-sym e
  ~-sym exch = exch

Smart constructors

  _∘simp_ : ∀ {n} {xs ys zs : V n}  → xs ~ ys → ys ~ zs → xs ~ zs
  zero ∘simp a = a
  suc zero ∘simp a = a
  (exch ∘ exch) ∘simp a = a
  a ∘simp (exch ∘ exch) = a
  a ∘simp b = a ∘ b

  sucSimp : ∀ {n x} {xs ys : V n}  → xs ~ ys → x ∷ xs ~ x ∷ ys
  sucSimp zero = suc zero
  sucSimp (suc zero) = exch ∘ exch
  sucSimp (exch ∘ exch) = exch ∘ exch
  sucSimp x = suc x

Permutation relation _≈_

  infix  _≋_ _≈_
  infixr  _↪_

  data Into (n : ℕ) : Set where
    _↪_ : A → V n → Into n

  data _≋_ : ∀ {n} → Into n → V (suc n) → Set where
    zero : ∀ {n x} {xs : V n} → x ↪ xs ≋ x ∷ xs
    suc  : ∀ {n x y} {xs : V n} {ys} → x ↪ xs ≋ ys → x ↪ y ∷ xs ≋ y ∷ ys

  data _≈_ : ∀ {n} → V n → V n → Set where
    [] : [] ≈ []
    _∷_  : ∀ {n x} {xs ys : V n} {xxs} → x ↪ xs ≋ xxs → ys ≈ xs → x ∷ ys ≈ xxs

Reflexivity of _≈_

  ≈-refl : ∀ {n} {xs : V n} → xs ≈ xs
  ≈-refl {xs = []} = []
  ≈-refl {xs = _ ∷ _} = zero ∷ ≈-refl

_≈_ → _∼_

  ~↪ : ∀ {n x} {xs : V n} {ys} → x ↪ xs ≋ ys → x ∷ xs ~ ys
  ~↪ zero = ~-refl
  ~↪ (suc e) = exch ∘simp sucSimp (~↪ e)

  ≈→~ : ∀ {n} {xs ys : V n} → xs ≈ ys → xs ~ ys
  ≈→~ [] = zero
  ≈→~ (x ∷ e) = sucSimp (≈→~ e) ∘simp ~↪ x

Transitivity of _≈_

  ↪-exch : ∀ {n x y} {xs : V n} {xxs yxxs} → x ↪ xs ≋ xxs → y ↪ xxs ≋ yxxs 
            → yxs ∣ (y ↪ xs ≋ yxs) × (x ↪ yxs ≋ yxxs)
  ↪-exch zero zero = _ , zero , suc zero
  ↪-exch zero (suc b) = _ , b , zero
  ↪-exch (suc a) zero = _ , zero , suc (suc a)
  ↪-exch (suc a) (suc b) with ↪-exch a b
  ... | _ , s , t = _ , suc s , suc t

  getOut : ∀ {n x} {xs : V n} {xxs xys} → x ↪ xs ≋ xxs → xxs ≈ xys 
       → ys ∣ (x ↪ ys ≋ xys) × (xs ≈ ys)
  getOut zero (x₁ ∷ b) = _ , x₁ , b
  getOut (suc a) (x₁ ∷ b) with getOut a b
  ... | (l , m , f) with ↪-exch m x₁
  ... | s , k , r = s , r , k ∷ f

  infixl  _∘≈_

  _∘≈_ : ∀ {n} {xs ys zs : V n} → xs ≈ ys → ys ≈ zs → xs ≈ zs
  []     ∘≈ f = f
  x₁ ∷ e ∘≈ f with getOut x₁ f
  ... | a , b , c = b ∷ (e ∘≈ c)

_∼_ → _≈_

  ~→≈ : ∀ {n} {xs ys : V n} → xs ~ ys → xs ≈ ys
  ~→≈ zero     = []
  ~→≈ (suc e)  = zero ∷ ~→≈ e
  ~→≈ (e ∘ e₁) = ~→≈ e ∘≈ ~→≈ e₁
  ~→≈ exch     = suc zero ∷ zero ∷ ≈-refl

Symmetry of _≈_

  ≈-sym : ∀ {n} {xs ys : V n} → xs ≈ ys → ys ≈ xs
  ≈-sym a = ~→≈ (~-sym (≈→~ a))

Cancellation property of _≈_

  cancel : ∀ {n} {x} {xs ys : V n} → x ∷ xs ≈ x ∷ ys → xs ≈ ys
  cancel (zero ∷ e) = e
  cancel (suc x₁ ∷ b ∷ e) = zero ∷ e ∘≈ b ∷ ≈-refl ∘≈ x₁ ∷ ≈-refl

Examples

t1 :  ∷  ∷  ∷  ∷ [] ≈  ∷  ∷  ∷  ∷ []
t1 = suc (suc (suc zero)) ∷ suc zero ∷ zero ∷ zero ∷ []

f2 :  ∷  ∷ [] ≈  ∷  ∷ [] → ⊥
f2 (zero ∷ () ∷ [])
f2 (suc x ∷ () ∷ [])

Decidable _≈_

module Dec≈ (A : Set) {{eq : Decidable {A = A} _≡_}} where

  private V = Vec A

  getOut' : ∀ {n} x (xs : V (suc n)) → Dec (ys ∣ x ↪ ys ≋ xs)
  getOut'  x  (x₁ ∷ xs) with eq x x₁
  getOut' .x₁ (x₁ ∷ xs) | yes refl = yes (xs , zero)
  getOut'  x  (x₁ ∷ []) | no ¬p = no (¬p ∘f f x refl)  where
    f : ∀ a → x ≡ a → (ys ∣ a ↪ ys ≋ x₁ ∷ []) → x ≡ x₁
    f .x₁ k (.[] , zero) = k
  getOut' x (x₁ ∷ y ∷ xs) | no ¬p with getOut' x (y ∷ xs)
  ... | yes (a , b) = yes (x₁ ∷ a , suc b)
  ... | no ¬q = no (f x refl)  where
    f : ∀ a → x ≡ a → (ys ∣ a ↪ ys ≋ x₁ ∷ y ∷ xs) → ⊥
    f .x₁ e (.(y ∷ xs) , zero) = ¬p e
    f a e (.x₁ ∷ xs , suc q) with a | e
    ... | .x | refl = ¬q (xs , q)

  infix  _≈?_

  _≈?_ : ∀ {n} → (xs ys : V n) → Dec (xs ≈ ys)
  []     ≈? [] = yes []
  x ∷ xs ≈? ys with getOut' x ys
  ... | no ¬p = no λ { (h ∷ _) → ¬p (_ , h)}
  ... | yes (zs , p) with xs ≈? zs
  ...  | yes p' = yes (p ∷ p')
  ...  | no ¬p = no λ e → ¬p (cancel (e ∘≈ ≈-sym (p ∷ ≈-refl)))

Examples

open Dec≈ ℕ {{_≟_}}  -- TODO: remove this

try =  ∷  ∷  ∷  ∷ [] ≈?  ∷  ∷  ∷  ∷ []

Imports for reflection

open import Reflection hiding (_≟_)
open import Data.List using ([]; _∷_)
open import Data.Maybe using (Maybe; just; nothing; maybe′)

Parsing a natural

parseℕ : Term → Maybe ℕ
parseℕ (con c []) with c ≟-Name quote ℕ.zero
... | yes _ = just 
... | _  = nothing
parseℕ (con c (arg _ x ∷ [])) with c ≟-Name quote ℕ.suc | parseℕ x
... | yes _ | just n = just (suc n)
... | _ | _ = nothing
parseℕ _ = nothing

parseℕ′ : Term → ℕ
parseℕ′ t = maybe′ id  (parseℕ t)

Representation of one side of a permutation relation

data Side : Set where
  side : ∀ {n} → Vec ℕ n → Side

Parsing of the side

parseSide : Term → Maybe Side
parseSide (con c []) = just (side [])
parseSide (con c (_ ∷ arg _ x ∷ arg _ xs ∷ [])) with parseSide xs | parseℕ x
... | just (side s) | just n = just (side (n ∷ s))
... | _ | _ = nothing
parseSide _ = nothing

Solution of a permutation test (with error codes)

data Solution : Set where
   ok : ∀ {n} {xs ys : Vec ℕ n} → Dec (xs ≈ ys) → Solution
   error : ℕ → Solution

Computing a solution

computeSolution : Term → Term → Solution
computeSolution l r with parseSide l | parseSide r
... | nothing | _ = error 
... | _ | nothing = error 
... | just (side {a} b) | just (side {a'} d)  with a ≟ a'
computeSolution l r | just (side b) | just (side d) | yes refl = ok (b ≈? d)
... | no ¬p = error 

Negation as a data

This simplifies parsing of a negation.

data Neg (A : Set) : Set where
  neg : (A → ⊥) → Neg A

Final steps

err : ℕ → Σ Set id
err n = (n ≡ n) , refl

parse : Term → Σ Set id
parse (def c (A ∷ n ∷ arg _ l ∷ arg _ r ∷ [])) with c ≟-Name quote _≈_
... | yes _ = ⟦ computeSolution l r ⟧  where
  ⟦_⟧ : Solution → Σ Set id 
  ⟦ ok (yes d) ⟧ = _ , d
  ⟦ error n ⟧ = err n
  ⟦ _ ⟧ = err 
... | no _ with c ≟-Name quote _~_ 
... | yes _ = ⟦ computeSolution l r ⟧  where
  ⟦_⟧ : Solution → Σ Set id 
  ⟦ ok (yes d) ⟧ = _ , ≈→~ d
  ⟦ error n ⟧ = err n
  ⟦ _ ⟧ = err 
... | no _ = err 
parse (def c' (arg _ (def c (A ∷ n ∷ arg _ l ∷ arg _ r ∷ [])) ∷ [])) with c' ≟-Name quote Neg
... | yes _ = ⟦ computeSolution l r ⟧ where
  ⟦_⟧ : Solution → Σ Set id 
  ⟦ ok (no d) ⟧ = _ , neg d
  ⟦ error n ⟧ = err n
  ⟦ _ ⟧ = err 
... | no _ = err 
parse _ = err 

solvePerm : (g : Term) → proj₁ (parse g)
solvePerm g = proj₂ (parse g)

Examples

{- todo
x : 1 ∷ 2 ∷ 2 ∷ 4 ∷ 5 ∷ [] ≈ 2 ∷ 2 ∷ 1 ∷ 4 ∷ 5 ∷ []
x = quoteGoal t in solvePerm t

x1 : 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ [] ~ 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ []
x1 = quoteGoal t in solvePerm t

x2 : 1 ∷ 2 ∷ 2 ∷ 4 ∷ 5 ∷ [] ~ 2 ∷ 2 ∷ 1 ∷ 4 ∷ 5 ∷ []
x2 = quoteGoal t in solvePerm t

x3 : 1 ∷ 2 ∷ 2 ∷ 4 ∷ 6 ∷ 7 ∷ 8 ∷ 1 ∷ 5 ∷ [] ~ 2 ∷ 8 ∷ 1 ∷ 6 ∷ 7 ∷ 2 ∷ 1 ∷ 4 ∷ 5 ∷ []
x3 = quoteGoal t in solvePerm t

x' : Neg (1 ∷ 2 ∷ 2 ∷ 4 ∷ 5 ∷ [] ≈ 2 ∷ 12 ∷ 1 ∷ 4 ∷ 5 ∷ [])
x' = quoteGoal t in solvePerm t
-}

x