{-# LANGUAGE CPP #-}

module UHC.Light.Compiler.CHR.CtxtRedOnly.Constraint
( Constraint, Constraint' (..)
, cnstrReducablePart
, CHRIntermediateUntilAssume
, mkProve, mkAssume, mkReduction
, gathPredLToProveCnstrMp, gathPredLToAssumeCnstrMp
, predOccCnstrMpLiftScope
, RedHowAnnotation (..)
, ByScopeRedHow (..)
, UnresolvedTrace' (..), UnresolvedTrace
, cnstrMpFromList
, ConstraintToInfoTraceMp
, cnstrTraceMpSingleton, cnstrTraceMpElimTrace, cnstrTraceMpFromList
, ConstraintToInfoMap
, emptyCnstrMp
, cnstrMpUnion, cnstrMpUnions
, mkProveConstraint, mkAssumeConstraint, mkAssumeConstraint'
, rhaMbId )
where
import UHC.Light.Compiler.Base.Common
import UHC.Light.Compiler.Ty
import UHC.Util.CHR
import UHC.Light.Compiler.CHR.CtxtRedOnly.Key
import UHC.Util.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 38 "src/ehc/CHR/CtxtRedOnly/Constraint.chs" #-}
type instance CHRMatchableKey VarMp = Key

{-# LINE 46 "src/ehc/CHR/CtxtRedOnly/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, Generic)

type Constraint = Constraint' CHRPredOcc RedHowAnnotation

type instance TTKey (Constraint' p info) = TTKey p
type instance TrTrKey (Constraint' p info) = TTKey p

{-# LINE 67 "src/ehc/CHR/CtxtRedOnly/Constraint.chs" #-}
#if __GLASGOW_HASKELL__ >= 708
deriving instance Typeable  Constraint'
#else
deriving instance Typeable2 Constraint'
#endif

{-# LINE 75 "src/ehc/CHR/CtxtRedOnly/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 83 "src/ehc/CHR/CtxtRedOnly/Constraint.chs" #-}
instance (CHRMatchable env p s, TTKey p ~ Key) => CHRMatchable env (Constraint' p info) s where
  chrMatchTo env s c1 c2
    = do { (_,p1,_) <- cnstrReducablePart c1
         ; (_,p2,_) <- cnstrReducablePart c2
         ; chrMatchTo env s p1 p2
         }
  -- chrBuiltinSolve e s x = Nothing

{-
-- not yet supported
instance (CHREmptySubstitution s, VarLookupCmb s s) => CHRBuiltinSolvable env (Constraint' p info) s where
  chrBuiltinSolve e s x = Nothing
-}

{-# LINE 99 "src/ehc/CHR/CtxtRedOnly/Constraint.chs" #-}
instance (TTKeyable p, TTKey p ~ Key) => TTKeyable (Constraint' p info) where
  -- type TTKey (Constraint' p info) = Key
  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 109 "src/ehc/CHR/CtxtRedOnly/Constraint.chs" #-}
type instance ExtrValVarKey (Constraint' p info) = ExtrValVarKey p

instance (VarExtractable p) => VarExtractable (Constraint' p info) 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 129 "src/ehc/CHR/CtxtRedOnly/Constraint.chs" #-}
-- | intermediate structure for holding constraint and related info until it can safely be assumed
type CHRIntermediateUntilAssume = (CHRPredOcc,(PredScope,ConstraintToInfoTraceMp))

{-# LINE 134 "src/ehc/CHR/CtxtRedOnly/Constraint.chs" #-}
mkProve :: CHRPredOcc -> Constraint
mkProve = Prove

mkAssume :: CHRPredOcc -> Constraint
mkAssume = Assume

mkReduction :: CHRPredOcc -> RedHowAnnotation -> [CHRPredOcc] -> Constraint
mkReduction p i ps
  = Reduction p i ps
              varlookupEmpty

{-# LINE 167 "src/ehc/CHR/CtxtRedOnly/Constraint.chs" #-}
mkProveConstraint :: Range -> Pred -> UID -> PredScope -> (Constraint,RedHowAnnotation)
mkProveConstraint r pr i sc =  (mkProve (mkCHRPredOccRng r pr sc),RedHow_ProveObl i sc)

mkAssumeConstraint'' :: Range -> Pred -> VarUIDHsName -> PredScope -> (Constraint,RedHowAnnotation)
mkAssumeConstraint'' r pr vun sc =  (mkAssume (mkCHRPredOccRng r pr sc),RedHow_Assumption vun sc)

mkAssumeConstraint' :: Range -> Pred -> UID -> HsName -> PredScope -> (Constraint,RedHowAnnotation)
mkAssumeConstraint' r pr i n sc =  mkAssumeConstraint'' r pr (VarUIDHs_Name i n) sc

mkAssumeConstraint :: Range -> Pred -> UID -> PredScope -> (Constraint,RedHowAnnotation)
mkAssumeConstraint r pr i sc =  mkAssumeConstraint'' r pr (VarUIDHs_UID i) sc

{-# LINE 185 "src/ehc/CHR/CtxtRedOnly/Constraint.chs" #-}
gathPredLToProveCnstrMp :: [PredOcc] -> ConstraintToInfoMap
gathPredLToProveCnstrMp l = cnstrMpFromList [ rngLift (poRange po) mkProveConstraint (poPr po) (poId po) (poScope po) | po <- l ]

gathPredLToAssumeCnstrMp :: [PredOcc] -> ConstraintToInfoMap
gathPredLToAssumeCnstrMp l = cnstrMpFromList [ rngLift (poRange po) mkAssumeConstraint (poPr po) (poId po) (poScope po) | po <- l ]

{-# LINE 193 "src/ehc/CHR/CtxtRedOnly/Constraint.chs" #-}
-- | Lift predicate occurrences to new scope, used to lift unproven predicates to an outer scope.
predOccCnstrMpLiftScope :: PredScope -> ConstraintToInfoMap -> ConstraintToInfoMap
predOccCnstrMpLiftScope sc
  = Map.mapKeysWith (++) c . Map.map (map i)
  where c (Prove o@(CHRPredOcc {cpoCxt=cx}))
            = mkProve (o {cpoCxt = cx {cpocxScope = sc}})
        c x = x
        i (RedHow_ProveObl id _)
            = RedHow_ProveObl id sc
        i x = x

{-# LINE 210 "src/ehc/CHR/CtxtRedOnly/Constraint.chs" #-}
data RedHowAnnotation
  =  RedHow_ByInstance    !HsName  !Pred  !PredScope		-- inst name, for pred, in scope
  |  RedHow_BySuperClass  !HsName  !Int   !CTag						-- field name, offset, tag info of dict
  |  RedHow_ProveObl      !UID  !PredScope
  |  RedHow_Assumption    !VarUIDHsName  !PredScope
  |  RedHow_ByScope		  !ByScopeRedHow							-- variant, for distinguishing during debugging
  |  RedHow_ByLabel       !Label !LabelOffset !PredScope
  |  RedHow_Lambda        !UID !PredScope
  deriving
    ( Eq, Ord
    , Typeable
    , Generic
    )

{-# LINE 241 "src/ehc/CHR/CtxtRedOnly/Constraint.chs" #-}
rhaMbId :: RedHowAnnotation -> Maybe UID
rhaMbId (RedHow_ProveObl i _) = Just i
rhaMbId _                     = Nothing

{-# LINE 247 "src/ehc/CHR/CtxtRedOnly/Constraint.chs" #-}
instance Show RedHowAnnotation where
  show = showPP . pp

{-# LINE 252 "src/ehc/CHR/CtxtRedOnly/Constraint.chs" #-}
instance PP RedHowAnnotation where
  pp (RedHow_ByInstance   s p sc)       =    "inst"   >#< {- ppParens (vm >#< "`varUpd`") >#< -} ppParensCommas [pp p, pp s, pp sc]
  pp (RedHow_BySuperClass s _ _ )       =    "super"  >#< s
  pp (RedHow_ProveObl     i   sc)       =    "prove"  >#< i >#< sc
  pp (RedHow_Assumption   vun sc)       =    "assume" >#< ppParensCommas [pp vun, pp sc]
  pp (RedHow_ByScope      v     )       =    "scope"  >|< ppParens v
  pp (RedHow_ByLabel      l o sc)       =    "label"  >#< l >|< "@" >|< o >|< sc
  pp (RedHow_Lambda       i   sc)       =    "lambda" >#< i >#< sc

{-# LINE 280 "src/ehc/CHR/CtxtRedOnly/Constraint.chs" #-}
data ByScopeRedHow
  = ByScopeRedHow_Prove							-- scope reduction based on Prove
  | ByScopeRedHow_Assume						-- scope reduction based on Assume
  | ByScopeRedHow_Other (AlwaysEq String)		-- other reason
  deriving
    ( Eq, Ord
    , Typeable, Generic
    )

-- equality plays no role ??
{-
instance Eq ByScopeRedHow where
  _ == _ = True

instance Ord ByScopeRedHow where
  _ `compare` _ = EQ
-}

instance Show ByScopeRedHow where
  show ByScopeRedHow_Prove     = "prv"
  show ByScopeRedHow_Assume    = "ass"
  show (ByScopeRedHow_Other s) = show s

instance PP ByScopeRedHow where
  pp = pp . show

{-# LINE 314 "src/ehc/CHR/CtxtRedOnly/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

type UnresolvedTrace = UnresolvedTrace' CHRPredOcc RedHowAnnotation

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 351 "src/ehc/CHR/CtxtRedOnly/Constraint.chs" #-}
-- | Map from constraint to something
type ConstraintMp'' p info x = Map.Map (Constraint' p info) [x]
type ConstraintMp'         x = ConstraintMp'' CHRPredOcc RedHowAnnotation x

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

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

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

cnstrMpMap :: (x -> y) -> ConstraintMp' x -> ConstraintMp' y
cnstrMpMap f = Map.map (map f)

{-# LINE 371 "src/ehc/CHR/CtxtRedOnly/Constraint.chs" #-}
-- type ConstraintToInfoTraceMp' p info = ConstraintMp'' p info (info,[UnresolvedTrace' p info])

-- | Map from constraint to info + trace
type ConstraintToInfoTraceMp = ConstraintMp' (RedHowAnnotation,[UnresolvedTrace])

{-# LINE 378 "src/ehc/CHR/CtxtRedOnly/Constraint.chs" #-}
cnstrTraceMpFromList :: [(Constraint,(RedHowAnnotation,[UnresolvedTrace]))] -> ConstraintToInfoTraceMp
cnstrTraceMpFromList = cnstrMpFromList

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

cnstrTraceMpElimTrace :: ConstraintToInfoTraceMp -> ConstraintToInfoMap
cnstrTraceMpElimTrace = cnstrMpMap fst

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

{-# LINE 392 "src/ehc/CHR/CtxtRedOnly/Constraint.chs" #-}
-- type ConstraintToInfoMap'     p info = ConstraintMp'' p info info

-- | Map from constraint to info
type ConstraintToInfoMap = ConstraintMp' RedHowAnnotation

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

{-# LINE 404 "src/ehc/CHR/CtxtRedOnly/Constraint.chs" #-}
cnstrMpUnion :: ConstraintMp' x -> ConstraintMp' x -> ConstraintMp' x
cnstrMpUnion = Map.unionWith (++)

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

{-# LINE 416 "src/ehc/CHR/CtxtRedOnly/Constraint.chs" #-}
instance IsConstraint (Constraint' p info) where
  cnstrRequiresSolve (Reduction {}) = False
  cnstrRequiresSolve _              = True

{-# LINE 426 "src/ehc/CHR/CtxtRedOnly/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 438 "src/ehc/CHR/CtxtRedOnly/Constraint.chs" #-}
instance (Serialize p, Serialize i) => Serialize (Constraint' p i)

{-# LINE 454 "src/ehc/CHR/CtxtRedOnly/Constraint.chs" #-}
instance Serialize ByScopeRedHow
instance Serialize RedHowAnnotation