[commit: ghc] wip/ext-solver: Parsing of SMT results back into types. (e7fe976)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : wip/ext-solver
Link       : http://ghc.haskell.org/trac/ghc/changeset/e7fe97661ce2f2bbc562caf94166f9db36c1990e/ghc

>---------------------------------------------------------------

commit e7fe97661ce2f2bbc562caf94166f9db36c1990e
Author: Iavor S. Diatchki <iavor.diatchki at gmail.com>
Date:   Mon Apr 28 19:34:12 2014 -0700

    Parsing of SMT results back into types.


>---------------------------------------------------------------

e7fe97661ce2f2bbc562caf94166f9db36c1990e
 compiler/typecheck/TcTypeNats.hs |   44 +++++++++++++++++++++++++++++++++++---
 1 file changed, 41 insertions(+), 3 deletions(-)

diff --git a/compiler/typecheck/TcTypeNats.hs b/compiler/typecheck/TcTypeNats.hs
index b455efe..17a1037 100644
--- a/compiler/typecheck/TcTypeNats.hs
+++ b/compiler/typecheck/TcTypeNats.hs
@@ -41,10 +41,12 @@ import           Data.Map (Map)
 import qualified Data.Map as Map
 import           Data.Set (Set)
 import qualified Data.Set as Set
-import           Data.Maybe ( isJust )
+import           Data.Maybe ( isJust, mapMaybe )
 import           Data.Char  ( isSpace )
 import           Data.List ( unfoldr, mapAccumL, foldl' )
-import           Data.IORef ( newIORef, atomicModifyIORef', modifyIORef' )
+import           Data.IORef ( newIORef, atomicModifyIORef', modifyIORef'
+                            , readIORef
+                            )
 import           Control.Monad (forever)
 import           Control.Concurrent ( forkIO )
 import qualified Control.Exception as X
@@ -756,7 +758,10 @@ newExternalSolver exe opts =
              case res of
                SAtom "unsat"   -> return ExtSolUnsat
                SAtom "unknown" -> return ExtSolUnknown
-               SAtom "sat" -> undefined
+               SAtom "sat" ->
+                 do vs <- readIORef viRef
+                    model <- smtGetModel proc vs
+                    return (ExtSolSat model)
 
                _ -> unexpected res
 
@@ -766,6 +771,16 @@ newExternalSolver exe opts =
   unexpected e = fail $ "Unexpected response by the solver: " ++
                         (renderSExpr e "")
 
+smtGetModel :: SolverProcess -> VarInfo -> IO [(TyVar,Type)]
+smtGetModel proc vi =
+  do res <- solverDo proc
+          $ SList [ SAtom "get-value", SList [ SAtom v | v <- inScope vi ] ]
+     return $ mapMaybe resolve $ Map.toList $ smtVals res
+  where
+  resolve (x,se) = do tv <- Map.lookup x (smtDeclaredVars vi)
+                      ty <- knownValue se
+                      return (tv,ty)
+
 smtDeclarePerhaps :: VarInfo -> (TyVar, String, Ty) -> (VarInfo, [SExpr])
 smtDeclarePerhaps vi (tv,x,ty) = (vi1, decls)
   where
@@ -868,6 +883,13 @@ knownKind k =
       | tc == typeNatKindCon    -> Just TNat
     _ -> Nothing
 
+knownValue :: Expr -> Maybe Xi
+knownValue expr =
+  case expr of
+    Num x  -> Just (num x)
+    Bool x -> Just (bool x)
+    _      -> Nothing
+
 
 thyVarName :: TyVar -> String
 thyVarName x = occNameString (nameOccName n) ++ "_" ++ show u
@@ -915,6 +937,19 @@ smtDeclare x t = SList [SAtom "declare-fun", SAtom x, SList [], smtTy t]
 smtAssert :: Expr -> SExpr
 smtAssert e = SList [SAtom "assert", smtExpr e]
 
+smtVals :: SExpr -> Map String Expr
+smtVals (SList xs) =
+  Map.fromList [ (x,v) | SList [ SAtom x, SAtom sa ] <- xs, v <- parse sa ]
+  where
+  parse "true"  = [Bool True]
+  parse "false" = [Bool False]
+  parse xs      = [Num x | (x,"") <- reads xs ]
+smtVals _ = Map.empty
+
+
+
+
+
 --------------------------------------------------------------------------------
 
 {-
@@ -955,6 +990,9 @@ emptyVarInfo = VarInfo
   , smtOtherScopes  = []
   }
 
+inScope :: VarInfo -> [String]
+inScope vi = Set.toList $ Set.unions $ smtCurScope vi : smtOtherScopes vi
+
 startScope :: VarInfo -> VarInfo
 startScope vi = vi { smtCurScope    = Set.empty
                    , smtOtherScopes = smtCurScope vi : smtOtherScopes vi }