{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE UndecidableInstances #-}

{- |
This module provides the types 'Solution' and 'Result'.

External SMT-Solvers responses are parsed into these types.
-}
module Language.Hasmtlib.Type.Solution
(
  -- * Result
  Result(..)

  -- * Solution
, Solution
, OrdHaskellType
, SomeKnownOrdSMTSort
, fromSomeVarSols

  -- ** IntValueMap
, IntValueMap(..)

  -- ** SMTVarVol
  -- *** Type
, SMTVarSol(..)

  -- *** Lens
, solVar, solVal

)
where

import Language.Hasmtlib.Type.Expr
import Language.Hasmtlib.Type.Value
import Language.Hasmtlib.Type.SMTSort
import Data.IntMap as IMap hiding (foldl)
import Data.Dependent.Map as DMap
import Data.Dependent.Map.Lens
import Data.Some.Constraint
import Control.Lens

-- | Results of check-sat commands.
data Result = Unsat | Unknown | Sat deriving (Int -> Result -> ShowS
[Result] -> ShowS
Result -> String
(Int -> Result -> ShowS)
-> (Result -> String) -> ([Result] -> ShowS) -> Show Result
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Result -> ShowS
showsPrec :: Int -> Result -> ShowS
$cshow :: Result -> String
show :: Result -> String
$cshowList :: [Result] -> ShowS
showList :: [Result] -> ShowS
Show, Result -> Result -> Bool
(Result -> Result -> Bool)
-> (Result -> Result -> Bool) -> Eq Result
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Result -> Result -> Bool
== :: Result -> Result -> Bool
$c/= :: Result -> Result -> Bool
/= :: Result -> Result -> Bool
Eq, Eq Result
Eq Result =>
(Result -> Result -> Ordering)
-> (Result -> Result -> Bool)
-> (Result -> Result -> Bool)
-> (Result -> Result -> Bool)
-> (Result -> Result -> Bool)
-> (Result -> Result -> Result)
-> (Result -> Result -> Result)
-> Ord Result
Result -> Result -> Bool
Result -> Result -> Ordering
Result -> Result -> Result
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Result -> Result -> Ordering
compare :: Result -> Result -> Ordering
$c< :: Result -> Result -> Bool
< :: Result -> Result -> Bool
$c<= :: Result -> Result -> Bool
<= :: Result -> Result -> Bool
$c> :: Result -> Result -> Bool
> :: Result -> Result -> Bool
$c>= :: Result -> Result -> Bool
>= :: Result -> Result -> Bool
$cmax :: Result -> Result -> Result
max :: Result -> Result -> Result
$cmin :: Result -> Result -> Result
min :: Result -> Result -> Result
Ord)

type Solution = DMap SSMTSort IntValueMap

-- | Newtype for 'IntMap' 'Value' so we can use it as right-hand-side of 'DMap'.
newtype IntValueMap t = IntValueMap (IntMap (Value t))
  deriving newtype (NonEmpty (IntValueMap t) -> IntValueMap t
IntValueMap t -> IntValueMap t -> IntValueMap t
(IntValueMap t -> IntValueMap t -> IntValueMap t)
-> (NonEmpty (IntValueMap t) -> IntValueMap t)
-> (forall b. Integral b => b -> IntValueMap t -> IntValueMap t)
-> Semigroup (IntValueMap t)
forall b. Integral b => b -> IntValueMap t -> IntValueMap t
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
forall (t :: SMTSort). NonEmpty (IntValueMap t) -> IntValueMap t
forall (t :: SMTSort).
IntValueMap t -> IntValueMap t -> IntValueMap t
forall (t :: SMTSort) b.
Integral b =>
b -> IntValueMap t -> IntValueMap t
$c<> :: forall (t :: SMTSort).
IntValueMap t -> IntValueMap t -> IntValueMap t
<> :: IntValueMap t -> IntValueMap t -> IntValueMap t
$csconcat :: forall (t :: SMTSort). NonEmpty (IntValueMap t) -> IntValueMap t
sconcat :: NonEmpty (IntValueMap t) -> IntValueMap t
$cstimes :: forall (t :: SMTSort) b.
Integral b =>
b -> IntValueMap t -> IntValueMap t
stimes :: forall b. Integral b => b -> IntValueMap t -> IntValueMap t
Semigroup, Semigroup (IntValueMap t)
IntValueMap t
Semigroup (IntValueMap t) =>
IntValueMap t
-> (IntValueMap t -> IntValueMap t -> IntValueMap t)
-> ([IntValueMap t] -> IntValueMap t)
-> Monoid (IntValueMap t)
[IntValueMap t] -> IntValueMap t
IntValueMap t -> IntValueMap t -> IntValueMap t
forall a.
Semigroup a =>
a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
forall (t :: SMTSort). Semigroup (IntValueMap t)
forall (t :: SMTSort). IntValueMap t
forall (t :: SMTSort). [IntValueMap t] -> IntValueMap t
forall (t :: SMTSort).
IntValueMap t -> IntValueMap t -> IntValueMap t
$cmempty :: forall (t :: SMTSort). IntValueMap t
mempty :: IntValueMap t
$cmappend :: forall (t :: SMTSort).
IntValueMap t -> IntValueMap t -> IntValueMap t
mappend :: IntValueMap t -> IntValueMap t -> IntValueMap t
$cmconcat :: forall (t :: SMTSort). [IntValueMap t] -> IntValueMap t
mconcat :: [IntValueMap t] -> IntValueMap t
Monoid)

deriving stock instance Show (Value t) => Show (IntValueMap t)

-- | A solution for a single variable.
data SMTVarSol (t :: SMTSort) = SMTVarSol
  { forall (t :: SMTSort). SMTVarSol t -> SMTVar t
_solVar :: SMTVar t                       -- ^ A variable in the SMT-Problem
  , forall (t :: SMTSort). SMTVarSol t -> Value t
_solVal :: Value t                        -- ^ An assignment for this variable in a solution
  }
$(makeLenses ''SMTVarSol)
deriving stock instance Show (Value t) => Show (SMTVarSol t)

-- | Alias class for constraint 'Ord' ('HaskellType' t)
class Ord (HaskellType t) => OrdHaskellType t
instance Ord (HaskellType t) => OrdHaskellType t

-- | An existential wrapper that hides some known 'SMTSort' with an 'Ord' 'HaskellType'
type SomeKnownOrdSMTSort f = Somes1 '[(~) f] '[KnownSMTSort, OrdHaskellType]

-- | Create a 'Solution' from some 'SMTVarSol's.
fromSomeVarSols :: [SomeKnownOrdSMTSort SMTVarSol] -> Solution
fromSomeVarSols :: [SomeKnownOrdSMTSort SMTVarSol] -> Solution
fromSomeVarSols = (Solution -> SomeKnownOrdSMTSort SMTVarSol -> Solution)
-> Solution -> [SomeKnownOrdSMTSort SMTVarSol] -> Solution
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl
  (\Solution
dsol (Some1 f a
s) -> let sSort :: SSMTSort a
sSort = f a -> SSMTSort a
forall (prxy :: SMTSort -> *) (t :: SMTSort).
KnownSMTSort t =>
prxy t -> SSMTSort t
sortSing' f a
s in
    Solution
dsol Solution -> (Solution -> Solution) -> Solution
forall a b. a -> (a -> b) -> b
& SSMTSort a
-> (Maybe (IntValueMap a) -> Identity (Maybe (IntValueMap a)))
-> Solution
-> Identity Solution
forall {k1} (k2 :: k1 -> *) (f :: * -> *) (v :: k1) (g :: k1 -> *).
(GCompare k2, Functor f) =>
k2 v
-> (Maybe (g v) -> f (Maybe (g v))) -> DMap k2 g -> f (DMap k2 g)
dmat SSMTSort a
sSort ((Maybe (IntValueMap a) -> Identity (Maybe (IntValueMap a)))
 -> Solution -> Identity Solution)
-> (Maybe (IntValueMap a) -> Maybe (IntValueMap a))
-> Solution
-> Solution
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~
      (\case
        Maybe (IntValueMap a)
Nothing -> IntValueMap a -> Maybe (IntValueMap a)
forall a. a -> Maybe a
Just (IntValueMap a -> Maybe (IntValueMap a))
-> IntValueMap a -> Maybe (IntValueMap a)
forall a b. (a -> b) -> a -> b
$ IntMap (Value a) -> IntValueMap a
forall (t :: SMTSort). IntMap (Value t) -> IntValueMap t
IntValueMap (IntMap (Value a) -> IntValueMap a)
-> IntMap (Value a) -> IntValueMap a
forall a b. (a -> b) -> a -> b
$ Int -> Value a -> IntMap (Value a)
forall a. Int -> a -> IntMap a
IMap.singleton (f a
sf a -> Getting Int (f a) Int -> Int
forall s a. s -> Getting a s a -> a
^.(SMTVar a -> Const Int (SMTVar a)) -> f a -> Const Int (f a)
(SMTVar a -> Const Int (SMTVar a))
-> SMTVarSol a -> Const Int (SMTVarSol a)
forall (t :: SMTSort) (f :: * -> *).
Functor f =>
(SMTVar t -> f (SMTVar t)) -> SMTVarSol t -> f (SMTVarSol t)
solVar((SMTVar a -> Const Int (SMTVar a)) -> f a -> Const Int (f a))
-> ((Int -> Const Int Int) -> SMTVar a -> Const Int (SMTVar a))
-> Getting Int (f a) Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Int -> Const Int Int) -> SMTVar a -> Const Int (SMTVar a)
forall (t1 :: SMTSort) (t2 :: SMTSort) (p :: * -> * -> *)
       (f :: * -> *).
(Profunctor p, Functor f) =>
p Int (f Int) -> p (SMTVar t1) (f (SMTVar t2))
varId) (f a
sf a -> Getting (Value a) (f a) (Value a) -> Value a
forall s a. s -> Getting a s a -> a
^.Getting (Value a) (f a) (Value a)
(Value a -> Const (Value a) (Value a))
-> SMTVarSol a -> Const (Value a) (SMTVarSol a)
forall (t :: SMTSort) (f :: * -> *).
Functor f =>
(Value t -> f (Value t)) -> SMTVarSol t -> f (SMTVarSol t)
solVal)
        Just (IntValueMap IntMap (Value a)
im) -> IntValueMap a -> Maybe (IntValueMap a)
forall a. a -> Maybe a
Just (IntValueMap a -> Maybe (IntValueMap a))
-> IntValueMap a -> Maybe (IntValueMap a)
forall a b. (a -> b) -> a -> b
$ IntMap (Value a) -> IntValueMap a
forall (t :: SMTSort). IntMap (Value t) -> IntValueMap t
IntValueMap (IntMap (Value a) -> IntValueMap a)
-> IntMap (Value a) -> IntValueMap a
forall a b. (a -> b) -> a -> b
$ Int -> Value a -> IntMap (Value a) -> IntMap (Value a)
forall a. Int -> a -> IntMap a -> IntMap a
IMap.insert (f a
sf a -> Getting Int (f a) Int -> Int
forall s a. s -> Getting a s a -> a
^.(SMTVar a -> Const Int (SMTVar a)) -> f a -> Const Int (f a)
(SMTVar a -> Const Int (SMTVar a))
-> SMTVarSol a -> Const Int (SMTVarSol a)
forall (t :: SMTSort) (f :: * -> *).
Functor f =>
(SMTVar t -> f (SMTVar t)) -> SMTVarSol t -> f (SMTVarSol t)
solVar((SMTVar a -> Const Int (SMTVar a)) -> f a -> Const Int (f a))
-> ((Int -> Const Int Int) -> SMTVar a -> Const Int (SMTVar a))
-> Getting Int (f a) Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Int -> Const Int Int) -> SMTVar a -> Const Int (SMTVar a)
forall (t1 :: SMTSort) (t2 :: SMTSort) (p :: * -> * -> *)
       (f :: * -> *).
(Profunctor p, Functor f) =>
p Int (f Int) -> p (SMTVar t1) (f (SMTVar t2))
varId) (f a
sf a -> Getting (Value a) (f a) (Value a) -> Value a
forall s a. s -> Getting a s a -> a
^.Getting (Value a) (f a) (Value a)
(Value a -> Const (Value a) (Value a))
-> SMTVarSol a -> Const (Value a) (SMTVarSol a)
forall (t :: SMTSort) (f :: * -> *).
Functor f =>
(Value t -> f (Value t)) -> SMTVarSol t -> f (SMTVarSol t)
solVal) IntMap (Value a)
im
      )
  )
  Solution
forall a. Monoid a => a
mempty