never executed always true always false

    1 module Conjure.UI.NormaliseQuantified
    2     ( normaliseQuantifiedVariables
    3     , normaliseQuantifiedVariablesE
    4     , normaliseQuantifiedVariablesS
    5     , distinctQuantifiedVars
    6     , renameQuantifiedVarsToAvoidShadowing
    7     ) where
    8 
    9 import Conjure.Prelude
   10 import Conjure.Language
   11 
   12 
   13 normaliseQuantifiedVariables :: Model -> Model
   14 normaliseQuantifiedVariables m@Model{mStatements=st} =
   15     let stOut = map normaliseQuantifiedVariablesS st
   16     in  m { mStatements = stOut }
   17 
   18 normaliseQuantifiedVariablesE :: Expression -> Expression
   19 normaliseQuantifiedVariablesE = normX_Leveled 1
   20 
   21 normaliseQuantifiedVariablesS :: Statement -> Statement
   22 normaliseQuantifiedVariablesS = descendBi normaliseQuantifiedVariablesE
   23 
   24 normX_Leveled :: Int -> Expression -> Expression
   25 normX_Leveled nextInt p@(Comprehension _ gocs) =
   26     let
   27         quantifiedNames = getQuantifiedNames gocs
   28         oldNew =
   29             [ (qn, MachineName "q" i [])
   30             | (qn, i) <- zip quantifiedNames [nextInt..]
   31             ]
   32         nextInt' = nextInt + length oldNew
   33         f :: Name -> Name
   34         f nm = fromMaybe nm (lookup nm oldNew)
   35     in
   36         p |> descend (normX_Leveled nextInt')
   37           |> transformBi f
   38 normX_Leveled nextInt p =
   39         p |> descend (normX_Leveled nextInt)
   40 
   41 
   42 distinctQuantifiedVars :: NameGen m => Model -> m Model
   43 distinctQuantifiedVars m@Model{mStatements=stmts} = do
   44     let
   45         -- usedOnce :: [Name]
   46         -- usedOnce =
   47         --     [ nm
   48         --     | (nm, nb) <- histogram
   49         --                     [ nm
   50         --                     | Comprehension _ gocs <- universeBi stmts
   51         --                     , nm <- getQuantifiedNames gocs
   52         --                     ]
   53         --     , nb == 1
   54         --     ]
   55 
   56         usedInALetting :: [Name]
   57         usedInALetting =
   58             [ nm
   59             | Declaration (Letting _ x) <- stmts
   60             , Comprehension _ gocs <- universe x
   61             , nm <- getQuantifiedNames gocs
   62             ]
   63 
   64         normX_Distinct :: NameGen m => Expression -> m Expression
   65         normX_Distinct p@(Comprehension _ gocs) = do
   66             let quantifiedNames = getQuantifiedNames gocs
   67             oldNew <- sequence
   68                     [ do
   69                         if qn `elem` usedInALetting
   70                             then do
   71                                 new <- nextName "q"
   72                                 return (qn, new)
   73                             else
   74                                 return (qn, qn)
   75                     | qn <- quantifiedNames
   76                     ]
   77             let
   78                 f :: Name -> Name
   79                 f nm = fromMaybe nm (lookup nm oldNew)
   80 
   81             p' <- descendM normX_Distinct p
   82             return (transformBi f p')
   83         normX_Distinct p = descendM normX_Distinct p
   84 
   85     if null usedInALetting
   86         then return m
   87         else do
   88             stmtsOut <- forM stmts $ \ stmt ->
   89                 case stmt of
   90                     Declaration Letting{} -> return stmt
   91                     _                     -> descendBiM normX_Distinct stmt
   92             namegenst <- exportNameGenState
   93             let miInfoOut = (mInfo m) { miNameGenState = namegenst }
   94             return m { mStatements = stmtsOut, mInfo = miInfoOut }
   95 
   96 
   97 renameQuantifiedVarsToAvoidShadowing :: NameGen m => Model -> m Model
   98 renameQuantifiedVarsToAvoidShadowing model = do
   99     let
  100 
  101         allDecls :: [Name]
  102         allDecls = concat [ case d of
  103                                 FindOrGiven _ nm _ -> [nm]
  104                                 Letting nm _ -> [nm]
  105                                 GivenDomainDefnEnum nm -> [nm]
  106                                 LettingDomainDefnEnum nm nms -> nm : nms
  107                                 LettingDomainDefnUnnamed nm _ -> [nm]
  108                           | Declaration d <- mStatements model
  109                           ]
  110 
  111         rename :: NameGen m => Expression -> m Expression
  112         rename p@(Comprehension _ gocs) = do
  113             let quantifiedNames = getQuantifiedNames gocs
  114             oldNew <- concat <$> sequence
  115                     [ do
  116                         if qn `elem` allDecls
  117                             then do
  118                                 new <- nextName "shadow"
  119                                 return [(qn, new)]
  120                             else
  121                                 return []
  122                     | qn <- quantifiedNames
  123                     ]
  124             let
  125                 f :: Name -> Name
  126                 f nm = fromMaybe nm (lookup nm oldNew)
  127 
  128             let p' = transformBi f p
  129             descendM rename p'
  130         rename p = descendM rename p
  131 
  132     stmtsOut <- descendBiM rename (mStatements model)
  133     namegenst <- exportNameGenState
  134     let miInfoOut = (mInfo model) { miNameGenState = namegenst }
  135     return model { mStatements = stmtsOut, mInfo = miInfoOut }
  136 
  137 
  138 getQuantifiedNames :: [GeneratorOrCondition] -> [Name]
  139 getQuantifiedNames gocs = concat
  140     [ case gen of
  141         GenDomainNoRepr  pat _ -> universeBi pat
  142         GenDomainHasRepr nm  _ -> [nm]
  143         GenInExpr        pat _ -> universeBi pat
  144     | Generator gen <- gocs
  145     ]
  146