never executed always true always false
    1 {-# LANGUAGE TupleSections #-}
    2 {-# LANGUAGE QuasiQuotes #-}
    3 
    4 module Conjure.Language.NameResolution
    5     ( resolveNames
    6     , resolveNamesMulti
    7     , resolveNamesX
    8     , resolveX, resolveD -- actually internal, use with care
    9     ) where
   10 
   11 import Conjure.Prelude
   12 import Conjure.Bug
   13 import Conjure.UserError
   14 import Conjure.Language.Definition
   15 import Conjure.Language.Domain
   16     ( changeRepr,
   17       typeOfDomain,
   18       Domain(DomainUnnamed, DomainReference, DomainRecord,
   19              DomainVariant) )
   20 import Conjure.Language.Constant
   21 import Conjure.Language.Type
   22 import Conjure.Language.Pretty
   23 import Conjure.Language.TH
   24 
   25 
   26 resolveNamesMulti ::
   27     MonadLog m =>
   28     MonadUserError m =>
   29     NameGen m =>
   30     (?typeCheckerMode :: TypeCheckerMode) =>
   31     [Model] -> m [Model]
   32 resolveNamesMulti = flip evalStateT [] . go
   33     where
   34         go [] = return []
   35         go (m:ms) = (:) <$> resolveNames_ m <*> go ms
   36 
   37 resolveNames ::
   38     MonadLog m =>
   39     MonadUserError m =>
   40     NameGen m =>
   41     (?typeCheckerMode :: TypeCheckerMode) =>
   42     Model -> m Model
   43 resolveNames = flip evalStateT [] . resolveNames_
   44 
   45 resolveNames_ ::
   46     MonadLog m =>
   47     MonadState [(Name, ReferenceTo)] m =>
   48     MonadUserError m =>
   49     NameGen m =>
   50     (?typeCheckerMode :: TypeCheckerMode) =>
   51     Model -> m Model
   52 resolveNames_ model = failToUserError $ do
   53     statements <- mapM resolveStatement (mStatements model)
   54     mapM_ check (universeBi statements)
   55     return model { mStatements = toTaggedInt statements }
   56 
   57 -- this is for when a name will shadow an already existing name that is outside of this expression
   58 -- we rename the new names to avoid name shadowing
   59 shadowing ::
   60     MonadFailDoc m =>
   61     MonadState [(Name, ReferenceTo)] m =>
   62     NameGen m =>
   63     Expression -> m Expression
   64 shadowing p@(Comprehension _ is) = do
   65     -- list of names originating from this comprehension
   66     let generators = concat
   67             [ names
   68             | Generator gen <- is
   69             , let pat = generatorPat gen
   70             , let names = [ n | n@Name{} <- universeBi pat ]
   71             ]
   72     ctxt <- gets id
   73     -- a subset of names originating from this comprehension that will shadow already existing names
   74     let shadows = [ g | g <- generators, g `elem` map fst ctxt ]
   75     shadowsNew <- forM shadows $ \ s -> do n <- nextName "shadow" ; return (s,n)
   76     let f n = fromMaybe n (lookup n shadowsNew)
   77     return (transformBi f p)
   78 shadowing p = return p
   79 
   80 
   81 addName ::
   82     MonadState [(Name, ReferenceTo)] m =>
   83     MonadUserError m =>
   84     Name -> ReferenceTo -> m ()
   85 addName n thing = do
   86     ctxt <- gets id
   87     let
   88         allowed (DeclNoRepr _ _ _ _) (Alias _) = True -- needed when instantiating stuff
   89         allowed (DeclHasRepr _ _ _) (Alias _) = True -- needed when instantiating stuff
   90         allowed old new = old == new
   91     let mdefined = [ thing' | (n', thing') <- ctxt, n == n' && not (allowed thing' thing) ]
   92     case mdefined of
   93         [] -> return ()
   94         (thing':_) -> userErr1 $ vcat [ "Redefinition of name:" <+> pretty n
   95                                       , "When trying to define it as" <+> pretty thing
   96                                       , "It was already defined as" <+> pretty thing'
   97                                       ]
   98     modify ((n, thing) :)
   99 
  100 
  101 resolveNamesX ::
  102     MonadFailDoc m =>
  103     MonadUserError m =>
  104     NameGen m =>
  105     (?typeCheckerMode :: TypeCheckerMode) =>
  106     Expression -> m Expression
  107 resolveNamesX x = do
  108     x' <- evalStateT (resolveX x) []
  109     mapM_ check (universe x')
  110     return x'
  111 
  112 
  113 toTaggedInt :: Data a => a -> a
  114 toTaggedInt = transformBi f
  115     where
  116         f :: Type -> Type
  117         f (TypeEnum (Name nm)) = TypeInt (TagEnum nm)
  118         f ty = ty
  119 
  120 
  121 check :: MonadFailDoc m => Expression -> m ()
  122 check (Reference nm Nothing) = failDoc ("Undefined:" <+> pretty nm)
  123 check _ = return ()
  124 
  125 
  126 resolveStatement ::
  127     MonadFailDoc m =>
  128     MonadState [(Name, ReferenceTo)] m =>
  129     MonadUserError m =>
  130     NameGen m =>
  131     (?typeCheckerMode :: TypeCheckerMode) =>
  132     Statement -> m Statement
  133 resolveStatement st =
  134     case st of
  135         Declaration decl ->
  136             case decl of
  137                 FindOrGiven forg nm dom       -> do
  138                     dom' <- resolveD dom
  139                     addName nm $ DeclNoRepr forg nm dom' NoRegion
  140                     return (Declaration (FindOrGiven forg nm dom'))
  141                 Letting nm x                  -> do
  142                     x' <- resolveX x
  143                     addName nm $ Alias x'
  144                     return (Declaration (Letting nm x'))
  145                 LettingDomainDefnUnnamed nm x -> do
  146                     x' <- resolveX x
  147                     addName nm $ Alias (Domain (DomainUnnamed nm x'))
  148                     return (Declaration (LettingDomainDefnUnnamed nm x'))
  149                 LettingDomainDefnEnum (Name ename) nms -> do
  150                     sequence_ [ addName nm $ Alias (Constant (ConstantInt (TagEnum ename) i))
  151                               | (nm, i) <- zip nms [1..]
  152                               ]
  153                     return st
  154                 LettingDomainDefnEnum{} -> bug "resolveStatement, Name"
  155                 GivenDomainDefnEnum{}       -> return st             -- ignoring
  156         SearchOrder xs -> SearchOrder <$> mapM resolveSearchOrder xs
  157         SearchHeuristic nm -> do
  158             let allowed = ["static", "sdf", "conflict", "srf", "ldf", "wdeg", "domoverwdeg"]
  159             if nm `elem` allowed
  160                 then return (SearchHeuristic nm)
  161                 else userErr1 $ vcat [ "Invalid heuristic:" <+> pretty nm
  162                                      , "Allowed values are:" <+> prettyList id "," allowed
  163                                      ]
  164         Where xs -> Where <$> mapM resolveX xs
  165         Objective obj x -> Objective obj <$> resolveX x
  166         SuchThat xs -> SuchThat <$> mapM resolveX xs
  167 
  168 
  169 resolveSearchOrder ::
  170     MonadFailDoc m =>
  171     MonadState [(Name, ReferenceTo)] m =>
  172     MonadUserError m =>
  173     NameGen m =>
  174     (?typeCheckerMode :: TypeCheckerMode) =>
  175     SearchOrder -> m SearchOrder
  176 resolveSearchOrder (BranchingOn nm) = do
  177     ctxt <- gets id
  178     mval <- gets (lookup nm)
  179     case mval of
  180         Nothing -> userErr1 $ vcat $ ("Undefined reference:" <+> pretty nm)
  181                                    : ("Bindings in context:" : prettyContext ctxt)
  182         Just{}  -> return (BranchingOn nm)
  183 resolveSearchOrder (Cut x) =
  184     let f Find = CutFind
  185         f forg = forg
  186     in  Cut . transformBi f <$> resolveX x
  187 
  188 
  189 resolveX ::
  190     MonadFailDoc m =>
  191     MonadState [(Name, ReferenceTo)] m =>
  192     MonadUserError m =>
  193     NameGen m =>
  194     (?typeCheckerMode :: TypeCheckerMode) =>
  195     Expression -> m Expression
  196 resolveX (Reference nm Nothing) = do
  197     ctxt <- gets id
  198     mval <- gets (lookup nm)
  199     case mval of
  200         Nothing -> userErr1 $ vcat $ ("Undefined reference:" <+> pretty nm)
  201                                    : ("Bindings in context:" : prettyContext ctxt)
  202         Just r  -> return (Reference nm (Just r))
  203 
  204 resolveX p@(Reference nm (Just refto)) = do             -- this is for re-resolving
  205     mval <- gets (lookup nm)
  206     case mval of
  207         Nothing -> return p                             -- hence, do not failDoc if not in the context
  208         Just DeclNoRepr{}                               -- if the newly found guy doesn't have a repr
  209             | DeclHasRepr{} <- refto                    -- but the old one did, do not update
  210             -> return p
  211         Just (DeclNoRepr forg_ nm_ dom_ _)              -- if the newly found guy doesn't have a repr
  212             | DeclNoRepr _ _ _ region <- refto          -- and the old one didn't have one either
  213                                                         -- preserve the region information
  214             -> return (Reference nm (Just (DeclNoRepr forg_ nm_ dom_ region)))
  215         Just (Alias r) -> do
  216             r' <- resolveX r
  217             return (Reference nm (Just (Alias r')))
  218         Just r ->
  219             return (Reference nm (Just r))
  220 
  221 resolveX (AbstractLiteral lit) = AbstractLiteral <$> resolveAbsLit lit
  222 
  223 resolveX (Domain x) = Domain <$> resolveD x
  224 
  225 resolveX p@Comprehension{} = scope $ do
  226     p' <- shadowing p
  227     case p' of
  228         Comprehension x is -> do
  229             is' <- forM is $ \ i -> case i of
  230                 Generator gen -> do
  231                     (gen', refto) <- case gen of
  232                         GenDomainNoRepr pat dom -> do
  233                             dom' <- resolveD dom
  234                             let gen'' = GenDomainNoRepr pat dom'
  235                             return
  236                                 ( gen''
  237                                 , case pat of
  238                                     Single nm' -> DeclNoRepr Quantified nm' dom' NoRegion
  239                                     _ -> InComprehension gen''
  240                                 )
  241                         GenDomainHasRepr nm dom -> do
  242                             dom' <- resolveD dom
  243                             return
  244                                 ( GenDomainHasRepr nm dom'
  245                                 , DeclHasRepr Quantified nm dom'
  246                                 )
  247                         GenInExpr pat expr -> do
  248                             expr' <- resolveX expr
  249                             let gen'' = GenInExpr pat expr'
  250                             return ( gen'' , InComprehension gen'' )
  251                     forM_ (universeBi (generatorPat gen)) $ \ nm ->
  252                         addName nm refto
  253                     return (Generator gen')
  254                 Condition y -> Condition <$> resolveX y
  255                 ComprehensionLetting pat expr -> do
  256                     expr' <- resolveX expr
  257                     resolveAbsPat p pat expr'
  258                     return (ComprehensionLetting pat expr')
  259             x' <- resolveX x
  260             return (Comprehension x' is')
  261         _ -> bug "NameResolution.resolveX.shadowing"
  262 
  263 resolveX (WithLocals body (AuxiliaryVars locals)) = scope $ do
  264     locals' <- mapM resolveStatement locals
  265     body'   <- resolveX body
  266     return (WithLocals body' (AuxiliaryVars locals'))
  267 
  268 resolveX (WithLocals body (DefinednessConstraints locals)) = scope $ do
  269     locals' <- mapM resolveX locals
  270     body'   <- resolveX body
  271     return (WithLocals body' (DefinednessConstraints locals'))
  272 
  273 resolveX x = descendM resolveX x
  274 
  275 
  276 resolveD ::
  277     MonadFailDoc m =>
  278     MonadState [(Name, ReferenceTo)] m =>
  279     MonadUserError m =>
  280     NameGen m =>
  281     Data r =>
  282     Default r =>
  283     Pretty r =>
  284     (?typeCheckerMode :: TypeCheckerMode) =>
  285     Domain r Expression -> m (Domain r Expression)
  286 resolveD (DomainReference nm (Just d)) = DomainReference nm . Just <$> resolveD d
  287 resolveD (DomainReference nm Nothing) = do
  288     mval <- gets (lookup nm)
  289     case mval of
  290         Nothing -> userErr1 ("Undefined reference to a domain:" <+> pretty nm)
  291         Just (Alias (Domain r)) -> DomainReference nm . Just <$> resolveD (changeRepr def r)
  292         Just x -> userErr1 ("Expected a domain, but got an expression:" <+> pretty x)
  293 resolveD (DomainRecord ds) = fmap DomainRecord $ forM ds $ \ (n, d) -> do
  294     d' <- resolveD d
  295     t  <- typeOfDomain d'
  296     addName n $ RecordField n t
  297     return (n, d')
  298 resolveD (DomainVariant ds) = fmap DomainVariant $ forM ds $ \ (n, d) -> do
  299     d' <- resolveD d
  300     t  <- typeOfDomain d'
  301     addName n $ VariantField n t
  302     return (n, d')
  303 resolveD d = do
  304     d' <- descendM resolveD d
  305     mapM resolveX d'
  306 
  307 
  308 resolveAbsPat ::
  309     MonadState [(Name, ReferenceTo)] m =>
  310     MonadUserError m =>
  311     Expression -> AbstractPattern -> Expression -> m ()
  312 resolveAbsPat _ AbstractPatternMetaVar{} _ = bug "resolveAbsPat AbstractPatternMetaVar"
  313 resolveAbsPat _ (Single nm) x = addName nm $ Alias x
  314 resolveAbsPat context (AbsPatTuple ps) x =
  315     sequence_ [ resolveAbsPat context p [essence| &x[&i] |]
  316               | (p, i_) <- zip ps allNats
  317               , let i   = fromInt i_ 
  318               ]
  319 resolveAbsPat context (AbsPatMatrix ps) x =
  320     sequence_ [ resolveAbsPat context p [essence| &x[&i] |]
  321               | (p, i_) <- zip ps allNats
  322               , let i  = fromInt i_
  323               ]
  324 resolveAbsPat context (AbsPatSet ps) x = do
  325     ys <- case x of
  326         Constant (viewConstantSet -> Just xs) -> return (map Constant xs)
  327         AbstractLiteral (AbsLitSet xs) -> return xs
  328         _ -> userErr1 $ "Abstract set pattern cannot be used in this context:" <++> pretty context
  329     sequence_ [ resolveAbsPat context p y
  330               | (p,y) <- zip ps ys
  331               ]
  332 
  333 
  334 resolveAbsLit ::
  335     MonadFailDoc m =>
  336     MonadState [(Name, ReferenceTo)] m =>
  337     MonadUserError m =>
  338     NameGen m =>
  339     (?typeCheckerMode :: TypeCheckerMode) =>
  340     AbstractLiteral Expression -> m (AbstractLiteral Expression)
  341 resolveAbsLit (AbsLitVariant Nothing n x) = do
  342     x'   <- resolveX x
  343     mval <- gets id
  344     let
  345         isTheVariant (Alias (Domain d@(DomainVariant nms))) | Just{} <- lookup n nms = Just d
  346         isTheVariant _ = Nothing
  347     case mapMaybe (isTheVariant . snd) mval of
  348         (DomainVariant dom:_) -> return (AbsLitVariant (Just dom) n x')
  349         _ -> return (AbsLitVariant Nothing n x')
  350 resolveAbsLit lit = (descendBiM resolveX >=> descendBiM resolveD') lit
  351     where
  352         resolveD' d = resolveD (d :: Domain () Expression)