| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
Language.Haskell.Liquid.Synthesize.Monad
Synopsis
- localMaxMatchDepth :: SM Int
- type SSEnv = HashMap Symbol (SpecType, Var)
- type SSDecrTerm = [(Var, [Var])]
- type ExprMemory = [(Type, CoreExpr, Int)]
- type T = HashMap Type (CoreExpr, Int)
- data SState = SState {
- 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]
- 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
- insEMem0 :: SSEnv -> SM ExprMemory
- instantiateTy :: CoreExpr -> Maybe [Type] -> CoreExpr
- applyTy :: [Type] -> CoreExpr -> Maybe CoreExpr
- fixEMem :: SpecType -> SM ()
- instantiateTL :: SM (Type, CoreExpr)
- apply :: [Var] -> CoreExpr -> Maybe CoreExpr
- 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
Documentation
type SSEnv = HashMap Symbol (SpecType, Var) Source #
Synthesis Monad ----------------------------------------------------------
type SSDecrTerm = [(Var, [Var])] Source #
Constructors
| SState | |
Fields
| |
localMaxAppDepth :: SM Int Source #
initState :: Context -> Config -> CGInfo -> CGEnv -> REnv -> Var -> [Var] -> SSEnv -> IO SState Source #
getSEMem :: SM ExprMemory Source #
getSUniVars :: SM [Var] Source #
thisReplace :: Int -> a -> [a] -> [a] Source #
notStructural :: SSDecrTerm -> Var -> CoreExpr -> Bool Source #
isDecreasing' :: CoreExpr -> SSDecrTerm -> Bool Source #
initExprMem :: SSEnv -> ExprMemory Source #
Initializes ExprMemory structure.
1. Transforms refinement types to conventional (Haskell) types.
2. All Depths are initialized to 0.
applyTy :: [Type] -> CoreExpr -> Maybe CoreExpr Source #
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.
apply :: [Var] -> CoreExpr -> Maybe CoreExpr Source #
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.
findCandidates :: Type -> SM ExprMemory Source #