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

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

module Language.Grammars.AspectAG.RecordInstances where

import Data.Type.Require
import Data.GenRec
import GHC.TypeLits
import Data.Kind
import Data.Proxy

data Att   = Att Symbol Type                -- deriving Eq
data Prod  = Prd Symbol NT                  -- deriving Eq
data Child = Chi Symbol Prod (Either NT T)  -- deriving Eq
data NT    = NT Symbol                      -- deriving Eq
data T     = T Type                         -- deriving Eq

prdFromChi :: Label (Chi nam prd tnt) -> Label prd
prdFromChi :: Label ('Chi nam prd tnt) -> Label prd
prdFromChi Label ('Chi nam prd tnt)
_ = Label prd
forall k (l :: k). Label l
Label


instance OrdType Att where
   type Cmp ('Att a _) ('Att b _)
     = CmpSymbol a b

instance OrdType Prod where 
  type Cmp ('Prd a _) ('Prd b _)
    = CmpSymbol a b

instance OrdType Child where
  type Cmp ('Chi a _ _) ('Chi b _ _) = CmpSymbol a b


type instance ShowTE ('Att l t) = Text ("(" `AppendSymbol` l
  `AppendSymbol` ":" `AppendSymbol` FromEM(ShowTE t) `AppendSymbol`
  ")")

type instance ShowTE ('Prd l nt) = Text ( "(" `AppendSymbol` l
    `AppendSymbol` " of " `AppendSymbol` FromEM (ShowTE nt)
    `AppendSymbol` ")")

type instance ShowTE ('Chi l p s) = Text ("Child " `AppendSymbol` l
  `AppendSymbol` " of producion " `AppendSymbol` FromEM (ShowTE p))
  
type instance  ShowTE ('Left l)    = ShowTE l
type instance  ShowTE ('Right r)   = ShowTE r
type instance  ShowTE ('NT l)      = Text ("Non-Terminal " `AppendSymbol` l)
type instance  ShowTE ('T  l)
  = Text ("Terminal " `AppendSymbol` FromEM (ShowTE l))

--type instance ShowLabel (l :: Symbol) = l
--type instance ShowLabel (c :: k) = FromEM (ShowTE c)

-- | * Records

-- | datatype definition
type Record        = Rec Reco

-- | 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"


type Tagged = TagField Reco
pattern Tagged :: v -> Tagged l v
pattern $bTagged :: v -> Tagged l v
$mTagged :: forall r k' v (l :: k').
Tagged l v -> (v -> r) -> (Void# -> r) -> r
Tagged v = TagField Label Label v


-- ** Constructors

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

-- -- | For the empty Record
-- emptyRecord :: Record '[]
-- emptyRecord = EmptyRec

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

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

-- -- | Same, mnemonically defined
-- labelTChAtt :: Tagged l v -> Label l
-- labelTChAtt _ = Label


-- -- | Show instance, used for debugging
-- instance Show (Record '[]) where
--   show _ = "{}"

-- instance (Show v, Show (Record xs)) =>
--          Show (Record ( '(l,v) ': xs ) ) where
--   show (ConsRec lv xs) = let tail = show xs
--                          in "{" ++ show (unTagged lv)
--                             ++ "," ++ drop 1 tail



-- | * Attribution
-- | An attribution is a record constructed from attributes

-- | datatype implementation
type Attribution (attr :: [(Att,Type)]) =  Rec AttReco attr

-- | index type
data AttReco

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

-- | type level utilities
type instance ShowRec AttReco      = "Attribution"
type instance ShowField AttReco       = "attribute"

-- | Pattern Synonyms
-- pattern EmptyAtt :: Attribution '[]
-- pattern EmptyAtt = EmptyRec
-- pattern ConsAtt :: LabelSet ( '(att, val) ': atts) =>
--     Attribute att val -> Attribution atts -> Attribution ( '(att,val) ': atts)
-- pattern ConsAtt att atts = ConsRec att atts

-- | Attribute

type Attribute (l :: Att) (v :: Type) = TagField AttReco l v
pattern Attribute :: v -> TagField AttReco l v
pattern $bAttribute :: v -> TagField AttReco l v
$mAttribute :: forall r k' v (l :: k').
TagField AttReco l v -> (v -> r) -> (Void# -> r) -> r
Attribute v = TagField Label Label v

-- ** Constructors
-- | Apretty constructor for an attribute 
infixr 4 =.

(=.) :: Label l -> v -> Attribute l v
Label l
Label =. :: Label l -> v -> Attribute l v
=. v
v = v -> Attribute l v
forall k' v (l :: k'). v -> TagField AttReco l v
Attribute v
v


-- | Extending
infixr 2 *.
-- (*.) :: Attribute att val -> Attribution atts
--       -> Attribution (ReqR (OpExtend AttReco att val atts) ctx)
(Attribute att val
l :: Attribute att val) *. :: Attribute att val
-> Attribution atts -> ReqR (OpExtend AttReco att val atts)
*. (Attribution atts
r :: Attribution atts) = Attribute att val
l Attribute att val
-> Attribution atts -> ReqR (OpExtend AttReco att val atts)
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)
.*. Attribution atts
r

-- | Empty
emptyAtt :: Attribution '[]
emptyAtt :: Attribution '[]
emptyAtt = Attribution '[]
forall k k' k'' (c :: k). Rec c '[]
EmptyRec

-- ** Destructors
infixl 7 #.

(#.) ::
  ( msg ~ '[Text "looking up attribute " :<>: ShowTE l :$$:
            Text "on " :<>: ShowTE r
           ]
  , Require (OpLookup AttReco l r) msg
  )
  => Attribution r -> Label l -> ReqR (OpLookup AttReco l r)
(Attribution r
attr :: Attribution r) #. :: Attribution r -> Label l -> ReqR (OpLookup AttReco l r)
#. (Label l
l :: Label l)
  = let prctx :: Proxy
  '[ ('Text "looking up attribute " ':<>: ShowTE l)
     ':$$: ('Text "on " ':<>: ShowTE r)]
prctx = Proxy
  '[ ('Text "looking up attribute " ':<>: ShowTE l)
     ':$$: ('Text "on " ':<>: ShowTE r)]
forall k (t :: k). Proxy t
Proxy @ '[Text "looking up attribute " :<>: ShowTE l :$$:
                          Text "on " :<>: ShowTE r
                         ]
    in Proxy
  '[ ('Text "looking up attribute " ':<>: ShowTE l)
     ':$$: ('Text "on " ':<>: ShowTE r)]
-> OpLookup AttReco l r -> ReqR (OpLookup AttReco l r)
forall op (ctx :: [ErrorMessage]).
Require op ctx =>
Proxy ctx -> op -> ReqR op
req Proxy
  '[ ('Text "looking up attribute " ':<>: ShowTE l)
     ':$$: ('Text "on " ':<>: ShowTE r)]
prctx (Label l -> Attribution r -> OpLookup AttReco l r
forall k k' (l :: k) c (r :: [(k, k')]).
Label l -> Rec c r -> OpLookup c l r
OpLookup @_ @(AttReco) Label l
l Attribution r
attr)


-- * Children
-- | operations for the children

-- | datatype implementation
type ChAttsRec prd (chs :: [(Child,[(Att,Type)])])
   = Rec (ChiReco prd) chs

-- | index type
data ChiReco (prd :: Prod)

-- | Field type
type instance  WrapField (ChiReco prd) v
  = Attribution v

-- | Type level Show utilities
type instance ShowRec (ChiReco a)     = "Children Map"
type instance ShowField (ChiReco a)   = "child labelled "

-- ** Pattern synonyms

-- |since now we implement ChAttsRec as a generic record, this allows us to
--   recover pattern matching
-- pattern EmptyCh :: ChAttsRec prd '[]
-- pattern EmptyCh = EmptyRec
-- pattern ConsCh :: (LabelSet ( '( 'Chi ch prd nt, v) ': xs)) =>
--   TaggedChAttr prd ( 'Chi ch prd nt) v -> ChAttsRec prd xs
--                          -> ChAttsRec prd ( '( 'Chi ch prd nt,v) ': xs)
-- pattern ConsCh h t = ConsRec h t

-- | Attributions tagged by a child
type TaggedChAttr prd = TagField (ChiReco prd)
pattern TaggedChAttr :: Label l -> WrapField (ChiReco prd) v
                     -> TaggedChAttr prd l v
pattern $bTaggedChAttr :: Label l -> WrapField (ChiReco prd) v -> TaggedChAttr prd l v
$mTaggedChAttr :: forall r k' k'' (l :: k') (prd :: Prod) (v :: k'').
TaggedChAttr prd l v
-> (Label l -> WrapField (ChiReco prd) v -> r) -> (Void# -> r) -> r
TaggedChAttr l v
  = TagField (Label :: Label (ChiReco prd)) l v


-- ** Constructors
-- | Pretty constructor for tagging a child
infixr 4 .=
(.=) :: Label l -> WrapField (ChiReco prd) v -> TaggedChAttr prd l v
.= :: Label l -> WrapField (ChiReco prd) v -> TaggedChAttr prd l v
(.=) = Label l -> WrapField (ChiReco prd) v -> TaggedChAttr prd l v
forall k' k'' (l :: k') (prd :: Prod) (v :: k'').
Label l -> WrapField (ChiReco prd) v -> TaggedChAttr prd l v
TaggedChAttr

-- | Pretty constructors
infixr 2 .*
(TaggedChAttr prd ch attrib
tch :: TaggedChAttr prd ch attrib) .* :: TaggedChAttr prd ch attrib
-> ChAttsRec prd attribs
-> ReqR (OpExtend (ChiReco prd) ch attrib attribs)
.* (ChAttsRec prd attribs
chs :: ChAttsRec prd attribs) = TaggedChAttr prd ch attrib
tch TaggedChAttr prd ch attrib
-> ChAttsRec prd attribs
-> ReqR (OpExtend (ChiReco prd) ch attrib attribs)
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)
.*. ChAttsRec prd attribs
chs
-- TODO: error instances if different prds are used?

-- | empty
emptyCh :: ChAttsRec prd '[]
emptyCh :: ChAttsRec prd '[]
emptyCh = ChAttsRec prd '[]
forall k k' k'' (c :: k). Rec c '[]
EmptyRec

-- ** Destructors
unTaggedChAttr :: TaggedChAttr prd l v -> WrapField (ChiReco prd) v
unTaggedChAttr :: TaggedChAttr prd l v -> WrapField (ChiReco prd) v
unTaggedChAttr (TaggedChAttr Label l
_ WrapField (ChiReco prd) v
a) = WrapField (ChiReco prd) v
a

labelChAttr :: TaggedChAttr prd l a -> Label l
labelChAttr :: TaggedChAttr prd l a -> Label l
labelChAttr TaggedChAttr prd l a
_ = Label l
forall k (l :: k). Label l
Label

infixl 8 .#
(.#) ::
  (  c ~ ('Chi ch prd nt)
  ,  ctx ~ '[Text "looking up " :<>: ShowTE c :$$:
            Text "on " :<>: ShowTE r :$$:
            Text "producion: " :<>: ShowTE prd
           ]
  , Require (OpLookup (ChiReco prd) c r) ctx
  ) =>
     Rec (ChiReco prd) r -> Label c -> ReqR (OpLookup (ChiReco prd) c r)
(Rec (ChiReco prd) r
chi :: Rec (ChiReco prd) r) .# :: Rec (ChiReco prd) r -> Label c -> ReqR (OpLookup (ChiReco prd) c r)
.# (Label c
l :: Label c)
  = let prctx :: Proxy
  '[ (('Text "looking up " ':<>: ShowTE c)
      ':$$: ('Text "on " ':<>: ShowTE r))
     ':$$: ('Text "producion: " ':<>: ShowTE prd)]
prctx = Proxy
  '[ (('Text "looking up " ':<>: ShowTE c)
      ':$$: ('Text "on " ':<>: ShowTE r))
     ':$$: ('Text "producion: " ':<>: ShowTE prd)]
forall k (t :: k). Proxy t
Proxy @ '[Text "looking up " :<>: ShowTE c :$$:
                          Text "on " :<>: ShowTE r :$$:
                          Text "producion: " :<>: ShowTE prd
                         ]
    in Proxy
  '[ (('Text "looking up "
       ':<>: 'Text
               (AppendSymbol
                  (AppendSymbol (AppendSymbol "Child " ch) " of producion ")
                  (FromEM (ShowTE prd))))
      ':$$: ('Text "on " ':<>: ShowTE r))
     ':$$: ('Text "producion: " ':<>: ShowTE prd)]
-> OpLookup (ChiReco prd) c r -> ReqR (OpLookup (ChiReco prd) c r)
forall op (ctx :: [ErrorMessage]).
Require op ctx =>
Proxy ctx -> op -> ReqR op
req Proxy
  '[ (('Text "looking up "
       ':<>: 'Text
               (AppendSymbol
                  (AppendSymbol (AppendSymbol "Child " ch) " of producion ")
                  (FromEM (ShowTE prd))))
      ':$$: ('Text "on " ':<>: ShowTE r))
     ':$$: ('Text "producion: " ':<>: ShowTE prd)]
Proxy
  '[ (('Text "looking up " ':<>: ShowTE c)
      ':$$: ('Text "on " ':<>: ShowTE r))
     ':$$: ('Text "producion: " ':<>: ShowTE prd)]
prctx (Label c -> Rec (ChiReco prd) r -> OpLookup (ChiReco prd) c r
forall k k' (l :: k) c (r :: [(k, k')]).
Label l -> Rec c r -> OpLookup c l r
OpLookup @_ @(ChiReco prd) Label c
l Rec (ChiReco prd) r
chi)



-- * Productions

data PrdReco

type instance  WrapField PrdReco (rule :: Type)
  = rule

type Aspect (asp :: [(Prod, Type)]) = Rec PrdReco asp
type instance ShowRec PrdReco       = "Aspect"
type instance ShowField PrdReco     = "production named "