{-# OPTIONS -v DecEq:100 #-}
module Prelude.DecEq.Derive where

open import Prelude.Init
open Meta
import Reflection.Argument as RArg
open import Reflection.Name renaming (_≟_ to _≟ₙ_)
open import Reflection.Term renaming (_≟_ to _≟ₜ_)
open import Reflection.Argument.Visibility renaming (_≟_ to _≟ᵥ_)


open import Prelude.Generics
open import Prelude.Generics using (DERIVE) public
open Debug ("DecEq" , 100)
open import Prelude.Lists
open import Prelude.Show
open import Prelude.Monoid
open import Prelude.Functor
open import Prelude.Bifunctor
open import Prelude.Monad
open import Prelude.ToN

open import Prelude.DecEq.Core

-------------------------------
-- ** Generic deriving of DecEq

pattern `yes x  = quote _because_ ◆⟦ quote true ◆  ∣ quote ofʸ ◆⟦ x ⟧ ⟧
pattern ``yes x = quote _because_ ◇⟦ quote true ◇  ∣ quote ofʸ ◇⟦ x ⟧ ⟧
pattern `no x   = quote _because_ ◆⟦ quote false ◆ ∣ quote ofⁿ ◆⟦ x ⟧ ⟧
pattern ``no x  = quote _because_ ◇⟦ quote false ◇ ∣ quote ofⁿ ◇⟦ x ⟧ ⟧

compatible? : Type → Type → TC Bool
compatible? ty ty′ = do
  -- print $ show ty ◇ " ≈? " ◇ show ty′
  b ← runSpeculative $ (_, false) <$>
    catchTC (unify (varsToUnknown ty) (varsToUnknown ty′) >> return true)
            (return false)
  -- print $ "  ——→ " ◇ show b
  return b

`λ∅∅ = `λ⦅ [ "()" , vArg? ] ⦆∅

derive-DecEq : ℕ → (Name × Name) → Definition → TC Term

derive-DecEq _ _              (data-type _  []) = return `λ∅∅
derive-DecEq toDrop (this , ≟-rec) (data-type ps cs) = do
  print $ "DATATYPE {pars = " ◇ show ps ◇ "; cs = " ◇ show cs ◇ "}"
  cls ← concatMap L.fromMaybe <$> mapM f (allPairs cs)
  return $ pat-lam cls []
  where
    go : ℕ → List (ℕ × Arg Type) → Term
    go _ []              = `yes (quote refl ◆)
    go n ((x , _) ∷ xs) =
      let i = n ∸ suc x in
      quote case_of_
        ∙⟦ quote _≟_ ∙⟦ ♯ (i + n) ∣ ♯ i ⟧
         ∣ `λ⟦ ``no (Pattern.var 0 {-"¬p"-})
               ⦅ [ "¬p" , vArg? ] ⦆⇒
               `no (`λ⟦ (quote refl ◇)
                        ⦅ [] ⦆⇒ (♯ 0 ⟦ quote refl ◆ ⟧)
                      ⟧)
             ∣ ``yes (quote refl ◇)
               ⦅ [] ⦆⇒ go n xs
             ⟧
         ⟧

    mkPattern : Name → TC
      ( Pattern             -- ^ generated pattern for given constructor
      × ℕ                   -- ^ # of introduced variables
      × List (ℕ × Arg Type) -- ^ generated variables along with their type
      -- × List (Arg Type)     -- ^ module telescope
      )
    mkPattern c = do
      -- print $ "c: " ◇ show c
      ty ← getType c
      -- print $ "ty: " ◇ show ty
      let tys  = drop toDrop (argTys ty)
          n    = length tys
          vars = map (map₁ toℕ) (enumerate tys)
      return $ Pattern.con c (map (λ{ (i , arg x _) → arg x (` i) }) vars)
             , n
             , vars

    bumpFreeVars : (ℕ → ℕ) → List (ℕ × Arg Type) → List (ℕ × Arg Type)
    bumpFreeVars bump = go′ 0
      where
        go′ : ℕ → List (ℕ × Arg Type) → List (ℕ × Arg Type)
        go′ _ []            = []
        go′ x ((i , p) ∷ ps) = (bump i , fmap (mapFreeVars bump x) p) ∷ go′ (suc x) ps

    f : Name × Name → TC (Maybe Clause)
    f (c , c′) = do
      (pc  , n , pvs) ← mkPattern c
      -- print $ "pvs: " ◇ show pvs
      (pc′ , n′ , pvs′)   ← mkPattern c′
      -- print $ "pvs′: " ◇ show pvs′
      let
        tel = map (λ (i , argTy) → ("v" ◇ show i) , argTy) (pvs ++ bumpFreeVars (_+ n) pvs′)
        PC  = mapVariables (λ i → n + n′ ∸ suc i) pc
        PC′ = mapVariables (λ i → n′ ∸ suc i) pc′
      -- print $ "tel: " ◇ show tel
      -- print $ "pc: " ◇ show PC
      -- print $ "pc′: " ◇ show PC′
      ty  ← getType c
      ty′ ← getType c′
      b   ← compatible? (resultTy ty) (resultTy ty′)
      return $
        if b then just (⟦ PC ∣ PC′ ⦅ tel ⦆⇒ if c == c′ then go n (filter (isVisible? ∘ proj₂) pvs)
                                                       else `no `λ∅∅ ⟧)
             else nothing
derive-DecEq _ _ (record-type rn fs) = do
  print $ "RECORD {name = " ◇ show rn ◇ "; fs = " ◇ show fs ◇ "}"
  return $ `λ⟦ "r" ∣ "r′" ⇒ go fs ⟧
  where
    go : List (Arg Name) → Term
    go [] = `yes (quote refl ◆)
    go (arg (arg-info _ (modality relevant _)) n ∷ args) =
      quote case_of_
        ∙⟦ quote _≟_ ∙⟦ n ∙⟦ ♯ 1 ⟧ ∣ n ∙⟦ ♯ 0 ⟧ ⟧
         ∣ `λ⟦ ``no (Pattern.var 0 {-"¬p"-})
             ⦅ [ "¬p" , vArg? ] ⦆⇒
                 `no (`λ⟦ (quote refl ◇)
                        ⦅ [] ⦆⇒ (♯ 0 ⟦ quote refl ◆ ⟧)
                        ⟧)
             ∣ ``yes (quote refl ◇)
             ⦅ [] ⦆⇒ go args
             ⟧
         ⟧
    go (arg (arg-info _ _) _ ∷ args) = go args
derive-DecEq _ _ _ = error "impossible"

instance
  Derivable-DecEq : Derivable DecEq
  Derivable-DecEq .DERIVE' xs = do
    print "*************************************************************************"
    (record-type c _) ← getDefinition (quote DecEq)
      where _ → error "impossible"

    ys ← forM xs λ (n , f) → do
      print $ "Deriving " ◇ parens (show f ◇ " : DecEq " ◇ show n)
      f′ ← freshName (show {A = Name} f)
      T ← getType n
      ctx ← getContext
      print $ "  Context: " ◇ show ctx
      print $ "  Type: " ◇ show T
      d ← getDefinition n

      let is = drop (length ctx) (argTys T)
      let n′ = apply⋯ is n
      print $ "  Parameters: " ◇ show (parameters d)
      print $ "  Indices: " ◇ show is
      print $ "  n′: " ◇ show n′
      let mctx = take (parameters d ∸ length ctx) (argTys T)
          mtel = map ("_" ,_) mctx
          pc = map (λ where (i , _) → hArg (` toℕ i) ) (enumerate mctx)
      print $ "  Mctx: " ◇ show mctx

      -- fᵢ′ : ∀ ⋯ → Decidable² {A = Tᵢ ⋯} _≡_
      let ty′ = ∀indices⋯ is $ def (quote Decidable²) (hArg? ∷ hArg n′ ∷ vArg (quote _≡_ ∙) ∷ [])
      print $ "  Ty′: " ◇ show ty′
      declareDef (vArg f′) ty′

      -- instance fᵢ : ∀ ⋯ → DecEq (Tᵢ ⋯)
      let ty = ∀indices⋯ is $ quote DecEq ∙⟦ n′ ⟧
      print $ "  Ty: " ◇ show ty
      declareDef (iArg f) ty
      -- fᵢ ⋯ = λ where ._≟_ → fᵢ′
      -- defineFun f [ ⟦⇒ c ◆⟦ f′ ∙ ⟧ ⟧ ]
      defineFun f [ clause mtel pc (c ◆⟦ f′ ∙ ⟧) ]

      -- fᵢ′ ⋯ = λ where
      --    (c₀ x y) (c₀ x′ y′) → case x ≟ x′ of ⋯
      --    ⋯
      t ← inContext (ctx ++ L.reverse mctx) $ do
        ctx ← getContext
        print $ "  Context′: " ◇ show ctx
        derive-DecEq (length ctx) (n , f′) d
      -- print $ "  Term: " ◇ show t

      return (f′ , (pc , mtel) , t)

    return⊤ $ forM ys λ (f′ , (pc , mtel) , t) →
      defineFun f′ [ clause mtel pc t ]
      -- defineFun f′ [ ⟦⇒ t ⟧ ]

--------------------------
-- Example

private

-- ** record types

  record R⁰ : Set where
  unquoteDecl r⁰ = DERIVE DecEq [ quote R⁰ , r⁰ ]

  record R¹ : Set where
    field
      x : ℕ
  unquoteDecl r¹ = DERIVE DecEq [ quote R¹ , r¹ ]

  record R² : Set where
    field
      x : ℕ × ℤ
      y : ⊤ ⊎ Bool
  unquoteDecl r² = DERIVE DecEq [ quote R² , r² ]

-- ** inductive datatypes

  data X⁰ : Set where
  unquoteDecl x⁰ = DERIVE DecEq [ quote X⁰ , x⁰ ]

  data X¹ : Set where
    x : X¹
  unquoteDecl x¹ = DERIVE DecEq [ quote X¹ , x¹ ]

  data X² : Set where
    x y : X²
  unquoteDecl x² = DERIVE DecEq [ quote X² , x² ]

  data XX : Set where
    c₂ : List X² → XX
    c₁ : X¹ → X² → XX
  unquoteDecl xx = DERIVE DecEq [ quote XX , xx ]

-- ** recursive datatypes

  data ℕ′ : Set where
    O : ℕ′
    S : ℕ′ → ℕ′
  unquoteDecl DecEq-ℕ′ = DERIVE DecEq [ quote ℕ′ , DecEq-ℕ′ ]

-- ** list recursion

  data Nats : Set where
    O : Nats
    S : List Nats → Nats

  {-# TERMINATING #-}
{- *** T0D0: figure out how to pass termination checker

  go : Decidable² {A = Nat} _≡_
  instance
    dn : DecEq Nat
    dn ._≟_ = go
  go = λ
    { O O → yes refl
    ; O (S x0) → no (λ { () })
    ; (S x0) O → no (λ { () })
    ; (S x0) (S x0′)
        → case _≟_ ⦃ DecEq-List ⦃ dn ⦄ ⦄ x0 x0′ of λ
            { (no ¬p) → no λ { refl → ¬p refl }
            ; (yes refl) → yes refl  ⦄
-}
  unquoteDecl DecEq-Nats = DERIVE DecEq [ quote Nats , DecEq-Nats ]

-- ** mutually recursive datatypes

  data M₁ : Set
  data M₂ : Set
  data M₁ where
    m₁ : M₁
    m₂→₁ : M₂ → M₁
  data M₂ where
    m₂ : M₂
    m₁→₂ : M₁ → M₂
  unquoteDecl DecEq-M₁ DecEq-M₂ = DERIVE DecEq $ (quote M₁ , DecEq-M₁) ∷ (quote M₂ , DecEq-M₂) ∷ []

-- ** make sure all derivations were successful
  open import Data.List.Relation.Unary.All using (All; []; _∷_)
  _ : All (λ x → Decidable² {A = x} _≡_) (R⁰ ∷ R¹ ∷ R² ∷ X⁰ ∷ X¹ ∷ X² ∷ XX ∷ ℕ′ ∷ M₁ ∷ M₂ ∷ [])
  _ = _≟_ ∷ _≟_ ∷ _≟_ ∷ _≟_ ∷ _≟_ ∷ _≟_ ∷ _≟_ ∷ _≟_ ∷ _≟_ ∷ _≟_ ∷ []

-- ** indexed types

  data Fin′ : ℕ → Set where
    O : ∀ {n} → Fin′ (suc n)
    S : ∀ {n} → Fin′ n → Fin′ (suc n)
  unquoteDecl DecEq-Fin′ = DERIVE DecEq [ quote Fin′ , DecEq-Fin′ ]
  _ : ∀ {n} → Decidable² {A = Fin′ n} _≡_
  _ = _≟_

  data λExprℕ (n : ℕ) : Set where
    ƛ_ : Fin n → λExprℕ n
  unquoteDecl DecEq-λExprℕ = DERIVE DecEq [ quote λExprℕ , DecEq-λExprℕ ]

  data Boolℕ : Bool → ℕ → Set where
    O : Boolℕ true 0
  unquoteDecl DecEq-Boolℕ = DERIVE DecEq [ quote Boolℕ , DecEq-Boolℕ ]
  _ : ∀ {b n} → Decidable² {A = Boolℕ b n} _≡_
  _ = _≟_

  data Boolℕ² : Bool → ℕ → Set where
    O : Boolℕ² false 0
    I : Boolℕ² true  1
  unquoteDecl DecEq-Boolℕ² = DERIVE DecEq [ quote Boolℕ² , DecEq-Boolℕ² ]
  _ : ∀ {b n} → Decidable² {A = Boolℕ² b n} _≡_
  _ = _≟_

  data Wrapℕ : Set where
    Mk : ℕ → Wrapℕ
  unquoteDecl DecEq-Wrapℕ = DERIVE DecEq [ quote Wrapℕ , DecEq-Wrapℕ ]

  variable
    n : ℕ
    wn : Wrapℕ

  data Exprℕ : Wrapℕ → Set where
    var : Fin n → Exprℕ (Mk n)
    ‵ : ∀ {x} → ℕ → Exprℕ x
  unquoteDecl DecEq-Exprℕ = DERIVE DecEq [ quote Exprℕ , DecEq-Exprℕ ]

  data Enum : Set where
    I II : Enum
  unquoteDecl DecEq-Enum = DERIVE DecEq [ quote Enum , DecEq-Enum ]

  variable en : Enum

  Time = ℕ

  data Exprℕ′ : Wrapℕ → Enum → Set where
    var : Fin n → Exprℕ′ (Mk n) I
    ‵ : ℕ → Exprℕ′ wn II
    _`+_ : Exprℕ′ wn II → Exprℕ′ wn II → Exprℕ′ wn II
    _`-_ : Exprℕ′ wn II → Exprℕ′ wn II → Exprℕ′ wn II
    _`=_ : Exprℕ′ wn II → Exprℕ′ wn II → Exprℕ′ wn I
    _`<_ : Exprℕ′ wn II → Exprℕ′ wn II → Exprℕ′ wn I

    `if_then_else_ : Exprℕ′ wn I → Exprℕ′ wn en → Exprℕ′ wn en → Exprℕ′ wn en

    -- Size
    ∣_∣ : Exprℕ′ wn II → Exprℕ′ wn II

    -- Hashing
    hash : Exprℕ′ wn II → Exprℕ′ wn II

    -- Signature verification
    versig : List ℕ → List (Fin n) → Exprℕ′ (Mk n) I

    -- Temporal constraints
    absAfter_⇒_ : Time → Exprℕ′ wn en → Exprℕ′ wn en
    relAfter_⇒_ : Time → Exprℕ′ wn en → Exprℕ′ wn en

  unquoteDecl DecEq-Exprℕ′ = DERIVE DecEq [ quote Exprℕ′ , DecEq-Exprℕ′ ]

-- ** parametrized datatypes
{-
  data Expr (A : Set) : Set where
    Con : A → Expr A
    _⊕_ : Expr A → Expr A → Expr A
  unquoteDecl DecEq-Expr  = DERIVE DecEq [ quote Expr , DecEq-Expr ]
  _ : ∀ {A} ⦃ _ : DecEq A ⦄ → Decidable² {A = Expr A} _≡_
  _ = _≟_

  data Exprℤ : ℤ → Set where
    Con : ∀ {n} → ℤ → Exprℤ n
    _⊕_ : ∀ {x y z} → Exprℤ x → Exprℤ y → Exprℤ z
  unquoteDecl DecEq-Exprℤ  = DERIVE DecEq [ quote Exprℤ , DecEq-Exprℤ ]
  _ : ∀ {n} → Decidable² {A = Exprℤ n} _≡_
  _ = _≟_
-}

-- ** indexed records

  record Pos (n : ℕ) : Set where
    field
      pos : Fin n
  unquoteDecl DecEq-Pos  = DERIVE DecEq [ quote Pos , DecEq-Pos ]
  _ : ∀ {n} → Decidable² {A = Pos n} _≡_
  _ = _≟_

-- ** datatypes inside module

  module Test₁ (A : Set) ⦃ _ : DecEq A ⦄ (B : Set) ⦃ _ : DecEq B ⦄ where

    data X : ℕ → Set where
      x₀ y₀ z₀ : X 0
      x₁ y₁ z₁ : X 1
      fromA    : ∀ {n} → A → X n
      fromB    : ∀ {n} → B → X n
    unquoteDecl DecEq-Test1X = DERIVE DecEq [ quote X , DecEq-Test1X ]

    _ : ∀ {n} → Decidable² {A = X n} _≡_
    _ = _≟_

    record R : Set where
      field
        r₁ : A
        r₂ : B
    unquoteDecl DecEq-Test1R = DERIVE DecEq [ quote R , DecEq-Test1R ]
    _ : Decidable² {A = R} _≡_
    _ = _≟_

    record R′ : Set where
      field
        r₁ : A × B
        r₂ : X 0
    unquoteDecl DecEq-Test1R′ = DERIVE DecEq [ quote R′ , DecEq-Test1R′ ]
    _ : Decidable² {A = R′} _≡_
    _ = _≟_

  module _ (A : Set) ⦃ _ : DecEq A ⦄ {B : Set} ⦃ _ : DecEq B ⦄ where
    open Test₁ A B

    _ : ∀ {n} → Decidable² {A = X n} _≡_
    _ = _≟_
    _ : Decidable² {A = R} _≡_
    _ = _≟_
    _ : Decidable² {A = R′} _≡_
    _ = _≟_

  unquoteDecl DecEq-Test1R = DERIVE DecEq [ quote Test₁.R , DecEq-Test1R ]
  _ : ∀ {A : Set} ⦃ _ : DecEq A ⦄ {B : Set} ⦃ _ : DecEq B ⦄
    → Decidable² {A = Test₁.R A B} _≡_
  _ = _≟_

  -- unquoteDecl DecEq-Test1R′ = DERIVE DecEq [ quote Test₁.R′ , DecEq-Test1R′ ]
  -- _ : ∀ {A : Set} ⦃ _ : DecEq A ⦄ {B : Set} ⦃ _ : DecEq B ⦄
  --   → Decidable² {A = Test₁.R′ A B} _≡_
  -- _ = _≟_

  data λExprℕ′ (mn : Wrapℕ) : Set where
    ƛ_ : Exprℕ′ mn II → λExprℕ′ mn
  unquoteDecl DecEq-λExprℕ′ = DERIVE DecEq [ quote λExprℕ′ , DecEq-λExprℕ′ ]


  module Test₂ (A : Set) ⦃ _ : DecEq A ⦄ where
    data Label : Set where
      auth-divide : A → ℕ → ℕ → ℕ → Label
    unquoteDecl DecEq-Label = DERIVE DecEq [ quote Label , DecEq-Label ]