{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

-- | Provides variables (V era t), and mappings of them to objects of type 't'
module Test.Cardano.Ledger.Constrained.Env (
  V (V, VRaw),
  pV,
  Field (..),
  AnyF (..),
  vToField,
  fieldToV,
  Env (..),
  Payload (..),
  emptyEnv,
  findVar,
  storeVar,
  findName,
  storeName,
  restrictEnv,
  P (..),
  bulkStore,
  Name (..),
  Access (..),
  otherFromEnv,
  sameName,
) where

import Cardano.Ledger.Era (Era)
import Data.Hashable
import Data.List (intercalate)
import qualified Data.List as List
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Universe (Shape (..), Shaped (..))
import Lens.Micro
import Test.Cardano.Ledger.Constrained.Monad (Typed (..), failT)
import Test.Cardano.Ledger.Constrained.TypeRep
import Test.Cardano.Ledger.Generic.Proof (BabbageEra, ConwayEra, StandardCrypto)

-- ================================================================
-- V

-- | A proto variable. May or may not contain a Lens (encoded as Access)
data V era t where
  VRaw :: Era era => String -> Rep era t -> Int -> Access era s t -> V era t

data Access era s t where
  Yes :: Rep era s -> Lens' s t -> Access era s t
  No :: Access era s t

instance Show (V era t) where
  show :: V era t -> String
show (VRaw String
nm Rep era t
rep Int
_ Access era s t
_) = String
nm forall a. [a] -> [a] -> [a]
++ String
" :: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Rep era t
rep

-- | We make hashing of 'V' cheap by memoizing most of the hash computation in in the
--   3rd argument of 'VRaw', we provide this pattern to hide this from every other use.
pattern V :: () => Era era => String -> Rep era t -> Access era s t -> V era t
pattern $bV :: forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
$mV :: forall {r} {era} {t}.
V era t
-> (forall {s}.
    Era era =>
    String -> Rep era t -> Access era s t -> r)
-> ((# #) -> r)
-> r
V s r a <- VRaw s r _ a
  where
    V String
s Rep era t
r Access era s t
a = forall era t t.
Era era =>
String -> Rep era t -> Int -> Access era t t -> V era t
VRaw String
s Rep era t
r (Int
0 forall a. Hashable a => Int -> a -> Int
`hashWithSalt` String
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Rep era t
r) Access era s t
a

-- | Construct a V, dsicharging the (Era era) constraint, using the Proof
pV :: Proof era -> String -> Rep era t -> Access era s t -> V era t
pV :: forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
Shelley = forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V
pV Proof era
Allegra = forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V
pV Proof era
Mary = forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V
pV Proof era
Alonzo = forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V
pV Proof era
Babbage = forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V
pV Proof era
Conway = forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V

{-# COMPLETE V #-}

-- ===========================================================
-- Name

-- | An existentially quantified (V era t), hiding the 't'
--   The Hashable instance is inherited from 'V'
data Name era where
  Name :: V era t -> Name era

instance Show (Name era) where
  show :: Name era -> String
show (Name (VRaw String
n Rep era t
_ Int
_ Access era s t
_)) = String
n

-- | Does not satisfy extensionality
instance Eq (Name era) where
  Name (V String
n1 Rep era t
rep1 Access era s t
_) == :: Name era -> Name era -> Bool
== Name (V String
n2 Rep era t
rep2 Access era s t
_) = case forall {k} (t :: k -> *) (i :: k) (j :: k).
Singleton t =>
t i -> t j -> Maybe (i :~: j)
testEql Rep era t
rep1 Rep era t
rep2 of
    Maybe (t :~: t)
Nothing -> Bool
False
    Just t :~: t
Refl -> String
n1 forall a. Eq a => a -> a -> Bool
== String
n2
  {-# INLINE (==) #-}

instance Ord (Name era) where
  {-# SPECIALIZE instance Ord (Name (BabbageEra StandardCrypto)) #-}
  {-# SPECIALIZE instance Ord (Name (ConwayEra StandardCrypto)) #-}
  compare :: Name era -> Name era -> Ordering
compare (Name (V String
n1 Rep era t
rep1 Access era s t
_)) (Name (V String
n2 Rep era t
rep2 Access era s t
_)) =
    case forall a. Ord a => a -> a -> Ordering
compare String
n1 String
n2 of
      Ordering
EQ -> forall {k} (t :: k -> *) (a :: k) (b :: k).
Singleton t =>
t a -> t b -> Ordering
cmpIndex Rep era t
rep1 Rep era t
rep2
      Ordering
other -> Ordering
other
  {-# INLINE compare #-}

sameName :: V era t -> V era s -> Maybe (t :~: s)
sameName :: forall era t s. V era t -> V era s -> Maybe (t :~: s)
sameName (V String
x Rep era t
r1 Access era s t
_) (V String
y Rep era s
r2 Access era s s
_) | String
x forall a. Eq a => a -> a -> Bool
== String
y = forall {k} (t :: k -> *) (i :: k) (j :: k).
Singleton t =>
t i -> t j -> Maybe (i :~: j)
testEql Rep era t
r1 Rep era s
r2
sameName V era t
_ V era s
_ = forall a. Maybe a
Nothing

-- ================================================================
-- Field

-- | Fields are like V, except they expose the type of the Lens
data Field era s t where
  Field :: Era era => String -> Rep era t -> Rep era s -> Lens' s t -> Field era s t
  FConst :: Rep era t -> t -> Rep era s -> Lens' s t -> Field era s t

-- SubField :: String -> Rep era t -> Access era s t -> Field era t r -> Field era s t

instance Show (Field era s t) where
  show :: Field era s t -> String
show (Field String
n Rep era t
t Rep era s
s Lens' s t
_) = forall a. [a] -> [[a]] -> [a]
intercalate String
" " [String
"Field", forall a. Show a => a -> String
show String
n, forall a. Show a => a -> String
show Rep era s
s, forall a. Show a => a -> String
show Rep era t
t]
  show (FConst Rep era t
r t
t Rep era s
_ Lens' s t
_) = String
"FConst " forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis Rep era t
r t
t

-- | Hide the type of 't' in a Field.
data AnyF era s where
  AnyF :: -- Eq t =>
    Field era s t -> AnyF era s

instance Show (AnyF era s) where
  show :: AnyF era s -> String
show (AnyF (Field String
n Rep era t
r Rep era s
t Lens' s t
_)) = String
"Field " forall a. [a] -> [a] -> [a]
++ String
n forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Rep era s
t forall a. [a] -> [a] -> [a]
++ String
" " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Rep era t
r
  show (AnyF (FConst Rep era t
r t
t Rep era s
_ Lens' s t
_)) = String
"FConst " forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis Rep era t
r t
t

vToField :: Era era => Rep era s -> V era t -> Typed (Field era s t)
vToField :: forall era s t.
Era era =>
Rep era s -> V era t -> Typed (Field era s t)
vToField Rep era s
reps (V String
name Rep era t
rept (Yes Rep era s
reps' Lens' s t
l)) = case forall {k} (t :: k -> *) (i :: k) (j :: k).
Singleton t =>
t i -> t j -> Maybe (i :~: j)
testEql Rep era s
reps Rep era s
reps' of
  Just s :~: s
Refl -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall era t s.
Era era =>
String -> Rep era t -> Rep era s -> Lens' s t -> Field era s t
Field String
name Rep era t
rept Rep era s
reps Lens' s t
l
  Maybe (s :~: s)
Nothing ->
    forall a. [String] -> Typed a
failT
      [ String
"Given rep and lens target do not match: "
      , String
"rep: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Rep era s
reps
      , String
"lens target: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Rep era s
reps'
      ]
vToField Rep era s
_ v :: V era t
v@(V String
_ Rep era t
_ Access era s t
No) = forall a. [String] -> Typed a
failT [String
"Cannot convert a V with a No access to a Field", forall a. Show a => a -> String
show V era t
v]

fieldToV :: Era era => Field era s t -> Typed (V era t)
fieldToV :: forall era s t. Era era => Field era s t -> Typed (V era t)
fieldToV (Field String
name Rep era t
rep Rep era s
repx Lens' s t
l) = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall era t s.
Era era =>
String -> Rep era t -> Access era s t -> V era t
V String
name Rep era t
rep (forall era s t. Rep era s -> Lens' s t -> Access era s t
Yes Rep era s
repx Lens' s t
l)
fieldToV (FConst Rep era t
_ t
_ Rep era s
_ Lens' s t
_) = forall a. [String] -> Typed a
failT [String
"Cannot convert a FieldConst to a V"]

-- ===================================================
-- Env

data Payload era where
  Payload :: Rep era t -> t -> Access era s t -> Payload era

newtype Env era = Env (Map String (Payload era))

instance Show (Env era) where
  show :: Env era -> String
show (Env Map String (Payload era)
m) = [String] -> String
unlines (forall a b. (a -> b) -> [a] -> [b]
map forall {era}. (String, Payload era) -> String
f (forall k a. Map k a -> [(k, a)]
Map.toList Map String (Payload era)
m))
    where
      f :: (String, Payload era) -> String
f (String
nm, Payload Rep era t
rep t
t Access era s t
_) = String
nm forall a. [a] -> [a] -> [a]
++ String
" -> " forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis Rep era t
rep t
t

emptyEnv :: Env era
emptyEnv :: forall era. Env era
emptyEnv = forall era. Map String (Payload era) -> Env era
Env forall k a. Map k a
Map.empty

findVar :: V era t -> Env era -> Typed t
findVar :: forall era t. V era t -> Env era -> Typed t
findVar (V String
name Rep era t
rep1 Access era s t
_) (Env Map String (Payload era)
m) =
  case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
name Map String (Payload era)
m of
    Maybe (Payload era)
Nothing -> forall a. [String] -> Typed a
failT [String
"Cannot find " forall a. [a] -> [a] -> [a]
++ String
name forall a. [a] -> [a] -> [a]
++ String
" in env"]
    Just (Payload Rep era t
rep2 t
t Access era s t
_) ->
      case forall {k} (t :: k -> *) (i :: k) (j :: k).
Singleton t =>
t i -> t j -> Maybe (i :~: j)
testEql Rep era t
rep1 Rep era t
rep2 of
        Just t :~: t
Refl -> forall (f :: * -> *) a. Applicative f => a -> f a
pure t
t
        Maybe (t :~: t)
Nothing ->
          forall a. [String] -> Typed a
failT
            [String
"We found: " forall a. [a] -> [a] -> [a]
++ String
name forall a. [a] -> [a] -> [a]
++ String
", but the types did not match. " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Rep era t
rep1 forall a. [a] -> [a] -> [a]
++ String
" =/= " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Rep era t
rep2]

storeVar :: V era t -> t -> Env era -> Env era
storeVar :: forall era t. V era t -> t -> Env era -> Env era
storeVar (V String
name Rep era t
rep Access era s t
access) t
t (Env Map String (Payload era)
m) = forall era. Map String (Payload era) -> Env era
Env (forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
name (forall era t s. Rep era t -> t -> Access era s t -> Payload era
Payload Rep era t
rep t
t Access era s t
access) Map String (Payload era)
m)

-- | Untyped version of 'findVar'.
findName :: Name era -> Env era -> Maybe (Payload era)
findName :: forall era. Name era -> Env era -> Maybe (Payload era)
findName (Name (V String
name Rep era t
_ Access era s t
_)) (Env Map String (Payload era)
env) = forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
name Map String (Payload era)
env

-- | Untyped version of 'storeVar'.
storeName :: Name era -> Payload era -> Env era -> Env era
storeName :: forall era. Name era -> Payload era -> Env era -> Env era
storeName (Name (V String
name Rep era t
_ Access era s t
_)) Payload era
p (Env Map String (Payload era)
env) = forall era. Map String (Payload era) -> Env era
Env forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert String
name Payload era
p Map String (Payload era)
env

-- | Drop any names that are not in the given list from an environment.
restrictEnv :: [Name era] -> Env era -> Env era
restrictEnv :: forall era. [Name era] -> Env era -> Env era
restrictEnv [Name era]
names (Env Map String (Payload era)
env) = forall era. Map String (Payload era) -> Env era
Env forall a b. (a -> b) -> a -> b
$ forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\String
x Payload era
_ -> forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem String
x [String]
xs) Map String (Payload era)
env
  where
    xs :: [String]
xs = [String
x | Name (V String
x Rep era t
_ Access era s t
_) <- [Name era]
names]

otherFromEnv :: [String] -> Env era -> [String]
otherFromEnv :: forall era. [String] -> Env era -> [String]
otherFromEnv [String]
known (Env Map String (Payload era)
m) = [String
n forall a. [a] -> [a] -> [a]
++ String
" = " forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis Rep era t
r t
t | (String
n, Payload Rep era t
r t
t Access era s t
_) <- forall k a. Map k a -> [(k, a)]
Map.toList Map String (Payload era)
m, Bool -> Bool
not (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem String
n [String]
known)]

-- ============================================
-- Group a bunch of bindings into a list

data P era where
  P :: V era t -> t -> P era

instance Show (P era) where
  show :: P era -> String
show (P (V String
nm Rep era t
rep Access era s t
_) t
t) = String
nm forall a. [a] -> [a] -> [a]
++ String
" = " forall a. [a] -> [a] -> [a]
++ forall e t. Rep e t -> t -> String
synopsis Rep era t
rep t
t
  showList :: [P era] -> ShowS
showList [P era]
xs String
ans = [String] -> String
unlines (String
ans forall a. a -> [a] -> [a]
: (forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show [P era]
xs))

bulkStore :: [P era] -> Env era -> Env era
bulkStore :: forall era. [P era] -> Env era -> Env era
bulkStore [P era]
ps Env era
env = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' forall {era}. Env era -> P era -> Env era
accum Env era
env [P era]
ps
  where
    accum :: Env era -> P era -> Env era
accum Env era
e (P V era t
v t
t) = forall era t. V era t -> t -> Env era -> Env era
storeVar V era t
v t
t Env era
e

-- ==========================================================================
--  Hashable instances so we can make HashSets of Name
--  Something like 60% of all time consumed involves manipulating sets of Name
--  If the set is Data.Set, then we need instance Ord (Name era). This is very expensive
--  So instead we use Data.HashSet where we need instance Hashable(Name era). We can
--  make this very cheap by memoizing most of the hash computation in 'V' in the
--  constructor 'VRaw' and hiding 'VRaw' with pattern 'V'

-- | Inheriting the Hashable instancefor types that have Shapes, Works for types whose
--   Shaped instances don't mention 'Esc', Like Evidence, Proof, Rep
--   But we CANNOT use this strategy for (V era t)  since its's Shape instance use Esc
instance Hashable (Shape a) where
  hashWithSalt :: Int -> Shape a -> Int
hashWithSalt Int
s (Nullary Int
n) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
0 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
n
  hashWithSalt Int
s (Nary Int
n [Shape a]
xs) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
1 :: Int) forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
n forall a. Hashable a => Int -> a -> Int
`hashWithSalt` [Shape a]
xs
  hashWithSalt Int
s (Esc a t
_ t
_) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (Int
2 :: Int)
  {-# INLINE hashWithSalt #-}

instance Hashable (Proof e) where
  hashWithSalt :: Int -> Proof e -> Int
hashWithSalt Int
s Proof e
x = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` (forall {k} (t :: k -> *) (rep :: * -> *) (i :: k).
Shaped t rep =>
t i -> Shape rep
shape Proof e
x)
  {-# INLINE hashWithSalt #-}

instance Eq (Proof e) where
  Proof e
x == :: Proof e -> Proof e -> Bool
== Proof e
y = forall {k} (t :: k -> *) (rep :: * -> *) (i :: k).
Shaped t rep =>
t i -> Shape rep
shape Proof e
x forall a. Eq a => a -> a -> Bool
== forall {k} (t :: k -> *) (rep :: * -> *) (i :: k).
Shaped t rep =>
t i -> Shape rep
shape Proof e
y
  {-# INLINE (==) #-}

instance Hashable (Rep e t) where
  hashWithSalt :: Int -> Rep e t -> Int
hashWithSalt Int
s Rep e t
r = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` forall era t. Rep era t -> TypeRep
typeRepOf Rep e t
r
  {-# INLINE hashWithSalt #-}

instance Eq (Rep e t) where
  Rep e t
x == :: Rep e t -> Rep e t -> Bool
== Rep e t
y = forall era t. Rep era t -> TypeRep
typeRepOf Rep e t
x forall a. Eq a => a -> a -> Bool
== forall era t. Rep era t -> TypeRep
typeRepOf Rep e t
y
  {-# INLINE (==) #-}

instance Hashable (V era t) where
  hashWithSalt :: Int -> V era t -> Int
hashWithSalt Int
s (VRaw String
_ Rep era t
_ Int
h Access era s t
_) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
h
  {-# INLINE hashWithSalt #-}

instance Eq (V era t) where
  (V String
n1 Rep era t
r1 Access era s t
_) == :: V era t -> V era t -> Bool
== (V String
n2 Rep era t
r2 Access era s t
_) = String
n1 forall a. Eq a => a -> a -> Bool
== String
n2 Bool -> Bool -> Bool
&& Rep era t
r1 forall a. Eq a => a -> a -> Bool
== Rep era t
r2
  {-# INLINE (==) #-}

instance Era era => Hashable (Name era) where
  hashWithSalt :: Int -> Name era -> Int
hashWithSalt Int
s (Name (VRaw String
_ Rep era t
_ Int
h Access era s t
_)) = Int
s forall a. Hashable a => Int -> a -> Int
`hashWithSalt` Int
h
  {-# INLINE hashWithSalt #-}