STLC0.hs

-- http://siek.blogspot.com/2013/05/type-safety-in-three-easy-lemmas.html 

{-@ LIQUID "--reflection"     @-}
{-@ LIQUID "--ple"            @-}
{-@ LIQUID "--no-termination" @-}

{-# LANGUAGE GADTs #-}

module STLC where 

type Var = String 

data Type 
  = TInt 
  | TBool 
  deriving (Eq, Show) 
 -- | TFun Type Type 

data Op  
  = Add 
  | Leq 
  | And 
  deriving (Eq, Show) 

data Expr 
  = EBool Bool 
  | EInt  Int 
  | EBin  Op Expr Expr       
  deriving (Eq, Show) 
 
-- | EVar Var                -- ^ 'EVar x'       is 'x'
-- | EFun Var Var Type Expr  -- ^ 'EFun f x t e' is 'fun f(x:t) e'

data Val 
  = VBool Bool 
  | VInt  Int
  deriving (Eq, Show) 

data Result 
  = Result Val  
  | Stuck 
  | Timeout
  deriving (Eq, Show) 

{-@ reflect seq2 @-}
-- seq2 :: (a -> b -> Result c) -> Result a -> Result b -> Result c
seq2 :: (Val -> Val -> Result) -> Result -> Result -> Result
seq2 f r1 r2 = case r1 of 
                 Stuck     -> Stuck 
                 Timeout   -> Timeout 
                 Result v1 -> case r2 of 
                                Stuck     -> Stuck 
                                Timeout   -> Timeout 
                                Result v2 -> f v1 v2 

--------------------------------------------------------------------------------
-- | Evaluator 
--------------------------------------------------------------------------------

{-@ reflect eval @-}
eval :: Expr -> Result 
eval (EBool b)      = Result (VBool b)
eval (EInt  n)      = Result (VInt  n)
eval (EBin o e1 e2) = seq2 (evalOp o) (eval e1) (eval e2) 

{-@ reflect evalOp @-}
evalOp :: Op -> Val -> Val -> Result 
evalOp Add (VInt n1)  (VInt n2)  = Result (VInt  (n1 +  n2))
evalOp Leq (VInt n1)  (VInt n2)  = Result (VBool (n1 <= n2))
evalOp And (VBool b1) (VBool b2) = Result (VBool (b1 && b2)) 
evalOp _   _          _          = Stuck 

--------------------------------------------------------------------------------
-- | Tests before proofs 
--------------------------------------------------------------------------------

tests  = [ e1              -- 15
         , EBin Leq e1 e1  -- True
         , EBin And e1 e1  -- Stuck!
         ]
  where 
    e1 = EBin Add (EInt 5) (EInt 10)


--------------------------------------------------------------------------------
-- | Typing Results 
--------------------------------------------------------------------------------

{- [ |- r : T ]


    |- v : T 
  -------------------- [R_Res]
    |- Result v : T  

  -------------------- [R_Time]
    |- Timeout  : T  

-}

{-@ data ResTy where
        R_Res  :: x:Val -> t:Type -> Prop (ValTy x t) -> Prop (ResTy (Result x) t) 
        R_Time :: t:Type -> Prop (ResTy Timeout t) 
  @-}

data ResTyP where 
  ResTy  :: Result -> Type -> ResTyP 

data ResTy where 
  R_Res  :: Val -> Type -> ValTy -> ResTy 
  R_Time :: Type -> ResTy 

--------------------------------------------------------------------------------
-- | Typing Values 
--------------------------------------------------------------------------------

{- [ |- v : T ] 

    ----------------------- [V_Bool]
      |- VBool b : TBool

    ----------------------- [V_Int]
      |- VInt i : TInt 
    
 -}

{-@ data ValTy where
        V_Bool :: b:Bool -> Prop (ValTy (VBool b) TBool) 
        V_Int  :: i:Int  -> Prop (ValTy (VInt i)  TInt) 
  @-}

data ValTyP where 
  ValTy  :: Val -> Type -> ValTyP 

data ValTy where 
  V_Bool :: Bool -> ValTy 
  V_Int  :: Int  -> ValTy 

--------------------------------------------------------------------------------
-- | Typing Expressions 
--------------------------------------------------------------------------------

{-@ reflect opIn1 @-}
opIn1 :: Op -> Type 
opIn1 Add = TInt 
opIn1 Leq = TInt 
opIn1 And = TBool

{-@ reflect opIn2 @-}
opIn2 :: Op -> Type 
opIn2 Add = TInt 
opIn2 Leq = TInt 
opIn2 And = TBool

{-@ reflect opOut @-}
opOut :: Op -> Type 
opOut Add = TInt 
opOut Leq = TBool 
opOut And = TBool

{- 

  --------------------------------------[E-Bool]
    |- EBool b : TBool

  --------------------------------------[E-Int]
    |- EInt n  : TInt 

    |- e1 : opIn1 o   |- e2 : opIn2 o 
  --------------------------------------[E-Bin]
    |- EBin o e1 e2 : opOut o

-}

{-@ data ExprTy where 
        E_Bool :: b:Bool 
               -> Prop (ExprTy (EBool b) TBool)
        E_Int  :: i:Int  
               -> Prop (ExprTy (EInt i)  TInt)
        E_Bin  :: o:Op -> e1:Expr -> e2:Expr 
               -> Prop (ExprTy e1 (opIn1 o)) 
               -> Prop (ExprTy e2 (opIn2 o))
               -> Prop (ExprTy (EBin o e1 e2) (opOut o))
  @-}
data ExprTyP where 
  ExprTy :: Expr -> Type -> ExprTyP  

data ExprTy where 
  E_Bool :: Bool -> ExprTy 
  E_Int  :: Int  -> ExprTy 
  E_Bin  :: Op   -> Expr -> Expr -> ExprTy -> ExprTy -> ExprTy 

--------------------------------------------------------------------------------
-- | Lemma 1: "evalOp_safe" 
--------------------------------------------------------------------------------

{-@ evalOp_safe 
      :: o:Op -> v1:Val -> v2:Val 
      -> Prop (ValTy v1 (opIn1 o)) 
      -> Prop (ValTy v2 (opIn2 o)) 
      -> (v :: Val, ( {y:() | evalOp o v1 v2 == Result v} , {z:ValTy | prop z = ValTy v (opOut o)}))
  @-}

evalOp_safe :: Op -> Val -> Val -> ValTy -> ValTy -> (Val, ((), ValTy))
evalOp_safe Add (VInt n1) (VInt n2) _ _   = (VInt n, ((), V_Int n))   where n = n1 + n2 
evalOp_safe Add (VBool _) _ (V_Int _) _   = trivial ()  -- weird join point, early break shenanigans 
evalOp_safe Add _ (VBool _) _ (V_Int _)   = trivial () 

evalOp_safe Leq (VInt n1) (VInt n2) _ _   = (VBool b, ((), V_Bool b)) where b = n1 <= n2 
evalOp_safe Leq (VBool _) _ (V_Int _) _   = trivial () 
evalOp_safe Leq _ (VBool _) _ (V_Int _)   = trivial () 

evalOp_safe And (VBool b1) (VBool b2) _ _ = (VBool b, ((), V_Bool b)) where b = b1 && b2 
evalOp_safe And (VInt _) _ (V_Bool _) _   = trivial () 
evalOp_safe And _ (VInt _) _ (V_Bool _)   = trivial () 

{-@ evalOp_res_safe 
      :: o:Op -> r1:Result -> r2:Result
      -> Prop (ResTy r1 (opIn1 o))
      -> Prop (ResTy r2 (opIn2 o))
      -> Prop (ResTy (seq2 (evalOp o) r1 r2) (opOut o)) 
  @-}
evalOp_res_safe :: Op -> Result -> Result -> ResTy -> ResTy -> ResTy
evalOp_res_safe o (Result v1) (Result v2) (R_Res _ _ vt1) (R_Res _ _ vt2) 
  = case evalOp_safe o v1 v2 vt1 vt2 of 
      (v, (_, vt)) -> R_Res v (opOut o) vt  
evalOp_res_safe o _ _  (R_Time t1) _ 
  = R_Time (opOut o)
evalOp_res_safe o _ _  _ (R_Time t2) 
  = R_Time (opOut o)

--------------------------------------------------------------------------------
-- | Lemma 3: "eval_safe" 
--------------------------------------------------------------------------------

{-@ eval_safe :: e:Expr -> t:Type -> Prop (ExprTy e t) -> Prop (ResTy (eval e) t) @-}
eval_safe :: Expr -> Type -> ExprTy -> ResTy 
eval_safe (EBool b) TBool _         = R_Res (VBool b) TBool (V_Bool b) 
eval_safe (EBool _) _     (E_Int _) = trivial ()  -- WHY is this needed?
 
eval_safe (EInt n) TInt  _          = R_Res (VInt n) TInt (V_Int n) 
eval_safe (EInt _) _     (E_Bool _) = trivial ()  -- WHY is this needed?

eval_safe (EBin o e1 e2) t (E_Bin _ _ _ et1 et2)
                                    = evalOp_res_safe o (eval e1) (eval e2) rt1 rt2     
  where 
    rt1                             = eval_safe e1 (opIn1 o) et1
    rt2                             = eval_safe e2 (opIn2 o) et2

--------------------------------------------------------------------------------
-- | Boilerplate 
--------------------------------------------------------------------------------

{-@ measure prop :: a -> b           @-}
{-@ type Prop E = {v:_ | prop v = E} @-}

{-@ trivial :: {v:a | false} -> b @-}
trivial :: a -> b
trivial x = trivial x