convert SingleNodeEntry to be a specialization of NodeEntry'

src/Data/Quant.hs

@@ -64,6 +64,7 @@ module Data.Quant
     , pattern Single
     , viewQuantEach
     , pattern QuantEach
+    , AsSingle(..)
   ) where
 
 import           Prelude hiding (map, traverse)
@@ -287,38 +288,37 @@ instance (HasReprK k, forall x. Ord (f x)) => Ord (Quant (f :: k -> Type) tp) wh
 
 -- Defining which conversions are always possible
 class ToQuant f (t1 :: QuantK k) (t2 :: QuantK k) where
-    toQuant :: f t1 -> QuantRepr t2 -> f t2
+    toQuant :: QuantRepr t2  -> f t1 -> f t2
 
 -- Can take a universally quantified variant to any variant
 instance HasReprK k => ToQuant (Quant f) AllK (tp :: QuantK k) where
-    toQuant z@(QuantAll f) repr = case repr of
+    toQuant repr z@(QuantAll f) = case repr of
         QuantOneRepr baserepr -> QuantOne baserepr (TMF.apply f baserepr)
         QuantAllRepr -> QuantAll f
         QuantSomeRepr -> QuantSome z
 
 -- Can take any variant to an existentially quantified variant
 instance ToQuant (Quant f) (tp :: QuantK k) ExistsK where
-    toQuant z _ = case z of
+    toQuant _ z = case z of
         QuantSome{} -> z
         _ -> QuantSome z
 
 -- Can always take a variant to the same kind
 instance ToQuant f (OneK k1) (OneK k1) where 
-    toQuant x _ = x
-
+    toQuant _ x = x
 
 class ToMaybeQuant f (t1 :: QuantK k) (t2 :: QuantK k) where
-    toMaybeQuant :: f t1 -> QuantRepr t2 -> Maybe (f t2)
+    toMaybeQuant :: QuantRepr t2 -> f t1 -> Maybe (f t2)
 
 instance HasReprK k => ToMaybeQuant (Quant f) (tp1 :: QuantK k) (tp2 :: QuantK k) where
-    toMaybeQuant x repr = case (x, repr) of
-        (QuantAll{}, _) -> Just (toQuant x repr)
-        (_, QuantSomeRepr) -> Just (toQuant x repr)
+    toMaybeQuant repr x = case (x, repr) of
+        (QuantAll{}, _) -> Just (toQuant repr x)
+        (_, QuantSomeRepr) -> Just (toQuant repr x)
         (QuantOne baseX x', QuantOneRepr baseY) -> case testEquality baseX baseY of
             Just Refl -> Just $ QuantOne baseX x'
             -- by definition we can't convert between base types
             Nothing -> Nothing
-        (QuantSome x', _) -> toMaybeQuant x' repr
+        (QuantSome x', _) -> toMaybeQuant repr x'
         -- by definition a base type cannot be turned into a universal quantifier
         (QuantOne{}, QuantAllRepr) -> Nothing
         -- in general we could consider types that themselves have defined conversions between
@@ -426,54 +426,54 @@ pattern Single repr x <- (quantAsOne -> Just (QuantAsOneProof repr x))
 {-# COMPLETE All, QuantOne, QuantExists #-}
 {-# COMPLETE All, QuantOne, QuantSome #-}
 
-newtype AsOneK (f :: QuantK k -> Type) (y :: k) where
-    AsOneK :: f (OneK y) -> AsOneK f y
+newtype AsSingle (f :: QuantK k -> Type) (y :: k) where
+    AsSingle :: f (OneK y) -> AsSingle f y
 
-deriving instance Eq (f (OneK x)) => Eq ((AsOneK f) x)
-deriving instance Ord (f (OneK x)) => Ord ((AsOneK f) x)
-deriving instance Show (f (OneK x)) => Show ((AsOneK f) x)
+deriving instance Eq (f (OneK x)) => Eq ((AsSingle f) x)
+deriving instance Ord (f (OneK x)) => Ord ((AsSingle f) x)
+deriving instance Show (f (OneK x)) => Show ((AsSingle f) x)
 
-instance TestEquality f => TestEquality (AsOneK f) where
-    testEquality (AsOneK x) (AsOneK y) = case testEquality x y of
+instance TestEquality f => TestEquality (AsSingle f) where
+    testEquality (AsSingle x) (AsSingle y) = case testEquality x y of
         Just Refl -> Just Refl
         Nothing -> Nothing
 
-instance OrdF f => OrdF (AsOneK f) where
-    compareF (AsOneK x) (AsOneK y) = case compareF x y of
+instance OrdF f => OrdF (AsSingle f) where
+    compareF (AsSingle x) (AsSingle y) = case compareF x y of
         EQF -> EQF
         LTF -> LTF
         GTF -> GTF
 
-instance forall f. ShowF f => ShowF (AsOneK f) where
-    showF (AsOneK x) = showF x
+instance forall f. ShowF f => ShowF (AsSingle f) where
+    showF (AsSingle x) = showF x
     withShow _ (_ :: q tp) f = withShow (Proxy :: Proxy f) (Proxy :: Proxy (OneK tp)) f
 
-type QuantEach (f :: QuantK k -> Type) = Quant (AsOneK f) AllK
+type QuantEach (f :: QuantK k -> Type) = Quant (AsSingle f) AllK
 
 viewQuantEach :: HasReprK k => QuantEach f -> (forall (x :: k). ReprOf x -> f (OneK x))
-viewQuantEach (QuantAll f) = \r -> case TMF.apply f r of AsOneK x -> x
+viewQuantEach (QuantAll f) = \r -> case TMF.apply f r of AsSingle x -> x
 
-viewQuantEach' :: HasReprK k => Quant (AsOneK f) tp -> Maybe (Dict (IsExistsOr tp AllK), forall (x :: k). ReprOf x -> f (OneK x))
+viewQuantEach' :: HasReprK k => Quant (AsSingle f) tp -> Maybe (Dict (IsExistsOr tp AllK), forall (x :: k). ReprOf x -> f (OneK x))
 viewQuantEach' q = case q of
     QuantOne{} -> Nothing
-    QuantAll f -> Just (Dict, \r -> case TMF.apply f r of AsOneK x -> x)
+    QuantAll f -> Just (Dict, \r -> case TMF.apply f r of AsSingle x -> x)
     QuantSome q' -> case viewQuantEach' q' of
         Just (Dict, g) -> Just (Dict, g)
         Nothing -> Nothing
 
-pattern QuantEach :: forall {k} f tp. (HasReprK k) => (IsExistsOr tp AllK) => (forall (x :: k). ReprOf x -> f (OneK x)) -> Quant (AsOneK f) tp
+pattern QuantEach :: forall {k} f tp. (HasReprK k) => (IsExistsOr tp AllK) => (forall (x :: k). ReprOf x -> f (OneK x)) -> Quant (AsSingle f) tp
 pattern QuantEach f <- (viewQuantEach' -> Just (Dict, f))
     where
-        QuantEach f = existsOrCases @tp @AllK (QuantAny (QuantEach f)) (QuantAll (TMF.mapWithKey (\r _ -> AsOneK (f r)) (allReprs @k)))
+        QuantEach f = existsOrCases @tp @AllK (QuantAny (QuantEach f)) (QuantAll (TMF.mapWithKey (\r _ -> AsSingle (f r)) (allReprs @k)))
 
 {-# COMPLETE QuantEach, Single #-}
 
-_testQuantEach :: forall {k} f tp. HasReprK k => Quant (AsOneK (f :: QuantK k -> Type)) tp -> ()
+_testQuantEach :: forall {k} f tp. HasReprK k => Quant (AsSingle (f :: QuantK k -> Type)) tp -> ()
 _testQuantEach = \case
     QuantEach (_f :: forall (x :: k). ReprOf x -> f (OneK x)) -> ()
-    Single (_repr :: ReprOf (x :: k)) (AsOneK (_x :: f (OneK x))) -> ()
+    Single (_repr :: ReprOf (x :: k)) (AsSingle (_x :: f (OneK x))) -> ()
 
-_testQuantEach1 :: HasReprK k => Quant (AsOneK (f :: QuantK k -> Type)) AllK -> ()
+_testQuantEach1 :: HasReprK k => Quant (AsSingle (f :: QuantK k -> Type)) AllK -> ()
 _testQuantEach1 = \case
     QuantEach (_f :: forall (x :: k). ReprOf x -> f (OneK x)) -> ()
     -- complete match, since Single has an unsolvable constraint

src/Pate/PatchPair.hs

@@ -331,8 +331,8 @@ mkSingle bin a = PatchPairSingle bin a
 -- | Return the single 'tp' and which binary if the input is a singleton 'PatchPair'.
 --   'asSingleton (toSingleton bin x) == (bin, x)' when 'x' contains an entry for 'bin'
 --   '(y,bin) <- asSingleton x; toSingleton bin y == x' when 'x' is a singleton
-asSingleton :: PatchPairM m => PatchPair tp -> m (Pair PB.WhichBinaryRepr tp)
-asSingleton (PatchPairSingle bin v) = return (Pair bin v)
+asSingleton :: PatchPairM m => Qu.Quant tp qbin -> m (Pair PB.WhichBinaryRepr tp)
+asSingleton (Qu.Single bin v) = return (Pair bin v)
 asSingleton _ = throwPairErr
 
 -- | Convert a 'PatchPair' into a singleton containing only

src/Pate/Verification/PairGraph.hs

@@ -157,6 +157,7 @@ import           Data.Parameterized.Classes
 import           Data.Set (Set)
 import qualified Data.Set as Set
 import           Data.Word (Word32)
+import qualified Data.Quant as Qu
 import qualified Lumberjack as LJ
 
 import           Data.Parameterized (Some(..), Pair (..))
@@ -333,8 +334,10 @@ data WorkItem arch =
       (SingleNodeEntry arch PBi.Original) 
       (SingleNodeEntry arch PBi.Patched)
   -- | Handle starting a split analysis from a diverging node.
-  | ProcessSplitCtor (Some (SingleNodeEntry arch)) 
-  deriving (Eq, Ord)
+  | ProcessSplitCtor (Some (Qu.AsSingle (NodeEntry' arch)))
+
+deriving instance Eq (WorkItem arch)
+deriving instance Ord (WorkItem arch)
 
 instance PA.ValidArch arch => Show (WorkItem arch) where
   show = \case
@@ -362,8 +365,7 @@ pattern ProcessMerge:: SingleNodeEntry arch PBi.Original -> SingleNodeEntry arch
 pattern ProcessMerge sneO sneP <- (processMergeSinglePair -> Just (sneO, sneP))
 
 pattern ProcessSplit :: SingleNodeEntry arch bin -> WorkItem arch
-pattern ProcessSplit sne <- ProcessSplitCtor (Some sne)
-
+pattern ProcessSplit sne = ProcessSplitCtor (Some (Qu.AsSingle sne))
 
 {-# COMPLETE ProcessNode, ProcessMergeAtExits, ProcessMergeAtEntry, ProcessSplit #-}
 {-# COMPLETE ProcessNode, ProcessMerge, ProcessSplit #-}
@@ -436,7 +438,7 @@ data SyncData arch =
       -- | Defines exceptions for exits that would otherwise be considered sync points.
       --   In these cases, the single-sided analysis continues instead, with the intention
       --   that another sync point is encountered after additional instructions are executed
-    , _syncExceptions :: PPa.PatchPair (SetF (TupleF '(SingleNodeEntry arch, PB.BlockTarget arch)))
+    , _syncExceptions :: PPa.PatchPair (SetF (TupleF '(Qu.AsSingle (NodeEntry' arch), PB.BlockTarget arch)))
       -- Exits from the corresponding desync node that start the single-sided analysis
     , _syncDesyncExits :: PPa.PatchPair (SetF (PB.BlockTarget arch))
     }
@@ -451,7 +453,9 @@ syncPointBin :: SyncPoint arch bin -> PBi.WhichBinaryRepr bin
 syncPointBin sp = singleEntryBin $ syncPointNode sp
 
 instance TestEquality (SyncPoint arch) where
-  testEquality e1 e2 = testEquality (syncPointNode e1) (syncPointNode e2)
+  testEquality e1 e2 = case testEquality (syncPointNode e1) (syncPointNode e2) of
+    Just Refl -> Just Refl
+    Nothing -> Nothing
 
 instance OrdF (SyncPoint arch) where
   compareF sp1 sp2 = lexCompareF (syncPointBin sp1) (syncPointBin sp2) $
@@ -595,7 +599,7 @@ mkProcessSplit sne = do
   GraphNode dp_ne <- return $ singleNodeDivergePoint sne
   sne_dp <- toSingleNodeEntry (singleEntryBin sne) dp_ne
   guard (sne_dp == sne)
-  return (ProcessSplitCtor (Some sne))
+  return (ProcessSplit sne)
 
 
 workItemNode :: WorkItem arch -> GraphNode arch
@@ -1271,9 +1275,9 @@ pgMaybe msg Nothing = throwError $ PEE.PairGraphErr msg
 -- FIXME: do we need to support mismatched node kinds here?
 combineNodes :: SingleNodeEntry arch bin -> SingleNodeEntry arch (PBi.OtherBinary bin) -> Maybe (GraphNode arch)
 combineNodes node1 node2 = do
-  let ndPair = PPa.mkPair (singleEntryBin node1) node1 node2
-  nodeO <- PPa.get PBi.OriginalRepr ndPair
-  nodeP <- PPa.get PBi.PatchedRepr ndPair
+  let ndPair = PPa.mkPair (singleEntryBin node1) (Qu.AsSingle node1) (Qu.AsSingle node2)
+  Qu.AsSingle nodeO <- PPa.get PBi.OriginalRepr ndPair
+  Qu.AsSingle nodeP <- PPa.get PBi.PatchedRepr ndPair
   -- it only makes sense to combine nodes that share a divergence point,
   -- where that divergence point will be used as the calling context for the
   -- merged point
@@ -1458,7 +1462,7 @@ isSyncExit ::
 isSyncExit sne blkt@(PB.BlockTarget{}) = do
   excepts <- getSingleNodeData syncExceptions sne
   syncs <- getSingleNodeData syncPoints sne
-  let isExcept = Set.member (TupleF2 sne blkt) excepts 
+  let isExcept = Set.member (TupleF2 (Qu.AsSingle sne) blkt) excepts 
   case isExcept of
     True -> return Nothing
     False -> isCutAddressFor sne (PB.targetRawPC blkt) >>= \case
@@ -1528,7 +1532,7 @@ filterSyncExits priority (ProcessSplit sne) blktPairs = pgValid $ do
       return x
 filterSyncExits priority (ProcessNode (GraphNode ne)) blktPairs = case asSingleNodeEntry ne of
   Nothing -> return blktPairs
-  Just (Some sne) -> do
+  Just (Some (Qu.AsSingle sne)) -> do
     let bin = singleEntryBin sne
     blkts <- mapM (PPa.get bin) blktPairs
     syncExits <- catMaybes <$> mapM (isSyncExit sne) blkts
@@ -1543,14 +1547,14 @@ addReturnPointSync ::
   PPa.PatchPair (PB.BlockTarget arch) ->
   PairGraphM sym arch ()
 addReturnPointSync priority ne blktPair = case asSingleNodeEntry ne of
-  Just (Some sne) -> do
+  Just (Some (Qu.AsSingle sne)) -> do
     let bin = singleEntryBin sne
     blkt <- PPa.get bin blktPair
     case PB.targetReturn blkt of
       Just ret -> do
         cuts <- getSingleNodeData syncCutAddresses sne
         excepts <- getSingleNodeData syncExceptions sne
-        let isExcept = Set.member (TupleF2 sne blkt) excepts
+        let isExcept = Set.member (TupleF2 (Qu.AsSingle sne) blkt) excepts
         case (not isExcept) &&
           Set.member (PPa.WithBin (singleEntryBin sne) (PB.concreteAddress ret)) cuts of
             True -> do
@@ -1600,7 +1604,7 @@ handleSingleSidedReturnTo ::
   NodeEntry arch ->
   PairGraphM sym arch ()
 handleSingleSidedReturnTo priority ne = case asSingleNodeEntry ne of
-  Just (Some sne) -> do
+  Just (Some (Qu.AsSingle sne)) -> do
     let bin = singleEntryBin sne
     let dp = singleNodeDivergePoint sne
     syncAddrs <- getSyncData syncCutAddresses bin dp