Merge pull request #1386 from ucsd-progsys/ple-opt

Incremental PLE

README.md

@@ -249,7 +249,7 @@ This flag is **global** and will symbolically evaluate all the terms that appear
 As an alternative, the `liquidinstanceslocal` flag has local behavior. [See](https://github.com/ucsd-progsys/liquidhaskell/blob/develop/benchmarks/proofautomation/pos/Unification.hs)
 
 ```
-{-@ LIQUID "--automatic-instances=liquidinstanceslocal" @-}
+{-@ LIQUID "--ple-local" @-}
 ```
 
 will only evaluate terms appearing in the specifications

TODO.md

@@ -1,12 +1,23 @@
 # TODO
 
-- [] Fix termination tests in fail.txt 
-- [] Fix resolve     tests in fail.txt 
-- [] Fix eq-repr     tests in fail.txt 
-- [] Remove trace 
-- [] Remove warnings 
-- [] fix circle
-- [] merge PR
+## PLE-OPT 
+
+- [x] Don't generate KVars inside "proofs" [somehow causes proofs to fail]
+- []  Only run INSTANTIATE/PLE on constraints with a concrete LHS?
+- []  Fancy TRIE to do INCREMENTAL PLE.
+
+
+```
+$ time stack exec -- fixpoint ple-overhead.bfq --allowho --eliminate=some
+
+Safe
+        0.29 real         0.26 user         0.13 sys
+
+$ time stack exec -- fixpoint ple-overhead.bfq --allowho --eliminate=some --rewrite
+
+Safe
+        0.54 real         0.53 user         0.18 sys
+```
 
 
 ## CallStack/Error

benchmarks/popl18/ple/pos/Ackermann.hs

@@ -3,7 +3,7 @@
 -- | http://www.cs.yorku.ca/~gt/papers/Ackermann-function.pdf
 
 {-@ LIQUID "--higherorder"     @-}
-{-@ LIQUID "--automatic-instances=liquidinstances" @-}
+{-@ LIQUID "--ple" @-}
 
 
 module Ackermann where

benchmarks/popl18/ple/pos/Fibonacci.hs

@@ -1,5 +1,5 @@
 {-@ LIQUID "--higherorder"     @-}
-{-@ LIQUID "--automatic-instances=liquidinstances" @-}
+{-@ LIQUID "--ple" @-}
 
 -- TAG: absref 
 

benchmarks/popl18/ple/pos/Unification.hs

@@ -6,7 +6,7 @@
 -- where? switch off non-lin-cuts in higher-order mode?
 
 {-@ LIQUID "--reflection"      @-}
-{-@ LIQUID "--automatic-instances=liquidinstanceslocal" @-}
+{-@ LIQUID "--ple-local" @-}
 
 module Unify where
 

benchmarks/sf/Induction.hs

@@ -1,6 +1,6 @@
 {-@ LIQUID "--exact-data-con"                      @-}
 {-@ LIQUID "--higherorder"                         @-}
-{-@ LIQUID "--automatic-instances=liquidinstances" @-}
+{-@ LIQUID "--ple" @-}
 
 module Induction where
 

include/Language/Haskell/Liquid/ProofCombinators.hs

@@ -116,7 +116,8 @@ _ =>= y  = y
 
 infixl 3 ?
 
-(?) :: a -> Proof -> a 
+{-@ (?) :: forall a b <pa :: a -> Bool, pb :: b -> Bool>. a<pa> -> b<pb> -> a<pa> @-}
+(?) :: a -> b -> a 
 x ? _ = x 
 {-# INLINE (?)   #-} 
 
@@ -165,7 +166,7 @@ x &&& _ = x
 
 {-@ withProof :: x:a -> b -> {v:a | v = x} @-}
 withProof :: a -> b -> a
-withProof x y = x
+withProof x _ = x
 
 {-@ impossible :: {v:a | false} -> b @-}
 impossible :: a -> b

src/Language/Haskell/Liquid/Bare.hs

@@ -21,7 +21,6 @@ module Language.Haskell.Liquid.Bare (
   , saveLiftedSpec
   ) where
 
-
 import           Prelude                                    hiding (error)
 import qualified Control.Exception                          as Ex
 import qualified Data.Binary                                as B
@@ -438,8 +437,7 @@ addReflSigs refl sig = sig { gsAsmSigs = reflSigs ++ gsAsmSigs sig }
     reflSigs         = [ (x, t) | (x, t, _) <- gsHAxioms refl ]   
 
 makeAutoInst :: Bare.Env -> ModName -> Ms.BareSpec -> M.HashMap Ghc.Var (Maybe Int)
-makeAutoInst env name spec = 
-  Misc.hashMapMapKeys (Bare.lookupGhcVar env name "Var") (Ms.autois spec)
+makeAutoInst env name spec = Misc.hashMapMapKeys (Bare.lookupGhcVar env name "Var") (Ms.autois spec)
 
 ----------------------------------------------------------------------------------------
 makeSpecSig :: ModName -> Bare.ModSpecs -> Bare.Env -> Bare.SigEnv -> Bare.TycEnv -> Bare.MeasEnv 
@@ -750,7 +748,7 @@ mkInvariant x z t tr = strengthen (top <$> t) (MkUReft reft mempty mempty)
 
 
 mkReft :: LocSymbol -> Symbol -> SpecType -> SpecType -> Maybe (Symbol, Expr)
-mkReft x z t tr 
+mkReft x z _t tr 
   | Just q <- stripRTypeBase tr
   = let Reft (v, p) = toReft q
         su          = mkSubst [(v, mkEApp x [EVar v])]
@@ -851,14 +849,6 @@ makeMeasEnv env tycEnv sigEnv specs = Bare.MeasEnv
     name          = Bare.tcName        tycEnv
     dms           = Bare.makeDefaultMethods env mts  
     (cls, mts)    = Bare.makeClasses        env sigEnv name specs
-    -- TODO-REBARE: -- xs'      = fst <$> ms'
-
--- checkMeasures :: MSpec SpecType Ghc.DataCon  
--- _checkMeasures ms = checkMeasure <$> ms 
--- checkMeasure m    = F.tracepp msg m 
-  -- where 
-    -- msg         = "CHECK-MEASURES: " ++ F.showpp syms
-    -- syms        = M.keys (Ms.measMap m) ++ M.keys (Ms.cmeasMap m) 
 
 -----------------------------------------------------------------------------------------
 -- | @makeLiftedSpec@ is used to generate the BareSpec object that should be serialized 

src/Language/Haskell/Liquid/Bare/Check.hs

@@ -8,29 +8,15 @@
 module Language.Haskell.Liquid.Bare.Check 
   ( checkGhcSpec
   , checkBareSpec
-  -- , checkTy
-  -- , checkTerminationExpr
   ) where
 
--- import           BasicTypes
--- import           DataCon
--- import           Id
--- import           Name                                      (getSrcSpan)
--- import           Prelude                                   hiding (error)
--- import           TyCon
--- import           Var
--- import qualified SrcLoc
-
 import           Language.Haskell.Liquid.GHC.API          as Ghc hiding (Located) 
 import           Language.Haskell.Liquid.GHC.TypeRep (Type(TyConApp, TyVarTy))
-
 import           Control.Applicative                       ((<|>))
 import           Control.Arrow                             ((&&&))
-
 import           Data.Maybe
 import           Data.Function                             (on)
 import           Text.PrettyPrint.HughesPJ
-
 import qualified Data.List                                 as L
 import qualified Data.HashMap.Strict                       as M
 import qualified Data.HashSet                              as S

src/Language/Haskell/Liquid/Bare/Class.hs

@@ -4,7 +4,6 @@
 {-# LANGUAGE TupleSections     #-}
 {-# LANGUAGE BangPatterns      #-}
 
--- REBARE: formerly, Language.Haskell.Liquid.Bare.Spec
 module Language.Haskell.Liquid.Bare.Class 
   ( makeClasses
   , makeSpecDictionaries
@@ -71,7 +70,6 @@ mkClassE env sigEnv _myName name (RClass cc ss as ms) tc = do
     ms'    = [ (s, rFun "" (RApp cc (flip RVar mempty <$> as) [] mempty) <$> t) | (s, t) <- ms]
     t      = rCls tc as'
 
-
 mkConstr :: Bare.Env -> Bare.SigEnv -> ModName -> LocBareType -> Either UserError LocSpecType     
 mkConstr env sigEnv name = fmap (fmap dropUniv) . Bare.cookSpecTypeE env sigEnv name Bare.GenTV 
   where 
@@ -81,7 +79,6 @@ mkConstr env sigEnv name = fmap (fmap dropUniv) . Bare.cookSpecTypeE env sigEnv
 unClass :: SpecType -> SpecType 
 unClass = snd . bkClass . fourth4 . bkUniv
 
--- formerly, makeSpec
 makeMethod :: Bare.Env -> Bare.SigEnv -> ModName -> (LocSymbol, LocBareType) 
          -> Either UserError (ModName, PlugTV Ghc.Var, LocSpecType)
 makeMethod env sigEnv name (lx, bt) = (name, mbV,) <$> Bare.cookSpecTypeE env sigEnv name mbV bt
@@ -90,7 +87,6 @@ makeMethod env sigEnv name (lx, bt) = (name, mbV,) <$> Bare.cookSpecTypeE env si
             Just v  -> Bare.LqTV v 
             Nothing -> Bare.GenTV 
 
-
 -------------------------------------------------------------------------------
 makeSpecDictionaries :: Bare.Env -> Bare.SigEnv -> ModSpecs -> DEnv Ghc.Var SpecType 
 -------------------------------------------------------------------------------

src/Language/Haskell/Liquid/Bare/DataType.hs

@@ -3,8 +3,7 @@
 {-# LANGUAGE TupleSections     #-}
 
 module Language.Haskell.Liquid.Bare.DataType
-  ( 
-    dataConMap
+  ( dataConMap
 
   -- * Names for accessing Data Constuctors 
   , makeDataConChecker
@@ -33,7 +32,7 @@ import qualified Data.HashMap.Strict                    as M
 import qualified Data.HashSet                           as S
 import qualified Data.Maybe                             as Mb 
 
-import qualified Language.Fixpoint.Types.Visitor        as V
+-- import qualified Language.Fixpoint.Types.Visitor        as V
 import qualified Language.Fixpoint.Types                as F
 import qualified Language.Haskell.Liquid.GHC.Misc       as GM 
 import qualified Language.Haskell.Liquid.GHC.API        as Ghc 
@@ -332,7 +331,7 @@ fieldName d dp x
 
 makeDataFields :: F.TCEmb Ghc.TyCon -> F.FTycon -> [RTyVar] -> [(F.LocSymbol, SpecType)]
                -> [F.DataField]
-makeDataFields tce c as xts = [ F.DField x (fSort t) | (x, t) <- xts]
+makeDataFields tce _c as xts = [ F.DField x (fSort t) | (x, t) <- xts]
   where
     su                      = zip (F.symbol <$> as) [0..]
     fSort                   = {- muSort c (length as) . -}  F.substVars su . RT.rTypeSort tce

src/Language/Haskell/Liquid/Bare/Resolve.hs

@@ -433,7 +433,7 @@ lookupGhcVar env name kind lx =
     Right v -> Mb.fromMaybe v       (lookupLocalVar env lx [v]) 
     Left  e -> Mb.fromMaybe (err e) (lookupLocalVar env lx []) 
   where
-    -- err e   = Misc.errorP "error-lookupGhcVar" (F.showpp e)
+    -- err e   = Misc.errorP "error-lookupGhcVar" (F.showpp (e, F.loc lx, lx))
     err     = Ex.throw
 
 -- | @lookupLocalVar@ takes as input the list of "global" (top-level) vars 

src/Language/Haskell/Liquid/Bare/Types.hs

@@ -125,13 +125,12 @@ type DataConMap = M.HashMap (F.Symbol, Int) F.Symbol
 -------------------------------------------------------------------------------
 -- REBARE: used to be output of makeGhcSpecCHOP2
 data MeasEnv = MeasEnv 
-  { meMeasureSpec :: !(MSpec SpecType Ghc.DataCon)          -- measures
-  , meClassSyms   :: ![(F.Symbol, Located (RRType F.Reft))] -- cms' 
-  , meSyms        :: ![(F.Symbol, Located (RRType F.Reft))] -- ms' 
-  , meDataCons    :: ![(Ghc.Var,  LocSpecType)]             -- cs'
-                                                            -- xs' :: [Symbol] = fst <$> meSyms
-  , meClasses     :: ![DataConP]                            -- cls 
-  , meMethods     :: ![(ModName, Ghc.Var, LocSpecType)]     -- mts 
+  { meMeasureSpec :: !(MSpec SpecType Ghc.DataCon)          
+  , meClassSyms   :: ![(F.Symbol, Located (RRType F.Reft))] 
+  , meSyms        :: ![(F.Symbol, Located (RRType F.Reft))]
+  , meDataCons    :: ![(Ghc.Var,  LocSpecType)]           
+  , meClasses     :: ![DataConP]                           
+  , meMethods     :: ![(ModName, Ghc.Var, LocSpecType)]    
   }
 
 -------------------------------------------------------------------------------

src/Language/Haskell/Liquid/Constraint/Fresh.hs

@@ -42,6 +42,7 @@ import           Language.Haskell.Liquid.Types
 -- import           Language.Haskell.Liquid.Types.RefType
 -- import           Language.Haskell.Liquid.Types.Fresh
 import           Language.Haskell.Liquid.Constraint.Types
+import qualified Language.Haskell.Liquid.GHC.Misc as GM 
 
 --------------------------------------------------------------------------------
 -- | This is all hardwiring stuff to CG ----------------------------------------
@@ -70,7 +71,8 @@ refreshArgsTop (x, t)
 --   Constraint generation should ONLY use @freshTy_type@ and @freshTy_expr@
 
 freshTy_type        :: KVKind -> CoreExpr -> Type -> CG SpecType
-freshTy_type k _ τ  = freshTy_reftype k $ ofType τ
+freshTy_type k e τ  =  F.notracepp ("freshTy_type: " ++ F.showpp k ++ GM.showPpr e) 
+                   <$> freshTy_reftype k (ofType τ)
 
 freshTy_expr        :: KVKind -> CoreExpr -> Type -> CG SpecType
 freshTy_expr k e _  = freshTy_reftype k $ exprRefType e