Unordered.hs

{-|
Module      : Data.GenRecord.Unordered
Description : polykinded extensible record library
Copyright   : (c) Juan García Garland (2023)
License     : GPL
Maintainer  : jpgarcia@fing.edu.uy
Stability   : experimental
Portability : POSIX

Records where labels are names (|Symbol|s) and preserve the insertion
order (hence they are not ordered alphanumerically).

We did not reuse Generic record constructs from |Data.GenRec| and
built new definitions instead. This module is intended to mimmick
ordinary Haskell records, while being extensive.

One quirk of the definitions in this module is that we admit repeated
labels. Ordinary lookup will get the first occurrence, but we build
different kind of projections to get all values under a label. This
development was first intended to represent a collection of registers
with names and values, hence the field name.

-}

{-# OPTIONS_GHC -fno-warn-missing-methods #-}

{-# LANGUAGE DataKinds,
             TypeOperators,
             PolyKinds,
             GADTs,
             RankNTypes,
             StandaloneDeriving,
             FlexibleInstances,
             FlexibleContexts,
             ConstraintKinds,
             MultiParamTypeClasses,
             FunctionalDependencies,
             UndecidableInstances,
             ScopedTypeVariables,
             TypeFamilies,
             InstanceSigs,
             AllowAmbiguousTypes,
             TypeApplications,
             PatternSynonyms,
             DataKinds, PolyKinds
#-}

module Data.GenRec.Unordered where
import Data.Label
import GHC.TypeLits (Symbol, symbolVal, KnownSymbol)
import Data.Kind
import Data.Proxy
import Data.Type.Require

import Data.GenRec (UnWrap)

data Reg (l :: Symbol) v where
  Reg :: (KnownSymbol l) => v -> Reg l v

instance
  Show v
  =>
  Show (Reg l v) where
  show (Reg v) = symbolVal (Proxy @l) ++ " : " ++ show v

infixr 5 :<
data Record (r :: [(Symbol, Type)]) :: Type where
  Empty :: Record '[] -- ^ empty record
  (:<) :: Reg l v -> Record r -> Record ('( l, v) ': r) -- ^

instance
  Show (Record '[]) where
  show Empty = "{}"

instance
  (Show v)
  =>
  Show (Record '[ '(l,v)]) where
  show (reg :< _) = "{ " ++ show reg ++ "}"
  
instance
  ( Show v
  , Show (Record (lv ': r)))
  =>
  Show (Record ( '(l, v) ': lv ': r)) where
  show (reg :< r) =  "{" ++ show reg ++ ", " ++ tail (show r)

ex1 =  Reg @"x" 3.0
    :< Reg @"y" 2.1
    :< Reg @"z" ()
    :< Reg @"t" 0
    :< Empty

ex2 =  Reg @"header" ()
    :< Reg @"val" 2.1
    :< Reg @"val" 1.1
    :< Reg @"val" 0.0
    :< Reg @"footer" "END"
    :< Empty

type instance UnWrap (Record l) = l

data OpSnoc (l :: Symbol) (v :: Type) (r :: [(Symbol, Type)]) where
  OpSnoc :: Reg l v -> Record r -> OpSnoc l v r

instance
  Require (OpSnoc l v '[]) ctx where
  type ReqR (OpSnoc l v '[])
    = Record '[ '(l, v)]
  req ctx (OpSnoc lv _) = lv :< Empty


instance
  RequireR (OpSnoc l v r) (Record (UnWrap (ReqR (OpSnoc l v r)))) ctx
  =>
  Require (OpSnoc l v ( '(l',v') ': r)) ctx where
  type ReqR (OpSnoc l v ( '(l',v') ': r)) =
    Record ( '(l',v') ': UnWrap @Symbol @Type (ReqR (OpSnoc l v r)))
  req ctx (OpSnoc lv (lv' :< r)) = lv' :< req ctx (OpSnoc lv r) 

r >: lv = req (Proxy @'[]) (OpSnoc lv r)