Support for lambdas :)

.gitmodules

@@ -1,3 +1,3 @@
 [submodule "liquid-fixpoint"]
 	path = liquid-fixpoint
-	url = https://github.com/ucsd-progsys/liquid-fixpoint.git
+	url = https://github.com/alecsferra/liquid-fixpoint.git

liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Axiom.hs

@@ -41,6 +41,7 @@ import           Language.Haskell.Liquid.Bare.Measure as Bare
 import           Language.Haskell.Liquid.UX.Config
 import qualified Data.List as L
 import Control.Applicative
+import Control.Arrow (second)
 import Data.Function (on)
 import qualified Data.Map as Map
 import qualified Data.HashMap.Strict as M
@@ -324,13 +325,20 @@ makeAxiom env tycEnv lmap (x, mbT, v, def)
 mkError :: PPrint a => Located a -> String -> Error
 mkError x str = ErrHMeas (sourcePosSrcSpan $ loc x) (pprint $ val x) (PJ.text str)
 
+-- This function is uded to generate the fixpoint code for reflected functions
 makeAssumeType
   :: Bool -- ^ typeclass enabled
   -> F.TCEmb Ghc.TyCon -> LogicMap -> DataConMap -> LocSymbol -> Maybe SpecType
   -> Ghc.Var -> Ghc.CoreExpr
   -> (LocSpecType, F.Equation)
 makeAssumeType allowTC tce lmap dm sym mbT v def
-  = (sym {val = aty at `strengthenRes` F.subst su ref},  F.mkEquation symbolV xts (F.subst su le) out)
+  = ( sym {val = aty at `strengthenRes` F.subst su ref}
+    , F.mkEquation 
+        symbolV 
+        (fmap (second $ F.sortSubst sortSub) xts)
+        (F.sortSubstInExpr sortSub (F.subst su le))
+        (F.sortSubst sortSub out)
+    )
   where
     symbolV = F.symbol v
     rt    = fromRTypeRep .
@@ -348,6 +356,26 @@ makeAssumeType allowTC tce lmap dm sym mbT v def
     ref        = F.Reft (F.vv_, F.PAtom F.Eq (F.EVar F.vv_) le)
     mkErr s    = ErrHMeas (sourcePosSrcSpan $ loc sym) (pprint $ val sym) (PJ.text s)
     bbs        = filter isBoolBind xs
+
+    -- rTypeSortExp produces monomorphic sorts from polymorphic types.
+    -- As an example, for 
+    -- id :: a -> a ... id x = x 
+    -- we got: 
+    -- define id (x : a#foobar) : a#foobar = { (x : a#foobar) }
+    -- Using FObj instead of a real type variable (FVar i) This code solves the
+    -- issue by creating a sort substitution that replaces those "fake" type variables
+    -- with actual ones.
+    -- define id (x : @-1) : a@-1 = { (x : a@-1) }
+    (tyVars, _) = Ghc.splitForAllTyCoVars τ
+    sortSub     = F.mkSortSubst $ zip (fmap F.symbol tyVars) (F.FVar <$> freeSort)
+    -- We need sorts that aren't polluted by rank-n types, we can't just look at
+    -- the term to determine statically what is the "maximum" sort bound ex:
+    -- freeSort = [1 + (maximum $ -1 : F.sortAbs out : fmap (F.sortAbs . snd) xts) ..] 
+    -- as some variable may be bound to something of rank-n type.  In
+    -- SortCheck.hs in fixpoint they just start at 42 for some reason.  I think
+    -- Negative Debruijn indices (levels :^)) are safer
+    freeSort    = [-1, -2 ..]
+
     (xs, def') = GM.notracePpr "grabBody" $ grabBody allowTC (Ghc.expandTypeSynonyms τ) $ normalize allowTC def
     su         = F.mkSubst  $ zip (F.symbol     <$> xs) xArgs
                            ++ zip (simplesymbol <$> xs) xArgs
@@ -428,6 +456,7 @@ instance Subable Ghc.CoreAlt where
   subst su (Ghc.Alt c xs e) = Ghc.Alt c xs (subst su e)
 
 data AxiomType = AT { aty :: SpecType, aargs :: [(F.Symbol, SpecType)], ares :: SpecType }
+  deriving Show
 
 -- | Specification for Haskell function
 --

liquidhaskell-boot/src/Language/Haskell/Liquid/Constraint/Init.hs

@@ -194,7 +194,7 @@ measEnv sp xts cbs _tcb lt1s lt2s asms itys hs info = CGE
         [ tcb'
         , lts
         , second (rTypeSort tce . val) <$> gsMeas (gsData sp)
-        , [(F.eqName e, eqToPolySort e) | e <- gsImpAxioms (gsRefl sp)]
+        , [(F.eqName e, eqSort e) | e <- gsImpAxioms (gsRefl sp)]
         ]
   , denv     = dmapty val $ gsDicts (gsSig sp)
   , recs     = S.empty
@@ -222,14 +222,12 @@ measEnv sp xts cbs _tcb lt1s lt2s asms itys hs info = CGE
       lts         = lt1s ++ lt2s
       tcb'        = []
 
--- | Given an equation whose sorts are @FObj "a##..."@, @FObj "b##..."@, etc,
--- replaces those with @FVar@s.
-eqToPolySort :: F.EquationV v -> F.Sort
-eqToPolySort e  =
+-- | Constructs the sort of an equation
+eqSort :: F.EquationV v -> F.Sort
+eqSort e  =
     let s = foldr (F.FFunc . snd) (F.eqSort e) (F.eqArgs e)
         ss = filter (isTyVarName . F.symbolString) $ S.toList $ F.sortSymbols s
-        su = F.mkSortSubst $ zip ss $ map F.FVar [0..]
-     in F.mkPoly (length ss - 1) $ F.sortSubst su s
+     in F.mkPoly (length ss - 1) s
   where
     isTyVarName s = all isLower (take 1 s) && L.isInfixOf "##" s
 

liquidhaskell-boot/src/Language/Haskell/Liquid/Transforms/CoreToLogic.hs

@@ -290,11 +290,9 @@ coreToLg allowTC (C.Cast e c)          = do (s, t) <- coerceToLg c
                                             return (ECoerc s t e')
 -- elaboration reuses coretologic
 -- TODO: fix this
-coreToLg True (C.Lam x e) = do p     <- coreToLg True e
-                               tce   <- lsEmb <$> getState
-                               return $ ELam (symbol x, typeSort tce (GM.expandVarType x)) p
-coreToLg _ e@(C.Lam _ _)        = throw ("Cannot transform lambda abstraction to Logic:\t" ++ GM.showPpr e ++
-                                            "\n\n Try using a helper function to remove the lambda.")
+coreToLg allowTC    (C.Lam x e) = do p     <- coreToLg allowTC e
+                                     tce   <- lsEmb <$> getState
+                                     return $ ELam (symbol x, typeSort tce (GM.expandVarType x)) p
 coreToLg _ e                     = throw ("Cannot transform to Logic:\t" ++ GM.showPpr e)
 
 

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) 
+