Examples for lambdas

ExprCompiler.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}

{-@ LIQUID "--ple"           @-}
{-@ LIQUID "--etabeta"       @-}
{-@ LIQUID "--reflection"    @-}
{-@ LIQUID "--dependantcase" @-}

module ExprCompiler where

import Prelude hiding ((.))
import Language.Haskell.Liquid.ProofCombinators

{-@ reflect id @-}
{-@ reflect $  @-}
{-@ infix $    @-}

{-@ reflect .  @-}
{-@ infix .    @-}
infixr 9 .
(.) :: (b -> c) -> (a -> b) -> a -> c
(.) f g x = f (g x)

data Expr where
  EConst :: Int -> Expr
  EAdd   :: Expr -> Expr -> Expr
  EMul   :: Expr -> Expr -> Expr
  ENeg   :: Expr -> Expr

{-@ reflect eval @-}
eval :: Expr -> Int
eval (EConst x) = x
eval (EAdd e1 e2) = eval e1 + eval e2
eval (EMul e1 e2) = eval e1 * eval e2
eval (ENeg e)     = - (eval e)

type Stack = [Int]

data OpCode where
  OpPush :: Int -> OpCode
  OpAdd :: OpCode
  OpMul :: OpCode
  deriving Show


{-@ reflect push @-}
push :: Int -> Stack -> Stack
push v s = v : s

{-@ reflect execOpCode @-}
{-@ execOpCode :: o:OpCode -> { v:Stack | len v >= minStackSize o } -> Stack @-}
execOpCode :: OpCode -> Stack -> Stack
execOpCode (OpPush x) = push x
execOpCode OpAdd      = \case (x : y : xs) -> (y + x) : xs
execOpCode OpMul      = \case (x : y : xs) -> (y * x) : xs

{-@ reflect minStackSize @-}
minStackSize :: OpCode -> Int
minStackSize (OpPush x) = 0
minStackSize _          = 2

data Program where
{-@ PNil :: Prop (Program id) @-}
  PNil :: Program
{-@ PCons :: op:OpCode
          -> p:(Stack -> { v:Stack | len v >= minStackSize op }) -> Prop (Program p)
          -> Prop (Program (execOpCode op . p)) @-}
  PCons :: OpCode -> (Stack -> Stack) -> Program -> Program
data PROGRAM = Program (Stack -> Stack)

{-@ reflect compose @-}
{-@ compose :: p1:(Stack -> Stack) -> p2:(Stack -> Stack)  
            -> Prop (Program p1) -> Prop (Program p2)
            -> Prop (Program (p2 . p1)) @-}
compose :: (Stack -> Stack) -> (Stack -> Stack) -> Program -> Program -> Program
compose s1 s2 p1 PNil                   = p1
compose s1 s2 p1 (PCons cmd srest rest) =
  PCons cmd (srest . s1) (compose s1 srest p1 rest)

{-@ compile :: e:Expr -> Prop (Program (push $ eval e)) @-}
compile :: Expr -> Program
compile (EConst x)   = PCons (OpPush x) id PNil
compile (EAdd e1 e2) =
  PCons
    OpAdd
    ((push $ eval e1) . (push $ eval e2))
    (compose (push $ eval e2) (push $ eval e1) (compile e2) (compile e1))
compile (EMul e1 e2) =
  PCons
    OpMul
    ((push $ eval e1) . (push $ eval e2))
    (compose (push $ eval e2) (push $ eval e1) (compile e2) (compile e1))
compile (ENeg e)     =
  PCons
    OpMul
    ((push $ -1) . (push $ eval e))
    (PCons (OpPush $ -1) (push $ eval e) (compile e))

MapFusion.hs

{-# LANGUAGE RankNTypes #-}

{-@ LIQUID "--reflection" @-}
{-@ LIQUID "--ple"        @-}
{-@ LIQUID "--etabeta"    @-}

module MapFusion where

import Prelude hiding (map, foldr)
import Language.Haskell.Liquid.ProofCombinators

-- When we allow the parser to accept : in refinements this wont be needed
{-@ reflect append @-}
append :: a -> [a] -> [a]
append = (:)

{-@ reflect map @-}
map :: (a -> b) -> [a] -> [b]
map _ []     = []
map f (x:xs) = f x : map f xs

{-@ reflect foldr @-}
foldr :: (a -> b -> b) -> b -> [a] -> b
foldr _ e []     = e
foldr f e (x:xs) = f x (foldr f e xs)

{-@ reflect build @-}
build :: forall a. (forall b. (a -> b -> b) -> b -> b) -> [a]
build g = g (:) []

{-@ reflect mapFB @-}
mapFB :: forall elt lst a . (elt -> lst -> lst) -> (a -> elt) -> a -> lst -> lst
mapFB c f = \x ys -> c (f x) ys

{-@ rewriteMapList :: f:_ -> b:_ -> { foldr (mapFB append f) [] b = map f b } @-}
rewriteMapList :: (a -> b) -> [a] -> ()
rewriteMapList f []     = trivial
rewriteMapList f (x:xs) = trivial ? (rewriteMapList f xs)

{-@ rewriteMapFB :: c:_ -> f:_ -> g:_ -> { mapFB (mapFB c f) g = mapFB c (f . g) } @-}
rewriteMapFB :: (a -> b -> b) -> (c -> a) -> (d -> c) -> Proof
rewriteMapFB c f g = trivial

{-@ rewriteMapFBid :: c:(a -> b -> b) -> { mapFB c (\x:a -> x) = c } @-}
rewriteMapFBid :: (a -> b -> b) -> ()
rewriteMapFBid c = trivial

{-@ rewriteMap :: f:(a1 -> a2) -> xs:[a1] 
               -> { build (\c:func(1, [a2, @(0), @(0)]) -> \n:@(0) -> foldr (mapFB c f) n xs) 
                  = map f xs } @-}
rewriteMap :: (a1 -> a2) -> [a1] -> ()
rewriteMap f []     = trivial
rewriteMap f (x:xs) = trivial ? rewriteMap f xs

ReaderLaws.hs

{-@ LIQUID "--reflection"                @-}
{-@ LIQUID "--ple"                       @-}
{-@ LIQUID "--etabeta"                   @-}

module ReaderLaws where

import Language.Haskell.Liquid.ProofCombinators

import Prelude hiding (return, (>>=))


{-@ data Reader r a = Reader { runReader :: r -> a } @-}
data Reader r a     = Reader { runReader :: r -> a }

{-@ reflect return @-}
return :: a -> Reader r a
return x = Reader $ \y -> x

{-@ infix   >>= @-}
{-@ reflect >>= @-}
(>>=) :: Reader r a -> (a -> Reader r b) -> Reader r b
(Reader x) >>= f = Reader $ \r -> runReader (f $ x r) r

{-@ readerId :: f:(Reader r a) -> { f = Reader (runReader f) } @-} 
readerId :: (Reader r a) -> Proof 
readerId (Reader _) = trivial

{-@ rightIdentity :: x:Reader r a -> { x >>= return = x } @-}
rightIdentity :: Reader r a -> Proof
rightIdentity (Reader _) = trivial

{-@ associativity :: x:Reader r a -> f: (a -> Reader r a) -> g:(a -> Reader r a) 
                  -> { (x >>= f) >>= g = x >>= (\r:a -> f r >>= g) } @-}
associativity :: Reader r a -> (a -> Reader r a) -> (a -> Reader r a) -> Proof
associativity (Reader _) _ _ = trivial

{-@ leftIdentity :: x:a -> f:(a -> Reader r b) -> { return x >>= f = f x } @-}
leftIdentity :: a -> (a -> Reader r b) -> Proof
leftIdentity x f = case f x of Reader _ -> trivial