module Language.Haskell.Liquid.Bare.RefToLogic (
txRefToLogic, Transformable
) where
import Language.Haskell.Liquid.Types
import Language.Haskell.Liquid.Bare.Env
import Language.Fixpoint.Types hiding (Def, R)
import Language.Fixpoint.Misc
import Language.Fixpoint.Names (dropModuleNames)
import qualified Data.HashMap.Strict as M
import Control.Applicative ((<$>))
txRefToLogic :: (Transformable r) => LogicMap -> InlnEnv -> r -> r
txRefToLogic lmap imap t = tx' lmap imap t
class Transformable a where
tx :: Symbol -> (Either LMap TInline) -> a -> a
tx' :: LogicMap -> InlnEnv -> a -> a
tx' lmap imap x = M.foldrWithKey tx x limap
where limap = M.fromList ((mapSnd Left <$> M.toList lmap) ++ (mapSnd Right <$> M.toList imap))
instance (Transformable a) => (Transformable [a]) where
tx s m xs = tx s m <$> xs
instance Transformable DataConP where
tx s m x = x{ tyConsts = tx s m (tyConsts x)
, tyArgs = mapSnd (tx s m) <$> (tyArgs x)
, tyRes = tx s m (tyRes x)
}
instance Transformable TInline where
tx s m (TI xs e) = TI xs (tx s m e)
instance (Transformable r) => Transformable (RType c v r) where
tx s m = fmap (tx s m)
instance Transformable RReft where
tx s m = fmap (tx s m)
instance Transformable Reft where
tx s m (Reft(v, refas))
= if v == s
then errorstar "Transformable: this should not happen"
else Reft(v, tx s m <$> refas)
instance Transformable Refa where
tx s m (RConc p) = RConc $ tx s m p
tx _ _ (RKvar x sub) = RKvar x sub
instance (Transformable a, Transformable b) => Transformable (Either a b) where
tx s m (Left x) = Left (tx s m x)
tx s m (Right x) = Right (tx s m x)
instance Transformable Pred where
tx _ _ PTrue = PTrue
tx _ _ PFalse = PFalse
tx _ _ PTop = PTop
tx s m (PAnd ps) = PAnd (tx s m <$> ps)
tx s m (POr ps) = POr (tx s m <$> ps)
tx s m (PNot p) = PNot (tx s m p)
tx s m (PImp p1 p2) = PImp (tx s m p1) (tx s m p2)
tx s m (PIff p1 p2) = PIff (tx s m p1) (tx s m p2)
tx s m (PBexp (EApp f es)) = txPApp (s, m) f es
tx s m (PBexp e) = PBexp (tx s m e)
tx s m (PAtom r e1 e2) = PAtom r (tx s m e1) (tx s m e2)
tx s m (PAll xss p)
= if (s `elem` (fst <$> xss))
then errorstar "Transformable.tx on Pred: this should not happen"
else PAll xss (tx s m p)
instance Transformable Expr where
tx s m (EVar s')
| cmpSymbol s s' = mexpr m
| otherwise = EVar s'
tx s m (EApp f es) = txEApp (s, m) f es
tx _ _ (ESym c) = ESym c
tx _ _ (ECon c) = ECon c
tx _ _ (ELit l s') = ELit l s'
tx s m (EBin o e1 e2) = EBin o (tx s m e1) (tx s m e2)
tx s m (EIte p e1 e2) = EIte (tx s m p) (tx s m e1) (tx s m e2)
tx s m (ECst e s') = ECst (tx s m e) s'
tx _ _ EBot = EBot
instance Transformable (Measure t c) where
tx s m x = x{eqns = tx s m <$> (eqns x)}
instance Transformable (Def c) where
tx s m x = x{body = tx s m (body x)}
instance Transformable Body where
tx s m (E e) = E $ tx s m e
tx s m (P p) = P $ tx s m p
tx s m (R v p) = R v $ tx s m p
mexpr (Left (LMap _ _ e)) = e
mexpr (Right (TI _ (Right e))) = e
mexpr _ = errorstar "mexpr"
txEApp (s, (Left (LMap _ xs e))) f es
| cmpSymbol s (val f)
= subst (mkSubst $ zip xs es) e
| otherwise
= EApp f es
txEApp (s, (Right (TI xs (Right e)))) f es
| cmpSymbol s (val f)
= subst (mkSubst $ zip xs es) e
| otherwise
= EApp f es
txEApp (s, (Right (TI _ (Left _)))) f es
| cmpSymbol s (val f)
= errorstar "txEApp: deep internal error"
| otherwise
= EApp f es
txPApp (s, (Right (TI xs (Left e)))) f es
| cmpSymbol s (val f)
= subst (mkSubst $ zip xs es) e
| otherwise
= PBexp $ EApp f es
txPApp (s, m) f es = PBexp $ txEApp (s, m) f es
cmpSymbol s1 s2
= (dropModuleNames s1) == s2