content: {-# LANGUAGE OverloadedStrings #-}
  {-# LANGUAGE TemplateHaskellQuotes #-}
  
  {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
  
  module Language.Haskell.Liquid.WiredIn
         ( wiredTyCons
         , wiredDataCons
         , wiredSortedSyms
  
         , charDataCon
  
         -- * Constants for automatic proofs
         , dictionaryVar
         , dictionaryTyVar
         , dictionaryBind
         , proofTyConName
         , combineProofsName
  
         -- * Built in symbols
         , isWiredIn
         , isWiredInName
         , dcPrefix
  
         -- * Deriving classes
         , isDerivedInstance
         , derivingClasses
         ) where
  
  import Prelude                                hiding (error)
  
  -- import Language.Fixpoint.Misc           (mapSnd)
  import Language.Haskell.Liquid.GHC.Misc
  import qualified Liquid.GHC.API as Ghc
  import Liquid.GHC.API (Var, Arity, TyVar, Bind(..), Boxity(..), Expr(..), ForAllTyFlag(Required))
  import Language.Haskell.Liquid.Types.Errors
  import Language.Haskell.Liquid.Types.Names
  import Language.Haskell.Liquid.Types.RType
  import Language.Haskell.Liquid.Types.Types
  import Language.Haskell.Liquid.Types.RefType
  import Language.Haskell.Liquid.Types.Variance
  import Language.Haskell.Liquid.Types.PredType
  
  -- import Language.Fixpoint.Types hiding (panic)
  import qualified Language.Fixpoint.Types.Config as F
  import qualified Language.Fixpoint.Smt.Theories as F
  import qualified Language.Fixpoint.Types as F
  import           Data.Bifunctor (first)
  import qualified Data.HashSet as S
  import           Data.Maybe
  
  import Language.Haskell.Liquid.GHC.TypeRep ()
  
  -- | Horrible hack to support hardwired symbols like
  --      `head`, `tail`, `fst`, `snd`
  --   and other LH generated symbols that
  --   *do not* correspond to GHC Vars and
  --   *should not* be resolved to GHC Vars.
  
  isWiredIn :: F.LocSymbol -> Bool
  isWiredIn x = isWiredInLoc x  || isWiredInName (val x) || isWiredInShape x
  
  isWiredInLoc :: F.LocSymbol -> Bool
  isWiredInLoc sym  = ln == ln' && ln == F.safePos 1 && c == c' && c' == F.safePos 1
    where
      (ln , c)  = spe (loc sym)
      (ln', c') = spe (locE sym)
      spe l    = (x, y) where (_, x, y) = F.sourcePosElts l
  
  isWiredInName :: F.Symbol -> Bool
  isWiredInName x = x `S.member` wiredInNames
  
  wiredInNames :: S.HashSet F.Symbol
  wiredInNames = S.fromList [ "head", "tail", "fst", "snd", "len"]
  
  isWiredInShape :: F.LocSymbol -> Bool
  isWiredInShape x = any (`F.isPrefixOfSym` val x) [F.anfPrefix, F.tempPrefix, dcPrefix]
    -- where s        = val x
          -- dcPrefix = "lqdc"
  
  dcPrefix :: F.Symbol
  dcPrefix = "lqdc"
  
  wiredSortedSyms :: [(F.Symbol, F.Sort)]
  wiredSortedSyms =
      (selfSymbol,selfSort) :
      [(pappSym n, pappSort n) | n <- [1..pappArity]] ++
      wiredTheorySortedSyms
    where
      selfSort = F.FAbs 1 (F.FVar 0)
  
  wiredTheorySortedSyms :: [(F.Symbol, F.Sort)]
  wiredTheorySortedSyms =
      [ (s, srt)
      | s <- wiredTheorySyms
      , let srt = F.tsSort $
                    fromMaybe (panic Nothing ("unknown symbol: " ++ show s)) $
                      F.lookupSEnv s (F.theorySymbols F.Z3)
      ]
    where
      wiredTheorySyms =
        [ "Map_default"
        , "Map_select"
        , "Map_store"
  
        , "Set_cup"
        , "Set_cap"
        , "Set_dif"
        , "Set_sng"
        , "Set_emp"
        , "Set_empty"
        , "Set_mem"
        , "Set_sub"
        , "Set_add"
        , "Set_com"
  
        , "Bag_count"
        , "Bag_empty"
        , "Bag_inter_min"
        , "Bag_sng"
        , "Bag_sub"
        , "Bag_union"
        , "Bag_union_max"
  
        , "strLen"
        ]
  
  --------------------------------------------------------------------------------
  -- | LH Primitive TyCons -------------------------------------------------------
  --------------------------------------------------------------------------------
  
  dictionaryVar :: Var
  dictionaryVar   = stringVar "tmp_dictionary_var" (Ghc.ForAllTy (Ghc.Bndr dictionaryTyVar Required) $ Ghc.TyVarTy dictionaryTyVar)
  
  dictionaryTyVar :: TyVar
  dictionaryTyVar = stringTyVar "da"
  
  dictionaryBind :: Bind Var
  dictionaryBind = Rec [(v, Lam a $ App (Var v) (Type $ Ghc.TyVarTy a))]
    where
     v = dictionaryVar
     a = dictionaryTyVar
  
  -----------------------------------------------------------------------
  -- | LH Primitive TyCons ----------------------------------------------
  -----------------------------------------------------------------------
  
  
  combineProofsName :: String
  combineProofsName = "combineProofs"
  
  proofTyConName :: F.Symbol
  proofTyConName = "Proof"
  
  --------------------------------------------------------------------------------
  -- | Predicate Types for WiredIns ----------------------------------------------
  --------------------------------------------------------------------------------
  
  maxArity :: Arity
  maxArity = 7
  
  wiredTyCons :: [TyConP]
  wiredTyCons  = fst wiredTyDataCons
  
  wiredDataCons :: [Located DataConP]
  wiredDataCons = snd wiredTyDataCons
  
  wiredTyDataCons :: ([TyConP] , [Located DataConP])
  wiredTyDataCons = (concat tcs, dummyLoc <$> concat dcs)
    where
      (tcs, dcs)  = unzip $ listTyDataCons : map tupleTyDataCons [2..maxArity]
  
  charDataCon :: Located DataConP
  charDataCon = dummyLoc (DataConP l0 Ghc.charDataCon  [] [] [] [(makeGeneratedLogicLHName "charX",lt)] lt False wiredInName l0)
    where
      l0 = F.dummyPos "LH.Bare.charTyDataCons"
      c  = Ghc.charTyCon
      lt = rApp c [] [] mempty
  
  listTyDataCons :: ([TyConP] , [DataConP])
  listTyDataCons   = ( [TyConP l0 c [RTV tyv] [p] [Covariant] [Covariant] (Just fsize)]
                     , [DataConP l0 Ghc.nilDataCon  [RTV tyv] [p] [] []    lt False wiredInName l0
                     ,  DataConP l0 Ghc.consDataCon [RTV tyv] [p] [] cargs lt False wiredInName l0])
      where
        l0         = F.dummyPos "LH.Bare.listTyDataCons"
        c          = Ghc.listTyCon
        [tyv]      = tyConTyVarsDef c
        t          = rVar tyv :: RSort
        fld        = "fldList"
        xHead      = "head"
        xTail      = "tail"
        p          = PV "p" t (F.vv Nothing) [(t, fld, F.EVar fld)]
        px         = pdVarReft $ PV "p" t (F.vv Nothing) [(t, fld, F.EVar xHead)]
        lt         = rApp c [xt] [rPropP [] $ pdVarReft p] mempty
        xt         = rVar tyv
        xst        = rApp c [RVar (RTV tyv) px] [rPropP [] $ pdVarReft p] mempty
        cargs      = map (first makeGeneratedLogicLHName) [(xTail, xst), (xHead, xt)]
        fsize      = SymSizeFun (dummyLoc "GHC.Types_LHAssumptions.len")
  
  wiredInName :: F.Symbol
  wiredInName = "WiredIn"
  
  tupleTyDataCons :: Int -> ([TyConP] , [DataConP])
  tupleTyDataCons n = ( [TyConP   l0 c  (RTV <$> tyvs) ps tyvarinfo pdvarinfo Nothing]
                      , [DataConP l0 dc (RTV <$> tyvs) ps []  cargs  lt False wiredInName l0])
    where
      tyvarinfo     = replicate n     Covariant
      pdvarinfo     = replicate (n-1) Covariant
      l0            = F.dummyPos "LH.Bare.tupleTyDataCons"
      c             = Ghc.tupleTyCon   Boxed n
      dc            = Ghc.tupleDataCon Boxed n
      tyvs@(tv:tvs) = tyConTyVarsDef c
      (ta:ts)       = (rVar <$> tyvs) :: [RSort]
      flds          = mks "fld_Tuple"
      fld           = "fld_Tuple"
      x1:xs         = mks ("x_Tuple" ++ show n)
      ps            = mkps pnames (ta:ts) ((fld, F.EVar fld) : zip flds (F.EVar <$> flds))
      ups           = uPVar <$> ps
      pxs           = mkps pnames (ta:ts) ((fld, F.EVar x1) : zip flds (F.EVar <$> xs))
      lt            = rApp c (rVar <$> tyvs) (rPropP [] . pdVarReft <$> ups) mempty
      xts           = zipWith (\v p -> RVar (RTV v) (pdVarReft p)) tvs pxs
      cargs         = map (first makeGeneratedLogicLHName) $ reverse $ (x1, rVar tv) : zip xs xts
      pnames        = mks_ "p"
      mks  x        = (\i -> F.symbol (x++ show i)) <$> [1..n]
      mks_ x        = (\i -> F.symbol (x++ show i)) <$> [2..n]
  
  
  mkps :: [F.Symbol]
       -> [t] -> [(F.Symbol, F.Expr)] -> [PVar t]
  mkps ns (t:ts) ((f,x):fxs) = reverse $ mkps_ ns ts fxs [(t, f, x)] []
  mkps _  _      _           = panic Nothing "Bare : mkps"
  
  mkps_ :: [F.Symbol]
        -> [t]
        -> [(F.Symbol, F.Expr)]
        -> [(t, F.Symbol, F.Expr)]
        -> [PVar t]
        -> [PVar t]
  mkps_ []     _       _          _    ps = ps
  mkps_ (n:ns) (t:ts) ((f, x):xs) args ps = mkps_ ns ts xs (a:args) (p:ps)
    where
      p                                   = PV n t (F.vv Nothing) args
      a                                   = (t, f, x)
  mkps_ _     _       _          _    _ = panic Nothing "Bare : mkps_"
  
  
  --------------------------------------------------------------------------------
  isDerivedInstance :: Ghc.ClsInst -> Bool
  --------------------------------------------------------------------------------
  isDerivedInstance i = F.notracepp ("IS-DERIVED: " ++ F.showpp classSym)
                      $ S.member classSym derivingClassesSet
    where
      classSym        = F.symbol . Ghc.is_cls $ i
  
  derivingClassesSet :: S.HashSet F.Symbol
  derivingClassesSet = S.fromList $ map F.symbol derivingClasses
  
  derivingClasses :: [String]
  derivingClasses =
    [ show ''Eq
    , show ''Ord
    , show ''Enum
    , show ''Show
    , show ''Read
    , show ''Monad
    , show ''Applicative
    , show ''Functor
    , show ''Foldable
    , show ''Traversable
    , show ''Fractional
    -- , "GHC.Enum.Bounded"
    -- , "GHC.Base.Monoid"
    ]
  