-- SPDX-FileCopyrightText: 2020 Tocqueville Group
--
-- SPDX-License-Identifier: LicenseRef-MIT-TQ

module Lorentz.UStore.Migration.Diff
  ( FieldInfo
  , DiffKind (..)
  , DiffItem
  , BuildDiff
  , ShowDiff
  , RequireEmptyDiff

  , LinearizeUStore
  , LinearizeUStoreF
  , AllUStoreFieldsF

  , DiffCoverage (..)
  , CoverDiff
  , CoverDiffMany
  ) where

import qualified Data.Kind as Kind
import Fcf (type (***), type (=<<), Eval, Exp, Fst, Pure)
import qualified Fcf
import Fcf.Data.List (Cons)
import Fcf.Utils (TError)
import GHC.Generics ((:*:), (:+:))
import qualified GHC.Generics as G

import Lorentz.UStore.Types
import Util.Type
import Util.TypeLits

-- Diff definition
----------------------------------------------------------------------------

-- | Information about single field of UStore.
type FieldInfo = (Symbol, Kind.Type)

-- | What should happen with a particular 'UStoreItem'.
data DiffKind = ToAdd | ToDel

-- | Single piece of a diff.
type DiffItem = (DiffKind, FieldInfo)

-- Building diff
----------------------------------------------------------------------------

-- | Get information about all fields of UStore template in a list.
--
-- In particular, this recursivelly traverses template and retrives
-- names and types of fields. Semantic wrappers like 'UStoreField'
-- and '|~>' in field types are returned as-is.
type LinearizeUStore a = GLinearizeUStore (G.Rep a)

data LinearizeUStoreF (template :: Kind.Type) :: Exp [FieldInfo]
type instance Eval (LinearizeUStoreF template) = LinearizeUStore template

-- | Get only field names of UStore template.
type family AllUStoreFieldsF (template :: Kind.Type) :: Exp [Symbol] where
  AllUStoreFieldsF template = Fcf.Map Fst =<< LinearizeUStoreF template

type family GLinearizeUStore (template :: Kind.Type -> Kind.Type)
    :: [FieldInfo] where
  GLinearizeUStore (G.D1 _ x) = GLinearizeUStore x
  GLinearizeUStore (G.C1 _ x) = GLinearizeUStore x
  GLinearizeUStore (_ :+: _) = TypeError
    ('Text "Unexpected sum type in UStore template")
  GLinearizeUStore G.V1 = TypeError
    ('Text "Unexpected void-like type in UStore template")
  GLinearizeUStore G.U1 = '[]
  GLinearizeUStore (x :*: y) = GLinearizeUStore x ++ GLinearizeUStore y

  GLinearizeUStore (G.S1 ('G.MetaSel mfield _ _ _) (G.Rec0 (k |~> v))) =
    '[ '(RequireFieldName mfield, k |~> v) ]
  GLinearizeUStore (G.S1 ('G.MetaSel mfield _ _ _) (G.Rec0 (UStoreFieldExt m v))) =
    '[ '(RequireFieldName mfield, UStoreFieldExt m v) ]
  GLinearizeUStore (G.S1 _ (G.Rec0 a)) =
    LinearizeUStore a

-- | Helper to make sure that datatype field is named and then extract this name.
type family RequireFieldName (mfield :: Maybe Symbol) :: Symbol where
  RequireFieldName ('Just field) = field
  RequireFieldName 'Nothing = TypeError ('Text "Unnamed field in UStore template")

-- | Lift a list of 'FieldInfo' to 'DiffItem's via attaching given 'DiffKind'.
type family LiftToDiff (kind :: DiffKind) (items :: [FieldInfo]) :: [DiffItem] where
  LiftToDiff _ '[] = '[]
  LiftToDiff kind (item ': items) = '(kind, item) ': LiftToDiff kind items

-- | Make up a migration diff between given old and new 'UStore' templates.
type BuildDiff oldTemplate newTemplate =
  LiftToDiff 'ToAdd (LinearizeUStore newTemplate // LinearizeUStore oldTemplate)
  ++
  LiftToDiff 'ToDel (LinearizeUStore oldTemplate // LinearizeUStore newTemplate)

-- Pretty-printing diff
----------------------------------------------------------------------------

-- | Renders human-readable message describing given diff.
type ShowDiff diff =
  'Text "Migration is incomplete, remaining diff:" ':$$: ShowDiffItems diff

type family ShowDiffItems (diff :: [DiffItem]) :: ErrorMessage where
  ShowDiffItems '[d] = ShowDiffItem d
  ShowDiffItems (d : ds) = ShowDiffItem d ':$$: ShowDiffItems ds

type family ShowDiffKind (kind :: DiffKind) :: Symbol where
  ShowDiffKind 'ToAdd = "+"
  ShowDiffKind 'ToDel = "-"

type family ShowUStoreElement (ty :: Kind.Type) :: ErrorMessage where
  ShowUStoreElement (UStoreFieldExt m f) =
    ShowUStoreField m f
  ShowUStoreElement (k |~> v) =
    'Text "submap " ':<>: 'ShowType k ':<>: 'Text " -> " ':<>: 'ShowType v

type family ShowDiffItem (diff :: DiffItem) :: ErrorMessage where
  ShowDiffItem '(kind, '(field, ty)) =
    'Text (ShowDiffKind kind `AppendSymbol`
           " `" `AppendSymbol`
           field `AppendSymbol`
           "`") ':<>:
    'Text ": " ':<>: ShowUStoreElement ty

-- | Helper type family which dumps error message about remaining diff
-- if such is present.
type family RequireEmptyDiff (diff :: [DiffItem]) :: Constraint where
  RequireEmptyDiff '[] = ()
  RequireEmptyDiff diff = TypeError (ShowDiff diff)

-- Diff coverage
----------------------------------------------------------------------------

-- | Cover the respective part of diff.
-- Maybe fail if such action is not required.
--
-- This type is very similar to 'DiffKind', but we still use another type as
-- 1. Their kinds will differ - no chance to mix up anything.
-- 2. One day there might appear more complex actions.
data DiffCoverage
  = DcAdd
  | DcRemove

type family PrefixSecond (a :: k2) (r :: (k1, [k2])) :: (k1, [k2]) where
  PrefixSecond a '(t, l) = '(t, (a ': l))

-- | Apply given diff coverage, returning type of affected field and modified
-- diff.
type family CoverDiff (cover :: DiffCoverage) (field :: Symbol) (diff :: [DiffItem])
            :: (Kind.Type, [DiffItem]) where
  CoverDiff cover field diff = Eval (CoverDiffF '(cover, field) diff)

type family CoverDiffF (arg :: (DiffCoverage, Symbol)) (diff :: [DiffItem])
            :: Exp (Kind.Type, [DiffItem]) where
  CoverDiffF '( 'DcAdd, field) diff = RemoveDiffF 'ToAdd field diff
  CoverDiffF '( 'DcRemove, field) diff = RemoveDiffF 'ToDel field diff

type family RemoveDiffF (kind :: DiffKind) (field :: Symbol) (diff :: [DiffItem])
            :: Exp (Kind.Type, [DiffItem]) where
  RemoveDiffF kind field ('(kind, '(field, ty)) ': diff) = Pure '(ty, diff)
  RemoveDiffF kind field (d ': diff) = (Pure *** Cons d) =<< RemoveDiffF kind field diff
  RemoveDiffF kind field '[] =
    TError ('Text (ShowDiffKindWord kind) ':<>: 'Text " field " ':<>:
            'ShowType field ':<>: 'Text " is not required")

type family ShowDiffKindWord (kind :: DiffKind) :: Symbol where
  ShowDiffKindWord 'ToAdd = "Adding"
  ShowDiffKindWord 'ToDel = "Removing"

-- | Single piece of a coverage.
type DiffCoverageItem = (DiffCoverage, FieldInfo)

-- | Apply multiple coverage steps.
type family CoverDiffMany (diff :: [DiffItem]) (covers :: [DiffCoverageItem])
            :: [DiffItem] where
  CoverDiffMany diff '[] = diff
  CoverDiffMany diff ('(dc, '(field, ty)) ': cs) =
    CoverDiffMany (HandleCoverRes field ty (CoverDiff dc field diff)) cs

type family HandleCoverRes (field :: Symbol) (ty :: Kind.Type) (res :: (Kind.Type, [DiffItem]))
            :: [DiffItem] where
  HandleCoverRes _ ty '(ty, diff) = diff
  HandleCoverRes field tyCover '(tyDiff, _) = TypeError
    ('Text "Type mismatch when covering diff for field " ':<>: 'ShowType field
     ':$$:
     'Text "Expected type `" ':<>: 'ShowType tyDiff ':<>: 'Text "` (in requested diff)"
     ':$$:
     'Text "but covered with value of type `" ':<>: 'ShowType tyCover ':<>: 'Text "`"
    )

type family EnsureDiffHasNoRemovalF (field :: Symbol) (diff :: [DiffItem])
             :: Exp [DiffItem] where
  EnsureDiffHasNoRemovalF _ '[] = Pure '[]
  EnsureDiffHasNoRemovalF field ('( 'ToDel, '(field, _)) ': _) =
    TError ('Text "Field with name " ':<>: 'ShowType field ':<>:
            'Text " is present in old version of storage"
           )
  EnsureDiffHasNoRemovalF field (d ': diff) =
    Cons d =<< EnsureDiffHasNoRemovalF field diff