generalized PairGraph.Node over QuantK cases

src/Data/Quant.hs

@@ -46,6 +46,10 @@ module Data.Quant
     , type OneK
     , type ExistsK
     , type AllK
+    , map
+    , traverse
+    , mapWithRepr
+    , traverseWithRepr
     , pattern QuantSome
     , toQuantExists
     , quantToRepr
@@ -56,10 +60,13 @@ module Data.Quant
     , pattern QuantToOne
     , generateAll
     , generateAllM
-    , pattern QuantAsAll
-    , pattern QuantAsOne
+    , pattern All
+    , pattern Single
+    , viewQuantEach
   ) where
 
+import           Prelude hiding (map, traverse)
+
 import           Data.Kind (Type)
 import           Data.Constraint
 
@@ -156,8 +163,23 @@ instance forall k. HasReprK k => TraversableFC (Quant :: (k -> Type) -> QuantK k
         QuantAll g -> QuantAll <$> traverseF f g
         QuantSome x -> QuantSome <$> traverseFC f x
 
+map :: (forall x. f x -> g x) -> Quant f tp -> Quant g tp
+map = fmapFC
+
+mapWithRepr :: (forall (x :: k). ReprOf x -> f x -> g x) -> Quant f tp -> Quant g tp
+mapWithRepr f = \case
+    QuantOne repr x -> QuantOne repr $ f repr x
+    QuantAll tm -> QuantAll $ TMF.mapWithKey f tm
+    QuantSome x -> QuantSome $ mapWithRepr f x
 
+traverse :: (HasReprK k, Applicative m) => (forall (x :: k). f x -> m (g x)) -> Quant f tp -> m (Quant g tp)
+traverse = traverseFC
 
+traverseWithRepr :: (HasReprK k, Applicative m) => (forall (x :: k). ReprOf x -> f x -> m (g x)) -> Quant f tp -> m (Quant g tp)
+traverseWithRepr f = \case
+    QuantOne repr x -> QuantOne <$> pure repr <*> f repr x
+    QuantAll tm -> QuantAll <$> TMF.traverseWithKey f tm
+    QuantSome x -> QuantSome <$> traverseWithRepr f x
 
 quantToRepr :: Quant f tp -> QuantRepr tp
 quantToRepr = \case
@@ -303,10 +325,6 @@ instance HasReprK k => ToMaybeQuant (Quant f) (tp1 :: QuantK k) (tp2 :: QuantK k
         -- good reason
 
 
-data AsOneK (f :: QuantK k -> Type) (y :: k) where
-    AsOneK :: f (OneK y) -> AsOneK f y
-
-
 class (Antecedent p c => c) => Implies p c where
     type Antecedent p c :: Constraint
 
@@ -341,13 +359,39 @@ pattern QuantToOne :: forall {k} x f tp. (KnownHasRepr (x :: k), HasReprK k) =>
 pattern QuantToOne fx <- (asQuantOne (knownRepr :: ReprOf x) -> Just (Dict, Dict, _, fx))
 
 
--- | Project a total function from a 'Quant' if it is universally quantified.
-pattern QuantAsAll :: forall {k} f tp. (HasReprK k) => () => (forall x. ReprOf x -> f x) -> Quant (f :: k -> Type) tp
-pattern QuantAsAll f <- ((\l -> (case toMaybeQuant l QuantAllRepr of Just (QuantAll f) -> Just (TMF.apply f); _ -> Nothing)  :: Maybe (forall (x :: k). ReprOf x -> f x) ) -> Just (f))
+class IsExistsOr (tp1 :: QuantK k) (tp2 :: QuantK k) where
+    isExistsOr :: Either (tp1 :~: ExistsK) (tp1 :~: tp2)
 
-data QuantAsOneProof (f :: k -> Type) (tp :: QuantK k) where
-    QuantAsOneProof :: (KnownRepr QuantRepr tp, Implies (IsOneK tp) (x ~ TheOneK tp)) => ReprOf x -> f x -> QuantAsOneProof f tp
+instance IsExistsOr x x where
+    isExistsOr = Right Refl
+
+instance IsExistsOr ExistsK (OneK k) where
+    isExistsOr = Left Refl
 
+instance IsExistsOr ExistsK AllK where
+    isExistsOr = Left Refl
+
+data QuantAsAllProof (f :: k -> Type) (tp :: QuantK k) where
+    QuantAsAllProof :: (IsExistsOr tp AllK) => (forall x. ReprOf x -> f x) -> QuantAsAllProof f tp
+
+quantAsAll :: HasReprK k => Quant (f :: k -> Type) tp -> Maybe (QuantAsAllProof f tp)
+quantAsAll q = case q of
+    QuantOne{} -> Nothing
+    QuantAll f -> Just (QuantAsAllProof (TMF.apply f))
+    QuantSome q' -> case quantAsAll q' of
+        Just (QuantAsAllProof f) -> Just $ QuantAsAllProof f
+        Nothing -> Nothing
+
+-- | Pattern for creating or matching a universally quantified 'Quant', generalized over the existential cases
+pattern All :: forall {k} f tp. (HasReprK k) => (IsExistsOr tp AllK) => (forall x. ReprOf x -> f x) -> Quant (f :: k -> Type) tp
+pattern All f <- (quantAsAll -> Just (QuantAsAllProof f))
+    where
+        All f = case (isExistsOr :: Either (tp :~: ExistsK) (tp :~: AllK)) of
+            Left Refl -> QuantAny (All f)
+            Right Refl -> QuantAll (TMF.mapWithKey (\repr _ -> f repr) (allReprs @k))
+
+data QuantAsOneProof (f :: k -> Type) (tp :: QuantK k) where
+    QuantAsOneProof :: (IsExistsOr tp (OneK (TheOneK tp)), Implies (IsOneK tp) (x ~ TheOneK tp)) => ReprOf x -> f x -> QuantAsOneProof f tp
 
 quantAsOne :: forall k f tp. HasReprK k => Quant (f :: k -> Type) (tp :: QuantK k) -> Maybe (QuantAsOneProof f tp)
 quantAsOne q = case q of
@@ -358,6 +402,46 @@ quantAsOne q = case q of
     _ -> Nothing
 
 
--- | Project out the element of a singleton 'Quant'
-pattern QuantAsOne :: forall {k} f tp. (HasReprK k) => forall x. (KnownRepr QuantRepr tp, Implies (IsOneK tp) (x ~ TheOneK tp)) => ReprOf x -> f x -> Quant (f :: k -> Type) tp
-pattern QuantAsOne repr x <- (quantAsOne -> Just (QuantAsOneProof repr x))
+-- | Pattern for creating or matching a singleton 'Quant', generalized over the existential cases
+pattern Single :: forall {k} f tp. (HasReprK k) => forall x. (IsExistsOr tp (OneK (TheOneK tp)), Implies (IsOneK tp) (x ~ TheOneK tp)) => ReprOf x -> f x -> Quant (f :: k -> Type) tp
+pattern Single repr x <- (quantAsOne -> Just (QuantAsOneProof repr x))
+    where
+        Single repr x = case (isExistsOr :: Either (tp :~: ExistsK) (tp :~: (OneK (TheOneK tp)))) of
+            Left Refl -> QuantExists (Single repr x)
+            Right Refl -> QuantOne repr x
+
+{-# COMPLETE Single, All #-}
+{-# COMPLETE Single, QuantAll, QuantAny #-}
+{-# COMPLETE Single, QuantAll, QuantSome #-}
+
+{-# COMPLETE All, QuantOne, QuantExists #-}
+{-# COMPLETE All, QuantOne, QuantSome #-}
+
+newtype AsOneK (f :: QuantK k -> Type) (y :: k) where
+    AsOneK :: f (OneK y) -> AsOneK 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)
+
+instance TestEquality f => TestEquality (AsOneK f) where
+    testEquality (AsOneK x) (AsOneK 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
+        EQF -> EQF
+        LTF -> LTF
+        GTF -> GTF
+
+instance forall f. ShowF f => ShowF (AsOneK f) where
+    showF (AsOneK 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
+
+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
+
+

src/Pate/Binary.hs

@@ -19,11 +19,13 @@
 {-# LANGUAGE TypeSynonymInstances #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE OverloadedStrings #-}
 
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 
 module Pate.Binary
   ( type WhichBinary
+  , type BinaryPair
   , KnownBinary
   , Original
   , Patched
@@ -33,17 +35,29 @@ module Pate.Binary
   , flipRepr
   , short
   , otherInvolutive
+  , ppBinaryPair
+  , ppBinaryPairEq
+  , ppBinaryPair'
+  , w4SerializePair
   )
 where
 
+import           Data.Kind ( Type )
+import           Control.Applicative.Alternative ( (<|>) )
+
 import           Data.Parameterized.WithRepr
 import           Data.Parameterized.Classes
 import           Data.Parameterized.Some
 import qualified Data.Parameterized.TotalMapF as TMF
+import qualified Data.Aeson as JSON
+
 import qualified Data.Quant as Qu
 import           Data.Quant ( Quant, QuantK)
 import qualified Prettyprinter as PP
 import           Pate.TraceTree
+import qualified What4.JSON as W4S
+import           What4.JSON ( (.:) )
+import qualified Pate.ExprMappable as PEM
 
 -- | A type-level tag describing whether the data value is from an original binary or a patched binary
 data WhichBinary = Original | Patched deriving (Bounded, Enum, Eq, Ord, Read, Show)
@@ -129,3 +143,89 @@ instance TMF.HasTotalMapF WhichBinaryRepr where
 instance Qu.HasReprK WhichBinary where
   type ReprOf = WhichBinaryRepr
 
+type BinaryPair f = Qu.Quant (f :: WhichBinary -> Type)
+
+jsonQuant ::
+  (forall bin. f bin -> JSON.Value) -> BinaryPair f (qbin :: QuantK WhichBinary) -> JSON.Value
+jsonQuant f q = case q of
+  Qu.All g -> JSON.object [ "original" JSON..= f (g OriginalRepr), "patched" JSON..= f (g PatchedRepr)]
+  Qu.Single bin x -> case bin of
+    OriginalRepr -> JSON.object [ "original" JSON..= f x ]
+    PatchedRepr ->  JSON.object [ "patched" JSON..= f x ]
+
+
+instance (forall bin. JSON.ToJSON (f bin)) => JSON.ToJSON (Qu.Quant f (qbin :: QuantK WhichBinary)) where
+  toJSON p = jsonQuant (JSON.toJSON) p
+
+
+w4SerializePair :: BinaryPair f qbin -> (forall bin. f bin -> W4S.W4S sym JSON.Value) -> W4S.W4S sym JSON.Value
+w4SerializePair bpair f = case bpair of
+    Qu.All g -> do
+      o_v <- f (g OriginalRepr)
+      p_v <- f (g PatchedRepr)
+      return $ JSON.object ["original" JSON..= o_v, "patched" JSON..= p_v]
+    Qu.Single bin x -> case bin of
+      OriginalRepr -> do
+        o_v <- f x
+        return $ JSON.object ["original" JSON..= o_v]
+      PatchedRepr -> do
+        p_v <- f x
+        return $ JSON.object ["patched" JSON..= p_v]
+
+instance W4S.W4SerializableF sym f => W4S.W4Serializable sym (Qu.Quant f (qbin :: QuantK WhichBinary)) where
+  w4Serialize ppair = w4SerializePair ppair W4S.w4SerializeF
+
+
+instance forall f sym. (forall bin. KnownRepr WhichBinaryRepr bin => W4S.W4Deserializable sym (f bin)) => W4S.W4Deserializable sym (Quant f Qu.ExistsK) where
+  w4Deserialize_ v = do
+    JSON.Object o <- return v
+    let
+      case_pair = do
+        (vo :: f Original) <- o .: "original"
+        (vp :: f Patched) <- o .: "patched"
+        return $ Qu.All $ \case OriginalRepr -> vo; PatchedRepr -> vp
+      case_orig = do
+        (vo :: f Original) <- o .: "original"
+        return $ Qu.Single OriginalRepr vo
+      case_patched = do
+        (vp :: f Patched) <- o .: "patched"
+        return $ Qu.Single PatchedRepr vp
+    case_pair <|> case_orig <|> case_patched
+
+ppBinaryPair :: (forall bin. tp bin -> PP.Doc a) -> BinaryPair tp qbin -> PP.Doc a
+ppBinaryPair f (Qu.All g) = f (g OriginalRepr) PP.<+> "(original) vs." PP.<+> f (g PatchedRepr) PP.<+> "(patched)"
+ppBinaryPair f (Qu.Single OriginalRepr a1) = f a1 PP.<+> "(original)"
+ppBinaryPair f (Qu.Single PatchedRepr a1) = f a1 PP.<+> "(patched)"
+
+ppBinaryPair' :: (forall bin. tp bin -> PP.Doc a) -> BinaryPair tp qbin -> PP.Doc a
+ppBinaryPair' f pPair = ppBinaryPairEq (\x y -> show (f x) == show (f y)) f pPair
+
+-- | True if the two given values would be printed identically
+ppEq :: PP.Pretty x => PP.Pretty y => x -> y -> Bool
+ppEq x y = show (PP.pretty x) == show (PP.pretty y)
+
+instance ShowF tp => Show (Quant tp (qbin :: QuantK WhichBinary)) where
+  show (Qu.All g) = 
+    let
+      s1 = showF (g OriginalRepr)
+      s2 = showF (g PatchedRepr)
+    in if s1 == s2 then s1 else s1 ++ " vs. " ++ s2
+  show (Qu.Single OriginalRepr a1) = showF a1 ++ " (original)"
+  show (Qu.Single PatchedRepr a1) = showF a1 ++ " (patched)"
+
+
+ppBinaryPairEq ::
+  (tp Original -> tp Patched -> Bool) ->
+  (forall bin. tp bin -> PP.Doc a) ->
+  BinaryPair tp qbin ->
+  PP.Doc a
+ppBinaryPairEq test f (Qu.All g) = case test (g OriginalRepr) (g PatchedRepr) of
+  True -> f $ g OriginalRepr
+  False -> f (g OriginalRepr) PP.<+> "(original) vs." PP.<+> f (g PatchedRepr) PP.<+> "(patched)"
+ppBinaryPairEq _ f pPair = ppBinaryPair f pPair
+
+instance (forall bin. PP.Pretty (f bin)) => PP.Pretty (Quant f (qbin :: QuantK WhichBinary)) where
+  pretty = ppBinaryPairEq ppEq PP.pretty
+
+instance (Qu.HasReprK k, forall (bin :: k). PEM.ExprMappable sym (f bin)) => PEM.ExprMappable sym (Quant f qbin) where
+  mapExpr sym f pp = Qu.traverse (PEM.mapExpr sym f) pp