{-# OPTIONS_GHC -Wno-orphans #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RoleAnnotations #-}
{-# LANGUAGE ScopedTypeVariables #-}
module GHC.Core.Coercion.Axiom (
BranchFlag, Branched, Unbranched, BranchIndex, Branches(..),
manyBranches, unbranched,
fromBranches, numBranches,
mapAccumBranches,
CoAxiom(..), CoAxBranch(..),
toBranchedAxiom, toUnbranchedAxiom,
coAxiomName, coAxiomArity, coAxiomBranches,
coAxiomTyCon, isImplicitCoAxiom, coAxiomNumPats,
coAxiomNthBranch, coAxiomSingleBranch_maybe, coAxiomRole,
coAxiomSingleBranch, coAxBranchTyVars, coAxBranchCoVars,
coAxBranchRoles,
coAxBranchLHS, coAxBranchRHS, coAxBranchSpan, coAxBranchIncomps,
placeHolderIncomps,
Role(..), fsFromRole,
CoAxiomRule(..), TypeEqn,
BuiltInSynFamily(..), trivialBuiltInFamily
) where
import GHC.Prelude
import Language.Haskell.Syntax.Basic (Role(..))
import {-# SOURCE #-} GHC.Core.TyCo.Rep ( Type )
import {-# SOURCE #-} GHC.Core.TyCo.Ppr ( pprType, pprTyVar )
import {-# SOURCE #-} GHC.Core.TyCon ( TyCon )
import GHC.Utils.Outputable
import GHC.Data.FastString
import GHC.Types.Name
import GHC.Types.Unique
import GHC.Types.Var
import GHC.Utils.Misc
import GHC.Utils.Binary
import GHC.Utils.Panic
import GHC.Utils.Panic.Plain
import GHC.Data.Pair
import GHC.Types.Basic
import Data.Typeable ( Typeable )
import GHC.Types.SrcLoc
import qualified Data.Data as Data
import Data.Array
import Data.List ( mapAccumL )
type BranchIndex = Int
data BranchFlag = Branched | Unbranched
type Branched = 'Branched
type Unbranched = 'Unbranched
newtype Branches (br :: BranchFlag)
= MkBranches { forall (br :: BranchFlag).
Branches br -> Array BranchIndex CoAxBranch
unMkBranches :: Array BranchIndex CoAxBranch }
type role Branches nominal
manyBranches :: [CoAxBranch] -> Branches Branched
manyBranches :: [CoAxBranch] -> Branches Branched
manyBranches [CoAxBranch]
brs = Bool
-> (Array BranchIndex CoAxBranch -> Branches Branched)
-> Array BranchIndex CoAxBranch
-> Branches Branched
forall a. HasCallStack => Bool -> a -> a
assert ((BranchIndex, BranchIndex) -> BranchIndex
forall a b. (a, b) -> b
snd (BranchIndex, BranchIndex)
bnds BranchIndex -> BranchIndex -> Bool
forall a. Ord a => a -> a -> Bool
>= (BranchIndex, BranchIndex) -> BranchIndex
forall a b. (a, b) -> a
fst (BranchIndex, BranchIndex)
bnds )
Array BranchIndex CoAxBranch -> Branches Branched
forall (br :: BranchFlag).
Array BranchIndex CoAxBranch -> Branches br
MkBranches ((BranchIndex, BranchIndex)
-> [CoAxBranch] -> Array BranchIndex CoAxBranch
forall i e. Ix i => (i, i) -> [e] -> Array i e
listArray (BranchIndex, BranchIndex)
bnds [CoAxBranch]
brs)
where
bnds :: (BranchIndex, BranchIndex)
bnds = (BranchIndex
0, [CoAxBranch] -> BranchIndex
forall a. [a] -> BranchIndex
forall (t :: * -> *) a. Foldable t => t a -> BranchIndex
length [CoAxBranch]
brs BranchIndex -> BranchIndex -> BranchIndex
forall a. Num a => a -> a -> a
- BranchIndex
1)
unbranched :: CoAxBranch -> Branches Unbranched
unbranched :: CoAxBranch -> Branches Unbranched
unbranched CoAxBranch
br = Array BranchIndex CoAxBranch -> Branches Unbranched
forall (br :: BranchFlag).
Array BranchIndex CoAxBranch -> Branches br
MkBranches ((BranchIndex, BranchIndex)
-> [CoAxBranch] -> Array BranchIndex CoAxBranch
forall i e. Ix i => (i, i) -> [e] -> Array i e
listArray (BranchIndex
0, BranchIndex
0) [CoAxBranch
br])
toBranched :: Branches br -> Branches Branched
toBranched :: forall (br :: BranchFlag). Branches br -> Branches Branched
toBranched = Array BranchIndex CoAxBranch -> Branches Branched
forall (br :: BranchFlag).
Array BranchIndex CoAxBranch -> Branches br
MkBranches (Array BranchIndex CoAxBranch -> Branches Branched)
-> (Branches br -> Array BranchIndex CoAxBranch)
-> Branches br
-> Branches Branched
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Branches br -> Array BranchIndex CoAxBranch
forall (br :: BranchFlag).
Branches br -> Array BranchIndex CoAxBranch
unMkBranches
toUnbranched :: Branches br -> Branches Unbranched
toUnbranched :: forall (br :: BranchFlag). Branches br -> Branches Unbranched
toUnbranched (MkBranches Array BranchIndex CoAxBranch
arr) = Bool
-> (Array BranchIndex CoAxBranch -> Branches Unbranched)
-> Array BranchIndex CoAxBranch
-> Branches Unbranched
forall a. HasCallStack => Bool -> a -> a
assert (Array BranchIndex CoAxBranch -> (BranchIndex, BranchIndex)
forall i e. Array i e -> (i, i)
bounds Array BranchIndex CoAxBranch
arr (BranchIndex, BranchIndex) -> (BranchIndex, BranchIndex) -> Bool
forall a. Eq a => a -> a -> Bool
== (BranchIndex
0,BranchIndex
0) )
Array BranchIndex CoAxBranch -> Branches Unbranched
forall (br :: BranchFlag).
Array BranchIndex CoAxBranch -> Branches br
MkBranches Array BranchIndex CoAxBranch
arr
fromBranches :: Branches br -> [CoAxBranch]
fromBranches :: forall (br :: BranchFlag). Branches br -> [CoAxBranch]
fromBranches = Array BranchIndex CoAxBranch -> [CoAxBranch]
forall i e. Array i e -> [e]
elems (Array BranchIndex CoAxBranch -> [CoAxBranch])
-> (Branches br -> Array BranchIndex CoAxBranch)
-> Branches br
-> [CoAxBranch]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Branches br -> Array BranchIndex CoAxBranch
forall (br :: BranchFlag).
Branches br -> Array BranchIndex CoAxBranch
unMkBranches
branchesNth :: Branches br -> BranchIndex -> CoAxBranch
branchesNth :: forall (br :: BranchFlag). Branches br -> BranchIndex -> CoAxBranch
branchesNth (MkBranches Array BranchIndex CoAxBranch
arr) BranchIndex
n = Array BranchIndex CoAxBranch
arr Array BranchIndex CoAxBranch -> BranchIndex -> CoAxBranch
forall i e. Ix i => Array i e -> i -> e
! BranchIndex
n
numBranches :: Branches br -> Int
numBranches :: forall (br :: BranchFlag). Branches br -> BranchIndex
numBranches (MkBranches Array BranchIndex CoAxBranch
arr) = (BranchIndex, BranchIndex) -> BranchIndex
forall a b. (a, b) -> b
snd (Array BranchIndex CoAxBranch -> (BranchIndex, BranchIndex)
forall i e. Array i e -> (i, i)
bounds Array BranchIndex CoAxBranch
arr) BranchIndex -> BranchIndex -> BranchIndex
forall a. Num a => a -> a -> a
+ BranchIndex
1
mapAccumBranches :: ([CoAxBranch] -> CoAxBranch -> CoAxBranch)
-> Branches br -> Branches br
mapAccumBranches :: forall (br :: BranchFlag).
([CoAxBranch] -> CoAxBranch -> CoAxBranch)
-> Branches br -> Branches br
mapAccumBranches [CoAxBranch] -> CoAxBranch -> CoAxBranch
f (MkBranches Array BranchIndex CoAxBranch
arr)
= Array BranchIndex CoAxBranch -> Branches br
forall (br :: BranchFlag).
Array BranchIndex CoAxBranch -> Branches br
MkBranches ((BranchIndex, BranchIndex)
-> [CoAxBranch] -> Array BranchIndex CoAxBranch
forall i e. Ix i => (i, i) -> [e] -> Array i e
listArray (Array BranchIndex CoAxBranch -> (BranchIndex, BranchIndex)
forall i e. Array i e -> (i, i)
bounds Array BranchIndex CoAxBranch
arr) (([CoAxBranch], [CoAxBranch]) -> [CoAxBranch]
forall a b. (a, b) -> b
snd (([CoAxBranch], [CoAxBranch]) -> [CoAxBranch])
-> ([CoAxBranch], [CoAxBranch]) -> [CoAxBranch]
forall a b. (a -> b) -> a -> b
$ ([CoAxBranch] -> CoAxBranch -> ([CoAxBranch], CoAxBranch))
-> [CoAxBranch] -> [CoAxBranch] -> ([CoAxBranch], [CoAxBranch])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL [CoAxBranch] -> CoAxBranch -> ([CoAxBranch], CoAxBranch)
go [] (Array BranchIndex CoAxBranch -> [CoAxBranch]
forall i e. Array i e -> [e]
elems Array BranchIndex CoAxBranch
arr)))
where
go :: [CoAxBranch] -> CoAxBranch -> ([CoAxBranch], CoAxBranch)
go :: [CoAxBranch] -> CoAxBranch -> ([CoAxBranch], CoAxBranch)
go [CoAxBranch]
prev_branches CoAxBranch
cur_branch = ( CoAxBranch
cur_branch CoAxBranch -> [CoAxBranch] -> [CoAxBranch]
forall a. a -> [a] -> [a]
: [CoAxBranch]
prev_branches
, [CoAxBranch] -> CoAxBranch -> CoAxBranch
f [CoAxBranch]
prev_branches CoAxBranch
cur_branch )
data CoAxiom br
= CoAxiom
{ forall (br :: BranchFlag). CoAxiom br -> Unique
co_ax_unique :: Unique
, forall (br :: BranchFlag). CoAxiom br -> Name
co_ax_name :: Name
, forall (br :: BranchFlag). CoAxiom br -> Role
co_ax_role :: Role
, forall (br :: BranchFlag). CoAxiom br -> TyCon
co_ax_tc :: TyCon
, forall (br :: BranchFlag). CoAxiom br -> Branches br
co_ax_branches :: Branches br
, forall (br :: BranchFlag). CoAxiom br -> Bool
co_ax_implicit :: Bool
}
data CoAxBranch
= CoAxBranch
{ CoAxBranch -> SrcSpan
cab_loc :: SrcSpan
, CoAxBranch -> [TyVar]
cab_tvs :: [TyVar]
, CoAxBranch -> [TyVar]
cab_eta_tvs :: [TyVar]
, CoAxBranch -> [TyVar]
cab_cvs :: [CoVar]
, CoAxBranch -> [Role]
cab_roles :: [Role]
, CoAxBranch -> [Type]
cab_lhs :: [Type]
, CoAxBranch -> Type
cab_rhs :: Type
, CoAxBranch -> [CoAxBranch]
cab_incomps :: [CoAxBranch]
}
deriving Typeable CoAxBranch
Typeable CoAxBranch =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CoAxBranch -> c CoAxBranch)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CoAxBranch)
-> (CoAxBranch -> Constr)
-> (CoAxBranch -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c CoAxBranch))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c CoAxBranch))
-> ((forall b. Data b => b -> b) -> CoAxBranch -> CoAxBranch)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CoAxBranch -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CoAxBranch -> r)
-> (forall u. (forall d. Data d => d -> u) -> CoAxBranch -> [u])
-> (forall u.
BranchIndex -> (forall d. Data d => d -> u) -> CoAxBranch -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> CoAxBranch -> m CoAxBranch)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CoAxBranch -> m CoAxBranch)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CoAxBranch -> m CoAxBranch)
-> Data CoAxBranch
CoAxBranch -> Constr
CoAxBranch -> DataType
(forall b. Data b => b -> b) -> CoAxBranch -> CoAxBranch
forall a.
Typeable a =>
(forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u.
BranchIndex -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
BranchIndex -> (forall d. Data d => d -> u) -> CoAxBranch -> u
forall u. (forall d. Data d => d -> u) -> CoAxBranch -> [u]
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CoAxBranch -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CoAxBranch -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> CoAxBranch -> m CoAxBranch
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CoAxBranch -> m CoAxBranch
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CoAxBranch
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CoAxBranch -> c CoAxBranch
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c CoAxBranch)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CoAxBranch)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CoAxBranch -> c CoAxBranch
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> CoAxBranch -> c CoAxBranch
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CoAxBranch
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CoAxBranch
$ctoConstr :: CoAxBranch -> Constr
toConstr :: CoAxBranch -> Constr
$cdataTypeOf :: CoAxBranch -> DataType
dataTypeOf :: CoAxBranch -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c CoAxBranch)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c CoAxBranch)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CoAxBranch)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c CoAxBranch)
$cgmapT :: (forall b. Data b => b -> b) -> CoAxBranch -> CoAxBranch
gmapT :: (forall b. Data b => b -> b) -> CoAxBranch -> CoAxBranch
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CoAxBranch -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> CoAxBranch -> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CoAxBranch -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> CoAxBranch -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> CoAxBranch -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> CoAxBranch -> [u]
$cgmapQi :: forall u.
BranchIndex -> (forall d. Data d => d -> u) -> CoAxBranch -> u
gmapQi :: forall u.
BranchIndex -> (forall d. Data d => d -> u) -> CoAxBranch -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> CoAxBranch -> m CoAxBranch
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> CoAxBranch -> m CoAxBranch
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CoAxBranch -> m CoAxBranch
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CoAxBranch -> m CoAxBranch
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CoAxBranch -> m CoAxBranch
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> CoAxBranch -> m CoAxBranch
Data.Data
toBranchedAxiom :: CoAxiom br -> CoAxiom Branched
toBranchedAxiom :: forall (br :: BranchFlag). CoAxiom br -> CoAxiom Branched
toBranchedAxiom (CoAxiom Unique
unique Name
name Role
role TyCon
tc Branches br
branches Bool
implicit)
= Unique
-> Name
-> Role
-> TyCon
-> Branches Branched
-> Bool
-> CoAxiom Branched
forall (br :: BranchFlag).
Unique
-> Name -> Role -> TyCon -> Branches br -> Bool -> CoAxiom br
CoAxiom Unique
unique Name
name Role
role TyCon
tc (Branches br -> Branches Branched
forall (br :: BranchFlag). Branches br -> Branches Branched
toBranched Branches br
branches) Bool
implicit
toUnbranchedAxiom :: CoAxiom br -> CoAxiom Unbranched
toUnbranchedAxiom :: forall (br :: BranchFlag). CoAxiom br -> CoAxiom Unbranched
toUnbranchedAxiom (CoAxiom Unique
unique Name
name Role
role TyCon
tc Branches br
branches Bool
implicit)
= Unique
-> Name
-> Role
-> TyCon
-> Branches Unbranched
-> Bool
-> CoAxiom Unbranched
forall (br :: BranchFlag).
Unique
-> Name -> Role -> TyCon -> Branches br -> Bool -> CoAxiom br
CoAxiom Unique
unique Name
name Role
role TyCon
tc (Branches br -> Branches Unbranched
forall (br :: BranchFlag). Branches br -> Branches Unbranched
toUnbranched Branches br
branches) Bool
implicit
coAxiomNumPats :: CoAxiom br -> Int
coAxiomNumPats :: forall (br :: BranchFlag). CoAxiom br -> BranchIndex
coAxiomNumPats = [Type] -> BranchIndex
forall a. [a] -> BranchIndex
forall (t :: * -> *) a. Foldable t => t a -> BranchIndex
length ([Type] -> BranchIndex)
-> (CoAxiom br -> [Type]) -> CoAxiom br -> BranchIndex
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoAxBranch -> [Type]
coAxBranchLHS (CoAxBranch -> [Type])
-> (CoAxiom br -> CoAxBranch) -> CoAxiom br -> [Type]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((CoAxiom br -> BranchIndex -> CoAxBranch)
-> BranchIndex -> CoAxiom br -> CoAxBranch
forall a b c. (a -> b -> c) -> b -> a -> c
flip CoAxiom br -> BranchIndex -> CoAxBranch
forall (br :: BranchFlag). CoAxiom br -> BranchIndex -> CoAxBranch
coAxiomNthBranch BranchIndex
0)
coAxiomNthBranch :: CoAxiom br -> BranchIndex -> CoAxBranch
coAxiomNthBranch :: forall (br :: BranchFlag). CoAxiom br -> BranchIndex -> CoAxBranch
coAxiomNthBranch (CoAxiom { co_ax_branches :: forall (br :: BranchFlag). CoAxiom br -> Branches br
co_ax_branches = Branches br
bs }) BranchIndex
index
= Branches br -> BranchIndex -> CoAxBranch
forall (br :: BranchFlag). Branches br -> BranchIndex -> CoAxBranch
branchesNth Branches br
bs BranchIndex
index
coAxiomArity :: CoAxiom br -> BranchIndex -> Arity
coAxiomArity :: forall (br :: BranchFlag). CoAxiom br -> BranchIndex -> BranchIndex
coAxiomArity CoAxiom br
ax BranchIndex
index
= [TyVar] -> BranchIndex
forall a. [a] -> BranchIndex
forall (t :: * -> *) a. Foldable t => t a -> BranchIndex
length [TyVar]
tvs BranchIndex -> BranchIndex -> BranchIndex
forall a. Num a => a -> a -> a
+ [TyVar] -> BranchIndex
forall a. [a] -> BranchIndex
forall (t :: * -> *) a. Foldable t => t a -> BranchIndex
length [TyVar]
cvs
where
CoAxBranch { cab_tvs :: CoAxBranch -> [TyVar]
cab_tvs = [TyVar]
tvs, cab_cvs :: CoAxBranch -> [TyVar]
cab_cvs = [TyVar]
cvs } = CoAxiom br -> BranchIndex -> CoAxBranch
forall (br :: BranchFlag). CoAxiom br -> BranchIndex -> CoAxBranch
coAxiomNthBranch CoAxiom br
ax BranchIndex
index
coAxiomName :: CoAxiom br -> Name
coAxiomName :: forall (br :: BranchFlag). CoAxiom br -> Name
coAxiomName = CoAxiom br -> Name
forall (br :: BranchFlag). CoAxiom br -> Name
co_ax_name
coAxiomRole :: CoAxiom br -> Role
coAxiomRole :: forall (br :: BranchFlag). CoAxiom br -> Role
coAxiomRole = CoAxiom br -> Role
forall (br :: BranchFlag). CoAxiom br -> Role
co_ax_role
coAxiomBranches :: CoAxiom br -> Branches br
coAxiomBranches :: forall (br :: BranchFlag). CoAxiom br -> Branches br
coAxiomBranches = CoAxiom br -> Branches br
forall (br :: BranchFlag). CoAxiom br -> Branches br
co_ax_branches
coAxiomSingleBranch_maybe :: CoAxiom br -> Maybe CoAxBranch
coAxiomSingleBranch_maybe :: forall (br :: BranchFlag). CoAxiom br -> Maybe CoAxBranch
coAxiomSingleBranch_maybe (CoAxiom { co_ax_branches :: forall (br :: BranchFlag). CoAxiom br -> Branches br
co_ax_branches = MkBranches Array BranchIndex CoAxBranch
arr })
| (BranchIndex, BranchIndex) -> BranchIndex
forall a b. (a, b) -> b
snd (Array BranchIndex CoAxBranch -> (BranchIndex, BranchIndex)
forall i e. Array i e -> (i, i)
bounds Array BranchIndex CoAxBranch
arr) BranchIndex -> BranchIndex -> Bool
forall a. Eq a => a -> a -> Bool
== BranchIndex
0
= CoAxBranch -> Maybe CoAxBranch
forall a. a -> Maybe a
Just (CoAxBranch -> Maybe CoAxBranch) -> CoAxBranch -> Maybe CoAxBranch
forall a b. (a -> b) -> a -> b
$ Array BranchIndex CoAxBranch
arr Array BranchIndex CoAxBranch -> BranchIndex -> CoAxBranch
forall i e. Ix i => Array i e -> i -> e
! BranchIndex
0
| Bool
otherwise
= Maybe CoAxBranch
forall a. Maybe a
Nothing
coAxiomSingleBranch :: CoAxiom Unbranched -> CoAxBranch
coAxiomSingleBranch :: CoAxiom Unbranched -> CoAxBranch
coAxiomSingleBranch (CoAxiom { co_ax_branches :: forall (br :: BranchFlag). CoAxiom br -> Branches br
co_ax_branches = MkBranches Array BranchIndex CoAxBranch
arr })
= Array BranchIndex CoAxBranch
arr Array BranchIndex CoAxBranch -> BranchIndex -> CoAxBranch
forall i e. Ix i => Array i e -> i -> e
! BranchIndex
0
coAxiomTyCon :: CoAxiom br -> TyCon
coAxiomTyCon :: forall (br :: BranchFlag). CoAxiom br -> TyCon
coAxiomTyCon = CoAxiom br -> TyCon
forall (br :: BranchFlag). CoAxiom br -> TyCon
co_ax_tc
coAxBranchTyVars :: CoAxBranch -> [TyVar]
coAxBranchTyVars :: CoAxBranch -> [TyVar]
coAxBranchTyVars = CoAxBranch -> [TyVar]
cab_tvs
coAxBranchCoVars :: CoAxBranch -> [CoVar]
coAxBranchCoVars :: CoAxBranch -> [TyVar]
coAxBranchCoVars = CoAxBranch -> [TyVar]
cab_cvs
coAxBranchLHS :: CoAxBranch -> [Type]
coAxBranchLHS :: CoAxBranch -> [Type]
coAxBranchLHS = CoAxBranch -> [Type]
cab_lhs
coAxBranchRHS :: CoAxBranch -> Type
coAxBranchRHS :: CoAxBranch -> Type
coAxBranchRHS = CoAxBranch -> Type
cab_rhs
coAxBranchRoles :: CoAxBranch -> [Role]
coAxBranchRoles :: CoAxBranch -> [Role]
coAxBranchRoles = CoAxBranch -> [Role]
cab_roles
coAxBranchSpan :: CoAxBranch -> SrcSpan
coAxBranchSpan :: CoAxBranch -> SrcSpan
coAxBranchSpan = CoAxBranch -> SrcSpan
cab_loc
isImplicitCoAxiom :: CoAxiom br -> Bool
isImplicitCoAxiom :: forall (br :: BranchFlag). CoAxiom br -> Bool
isImplicitCoAxiom = CoAxiom br -> Bool
forall (br :: BranchFlag). CoAxiom br -> Bool
co_ax_implicit
coAxBranchIncomps :: CoAxBranch -> [CoAxBranch]
coAxBranchIncomps :: CoAxBranch -> [CoAxBranch]
coAxBranchIncomps = CoAxBranch -> [CoAxBranch]
cab_incomps
placeHolderIncomps :: [CoAxBranch]
placeHolderIncomps :: [CoAxBranch]
placeHolderIncomps = String -> [CoAxBranch]
forall a. HasCallStack => String -> a
panic String
"placeHolderIncomps"
instance Eq (CoAxiom br) where
CoAxiom br
a == :: CoAxiom br -> CoAxiom br -> Bool
== CoAxiom br
b = CoAxiom br -> Unique
forall a. Uniquable a => a -> Unique
getUnique CoAxiom br
a Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
== CoAxiom br -> Unique
forall a. Uniquable a => a -> Unique
getUnique CoAxiom br
b
CoAxiom br
a /= :: CoAxiom br -> CoAxiom br -> Bool
/= CoAxiom br
b = CoAxiom br -> Unique
forall a. Uniquable a => a -> Unique
getUnique CoAxiom br
a Unique -> Unique -> Bool
forall a. Eq a => a -> a -> Bool
/= CoAxiom br -> Unique
forall a. Uniquable a => a -> Unique
getUnique CoAxiom br
b
instance Uniquable (CoAxiom br) where
getUnique :: CoAxiom br -> Unique
getUnique = CoAxiom br -> Unique
forall (br :: BranchFlag). CoAxiom br -> Unique
co_ax_unique
instance NamedThing (CoAxiom br) where
getName :: CoAxiom br -> Name
getName = CoAxiom br -> Name
forall (br :: BranchFlag). CoAxiom br -> Name
co_ax_name
instance Typeable br => Data.Data (CoAxiom br) where
toConstr :: CoAxiom br -> Constr
toConstr CoAxiom br
_ = String -> Constr
abstractConstr String
"CoAxiom"
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (CoAxiom br)
gunfold forall b r. Data b => c (b -> r) -> c r
_ forall r. r -> c r
_ = String -> Constr -> c (CoAxiom br)
forall a. HasCallStack => String -> a
error String
"gunfold"
dataTypeOf :: CoAxiom br -> DataType
dataTypeOf CoAxiom br
_ = String -> DataType
mkNoRepType String
"CoAxiom"
instance Outputable (CoAxiom br) where
ppr :: CoAxiom br -> SDoc
ppr = Name -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Name -> SDoc) -> (CoAxiom br -> Name) -> CoAxiom br -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoAxiom br -> Name
forall a. NamedThing a => a -> Name
getName
instance Outputable CoAxBranch where
ppr :: CoAxBranch -> SDoc
ppr (CoAxBranch { cab_tvs :: CoAxBranch -> [TyVar]
cab_tvs = [TyVar]
tvs, cab_cvs :: CoAxBranch -> [TyVar]
cab_cvs = [TyVar]
cvs
, cab_lhs :: CoAxBranch -> [Type]
cab_lhs = [Type]
lhs_tys, cab_rhs :: CoAxBranch -> Type
cab_rhs = Type
rhs, cab_incomps :: CoAxBranch -> [CoAxBranch]
cab_incomps = [CoAxBranch]
incomps })
= String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"CoAxBranch" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc
braces SDoc
payload
where
payload :: SDoc
payload = SDoc -> BranchIndex -> SDoc -> SDoc
hang (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"forall" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> (TyVar -> SDoc) -> [TyVar] -> SDoc
forall a. (a -> SDoc) -> [a] -> SDoc
pprWithCommas TyVar -> SDoc
pprTyVar ([TyVar]
tvs [TyVar] -> [TyVar] -> [TyVar]
forall a. [a] -> [a] -> [a]
++ [TyVar]
cvs) SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<> SDoc
forall doc. IsLine doc => doc
dot)
BranchIndex
2 ([SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat [ String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"<tycon>" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [SDoc] -> SDoc
forall doc. IsLine doc => [doc] -> doc
sep ((Type -> SDoc) -> [Type] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map Type -> SDoc
pprType [Type]
lhs_tys)
, BranchIndex -> SDoc -> SDoc
nest BranchIndex
2 (String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"=" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
rhs)
, Bool -> SDoc -> SDoc
forall doc. IsOutput doc => Bool -> doc -> doc
ppUnless ([CoAxBranch] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [CoAxBranch]
incomps) (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$
String -> SDoc
forall doc. IsLine doc => String -> doc
text String
"incomps:" SDoc -> SDoc -> SDoc
forall doc. IsLine doc => doc -> doc -> doc
<+> [SDoc] -> SDoc
forall doc. IsDoc doc => [doc] -> doc
vcat ((CoAxBranch -> SDoc) -> [CoAxBranch] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map CoAxBranch -> SDoc
forall a. Outputable a => a -> SDoc
ppr [CoAxBranch]
incomps) ])
fsFromRole :: Role -> FastString
fsFromRole :: Role -> FastString
fsFromRole Role
Nominal = String -> FastString
fsLit String
"nominal"
fsFromRole Role
Representational = String -> FastString
fsLit String
"representational"
fsFromRole Role
Phantom = String -> FastString
fsLit String
"phantom"
instance Outputable Role where
ppr :: Role -> SDoc
ppr = FastString -> SDoc
forall doc. IsLine doc => FastString -> doc
ftext (FastString -> SDoc) -> (Role -> FastString) -> Role -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Role -> FastString
fsFromRole
instance Binary Role where
put_ :: BinHandle -> Role -> IO ()
put_ BinHandle
bh Role
Nominal = BinHandle -> Word8 -> IO ()
putByte BinHandle
bh Word8
1
put_ BinHandle
bh Role
Representational = BinHandle -> Word8 -> IO ()
putByte BinHandle
bh Word8
2
put_ BinHandle
bh Role
Phantom = BinHandle -> Word8 -> IO ()
putByte BinHandle
bh Word8
3
get :: BinHandle -> IO Role
get BinHandle
bh = do Word8
tag <- BinHandle -> IO Word8
getByte BinHandle
bh
case Word8
tag of Word8
1 -> Role -> IO Role
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Role
Nominal
Word8
2 -> Role -> IO Role
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Role
Representational
Word8
3 -> Role -> IO Role
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Role
Phantom
Word8
_ -> String -> IO Role
forall a. HasCallStack => String -> a
panic (String
"get Role " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Word8 -> String
forall a. Show a => a -> String
show Word8
tag)
type TypeEqn = Pair Type
data CoAxiomRule = CoAxiomRule
{ CoAxiomRule -> FastString
coaxrName :: FastString
, CoAxiomRule -> [Role]
coaxrAsmpRoles :: [Role]
, CoAxiomRule -> Role
coaxrRole :: Role
, CoAxiomRule -> [TypeEqn] -> Maybe TypeEqn
coaxrProves :: [TypeEqn] -> Maybe TypeEqn
}
instance Data.Data CoAxiomRule where
toConstr :: CoAxiomRule -> Constr
toConstr CoAxiomRule
_ = String -> Constr
abstractConstr String
"CoAxiomRule"
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c CoAxiomRule
gunfold forall b r. Data b => c (b -> r) -> c r
_ forall r. r -> c r
_ = String -> Constr -> c CoAxiomRule
forall a. HasCallStack => String -> a
error String
"gunfold"
dataTypeOf :: CoAxiomRule -> DataType
dataTypeOf CoAxiomRule
_ = String -> DataType
mkNoRepType String
"CoAxiomRule"
instance Uniquable CoAxiomRule where
getUnique :: CoAxiomRule -> Unique
getUnique = FastString -> Unique
forall a. Uniquable a => a -> Unique
getUnique (FastString -> Unique)
-> (CoAxiomRule -> FastString) -> CoAxiomRule -> Unique
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoAxiomRule -> FastString
coaxrName
instance Eq CoAxiomRule where
CoAxiomRule
x == :: CoAxiomRule -> CoAxiomRule -> Bool
== CoAxiomRule
y = CoAxiomRule -> FastString
coaxrName CoAxiomRule
x FastString -> FastString -> Bool
forall a. Eq a => a -> a -> Bool
== CoAxiomRule -> FastString
coaxrName CoAxiomRule
y
instance Ord CoAxiomRule where
compare :: CoAxiomRule -> CoAxiomRule -> Ordering
compare CoAxiomRule
x CoAxiomRule
y = FastString -> FastString -> Ordering
lexicalCompareFS (CoAxiomRule -> FastString
coaxrName CoAxiomRule
x) (CoAxiomRule -> FastString
coaxrName CoAxiomRule
y)
instance Outputable CoAxiomRule where
ppr :: CoAxiomRule -> SDoc
ppr = FastString -> SDoc
forall a. Outputable a => a -> SDoc
ppr (FastString -> SDoc)
-> (CoAxiomRule -> FastString) -> CoAxiomRule -> SDoc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CoAxiomRule -> FastString
coaxrName
data BuiltInSynFamily = BuiltInSynFamily
{ BuiltInSynFamily -> [Type] -> Maybe (CoAxiomRule, [Type], Type)
sfMatchFam :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
, BuiltInSynFamily -> [Type] -> Type -> [TypeEqn]
sfInteractTop :: [Type] -> Type -> [TypeEqn]
, BuiltInSynFamily -> [Type] -> Type -> [Type] -> Type -> [TypeEqn]
sfInteractInert :: [Type] -> Type ->
[Type] -> Type -> [TypeEqn]
}
trivialBuiltInFamily :: BuiltInSynFamily
trivialBuiltInFamily :: BuiltInSynFamily
trivialBuiltInFamily = BuiltInSynFamily
{ sfMatchFam :: [Type] -> Maybe (CoAxiomRule, [Type], Type)
sfMatchFam = \[Type]
_ -> Maybe (CoAxiomRule, [Type], Type)
forall a. Maybe a
Nothing
, sfInteractTop :: [Type] -> Type -> [TypeEqn]
sfInteractTop = \[Type]
_ Type
_ -> []
, sfInteractInert :: [Type] -> Type -> [Type] -> Type -> [TypeEqn]
sfInteractInert = \[Type]
_ Type
_ [Type]
_ Type
_ -> []
}