{-|
Module      : Language.Grammars.AspectAG
Description : Main module, First-class attribute grammars
Copyright   : (c) Juan García-Garland, Marcos Viera, 2019, 2020
License     : GPL
Maintainer  : jpgarcia@fing.edu.uy
Stability   : experimental
Portability : POSIX
-}

{-# LANGUAGE PolyKinds                 #-}
{-# LANGUAGE KindSignatures            #-}
{-# LANGUAGE DataKinds                 #-}
{-# LANGUAGE ConstraintKinds           #-}
{-# LANGUAGE RankNTypes                #-}
{-# LANGUAGE TypeOperators             #-}
{-# LANGUAGE FlexibleInstances         #-}
{-# LANGUAGE FlexibleContexts          #-}
{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE UndecidableInstances      #-}
{-# LANGUAGE MultiParamTypeClasses     #-}
{-# LANGUAGE TypeFamilies              #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE ScopedTypeVariables       #-}
{-# LANGUAGE TypeFamilies              #-}
{-# LANGUAGE TypeApplications          #-}
{-# LANGUAGE FunctionalDependencies    #-}
{-# LANGUAGE TypeFamilyDependencies    #-}
{-# LANGUAGE PartialTypeSignatures     #-}
{-# LANGUAGE IncoherentInstances       #-}
{-# LANGUAGE AllowAmbiguousTypes       #-}
{-# LANGUAGE UnicodeSyntax             #-}
{-# LANGUAGE ImpredicativeTypes        #-}

module Language.Grammars.AspectAG
  (

    -- * Rules
    Rule, CRule(..),
    Fam,
    chi, par,
    
    -- ** Defining Rules
    syndef, syndefM, syn, -- syndefC,
    
    synmod, synmodM, -- synP,

    inh,
    inhdef, inhdefM,

    inhmod, inhmodM, 

    emptyRule,
    emptyRuleAtPrd,
    emptyRuleInst,
    ext, (.+.), extP,
    
    -- * Aspects 
    -- ** Building Aspects.
    
    emptyAspect,
    singAsp,
    extAspect,
    comAspect,
    (.+:),(◃),
    (.:+.),(▹),
    (.:+:),(⋈),
    (.#..), 
    
    CAspect(..),
    Label(Label), Prod(..), T(..), NT(..), Child(..), Att(..),
    (.#), (#.), (=.), (.=), (.*), (*.),
    emptyAtt,
    ter,
    at, lhs,
    sem_Lit,
    knitAspect,
    knit,
    traceAspect,
    traceRule,
    copyAtChi,
    -- use,
    emptyAspectC,
    emptyAspectForProds,
    module Data.GenRec,
    module Language.Grammars.AspectAG.HList,
    Terminal,
    NonTerminal,

    (+++),
    empties
  )
  where


import Language.Grammars.AspectAG.HList
import Language.Grammars.AspectAG.RecordInstances


import Data.Type.Require hiding (emptyCtx)

import Data.GenRec
import Data.GenRec.Label

import Data.Kind
import Data.Proxy
import GHC.TypeLits

import Data.Maybe
import Data.Type.Equality
import Control.Monad.Reader
import Data.Functor.Identity
import GHC.Types

import Debug.Trace.LocationTH

infixr 3 &&
type family (a :: Bool) && (b :: Bool) where
  True && True = True
  _ && _ = False

class SemLit a where
  sem_Lit :: a -> Attribution ('[] :: [(Att,Type)])
               -> Attribution '[ '( 'Att "term" a , a)]
  lit     :: Label ('Att "term" a)
instance SemLit a where
  sem_Lit :: a -> Attribution '[] -> Attribution '[ '( 'Att "term" a, a)]
sem_Lit a
a Attribution '[]
_ = (Label ('Att "term" a)
forall k (l :: k). Label l
Label Label ('Att "term" a) -> a -> Attribute ('Att "term" a) a
forall (l :: Att) v. Label l -> v -> Attribute l v
=. a
a) Attribute ('Att "term" a) a
-> Attribution '[] -> ReqR (OpExtend AttReco ('Att "term" a) a '[])
forall (att :: Att) val (atts :: [(Att, *)]).
Require (OpExtend AttReco att val atts) '[ 'Text ""] =>
Attribute att val
-> Attribution atts -> ReqR (OpExtend AttReco att val atts)
*. Attribution '[]
emptyAtt
  lit :: Label ('Att "term" a)
lit         = Label ('Att "term" a)
forall k (l :: k). Label l
Label @ ('Att "term" a)


-- * Families and Rules

-- | In each node of the grammar, the "Fam" contains a single attribution
-- for the parent, and a collection (Record) of attributions for
-- the children:
data Fam (prd :: Prod)
         (c :: [(Child, [(Att, Type)])])
         (p :: [(Att, Type)]) :: Type
 where
  Fam :: ChAttsRec prd c -> Attribution p -> Fam prd c p


-- | getter
chi :: Fam prd c p -> ChAttsRec prd c
chi :: Fam prd c p -> ChAttsRec prd c
chi (Fam ChAttsRec prd c
c Attribution p
p) = ChAttsRec prd c
c

-- | getter
par :: Fam prd c p -> Attribution p
par :: Fam prd c p -> Attribution p
par (Fam ChAttsRec prd c
c Attribution p
p) = Attribution p
p

-- | getter (extracts a 'Label')
prd :: Fam prd c p -> Label prd
prd :: Fam prd c p -> Label prd
prd (Fam ChAttsRec prd c
c Attribution p
p) = Label prd
forall k (l :: k). Label l
Label

-- | Rules are a function from the input family to the output family,
-- with an extra arity to make them composable.  They are indexed by a production.
type Rule
  (prd  :: Prod)
  (sc   :: [(Child, [(Att, Type)])])
  (ip   :: [(Att,       Type)])
  (ic   :: [(Child, [(Att, Type)])])
  (sp   :: [(Att,       Type)])
  (ic'  :: [(Child, [(Att, Type)])])
  (sp'  :: [(Att,       Type)])
  = Fam prd sc ip -> Fam prd ic sp -> Fam prd ic' sp'

-- | Rules with context (used to print domain specific type errors).
newtype CRule (ctx :: [ErrorMessage]) prd sc ip ic sp ic' sp'
  = CRule { CRule ctx prd sc ip ic sp ic' sp'
-> Proxy ctx -> Rule prd sc ip ic sp ic' sp'
mkRule :: (Proxy ctx -> Rule prd sc ip ic sp ic' sp')}

emptyRule :: CRule ctx prd sc ip ic' sp' ic' sp'
emptyRule =
  (Proxy ctx -> Rule prd sc ip ic' sp' ic' sp')
-> CRule ctx prd sc ip ic' sp' ic' sp'
forall (ctx :: [ErrorMessage]) (prd :: Prod)
       (sc :: [(Child, [(Att, *)])]) (ip :: [(Att, *)])
       (ic :: [(Child, [(Att, *)])]) (sp :: [(Att, *)])
       (ic' :: [(Child, [(Att, *)])]) (sp' :: [(Att, *)]).
(Proxy ctx -> Rule prd sc ip ic sp ic' sp')
-> CRule ctx prd sc ip ic sp ic' sp'
CRule ((Proxy ctx -> Rule prd sc ip ic' sp' ic' sp')
 -> CRule ctx prd sc ip ic' sp' ic' sp')
-> (Proxy ctx -> Rule prd sc ip ic' sp' ic' sp')
-> CRule ctx prd sc ip ic' sp' ic' sp'
forall a b. (a -> b) -> a -> b
$ \Proxy ctx
Proxy -> \Fam prd sc ip
fam Fam prd ic' sp'
inp -> Fam prd ic' sp'
inp

emptyRuleInst :: KList sc -> CRule ctx prd sc ip ic sp ic sp
emptyRuleInst :: KList sc -> CRule ctx prd sc ip ic sp ic sp
emptyRuleInst KList sc
_ =
  (Proxy ctx -> Rule prd sc ip ic sp ic sp)
-> CRule ctx prd sc ip ic sp ic sp
forall (ctx :: [ErrorMessage]) (prd :: Prod)
       (sc :: [(Child, [(Att, *)])]) (ip :: [(Att, *)])
       (ic :: [(Child, [(Att, *)])]) (sp :: [(Att, *)])
       (ic' :: [(Child, [(Att, *)])]) (sp' :: [(Att, *)]).
(Proxy ctx -> Rule prd sc ip ic sp ic' sp')
-> CRule ctx prd sc ip ic sp ic' sp'
CRule ((Proxy ctx -> Rule prd sc ip ic sp ic sp)
 -> CRule ctx prd sc ip ic sp ic sp)
-> (Proxy ctx -> Rule prd sc ip ic sp ic sp)
-> CRule ctx prd sc ip ic sp ic sp
forall a b. (a -> b) -> a -> b
$ \Proxy ctx
Proxy -> \Fam prd sc ip
fam ->
    case Fam prd sc ip
fam of
      Fam ChAttsRec prd sc
_ Attribution ip
_ -> \Fam prd ic sp
fam -> Fam prd ic sp
fam

emptyRuleAtPrd :: Label prd -> CRule ctx prd sc ip ic' sp' ic' sp'
emptyRuleAtPrd :: Label prd -> CRule ctx prd sc ip ic' sp' ic' sp'
emptyRuleAtPrd Label prd
Label = CRule ctx prd sc ip ic' sp' ic' sp'
forall (ctx :: [ErrorMessage]) (prd :: Prod)
       (sc :: [(Child, [(Att, *)])]) (ip :: [(Att, *)])
       (ic' :: [(Child, [(Att, *)])]) (sp' :: [(Att, *)]).
CRule ctx prd sc ip ic' sp' ic' sp'
emptyRule

-- | Aspects, tagged with context. 'Aspect' is a record instance having
-- productions as labels, containing 'Rule's as fields.
newtype CAspect (ctx :: [ErrorMessage]) (asp :: [(Prod, Type)] )
  = CAspect { CAspect ctx asp -> Proxy ctx -> Aspect asp
mkAspect :: Proxy ctx -> Aspect asp}

-- | Recall that Aspects are mappings from productions to rules. They
-- have a record-like interface to build them. This is the constructor
-- for the empty Aspect.
emptyAspect :: CAspect ctx '[]
emptyAspect :: CAspect ctx '[]
emptyAspect  = (Proxy ctx -> Aspect '[]) -> CAspect ctx '[]
forall (ctx :: [ErrorMessage]) (asp :: [(Prod, *)]).
(Proxy ctx -> Aspect asp) -> CAspect ctx asp
CAspect ((Proxy ctx -> Aspect '[]) -> CAspect ctx '[])
-> (Proxy ctx -> Aspect '[]) -> CAspect ctx '[]
forall a b. (a -> b) -> a -> b
$ Aspect '[] -> Proxy ctx -> Aspect '[]
forall a b. a -> b -> a
const Aspect '[]
forall k k' k'' (c :: k). Rec c '[]
EmptyRec

-- | combination of two Aspects. It merges them. When both aspects
-- have rules for a given production, in the resulting Aspect the rule
-- at that field is the combination of the rules for the arguments
-- (with 'ext').
comAspect ::
  ( Require (OpComAsp al ar) ctx
  , ReqR (OpComAsp al ar) ~ Aspect asp
  )
  =>  CAspect ctx al -> CAspect ctx ar -> CAspect ctx asp
comAspect :: CAspect ctx al -> CAspect ctx ar -> CAspect ctx asp
comAspect CAspect ctx al
al CAspect ctx ar
ar
  = (Proxy ctx -> Aspect asp) -> CAspect ctx asp
forall (ctx :: [ErrorMessage]) (asp :: [(Prod, *)]).
(Proxy ctx -> Aspect asp) -> CAspect ctx asp
CAspect ((Proxy ctx -> Aspect asp) -> CAspect ctx asp)
-> (Proxy ctx -> Aspect asp) -> CAspect ctx asp
forall a b. (a -> b) -> a -> b
$ \Proxy ctx
ctx -> Proxy ctx -> OpComAsp al ar -> ReqR (OpComAsp al ar)
forall op (ctx :: [ErrorMessage]).
Require op ctx =>
Proxy ctx -> op -> ReqR op
req Proxy ctx
ctx (Aspect al -> Aspect ar -> OpComAsp al ar
forall (al :: [(Prod, *)]) (ar :: [(Prod, *)]).
Aspect al -> Aspect ar -> OpComAsp al ar
OpComAsp (CAspect ctx al -> Proxy ctx -> Aspect al
forall (ctx :: [ErrorMessage]) (asp :: [(Prod, *)]).
CAspect ctx asp -> Proxy ctx -> Aspect asp
mkAspect CAspect ctx al
al Proxy ctx
ctx) (CAspect ctx ar -> Proxy ctx -> Aspect ar
forall (ctx :: [ErrorMessage]) (asp :: [(Prod, *)]).
CAspect ctx asp -> Proxy ctx -> Aspect asp
mkAspect CAspect ctx ar
ar Proxy ctx
ctx))


-- * Trace utils

-- | |traceAspect| adds context to an aspect.
traceAspect :: Proxy e
-> CAspect (('Text "- traceAspect: " ':<>: e) : ctx) r
-> CAspect
     ctx (ResMapCtx r ctx (('Text "- traceAspect: " ':<>: e) : ctx))
traceAspect (Proxy e
_ :: Proxy (e::ErrorMessage))
  = (Proxy ctx -> Proxy (('Text "- traceAspect: " ':<>: e) : ctx))
-> CAspect (('Text "- traceAspect: " ':<>: e) : ctx) r
-> CAspect
     ctx (ResMapCtx r ctx (('Text "- traceAspect: " ':<>: e) : ctx))
forall (r :: [(Prod, *)]) (ctx :: [ErrorMessage])
       (ctx :: [ErrorMessage]).
MapCtxAsp r ctx ctx =>
(Proxy ctx -> Proxy ctx)
-> CAspect ctx r -> CAspect ctx (ResMapCtx r ctx ctx)
mapCAspect ((Proxy ctx -> Proxy (('Text "- traceAspect: " ':<>: e) : ctx))
 -> CAspect (('Text "- traceAspect: " ':<>: e) : ctx) r
 -> CAspect
      ctx (ResMapCtx r ctx (('Text "- traceAspect: " ':<>: e) : ctx)))
-> (Proxy ctx -> Proxy (('Text "- traceAspect: " ':<>: e) : ctx))
-> CAspect (('Text "- traceAspect: " ':<>: e) : ctx) r
-> CAspect
     ctx (ResMapCtx r ctx (('Text "- traceAspect: " ':<>: e) : ctx))
forall a b. (a -> b) -> a -> b
$ \(Proxy ctx
_ :: Proxy ctx) ->
                   Proxy (('Text "- traceAspect: " ':<>: e) : ctx)
forall k (t :: k). Proxy t
Proxy @ ((Text "- traceAspect: " :<>: e) : ctx)

traceRule :: Proxy e
-> CRule
     (('Text "- traceRule: " ':<>: e) : ctx) prd sc ip ic sp ic' sp'
-> CRule ctx prd sc ip ic sp ic' sp'
traceRule (Proxy e
_ :: Proxy (e::ErrorMessage))
  = (Proxy ctx -> Proxy (('Text "- traceRule: " ':<>: e) : ctx))
-> CRule
     (('Text "- traceRule: " ':<>: e) : ctx) prd sc ip ic sp ic' sp'
-> CRule ctx prd sc ip ic sp ic' sp'
forall (ctx :: [ErrorMessage]) (ctx' :: [ErrorMessage])
       (prd :: Prod) (sc :: [(Child, [(Att, *)])]) (ip :: [(Att, *)])
       (ic :: [(Child, [(Att, *)])]) (sp :: [(Att, *)])
       (ic' :: [(Child, [(Att, *)])]) (sp' :: [(Att, *)]).
(Proxy ctx -> Proxy ctx')
-> CRule ctx' prd sc ip ic sp ic' sp'
-> CRule ctx prd sc ip ic sp ic' sp'
mapCRule ((Proxy ctx -> Proxy (('Text "- traceRule: " ':<>: e) : ctx))
 -> CRule
      (('Text "- traceRule: " ':<>: e) : ctx) prd sc ip ic sp ic' sp'
 -> CRule ctx prd sc ip ic sp ic' sp')
-> (Proxy ctx -> Proxy (('Text "- traceRule: " ':<>: e) : ctx))
-> CRule
     (('Text "- traceRule: " ':<>: e) : ctx) prd sc ip ic sp ic' sp'
-> CRule ctx prd sc ip ic sp ic' sp'
forall a b. (a -> b) -> a -> b
$ \(Proxy ctx
_ :: Proxy ctx) ->
                 Proxy (('Text "- traceRule: " ':<>: e) : ctx)
forall k (t :: k). Proxy t
Proxy @ (Text "- traceRule: " :<>: e : ctx)


mapCRule :: (Proxy ctx -> Proxy ctx')
          -> CRule ctx' prd sc ip ic sp ic' sp'
          -> CRule ctx  prd sc ip ic sp ic' sp'
mapCRule :: (Proxy ctx -> Proxy ctx')
-> CRule ctx' prd sc ip ic sp ic' sp'
-> CRule ctx prd sc ip ic sp ic' sp'
mapCRule Proxy ctx -> Proxy ctx'
fctx (CRule Proxy ctx' -> Rule prd sc ip ic sp ic' sp'
frule) = (Proxy ctx -> Rule prd sc ip ic sp ic' sp')
-> CRule ctx prd sc ip ic sp ic' sp'
forall (ctx :: [ErrorMessage]) (prd :: Prod)
       (sc :: [(Child, [(Att, *)])]) (ip :: [(Att, *)])
       (ic :: [(Child, [(Att, *)])]) (sp :: [(Att, *)])
       (ic' :: [(Child, [(Att, *)])]) (sp' :: [(Att, *)]).
(Proxy ctx -> Rule prd sc ip ic sp ic' sp')
-> CRule ctx prd sc ip ic sp ic' sp'
CRule ((Proxy ctx -> Rule prd sc ip ic sp ic' sp')
 -> CRule ctx prd sc ip ic sp ic' sp')
-> (Proxy ctx -> Rule prd sc ip ic sp ic' sp')
-> CRule ctx prd sc ip ic sp ic' sp'
forall a b. (a -> b) -> a -> b
$ Proxy ctx' -> Rule prd sc ip ic sp ic' sp'
frule (Proxy ctx' -> Rule prd sc ip ic sp ic' sp')
-> (Proxy ctx -> Proxy ctx')
-> Proxy ctx
-> Rule prd sc ip ic sp ic' sp'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy ctx -> Proxy ctx'
fctx

mapCAspect :: (Proxy ctx -> Proxy ctx)
-> CAspect ctx r -> CAspect ctx (ResMapCtx r ctx ctx)
mapCAspect Proxy ctx -> Proxy ctx
fctx (CAspect Proxy ctx -> Aspect r
fasp) = (Proxy ctx -> Aspect (ResMapCtx r ctx ctx))
-> CAspect ctx (ResMapCtx r ctx ctx)
forall (ctx :: [ErrorMessage]) (asp :: [(Prod, *)]).
(Proxy ctx -> Aspect asp) -> CAspect ctx asp
CAspect ((Proxy ctx -> Aspect (ResMapCtx r ctx ctx))
 -> CAspect ctx (ResMapCtx r ctx ctx))
-> (Proxy ctx -> Aspect (ResMapCtx r ctx ctx))
-> CAspect ctx (ResMapCtx r ctx ctx)
forall a b. (a -> b) -> a -> b
$
       (Proxy ctx -> Proxy ctx)
-> Aspect r -> Aspect (ResMapCtx r ctx ctx)
forall (r :: [(Prod, *)]) (ctx :: [ErrorMessage])
       (ctx' :: [ErrorMessage]).
MapCtxAsp r ctx ctx' =>
(Proxy ctx -> Proxy ctx')
-> Aspect r -> Aspect (ResMapCtx r ctx ctx')
mapCtxRec Proxy ctx -> Proxy ctx
fctx (Aspect r -> Aspect (ResMapCtx r ctx ctx))
-> (Proxy ctx -> Aspect r)
-> Proxy ctx
-> Aspect (ResMapCtx r ctx ctx)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy ctx -> Aspect r
fasp (Proxy ctx -> Aspect r)
-> (Proxy ctx -> Proxy ctx) -> Proxy ctx -> Aspect r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy ctx -> Proxy ctx
fctx

class MapCtxAsp (r :: [(Prod,Type)]) (ctx :: [ErrorMessage])
                                     (ctx' :: [ErrorMessage])  where
  type ResMapCtx r ctx ctx' :: [(Prod,Type)]
  mapCtxRec :: (Proxy ctx -> Proxy ctx')
            -> Aspect r -> Aspect (ResMapCtx r ctx ctx')

instance
  ( MapCtxAsp r ctx ctx' 
  , ResMapCtx r ctx ctx' ~ r'
  )
  =>
  MapCtxAsp ( '(l, CRule ctx' prd sc ip ic sp ic' sp') ': r) ctx ctx' where
  type ResMapCtx ( '(l, CRule ctx' prd sc ip ic sp ic' sp') ': r) ctx ctx'
     =  '(l, CRule ctx prd sc ip ic sp ic' sp') ':  ResMapCtx r ctx ctx'
  mapCtxRec :: (Proxy ctx -> Proxy ctx')
-> Aspect ('(l, CRule ctx' prd sc ip ic sp ic' sp') : r)
-> Aspect
     (ResMapCtx ('(l, CRule ctx' prd sc ip ic sp ic' sp') : r) ctx ctx')
mapCtxRec Proxy ctx -> Proxy ctx'
fctx (ConsRec (TagField Label PrdReco
c Label l
l WrapField PrdReco v
r) Rec PrdReco r1
rs) = (TagField PrdReco l (CRule ctx prd sc ip ic sp ic' sp')
-> Rec PrdReco r'
-> Rec PrdReco ('(l, CRule ctx prd sc ip ic sp ic' sp') : r')
forall k k' k'' (c :: k) (l :: k') (v :: k'') (r1 :: [(k', k'')]).
TagField c l v -> Rec c r1 -> Rec c ('(l, v) : r1)
ConsRec (Label PrdReco
-> Label l
-> WrapField PrdReco (CRule ctx prd sc ip ic sp ic' sp')
-> TagField PrdReco l (CRule ctx prd sc ip ic sp ic' sp')
forall k k' k'' (c :: k) (l :: k') (v :: k'').
Label c -> Label l -> WrapField c v -> TagField c l v
TagField Label PrdReco
c Label l
l
                                                            ((Proxy ctx -> Proxy ctx')
-> CRule ctx' prd sc ip ic sp ic' sp'
-> CRule ctx prd sc ip ic sp ic' sp'
forall (ctx :: [ErrorMessage]) (ctx' :: [ErrorMessage])
       (prd :: Prod) (sc :: [(Child, [(Att, *)])]) (ip :: [(Att, *)])
       (ic :: [(Child, [(Att, *)])]) (sp :: [(Att, *)])
       (ic' :: [(Child, [(Att, *)])]) (sp' :: [(Att, *)]).
(Proxy ctx -> Proxy ctx')
-> CRule ctx' prd sc ip ic sp ic' sp'
-> CRule ctx prd sc ip ic sp ic' sp'
mapCRule Proxy ctx -> Proxy ctx'
fctx WrapField PrdReco v
CRule ctx' prd sc ip ic sp ic' sp'
r))
                                                          ((Proxy ctx -> Proxy ctx')
-> Rec PrdReco r1 -> Aspect (ResMapCtx r1 ctx ctx')
forall (r :: [(Prod, *)]) (ctx :: [ErrorMessage])
       (ctx' :: [ErrorMessage]).
MapCtxAsp r ctx ctx' =>
(Proxy ctx -> Proxy ctx')
-> Aspect r -> Aspect (ResMapCtx r ctx ctx')
mapCtxRec Proxy ctx -> Proxy ctx'
fctx Rec PrdReco r1
rs))

instance MapCtxAsp ('[] :: [(Prod,Type)]) ctx ctx' where
  type ResMapCtx ('[] :: [(Prod,Type)]) ctx ctx'
     =  '[]
  mapCtxRec :: (Proxy ctx -> Proxy ctx')
-> Aspect '[] -> Aspect (ResMapCtx '[] ctx ctx')
mapCtxRec Proxy ctx -> Proxy ctx'
_ Aspect '[]
EmptyRec = Aspect (ResMapCtx '[] ctx ctx')
forall k k' k'' (c :: k). Rec c '[]
EmptyRec


-- | The "cons" for 'CAspect's. It adds a 'Rule' `rule`
-- to a 'CAspect'. If there is no rule for that production in the
-- argument it is a record extension. If the production is there, the
-- rules are combined.
extAspect
  :: ExtAspect ctx prd sc ip ic sp ic' sp' a asp =>
     CRule ctx prd sc ip ic sp ic' sp'
     -> CAspect ctx a -> CAspect ctx asp
extAspect :: CRule ctx prd sc ip ic sp ic' sp'
-> CAspect ctx a -> CAspect ctx asp
extAspect CRule ctx prd sc ip ic sp ic' sp'
rule (CAspect Proxy ctx -> Aspect a
fasp)
  = (Proxy ctx -> Aspect asp) -> CAspect ctx asp
forall (ctx :: [ErrorMessage]) (asp :: [(Prod, *)]).
(Proxy ctx -> Aspect asp) -> CAspect ctx asp
CAspect ((Proxy ctx -> Aspect asp) -> CAspect ctx asp)
-> (Proxy ctx -> Aspect asp) -> CAspect ctx asp
forall a b. (a -> b) -> a -> b
$ \Proxy ctx
ctx -> Proxy ctx
-> OpComRA ctx prd (CRule ctx prd sc ip ic sp ic' sp') a
-> ReqR (OpComRA ctx prd (CRule ctx prd sc ip ic sp ic' sp') a)
forall op (ctx :: [ErrorMessage]).
Require op ctx =>
Proxy ctx -> op -> ReqR op
req Proxy ctx
ctx (CRule ctx prd sc ip ic sp ic' sp'
-> Aspect a
-> OpComRA ctx prd (CRule ctx prd sc ip ic sp ic' sp') a
forall (ctx :: [ErrorMessage]) (prd :: Prod)
       (sc :: [(Child, [(Att, *)])]) (ip :: [(Att, *)])
       (ic :: [(Child, [(Att, *)])]) (sp :: [(Att, *)])
       (ic' :: [(Child, [(Att, *)])]) (sp' :: [(Att, *)])
       (a :: [(Prod, *)]).
CRule ctx prd sc ip ic sp ic' sp'
-> Aspect a
-> OpComRA ctx prd (CRule ctx prd sc ip ic sp ic' sp') a
OpComRA CRule ctx prd sc ip ic sp ic' sp'
rule (Proxy ctx -> Aspect a
fasp Proxy ctx
ctx))

type ExtAspect ctx prd sc ip ic sp ic' sp' a asp
  = (Require
        (OpComRA ctx prd (CRule ctx prd sc ip ic sp ic' sp') a) ctx,
      ReqR (OpComRA ctx prd (CRule ctx prd sc ip ic sp ic' sp') a)
      ~ Rec PrdReco asp) 

-- | An operator, alias for 'extAspect'. It combines a rule with an
-- aspect, to build a bigger one.
.+: :: CRule ctx prd sc ip ic sp ic' sp'
-> CAspect ctx a -> CAspect ctx asp
(.+:) = CRule ctx prd sc ip ic sp ic' sp'
-> CAspect ctx a -> CAspect ctx asp
forall (ctx :: [ErrorMessage]) (prd :: Prod)
       (sc :: [(Child, [(Att, *)])]) (ip :: [(Att, *)])
       (ic :: [(Child, [(Att, *)])]) (sp :: [(Att, *)])
       (ic' :: [(Child, [(Att, *)])]) (sp' :: [(Att, *)])
       (a :: [(Prod, *)]) (asp :: [(Prod, *)]).
ExtAspect ctx prd sc ip ic sp ic' sp' a asp =>
CRule ctx prd sc ip ic sp ic' sp'
-> CAspect ctx a -> CAspect ctx asp
extAspect
infixr 3 .+:

-- | Unicode version of 'extAspect' or '.+:' (\\triangleleft)
◃ :: CRule ctx prd sc ip ic sp ic' sp'
-> CAspect ctx a -> CAspect ctx asp
(◃) = CRule ctx prd sc ip ic sp ic' sp'
-> CAspect ctx a -> CAspect ctx asp
forall (ctx :: [ErrorMessage]) (prd :: Prod)
       (sc :: [(Child, [(Att, *)])]) (ip :: [(Att, *)])
       (ic :: [(Child, [(Att, *)])]) (sp :: [(Att, *)])
       (ic' :: [(Child, [(Att, *)])]) (sp' :: [(Att, *)])
       (a :: [(Prod, *)]) (asp :: [(Prod, *)]).
ExtAspect ctx prd sc ip ic sp ic' sp' a asp =>
CRule ctx prd sc ip ic sp ic' sp'
-> CAspect ctx a -> CAspect ctx asp
extAspect
infixr 3 ◃

-- | The other way, combines an aspect with a rule. It is a `flip`ped
-- 'extAspect'.
.:+. :: CAspect ctx a
-> CRule ctx prd sc ip ic sp ic' sp' -> CAspect ctx asp
(.:+.) = (CRule ctx prd sc ip ic sp ic' sp'
 -> CAspect ctx a -> CAspect ctx asp)
-> CAspect ctx a
-> CRule ctx prd sc ip ic sp ic' sp'
-> CAspect ctx asp
forall a b c. (a -> b -> c) -> b -> a -> c
flip CRule ctx prd sc ip ic sp ic' sp'
-> CAspect ctx a -> CAspect ctx asp
forall (ctx :: [ErrorMessage]) (prd :: Prod)
       (sc :: [(Child, [(Att, *)])]) (ip :: [(Att, *)])
       (ic :: [(Child, [(Att, *)])]) (sp :: [(Att, *)])
       (ic' :: [(Child, [(Att, *)])]) (sp' :: [(Att, *)])
       (a :: [(Prod, *)]) (asp :: [(Prod, *)]).
ExtAspect ctx prd sc ip ic sp ic' sp' a asp =>
CRule ctx prd sc ip ic sp ic' sp'
-> CAspect ctx a -> CAspect ctx asp
extAspect
infixl 3 .:+.

-- | Unicode operator for '.:+.' or `flip extAspect`.
▹ :: CAspect ctx a
-> CRule ctx prd sc ip ic sp ic' sp' -> CAspect ctx asp
(▹) = (CRule ctx prd sc ip ic sp ic' sp'
 -> CAspect ctx a -> CAspect ctx asp)
-> CAspect ctx a
-> CRule ctx prd sc ip ic sp ic' sp'
-> CAspect ctx asp
forall a b c. (a -> b -> c) -> b -> a -> c
flip CRule ctx prd sc ip ic sp ic' sp'
-> CAspect ctx a -> CAspect ctx asp
forall (ctx :: [ErrorMessage]) (prd :: Prod)
       (sc :: [(Child, [(Att, *)])]) (ip :: [(Att, *)])
       (ic :: [(Child, [(Att, *)])]) (sp :: [(Att, *)])
       (ic' :: [(Child, [(Att, *)])]) (sp' :: [(Att, *)])
       (a :: [(Prod, *)]) (asp :: [(Prod, *)]).
ExtAspect ctx prd sc ip ic sp ic' sp' a asp =>
CRule ctx prd sc ip ic sp ic' sp'
-> CAspect ctx a -> CAspect ctx asp
extAspect
infixl 3 ▹


-- | Operator for 'comAspect'. It takes two 'CAspect's to build the
-- combination of both.
.:+: :: CAspect ctx al -> CAspect ctx ar -> CAspect ctx asp
(.:+:) = CAspect ctx al -> CAspect ctx ar -> CAspect ctx asp
forall (al :: [(Prod, *)]) (ar :: [(Prod, *)])
       (ctx :: [ErrorMessage]) (asp :: [(Prod, *)]).
(Require (OpComAsp al ar) ctx,
 ReqR (OpComAsp al ar) ~ Aspect asp) =>
CAspect ctx al -> CAspect ctx ar -> CAspect ctx asp
comAspect
infixr 4 .:+:

-- | Unicode operator for 'comAspect' or '.:+:'. (\\bowtie)
⋈ :: CAspect ctx al -> CAspect ctx ar -> CAspect ctx asp
(⋈) = CAspect ctx al -> CAspect ctx ar -> CAspect ctx asp
forall (al :: [(Prod, *)]) (ar :: [(Prod, *)])
       (ctx :: [ErrorMessage]) (asp :: [(Prod, *)]).
(Require (OpComAsp al ar) ctx,
 ReqR (OpComAsp al ar) ~ Aspect asp) =>
CAspect ctx al -> CAspect ctx ar -> CAspect ctx asp
comAspect
infixr 4 ⋈

ext' ::  RequireEq prd prd' (Text "ext":ctx) =>
         CRule ctx prd sc ip ic sp ic' sp'
     ->  CRule ctx prd' sc ip a b ic sp
     ->  CRule ctx prd sc ip a b ic' sp'
(CRule Proxy ctx -> Rule prd sc ip ic sp ic' sp'
f) ext' :: CRule ctx prd sc ip ic sp ic' sp'
-> CRule ctx prd' sc ip a b ic sp
-> CRule ctx prd sc ip a b ic' sp'
`ext'` (CRule Proxy ctx -> Rule prd' sc ip a b ic sp
g)
 = (Proxy ctx -> Rule prd sc ip a b ic' sp')
-> CRule ctx prd sc ip a b ic' sp'
forall (ctx :: [ErrorMessage]) (prd :: Prod)
       (sc :: [(Child, [(Att, *)])]) (ip :: [(Att, *)])
       (ic :: [(Child, [(Att, *)])]) (sp :: [(Att, *)])
       (ic' :: [(Child, [(Att, *)])]) (sp' :: [(Att, *)]).
(Proxy ctx -> Rule prd sc ip ic sp ic' sp')
-> CRule ctx prd sc ip ic sp ic' sp'
CRule ((Proxy ctx -> Rule prd sc ip a b ic' sp')
 -> CRule ctx prd sc ip a b ic' sp')
-> (Proxy ctx -> Rule prd sc ip a b ic' sp')
-> CRule ctx prd sc ip a b ic' sp'
forall a b. (a -> b) -> a -> b
$ \Proxy ctx
ctx Fam prd sc ip
input -> Proxy ctx -> Rule prd sc ip ic sp ic' sp'
f Proxy ctx
ctx Fam prd sc ip
input (Fam prd ic sp -> Fam prd ic' sp')
-> (Fam prd' a b -> Fam prd ic sp)
-> Fam prd' a b
-> Fam prd ic' sp'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy ctx -> Rule prd' sc ip a b ic sp
g Proxy ctx
ctx Fam prd sc ip
Fam prd' sc ip
input

type PCRule p ctx prd sc ip ic sp ic' sp'
  = Reader p (CRule ctx prd sc ip ic sp ic' sp') 

-- | extension of polymorphic rules
extP :: (Proxy p -> CRule ctx prd' sc ip ic sp ic' sp')
-> (Proxy p -> CRule ctx prd' sc ip a b ic sp)
-> Proxy p
-> CRule ctx prd' sc ip a b ic' sp'
extP Proxy p -> CRule ctx prd' sc ip ic sp ic' sp'
l Proxy p -> CRule ctx prd' sc ip a b ic sp
r = \(Proxy p
p ::Proxy p) -> Proxy p -> CRule ctx prd' sc ip ic sp ic' sp'
l Proxy p
p CRule ctx prd' sc ip ic sp ic' sp'
-> CRule ctx prd' sc ip a b ic sp
-> CRule ctx prd' sc ip a b ic' sp'
forall (prd :: Prod) (prd' :: Prod) (ctx :: [ErrorMessage])
       (sc :: [(Child, [(Att, *)])]) (ip :: [(Att, *)])
       (ic :: [(Child, [(Att, *)])]) (sp :: [(Att, *)])
       (ic' :: [(Child, [(Att, *)])]) (sp' :: [(Att, *)])
       (a :: [(Child, [(Att, *)])]) (b :: [(Att, *)]).
RequireEq prd prd' ('Text "ext" : ctx) =>
CRule ctx prd sc ip ic sp ic' sp'
-> CRule ctx prd' sc ip a b ic sp
-> CRule ctx prd sc ip a b ic' sp'
`ext` Proxy p -> CRule ctx prd' sc ip a b ic sp
r Proxy p
p


-- | Given two rules for a given (the same) production, it combines
-- them. Note that the production equality is visible in the context,
-- not sintactically. This is a use of the 'Require' pattern.
ext ::   RequireEq prd prd' (Text "ext":ctx) 
     => CRule ctx prd sc ip ic sp ic' sp'
     -> CRule ctx prd' sc ip a b ic sp
     -> CRule ctx prd sc ip a b ic' sp'
ext :: CRule ctx prd sc ip ic sp ic' sp'
-> CRule ctx prd' sc ip a b ic sp
-> CRule ctx prd sc ip a b ic' sp'
ext = CRule ctx prd sc ip ic sp ic' sp'
-> CRule ctx prd' sc ip a b ic sp
-> CRule ctx prd sc ip a b ic' sp'
forall (prd :: Prod) (prd' :: Prod) (ctx :: [ErrorMessage])
       (sc :: [(Child, [(Att, *)])]) (ip :: [(Att, *)])
       (ic :: [(Child, [(Att, *)])]) (sp :: [(Att, *)])
       (ic' :: [(Child, [(Att, *)])]) (sp' :: [(Att, *)])
       (a :: [(Child, [(Att, *)])]) (b :: [(Att, *)]).
RequireEq prd prd' ('Text "ext" : ctx) =>
CRule ctx prd sc ip ic sp ic' sp'
-> CRule ctx prd' sc ip a b ic sp
-> CRule ctx prd sc ip a b ic' sp'
ext'

-- | Singleton Aspect. Wraps a rule to build an Aspect from it.
singAsp :: CRule ctx prd sc ip ic sp ic' sp'
-> CAspect ctx '[ '(prd, CRule ctx prd sc ip ic sp ic' sp')]
singAsp CRule ctx prd sc ip ic sp ic' sp'
r
  = CRule ctx prd sc ip ic sp ic' sp'
r CRule ctx prd sc ip ic sp ic' sp'
-> CAspect ctx '[]
-> CAspect ctx '[ '(prd, CRule ctx prd sc ip ic sp ic' sp')]
forall (ctx :: [ErrorMessage]) (prd :: Prod)
       (sc :: [(Child, [(Att, *)])]) (ip :: [(Att, *)])
       (ic :: [(Child, [(Att, *)])]) (sp :: [(Att, *)])
       (ic' :: [(Child, [(Att, *)])]) (sp' :: [(Att, *)])
       (a :: [(Prod, *)]) (asp :: [(Prod, *)]).
(Require
   (OpComRA ctx prd (CRule ctx prd sc ip ic sp ic' sp') a) ctx,
 ReqR (OpComRA ctx prd (CRule ctx prd sc ip ic sp ic' sp') a)
 ~ Rec PrdReco asp) =>
CRule ctx prd sc ip ic sp ic' sp'
-> CAspect ctx a -> CAspect ctx asp
.+: CAspect ctx '[]
forall (ctx :: [ErrorMessage]). CAspect ctx '[]
emptyAspect

infixr 6 .+.
.+. :: CRule ctx prd' sc ip ic sp ic' sp'
-> CRule ctx prd' sc ip a b ic sp
-> CRule ctx prd' sc ip a b ic' sp'
(.+.) = CRule ctx prd' sc ip ic sp ic' sp'
-> CRule ctx prd' sc ip a b ic sp
-> CRule ctx prd' sc ip a b ic' sp'
forall (prd :: Prod) (prd' :: Prod) (ctx :: [ErrorMessage])
       (sc :: [(Child, [(Att, *)])]) (ip :: [(Att, *)])
       (ic :: [(Child, [(Att, *)])]) (sp :: [(Att, *)])
       (ic' :: [(Child, [(Att, *)])]) (sp' :: [(Att, *)])
       (a :: [(Child, [(Att, *)])]) (b :: [(Att, *)]).
RequireEq prd prd' ('Text "ext" : ctx) =>
CRule ctx prd sc ip ic sp ic' sp'
-> CRule ctx prd' sc ip a b ic sp
-> CRule ctx prd sc ip a b ic' sp'
ext


-- | combine a rule with an aspect (wrapper)
data OpComRA (ctx  :: [ErrorMessage])
             (prd  :: Prod)
             (rule :: Type) -- TODO : doc this
             (a    :: [(Prod, Type)]) where
  OpComRA :: CRule ctx prd sc ip ic sp ic' sp'
          -> Aspect a -> OpComRA ctx prd (CRule ctx prd sc ip ic sp ic' sp') a

-- | combine a rule with an aspect (inner)
data OpComRA' (cmp  :: Ordering)
              (ctx  :: [ErrorMessage])
              (prd  :: Prod)
              (rule :: Type) -- TODO : doc this
              (a    :: [(Prod, Type)]) where
  OpComRA' :: Proxy cmp
           -> CRule ctx prd sc ip ic sp ic' sp'
           -> Aspect a
           -> OpComRA' cmp ctx prd (CRule ctx prd sc ip ic sp ic' sp') a

cRuleToTagField :: (CRule ctx prd sc ip ic sp ic' sp')
                -> TagField PrdReco prd (CRule ctx prd sc ip ic sp ic' sp')
cRuleToTagField :: CRule ctx prd sc ip ic sp ic' sp'
-> TagField PrdReco prd (CRule ctx prd sc ip ic sp ic' sp')
cRuleToTagField =
  Label PrdReco
-> Label prd
-> WrapField PrdReco (CRule ctx prd sc ip ic sp ic' sp')
-> TagField PrdReco prd (CRule ctx prd sc ip ic sp ic' sp')
forall k k' k'' (c :: k) (l :: k') (v :: k'').
Label c -> Label l -> WrapField c v -> TagField c l v
TagField Label PrdReco
forall k (l :: k). Label l
Label Label prd
forall k (l :: k). Label l
Label

instance
  Require (OpComRA ctx prd (CRule ctx prd sc ip ic sp ic' sp') '[]) ctx where
  type ReqR (OpComRA ctx prd (CRule ctx prd sc ip ic sp ic' sp') '[]) =
    Aspect '[ '(prd, CRule ctx prd sc ip ic sp ic' sp')]
  req :: Proxy ctx
-> OpComRA ctx prd (CRule ctx prd sc ip ic sp ic' sp') '[]
-> ReqR (OpComRA ctx prd (CRule ctx prd sc ip ic sp ic' sp') '[])
req Proxy ctx
ctx (OpComRA CRule ctx prd sc ip ic sp ic' sp'
rule Aspect '[]
EmptyRec) =
    TagField PrdReco prd (CRule ctx prd sc ip ic sp ic' sp')
-> Aspect '[]
-> Rec PrdReco '[ '(prd, CRule ctx prd sc ip ic sp ic' sp')]
forall k k' k'' (c :: k) (l :: k') (v :: k'') (r1 :: [(k', k'')]).
TagField c l v -> Rec c r1 -> Rec c ('(l, v) : r1)
ConsRec (CRule ctx prd sc ip ic sp ic' sp'
-> TagField PrdReco prd (CRule ctx prd sc ip ic sp ic' sp')
forall (ctx :: [ErrorMessage]) (prd :: Prod)
       (sc :: [(Child, [(Att, *)])]) (ip :: [(Att, *)])
       (ic :: [(Child, [(Att, *)])]) (sp :: [(Att, *)])
       (ic' :: [(Child, [(Att, *)])]) (sp' :: [(Att, *)]).
CRule ctx prd sc ip ic sp ic' sp'
-> TagField PrdReco prd (CRule ctx prd sc ip ic sp ic' sp')
cRuleToTagField CRule ctx prd sc ip ic sp ic' sp'
rule) Aspect '[]
forall k k' k'' (c :: k). Rec c '[]
EmptyRec

instance
  Require (OpComRA' (Cmp prd prd') ctx prd rule ( '(prd', rule') ': asp )) ctx
  =>
  Require (OpComRA ctx prd rule ( '(prd', rule') ': asp )) ctx where
  type ReqR (OpComRA ctx prd rule ( '(prd', rule') ': asp )) =
    ReqR (OpComRA' (Cmp prd prd') ctx prd rule ( '(prd', rule') ': asp ))
  req :: Proxy ctx
-> OpComRA ctx prd rule ('(prd', rule') : asp)
-> ReqR (OpComRA ctx prd rule ('(prd', rule') : asp))
req Proxy ctx
ctx (OpComRA CRule ctx prd sc ip ic sp ic' sp'
rule Aspect ('(prd', rule') : asp)
asp) =
    Proxy ctx
-> OpComRA'
     (Cmp prd prd')
     ctx
     prd
     (CRule ctx prd sc ip ic sp ic' sp')
     ('(prd', rule') : asp)
-> ReqR
     (OpComRA'
        (Cmp prd prd')
        ctx
        prd
        (CRule ctx prd sc ip ic sp ic' sp')
        ('(prd', rule') : asp))
forall op (ctx :: [ErrorMessage]).
Require op ctx =>
Proxy ctx -> op -> ReqR op
req Proxy ctx
ctx (Proxy (Cmp prd prd')
-> CRule ctx prd sc ip ic sp ic' sp'
-> Aspect ('(prd', rule') : asp)
-> OpComRA'
     (Cmp prd prd')
     ctx
     prd
     (CRule ctx prd sc ip ic sp ic' sp')
     ('(prd', rule') : asp)
forall (cmp :: Ordering) (ctx :: [ErrorMessage]) (prd :: Prod)
       (sc :: [(Child, [(Att, *)])]) (ip :: [(Att, *)])
       (ic :: [(Child, [(Att, *)])]) (sp :: [(Att, *)])
       (ic' :: [(Child, [(Att, *)])]) (sp' :: [(Att, *)])
       (a :: [(Prod, *)]).
Proxy cmp
-> CRule ctx prd sc ip ic sp ic' sp'
-> Aspect a
-> OpComRA' cmp ctx prd (CRule ctx prd sc ip ic sp ic' sp') a
OpComRA' (Proxy (Cmp prd prd')
forall k (t :: k). Proxy t
Proxy @ (Cmp prd prd')) CRule ctx prd sc ip ic sp ic' sp'
rule Aspect ('(prd', rule') : asp)
asp)

instance
  ( Require (OpUpdate PrdReco prd (CRule ctx prd sc ip ic sp ic'' sp'') a) ctx
  , Require (OpLookup PrdReco prd a) ctx
  , ReqR (OpLookup PrdReco prd a) ~ CRule ctx prd sc ip ic sp ic' sp'
  , (IC (ReqR (OpLookup PrdReco prd a))) ~ ic
  , (SP (ReqR (OpLookup PrdReco prd a))) ~ sp
  ) =>
  Require
   (OpComRA' 'EQ ctx prd (CRule ctx prd sc ip ic' sp' ic'' sp'') a) ctx where
  type ReqR (OpComRA' 'EQ ctx prd (CRule ctx prd sc ip ic' sp' ic'' sp'') a) =
    ReqR (OpUpdate PrdReco prd
            (CRule ctx prd sc ip
             (IC (ReqR (OpLookup PrdReco prd a)))
             (SP (ReqR (OpLookup PrdReco prd a)))
            ic'' sp'') a)
  req :: Proxy ctx
-> OpComRA' 'EQ ctx prd (CRule ctx prd sc ip ic' sp' ic'' sp'') a
-> ReqR
     (OpComRA' 'EQ ctx prd (CRule ctx prd sc ip ic' sp' ic'' sp'') a)
req Proxy ctx
ctx (OpComRA' Proxy 'EQ
_ CRule ctx prd sc ip ic sp ic' sp'
crule Aspect a
asp) =
    let prd :: Label prd
prd     = Label prd
forall k (l :: k). Label l
Label @ prd
        oldRule :: ReqR (OpLookup PrdReco prd a)
oldRule = Proxy ctx
-> OpLookup PrdReco prd a -> ReqR (OpLookup PrdReco prd a)
forall op (ctx :: [ErrorMessage]).
Require op ctx =>
Proxy ctx -> op -> ReqR op
req Proxy ctx
ctx (Label prd -> Aspect a -> OpLookup PrdReco prd a
forall k k' (l :: k) c (r :: [(k, k')]).
Label l -> Rec c r -> OpLookup c l r
OpLookup Label prd
prd Aspect a
asp)
        newRule :: CRule ctx prd sc ip ic sp ic' sp'
newRule = CRule ctx prd sc ip ic sp ic' sp'
crule CRule ctx prd sc ip ic sp ic' sp'
-> CRule ctx prd sc ip ic sp ic sp
-> CRule ctx prd sc ip ic sp ic' sp'
forall (prd :: Prod) (prd' :: Prod) (ctx :: [ErrorMessage])
       (sc :: [(Child, [(Att, *)])]) (ip :: [(Att, *)])
       (ic :: [(Child, [(Att, *)])]) (sp :: [(Att, *)])
       (ic' :: [(Child, [(Att, *)])]) (sp' :: [(Att, *)])
       (a :: [(Child, [(Att, *)])]) (b :: [(Att, *)]).
RequireEq prd prd' ('Text "ext" : ctx) =>
CRule ctx prd sc ip ic sp ic' sp'
-> CRule ctx prd' sc ip a b ic sp
-> CRule ctx prd sc ip a b ic' sp'
`ext` ReqR (OpLookup PrdReco prd a)
CRule ctx prd sc ip ic sp ic sp
oldRule
    in  Proxy ctx
-> OpUpdate PrdReco prd (CRule ctx prd sc ip ic sp ic'' sp'') a
-> ReqR
     (OpUpdate PrdReco prd (CRule ctx prd sc ip ic sp ic'' sp'') a)
forall op (ctx :: [ErrorMessage]).
Require op ctx =>
Proxy ctx -> op -> ReqR op
req Proxy ctx
ctx (Label prd
-> WrapField PrdReco (CRule ctx prd sc ip ic sp ic'' sp'')
-> Aspect a
-> OpUpdate PrdReco prd (CRule ctx prd sc ip ic sp ic'' sp'') a
forall k k' (l :: k) c (v :: k') (r :: [(k, k')]).
Label l -> WrapField c v -> Rec c r -> OpUpdate c l v r
OpUpdate Label prd
prd WrapField PrdReco (CRule ctx prd sc ip ic sp ic'' sp'')
CRule ctx prd sc ip ic sp ic' sp'
newRule Aspect a
asp)

instance
  ( Require (OpComRA ctx prd rule asp) ctx
  , ReqR (OpComRA ctx prd rule asp) ~ Aspect a0
  )
  =>
  Require (OpComRA' 'GT ctx prd rule ( '(prd' , rule') ': asp)) ctx where
  type ReqR (OpComRA' 'GT ctx prd rule ( '(prd' , rule') ': asp)) =
    Aspect ( '(prd' , rule') ': UnWrap (ReqR (OpComRA ctx prd rule asp)))
  req :: Proxy ctx
-> OpComRA' 'GT ctx prd rule ('(prd', rule') : asp)
-> ReqR (OpComRA' 'GT ctx prd rule ('(prd', rule') : asp))
req Proxy ctx
ctx (OpComRA' Proxy 'GT
_ CRule ctx prd sc ip ic sp ic' sp'
crule (ConsRec TagField PrdReco l v
crule' Rec PrdReco r1
asp)) =
    TagField PrdReco l v -> Aspect a0 -> Rec PrdReco ('(l, v) : a0)
forall k k' k'' (c :: k) (l :: k') (v :: k'') (r1 :: [(k', k'')]).
TagField c l v -> Rec c r1 -> Rec c ('(l, v) : r1)
ConsRec TagField PrdReco l v
crule' (Aspect a0 -> Rec PrdReco ('(l, v) : a0))
-> Aspect a0 -> Rec PrdReco ('(l, v) : a0)
forall a b. (a -> b) -> a -> b
$ Proxy ctx
-> OpComRA ctx prd (CRule ctx prd sc ip ic sp ic' sp') r1
-> ReqR (OpComRA ctx prd (CRule ctx prd sc ip ic sp ic' sp') r1)
forall op (ctx :: [ErrorMessage]).
Require op ctx =>
Proxy ctx -> op -> ReqR op
req Proxy ctx
ctx (CRule ctx prd sc ip ic sp ic' sp'
-> Rec PrdReco r1
-> OpComRA ctx prd (CRule ctx prd sc ip ic sp ic' sp') r1
forall (ctx :: [ErrorMessage]) (prd :: Prod)
       (sc :: [(Child, [(Att, *)])]) (ip :: [(Att, *)])
       (ic :: [(Child, [(Att, *)])]) (sp :: [(Att, *)])
       (ic' :: [(Child, [(Att, *)])]) (sp' :: [(Att, *)])
       (a :: [(Prod, *)]).
CRule ctx prd sc ip ic sp ic' sp'
-> Aspect a
-> OpComRA ctx prd (CRule ctx prd sc ip ic sp ic' sp') a
OpComRA CRule ctx prd sc ip ic sp ic' sp'
crule Rec PrdReco r1
asp)

instance 
  Require (OpComRA' 'LT ctx prd rule ( '(prd' , rule') ': asp)) ctx where
  type ReqR (OpComRA' 'LT ctx prd rule ( '(prd' , rule') ': asp)) =
    Aspect ( '(prd, rule) ': '(prd' , rule') ': asp)
  req :: Proxy ctx
-> OpComRA' 'LT ctx prd rule ('(prd', rule') : asp)
-> ReqR (OpComRA' 'LT ctx prd rule ('(prd', rule') : asp))
req Proxy ctx
ctx (OpComRA' Proxy 'LT
_ CRule ctx prd sc ip ic sp ic' sp'
crule Aspect ('(prd', rule') : asp)
asp) =
    TagField PrdReco prd (CRule ctx prd sc ip ic sp ic' sp')
-> Aspect ('(prd', rule') : asp)
-> Rec
     PrdReco
     ('(prd, CRule ctx prd sc ip ic sp ic' sp') : '(prd', rule') : asp)
forall k k' k'' (c :: k) (l :: k') (v :: k'') (r1 :: [(k', k'')]).
TagField c l v -> Rec c r1 -> Rec c ('(l, v) : r1)
ConsRec (Label PrdReco
-> Label prd
-> WrapField PrdReco (CRule ctx prd sc ip ic sp ic' sp')
-> TagField PrdReco prd (CRule ctx prd sc ip ic sp ic' sp')
forall k k' k'' (c :: k) (l :: k') (v :: k'').
Label c -> Label l -> WrapField c v -> TagField c l v
TagField Label PrdReco
forall k (l :: k). Label l
Label Label prd
forall k (l :: k). Label l
Label WrapField PrdReco (CRule ctx prd sc ip ic sp ic' sp')
CRule ctx prd sc ip ic sp ic' sp'
crule) Aspect ('(prd', rule') : asp)
asp



-- | extract Rule from Aspect
-- data OpGetRule (prd :: Prod)
--                (a   :: [(Prod, Type)]) where
--   OpGetRule :: Label prd -> CAspect ctx a -> OpGetRule prd a

-- instance
--   (Require (OpLookup AttReco prd a) ctx,
--    ReqR (OpLookup PrdReco prd a) ~ Rule prd sc ip ic sp ic' sp'
--   )
--   =>
--   Require (OpGetRule prd a) ctx where
--   type ReqR (OpGetRule prd a) = ReqR (OpLookup @Prod @Type AttReco prd a)
--   req ctx (OpGetRule prd (CAspect ca)) =
--     let rule = req ctx (OpLookup prd (ca Proxy))
--     in CRule $ \ctx -> rule

data OpGetRA (ctx  :: [ErrorMessage])
             (prd  :: Prod)
             (a    :: [(Prod, Type)]) where
  OpGetRA :: Label prd -> Aspect a -> OpGetRA ctx prd a

instance
  (Require (OpLookup PrdReco prd a) ctx)
  =>
  Require (OpGetRA ctx prd a) ctx where
  type ReqR (OpGetRA ctx prd a) = ReqR (OpLookup PrdReco prd a)
  req :: Proxy ctx -> OpGetRA ctx prd a -> ReqR (OpGetRA ctx prd a)
req Proxy ctx
ctx (OpGetRA Label prd
prd Aspect a
a) = Proxy ctx
-> OpLookup PrdReco prd a -> ReqR (OpLookup PrdReco prd a)
forall op (ctx :: [ErrorMessage]).
Require op ctx =>
Proxy ctx -> op -> ReqR op
req Proxy ctx
ctx (Label prd -> Aspect a -> OpLookup PrdReco prd a
forall k k' (l :: k) c (r :: [(k, k')]).
Label l -> Rec c r -> OpLookup c l r
OpLookup Label prd
prd Aspect a
a)
-- todo: do not return units when not found


-- (.#..)
--   :: (Require (OpLookup PrdReco prd r) (('ShowType r : ctx0)),
--       ReqR (OpLookup PrdReco prd r) ~ CRule ctx prd sc ip ic sp ic' sp') =>
--      CAspect ctx r -> Label prd -> CRule ctx prd sc ip ic sp ic' sp'
CAspect ctx r
ca .#.. :: CAspect ctx r -> Label l -> ReqR (OpLookup PrdReco l r)
.#.. Label l
prd
  = (CAspect ctx r -> Proxy ctx -> Aspect r
forall (ctx :: [ErrorMessage]) (asp :: [(Prod, *)]).
CAspect ctx asp -> Proxy ctx -> Aspect asp
mkAspect CAspect ctx r
ca Proxy ctx
forall k (t :: k). Proxy t
Proxy) Aspect r -> Label l -> ReqR (OpLookup PrdReco 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
# Label l
prd




-- | add rule to an aspect
data OpComAsp  (al :: [(Prod, Type)])
               (ar :: [(Prod, Type)]) where
  OpComAsp :: Aspect al -> Aspect ar -> OpComAsp al ar

instance
  Require (OpComAsp '[] ar) ctx where
  type ReqR (OpComAsp '[] ar) = Aspect ar
  req :: Proxy ctx -> OpComAsp '[] ar -> ReqR (OpComAsp '[] ar)
req Proxy ctx
ctx (OpComAsp Aspect '[]
_ Aspect ar
ar) = Aspect ar
ReqR (OpComAsp '[] ar)
ar

instance
 ( (ReqR (OpComRA ctx prd (CRule ctx prd sc ip ic sp ic' sp') ar))
   ~ (Rec PrdReco
    (UnWrap
      (ReqR (OpComRA ctx prd (CRule ctx prd sc ip ic sp ic' sp') ar))))
 , ReqR (OpComRA ctx prd (CRule ctx prd sc ip ic sp ic' sp') ar)
   ~ Rec PrdReco ar0
 , (Require (OpComAsp al ar0) ctx)
 , (Require
     (OpComRA ctx prd (CRule ctx prd sc ip ic sp ic' sp') ar) ctx)
 ) =>
  Require (OpComAsp
           ('(prd, CRule ctx prd sc ip ic sp ic' sp') ': al) ar) ctx where
  type ReqR (OpComAsp ('(prd, CRule ctx prd sc ip ic sp ic' sp') ': al) ar) =
    ReqR (OpComAsp al
      (UnWrap (ReqR
                (OpComRA ctx prd (CRule ctx prd sc ip ic sp ic' sp') ar))))
  req :: Proxy ctx
-> OpComAsp ('(prd, CRule ctx prd sc ip ic sp ic' sp') : al) ar
-> ReqR
     (OpComAsp ('(prd, CRule ctx prd sc ip ic sp ic' sp') : al) ar)
req Proxy ctx
ctx (OpComAsp (ConsRec (TagField Label PrdReco
_ Label l
_ WrapField PrdReco v
rul) Rec PrdReco r1
al) Aspect ar
ar)
    = Proxy ctx -> OpComAsp r1 ar0 -> ReqR (OpComAsp r1 ar0)
forall op (ctx :: [ErrorMessage]).
Require op ctx =>
Proxy ctx -> op -> ReqR op
req Proxy ctx
ctx (Rec PrdReco r1 -> Rec PrdReco ar0 -> OpComAsp r1 ar0
forall (al :: [(Prod, *)]) (ar :: [(Prod, *)]).
Aspect al -> Aspect ar -> OpComAsp al ar
OpComAsp Rec PrdReco r1
al (Proxy ctx
-> OpComRA ctx prd (CRule ctx prd sc ip ic sp ic' sp') ar
-> ReqR (OpComRA ctx prd (CRule ctx prd sc ip ic sp ic' sp') ar)
forall op (ctx :: [ErrorMessage]).
Require op ctx =>
Proxy ctx -> op -> ReqR op
req Proxy ctx
ctx (CRule ctx prd sc ip ic sp ic' sp'
-> Aspect ar
-> OpComRA ctx prd (CRule ctx prd sc ip ic sp ic' sp') ar
forall (ctx :: [ErrorMessage]) (prd :: Prod)
       (sc :: [(Child, [(Att, *)])]) (ip :: [(Att, *)])
       (ic :: [(Child, [(Att, *)])]) (sp :: [(Att, *)])
       (ic' :: [(Child, [(Att, *)])]) (sp' :: [(Att, *)])
       (a :: [(Prod, *)]).
CRule ctx prd sc ip ic sp ic' sp'
-> Aspect a
-> OpComRA ctx prd (CRule ctx prd sc ip ic sp ic' sp') a
OpComRA WrapField PrdReco v
CRule ctx prd sc ip ic sp ic' sp'
rul Aspect ar
ar)))

type family IC (rule :: Type) where
  IC (Rule prd sc ip ic sp ic' sp') = ic
  IC (CRule ctx prd sc ip ic sp ic' sp') = ic
type family SP (rule :: Type) where
  SP (Rule prd sc ip ic sp ic' sp') = sp
  SP (CRule ctx prd sc ip ic sp ic' sp') = sp
   

type family Syndef t t' ctx att sp sp' prd prd' :: Constraint where
  Syndef t t' ctx att sp sp' prd prd' =
     ( RequireEqWithMsg t t' AttTypeMatch ctx--
     , RequireEqWithMsg prd prd' PrdTypeMatch ctx
     , RequireR (OpExtend AttReco ('Att att t) t' sp) ctx (Attribution sp')
     )

data AttTypeMatch (a::k)(b::k) -- where
  -- AttTypeMatch :: a -> b -> AttTypeMatch a b
type instance Eval (AttTypeMatch t1 t2) =
    ( ShowTE t1 :<>: Text " /= " :<>: ShowTE t2 :$$:
      Text "type mismatch in attribute definition" :$$:
      Text "attribute type does not match with \
          \the computation that defines it")

data PrdTypeMatch (a :: k)(b :: k)
type instance Eval (PrdTypeMatch t1 t2) =
    ( ShowTE t1 :<>: Text " /= " :<>: ShowTE t2 :$$:
      Text "mismatch in production type. \
           \Perhaps you are trying to get data from a \
           \children of a wrong production?")

data ChiPrdMatch (a :: Prod)(b :: Prod)
type instance Eval (ChiPrdMatch ('Prd att nt) ('Prd att' nt')) =
    ( ShowTE  ('Prd att nt) :<>: Text " /= " :<>: ShowTE ('Prd att' nt') :$$:
      Text "production and child mismatch in inherited attribute definition")


data GetAttTypeMatch (a::k)(b::k) where
  GetAttTypeMatch :: a -> b -> GetAttTypeMatch a b
type instance Eval (GetAttTypeMatch t1 t2) =
    ( ShowTE t1 :<>: Text " /= " :<>: ShowTE t2 :$$:
      Text "ill typed attribute computation")

-- | The function 'syndef' adds the definition of a synthesized
--   attribute.  It takes an attribute label 'att' representing the
--   name of the new attribute; a production label 'prd' representing
--   the production where the rule is defined; a value 't'' to be
--   assigned to this attribute, given a context and an input
--   family. It updates the output constructed thus far.
syndef
  :: Syndef t t' ctx att sp sp' prd prd' 
  => forall sc ip ic .
     Label ('Att att t)
  -> Label prd
  -> (Proxy ctx -> Fam prd' sc ip -> t')
  -> CRule ctx prd sc ip ic sp ic sp'
syndef :: forall (sc :: [(Child, [(Att, *)])]) (ip :: [(Att, *)])
       (ic :: [(Child, [(Att, *)])]).
Label ('Att att t)
-> Label prd
-> (Proxy ctx -> Fam prd' sc ip -> t')
-> CRule ctx prd sc ip ic sp ic sp'
syndef Label ('Att att t)
att Label prd
prd Proxy ctx -> Fam prd' sc ip -> t'
f
  = (Proxy ctx -> Rule prd' sc ip ic sp ic sp')
-> CRule ctx prd' sc ip ic sp ic sp'
forall (ctx :: [ErrorMessage]) (prd :: Prod)
       (sc :: [(Child, [(Att, *)])]) (ip :: [(Att, *)])
       (ic :: [(Child, [(Att, *)])]) (sp :: [(Att, *)])
       (ic' :: [(Child, [(Att, *)])]) (sp' :: [(Att, *)]).
(Proxy ctx -> Rule prd sc ip ic sp ic' sp')
-> CRule ctx prd sc ip ic sp ic' sp'
CRule ((Proxy ctx -> Rule prd' sc ip ic sp ic sp')
 -> CRule ctx prd' sc ip ic sp ic sp')
-> (Proxy ctx -> Rule prd' sc ip ic sp ic sp')
-> CRule ctx prd' sc ip ic sp ic sp'
forall a b. (a -> b) -> a -> b
$ \Proxy ctx
ctx Fam prd' sc ip
inp (Fam ChAttsRec prd' ic
ic Attribution sp
sp)
   ->  ChAttsRec prd' ic -> Attribution sp' -> Fam prd' ic sp'
forall (prd :: Prod) (c :: [(Child, [(Att, *)])])
       (p :: [(Att, *)]).
ChAttsRec prd c -> Attribution p -> Fam prd c p
Fam ChAttsRec prd' ic
ic (Attribution sp' -> Fam prd' ic sp')
-> Attribution sp' -> Fam prd' ic sp'
forall a b. (a -> b) -> a -> b
$ Proxy ctx
-> OpExtend AttReco ('Att att t) t' sp
-> ReqR (OpExtend AttReco ('Att att t) t' sp)
forall op (ctx :: [ErrorMessage]).
Require op ctx =>
Proxy ctx -> op -> ReqR op
req Proxy ctx
ctx (Label ('Att att t)
-> WrapField AttReco t'
-> Attribution sp
-> OpExtend AttReco ('Att att t) t' sp
forall k k' (l :: k) c (v :: k') (r :: [(k, k')]).
Label l -> WrapField c v -> Rec c r -> OpExtend c l v r
OpExtend Label ('Att att t)
att (Proxy ctx -> Fam prd' sc ip -> t'
f Proxy ctx
forall k (t :: k). Proxy t
Proxy Fam prd' sc ip
inp) Attribution sp
sp)


data  SyndefT t t' (ctx :: [ErrorMessage])
                   (att :: Symbol)
                   (sp :: [(Att, Type)])
                   (sp' :: [(Att, Type)]) prd prd'

class Syndef' a
instance
     ( RequireEqWithMsg t t' AttTypeMatch ctx--
     , RequireEqWithMsg prd prd' PrdTypeMatch ctx
     , RequireR (OpExtend AttReco ('Att att t) t' sp) ctx (Attribution sp')
     )
      => Syndef' (SyndefT t t' ctx att sp sp' prd prd' )

data Dummy
instance Syndef' Dummy

-- syndef'
--   :: Syndef' (SyndefT t t' ctx att sp sp' prd prd') 
--   => forall sc ip ic .
--      Label ('Att att t)
--   -> Label prd
--   -> (Proxy ctx -> Fam prd' sc ip -> t')
--   -> CRule ctx prd' sc ip ic sp ic sp'
-- syndef' att prd f
--   = CRule $ \ctx inp (Fam ic sp)
--    ->  Fam ic $ req ctx (OpExtend att (f Proxy inp) sp)




-- | As 'syndef', the function 'syndefM' adds the definition of a
--   synthesized attribute.  It takes an attribute label 'att'
--   representing the name of the new attribute; a production label
--   'prd' representing the production where the rule is defined; a
--   value 't'' to be assigned to this attribute, given a context and
--   an input family. It updates the output constructed thus far. This
--   function captures the monadic behaviour of the family
--   updating. For instance, the following definition specifies a rule
--   for an attribute `att_size :: Label (Att "size" Int)` at the
--   prduction `p_cons :: Label (Prd "cons" (NT "List"))`. The value
--   is computed from the very same attribute value at a child
--   `ch_tail :: Chi "tail" (Prd "cons" (NT "List") (Left NT))`
--
-- @
-- foo = syndefM att_size p_cons $ do sizeatchi <- at ch_tail att_size
--                                    return (sizeatchi + 1)
-- @


data SyndefMsg
data InhdefMsg

type family MkMsg msgtype att t prd nt where
  MkMsg SyndefMsg att t prd nt =
         Text "- syndef: definition of attribute "
    :<>: ShowTE ('Att att t) :$$: Text "   in production "
    :<>: ShowTE ('Prd prd nt)
  MkMsg InhdefMsg att t prd nt =
         Text "- inhdef: definition of attribute "
    :<>: ShowTE ('Att att t) :$$: Text "   in production "
    :<>: ShowTE ('Prd prd nt)

mkSyndefMsg :: Label ('Att att t) -> Label ('Prd prd nt)
  -> Proxy (MkMsg SyndefMsg att t prd nt)
mkSyndefMsg :: Label ('Att att t)
-> Label ('Prd prd nt) -> Proxy (MkMsg SyndefMsg att t prd nt)
mkSyndefMsg Label ('Att att t)
Label Label ('Prd prd nt)
Label = Proxy (MkMsg SyndefMsg att t prd nt)
forall k (t :: k). Proxy t
Proxy

mkMsg :: Proxy msg -> Label ('Att att t) -> Label ('Prd prd nt)
  -> Proxy (MkMsg msg att t prd nt)
mkMsg :: Proxy msg
-> Label ('Att att t)
-> Label ('Prd prd nt)
-> Proxy (MkMsg msg att t prd nt)
mkMsg Proxy msg
Proxy Label ('Att att t)
Label Label ('Prd prd nt)
Label = Proxy (MkMsg msg att t prd nt)
forall k (t :: k). Proxy t
Proxy


-- | This is simply an alias for 'syndef'
syn
  :: Syndef t t' (MkMsg SyndefMsg att t prd nt ': ctx) att sp sp' prd prd'
  => Label ('Att att t)
  -> Label ('Prd prd nt)
  -> Reader (Proxy (MkMsg SyndefMsg att t prd nt ': ctx),
             Fam ('Prd prd' nt) sc ip) t'
  -> CRule ctx ('Prd prd nt) sc ip ic sp ic sp'
syn :: Label ('Att att t)
-> Label ('Prd prd nt)
-> Reader
     (Proxy (MkMsg SyndefMsg att t prd nt : ctx),
      Fam ('Prd prd' nt) sc ip)
     t'
-> CRule ctx ('Prd prd nt) sc ip ic sp ic sp'
syn Label ('Att att t)
att Label ('Prd prd nt)
prd Reader
  (Proxy (MkMsg SyndefMsg att t prd nt : ctx),
   Fam ('Prd prd' nt) sc ip)
  t'
f
  = (Proxy ctx
 -> Proxy
      ((('Text "- syndef: definition of attribute "
         ':<>: 'Text
                 (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
        ':$$: ('Text "   in production "
               ':<>: 'Text
                       (AppendSymbol
                          (AppendSymbol
                             (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                          ")")))
         : ctx))
-> CRule
     ((('Text "- syndef: definition of attribute "
        ':<>: 'Text
                (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
       ':$$: ('Text "   in production "
              ':<>: 'Text
                      (AppendSymbol
                         (AppendSymbol
                            (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                         ")")))
        : ctx)
     ('Prd prd nt)
     sc
     ip
     ic
     sp
     ic
     sp'
-> CRule ctx ('Prd prd nt) sc ip ic sp ic sp'
forall (ctx :: [ErrorMessage]) (ctx' :: [ErrorMessage])
       (prd :: Prod) (sc :: [(Child, [(Att, *)])]) (ip :: [(Att, *)])
       (ic :: [(Child, [(Att, *)])]) (sp :: [(Att, *)])
       (ic' :: [(Child, [(Att, *)])]) (sp' :: [(Att, *)]).
(Proxy ctx -> Proxy ctx')
-> CRule ctx' prd sc ip ic sp ic' sp'
-> CRule ctx prd sc ip ic sp ic' sp'
mapCRule (Label ('Att att t)
-> Label ('Prd prd nt) -> Proxy (MkMsg SyndefMsg att t prd nt)
forall (att :: Symbol) t (prd :: Symbol) (nt :: NT).
Label ('Att att t)
-> Label ('Prd prd nt) -> Proxy (MkMsg SyndefMsg att t prd nt)
mkSyndefMsg Label ('Att att t)
att Label ('Prd prd nt)
prd Proxy
  (('Text "- syndef: definition of attribute "
    ':<>: 'Text
            (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
   ':$$: ('Text "   in production "
          ':<>: 'Text
                  (AppendSymbol
                     (AppendSymbol
                        (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                     ")")))
-> Proxy ctx
-> Proxy
     ((('Text "- syndef: definition of attribute "
        ':<>: 'Text
                (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
       ':$$: ('Text "   in production "
              ':<>: 'Text
                      (AppendSymbol
                         (AppendSymbol
                            (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                         ")")))
        : ctx)
forall a (e :: a) (es :: [a]).
Proxy e -> Proxy es -> Proxy (e : es)
`consErr`) (CRule
   ((('Text "- syndef: definition of attribute "
      ':<>: 'Text
              (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
     ':$$: ('Text "   in production "
            ':<>: 'Text
                    (AppendSymbol
                       (AppendSymbol
                          (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                       ")")))
      : ctx)
   ('Prd prd nt)
   sc
   ip
   ic
   sp
   ic
   sp'
 -> CRule ctx ('Prd prd nt) sc ip ic sp ic sp')
-> CRule
     ((('Text "- syndef: definition of attribute "
        ':<>: 'Text
                (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
       ':$$: ('Text "   in production "
              ':<>: 'Text
                      (AppendSymbol
                         (AppendSymbol
                            (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                         ")")))
        : ctx)
     ('Prd prd nt)
     sc
     ip
     ic
     sp
     ic
     sp'
-> CRule ctx ('Prd prd nt) sc ip ic sp ic sp'
forall a b. (a -> b) -> a -> b
$ (Label ('Att att t)
-> Label ('Prd prd nt)
-> (Proxy
      ((('Text "- syndef: definition of attribute "
         ':<>: 'Text
                 (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
        ':$$: ('Text "   in production "
               ':<>: 'Text
                       (AppendSymbol
                          (AppendSymbol
                             (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                          ")")))
         : ctx)
    -> Fam ('Prd prd' nt) sc ip -> t')
-> CRule
     ((('Text "- syndef: definition of attribute "
        ':<>: 'Text
                (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
       ':$$: ('Text "   in production "
              ':<>: 'Text
                      (AppendSymbol
                         (AppendSymbol
                            (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                         ")")))
        : ctx)
     ('Prd prd nt)
     sc
     ip
     ic
     sp
     ic
     sp'
forall t t' (ctx :: [ErrorMessage]) (att :: Symbol)
       (sp :: [(Att, *)]) (sp' :: [(Att, *)]) (prd :: Prod) (prd' :: Prod)
       (sc :: [(Child, [(Att, *)])]) (ip :: [(Att, *)])
       (ic :: [(Child, [(Att, *)])]).
Syndef t t' ctx att sp sp' prd prd' =>
Label ('Att att t)
-> Label prd
-> (Proxy ctx -> Fam prd' sc ip -> t')
-> CRule ctx prd sc ip ic sp ic sp'
syndef Label ('Att att t)
att Label ('Prd prd nt)
prd ((Proxy
    ((('Text "- syndef: definition of attribute "
       ':<>: 'Text
               (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
      ':$$: ('Text "   in production "
             ':<>: 'Text
                     (AppendSymbol
                        (AppendSymbol
                           (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                        ")")))
       : ctx)
  -> Fam ('Prd prd' nt) sc ip -> t')
 -> CRule
      ((('Text "- syndef: definition of attribute "
         ':<>: 'Text
                 (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
        ':$$: ('Text "   in production "
               ':<>: 'Text
                       (AppendSymbol
                          (AppendSymbol
                             (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                          ")")))
         : ctx)
      ('Prd prd nt)
      sc
      ip
      ic
      sp
      ic
      sp')
-> (Reader
      (Proxy
         ((('Text "- syndef: definition of attribute "
            ':<>: 'Text
                    (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
           ':$$: ('Text "   in production "
                  ':<>: 'Text
                          (AppendSymbol
                             (AppendSymbol
                                (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                             ")")))
            : ctx),
       Fam ('Prd prd' nt) sc ip)
      t'
    -> Proxy
         ((('Text "- syndef: definition of attribute "
            ':<>: 'Text
                    (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
           ':$$: ('Text "   in production "
                  ':<>: 'Text
                          (AppendSymbol
                             (AppendSymbol
                                (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                             ")")))
            : ctx)
    -> Fam ('Prd prd' nt) sc ip
    -> t')
-> Reader
     (Proxy
        ((('Text "- syndef: definition of attribute "
           ':<>: 'Text
                   (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
          ':$$: ('Text "   in production "
                 ':<>: 'Text
                         (AppendSymbol
                            (AppendSymbol
                               (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                            ")")))
           : ctx),
      Fam ('Prd prd' nt) sc ip)
     t'
-> CRule
     ((('Text "- syndef: definition of attribute "
        ':<>: 'Text
                (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
       ':$$: ('Text "   in production "
              ':<>: 'Text
                      (AppendSymbol
                         (AppendSymbol
                            (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                         ")")))
        : ctx)
     ('Prd prd nt)
     sc
     ip
     ic
     sp
     ic
     sp'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Reader
  (Proxy
     ((('Text "- syndef: definition of attribute "
        ':<>: 'Text
                (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
       ':$$: ('Text "   in production "
              ':<>: 'Text
                      (AppendSymbol
                         (AppendSymbol
                            (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                         ")")))
        : ctx),
   Fam ('Prd prd' nt) sc ip)
  t'
-> Proxy
     ((('Text "- syndef: definition of attribute "
        ':<>: 'Text
                (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
       ':$$: ('Text "   in production "
              ':<>: 'Text
                      (AppendSymbol
                         (AppendSymbol
                            (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                         ")")))
        : ctx)
-> Fam ('Prd prd' nt) sc ip
-> t'
forall a b c. Reader (a, b) c -> a -> b -> c
def) Reader
  (Proxy
     ((('Text "- syndef: definition of attribute "
        ':<>: 'Text
                (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
       ':$$: ('Text "   in production "
              ':<>: 'Text
                      (AppendSymbol
                         (AppendSymbol
                            (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                         ")")))
        : ctx),
   Fam ('Prd prd' nt) sc ip)
  t'
Reader
  (Proxy (MkMsg SyndefMsg att t prd nt : ctx),
   Fam ('Prd prd' nt) sc ip)
  t'
f

syndefM
  :: Syndef t t' (MkMsg SyndefMsg att t prd nt ': ctx) att sp sp' prd prd'
  => Label ('Att att t)
  -> Label ('Prd prd nt)
  -> Reader (Proxy (MkMsg SyndefMsg att t prd nt ': ctx),
             Fam ('Prd prd' nt) sc ip) t'
  -> CRule ctx ('Prd prd nt) sc ip ic sp ic sp'
syndefM :: Label ('Att att t)
-> Label ('Prd prd nt)
-> Reader
     (Proxy (MkMsg SyndefMsg att t prd nt : ctx),
      Fam ('Prd prd' nt) sc ip)
     t'
-> CRule ctx ('Prd prd nt) sc ip ic sp ic sp'
syndefM Label ('Att att t)
att Label ('Prd prd nt)
prd Reader
  (Proxy (MkMsg SyndefMsg att t prd nt : ctx),
   Fam ('Prd prd' nt) sc ip)
  t'
f
  = (Proxy ctx
 -> Proxy
      ((('Text "- syndef: definition of attribute "
         ':<>: 'Text
                 (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
        ':$$: ('Text "   in production "
               ':<>: 'Text
                       (AppendSymbol
                          (AppendSymbol
                             (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                          ")")))
         : ctx))
-> CRule
     ((('Text "- syndef: definition of attribute "
        ':<>: 'Text
                (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
       ':$$: ('Text "   in production "
              ':<>: 'Text
                      (AppendSymbol
                         (AppendSymbol
                            (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                         ")")))
        : ctx)
     ('Prd prd nt)
     sc
     ip
     ic
     sp
     ic
     sp'
-> CRule ctx ('Prd prd nt) sc ip ic sp ic sp'
forall (ctx :: [ErrorMessage]) (ctx' :: [ErrorMessage])
       (prd :: Prod) (sc :: [(Child, [(Att, *)])]) (ip :: [(Att, *)])
       (ic :: [(Child, [(Att, *)])]) (sp :: [(Att, *)])
       (ic' :: [(Child, [(Att, *)])]) (sp' :: [(Att, *)]).
(Proxy ctx -> Proxy ctx')
-> CRule ctx' prd sc ip ic sp ic' sp'
-> CRule ctx prd sc ip ic sp ic' sp'
mapCRule (Proxy SyndefMsg
-> Label ('Att att t)
-> Label ('Prd prd nt)
-> Proxy (MkMsg SyndefMsg att t prd nt)
forall msg (att :: Symbol) t (prd :: Symbol) (nt :: NT).
Proxy msg
-> Label ('Att att t)
-> Label ('Prd prd nt)
-> Proxy (MkMsg msg att t prd nt)
mkMsg (Proxy SyndefMsg
forall k (t :: k). Proxy t
Proxy @SyndefMsg) Label ('Att att t)
att Label ('Prd prd nt)
prd Proxy
  (('Text "- syndef: definition of attribute "
    ':<>: 'Text
            (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
   ':$$: ('Text "   in production "
          ':<>: 'Text
                  (AppendSymbol
                     (AppendSymbol
                        (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                     ")")))
-> Proxy ctx
-> Proxy
     ((('Text "- syndef: definition of attribute "
        ':<>: 'Text
                (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
       ':$$: ('Text "   in production "
              ':<>: 'Text
                      (AppendSymbol
                         (AppendSymbol
                            (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                         ")")))
        : ctx)
forall a (e :: a) (es :: [a]).
Proxy e -> Proxy es -> Proxy (e : es)
`consErr`)
    (CRule
   ((('Text "- syndef: definition of attribute "
      ':<>: 'Text
              (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
     ':$$: ('Text "   in production "
            ':<>: 'Text
                    (AppendSymbol
                       (AppendSymbol
                          (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                       ")")))
      : ctx)
   ('Prd prd nt)
   sc
   ip
   ic
   sp
   ic
   sp'
 -> CRule ctx ('Prd prd nt) sc ip ic sp ic sp')
-> CRule
     ((('Text "- syndef: definition of attribute "
        ':<>: 'Text
                (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
       ':$$: ('Text "   in production "
              ':<>: 'Text
                      (AppendSymbol
                         (AppendSymbol
                            (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                         ")")))
        : ctx)
     ('Prd prd nt)
     sc
     ip
     ic
     sp
     ic
     sp'
-> CRule ctx ('Prd prd nt) sc ip ic sp ic sp'
forall a b. (a -> b) -> a -> b
$ (Label ('Att att t)
-> Label ('Prd prd nt)
-> (Proxy
      ((('Text "- syndef: definition of attribute "
         ':<>: 'Text
                 (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
        ':$$: ('Text "   in production "
               ':<>: 'Text
                       (AppendSymbol
                          (AppendSymbol
                             (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                          ")")))
         : ctx)
    -> Fam ('Prd prd' nt) sc ip -> t')
-> CRule
     ((('Text "- syndef: definition of attribute "
        ':<>: 'Text
                (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
       ':$$: ('Text "   in production "
              ':<>: 'Text
                      (AppendSymbol
                         (AppendSymbol
                            (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                         ")")))
        : ctx)
     ('Prd prd nt)
     sc
     ip
     ic
     sp
     ic
     sp'
forall t t' (ctx :: [ErrorMessage]) (att :: Symbol)
       (sp :: [(Att, *)]) (sp' :: [(Att, *)]) (prd :: Prod) (prd' :: Prod)
       (sc :: [(Child, [(Att, *)])]) (ip :: [(Att, *)])
       (ic :: [(Child, [(Att, *)])]).
Syndef t t' ctx att sp sp' prd prd' =>
Label ('Att att t)
-> Label prd
-> (Proxy ctx -> Fam prd' sc ip -> t')
-> CRule ctx prd sc ip ic sp ic sp'
syndef Label ('Att att t)
att Label ('Prd prd nt)
prd ((Proxy
    ((('Text "- syndef: definition of attribute "
       ':<>: 'Text
               (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
      ':$$: ('Text "   in production "
             ':<>: 'Text
                     (AppendSymbol
                        (AppendSymbol
                           (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                        ")")))
       : ctx)
  -> Fam ('Prd prd' nt) sc ip -> t')
 -> CRule
      ((('Text "- syndef: definition of attribute "
         ':<>: 'Text
                 (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
        ':$$: ('Text "   in production "
               ':<>: 'Text
                       (AppendSymbol
                          (AppendSymbol
                             (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                          ")")))
         : ctx)
      ('Prd prd nt)
      sc
      ip
      ic
      sp
      ic
      sp')
-> (Reader
      (Proxy
         ((('Text "- syndef: definition of attribute "
            ':<>: 'Text
                    (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
           ':$$: ('Text "   in production "
                  ':<>: 'Text
                          (AppendSymbol
                             (AppendSymbol
                                (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                             ")")))
            : ctx),
       Fam ('Prd prd' nt) sc ip)
      t'
    -> Proxy
         ((('Text "- syndef: definition of attribute "
            ':<>: 'Text
                    (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
           ':$$: ('Text "   in production "
                  ':<>: 'Text
                          (AppendSymbol
                             (AppendSymbol
                                (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                             ")")))
            : ctx)
    -> Fam ('Prd prd' nt) sc ip
    -> t')
-> Reader
     (Proxy
        ((('Text "- syndef: definition of attribute "
           ':<>: 'Text
                   (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
          ':$$: ('Text "   in production "
                 ':<>: 'Text
                         (AppendSymbol
                            (AppendSymbol
                               (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                            ")")))
           : ctx),
      Fam ('Prd prd' nt) sc ip)
     t'
-> CRule
     ((('Text "- syndef: definition of attribute "
        ':<>: 'Text
                (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
       ':$$: ('Text "   in production "
              ':<>: 'Text
                      (AppendSymbol
                         (AppendSymbol
                            (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                         ")")))
        : ctx)
     ('Prd prd nt)
     sc
     ip
     ic
     sp
     ic
     sp'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Reader
  (Proxy
     ((('Text "- syndef: definition of attribute "
        ':<>: 'Text
                (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
       ':$$: ('Text "   in production "
              ':<>: 'Text
                      (AppendSymbol
                         (AppendSymbol
                            (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                         ")")))
        : ctx),
   Fam ('Prd prd' nt) sc ip)
  t'
-> Proxy
     ((('Text "- syndef: definition of attribute "
        ':<>: 'Text
                (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
       ':$$: ('Text "   in production "
              ':<>: 'Text
                      (AppendSymbol
                         (AppendSymbol
                            (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                         ")")))
        : ctx)
-> Fam ('Prd prd' nt) sc ip
-> t'
forall a b c. Reader (a, b) c -> a -> b -> c
def) Reader
  (Proxy
     ((('Text "- syndef: definition of attribute "
        ':<>: 'Text
                (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
       ':$$: ('Text "   in production "
              ':<>: 'Text
                      (AppendSymbol
                         (AppendSymbol
                            (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                         ")")))
        : ctx),
   Fam ('Prd prd' nt) sc ip)
  t'
Reader
  (Proxy (MkMsg SyndefMsg att t prd nt : ctx),
   Fam ('Prd prd' nt) sc ip)
  t'
f

-- |synthesized poly rule
--synP (att :: forall v. Label ('Att k v)) prd rul
--  = \(p :: Proxy p) -> syndefM (att @ p) prd rul

-- | This is simply an alias for 'inhdefM'
--inh = inhdefM

--inhP (att :: forall v. Label ('Att k v)) prd chi rul
--  = \(p :: Proxy p) -> inhdefM (att @ p) prd chi rul

synmod
  :: RequireR (OpUpdate AttReco ('Att att t) t r) ctx (Attribution sp')
  => Label ('Att att t)
     -> Label prd
     -> (Proxy
           ((('Text "synmod(" ':<>: ShowTE ('Att att t)) :<>: Text ", "
                              ':<>: ShowTE prd :<>: Text ")")
              : ctx)
         -> Fam prd sc ip -> t)
     -> CRule ctx prd sc ip ic' r ic' sp'
synmod :: Label ('Att att t)
-> Label prd
-> (Proxy
      ((((('Text "synmod(" ':<>: ShowTE ('Att att t)) ':<>: 'Text ", ")
         ':<>: ShowTE prd)
        ':<>: 'Text ")")
         : ctx)
    -> Fam prd sc ip -> t)
-> CRule ctx prd sc ip ic' r ic' sp'
synmod Label ('Att att t)
att Label prd
prd Proxy
  ((((('Text "synmod(" ':<>: ShowTE ('Att att t)) ':<>: 'Text ", ")
     ':<>: ShowTE prd)
    ':<>: 'Text ")")
     : ctx)
-> Fam prd sc ip -> t
f
  = (Proxy ctx -> Rule prd sc ip ic' r ic' sp')
-> CRule ctx prd sc ip ic' r ic' sp'
forall (ctx :: [ErrorMessage]) (prd :: Prod)
       (sc :: [(Child, [(Att, *)])]) (ip :: [(Att, *)])
       (ic :: [(Child, [(Att, *)])]) (sp :: [(Att, *)])
       (ic' :: [(Child, [(Att, *)])]) (sp' :: [(Att, *)]).
(Proxy ctx -> Rule prd sc ip ic sp ic' sp')
-> CRule ctx prd sc ip ic sp ic' sp'
CRule ((Proxy ctx -> Rule prd sc ip ic' r ic' sp')
 -> CRule ctx prd sc ip ic' r ic' sp')
-> (Proxy ctx -> Rule prd sc ip ic' r ic' sp')
-> CRule ctx prd sc ip ic' r ic' sp'
forall a b. (a -> b) -> a -> b
$ \Proxy ctx
ctx  Fam prd sc ip
inp (Fam ChAttsRec prd ic'
ic Attribution r
sp)
           -> ChAttsRec prd ic' -> Attribution sp' -> Fam prd ic' sp'
forall (prd :: Prod) (c :: [(Child, [(Att, *)])])
       (p :: [(Att, *)]).
ChAttsRec prd c -> Attribution p -> Fam prd c p
Fam ChAttsRec prd ic'
ic (Attribution sp' -> Fam prd ic' sp')
-> Attribution sp' -> Fam prd ic' sp'
forall a b. (a -> b) -> a -> b
$ Proxy ctx
-> OpUpdate AttReco ('Att att t) t r
-> ReqR (OpUpdate AttReco ('Att att t) t r)
forall op (ctx :: [ErrorMessage]).
Require op ctx =>
Proxy ctx -> op -> ReqR op
req Proxy ctx
ctx (Label ('Att att t)
-> WrapField AttReco t
-> Attribution r
-> OpUpdate AttReco ('Att att t) t r
forall k k' (l :: k) c (v :: k') (r :: [(k, k')]).
Label l -> WrapField c v -> Rec c r -> OpUpdate c l v r
OpUpdate Label ('Att att t)
att (Proxy
  ((((('Text "synmod(" ':<>: ShowTE ('Att att t)) ':<>: 'Text ", ")
     ':<>: ShowTE prd)
    ':<>: 'Text ")")
     : ctx)
-> Fam prd sc ip -> t
f Proxy
  ((((('Text "synmod(" ':<>: ShowTE ('Att att t)) ':<>: 'Text ", ")
     ':<>: ShowTE prd)
    ':<>: 'Text ")")
     : ctx)
forall k (t :: k). Proxy t
Proxy Fam prd sc ip
inp) Attribution r
sp)


synmodM
  :: RequireR (OpUpdate AttReco ('Att att t) t r) ctx (Attribution sp')
  => Label ('Att att t)
     -> Label prd
     -> Reader ( Proxy ((('Text "synmod(" ':<>: ShowTE ('Att att t)) :<>: Text ", "
                                          ':<>: ShowTE prd :<>: Text ")")
                       : ctx)
               , Fam prd sc ip)
               t
     -> CRule ctx prd sc ip ic' r ic' sp'
synmodM :: Label ('Att att t)
-> Label prd
-> Reader
     (Proxy
        ((((('Text "synmod(" ':<>: ShowTE ('Att att t)) ':<>: 'Text ", ")
           ':<>: ShowTE prd)
          ':<>: 'Text ")")
           : ctx),
      Fam prd sc ip)
     t
-> CRule ctx prd sc ip ic' r ic' sp'
synmodM Label ('Att att t)
att Label prd
prd = Label ('Att att t)
-> Label prd
-> (Proxy
      ((((('Text "synmod(" ':<>: ShowTE ('Att att t)) ':<>: 'Text ", ")
         ':<>: ShowTE prd)
        ':<>: 'Text ")")
         : ctx)
    -> Fam prd sc ip -> t)
-> CRule ctx prd sc ip ic' r ic' sp'
forall (att :: Symbol) t (r :: [(Att, *)]) (ctx :: [ErrorMessage])
       (sp' :: [(Att, *)]) (prd :: Prod) (sc :: [(Child, [(Att, *)])])
       (ip :: [(Att, *)]) (ic' :: [(Child, [(Att, *)])]).
RequireR
  (OpUpdate AttReco ('Att att t) t r) ctx (Attribution sp') =>
Label ('Att att t)
-> Label prd
-> (Proxy
      ((((('Text "synmod(" ':<>: ShowTE ('Att att t)) ':<>: 'Text ", ")
         ':<>: ShowTE prd)
        ':<>: 'Text ")")
         : ctx)
    -> Fam prd sc ip -> t)
-> CRule ctx prd sc ip ic' r ic' sp'
synmod Label ('Att att t)
att Label prd
prd ((Proxy
    ((((('Text "synmod("
         ':<>: 'Text
                 (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
        ':<>: 'Text ", ")
       ':<>: ShowTE prd)
      ':<>: 'Text ")")
       : ctx)
  -> Fam prd sc ip -> t)
 -> CRule ctx prd sc ip ic' r ic' sp')
-> (Reader
      (Proxy
         ((((('Text "synmod("
              ':<>: 'Text
                      (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
             ':<>: 'Text ", ")
            ':<>: ShowTE prd)
           ':<>: 'Text ")")
            : ctx),
       Fam prd sc ip)
      t
    -> Proxy
         ((((('Text "synmod("
              ':<>: 'Text
                      (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
             ':<>: 'Text ", ")
            ':<>: ShowTE prd)
           ':<>: 'Text ")")
            : ctx)
    -> Fam prd sc ip
    -> t)
-> Reader
     (Proxy
        ((((('Text "synmod("
             ':<>: 'Text
                     (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
            ':<>: 'Text ", ")
           ':<>: ShowTE prd)
          ':<>: 'Text ")")
           : ctx),
      Fam prd sc ip)
     t
-> CRule ctx prd sc ip ic' r ic' sp'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Reader
  (Proxy
     ((((('Text "synmod("
          ':<>: 'Text
                  (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
         ':<>: 'Text ", ")
        ':<>: ShowTE prd)
       ':<>: 'Text ")")
        : ctx),
   Fam prd sc ip)
  t
-> Proxy
     ((((('Text "synmod("
          ':<>: 'Text
                  (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
         ':<>: 'Text ", ")
        ':<>: ShowTE prd)
       ':<>: 'Text ")")
        : ctx)
-> Fam prd sc ip
-> t
forall a b c. Reader (a, b) c -> a -> b -> c
def


type family Inhdef t t' ctx att r v2 prd prd' nt nt' chi ntch ic ic' n
  where
  Inhdef t t' ctx att r v2 prd prd' nt nt' chi ntch ic ic' n
   = ( RequireEqWithMsg t t' AttTypeMatch ctx
     , RequireEqWithMsg ('Prd prd nt) ('Prd prd' nt') ChiPrdMatch ctx
     --, RequireEq nt  nt'  ctx
     , RequireR (OpExtend AttReco ('Att att t) t' r) ctx (Attribution v2)
     , RequireR (OpUpdate (ChiReco ('Prd prd nt))
                  ('Chi chi ('Prd prd' nt') ntch) v2 ic) ctx
                    (ChAttsRec ('Prd prd' nt') ic')
     , RequireR (OpLookup (ChiReco ('Prd prd nt))
                  ('Chi chi ('Prd prd' nt') ntch) ic) ctx (Attribution r)
    --, ntch ~ ('Left n)
    )

inhdef
  :: Inhdef t t' ctx att r v2 prd prd' nt nt' chi ntch ic ic' n
  => Label ('Att att t)
  -> Label ('Prd prd nt)
  -> Label ('Chi chi ('Prd prd' nt') ntch)
  -> (Proxy ctx -> Fam ('Prd prd nt) sc ip -> t')
  -> forall sp . CRule ctx ('Prd prd nt) sc ip ic sp ic' sp

inhdef :: Label ('Att att t)
-> Label ('Prd prd nt)
-> Label ('Chi chi ('Prd prd' nt') ntch)
-> (Proxy ctx -> Fam ('Prd prd nt) sc ip -> t')
-> forall (sp :: [(Att, *)]).
   CRule ctx ('Prd prd nt) sc ip ic sp ic' sp
inhdef Label ('Att att t)
att Label ('Prd prd nt)
prd Label ('Chi chi ('Prd prd' nt') ntch)
chi Proxy ctx -> Fam ('Prd prd nt) sc ip -> t'
f =
  (Proxy ctx -> Rule ('Prd prd nt) sc ip ic sp ic' sp)
-> CRule ctx ('Prd prd nt) sc ip ic sp ic' sp
forall (ctx :: [ErrorMessage]) (prd :: Prod)
       (sc :: [(Child, [(Att, *)])]) (ip :: [(Att, *)])
       (ic :: [(Child, [(Att, *)])]) (sp :: [(Att, *)])
       (ic' :: [(Child, [(Att, *)])]) (sp' :: [(Att, *)]).
(Proxy ctx -> Rule prd sc ip ic sp ic' sp')
-> CRule ctx prd sc ip ic sp ic' sp'
CRule ((Proxy ctx -> Rule ('Prd prd nt) sc ip ic sp ic' sp)
 -> CRule ctx ('Prd prd nt) sc ip ic sp ic' sp)
-> (Proxy ctx -> Rule ('Prd prd nt) sc ip ic sp ic' sp)
-> CRule ctx ('Prd prd nt) sc ip ic sp ic' sp
forall a b. (a -> b) -> a -> b
$ \Proxy ctx
ctx Fam ('Prd prd nt) sc ip
inp (Fam ChAttsRec ('Prd prd nt) ic
ic Attribution sp
sp) ->
    let ic' :: ReqR
  (OpUpdate
     (ChiReco ('Prd prd nt)) ('Chi chi ('Prd prd' nt') ntch) v2 ic)
ic' = Proxy ctx
-> OpUpdate
     (ChiReco ('Prd prd nt)) ('Chi chi ('Prd prd' nt') ntch) v2 ic
-> ReqR
     (OpUpdate
        (ChiReco ('Prd prd nt)) ('Chi chi ('Prd prd' nt') ntch) v2 ic)
forall op (ctx :: [ErrorMessage]).
Require op ctx =>
Proxy ctx -> op -> ReqR op
req Proxy ctx
ctx (Label ('Chi chi ('Prd prd' nt') ntch)
-> WrapField (ChiReco ('Prd prd nt)) v2
-> ChAttsRec ('Prd prd nt) ic
-> OpUpdate
     (ChiReco ('Prd prd nt)) ('Chi chi ('Prd prd' nt') ntch) v2 ic
forall k k' (l :: k) c (v :: k') (r :: [(k, k')]).
Label l -> WrapField c v -> Rec c r -> OpUpdate c l v r
OpUpdate Label ('Chi chi ('Prd prd' nt') ntch)
chi WrapField (ChiReco ('Prd prd nt)) v2
ReqR (OpExtend AttReco ('Att att t) t' r)
catts' ChAttsRec ('Prd prd nt) ic
ic)
        catts :: ReqR
  (OpLookup
     (ChiReco ('Prd prd nt)) ('Chi chi ('Prd prd' nt') ntch) ic)
catts = Proxy ctx
-> OpLookup
     (ChiReco ('Prd prd nt)) ('Chi chi ('Prd prd' nt') ntch) ic
-> ReqR
     (OpLookup
        (ChiReco ('Prd prd nt)) ('Chi chi ('Prd prd' nt') ntch) ic)
forall op (ctx :: [ErrorMessage]).
Require op ctx =>
Proxy ctx -> op -> ReqR op
req Proxy ctx
ctx (Label ('Chi chi ('Prd prd' nt') ntch)
-> ChAttsRec ('Prd prd nt) ic
-> OpLookup
     (ChiReco ('Prd prd nt)) ('Chi chi ('Prd prd' nt') ntch) ic
forall k k' (l :: k) c (r :: [(k, k')]).
Label l -> Rec c r -> OpLookup c l r
OpLookup Label ('Chi chi ('Prd prd' nt') ntch)
chi ChAttsRec ('Prd prd nt) ic
ic)
        catts' :: ReqR (OpExtend AttReco ('Att att t) t' r)
catts' = Proxy ctx
-> OpExtend AttReco ('Att att t) t' r
-> ReqR (OpExtend AttReco ('Att att t) t' r)
forall op (ctx :: [ErrorMessage]).
Require op ctx =>
Proxy ctx -> op -> ReqR op
req Proxy ctx
ctx (Label ('Att att t)
-> WrapField AttReco t'
-> Rec AttReco r
-> OpExtend AttReco ('Att att t) t' r
forall k k' (l :: k) c (v :: k') (r :: [(k, k')]).
Label l -> WrapField c v -> Rec c r -> OpExtend c l v r
OpExtend Label ('Att att t)
att (Proxy ctx -> Fam ('Prd prd nt) sc ip -> t'
f Proxy ctx
forall k (t :: k). Proxy t
Proxy Fam ('Prd prd nt) sc ip
inp) Rec AttReco r
ReqR
  (OpLookup
     (ChiReco ('Prd prd nt)) ('Chi chi ('Prd prd' nt') ntch) ic)
catts)
     in ChAttsRec ('Prd prd nt) ic'
-> Attribution sp -> Fam ('Prd prd nt) ic' sp
forall (prd :: Prod) (c :: [(Child, [(Att, *)])])
       (p :: [(Att, *)]).
ChAttsRec prd c -> Attribution p -> Fam prd c p
Fam ChAttsRec ('Prd prd nt) ic'
ReqR
  (OpUpdate
     (ChiReco ('Prd prd nt)) ('Chi chi ('Prd prd' nt') ntch) v2 ic)
ic' Attribution sp
sp


inhdefM
  :: Inhdef t t' (MkMsg InhdefMsg att t prd nt ': ctx)
       att r v2 prd prd' nt nt' chi ntch ic ic' n
  => Label ('Att att t)
  -> Label ('Prd prd nt)
  -> Label ('Chi chi ('Prd prd' nt') ntch)
  -> Reader (Proxy (MkMsg InhdefMsg att t prd nt ': ctx), Fam ('Prd prd nt) sc ip) t'
  -> CRule ctx ('Prd prd nt) sc ip ic sp ic' sp
inhdefM :: Label ('Att att t)
-> Label ('Prd prd nt)
-> Label ('Chi chi ('Prd prd' nt') ntch)
-> Reader
     (Proxy (MkMsg InhdefMsg att t prd nt : ctx),
      Fam ('Prd prd nt) sc ip)
     t'
-> CRule ctx ('Prd prd nt) sc ip ic sp ic' sp
inhdefM Label ('Att att t)
att Label ('Prd prd nt)
prd Label ('Chi chi ('Prd prd' nt') ntch)
chi Reader
  (Proxy (MkMsg InhdefMsg att t prd nt : ctx),
   Fam ('Prd prd nt) sc ip)
  t'
f = (Proxy ctx
 -> Proxy
      ((('Text "- inhdef: definition of attribute "
         ':<>: 'Text
                 (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
        ':$$: ('Text "   in production "
               ':<>: 'Text
                       (AppendSymbol
                          (AppendSymbol
                             (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                          ")")))
         : ctx))
-> CRule
     ((('Text "- inhdef: definition of attribute "
        ':<>: 'Text
                (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
       ':$$: ('Text "   in production "
              ':<>: 'Text
                      (AppendSymbol
                         (AppendSymbol
                            (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                         ")")))
        : ctx)
     ('Prd prd nt)
     sc
     ip
     ic
     sp
     ic'
     sp
-> CRule ctx ('Prd prd nt) sc ip ic sp ic' sp
forall (ctx :: [ErrorMessage]) (ctx' :: [ErrorMessage])
       (prd :: Prod) (sc :: [(Child, [(Att, *)])]) (ip :: [(Att, *)])
       (ic :: [(Child, [(Att, *)])]) (sp :: [(Att, *)])
       (ic' :: [(Child, [(Att, *)])]) (sp' :: [(Att, *)]).
(Proxy ctx -> Proxy ctx')
-> CRule ctx' prd sc ip ic sp ic' sp'
-> CRule ctx prd sc ip ic sp ic' sp'
mapCRule (Proxy InhdefMsg
-> Label ('Att att t)
-> Label ('Prd prd nt)
-> Proxy (MkMsg InhdefMsg att t prd nt)
forall msg (att :: Symbol) t (prd :: Symbol) (nt :: NT).
Proxy msg
-> Label ('Att att t)
-> Label ('Prd prd nt)
-> Proxy (MkMsg msg att t prd nt)
mkMsg (Proxy InhdefMsg
forall k (t :: k). Proxy t
Proxy @InhdefMsg) Label ('Att att t)
att Label ('Prd prd nt)
prd Proxy
  (('Text "- inhdef: definition of attribute "
    ':<>: 'Text
            (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
   ':$$: ('Text "   in production "
          ':<>: 'Text
                  (AppendSymbol
                     (AppendSymbol
                        (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                     ")")))
-> Proxy ctx
-> Proxy
     ((('Text "- inhdef: definition of attribute "
        ':<>: 'Text
                (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
       ':$$: ('Text "   in production "
              ':<>: 'Text
                      (AppendSymbol
                         (AppendSymbol
                            (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                         ")")))
        : ctx)
forall a (e :: a) (es :: [a]).
Proxy e -> Proxy es -> Proxy (e : es)
`consErr`)
    (CRule
   ((('Text "- inhdef: definition of attribute "
      ':<>: 'Text
              (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
     ':$$: ('Text "   in production "
            ':<>: 'Text
                    (AppendSymbol
                       (AppendSymbol
                          (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                       ")")))
      : ctx)
   ('Prd prd nt)
   sc
   ip
   ic
   sp
   ic'
   sp
 -> CRule ctx ('Prd prd nt) sc ip ic sp ic' sp)
-> CRule
     ((('Text "- inhdef: definition of attribute "
        ':<>: 'Text
                (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
       ':$$: ('Text "   in production "
              ':<>: 'Text
                      (AppendSymbol
                         (AppendSymbol
                            (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                         ")")))
        : ctx)
     ('Prd prd nt)
     sc
     ip
     ic
     sp
     ic'
     sp
-> CRule ctx ('Prd prd nt) sc ip ic sp ic' sp
forall a b. (a -> b) -> a -> b
$ (Label ('Att att t)
-> Label ('Prd prd nt)
-> Label ('Chi chi ('Prd prd' nt') ntch)
-> (Proxy
      ((('Text "- inhdef: definition of attribute "
         ':<>: 'Text
                 (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
        ':$$: ('Text "   in production "
               ':<>: 'Text
                       (AppendSymbol
                          (AppendSymbol
                             (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                          ")")))
         : ctx)
    -> Fam ('Prd prd nt) sc ip -> t')
-> forall (sp :: [(Att, *)]).
   CRule
     ((('Text "- inhdef: definition of attribute "
        ':<>: 'Text
                (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
       ':$$: ('Text "   in production "
              ':<>: 'Text
                      (AppendSymbol
                         (AppendSymbol
                            (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                         ")")))
        : ctx)
     ('Prd prd nt)
     sc
     ip
     ic
     sp
     ic'
     sp
forall k t t' (ctx :: [ErrorMessage]) (att :: Symbol)
       (r :: [(Att, *)]) (v2 :: [(Att, *)]) (prd :: Symbol)
       (prd' :: Symbol) (nt :: NT) (nt' :: NT) (chi :: Symbol)
       (ntch :: Either NT T) (ic :: [(Child, [(Att, *)])])
       (ic' :: [(Child, [(Att, *)])]) (n :: k)
       (sc :: [(Child, [(Att, *)])]) (ip :: [(Att, *)]).
Inhdef t t' ctx att r v2 prd prd' nt nt' chi ntch ic ic' n =>
Label ('Att att t)
-> Label ('Prd prd nt)
-> Label ('Chi chi ('Prd prd' nt') ntch)
-> (Proxy ctx -> Fam ('Prd prd nt) sc ip -> t')
-> forall (sp :: [(Att, *)]).
   CRule ctx ('Prd prd nt) sc ip ic sp ic' sp
inhdef Label ('Att att t)
att Label ('Prd prd nt)
prd Label ('Chi chi ('Prd prd' nt') ntch)
chi ((Proxy
    ((('Text "- inhdef: definition of attribute "
       ':<>: 'Text
               (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
      ':$$: ('Text "   in production "
             ':<>: 'Text
                     (AppendSymbol
                        (AppendSymbol
                           (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                        ")")))
       : ctx)
  -> Fam ('Prd prd nt) sc ip -> t')
 -> CRule
      ((('Text "- inhdef: definition of attribute "
         ':<>: 'Text
                 (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
        ':$$: ('Text "   in production "
               ':<>: 'Text
                       (AppendSymbol
                          (AppendSymbol
                             (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                          ")")))
         : ctx)
      ('Prd prd nt)
      sc
      ip
      ic
      sp
      ic'
      sp)
-> (Reader
      (Proxy
         ((('Text "- inhdef: definition of attribute "
            ':<>: 'Text
                    (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
           ':$$: ('Text "   in production "
                  ':<>: 'Text
                          (AppendSymbol
                             (AppendSymbol
                                (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                             ")")))
            : ctx),
       Fam ('Prd prd nt) sc ip)
      t'
    -> Proxy
         ((('Text "- inhdef: definition of attribute "
            ':<>: 'Text
                    (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
           ':$$: ('Text "   in production "
                  ':<>: 'Text
                          (AppendSymbol
                             (AppendSymbol
                                (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                             ")")))
            : ctx)
    -> Fam ('Prd prd nt) sc ip
    -> t')
-> Reader
     (Proxy
        ((('Text "- inhdef: definition of attribute "
           ':<>: 'Text
                   (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
          ':$$: ('Text "   in production "
                 ':<>: 'Text
                         (AppendSymbol
                            (AppendSymbol
                               (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                            ")")))
           : ctx),
      Fam ('Prd prd nt) sc ip)
     t'
-> CRule
     ((('Text "- inhdef: definition of attribute "
        ':<>: 'Text
                (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
       ':$$: ('Text "   in production "
              ':<>: 'Text
                      (AppendSymbol
                         (AppendSymbol
                            (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                         ")")))
        : ctx)
     ('Prd prd nt)
     sc
     ip
     ic
     sp
     ic'
     sp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Reader
  (Proxy
     ((('Text "- inhdef: definition of attribute "
        ':<>: 'Text
                (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
       ':$$: ('Text "   in production "
              ':<>: 'Text
                      (AppendSymbol
                         (AppendSymbol
                            (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                         ")")))
        : ctx),
   Fam ('Prd prd nt) sc ip)
  t'
-> Proxy
     ((('Text "- inhdef: definition of attribute "
        ':<>: 'Text
                (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
       ':$$: ('Text "   in production "
              ':<>: 'Text
                      (AppendSymbol
                         (AppendSymbol
                            (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                         ")")))
        : ctx)
-> Fam ('Prd prd nt) sc ip
-> t'
forall a b c. Reader (a, b) c -> a -> b -> c
def) Reader
  (Proxy
     ((('Text "- inhdef: definition of attribute "
        ':<>: 'Text
                (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
       ':$$: ('Text "   in production "
              ':<>: 'Text
                      (AppendSymbol
                         (AppendSymbol
                            (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                         ")")))
        : ctx),
   Fam ('Prd prd nt) sc ip)
  t'
Reader
  (Proxy (MkMsg InhdefMsg att t prd nt : ctx),
   Fam ('Prd prd nt) sc ip)
  t'
f

inh
  :: Inhdef t t' (MkMsg InhdefMsg att t prd nt ': ctx)
       att r v2 prd prd' nt nt' chi ntch ic ic' n
  => Label ('Att att t)
  -> Label ('Prd prd nt)
  -> Label ('Chi chi ('Prd prd' nt') ntch)
  -> Reader (Proxy (MkMsg InhdefMsg att t prd nt ': ctx), Fam ('Prd prd nt) sc ip) t'
  -> CRule ctx ('Prd prd nt) sc ip ic sp ic' sp
inh :: Label ('Att att t)
-> Label ('Prd prd nt)
-> Label ('Chi chi ('Prd prd' nt') ntch)
-> Reader
     (Proxy (MkMsg InhdefMsg att t prd nt : ctx),
      Fam ('Prd prd nt) sc ip)
     t'
-> CRule ctx ('Prd prd nt) sc ip ic sp ic' sp
inh Label ('Att att t)
att Label ('Prd prd nt)
prd Label ('Chi chi ('Prd prd' nt') ntch)
chi Reader
  (Proxy (MkMsg InhdefMsg att t prd nt : ctx),
   Fam ('Prd prd nt) sc ip)
  t'
f = (Proxy ctx
 -> Proxy
      ((('Text "- inhdef: definition of attribute "
         ':<>: 'Text
                 (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
        ':$$: ('Text "   in production "
               ':<>: 'Text
                       (AppendSymbol
                          (AppendSymbol
                             (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                          ")")))
         : ctx))
-> CRule
     ((('Text "- inhdef: definition of attribute "
        ':<>: 'Text
                (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
       ':$$: ('Text "   in production "
              ':<>: 'Text
                      (AppendSymbol
                         (AppendSymbol
                            (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                         ")")))
        : ctx)
     ('Prd prd nt)
     sc
     ip
     ic
     sp
     ic'
     sp
-> CRule ctx ('Prd prd nt) sc ip ic sp ic' sp
forall (ctx :: [ErrorMessage]) (ctx' :: [ErrorMessage])
       (prd :: Prod) (sc :: [(Child, [(Att, *)])]) (ip :: [(Att, *)])
       (ic :: [(Child, [(Att, *)])]) (sp :: [(Att, *)])
       (ic' :: [(Child, [(Att, *)])]) (sp' :: [(Att, *)]).
(Proxy ctx -> Proxy ctx')
-> CRule ctx' prd sc ip ic sp ic' sp'
-> CRule ctx prd sc ip ic sp ic' sp'
mapCRule (Proxy InhdefMsg
-> Label ('Att att t)
-> Label ('Prd prd nt)
-> Proxy (MkMsg InhdefMsg att t prd nt)
forall msg (att :: Symbol) t (prd :: Symbol) (nt :: NT).
Proxy msg
-> Label ('Att att t)
-> Label ('Prd prd nt)
-> Proxy (MkMsg msg att t prd nt)
mkMsg (Proxy InhdefMsg
forall k (t :: k). Proxy t
Proxy @InhdefMsg) Label ('Att att t)
att Label ('Prd prd nt)
prd Proxy
  (('Text "- inhdef: definition of attribute "
    ':<>: 'Text
            (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
   ':$$: ('Text "   in production "
          ':<>: 'Text
                  (AppendSymbol
                     (AppendSymbol
                        (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                     ")")))
-> Proxy ctx
-> Proxy
     ((('Text "- inhdef: definition of attribute "
        ':<>: 'Text
                (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
       ':$$: ('Text "   in production "
              ':<>: 'Text
                      (AppendSymbol
                         (AppendSymbol
                            (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                         ")")))
        : ctx)
forall a (e :: a) (es :: [a]).
Proxy e -> Proxy es -> Proxy (e : es)
`consErr`)
    (CRule
   ((('Text "- inhdef: definition of attribute "
      ':<>: 'Text
              (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
     ':$$: ('Text "   in production "
            ':<>: 'Text
                    (AppendSymbol
                       (AppendSymbol
                          (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                       ")")))
      : ctx)
   ('Prd prd nt)
   sc
   ip
   ic
   sp
   ic'
   sp
 -> CRule ctx ('Prd prd nt) sc ip ic sp ic' sp)
-> CRule
     ((('Text "- inhdef: definition of attribute "
        ':<>: 'Text
                (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
       ':$$: ('Text "   in production "
              ':<>: 'Text
                      (AppendSymbol
                         (AppendSymbol
                            (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                         ")")))
        : ctx)
     ('Prd prd nt)
     sc
     ip
     ic
     sp
     ic'
     sp
-> CRule ctx ('Prd prd nt) sc ip ic sp ic' sp
forall a b. (a -> b) -> a -> b
$ (Label ('Att att t)
-> Label ('Prd prd nt)
-> Label ('Chi chi ('Prd prd' nt') ntch)
-> (Proxy
      ((('Text "- inhdef: definition of attribute "
         ':<>: 'Text
                 (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
        ':$$: ('Text "   in production "
               ':<>: 'Text
                       (AppendSymbol
                          (AppendSymbol
                             (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                          ")")))
         : ctx)
    -> Fam ('Prd prd nt) sc ip -> t')
-> forall (sp :: [(Att, *)]).
   CRule
     ((('Text "- inhdef: definition of attribute "
        ':<>: 'Text
                (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
       ':$$: ('Text "   in production "
              ':<>: 'Text
                      (AppendSymbol
                         (AppendSymbol
                            (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                         ")")))
        : ctx)
     ('Prd prd nt)
     sc
     ip
     ic
     sp
     ic'
     sp
forall k t t' (ctx :: [ErrorMessage]) (att :: Symbol)
       (r :: [(Att, *)]) (v2 :: [(Att, *)]) (prd :: Symbol)
       (prd' :: Symbol) (nt :: NT) (nt' :: NT) (chi :: Symbol)
       (ntch :: Either NT T) (ic :: [(Child, [(Att, *)])])
       (ic' :: [(Child, [(Att, *)])]) (n :: k)
       (sc :: [(Child, [(Att, *)])]) (ip :: [(Att, *)]).
Inhdef t t' ctx att r v2 prd prd' nt nt' chi ntch ic ic' n =>
Label ('Att att t)
-> Label ('Prd prd nt)
-> Label ('Chi chi ('Prd prd' nt') ntch)
-> (Proxy ctx -> Fam ('Prd prd nt) sc ip -> t')
-> forall (sp :: [(Att, *)]).
   CRule ctx ('Prd prd nt) sc ip ic sp ic' sp
inhdef Label ('Att att t)
att Label ('Prd prd nt)
prd Label ('Chi chi ('Prd prd' nt') ntch)
chi ((Proxy
    ((('Text "- inhdef: definition of attribute "
       ':<>: 'Text
               (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
      ':$$: ('Text "   in production "
             ':<>: 'Text
                     (AppendSymbol
                        (AppendSymbol
                           (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                        ")")))
       : ctx)
  -> Fam ('Prd prd nt) sc ip -> t')
 -> CRule
      ((('Text "- inhdef: definition of attribute "
         ':<>: 'Text
                 (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
        ':$$: ('Text "   in production "
               ':<>: 'Text
                       (AppendSymbol
                          (AppendSymbol
                             (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                          ")")))
         : ctx)
      ('Prd prd nt)
      sc
      ip
      ic
      sp
      ic'
      sp)
-> (Reader
      (Proxy
         ((('Text "- inhdef: definition of attribute "
            ':<>: 'Text
                    (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
           ':$$: ('Text "   in production "
                  ':<>: 'Text
                          (AppendSymbol
                             (AppendSymbol
                                (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                             ")")))
            : ctx),
       Fam ('Prd prd nt) sc ip)
      t'
    -> Proxy
         ((('Text "- inhdef: definition of attribute "
            ':<>: 'Text
                    (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
           ':$$: ('Text "   in production "
                  ':<>: 'Text
                          (AppendSymbol
                             (AppendSymbol
                                (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                             ")")))
            : ctx)
    -> Fam ('Prd prd nt) sc ip
    -> t')
-> Reader
     (Proxy
        ((('Text "- inhdef: definition of attribute "
           ':<>: 'Text
                   (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
          ':$$: ('Text "   in production "
                 ':<>: 'Text
                         (AppendSymbol
                            (AppendSymbol
                               (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                            ")")))
           : ctx),
      Fam ('Prd prd nt) sc ip)
     t'
-> CRule
     ((('Text "- inhdef: definition of attribute "
        ':<>: 'Text
                (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
       ':$$: ('Text "   in production "
              ':<>: 'Text
                      (AppendSymbol
                         (AppendSymbol
                            (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                         ")")))
        : ctx)
     ('Prd prd nt)
     sc
     ip
     ic
     sp
     ic'
     sp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Reader
  (Proxy
     ((('Text "- inhdef: definition of attribute "
        ':<>: 'Text
                (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
       ':$$: ('Text "   in production "
              ':<>: 'Text
                      (AppendSymbol
                         (AppendSymbol
                            (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                         ")")))
        : ctx),
   Fam ('Prd prd nt) sc ip)
  t'
-> Proxy
     ((('Text "- inhdef: definition of attribute "
        ':<>: 'Text
                (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
       ':$$: ('Text "   in production "
              ':<>: 'Text
                      (AppendSymbol
                         (AppendSymbol
                            (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                         ")")))
        : ctx)
-> Fam ('Prd prd nt) sc ip
-> t'
forall a b c. Reader (a, b) c -> a -> b -> c
def) Reader
  (Proxy
     ((('Text "- inhdef: definition of attribute "
        ':<>: 'Text
                (AppendSymbol (AppendSymbol (AppendSymbol "(" att) ":") ")"))
       ':$$: ('Text "   in production "
              ':<>: 'Text
                      (AppendSymbol
                         (AppendSymbol
                            (AppendSymbol (AppendSymbol "(" prd) " of ") (FromEM (ShowTE nt)))
                         ")")))
        : ctx),
   Fam ('Prd prd nt) sc ip)
  t'
Reader
  (Proxy (MkMsg InhdefMsg att t prd nt : ctx),
   Fam ('Prd prd nt) sc ip)
  t'
f


inhmod
  :: ( RequireEq t t' ctx'
     , RequireR (OpUpdate AttReco ('Att att t) t' r) ctx
                (Attribution v2)
     , RequireR (OpUpdate (ChiReco ('Prd prd nt))
                ('Chi chi ('Prd prd nt) ntch) v2 ic) ctx
                (ChAttsRec ('Prd prd nt) ic')
     , RequireR (OpLookup (ChiReco ('Prd prd nt))
                ('Chi chi ('Prd prd nt) ntch) ic) ctx
                (Attribution r)
     , ntch ~ ('Left n)
     , ctx' ~ ((Text "inhmod("
                :<>: ShowTE ('Att att t)  :<>: Text ", "
                :<>: ShowTE ('Prd prd nt) :<>: Text ", "
                :<>: ShowTE ('Chi chi ('Prd prd nt) ntch) :<>: Text ")")
                ': ctx))
     =>
     Label ('Att att t)
     -> Label ('Prd prd nt)
     -> Label ('Chi chi ('Prd prd nt) ntch)
     -> (Proxy ctx' -> Fam ('Prd prd nt) sc ip -> t')
     -> CRule ctx ('Prd prd nt) sc ip ic sp ic' sp
inhmod :: Label ('Att att t)
-> Label ('Prd prd nt)
-> Label ('Chi chi ('Prd prd nt) ntch)
-> (Proxy ctx' -> Fam ('Prd prd nt) sc ip -> t')
-> CRule ctx ('Prd prd nt) sc ip ic sp ic' sp
inhmod Label ('Att att t)
att Label ('Prd prd nt)
prd Label ('Chi chi ('Prd prd nt) ntch)
chi Proxy ctx' -> Fam ('Prd prd nt) sc ip -> t'
f
  = (Proxy ctx -> Rule ('Prd prd nt) sc ip ic sp ic' sp)
-> CRule ctx ('Prd prd nt) sc ip ic sp ic' sp
forall (ctx :: [ErrorMessage]) (prd :: Prod)
       (sc :: [(Child, [(Att, *)])]) (ip :: [(Att, *)])
       (ic :: [(Child, [(Att, *)])]) (sp :: [(Att, *)])
       (ic' :: [(Child, [(Att, *)])]) (sp' :: [(Att, *)]).
(Proxy ctx -> Rule prd sc ip ic sp ic' sp')
-> CRule ctx prd sc ip ic sp ic' sp'
CRule ((Proxy ctx -> Rule ('Prd prd nt) sc ip ic sp ic' sp)
 -> CRule ctx ('Prd prd nt) sc ip ic sp ic' sp)
-> (Proxy ctx -> Rule ('Prd prd nt) sc ip ic sp ic' sp)
-> CRule ctx ('Prd prd nt) sc ip ic sp ic' sp
forall a b. (a -> b) -> a -> b
$ \Proxy ctx
ctx Fam ('Prd prd nt) sc ip
inp (Fam ChAttsRec ('Prd prd nt) ic
ic Attribution sp
sp)
       -> let ic' :: ReqR
  (OpUpdate
     (ChiReco ('Prd prd nt)) ('Chi chi ('Prd prd nt) ntch) v2 ic)
ic'   = Proxy ctx
-> OpUpdate
     (ChiReco ('Prd prd nt)) ('Chi chi ('Prd prd nt) ntch) v2 ic
-> ReqR
     (OpUpdate
        (ChiReco ('Prd prd nt)) ('Chi chi ('Prd prd nt) ntch) v2 ic)
forall op (ctx :: [ErrorMessage]).
Require op ctx =>
Proxy ctx -> op -> ReqR op
req Proxy ctx
ctx (Label ('Chi chi ('Prd prd nt) ntch)
-> WrapField (ChiReco ('Prd prd nt)) v2
-> ChAttsRec ('Prd prd nt) ic
-> OpUpdate
     (ChiReco ('Prd prd nt)) ('Chi chi ('Prd prd nt) ntch) v2 ic
forall k k' (l :: k) c (v :: k') (r :: [(k, k')]).
Label l -> WrapField c v -> Rec c r -> OpUpdate c l v r
OpUpdate Label ('Chi chi ('Prd prd nt) ntch)
chi WrapField (ChiReco ('Prd prd nt)) v2
ReqR (OpUpdate AttReco ('Att att t) t' r)
catts' ChAttsRec ('Prd prd nt) ic
ic)
              catts :: ReqR
  (OpLookup (ChiReco ('Prd prd nt)) ('Chi chi ('Prd prd nt) ntch) ic)
catts = Proxy ctx
-> OpLookup
     (ChiReco ('Prd prd nt)) ('Chi chi ('Prd prd nt) ntch) ic
-> ReqR
     (OpLookup (ChiReco ('Prd prd nt)) ('Chi chi ('Prd prd nt) ntch) ic)
forall op (ctx :: [ErrorMessage]).
Require op ctx =>
Proxy ctx -> op -> ReqR op
req Proxy ctx
ctx (Label ('Chi chi ('Prd prd nt) ntch)
-> ChAttsRec ('Prd prd nt) ic
-> OpLookup
     (ChiReco ('Prd prd nt)) ('Chi chi ('Prd prd nt) ntch) ic
forall k k' (l :: k) c (r :: [(k, k')]).
Label l -> Rec c r -> OpLookup c l r
OpLookup  Label ('Chi chi ('Prd prd nt) ntch)
chi ChAttsRec ('Prd prd nt) ic
ic)
              catts' :: ReqR (OpUpdate AttReco ('Att att t) t' r)
catts'= Proxy ctx
-> OpUpdate AttReco ('Att att t) t' r
-> ReqR (OpUpdate AttReco ('Att att t) t' r)
forall op (ctx :: [ErrorMessage]).
Require op ctx =>
Proxy ctx -> op -> ReqR op
req Proxy ctx
ctx (Label ('Att att t)
-> WrapField AttReco t'
-> Rec AttReco r
-> OpUpdate AttReco ('Att att t) t' r
forall k k' (l :: k) c (v :: k') (r :: [(k, k')]).
Label l -> WrapField c v -> Rec c r -> OpUpdate c l v r
OpUpdate  Label ('Att att t)
att (Proxy ctx' -> Fam ('Prd prd nt) sc ip -> t'
f Proxy ctx'
forall k (t :: k). Proxy t
Proxy Fam ('Prd prd nt) sc ip
inp) Rec AttReco r
ReqR
  (OpLookup (ChiReco ('Prd prd nt)) ('Chi chi ('Prd prd nt) ntch) ic)
catts)
          in  ChAttsRec ('Prd prd nt) ic'
-> Attribution sp -> Fam ('Prd prd nt) ic' sp
forall (prd :: Prod) (c :: [(Child, [(Att, *)])])
       (p :: [(Att, *)]).
ChAttsRec prd c -> Attribution p -> Fam prd c p
Fam ChAttsRec ('Prd prd nt) ic'
ReqR
  (OpUpdate
     (ChiReco ('Prd prd nt)) ('Chi chi ('Prd prd nt) ntch) v2 ic)
ic' Attribution sp
sp


inhmodM
  :: ( RequireEq t t' ctx'
     , RequireR (OpUpdate AttReco ('Att att t) t' r) ctx
                (Attribution v2)
     , RequireR (OpUpdate (ChiReco ('Prd prd nt))
                ('Chi chi ('Prd prd nt) ntch) v2 ic) ctx
                (ChAttsRec ('Prd prd nt) ic')
     , RequireR (OpLookup (ChiReco ('Prd prd nt))
                ('Chi chi ('Prd prd nt) ntch) ic) ctx
                (Attribution r)
     , ntch ~ ('Left n)
     , ctx' ~ ((Text "inhmod("
                :<>: ShowTE ('Att att t)  :<>: Text ", "
                :<>: ShowTE ('Prd prd nt) :<>: Text ", "
                :<>: ShowTE ('Chi chi ('Prd prd nt) ntch) :<>: Text ")")
                ': ctx))
     =>
     Label ('Att att t)
     -> Label ('Prd prd nt)
     -> Label ('Chi chi ('Prd prd nt) ntch)
     -> Reader (Proxy ctx', Fam ('Prd prd nt) sc ip) t'
     -> CRule ctx ('Prd prd nt) sc ip ic sp ic' sp
inhmodM :: Label ('Att att t)
-> Label ('Prd prd nt)
-> Label ('Chi chi ('Prd prd nt) ntch)
-> Reader (Proxy ctx', Fam ('Prd prd nt) sc ip) t'
-> CRule ctx ('Prd prd nt) sc ip ic sp ic' sp
inhmodM Label ('Att att t)
att Label ('Prd prd nt)
prd Label ('Chi chi ('Prd prd nt) ntch)
chi = Label ('Att att t)
-> Label ('Prd prd nt)
-> Label ('Chi chi ('Prd prd nt) ntch)
-> (Proxy ctx' -> Fam ('Prd prd nt) sc ip -> t')
-> CRule ctx ('Prd prd nt) sc ip ic sp ic' sp
forall t t' (ctx' :: [ErrorMessage]) (att :: Symbol)
       (r :: [(Att, *)]) (ctx :: [ErrorMessage]) (v2 :: [(Att, *)])
       (prd :: Symbol) (nt :: NT) (chi :: Symbol) (ntch :: Either NT T)
       (ic :: [(Child, [(Att, *)])]) (ic' :: [(Child, [(Att, *)])])
       (n :: NT) (sc :: [(Child, [(Att, *)])]) (ip :: [(Att, *)])
       (sp :: [(Att, *)]).
(RequireEq t t' ctx',
 RequireR (OpUpdate AttReco ('Att att t) t' r) ctx (Attribution v2),
 RequireR
   (OpUpdate
      (ChiReco ('Prd prd nt)) ('Chi chi ('Prd prd nt) ntch) v2 ic)
   ctx
   (ChAttsRec ('Prd prd nt) ic'),
 RequireR
   (OpLookup (ChiReco ('Prd prd nt)) ('Chi chi ('Prd prd nt) ntch) ic)
   ctx
   (Attribution r),
 ntch ~ 'Left n,
 ctx'
 ~ ((((((('Text "inhmod(" ':<>: ShowTE ('Att att t))
         ':<>: 'Text ", ")
        ':<>: ShowTE ('Prd prd nt))
       ':<>: 'Text ", ")
      ':<>: ShowTE ('Chi chi ('Prd prd nt) ntch))
     ':<>: 'Text ")")
      : ctx)) =>
Label ('Att att t)
-> Label ('Prd prd nt)
-> Label ('Chi chi ('Prd prd nt) ntch)
-> (Proxy ctx' -> Fam ('Prd prd nt) sc ip -> t')
-> CRule ctx ('Prd prd nt) sc ip ic sp ic' sp
inhmod Label ('Att att t)
att Label ('Prd prd nt)
prd Label ('Chi chi ('Prd prd nt) ntch)
chi ((Proxy ctx' -> Fam ('Prd prd nt) sc ip -> t')
 -> CRule ctx ('Prd prd nt) sc ip ic sp ic' sp)
-> (Reader (Proxy ctx', Fam ('Prd prd nt) sc ip) t'
    -> Proxy ctx' -> Fam ('Prd prd nt) sc ip -> t')
-> Reader (Proxy ctx', Fam ('Prd prd nt) sc ip) t'
-> CRule ctx ('Prd prd nt) sc ip ic sp ic' sp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Reader (Proxy ctx', Fam ('Prd prd nt) sc ip) t'
-> Proxy ctx' -> Fam ('Prd prd nt) sc ip -> t'
forall a b c. Reader (a, b) c -> a -> b -> c
def

data Lhs
lhs :: Label Lhs
lhs :: Label Lhs
lhs = Label Lhs
forall k (l :: k). Label l
Label

class Monad m => At pos att m where
 type ResAt pos att m
 at :: Label pos -> Label att -> m (ResAt pos att m)


instance ( RequireR (OpLookup (ChiReco prd') ('Chi ch prd nt) chi) ctx
                    (Attribution r)
         , RequireR (OpLookup AttReco ('Att att t) r) ctx t'
         , RequireEqWithMsg prd prd' PrdTypeMatch ctx
         , RequireEqWithMsg t t' GetAttTypeMatch ctx
         , ReqR (OpLookup @Att @Type AttReco ('Att att t')
                 (UnWrap @Att @Type (Rec AttReco r)))
           ~ t'         
         , r ~ UnWrap (Attribution r)
         )
      => At ('Chi ch prd nt) ('Att att t)
            (Reader (Proxy ctx, Fam prd' chi par))  where
 type ResAt ('Chi ch prd nt) ('Att att t) (Reader (Proxy ctx, Fam prd' chi par))
         = ReqR (OpLookup AttReco ('Att att t)
                 (UnWrap @Att @Type (ReqR (OpLookup (ChiReco prd) ('Chi ch prd nt) chi))))
 at :: Label ('Chi ch prd nt)
-> Label ('Att att t)
-> Reader
     (Proxy ctx, Fam prd' chi par)
     (ResAt
        ('Chi ch prd nt)
        ('Att att t)
        (Reader (Proxy ctx, Fam prd' chi par)))
at Label ('Chi ch prd nt)
ch Label ('Att att t)
att
  = ((Proxy ctx, Fam prd' chi par) -> t')
-> ReaderT
     (Proxy ctx, Fam prd' chi par)
     Identity
     (Proxy ctx, Fam prd' chi par)
-> ReaderT (Proxy ctx, Fam prd' chi par) Identity t'
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (\(Proxy ctx
ctx, Fam ChAttsRec prd' chi
chi Attribution par
_)  -> let atts :: ReqR (OpLookup (ChiReco prd') ('Chi ch prd nt) chi)
atts = Proxy ctx
-> OpLookup (ChiReco prd') ('Chi ch prd nt) chi
-> ReqR (OpLookup (ChiReco prd') ('Chi ch prd nt) chi)
forall op (ctx :: [ErrorMessage]).
Require op ctx =>
Proxy ctx -> op -> ReqR op
req Proxy ctx
ctx (Label ('Chi ch prd nt)
-> ChAttsRec prd' chi
-> OpLookup (ChiReco prd') ('Chi ch prd nt) chi
forall k k' (l :: k) c (r :: [(k, k')]).
Label l -> Rec c r -> OpLookup c l r
OpLookup Label ('Chi ch prd nt)
ch ChAttsRec prd' chi
chi)
                                 in  Proxy ctx
-> OpLookup AttReco ('Att att t) r
-> ReqR (OpLookup AttReco ('Att att t) r)
forall op (ctx :: [ErrorMessage]).
Require op ctx =>
Proxy ctx -> op -> ReqR op
req Proxy ctx
ctx (Label ('Att att t)
-> Attribution r -> OpLookup AttReco ('Att att t) r
forall k k' (l :: k) c (r :: [(k, k')]).
Label l -> Rec c r -> OpLookup c l r
OpLookup Label ('Att att t)
att Attribution r
ReqR (OpLookup (ChiReco prd') ('Chi ch prd nt) chi)
atts))
          ReaderT
  (Proxy ctx, Fam prd' chi par)
  Identity
  (Proxy ctx, Fam prd' chi par)
forall r (m :: * -> *). MonadReader r m => m r
ask



instance
  ( RequireR (OpLookup @Att @Type AttReco ('Att att t) par) ctx t
  , RequireEqWithMsg t t' AttTypeMatch ctx
  )
  =>
  At Lhs ('Att att t) (Reader (Proxy ctx, Fam prd chi par))  where
  type ResAt Lhs ('Att att t) (Reader (Proxy ctx, Fam prd chi par))
    = ReqR (OpLookup @Att @Type AttReco ('Att att t) (UnWrap @Att @Type (Rec AttReco par)))
  at :: Label Lhs
-> Label ('Att att t)
-> Reader
     (Proxy ctx, Fam prd chi par)
     (ResAt Lhs ('Att att t) (Reader (Proxy ctx, Fam prd chi par)))
at Label Lhs
lhs Label ('Att att t)
att
    = ((Proxy ctx, Fam prd chi par) -> t')
-> ReaderT
     (Proxy ctx, Fam prd chi par) Identity (Proxy ctx, Fam prd chi par)
-> ReaderT (Proxy ctx, Fam prd chi par) Identity t'
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (\(Proxy ctx
ctx, Fam ChAttsRec prd chi
_ Attribution par
par) -> Proxy ctx
-> OpLookup AttReco ('Att att t) par
-> ReqR (OpLookup AttReco ('Att att t) par)
forall op (ctx :: [ErrorMessage]).
Require op ctx =>
Proxy ctx -> op -> ReqR op
req Proxy ctx
ctx (Label ('Att att t)
-> Attribution par -> OpLookup AttReco ('Att att t) par
forall k k' (l :: k) c (r :: [(k, k')]).
Label l -> Rec c r -> OpLookup c l r
OpLookup Label ('Att att t)
att Attribution par
par)) ReaderT
  (Proxy ctx, Fam prd chi par) Identity (Proxy ctx, Fam prd chi par)
forall r (m :: * -> *). MonadReader r m => m r
ask

def :: Reader (a, b) c -> a -> b -> c
def = ((a, b) -> c) -> a -> b -> c
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (((a, b) -> c) -> a -> b -> c)
-> (Reader (a, b) c -> (a, b) -> c)
-> Reader (a, b) c
-> a
-> b
-> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Reader (a, b) c -> (a, b) -> c
forall r a. Reader r a -> r -> a
runReader

ter :: ( RequireR (OpLookup (ChiReco prd) pos chi) ctx
                  (Attribution r)
       , RequireR (OpLookup AttReco ('Att "term" t) r) ctx t
       , RequireEqWithMsg prd prd' PrdTypeMatch ctx
       , ReqR (OpLookup AttReco ('Att "term" t) (UnWrap @Att @Type (Attribution r)))
                        ~ t
       , RequireEq pos ('Chi ch prd rtt) ctx
       , RequireEq rtt (Right ('T t)) ctx)
    =>  Label pos -> Reader (Proxy ctx, Fam prd' chi par) t
ter :: Label pos -> Reader (Proxy ctx, Fam prd' chi par) t
ter (ch :: Label ('Chi ch prd rtt))
  = ((Proxy ctx, Fam prd' chi par) -> t)
-> ReaderT
     (Proxy ctx, Fam prd' chi par)
     Identity
     (Proxy ctx, Fam prd' chi par)
-> Reader (Proxy ctx, Fam prd' chi par) t
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (\(Proxy ctx
ctx, Fam ChAttsRec prd' chi
chi Attribution par
_)  ->
    let atts :: ReqR (OpLookup (ChiReco prd') ('Chi ch prd' ('Right ('T t))) chi)
atts = Proxy ctx
-> OpLookup (ChiReco prd') ('Chi ch prd' ('Right ('T t))) chi
-> ReqR
     (OpLookup (ChiReco prd') ('Chi ch prd' ('Right ('T t))) chi)
forall op (ctx :: [ErrorMessage]).
Require op ctx =>
Proxy ctx -> op -> ReqR op
req Proxy ctx
ctx (Label ('Chi ch prd' ('Right ('T t)))
-> ChAttsRec prd' chi
-> OpLookup (ChiReco prd') ('Chi ch prd' ('Right ('T t))) chi
forall k k' (l :: k) c (r :: [(k, k')]).
Label l -> Rec c r -> OpLookup c l r
OpLookup Label ('Chi ch prd' ('Right ('T t)))
ch ChAttsRec prd' chi
chi)
    in  Proxy ctx
-> OpLookup AttReco ('Att "term" t) r
-> ReqR (OpLookup AttReco ('Att "term" t) r)
forall op (ctx :: [ErrorMessage]).
Require op ctx =>
Proxy ctx -> op -> ReqR op
req Proxy ctx
ctx (Label ('Att "term" t)
-> Rec AttReco r -> OpLookup AttReco ('Att "term" t) r
forall k k' (l :: k) c (r :: [(k, k')]).
Label l -> Rec c r -> OpLookup c l r
OpLookup (SemLit (FromT (FromRight ('Right ('T t)))) =>
Label ('Att "term" (FromT (FromRight ('Right ('T t)))))
forall a. SemLit a => Label ('Att "term" a)
lit @(FromT (FromRight rtt))) Rec AttReco r
ReqR (OpLookup (ChiReco prd') ('Chi ch prd' ('Right ('T t))) chi)
atts))
          ReaderT
  (Proxy ctx, Fam prd' chi par)
  Identity
  (Proxy ctx, Fam prd' chi par)
forall r (m :: * -> *). MonadReader r m => m r
ask

type family FromRight (t :: Either a b) :: b where
     FromRight (Right t) = t

type family FromT (t :: T) :: b where
     FromT ('T t) = t


-- ter :: ( RequireR (OpLookup (ChiReco prd) pos chi) ctx
--                   (Attribution r)
--        , RequireR (OpLookup AttReco ('Att "term" t) r) ctx t
--        , RequireEqWithMsg prd prd' PrdTypeMatch ctx
--        , ReqR (OpLookup AttReco ('Att "term" t) (UnWrap @Att @Type (Attribution r)))
--                         ~ t
--        , RequireEq pos ('Chi ch prd (Right ('T t))) ctx
--        , m ~ Reader (Proxy ctx, Fam prd' chi par) )
--     =>  Label pos -> m t -- (ResAt pos ('Att "term" t) m) 
-- ter (ch :: Label ('Chi ch prd (Right ('T t))))
--   = liftM (\(ctx, Fam chi _)  -> let atts = req ctx (OpLookup ch chi)
--                                  in  req ctx (OpLookup (lit @ t) atts))
--           ask


type instance (UnWrap (Attribution r)) = r
type instance (UnWrap @Att @Type (Rec c r)) = r


class Kn (fcr :: [(Child, Type)]) (prd :: Prod) where
  type ICh fcr :: [(Child, [(Att, Type)])]
  type SCh fcr :: [(Child, [(Att, Type)])]
  kn :: Record fcr -> ChAttsRec prd (ICh fcr) -> ChAttsRec prd (SCh fcr)

instance Kn '[] prod where
  type ICh '[] = '[]
  type SCh '[] = '[] 
  kn :: Record '[] -> ChAttsRec prod (ICh '[]) -> ChAttsRec prod (SCh '[])
kn Record '[]
_ ChAttsRec prod (ICh '[])
_ = ChAttsRec prod (SCh '[])
forall (prd :: Prod). ChAttsRec prd '[]
emptyCh

instance
  Kn fc prd
  =>
  Kn ( '(lch , Attribution ich -> Attribution sch) ': fc) prd where
  type ICh ( '(lch , Attribution ich -> Attribution sch) ': fc)
    = '(lch , ich) ': ICh fc
  type SCh ( '(lch , Attribution ich -> Attribution sch) ': fc)
    = '(lch , sch) ': SCh fc
  kn :: Record ('(lch, Attribution ich -> Attribution sch) : fc)
-> ChAttsRec
     prd (ICh ('(lch, Attribution ich -> Attribution sch) : fc))
-> ChAttsRec
     prd (SCh ('(lch, Attribution ich -> Attribution sch) : fc))
kn ((ConsRec (TagField Label Reco
_ Label l
lch WrapField Reco v
fch) (fcr :: Record fc)))
   = \((ConsRec pich icr) :: ChAttsRec prd ( '(lch, ich) ': ICh fc))
   -> let scr :: ChAttsRec prd (SCh fc)
scr = Record fc -> ChAttsRec prd (ICh fc) -> ChAttsRec prd (SCh fc)
forall (fcr :: [(Child, *)]) (prd :: Prod).
Kn fcr prd =>
Record fcr -> ChAttsRec prd (ICh fcr) -> ChAttsRec prd (SCh fcr)
kn Record fc
fcr Rec (ChiReco prd) r1
ChAttsRec prd (ICh fc)
icr
          ich :: WrapField (ChiReco prd) v
ich = TaggedChAttr prd l v -> WrapField (ChiReco prd) v
forall k' k (prd :: Prod) (l :: k') (v :: k).
TaggedChAttr prd l v -> WrapField (ChiReco prd) v
unTaggedChAttr TaggedChAttr prd l v
pich
      in TagField (ChiReco prd) l sch
-> ChAttsRec prd (SCh fc) -> Rec (ChiReco prd) ('(l, sch) : SCh fc)
forall k k' k'' (c :: k) (l :: k') (v :: k'') (r1 :: [(k', k'')]).
TagField c l v -> Rec c r1 -> Rec c ('(l, v) : r1)
ConsRec (Label l
-> WrapField (ChiReco prd) sch -> TagField (ChiReco prd) l sch
forall k' k'' (l :: k') (prd :: Prod) (v :: k'').
Label l -> WrapField (ChiReco prd) v -> TaggedChAttr prd l v
TaggedChAttr Label l
lch
               (WrapField Reco v
Attribution ich -> Attribution sch
fch Attribution ich
WrapField (ChiReco prd) v
ich)) ChAttsRec prd (SCh fc)
scr



emptyCtx :: Proxy '[]
emptyCtx = Proxy '[]
forall k (t :: k). Proxy t
Proxy @ '[]

knit'
  :: ( Kn fc prd
     , Empties fc prd)
  => CRule '[] prd (SCh fc) ip (EmptiesR fc) '[] (ICh fc) sp
  -> Record fc -> Attribution ip -> Attribution sp
knit' :: CRule '[] prd (SCh fc) ip (EmptiesR fc) '[] (ICh fc) sp
-> Record fc -> Attribution ip -> Attribution sp
knit' (rule :: CRule '[] prd (SCh fc) ip
              (EmptiesR fc) '[] (ICh fc) sp)
              (Record fc
fc :: Record fc) Attribution ip
ip =
  let (Fam ChAttsRec prd (ICh fc)
ic Attribution sp
sp) = CRule '[] prd (SCh fc) ip (EmptiesR fc) '[] (ICh fc) sp
-> Proxy '[] -> Rule prd (SCh fc) ip (EmptiesR fc) '[] (ICh fc) sp
forall (ctx :: [ErrorMessage]) (prd :: Prod)
       (sc :: [(Child, [(Att, *)])]) (ip :: [(Att, *)])
       (ic :: [(Child, [(Att, *)])]) (sp :: [(Att, *)])
       (ic' :: [(Child, [(Att, *)])]) (sp' :: [(Att, *)]).
CRule ctx prd sc ip ic sp ic' sp'
-> Proxy ctx -> Rule prd sc ip ic sp ic' sp'
mkRule CRule '[] prd (SCh fc) ip (EmptiesR fc) '[] (ICh fc) sp
rule Proxy '[]
forall k. Proxy '[]
emptyCtx
                    (ChAttsRec prd (SCh fc) -> Attribution ip -> Fam prd (SCh fc) ip
forall (prd :: Prod) (c :: [(Child, [(Att, *)])])
       (p :: [(Att, *)]).
ChAttsRec prd c -> Attribution p -> Fam prd c p
Fam ChAttsRec prd (SCh fc)
sc Attribution ip
ip) (ChAttsRec prd (EmptiesR fc)
-> Attribution '[] -> Fam prd (EmptiesR fc) '[]
forall (prd :: Prod) (c :: [(Child, [(Att, *)])])
       (p :: [(Att, *)]).
ChAttsRec prd c -> Attribution p -> Fam prd c p
Fam ChAttsRec prd (EmptiesR fc)
ec Attribution '[]
emptyAtt)
      sc :: ChAttsRec prd (SCh fc)
sc          = Record fc -> ChAttsRec prd (ICh fc) -> ChAttsRec prd (SCh fc)
forall (fcr :: [(Child, *)]) (prd :: Prod).
Kn fcr prd =>
Record fcr -> ChAttsRec prd (ICh fcr) -> ChAttsRec prd (SCh fcr)
kn Record fc
fc ChAttsRec prd (ICh fc)
ic
      ec :: ChAttsRec prd (EmptiesR fc)
ec          = Record fc -> ChAttsRec prd (EmptiesR fc)
forall (fc :: [(Child, *)]) (prd :: Prod).
Empties fc prd =>
Record fc -> ChAttsRec prd (EmptiesR fc)
empties Record fc
fc
  in  Attribution sp
sp


class Empties (fc :: [(Child,Type)]) (prd :: Prod) where
  type EmptiesR fc :: [(Child, [(Att, Type)])] 
  empties :: Record fc -> ChAttsRec prd (EmptiesR fc)

instance Empties '[] prd where
  type EmptiesR '[] = '[]
  empties :: Record '[] -> ChAttsRec prd (EmptiesR '[])
empties Record '[]
_ = ChAttsRec prd (EmptiesR '[])
forall (prd :: Prod). ChAttsRec prd '[]
emptyCh

instance
  ( Empties fcr prd
  -- , chi ~ 'Chi ch prd nt
  )
  =>
  Empties ( '(chi, Attribution e -> Attribution a) ': fcr) prd where
  type EmptiesR ( '(chi, Attribution e -> Attribution a) ': fcr) =
    '(chi, '[]) ': EmptiesR fcr
  empties :: Record ('(chi, Attribution e -> Attribution a) : fcr)
-> ChAttsRec
     prd (EmptiesR ('(chi, Attribution e -> Attribution a) : fcr))
empties (ConsRec (TagField Label Reco
labelc
                   (labelch :: Label chi) WrapField Reco v
fch) Rec Reco r1
r) =
    TagField (ChiReco prd) chi '[]
-> Rec (ChiReco prd) (EmptiesR fcr)
-> Rec (ChiReco prd) ('(chi, '[]) : EmptiesR fcr)
forall k k' k'' (c :: k) (l :: k') (v :: k'') (r1 :: [(k', k'')]).
TagField c l v -> Rec c r1 -> Rec c ('(l, v) : r1)
ConsRec (Label (ChiReco prd)
-> Label chi
-> WrapField (ChiReco prd) '[]
-> TagField (ChiReco prd) chi '[]
forall k k' k'' (c :: k) (l :: k') (v :: k'').
Label c -> Label l -> WrapField c v -> TagField c l v
TagField (Label (ChiReco prd)
forall k (l :: k). Label l
Label @(ChiReco prd)) Label chi
labelch Attribution '[]
WrapField (ChiReco prd) '[]
emptyAtt) (Rec (ChiReco prd) (EmptiesR fcr)
 -> Rec (ChiReco prd) ('(chi, '[]) : EmptiesR fcr))
-> Rec (ChiReco prd) (EmptiesR fcr)
-> Rec (ChiReco prd) ('(chi, '[]) : EmptiesR fcr)
forall a b. (a -> b) -> a -> b
$ Rec Reco r1 -> ChAttsRec prd (EmptiesR r1)
forall (fc :: [(Child, *)]) (prd :: Prod).
Empties fc prd =>
Record fc -> ChAttsRec prd (EmptiesR fc)
empties Rec Reco r1
r


knit :: Proxy ctx
-> CRule ctx prd (SCh fc) ip (EmptiesR fc) '[] (ICh fc) sp
-> Record fc
-> Attribution ip
-> Attribution sp
knit (Proxy ctx
ctx  :: Proxy ctx)
     (CRule ctx prd (SCh fc) ip (EmptiesR fc) '[] (ICh fc) sp
rule :: CRule ctx prd (SCh fc) ip (EmptiesR fc) '[] (ICh fc) sp)
     (Record fc
fc   :: Record fc)
     (Attribution ip
ip   :: Attribution ip)
  = let (Fam ChAttsRec prd (ICh fc)
ic Attribution sp
sp) = CRule ctx prd (SCh fc) ip (EmptiesR fc) '[] (ICh fc) sp
-> Proxy ctx -> Rule prd (SCh fc) ip (EmptiesR fc) '[] (ICh fc) sp
forall (ctx :: [ErrorMessage]) (prd :: Prod)
       (sc :: [(Child, [(Att, *)])]) (ip :: [(Att, *)])
       (ic :: [(Child, [(Att, *)])]) (sp :: [(Att, *)])
       (ic' :: [(Child, [(Att, *)])]) (sp' :: [(Att, *)]).
CRule ctx prd sc ip ic sp ic' sp'
-> Proxy ctx -> Rule prd sc ip ic sp ic' sp'
mkRule CRule ctx prd (SCh fc) ip (EmptiesR fc) '[] (ICh fc) sp
rule Proxy ctx
ctx
                       (ChAttsRec prd (SCh fc) -> Attribution ip -> Fam prd (SCh fc) ip
forall (prd :: Prod) (c :: [(Child, [(Att, *)])])
       (p :: [(Att, *)]).
ChAttsRec prd c -> Attribution p -> Fam prd c p
Fam ChAttsRec prd (SCh fc)
sc Attribution ip
ip) (ChAttsRec prd (EmptiesR fc)
-> Attribution '[] -> Fam prd (EmptiesR fc) '[]
forall (prd :: Prod) (c :: [(Child, [(Att, *)])])
       (p :: [(Att, *)]).
ChAttsRec prd c -> Attribution p -> Fam prd c p
Fam ChAttsRec prd (EmptiesR fc)
ec Attribution '[]
emptyAtt)
        sc :: ChAttsRec prd (SCh fc)
sc          = Record fc -> ChAttsRec prd (ICh fc) -> ChAttsRec prd (SCh fc)
forall (fcr :: [(Child, *)]) (prd :: Prod).
Kn fcr prd =>
Record fcr -> ChAttsRec prd (ICh fcr) -> ChAttsRec prd (SCh fcr)
kn Record fc
fc ChAttsRec prd (ICh fc)
ic
        ec :: ChAttsRec prd (EmptiesR fc)
ec          = Record fc -> ChAttsRec prd (EmptiesR fc)
forall (fc :: [(Child, *)]) (prd :: Prod).
Empties fc prd =>
Record fc -> ChAttsRec prd (EmptiesR fc)
empties Record fc
fc
    in  Attribution sp
sp


knitAspect :: Label prd
-> CAspect '[] r -> Record fc -> Attribution ip -> Attribution sp
knitAspect (Label prd
prd :: Label prd) CAspect '[] r
asp Record fc
fc Attribution ip
ip
  = let ctx :: Proxy '[]
ctx  = Proxy '[]
forall k (t :: k). Proxy t
Proxy @ '[]
        ctx' :: Proxy '[ 'Text (AppendSymbol "knit:" (FromEM (ShowTE prd)))]
ctx' = Proxy '[ 'Text (AppendSymbol "knit:" (FromEM (ShowTE prd)))]
forall k (t :: k). Proxy t
Proxy @ '[Text ("knit:" `AppendSymbol` FromEM (ShowTE prd))]
    in  Proxy '[]
-> CRule '[] prd (SCh fc) ip (EmptiesR fc) '[] (ICh fc) sp
-> Record fc
-> Attribution ip
-> Attribution sp
forall (fc :: [(Child, *)]) (prd :: Prod) (ctx :: [ErrorMessage])
       (ip :: [(Att, *)]) (sp :: [(Att, *)]).
(Empties fc prd, Kn fc prd) =>
Proxy ctx
-> CRule ctx prd (SCh fc) ip (EmptiesR fc) '[] (ICh fc) sp
-> Record fc
-> Attribution ip
-> Attribution sp
knit Proxy '[]
forall k. Proxy '[]
ctx (Proxy '[ 'Text (AppendSymbol "knit:" (FromEM (ShowTE prd)))]
-> OpLookup PrdReco prd r -> ReqR (OpLookup PrdReco prd r)
forall op (ctx :: [ErrorMessage]).
Require op ctx =>
Proxy ctx -> op -> ReqR op
req Proxy '[ 'Text (AppendSymbol "knit:" (FromEM (ShowTE prd)))]
ctx' (Label prd -> Rec PrdReco r -> OpLookup PrdReco prd r
forall k k' (l :: k) c (r :: [(k, k')]).
Label l -> Rec c r -> OpLookup c l r
OpLookup Label prd
prd ((CAspect '[] r -> Proxy '[] -> Rec PrdReco r
forall (ctx :: [ErrorMessage]) (asp :: [(Prod, *)]).
CAspect ctx asp -> Proxy ctx -> Aspect asp
mkAspect CAspect '[] r
asp) Proxy '[]
forall k. Proxy '[]
ctx))) Record fc
fc Attribution ip
ip

-- | use
class Use (att :: Att) (prd :: Prod) (nts :: [NT]) (a :: Type) sc
 where
  usechi :: Label att -> Label prd -> KList nts -> (a -> a -> a) -> ChAttsRec prd sc
         -> Maybe a

class Use' (mnts :: Bool) (att :: Att) (prd :: Prod) (nts :: [NT])
           (a :: Type) sc
 where
  usechi' :: Proxy mnts -> Label att -> Label prd -> KList nts
   -> (a -> a -> a)
   -> ChAttsRec prd sc -> Maybe a

instance Use prd att nts a '[] where
  usechi :: Label prd
-> Label att
-> KList nts
-> (a -> a -> a)
-> ChAttsRec att '[]
-> Maybe a
usechi Label prd
_ Label att
_ KList nts
_ a -> a -> a
_ ChAttsRec att '[]
_ = Maybe a
forall a. Maybe a
Nothing

instance
  ( HMember' nt nts
  , HMemberRes' nt nts ~ mnts
  , Use' mnts att prd nts a ( '( 'Chi ch prd ('Left nt), attr) ': cs))
  =>
  Use att prd nts a ( '( 'Chi ch prd ('Left nt), attr) ': cs) where
  usechi :: Label att
-> Label prd
-> KList nts
-> (a -> a -> a)
-> ChAttsRec prd ('( 'Chi ch prd ('Left nt), attr) : cs)
-> Maybe a
usechi Label att
att Label prd
prd KList nts
nts a -> a -> a
op ChAttsRec prd ('( 'Chi ch prd ('Left nt), attr) : cs)
ch
    = Proxy mnts
-> Label att
-> Label prd
-> KList nts
-> (a -> a -> a)
-> ChAttsRec prd ('( 'Chi ch prd ('Left nt), attr) : cs)
-> Maybe a
forall (mnts :: Bool) (att :: Att) (prd :: Prod) (nts :: [NT]) a
       (sc :: [(Child, [(Att, *)])]).
Use' mnts att prd nts a sc =>
Proxy mnts
-> Label att
-> Label prd
-> KList nts
-> (a -> a -> a)
-> ChAttsRec prd sc
-> Maybe a
usechi' (Proxy mnts
forall k (t :: k). Proxy t
Proxy @ mnts) Label att
att Label prd
prd KList nts
nts a -> a -> a
op ChAttsRec prd ('( 'Chi ch prd ('Left nt), attr) : cs)
ch

instance
  Use att prd nts a cs
  =>
  Use att prd nts a ( '( 'Chi ch prd ('Right t), attr) ': cs) where
  usechi :: Label att
-> Label prd
-> KList nts
-> (a -> a -> a)
-> ChAttsRec prd ('( 'Chi ch prd ('Right t), attr) : cs)
-> Maybe a
usechi Label att
att Label prd
prd KList nts
nts a -> a -> a
op (ConsRec TagField (ChiReco prd) l v
_ Rec (ChiReco prd) r1
ch)
    = Label att
-> Label prd
-> KList nts
-> (a -> a -> a)
-> Rec (ChiReco prd) r1
-> Maybe a
forall (att :: Att) (prd :: Prod) (nts :: [NT]) a
       (sc :: [(Child, [(Att, *)])]).
Use att prd nts a sc =>
Label att
-> Label prd
-> KList nts
-> (a -> a -> a)
-> ChAttsRec prd sc
-> Maybe a
usechi Label att
att Label prd
prd KList nts
nts a -> a -> a
op Rec (ChiReco prd) r1
ch


instance
  Use att prd nts a cs
  =>
  Use' False att prd nts a ( '( 'Chi ch prd ('Left nt), attr) ': cs) where
  usechi' :: Proxy 'False
-> Label att
-> Label prd
-> KList nts
-> (a -> a -> a)
-> ChAttsRec prd ('( 'Chi ch prd ('Left nt), attr) : cs)
-> Maybe a
usechi' Proxy 'False
_ Label att
att Label prd
prd KList nts
nts a -> a -> a
op (ConsRec TagField (ChiReco prd) l v
_ Rec (ChiReco prd) r1
cs) = Label att
-> Label prd
-> KList nts
-> (a -> a -> a)
-> Rec (ChiReco prd) r1
-> Maybe a
forall (att :: Att) (prd :: Prod) (nts :: [NT]) a
       (sc :: [(Child, [(Att, *)])]).
Use att prd nts a sc =>
Label att
-> Label prd
-> KList nts
-> (a -> a -> a)
-> ChAttsRec prd sc
-> Maybe a
usechi Label att
att Label prd
prd KList nts
nts a -> a -> a
op Rec (ChiReco prd) r1
cs

instance
  ( Require (OpLookup AttReco att attr)
            '[('Text "looking up attribute " ':<>: ShowTE att)
              ':$$: ('Text "on " ':<>: ShowTE attr)]
  , ReqR (OpLookup AttReco att attr) ~ a
  , Use att prd nts a cs
  , WrapField (ChiReco prd) attr ~ Attribution attr)  --ayudín
  =>
  Use' True att prd nts a ( '( 'Chi ch prd ('Left nt), attr) : cs) where
  usechi' :: Proxy 'True
-> Label att
-> Label prd
-> KList nts
-> (a -> a -> a)
-> ChAttsRec prd ('( 'Chi ch prd ('Left nt), attr) : cs)
-> Maybe a
usechi' Proxy 'True
_ Label att
att Label prd
prd KList nts
nts a -> a -> a
op (ConsRec TagField (ChiReco prd) l v
lattr Rec (ChiReco prd) r1
scr) =
    let attr :: WrapField (ChiReco prd) v
attr = TagField (ChiReco prd) l v -> WrapField (ChiReco prd) v
forall k' k (prd :: Prod) (l :: k') (v :: k).
TaggedChAttr prd l v -> WrapField (ChiReco prd) v
unTaggedChAttr TagField (ChiReco prd) l v
lattr
        val :: ReqR (OpLookup AttReco att attr)
val  = Attribution attr
WrapField (ChiReco prd) v
attr Attribution attr -> Label att -> ReqR (OpLookup AttReco att attr)
forall (msg :: [ErrorMessage]) (l :: Att) (r :: [(Att, *)]).
(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)
#. Label att
att
    in  a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ a -> (a -> a) -> Maybe a -> a
forall b a. b -> (a -> b) -> Maybe a -> b
maybe a
ReqR (OpLookup AttReco att attr)
val (a -> a -> a
op a
ReqR (OpLookup AttReco att attr)
val) (Maybe a -> a) -> Maybe a -> a
forall a b. (a -> b) -> a -> b
$ Label att
-> Label prd
-> KList nts
-> (a -> a -> a)
-> Rec (ChiReco prd) r1
-> Maybe a
forall (att :: Att) (prd :: Prod) (nts :: [NT]) a
       (sc :: [(Child, [(Att, *)])]).
Use att prd nts a sc =>
Label att
-> Label prd
-> KList nts
-> (a -> a -> a)
-> ChAttsRec prd sc
-> Maybe a
usechi Label att
att Label prd
prd KList nts
nts a -> a -> a
op Rec (ChiReco prd) r1
scr


-- | Defines a rule to compute an attribute 'att' in the production
-- 'prd', by applying an operator to the values of 'att' in each non
-- terminal in the list 'nts'.

-- use
--   :: UseC att prd nts t' sp sc sp' ctx
--   => Label ('Att att t')
--   -> Label prd
--   -> KList nts
--   -> (t' -> t' -> t')
--   -> t'
--   -> forall ip ic' . CRule ctx prd sc ip ic' sp ic' sp'
-- use att prd nts op unit
--   = syndef att prd
--   $ \_ fam -> maybe unit id (usechi att prd nts op $ chi fam)


type UseC att prd nts t' sp sc sp' ctx =
  ( Require (OpExtend  AttReco ('Att att t') t' sp) ctx
  ,  Use ('Att att t') prd nts t' sc
  ,  ReqR (OpExtend AttReco ('Att att t') t' sp)
     ~ Rec AttReco sp'
  )

class EmptyAspectSameShape (es1 :: [k]) (es2 :: [m])

instance (es2 ~ '[]) => EmptyAspectSameShape '[] es2
instance (EmptyAspectSameShape xs ys, es2 ~ ( '(y1,y2,y3,y4) ': ys))
  => EmptyAspectSameShape (x ': xs) es2


-- require KLIST de prods?, NO, eso está en el kind!
class
  EmptyAspectSameShape prds polyArgs
  =>
  EmptyAspect (prds :: [Prod])
              (polyArgs :: [([(Child, [(Att, Type)])], [(Att, Type)],
                             [(Child, [(Att, Type)])], [(Att, Type)] )])
              ctx where
  type EmptyAspectR prds polyArgs ctx :: [(Prod, Type)]
  emptyAspectC :: KList prds -> Proxy polyArgs
    -> CAspect ctx (EmptyAspectR prds polyArgs ctx)

instance
  EmptyAspect '[] '[] ctx where
  type EmptyAspectR '[] '[] ctx = '[]
  emptyAspectC :: KList '[] -> Proxy '[] -> CAspect ctx (EmptyAspectR '[] '[] ctx)
emptyAspectC KList '[]
_ Proxy '[]
_ = CAspect ctx (EmptyAspectR '[] '[] ctx)
forall (ctx :: [ErrorMessage]). CAspect ctx '[]
emptyAspect

instance
  ( EmptyAspect prds polys ctx
  , ExtAspect ctx prd sc ip ic sp ic sp
    (EmptyAspectR prds polys ctx)
    (EmptyAspectR (prd ': prds) ( '(sc, ip, ic, sp) ': polys) ctx)
  )
  =>
  EmptyAspect (prd ': prds) ( '(sc, ip, ic, sp) ': polys) ctx where
  type EmptyAspectR (prd ': prds) ( '(sc, ip, ic, sp) ': polys) ctx =
    UnWrap (ReqR (OpComRA '[] prd ((CRule '[] prd sc ip ic sp ic sp))
                  (EmptyAspectR prds polys ctx)))
  emptyAspectC :: KList (prd : prds)
-> Proxy ('(sc, ip, ic, sp) : polys)
-> CAspect
     ctx (EmptyAspectR (prd : prds) ('(sc, ip, ic, sp) : polys) ctx)
emptyAspectC (KCons Label h
prd KList l
prds) (Proxy ('(sc, ip, ic, sp) : polys)
p :: Proxy ( '(sc, ip, ic, sp) ': polys)) =
    (CRule ctx prd sc ip ic sp ic sp
forall (ctx :: [ErrorMessage]) (prd :: Prod)
       (sc :: [(Child, [(Att, *)])]) (ip :: [(Att, *)])
       (ic' :: [(Child, [(Att, *)])]) (sp' :: [(Att, *)]).
CRule ctx prd sc ip ic' sp' ic' sp'
emptyRule :: CRule ctx prd sc ip ic sp ic sp) 
    CRule ctx prd sc ip ic sp ic sp
-> CAspect ctx (EmptyAspectR prds polys ctx)
-> CAspect
     ctx
     (UnWrap
        (ReqR
           (OpComRA
              '[]
              prd
              (CRule '[] prd sc ip ic sp ic sp)
              (EmptyAspectR prds polys ctx))))
forall (ctx :: [ErrorMessage]) (prd :: Prod)
       (sc :: [(Child, [(Att, *)])]) (ip :: [(Att, *)])
       (ic :: [(Child, [(Att, *)])]) (sp :: [(Att, *)])
       (ic' :: [(Child, [(Att, *)])]) (sp' :: [(Att, *)])
       (a :: [(Prod, *)]) (asp :: [(Prod, *)]).
(Require
   (OpComRA ctx prd (CRule ctx prd sc ip ic sp ic' sp') a) ctx,
 ReqR (OpComRA ctx prd (CRule ctx prd sc ip ic sp ic' sp') a)
 ~ Rec PrdReco asp) =>
CRule ctx prd sc ip ic sp ic' sp'
-> CAspect ctx a -> CAspect ctx asp
.+: KList prds
-> Proxy polys -> CAspect ctx (EmptyAspectR prds polys ctx)
forall (prds :: [Prod])
       (polyArgs :: [([(Child, [(Att, *)])], [(Att, *)],
                      [(Child, [(Att, *)])], [(Att, *)])])
       (ctx :: [ErrorMessage]).
EmptyAspect prds polyArgs ctx =>
KList prds
-> Proxy polyArgs -> CAspect ctx (EmptyAspectR prds polyArgs ctx)
emptyAspectC @prds @polys KList prds
KList l
prds (Proxy polys
forall k (t :: k). Proxy t
Proxy @ polys)

emptyAspectForProds :: KList prds -> CAspect ctx (EmptyAspectR prds polyArgs ctx)
emptyAspectForProds KList prds
prdList = KList prds
-> Proxy polyArgs -> CAspect ctx (EmptyAspectR prds polyArgs ctx)
forall (prds :: [Prod])
       (polyArgs :: [([(Child, [(Att, *)])], [(Att, *)],
                      [(Child, [(Att, *)])], [(Att, *)])])
       (ctx :: [ErrorMessage]).
EmptyAspect prds polyArgs ctx =>
KList prds
-> Proxy polyArgs -> CAspect ctx (EmptyAspectR prds polyArgs ctx)
emptyAspectC KList prds
prdList Proxy polyArgs
forall k (t :: k). Proxy t
Proxy

-- ** copy rules

-- | a rule to copy one attribute `att` from the parent to the children `chi`

copyAtChi :: Label ('Att att t')
-> Label ('Chi chi ('Prd prd' nt') ntch)
-> CRule ctx ('Prd prd' nt') sc ip ic sp ic' sp
copyAtChi Label ('Att att t')
att Label ('Chi chi ('Prd prd' nt') ntch)
chi
  = Label ('Att att t')
-> Label ('Prd prd' nt')
-> Label ('Chi chi ('Prd prd' nt') ntch)
-> (Proxy ctx -> Fam ('Prd prd' nt') sc ip -> t')
-> forall (sp :: [(Att, *)]).
   CRule ctx ('Prd prd' nt') sc ip ic sp ic' sp
forall k t t' (ctx :: [ErrorMessage]) (att :: Symbol)
       (r :: [(Att, *)]) (v2 :: [(Att, *)]) (prd :: Symbol)
       (prd' :: Symbol) (nt :: NT) (nt' :: NT) (chi :: Symbol)
       (ntch :: Either NT T) (ic :: [(Child, [(Att, *)])])
       (ic' :: [(Child, [(Att, *)])]) (n :: k)
       (sc :: [(Child, [(Att, *)])]) (ip :: [(Att, *)]).
Inhdef t t' ctx att r v2 prd prd' nt nt' chi ntch ic ic' n =>
Label ('Att att t)
-> Label ('Prd prd nt)
-> Label ('Chi chi ('Prd prd' nt') ntch)
-> (Proxy ctx -> Fam ('Prd prd nt) sc ip -> t')
-> forall (sp :: [(Att, *)]).
   CRule ctx ('Prd prd nt) sc ip ic sp ic' sp
inhdef Label ('Att att t')
att (Label ('Chi chi ('Prd prd' nt') ntch) -> Label ('Prd prd' nt')
forall (nam :: Symbol) (prd :: Prod) (tnt :: Either NT T).
Label ('Chi nam prd tnt) -> Label prd
prdFromChi Label ('Chi chi ('Prd prd' nt') ntch)
chi) Label ('Chi chi ('Prd prd' nt') ntch)
chi (Label Lhs
-> Label ('Att att t')
-> Proxy ctx
-> ResAt Lhs ('Att att t') ((->) (Proxy ctx))
forall k k (pos :: k) (att :: k) (m :: * -> *).
At pos att m =>
Label pos -> Label att -> m (ResAt pos att m)
at Label Lhs
lhs Label ('Att att t')
att)

--copyAtChiP (att :: forall t. Label ('Att "" t)) chi
--  = \(p :: Proxy val) -> inhP (att @val) (prdFromChi chi) chi (at lhs att)


-- | to copy at many children
class CopyAtChiList (att :: Att)
                    (chi :: [Child])
                    (polyArgs :: [([(Child, [(Att, Type)])], [(Att, Type)],
                                   [(Child, [(Att, Type)])], [(Att, Type)],
                                   [(Child, [(Att, Type)])], [(Att, Type)] )])
                     ctx where
  type CopyAtChiListR att chi polyArgs ctx :: [(Prod, Type)]
  copyAtChiList :: Label att -> KList chi -> Proxy polyArgs
                -> CAspect ctx (CopyAtChiListR att chi polyArgs ctx)

instance CopyAtChiList att '[] '[] ctx where
  type CopyAtChiListR att '[] '[] ctx = '[]
  copyAtChiList :: Label att
-> KList '[]
-> Proxy '[]
-> CAspect ctx (CopyAtChiListR att '[] '[] ctx)
copyAtChiList Label att
_ KList '[]
_ Proxy '[]
_ = CAspect ctx (CopyAtChiListR att '[] '[] ctx)
forall (ctx :: [ErrorMessage]). CAspect ctx '[]
emptyAspect

-- instance
--   ( CopyAtChiList ('Att att t) chi polys ctx
--   , prd ~ Prd p nt
--   , tnt ~ Left nc
--   )
--   =>
--   CopyAtChiList ('Att att t) (Chi ch prd tnt ': chi)
--    ('(sc, ip, ic, sp, ic', sp') ': polys) ctx where
--   type CopyAtChiListR ('Att att t) (Chi ch prd tnt ': chi)
--    ('(sc, ip, ic, sp, ic', sp') ': polys) ctx =
--     UnWrap (ReqR (OpComRA '[] prd ((CRule '[] prd sc ip ic sp ic' sp'))
--                   (CopyAtChiListR ('Att att t) chi polys ctx)))
--   copyAtChiList att (KCons chi chs :: KList ('Chi ch prd tnt ': chs) )
--    (p :: Proxy ( '(sc, ip, ic, sp, ic', sp') ': polys))
--     = copyAtChi att chi
--     .+: copyAtChiList @('Att att t) @chs att chs (Proxy @polys)




-- * Productions
--data Symbol = N String | Te Name
type family Terminal s :: Either NT T where
  Terminal s = 'Right ('T s)

type family NonTerminal s where
  NonTerminal s = 'Left s


(+++) :: Proxy e1 -> Proxy e2 -> Proxy (e1 :$$: e2)
Proxy e1
Proxy +++ :: Proxy e1 -> Proxy e2 -> Proxy (e1 ':$$: e2)
+++ Proxy e2
Proxy = Proxy (e1 ':$$: e2)
forall k (t :: k). Proxy t
Proxy

consErr :: Proxy e -> Proxy es -> Proxy (e : es)
consErr :: Proxy e -> Proxy es -> Proxy (e : es)
consErr Proxy e
Proxy Proxy es
Proxy = Proxy (e : es)
forall k (t :: k). Proxy t
Proxy