{-# 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