module Gradual.Concretize (Gradual(..)) where
import Gradual.Types
import Language.Fixpoint.Types
import Gradual.Misc
import qualified Data.HashMap.Strict as M
class Gradual a where
concretize :: GMap GWInfo -> a -> [(GSub GWInfo, a)]
concretize _ x = [(mempty, x)]
instance Gradual (SInfo a) where
concretize i sinfo = (\su -> (su,
sinfo {bs = gsubst (bs sinfo,su) (bs sinfo), cm = gsubst (bs sinfo,su) (cm sinfo)}
)) <$> (M.fromList <$> flatten (M.toList i))
class GSubable a where
gsubst :: (BindEnv, GSub GWInfo) -> a -> a
gsubst _ x = x
instance GSubable BindEnv where
gsubst i benv = bindEnvFromList (mapThd3 (gsubst i) <$> bindEnvToList benv)
instance GSubable (SimpC a) where
gsubst (benv,i) c = c {_crhs = substGrad x i (_crhs c)}
where
x = fst $ lookupBindEnv (_cbind c) benv
instance (GSubable v) => GSubable (M.HashMap SubcId v) where
gsubst i m = M.map (gsubst i) m
instance GSubable SortedReft where
gsubst i (RR s r) = RR s $ gsubst i r
instance GSubable Reft where
gsubst (_,i) (Reft (x,p)) = Reft . (x,) $ substGrad x i p
substGrad :: Symbol -> GSub GWInfo -> Expr -> Expr
substGrad x m (PGrad k su _ e)
= case M.lookup k m of
Just (i, ek) -> pAnd [subst su $ subst1 ek (gsym i, EVar x), e]
Nothing -> PTrue
substGrad x m (PAnd es)
= PAnd (substGrad x m <$> es)
substGrad _ _ e
= e