Language.Haskell.Liquid.Synthesize.Monad

Documentation

localMaxMatchDepth :: SM Int

type SSEnv = HashMap Symbol (SpecType, Var)

Synthesis Monad ----------------------------------------------------------

type SSDecrTerm = [(Var, [Var])]

type ExprMemory = [(Type, CoreExpr, Int)]

type T = HashMap Type (CoreExpr, Int)

data SState

Constructors

SState

Fields

• rEnv :: !REnv
• ssEnv :: !SSEnv
• ssIdx :: !Int
• ssDecrTerm :: !SSDecrTerm
• sContext :: !Context
• sCGI :: !CGInfo
• sCGEnv :: !CGEnv
• sFCfg :: !Config
• sDepth :: !Int
• sExprMem :: !ExprMemory
• sExprId :: !Int
• sArgsId :: !Int
• sArgsDepth :: !Int
• sUniVars :: ![Var]
• sFix :: !Var
• sGoalTys :: ![Type]
• sGoalTyVar :: !(Maybe [TyVar])
• sUGoalTy :: !(Maybe [Type])
• sForalls :: !([Var], [[Type]])
• caseIdx :: !Int
• scrutinees :: ![(CoreExpr, Type, TyCon)]

type SM = StateT SState IO

localMaxAppDepth :: SM Int

localMaxArgsDepth :: SM Int

locally :: SM a -> SM a

evalSM :: SM a -> Context -> SSEnv -> SState -> IO a

initState :: Context -> Config -> CGInfo -> CGEnv -> REnv -> Var -> [Var] -> SSEnv -> IO SState

getSEnv :: SM SSEnv

getSEMem :: SM ExprMemory

getSFix :: SM Var

getSUniVars :: SM [Var]

getSDecrTerms :: SM SSDecrTerm

addsEnv :: [(Var, SpecType)] -> SM ()

addsEmem :: [(Var, SpecType)] -> SM ()

addEnv :: Var -> SpecType -> SM ()

addEmem :: Var -> SpecType -> SM ()

addDecrTerm :: Var -> [Var] -> SM ()

lookupAll :: Var -> [Var] -> SSDecrTerm -> SM ()

thisReplace :: Int -> a -> [a] -> [a]

structuralCheck :: [CoreExpr] -> SM [CoreExpr]

Entry point.

structCheck :: Var -> CoreExpr -> (Maybe Var, [CoreExpr])

notStructural :: SSDecrTerm -> Var -> CoreExpr -> Bool

isDecreasing' :: CoreExpr -> SSDecrTerm -> Bool

liftCG0 :: (CGEnv -> CG CGEnv) -> SM ()

liftCG :: CG a -> SM a

freshVarType :: Type -> SM Var

freshVar :: SpecType -> SM Var

withIncrDepth :: Monoid a => SM a -> SM a

incrSM :: SM Int

incrCase :: SM Int

safeIxScruts :: Int -> [a] -> Maybe Int

symbolExpr :: Type -> Symbol -> SM CoreExpr

initExprMem :: SSEnv -> ExprMemory

Initializes ExprMemory structure. 1. Transforms refinement types to conventional (Haskell) types. 2. All Depths are initialized to 0.

insEMem0 :: SSEnv -> SM ExprMemory

instantiateTy :: CoreExpr -> Maybe [Type] -> CoreExpr

applyTy :: [Type] -> CoreExpr -> Maybe CoreExpr

Used for instantiation: Applies types to an expression. > The result does not have forall. Nothing as a result suggests that there are more types than foralls in the expression.

fixEMem :: SpecType -> SM ()

Instantiation based on current goal-type.

instantiateTL :: SM (Type, CoreExpr)

Instantiate the top-level variable.

apply :: [Var] -> CoreExpr -> Maybe CoreExpr

Applies type variables (1st argument) to an expression. The expression is guaranteed to have the same level of parametricity (same number of forall) as the length of the 1st argument. > The result has zero forall.

instantiate :: CoreExpr -> Maybe [Var] -> CoreExpr

withTypeEs :: SpecType -> SM [CoreExpr]

findCandidates :: Type -> SM ExprMemory

functionCands :: Type -> SM [(Type, CoreExpr, Int)]

varError :: SM Var

toGhcSrc :: TargetSrc -> GhcSrc