Remove the WithAssertions syntax constructor and related

typeclass constraints.

crucible/src/Lang/Crucible/CFG/Core.hs

@@ -174,12 +174,10 @@ ppAssignment :: Assignment (Reg ctx) args -> [Doc]
 ppAssignment = toListFC pretty
 
 instance ( TraversableFC (ExprExtension ext)
- , TraversableF (AssertionClassifier ext)
  ) => ApplyEmbedding' (Expr ext) where
  applyEmbedding' ctxe (App e) = App (mapApp (applyEmbedding' ctxe) e)
 
 instance ( TraversableFC (ExprExtension ext)
- , TraversableF (AssertionClassifier ext)
  ) => ExtendContext' (Expr ext) where
  extendContext' diff (App e) = App (mapApp (extendContext' diff) e)
 

crucible/src/Lang/Crucible/CFG/Expr.hs

@@ -71,10 +71,8 @@ import Text.PrettyPrint.ANSI.Leijen hiding ((<$>))
 import qualified Data.Vector as V
 
 import Data.Parameterized.Classes
-import Data.Parameterized.ClassesC (TestEqualityC(..), OrdC(..))
 import qualified Data.Parameterized.Context as Ctx
 import qualified Data.Parameterized.TH.GADT as U
-import Data.Parameterized.TraversableF
 import Data.Parameterized.TraversableFC
 
 import What4.Interface (RoundingMode(..),StringLiteral(..), stringLiteralInfo)
@@ -476,14 +474,6 @@ data App (ext :: Type) (f :: CrucibleType -> Type) (tp :: CrucibleType) where
  -> !(f (StringType Unicode))
  -> App ext f tp
 
-
- ----------------------------------------------------------------------
- -- Side conditions
-
- WithAssertion :: !(TypeRepr tp)
- -> !(PartialExpr ext f tp)
- -> App ext f tp
-
  ----------------------------------------------------------------------
  -- Recursive Types
  RollRecursive :: IsRecursiveType nm
@@ -1129,10 +1119,6 @@ instance TypeApp (ExprExtension ext) => TypeApp (App ext) where
  NothingValue tp -> MaybeRepr tp
  FromJustValue tp _ _ -> tp
 
- ----------------------------------------------------------------------
- -- Side conditions
- WithAssertion tp _ -> tp
-
  ----------------------------------------------------------------------
  -- Recursive Types
 
@@ -1359,7 +1345,6 @@ traverseBaseTerm f = traverseFC (traverseFC f)
 -- subterm of an application. Used for the 'TraversableFC' instance.
 traverseApp :: forall ext m f g tp.
  ( TraversableFC (ExprExtension ext)
- , TraversableF (AssertionClassifier ext)
  , Applicative m
  )
  => (forall u . f u -> m (g u))
@@ -1390,7 +1375,6 @@ traverseApp =
 -- Parameterized Eq and Ord instances
 
 instance ( TestEqualityFC (ExprExtension ext)
- , TestEqualityC (AssertionClassifier ext)
  ) => TestEqualityFC (App ext) where
  testEqualityFC testSubterm =
  $(U.structuralTypeEquality [t|App|]
@@ -1427,14 +1411,11 @@ instance ( TestEqualityFC (ExprExtension ext)
  ])
 
 instance ( TestEqualityFC (ExprExtension ext)
- , TestEqualityC (AssertionClassifier ext)
  , TestEquality f
  ) => TestEquality (App ext f) where
  testEquality = testEqualityFC testEquality
 
 instance ( OrdFC (ExprExtension ext)
- , OrdC (AssertionClassifier ext)
- , TestEqualityC (AssertionClassifier ext)
  ) => OrdFC (App ext) where
  compareFC compareSubterm
  = $(U.structuralTypeOrd [t|App|]
@@ -1472,8 +1453,6 @@ instance ( OrdFC (ExprExtension ext)
  )
 
 instance ( OrdFC (ExprExtension ext)
- , OrdC (AssertionClassifier ext)
- , TestEqualityC (AssertionClassifier ext)
  , OrdF f
  ) => OrdF (App ext f) where
  compareF = compareFC compareF
@@ -1482,23 +1461,19 @@ instance ( OrdFC (ExprExtension ext)
 -- Traversals and such
 
 instance ( TraversableFC (ExprExtension ext)
- , TraversableF (AssertionClassifier ext)
  ) => FunctorFC (App ext) where
  fmapFC = fmapFCDefault
 
 instance ( TraversableFC (ExprExtension ext)
- , TraversableF (AssertionClassifier ext)
  ) => FoldableFC (App ext) where
  foldMapFC = foldMapFCDefault
 
 instance ( TraversableFC (ExprExtension ext)
- , TraversableF (AssertionClassifier ext)
  ) => TraversableFC (App ext) where
  traverseFC = traverseApp
 
 -- | Fold over an application.
 foldApp :: ( TraversableFC (ExprExtension ext)
- , TraversableF (AssertionClassifier ext)
  )
  => (forall x . f x -> r -> r)
  -> r
@@ -1510,7 +1485,6 @@ foldApp f0 r0 a = execState (traverseApp (go f0) a) r0
 -- | Map a Crucible-type-preserving function over the immediate
 -- subterms of an application.
 mapApp :: ( TraversableFC (ExprExtension ext)
- , TraversableF (AssertionClassifier ext)
  )
  => (forall u . f u -> g u) -> App ext f tp -> App ext g tp
 mapApp f a = runIdentity (traverseApp (pure . f) a)

crucible/src/Lang/Crucible/CFG/Extension.hs

@@ -40,13 +40,10 @@ module Lang.Crucible.CFG.Extension
 ) where
 
 import Data.Kind (Type)
-import Data.Parameterized.ClassesC (OrdC(..))
-import Data.Parameterized.TraversableF (TraversableF)
 import Data.Parameterized.TraversableFC
 import Text.PrettyPrint.ANSI.Leijen (Doc)
 
 import Lang.Crucible.Types
-import Lang.Crucible.CFG.Extension.Safety
 
 
 class PrettyApp (app :: (k -> Type) -> k -> Type) where
@@ -66,7 +63,6 @@ type PrettyExt ext =
 type TraverseExt ext =
  ( TraversableFC (ExprExtension ext)
  , TraversableFC (StmtExtension ext)
- , TraversableF (AssertionClassifier ext)
  )
 
 -- | This class captures all the grungy technical capabilities
@@ -86,10 +82,6 @@ class
  , TraversableFC (StmtExtension ext)
  , PrettyApp (StmtExtension ext)
  , TypeApp (StmtExtension ext)
- --
- , OrdC (AssertionClassifier ext)
- , TraversableF (AssertionClassifier ext)
- , HasStructuredAssertions ext
  ) =>
  IsSyntaxExtension ext
 

crucible/src/Lang/Crucible/CFG/SSAConversion.hs

@@ -39,9 +39,7 @@ import Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
 import Data.Maybe (isJust, fromMaybe)
 import qualified Data.Parameterized.Context as Ctx
-import Data.Parameterized.ClassesC (OrdC(..))
 import Data.Parameterized.Some
-import Data.Parameterized.TraversableF (TraversableF)
 import Data.Parameterized.TraversableFC
 import Data.Sequence (Seq)
 import qualified Data.Sequence as Seq
@@ -56,7 +54,6 @@ import What4.ProgramLoc
 import Lang.Crucible.Analysis.Reachable
 import qualified Lang.Crucible.CFG.Core as C
 import qualified Lang.Crucible.CFG.Expr as C
-import qualified Lang.Crucible.CFG.Extension.Safety as C
 import Lang.Crucible.CFG.Reg
 import Lang.Crucible.FunctionHandle
 
@@ -701,8 +698,6 @@ appRegMap_extend = unsafeCoerce
 
 appRegMap_insert :: ( TraversableFC (C.ExprExtension ext)
  , OrdFC (C.ExprExtension ext)
- , TraversableF (C.AssertionClassifier ext)
- , OrdC (C.AssertionClassifier ext)
  )
  => C.App ext (C.Reg ctx) tp
  -> C.Reg (ctx ::> tp) tp
@@ -711,7 +706,6 @@ appRegMap_insert :: ( TraversableFC (C.ExprExtension ext)
 appRegMap_insert k v m = MapF.insert (fmapFC C.extendReg k) v (appRegMap_extend m)
 
 appRegMap_lookup :: ( OrdFC (C.ExprExtension ext)
- , OrdC (C.AssertionClassifier ext)
  )
  => C.App ext (C.Reg ctx) tp
  -> AppRegMap ext ctx

crucible/src/Lang/Crucible/Simulator/Evaluation.hs

@@ -42,10 +42,8 @@ import Control.Monad.Fail( MonadFail )
 import qualified Control.Exception as Ex
 import Control.Lens
 import Control.Monad
-import Data.Bitraversable (bitraverse)
 import qualified Data.Map.Strict as Map
 import Data.Maybe
-import Data.Proxy (Proxy(..))
 import qualified Data.Text as Text
 import qualified Data.Vector as V
 import Data.Word
@@ -54,7 +52,6 @@ import Numeric.Natural
 
 import Data.Parameterized.Classes
 import Data.Parameterized.Context as Ctx
-import Data.Parameterized.TraversableF (TraversableF(traverseF))
 import Data.Parameterized.TraversableFC
 
 import What4.Interface
@@ -66,7 +63,6 @@ import What4.WordMap
 
 import Lang.Crucible.Backend
 import Lang.Crucible.CFG.Expr
-import Lang.Crucible.CFG.Extension.Safety as Safety
 import Lang.Crucible.Simulator.Intrinsics
 import Lang.Crucible.Simulator.RegMap
 import Lang.Crucible.Simulator.SimError
@@ -265,9 +261,6 @@ type EvalAppFunc sym app = forall f.
 -- | Evaluate the application.
 evalApp :: forall sym ext.
  ( IsSymInterface sym
- , HasStructuredAssertions ext
- , TraversableF (AssertionClassifier ext)
- , TraversableFC (PartialExpr ext)
  )
  => sym
  -> IntrinsicTypes sym
@@ -430,27 +423,6 @@ evalApp sym itefns _logFn evalExt (evalSub :: forall tp. f tp -> IO (RegValue sy
  addFailedAssertion sym $
  Unsupported "Symbolic string in fromJustValue"
 
- ----------------------------------------------------------------------
- -- Side conditions
-
- WithAssertion _tyRep (Safety.PartialExp assertions val) -> do
- let (pext, psym) = (Proxy :: Proxy ext, Proxy :: Proxy sym)
-
- -- Evaluate any subexpressions and massage the type parameter into
- -- @'SymExpr' sym@. This works because
- -- @RegValue sym (BaseToType BaseBoolType) = SymExpr sym BaseBoolType@
- assertions' <-
- let rvEval :: forall tp. f tp -> IO (RegValue' sym tp)
- rvEval x = RV <$> evalSub x
- in bitraverse rvEval (traverseF rvEval) assertions
-
- let expl = explainTree pext psym assertions'
- let err = AssertFailureSimError (summarizeTree pext assertions') (show expl)
- addAssertionM sym (treeToPredicate pext sym assertions') err
- evalSub val
-
- WithAssertion _tyRep _ -> error "evalApp: Impossible"
-
  ----------------------------------------------------------------------
  -- Recursive Types