Constraint.hs

{-# LANGUAGE CPP #-}

module UHC.Light.Compiler.CHR.Constraint
( Constraint (..)
, mkReduction
, cnstrReducablePart
, UnresolvedTrace (..)
, cnstrMpSingletonL, cnstrMpFromList
, ConstraintToInfoTraceMp
, cnstrTraceMpSingleton, cnstrTraceMpLiftTrace, cnstrTraceMpElimTrace, cnstrTraceMpFromList
, ConstraintToInfoMap
, emptyCnstrMp
, cnstrMpUnion, cnstrMpUnions
, cnstrRequiresSolve )
where
import UHC.Light.Compiler.Base.Common
import UHC.Light.Compiler.Ty
import UHC.Light.Compiler.CHR
import UHC.Light.Compiler.CHR.Key
import UHC.Light.Compiler.Base.TreeTrie
import UHC.Light.Compiler.Substitutable
import UHC.Util.Pretty as PP
import UHC.Util.Utils
import qualified Data.Set as Set
import qualified Data.Map as Map
import UHC.Light.Compiler.VarMp
import Control.Monad
import UHC.Util.Binary
import UHC.Util.Serialize
import UHC.Light.Compiler.Opts.Base




{-# LINE 35 "src/ehc/CHR/Constraint.chs" #-}
-- | A Constraint is abstracted over the exact predicate, but differentiates on the role: to prove, can be assumed, and side effect of reduction
data Constraint p info
  = Prove           { cnstrPred :: !p }             -- proof obligation
  | Assume          { cnstrPred :: !p }             -- assumed constraint
  | Reduction                                       -- 'side effect', residual info used by (e.g.) codegeneration
                    { cnstrPred :: !p               -- the pred to which reduction was done
                    , cnstrInfo :: !info            -- additional reduction specific info w.r.t. codegeneration
                    , cnstrFromPreds :: ![p]        -- the preds from which reduction was done
                    , cnstrVarMp :: VarMp           -- additional bindings for type (etc.) variables, i.e. improving substitution
                    }
  deriving (Eq, Ord, Show)

{-# LINE 51 "src/ehc/CHR/Constraint.chs" #-}
mkReduction :: p -> info -> [p] -> Constraint p info
mkReduction p i ps
  = Reduction p i ps
              varlookupEmpty

{-# LINE 60 "src/ehc/CHR/Constraint.chs" #-}
#if __GLASGOW_HASKELL__ >= 708
deriving instance Typeable  Constraint
#else
deriving instance Typeable2 Constraint
#endif
deriving instance (Data x, Data y) => Data (Constraint x y)

{-# LINE 69 "src/ehc/CHR/Constraint.chs" #-}
-- | Dissection of Constraint, including reconstruction function
cnstrReducablePart :: Constraint p info -> Maybe (String,p,p->Constraint p info)
cnstrReducablePart (Prove  p) = Just ("Prf",p,Prove)
cnstrReducablePart (Assume p) = Just ("Ass",p,Assume)
cnstrReducablePart _          = Nothing

{-# LINE 82 "src/ehc/CHR/Constraint.chs" #-}
instance (CHRMatchable env p s) => CHRMatchable env (Constraint p info) s where
  chrMatchTo env s c1 c2
    = do { (_,p1,_) <- cnstrReducablePart c1
         ; (_,p2,_) <- cnstrReducablePart c2
         ; chrMatchTo env s p1 p2
         }

{-# LINE 91 "src/ehc/CHR/Constraint.chs" #-}
instance TTKeyable p => TTKeyable (Constraint p info) where
  toTTKey' o c -- = maybe [] (\(s,p,_) -> ttkAdd (TT1K_One $ Key_Str s) [toTTKey' o p]) $ cnstrReducablePart c
    = case cnstrReducablePart c of
        Just (s,p,_) -> ttkAdd' (TT1K_One $ Key_Str s) cs
                     where (_,cs) = toTTKeyParentChildren' o p
        _            -> panic "TTKeyable (Constraint p info).toTTKey'" -- ttkEmpty

{-# LINE 100 "src/ehc/CHR/Constraint.chs" #-}
instance (VarExtractable p v,VarExtractable info v) => VarExtractable (Constraint p info) v where
  varFreeSet c
    = case cnstrReducablePart c of
        Just (_,p,_) -> varFreeSet p
        _            -> Set.empty

instance (VarUpdatable p s,VarUpdatable info s) => VarUpdatable (Constraint p info) s where
  varUpd s      (Prove     p       ) = Prove      (varUpd s p)
  varUpd s      (Assume    p       ) = Assume     (varUpd s p)
  varUpd s      r@(Reduction {cnstrPred=p, cnstrInfo=i, cnstrFromPreds=ps})
                                     = r {cnstrPred=varUpd s p, cnstrInfo=varUpd s i, cnstrFromPreds=map (varUpd s) ps}

{-# LINE 118 "src/ehc/CHR/Constraint.chs" #-}
-- | The trace of an unresolved predicate
data UnresolvedTrace p info
  = UnresolvedTrace_None									-- no trace required when all is resolved
  | UnresolvedTrace_Red										-- ok reduction, with failure deeper down
      { utraceRedFrom		:: p
      , utraceInfoTo2From	:: info
      , utraceRedTo			:: [UnresolvedTrace p info]
      }
  | UnresolvedTrace_Fail									-- failed reduction
      { utraceRedFrom		:: p
      -- , utraceInfoTo2From	:: info
      , utraceRedTo			:: [UnresolvedTrace p info]
      }
  | UnresolvedTrace_Overlap									-- choice could not be made
      { utraceRedFrom		:: p
      , utraceRedChoices	:: [(info,[UnresolvedTrace p info])]
      }
  deriving Show

instance Eq p => Eq (UnresolvedTrace p info) where
  t1 == t2 = True -- utraceRedFrom t1 == utraceRedFrom t2

instance (PP p, PP info) => PP (UnresolvedTrace p info) where
  pp x = case x of
  		   UnresolvedTrace_None 			-> PP.empty
  		   UnresolvedTrace_Red 		p i us 	-> p >|< ":" >#< i >-< indent 2 (vlist $ map pp us)
  		   UnresolvedTrace_Fail 	p   us  -> p >|< ": FAIL" >-< indent 2 (vlist $ map pp us)
  		   UnresolvedTrace_Overlap 	p uss 	-> p >|< ": OVERLAP" >-< indent 2 (vlist $ map (\(i,u) -> i >-< indent 2 (vlist $ map pp u)) uss)

{-# LINE 153 "src/ehc/CHR/Constraint.chs" #-}
-- | Map from constraint to something
type ConstraintMp' p info x = Map.Map (Constraint p info) [x]

{-# LINE 158 "src/ehc/CHR/Constraint.chs" #-}
cnstrMpSingletonL :: Constraint p i -> [x] -> ConstraintMp' p i x
cnstrMpSingletonL c xs = Map.singleton c xs

cnstrMpSingleton :: Constraint p i -> x -> ConstraintMp' p i x
cnstrMpSingleton c x = cnstrMpSingletonL c [x]

cnstrMpFromList :: (Ord p, Ord i) => [(Constraint p i,x)] -> ConstraintMp' p i x
cnstrMpFromList l = Map.fromListWith (++) [ (c,[x]) | (c,x) <- l ]

cnstrMpMap :: (Ord p, Ord i) => (x -> y) -> ConstraintMp' p i x -> ConstraintMp' p i y
cnstrMpMap f = Map.map (map f)

{-# LINE 172 "src/ehc/CHR/Constraint.chs" #-}
-- | Map from constraint to info + trace
type ConstraintToInfoTraceMp p info = ConstraintMp' p info (info,[UnresolvedTrace p info])

{-# LINE 177 "src/ehc/CHR/Constraint.chs" #-}
cnstrTraceMpFromList :: (Ord p, Ord i) => [(Constraint p i,(i,[UnresolvedTrace p i]))] -> ConstraintToInfoTraceMp p i
cnstrTraceMpFromList = cnstrMpFromList

cnstrTraceMpSingleton :: Constraint p i -> i -> [UnresolvedTrace p i] -> ConstraintToInfoTraceMp p i
cnstrTraceMpSingleton c i ts = cnstrMpSingleton c (i,ts)

cnstrTraceMpElimTrace :: (Ord p, Ord i) => ConstraintToInfoTraceMp p i -> ConstraintToInfoMap p i
cnstrTraceMpElimTrace = cnstrMpMap fst

cnstrTraceMpLiftTrace :: (Ord p, Ord i) => ConstraintToInfoMap p i -> ConstraintToInfoTraceMp p i
cnstrTraceMpLiftTrace = cnstrMpMap (\x -> (x,[]))

{-# LINE 191 "src/ehc/CHR/Constraint.chs" #-}
-- | Map from constraint to info
type ConstraintToInfoMap     p info = ConstraintMp' p info info

{-# LINE 196 "src/ehc/CHR/Constraint.chs" #-}
emptyCnstrMp :: ConstraintMp' p info x
emptyCnstrMp = Map.empty

{-# LINE 206 "src/ehc/CHR/Constraint.chs" #-}
cnstrMpUnion :: (Ord p, Ord i) => ConstraintMp' p i x -> ConstraintMp' p i x -> ConstraintMp' p i x
cnstrMpUnion = Map.unionWith (++)

cnstrMpUnions :: (Ord p, Ord i) => [ConstraintMp' p i x] -> ConstraintMp' p i x
cnstrMpUnions = Map.unionsWith (++)

{-# LINE 218 "src/ehc/CHR/Constraint.chs" #-}
-- | Predicate for whether solving is required
cnstrRequiresSolve :: Constraint p info -> Bool
cnstrRequiresSolve (Reduction {}) = False
cnstrRequiresSolve _              = True

{-# LINE 229 "src/ehc/CHR/Constraint.chs" #-}
instance (PP p, PP info) => PP (Constraint p info) where
  pp (Prove     p     ) = "Prove"  >#< p
  pp (Assume    p     ) = "Assume" >#< p
  pp (Reduction {cnstrPred=p, cnstrInfo=i, cnstrFromPreds=ps})
                        = "Red"    >#< p >#< "<" >#< i >#< "<" >#< ppBracketsCommas ps

{-# LINE 241 "src/ehc/CHR/Constraint.chs" #-}
instance (Serialize p, Serialize i) => Serialize (Constraint p i) where
  sput (Prove     a      ) = sputWord8 0 >> sput a
  sput (Assume    a      ) = sputWord8 1 >> sput a
  sput (Reduction a b c d) = sputWord8 2 >> sput a >> sput b >> sput c >> sput d
  sget = do t <- sgetWord8
            case t of
              0 -> liftM  Prove     sget
              1 -> liftM  Assume    sget
              2 -> liftM4 Reduction sget sget sget sget