{-# 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
  )
  where

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


-- | * 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 $bTagged :: v -> Tagged l v
$mTagged :: forall r v (l :: Symbol).
Tagged l v -> (v -> r) -> (Void# -> r) -> r
Tagged v = TagField Label Label v


-- ** Constructors

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

-- | For the empty Record
emptyRecord :: Record ('[] :: [(Symbol, Type)])
emptyRecord :: Record '[]
emptyRecord = Record '[]
forall k k' k'' (c :: k). Rec c '[]
EmptyRec

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

-- * Destructors
-- | Get a label
getLabel :: Tagged l v -> Label l
getLabel :: Tagged l v -> Label l
getLabel Tagged l v
_ = Label l
forall k (l :: k). Label l
Label

-- | Lookup
infixl 5 ##
Rec Reco r
r ## :: Rec Reco r -> Label l -> ReqR (OpLookup Reco l r)
## (Label l
l :: Label l) = Rec Reco r -> Label l -> ReqR (OpLookup Reco l r)
forall k k'' c (l :: k) (r :: [(k, k'')]) (ctx :: [ErrorMessage])
       v.
RequireR (OpLookupCall c l r) ctx v =>
Rec c r -> Label l -> v
(#) @Reco @l Rec Reco r
r Label l
l

-- | extension
infixr 2 .**.
(Tagged l v
lv :: Tagged l v) .**. :: Tagged l v -> Rec Reco r -> ReqR (OpExtend Reco l v r)
.**. Rec Reco r
r = Tagged l v -> Rec Reco r -> ReqR (OpExtend Reco l v r)
forall k k' c (l :: k) (v :: k') (r :: [(k, k')]).
Require (OpExtend c l v r) '[ 'Text ""] =>
TagField c l v -> Rec c r -> ReqR (OpExtend c l v r)
(.*.)  Tagged l v
lv Rec Reco r
r
-- The Tagged annotation is enough to unify everything

instance ( Show v
         , KnownSymbol l )
  =>
  Show (Tagged l v) where
  show :: Tagged l v -> String
show (Tagged v
v :: TagField Reco l v) =
    Proxy l -> String
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> String
symbolVal (Label l -> Proxy l
proxyFrom (Label l
forall k (l :: k). Label l
Label @l)) String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" : "String -> ShowS
forall a. [a] -> [a] -> [a]
++ v -> String
forall a. Show a => a -> String
show v
v
     where proxyFrom :: Label l -> Proxy l
           proxyFrom :: Label l -> Proxy l
proxyFrom Label l
_ = Proxy l
forall k (t :: k). Proxy t
Proxy

instance Show (Record '[]) where
  show :: Record '[] -> String
show Record '[]
_ = String
"{}"

instance ( Show v
         , KnownSymbol l)
  =>
  Show (Record '[ '(l, v)]) where
  show :: Record '[ '(l, v)] -> String
show (ConsRec TagField Reco l v
lv Rec Reco r
EmptyRec) =
    Char
'{' Char -> ShowS
forall a. a -> [a] -> [a]
: TagField Reco l v -> String
forall a. Show a => a -> String
show TagField Reco l v
lv String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"}"

instance ( Show v
         , KnownSymbol l
         , Show (Record ( '(l', v') ': r )))
  =>
  Show (Record ( '(l, v) ': '(l', v') ': r )) where
  show :: Record ('(l, v) : '(l', v') : r) -> String
show (ConsRec TagField Reco l v
lv Rec Reco r
r) =
    let (Char
'{':String
shr) = Rec Reco r -> String
forall a. Show a => a -> String
show Rec Reco r
r
    in Char
'{' Char -> ShowS
forall a. a -> [a] -> [a]
: TagField Reco l v -> String
forall a. Show a => a -> String
show TagField Reco l v
lv String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
shr


r :: ReqR (OpExtend Reco "integer" Integer '[ '("boolean", Bool)])
r =        (Label "integer"
forall k (l :: k). Label l
Label @"integer" Label "integer" -> Integer -> Tagged "integer" Integer
forall (l :: Symbol) v. Label l -> v -> Tagged l v
.==. (Integer
3 :: Integer))
     Tagged "integer" Integer
-> Rec Reco '[ '("boolean", Bool)]
-> ReqR (OpExtend Reco "integer" Integer '[ '("boolean", Bool)])
forall (l :: Symbol) v (r :: [(Symbol, *)]).
Require (OpExtend Reco l v r) '[ 'Text ""] =>
Tagged l v -> Rec Reco r -> ReqR (OpExtend Reco l v r)
.**.  (Label "boolean"
forall k (l :: k). Label l
Label @"boolean" Label "boolean" -> Bool -> Tagged "boolean" Bool
forall (l :: Symbol) v. Label l -> v -> Tagged l v
.==. Bool
True)
     Tagged "boolean" Bool
-> Record '[] -> ReqR (OpExtend Reco "boolean" Bool '[])
forall (l :: Symbol) v (r :: [(Symbol, *)]).
Require (OpExtend Reco l v r) '[ 'Text ""] =>
Tagged l v -> Rec Reco r -> ReqR (OpExtend Reco l v r)
.**.  Record '[]
emptyRecord


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 $bTaggedRecord :: Record r -> TaggedRecord l r
$mTaggedRecord :: forall r (l :: Nat) (r :: [(Symbol, *)]).
TaggedRecord l r -> (Record r -> r) -> (Void# -> r) -> r
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 :: ReqR
  (OpExtend
     Mat 1 '[ '("boolean", Bool), '("integer", Integer)] '[ '(2, '[])])
m = let tf :: Label Mat -> Label l -> Record r -> TagField Mat l r
tf = (forall k' (l :: k') (r :: [(Symbol, *)]).
Label Mat -> Label l -> Record r -> TagField Mat l r
forall k k' k'' (c :: k) (l :: k') (v :: k'').
Label c -> Label l -> WrapField c v -> TagField c l v
TagField :: forall l r . -- (l::Nat) (r :: [(Symbol, Type)]).
               Label Mat -> Label l -> Record r -> TagField Mat l r)
    in      Label Mat
-> Label 1
-> Record '[ '("boolean", Bool), '("integer", Integer)]
-> TagField Mat 1 '[ '("boolean", Bool), '("integer", Integer)]
forall k' (l :: k') (r :: [(Symbol, *)]).
Label Mat -> Label l -> Record r -> TagField Mat l r
tf Label Mat
forall k (l :: k). Label l
Label (Label 1
forall k (l :: k). Label l
Label @1) Record '[ '("boolean", Bool), '("integer", Integer)]
r
       TagField Mat 1 '[ '("boolean", Bool), '("integer", Integer)]
-> Rec Mat '[ '(2, '[])]
-> ReqR
     (OpExtend
        Mat 1 '[ '("boolean", Bool), '("integer", Integer)] '[ '(2, '[])])
forall k k' c (l :: k) (v :: k') (r :: [(k, k')]).
Require (OpExtend c l v r) '[ 'Text ""] =>
TagField c l v -> Rec c r -> ReqR (OpExtend c l v r)
.*.  Label Mat -> Label 2 -> Record '[] -> TagField Mat 2 '[]
forall k' (l :: k') (r :: [(Symbol, *)]).
Label Mat -> Label l -> Record r -> TagField Mat l r
tf Label Mat
forall k (l :: k). Label l
Label (Label 2
forall k (l :: k). Label l
Label @2) Record '[]
emptyRecord
       TagField Mat 2 '[] -> Rec Mat '[] -> ReqR (OpExtend Mat 2 '[] '[])
forall k k' c (l :: k) (v :: k') (r :: [(k, k')]).
Require (OpExtend c l v r) '[ 'Text ""] =>
TagField c l v -> Rec c r -> ReqR (OpExtend c l v r)
.*.  Rec Mat '[]
forall k k' k'' (c :: k). Rec c '[]
EmptyRec

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