{-# LANGUAGE DerivingStrategies         #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE StandaloneDeriving         #-}
{-# LANGUAGE TypeApplications           #-}
{-# LANGUAGE TypeFamilies               #-}
{-# LANGUAGE UndecidableInstances       #-}

{-# OPTIONS_GHC -Wno-orphans #-}

-- | Implements @CanDiff@ with our vendored version of @tree-diff@.
module Test.StateMachine.TreeDiff.Diffing () where

import           Data.SOP
import           Test.StateMachine.Diffing
import qualified Test.StateMachine.Lockstep.NAry    as NAry
import qualified Test.StateMachine.Lockstep.Simple  as Simple
import           Test.StateMachine.TreeDiff.Class
import           Test.StateMachine.TreeDiff.Expr
import           Test.StateMachine.TreeDiff.Pretty
import           Test.StateMachine.Types.References

instance ToExpr x => CanDiff x where
  type ADiff  x = Edit EditExpr
  type AnExpr x = Expr

  toDiff :: x -> AnExpr x
toDiff             = x -> AnExpr x
x -> Expr
forall a. ToExpr a => a -> Expr
toExpr
  exprDiff :: Proxy x -> AnExpr x -> AnExpr x -> ADiff x
exprDiff         Proxy x
_ = AnExpr x -> AnExpr x -> ADiff x
Expr -> Expr -> Edit EditExpr
Test.StateMachine.TreeDiff.Expr.exprDiff
  diffToDocCompact :: Proxy x -> ADiff x -> Doc
diffToDocCompact Proxy x
_ = ADiff x -> Doc
Edit EditExpr -> Doc
ansiWlBgEditExprCompact
  diffToDoc :: Proxy x -> ADiff x -> Doc
diffToDoc        Proxy x
_ = ADiff x -> Doc
Edit EditExpr -> Doc
ansiWlBgEditExpr
  exprToDoc :: Proxy x -> AnExpr x -> Doc
exprToDoc        Proxy x
_ = AnExpr x -> Doc
Expr -> Doc
ansiWlBgExpr

-- References

deriving newtype instance ToExpr Var

instance ToExpr a => ToExpr (Symbolic a) where
  toExpr :: Symbolic a -> Expr
toExpr (Symbolic Var
x) = Var -> Expr
forall a. ToExpr a => a -> Expr
toExpr Var
x

instance ToExpr a => ToExpr (Concrete a) where
  toExpr :: Concrete a -> Expr
toExpr (Concrete a
x) = a -> Expr
forall a. ToExpr a => a -> Expr
toExpr a
x

instance ToExpr (r a) => ToExpr (Reference a r)

instance ToExpr (Opaque a) where
  toExpr :: Opaque a -> Expr
toExpr Opaque a
_ = ConstructorName -> [Expr] -> Expr
App ConstructorName
"Opaque" []

-- Simple

instance ToExpr (Simple.MockHandle t)
      => ToExpr (NAry.MockHandleN (Simple.Simple t) (Simple.RealHandle t)) where
  toExpr :: MockHandleN (Simple t) (RealHandle t) -> Expr
toExpr (Simple.SimpleToMock MockHandle t
h) = MockHandle t -> Expr
forall a. ToExpr a => a -> Expr
toExpr MockHandle t
h

-- NAry

deriving
  newtype
  instance (ToExpr a, ToExpr (NAry.MockHandleN t a)) => ToExpr (NAry.Refs t Concrete a)

instance All (And ToExpr (Compose ToExpr (NAry.MockHandleN t))) (NAry.RealHandles t)
      => ToExpr (NAry.Refss t Concrete) where
  toExpr :: Refss t Concrete -> Expr
toExpr = [Expr] -> Expr
Lst
         ([Expr] -> Expr)
-> (Refss t Concrete -> [Expr]) -> Refss t Concrete -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NP (K Expr) (RealHandles t) -> [Expr]
NP (K Expr) (RealHandles t) -> CollapseTo NP Expr
forall (xs :: [*]) a.
SListIN NP xs =>
NP (K a) xs -> CollapseTo NP a
forall k l (h :: (k -> *) -> l -> *) (xs :: l) a.
(HCollapse h, SListIN h xs) =>
h (K a) xs -> CollapseTo h a
hcollapse
         (NP (K Expr) (RealHandles t) -> [Expr])
-> (Refss t Concrete -> NP (K Expr) (RealHandles t))
-> Refss t Concrete
-> [Expr]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proxy (And ToExpr (Compose ToExpr (MockHandleN t)))
-> (forall a.
    And ToExpr (Compose ToExpr (MockHandleN t)) a =>
    Refs t Concrete a -> K Expr a)
-> NP (Refs t Concrete) (RealHandles t)
-> NP (K Expr) (RealHandles t)
forall {k} {l} (h :: (k -> *) -> l -> *) (c :: k -> Constraint)
       (xs :: l) (proxy :: (k -> Constraint) -> *) (f :: k -> *)
       (f' :: k -> *).
(AllN (Prod h) c xs, HAp h) =>
proxy c
-> (forall (a :: k). c a => f a -> f' a) -> h f xs -> h f' xs
hcmap (forall {k} (t :: k). Proxy t
forall (t :: * -> Constraint). Proxy t
Proxy @(And ToExpr (Compose ToExpr (NAry.MockHandleN t)))) Refs t Concrete a -> K Expr a
forall a.
And ToExpr (Compose ToExpr (MockHandleN t)) a =>
Refs t Concrete a -> K Expr a
forall a.
(ToExpr a, ToExpr (MockHandleN t a)) =>
Refs t Concrete a -> K Expr a
toExprOne
         (NP (Refs t Concrete) (RealHandles t)
 -> NP (K Expr) (RealHandles t))
-> (Refss t Concrete -> NP (Refs t Concrete) (RealHandles t))
-> Refss t Concrete
-> NP (K Expr) (RealHandles t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Refss t Concrete -> NP (Refs t Concrete) (RealHandles t)
forall t (r :: * -> *). Refss t r -> NP (Refs t r) (RealHandles t)
NAry.unRefss
    where
      toExprOne :: (ToExpr a, ToExpr (NAry.MockHandleN t a))
                => NAry.Refs t Concrete a -> K Expr a
      toExprOne :: forall a.
(ToExpr a, ToExpr (MockHandleN t a)) =>
Refs t Concrete a -> K Expr a
toExprOne = Expr -> K Expr a
forall k a (b :: k). a -> K a b
K (Expr -> K Expr a)
-> (Refs t Concrete a -> Expr) -> Refs t Concrete a -> K Expr a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Refs t Concrete a -> Expr
forall a. ToExpr a => a -> Expr
toExpr

instance ( ToExpr (NAry.MockState t)
         , All (And ToExpr (Compose ToExpr (NAry.MockHandleN t))) (NAry.RealHandles t)
         ) => ToExpr (NAry.Model t Concrete)