Hoogle Search

Within LTS Haskell 24.33 (ghc-9.10.3)

Note that Stackage only displays results for the latest LTS and Nightly snapshot. Learn more.

Exact lookup

1. nontrivsorts :: Fixpoint a => Config -> FInfo a -> IO (Result a)

   liquid-fixpoint	Language.Fixpoint.Solver.TrivialSort

   No documentation available.

2. applySorts :: Foldable t => t -> [Sort]

   liquid-fixpoint	Language.Fixpoint.SortCheck

   • NOTE:apply-monomorphization Because SMTLIB does not support higher-order functions, all _non-theory_ function applicationsEApp e1 e2are 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 {- reflect proj -} 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 {- reflect unwrap -} unwrap :: Field a -> a -> a unwrap fld x = proj fld x {- test :: _ -> TT -} 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?

3. boolSort :: Sort

   liquid-fixpoint	Language.Fixpoint.SortCheck

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

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

   liquid-fixpoint	Language.Fixpoint.SortCheck

   No documentation available.

5. checkSortFull :: Checkable a => SrcSpan -> SEnv SortedReft -> Sort -> a -> ElabM (Maybe Doc)

   liquid-fixpoint	Language.Fixpoint.SortCheck

   No documentation available.

6. checkSorted :: Checkable a => SrcSpan -> SEnv Sort -> a -> ElabM (Maybe Doc)

   liquid-fixpoint	Language.Fixpoint.SortCheck

   No documentation available.

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

   liquid-fixpoint	Language.Fixpoint.SortCheck

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

8. checkSortedReftFull :: Checkable a => SrcSpan -> SEnv SortedReft -> a -> ElabM (Maybe Doc)

   liquid-fixpoint	Language.Fixpoint.SortCheck

   No documentation available.

9. exprSort :: String -> Expr -> Sort

   liquid-fixpoint	Language.Fixpoint.SortCheck

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

10. exprSortMaybe :: Expr -> Maybe Sort

    liquid-fixpoint	Language.Fixpoint.SortCheck

    No documentation available.

Page 151 of many | Previous | Next