<commit_before>{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module SAWServer.Eval
  ( evalInt
  , evalIntDescr
  , evalBool
  , evalBoolDescr
  ) where

import Control.Exception ( throw )
import Control.Lens ( view )
import Control.Monad.IO.Class ( MonadIO(liftIO) )
import Data.Aeson
    ( (.:),
      withObject,
      object,
      FromJSON(parseJSON),
      KeyValue((.=)),
      ToJSON(toJSON) )

import qualified Argo
import qualified Argo.Doc as Doc
import CryptolServer.Data.Expression ( Expression(..), getCryptolExpr )
import Verifier.SAW.TypedTerm (TypedTerm)
import qualified SAWScript.Builtins as SB
import qualified SAWScript.Value as SV
import SAWServer
    ( SAWState,
      sawBIC,
      sawTopLevelRW)
import SAWServer.CryptolExpression ( CryptolModuleException(..), getTypedTermOfCExp )
import SAWServer.TopLevel ( tl )

-- The phantom type here is used to prevent a functional dependency conflict when
-- writing instances of Doc.DescribedMethod, and should match the type parameter
-- of EvalResult
data EvalParams evalty cryptolExpr =
  EvalParams
  { evalExpr :: cryptolExpr
  }

instance (FromJSON cryptolExpr) => FromJSON (EvalParams a cryptolExpr) where
  parseJSON =
    withObject "SAW/eval params" $ \o ->
    EvalParams <$> o .: "expr"

data EvalResult evalty =
  EvalResult
  { evalValue :: evalty
  }

instance ToJSON a => ToJSON (EvalResult a) where
  toJSON r = object [ "value" .= evalValue r ]

instance Doc.DescribedMethod (EvalParams Integer cryptolExpr) (EvalResult Integer) where
  parameterFieldDescription =
    [ ("expr",
       Doc.Paragraph [Doc.Text "The Cryptol expression to evaluate."])
    ]
  resultFieldDescription =
    [ ("value",
      Doc.Paragraph [Doc.Text "The integer value of the expresssion."])
    ]

instance Doc.DescribedMethod (EvalParams Bool cryptolExpr) (EvalResult Bool) where
  parameterFieldDescription =
    [ ("expr",
       Doc.Paragraph [Doc.Text "The Cryptol expression to evaluate."])
    ]
  resultFieldDescription =
    [ ("value",
      Doc.Paragraph [Doc.Text "The boolean value of the expresssion."])
    ]

eval :: (TypedTerm -> SV.TopLevel a) -> EvalParams a Expression -> Argo.Command SAWState (EvalResult a)
eval f params = do
  state <- Argo.getState
  fileReader <- Argo.getFileReader
  let cenv = SV.rwCryptol (view sawTopLevelRW state)
      bic = view sawBIC state
  cexp <- getCryptolExpr $ evalExpr params
  (eterm, warnings) <- liftIO $ getTypedTermOfCExp fileReader (SV.biSharedContext bic) cenv cexp
  t <- case eterm of
         Right (t, _) -> return t -- TODO: report warnings
         Left err -> throw $ CryptolModuleException err warnings
  i <- tl $ f t
  pure $ EvalResult i

evalIntDescr :: Doc.Block
evalIntDescr =
  Doc.Paragraph [ Doc.Text "Attempt to evaluate the given term to a concrete integer." ]

evalInt :: EvalParams Integer Expression -> Argo.Command SAWState (EvalResult Integer)
evalInt = eval SB.eval_int

evalBoolDescr :: Doc.Block
evalBoolDescr =
  Doc.Paragraph [ Doc.Text "Attempt to evaluate the given term to a concrete boolean." ]

evalBool :: EvalParams Bool Expression -> Argo.Command SAWState (EvalResult Bool)
evalBool = eval SB.eval_bool
<commit_msg>data -> newtype<commit_after>{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module SAWServer.Eval
  ( evalInt
  , evalIntDescr
  , evalBool
  , evalBoolDescr
  ) where

import Control.Exception ( throw )
import Control.Lens ( view )
import Control.Monad.IO.Class ( MonadIO(liftIO) )
import Data.Aeson
    ( (.:),
      withObject,
      object,
      FromJSON(parseJSON),
      KeyValue((.=)),
      ToJSON(toJSON) )

import qualified Argo
import qualified Argo.Doc as Doc
import CryptolServer.Data.Expression ( Expression(..), getCryptolExpr )
import Verifier.SAW.TypedTerm (TypedTerm)
import qualified SAWScript.Builtins as SB
import qualified SAWScript.Value as SV
import SAWServer
    ( SAWState,
      sawBIC,
      sawTopLevelRW)
import SAWServer.CryptolExpression ( CryptolModuleException(..), getTypedTermOfCExp )
import SAWServer.TopLevel ( tl )

-- The phantom type here is used to prevent a functional dependency conflict when
-- writing instances of Doc.DescribedMethod, and should match the type parameter
-- of EvalResult
newtype EvalParams evalty cryptolExpr =
  EvalParams
  { evalExpr :: cryptolExpr
  }

instance (FromJSON cryptolExpr) => FromJSON (EvalParams a cryptolExpr) where
  parseJSON =
    withObject "SAW/eval params" $ \o ->
    EvalParams <$> o .: "expr"

newtype EvalResult evalty =
  EvalResult
  { evalValue :: evalty
  }

instance ToJSON a => ToJSON (EvalResult a) where
  toJSON r = object [ "value" .= evalValue r ]

instance Doc.DescribedMethod (EvalParams Integer cryptolExpr) (EvalResult Integer) where
  parameterFieldDescription =
    [ ("expr",
       Doc.Paragraph [Doc.Text "The Cryptol expression to evaluate."])
    ]
  resultFieldDescription =
    [ ("value",
      Doc.Paragraph [Doc.Text "The integer value of the expresssion."])
    ]

instance Doc.DescribedMethod (EvalParams Bool cryptolExpr) (EvalResult Bool) where
  parameterFieldDescription =
    [ ("expr",
       Doc.Paragraph [Doc.Text "The Cryptol expression to evaluate."])
    ]
  resultFieldDescription =
    [ ("value",
      Doc.Paragraph [Doc.Text "The boolean value of the expresssion."])
    ]

eval :: (TypedTerm -> SV.TopLevel a) -> EvalParams a Expression -> Argo.Command SAWState (EvalResult a)
eval f params = do
  state <- Argo.getState
  fileReader <- Argo.getFileReader
  let cenv = SV.rwCryptol (view sawTopLevelRW state)
      bic = view sawBIC state
  cexp <- getCryptolExpr $ evalExpr params
  (eterm, warnings) <- liftIO $ getTypedTermOfCExp fileReader (SV.biSharedContext bic) cenv cexp
  t <- case eterm of
         Right (t, _) -> return t -- TODO: report warnings
         Left err -> throw $ CryptolModuleException err warnings
  i <- tl $ f t
  pure $ EvalResult i

evalIntDescr :: Doc.Block
evalIntDescr =
  Doc.Paragraph [ Doc.Text "Attempt to evaluate the given term to a concrete integer." ]

evalInt :: EvalParams Integer Expression -> Argo.Command SAWState (EvalResult Integer)
evalInt = eval SB.eval_int

evalBoolDescr :: Doc.Block
evalBoolDescr =
  Doc.Paragraph [ Doc.Text "Attempt to evaluate the given term to a concrete boolean." ]

evalBool :: EvalParams Bool Expression -> Argo.Command SAWState (EvalResult Bool)
evalBool = eval SB.eval_bool

{'fraction_non_alphanumeric': 0.09662853702588801, 'fraction_numerical': 0.0, 'mean_word_length': 3.6795774647887325, 'pattern_counts': {'":': 0, '<': 17, '<?xml version=': 0, '>': 26, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '957596', 'n_tokens_mistral': 2076, 'n_tokens_neox': 2023, 'n_words': 621}