liquidtypes-0.1: Liquid Types for Haskell

Safe HaskellSafe-Infered

Language.Haskell.Liquid.Fixpoint

Contents

Description

This module contains the data types, operations and serialization functions for representing Fixpoint's implication (i.e. subtyping) and well-formedness constraints in Haskell. The actual constraint solving is done by the `fixpoint.native` which is written in Ocaml.

Synopsis

Top level serialization

Embedding to Fixpoint Types

data Sort Source

Constructors

FInt 
FNum

numeric kind for Num tyvars

FObj Symbol

uninterpreted type

FVar !Int

fixpoint type variable

FFunc !Int ![Sort]

type-var arity, in-ts ++ [out-t]

FApp FTycon [Sort]

constructed type

type TCEmb a = HashMap a FTyconSource

Symbols

intSymbol :: Show a => [Char] -> a -> SymbolSource

Expressions and Predicates

data Bop Source

Constructors

Plus 
Minus 
Times 
Div 
Mod 

data Brel Source

Constructors

Eq 
Ne 
Gt 
Ge 
Lt 
Le 

Constraints and Solutions

data SubC a Source

Instances

data WfC a Source

Instances

NFData a => NFData (WfC a) 
Outputable (WfC a) 
Fixpoint (WfC a) 

type Tag = [Int]Source

data FInfo a Source

Constructors

FI 

Fields

cs :: ![SubC a]
 
ws :: ![WfC a]
 
bs :: !BindEnv
 
gs :: !FEnv
 
lits :: ![(Symbol, Sort)]
 
kuts :: Kuts
 

addIds :: [SubC a] -> [(Integer, SubC a)]Source

sinfo :: SubC a -> aSource

Environments

data SEnv a Source

Instances

insertSEnv :: Symbol -> a -> SEnv a -> SEnv aSource

insertFEnv :: Symbol -> a -> SEnv a -> SEnv aSource

emptyIBindEnv :: IBindEnvSource

Functions for Indexed Bind Environment

insertBindEnv :: Symbol -> SortedReft -> BindEnv -> (Int, BindEnv)Source

Functions for Global Binder Environment

Refinements

data Refa Source

Constructors

RConc !Pred 
RKvar !Symbol !Subst 

Instances

newtype Reft Source

Constructors

Reft (Symbol, [Refa]) 

Substitutions

class Subable a whereSource

Methods

syms :: a -> [Symbol]Source

substa :: (Symbol -> Symbol) -> a -> aSource

substf :: (Symbol -> Expr) -> a -> aSource

subst :: Subst -> a -> aSource

subst1 :: a -> (Symbol, Expr) -> aSource

Instances

subst1Except :: Subable a => [Symbol] -> a -> (Symbol, Expr) -> aSource

Visitors

Functions on Result

Cut KVars

newtype Kuts Source

Constructors

KS (HashSet Symbol) 

Checking Well-Formedness