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 Data.Typeable
import Data.Generics (Data)
import UHC.Light.Compiler.Opts.Base




{-# LINE 37 "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 53 "src/ehc/CHR/Constraint.chs" #-}
mkReduction :: p -> info -> [p] -> Constraint p info
mkReduction p i ps
  = Reduction p i ps
              varlookupEmpty

{-# LINE 62 "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 71 "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 84 "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 93 "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 102 "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 120 "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 155 "src/ehc/CHR/Constraint.chs" #-}
-- | Map from constraint to something
type ConstraintMp' p info x = Map.Map (Constraint p info) [x]

{-# LINE 160 "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 174 "src/ehc/CHR/Constraint.chs" #-}
-- | Map from constraint to info + trace
type ConstraintToInfoTraceMp p info = ConstraintMp' p info (info,[UnresolvedTrace p info])

{-# LINE 179 "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 193 "src/ehc/CHR/Constraint.chs" #-}
-- | Map from constraint to info
type ConstraintToInfoMap     p info = ConstraintMp' p info info

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

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

{-# LINE 231 "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 243 "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