{-# 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 Language.Drasil.Development (showUID)
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 = 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 forall s a. s -> Getting a s a -> a
^. Lens' SimpleQDef a
lqde
    g (DDME ModelQDef
qd DDPkt
_) = ModelQDef
qd forall s a. s -> Getting a s a -> a
^. Lens' ModelQDef a
lqdme
    s :: DataDefinition -> a -> DataDefinition
s (DDE  SimpleQDef
qd DDPkt
pkt) a
u = SimpleQDef -> DDPkt -> DataDefinition
DDE  (SimpleQDef
qd forall a b. a -> (a -> b) -> b
& Lens' SimpleQDef a
lqde 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 forall a b. a -> (a -> b) -> b
& Lens' ModelQDef a
lqdme 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 = 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 forall s a. s -> Getting a s a -> a
^. Getter SimpleQDef a
gsqd
    g (DDME ModelQDef
qd DDPkt
_) = ModelQDef
qd forall s a. s -> Getting a s a -> 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 = 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 forall s a. s -> Getting a s a -> a
^. Lens' DDPkt a
lpkt
    g (DDME ModelQDef
_ DDPkt
pkt) = DDPkt
pkt forall s a. s -> Getting a s a -> 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 forall a b. a -> (a -> b) -> b
& Lens' DDPkt a
lpkt 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 forall a b. a -> (a -> b) -> b
& Lens' DDPkt a
lpkt 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 :: Lens' DataDefinition UID
uid = forall a.
Lens' SimpleQDef a -> Lens' ModelQDef a -> Lens' DataDefinition a
ddQD forall c. HasUID c => Lens' c UID
uid forall c. HasUID c => Lens' c UID
uid
-- | Finds the term ('NP') of the 'QDefinition' used to make the 'DataDefinition where'.
instance NamedIdea          DataDefinition where term :: Lens' DataDefinition NP
term = forall a.
Lens' SimpleQDef a -> Lens' ModelQDef a -> Lens' DataDefinition a
ddQD forall c. NamedIdea c => Lens' c NP
term forall c. NamedIdea c => Lens' c NP
term
-- | Finds the idea contained in the 'QDefinition' used to make the 'DataDefinition where'.
instance Idea               DataDefinition where getA :: DataDefinition -> Maybe String
getA = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall c. Idea c => c -> Maybe String
getA forall c. Idea c => c -> Maybe String
getA 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 = forall (p :: * -> * -> *) (f :: * -> *) a.
(Profunctor p, Contravariant f) =>
Getter SimpleQDef a
-> Getter ModelQDef a -> Optic' p f DataDefinition a
ddQDGetter forall d. DefinesQuantity d => Getter d QuantityDict
defLhs forall d. DefinesQuantity d => Getter d QuantityDict
defLhs
-- | Finds the output variable of the 'DataDefinition'
instance HasOutput          DataDefinition where
  output :: Getter DataDefinition QuantityDict
output = forall (p :: * -> * -> *) (f :: * -> *) a.
(Profunctor p, Contravariant f) =>
Getter SimpleQDef a
-> Getter ModelQDef a -> Optic' p f DataDefinition a
ddQDGetter forall d. DefinesQuantity d => Getter d QuantityDict
defLhs forall d. DefinesQuantity d => Getter d QuantityDict
defLhs
  out_constraints :: Getter DataDefinition [RealInterval Expr Expr]
out_constraints = forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to (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 = forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall c. Express c => c -> ModelExpr
express forall c. Express c => c -> ModelExpr
express 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 = forall a. Lens' DDPkt a -> Lens' DataDefinition a
ddPkt Lens' DDPkt [DecRef]
pktDR
-- | Equal if 'UID's are equal.
instance Eq                 DataDefinition where DataDefinition
a == :: DataDefinition -> DataDefinition -> Bool
== DataDefinition
b = (DataDefinition
a forall s a. s -> Getting a s a -> a
^. forall c. HasUID c => Lens' c UID
uid) forall a. Eq a => a -> a -> Bool
== (DataDefinition
b forall s a. s -> Getting a s a -> a
^. forall c. HasUID c => Lens' c UID
uid)
-- | Finds the derivation of the 'DataDefinition where'. May contain Nothing.
instance MayHaveDerivation  DataDefinition where derivations :: Lens' DataDefinition (Maybe Derivation)
derivations = forall a. Lens' DDPkt a -> Lens' DataDefinition a
ddPkt Lens' DDPkt (Maybe Derivation)
pktMD
-- | Finds any additional notes for the 'DataDefinition where'.
instance HasAdditionalNotes DataDefinition where getNotes :: Lens' DataDefinition [Sentence]
getNotes = forall a. Lens' DDPkt a -> Lens' DataDefinition a
ddPkt Lens' DDPkt [Sentence]
pktSS
-- | Finds the 'ShortName' of the 'DataDefinition where'.
instance HasShortName       DataDefinition where shortname :: DataDefinition -> ShortName
shortname = (forall s a. s -> Getting a s a -> a
^. forall a. Lens' DDPkt a -> Lens' DataDefinition a
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 forall a b. (a -> b) -> a -> b
$ forall c. CommonIdea c => c -> String
abrv DataDefinition
l) (DataDefinition
l forall s a. s -> Getting a s a -> a
^. forall a. Lens' DDPkt a -> Lens' DataDefinition a
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
_ = 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
_ = 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      = (forall s a. s -> Getting a s a -> a
^. forall a. Lens' DDPkt a -> Lens' DataDefinition a
ddPkt Lens' DDPkt String
pktS)
  renderRef :: DataDefinition -> LblType
renderRef DataDefinition
l = IRefProg -> String -> LblType
RP (String -> IRefProg
prepend forall a b. (a -> b) -> a -> b
$ forall c. CommonIdea c => c -> String
abrv DataDefinition
l) (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
_) = 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
_  = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Source field of " forall a. [a] -> [a] -> [a]
++ forall a. HasUID a => a -> String
showUID SimpleQDef
q forall a. [a] -> [a] -> [a]
++ String
" is empty"
ddE SimpleQDef
q [DecRef]
refs Maybe Derivation
der String
sn = SimpleQDef -> DDPkt -> DataDefinition
DDE SimpleQDef
q 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' forall a b. (a -> b) -> a -> b
$ String -> Sentence
S String
sn) (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 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' forall a b. (a -> b) -> a -> b
$ String -> Sentence
S String
sn) (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
_  = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$ String
"Source field of " forall a. [a] -> [a] -> [a]
++ forall a. HasUID a => a -> String
showUID ModelQDef
q forall a. [a] -> [a] -> [a]
++ String
" is empty"
ddME ModelQDef
q [DecRef]
refs Maybe Derivation
der String
sn = ModelQDef -> DDPkt -> DataDefinition
DDME ModelQDef
q 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' forall a b. (a -> b) -> a -> b
$ String -> Sentence
S String
sn) (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 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' forall a b. (a -> b) -> a -> b
$ String -> Sentence
S String
sn) (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
_) = forall a b. a -> Either a b
Left SimpleQDef
qd
qdFromDD (DDME ModelQDef
qd DDPkt
_) = forall a b. b -> Either a b
Right ModelQDef
qd

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