Add some tests with lambdas

tests/ple/pos/FuseMapLam.hs

@@ -0,0 +1,54 @@
+{-# LANGUAGE RankNTypes #-}
+
+{-@ LIQUID "--reflection" @-}
+{-@ LIQUID "--ple"        @-}
+{-@ LIQUID "--etabeta"    @-}
+
+module FuseMapLam 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

tests/ple/pos/SKILam.hs

@@ -0,0 +1,215 @@
+{-# Language GADTs, TypeFamilies, DataKinds #-}
+
+{-@ LIQUID "--reflection"        @-}
+{-@ LIQUID "--ple"               @-}
+{-@ LIQUID "--full"              @-}
+{-@ LIQUID "--max-case-expand=4" @-}
+{-@ LIQUID "--etabeta"           @-}
+{-@ LIQUID "--dependantcase"     @-}
+
+module SKILam where
+
+import Prelude
+
+import Language.Haskell.Liquid.ProofCombinators
+
+{-@ reflect id @-}
+{-@ reflect $  @-}
+
+data List a = Nil | Cons a (List a)
+  deriving (Show)
+
+data Ty
+  = Iota
+  | Arrow Ty Ty
+  deriving Eq
+
+type Ctx = List Ty
+
+data Ref where
+  {-@ Here :: σ:Ty -> γ:Ctx -> Prop (Ref σ (Cons σ γ)) @-}
+  Here :: Ty -> Ctx -> Ref
+
+  {-@ There :: τ:Ty -> σ:Ty -> γ:Ctx -> Prop (Ref σ γ) 
+            -> Prop (Ref σ (Cons τ γ)) @-}
+  There :: Ty -> Ty -> Ctx -> Ref -> Ref
+data REF = Ref Ty Ctx
+
+data Term where
+  {-@ App :: σ:Ty -> τ:Ty -> γ:Ctx -> Prop (Term γ (Arrow σ τ)) 
+          -> Prop (Term γ σ) -> Prop (Term γ τ) @-}
+  App :: Ty -> Ty -> Ctx -> Term -> Term -> Term
+  {-@ Lam :: σ:Ty -> τ:Ty -> γ:Ctx -> Prop (Term (Cons σ γ) τ) 
+          -> Prop (Term γ (Arrow σ τ)) @-}
+  Lam :: Ty -> Ty -> Ctx -> Term -> Term
+  {-@ Var :: σ:Ty -> γ:Ctx -> Prop (Ref σ γ) -> Prop (Term γ σ) @-}
+  Var :: Ty -> Ctx -> Ref -> Term
+data TERM = Term Ctx Ty
+
+{-@ measure tlen @-}
+{-@ tlen :: Term -> Nat @-}
+tlen :: Term -> Int
+tlen (App _ _ _ t₁ t₂) = 1 + tlen t₁ + tlen t₂
+tlen (Lam _ _ _ t)     = 1 + tlen t
+tlen (Var _ _ _)       = 0
+
+
+-- VFun function is non positive idk how to fix
+{-@ LIQUID "--no-positivity-check" @-}
+data Value where
+  {-@ VIota :: Int -> Prop (Value Iota) @-}
+  VIota :: Int -> Value
+  {-@ VFun :: σ:Ty -> τ:Ty -> (Prop (Value σ) -> Prop (Value τ)) 
+           -> Prop (Value (Arrow σ τ)) @-}
+  VFun :: Ty -> Ty -> (Value -> Value) -> Value
+data VALUE = Value Ty
+
+data Env where
+  {-@ Empty :: Prop (Env Nil) @-}
+  Empty :: Env
+  {-@ With :: σ:Ty -> γ:Ctx -> Prop (Value σ) -> Prop (Env γ) 
+           -> Prop (Env (Cons σ γ)) @-}
+  With  :: Ty -> Ctx -> Value -> Env -> Env
+data ENV = Env Ctx
+
+{-@ reflect lookupRef @-}
+{-@ lookupRef :: σ:Ty -> γ:Ctx -> r:Prop (Ref σ γ) -> Prop (Env γ) 
+              -> Prop (Value σ) @-}
+lookupRef :: Ty -> Ctx -> Ref -> Env -> Value
+lookupRef _ _           (Here _ _)          (With _ _ a _)  = a
+lookupRef σ (Cons γ γs) (There _ _ _ there) (With _ _ _ as) =
+  lookupRef σ γs there as
+
+{-@ reflect eval @-}
+{-@ eval :: σ:Ty -> γ:Ctx -> t:Prop (Term γ σ) -> Prop (Env γ) 
+         -> Prop (Value σ) @-}
+eval :: Ty -> Ctx -> Term -> Env -> Value
+eval σ           γ (App α _ _ t₁ t₂) e = case eval (Arrow α σ) γ t₁ e of
+    VFun _ _ f -> f (eval α γ t₂ e)
+eval σ           γ (Var _ _ x)       e = lookupRef σ γ x e
+eval (Arrow α σ) γ (Lam _ _ _ t)     e = VFun α σ (\y -> eval σ (Cons α γ) t (With α γ y e))
+
+{-@ reflect makeId @-}
+{-@ makeId :: σ:Ty -> γ:Ctx -> (Prop (Env γ) -> Prop (Value (Arrow σ σ))) @-}
+makeId :: Ty -> Ctx -> (Env -> Value)
+makeId σ γ v = VFun σ σ id
+
+{-@ reflect makeApp @-}
+{-@ makeApp :: σ:Ty -> τ:Ty -> γ:Ctx 
+            -> (Prop (Env γ) -> Prop (Value (Arrow σ τ)))
+            -> (Prop (Env γ) -> Prop (Value σ))
+            -> Prop (Env γ) -> Prop (Value τ) @-}
+makeApp :: Ty -> Ty -> Ctx -> (Env -> Value) -> (Env -> Value) -> Env -> Value
+makeApp σ τ γ fun arg env = case fun env of
+  VFun _ _ f -> f (arg env)
+
+{-@ reflect makeConst @-}
+{-@ makeConst :: σ:Ty -> τ:Ty -> γ:Ctx 
+              -> (Prop (Env γ) -> Prop (Value (Arrow σ (Arrow τ σ)))) @-}
+makeConst :: Ty -> Ty -> Ctx -> (Env -> Value)
+makeConst σ τ γ e = VFun σ (Arrow τ σ) $ \x -> VFun τ σ $ \y -> x
+
+
+{-@ reflect makeS @-}
+{-@ makeS :: σ:Ty -> τ:Ty -> υ:Ty -> γ:Ctx 
+          -> (Prop (Env γ) 
+             -> Prop (Value (Arrow (Arrow σ (Arrow τ υ)) 
+                                   (Arrow (Arrow σ τ) (Arrow σ υ)))))@-}
+makeS :: Ty -> Ty -> Ty -> Ctx -> (Env -> Value)
+makeS σ τ υ γ e = VFun (Arrow σ (Arrow τ υ)) (Arrow (Arrow σ τ) (Arrow σ υ)) 
+                    $ \(VFun _ _ x) -> VFun (Arrow σ τ) (Arrow σ υ) $ \(VFun _ _ y) -> VFun σ υ $ \z -> case (x z) 
+                        of VFun _ _ xz -> xz (y z)
+
+
+{-@ reflect sType @-}
+sType σ τ υ = Arrow (Arrow σ (Arrow τ υ)) (Arrow (Arrow σ τ) (Arrow σ υ))
+
+{-@ reflect kType @-}
+kType σ τ = Arrow σ (Arrow τ σ)
+
+{-@ reflect iType @-}
+iType σ = Arrow σ σ
+
+{-@ reflect dom @-}
+{-@ dom :: { σ:Ty | σ /= Iota } -> Ty @-}
+dom (Arrow σ τ) = σ
+
+{-@ reflect cod @-}
+{-@ cod :: { σ:Ty | σ /= Iota } -> Ty @-}
+cod (Arrow σ τ) = τ
+
+
+data Comb where
+  {-@ S :: σ:Ty -> τ:Ty -> υ:Ty -> γ:Ctx 
+        -> Prop (Comb γ (sType σ τ υ) (makeS σ τ υ γ)) @-}
+  S :: Ty -> Ty -> Ty -> Ctx -> Comb
+  {-@ K :: σ:Ty -> τ:Ty -> γ:Ctx
+        -> Prop (Comb γ (kType σ τ) (makeConst σ τ γ)) @-}
+  K :: Ty -> Ty -> Ctx -> Comb
+  {-@ I :: σ:Ty -> γ:Ctx 
+        -> Prop (Comb γ (iType σ) (makeId σ γ)) @-}
+  I :: Ty -> Ctx -> Comb
+  {-@ CApp :: σ:Ty -> τ:Ty -> γ:Ctx 
+           -> fun:(Prop (Env γ) -> Prop (Value (Arrow σ τ)))
+           -> arg:(Prop (Env γ) -> Prop (Value σ))
+           -> Prop (Comb γ (Arrow σ τ) fun)
+           -> Prop (Comb γ σ arg) 
+           -> Prop (Comb γ τ (makeApp σ τ γ fun arg)) @-}
+  CApp :: Ty -> Ty -> Ctx -> (Env -> Value) -> (Env -> Value) -> Comb -> Comb 
+       -> Comb
+  {-@ CVar :: σ:Ty -> γ:Ctx -> r:Prop (Ref σ γ)
+           -> Prop (Comb γ σ (lookupRef σ γ r)) @-}
+  CVar :: Ty -> Ctx -> Ref -> Comb
+data COMB = Comb Ctx Ty (Env -> Value)
+
+{-@ translate :: σ:Ty -> γ:Ctx -> t:Prop (Term γ σ) 
+              -> Prop (Comb γ σ (eval σ γ t))  @-}
+translate :: Ty -> Ctx -> Term -> Comb
+translate σ           γ (App α _ _ t₁ t₂) = 
+  CApp α σ γ (eval (Arrow α σ) γ t₁) (eval α γ t₂) t₁ₜ t₂ₜ 
+  where t₁ₜ = translate (Arrow α σ) γ t₁
+        t₂ₜ = translate α           γ t₂
+translate σ           γ (Var _ _ x)       = 
+  CVar σ γ x 
+translate (Arrow σ τ) γ (Lam _ _ _ t)     = 
+  bracket σ τ γ (eval τ (Cons σ γ) t) (translate τ (Cons σ γ) t)
+
+{-@ reflect makeBracketing @-}
+{-@ makeBracketing :: σ:Ty -> τ:Ty -> γ:Ctx 
+                   -> f:(Prop (Env (Cons σ γ)) -> Prop (Value τ))
+                   -> Prop (Env γ)
+                   -> Prop (Value (Arrow σ τ)) @-}
+makeBracketing :: Ty -> Ty -> Ctx -> (Env -> Value) -> Env -> Value
+makeBracketing σ τ γ f env = VFun σ τ $ \x -> f (With σ γ x env)
+
+{-@ bracket :: σ:Ty -> τ:Ty -> γ:Ctx -> f:(Prop (Env (Cons σ γ)) -> Prop (Value τ)) 
+            -> Prop (Comb (Cons σ γ) τ f) 
+            -> Prop (Comb γ (Arrow σ τ) (makeBracketing σ τ γ f)) @-}
+bracket :: Ty -> Ty -> Ctx -> (Env -> Value) -> Comb -> Comb
+bracket σ τ γ f (CApp α _ _ ft₁ ft₂ t₁ t₂)             =
+  CApp (Arrow σ α) (Arrow σ τ) γ 
+       (makeApp (Arrow σ (Arrow α τ)) (Arrow (Arrow σ α) (Arrow σ τ)) 
+                γ (makeS σ α τ γ) (makeBracketing σ (Arrow α τ) γ ft₁))
+       (makeBracketing σ α γ ft₂) st t₂ᵣ
+  where t₁ᵣ = bracket σ (Arrow α τ) γ ft₁ t₁
+        t₂ᵣ = bracket σ α           γ ft₂ t₂
+        st  = CApp (dom $ sType σ α τ) (cod $ sType σ α τ)
+                   γ
+                   (makeS σ α τ γ)
+                   (makeBracketing σ (Arrow α τ) γ ft₁)
+                   (S σ α τ γ) t₁ᵣ
+bracket σ τ γ f (S τ₁ τ₂ τ₃ _)                 =
+  CApp τ (Arrow σ τ) γ (makeConst τ σ γ) (makeS τ₁ τ₂ τ₃ γ) 
+       (K τ σ γ) (S τ₁ τ₂ τ₃ γ) 
+bracket σ τ γ f (K τ₁ τ₂ _)                    = 
+  CApp τ (Arrow σ τ) γ (makeConst τ σ γ) (makeConst τ₁ τ₂ γ)
+       (K τ σ γ) (K τ₁ τ₂ γ) 
+bracket σ τ γ f (I τ₁ _)                       =
+  CApp τ (Arrow σ τ) γ (makeConst τ σ γ) (makeId τ₁ γ) 
+       (K τ σ γ) (I τ₁ γ) 
+bracket σ τ γ f (CVar _ _ (Here _ _))          =
+  I σ γ
+bracket σ τ γ f (CVar _ _ (There _ _ _ there)) = 
+  CApp τ (Arrow σ τ) γ (makeConst τ σ γ) (lookupRef τ γ there) 
+       (K τ σ γ) (CVar τ γ there) 
+

tests/tests.cabal

@@ -2471,9 +2471,11 @@ executable ple-pos
                     , Tmp
                     , ReaderEta
                     , SKIEta
+                    , SKIDC
+                    , SKILam
                     , FuseMap
+                    , FuseMapLam
                     , ProposalLocalRewrites
-                    , SKIDC
 
     -- XXX(matt.walker): dies on lists on first compile in ghc 8107
     --                   ... and on GHC 9+ now too