ruler-0.4.0.0: src/TrfAS2/GenARule.cag
-------------------------------------------------------------------------
-- Generate ARule's from attr bindings
-------------------------------------------------------------------------
%%[1 hs module (TrfAS2.GenARule)
%%]
%%[1 hs export (as2ARule)
%%]
%%[1 hs import (Data.Maybe, Data.Char, Data.List, qualified Data.Set as Set, qualified Data.Map as Map, UHC.Util.Utils)
%%]
%%[1 hs import (Opts, Err, Common, KeywParser( propsSynInhMp ), Expr.Utils, ARule.Utils, FmGam, RwExprGam)
%%]
%%[1 hs import (ECnstrGam, AbsSyn.AbsSyn2, Admin, Utils( sc2DATA ))
%%]
%%[1 hs import (UHC.Util.Pretty)
%%]
-------------------------------------------------------------------------
-- Inclusion of split off parts
-------------------------------------------------------------------------
%%[1 ag import ({AbsSyn/AbsSyn2AG}, {AbsSyn/CommonAG}, {AS2/Opts}, {TrfAS2/CommonAG})
%%]
%%[1 ag import ({Expr/AbsSynAG}, {Expr/SelfAG})
%%]
%%[1 ag import ({ARule/AbsSynAG}, {ARule/SelfAG})
%%]
-------------------------------------------------------------------------
-- Interfacing to AST
-------------------------------------------------------------------------
%%[1 ag
WRAPPER AGItf
%%]
%%[1 hs
as2ARule :: Opts -> DtInvGam -> ScGam Expr -> FmGam Expr -> RwExprGam -> Decls -> (Decls,PP_Doc,[Err])
as2ARule o dig scg fmg rwg r
= (self_Syn_AGItf r2,ppDbg_Syn_AGItf r2,errL_Syn_AGItf r2)
where r1 = sem_AGItf (AGItf_AGItf r)
r2 = wrap_AGItf r1
(Inh_AGItf {opts_Inh_AGItf = o, fmGam_Inh_AGItf = fmg, rwGam_Inh_AGItf = rwg, scGam_Inh_AGItf = scg, dtInvGam_Inh_AGItf = dig})
%%]
-------------------------------------------------------------------------
-- Context: dtInvGam
-------------------------------------------------------------------------
%%[1 ag
ATTR AllAS2 AGItf [ dtInvGam: DtInvGam | | ]
%%]
-------------------------------------------------------------------------
-- Context: options, position, etc
-------------------------------------------------------------------------
%%[1 ag
ATTR AllJd AllAt [ pos: SPos | | ]
SEM RlDecl
| Rl LTX loc . pos = @pos
%%]
-------------------------------------------------------------------------
-- Context: substitution
-------------------------------------------------------------------------
%%[1 ag
SEM JdAt
| At loc . sbse = exprSubst (@lhs.opts {optSubstFullNm=False}) @lhs.fmGam
. sbsn = nmSubst (@lhs.opts {optSubstFullNm=False}) @lhs.fmGam
SEM Jd
| Ats loc . sbse = exprSubst (@lhs.opts {optSubstFullNm=False}) @lhs.fmGam
. sbsn = nmSubst (@lhs.opts {optSubstFullNm=False}) @lhs.fmGam
SEM RlDecl
| Rl loc . sbse = exprSubst (@lhs.opts {optSubstFullNm=False}) @lhs.fmGam
. sbsn = nmSubst (@lhs.opts {optSubstFullNm=False}) @lhs.fmGam
%%]
-------------------------------------------------------------------------
-- Context: scInfo, ... + dtInfo, ...
-------------------------------------------------------------------------
%%[1 ag
SEM RlDecl
| Rl loc . rsScInfo = maybe (panic "RlDecl_Rl: rsScInfo") id $ gamLookup @lhs.rsScNm @lhs.scGam
. (_,_,daInvInfo)
= maybe (undefined,undefined,emptyDtAltInvInfo) id
$ dtVwRlInvGamLookup @lhs.rsScNm @lhs.vwNm @rlNm @lhs.dtInvGam
SEM Jd
| Ats loc . (scInfo,vwScInfo)
= maybe (panic "Jd_Ats: scInfo") id
$ scVwGamLookup @scNm @lhs.vwNm @lhs.scGam
%%]
-------------------------------------------------------------------------
-- Context: is a judgement (and not a relation)?
-------------------------------------------------------------------------
%%[1 ag
ATTR AllAt [ isJd: Bool | | ]
SEM Jd
| Ats loc . isJd = scKind @scInfo == ScJudge
%%]
-------------------------------------------------------------------------
-- Context: is in premise?
-------------------------------------------------------------------------
%%[1 ag
ATTR AllJd AllAt [ isPre: Bool | | ]
SEM RlDecl
| Rl LTX preJds . isPre = True
postJds . isPre = False
%%]
-------------------------------------------------------------------------
-- Context: name info from higher up
-------------------------------------------------------------------------
%%[1 ag
ATTR AllJd [ agStr: Nm | | ]
SEM RlDecl
| Rl loc . agStr = @agStr
| * - Rl loc . agStr = nmNone
%%]
-------------------------------------------------------------------------
-- Context: scAtGam
-------------------------------------------------------------------------
%%[1 ag
ATTR AllAt [ scAtGam: AtGam | | ]
SEM Jd
| Ats ats . scAtGam = vwscFullAtGam @vwScInfo
SEM JdAt
| At loc . atInfo = maybe emptyAtInfo id $ gamLookup @nm @lhs.scAtGam
. propRetain = [AtRetain] `atFilterProps` @atInfo
%%]
-------------------------------------------------------------------------
-- Local properties for attr
-------------------------------------------------------------------------
%%[1 ag
SEM JdAt
| At loc . dir = atDefUse @lhs.isPre @atInfo
. isBi = Map.elems propsSynInhMp `atHasProps` @atInfo
. isExtern = AtExtern `atHasProp` @atInfo
SEM JdAt
| At loc . atTy = atTy @atInfo
. atCnstr = ECnstr_Ty [@atTy]
%%]
-------------------------------------------------------------------------
-- Context: node name
-------------------------------------------------------------------------
%%[1 ag
ATTR JdAt [ | | mbNmNd: {Maybe Nm} ]
ATTR JdAts [ | | gathNmNd: Nm ]
ATTR AllAt [ | | gathExNd: Expr ]
SEM JdAt
| At lhs . mbNmNd = if @dir == ADNode then Just @nm else Nothing
. gathExNd = @expr.self
SEM JdAts
| Nil lhs . gathNmNd = nmUnk
. gathExNd = exprUnk
| Cons lhs . (gathNmNd,gathExNd)
= maybe (@tl.gathNmNd,@tl.gathExNd) (\n -> (n,@hd.gathExNd)) @hd.mbNmNd
ATTR AllAt [ nmNd: Nm | | ]
SEM Jd
| Ats loc . nmNd = if @lhs.isPre then exprAsNm $ @sbse $ @ats.gathExNd else nmLhs
%%]
-------------------------------------------------------------------------
-- Scheme of children node map/gam
-------------------------------------------------------------------------
ATTR AllJd [ | | ndToScGam USE {`gamUnion`} {Map.empty}: {Gam Nm Nm} ]
SEM Jd
| Ats lhs . ndToScGam = gamSingleton @nmNd @scNm
-------------------------------------------------------------------------
-- Node order gam
-------------------------------------------------------------------------
%%[1 ag
ATTR AllJd [ | | coGam USE {`gamUnion`} {emptyGam}: ChOrdGam ]
SEM Jd
| Ats loc . exNdNmS = exprNmS @ats.gathExNd
. exNdFmGam = fmGamFromList' @lhs.fm [ (n,mkAFld . @sbsn $ n) | n <- Set.toList @exNdNmS ]
lhs . coGam = let sbse = exprSubst (@lhs.opts {optSubstFullNm=False}) @exNdFmGam
cg1 = exprCoGam . sbse $ @ats.gathExNd
in cg1
SEM RlDecl
| Rl loc . coNmL = let cg1 = @postJds.coGam
cg2 = gamMapKeys @sbsn $ daiChOrdGam @daInvInfo
in coGamNmL (if gamIsEmpty cg1 then cg2 else cg1)
%%]
-------------------------------------------------------------------------
-- Attr bindings as FmGam
-------------------------------------------------------------------------
%%[1 ag
ATTR AllAt [ | | atFmGam USE {`fmGamUnion`} {emptyGam}: {FmGam (Expr,ECnstr)} ]
SEM JdAt
| At lhs . atFmGam = if False -- exprAsNm @expr.self == nmWild
then emptyGam
else fmSingleton @nm @lhs.fm (@expr.self,@atCnstr)
%%]
-------------------------------------------------------------------------
-- Building blocks for transforming
-------------------------------------------------------------------------
%%[1 ag
SEM JdAt
| At loc . nmAdapt = if @isBi then nmInit else id
. nmSbs = Nm . nmShowAG . @sbsn . @nmAdapt $ @nm
. defLhs = if @lhs.isPre then mkANd @lhs.nmNd @nmSbs else mkALhs' @propRetain @nmSbs
. defRhs = @expr.self
. useLhs = @expr.self
. useRhs = if @lhs.isPre then mkANd @lhs.nmNd @nmSbs else mkALhs @nmSbs
%%]
-------------------------------------------------------------------------
-- Introduced names, mapped to AG equivalent
-------------------------------------------------------------------------
%%[1 ag
ATTR AllJd AllAt [ | | introFmGam USE {`fmGamUnion`} {emptyGam}: {FmGam Expr} ]
SEM JdAt
| At loc . introFmGam = case @dir of
ADUse -> fmGamFromList' @lhs.fm [ (n,mkALoc' n') | (n,n') <- nmRefAscL ]
where nmRefAscL = [ (n,Nm . nmShowAG . @sbsn {- . nmAdapt -} $ n) | n <- Set.toList (exprNmS @useLhs), n /= nmWild ]
_ -> emptyGam
SEM Jd
| Ats lhs . introFmGam = case scKind @scInfo of
ScJudge | not @lhs.isPre -> @exNdFmGam `fmGamUnion` @ats.introFmGam
_ -> @ats.introFmGam
SEM RlDecl
| Rl loc . introFmGam = @preJds.introFmGam `fmGamUnion` @postJds.introFmGam
%%]
-------------------------------------------------------------------------
-- Full fmGam
-------------------------------------------------------------------------
%%[1 ag
SEM RlDecl
| Rl loc . fullFmGam = @introFmGam `fmGamUnion` @lhs.fmGam
%%]
-------------------------------------------------------------------------
-- Constraint gam
-------------------------------------------------------------------------
%%[1 ag
ATTR AllJd AllAt [ | | introECGam USE {`gamUnion`} {emptyGam}: ECnstrGam ]
SEM JdAt
| At lhs . introECGam = @introECGam
SEM Jd
| Ats lhs . introECGam = @introECGam
SEM RlDecl
| Rl loc . introECGam = gamMapKeys
(exprSubst (@lhs.opts {optSubstFullNm=False}) @fullFmGam)
(@preJds.introECGam `gamUnion` @postJds.introECGam)
%%]
-------------------------------------------------------------------------
-- 'Attr defined' gam
-------------------------------------------------------------------------
%%[1 ag
ATTR AllJd AllAt [ | | introADGam USE {`gamUnion`} {emptyGam}: AtDefdGam ]
SEM JdAt
| At lhs . introADGam = case @dir of
ADDef -> gamFromAssocs [(@nmSbs,@isBi)]
_ -> emptyGam
SEM RlDecl
| Rl loc . adGam = @preJds.introADGam `gamUnion` @postJds.introADGam
%%]
-------------------------------------------------------------------------
-- 'Attr defined' gam, new version
-------------------------------------------------------------------------
%%[1 ag
ATTR AllJd AllAt [ | | introAD2Gam USE {`adGamUnion`} {emptyGam}: {AtDefdGam'} ]
SEM JdAt
| At lhs . introAD2Gam = case @dir of
ADUse | @lhs.isJd
-> gamFromAssocs [(@nmSbs,Set.singleton @lhs.nmNd)]
_ -> emptyGam
SEM RlDecl
| Rl loc . ad2Gam = @preJds.introAD2Gam `adGamUnion` @postJds.introAD2Gam
%%]
-------------------------------------------------------------------------
-- Replica
-------------------------------------------------------------------------
%%[1 ag
ATTR AllAt AllJd [ | | exprEqnL USE {++} {[]}: {[Expr]} ]
SEM JdAt
| At loc . (exprEqnL,introECGam)
= let mk l r = ([eqn2],ecGam `gamUnion` ecGamFromList [ (l,@atCnstr), (r,@atCnstr) ])
where eqn1 = mkExprEqn l r
(eqn2,ecGam) = exprElimCnstr eqn1
in case @dir of
ADUse | not (fmNull @introFmGam)
-> mk @useLhs @useRhs
ADDef | not @isExtern
-> mk @defLhs @defRhs
_ -> ([],emptyGam)
SEM Jd
| Ats loc . (exprEqnL,introECGam,eqnErrs)
= case scKind @scInfo of
ScJudge
-> (@ats.exprEqnL,@ats.introECGam,[])
ScRelation
-> (exprLines jd2,introECGam2,concat jd1ErrLL)
where jd1 = fkGamLookup exprUnk jdshExpr [@lhs.fm] . vwscJdShpGam $ @vwScInfo
(jd1EqlL,jd1ErrLL)
= unzip
[ maybe (Map.empty,[Err_NotAEqnForm @lhs.pos (pp l)]) (\e -> (e,[])) (exprCheckAEqnForm l)
| l <- exprLines jd1
]
jd2 = exprSubst (@lhs.opts {optSubstOnce=True}) (fmGamMap (const fst) @ats.atFmGam) jd1
mkG eqm gn
= if null n1 then [] else n1 ++ mkG (foldr (\(e,_) m -> Map.delete e m) eqm n1) n1
where n1 = [ (exprEnsureAppTop e',c) | (e,c) <- gn, e' <- maybeToList (Map.lookup e eqm) ]
(introECL,introECGL)
= unzip [ ((e,c),eg) | (_,(e,c)) <- fmGamToList' @lhs.fm @ats.atFmGam, let (e',eg) = exprElimCnstr e ]
introECGam2
= (ecGamFromList $ introECL ++ mkG (Map.unions jd1EqlL) introECL)
`gamUnion` gamUnions introECGL
SEM RlDecl
| Rl (lhs.self,loc.selfNonOptim1,loc.selfNonOptim2)
= let (eqnLL,eqnGamL)
= unzip
[ (es,g)
| e <- @preJds.exprEqnL ++ @postJds.exprEqnL
, let (_,es,g) = exprRewrite' (@lhs.opts {optSubstFullNm=False}) @fullFmGam @lhs.rwGam @introECGam e
]
aRule1
= ARule_Rule
[sc2DATA @rsScInfo @lhs.dtInvGam]
@agStr
["rule " ++ show @rlNm,"view " ++ show @lhs.vwNm]
(concat eqnLL)
aRule2
= arlUniq @lhs.fmGam @coNmL
$ arlSubst (fmGamUnions eqnGamL)
$ aRule1
aRule3
= arlElimAlphaRename
$ aRule2
aRule4
= arlElimWild
$ (if optAGCopyElim @lhs.opts then arlElimCopyRule @coNmL @adGam @ad2Gam else id)
$ aRule3
in (RlDecl_AG @nm @pos aRule4,aRule2,aRule3)
%%]
-------------------------------------------------------------------------
-- Debug pretty printing of ruler AST2
-------------------------------------------------------------------------
%%[1 ag
SEM RlDecl
| Rl lhs . ppDbg = "-- debug info"
>-< @nm >#< ppBracketsCommas [pp @pos,pp @agStr]
>-< "introFmGam" >#< ppGam @introFmGam
>-< "introECGam" >#< ppECGam @introECGam
>-< "lhs.rwGam" >#< ppGam @lhs.rwGam
>-< "adGam" >#< ppGam @adGam
>-< "ad2Gam" >#< ppADGam @ad2Gam
>-< "lhs.opts" >#< text (show @lhs.opts)
>-< "coNmL" >#< ppListSep "[" "]" "," @coNmL
>-< "non optim1" >#< pp @selfNonOptim1
>-< "non optim2" >#< pp @selfNonOptim2
%%]
-------------------------------------------------------------------------
-- Error
-------------------------------------------------------------------------
%%[1 ag
SEM Jd
| Ats lhs . errL = @eqnErrs
%%]