{-# 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.Light.Compiler.Substitutable
import UHC.Util.TreeTrie
import qualified CHR.Data.TreeTrie as TT2
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 41 "src/ehc/CHR/CtxtRedOnly/Constraint.chs" #-}
type instance CHRMatchableKey VarMp = Key

{-# LINE 49 "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
type instance TT2.TrTrKey (Constraint' p info) = TT2.TrTrKey p

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

{-# LINE 79 "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 87 "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 103 "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

instance (TT2.TreeTrieKeyable p, TT2.TrTrKey p ~ Key) => TT2.TreeTrieKeyable (Constraint' p info) where
  toTreeTriePreKey1 c
    = case cnstrReducablePart c of
        Just (s,p,_) -> TT2.prekey1WithChild (Key_Str s) p
        _            -> panic "TT2.TTKeyable (Constraint' p info).toTTKey'" -- ttkEmpty

{-# LINE 119 "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 139 "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 144 "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 177 "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 195 "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 203 "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 220 "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 251 "src/ehc/CHR/CtxtRedOnly/Constraint.chs" #-}
rhaMbId :: RedHowAnnotation -> Maybe UID
rhaMbId (RedHow_ProveObl i _) = Just i
rhaMbId _                     = Nothing

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

{-# LINE 262 "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 290 "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 324 "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 361 "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 367 "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 381 "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 388 "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 402 "src/ehc/CHR/CtxtRedOnly/Constraint.chs" #-}
-- type ConstraintToInfoMap'     p info = ConstraintMp'' p info info

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

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

{-# LINE 414 "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 426 "src/ehc/CHR/CtxtRedOnly/Constraint.chs" #-}
instance IsConstraint (Constraint' p info) where
  cnstrRequiresSolve (Reduction {}) = False
  cnstrRequiresSolve _              = True

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

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