{-# LANGUAGE BangPatterns          #-}
{-# LANGUAGE ConstraintKinds       #-}
{-# LANGUAGE DeriveAnyClass        #-}
{-# LANGUAGE DerivingVia           #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE GADTs                 #-}
{-# LANGUAGE LambdaCase            #-}
{-# LANGUAGE NumericUnderscores    #-}
{-# LANGUAGE OverloadedStrings     #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE PatternSynonyms       #-}
{-# LANGUAGE RecordWildCards       #-}
{-# LANGUAGE TemplateHaskell       #-}
{-# LANGUAGE TupleSections         #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeFamilies          #-}
{-# LANGUAGE UndecidableInstances  #-}
{-# LANGUAGE ViewPatterns          #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}
{-# OPTIONS_GHC -Wno-name-shadowing #-}

module Plutus.Contract.Test.Coverage.Analysis.Types where
import Control.Arrow (first)
import Data.Set (Set)
import GHC.Generics (Generic)
import GHC.Stack
import PlutusCore.DeBruijn hiding (DeBruijn)
import PlutusTx.Coverage

import Plutus.Contract.Test.Coverage.Analysis.Common

infixl 5 :>
data SnocList a = Nil | SnocList a :> a
  deriving (a -> SnocList b -> SnocList a
(a -> b) -> SnocList a -> SnocList b
(forall a b. (a -> b) -> SnocList a -> SnocList b)
-> (forall a b. a -> SnocList b -> SnocList a) -> Functor SnocList
forall a b. a -> SnocList b -> SnocList a
forall a b. (a -> b) -> SnocList a -> SnocList b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> SnocList b -> SnocList a
$c<$ :: forall a b. a -> SnocList b -> SnocList a
fmap :: (a -> b) -> SnocList a -> SnocList b
$cfmap :: forall a b. (a -> b) -> SnocList a -> SnocList b
Functor, SnocList a -> Bool
(a -> m) -> SnocList a -> m
(a -> b -> b) -> b -> SnocList a -> b
(forall m. Monoid m => SnocList m -> m)
-> (forall m a. Monoid m => (a -> m) -> SnocList a -> m)
-> (forall m a. Monoid m => (a -> m) -> SnocList a -> m)
-> (forall a b. (a -> b -> b) -> b -> SnocList a -> b)
-> (forall a b. (a -> b -> b) -> b -> SnocList a -> b)
-> (forall b a. (b -> a -> b) -> b -> SnocList a -> b)
-> (forall b a. (b -> a -> b) -> b -> SnocList a -> b)
-> (forall a. (a -> a -> a) -> SnocList a -> a)
-> (forall a. (a -> a -> a) -> SnocList a -> a)
-> (forall a. SnocList a -> [a])
-> (forall a. SnocList a -> Bool)
-> (forall a. SnocList a -> Int)
-> (forall a. Eq a => a -> SnocList a -> Bool)
-> (forall a. Ord a => SnocList a -> a)
-> (forall a. Ord a => SnocList a -> a)
-> (forall a. Num a => SnocList a -> a)
-> (forall a. Num a => SnocList a -> a)
-> Foldable SnocList
forall a. Eq a => a -> SnocList a -> Bool
forall a. Num a => SnocList a -> a
forall a. Ord a => SnocList a -> a
forall m. Monoid m => SnocList m -> m
forall a. SnocList a -> Bool
forall a. SnocList a -> Int
forall a. SnocList a -> [a]
forall a. (a -> a -> a) -> SnocList a -> a
forall m a. Monoid m => (a -> m) -> SnocList a -> m
forall b a. (b -> a -> b) -> b -> SnocList a -> b
forall a b. (a -> b -> b) -> b -> SnocList a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: SnocList a -> a
$cproduct :: forall a. Num a => SnocList a -> a
sum :: SnocList a -> a
$csum :: forall a. Num a => SnocList a -> a
minimum :: SnocList a -> a
$cminimum :: forall a. Ord a => SnocList a -> a
maximum :: SnocList a -> a
$cmaximum :: forall a. Ord a => SnocList a -> a
elem :: a -> SnocList a -> Bool
$celem :: forall a. Eq a => a -> SnocList a -> Bool
length :: SnocList a -> Int
$clength :: forall a. SnocList a -> Int
null :: SnocList a -> Bool
$cnull :: forall a. SnocList a -> Bool
toList :: SnocList a -> [a]
$ctoList :: forall a. SnocList a -> [a]
foldl1 :: (a -> a -> a) -> SnocList a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> SnocList a -> a
foldr1 :: (a -> a -> a) -> SnocList a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> SnocList a -> a
foldl' :: (b -> a -> b) -> b -> SnocList a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> SnocList a -> b
foldl :: (b -> a -> b) -> b -> SnocList a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> SnocList a -> b
foldr' :: (a -> b -> b) -> b -> SnocList a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> SnocList a -> b
foldr :: (a -> b -> b) -> b -> SnocList a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> SnocList a -> b
foldMap' :: (a -> m) -> SnocList a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> SnocList a -> m
foldMap :: (a -> m) -> SnocList a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> SnocList a -> m
fold :: SnocList m -> m
$cfold :: forall m. Monoid m => SnocList m -> m
Foldable, Functor SnocList
Foldable SnocList
Functor SnocList
-> Foldable SnocList
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> SnocList a -> f (SnocList b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    SnocList (f a) -> f (SnocList a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> SnocList a -> m (SnocList b))
-> (forall (m :: * -> *) a.
    Monad m =>
    SnocList (m a) -> m (SnocList a))
-> Traversable SnocList
(a -> f b) -> SnocList a -> f (SnocList b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => SnocList (m a) -> m (SnocList a)
forall (f :: * -> *) a.
Applicative f =>
SnocList (f a) -> f (SnocList a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> SnocList a -> m (SnocList b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> SnocList a -> f (SnocList b)
sequence :: SnocList (m a) -> m (SnocList a)
$csequence :: forall (m :: * -> *) a. Monad m => SnocList (m a) -> m (SnocList a)
mapM :: (a -> m b) -> SnocList a -> m (SnocList b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> SnocList a -> m (SnocList b)
sequenceA :: SnocList (f a) -> f (SnocList a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
SnocList (f a) -> f (SnocList a)
traverse :: (a -> f b) -> SnocList a -> f (SnocList b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> SnocList a -> f (SnocList b)
$cp2Traversable :: Foldable SnocList
$cp1Traversable :: Functor SnocList
Traversable, SnocList a -> SnocList a -> Bool
(SnocList a -> SnocList a -> Bool)
-> (SnocList a -> SnocList a -> Bool) -> Eq (SnocList a)
forall a. Eq a => SnocList a -> SnocList a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SnocList a -> SnocList a -> Bool
$c/= :: forall a. Eq a => SnocList a -> SnocList a -> Bool
== :: SnocList a -> SnocList a -> Bool
$c== :: forall a. Eq a => SnocList a -> SnocList a -> Bool
Eq, Eq (SnocList a)
Eq (SnocList a)
-> (SnocList a -> SnocList a -> Ordering)
-> (SnocList a -> SnocList a -> Bool)
-> (SnocList a -> SnocList a -> Bool)
-> (SnocList a -> SnocList a -> Bool)
-> (SnocList a -> SnocList a -> Bool)
-> (SnocList a -> SnocList a -> SnocList a)
-> (SnocList a -> SnocList a -> SnocList a)
-> Ord (SnocList a)
SnocList a -> SnocList a -> Bool
SnocList a -> SnocList a -> Ordering
SnocList a -> SnocList a -> SnocList a
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (SnocList a)
forall a. Ord a => SnocList a -> SnocList a -> Bool
forall a. Ord a => SnocList a -> SnocList a -> Ordering
forall a. Ord a => SnocList a -> SnocList a -> SnocList a
min :: SnocList a -> SnocList a -> SnocList a
$cmin :: forall a. Ord a => SnocList a -> SnocList a -> SnocList a
max :: SnocList a -> SnocList a -> SnocList a
$cmax :: forall a. Ord a => SnocList a -> SnocList a -> SnocList a
>= :: SnocList a -> SnocList a -> Bool
$c>= :: forall a. Ord a => SnocList a -> SnocList a -> Bool
> :: SnocList a -> SnocList a -> Bool
$c> :: forall a. Ord a => SnocList a -> SnocList a -> Bool
<= :: SnocList a -> SnocList a -> Bool
$c<= :: forall a. Ord a => SnocList a -> SnocList a -> Bool
< :: SnocList a -> SnocList a -> Bool
$c< :: forall a. Ord a => SnocList a -> SnocList a -> Bool
compare :: SnocList a -> SnocList a -> Ordering
$ccompare :: forall a. Ord a => SnocList a -> SnocList a -> Ordering
$cp1Ord :: forall a. Ord a => Eq (SnocList a)
Ord, Int -> SnocList a -> ShowS
[SnocList a] -> ShowS
SnocList a -> String
(Int -> SnocList a -> ShowS)
-> (SnocList a -> String)
-> ([SnocList a] -> ShowS)
-> Show (SnocList a)
forall a. Show a => Int -> SnocList a -> ShowS
forall a. Show a => [SnocList a] -> ShowS
forall a. Show a => SnocList a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SnocList a] -> ShowS
$cshowList :: forall a. Show a => [SnocList a] -> ShowS
show :: SnocList a -> String
$cshow :: forall a. Show a => SnocList a -> String
showsPrec :: Int -> SnocList a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> SnocList a -> ShowS
Show, (forall x. SnocList a -> Rep (SnocList a) x)
-> (forall x. Rep (SnocList a) x -> SnocList a)
-> Generic (SnocList a)
forall x. Rep (SnocList a) x -> SnocList a
forall x. SnocList a -> Rep (SnocList a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (SnocList a) x -> SnocList a
forall a x. SnocList a -> Rep (SnocList a) x
$cto :: forall a x. Rep (SnocList a) x -> SnocList a
$cfrom :: forall a x. SnocList a -> Rep (SnocList a) x
Generic)

instance Semigroup (SnocList a) where
  SnocList a
xs <> :: SnocList a -> SnocList a -> SnocList a
<> SnocList a
Nil       = SnocList a
xs
  SnocList a
xs <> (SnocList a
ys :> a
y) = (SnocList a
xs SnocList a -> SnocList a -> SnocList a
forall a. Semigroup a => a -> a -> a
<> SnocList a
ys) SnocList a -> a -> SnocList a
forall a. SnocList a -> a -> SnocList a
:> a
y

instance Monoid (SnocList a) where
  mempty :: SnocList a
mempty  = SnocList a
forall a. SnocList a
Nil
  mappend :: SnocList a -> SnocList a -> SnocList a
mappend = SnocList a -> SnocList a -> SnocList a
forall a. Semigroup a => a -> a -> a
(<>)

zipWithSnoc :: (a -> b -> c) -> SnocList a -> SnocList b -> SnocList c
zipWithSnoc :: (a -> b -> c) -> SnocList a -> SnocList b -> SnocList c
zipWithSnoc a -> b -> c
_ SnocList a
Nil SnocList b
_               = SnocList c
forall a. SnocList a
Nil
zipWithSnoc a -> b -> c
_ SnocList a
_ SnocList b
Nil               = SnocList c
forall a. SnocList a
Nil
zipWithSnoc a -> b -> c
f (SnocList a
xs :> a
x) (SnocList b
ys :> b
y) = (a -> b -> c) -> SnocList a -> SnocList b -> SnocList c
forall a b c.
(a -> b -> c) -> SnocList a -> SnocList b -> SnocList c
zipWithSnoc a -> b -> c
f SnocList a
xs SnocList b
ys SnocList c -> c -> SnocList c
forall a. SnocList a -> a -> SnocList a
:> a -> b -> c
f a
x b
y

-- *** Domain definitions
-- data DCon ctx = DCon [DTyp ctx] deriving Show
data DCon = DCon [DTyp]
  deriving (Int -> DCon -> ShowS
[DCon] -> ShowS
DCon -> String
(Int -> DCon -> ShowS)
-> (DCon -> String) -> ([DCon] -> ShowS) -> Show DCon
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DCon] -> ShowS
$cshowList :: [DCon] -> ShowS
show :: DCon -> String
$cshow :: DCon -> String
showsPrec :: Int -> DCon -> ShowS
$cshowsPrec :: Int -> DCon -> ShowS
Show, DCon -> DCon -> Bool
(DCon -> DCon -> Bool) -> (DCon -> DCon -> Bool) -> Eq DCon
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DCon -> DCon -> Bool
$c/= :: DCon -> DCon -> Bool
== :: DCon -> DCon -> Bool
$c== :: DCon -> DCon -> Bool
Eq, (forall x. DCon -> Rep DCon x)
-> (forall x. Rep DCon x -> DCon) -> Generic DCon
forall x. Rep DCon x -> DCon
forall x. DCon -> Rep DCon x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep DCon x -> DCon
$cfrom :: forall x. DCon -> Rep DCon x
Generic)

-- data DDat ctx = DDat (isRec : Bool) (x : NamedTyDeBruijn) (k : Kin) (pars : [NamedTyDeBruijn])
--                      [DCon (ctx :> (if rec then Nil else x ::: k) :> (pars ::: _someKinds)]
data DDat = DDat Bool NamedTyDeBruijn Kin [NamedTyDeBruijn] [DCon]
  deriving (Int -> DDat -> ShowS
[DDat] -> ShowS
DDat -> String
(Int -> DDat -> ShowS)
-> (DDat -> String) -> ([DDat] -> ShowS) -> Show DDat
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DDat] -> ShowS
$cshowList :: [DDat] -> ShowS
show :: DDat -> String
$cshow :: DDat -> String
showsPrec :: Int -> DDat -> ShowS
$cshowsPrec :: Int -> DDat -> ShowS
Show, DDat -> DDat -> Bool
(DDat -> DDat -> Bool) -> (DDat -> DDat -> Bool) -> Eq DDat
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DDat -> DDat -> Bool
$c/= :: DDat -> DDat -> Bool
== :: DDat -> DDat -> Bool
$c== :: DDat -> DDat -> Bool
Eq, (forall x. DDat -> Rep DDat x)
-> (forall x. Rep DDat x -> DDat) -> Generic DDat
forall x. Rep DDat x -> DDat
forall x. DDat -> Rep DDat x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep DDat x -> DDat
$cfrom :: forall x. DDat -> Rep DDat x
Generic)

data TyCtxEntry = NamedTyDeBruijn ::: Kin     -- db index always 0 (only used for the name for printing)
                | TyCtxRecDat (SnocList DDat) -- (Mutually) recursive data types
                | TyCtxDat DDat               -- Non-recursive data type
    deriving (Int -> TyCtxEntry -> ShowS
[TyCtxEntry] -> ShowS
TyCtxEntry -> String
(Int -> TyCtxEntry -> ShowS)
-> (TyCtxEntry -> String)
-> ([TyCtxEntry] -> ShowS)
-> Show TyCtxEntry
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [TyCtxEntry] -> ShowS
$cshowList :: [TyCtxEntry] -> ShowS
show :: TyCtxEntry -> String
$cshow :: TyCtxEntry -> String
showsPrec :: Int -> TyCtxEntry -> ShowS
$cshowsPrec :: Int -> TyCtxEntry -> ShowS
Show, TyCtxEntry -> TyCtxEntry -> Bool
(TyCtxEntry -> TyCtxEntry -> Bool)
-> (TyCtxEntry -> TyCtxEntry -> Bool) -> Eq TyCtxEntry
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TyCtxEntry -> TyCtxEntry -> Bool
$c/= :: TyCtxEntry -> TyCtxEntry -> Bool
== :: TyCtxEntry -> TyCtxEntry -> Bool
$c== :: TyCtxEntry -> TyCtxEntry -> Bool
Eq, (forall x. TyCtxEntry -> Rep TyCtxEntry x)
-> (forall x. Rep TyCtxEntry x -> TyCtxEntry) -> Generic TyCtxEntry
forall x. Rep TyCtxEntry x -> TyCtxEntry
forall x. TyCtxEntry -> Rep TyCtxEntry x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep TyCtxEntry x -> TyCtxEntry
$cfrom :: forall x. TyCtxEntry -> Rep TyCtxEntry x
Generic)

-- Γ :> TyCtxRecDat ds  ==>  ds : Dat (Γ :> TyCtxRecDat ds)
-- Γ :> TyCtxDat d      ==>  d  : Dat Γ
type TyCtx = SnocList TyCtxEntry

type Subst a = SnocList a

data Dom = DTop { Dom -> DTyp
ty         :: DTyp
                , Dom -> Int
depth      :: Int
                , Dom -> Set CoverageAnnotation
_locations :: Set CoverageAnnotation }

         | DError

         | DSusp { _locations :: Set CoverageAnnotation
                 , Dom -> Dom
inner      :: Dom }

         | DTySusp { Dom -> NamedTyDeBruijn
suspName   :: NamedTyDeBruijn
                   , Dom -> Kin
kind       :: Kin
                   , _locations :: Set CoverageAnnotation
                   , inner      :: Dom }

         | DIf { Dom -> DTyp
argTy      :: DTyp
               , _locations :: Set CoverageAnnotation }

         | DTrace { argTy      :: DTyp
                  , _locations :: Set CoverageAnnotation }

         | DLoc { Dom -> CoverageAnnotation
location :: CoverageAnnotation }

         | DLam { Dom -> NamedDeBruijn
lamName    :: NamedDeBruijn
                , argTy      :: DTyp        -- DTyp ctx
                , Dom -> Subst Dom
substD     :: Subst Dom   -- Subst _ctx (Dom ctx)
                , Dom -> Subst DTyp
substT     :: Subst DTyp  -- Subst _ctx (DTyp ctx)
                , Dom -> Trm
body       :: Trm         -- Trm (_ctx, x : argTy) -- remember that _ctx is really mixed type and term context - very confusing...
                , _locations :: Set CoverageAnnotation }

         | DConstr { Dom -> DTyp
dat        :: DTyp     -- Target type once fully applied
                   , Dom -> Int
constr     :: Int
                   , Dom -> Subst Dom
argsD      :: SnocList Dom
                   , _locations :: Set CoverageAnnotation }

         | DMatch { dat        :: DTyp
                  , _locations :: Set CoverageAnnotation }

         | DUnion [Dom] -- These are never DWeaken

         | DWeaken { Dom -> Weakening
wk    :: Weakening
                   , inner :: Dom }
  deriving (Int -> Dom -> ShowS
[Dom] -> ShowS
Dom -> String
(Int -> Dom -> ShowS)
-> (Dom -> String) -> ([Dom] -> ShowS) -> Show Dom
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Dom] -> ShowS
$cshowList :: [Dom] -> ShowS
show :: Dom -> String
$cshow :: Dom -> String
showsPrec :: Int -> Dom -> ShowS
$cshowsPrec :: Int -> Dom -> ShowS
Show, (forall x. Dom -> Rep Dom x)
-> (forall x. Rep Dom x -> Dom) -> Generic Dom
forall x. Rep Dom x -> Dom
forall x. Dom -> Rep Dom x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Dom x -> Dom
$cfrom :: forall x. Dom -> Rep Dom x
Generic)

data DTyp = DTVar NamedTyDeBruijn [DTyp]
          | DTFun DTyp DTyp
          | DTLam { DTyp -> NamedTyDeBruijn
dtName :: NamedTyDeBruijn, DTyp -> Kin
dtKind :: Kin, DTyp -> DTyp
dtBody :: DTyp }
          | DTForall { dtName :: NamedTyDeBruijn, dtKind :: Kin, dtBody :: DTyp }
          | DTWk { DTyp -> Weakening
dtWk :: Weakening , dtBody :: DTyp }
          | DTyBuiltin Kin -- we don't care which
  deriving (Int -> DTyp -> ShowS
[DTyp] -> ShowS
DTyp -> String
(Int -> DTyp -> ShowS)
-> (DTyp -> String) -> ([DTyp] -> ShowS) -> Show DTyp
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DTyp] -> ShowS
$cshowList :: [DTyp] -> ShowS
show :: DTyp -> String
$cshow :: DTyp -> String
showsPrec :: Int -> DTyp -> ShowS
$cshowsPrec :: Int -> DTyp -> ShowS
Show, DTyp -> DTyp -> Bool
(DTyp -> DTyp -> Bool) -> (DTyp -> DTyp -> Bool) -> Eq DTyp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: DTyp -> DTyp -> Bool
$c/= :: DTyp -> DTyp -> Bool
== :: DTyp -> DTyp -> Bool
$c== :: DTyp -> DTyp -> Bool
Eq, (forall x. DTyp -> Rep DTyp x)
-> (forall x. Rep DTyp x -> DTyp) -> Generic DTyp
forall x. Rep DTyp x -> DTyp
forall x. DTyp -> Rep DTyp x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep DTyp x -> DTyp
$cfrom :: forall x. DTyp -> Rep DTyp x
Generic)

data DArg = TyArg DTyp | DArg Dom
  deriving (Int -> DArg -> ShowS
[DArg] -> ShowS
DArg -> String
(Int -> DArg -> ShowS)
-> (DArg -> String) -> ([DArg] -> ShowS) -> Show DArg
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DArg] -> ShowS
$cshowList :: [DArg] -> ShowS
show :: DArg -> String
$cshow :: DArg -> String
showsPrec :: Int -> DArg -> ShowS
$cshowsPrec :: Int -> DArg -> ShowS
Show)

-- strictness?
newtype Weakening = Wk [(Index, Index)] -- increasing in k, (k, n) means weaken by n at index k (cumulative)
  deriving (Int -> Weakening -> ShowS
[Weakening] -> ShowS
Weakening -> String
(Int -> Weakening -> ShowS)
-> (Weakening -> String)
-> ([Weakening] -> ShowS)
-> Show Weakening
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Weakening] -> ShowS
$cshowList :: [Weakening] -> ShowS
show :: Weakening -> String
$cshow :: Weakening -> String
showsPrec :: Int -> Weakening -> ShowS
$cshowsPrec :: Int -> Weakening -> ShowS
Show, Weakening -> Weakening -> Bool
(Weakening -> Weakening -> Bool)
-> (Weakening -> Weakening -> Bool) -> Eq Weakening
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Weakening -> Weakening -> Bool
$c/= :: Weakening -> Weakening -> Bool
== :: Weakening -> Weakening -> Bool
$c== :: Weakening -> Weakening -> Bool
Eq, (forall x. Weakening -> Rep Weakening x)
-> (forall x. Rep Weakening x -> Weakening) -> Generic Weakening
forall x. Rep Weakening x -> Weakening
forall x. Weakening -> Rep Weakening x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Weakening x -> Weakening
$cfrom :: forall x. Weakening -> Rep Weakening x
Generic)

wkIndex :: HasCallStack => Weakening -> Index -> Index
wkIndex :: Weakening -> Index -> Index
wkIndex (Wk [(Index, Index)]
w) Index
i = Index
i Index -> Index -> Index
forall a. Num a => a -> a -> a
+ [Index] -> Index
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [ Index
n | (Index
k, Index
n) <- [(Index, Index)]
w, Index
i Index -> Index -> Bool
forall a. Ord a => a -> a -> Bool
>= Index
k ]

wkBy :: HasCallStack => Index -> Weakening
wkBy :: Index -> Weakening
wkBy Index
n | Index
n Index -> Index -> Bool
forall a. Eq a => a -> a -> Bool
== Index
0    = [(Index, Index)] -> Weakening
Wk []
       | Bool
otherwise = [(Index, Index)] -> Weakening
Wk [(Index
0, Index
n)]

shiftWeakening :: HasCallStack => Weakening -> Weakening
shiftWeakening :: Weakening -> Weakening
shiftWeakening (Wk [(Index, Index)]
w) = [(Index, Index)] -> Weakening
Wk ([(Index, Index)] -> Weakening) -> [(Index, Index)] -> Weakening
forall a b. (a -> b) -> a -> b
$ ((Index, Index) -> (Index, Index))
-> [(Index, Index)] -> [(Index, Index)]
forall a b. (a -> b) -> [a] -> [b]
map ((Index -> Index) -> (Index, Index) -> (Index, Index)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (b, d) (c, d)
first Index -> Index
forall a. Enum a => a -> a
succ) [(Index, Index)]
w

instance Semigroup Weakening where
  Wk [(Index, Index)]
w <> :: Weakening -> Weakening -> Weakening
<> (Wk [(Index, Index)]
w') = [(Index, Index)] -> Weakening
Wk ([(Index, Index)] -> Weakening) -> [(Index, Index)] -> Weakening
forall a b. (a -> b) -> a -> b
$ ([(Index, Index)] -> [(Index, Index)] -> [(Index, Index)])
-> [(Index, Index)] -> [[(Index, Index)]] -> [(Index, Index)]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr [(Index, Index)] -> [(Index, Index)] -> [(Index, Index)]
forall a b. (Num b, Ord a) => [(a, b)] -> [(a, b)] -> [(a, b)]
merge [(Index, Index)]
w' (((Index, Index) -> [(Index, Index)])
-> [(Index, Index)] -> [[(Index, Index)]]
forall a b. (a -> b) -> [a] -> [b]
map ([(Index, Index)] -> (Index, Index) -> [(Index, Index)]
forall a b. (Ord a, Num a) => [(a, a)] -> (a, b) -> [(a, b)]
unweaken [(Index, Index)]
w') [(Index, Index)]
w)
    where
      unweaken :: [(a, a)] -> (a, b) -> [(a, b)]
unweaken [] (a
k, b
i)           = [(a
k, b
i)]
      unweaken ((a
k', a
i'):[(a, a)]
w) (a
k, b
i)
        | a
k' a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
k   = [(a, a)] -> (a, b) -> [(a, b)]
unweaken [(a, a)]
w (if a
i' a -> a -> Bool
forall a. Ord a => a -> a -> Bool
> a
k then a
k' else a -> a -> a
forall a. Ord a => a -> a -> a
max a
k' (a
k a -> a -> a
forall a. Num a => a -> a -> a
- a
i'), b
i)
        | Bool
otherwise = [(a
k, b
i)]

      merge :: [(a, b)] -> [(a, b)] -> [(a, b)]
merge w1 :: [(a, b)]
w1@((a
k1, b
n1) : [(a, b)]
w1') w2 :: [(a, b)]
w2@((a
k2, b
n2) : [(a, b)]
w2')
        | a
k1 a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
k2  = (a
k1, b
n1 b -> b -> b
forall a. Num a => a -> a -> a
+ b
n2) (a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
: [(a, b)] -> [(a, b)] -> [(a, b)]
merge [(a, b)]
w1' [(a, b)]
w2'
        | a
k1 a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
k2   = (a
k1, b
n1) (a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
: [(a, b)] -> [(a, b)] -> [(a, b)]
merge [(a, b)]
w1' [(a, b)]
w2
        | Bool
otherwise = (a
k2, b
n2) (a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
: [(a, b)] -> [(a, b)] -> [(a, b)]
merge [(a, b)]
w1 [(a, b)]
w2'
      merge [] [(a, b)]
w2 = [(a, b)]
w2
      merge [(a, b)]
w1 [] = [(a, b)]
w1

instance Monoid Weakening where
  mempty :: Weakening
mempty = [(Index, Index)] -> Weakening
Wk []
  mappend :: Weakening -> Weakening -> Weakening
mappend = Weakening -> Weakening -> Weakening
forall a. Semigroup a => a -> a -> a
(<>)

-- Some helper functions
topLevelLocations :: HasCallStack => Dom -> Set CoverageAnnotation
topLevelLocations :: Dom -> Set CoverageAnnotation
topLevelLocations (DUnion [Dom]
ds)   = (Dom -> Set CoverageAnnotation) -> [Dom] -> Set CoverageAnnotation
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap HasCallStack => Dom -> Set CoverageAnnotation
Dom -> Set CoverageAnnotation
topLevelLocations [Dom]
ds
topLevelLocations (DWeaken Weakening
_ Dom
d) = HasCallStack => Dom -> Set CoverageAnnotation
Dom -> Set CoverageAnnotation
topLevelLocations Dom
d
topLevelLocations Dom
DError        = Set CoverageAnnotation
forall a. Monoid a => a
mempty
topLevelLocations DLoc{}        = Set CoverageAnnotation
forall a. Monoid a => a
mempty
topLevelLocations Dom
d             = Dom -> Set CoverageAnnotation
_locations Dom
d