GaloisInc/what4
1
1
Fork 0
mirror of https://github.com/GaloisInc/what4.git synced 2024-11-29 05:45:01 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #117 from GaloisInc/dm/groundfix

Browse Source 
Avoid spurious failure when grounding NonceApps
This commit is contained in:
Daniel Matichuk 2021-05-04 16:09:25 -07:00 committed by GitHub
commit 7b51ca3cdb
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 7 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
what4/src/What4/Expr/GroundEval.hs
View File

@ -39,10 +39,6 @@ module What4.Expr.GroundEval
, groundEq
) where
#if !MIN_VERSION_base(4,13,0)
import Control.Monad.Fail( MonadFail )
#endif
import Control.Monad
import Control.Monad.Trans.Class
import Control.Monad.Trans.Maybe
@ -186,19 +182,19 @@ tryEvalGroundExpr _ (BoundVarExpr _) = mzero
-- | Helper function for evaluating @NonceApp@ expressions.
--
-- This function is intended for implementers of symbolic backends.
evalGroundNonceApp :: MonadFail m
evalGroundNonceApp :: Monad m
=> (forall u . Expr t u -> MaybeT m (GroundValue u))
-> NonceApp t (Expr t) tp
-> MaybeT m (GroundValue tp)
evalGroundNonceApp fn a0 =
case a0 of
Annotation _ _ t -> fn t
Forall{} -> lift $ fail $ "The ground evaluator does not support quantifiers."
Exists{} -> lift $ fail $ "The ground evaluator does not support quantifiers."
MapOverArrays{} -> lift $ fail $ "The ground evaluator does not support mapping arrays from arbitrary functions."
ArrayFromFn{} -> lift $ fail $ "The ground evaluator does not support arrays from arbitrary functions."
ArrayTrueOnEntries{} -> lift $ fail $ "The ground evaluator does not support arrayTrueOnEntries."
FnApp{} -> lift $ fail $ "The ground evaluator does not support function applications."
Forall{} -> mzero
Exists{} -> mzero
MapOverArrays{} -> mzero
ArrayFromFn{} -> mzero
ArrayTrueOnEntries{} -> mzero
FnApp{} -> mzero
{-# INLINABLE evalGroundApp #-}