never executed always true always false

    1 {-# LANGUAGE QuasiQuotes #-}
    2 
    3 module Conjure.Representations.Set.Explicit ( setExplicit ) where
    4 
    5 -- conjure
    6 import Conjure.Prelude
    7 import Conjure.Language
    8 import Conjure.Representations.Internal
    9 
   10 
   11 setExplicit :: forall m . (MonadFailDoc m, NameGen m) => Representation m
   12 setExplicit = Representation chck downD structuralCons downC up symmetryOrdering
   13 
   14     where
   15         
   16         -- | We can represent any inner domain but set must be fixed size
   17         chck :: TypeOf_ReprCheck m
   18         chck f (DomainSet _ attrs@(SetAttr SizeAttr_Size{}) innerDomain) =
   19             map (DomainSet Set_Explicit attrs) <$> f innerDomain
   20         chck _ _ = return []
   21 
   22         outName :: Domain HasRepresentation x -> Name -> Name
   23         outName = mkOutName Nothing
   24 
   25         -- | A 1D matrix of size of set containing innerDomain objects 
   26         downD :: TypeOf_DownD m
   27         downD (name, domain@(DomainSet Set_Explicit (SetAttr (SizeAttr_Size size)) innerDomain)) = return $ Just
   28             [ ( outName domain name
   29               , DomainMatrix
   30                   (DomainInt TagInt [RangeBounded 1 size])
   31                   innerDomain
   32               ) ]
   33         downD _ = na "{downD} Explicit"
   34 
   35         -- | Enforce lex ordering of matrix (symmetry breaking) and inner structural constraints of
   36         -- 'active' elements of inner domain
   37         structuralCons :: TypeOf_Structural m
   38         structuralCons f downX1 (DomainSet Set_Explicit (SetAttr (SizeAttr_Size size)) innerDomain) = do
   39             let
   40                 -- | Makes sure i'th value is lex less than (i+1)'th value
   41                 -- a symmetry breaking structural constraint
   42                 ordering m = do
   43                     (iPat, i) <- quantifiedVar
   44                     return $ return -- for list
   45                         [essence|
   46                             forAll &iPat : int(1..&size-1) .
   47                                 &m[&i] .< &m[&i+1]
   48                         |]
   49 
   50                 -- | Enforces structural constraints for the elements of the inner domain
   51                 -- that are in the set. 
   52                 innerStructuralCons m = do
   53                     (iPat, i) <- quantifiedVarOverDomain [essenceDomain| int(1..&size) |]
   54                     let activeZone b = [essence| forAll &iPat : int(1..&size) . &b |]
   55 
   56                     -- preparing structural constraints for the inner guys
   57                     innerStructuralConsGen <- f innerDomain
   58 
   59                     let inLoop = [essence| &m[&i] |]
   60                     outs <- innerStructuralConsGen inLoop
   61                     return (map activeZone outs)
   62 
   63             return $ \ ref -> do
   64                 refs <- downX1 ref
   65                 case refs of
   66                     [m] ->
   67                         concat <$> sequence
   68                             [ ordering m
   69                             , innerStructuralCons m
   70                             ]
   71                     _ -> na "{structuralCons} Explicit"
   72         structuralCons _ _ _ = na "{structuralCons} Explicit"
   73 
   74         downC :: TypeOf_DownC m
   75         downC ( name
   76               , domain@(DomainSet Set_Explicit (SetAttr (SizeAttr_Size size)) innerDomain)
   77               , viewConstantSet -> Just constants
   78               ) =
   79             let outIndexDomain = mkDomainIntB 1 size
   80             in  return $ Just
   81                     [ ( outName domain name
   82                       , DomainMatrix outIndexDomain innerDomain
   83                       , ConstantAbstract $ AbsLitMatrix outIndexDomain constants
   84                       ) ]
   85         downC _ = na "{downC} Explicit"
   86 
   87         up :: TypeOf_Up m
   88         up ctxt (name, domain@(DomainSet Set_Explicit (SetAttr (SizeAttr_Size _)) _)) =
   89             case lookup (outName domain name) ctxt of
   90                 Nothing -> failDoc $ vcat $
   91                     [ "(in Set Explicit up)"
   92                     , "No value for:" <+> pretty (outName domain name)
   93                     , "When working on:" <+> pretty name
   94                     , "With domain:" <+> pretty domain
   95                     ] ++
   96                     ("Bindings in context:" : prettyContext ctxt)
   97                 Just constant ->
   98                     case viewConstantMatrix constant of
   99                         Just (_, vals) ->
  100                             return (name, ConstantAbstract (AbsLitSet vals))
  101                         _ -> failDoc $ vcat
  102                                 [ "Expecting a matrix literal for:" <+> pretty (outName domain name)
  103                                 , "But got:" <+> pretty constant
  104                                 , "When working on:" <+> pretty name
  105                                 , "With domain:" <+> pretty domain
  106                                 ]
  107         up _ _ = na "{up} Explicit"
  108 
  109         symmetryOrdering :: TypeOf_SymmetryOrdering m
  110         symmetryOrdering innerSO downX1 inp domain = do
  111             [inner] <- downX1 inp
  112             Just [(_, innerDomain)] <- downD ("SO", domain)
  113             innerSO downX1 inner innerDomain