{-# LANGUAGE DeriveDataTypeable         #-}
{-# LANGUAGE DeriveFoldable             #-}
{-# LANGUAGE DeriveGeneric              #-}
{-# LANGUAGE DeriveTraversable          #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE NoMonomorphismRestriction  #-}
{-# LANGUAGE OverloadedStrings          #-}
{-# LANGUAGE UndecidableInstances       #-}

-- | This module contains the data types, operations and
--   serialization functions for representing Fixpoint's
--   implication (i.e. subtyping) and well-formedness
--   constraints in Haskell. The actual constraint
--   solving is done by the `fixpoint.native` which
--   is written in Ocaml.

module Language.Fixpoint.Types (

  -- * Top level serialization
    Fixpoint (..)
  , toFixpoint
  , FInfo (..)

  -- * Rendering
  , showFix
  , traceFix
  , resultDoc

  -- * Symbols
  , Symbol
  , KVar (..)
  , anfPrefix, tempPrefix, vv, vv_, intKvar
  , symChars, isNonSymbol, nonSymbol
  , isNontrivialVV
  , symbolText, symbolString

  -- * Creating Symbols
  , dummySymbol
  , intSymbol
  , tempSymbol
  , qualifySymbol
  , suffixSymbol

  -- * Embedding to Fixpoint Types
  , Sort (..), FTycon, TCEmb
  , intFTyCon
  , boolFTyCon
  , realFTyCon
  , strFTyCon
  , propFTyCon
  , listFTyCon
  , appFTyCon
  , fTyconSymbol
  , symbolFTycon

  , strSort
  , fApp
  , fObj
  , isListTC
  , isFAppTyTC

  -- * Expressions and Predicates
  , SymConst (..)
  , Constant (..)
  , Bop (..), Brel (..)
  , Expr (..), Pred (..)
  , eVar
  , eProp
  , pAnd, pOr, pIte
  , isTautoPred
  , symConstLits

  -- * Generalizing Embedding with Typeclasses
  , Symbolic (..)
  , Expression (..)
  , Predicate (..)

  -- * Constraints
  , WfC (..)
  , SubC, sid, sgrd, senv, slhs, srhs, subC, lhsCs, rhsCs, wfC
  , Tag

  -- * Accessing Constraints
  , envCs
  , addIds, sinfo
  , trueSubCKvar
  , removeLhsKvars

  -- * Solutions
  , Result
  , FixResult (..)
  , FixSolution

  -- * Environments
  , SEnv, SESearch(..)
  , emptySEnv, toListSEnv, fromListSEnv
  -- , mapSEnv
  , mapSEnvWithKey
  , insertSEnv, deleteSEnv, memberSEnv, lookupSEnv
  , intersectWithSEnv
  , filterSEnv
  , lookupSEnvWithDistance

  , FEnv, insertFEnv
  , IBindEnv, BindId, BindMap
  , emptyIBindEnv, insertsIBindEnv, deleteIBindEnv, elemsIBindEnv

  , BindEnv
  , insertBindEnv, emptyBindEnv, lookupBindEnv, mapBindEnv
  , bindEnvFromList, bindEnvToList
  , unionIBindEnv

  -- * Refinements
  , Refa (..), SortedReft (..), Reft(..), Reftable(..)

  -- * Constructing Refinements
  , refa
  , reft                    -- "smart
  , trueSortedReft          -- trivial reft
  , trueRefa                -- trivial reft
  , trueReft                -- trivial reft
  , exprReft                -- singleton: v == e
  , notExprReft             -- singleton: v /= e
  , uexprReft               -- singleton: v ~~ e
  , symbolReft              -- singleton: v == x
  , usymbolReft             -- singleton: v ~~ x
  , propReft                -- singleton: Prop(v) <=> p
  , predReft                -- any pred : p
  , reftPred, reftBind
  , isFunctionSortedReft, functionSort
  , isNonTrivial
  , isSingletonReft
  , isEVar
  , isFalse
  , flattenRefas, squishRefas, conjuncts
  , shiftVV
  , mapPredReft

  -- * Substitutions
  , Subst (..)
  , Subable (..)
  , mkSubst
  , isEmptySubst
  -- , emptySubst
  -- , catSubst
  , substExcept
  , substfExcept
  , subst1Except
  , sortSubst
  , targetSubstSyms

  -- * Functions on @Result@
  , colorResult

  -- * Cut KVars
  , Kuts (..)
  , ksEmpty
  , ksUnion

  -- * Qualifiers
  , Qualifier (..)

  -- * FQ Definitions
  , Def (..)

  -- * Located Values
  , Located (..)
  , LocSymbol, LocText
  , dummyLoc, dummyPos, dummyName, isDummy
  ) where

import           Debug.Trace               (trace)

import           Data.Generics             (Data)
import           Data.Typeable             (Typeable)
import           GHC.Generics              (Generic)

import           Data.Char                 (toLower)
import qualified Data.Foldable             as F
import           Data.Functor
import           Data.Hashable
-- import           Data.Interned
import           Data.List                 (foldl', intersect, nub, sort)
import           Data.Monoid               hiding ((<>))
import           Data.String
import           Data.Text                 (Text)
import qualified Data.Text                 as T
import           Data.Traversable
import           Control.DeepSeq
import           Control.Exception         (assert)
import           Data.Maybe                (isJust, mapMaybe, listToMaybe, fromMaybe)
import           Text.Printf               (printf)

import           Language.Fixpoint.Misc
import           Text.Parsec.Pos
import           Text.PrettyPrint.HughesPJ

import           Data.Array                hiding (indices)
import qualified Data.HashMap.Strict       as M
import qualified Data.HashSet              as S
import           Language.Fixpoint.Names


class Fixpoint a where
  toFix    :: a -> Doc

  simplify :: a -> a
  simplify =  id

------------------------------------------------------------------------
-- | Entities in Query File --------------------------------------------
------------------------------------------------------------------------

data Def a
  = Srt Sort
  | Axm Pred
  | Cst (SubC a)
  | Wfc (WfC a)
  | Con Symbol Sort
  | Qul Qualifier
  | Kut KVar
  | IBind Int Symbol SortedReft
  deriving (Generic)
  --  Sol of solbind
  --  Dep of FixConstraint.dep

------------------------------------------------------------------------

showFix :: (Fixpoint a) => a -> String
showFix =  render . toFix

traceFix     ::  (Fixpoint a) => String -> a -> a
traceFix s x = trace ("\nTrace: [" ++ s ++ "] : " ++ showFix x) x

type TCEmb a    = M.HashMap a FTycon

exprSymbols :: Expr -> [Symbol]
exprSymbols = go
  where
    go (EVar x)        = [x]
    go (ELit x _)      = [val x]
    go (EApp f es)     = val f : concatMap go es
    go (ENeg e)        = go e
    go (EBin _ e1 e2)  = go e1 ++ go e2
    go (EIte p e1 e2)  = predSymbols p ++ go e1 ++ go e2
    go (ECst e _)      = go e
    go _               = []

predSymbols :: Pred -> [Symbol]
predSymbols = go
  where
    go (PAnd ps)          = concatMap go ps
    go (POr ps)           = concatMap go ps
    go (PNot p)           = go p
    go (PIff p1 p2)       = go p1 ++ go p2
    go (PImp p1 p2)       = go p1 ++ go p2
    go (PBexp e)          = exprSymbols e
    go (PAtom _ e1 e2)    = exprSymbols e1 ++ exprSymbols e2
    go (PKVar _ (Su su')) = {- CUTSOLVER k : -} concatMap syms su'
    go (PAll xts p)       = (fst <$> xts) ++ go p
    go _                  = []

---------------------------------------------------------------
---------- (Kut) Sets of Kvars --------------------------------
---------------------------------------------------------------
newtype KVar = KV {kv :: Symbol } deriving (Eq, Ord, Data, Typeable, Generic, IsString)

intKvar :: Integer -> KVar
intKvar = KV . intSymbol "k_"

instance Show KVar where
  show (KV x) = "$" ++ show x

instance Hashable KVar

newtype Kuts = KS { ksVars :: S.HashSet KVar } deriving (Show)

instance NFData Kuts where
  rnf (KS _) = () -- rnf s

instance Fixpoint Kuts where
  toFix (KS s) = vcat $ ((text "cut " <>) . toFix) <$> S.toList s

ksEmpty :: Kuts
ksEmpty             = KS S.empty

ksUnion :: [KVar] -> Kuts -> Kuts
ksUnion kvs (KS s') = KS (S.union (S.fromList kvs) s')

---------------------------------------------------------------
---------- Converting Constraints to Fixpoint Input -----------
---------------------------------------------------------------

instance (Eq a, Hashable a, Fixpoint a) => Fixpoint (S.HashSet a) where
  toFix xs = brackets $ sep $ punctuate (text ";") (toFix <$> S.toList xs)
  simplify = S.fromList . map simplify . S.toList

instance Fixpoint a => Fixpoint (Maybe a) where
  toFix    = maybe (text "Nothing") ((text "Just" <+>) . toFix)
  simplify = fmap simplify

instance Fixpoint a => Fixpoint [a] where
  toFix xs = brackets $ sep $ punctuate (text ";") (fmap toFix xs)
  simplify = map simplify

instance (Fixpoint a, Fixpoint b) => Fixpoint (a,b) where
  toFix   (x,y)  = toFix x <+> text ":" <+> toFix y
  simplify (x,y) = (simplify x, simplify y)

toFixGs :: SEnv SortedReft -> Doc
toFixGs (SE e) = vcat  $ map (toFixConstant . mapSnd sr_sort) $ hashMapToAscList e

toFixConstant (c, so)
  = text "constant" <+> toFix c <+> text ":" <+> parens (toFix so)

----------------------------------------------------------------------
------------------------ Type Constructors ---------------------------
----------------------------------------------------------------------

newtype FTycon = TC LocSymbol deriving (Eq, Ord, Show, Data, Typeable, Generic)

intFTyCon, boolFTyCon, realFTyCon, strFTyCon, propFTyCon, appFTyCon, listFTyCon :: FTycon
intFTyCon  = TC $ dummyLoc "int"
boolFTyCon = TC $ dummyLoc "bool"
realFTyCon = TC $ dummyLoc "real"
strFTyCon  = TC $ dummyLoc strConName
propFTyCon = TC $ dummyLoc propConName
listFTyCon = TC $ dummyLoc listConName
appFTyCon  = TC $ dummyLoc "FAppTy"

isListTC, isFAppTyTC :: FTycon -> Bool
isListTC (TC (Loc _ _ c)) = c == listConName
isTupTC  (TC (Loc _ _ c)) = c == tupConName
isFAppTyTC = (== appFTyCon)

fTyconSymbol :: FTycon -> Located Symbol
fTyconSymbol (TC s) = s

symbolFTycon :: LocSymbol -> FTycon
symbolFTycon c
  | val c == listConName
  = TC $ fmap (const listConName) c
  | otherwise
  = TC c

-- stringSort   :: String -> Sort
-- stringSort s = FApp (stringFTycon s) []
--            -- ALTERNATIVEL = FObj . stringSymbol

fApp                  :: Either FTycon Sort -> [Sort] -> Sort
fApp (Left c) ts
  | c == intFTyCon    = FInt
  | c == realFTyCon   = FReal
  | otherwise         = fAppSorts (fTyconSort c) ts
fApp (Right t) ts     = fAppSorts t ts

fAppSorts :: Sort -> [Sort] -> Sort
fAppSorts = foldl' (\t1 t2 -> FApp appFTyCon [t1, t2])

fTyconSort :: FTycon -> Sort
fTyconSort = (`FApp` [])

fObj :: LocSymbol -> Sort
fObj = fTyconSort . TC


----------------------------------------------------------------------
------------------------------- Sorts --------------------------------
----------------------------------------------------------------------

data Sort = FInt
          | FReal
          | FNum                 -- ^ numeric kind for Num tyvars
          | FFrac                -- ^ numeric kind for Fractional tyvars
          | FObj  Symbol         -- ^ uninterpreted type
          | FVar  !Int           -- ^ fixpoint type variable
          | FFunc !Int ![Sort]   -- ^ type-var arity, in-ts ++ [out-t]
          | FApp FTycon [Sort]   -- ^ constructed type
              deriving (Eq, Ord, Show, Data, Typeable, Generic)

{-@ FFunc :: Nat -> ListNE Sort -> Sort @-}

instance Hashable Sort

newtype Sub = Sub [(Int, Sort)]

instance Fixpoint Sort where
  toFix = toFixSort

toFixSort :: Sort -> Doc
toFixSort (FVar i)        = text "@"   <> parens (toFix i)
toFixSort FInt            = text "int"
toFixSort FReal           = text "real"
toFixSort FFrac           = text "frac"
toFixSort (FObj x)        = toFix x
toFixSort FNum            = text "num"
toFixSort (FFunc n ts)    = text "func" <> parens (toFix n <> text ", " <> toFix ts)
toFixSort (FApp c [t])
  | isListTC c            = brackets $ toFixSort t
toFixSort (FApp c [FApp c' [],t])
  | isFAppTyTC c &&
    isListTC c'           = brackets $ toFixSort t
toFixSort (FApp c ts)     = toFix c <+> intersperse space (fp <$> ts)
    where
      fp s@(FApp _ (_:_)) = parens $ toFixSort s
      fp s                = toFixSort s


instance Fixpoint FTycon where
  toFix (TC s)       = toFix s


------------------------------------------------------------------------
sortSubst                  :: M.HashMap Symbol Sort -> Sort -> Sort
------------------------------------------------------------------------
sortSubst θ t@(FObj x)   = fromMaybe t (M.lookup x θ)
sortSubst θ (FFunc n ts) = FFunc n (sortSubst θ <$> ts)
sortSubst θ (FApp c ts)  = FApp c  (sortSubst θ <$> ts)
sortSubst _  t           = t


instance Show Subst where
  show = showFix

instance Fixpoint Subst where
  toFix (Su m) = case {- hashMapToAscList -} m of
                   []  -> empty
                   xys -> hcat $ map (\(x,y) -> brackets $ toFix x <> text ":=" <> toFix y) xys

targetSubstSyms :: Subst -> [Symbol]
targetSubstSyms (Su ms) = syms $ snd <$> ms


---------------------------------------------------------------
------------------------- Expressions -------------------------
---------------------------------------------------------------

-- | Uninterpreted constants that are embedded as  "constant symbol : Str"

data SymConst = SL !Text
              deriving (Eq, Ord, Show, Data, Typeable, Generic)

data Constant = I !Integer
              | R !Double
              | L !Text !Sort
              deriving (Eq, Ord, Show, Data, Typeable, Generic)

data Brel = Eq | Ne | Gt | Ge | Lt | Le | Ueq | Une
            deriving (Eq, Ord, Show, Data, Typeable, Generic)

data Bop  = Plus | Minus | Times | Div | Mod
            deriving (Eq, Ord, Show, Data, Typeable, Generic)
              -- NOTE: For "Mod" 2nd expr should be a constant or a var *)

data Expr = ESym !SymConst
          | ECon !Constant
          | EVar !Symbol
          | ELit !LocSymbol !Sort
          | EApp !LocSymbol ![Expr]
          | ENeg !Expr
          | EBin !Bop !Expr !Expr
          | EIte !Pred !Expr !Expr
          | ECst !Expr !Sort
          | EBot
          deriving (Eq, Ord, Show, Data, Typeable, Generic)

instance Fixpoint Integer where
  toFix = integer

instance Fixpoint Double where
  toFix = double

instance Fixpoint Constant where
  toFix (I i)   = toFix i
  toFix (R i)   = toFix i
  toFix (L s t) = parens $ text "lit" <+> text "\"" <> toFix s <> text "\"" <+> toFix t

instance Fixpoint SymConst where
  toFix  = toFix . encodeSymConst

instance Fixpoint Symbol where
  toFix = text . encode . T.unpack . symbolText

instance Fixpoint KVar where
  toFix (KV k) = text "$" <> toFix k

instance Fixpoint Text where
  toFix = text . T.unpack


instance Fixpoint Brel where
  toFix Eq  = text "="
  toFix Ne  = text "!="
  toFix Ueq = text "~~"
  toFix Une = text "!~"
  toFix Gt  = text ">"
  toFix Ge  = text ">="
  toFix Lt  = text "<"
  toFix Le  = text "<="

instance Fixpoint Bop where
  toFix Plus  = text "+"
  toFix Minus = text "-"
  toFix Times = text "*"
  toFix Div   = text "/"
  toFix Mod   = text "mod"

instance Fixpoint Expr where
  toFix (ESym c)       = toFix $ encodeSymConst c
  toFix (ECon c)       = toFix c
  toFix (EVar s)       = toFix s
  toFix (ELit s _)     = toFix s
  toFix (EApp f es)    = toFix f <> parens (toFix es)
  toFix (ENeg e)       = parens $ text "-" <+> parens (toFix e)
  toFix (EBin o e1 e2) = parens $ toFix e1 <+> toFix o <+> toFix e2
  toFix (EIte p e1 e2) = parens $ toFix p <+> text "?" <+> toFix e1 <+> text ":" <+> toFix e2
  toFix (ECst e so)    = parens $ toFix e <+> text " : " <+> toFix so
  toFix (EBot)         = text "_|_"

----------------------------------------------------------
--------------------- Predicates -------------------------
----------------------------------------------------------


data Pred = PTrue
          | PFalse
          | PAnd   ![Pred]
          | POr    ![Pred]
          | PNot   !Pred
          | PImp   !Pred !Pred
          | PIff   !Pred !Pred
          | PBexp  !Expr
          | PAtom  !Brel  !Expr !Expr
          | PKVar  !KVar !Subst
          | PAll   ![(Symbol, Sort)] !Pred
          | PTop
          deriving (Eq, Ord, Show, Data, Typeable, Generic)

{-@ type ListNE a = {v:[a] | 0 < len v} @-}

{-@ PAnd :: ListNE Pred -> Pred @-}



instance Hashable Brel
instance Hashable Bop
instance Hashable SymConst
instance Hashable Constant
instance Hashable Subst
instance Hashable Expr
instance Hashable Pred

instance Fixpoint Pred where
  toFix PTop             = text "???"
  toFix PTrue            = text "true"
  toFix PFalse           = text "false"
  toFix (PBexp e)        = parens $ text "?" <+> toFix e
  toFix (PNot p)         = parens $ text "~" <+> parens (toFix p)
  toFix (PImp p1 p2)     = parens $ toFix p1 <+> text "=>" <+> toFix p2
  toFix (PIff p1 p2)     = parens $ toFix p1 <+> text "<=>" <+> toFix p2
  toFix (PAnd ps)        = text "&&" <+> toFix ps
  toFix (POr  ps)        = text "||" <+> toFix ps
  toFix (PAtom r e1 e2)  = parens $ toFix e1 <+> toFix r <+> toFix e2
  toFix (PKVar k su)     = toFix k <> toFix su
  toFix (PAll xts p)     = text "forall" <+> toFix xts <+> text "." <+> toFix p

  simplify (PAnd [])     = PTrue
  simplify (POr  [])     = PFalse
  simplify (PAnd [p])    = simplify p
  simplify (POr  [p])    = simplify p

  simplify (PAnd ps)
    | any isContraPred ps = PFalse
    | otherwise           = PAnd $ filter (not . isTautoPred) $ map simplify ps

  simplify (POr  ps)
    | any isTautoPred ps = PTrue
    | otherwise          = POr  $ filter (not . isContraPred) $ map simplify ps

  simplify p
    | isContraPred p     = PFalse
    | isTautoPred  p     = PTrue
    | otherwise          = p

isContraPred   :: Pred -> Bool
isContraPred z = eqC z || (z `elem` contras)
  where
    contras    = [PFalse]

    eqC (PAtom Eq (ECon x) (ECon y))
               = x /= y
    eqC (PAtom Ueq (ECon x) (ECon y))
               = x /= y
    eqC (PAtom Ne x y)
               = x == y
    eqC (PAtom Une x y)
               = x == y
    eqC _      = False

isTautoPred   :: Pred -> Bool
isTautoPred z  = z == PTop || z == PTrue || eqT z
  where
    eqT (PAtom Le x y)
               = x == y
    eqT (PAtom Ge x y)
               = x == y
    eqT (PAtom Eq x y)
               = x == y
    eqT (PAtom Ueq x y)
               = x == y
    eqT (PAtom Ne (ECon x) (ECon y))
               = x /= y
    eqT (PAtom Une (ECon x) (ECon y))
               = x /= y
    eqT _      = False

isEVar :: Expr -> Bool
isEVar (EVar _) = True
isEVar _        = False

isEq  :: Brel -> Bool
isEq r          = r == Eq || r == Ueq

isSingletonReft :: Reft -> Maybe Expr
isSingletonReft (Reft (v, ra)) = firstMaybe (isSingletonExpr v) $ conjuncts $ raPred ra

firstMaybe :: (a -> Maybe b) -> [a] -> Maybe b
firstMaybe f = listToMaybe . mapMaybe f

--   where 
--     go (PAtom r e1 e2) | e1 == EVar v && isEq r = Just e2
--                        | e2 == EVar v && isEq r = Just e1
--     go _                                        = Nothing

isSingletonExpr :: Symbol -> Pred -> Maybe Expr
isSingletonExpr v (PAtom r e1 e2)
  | e1 == EVar v && isEq r = Just e2
  | e2 == EVar v && isEq r = Just e1
isSingletonExpr _ _        = Nothing

pAnd          = simplify . PAnd
pOr           = simplify . POr
pIte p1 p2 p3 = pAnd [p1 `PImp` p2, (PNot p1) `PImp` p3]

mkProp        = PBexp . EApp (dummyLoc propConName) . (: [])

pprReft (Reft (v, Refa p)) d
  | isTautoPred p
  = d
  | otherwise
  = braces (toFix v <+> colon <+> d <+> text "|" <+> ppRas [Refa p])

pprReftPred (Reft (_, Refa p))
  | isTautoPred p
  = text "true"
  | otherwise
  = ppRas [Refa p]

ppRas = cat . punctuate comma . map toFix . flattenRefas

------------------------------------------------------------------------
-- | Generalizing Symbol, Expression, Predicate into Classes -----------
------------------------------------------------------------------------

-- | Values that can be viewed as Constants

-- | Values that can be viewed as Expressions

class Expression a where
  expr   :: a -> Expr

-- | Values that can be viewed as Predicates

class Predicate a where
  prop   :: a -> Pred

instance Expression Expr where
  expr = id

-- | The symbol may be an encoding of a SymConst.

instance Expression Symbol where
  expr s = maybe (eVar s) ESym (decodeSymConst s)
  -- expr = eVar

instance Expression Text where
  expr = ESym . SL

instance Expression Integer where
  expr = ECon . I

instance Expression Int where
  expr = expr . toInteger

instance Predicate Symbol where
  prop = eProp

instance Predicate Pred where
  prop = id

instance Predicate Bool where
  prop True  = PTrue
  prop False = PFalse

eVar ::  Symbolic a => a -> Expr
eVar = EVar . symbol

eProp ::  Symbolic a => a -> Pred
eProp = mkProp . eVar

relReft :: (Expression a) => Brel -> a -> Reft
relReft r e   = Reft (vv_, Refa $ PAtom r (eVar vv_)  (expr e))

exprReft, notExprReft, uexprReft ::  (Expression a) => a -> Reft
exprReft      = relReft Eq
notExprReft   = relReft Ne
uexprReft     = relReft Ueq

propReft      ::  (Predicate a) => a -> Reft
propReft p    = Reft (vv_, Refa $ PIff (eProp vv_) (prop p))

predReft      :: (Predicate a) => a -> Reft
predReft p    = Reft (vv_, Refa $ prop p)

reft :: Symbol -> Pred -> Reft
reft v p = Reft (v, Refa p)

mapPredReft :: (Pred -> Pred) -> Reft -> Reft
mapPredReft f (Reft (v, Refa p)) = Reft (v, Refa (f p))


---------------------------------------------------------------
----------------- Refinements ---------------------------------
---------------------------------------------------------------

newtype Refa = Refa { raPred :: Pred }
               deriving (Eq, Ord, Show, Data, Typeable, Generic)

newtype Reft = Reft (Symbol, Refa)
               deriving (Eq, Ord, Data, Typeable, Generic)

instance Show Reft where
  show (Reft x) = render $ toFix x

data SortedReft = RR { sr_sort :: !Sort, sr_reft :: !Reft }
                  deriving (Eq, Show, Data, Typeable, Generic)

isFunctionSortedReft :: SortedReft -> Bool
isFunctionSortedReft = isJust . functionSort . sr_sort

functionSort :: Sort -> Maybe (Int, [Sort], Sort)
functionSort (FFunc n ts) = Just (n, its, t)
  where
    (its, t)              = safeUnsnoc "functionSort" ts
functionSort _            = Nothing




isNonTrivial :: Reftable r => r -> Bool
isNonTrivial = not .isTauto

-- sortedReftValueVariable (RR _ (Reft (v,_))) = v

reftPred :: Reft -> Pred
reftPred (Reft (_, Refa p)) = p

reftBind :: Reft -> Symbol
reftBind (Reft (x, _)) = x

refa :: [Pred] -> Refa
refa = Refa . pAnd


---------------------------------------------------------------
-- | Environments ---------------------------------------------
---------------------------------------------------------------


toListSEnv              ::  SEnv a -> [(Symbol, a)]
toListSEnv (SE env)     = M.toList env
fromListSEnv            ::  [(Symbol, a)] -> SEnv a
fromListSEnv            = SE . M.fromList

mapSEnv f (SE env)      = SE (fmap f env)
mapSEnvWithKey f        = fromListSEnv . fmap f . toListSEnv
deleteSEnv x (SE env)   = SE (M.delete x env)
insertSEnv x y (SE env) = SE (M.insert x y env)
lookupSEnv x (SE env)   = M.lookup x env
emptySEnv               = SE M.empty
memberSEnv x (SE env)   = M.member x env
intersectWithSEnv f (SE m1) (SE m2) = SE (M.intersectionWith f m1 m2)
filterSEnv f (SE m)     = SE (M.filter f m)
lookupSEnvWithDistance x (SE env)
  = case M.lookup x env of
     Just z  -> Found z
     Nothing -> Alts $ symbol . T.pack <$> alts
  where
    alts       = takeMin $ zip (editDistance x' <$> ss) ss
    ss         = T.unpack . symbolText <$> fst <$> M.toList env
    x'         = T.unpack $ symbolText x
    takeMin xs = [z | (d, z) <- xs, d == getMin xs]
    getMin     = minimum . (fst <$>)

data SESearch a = Found a | Alts [Symbol]

-- | Functions for Indexed Bind Environment

emptyIBindEnv :: IBindEnv
emptyIBindEnv = FB S.empty

deleteIBindEnv :: BindId -> IBindEnv -> IBindEnv
deleteIBindEnv i (FB s) = FB (S.delete i s)

insertsIBindEnv :: [BindId] -> IBindEnv -> IBindEnv
insertsIBindEnv is (FB s) = FB (foldr S.insert s is)

elemsIBindEnv :: IBindEnv -> [BindId]
elemsIBindEnv (FB s) = S.toList s


-- | Functions for Global Binder Environment
insertBindEnv :: Symbol -> SortedReft -> BindEnv -> (BindId, BindEnv)
insertBindEnv x r (BE n m) = (n, BE (n + 1) (M.insert n (x, r) m))

emptyBindEnv :: BindEnv
emptyBindEnv = BE 0 M.empty

bindEnvFromList :: [(BindId, Symbol, SortedReft)] -> BindEnv
bindEnvFromList bs = BE (1 + nbs) be'
  where
    nbs            = length bs
    be             = M.fromList [(n, (x, r)) | (n, x, r) <- bs]
    be'            = assert (M.size be == nbs) be

bindEnvToList :: BindEnv -> [(BindId, Symbol, SortedReft)]
bindEnvToList (BE _ be) = [(n, x, r) | (n, (x, r)) <- M.toList be]

mapBindEnv :: ((Symbol, SortedReft) -> (Symbol, SortedReft)) -> BindEnv -> BindEnv
mapBindEnv f (BE n m) = BE n $ M.map f m

lookupBindEnv :: BindId -> BindEnv -> (Symbol, SortedReft)
lookupBindEnv k (BE _ m) = fromMaybe err (M.lookup k m)
  where
    err                  = errorstar $ "lookupBindEnv: cannot find binder" ++ show k

unionIBindEnv :: IBindEnv -> IBindEnv -> IBindEnv
unionIBindEnv (FB m1) (FB m2) = FB $ m1 `S.union` m2

instance Functor SEnv where
  fmap = mapSEnv

instance Fixpoint Refa where
  toFix (Refa p)     = toFix $ conjuncts p
  -- toFix (RPvar p)    = toFix p

instance Fixpoint Reft where
  toFix = pprReftPred

instance Fixpoint SortedReft where
  toFix (RR so (Reft (v, ra)))
    = braces
    $ toFix v <+> text ":" <+> toFix so <+> text "|" <+> toFix ra

instance Fixpoint BindEnv where
  toFix (BE _ m) = vcat $ map toFixBind $ hashMapToAscList m

toFixBind (i, (x, r)) = text "bind" <+> toFix i <+> toFix x <+> text ":" <+> toFix r

insertFEnv   = insertSEnv . lower
  where lower s = case unconsSym s of
                    Nothing     -> s
                    Just (c,s') -> consSym (toLower c) s'

-- instance (Fixpoint a) => Fixpoint (SEnv a) where
--   toFix (SE e)    = vcat $ map pprxt $ hashMapToAscList e
--     where
--       pprxt (x,t) = toFix x <+> colon <> colon  <+> toFix t

instance (Fixpoint a) => Fixpoint (SEnv a) where
   toFix (SE m)   = toFix (hashMapToAscList m)

instance Fixpoint (SEnv a) => Show (SEnv a) where
  show = render . toFix

-----------------------------------------------------------------------------
------------------- Constraints ---------------------------------------------
-----------------------------------------------------------------------------

{-@ type Tag = { v : [Int] | len(v) = 1 } @-}
type Tag           = [Int]

type BindId        = Int
type FEnv          = SEnv SortedReft
type BindMap a     = M.HashMap BindId a -- (Symbol, SortedReft)

newtype IBindEnv   = FB (S.HashSet BindId) deriving (Data, Typeable)
newtype SEnv a     = SE { seBinds :: M.HashMap Symbol a }
                     deriving (Eq, Data, Typeable, Generic, F.Foldable, Traversable)


data BindEnv       = BE { beSize  :: Int
                        , beBinds :: BindMap (Symbol, SortedReft)
                        }
                     deriving (Show)

data SubC a = SubC { senv  :: !IBindEnv
                   , sgrd  :: !Pred
                   , slhs  :: !SortedReft
                   , srhs  :: !SortedReft
                   , sid   :: !(Maybe Integer)
                   , stag  :: !Tag
                   , sinfo :: !a
                   }
              deriving (Generic)

data WfC a  = WfC  { wenv  :: !IBindEnv
                   , wrft  :: !SortedReft
                   , wid   :: !(Maybe Integer)
                   , winfo :: !a
                   }
              deriving (Generic)


---------------------------------------------------------------------------
-- | The output of the Solver
---------------------------------------------------------------------------
type Result a = (FixResult (SubC a), M.HashMap KVar Pred)
---------------------------------------------------------------------------


data FixResult a = Crash [a] String
                 | Safe
                 | Unsafe ![a]
                 | UnknownError !String
                   deriving (Show, Generic)

type FixSolution = M.HashMap KVar Pred

instance Eq a => Eq (FixResult a) where
  Crash xs _ == Crash ys _        = xs == ys
  Unsafe xs == Unsafe ys          = xs == ys
  Safe      == Safe               = True
  _         == _                  = False

instance Monoid (FixResult a) where
  mempty                          = Safe
  mappend Safe x                  = x
  mappend x Safe                  = x
  mappend _ c@(Crash _ _)         = c
  mappend c@(Crash _ _) _         = c
  mappend (Unsafe xs) (Unsafe ys) = Unsafe (xs ++ ys)
  mappend u@(UnknownError _) _    = u
  mappend _ u@(UnknownError _)    = u

instance Functor FixResult where
  fmap f (Crash xs msg)   = Crash (f <$> xs) msg
  fmap f (Unsafe xs)      = Unsafe (f <$> xs)
  fmap _ Safe             = Safe
  fmap _ (UnknownError d) = UnknownError d

instance (Ord a, Fixpoint a) => Fixpoint (FixResult (SubC a)) where
  toFix Safe             = text "Safe"
  toFix (UnknownError d) = text $ "Unknown Error: " ++ d
  toFix (Crash xs msg)   = vcat $ [ text "Crash!" ] ++  pprSinfos "CRASH: " xs ++ [parens (text msg)]
  toFix (Unsafe xs)      = vcat $ text "Unsafe:" : pprSinfos "WARNING: " xs

pprSinfos :: (Ord a, Fixpoint a) => String -> [SubC a] -> [Doc]
pprSinfos msg = map ((text msg <>) . toFix) . sort . fmap sinfo


resultDoc :: (Ord a, Fixpoint a) => FixResult a -> Doc
resultDoc Safe             = text "Safe"
resultDoc (UnknownError d) = text $ "Unknown Error: " ++ d
resultDoc (Crash xs msg)   = vcat $ text ("Crash!: " ++ msg) : (((text "CRASH:" <+>) . toFix) <$> xs)
resultDoc (Unsafe xs)      = vcat $ text "Unsafe:"           : (((text "WARNING:" <+>) . toFix) <$> xs)


colorResult (Safe)      = Happy
colorResult (Unsafe _)  = Angry
colorResult (_)         = Sad

instance Show (WfC a) where
  show = showFix

instance Show (SubC a) where
  show = showFix

instance Fixpoint (IBindEnv) where
  toFix (FB ids) = text "env" <+> toFix ids

instance Fixpoint (SubC a) where
  toFix c     = hang (text "\n\nconstraint:") 2 bd
     where bd =   -- text "env" <+> toFix (senv c)
                  toFix (senv c)
              $+$ text "grd" <+> toFix (sgrd c)
              $+$ text "lhs" <+> toFix (slhs c)
              $+$ text "rhs" <+> toFix (srhs c)
              $+$ (pprId (sid c) <+> pprTag (stag c))

instance Fixpoint (WfC a) where
  toFix w     = hang (text "\n\nwf:") 2 bd
    where bd  =   -- text "env"  <+> toFix (wenv w)
                  toFix (wenv w)
              $+$ text "reft" <+> toFix (wrft w)
              $+$ pprId (wid w)

pprId (Just i)  = text "id" <+> tshow i
pprId _         = text ""

pprTag []       = text ""
pprTag is       = text "tag" <+> toFix is

instance Fixpoint Int where
  toFix = tshow

-------------------------------------------------------
------------------- Substitutions ---------------------
-------------------------------------------------------

class Subable a where
  syms   :: a -> [Symbol]
  substa :: (Symbol -> Symbol) -> a -> a
  -- substa f  = substf (EVar . f)

  substf :: (Symbol -> Expr) -> a -> a
  subst  :: Subst -> a -> a
  subst1 :: a -> (Symbol, Expr) -> a
  -- subst1 y (x, e) = subst (Su $ M.singleton x e) y
  subst1 y (x, e) = subst (Su [(x,e)]) y

subst1Except :: (Subable a) => [Symbol] -> a -> (Symbol, Expr) -> a
subst1Except xs z su@(x, _)
  | x `elem` xs = z
  | otherwise   = subst1 z su

substfExcept :: (Symbol -> Expr) -> [Symbol] -> Symbol -> Expr
substfExcept f xs y = if y `elem` xs then EVar y else f y

substExcept  :: Subst -> [Symbol] -> Subst
-- substExcept  (Su m) xs = Su (foldr M.delete m xs)
substExcept  (Su xes) xs = Su $ filter (not . (`elem` xs) . fst) xes

instance Subable Symbol where
  substa f                 = f
  substf f x               = subSymbol (Just (f x)) x
  subst su x               = subSymbol (Just $ appSubst su x) x -- subSymbol (M.lookup x s) x
  syms x                   = [x]

subSymbol (Just (EVar y)) _ = y
subSymbol Nothing         x = x
subSymbol a               b = errorstar (printf "Cannot substitute symbol %s with expression %s" (showFix b) (showFix a))

instance Subable Expr where
  syms                     = exprSymbols
  substa f                 = substf (EVar . f)
  substf f (EApp s es)     = EApp (substf f s) $ map (substf f) es
  substf f (ENeg e)        = ENeg (substf f e)
  substf f (EBin op e1 e2) = EBin op (substf f e1) (substf f e2)
  substf f (EIte p e1 e2)  = EIte (substf f p) (substf f e1) (substf f e2)
  substf f (ECst e so)     = ECst (substf f e) so
  substf f e@(EVar x)      = f x
  substf _ e               = e

  subst su (EApp f es)     = EApp (subst su f) $ map (subst su) es
  subst su (ENeg e)        = ENeg (subst su e)
  subst su (EBin op e1 e2) = EBin op (subst su e1) (subst su e2)
  subst su (EIte p e1 e2)  = EIte (subst su p) (subst su e1) (subst su e2)
  subst su (ECst e so)     = ECst (subst su e) so
  subst su (EVar x)        = appSubst su x
  subst _ e                = e


instance Subable Pred where
  syms                     = predSymbols
  substa f                 = substf (EVar . f)
  substf f (PAnd ps)       = PAnd $ map (substf f) ps
  substf f (POr  ps)       = POr  $ map (substf f) ps
  substf f (PNot p)        = PNot $ substf f p
  substf f (PImp p1 p2)    = PImp (substf f p1) (substf f p2)
  substf f (PIff p1 p2)    = PIff (substf f p1) (substf f p2)
  substf f (PBexp e)       = PBexp $ substf f e
  substf f (PAtom r e1 e2) = PAtom r (substf f e1) (substf f e2)
  substf _ p@(PKVar _ _)   = p
  substf _  (PAll _ _)     = errorstar "substf: FORALL"
  substf _  p              = p

  subst su (PAnd ps)       = PAnd $ map (subst su) ps
  subst su (POr  ps)       = POr  $ map (subst su) ps
  subst su (PNot p)        = PNot $ subst su p
  subst su (PImp p1 p2)    = PImp (subst su p1) (subst su p2)
  subst su (PIff p1 p2)    = PIff (subst su p1) (subst su p2)
  subst su (PBexp e)       = PBexp $ subst su e
  subst su (PAtom r e1 e2) = PAtom r (subst su e1) (subst su e2)
  subst su (PKVar k su')   = PKVar k $ su' `catSubst` su
  subst _  (PAll _ _)      = errorstar "subst: FORALL"
  subst _  p               = p

instance Subable Refa where
  syms (Refa p)           = syms p
  -- syms (RKvar k (Su su'))  = k : concatMap syms ({- M.elems -} su')
  subst su (Refa p)       = Refa $ subst su p
  substa f                 = substf (EVar . f)
  substf f (Refa p)       = Refa (substf f p)

instance (Subable a, Subable b) => Subable (a,b) where
  syms  (x, y)   = syms x ++ syms y
  subst su (x,y) = (subst su x, subst su y)
  substf f (x,y) = (substf f x, substf f y)
  substa f (x,y) = (substa f x, substa f y)

instance Subable a => Subable [a] where
  syms   = concatMap syms
  subst  = map . subst
  substf = map . substf
  substa = map . substa

instance Subable a => Subable (M.HashMap k a) where
  syms   = syms . M.elems
  subst  = M.map . subst
  substf = M.map . substf
  substa = M.map . substa

instance Subable Reft where
  syms (Reft (v, ras))      = v : syms ras
  substa f (Reft (v, ras))  = Reft (f v, substa f ras)
  subst su (Reft (v, ras))  = Reft (v, subst (substExcept su [v]) ras)
  substf f (Reft (v, ras))  = Reft (v, substf (substfExcept f [v]) ras)
  subst1 (Reft (v, ras)) su = Reft (v, subst1Except [v] ras su)


instance Subable SortedReft where
  syms               = syms . sr_reft
  subst su (RR so r) = RR so $ subst su r
  substf f (RR so r) = RR so $ substf f r
  substa f (RR so r) = RR so $ substa f r

newtype Subst = Su [(Symbol, Expr)]
                deriving (Eq, Ord, Data, Typeable, Generic)

appSubst :: Subst -> Symbol -> Expr
appSubst (Su s) x        = fromMaybe (EVar x) (lookup x s)

emptySubst :: Subst
emptySubst = Su [] -- M.empty

catSubst :: Subst -> Subst -> Subst
catSubst = unsafeCatSubst

mkSubst  :: [(Symbol, Expr)] -> Subst
mkSubst  = unsafeMkSubst

isEmptySubst :: Subst -> Bool
isEmptySubst (Su xes) = null xes

unsafeMkSubst  = Su

unsafeCatSubst (Su s1) θ2@(Su s2) = Su $ s1' ++ s2
  where
    s1'                           = mapSnd (subst θ2) <$> s1

-- TODO: this is **not used**, because of degenerate substitutions.
-- e.g. consider: s1 = [v := v], s2 = [v := x].
-- We want s1 `cat` s2 to be [v := x] and not [v := v] ...

unsafeCatSubstIgnoringDead (Su s1) (Su s2) = Su $ s1' ++ s2'
  where
    s1' = mapSnd (subst (Su s2')) <$> s1
    s2' = filter (\(x,_) -> (x `notElem` (fst <$> s1))) s2

-- TODO: nano-js throws all sorts of issues, will look into this later...
-- but also, the check is too conservative, because of degenerate substitutions,
-- see above.
safeCatSubst θ1@(Su s1) θ2@(Su s2)
  | null $ intersect xs1 xs2
  = unsafeCatSubst θ1 θ2
  | otherwise
  = errorstar msg
  where
    s1' = mapSnd (subst (Su s2)) <$> s1
    xs1 = fst <$> s1
    xs2 = fst <$> s2
    msg = printf "Fixpoint.Types catSubst on overlapping substitutions θ1 = %s, θ2 = %s" (showFix θ1) (showFix θ2)


safeMkSubst θ
  | nub θ == θ
  = Su θ
  | otherwise
  = errorstar msg
  where
    msg = printf "Fixpoint.Types mkSubst on overlapping substitution θ = %s" (showFix θ)

instance Monoid Subst where
  mempty  = emptySubst
  mappend = catSubst

------------------------------------------------------------
------------- Generally Useful Refinements -----------------
------------------------------------------------------------

symbolReft    :: (Symbolic a) => a -> Reft
symbolReft    = exprReft . eVar

usymbolReft   :: (Symbolic a) => a -> Reft
usymbolReft   = uexprReft . eVar

vv_ :: Symbol
vv_ = vv Nothing

trueSortedReft :: Sort -> SortedReft
trueSortedReft = (`RR` trueReft)

trueReft  = Reft (vv_, trueRefa)
falseReft = Reft (vv_, Refa PFalse)

trueRefa  :: Refa
trueRefa  = Refa PTrue

flattenRefas ::  [Refa] -> [Refa]
flattenRefas         = concatMap flatRa
  where
    flatRa (Refa p)  = Refa <$> flatP p
    flatRa ra        = [ra]
    flatP  (PAnd ps) = concatMap flatP ps
    flatP  p         = [p]

squishRefas     :: [Refa] -> [Refa]
squishRefas ras =  [squish (raPred <$> ras)]
  where
    squish      = Refa . pAnd . sortNub . filter (not . isTautoPred) . concatMap conjuncts

conjuncts (PAnd ps) = concatMap conjuncts ps
conjuncts p
  | isTautoPred p   = []
  | otherwise       = [p]

----------------------------------------------------------------
---------------------- Strictness ------------------------------
----------------------------------------------------------------

instance NFData FTycon where
  rnf (TC c)       = rnf c

instance NFData Sort where
  rnf (FVar x)     = rnf x
  rnf (FFunc n ts) = rnf n `seq` (rnf <$> ts) `seq` ()
  rnf (FApp c ts)  = rnf c `seq` (rnf <$> ts) `seq` ()
  rnf (z)          = z `seq` ()

instance NFData Sub where
  rnf (Sub x) = rnf x

instance NFData Subst where
  rnf (Su x) = rnf x

instance NFData FEnv where
  rnf (SE x) = rnf x

instance NFData IBindEnv where
  rnf (FB x) = rnf x

instance NFData BindEnv where
  rnf (BE x m) = rnf x `seq` rnf m

instance NFData Constant where
  rnf (I x)     = rnf x
  rnf (R x)     = rnf x
  rnf (L s t) = rnf s `seq` rnf t

instance NFData SymConst where
  rnf (SL x) = rnf x

instance NFData Brel
instance NFData Bop

instance NFData Expr where
  rnf (ESym x)        = rnf x
  rnf (ECon x)        = rnf x
  rnf (EVar x)        = rnf x
  -- rnf (EDat x1 x2)    = rnf x1 `seq` rnf x2
  rnf (ELit x1 x2)    = rnf x1 `seq` rnf x2
  rnf (EApp x1 x2)    = rnf x1 `seq` rnf x2
  rnf (ENeg x1)       = rnf x1
  rnf (EBin x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3
  rnf (EIte x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3
  rnf (ECst x1 x2)    = rnf x1 `seq` rnf x2
  rnf (_)             = ()

instance NFData Pred where
  rnf (PAnd x)         = rnf x
  rnf (POr  x)         = rnf x
  rnf (PNot x)         = rnf x
  rnf (PBexp x)        = rnf x
  rnf (PImp x1 x2)     = rnf x1 `seq` rnf x2
  rnf (PIff x1 x2)     = rnf x1 `seq` rnf x2
  rnf (PAll x1 x2)     = rnf x1 `seq` rnf x2
  rnf (PAtom x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3
  rnf (_)              = ()

instance NFData Refa where
  rnf (Refa x)     = rnf x
  -- rnf (RKvar x1 x2) = rnf x1 `seq` rnf x2
  -- rnf (RPvar _)     = () -- rnf x

instance NFData Reft where
  rnf (Reft (v, ras)) = rnf v `seq` rnf ras

instance NFData SortedReft where
  rnf (RR so r) = rnf so `seq` rnf r

instance (NFData a) => NFData (SubC a) where
  rnf (SubC x1 x2 x3 x4 x5 x6 x7)
    = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7

instance (NFData a) => NFData (WfC a) where
  rnf (WfC x1 x2 x3 x4)
    = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4

----------------------------------------------------------------------------
-------------- Hashable Instances -----------------------------------------
---------------------------------------------------------------------------

instance Hashable FTycon where
  hashWithSalt i (TC s) = hashWithSalt i s

---------------------------------------------------------------------------
-------- Constraint Constructor Wrappers ----------------------------------
---------------------------------------------------------------------------

wfC  :: IBindEnv -> SortedReft -> Maybe Integer -> a -> WfC a
wfC  = WfC

-- subC :: IBindEnv -> Pred -> SortedReft -> SortedReft -> Maybe Integer -> Tag -> a -> [SubC a]
-- subC γ p (RR t1 r1) (RR t2 (Reft (v2, ra2s))) i y z
--   = error "TODO:subC" -- NEW [subC' r2' | r2' <- [r2P], not $ isTauto r2']
--   where
--     subC' r2'  = SubC γ p (RR t1 (shiftVV r1 vv')) (RR t2 (shiftVV r2' vv')) i y z
--     r2P        = Reft (v2, ra2s) -- ORIG [ra | ra@(Refa _  ) <- ra2s])
--     -- ORIG r2K        = Reft (v2, [ra | ra@(RKvar _ _) <- ra2s])
--     vv'        = mkVV i


-- ORIG subC γ p (RR t1 r1) (RR t2 (Reft (v2, ra2s))) x y z
-- ORIG   = [subC' r2' | r2' <- [r2K, r2P], not $ isTauto r2']
-- ORIG   where
-- ORIG     subC' r2'  = SubC γ p (RR t1 (shiftVV r1 vvCon)) (RR t2 (shiftVV r2' vvCon)) x y z
-- ORIG     r2K        = Reft (v2, [ra | ra@(RKvar _ _) <- ra2s])
-- ORIG     r2P        = Reft (v2, [ra | ra@(RConc _  ) <- ra2s])


subC :: IBindEnv -> Pred -> SortedReft -> SortedReft -> Maybe Integer -> Tag -> a -> [SubC a]
-- subC γ p (RR t1 r1) (RR t2 r2) i y z
subC γ p sr1 sr2 i y z = [SubC γ p sr1' (sr2' r2') i y z | r2' <- reftConjuncts r2]
   where
     RR t1 r1          = sr1
     RR t2 r2          = sr2
     sr1'              = RR t1 $ shiftVV r1  vv'
     sr2' r2'          = RR t2 $ shiftVV r2' vv'
     vv'               = mkVV i

reftConjuncts :: Reft -> [Reft]
reftConjuncts (Reft (v, ra)) = [Reft (v, ra') | ra' <- refaConjuncts ra]

refaConjuncts :: Refa -> [Refa]
refaConjuncts (Refa p)       = [Refa p' | p' <- conjuncts p, not $ isTautoPred p']

mkVV :: Maybe Integer -> Symbol
mkVV (Just i)  = vv $ Just i
mkVV Nothing   = vvCon

lhsCs, rhsCs :: SubC a -> Reft
lhsCs      = sr_reft . slhs
rhsCs      = sr_reft . srhs

envCs :: BindEnv -> IBindEnv -> [(Symbol, SortedReft)]
envCs be env = [lookupBindEnv i be | i <- elemsIBindEnv env]

-- mkFEnv :: BindEnv -> IBindEnv -> FEnv
-- mkFEnv be env = fromListSEnv $ envCs be env



removeLhsKvars cs vs
  = error "TODO:cutsolver: removeLhsKvars (why is this function needed?)"

-- CUTSOLVER   = cs {slhs = goRR (slhs cs)}
-- CUTSOLVER  where goRR rr                     = rr{sr_reft = goReft (sr_reft rr)}
-- CUTSOLVER        goReft (Reft(v, rs))        = Reft(v, filter f rs)
-- CUTSOLVER        f (RKvar v _) | v `elem` vs = False
-- CUTSOLVER        f r                         = True

trueSubCKvar k = subC emptyIBindEnv PTrue mempty rhs  Nothing [0]
  where
    rhs        = RR mempty (Reft (vv_, Refa $ PKVar k mempty))

shiftVV :: Reft -> Symbol -> Reft
shiftVV r@(Reft (v, ras)) v'
   | v == v'   = r
   | otherwise = Reft (v', subst1 ras (v, EVar v'))


addIds = zipWith (\i c -> (i, shiftId i $ c {sid = Just i})) [1..]
  where -- Adding shiftId to have distinct VV for SMT conversion
    shiftId i c = c { slhs = shiftSR i $ slhs c }
                    { srhs = shiftSR i $ srhs c }
    shiftSR i sr = sr { sr_reft = shiftR i $ sr_reft sr }
    shiftR i r@(Reft (v, _)) = shiftVV r (v `mappend` symbol (show i))


------------------------------------------------------------------------
----------------- Qualifiers -------------------------------------------
------------------------------------------------------------------------


data Qualifier = Q { q_name   :: Symbol           -- ^ Name
                   , q_params :: [(Symbol, Sort)] -- ^ Parameters
                   , q_body   :: Pred             -- ^ Predicate
                   , q_pos    :: !SourcePos       -- ^ Source Location
                   }
               deriving (Eq, Ord, Show, Data, Typeable, Generic)

instance Fixpoint Qualifier where
  toFix = pprQual

instance NFData Qualifier where
  rnf (Q x1 x2 x3 _) = rnf x1 `seq` rnf x2 `seq` rnf x3

pprQual (Q n xts p l) = text "qualif" <+> text (symbolString n) <> parens args <> colon <+> toFix p <+> text "//" <+> toFix l
  where
    args              = intersperse comma (toFix <$> xts)

------------------------------------------------------------------------
----------------- Top-Level Constraint System --------------------------
------------------------------------------------------------------------

data FInfo a = FI { cm    :: M.HashMap Integer (SubC a)
                  , ws    :: ![WfC a]
                  , bs    :: !BindEnv
                  , gs    :: !FEnv
                  , lits  :: ![(Symbol, Sort)]
                  , kuts  :: Kuts
                  , quals :: ![Qualifier]
                  }
               deriving (Show)

instance Monoid Kuts where
  mempty        = KS S.empty
  mappend k1 k2 = KS $ S.union (ksVars k1) (ksVars k2)

instance Monoid (SEnv a) where
  mempty        = SE M.empty
  mappend s1 s2 = SE $ M.union (seBinds s1) (seBinds s2)

instance Monoid BindEnv where
  mempty = BE 0 M.empty
  mappend (BE 0 _) b = b
  mappend b (BE 0 _) = b
  mappend _ _        = errorstar "mappend on non-trivial BindEnvs"

instance Monoid (FInfo a) where
  mempty        = FI M.empty mempty mempty mempty mempty mempty mempty
  mappend i1 i2 = FI { cm    = mappend (cm i1)    (cm i2)
                     , ws    = mappend (ws i1)    (ws i2)
                     , bs    = mappend (bs i1)    (bs i2)
                     , gs    = mappend (gs i1)    (gs i2)
                     , lits  = mappend (lits i1)  (lits i2)
                     , kuts  = mappend (kuts i1)  (kuts i2)
                     , quals = mappend (quals i1) (quals i2)
                     }

toFixpoint x' = kutsDoc x' $+$ gsDoc x' $+$ conDoc x' $+$ bindsDoc x' $+$ csDoc x' $+$ wsDoc x'
  where
    conDoc    = vcat     . map toFixConstant . lits
    csDoc     = vcat     . map toFix . M.elems . cm
    wsDoc     = vcat     . map toFix . ws
    kutsDoc   = toFix    . kuts
    bindsDoc  = toFix    . bs
    gsDoc     = toFixGs  . gs

-------------------------------------------------------------------------
-- | A Class Predicates for Valid Refinements Types ---------------------
-------------------------------------------------------------------------

class (Monoid r, Subable r) => Reftable r where
  isTauto :: r -> Bool
  ppTy    :: r -> Doc -> Doc

  top     :: r -> r
  top _   =  mempty

  bot     :: r -> r

  meet    :: r -> r -> r
  meet    = mappend

  toReft  :: r -> Reft
  ofReft  :: Reft -> r
  params  :: r -> [Symbol]          -- ^ parameters for Reft, vv + others

instance Monoid Pred where
  mempty      = PTrue
  mappend p q = pAnd [p, q]
  mconcat     = pAnd

instance Monoid Refa where
  mempty          = Refa mempty
  mappend ra1 ra2 = Refa $ mappend (raPred ra1) (raPred ra2)

instance Monoid Reft where
  mempty  = trueReft
  mappend = meetReft

meetReft (Reft (v, ra)) (Reft (v', ra'))
  | v == v'          = Reft (v , ra  `mappend` ra')
  | v == dummySymbol = Reft (v', ra' `mappend` (ra `subst1`  (v , EVar v')))
  | otherwise        = Reft (v , ra  `mappend` (ra' `subst1` (v', EVar v )))

instance Subable () where
  syms _      = []
  subst _ ()  = ()
  substf _ () = ()
  substa _ () = ()

instance Reftable () where
  isTauto _ = True
  ppTy _  d = d
  top  _    = ()
  bot  _    = ()
  meet _ _  = ()
  toReft _  = mempty
  ofReft _  = mempty
  params _  = []

-- NUKE isTautoReft :: Reft -> Bool
-- NUKE isTautoReft (Reft (_, ra)) = isTautoRa ra
-- NUKE
-- NUKE isTautoRa :: Refa -> Bool
-- NUKE isTautoRa = isTautoPred . raPred


instance Reftable Reft where
  isTauto  = all isTautoPred . conjuncts . reftPred
  ppTy     = pprReft
  toReft   = id
  ofReft   = id
  params _ = []

  bot    _        = falseReft
  top (Reft(v,_)) = Reft (v, mempty)

instance Monoid Sort where
  mempty            = FObj "any"
  mappend t1 t2
    | t1 == mempty  = t2
    | t2 == mempty  = t1
    | t1 == t2      = t1
    | otherwise     = errorstar $ "mappend-sort: conflicting sorts t1 =" ++ show t1 ++ " t2 = " ++ show t2

instance Monoid SortedReft where
  mempty        = RR mempty mempty
  mappend t1 t2 = RR (mappend (sr_sort t1) (sr_sort t2)) (mappend (sr_reft t1) (sr_reft t2))

instance Reftable SortedReft where
  isTauto  = isTauto . toReft
  ppTy     = ppTy . toReft
  toReft   = sr_reft
  ofReft   = error "No instance of ofReft for SortedReft"
  params _ = []
  bot s    = s { sr_reft = falseReft }

class Falseable a where
  isFalse :: a -> Bool

instance Falseable Pred where
  isFalse (PFalse) = True
  isFalse _        = False

instance Falseable Refa where
  isFalse (Refa p) = isFalse p

instance Falseable Reft where
  isFalse (Reft(_, (Refa p))) = isFalse p

---------------------------------------------------------------
-- | String Constants -----------------------------------------
---------------------------------------------------------------

symConstLits    :: FInfo a -> [(Symbol, Sort)]
symConstLits fi = [(encodeSymConst c, sortSymConst c) | c <- symConsts fi]

-- | Replace all symbol-representations-of-string-literals with string-literal
--   Used to transform parsed output from fixpoint back into fq.


instance Symbolic SymConst where
  symbol = encodeSymConst

encodeSymConst        :: SymConst -> Symbol
encodeSymConst (SL s) = symbol $ litPrefix `mappend` s

sortSymConst          :: SymConst -> Sort
sortSymConst (SL _)   = strSort

decodeSymConst :: Symbol -> Maybe SymConst
decodeSymConst = fmap SL . T.stripPrefix litPrefix . symbolText

litPrefix    :: Text
litPrefix    = "lit" `T.snoc` symSepName

strSort      :: Sort
strSort      = FInt 

class SymConsts a where
  symConsts :: a -> [SymConst]

instance SymConsts (FInfo a) where
  symConsts fi = sortNub $ csLits ++ bsLits ++ gsLits ++ qsLits
    where
      csLits   = concatMap symConsts                     $ M.elems  $  cm    fi
      bsLits   = concatMap symConsts $ map snd $ M.elems $ beBinds $  bs    fi
      gsLits   = concatMap symConsts $           M.elems $ seBinds $  gs    fi
      qsLits   = concatMap symConsts $                     q_body  <$> quals fi

instance SymConsts (SubC a) where
  symConsts c  = symConsts (sgrd c) ++
                 symConsts (slhs c) ++
                 symConsts (srhs c)

instance SymConsts SortedReft where
  symConsts = symConsts . sr_reft

instance SymConsts Reft where
  symConsts (Reft (_, ra)) = symConsts ra

instance SymConsts Refa where
  symConsts (Refa p)           = symConsts p

instance SymConsts Expr where
  symConsts (ESym c)       = [c]
  symConsts (EApp _ es)    = concatMap symConsts es
  symConsts (ENeg e)       = symConsts e
  symConsts (EBin _ e e')  = concatMap symConsts [e, e']
  symConsts (EIte p e e')  = symConsts p ++ concatMap symConsts [e, e']
  symConsts (ECst e _)     = symConsts e
  symConsts _              = []

instance SymConsts Pred where
  symConsts (PNot p)           = symConsts p
  symConsts (PAnd ps)          = concatMap symConsts ps
  symConsts (POr ps)           = concatMap symConsts ps
  symConsts (PImp p q)         = concatMap symConsts [p, q]
  symConsts (PIff p q)         = concatMap symConsts [p, q]
  symConsts (PAll _ p)         = symConsts p
  symConsts (PBexp e)          = symConsts e
  symConsts (PAtom _ e e')     = concatMap symConsts [e, e']
  symConsts (PKVar _ (Su xes)) = concatMap symConsts $ snd <$> xes
  symConsts _                  = []

---------------------------------------------------------------
-- | Edit Distance --------------------------------------------
---------------------------------------------------------------


editDistance :: Eq a => [a] -> [a] -> Int
editDistance xs ys = table ! (m,n)
    where
    (m,n) = (length xs, length ys)
    x     = array (1,m) (zip [1..] xs)
    y     = array (1,n) (zip [1..] ys)

    table :: Array (Int,Int) Int
    table = array bnds [(ij, dist ij) | ij <- range bnds]
    bnds  = ((0,0),(m,n))

    dist (0,j) = j
    dist (i,0) = i
    dist (i,j) = minimum [table ! (i-1,j) + 1, table ! (i,j-1) + 1,
        if x ! i == y ! j then table ! (i-1,j-1) else 1 + table ! (i-1,j-1)]


-----------------------------------------------------------------------------
-- | Located Values ---------------------------------------------------------
-----------------------------------------------------------------------------

data Located a = Loc { loc  :: !SourcePos -- ^ Start Position
                     , locE :: !SourcePos -- ^ End Position
                     , val  :: a
                     } deriving (Data, Typeable, Generic)

instance (IsString a) => IsString (Located a) where
  fromString = dummyLoc . fromString

type LocSymbol = Located Symbol
type LocText   = Located Text

dummyLoc :: a -> Located a
dummyLoc = Loc l l where l = dummyPos "Fixpoint.Types.dummyLoc"

dummyPos   :: String -> SourcePos
dummyPos s = newPos s 0 0

isDummy :: (Symbolic a) => a -> Bool
isDummy a = symbol a == symbol dummyName

instance Fixpoint SourcePos where
  toFix = text . show

instance Fixpoint a => Fixpoint (Located a) where
  toFix = toFix . val

instance Symbolic a => Symbolic (Located a) where
  symbol = symbol . val

instance Expression a => Expression (Located a) where
  expr   = expr . val

instance Functor Located where
  fmap f (Loc l l' x) =  Loc l l' (f x)

instance F.Foldable Located where
  foldMap f (Loc _ _ x) = f x

instance Traversable Located where
  traverse f (Loc l l' x) = Loc l l' <$> f x

instance Show a => Show (Located a) where
  show (Loc l l' x) = show x ++ " defined from: " ++ show l ++ " to: " ++ show l'

instance Eq a => Eq (Located a) where
  (Loc _ _ x) == (Loc _ _ y) = x == y

instance Ord a => Ord (Located a) where
  compare x y = compare (val x) (val y)

instance Subable a => Subable (Located a) where
  syms (Loc _ _ x)   = syms x
  substa f (Loc l l' x) = Loc l l' (substa f x)
  substf f (Loc l l' x) = Loc l l' (substf f x)
  subst su (Loc l l' x) = Loc l l' (subst su x)

instance Hashable a => Hashable (Located a) where
  hashWithSalt i = hashWithSalt i . val

instance (NFData a) => NFData (Located a) where
  -- FIXME: no instance NFData SrcSpan
  rnf (Loc _ _  x) = rnf x