MM.hs

{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}

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

module MaybeMotivatingSafe where

import Language.Haskell.Liquid.ProofCombinators

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

{-@ infix .      @-}
{-@ reflect .    @-}

-- import Prelude hiding ((.))
-- {-@ reflect (.) @-}
-- (.) :: (a -> b) -> (c -> a) -> c -> b
-- (.) 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))