{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Data.HDiff.Diff.Preprocess where
import Data.Proxy
import Data.Functor.Const
import Generics.MRSOP.Base
import Generics.MRSOP.Holes
import Generics.MRSOP.HDiff.Digest
data PrepData a = PrepData
{ treeDigest :: Digest
, treeHeight :: Int
, treeParm :: a
} deriving (Eq , Show)
type PrepFix a ki codes phi
= HolesAnn (Const (PrepData a)) ki codes phi
preprocess :: forall ki codes phi at
. (DigestibleHO ki, DigestibleHO phi)
=> Holes ki codes phi at
-> PrepFix () ki codes phi at
preprocess = holesSynthesize (const ppHole) (const ppOpq) ppPeel
where
pCodes :: Proxy codes
pCodes = Proxy
safeMax [] = 0
safeMax l = maximum l
ppHole :: forall at' . phi at' -> Const (PrepData ()) at'
ppHole x = Const $ PrepData (digestHO x) 1 ()
ppOpq :: forall k . ki k -> Const (PrepData ()) ('K k)
ppOpq x = Const $ PrepData (digestHO x) 1 ()
ppPeel :: forall i x
. IsNat x
=> Const () ('I x)
-> Constr (Lkup x codes) i
-> NP (Const (PrepData ())) (Lkup i (Lkup x codes))
-> Const (PrepData ()) ('I x)
ppPeel _ c p
= let pix :: Proxy x
pix = Proxy
dig = authPeel (treeDigest . getConst) pCodes pix c p
h = 1 + safeMax (elimNP (treeHeight . getConst) p)
in Const $ PrepData dig h ()