AspectAG-0.8.0.0: src/Language/AspectAG.hs
{-# 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 #-}
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RebindableSyntax #-}
{-# LANGUAGE UndecidableSuperClasses #-}
module Language.AspectAG where
import Prelude hiding ((>>), (>>=), return)
import Language.AspectAG.Types
import Data.GenRec (Rec(..), TagField(..), WrapField, UnWrap,
OpLJoin(..), OpLookup(..), OpLeftProj(..),
OpExtend(..), (.=.), (.//), (.*.),
LabelsOf, Cmp)
import Data.Label (Label(..))
import Data.Kind
import Language.AspectAG.RecordInstances
import Data.Type.Require
import Data.Proxy
import Control.IMonad
import Language.AspectAG.EADT
import Control.Monad.Reader
import Control.Monad qualified as M
import Data.Type.Equality
import Data.Type.Ord (Compare(..))
import Data.Type.Bool
import GHC.TypeLits
import Data.HList
import Data.GenRec.RecInstances.Record
-- | The data type 'Fam' stores a mapping from children to attributions,
-- and an attribution for the father.
data Fam (c :: [(ChildName, [(AttName, Type)])])
(p :: [(AttName, Type)]) :: Type
where
Fam :: ChAttsRec c -> Attribution p -> Fam c p
-- | The data type 'Rule' stores a mapping from an input family
-- (synthesized attributes of children, inherited from father) to the
-- output family (inherited to children, synthesized of father). It is
-- always related to a production 'prd'.
type Rule (prd :: (NTName,ProdName)) ip sc ic sp
= Fam ip sc -> Fam ic sp
-- | The type family 'Ext' computes the constraints needed so
-- @Fam prd scsc' ipip' icic' spsp'@ ' is the result of combining
-- @Fam prd sc ip ic sp@ and @Fam prd sc' ip' ic' sp' @
type family Ext (prd :: (NTName, ProdName))
(sc :: [(ChildName, [(AttName, Type)])])
(ip :: [(AttName, Type)])
(ic :: [(ChildName, [(AttName, Type)])])
(sp :: [(AttName, Type)])
(sc' :: [(ChildName, [(AttName, Type)])])
(ip' :: [(AttName, Type)])
(ic' :: [(ChildName, [(AttName, Type)])])
(sp' :: [(AttName, Type)])
(scsc' :: [(ChildName, [(AttName, Type)])])
(ipip' :: [(AttName, Type)])
(icic' :: [(ChildName, [(AttName, Type)])])
(spsp' :: [(AttName, Type)])
where
Ext prd sc ip ic sp sc' ip' ic' sp' scsc' ipip' icic' spsp'
= (ReqR (OpLeftProj AttReco (LabelsOf ip') ipip')
~ Rec AttReco ip',
ReqR (OpLeftProj AttReco (LabelsOf ip) ipip') ~ Rec AttReco ip,
ReqR (OpLJoin AttReco ip ip') ~ Rec AttReco ipip',
ReqR (OpLJoin AttReco sp sp') ~ Rec AttReco spsp',
ReqR (OpChiMerge ic ic') ~ Rec ChiReco icic',
ReqR (OpChiMerge sc sc') ~ Rec ChiReco scsc',
ProjChi scsc' sc', ProjChi scsc' sc,
Require (OpLeftProj AttReco (LabelsOf ip') ipip') '[ ],
Require (OpLeftProj AttReco (LabelsOf ip) ipip') '[ ],
sp :|: sp',
Require (OpChiMerge ic ic') '[])
-- | @ext@ combines two rules for the same production.
ext :: (Ext prd sc ip ic sp sc' ip' ic' sp' scsc' ipip' icic' spsp')
=> Rule prd sc ip ic sp
-> Rule prd sc' ip' ic' sp'
-> Rule prd scsc' ipip' icic' spsp'
ext (rule_1 :: Rule prd sc ip ic sp)
(rule_2 :: Rule prd sc' ip' ic' sp') =
\inp@(Fam (scv :: ReqR (OpChiMerge sc sc'))
(ipv :: ReqR (OpLJoin AttReco ip ip')))
-> let scv_1 = projChi (Proxy @sc) scv
scv_2 = projChi (Proxy @sc') scv
ipv_1 = Label @(LabelsOf ip) .// ipv
ipv_2 = Label @(LabelsOf ip') .// ipv
(Fam icv_1 spv) = rule_1 (Fam scv_1 ipv_1)
(Fam icv_2 spv') = rule_2 (Fam scv_2 ipv_2)
in (Fam (icv_1 .::><: icv_2) (spv .:>< spv'))
-- | operator version of ext
(.+.) :: Ext prd sc ip ic sp sc' ip' ic' sp' scsc' ipip' icic' spsp' =>
CRule prd sc ip ic sp
-> CRule prd sc' ip' ic' sp' -> CRule prd scsc' ipip' icic' spsp'
(CRule f) .+. (CRule g)
= CRule (f `ext` g)
-- the following function merges child records.
-- it assumes children records have the same shape (same domain).
-- This should be controlled as a requirement.
-- We can generalize this function. it will be useful if we want to make
-- productions extensible.
-- | builds an empty children record (i.e a record with one empty attribution
-- for non-terminals, and a singleton attribution for terminals)
class EmptyChiAtts prd (chs :: [(ChildName, GSym)]) where
type ChiAtts (b :: Bool) prd chs :: [(ChildName, [(AttName, Type)])]
emptyChiAtts :: Proxy chs -> Proxy prd -> Proxy b
-> ChAttsRec (ChiAtts b prd chs)
class EmptyChiAttsNormal prd (chs :: [(ChildName, GSym)]) ipsp where
type ChiAttsNormal (b :: Bool) prd chs
(ipsp :: [(NTName, [(AttName, Type)], [(AttName, Type)])])
:: [(ChildName, [(AttName, Type)])]
emptyChiAttsNormal :: Proxy chs -> Proxy prd -> Proxy b -> Proxy ipsp
-> ChAttsRec (ChiAttsNormal b prd chs ipsp)
instance EmptyChiAttsNormal prd '[] ipsp where
type ChiAttsNormal b prd '[] ipsp = '[]
emptyChiAttsNormal _ _ _ _ = EmptyRec
instance EmptyChiAtts prd '[] where
type ChiAtts b prd '[]= '[]
emptyChiAtts _ _ _ = EmptyRec
-- | in case of a non-terminal, the empty child has an empty attribution
instance
( EmptyChiAtts prd chs)
=> EmptyChiAtts prd ( '(chi, 'NonTer nt) ': chs) where
type ChiAtts b prd ( '(chi, 'NonTer nt) ': chs)
= '(chi, '[]) ': ChiAtts b prd chs
emptyChiAtts p q r = (Label .= emptyAtt)
`ConsRec` (emptyChiAtts (pTail p) (Proxy @prd) r)
instance
( EmptyChiAttsNormal prd chs ipsp)
=> EmptyChiAttsNormal prd ( '(chi, 'NonTer nt) ': chs) ipsp where
type ChiAttsNormal b prd ( '(chi, 'NonTer nt) ': chs) ipsp
= '(chi, If b (S nt ipsp) ('[])) ': ChiAttsNormal b prd chs ipsp
emptyChiAttsNormal p q r s = (Label .= undefined)
`ConsRec` (emptyChiAttsNormal (pTail p) q r s)
pTail :: Proxy (t ': ts) -> Proxy ts
pTail Proxy = Proxy
lTail :: Label (t ': ts) -> Label ts
lTail Label = Label
mkLabel :: l a -> Label a
mkLabel _ = Label
instance
(EmptyChiAtts prd chs)
=> EmptyChiAtts prd ( '(chi, 'Ter t) ': chs) where
type ChiAtts b prd ( '(chi, 'Ter t) ': chs)
= '(chi, If b ('[ '("term", t)]) ('[])) ': ChiAtts b prd chs
emptyChiAtts p q r
= (Label .= undefined) `ConsRec` (emptyChiAtts (pTail p) (Proxy @prd) r)
instance
(EmptyChiAttsNormal prd chs ipsp)
=> EmptyChiAttsNormal prd ( '(chi, 'Ter t) ': chs) ipsp where
type ChiAttsNormal b prd ( '(chi, 'Ter t) ': chs) ipsp
= '(chi, If b ('[ '("term", t)]) ('[])) ': ChiAttsNormal b prd chs ipsp
emptyChiAttsNormal pChs pPrd pBool pIPSP
= (Label .= undefined) `ConsRec`
(emptyChiAttsNormal (pTail pChs) pPrd pBool pIPSP)
class
EmptyChiAtts pnam (GetTChildrenOfProd (GetTProdsOfNT g nt) pnam)
=>
EmptyRule (g :: Grammar) (nt :: NTName) (pnam :: ProdName) where
emptyRule :: Label g -> Label (Prd pnam ('NT nt))
-> CRule '(nt,pnam)
(ChiAtts 'True pnam (GetTChildrenOfProd (GetTProdsOfNT g nt) pnam))
'[]
(ChiAtts 'False pnam (GetTChildrenOfProd (GetTProdsOfNT g nt) pnam))
'[]
class
EmptyRuleNormal (g :: Grammar) (nt :: NTName) (pnam :: ProdName)
(ipsp :: [(NTName, [(AttName, Type)], [(AttName, Type)])])
where
type EmptyRuleNormalR g nt pnam ipsp
emptyRuleNormal :: Label g -> Label pnam -> Label nt -> Label ipsp
-> EmptyRuleNormalR g nt pnam ipsp
instance EmptyChiAtts pnam (GetTChildrenOfProd (GetTProdsOfNT g nt) pnam)
=>
EmptyRule (g :: Grammar) (nt :: NTName) (pnam :: ProdName) where
emptyRule Label Label =
let pr = Proxy @(GetTChildrenOfProd (GetTProdsOfNT g nt) pnam)
in CRule $ \fam -> Fam (emptyChiAtts pr (Proxy @pnam) (Proxy @'False)) emptyAtt
instance EmptyChiAttsNormal pnam
(GetTChildrenOfProd (GetTProdsOfNT g nt) pnam) ipsp
=>
EmptyRuleNormal (g :: Grammar) (nt :: NTName) (pnam :: ProdName) ipsp where
type EmptyRuleNormalR g nt pnam ipsp =
CRule '(nt, pnam)
(ChiAttsNormal 'True pnam (GetTChildrenOfProd (GetTProdsOfNT g nt) pnam) ipsp)
(I nt ipsp)
(ChiAttsNormal 'False pnam (GetTChildrenOfProd (GetTProdsOfNT g nt) pnam) ipsp)
'[]
emptyRuleNormal lG lPnam lNT lIPSP =
let pr = Proxy @(GetTChildrenOfProd (GetTProdsOfNT g nt) pnam)
in CRule $ \fam -> Fam (emptyChiAttsNormal pr (lp lPnam) (Proxy @'False)
(lp lIPSP)) emptyAtt
--- hay que "proyectar" una regla: i e:
lp :: Label a -> Proxy a
lp Label = Proxy
-- | Rules with context (used to print domain specific type errors).
-- without tx now
newtype CRule (prd :: (NTName,ProdName)) sc ip ic sp
= CRule { mkRule :: (Rule prd sc ip ic sp)}
-- * Combinators to define rules
-- | syndef builds a rule to compute a synthesized attribute @att@ at production @prd@
syndef (att :: Label ('Att att t))
(prd :: Label ('Prd prd nt))
f
= CRule $ \inp
-> Fam EmptyRec $ Label @att .=. (f inp) .*. EmptyRec
-- | syndef builds a rule to compute an inherited attribute @att@ at child
-- @ch@ of production @prd@
inhdef (att :: Label ('Att att t))
(prd :: Label ('Prd prd nt))
(ch :: Label ('Chi ch ('Prd prd nt) ntch))
f
= CRule $ \inp
-> Fam (Label @ch .=. (Label @att .=. (f inp) .*. EmptyRec) .*. EmptyRec) EmptyRec
-- | takes chis proxy
syndefC :: EmptyChiAtts prdn chs
=> Proxy chs
-> Label ('Att att v)
-> Label ('Prd prdn ('NT nt))
-> (Fam sc ip -> v)
-> CRule '(nt, prdn) sc ip (ChiAtts 'False prdn chs) '[ '(att, v)]
syndefC (p :: Proxy chs)
(att :: Label ('Att att t))
(prd :: Label ('Prd prdn ('NT nt)))
f
= CRule $ \inp
-> Fam (emptyChiAtts p (Proxy @prdn) (Proxy @False))
$ Label @att .=. (f inp) .*. emptyAtt
class Monad m => At pos att (ctx :: [ErrorMessage]) m
| pos att ctx -> m where
type ResAt pos att ctx m
at :: Label pos -> Label att -> m (ResAt pos att ctx m)
instance At ('Chi ch ('Prd prdnam nt) ('NonTer nt')) ('Att att t) ctx
(Reader (Fam '[ '(ch, '[ '(att,t)])] '[]))
where
type ResAt ('Chi ch ('Prd prdnam nt) ('NonTer nt')) ('Att att t) ctx
(Reader (Fam '[ '(ch, '[ '(att,t)])] '[]))
= ReqR (OpLookup AttReco att
(UnWrap @AttName @Type
(ReqR (OpLookup ChiReco ch
'[ '(ch, '[ '(att,t)])] ))))
at (ch :: Label ('Chi ch ('Prd prdnam nt) ('NonTer nt')))
(att :: Label ('Att att t)) =
M.liftM (\(Fam chi _)
-> let atts = req Proxy (OpLookup (Label @ch) chi)
in req Proxy (OpLookup (Label @att) atts))
ask
def = runReader
data LHS = LHS
lhs = Label @LHS
-- ter = undefined
ter :: Label ('Chi ch ('Prd prdnam nt) ('Ter t))
-> (Reader (Fam '[ '(ch, '[ '("term", t)] )] '[])) t
ter (Label :: Label ('Chi ch ('Prd prdnam nt) ('Ter t)))
= M.liftM (\(Fam chi _)
-> req Proxy (OpLookup (Label @"term") (req Proxy (OpLookup (Label @ch) chi)))) ask
instance At LHS ('Att att t) ctx
(Reader (Fam '[] '[ '(att, t)]))
where
type ResAt LHS ('Att att t) ctx
(Reader (Fam '[] '[ '(att, t)]))
= ReqR (OpLookup AttReco att '[ '(att, t)])
at (Label :: Label LHS) (att :: Label ('Att att t))=
M.liftM (\(Fam _ par) -> req Proxy (OpLookup (Label @att) par)) ask
syndefM ::
(RequireEq t t' '[])
=> Label ('Att att t')
-> Label ('Prd prd ('NT nt))
-> Reader (Fam sc ip) t
-> CRule '(nt, prd) sc ip '[] '[ '(att, t)]
syndefM att prd f
= (syndef att prd . runReader) f
syndefMI ::
forall att prd nt t sc ip.
Reader (Fam sc ip) t
-> CRule '(nt, prd) sc ip '[] '[ '(att, t)]
syndefMI = syndefM Label Label
inhdefM
:: Label ('Att att t)
-> Label ('Prd prd ('NT nt))
-> Label ('Chi ch ('Prd prd ('NT nt)) ntch)
-> Reader (Fam sc ip) v
-> CRule '(nt, prd) sc ip '[ '(ch, '[ '(att, v)])] '[]
inhdefM att prd ch f
= (inhdef att prd ch . runReader) f
instance Return (Reader (Fam sc ip)) where
preturn a = M.return a -- we know it is a monad!
-- annoying but neccesary, otherwise the last monad of a chain of >>=.
-- cannot be inferred (therefore any), perhaps there is a way...
ret = preturn @(Reader (Fam '[] '[]))
instance
( ip :|: ip'
, ProjChiOp (OpChiMerge sc sc') sc
, ProjChiOp (OpChiMerge sc sc') sc'
)
=>
Bind (Reader (Fam sc ip))
(Reader (Fam sc' ip')) where
type (Reader (Fam sc ip))
:>>=
(Reader (Fam sc' ip'))
= (Reader (Fam (UnWrap (ReqR (OpChiMerge sc sc')))
(UnWrap (ReqR (OpLJoin AttReco ip ip')))
))
m >>=. f = reader $ \inp
-> let (Fam scsc' ipip') = inp
inp1 = Fam (projChi(Proxy @sc) scsc')
((Label @(LabelsOf ip).// ipip') :: Attribution ip)
inp2 = Fam (projChi(Proxy @sc') scsc')
((Label @(LabelsOf ip').// ipip') :: Attribution ip')
in runReader (f (runReader m inp1)) inp2
-- | Aspects, tagged with context. 'Aspect' is a record instance having
-- productions as labels, containing 'Rule's as fields.
newtype CAspect (asp :: [((NTName,ProdName), Type)] )
= CAspect { mkAspect :: 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 '[]
emptyAspect = CAspect $ 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) '[]
, ReqR (OpComAsp al ar) ~ Aspect asp
)
=> CAspect al -> CAspect ar -> CAspect asp
comAspect al ar
= CAspect $ req (Proxy @'[]) (OpComAsp (mkAspect al) (mkAspect ar))
-- | add rule to an aspect
data OpComAsp (al :: [((NTName, ProdName), Type)])
(ar :: [((NTName, ProdName), Type)]) where
OpComAsp :: Aspect al -> Aspect ar -> OpComAsp al ar
instance
Require (OpComAsp '[] ar) ctx where
type ReqR (OpComAsp '[] ar) = Aspect ar
req ctx (OpComAsp _ ar) = ar
instance
( (ReqR (OpComRA prd (CRule prd sc ip ic sp) ar))
~ (Rec PrdReco
(UnWrap
(ReqR (OpComRA prd (CRule prd sc ip ic sp) ar))))
, ReqR (OpComRA prd (CRule prd sc ip ic sp) ar)
~ Rec PrdReco ar0
, (Require (OpComAsp al ar0) ctx)
, (Require
(OpComRA prd (CRule prd sc ip ic sp) ar) ctx)
) =>
Require (OpComAsp
('(prd, CRule prd sc ip ic sp) ': al) ar) ctx where
type ReqR (OpComAsp ('(prd, CRule prd sc ip ic sp) ': al) ar) =
ReqR (OpComAsp al
(UnWrap (ReqR
(OpComRA prd (CRule prd sc ip ic sp) ar))))
req ctx (OpComAsp (ConsRec (TagField _ _ rul) al) ar)
= req ctx (OpComAsp al (req ctx (OpComRA rul ar)))
type family IC (rule :: Type) where
IC (CRule prd sc ip ic sp) = ic
-- IC (Rule prd sc ip ic sp) = ic
type family SP (rule :: Type) where
SP (CRule prd sc ip ic sp) = sp
-- SP (Rule prd sc ip ic sp) = sp
type family SC (rule :: Type) where
SC (CRule prd sc ip ic sp) = sc
-- SC (Rule prd sc ip ic sp) = sc
type family IP (rule :: Type) where
IP (CRule prd sc ip ic sp) = ip
-- IP (Rule prd sc ip ic sp) = ip
-- | combine a rule with an aspect (wrapper)
data OpComRA (prd :: (NTName, ProdName))
(rule :: Type) -- TODO : doc this
(a :: [((NTName, ProdName), Type)]) where
OpComRA :: CRule prd sc ip ic sp
-> Aspect a -> OpComRA prd (CRule prd sc ip ic sp) a
-- | combine a rule with an aspect (inner)
data OpComRA' (cmp :: Ordering)
(prd :: (NTName, ProdName))
(rule :: Type) -- TODO : doc this
(a :: [((NTName, ProdName), Type)]) where
OpComRA' :: Proxy cmp
-> CRule prd sc ip ic sp
-> Aspect a
-> OpComRA' cmp prd (CRule prd sc ip ic sp) a
type instance (WrapField PrdReco (CRule prd sc ip ic sp))
= CRule prd sc ip ic sp
type instance (WrapField PrdReco rule)
= rule
instance Require (OpComRA prd rule '[]) ctx where
type ReqR (OpComRA prd rule '[])
= Aspect '[ '(prd, rule)]
req ctx (OpComRA rule _) = ConsRec ((Label @prd) .=. rule) EmptyRec
instance
(Require (OpComRA' (Cmp prd prd') prd
(CRule prd sc ip ic sp)
( '(prd', rul) ': a)) ctx)
=>
Require (OpComRA prd (CRule prd sc ip ic sp)
( '(prd', rul) ': a)) ctx where
type ReqR (OpComRA prd (CRule prd sc ip ic sp)
( '(prd', rul) ': a))
= ReqR (OpComRA' (Cmp prd prd') prd (CRule prd sc ip ic sp)
( '(prd', rul) ': a))
req ctx (OpComRA rule a)
= req ctx (OpComRA' (Proxy @(Cmp prd prd'))rule a)
instance Require (OpComRA' 'LT prd (CRule prd sc ip ic sp)
a) ctx where
type ReqR (OpComRA' 'LT prd (CRule prd sc ip ic sp) a)
= Aspect ( '(prd, CRule prd sc ip ic sp) ': a)
req ctx (OpComRA' _ rule asp)
= (Label @prd .=. rule) `ConsRec` asp
instance
( Require (OpComRA prd rule a) ctx
, ReqR (OpComRA prd rule a)
~ Rec PrdReco (UnWrap @(NTName, ProdName) @Type (ReqR
(OpComRA prd rule
(a))))
)
=>
Require (OpComRA' 'GT prd rule
( '(prd', rule') ': a)) ctx where
type ReqR (OpComRA' 'GT prd rule
( '(prd', rule') ': a))
= Aspect ( '(prd', rule') ': (UnWrap @(NTName, ProdName)
(ReqR (OpComRA prd rule
(a)))))
req ctx (OpComRA' p rule (ConsRec tgrule' asp))
= tgrule' `ConsRec` (req ctx (OpComRA rule asp))
-- TODO: Do not allow mods
instance
( Ext prd sc ip ic sp sc' ip' ic' sp' scsc' ipip' icic' spsp'
, scsc' ~ (UnWrap @ChildName @[(AttName,Type)]
(ReqR (OpChiMerge sc sc')))
, ipip' ~ (UnWrap @AttName (ReqR (OpLJoin AttReco ip ip')))
, icic' ~ (UnWrap @ChildName @[(AttName,Type)]
(ReqR (OpChiMerge ic ic')))
, spsp' ~ (UnWrap @AttName (ReqR (OpLJoin AttReco sp sp')))
)
=> Require (OpComRA' 'EQ prd
(CRule prd sc ip ic sp)
( '(prd, CRule prd sc' ip' ic' sp') ': a)) ctx where
type ReqR (OpComRA' 'EQ prd
(CRule prd sc ip ic sp)
( '(prd, CRule prd sc' ip' ic' sp') ': a))
= Aspect ( '(prd, CRule prd
{-scsc'-} (UnWrap @ChildName @[(ProdName, Type)]
(ReqR (OpChiMerge sc sc')))
{-ipip'-} (UnWrap @AttName (ReqR (OpLJoin AttReco ip ip')))
{-icic'-} (UnWrap @ChildName @[(ProdName,Type)]
(ReqR (OpChiMerge ic ic')))
{-spsp'-} (UnWrap @AttName (ReqR (OpLJoin AttReco sp sp')))
) ': a)
req ctx (OpComRA' p rulef (ConsRec (TagField c l ruleg)
(asp :: Aspect a)))
= (TagField c l $ rulef .+. ruleg)
`ConsRec` asp
extAspect
:: ExtAspect prd sc ip ic sp a asp =>
CRule prd sc ip ic sp
-> CAspect a -> CAspect asp
extAspect rule (CAspect fasp)
= CAspect $ req (Proxy @'[]) (OpComRA rule (fasp))
type ExtAspect prd sc ip ic sp a asp
= (Require
(OpComRA prd (CRule prd sc ip ic sp) a) '[],
ReqR (OpComRA prd (CRule prd sc ip ic sp) a)
~ Rec PrdReco asp)
-- | An operator, alias for 'extAspect'. It combines a rule with an
-- aspect, to build a bigger one.
(.+:)
:: (RequireR (OpComRA prd (CRule prd sc ip ic sp) a)
(Rec PrdReco asp) '[]
) =>
CRule prd sc ip ic sp -> CAspect a -> CAspect asp
(.+:) = extAspect
infixr 3 .+:
-- | Unicode version of 'extAspect' or '.+:' (\\triangleleft)
(◃) = extAspect
infixr 3 ◃
-- | The other way, combines an aspect with a rule. It is a `flip`ped
-- 'extAspect'.
(.:+.) = flip extAspect
infixl 3 .:+.
-- | Unicode operator for '.:+.' or `flip extAspect`.
(▹) = flip extAspect
infixl 3 ▹
-- | Operator for 'comAspect'. It takes two 'CAspect's to build the
-- combination of both.
(.:+:) = comAspect
infixr 4 .:+:
-- | Unicode operator for 'comAspect' or '.:+:'. (\\bowtie)
(⋈) = comAspect
infixr 4 ⋈
-- rebinding syntax
(>>=) = (>>=.)
(>>) = (>>.)
return = ret
class EmptyAspect (g :: Grammar) where
type EmptyAspectR (g :: Grammar) :: [((NTName, ProdName), Type)]
emptyAspectFromGrammar :: Label g -> CAspect (EmptyAspectR g)
instance EmptyAspect ('Grammar '[]) where
type EmptyAspectR ('Grammar '[]) = '[]
emptyAspectFromGrammar Label = emptyAspect
instance
EmptyAspect ('Grammar nts)
=>
EmptyAspect ('Grammar ( '(nt, '[]) ': nts)) where
type EmptyAspectR ('Grammar ( '(nt, '[]) ': nts )) =
EmptyAspectR ('Grammar nts)
emptyAspectFromGrammar Label
= emptyAspectFromGrammar (Label @('Grammar nts))
instance
( RequireR
(OpComRA ntprd
(CRule ntprd
(ChiAtts 'True prd (GetTChildrenOfProd ('(prd, chis) : prds) prd))
'[]
(ChiAtts 'False prd (GetTChildrenOfProd ('(prd, chis) : prds) prd))
'[])
(EmptyAspectR ('Grammar ( '(nt, prds) ': nts)))
)
(Rec PrdReco
(UnWrap @(NTName, ProdName) @Type
(ReqR (OpComRA ntprd
(CRule ntprd
(ChiAtts 'True prd (GetTChildrenOfProd ('(prd, chis) : prds) prd))
'[]
(ChiAtts 'False prd (GetTChildrenOfProd ('(prd, chis) : prds) prd))
'[])
(EmptyAspectR ('Grammar ( '(nt, prds) ': nts))))))
) '[]
, ntprd ~ '(nt,prd)
, EmptyAspect ('Grammar ( '(nt, prds) ': nts))
, EmptyRule ('Grammar ( '(nt, '(prd, chis) ': prds) ': nts)) nt prd
)
=>
EmptyAspect ('Grammar ( '(nt, '(prd, chis) ': prds) ': nts)) where
type EmptyAspectR
('Grammar ( '(nt, '(prd, chis) ': prds) ': nts)) =
UnWrap
(ReqR (OpComRA '(nt, prd)
(CRule '(nt, prd)
(ChiAtts 'True prd (GetTChildrenOfProd ('(prd, chis) : prds) prd))
'[]
(ChiAtts 'False prd (GetTChildrenOfProd ('(prd, chis) : prds) prd))
'[])
(EmptyAspectR ('Grammar ( '(nt, prds) ': nts )))))
emptyAspectFromGrammar lgram
= (emptyRule lgram (Label @(Prd prd ('NT nt))))
.+: emptyAspectFromGrammar (Label @('Grammar ( '(nt, prds) ': nts)))
emptyAspG = emptyAspectFromGrammar
att :: forall (name :: AttName) (ty :: Type) . Label ('Att name ty)
att = Label
prd :: forall (g :: Grammar) (prd :: ProdName) .
(ProdG g prd) => --the way it is implemented requires both args instantiated
Label ('Prd prd (NTOfProd g prd))
prd = Label
chi :: forall (g :: Grammar) (chi :: ChildName) .
MemChiGram g chi ~ 'True => Label (GetChildL g chi)
chi = Label
class Kn (fcr :: [(ChildName, Type)]) where
type ICh fcr :: [(ChildName, [(AttName, Type)])]
type SCh fcr :: [(ChildName, [(AttName, Type)])]
kn :: Record fcr -> ChAttsRec (ICh fcr) -> ChAttsRec (SCh fcr)
instance Kn '[] where
type ICh '[] = '[]
type SCh '[] = '[]
kn _ _ = emptyCh
instance
Kn fc
=>
Kn ( '(lch , Attribution ich -> Attribution sch) ': fc) 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 ((ConsRec (TagField _ lch fch) (fcr :: Record fc)))
= \((ConsRec (TagField _ _ ich) icr)
:: ChAttsRec ( '(lch, ich) ': ICh fc))
-> let scr = kn fcr icr
in ConsRec (TaggedChAttr lch
(fch ich)) scr
knit ::
Kn (fc :: [(ChildName, Type)])
=> Proxy ctx
-> CRule prd (SCh fc) ip (ICh fc) sp
-> Record fc
-> Attribution ip
-> Attribution sp
knit ctx rule fc ip
= let (Fam ic sp) = mkRule rule (Fam sc ip)
sc = kn fc ic
in sp
-- building the argument of knit
class FC (g :: Grammar) (chis :: [(ChildName, GSym)])
(prd :: ProdName)
asp
(ipsp :: [(NTName, [(AttName, Type)], [(AttName, Type)])])
where
type BuildFC g chis prd asp ipsp :: [(ChildName, Type)]
buildFC :: Label g -> Label chis -> Label prd -> Label ipsp
-> CAspect asp
-> HList (ChList2HList g chis)
-> Record (BuildFC g chis prd asp ipsp)
instance FC g '[] prd asp ipsp where
type BuildFC g '[] prd asp ipsp = '[]
buildFC Label Label Label Label asp HNil = emptyRecord
instance
( FC g chis prd asp ipsp
, ReqR (OpExtend @ChildName @Type Reco chnam
(Attribution '[] -> Attribution '[ '("term", t)])
(BuildFC g chis prd asp ipsp))
~ Rec @Type @ChildName @Type Reco
( '(chnam, Attribution '[] -> Attribution '[ '("term", t)])
': (BuildFC g chis prd asp ipsp))
, ChList2HList g ('(chnam, 'Ter t) : chis)
~ (t : xs)
)
=>
FC g ( '(chnam, 'Ter t) ': chis) prd asp ipsp where
type BuildFC g ( '(chnam, 'Ter t) ': chis) prd asp ipsp
= '(chnam, Attribution '[] -> Attribution '[ '("term", t)])
': BuildFC g chis prd asp ipsp
buildFC prG pChis pprd p asp (HCons x xs)
= (Label @chnam .=. sem_Lit x) `ConsRec`
buildFC @g @_
prG (lTail pChis) pprd p asp xs
instance
( FC g chis prd r a
, SemAG' g a r nt (I nt a)(S nt a)
, GetChildL g chnam ~ Chi chnam ('Prd prdch nt2) nt1
)
=>
FC g ( '(chnam, 'NonTer nt) ': chis) prd r a where
type BuildFC g ( '(chnam, 'NonTer nt) ': chis) prd r a
= '(chnam, Attribution (I nt a)
-> Attribution (S nt a))
': BuildFC g chis prd r a
buildFC prG pChis pPrd pIPSP asp (HCons x xs)
= (Label @chnam .=. semAG' pIPSP asp x)
`ConsRec` buildFC prG (lTail pChis) pPrd pIPSP asp xs
-- | Semantic functions
class SemLit a where
sem_Lit :: a -> Attribution ('[] :: [(AttName,Type)])
-> Attribution '[ '("term", a)]
lit :: Label ('Att "term" a)
instance SemLit a where
sem_Lit a _ = (Label =. a) *. emptyAtt
lit = Label @('Att "term" a)
-- | The function 'sem' is the semantic function for an AG (g, ipsps, asp).
-- (corresponding to (G,A,R) in the usual definition).
type AttrTy = [(AttName, Type)]
type AttrCol = [(NTName, AttrTy, AttrTy)]
class SemAG' (g :: Grammar) (a :: AttrCol) r (nt :: NTName) ip sp where
semAG' :: Label a -> CAspect r -> EADT g nt
-> Attribution ip -> Attribution sp
class SemAGPrds (prds :: [(ProdName, [(ChildName, GSym)])])
(g :: Grammar) (a :: AttrCol) r (nt :: NTName) ip sp
where
semAGPrds :: Label prds -> Label a -> CAspect r -> EADT g nt
-> Attribution ip -> Attribution sp
instance
SemAGPrds (GetTProdsOfNT g nt) g a r nt ip sp
=>
SemAG' g a r nt ip sp where
semAG' p asp v = semAGPrds (Label @(GetTProdsOfNT g nt)) p asp v
instance
(KnownSymbol prd
, ChList2HList g (GetTChildrenOfProd (GetTProdsOfNT g nt) prd)
~ ChList2HList g chis
, RequireR (OpLookup PrdReco '(nt, prd) r)
(CRule '(nt, prd)
(SCh (BuildFC g chis prd r a))
ip
(ICh (BuildFC g chis prd r a))
sp) '[]
, FC g chis prd r a
, Kn (BuildFC g chis prd r a)
)
=> SemAGPrds '[ '(prd, chis)] g a r nt ip sp
where
semAGPrds lprds lipsp asp (Variant (lprd :: SSymbol prd') args)
= case sameSymbol lprd (symbolSing @prd) of
Just p@Refl -> knitAspect (Label @'(nt, prd)) asp
(buildFC (Label @g) (Label @chis)
(Label @prd) (Label @a) asp args)
_ -> error "impossible"
instance
( ChList2HList g (GetTChildrenOfProd (GetTProdsOfNT g nt) prd)
~ ChList2HList g chis
, (GetTChildrenOfProd (GetTProdsOfNT g nt) prd) ~ chis
, KnownSymbol prd
, RequireR (OpLeftProj AttReco (LabelsOf (I nt ipsp)) ip)
(Rec AttReco (I nt ipsp)) '[]
, RequireR (OpLookup PrdReco '(nt,prd) asp)
(CRule '(nt, prd)
(SCh (BuildFC g chis prd asp ipsp))
(I nt ipsp)
(ICh (BuildFC g chis prd asp ipsp))
(SP (Lookup1 nt asp)))
'[]
, FC g chis prd asp ipsp
, Kn (BuildFC g chis prd asp ipsp)
, SemAGPrds prds g ipsp asp nt ip sp
, IP (Lookup1 nt asp) ~ I nt ipsp
, SP (Lookup1 nt asp) ~ S nt ipsp
, S nt ipsp ~ sp
, I nt ipsp ~ ip
)
=>
SemAGPrds ( '(prd, chis) ': prds) g ipsp asp nt ip sp where
semAGPrds pprds pipsp asp v@(Variant (lprd :: SSymbol prd') args)
= case sameSymbol lprd (symbolSing @prd) of
Just p@Refl -> knitAspect (Label @('(nt,prd))) asp
(buildFC (Label @g) (Label @chis)
(Label @prd) (Label @ipsp) asp args)
Nothing -> semAGPrds (lTail pprds) pipsp asp v
-- exported
type family SemAG g a r nt ip sp where
SemAG g a r nt ip sp = ( SemAG' g a (NormalizeAspR g r a) nt ip sp
, NormalizeAsp g r a )
semAG ::
( SemAG g a r nt ip sp
, Check g a (NormalizeAspR g r a)
)
=> Label a -> CAspect r -> EADT g nt
-> Attribution ip -> Attribution sp
semAG a r (e :: EADT g nt) = semAG' a (normalizeAsp (Label @g) r a) e
type Sem :: Grammar
-> [((NTName, ProdName), Type)]
-> NTName
-> [(AttName, Type)]
-> [(AttName, Type)]
-> Constraint
type family Sem g r nt ip sp
type instance Sem g r nt ip sp
= ( SemAG g (Infer g r) r nt ip sp
, Check g (Infer g r) (NormalizeAspR g r (Infer g r)))
-- TODO: es mas elegante asi pero recomputamos Infer,
-- debería ser más eficiente agregar estas constraints a sem:
-- ( SemAG g a r nt ip sp
-- , Check g a (NormalizeAspR g r a)
-- , a ~ Infer g r)
--
-- se puede mejorar tambien con una tf intermedia,
-- igual no sabemos como va a decidir reducirse la tf...
-- | Semantic function, inferring the attribute occurrences @a@
sem :: Sem g r nt ip sp
=> CAspect r -> EADT g nt
-> Attribution ip -> Attribution sp
sem (r :: CAspect r) (e :: EADT g nt) = semAG (Label @(Infer g r)) r e
knitAspect ::
(RequireR (OpLookup PrdReco ntprd asp)
(CRule ntprd (SCh fc)
ip (ICh fc)
sp) '[]
, Kn fc
, ntprd ~ '(nt, prd)
)
=> Label ntprd
-> CAspect asp
-> Record fc
-> Attribution ip
-> Attribution sp
knitAspect (prd :: Label ntprd) asp fc ip
= let ctx = Proxy @'[]
in let rul = req ctx (OpLookup prd (mkAspect asp))
in knit ctx rul fc ip
-- | given a non-terminal 'nt' and an attribute declaration 'ipsp',
-- gets the inherited attributes
type family I
(nt :: NTName)
(ipsp :: [(NTName, [(AttName, Type)], [(AttName, Type)])])
:: [(AttName, Type)]
where
I nt ( '(nt, ip, sp) ': ipsps ) = ip
I nt ( _ ': ipsps ) = I nt ipsps
I nt '[] = '[] -- cuidado
type family S
(nt :: NTName)
(ipsp :: [(NTName, [(AttName, Type)], [(AttName, Type)])])
:: [(AttName, Type)]
where
S nt ( '(nt, ip, sp) ': ipsps ) = sp
S nt ( _ ': ipsps ) = S nt ipsps
S nt '[] = '[]
class NormalizeAsp (g :: Grammar) asp
(ipsp :: [(NTName, [(AttName, Type)], [(AttName, Type)])])
where
type NormalizeAspR g asp ipsp :: [((NTName, ProdName), Type)]
normalizeAsp :: Label g -> CAspect asp -> Label ipsp
-> CAspect (NormalizeAspR g asp ipsp)
instance NormalizeAsp g '[] ipsp where
type NormalizeAspR g '[] ipsp = '[]
normalizeAsp g asp ipsp = asp
instance
( NormalizeAsp g asp ipsp
, NormalizeRule g prd nt (CRule '(nt, prd) sc ip ic sp) ipsp
)
=> NormalizeAsp g ( '( '(nt, prd) , CRule '(nt, prd) sc ip ic sp) ': asp) ipsp
where
type NormalizeAspR g ( '( '(nt, prd) , CRule '(nt, prd) sc ip ic sp) ': asp) ipsp
= '( '(nt, prd) , NormalizeRuleR g prd nt (CRule '(nt, prd) sc ip ic sp) ipsp)
': NormalizeAspR g asp ipsp
normalizeAsp lG (CAspect (ConsRec (TagField (c@Label) l r) asp)) lIPSP
= CAspect $ (ConsRec (TagField c l
(normalizeRule lG (Label @prd) (Label @nt) r lIPSP))
(mkAspect $ normalizeAsp lG (CAspect asp) lIPSP))
class NormalizeRule (g :: Grammar)
(prd :: ProdName)
(nt :: NTName)
(rule :: Type)
(ipsp :: [(NTName, [(AttName, Type)], [(AttName, Type)])])
where
type NormalizeRuleR g prd nt rule ipsp :: Type
normalizeRule :: Label g -> Label prd -> Label nt-> rule -> Label ipsp
-> NormalizeRuleR g prd nt rule ipsp
instance
( EmptyRuleNormal g nt prd ipsp
, ReqR (OpChiMerge sc (SC (EmptyRuleNormalR g nt prd ipsp)))
~ Rec ChiReco scsc'
, Ext '(prd, nt) sc ip ic sp
(SC (EmptyRuleNormalR g nt prd ipsp))
(IP (EmptyRuleNormalR g nt prd ipsp))
(IC (EmptyRuleNormalR g nt prd ipsp))
(SP (EmptyRuleNormalR g nt prd ipsp))
scsc' ipip' ic sp
, ReqR (OpLeftProj AttReco (LabelsOf (I nt ipsp)) ipip')
~ Rec AttReco (I nt ipsp)
, ReqR (OpLJoin AttReco ip (I nt ipsp)) ~ Rec AttReco ipip'
, Require (OpLJoin AttReco sp '[]) '[]
, ReqR (OpLJoin AttReco sp '[]) ~ Rec AttReco sp
, ReqR (OpChiMerge ic (ChiAttsNormal False prd
(GetTChildrenOfProd' (GetTProdsOfNT g nt)
(GetTProdsOfNT g nt) prd) ipsp))
~ Rec ChiReco ic
, EmptyChiAttsNormal prd
(GetTChildrenOfProd' (GetTProdsOfNT g nt) (GetTProdsOfNT g nt) prd)
ipsp
)
=> NormalizeRule g prd nt (CRule '(nt, prd) sc ip ic sp) ipsp where
type NormalizeRuleR g prd nt (CRule '(nt, prd) sc ip ic sp) ipsp
= CRule '(nt, prd)
(UnWrap @ChildName
(ReqR (OpChiMerge sc (SC (EmptyRuleNormalR g nt prd ipsp)))))
(UnWrap (ReqR (OpLJoin AttReco ip (IP (EmptyRuleNormalR g nt prd ipsp)))))
ic sp
normalizeRule lG lPrd lNt rule lIPSP
= rule .+. (emptyRuleNormal lG lPrd lNt lIPSP)
-- infers ipsps from aspect, grammar is used to watch nts
type family Infer
(g :: Grammar)
(asp :: [((NTName, ProdName), Type)])
:: [(NTName, [(AttName, Type)], [(AttName, Type)])]
where
Infer g '[] = '[]
Infer g ( '( '(nt, prd), CRule '(nt, prd) sc ip ic sp) ': nts)
= CombineIPSPList '[ '[ '(nt, ip , sp)] ,
-- cada ocurrencia fuerza la aparicion en todos, esto se puede cambiar
InferSC g sc,
Infer g nts ]
-- computes synthesized atts from the input fam
-- to avoid
type family InferSC
(g :: Grammar)
(sc :: [(ChildName,[(AttName, Type)])])
:: [(NTName, [(AttName, Type)], [(AttName, Type)])]
where
InferSC g '[] = '[]
InferSC g ( '(chi, atts) ': chis)
= InferSCDec (GetNTChi (GetChildL g chi))
g ( '(chi, atts) ': chis)
type family InferSCDec
(b :: Maybe NTName)
(g :: Grammar)
(sc :: [(ChildName,[(AttName, Type)])])
:: [(NTName, [(AttName, Type)], [(AttName, Type)])]
where
InferSCDec ('Just nt) g ( '(chi, atts) ': chis)
= (CombineIPSPList
'[ '[ '(nt, '[], atts)]
, InferSC g chis])
InferSCDec 'Nothing g ( '(chi, atts) ': chis)
= InferSC g chis
type family Check
(g :: Grammar)
(ipsps :: [(NTName, [(AttName, Type)], [(AttName, Type)])])
(asp :: [((NTName, ProdName), Type)])
:: Constraint where
Check g ipsps asp = ToConstraint (CheckErrors g ipsps asp)
type family ToConstraint (e :: [ErrorMessage]) :: Constraint where
ToConstraint '[] = ()
ToConstraint (e ': es) = (TypeError e, ToConstraint es)
type family CheckErrors
(g :: Grammar)
(ipsps :: [(NTName, [(AttName, Type)], [(AttName, Type)])])
(asp :: [((NTName, ProdName), Type)])
:: [ErrorMessage]
where
CheckErrors g ipsps '[] = '[]
CheckErrors g ipsps
( '( '(nt, prd), CRule '(nt, prd) sc ip ic sp) ': asp) =
CheckIP g ipsps nt prd ip
:++ CheckSC g ipsps nt prd sc
-- ^ con estas hay que mirar que no se requieran args extra, TODO
:++ CheckSP g ipsps nt prd sp -- por lo menos los atts en ipsps
:++ CheckIC g ipsps nt prd ic -- lo mismo aca
:++ CheckErrors g ipsps asp
type family CheckIP g ipsps nt prd ip where
CheckIP g ipsps nt prd ip
= If (SubsetAtt ip (I nt ipsps)) '[]
'[Text ("error:\n\
\ Rule for production " :+ WrapQuotes prd
:+ " of non-terminal " :+ WrapQuotes nt :+
"\n requires inherited attributes: ")
:$$: ShowAsp ip
:$$: Text
"but it should require \
\a subset of:"
:$$: ShowAsp (I nt ipsps)]
type family CheckSP g ipsps nt prd sp where
CheckSP g ipsps nt prd sp
= If (SubsetAtt (S nt ipsps) sp) '[]
'[Text ("error:\n\
\ Rule for production " :+ WrapQuotes prd
:+ " of non-terminal " :+ WrapQuotes nt :+
"\n computes synthesized attributes: ")
:$$: ShowAsp sp
:$$: Text
"but from the full aspect type it is inferred it should compute:"
:$$: ShowAsp (S nt ipsps)]
type family WrapQuotes (t :: Symbol) where
WrapQuotes t = "\"" :+ t :+ "\""
type family ShowAsp asp :: ErrorMessage where
ShowAsp asp = Text "\t" :<>: ShowType asp
type family CheckIC g ipsps nt prd ic where
CheckIC g ipsps nt prd '[] = '[]
CheckIC g ipsps nt prd ( '(chnam, att) ': chis)
= CheckIC' g ipsps nt prd chnam att (GetGSymChildL (GetChildL g chnam))
:++ CheckIC g ipsps nt prd chis
type family CheckIC' g ipsps nt prd chnam att gsym where
CheckIC' g ipsps nt prd chnam att gsym
= CheckIC'' g ipsps nt prd chnam att (IsNonTer gsym) gsym
type family CheckIC'' g ipsps nt prd chnam att b gsym where
CheckIC'' g ipsps nt prd chnam att 'False gsym = '[]
CheckIC'' g ipsps nt prd chnam att 'True ('NonTer ntch)
= If (SubsetAtt (I ntch ipsps) att) '[]
'[Text ("error:\n\
\ Semantics for production " :+ WrapQuotes prd
:+ " of non-terminal " :+ WrapQuotes nt
:+ " at children " :+ WrapQuotes chnam
:+ "\n define in the following inherited attributes: ")
:$$: ShowAsp att
:$$: Text
"but from the full aspect type it is inferred the following are needed:"
:$$: ShowAsp (I nt ipsps)]
type family CheckSC g ipsps nt prd sc where
CheckSC g ipsps nt prd '[] = '[]
CheckSC g ipsps nt prd ( '(chnam, att) ': chis)
= CheckSC' g ipsps nt prd chnam att (GetGSymChildL (GetChildL g chnam))
:++ CheckSC g ipsps nt prd chis
type family CheckSC' g ipsps nt prd chnam att gsym where
CheckSC' g ipsps nt prd chnam att gsym
= CheckSC'' g ipsps nt prd chnam att (IsNonTer gsym) gsym
type family CheckSC'' g ipsps nt prd chnam att b gsym where
CheckSC'' g ipsps nt prd chnam att 'False gsym = '[]
CheckSC'' g ipsps nt prd chnam att 'True ('NonTer ntch)
= If (att == (S ntch ipsps)) '[]
'[Text ("error:\n\
\ Semantics for production " :+ WrapQuotes prd
:+ " of non-terminal " :+ WrapQuotes nt
:+ " at children " :+ WrapQuotes chnam
:+ "\n depend on the following synthesized attributes: ")
:$$: ShowAsp att
:$$: Text
"but they should depend at most of:"
:$$: ShowAsp (S ntch ipsps)
:$$: Text "..."]
infer :: Label g -> CAspect asp -> Label (Infer g asp)
infer Label asp = Label
check :: (Check g (Infer g asp) asp)
=> Label g -> CAspect asp -> Label (Infer g asp)
check Label asp = Label
type family SubsetAtt (atts :: [(AttName, Type)])
(atts' :: [(AttName, Type)]) :: Bool where
SubsetAtt '[] att' = 'True
SubsetAtt ( '(att, ty) ': atts) '[] = 'False
SubsetAtt ( '(att, ty) ': atts)
( '(att', ty') ': atts')
= SubsetAttAux (Compare att att')
( '(att, ty) ': atts)
( '(att', ty') ': atts')
type family SubsetAttAux (o :: Ordering)
(atts :: [(AttName, Type)])
(atts' :: [(AttName, Type)]) :: Bool where
SubsetAttAux 'EQ ( '(att, ty) ': atts)
( '(att', ty') ': atts') --y si distinto tipo?
= SubsetAtt atts atts'
SubsetAttAux 'LT ( '(att, ty) ': atts)
( '(att', ty') ': atts')
= 'False
SubsetAttAux 'GT ( '(att, ty) ': atts)
( '(att', ty') ': atts')
= SubsetAtt ( '(att, ty) ': atts) atts'
copyAtChi (att :: Label ('Att att t))
(l :: Label ('Chi ch ('Prd prd ('NT nt)) ntch))
= inhdefM att
(Label @('Prd prd ('NT nt)))
l (at lhs att)
class CopyAtChis (att :: Att) (g :: Grammar) (l :: [Child]) where
type CopyAtChisR att g l :: [((NTName,ProdName), Type)]
copyAtChis :: Label g -> Label att -> Proxy l
-> CAspect (CopyAtChisR att g l)
copyAtChiList :: (CopyAtChis ('Att att t) g l) =>
Label g -> Label ('Att att t)-> LList l -> CAspect (CopyAtChisR ('Att att t) g l)
copyAtChiList g att (l :: LList l) = copyAtChis g att (Proxy @l)
instance CopyAtChis att g '[] where
type CopyAtChisR att g '[] = '[]
copyAtChis _ att _ = emptyAspect
instance
( CopyAtChis ('Att att t) g chs
, RequireR
(OpComRA '(nt, prd)
(CRule '(nt, prd) '[] '[ '(att, t)] '[ '(ch, '[ '(att, t)])] '[])
(CopyAtChisR ('Att att t) g chs))
(Rec @Type @(NTName, ProdName) @Type
PrdReco (UnWrap (ReqR (OpComRA '(nt, prd)
(CRule '(nt, prd) '[] '[ '(att, t)] '[ '(ch, '[ '(att, t)])] '[])
(CopyAtChisR ('Att att t) g chs))))) '[]
)
=> CopyAtChis ('Att att t) g ( 'Chi ch ('Prd prd ('NT nt)) ntch ': chs)
where
type CopyAtChisR ('Att att t) g ( 'Chi ch('Prd prd ('NT nt)) ntch ': chs)
= UnWrap @(Symbol, Symbol)
(ReqR (OpComRA '(nt, prd)
(CRule '(nt, prd) '[] '[ '(att, t)] '[ '(ch, '[ '(att, t)])] '[])
(CopyAtChisR ('Att att t) g chs)))
copyAtChis lg att
(Proxy :: Proxy ('Chi ch('Prd prd ('NT nt)) ntch ': chis))
= (copyAtChi att (Label @('Chi ch('Prd prd ('NT nt)) ntch)))
.+: (copyAtChis lg att (Proxy @chis))