Language.Nano.Liquid.CGMonad

Contents

• Constraint Generation Monad
• Execute Action and Get FInfo
• Get Defined Function Type Signature
• Throw Errors
• Fresh Templates for Unknown Refinement Types
• Environment API
• Add Subtyping Constraints

Description

Synopsis

• type CGM = ErrorT String (State CGState)
• getFInfo :: NanoRefType -> CGM a -> FInfo Cinfo
• getDefType :: (PP a, Symbolic a, IsLocated a) => a -> ErrorT String (State CGState) RefType
• cgError :: IsLocated l => l -> String -> CGM a
• freshTyFun :: IsLocated l => CGEnv -> l -> RefType -> CGM RefType
• freshTyInst :: IsLocated l => l -> CGEnv -> [TVar] -> [Type] -> RefType -> CGM RefType
• freshTyPhis :: IsLocated l => l -> CGEnv -> [Id l] -> [Type] -> CGM (CGEnv, [RefType])
• envAddFresh :: IsLocated l => l -> RefType -> CGEnv -> CGM (Id l, CGEnv)
• envAdds :: (Symbolic x, IsLocated x) => [(x, RefType)] -> CGEnv -> CGM CGEnv
• envAddReturn :: IsLocated f => f -> RefType -> CGEnv -> CGEnv
• envAddGuard :: (Symbolic x, IsLocated x) => x -> Bool -> CGEnv -> CGEnv
• envFindTy :: (IsLocated x, Symbolic x, Expression x) => x -> CGEnv -> RefType
• envFindReturn :: CGEnv -> RefType
• subTypes :: (IsLocated l, IsLocated x, Expression x, Symbolic x) => l -> CGEnv -> [x] -> [RefType] -> CGM ()
• subType :: IsLocated l => l -> CGEnv -> RefType -> RefType -> CGM ()

Constraint Generation Monad

Execute Action and Get FInfo

Get Defined Function Type Signature

Throw Errors

Fresh Templates for Unknown Refinement Types

Environment API

Add Subtyping Constraints