Language.Fixpoint.SortCheck

This module has the functions that perform sort-checking, and related operations on Fixpoint expressions and predicates.

Sort Substitutions

data TVSubst

API for manipulating Sort Substitutions -----------------------------------

Instances

Monoid TVSubst

Defined in Language.Fixpoint.SortCheck

Methods

mempty :: TVSubst

mappend :: TVSubst -> TVSubst -> TVSubst

mconcat :: [TVSubst] -> TVSubst

Semigroup TVSubst

Defined in Language.Fixpoint.SortCheck

Methods

(<>) :: TVSubst -> TVSubst -> TVSubst

sconcat :: NonEmpty TVSubst -> TVSubst

stimes :: Integral b => b -> TVSubst -> TVSubst

Show TVSubst

Defined in Language.Fixpoint.SortCheck

Methods

showsPrec :: Int -> TVSubst -> ShowS

show :: TVSubst -> String

showList :: [TVSubst] -> ShowS

type Env = Symbol -> SESearch Sort

mkSearchEnv :: SEnv a -> Symbol -> SESearch a

Checking Well-Formedness

checkSorted :: Checkable a => SrcSpan -> SEnv Sort -> a -> Maybe Doc

checkSortedReft :: SEnv SortedReft -> [Symbol] -> SortedReft -> Maybe Doc

Checking Refinements ------------------------------------------------------

checkSortedReftFull :: Checkable a => SrcSpan -> SEnv SortedReft -> a -> Maybe Doc

checkSortFull :: Checkable a => SrcSpan -> SEnv SortedReft -> Sort -> a -> Maybe Doc

pruneUnsortedReft :: SEnv Sort -> Templates -> SortedReft -> SortedReft

Sort inference

sortExpr :: SrcSpan -> SEnv Sort -> Expr -> Sort

Sort Inference ------------------------------------------------------------

checkSortExpr :: SrcSpan -> SEnv Sort -> Expr -> Maybe Sort

exprSort :: String -> Expr -> Sort

Expressions sort ---------------------------------------------------------

exprSortMaybe :: Expr -> Maybe Sort

Unify

unifyFast :: Bool -> Env -> Sort -> Sort -> Maybe TVSubst

Fast Unification; `unifyFast True` is just equality

unifySorts :: Sort -> Sort -> Maybe TVSubst

unifyTo1 :: Env -> [Sort] -> Maybe Sort

unifys :: HasCallStack => Env -> Maybe Expr -> [Sort] -> [Sort] -> CheckM TVSubst

Apply Substitution

apply :: TVSubst -> Sort -> Sort

Applying a Type Substitution ----------------------------------------------

defuncEApp :: SymEnv -> Expr -> [(Expr, Sort)] -> Expr

defuncEApp monomorphizes function applications.

Exported Sorts

boolSort :: Sort

Exported Basic Sorts -----------------------------------------------

strSort :: Sort

Exported Basic Sorts -----------------------------------------------

Sort-Directed Transformations

class Elaborate a where

Elaborate: make polymorphic instantiation explicit via casts, make applications monomorphic for SMTLIB. This deals with polymorphism by elaborate-ing all refinements except for KVars. THIS IS NOW MANDATORY as sort-variables can be instantiated to int and bool.

Methods

elaborate :: Located String -> SymEnv -> a -> a

Instances

Elaborate AxiomEnv

Defined in Language.Fixpoint.SortCheck

Methods

elaborate :: Located String -> SymEnv -> AxiomEnv -> AxiomEnv

Elaborate Equation

Defined in Language.Fixpoint.SortCheck

Methods

elaborate :: Located String -> SymEnv -> Equation -> Equation

Elaborate Rewrite

Defined in Language.Fixpoint.SortCheck

Methods

elaborate :: Located String -> SymEnv -> Rewrite -> Rewrite

Elaborate Expr

Defined in Language.Fixpoint.SortCheck

Methods

elaborate :: Located String -> SymEnv -> Expr -> Expr

Elaborate SortedReft

Defined in Language.Fixpoint.SortCheck

Methods

elaborate :: Located String -> SymEnv -> SortedReft -> SortedReft

Elaborate Sort

Defined in Language.Fixpoint.SortCheck

Methods

elaborate :: Located String -> SymEnv -> Sort -> Sort

Loc a => Elaborate (SInfo a)

Defined in Language.Fixpoint.SortCheck

Methods

elaborate :: Located String -> SymEnv -> SInfo a -> SInfo a

Loc a => Elaborate (SimpC a)

Defined in Language.Fixpoint.SortCheck

Methods

elaborate :: Located String -> SymEnv -> SimpC a -> SimpC a

Loc a => Elaborate (BindEnv a)

Defined in Language.Fixpoint.SortCheck

Methods

elaborate :: Located String -> SymEnv -> BindEnv a -> BindEnv a

Elaborate e => Elaborate (Triggered e)

Defined in Language.Fixpoint.SortCheck

Methods

elaborate :: Located String -> SymEnv -> Triggered e -> Triggered e

Elaborate a => Elaborate (Maybe a)

Defined in Language.Fixpoint.SortCheck

Methods

elaborate :: Located String -> SymEnv -> Maybe a -> Maybe a

Elaborate a => Elaborate [a]

Defined in Language.Fixpoint.SortCheck

Methods

elaborate :: Located String -> SymEnv -> [a] -> [a]

Elaborate (Symbol, Sort)

Defined in Language.Fixpoint.SortCheck

Methods

elaborate :: Located String -> SymEnv -> (Symbol, Sort) -> (Symbol, Sort)

applySorts :: Visitable t => t -> [Sort]

NOTE:apply-monomorphization

Because SMTLIB does not support higher-order functions, all _non-theory_ function applications

EApp e1 e2

are represented, in SMTLIB, as

(Eapp (EApp apply e1) e2)

where apply is 'ECst (EVar "apply") t' and t is 'FFunc a b' a,b are the sorts of e2 and 'e1 e2' respectively.

Note that *all polymorphism* goes through this machinery.

Just before sending to the SMT solver, we use the cast t to generate a special apply_at_t symbol.

To let us do the above, we populate SymEnv with the _set_ of all sorts at which apply is used, computed by applySorts.

NOTE:coerce-apply

-- related to [NOTE:apply-monomorphism]

Haskell's GADTs cause a peculiar problem illustrated below:

```haskell data Field a where FInt :: Field Int FBool :: Field Bool

proj :: Field a -> a -> a proj fld x = case fld of FInt -> 1 + x FBool -> not b ```

## The Problem

The problem is you cannot encode the body of proj as a well-sorted refinement:

```haskell if is$FInt fld then (1 + (coerce (a ~ Int) x)) else (not (coerce (a ~ Bool) x)) ```

The catch is that x is being used BOTH as Int and as Bool which is not supported in SMTLIB.

## Approach: Uninterpreted Functions

We encode coerce as an explicit **uninterpreted function**:

```haskell if is$FInt fld then (1 + (coerce(a -> int) x)) else (not (coerce(a -> bool) x)) ```

where we define, extra constants in the style of apply

```haskell constant coerce(a -> int ) :: a -> int constant coerce(a -> bool) :: a -> int ```

However, it would not let us verify:

```haskell

unwrap :: Field a -> a -> a unwrap fld x = proj fld x

test = unwrap FInt 4 == 5 && unwrap FBool True == False ```

because we'd get

```haskell unwrap FInt 4 :: { if is$FInt FInt then (1 + coerce_int_int 4) else ... } ```

and the UIF nature of coerce_int_int renders the VC invalid.

## Solution: Eliminate Trivial Coercions

HOWEVER, the solution here, may simply be to use UIFs when the coercion is non-trivial (e.g. `a ~ int`) but to eschew them when they are trivial. That is we would encode:

| Expr | SMTLIB | |:-----------------------|:-------------------| | `coerce (a ~ int) x` | `coerce_a_int x` | | `coerce (int ~ int) x` | x |

which, I imagine is what happens _somewhere_ inside GHC too?

elabApply :: SymEnv -> Expr -> Expr

elabApply replaces all direct function calls indirect calls via apply

elabExpr :: Located String -> SymEnv -> Expr -> Expr

elabExpr adds "casts" to decorate polymorphic instantiation sites.

elabNumeric :: Expr -> Expr

unApply :: Expr -> Expr

unElab :: Expr -> Expr

unElabSortedReft :: SortedReft -> SortedReft

unApplySortedReft :: SortedReft -> SortedReft

unApplyAt :: Expr -> Maybe Sort

toInt :: SymEnv -> Expr -> Sort -> Expr

Predicates on Sorts

isFirstOrder :: Sort -> Bool

isMono :: Sort -> Bool

Predicates on Sorts -------------------------------------------------------

runCM0 :: SrcSpan -> CheckM a -> Either ChError a