liquid-fixpoint-0.4.0.0: src/Language/Fixpoint/Types.hs
{-# 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
, sortFTycon
, intFTyCon, boolFTyCon, realFTyCon -- TODO: hide these
-- , strFTyCon
-- , propFTyCon
, intSort, realSort, propSort, boolSort, strSort
, listFTyCon, appFTyCon
, isListTC, isFAppTyTC
, fTyconSymbol, symbolFTycon, fTyconSort
, fApp
, fObj
-- * 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, subcId, 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
, mapSEnvWithKey
, insertSEnv, deleteSEnv, memberSEnv, lookupSEnv
, intersectWithSEnv
, filterSEnv
, lookupSEnvWithDistance
, FEnv, insertFEnv
, IBindEnv, BindId, BindMap
, emptyIBindEnv, insertsIBindEnv, deleteIBindEnv, elemsIBindEnv
, BindEnv, beBinds
, insertBindEnv, emptyBindEnv, lookupBindEnv, mapBindEnv, adjustBindEnv
, bindEnvFromList, bindEnvToList
, unionIBindEnv
-- * Refinements
, Refa (..), SortedReft (..), Reft(..), Reftable(..)
, raConjuncts
-- * 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 (..)
-- * Located Values
, Located (..)
, LocSymbol, LocText
, locAt, 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.Config
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
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)
instance (Fixpoint a, Fixpoint b, Fixpoint c) => Fixpoint (a,b,c) where
toFix (x,y,z) = toFix x <+> text ":" <+> toFix y <+> text ":" <+> toFix z
simplify (x,y,z) = (simplify x, simplify y,simplify z)
instance Fixpoint Bool where
toFix True = text "True"
toFix False = text "False"
simplify z = z
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
sortFTycon :: Sort -> Maybe FTycon
sortFTycon FInt = Just intFTyCon
sortFTycon FReal = Just realFTyCon
sortFTycon (FApp c _) = Just c
sortFTycon _ = Nothing
----------------------------------------------------------------------
------------------------------- 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 $ text "if" <+> toFix p <+> text "then" <+> toFix e1 <+> text "else" <+> toFix e2
toFix (ECst e so) = parens $ toFix e <+> text " : " <+> toFix so
toFix (EBot) = text "_|_"
----------------------------------------------------------
--------------------- Predicates -------------------------
----------------------------------------------------------
data Pred = PTrue
| PFalse
| PAnd !(ListNE Pred) -- [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)
{-@ 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) $ raConjuncts ra
raConjuncts :: Refa -> [Pred]
raConjuncts = conjuncts . raPred
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
adjustBindEnv :: ((Symbol, SortedReft) -> (Symbol, SortedReft)) -> BindId -> BindEnv -> BindEnv
adjustBindEnv f id (BE n m) = BE n $ M.adjust f id m
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)
subcId :: SubC a -> Integer
subcId = mfromJust "subCId" . sid
---------------------------------------------------------------------------
-- | The output of the Solver
---------------------------------------------------------------------------
data Result a = Result { resStatus :: FixResult (SubC a)
, resSolution :: M.HashMap KVar Pred }
deriving (Show)
---------------------------------------------------------------------------
instance Monoid (Result a) where
mempty = Result mempty mempty
mappend r1 r2 = Result stat soln
where
stat = mappend (resStatus r1) (resStatus r2)
soln = mappend (resSolution r1) (resSolution r2)
-- instance Functor Result where
-- fmap f (Result x y) = Result (fmap (fmap f) x) y
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 :: FixResult a -> Moods
colorResult (Safe) = Happy
colorResult (Unsafe _) = Angry
colorResult (_) = Sad
instance Fixpoint a => Show (WfC a) where
show = showFix
instance Fixpoint a => Show (SubC a) where
show = showFix
instance Fixpoint (IBindEnv) where
toFix (FB ids) = text "env" <+> toFix ids
instance Fixpoint a => 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))
$+$ toFixMeta (text "constraint" <+> pprId (sid c)) (toFix (sinfo c))
instance Fixpoint a => 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)
$+$ toFixMeta (text "wf" <+> pprId (wid w)) (toFix (winfo w))
toFixMeta :: Doc -> Doc -> Doc
toFixMeta k v = text "// META" <+> k <+> text ":" <+> v
-- $+$ text "\n"
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
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 Fixpoint () where
toFix _ = text "()"
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]
, bindInfo :: M.HashMap BindId a
}
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 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)
, bindInfo = mappend (bindInfo i1) (bindInfo i2)
}
($++$) :: Doc -> Doc -> Doc
x $++$ y = x $+$ text "\n" $+$ y
toFixpoint :: (Fixpoint a) => Config -> FInfo a -> Doc
toFixpoint cfg x' = qualsDoc x'
$++$ kutsDoc x'
$++$ gsDoc x'
$++$ conDoc x'
$++$ bindsDoc x'
$++$ csDoc x'
$++$ wsDoc x'
$++$ binfoDoc x'
$++$ text "\n"
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
qualsDoc = vcat . map toFix . quals
metaDoc (i,d) = toFixMeta (text "bind" <+> toFix i) (toFix d)
mdata = metadata cfg
binfoDoc
| mdata = vcat . map metaDoc . M.toList . bindInfo
| otherwise = \_ -> text "\n"
-------------------------------------------------------------------------
-- | 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 (_, ra)) = isFalse $ raPred ra
---------------------------------------------------------------
-- | 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
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
locAt :: String -> a -> Located a
locAt s = Loc l l
where
l = dummyPos s
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
-------------------------------------------------------------------------
-- | Exported Basic Sorts -----------------------------------------------
-------------------------------------------------------------------------
boolSort, intSort, propSort, realSort, strSort :: Sort
boolSort = fTyconSort boolFTyCon
strSort = fTyconSort strFTyCon
intSort = fTyconSort intFTyCon
realSort = fTyconSort realFTyCon
propSort = fTyconSort propFTyCon
fTyConSort :: FTycon -> Sort
fTyConSort c = fApp (Left c) []