Language.Nano.Liquid.Types

Contents

• Refinement Types and Environments
• Constraint Environments
• Constraint Information
• Constraints
• Conversions
• Manipulating RefType
• Predicates On RefType
• Monadic map (TODO: Applicative/Traversable)
• Primitive Types

Description

Synopsis

• type RefType = RType Reft
• type REnv = Env RefType
• type NanoRefType = Nano AnnType RefType
• data CGEnv = CGE {
  • renv :: !(Env RefType)
  • fenv :: IBindEnv
  • guards :: ![Pred]
  }
• emptyCGEnv :: CGEnv
• newtype Cinfo = Ci SourcePos
• ci :: IsLocated a => a -> Cinfo
• data SubC = Sub {
  • senv :: !CGEnv
  • sinfo :: !Cinfo
  • slhs :: !RefType
  • srhs :: !RefType
  }
• data WfC = W {
  • wenv :: !CGEnv
  • winfo :: !Cinfo
  • wtyp :: !RefType
  }
• type FixSubC = SubC Cinfo
• type FixWfC = WfC Cinfo
• class RefTypable a where
  • rType :: a -> RefType
• eSingleton :: Expression e => RefType -> e -> RefType
• pSingleton :: Predicate p => RefType -> p -> RefType
• rTypeReft :: Reftable r => RType r -> Reft
• rTypeSort :: Reftable r => RType r -> Sort
• rTypeSortedReft :: Reftable r => RType r -> SortedReft
• rTypeValueVar :: Reftable r => RType r -> Symbol
• isBaseRType :: RType r -> Bool
• isTrivialRefType :: RefType -> Bool
• mapReftM :: (Reftable b, Monad m, Applicative m) => (a -> m b) -> RType a -> m (RType b)
• prefixOpRTy :: PrefixOp -> CGEnv -> RefType
• infixOpRTy :: InfixOp -> CGEnv -> RefType

Refinement Types and Environments

Constraint Environments

Constraint Information

Constraints

Conversions

Manipulating RefType

Predicates On RefType

Monadic map (TODO: Applicative/Traversable)

Primitive Types