-- SPDX-FileCopyrightText: 2025 Sören Tempel <soeren+git@soeren-tempel.net>
--
-- SPDX-License-Identifier: GPL-3.0-only
module Language.QBE.Backend.Model
  ( Model,
    toList,
    getModel,
  )
where

import Language.QBE.Simulator.Default.Expression qualified as DE
import SimpleBV qualified as SMT

-- Assignments returned by the Solver for a given query.
newtype Model = Model [(String, SMT.Value)]
  deriving (Int -> Model -> ShowS
[Model] -> ShowS
Model -> String
(Int -> Model -> ShowS)
-> (Model -> String) -> ([Model] -> ShowS) -> Show Model
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Model -> ShowS
showsPrec :: Int -> Model -> ShowS
$cshow :: Model -> String
show :: Model -> String
$cshowList :: [Model] -> ShowS
showList :: [Model] -> ShowS
Show, Model -> Model -> Bool
(Model -> Model -> Bool) -> (Model -> Model -> Bool) -> Eq Model
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Model -> Model -> Bool
== :: Model -> Model -> Bool
$c/= :: Model -> Model -> Bool
/= :: Model -> Model -> Bool
Eq)

-- | Get a new 'Model.Model' for a list of input variables that should be contained in it.
getModel :: SMT.Solver -> [SMT.SExpr] -> IO Model
getModel :: Solver -> [SExpr] -> IO Model
getModel Solver
solver [SExpr]
inputVars = [(String, Value)] -> Model
Model ([(String, Value)] -> Model) -> IO [(String, Value)] -> IO Model
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Solver -> [SExpr] -> IO [(String, Value)]
SMT.getValues Solver
solver [SExpr]
inputVars

-- | Convert a model to a list of concrete variable assignments.
toList :: Model -> [(String, DE.RegVal)]
toList :: Model -> [(String, RegVal)]
toList (Model [(String, Value)]
lst) = ((String, Value) -> (String, RegVal))
-> [(String, Value)] -> [(String, RegVal)]
forall a b. (a -> b) -> [a] -> [b]
map (String, Value) -> (String, RegVal)
go [(String, Value)]
lst
  where
    go :: (String, SMT.Value) -> (String, DE.RegVal)
    go :: (String, Value) -> (String, RegVal)
go (String
name, SMT.Bits Int
n Integer
v) =
      case Int -> Integer -> Maybe RegVal
DE.fromBits Int
n Integer
v of
        Just RegVal
x -> (String
name, RegVal
x)
        Maybe RegVal
Nothing -> String -> (String, RegVal)
forall a. HasCallStack => String -> a
error String
"invalid bitvector size"
    go (String, Value)
_ = String -> (String, RegVal)
forall a. HasCallStack => String -> a
error String
"unsupported value type"