Merge pull request #1623 from pbougou/synthesis

Add basic Synthesis Support

.ghci

@@ -1 +1,2 @@
 :set -isrc
+:set prompt "\ESC[34mλ> \ESC[m"

.gitignore

@@ -36,6 +36,8 @@ cabal.sandbox.config
 .ghc.environment.*
 cabal.project.local
 
+tests/synthesis/logs/*
+!tests/synthesis/logs/.gitkeep
 /tests/logs/
 /.stack-work/
 /.vagrant/

README.md

@@ -1294,7 +1294,7 @@ attaches a refinement to a datatype globally.
 Do not use this mechanism -- it is *unsound* and about to
 deprecated in favor of something that is [actually sound](https://github.com/ucsd-progsys/liquidhaskell/issues/126)
 
-Forexample,  the length of a list cannot be negative
+For example,  the length of a list cannot be negative
 
     {-@ invariant {v:[a] | (len v >= 0)} @-}
 
@@ -1449,6 +1449,54 @@ the specifications you write i.e.
 2. measure bodies and,
 3. data constructor definitions.
 
+Basic support for program synthesis
+===================================
+
+How to use it
+-------------
+
+Activate the flag for typed holes in LiquidHaskell. E.g.
+from command line: 
+
+    liquid --typedholes
+
+In a Haskell source file: 
+
+    {-@ LIQUID --typed-holes @-}
+
+Using the flag for typed holes, two more flags can be used:
+
+- **max-match-depth**: Maximum number of pattern match expressions used during synthesis (default value: 4).
+
+- **max-app-depth**: Maximum number of same function applications used during synthesis (default value: 2).
+
+Having the program specified in a Haskell source file, use 
+GHC' s hole variables, e.g.:
+
+    {-@ myMap :: (a -> b) -> xs:[a] -> {v:[b] | len v == len xs} @-}
+    myMap :: (a -> b) -> [a] -> [b]
+    myMap = _goal
+
+Current limitations
+-------------------
+
+This is an experimental feature, so potential users could only 
+expect to synthesize programs, like [these](https://github.com/ucsd-progsys/liquidhaskell/tree/develop/tests/synth).
+
+Current limitations include:
+
+- No boolean conditionals are synthesized.
+- Holes can only appear at top level, e.g.: 
+
+        {-@ f :: x: [a] -> { v: [a] | v == x } @-}
+        f :: [a] -> [a]
+        -- This works
+        f = _hole
+        -- This does not work
+        f x = _hole
+
+- Only one hole can appear in each module.
+
 
 Generating HTML Output
 ======================

include/Language/Haskell/Liquid/Synthesize/Error.hs

@@ -0,0 +1,5 @@
+module Language.Haskell.Liquid.Synthesize.Error where 
+
+{-@ err :: { v: Int | false } -> a @-}
+err :: Int -> a
+err s = undefined

liquidhaskell.cabal

@@ -41,6 +41,7 @@ data-files:         include/*.hquals
                     include/GHC/*.spec
                     include/GHC/IO/*.spec
                     include/Language/Haskell/Liquid/*.hs
+                    include/Language/Haskell/Liquid/Synthesize/*.hs
                     include/Language/Haskell/Liquid/*.pred
                     include/System/*.spec
                     include/710/Data/*.spec
@@ -120,6 +121,13 @@ library
                       Language.Haskell.Liquid.Parse
                       Language.Haskell.Liquid.Prelude
                       Language.Haskell.Liquid.ProofCombinators
+                      Language.Haskell.Liquid.Synthesize.GHC
+                      Language.Haskell.Liquid.Synthesize.Termination
+                      Language.Haskell.Liquid.Synthesize.Monad
+                      Language.Haskell.Liquid.Synthesize.Misc
+                      Language.Haskell.Liquid.Synthesize.Generate
+                      Language.Haskell.Liquid.Synthesize.Check
+                      Language.Haskell.Liquid.Synthesize.Env
                       Language.Haskell.Liquid.Termination.Structural
                       Language.Haskell.Liquid.Transforms.ANF
                       Language.Haskell.Liquid.Transforms.CoreToLogic
@@ -144,6 +152,7 @@ library
                       Language.Haskell.Liquid.Types.Types
                       Language.Haskell.Liquid.Types.Variance
                       Language.Haskell.Liquid.Types.Visitors
+                      Language.Haskell.Liquid.Synthesize
                       Language.Haskell.Liquid.UX.ACSS
                       Language.Haskell.Liquid.UX.Annotate
                       Language.Haskell.Liquid.UX.CTags
@@ -184,6 +193,7 @@ library
                     , githash
                     , parsec               >= 3.1
                     , pretty               >= 1.1
+                    , split
                     , syb                  >= 0.4.4
                     , template-haskell     >= 2.9
                     , temporary            >= 1.2
@@ -193,8 +203,9 @@ library
                     , transformers         >= 0.3
                     , unordered-containers >= 0.2
                     , vector               >= 0.10
+                    , extra 
   default-language:   Haskell98
-  default-extensions: PatternGuards
+  default-extensions: PatternGuards, RecordWildCards, DoAndIfThenElse
   ghc-options:        -W -fwarn-missing-signatures
 
   if flag(include)
@@ -273,3 +284,22 @@ test-suite liquidhaskell-parser
                   , tasty-hunit     >= 0.9
   default-language: Haskell2010
   ghc-options:      -W
+
+test-suite synthesis
+  type:             exitcode-stdio-1.0
+  main-is:          Synthesis.hs
+  other-modules:    Paths_liquidhaskell
+  hs-source-dirs:   tests
+  build-depends:    base            >= 4.8.1.0 && < 5
+                  , liquid-fixpoint >= 0.8.0.0
+                  , liquidhaskell
+                  , tasty           >= 0.7
+                  , tasty-hunit
+                  , process
+                  , filepath
+                  , text
+                  , directory 
+                  , ghc
+                  , extra
+  default-language: Haskell2010
+  ghc-options:      -W

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

@@ -18,7 +18,7 @@
 -- | This module defines the representation of Subtyping and WF Constraints,
 --   and the code for syntax-directed constraint generation.
 
-module Language.Haskell.Liquid.Constraint.Generate ( generateConstraints ) where
+module Language.Haskell.Liquid.Constraint.Generate ( generateConstraints, generateConstraintsWithEnv, caseEnv, consE ) where
 
 import           Outputable                                    (Outputable)
 import           Prelude                                       hiding (error)
@@ -76,6 +76,7 @@ import           Language.Haskell.Liquid.Transforms.CoreToLogic (weakenResult)
 import           Language.Haskell.Liquid.Bare.DataType (makeDataConChecker)
 
 import           Language.Haskell.Liquid.Types hiding (binds, Loc, loc, Def)
+import Debug.Trace
 
 --------------------------------------------------------------------------------
 -- | Constraint Generation: Toplevel -------------------------------------------
@@ -84,12 +85,18 @@ generateConstraints      :: TargetInfo -> CGInfo
 --------------------------------------------------------------------------------
 generateConstraints info = {-# SCC "ConsGen" #-} execState act $ initCGI cfg info
   where
-    act                  = consAct cfg info
+    act                  = do { γ <- initEnv info; consAct γ cfg info }
     cfg                  = getConfig   info
 
-consAct :: Config -> TargetInfo -> CG ()
-consAct cfg info = do
-  γ       <- initEnv      info
+generateConstraintsWithEnv :: TargetInfo -> CGInfo -> CGEnv -> CGInfo
+--------------------------------------------------------------------------------
+generateConstraintsWithEnv info cgi γ = {-# SCC "ConsGenEnv" #-} execState act cgi
+  where
+    act                  = consAct γ cfg info
+    cfg                  = getConfig   info
+
+consAct :: CGEnv -> Config -> TargetInfo -> CG ()
+consAct γ cfg info = do
   let sSpc = gsSig . giSpec $ info  
   let gSrc = giSrc info
   when (gradual cfg) (mapM_ (addW . WfC γ . val . snd) (gsTySigs sSpc ++ gsAsmSigs sSpc))
@@ -191,10 +198,11 @@ makeRecType :: (Enum a1, Eq a1, Num a1, F.Symbolic a)
 makeRecType autoenv t vs dxs is
   = mergecondition t $ fromRTypeRep $ trep {ty_binds = xs', ty_args = ts'}
   where
-    (xs', ts') = unzip $ replaceN (last is) (makeDecrType autoenv vdxs) xts
+    (xs', ts') = unzip $ replaceN (last is) (fromLeft $ makeDecrType autoenv vdxs) xts
     vdxs       = zip vs dxs
     xts        = zip (ty_binds trep) (ty_args trep)
     trep       = toRTypeRep $ unOCons t
+    fromLeft (Left x) = x 
 
 unOCons :: RType c tv r -> RType c tv r
 unOCons (RAllT v t r)      = RAllT v (unOCons t) r 
@@ -425,6 +433,9 @@ consCB _ _ γ (NonRec x _) | isDictionary x
        isDictionary = isJust . dlookup (denv γ)
 
 
+consCB _ _ γ (NonRec x _ ) | isHoleVar x && typedHoles (getConfig γ)
+  = return γ 
+
 consCB _ _ γ (NonRec x def)
   | Just (w, τ) <- grepDictionary def
   , Just d      <- dlookup (denv γ) w
@@ -673,9 +684,9 @@ cconsE' γ (Var x) t | isHoleVar x && typedHoles (getConfig γ)
   = addHole x t γ 
 
 cconsE' γ e t
-  = do te  <- consE γ e
-       te' <- instantiatePreds γ e te >>= addPost γ
-       addC (SubC γ te' t) ("cconsE: " ++ "\n t = " ++ showpp t ++ "\n te = " ++ showpp te ++ GM.showPpr e)
+  = do  te  <- consE γ e
+        te' <- instantiatePreds γ e te >>= addPost γ
+        addC (SubC γ te' t) ("cconsE: " ++ "\n t = " ++ showpp t ++ "\n te = " ++ showpp te ++ GM.showPpr e)
 
 lambdaSingleton :: CGEnv -> F.TCEmb TyCon -> Var -> CoreExpr -> UReft F.Reft
 lambdaSingleton γ tce x e

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

@@ -29,6 +29,7 @@ import           Language.Fixpoint.Misc hiding (errorstar)
 import           Language.Haskell.Liquid.GHC.Misc -- (concatMapM)
 import           Language.Haskell.Liquid.GHC.SpanStack (srcSpan)
 import qualified Language.Haskell.Liquid.GHC.API            as Ghc
+import qualified Language.Fixpoint.Types                    as F
 
 --------------------------------------------------------------------------------
 -- | `addC` adds a subtyping constraint into the global pool.
@@ -102,14 +103,17 @@ addLocA !xo !l !t
 -- | Used for annotating holes 
 
 addHole :: Var -> SpecType -> CGEnv -> CG () 
-addHole x t γ = do 
-  modify $ \s -> s {holesMap = M.insertWith (<>) x hinfo $ holesMap s}
-  addWarning $ ErrHole loc ("hole found") (reGlobal env <> reLocal env) x' t 
+addHole x t γ 
+  | typedHoles (getConfig γ) = 
+      do  st <- get 
+          modify $ \s -> s {holesMap = M.insert x (hinfo (st, γ)) $ holesMap s}
+          -- addWarning $ ErrHole loc ("hole found") (reGlobal env <> reLocal env) x' t 
+  | otherwise = return ()
     where 
-      hinfo = [HoleInfo t loc env]
+      hinfo = HoleInfo t loc env
       loc   = srcSpan $ cgLoc γ
       env   = mconcat [renv γ, grtys γ, assms γ, intys γ]
-      x'    = text $ showSDoc $ Ghc.pprNameUnqualified $ Ghc.getName x
+      x'    = F.symbol x -- text $ showSDoc $ Ghc.pprNameUnqualified $ Ghc.getName x
 
 --------------------------------------------------------------------------------
 -- | Update annotations for a location, due to (ghost) predicate applications

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

@@ -181,7 +181,7 @@ data CGInfo = CGInfo
   , binds      :: !F.BindEnv                   -- ^ set of environment binders
   , ebinds     :: ![F.BindId]                  -- ^ existentials
   , annotMap   :: !(AnnInfo (Annot SpecType))  -- ^ source-position annotation map
-  , holesMap   :: !(M.HashMap Var [HoleInfo SpecType])    -- ^ information for ghc hole expressions
+  , holesMap   :: !(M.HashMap Var (HoleInfo (CGInfo, CGEnv) SpecType))    -- ^ information for ghc hole expressions
   , tyConInfo  :: !TyConMap                    -- ^ information about type-constructors
   , specDecr   :: ![(Var, [Int])]              -- ^ ^ Lexicographic order of decreasing args (DEPRECATED) 
   , newTyEnv   :: !(M.HashMap TC.TyCon SpecType)        -- ^ Mapping of new type type constructors with their refined types.

src/Language/Haskell/Liquid/Liquid.hs

@@ -1,6 +1,7 @@
 {-# LANGUAGE NamedFieldPuns      #-}
 {-# LANGUAGE TupleSections       #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE RecordWildCards     #-}
 
 {-@ LIQUID "--diff"     @-}
 
@@ -37,6 +38,8 @@ import           Language.Haskell.Liquid.Misc
 import           Language.Fixpoint.Misc
 import           Language.Fixpoint.Solver
 import qualified Language.Fixpoint.Types as F
+import           Language.Haskell.Liquid.Types
+import           Language.Haskell.Liquid.Synthesize (synthesize)
 import           Language.Haskell.Liquid.Types.RefType (applySolution)
 import           Language.Haskell.Liquid.UX.Errors
 import           Language.Haskell.Liquid.UX.CmdLine
@@ -221,7 +224,6 @@ updTargetInfoTermVars i  = updInfo i  (ST.terminationVars i)
     updSpec   sp   vs = sp   { gsTerm = updSpTerm (gsTerm sp)   vs }
     updSpTerm gsT  vs = gsT  { gsNonStTerm = S.fromList vs         } 
 
-
 dumpCs :: CGInfo -> IO ()
 dumpCs cgi = do
   putStrLn "***************************** SubCs *******************************"
@@ -234,25 +236,29 @@ dumpCs cgi = do
 pprintMany :: (PPrint a) => [a] -> Doc
 pprintMany xs = vcat [ F.pprint x $+$ text " " | x <- xs ]
 
-instance Show Cinfo where
-  show = show . F.toFix
-
 solveCs :: Config -> FilePath -> CGInfo -> TargetInfo -> Maybe [String] -> IO (Output Doc)
 solveCs cfg tgt cgi info names = do
   finfo            <- cgInfoFInfo info cgi
-  F.Result r0 sol _ <- solve (fixConfig tgt cfg) finfo
+  let fcfg          = fixConfig tgt cfg
+  F.Result r0 sol _ <- solve fcfg finfo
   let failBs        = gsFail $ gsTerm $ giSpec info
   let (r,rf)        = splitFails (S.map val failBs) r0 
   let resErr        = applySolution sol . cinfoError . snd <$> r
   -- resModel_        <- fmap (e2u cfg sol) <$> getModels info cfg resErr
   let resModel_     = e2u cfg sol <$> resErr
-  let resModel      = resModel_  `addErrors` (e2u cfg sol <$> logErrors cgi)
+  let resModel'     = resModel_  `addErrors` (e2u cfg sol <$> logErrors cgi)
                                  `addErrors` makeFailErrors (S.toList failBs) rf 
-                                 `addErrors` makeFailUseErrors (S.toList failBs) (giCbs $ giSrc info) 
+                                 `addErrors` makeFailUseErrors (S.toList failBs) (giCbs $ giSrc info)
+  let lErrors       = applySolution sol <$> logErrors cgi
+  hErrors          <- if (typedHoles cfg) 
+                        then synthesize tgt fcfg (cgi{holesMap = applySolution sol <$> holesMap  cgi}) 
+                        else return [] 
+  let resModel      = resModel' `addErrors` (e2u cfg sol <$> (lErrors ++ hErrors)) 
   let out0          = mkOutput cfg resModel sol (annotMap cgi)
   return            $ out0 { o_vars    = names    }
                            { o_result  = resModel }
 
+
 e2u :: Config -> F.FixSolution -> Error -> UserError
 e2u cfg s = fmap F.pprint . tidyError cfg s