{-# LANGUAGE Trustworthy, TypeOperators, TypeFamilies, ScopedTypeVariables, IncoherentInstances, FlexibleInstances, FlexibleContexts, MultiParamTypeClasses, Rank2Types, OverlappingInstances #-}
-- | A serializer for the Data.Record module.
module Data.SwizRecord (KindSwiz(KindSwiz), module Data.Record, module Data.Kind, module Data.TypeFun, module File.Graph) where

import Data.Record
import Data.Kind
import Data.TypeFun
import Control.Monad
import File.Mapped
import File.Graph

type instance Represent (X style) = ()

type instance Represent ((n ::: v) style) = App style v

type instance Represent ((r :& v) style) = (Represent (r style), v style)

-- | The kind of swizzleable types.
data KindSwiz = KindSwiz

instance Kind KindSwiz where
	data All KindSwiz item = AllSwiz (forall val. (Swiz val) => item val)
	closed item = AllSwiz item

instance (Swiz val) => Inhabitant KindSwiz val where
	specialize (AllSwiz item) = item

split :: (r :& t ::: u) style -> (r style, App style u)
split _ = (undefined, undefined)

newtype Measure rec = Measure { unMeasure :: rec (Id KindSwiz) -> Int }

data Unswizzle rec = Unswizzle { unUnswizzle :: FilePtr (rec (Id KindSwiz)) -> rec (Id KindSwiz) -> UnswizM (), measure :: Measure rec }

data Swizzle rec = Swizzle { unSwizzle :: FilePtr (rec (Id KindSwiz)) -> SwizM (rec (Id KindSwiz)), measure1 :: Measure rec }

instance (Record KindSwiz rec) => Swiz (rec (Id KindSwiz)) where
	size = unMeasure $ fold (Measure (\_ -> 0)) (AllSwiz (Expander (\(Measure f) -> Measure (\r -> let (r', x) = split r in f r' + (size x `lcm` aligned x)))))
	aligned rec = aln rec `max` 1 where
		aln = unMeasure $ fold (Measure (\_ -> 0)) (AllSwiz (Expander (\(Measure f) -> Measure (\(r :& (_ := v)) ->
			let x = f r in
			if x == 0 then aligned v else x))))
	unswizzle = unUnswizzle $ fold (Unswizzle (\_ _ -> return ()) (Measure size)) (AllSwiz (Expander (\(Unswizzle f sz) ->
		Unswizzle (\p (r :& (_ := v)) -> do
			f (coerce p) r
			unswizzle (coerce (plus p (unMeasure sz r))) v)
			(Measure size))))
	swizzle = unSwizzle $ fold (Swizzle (\_ -> return X) (Measure size)) (AllSwiz (Expander (\(Swizzle f sz) ->
		Swizzle (\p -> do
			rec <- f (coerce p)
			v <- swizzle (coerce (plus p (unMeasure sz undefined)))
			return (rec :& (name := v)))
			(Measure size))))

instance Name () where
	name = ()