{-# LANGUAGE RankNTypes, NoMonomorphismRestriction, GADTs, TemplateHaskell #-}
{-# LANGUAGE MultiParamTypeClasses #-}
-- | Defines types and functions for Data Definitions.
module Theory.Drasil.DataDefinition where

import Control.Lens
import Language.Drasil
import Data.Drasil.TheoryConcepts (dataDefn)
import Theory.Drasil.Classes (HasOutput(..))

-- * Types

-- | A scope is an indirect reference to a 'UID'.
newtype Scope = Scp { Scope -> UID
_spec :: UID }

-- | Determines the scope of data.
data ScopeType =
    Local Scope -- ^ Only visible within a limited scope.
  | Global      -- ^ Visible everywhere.

data DDPkt = DDPkt {
  DDPkt -> ScopeType
_pktST :: ScopeType,
  DDPkt -> [DecRef]
_pktDR :: [DecRef],
  DDPkt -> Maybe Derivation
_pktMD :: Maybe Derivation,
  DDPkt -> ShortName
_pktSN :: ShortName,
  DDPkt -> String
_pktS  :: String,
  DDPkt -> [Sentence]
_pktSS :: [Sentence]
}
makeLenses ''DDPkt

-- | A data definition is a 'QDefinition' that may have additional notes: 
-- the scope, any references (as 'DecRef's), maybe a derivation, a label ('ShortName'), a reference address, and other notes ('Sentence's).
data DataDefinition where
  DDE  :: SimpleQDef -> DDPkt -> DataDefinition
  DDME :: ModelQDef -> DDPkt -> DataDefinition

ddQD :: Lens' SimpleQDef a -> Lens' ModelQDef a -> Lens' DataDefinition a
ddQD :: forall a.
Lens' SimpleQDef a -> Lens' ModelQDef a -> Lens' DataDefinition a
ddQD Lens' SimpleQDef a
lqde Lens' ModelQDef a
lqdme = (DataDefinition -> a)
-> (DataDefinition -> a -> DataDefinition)
-> Lens DataDefinition DataDefinition a a
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens DataDefinition -> a
g DataDefinition -> a -> DataDefinition
s
  where
    g :: DataDefinition -> a
g (DDE  SimpleQDef
qd DDPkt
_) = SimpleQDef
qd SimpleQDef -> Getting a SimpleQDef a -> a
forall s a. s -> Getting a s a -> a
^. Getting a SimpleQDef a
Lens' SimpleQDef a
lqde
    g (DDME ModelQDef
qd DDPkt
_) = ModelQDef
qd ModelQDef -> Getting a ModelQDef a -> a
forall s a. s -> Getting a s a -> a
^. Getting a ModelQDef a
Lens' ModelQDef a
lqdme
    s :: DataDefinition -> a -> DataDefinition
s (DDE  SimpleQDef
qd DDPkt
pkt) a
u = SimpleQDef -> DDPkt -> DataDefinition
DDE  (SimpleQDef
qd SimpleQDef -> (SimpleQDef -> SimpleQDef) -> SimpleQDef
forall a b. a -> (a -> b) -> b
& (a -> Identity a) -> SimpleQDef -> Identity SimpleQDef
Lens' SimpleQDef a
lqde ((a -> Identity a) -> SimpleQDef -> Identity SimpleQDef)
-> a -> SimpleQDef -> SimpleQDef
forall s t a b. ASetter s t a b -> b -> s -> t
.~ a
u)  DDPkt
pkt
    s (DDME ModelQDef
qd DDPkt
pkt) a
u = ModelQDef -> DDPkt -> DataDefinition
DDME (ModelQDef
qd ModelQDef -> (ModelQDef -> ModelQDef) -> ModelQDef
forall a b. a -> (a -> b) -> b
& (a -> Identity a) -> ModelQDef -> Identity ModelQDef
Lens' ModelQDef a
lqdme ((a -> Identity a) -> ModelQDef -> Identity ModelQDef)
-> a -> ModelQDef -> ModelQDef
forall s t a b. ASetter s t a b -> b -> s -> t
.~ a
u) DDPkt
pkt

-- The type signature is really
--
--     ddQDGetter :: Getter SimpleQDef a -> Getter ModelQDef a -> Getter DataDefinition a
--
-- But we need this more general type signature to avoid GHC warning us of
-- "redundant constraints"
ddQDGetter :: (Profunctor p, Contravariant f) => Getter SimpleQDef a
  -> Getter ModelQDef a
  -> Optic' p f DataDefinition a
ddQDGetter :: forall (p :: * -> * -> *) (f :: * -> *) a.
(Profunctor p, Contravariant f) =>
Getter SimpleQDef a
-> Getter ModelQDef a -> Optic' p f DataDefinition a
ddQDGetter Getter SimpleQDef a
gsqd Getter ModelQDef a
gmqd = (DataDefinition -> a) -> Optic' p f DataDefinition a
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to DataDefinition -> a
g
  where
    g :: DataDefinition -> a
g (DDE SimpleQDef
qd DDPkt
_) = SimpleQDef
qd SimpleQDef -> Getting a SimpleQDef a -> a
forall s a. s -> Getting a s a -> a
^. Getting a SimpleQDef a
Getter SimpleQDef a
gsqd
    g (DDME ModelQDef
qd DDPkt
_) = ModelQDef
qd ModelQDef -> Getting a ModelQDef a -> a
forall s a. s -> Getting a s a -> a
^. Getting a ModelQDef a
Getter ModelQDef a
gmqd

ddPkt :: Lens' DDPkt a -> Lens' DataDefinition a
ddPkt :: forall a. Lens' DDPkt a -> Lens' DataDefinition a
ddPkt Lens' DDPkt a
lpkt = (DataDefinition -> a)
-> (DataDefinition -> a -> DataDefinition)
-> Lens DataDefinition DataDefinition a a
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens DataDefinition -> a
g DataDefinition -> a -> DataDefinition
s
  where
    g :: DataDefinition -> a
g (DDE  SimpleQDef
_ DDPkt
pkt) = DDPkt
pkt DDPkt -> Getting a DDPkt a -> a
forall s a. s -> Getting a s a -> a
^. Getting a DDPkt a
Lens' DDPkt a
lpkt
    g (DDME ModelQDef
_ DDPkt
pkt) = DDPkt
pkt DDPkt -> Getting a DDPkt a -> a
forall s a. s -> Getting a s a -> a
^. Getting a DDPkt a
Lens' DDPkt a
lpkt
    s :: DataDefinition -> a -> DataDefinition
s (DDE  SimpleQDef
qd DDPkt
pkt) a
a' = SimpleQDef -> DDPkt -> DataDefinition
DDE  SimpleQDef
qd (DDPkt
pkt DDPkt -> (DDPkt -> DDPkt) -> DDPkt
forall a b. a -> (a -> b) -> b
& (a -> Identity a) -> DDPkt -> Identity DDPkt
Lens' DDPkt a
lpkt ((a -> Identity a) -> DDPkt -> Identity DDPkt)
-> a -> DDPkt -> DDPkt
forall s t a b. ASetter s t a b -> b -> s -> t
.~ a
a')
    s (DDME ModelQDef
qd DDPkt
pkt) a
a' = ModelQDef -> DDPkt -> DataDefinition
DDME ModelQDef
qd (DDPkt
pkt DDPkt -> (DDPkt -> DDPkt) -> DDPkt
forall a b. a -> (a -> b) -> b
& (a -> Identity a) -> DDPkt -> Identity DDPkt
Lens' DDPkt a
lpkt ((a -> Identity a) -> DDPkt -> Identity DDPkt)
-> a -> DDPkt -> DDPkt
forall s t a b. ASetter s t a b -> b -> s -> t
.~ a
a')

-- | Finds the 'UID' of a 'DataDefinition where'.
instance HasUID             DataDefinition where uid :: Getter DataDefinition UID
uid = Getter SimpleQDef UID
-> Getter ModelQDef UID
-> (UID -> f UID)
-> DataDefinition
-> f DataDefinition
forall (p :: * -> * -> *) (f :: * -> *) a.
(Profunctor p, Contravariant f) =>
Getter SimpleQDef a
-> Getter ModelQDef a -> Optic' p f DataDefinition a
ddQDGetter (UID -> f UID) -> SimpleQDef -> f SimpleQDef
forall c. HasUID c => Getter c UID
Getter SimpleQDef UID
uid (UID -> f UID) -> ModelQDef -> f ModelQDef
forall c. HasUID c => Getter c UID
Getter ModelQDef UID
uid
-- | Finds the term ('NP') of the 'QDefinition' used to make the 'DataDefinition where'.
instance NamedIdea          DataDefinition where term :: Lens' DataDefinition NP
term = Lens' SimpleQDef NP
-> Lens' ModelQDef NP -> Lens' DataDefinition NP
forall a.
Lens' SimpleQDef a -> Lens' ModelQDef a -> Lens' DataDefinition a
ddQD (NP -> f NP) -> SimpleQDef -> f SimpleQDef
forall c. NamedIdea c => Lens' c NP
Lens' SimpleQDef NP
term (NP -> f NP) -> ModelQDef -> f ModelQDef
forall c. NamedIdea c => Lens' c NP
Lens' ModelQDef NP
term
-- | Finds the idea contained in the 'QDefinition' used to make the 'DataDefinition where'.
instance Idea               DataDefinition where getA :: DataDefinition -> Maybe String
getA = (SimpleQDef -> Maybe String)
-> (ModelQDef -> Maybe String)
-> Either SimpleQDef ModelQDef
-> Maybe String
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either SimpleQDef -> Maybe String
forall c. Idea c => c -> Maybe String
getA ModelQDef -> Maybe String
forall c. Idea c => c -> Maybe String
getA (Either SimpleQDef ModelQDef -> Maybe String)
-> (DataDefinition -> Either SimpleQDef ModelQDef)
-> DataDefinition
-> Maybe String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataDefinition -> Either SimpleQDef ModelQDef
qdFromDD
-- | Finds the 'Quantity' defined by the 'DataDefinition'
instance DefinesQuantity    DataDefinition where
  defLhs :: Getter DataDefinition QuantityDict
defLhs = Getter SimpleQDef QuantityDict
-> Getter ModelQDef QuantityDict
-> (QuantityDict -> f QuantityDict)
-> DataDefinition
-> f DataDefinition
forall (p :: * -> * -> *) (f :: * -> *) a.
(Profunctor p, Contravariant f) =>
Getter SimpleQDef a
-> Getter ModelQDef a -> Optic' p f DataDefinition a
ddQDGetter (QuantityDict -> f QuantityDict) -> SimpleQDef -> f SimpleQDef
forall d. DefinesQuantity d => Getter d QuantityDict
Getter SimpleQDef QuantityDict
defLhs (QuantityDict -> f QuantityDict) -> ModelQDef -> f ModelQDef
forall d. DefinesQuantity d => Getter d QuantityDict
Getter ModelQDef QuantityDict
defLhs
-- | Finds the output variable of the 'DataDefinition'
instance HasOutput          DataDefinition where
  output :: Getter DataDefinition QuantityDict
output = Getter SimpleQDef QuantityDict
-> Getter ModelQDef QuantityDict
-> (QuantityDict -> f QuantityDict)
-> DataDefinition
-> f DataDefinition
forall (p :: * -> * -> *) (f :: * -> *) a.
(Profunctor p, Contravariant f) =>
Getter SimpleQDef a
-> Getter ModelQDef a -> Optic' p f DataDefinition a
ddQDGetter (QuantityDict -> f QuantityDict) -> SimpleQDef -> f SimpleQDef
forall d. DefinesQuantity d => Getter d QuantityDict
Getter SimpleQDef QuantityDict
defLhs (QuantityDict -> f QuantityDict) -> ModelQDef -> f ModelQDef
forall d. DefinesQuantity d => Getter d QuantityDict
Getter ModelQDef QuantityDict
defLhs
  out_constraints :: Getter DataDefinition [RealInterval Expr Expr]
out_constraints = (DataDefinition -> [RealInterval Expr Expr])
-> ([RealInterval Expr Expr] -> f [RealInterval Expr Expr])
-> DataDefinition
-> f DataDefinition
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to ([RealInterval Expr Expr]
-> DataDefinition -> [RealInterval Expr Expr]
forall a b. a -> b -> a
const [])
-- | Converts the defining expression of a 'DataDefinition where' into the model expression language.
instance Express            DataDefinition where express :: DataDefinition -> ModelExpr
express = (SimpleQDef -> ModelExpr)
-> (ModelQDef -> ModelExpr)
-> Either SimpleQDef ModelQDef
-> ModelExpr
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either SimpleQDef -> ModelExpr
forall c. Express c => c -> ModelExpr
express ModelQDef -> ModelExpr
forall c. Express c => c -> ModelExpr
express (Either SimpleQDef ModelQDef -> ModelExpr)
-> (DataDefinition -> Either SimpleQDef ModelQDef)
-> DataDefinition
-> ModelExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DataDefinition -> Either SimpleQDef ModelQDef
qdFromDD
{-- Finds 'Reference's contained in the 'DataDefinition where'.
instance HasReference       DataDefinition where getReferences = rf-}
-- | Finds 'DecRef's contained in the 'DataDefinition where'.
instance HasDecRef          DataDefinition where getDecRefs :: Lens' DataDefinition [DecRef]
getDecRefs = Lens' DDPkt [DecRef] -> Lens' DataDefinition [DecRef]
forall a. Lens' DDPkt a -> Lens' DataDefinition a
ddPkt ([DecRef] -> f [DecRef]) -> DDPkt -> f DDPkt
Lens' DDPkt [DecRef]
pktDR
-- | Equal if 'UID's are equal.
instance Eq                 DataDefinition where DataDefinition
a == :: DataDefinition -> DataDefinition -> Bool
== DataDefinition
b = (DataDefinition
a DataDefinition -> Getting UID DataDefinition UID -> UID
forall s a. s -> Getting a s a -> a
^. Getting UID DataDefinition UID
forall c. HasUID c => Getter c UID
Getter DataDefinition UID
uid) UID -> UID -> Bool
forall a. Eq a => a -> a -> Bool
== (DataDefinition
b DataDefinition -> Getting UID DataDefinition UID -> UID
forall s a. s -> Getting a s a -> a
^. Getting UID DataDefinition UID
forall c. HasUID c => Getter c UID
Getter DataDefinition UID
uid)
-- | Finds the derivation of the 'DataDefinition where'. May contain Nothing.
instance MayHaveDerivation  DataDefinition where derivations :: Lens' DataDefinition (Maybe Derivation)
derivations = Lens' DDPkt (Maybe Derivation)
-> Lens' DataDefinition (Maybe Derivation)
forall a. Lens' DDPkt a -> Lens' DataDefinition a
ddPkt (Maybe Derivation -> f (Maybe Derivation)) -> DDPkt -> f DDPkt
Lens' DDPkt (Maybe Derivation)
pktMD
-- | Finds any additional notes for the 'DataDefinition where'.
instance HasAdditionalNotes DataDefinition where getNotes :: Lens' DataDefinition [Sentence]
getNotes = Lens' DDPkt [Sentence] -> Lens' DataDefinition [Sentence]
forall a. Lens' DDPkt a -> Lens' DataDefinition a
ddPkt ([Sentence] -> f [Sentence]) -> DDPkt -> f DDPkt
Lens' DDPkt [Sentence]
pktSS
-- | Finds the 'ShortName' of the 'DataDefinition where'.
instance HasShortName       DataDefinition where shortname :: DataDefinition -> ShortName
shortname = (DataDefinition
-> Getting ShortName DataDefinition ShortName -> ShortName
forall s a. s -> Getting a s a -> a
^. Lens' DDPkt ShortName -> Lens' DataDefinition ShortName
forall a. Lens' DDPkt a -> Lens' DataDefinition a
ddPkt (ShortName -> f ShortName) -> DDPkt -> f DDPkt
Lens' DDPkt ShortName
pktSN)
-- | Finds the reference address of a 'DataDefinition where'.
instance HasRefAddress      DataDefinition where getRefAdd :: DataDefinition -> LblType
getRefAdd DataDefinition
l = IRefProg -> String -> LblType
RP (String -> IRefProg
prepend (String -> IRefProg) -> String -> IRefProg
forall a b. (a -> b) -> a -> b
$ DataDefinition -> String
forall c. CommonIdea c => c -> String
abrv DataDefinition
l) (DataDefinition
l DataDefinition -> Getting String DataDefinition String -> String
forall s a. s -> Getting a s a -> a
^. Lens' DDPkt String -> Lens' DataDefinition String
forall a. Lens' DDPkt a -> Lens' DataDefinition a
ddPkt (String -> f String) -> DDPkt -> f DDPkt
Lens' DDPkt String
pktS)
-- | Finds the domain of the 'QDefinition' used to make the 'DataDefinition where'.
instance ConceptDomain      DataDefinition where cdom :: DataDefinition -> [UID]
cdom DataDefinition
_ = CI -> [UID]
forall c. ConceptDomain c => c -> [UID]
cdom CI
dataDefn
-- | Finds the idea of a 'DataDefinition where' (abbreviation).
instance CommonIdea         DataDefinition where abrv :: DataDefinition -> String
abrv DataDefinition
_ = CI -> String
forall c. CommonIdea c => c -> String
abrv CI
dataDefn
-- | Finds the reference address of a 'DataDefinition where'.
instance Referable          DataDefinition where
  refAdd :: DataDefinition -> String
refAdd      = (DataDefinition -> Getting String DataDefinition String -> String
forall s a. s -> Getting a s a -> a
^. Lens' DDPkt String -> Lens' DataDefinition String
forall a. Lens' DDPkt a -> Lens' DataDefinition a
ddPkt (String -> f String) -> DDPkt -> f DDPkt
Lens' DDPkt String
pktS)
  renderRef :: DataDefinition -> LblType
renderRef DataDefinition
l = IRefProg -> String -> LblType
RP (String -> IRefProg
prepend (String -> IRefProg) -> String -> IRefProg
forall a b. (a -> b) -> a -> b
$ DataDefinition -> String
forall c. CommonIdea c => c -> String
abrv DataDefinition
l) (DataDefinition -> String
forall s. Referable s => s -> String
refAdd DataDefinition
l)
-- | Expose all expressions that need to be type-checked.
instance RequiresChecking DataDefinition Expr Space where
  requiredChecks :: DataDefinition -> [(Expr, Space)]
requiredChecks (DDE  SimpleQDef
qd DDPkt
_) = SimpleQDef -> [(Expr, Space)]
forall c e t. RequiresChecking c e t => c -> [(e, t)]
requiredChecks SimpleQDef
qd
  requiredChecks  DDME {}    = []

-- * Constructors

-- | Smart constructor for data definitions.
ddE :: SimpleQDef -> [DecRef] -> Maybe Derivation -> String -> [Sentence] -> DataDefinition
ddE :: SimpleQDef
-> [DecRef]
-> Maybe Derivation
-> String
-> [Sentence]
-> DataDefinition
ddE SimpleQDef
q []   Maybe Derivation
_   String
_  = String -> [Sentence] -> DataDefinition
forall a. HasCallStack => String -> a
error (String -> [Sentence] -> DataDefinition)
-> String -> [Sentence] -> DataDefinition
forall a b. (a -> b) -> a -> b
$ String
"Source field of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SimpleQDef -> String
forall a. HasUID a => a -> String
showUID SimpleQDef
q String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is empty"
ddE SimpleQDef
q [DecRef]
refs Maybe Derivation
der String
sn = SimpleQDef -> DDPkt -> DataDefinition
DDE SimpleQDef
q (DDPkt -> DataDefinition)
-> ([Sentence] -> DDPkt) -> [Sentence] -> DataDefinition
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScopeType
-> [DecRef]
-> Maybe Derivation
-> ShortName
-> String
-> [Sentence]
-> DDPkt
DDPkt ScopeType
Global [DecRef]
refs Maybe Derivation
der (Sentence -> ShortName
shortname' (Sentence -> ShortName) -> Sentence -> ShortName
forall a b. (a -> b) -> a -> b
$ String -> Sentence
S String
sn) (CI -> String -> String
forall c. CommonIdea c => c -> String -> String
prependAbrv CI
dataDefn String
sn)

-- | Smart constructor for data definitions with no references.
ddENoRefs :: SimpleQDef -> Maybe Derivation -> String -> [Sentence] -> DataDefinition
ddENoRefs :: SimpleQDef
-> Maybe Derivation -> String -> [Sentence] -> DataDefinition
ddENoRefs SimpleQDef
q Maybe Derivation
der String
sn = SimpleQDef -> DDPkt -> DataDefinition
DDE SimpleQDef
q (DDPkt -> DataDefinition)
-> ([Sentence] -> DDPkt) -> [Sentence] -> DataDefinition
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScopeType
-> [DecRef]
-> Maybe Derivation
-> ShortName
-> String
-> [Sentence]
-> DDPkt
DDPkt ScopeType
Global [] Maybe Derivation
der (Sentence -> ShortName
shortname' (Sentence -> ShortName) -> Sentence -> ShortName
forall a b. (a -> b) -> a -> b
$ String -> Sentence
S String
sn) (CI -> String -> String
forall c. CommonIdea c => c -> String -> String
prependAbrv CI
dataDefn String
sn)

-- | Smart constructor for data definitions.
ddME :: ModelQDef -> [DecRef] -> Maybe Derivation -> String -> [Sentence] -> DataDefinition
ddME :: ModelQDef
-> [DecRef]
-> Maybe Derivation
-> String
-> [Sentence]
-> DataDefinition
ddME ModelQDef
q []   Maybe Derivation
_   String
_  = String -> [Sentence] -> DataDefinition
forall a. HasCallStack => String -> a
error (String -> [Sentence] -> DataDefinition)
-> String -> [Sentence] -> DataDefinition
forall a b. (a -> b) -> a -> b
$ String
"Source field of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ModelQDef -> String
forall a. HasUID a => a -> String
showUID ModelQDef
q String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is empty"
ddME ModelQDef
q [DecRef]
refs Maybe Derivation
der String
sn = ModelQDef -> DDPkt -> DataDefinition
DDME ModelQDef
q (DDPkt -> DataDefinition)
-> ([Sentence] -> DDPkt) -> [Sentence] -> DataDefinition
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScopeType
-> [DecRef]
-> Maybe Derivation
-> ShortName
-> String
-> [Sentence]
-> DDPkt
DDPkt ScopeType
Global [DecRef]
refs Maybe Derivation
der (Sentence -> ShortName
shortname' (Sentence -> ShortName) -> Sentence -> ShortName
forall a b. (a -> b) -> a -> b
$ String -> Sentence
S String
sn) (CI -> String -> String
forall c. CommonIdea c => c -> String -> String
prependAbrv CI
dataDefn String
sn)

-- | Smart constructor for data definitions with no references.
ddMENoRefs :: ModelQDef -> Maybe Derivation -> String -> [Sentence] -> DataDefinition
ddMENoRefs :: ModelQDef
-> Maybe Derivation -> String -> [Sentence] -> DataDefinition
ddMENoRefs ModelQDef
q Maybe Derivation
der String
sn = ModelQDef -> DDPkt -> DataDefinition
DDME ModelQDef
q (DDPkt -> DataDefinition)
-> ([Sentence] -> DDPkt) -> [Sentence] -> DataDefinition
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScopeType
-> [DecRef]
-> Maybe Derivation
-> ShortName
-> String
-> [Sentence]
-> DDPkt
DDPkt ScopeType
Global [] Maybe Derivation
der (Sentence -> ShortName
shortname' (Sentence -> ShortName) -> Sentence -> ShortName
forall a b. (a -> b) -> a -> b
$ String -> Sentence
S String
sn) (CI -> String -> String
forall c. CommonIdea c => c -> String -> String
prependAbrv CI
dataDefn String
sn)

-- | Extracts the 'QDefinition e' from a 'DataDefinition'.
qdFromDD :: DataDefinition -> Either SimpleQDef ModelQDef
qdFromDD :: DataDefinition -> Either SimpleQDef ModelQDef
qdFromDD (DDE  SimpleQDef
qd DDPkt
_) = SimpleQDef -> Either SimpleQDef ModelQDef
forall a b. a -> Either a b
Left SimpleQDef
qd
qdFromDD (DDME ModelQDef
qd DDPkt
_) = ModelQDef -> Either SimpleQDef ModelQDef
forall a b. b -> Either a b
Right ModelQDef
qd

qdEFromDD :: DataDefinition -> Maybe SimpleQDef
qdEFromDD :: DataDefinition -> Maybe SimpleQDef
qdEFromDD (DDE SimpleQDef
qd DDPkt
_) = SimpleQDef -> Maybe SimpleQDef
forall a. a -> Maybe a
Just SimpleQDef
qd
qdEFromDD DataDefinition
_          = Maybe SimpleQDef
forall a. Maybe a
Nothing