Generics.cag

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Generics
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Additional datatypes, class instances introduced
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%[doesWhat doclatex
For each datatype:

\begin{verbatim}
data T = C1 .. | Cn ..
\end{verbatim}

additional datatypes and class instances are introduced.
%%]

%%[(92 hmtyinfer) hs
-- | The info for generics about datatypes, required higher in the syntax tree
type GenerDataInfo
  = (  ( HsName         -- orig type name
       , [TyVarId]      -- data type args
       , Ty             -- kind of type, without kiVarMap yet applied
       )
    , [( CTag           -- orig con tag
       , FldTyL         -- field types, with possible label
      )]
    , PredScope
    , Int               -- max kind arity over which genericity abstracts, currently \in {0,1}
    )

type GenerDataInfoMp = Map.Map HsName GenerDataInfo

-- | what kind of instance should be generated
data GenerInstKind
  = GenerInstKind_Datatype
  | GenerInstKind_Selector
  | GenerInstKind_Constructor       HsName      -- for a type
  | GenerInstKind_Representable     Int         -- remaining arity
                                    Proj        -- projection info
  deriving (Show)

-- | Info for generics, for generating data instances
type GenerDataInstInfo
  = ( HsName            -- original name of type, data
    , HsName            -- instance name
    , HsName            -- class name
    , GenerInstKind     -- what kind of instance
    , Pred              -- the predicate
    )

-- | Info for generics, for generating repr instances, in particular projection descriptors
type GenerTySynProjInfo
  = ( HsName                -- original name of datatype
    , [TyVarId]             -- data type args
    , PredScope             -- predicate scope
    , [( HsName             -- representation type name
       , Ty                 -- type synonym itself, i.e. the type lambda
       , Proj               -- projection descriptor
       , Int                -- the arity of remaining type args
      )]
    )
%%]

%%[(92 hmtyinfer) hs
mkGenerThing
  ::    thing
     -> (thing -> thing)
     -> (thing -> thing -> thing)
     -> [thing]
     -> thing
mkGenerThing zero one two things
  = mkSub things
  where mkSub [ ] = zero
        mkSub [s] = one s
        mkSub ss  = two (mkSub ss1) (mkSub ss2)
                  where (ss1,ss2) = splitAt (length ss `div` 2) ss
%%]

%%[(92 hmtyinfer) hs
mkGenerRepresentableTypeSynTyProj
  :: EHCOpts
     -> Int                     -- the arity of to be supplied type paramaters
     -> [HsName]                -- all type names defined in this binding group (i.e. let)
     -> (HsName -> Int-> Bool)  -- name of type has Representable<remArity>?
     -> HsName                  -- type name
     -> [TyVarId]               -- type args
     -- -> ([Ty],Ty)               -- kind, already split up in args + res
     -> [(CTag,HsName,FldTyL)]    -- tags, constructor type names, with type args
     -> ( Ty                    -- type
        , Proj                  -- intermediate description of projection
        )
mkGenerRepresentableTypeSynTyProj
     opts remArity allTyNmL isRepresentable
     tyNm tvarArgL
     -- (kiArgL,kiRes)
     conNmArgsL
  = mkTop $ mkSm [ mkAlt tg c (mkPr [ mkLblArg p | p <- ps ]) | (tg,c,ps) <- conNmArgsL ]
  where lamArity      = length tvarArgL - remArity
        (lamTvarArgL,remTvarArgL)
                      = splitAt lamArity tvarArgL
        mkC   f       = appCon $ ehcOptBuiltin  opts f
        mkC2  f i     = appCon $ ehcOptBuiltin2 opts f i
        mkSub (u,pu) (f,pf)
                      = mkGenerThing (mkC u,pu) id (\(x,px) (y,py) -> (appTopApp [mkC f, x, y], pf px py))
        mkPr          = mkSub (ehbnGenerDataUnit1, Proj_U1   ) (ehbnGenerDataProd, Proj_Prod                             )
        mkSm          = mkSub (ehbnGenerDataVoid1, Proj_Void ) (ehbnGenerDataSum , \x y -> Proj_L1 x `Proj_Sum` Proj_R1 y)
        mkLblArg (mbLbl,t)
                      = ( appTopApp [ mkC ehbnGenerDataMetaS1, sel, t' ], Proj_M1_S1 p )
                      where (t',p) = mkArg t
                            sel    = maybe (mkC ehbnGenerDataNoSelector) (appCon) mbLbl
        mkArg t       = (appTopApp funarg, proj)
                      where (funarg,proj)
                              | isJust mbVar     = case elemIndex tvar remTvarArgL of       -- TBD: check for kind *, check for one of tvarArgL
                                                     Just i -> ([ mkC ehbnGenerDataPar1    ], Proj_Par1 [t] (i+1))
                                                     _      -> ([ mkC ehbnGenerDataPar0, t ], Proj_K1   [t]      )
                              | remArity > 0 && {- isJust mbCon && -} length args > 0 && isRepr
                                                 = case (initlast remTvarArgL, initlast args) of
                                                     (Just (_,tv), Just (firstargs,lastarg)) | maybe False (tv==) $ tyMbVar lastarg
                                                       -> ([ mkC ehbnGenerDataRec1, appTopApp (fun : firstargs) ], Proj_Rec1 [t] remArity)
                                                     (_, Just (firstargs,lastarg)) | not $ Set.null $ varFreeSet lastarg
                                                       -> ( [ mkC ehbnGenerDataComp1, fmapTy, lastarg' ]
                                                          , Proj_Comp1 [t] fmapTy lastproj
                                                          )
                                                       where (lastarg',lastproj) = mkArg lastarg
                                                             fmapTy = appTopApp (fun : firstargs)
                                                     _ -> dflt
                              | otherwise        = dflt
                              where mbVar@(~(Just tvar      )) = tyMbVar        t
                                    funArgs@(     (fun,args) ) = appUnApp       t
                                    isRepr = maybe (isJust $ tyMbVar fun) (\con -> isRepresentable con remArity) $ tyMbCon fun
                                    dflt   = ([ mkC ehbnGenerDataRec0, t ], Proj_K1 [t])
        mkAlt tg c (t,p)  = (appTopApp [mkC2 ehbnGenerDataMetaCN 1, appCon c, t], Proj_M1 $ Proj_Con tg p)
        mkTop (t,p)   = ( mkTyLam lamTvarArgL (appTopApp [ mkC2 ehbnGenerDataMetaDN 1, appCon tyNm, t ])
                        , Proj $ Proj_M1 p
                        )
        -- eqLastTvar    = maybe (const False) (\(_,v) -> maybe False (v==) . tyMbVar) $ initlast tvarArgL
        -- isRec t       = not (null as) || tyConNm f `elem` allTyNmL
        --               where (f,as) = appUnApp t

mkGenerRepresentableTypeSynonymKi :: TyKiGam -> HsName -> Ty
mkGenerRepresentableTypeSynonymKi tyKiGam tyNm
  = maybe (appDbg $ "Generics.mkGenerRepresentableTypeSynonymKi: " ++ show tyNm) (addStar . tkgiKi) $ tyKiGamLookupByName tyNm tyKiGam
  where addStar ki = appArr (as ++ [kiStar]) r
                   where (as,r) = appUnArr ki

-- TBD: sort out additional pol param at end, just like for kinds
mkGenerRepresentableTypeSynonymPol :: PolGam -> HsName -> Ty
mkGenerRepresentableTypeSynonymPol polGam tyNm = maybe (appDbg $ "Generics.mkGenerRepresentableTypeSynonymPol: " ++ show tyNm) pgiPol $ polGamLookup tyNm polGam
%%]

%%[(92 hmtyinfer)
-- 20150924 AD
-- Generic info is threaded to the location where it actually is going to be used (i.e. stuff generated). This is dictated by placeholders 'GenerRep' for inserting the derived stuff.
ATTR AllDecl [ | | generDataInfoL USE {++} {[]} : {[GenerDataInfo]} ]
ATTR AllDecl AllExpr AllPatExpr AllCase [ | generDataInfoMp: GenerDataInfoMp | ]

SEM AGItf
  | AGItf		expr		.	generDataInfoMp		=	Map.empty

SEM Decl
  | Data        loc         -- all gathered info, required higher up in the AST to generate type and instance defs
                            .   (generDataInfoL, generDataInfoMpNew)
                                                    =   if isJust @mbGenerInfo -- ehcOptGenGenerics @lhs.opts
                                                        then let i = ( (@tyNm, @dataTyVarIdL, @dataKi)
                                                                     , [ ( dtiCTag dti, dtiFldTyL dti )
                                                                       | (c,cty) <- snd $ tyRecExts @dataAltTy
                                                                       , let dti = panicJust "Generics.Decl.Data.dataConstrTagMp" $ Map.lookup c @constrs.dataConstrTagMp
                                                                       ]
                                                                     , @lhs.predScope
                                                                     , fromJust @mbGenerInfo
                                                                     )
                                                             in  if ehcOptIsUnderDev UnderDev_NameAnalysis @lhs.opts
                                                                 then ([] , Map.singleton @tyNm i)
                                                                 else ([i], Map.empty            )
                                                        else ([], Map.empty)
                lhs         .   generDataInfoMp     =   @generDataInfoMpNew `Map.union` @lhs.generDataInfoMp
  | GenerRep    loc         .   (generDataInfoL, errsNoIntroNm)
                                                    =   case Map.lookup @tyNm @lhs.generDataInfoMp of
                                                            Just i  | @arity == @maxArity                              -> ([i], [])
                                                            Nothing | ehcOptIsUnderDev UnderDev_NameAnalysis @lhs.opts -> ([], [rngLift @range mkErr_NamesNotIntrod "datatype" [@tyNm]])
                                                            _                                                          -> ([], [])
  																						

SEM Expr
  | Let         loc         -- names for introduced datatypes
                            .   (generDataAllTyOrigNmL,generDataTyAndConNmLL)
                                                    =   unzip [ ( origtnm
                                                                , hsnNm2GenerDatatype origtnm : [ hsnNm2GenerConstructor $ ctagNm x | (x,_) <- cs ]
                                                                )
                                                              | ((origtnm,_,ki),cs,_,_) <- @decls.generDataInfoL
                                                              ]
                            .   generDataTyAndConNmL=   concat @generDataTyAndConNmLL
                            
                            -- representation type synonyms and projection descriptors
                            .   generTySynProjL     =   [ ( origtnm, tvs, sc
                                                          , [ (hsnNm2GenerReprSyn arity origtnm, syn, proj, arity)
                                                            | arity <- [0..remArity]
                                                            , let (syn,proj) = mkGenerRepresentableTypeSynTyProj @lhs.opts arity
                                                                                  @generDataAllTyOrigNmL
                                                                                  (\tnm remArity -> tnm `elem` @generDataAllTyOrigNmL || isJust (tyGamLookup (hsnNm2GenerReprSyn remArity tnm) @lhs.tyGam))
                                                                                  tnm tvs -- ki'
                                                                                  [ (c,hsnNm2GenerConstructor $ ctagNm c,assocLMapKey (fmap hsnNm2GenerSelector) ps) | (c,ps) <- cs ]
                                                            ]
                                                          )
                                                        | ((origtnm,tvs,ki),cs,sc,remArity) <- @decls.generDataInfoL
                                                        , let -- ki' = appUnArr $ @bodyTyKiVarMp1 `varUpd` ki
                                                              tnm = hsnNm2GenerDatatype origtnm
                                                        ]

                            -- various environments/gammas
                            .   generDataGam        =   gamFromAssocL [ (n, mkDGIPlain n (appCon n) kiStar [] Map.empty )
                                                                      | n <- @generDataTyAndConNmL
                                                                      ]
                            .   generTyGam          =   gamFromAssocL [ (n, mkTGIData (appCon n) (appDbg $ "Generics.Expr.Let.TyGam.DataTyAndCon: " ++ show n))
                                                                      | n <- @generDataTyAndConNmL
                                                                      ]
                                                        `gamUnion`
                                                        gamFromAssocL [ ( tnm, mkTGIData syn (appDbg $ "Generics.Expr.Let.TyGam.TySyn: " ++ show tnm))
                                                                      | (_,_,_,ts) <- @generTySynProjL
                                                                      , (tnm,syn,_,_) <- ts
                                                                      ]
                            .   generTyKiGam        =   gamUnions     [ (tyKiGamNameSingleton n (TyKiGamInfo kiStar))
                                                                      | n <- @generDataTyAndConNmL
                                                                      ]
                                                        `gamUnion`
                                                        gamUnions     [ (tyKiGamNameSingleton (hsnNm2GenerReprSyn arity origtnm) (TyKiGamInfo ki))
                                                                      | ((origtnm,_,_),_,_,remArity) <- @decls.generDataInfoL
                                                                      , let ki = mkGenerRepresentableTypeSynonymKi @lQuTyKiGam_ex origtnm
                                                                      , arity <- [0..remArity]
                                                                      ]
                            .   generPolGam         =   gamUnions     [ (gamSingleton (hsnNm2GenerReprSyn arity origtnm)
                                                                                      (PolGamInfo $ mkGenerRepresentableTypeSynonymPol @finGathPolGam origtnm)
                                                                        )
                                                                      | ((origtnm,tvs,_),_,_,remArity) <- @decls.generDataInfoL
                                                                      , arity <- [0..remArity]
                                                                      ]

                            -- instances to participate in context reduction machinery (codegen is done in ToCore)
                            -- TBD: factor out similarities...
                            .   (generInstDeclL,generInstInfoL)
                                                    =   let -- make names
                                                            mkn' cl kind (orignm,nm) = (orignm,nm,cl,hsnUniqifyStr HsNameUniqifier_GenericClass (hsnBaseString cl) nm,kind)
                                                            mkn  f   = mkn' (ehcOptBuiltin  @lhs.opts f  )
                                                            mkn2 f i = mkn' (ehcOptBuiltin2 @lhs.opts f i)
                                                            
                                                            -- make data label instance, i.e. Constructor $C1, Datatype $T
                                                            mkd sc (orignm,nm,cl,i,k)
                                                              = ( ( [], pr, RedHow_ByInstance i pr sc, sc )
                                                                , (orignm,i,cl,k,pr)
                                                                )
                                                              where pr = Pred_Class $ appConApp cl [appCon nm]
                                                            mkDataInst (t@(origtnm,_,_),cs,sc,_)
                                                              = map (mkd sc)
                                                                  $ [mkn ehbnGenerClassDatatype GenerInstKind_Datatype (origtnm, hsnNm2GenerDatatype origtnm)]
                                                                    ++ (map (mkn ehbnGenerClassConstructor $ GenerInstKind_Constructor origtnm)
                                                                            [ (origdnm, hsnNm2GenerConstructor origdnm) | (tg,_) <- cs, let origdnm = ctagNm tg ]
                                                                       )
                                                                    ++ (map (mkn ehbnGenerClassSelector $ GenerInstKind_Selector)
                                                                        $ Map.toList $ Map.fromList
                                                                          [ (origsnm, hsnNm2GenerSelector origsnm) | (_,fs) <- cs, (Just origsnm,_) <- fs ]
                                                                       )
                                                            
                                                            -- make representation instance, i.e. Representable0 (T x) (_Rep0T x)
                                                            mkr sc arity (tyNm,tyRepNm,repCl,i,k@(GenerInstKind_Representable remArity _))
                                                              = ( ( [], pr, RedHow_ByInstance i pr sc, sc )
                                                                , (tyNm,i,repCl,k,pr)
                                                                )
                                                              where pr = Pred_Class $ appConApp repCl [appConApp tyNm tvL, appConApp tyRepNm tvL]
                                                                    tvL = map mkTyMetaVar $ mkNewUIDL (arity - remArity) @lUniq_92_prTyMeta
                                                            mkReprInst (origtnm,tvL,sc,syns)
                                                              = map (mkr sc (length tvL))
                                                                  [ mkn2 ehbnGenerClassRepresentableN arity (GenerInstKind_Representable arity proj) (origtnm,tnm)
                                                                  | (tnm,_,proj,arity) <- syns
                                                                  ]
                                                        in  unzip
                                                            $ (concatMap mkReprInst @generTySynProjL)
                                                              ++ (concatMap mkDataInst @decls.generDataInfoL)
                loc         .   lUniq_92_prTyMeta   :   UNIQUEREF gUniq
%%]

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Additional fitsIn, proofing, etc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%[(92 hmtyinfer) hs
type GenerForFitsIn
  = ( HsName            -- field name
    , HsName            -- default value name
    , Ty                -- field type
    , Ty                -- default value type
    )
%%]

%%[(92 hmtyinfer)
SEM Decl
  | Instance    loc         -- the set of fld + default names, their types, to be used ...
                            .   generForFitsInL     =   case @instVariant of
                                                          InstDeriving _ | not @derivCanBeDoneBuiltin && not (null generDerivFlds)
                                                            -> [ ( fldNm, dfltvalNm
                                                                 , -- (\v -> tr "Decl.Instance.mbFSig" (ppTy v >-< ppTy (vgiTy (fromJust mbDSig))) v) $
                                                                   repTy `app1Arr` vgiTy (fromJust mbFSig)
                                                                 , vgiTy (fromJust mbDSig)
                                                                 )
                                                               | ((fldNm,dfltvalNm),u) <- zip generDerivFlds (mkNewLevUIDL (length generDerivFlds) @lUniq_generDeriv1)
                                                               , let mbFSig = valGamLookup fldNm     @tySigGam  , isJust mbFSig
                                                               , let mbDSig = valGamLookup dfltvalNm @lhs.valGam, isJust mbDSig
                                                               , let repTy  = appTopApp (  [appCon repTyNm]
                                                                                        ++ take (dataArity - @derivTruncTailArity) @derivDataTyArgs
                                                                                        ++ [mkTyVar u]
                                                                                        )
                                                               ]
                                                            where generDerivFlds = clgiGenerDerivableL @clgi
                                                                  dataArity = length @derivDataTyArgs
                                                                  repTyNm | dgiIsRec @derivDataDGI = ehcOptBuiltin @lhs.opts ehbnGenerTupleRepresentableN @derivArity dataArity
                                                                          | otherwise              = hsnNm2GenerReprSyn @derivArity @derivDataTyNm
                                                          _ -> []

                            -- for subsumption, to extract predicates to Prove + coercion
                            .   (foGenerDerivL,foGenerDeriv)
                                                    =   let (tfldL,tdfltL) = unzip [ (tfld,tdflt) | (_,_,tfld,tdflt) <- @generForFitsInL ]
                                                        in  fitsInL' strongFIOpts (@fe {fePredScope = @predScope}) @lUniq_generDeriv2 @decls.tyVarMp tdfltL tfldL 

                loc         .   lUniq_generDeriv1   :   UNIQUEREF gUniq
                loc         .   lUniq_generDeriv2   :   UNIQUEREF gUniq
%%]