Language.Nano.Types

Contents

• Configuration Options
• Some Operators on Pred
• Nano Definition
• Located Values
• Accessing Spec Annotations
• Error message
• Deconstructing Id

Synopsis

• data Config
  • = Esc {
    • files :: [FilePath]
    • incdirs :: [FilePath]
    }
  • | TC {
    • files :: [FilePath]
    • incdirs :: [FilePath]
    }
  • | Liquid {
    • files :: [FilePath]
    • incdirs :: [FilePath]
    }
• pAnd :: Pred -> Pred -> Pred
• pOr :: Pred -> Pred -> Pred
• class IsNano a where
  • isNano :: a -> Bool
• checkTopStmt :: Statement SourcePos -> Statement SourcePos
• data Located a = Loc {
  • loc :: !SourcePos
  • val :: a
  }
• class IsLocated a where
  • srcPos :: a -> SourcePos
• getSpec :: (Statement a -> Maybe Pred) -> [Statement a] -> Pred
• getRequires :: Statement a -> Maybe Pred
• getEnsures :: Statement a -> Maybe Pred
• getAssume :: Statement a -> Maybe Pred
• getAssert :: Statement a -> Maybe Pred
• getInvariant :: Statement a -> Pred
• isSpecification :: Statement a -> Bool
• returnSymbol :: Symbol
• returnId :: a -> Id a
• symbolId :: (IsLocated l, Symbolic x) => l -> x -> Id l
• mkId :: String -> Id SourcePos
• convertError :: PP a => [Char] -> a -> c
• idName :: Id t -> String
• idLoc :: Id t -> t

Configuration Options

Some Operators on Pred

Nano Definition

Located Values

Accessing Spec Annotations

Error message

Deconstructing Id