An unsuccessful attempt at distilling a GHC infinite loop during compilation

A.hs

{-# LANGUAGE Haskell2010 #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wall #-}
module A
  {-
  ( AnyPPC
  , ArchRegStruct
  , KnownVariant
  , GenArchInfo(..)
  , GenArchVals(..)
  , IsMemoryModel(..)
  , PPCReg
  , RegEntry(..)
  , RegValue
  , RegValue'(..)
  , ToCrucibleType
  , Variant(..)
  , updateReg
  )-} where

import Control.Exception (assert)
import Control.Monad.Catch (Exception, MonadThrow(..))
import Data.Kind (Constraint, Type)
import Data.Proxy (Proxy(..))
import qualified Data.Text as T
import Data.Type.Equality (TestEquality(..), (:~:)(..))
import Data.Typeable (Typeable)
import Data.Word (Word8)
import GHC.TypeLits (KnownSymbol, Symbol, symbolVal)
import GHC.TypeNats (KnownNat, Nat, type (-), type (<=), natVal)
import Numeric.Natural (Natural)
import Unsafe.Coerce (unsafeCoerce)

data Height = Zero | Succ Height

type EmptyCtx = 'EmptyCtx
type (c :: Ctx k) ::> (a::k) = c '::> a

type SingleCtx x = EmptyCtx ::> x

data Ctx k
  = EmptyCtx
  | Ctx k ::> k

type family (<+>) (x :: Ctx k) (y :: Ctx k) :: Ctx k where
  x <+> EmptyCtx = x
  x <+> (y ::> e) = (x <+> y) ::> e

type family CtxRepeat (n :: Nat) (c :: k) :: Ctx k where
  CtxRepeat 0 c = EmptyCtx
  CtxRepeat n c = CtxRepeat (n - 1) c ::> c

class RepeatAssign (tp :: k) (ctx :: Ctx k) where
  repeatAssign :: (Int -> f tp) -> Assignment f ctx

instance RepeatAssign tp EmptyCtx where
  repeatAssign _ = Empty

instance RepeatAssign tp ctx => RepeatAssign tp (ctx ::> tp) where
  repeatAssign f =
    let r = repeatAssign f
    in r :> f (sizeInt (size r))

appendBal :: Assignment f x -> BalancedTree h f y -> Assignment f (x <+> y)
appendBal x (BalLeaf a) = x `extend` a
appendBal x (BalPair y z) =
  case assoc x y z of
    Refl -> x `appendBal` y `appendBal` z

appendBin :: Assignment f x -> BinomialTree h f y -> Assignment f (x <+> y)
appendBin x BinomialEmpty = x
appendBin x (PlusOne _ y z) =
  case assoc x y z of
    Refl -> x `appendBin` y `appendBal` z
appendBin x (PlusZero _ y) = x `appendBin` y

(<++>) :: Assignment f x -> Assignment f y -> Assignment f (x <+> y)
x <++> Assignment y = x `appendBin` y

empty :: Assignment f EmptyCtx
empty = Assignment BinomialEmpty

extend :: Assignment f ctx -> f x -> Assignment f (ctx ::> x)
extend (Assignment x) y = Assignment $ append x (BalLeaf y)

pattern Empty :: () => ctx ~ EmptyCtx => Assignment f ctx
pattern Empty <- (viewAssign -> AssignEmpty)
  where Empty = empty

infixl :>

pattern (:>) :: () => ctx' ~ (ctx ::> tp) => Assignment f ctx -> f tp -> Assignment f ctx'
pattern (:>) a v <- (viewAssign -> AssignExtend a v)
  where a :> v = extend a v
{-# COMPLETE (:>), Empty :: Assignment  #-}

viewAssign :: forall f ctx . Assignment f ctx -> AssignView f ctx
viewAssign (Assignment x) =
  case bin_drop x of
    DropEmpty -> AssignEmpty
    DropExt t v -> AssignExtend (Assignment t) v

append :: BinomialTree h f x
       -> BalancedTree h f y
       -> BinomialTree h f (x <+> y)
append BinomialEmpty y = PlusOne 0 BinomialEmpty y
append (PlusOne _ t x) y =
  case assoc t x y of
    Refl ->
      let t' = append t (BalPair x y)
       in PlusZero (tsize t') t'
append (PlusZero s t) x = PlusOne s t x

unsafeAxiom :: forall a b. a :~: b
unsafeAxiom = unsafeCoerce (Refl @a)
{-# NOINLINE unsafeAxiom #-}

assoc :: p x -> q y -> r z -> x <+> (y <+> z) :~: (x <+> y) <+> z
assoc _ _ _ = unsafeAxiom

bal_drop :: forall h f x y
          . BinomialTree h f x
         -> BalancedTree h f y
         -> DropResult f (x <+> y)
bal_drop t (BalLeaf e) = DropExt t e
bal_drop t (BalPair x y) =
  unsafeCoerce (bal_drop (PlusOne (tsize t) (unsafeCoerce t) x) y)

bin_drop :: forall h f ctx
          . BinomialTree h f ctx
         -> DropResult f ctx
bin_drop BinomialEmpty = DropEmpty
bin_drop (PlusZero _ u) = bin_drop u
bin_drop (PlusOne s t u) =
  let m = case t of
            BinomialEmpty -> BinomialEmpty
            _ -> PlusZero s t
   in bal_drop m u

data BalancedTree h (f :: k -> Type) (p :: Ctx k) where
  BalLeaf :: !(f x) -> BalancedTree 'Zero f (SingleCtx x)
  BalPair :: !(BalancedTree h f x)
          -> !(BalancedTree h f y)
          -> BalancedTree ('Succ h) f (x <+> y)

data BinomialTree (h::Height) (f :: k -> Type) :: Ctx k -> Type where
  BinomialEmpty :: BinomialTree h f EmptyCtx

  -- Contains size of the subtree, subtree, then element.
  PlusOne  :: !Int
           -> !(BinomialTree ('Succ h) f x)
           -> !(BalancedTree h f y)
           -> BinomialTree h f (x <+> y)

  -- Contains size of the subtree, subtree, then element.
  PlusZero  :: !Int
            -> !(BinomialTree ('Succ h) f x)
            -> BinomialTree h f x

data DropResult f (ctx :: Ctx k) where
  DropEmpty :: DropResult f EmptyCtx
  DropExt   :: BinomialTree 'Zero f x
            -> f y
            -> DropResult f (x ::> y)

data AssignView f ctx where
  AssignEmpty :: AssignView f EmptyCtx
  AssignExtend :: Assignment f ctx
               -> f tp
               -> AssignView f (ctx ::> tp)

newtype Assignment (f :: k -> Type) (ctx :: Ctx k)
      = Assignment (BinomialTree 'Zero f ctx)

instance FunctorFC Assignment where
  fmapFC = \f (Assignment x) -> Assignment (fmap_bin f x)
  {-# INLINE fmapFC #-}

fmap_bin :: (forall tp . f tp -> g tp)
         -> BinomialTree h f c
         -> BinomialTree h g c
fmap_bin _ BinomialEmpty = BinomialEmpty
fmap_bin f (PlusOne s t x) = PlusOne s (fmap_bin f t) (fmap_bal f x)
fmap_bin f (PlusZero s t)  = PlusZero s (fmap_bin f t)
{-# INLINABLE fmap_bin #-}

fmap_bal :: (forall tp . f tp -> g tp)
         -> BalancedTree h f c
         -> BalancedTree h g c
fmap_bal = go
  where go :: (forall tp . f tp -> g tp)
              -> BalancedTree h f c
              -> BalancedTree h g c
        go f (BalLeaf x) = BalLeaf (f x)
        go f (BalPair x y) = BalPair (go f x) (go f y)
{-# INLINABLE fmap_bal #-}

newtype Size (ctx :: Ctx k) = Size Int

sizeInt :: Size ctx -> Int
sizeInt (Size n) = n

size :: Assignment f ctx -> Size ctx
size (Assignment t) = Size (tsize t)

tsize :: BinomialTree h f a -> Int
tsize BinomialEmpty = 0
tsize (PlusOne s _ _) = 2*s+1
tsize (PlusZero  s _) = 2*s

data MacawType
  = MacawBVType Nat
  -- | FloatType FloatInfo
  -- | BoolType
  -- | TupleType [MacawType]
  -- | VecType Nat MacawType

data MacawTypeRepr (tp :: MacawType) where
  MacawBVTypeRepr :: (1 <= n) => !(NatRepr n) -> MacawTypeRepr (MacawBVType n)
  -- BoolTypeRepr :: TypeRepr BoolType
  -- FloatTypeRepr :: !(FloatInfoRepr fi) -> TypeRepr (FloatType fi)
  -- TupleTypeRepr :: !(P.List TypeRepr ctx) -> TypeRepr (TupleType ctx)
  -- VecTypeRepr :: NatRepr n -> TypeRepr tp -> TypeRepr (VecType n tp)

data BaseType
  = BaseBVType Nat

data CrucibleType where
  BaseToType :: BaseType -> CrucibleType
  IntrinsicType :: Symbol -> Ctx CrucibleType -> CrucibleType
  StructType :: Ctx CrucibleType -> CrucibleType

data CrucibleTypeRepr :: CrucibleType -> Type where
  CrucibleBVRepr :: (1 <= n) => !(NatRepr n) -> CrucibleTypeRepr (CrucibleBVType n)
  IntrinsicRepr :: !(SymbolRepr nm)
                -> !(CtxRepr ctx)
                -> CrucibleTypeRepr (IntrinsicType nm ctx)
  -- StructRepr :: !(CtxRepr ctx) -> CrucibleTypeRepr (StructType ctx)

type CtxRepr = Assignment CrucibleTypeRepr

type CrucibleBVType w = BaseToType (BaseBVType w)
type LLVMPointerType w = IntrinsicType "LLVM_pointer" (EmptyCtx ::> CrucibleBVType w)

newtype NatRepr (n::Nat) = NatRepr { _natValue :: Natural }
newtype SymbolRepr (nm::Symbol) = SymbolRepr { _symbolRepr :: T.Text }

knownNat :: forall n . KnownNat n => NatRepr n
knownNat = NatRepr (natVal (Proxy :: Proxy n))

n32 :: NatRepr 32
n32 = knownNat

n128 :: NatRepr 128
n128 = knownNat

knownSymbol :: KnownSymbol s => SymbolRepr s
knownSymbol = go Proxy
  where go :: KnownSymbol s => Proxy s -> SymbolRepr s
        go p = SymbolRepr $! packSymbol (symbolVal p)

        packSymbol str
           | T.unpack txt == str = txt
           | otherwise = error $ "Unrepresentable symbol! "++ str
         where txt = T.pack str

instance TestEquality SymbolRepr where
   testEquality (SymbolRepr x :: SymbolRepr x) (SymbolRepr y)
      | x == y    = Just unsafeAxiom
      | otherwise = Nothing

pattern LLVMPointerRepr :: () => (1 <= w, ty ~ LLVMPointerType w) => NatRepr w -> CrucibleTypeRepr ty
pattern LLVMPointerRepr w <- IntrinsicRepr (testEquality (knownSymbol :: SymbolRepr "LLVM_pointer") -> Just Refl)
                                           (Empty :> CrucibleBVRepr w)
  where
    LLVMPointerRepr w = IntrinsicRepr knownSymbol (Empty :> CrucibleBVRepr w)

type family ToCrucibleType (tp :: MacawType) :: CrucibleType where
  ToCrucibleType (MacawBVType w) = LLVMPointerType w
  -- ToCrucibleType (M.FloatType fi)  = C.FloatType (ToCrucibleFloatInfo fi)
  -- ToCrucibleType ('M.TupleType l)  = C.StructType (ToCrucibleTypeList l)
  -- ToCrucibleType M.BoolType        = C.BaseToType C.BaseBoolType
  -- ToCrucibleType ('M.VecType n tp) = C.VectorType (ToCrucibleType tp)

type family CtxToCrucibleType (mtp :: Ctx MacawType) :: Ctx CrucibleType where
  CtxToCrucibleType EmptyCtx   = EmptyCtx
  CtxToCrucibleType (c ::> tp) = CtxToCrucibleType c ::> ToCrucibleType tp

typeToCrucible :: MacawTypeRepr tp -> CrucibleTypeRepr (ToCrucibleType tp)
typeToCrucible tp =
  case tp of
    MacawBVTypeRepr w -> LLVMPointerRepr w
    -- M.BoolTypeRepr  -> C.BoolRepr
    -- M.FloatTypeRepr fi -> C.FloatRepr $ floatInfoToCrucible fi
    -- M.TupleTypeRepr a -> C.StructRepr (typeListToCrucible a)
    -- M.VecTypeRepr _n e -> C.VectorRepr (typeToCrucible e)

macawAssignToCruc ::
  (forall tp . f tp -> g (ToCrucibleType tp)) ->
  Assignment f ctx ->
  Assignment g (CtxToCrucibleType ctx)
macawAssignToCruc f a =
  case a of
    Empty -> empty
    b :> x -> macawAssignToCruc f b :> f x

typeCtxToCrucible ::
  Assignment MacawTypeRepr ctx ->
  Assignment CrucibleTypeRepr (CtxToCrucibleType ctx)
typeCtxToCrucible = macawAssignToCruc typeToCrucible

data Updated a
   = Updated   !a
   | Unchanged !a

updatedValue :: Updated a -> a
updatedValue (Updated a) = a
updatedValue (Unchanged a) = a

data Pair (a :: k -> Type) (b :: k -> Type) where
  Pair :: !(a tp) -> !(b tp) -> Pair a b

comparePairKeys :: OrdF k => Pair k a -> Pair k a -> Ordering
comparePairKeys (Pair x _) (Pair y _) = toOrdering (compareF x y)
{-# INLINABLE comparePairKeys #-}

data TreeApp e t
   = BinTree !e !t !t
   | TipTree

class IsBinTree t e | t -> e where
  asBin :: t -> TreeApp e t
  tip :: t

  bin :: e -> t -> t -> t
  binTreeSize :: t -> Int

delta,ratio :: Int
delta = 3
ratio = 2

balanceL :: (IsBinTree c e) => e -> c -> c -> c
balanceL p l r = do
  case asBin l of
    BinTree l_pair ll lr | binTreeSize l > max 1 (delta*binTreeSize r) ->
      case asBin lr of
        BinTree lr_pair lrl lrr | binTreeSize lr >= max 2 (ratio*binTreeSize ll) ->
          bin lr_pair (bin l_pair ll lrl) (bin p lrr r)
        _ -> bin l_pair ll (bin p lr r)

    _ -> bin p l r
{-# INLINE balanceL #-}

balanceR :: (IsBinTree c e) => e -> c -> c -> c
balanceR p l r = do
  case asBin r of
    BinTree r_pair rl rr | binTreeSize r > max 1 (delta*binTreeSize l) ->
      case asBin rl of
        BinTree rl_pair rll rlr | binTreeSize rl >= max 2 (ratio*binTreeSize rr) ->
          (bin rl_pair $! bin p l rll) $! bin r_pair rlr rr
        _ -> bin r_pair (bin p l rl) rr
    _ -> bin p l r
{-# INLINE balanceR #-}

binInsert :: (IsBinTree c e) => (e -> e -> Ordering) -> e -> c -> Updated c
binInsert comp x t =
  case asBin t of
    TipTree -> Updated (bin x tip tip)
    BinTree y l r ->
      case comp x y of
        LT ->
          case binInsert comp x l of
            Updated l'   -> Updated   (balanceL y l' r)
            Unchanged l' -> Unchanged (bin       y l' r)
        GT ->
          case binInsert comp x r of
            Updated r'   -> Updated   (balanceR y l r')
            Unchanged r' -> Unchanged (bin       y l r')
        EQ -> Unchanged (bin x l r)
{-# INLINABLE binInsert #-}

data OrderingF x y where
  LTF :: OrderingF x y
  EQF :: OrderingF x x
  GTF :: OrderingF x y

toOrdering :: OrderingF x y -> Ordering
toOrdering LTF = LT
toOrdering EQF = EQ
toOrdering GTF = GT

class TestEquality ktp => OrdF (ktp :: k -> Type) where
  compareF :: ktp x -> ktp y -> OrderingF x y

class ShowF (f :: k -> Type) where
  showF :: forall tp . f tp -> String

class FunctorF m where
  fmapF :: (forall x . f x -> g x) -> m f -> m g

class FunctorFC (t :: (k -> Type) -> l -> Type) where
  fmapFC :: forall f g. (forall x. f x -> g x) ->
                        (forall x. t f x -> t g x)

data MapF (k :: v -> Type) (a :: v -> Type) where
  Bin :: {-# UNPACK #-}
         !Int
      -> !(k x)
      -> !(a x)
      -> !(MapF k a)
      -> !(MapF k a)
      -> MapF k a
  Tip :: MapF k a

instance FunctorF (MapF ktp) where
  fmapF = mapFMap

instance IsBinTree (MapF k a) (Pair k a) where
  asBin (Bin _ k v l r) = BinTree (Pair k v) l r
  asBin Tip = TipTree

  tip = Tip
  bin (Pair k v) l r = Bin (binTreeSize l + binTreeSize r + 1) k v l r

  binTreeSize Tip              = 0
  binTreeSize (Bin sz _ _ _ _) = sz

mapFEmpty :: MapF k a
mapFEmpty = Tip

mapFInsert :: OrdF k => k tp -> a tp -> MapF k a -> MapF k a
mapFInsert = \k v m -> seq k $ updatedValue (binInsert comparePairKeys (Pair k v) m)
{-# INLINABLE mapFInsert #-}

mapFMap :: (forall tp . f tp -> g tp) -> MapF ktp f -> MapF ktp g
mapFMap f = mapWithKey (\_ x -> f x)

mapWithKey
  :: (forall tp . ktp tp -> f tp -> g tp)
  -> MapF ktp f
  -> MapF ktp g
mapWithKey _ Tip = Tip
mapWithKey f (Bin sx kx x l r) = Bin sx kx (f kx x) (mapWithKey f l) (mapWithKey f r)

mapFLookup :: OrdF k => k tp -> MapF k a -> Maybe (a tp)
mapFLookup k0 = seq k0 (go k0)
  where
    go :: OrdF k => k tp -> MapF k a -> Maybe (a tp)
    go _ Tip = Nothing
    go k (Bin _ kx x l r) =
      case compareF k kx of
        LTF -> go k l
        GTF -> go k r
        EQF -> Just x
{-# INLINABLE mapFLookup #-}

newtype Diff (l :: Ctx k) (r :: Ctx k)
      = Diff { _contextExtSize :: Int }

noDiff :: Diff l l
noDiff = Diff 0
{-# INLINE noDiff #-}

extendRight :: Diff l r -> Diff l (r '::> tp)
extendRight (Diff i) = Diff (i+1)

class KnownDiff (l :: Ctx k) (r :: Ctx k) where
  knownDiff :: Diff l r

instance KnownDiff l l where
  knownDiff = noDiff

instance {-# INCOHERENT #-} KnownDiff l r => KnownDiff l (r '::> tp) where
  knownDiff = extendRight knownDiff

newtype Index (ctx :: Ctx k) (tp :: k) = Index { _indexVal :: Int }

{-# INLINE extendIndex #-}
extendIndex :: KnownDiff l r => Index l tp -> Index r tp
extendIndex = extendIndex' knownDiff

{-# INLINE extendIndex' #-}
extendIndex' :: Diff l r -> Index l tp -> Index r tp
extendIndex' _ = unsafeCoerce

nextIndex :: Size ctx -> Index (ctx ::> tp) tp
nextIndex n = Index (sizeInt n)

data IndexPair ctx tp = IndexPair
  { _macawIndex    :: !(Index ctx tp)
  , _crucibleIndex :: !(Index (CtxToCrucibleType ctx) (ToCrucibleType tp))
  }

extendIndexPair :: IndexPair ctx tp -> IndexPair (ctx::>utp) tp
extendIndexPair (IndexPair i j) = IndexPair (extendIndex i) (extendIndex j)

data SizeView (ctx :: Ctx k) where
  ZeroSize :: SizeView 'EmptyCtx
  IncSize :: !(Size ctx) -> SizeView (ctx '::> tp)

viewSize :: Size ctx -> SizeView ctx
viewSize (Size 0) = unsafeCoerce ZeroSize
viewSize (Size n) = assert (n > 0) (unsafeCoerce (IncSize (Size (n-1))))

type RegIndexMap arch = MapF (ArchReg arch) (IndexPair (ArchRegContext arch))

mkRegIndexMap :: OrdF r
              => Assignment r ctx
              -> Size (CtxToCrucibleType ctx)
              -> MapF r (IndexPair ctx)
mkRegIndexMap Empty _ = mapFEmpty
mkRegIndexMap (a :> r) csz =
  case viewSize csz of
    IncSize csz0 ->
      let m = fmapF extendIndexPair (mkRegIndexMap a csz0)
          idx = IndexPair (nextIndex (size a)) (nextIndex csz0)
       in mapFInsert r idx m

type family ArchReg (arch :: Type) = (reg :: MacawType -> Type) | reg -> arch
type family ArchRegContext (arch :: Type) :: Ctx MacawType
type MacawCrucibleRegTypes (arch :: Type) = CtxToCrucibleType (ArchRegContext arch)

data Some (f :: k -> Type) = forall x . Some (f x)

instance ShowF f => Show (Some f) where
  show (Some x) = showF x
instance ShowF (PPCReg v) where
  showF = show

data AnyPPC (v :: Variant)

data Variant = V32 | V64

type V32 = 'V32
type V64 = 'V64

type family AddrWidth v = w | w -> v where
  AddrWidth V32 = 32
  AddrWidth V64 = 64

addrWidth :: VariantRepr v -> NatRepr (AddrWidth v)
addrWidth V32Repr = knownNat
addrWidth V64Repr = knownNat

data VariantRepr v where
  V32Repr :: VariantRepr V32
  V64Repr :: VariantRepr V64

class (1 <= AddrWidth v, Typeable v) => KnownVariant v where
  knownVariant :: VariantRepr v

instance KnownVariant V32 where
  knownVariant = V32Repr

instance KnownVariant V64 where
  knownVariant = V64Repr

newtype GPR = GPR { unGPR :: Word8 }
  deriving (Eq, Ord, Show)
newtype VSReg = VSReg { unVSReg :: Word8 }
  deriving (Eq, Ord, Show)

data PPCReg (v :: Variant) (tp :: MacawType) where
  PPC_GP :: (w ~ AddrWidth v, 1 <= w) => GPR -> PPCReg v (MacawBVType w)
  PPC_FR :: VSReg -> PPCReg arch (MacawBVType 128)
  PPC_IP :: (w ~ AddrWidth v, 1 <= w) => PPCReg v (MacawBVType w)
  PPC_LNK :: (w ~ AddrWidth v, 1 <= w) => PPCReg v (MacawBVType w)
  PPC_CTR :: (w ~ AddrWidth v, 1 <= w) => PPCReg v (MacawBVType w)
  PPC_CR :: PPCReg v (MacawBVType 32)
  PPC_XER :: (w ~ AddrWidth v, 1 <= w) => PPCReg v (MacawBVType w)
  PPC_FPSCR :: PPCReg v (MacawBVType 32)
  PPC_VSCR :: PPCReg v (MacawBVType 32)

instance Show (PPCReg v tp) where
  show r =
    case r of
      PPC_GP (GPR gpr) -> 'r':show gpr
      PPC_FR (VSReg fr) -> 'f':show fr
      PPC_IP -> "ip"
      PPC_LNK -> "lnk"
      PPC_CTR -> "ctr"
      PPC_CR -> "cr"
      PPC_XER -> "xer"
      PPC_FPSCR -> "fpscr"
      PPC_VSCR -> "vscr"

instance TestEquality (PPCReg v) where
  testEquality = \ x_a1438 y_a1439
      -> case x_a1438 of
           PPC_GP x1_a143a
             -> case y_a1439 of
                  PPC_GP y1_a143b
                    -> if (x1_a143a == y1_a143b) then Just Refl else Nothing
                  _ -> Nothing
           PPC_FR x1_a143c
             -> case y_a1439 of
                  PPC_FR y1_a143d
                    -> if (x1_a143c == y1_a143d) then Just Refl else Nothing
                  _ -> Nothing
           PPC_IP
             -> case y_a1439 of
                  PPC_IP -> Just Refl
                  _ -> Nothing
           PPC_LNK
             -> case y_a1439 of
                  PPC_LNK -> Just Refl
                  _ -> Nothing
           PPC_CTR
             -> case y_a1439 of
                  PPC_CTR -> Just Refl
                  _ -> Nothing
           PPC_CR
             -> case y_a1439 of
                  PPC_CR -> Just Refl
                  _ -> Nothing
           PPC_XER
             -> case y_a1439 of
                  PPC_XER -> Just Refl
                  _ -> Nothing
           PPC_FPSCR
             -> case y_a1439 of
                  PPC_FPSCR -> Just Refl
                  _ -> Nothing
           PPC_VSCR
             -> case y_a1439 of
                  PPC_VSCR -> Just Refl
                  _ -> Nothing

instance OrdF (PPCReg v) where
  compareF = \ x_a1416 y_a1417
      -> let
           yn_a1418 :: Int
           yn_a1418
             = case y_a1417 of
                 PPC_GP {} -> 0
                 PPC_FR {} -> 1
                 PPC_IP {} -> 2
                 PPC_LNK {} -> 3
                 PPC_CTR {} -> 4
                 PPC_CR {} -> 5
                 PPC_XER {} -> 6
                 PPC_FPSCR {} -> 7
                 PPC_VSCR {} -> 8
         in
           case x_a1416 of
             PPC_GP x1_a1419
               -> case y_a1417 of
                    PPC_GP y1_a141a
                      -> case compare x1_a1419 y1_a141a of
                           LT -> LTF
                           GT -> GTF
                           EQ -> EQF
                    _ -> if (0 < yn_a1418) then LTF else GTF
             PPC_FR x1_a141b
               -> case y_a1417 of
                    PPC_FR y1_a141c
                      -> case compare x1_a141b y1_a141c of
                           LT -> LTF
                           GT -> GTF
                           EQ -> EQF
                    _ -> if (1 < yn_a1418) then LTF else GTF
             PPC_IP
               -> case y_a1417 of
                    PPC_IP -> EQF
                    _ -> if (2 < yn_a1418) then LTF else GTF
             PPC_LNK
               -> case y_a1417 of
                    PPC_LNK -> EQF
                    _ -> if (3 < yn_a1418) then LTF else GTF
             PPC_CTR
               -> case y_a1417 of
                    PPC_CTR -> EQF
                    _ -> if (4 < yn_a1418) then LTF else GTF
             PPC_CR
               -> case y_a1417 of
                    PPC_CR -> EQF
                    _ -> if (5 < yn_a1418) then LTF else GTF
             PPC_XER
               -> case y_a1417 of
                    PPC_XER -> EQF
                    _ -> if (6 < yn_a1418) then LTF else GTF
             PPC_FPSCR
               -> case y_a1417 of
                    PPC_FPSCR -> EQF
                    _ -> if (7 < yn_a1418) then LTF else GTF
             PPC_VSCR
               -> case y_a1417 of
                    PPC_VSCR -> EQF
                    _ -> if (8 < yn_a1418) then LTF else GTF

instance (KnownVariant v) => HasRepr (PPCReg v) MacawTypeRepr where
  typeRepr r =
    case r of
      PPC_GP {} -> MacawBVTypeRepr (addrWidth (knownVariant @v))
      PPC_FR {} -> MacawBVTypeRepr n128
      PPC_IP -> MacawBVTypeRepr (addrWidth (knownVariant @v))
      PPC_LNK -> MacawBVTypeRepr (addrWidth (knownVariant @v))
      PPC_CTR -> MacawBVTypeRepr (addrWidth (knownVariant @v))
      PPC_CR -> MacawBVTypeRepr n32
      PPC_XER -> MacawBVTypeRepr (addrWidth (knownVariant @v))
      PPC_FPSCR -> MacawBVTypeRepr n32
      PPC_VSCR -> MacawBVTypeRepr n32

type instance ArchReg (AnyPPC v) = PPCReg v
type instance ArchRegContext (AnyPPC v) = RegContext v
type instance RegAddrWidth (PPCReg v) = AddrWidth v

type family RegAddrWidth (r :: MacawType -> Type) :: Nat
type RegSize v = RegAddrWidth (PPCReg v)
type RegContext v
  =     (EmptyCtx ::> MacawBVType (RegSize v)) -- IP
  <+> (EmptyCtx ::> MacawBVType (RegSize v)) -- LNK
  <+> (EmptyCtx ::> MacawBVType (RegSize v)) -- CTR
  <+> (EmptyCtx ::> MacawBVType (RegSize v)) -- XER
  <+> (EmptyCtx ::> MacawBVType 32)          -- CR
  <+> (EmptyCtx ::> MacawBVType 32)          -- FPSCR
  <+> (EmptyCtx ::> MacawBVType 32)          -- VSCR
  <+> CtxRepeat 32 (MacawBVType (RegSize v))       -- GPRs
  <+> CtxRepeat 64 (MacawBVType 128)               -- VSRs

ppcRegAssignment :: forall v
                  . ( KnownVariant v )
                 => Assignment (PPCReg v) (RegContext v)
ppcRegAssignment =
  (Empty :> PPC_IP
         :> PPC_LNK
         :> PPC_CTR
         :> PPC_XER
         :> PPC_CR
         :> PPC_FPSCR
         :> PPC_VSCR)
  <++> (repeatAssign (PPC_GP . GPR . fromIntegral) :: Assignment (PPCReg v) (CtxRepeat 32 (MacawBVType (RegSize v))))
  <++> (repeatAssign (PPC_FR . VSReg . fromIntegral) :: Assignment (PPCReg v) (CtxRepeat 64 (MacawBVType 128)))

data PPCSymbolicException v = MissingRegisterInState (Some (PPCReg v))
deriving instance Show (PPCSymbolicException v)
instance Typeable v => Exception (PPCSymbolicException v)

class HasRepr (f :: k -> Type) (v :: k -> Type) | f -> v where
  typeRepr :: f tp -> v tp

regIndexMap :: forall v
             . KnownVariant v
            => RegIndexMap (AnyPPC v)
regIndexMap = mkRegIndexMap assgn sz
  where
    assgn = ppcRegAssignment @v
    sz = size (typeCtxToCrucible (fmapFC typeRepr assgn))

updateReg :: forall v ppc m f tp
           . (KnownVariant v,
               ppc ~ AnyPPC v,
               MonadThrow m)
          => PPCReg v tp
          -> (f (ToCrucibleType tp) -> f (ToCrucibleType tp))
          -> Assignment f (MacawCrucibleRegTypes ppc)
          -> m (Assignment f (MacawCrucibleRegTypes ppc))
updateReg r _upd _asgn = do
  case mapFLookup r regIndexMap of
    Nothing -> throwM (MissingRegisterInState (Some r))
    Just _pair -> throwM (MissingRegisterInState (Some r))
    -- Just pair -> return (asgn & MapF.ixF (MSB.crucibleIndex pair) %~ upd)

type family RegValue (sym :: Type) (tp :: CrucibleType) :: Type where
  RegValue sym (StructType ctx) = Assignment (RegValue' sym) ctx

newtype RegValue' sym tp = RV { unRV :: RegValue sym tp }

type ArchRegStruct (arch :: Type) = StructType (MacawCrucibleRegTypes arch)

data RegEntry sym tp = RegEntry { regType :: !(CrucibleTypeRepr tp)
                                , regValue :: !(RegValue sym tp)
                                }

class IsMemoryModel (mem :: Type) where
  type MemModelType mem arch :: CrucibleType
  type MemModelConstraint mem sym :: Constraint

class GenArchInfo mem arch where
  genArchVals :: proxy mem
              -> proxy' arch
              -> Maybe (GenArchVals mem arch)

data GenArchVals mem arch = GenArchVals
  { gavUpdateReg
      :: forall sym tp
       . {-(SymArchConstraints arch, IsSymInterface sym)
      =>-} RegEntry sym (ArchRegStruct arch)
      -> ArchReg arch tp
      -> RegValue sym (ToCrucibleType tp)
      -> RegEntry sym (ArchRegStruct arch)
  }

B.hs

{-# LANGUAGE Haskell2010 #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeOperators #-}
{-# OPTIONS_GHC -Wall -Wno-orphans #-}
module B where

import A

instance IsMemoryModel mem => GenArchInfo mem (AnyPPC V32) where
  genArchVals _ _ = Just $ GenArchVals
    { gavUpdateReg = archUpdateReg
    }

{-# NOINLINE archUpdateReg #-}
archUpdateReg :: ( KnownVariant v
                 , ppc ~ AnyPPC v
                 ) =>
                 RegEntry sym (ArchRegStruct (AnyPPC v))
              -> PPCReg v tp
              -> RegValue sym (ToCrucibleType tp)
              -> RegEntry sym (ArchRegStruct (AnyPPC v))
archUpdateReg regEntry reg val =
  case updateReg reg (const $ RV val) (regValue regEntry) of
    Just r -> regEntry { regValue = r }
    Nothing -> error "archUpdateReg"