liquidhaskell-0.8.10.7: tests/ple/pos/STLC2.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
| TFun Type Type
deriving (Eq, Show)
data Op
= Add
| Leq
| And
deriving (Eq, Show)
data Expr
= EBool Bool -- ^ 'EBool b' is 'b'
| EInt Int -- ^ 'EInt i' is 'i'
| EBin Op Expr Expr -- ^ 'EBin o e1 e2' is 'e1 o e2'
| EVar Var -- ^ 'EVar x' is 'x'
| EFun Var Var Type Expr -- ^ 'EFun f x t e' is 'fun f(x:t) e'
| EApp Expr Expr -- ^ 'EApp e1 e2' is 'e1 e2'
deriving (Eq, Show)
data Val
= VBool Bool
| VInt Int
| VClos Var Var Expr VEnv
deriving (Eq, Show)
data Result
= Result Val
| Stuck
| Timeout
deriving (Eq, Show)
data VEnv
= VBind Var Val VEnv
| VEmp
deriving (Eq, Show)
data TEnv
= TBind Var Type TEnv
| TEmp
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 lookupVEnv @-}
lookupVEnv :: Var -> VEnv -> Maybe Val
lookupVEnv x VEmp = Nothing
lookupVEnv x (VBind y v env) = if x == y then Just v else lookupVEnv x env
{-@ reflect eval @-}
eval :: VEnv -> Expr -> Result
eval _ (EBool b) = Result (VBool b)
eval _ (EInt n) = Result (VInt n)
eval s (EBin o e1 e2) = seq2 (evalOp o) (eval s e1) (eval s e2)
eval s (EVar x) = case lookupVEnv x s of
Nothing -> Stuck
Just v -> Result v
eval s (EFun f x t e) = Result (VClos f x e s)
eval s (EApp e1 e2) = seq2 evalApp (eval s e1) (eval s e2)
{-@ reflect evalApp @-}
evalApp :: Val -> Val -> Result
evalApp v1@(VClos f x e s) v2 = eval (VBind x v2 (VBind f v1 s)) e
evalApp _ _ = Stuck
{-@ 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
g |- s (x,t1), (f,t1->t2),g |- e : t2
--------------------------------------- [V_Clos]
|- VClos f x e s : t1 -> t2
-}
{-@ data ValTy where
V_Bool :: b:Bool -> Prop (ValTy (VBool b) TBool)
V_Int :: i:Int -> Prop (ValTy (VInt i) TInt)
V_Clos :: g:TEnv -> s:VEnv -> f:Var -> x:Var -> t1:Type -> t2:Type -> e:Expr
-> Prop (StoTy g s)
-> Prop (ExprTy (TBind x t1 (TBind f (TFun t1 t2) g)) e t2)
-> Prop (ValTy (VClos f x e s) (TFun t1 t2))
@-}
data ValTyP where
ValTy :: Val -> Type -> ValTyP
data ValTy where
V_Bool :: Bool -> ValTy
V_Int :: Int -> ValTy
V_Clos :: TEnv -> VEnv -> Var -> Var -> Type -> Type -> Expr -> StoTy -> ExprTy -> ValTy
--------------------------------------------------------------------------------
-- | Typing Stores
--------------------------------------------------------------------------------
{- [ G |- S ]
------------------------[S_Emp]
TEmp |- VEmp
|- v : t g |- s
------------------------[S_Bind]
(x, t), g |- (x, v), s
-}
{-@ data StoTy where
S_Emp :: Prop (StoTy TEmp VEmp)
S_Bind :: x:Var -> t:Type -> val:Val -> g:TEnv -> s:VEnv
-> Prop (ValTy val t)
-> Prop (StoTy g s)
-> Prop (StoTy (TBind x t g) (VBind x val s))
@-}
data StoTyP where
StoTy :: TEnv -> VEnv -> StoTyP
data StoTy where
S_Emp :: StoTy
S_Bind :: Var -> Type -> Val -> TEnv -> VEnv -> ValTy -> StoTy -> StoTy
--------------------------------------------------------------------------------
-- | Typing Expressions
--------------------------------------------------------------------------------
{-@ reflect opIn @-}
opIn :: Op -> Type
opIn Add = TInt
opIn Leq = TInt
opIn And = TBool
{-@ reflect opOut @-}
opOut :: Op -> Type
opOut Add = TInt
opOut Leq = TBool
opOut And = TBool
{-@ reflect lookupTEnv @-}
lookupTEnv :: Var -> TEnv -> Maybe Type
lookupTEnv x TEmp = Nothing
lookupTEnv x (TBind y v env) = if x == y then Just v else lookupTEnv x env
{-
--------------------------------------[E-Bool]
G |- EBool b : TBool
--------------------------------------[E-Int]
G |- EInt n : TInt
lookupTEnv x G = Just t
--------------------------------------[E-Var]
G |- Var x : t
G |- e1 : opIn o G |- e2 : opIn o
--------------------------------------[E-Bin]
G |- EBin o e1 e2 : opOut o
(x,t1), (f, t1->t2), G |- e : t2
--------------------------------------[E-Fun]
G |- EFun f x t1 e : t1 -> t2
G |- e1 : t1 -> t2 G |- e2 : t1
--------------------------------------[E-App]
G |- EApp e1 e2 : t2
-}
{-@ data ExprTy where
E_Bool :: g:TEnv -> b:Bool
-> Prop (ExprTy g (EBool b) TBool)
E_Int :: g:TEnv -> i:Int
-> Prop (ExprTy g (EInt i) TInt)
E_Bin :: g:TEnv -> o:Op -> e1:Expr -> e2:Expr
-> Prop (ExprTy g e1 (opIn o))
-> Prop (ExprTy g e2 (opIn o))
-> Prop (ExprTy g (EBin o e1 e2) (opOut o))
E_Var :: g:TEnv -> x:Var -> t:{Type| lookupTEnv x g == Just t}
-> Prop (ExprTy g (EVar x) t)
E_Fun :: g:TEnv -> f:Var -> x:Var -> t1:Type -> e:Expr -> t2:Type
-> Prop (ExprTy (TBind x t1 (TBind f (TFun t1 t2) g)) e t2)
-> Prop (ExprTy g (EFun f x t1 e) (TFun t1 t2))
E_App :: g:TEnv -> e1:Expr -> e2:Expr -> t1:Type -> t2:Type
-> Prop (ExprTy g e1 (TFun t1 t2))
-> Prop (ExprTy g e2 t1)
-> Prop (ExprTy g (EApp e1 e2) t2)
@-}
data ExprTyP where
ExprTy :: TEnv -> Expr -> Type -> ExprTyP
data ExprTy where
E_Bool :: TEnv -> Bool -> ExprTy
E_Int :: TEnv -> Int -> ExprTy
E_Var :: TEnv -> Var -> Type -> ExprTy
E_Bin :: TEnv -> Op -> Expr -> Expr -> ExprTy -> ExprTy -> ExprTy
E_Fun :: TEnv -> Var -> Var -> Type -> Expr -> Type -> ExprTy -> ExprTy
E_App :: TEnv -> Expr -> Expr -> Type -> Type -> ExprTy -> ExprTy -> ExprTy
--------------------------------------------------------------------------------
-- | Lemma 1: "evalOp_safe"
--------------------------------------------------------------------------------
{-@ reflect isValTy @-}
isValTy :: Val -> Type -> Bool
isValTy (VInt _) TInt = True
isValTy (VBool _) TBool = True
isValTy _ _ = False
{-@ propValTy :: o:Op -> w:Val -> Prop (ValTy w (opIn o)) -> { w' : Val | w = w' && isValTy w' (opIn o) } @-}
propValTy :: Op -> Val -> ValTy -> Val
propValTy Add w (V_Int _) = w
propValTy Leq w (V_Int _) = w
propValTy And w (V_Bool _) = w
{-@ evalOp_safe
:: o:Op -> v1:{Val | isValTy v1 (opIn o) } -> v2:{Val | isValTy v2 (opIn o) }
-> (v :: Val, ( {y:() | evalOp o v1 v2 == Result v} , {z:ValTy | prop z = ValTy v (opOut o)}))
@-}
evalOp_safe :: Op -> Val -> Val -> (Val, ((), ValTy))
evalOp_safe Add (VInt n1) (VInt n2) = (VInt n, ((), V_Int n)) where n = n1 + n2
evalOp_safe Leq (VInt n1) (VInt n2) = (VBool b, ((), V_Bool b)) where b = n1 <= n2
evalOp_safe And (VBool b1) (VBool b2) = (VBool b, ((), V_Bool b)) where b = b1 && b2
{-@ evalOp_res_safe
:: o:Op -> r1:Result -> r2:Result
-> Prop (ResTy r1 (opIn o))
-> Prop (ResTy r2 (opIn 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 _ t1 vt1) (R_Res _ t2 vt2)
= case evalOp_safe o (propValTy o v1 vt1) (propValTy o v2 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 2: "lookup_safe"
--------------------------------------------------------------------------------
{-@ lookup_safe :: g:TEnv -> s:VEnv -> x:Var -> t:{Type | lookupTEnv x g == Just t}
-> Prop (StoTy g s)
-> (w :: Val, ({z:() | lookupVEnv x s == Just w} , {z:ValTy | prop z = ValTy w t} ))
@-}
lookup_safe :: TEnv -> VEnv -> Var -> Type -> StoTy -> (Val, ((), ValTy))
lookup_safe _ _ _ _ S_Emp
= trivial ()
lookup_safe g s x t (S_Bind y yt yv g' s' yvt gs')
| x == y
= (yv, ((), yvt))
| otherwise
= lookup_safe g' s' x t gs'
--------------------------------------------------------------------------------
-- | Lemma 3: "app_safe"
--------------------------------------------------------------------------------
{-@ evalApp_safe
:: v1:Val -> v2:Val -> t1:Type -> t2:Type
-> Prop (ValTy v1 (TFun t1 t2))
-> Prop (ValTy v2 t1)
-> Prop (ResTy (evalApp v1 v2) t2)
@-}
evalApp_safe :: Val -> Val -> Type -> Type -> ValTy -> ValTy -> ResTy
evalApp_safe v1@(VClos f x e s) v2 t1 t2 v1_t1_t2@(V_Clos g _ _ _ _ _ _ g_s gxf_e_t2) v2_t1
= eval_safe gxf sxf e t2 gxf_e_t2 gxf_sxf
where
gf = TBind f (TFun t1 t2) g
sf = VBind f v1 s
gxf = TBind x t1 gf
sxf = VBind x v2 sf
gf_sf = S_Bind f (TFun t1 t2) v1 g s v1_t1_t2 g_s
gxf_sxf = S_Bind x t1 v2 gf sf v2_t1 gf_sf
evalApp_safe (VInt {}) _ _ _ (V_Clos {}) _
= trivial ()
evalApp_safe (VBool {}) _ _ _ (V_Clos {}) _
= trivial ()
{-@ evalApp_res_safe
:: r1:Result -> r2:Result -> t1:Type -> t2:Type
-> Prop (ResTy r1 (TFun t1 t2))
-> Prop (ResTy r2 t1)
-> Prop (ResTy (seq2 evalApp r1 r2) t2)
@-}
evalApp_res_safe :: Result -> Result -> Type -> Type -> ResTy -> ResTy -> ResTy
evalApp_res_safe (Result v1) (Result v2) t1 t2 (R_Res _ _ v1_t1_t2) (R_Res _ _ v2_t1)
= evalApp_safe v1 v2 t1 t2 v1_t1_t2 v2_t1
evalApp_res_safe _ _ _ t2 (R_Time {}) _
= R_Time t2
evalApp_res_safe _ _ _ t2 _ (R_Time {})
= R_Time t2
--------------------------------------------------------------------------------
-- | THEOREM: "eval_safe"
--------------------------------------------------------------------------------
{-@ eval_safe :: g:TEnv -> s:VEnv -> e:Expr -> t:Type
-> Prop (ExprTy g e t)
-> Prop (StoTy g s)
-> Prop (ResTy (eval s e) t)
@-}
eval_safe :: TEnv -> VEnv -> Expr -> Type -> ExprTy -> StoTy -> ResTy
eval_safe _ _ (EBool b) _ (E_Bool {}) _
= R_Res (VBool b) TBool (V_Bool b)
eval_safe _ _ (EInt n) _ (E_Int {}) _
= R_Res (VInt n) TInt (V_Int n)
eval_safe g s (EBin o e1 e2) t (E_Bin _ _ _ _ et1 et2) gs
= evalOp_res_safe o (eval s e1) (eval s e2) rt1 rt2
where
rt1 = eval_safe g s e1 (opIn o) et1 gs
rt2 = eval_safe g s e2 (opIn o) et2 gs
eval_safe g s (EVar x) t (E_Var {}) gs
= R_Res w t wt
where
(w, (_, wt)) = lookup_safe g s x t gs
eval_safe g s (EFun f x t1 e) t (E_Fun _ _ _ _ _ t2 et2) gs
= R_Res (VClos f x e s) t (V_Clos g s f x t1 t2 e gs et2)
eval_safe g s (EApp e1 e2) t2 (E_App _ _ _ t1 _ e1_t1_t2 e2_t1) gs
= evalApp_res_safe (eval s e1) (eval s e2) t1 t2 r1_t1_t2 r2_t1
where
r1_t1_t2 = eval_safe g s e1 (TFun t1 t2) e1_t1_t2 gs
r2_t1 = eval_safe g s e2 t1 e2_t1 gs
--------------------------------------------------------------------------------
-- | Boilerplate
--------------------------------------------------------------------------------
{-@ measure prop :: a -> b @-}
{-@ type Prop E = {v:_ | prop v = E} @-}
{-@ trivial :: {v:a | false} -> b @-}
trivial :: a -> b
trivial x = trivial x