Record.hs

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

module Data.GenRec.RecInstances.Record
  (Record, Reco,
   untag, getLabel,
   (.==.), (.**.), (##),
   emptyRecord, Tagged (..), Tagged
  )
  where

import GHC.TypeLits
import Data.Kind
import Data.Proxy
import Data.GenRec
import Data.Label

import Data.Type.Equality
import Unsafe.Coerce


-- | * Records

-- | datatype definition
type Record        = (Rec Reco :: [(Symbol, Type)] -> Type)

-- | index type
data Reco

-- | field type
type instance  WrapField Reco     (v :: Type) = v

-- | Type level show utilities
type instance ShowRec Reco         = "Record"
type instance ShowField Reco       = "field named "


type Tagged (l :: Symbol) (v :: Type) = TagField Reco l v
pattern Tagged :: v -> Tagged l v
pattern Tagged v = TagField Label Label v


-- ** Constructors

-- | Pretty Constructor
infix 4 .==.
(.==.) :: Label l -> v -> Tagged l v
l .==. v = Tagged v

-- | For the empty Record
emptyRecord :: Record ('[] :: [(Symbol, Type)])
emptyRecord = EmptyRec

untag :: Tagged l v -> v
untag (TagField _ _ v) = v

-- * Destructors
-- | Get a label
getLabel :: Tagged l v -> Label l
getLabel _ = Label

-- | Lookup
infixl 5 ##
r ## (l :: Label l) = (#) @Reco @l r l

-- | extension
infixr 2 .**.
(lv :: Tagged l v) .**. r = (.*.)  lv r
-- The Tagged annotation is enough to unify everything

instance ( Show v
         , KnownSymbol l )
  =>
  Show (Tagged l v) where
  show (Tagged v :: TagField Reco l v) =
    symbolVal (proxyFrom (Label @l)) ++ " : "++ show v
     where proxyFrom :: Label l -> Proxy l
           proxyFrom _ = Proxy

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

instance ( Show v
         , KnownSymbol l)
  =>
  Show (Record '[ '(l, v)]) where
  show (ConsRec lv EmptyRec) =
    '{' : show lv ++ "}"

instance ( Show v
         , KnownSymbol l
         , Show (Record ( '(l', v') ': r )))
  =>
  Show (Record ( '(l, v) ': '(l', v') ': r )) where
  show (ConsRec lv r) =
    let ('{':shr) = show r
    in '{' : show lv ++ ", " ++ shr


data Mat
type Matrix = Rec Mat :: [(Nat, [(Symbol, Type)])] -> Type

type instance  WrapField Mat  (r :: [(Symbol, Type)]) = Record r

-- | Type level show utilities
type instance ShowRec Mat         = "Matrix"
type instance ShowField Mat       = "record named "

type TaggedRecord (l :: Nat) (r :: [(Symbol, Type)]) = TagField Mat l r
pattern TaggedRecord :: forall l r. Record r -> TaggedRecord l r
pattern TaggedRecord r = TagField Label Label r


instance OrdType Nat where
  type Cmp (m :: Nat) (n :: Nat) = CmpNat m n


--m = TaggedRecord @1 r .*. TaggedRecord @2 emptyRecord .*. EmptyRec 

--m = (TagField @Mat (l::Nat) (r :: [(Symbol, Type)]))

m = let tf = (TagField :: forall l r . -- (l::Nat) (r :: [(Symbol, Type)]).
               Label Mat -> Label l -> Record r -> TagField Mat l r)
    in      tf Label (Label @1) r
       .*.  tf Label (Label @2) emptyRecord
       .*.  EmptyRec

-- m' =        TagField @Mat (Label @Mat) (Label @1) r
--        .*.  TagField (Label @Mat) (Label @2) (EmptyRec :: Record ('[] :: [(Symbol, Type)]))
--        .*.  EmptyRec

rCast :: Record '[ '("int", Int)]
rCast = castWith (sym bad) r
 where bad :: Record '[ '("int", Int)]
             :~: Record '[ '("boolean", Bool), '("int", Int)]
       bad = unsafeCoerce Refl -- undefined  no funciona porque se evalúa la prueba


r  =        (Label @"int" .==. (3 :: Int))
      .**.  (Label @"boolean" .==. True)
      .**.  emptyRecord


-- r1 :: Record
--        '[ '("boolean", Bool),
--           '("boolean2", Bool),
--           '("int", Int),
--           '("int2", Int)]
r1 =        (Label @"int" .==. (3 :: Int))
      .**.  (Label @"boolean" .==. True)
      .**.  (Label @"int2" .==. (5 :: Int))
      .**.  (Label @"boolean2" .==. False)
      .**.  emptyRecord

-- r2 :: Record
--        '[ '("char", Char),
--           '("int", Int),
--           '("integer", Integer),
--           '("unit", ())]
r2 =        (Label @"int" .==. (40 :: Int))
      .**.  (Label @"unit" .==. ())
      .**.  (Label @"integer" .==. (5 :: Integer))
      .**.  (Label @"boolean" .==. False)
      .**.  emptyRecord

t3    = r1 # Label @"int"
tTrue = r1 # Label @"boolean"

r12 = r1 .:>< r2

-- r12 == {boolean : True,
--         boolean2 : False,
--         int : 3,
--         int2 : 5,
--         integer : 5,
--         unit : ()}