{-# Language TemplateHaskell, RankNTypes #-}
-- | Defines types and functions for Theoretical Models.
module Theory.Drasil.Theory (
  -- * Types
  TheoryModel,
  -- * Constructors
  tm, tmNoRefs) where

import Control.Lens (view, makeLenses, (^.))

import Drasil.Database (HasUID(..), showUID, HasChunkRefs(..))
import Language.Drasil
import Drasil.Metadata.TheoryConcepts (thModel)

import Theory.Drasil.ModelKinds

-- | A TheoryModel is a collection of:
--
--      * tUid - a UID,
--      * con - a ConceptChunk,
--      * vctx - definition context ('TheoryModel's),
--      * spc - type definitions ('SpaceDefn's),
--      * quan - quantities ('DefinedQuantityDict's),
--      * ops - operations ('ConceptChunk's),
--      * defq - definitions ('QDefinition's),
--      * invs - invariants ('ModelExpr's),
--      * dfun - defined functions ('QDefinition's),
--      * ref - accompanying references ('DecRef's),
--      * lb - a label ('SpaceDefn'),
--      * ra - reference address ('SpaceDefn'),
--      * notes - additional notes ('Sentence's).
--
-- Right now, neither the definition context (vctx) nor the
-- spaces (spc) are ever defined.
data TheoryModel = TM
  { TheoryModel -> ModelKind ModelExpr
_mk    :: ModelKind ModelExpr
  , TheoryModel -> [DecRef]
_rf    :: [DecRef]
  ,  TheoryModel -> ShortName
lb    :: ShortName
  ,  TheoryModel -> String
ra    :: String
  , TheoryModel -> [Sentence]
_notes :: [Sentence]
  }
makeLenses ''TheoryModel

instance HasChunkRefs TheoryModel where
  chunkRefs :: TheoryModel -> Set UID
chunkRefs TheoryModel
tm' = [Set UID] -> Set UID
forall a. Monoid a => [a] -> a
mconcat
    [ ModelKind ModelExpr -> Set UID
forall a. HasChunkRefs a => a -> Set UID
chunkRefs (TheoryModel
tm' TheoryModel
-> Getting (ModelKind ModelExpr) TheoryModel (ModelKind ModelExpr)
-> ModelKind ModelExpr
forall s a. s -> Getting a s a -> a
^. Getting (ModelKind ModelExpr) TheoryModel (ModelKind ModelExpr)
Lens' TheoryModel (ModelKind ModelExpr)
mk)
    , ShortName -> Set UID
forall a. HasChunkRefs a => a -> Set UID
chunkRefs (TheoryModel -> ShortName
lb TheoryModel
tm')
    , [Sentence] -> Set UID
forall a. HasChunkRefs a => a -> Set UID
chunkRefs (TheoryModel
tm' TheoryModel
-> Getting [Sentence] TheoryModel [Sentence] -> [Sentence]
forall s a. s -> Getting a s a -> a
^. Getting [Sentence] TheoryModel [Sentence]
Lens' TheoryModel [Sentence]
notes)
    ]
  {-# INLINABLE chunkRefs #-}

-- | Finds the 'UID' of a 'TheoryModel'.
instance HasUID             TheoryModel where uid :: Getter TheoryModel UID
uid = (ModelKind ModelExpr -> f (ModelKind ModelExpr))
-> TheoryModel -> f TheoryModel
Lens' TheoryModel (ModelKind ModelExpr)
mk ((ModelKind ModelExpr -> f (ModelKind ModelExpr))
 -> TheoryModel -> f TheoryModel)
-> ((UID -> f UID)
    -> ModelKind ModelExpr -> f (ModelKind ModelExpr))
-> (UID -> f UID)
-> TheoryModel
-> f TheoryModel
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UID -> f UID) -> ModelKind ModelExpr -> f (ModelKind ModelExpr)
forall c. HasUID c => Getter c UID
Getter (ModelKind ModelExpr) UID
uid
-- | Finds the term ('NP') of the 'TheoryModel'.
instance NamedIdea          TheoryModel where term :: Lens' TheoryModel NP
term = (ModelKind ModelExpr -> f (ModelKind ModelExpr))
-> TheoryModel -> f TheoryModel
Lens' TheoryModel (ModelKind ModelExpr)
mk ((ModelKind ModelExpr -> f (ModelKind ModelExpr))
 -> TheoryModel -> f TheoryModel)
-> ((NP -> f NP) -> ModelKind ModelExpr -> f (ModelKind ModelExpr))
-> (NP -> f NP)
-> TheoryModel
-> f TheoryModel
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NP -> f NP) -> ModelKind ModelExpr -> f (ModelKind ModelExpr)
forall c. NamedIdea c => Lens' c NP
Lens' (ModelKind ModelExpr) NP
term
-- | Finds the idea of the 'ConceptChunk' contained in the 'TheoryModel'.
instance Idea               TheoryModel where getA :: TheoryModel -> Maybe String
getA = ModelKind ModelExpr -> Maybe String
forall c. Idea c => c -> Maybe String
getA (ModelKind ModelExpr -> Maybe String)
-> (TheoryModel -> ModelKind ModelExpr)
-> TheoryModel
-> Maybe String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting (ModelKind ModelExpr) TheoryModel (ModelKind ModelExpr)
-> TheoryModel -> ModelKind ModelExpr
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting (ModelKind ModelExpr) TheoryModel (ModelKind ModelExpr)
Lens' TheoryModel (ModelKind ModelExpr)
mk
-- | Finds the definition of the 'ConceptChunk' contained in a 'TheoryModel'.
instance Definition         TheoryModel where defn :: Lens' TheoryModel Sentence
defn = (ModelKind ModelExpr -> f (ModelKind ModelExpr))
-> TheoryModel -> f TheoryModel
Lens' TheoryModel (ModelKind ModelExpr)
mk ((ModelKind ModelExpr -> f (ModelKind ModelExpr))
 -> TheoryModel -> f TheoryModel)
-> ((Sentence -> f Sentence)
    -> ModelKind ModelExpr -> f (ModelKind ModelExpr))
-> (Sentence -> f Sentence)
-> TheoryModel
-> f TheoryModel
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Sentence -> f Sentence)
-> ModelKind ModelExpr -> f (ModelKind ModelExpr)
forall c. Definition c => Lens' c Sentence
Lens' (ModelKind ModelExpr) Sentence
defn
{-- | Finds 'Reference's contained in the 'TheoryModel'.
instance HasReference       TheoryModel where getReferences l = map ref $ rf l-}
-- | Finds 'DecRef's contained in the 'TheoryModel'.
instance HasDecRef          TheoryModel where getDecRefs :: Lens' TheoryModel [DecRef]
getDecRefs = ([DecRef] -> f [DecRef]) -> TheoryModel -> f TheoryModel
Lens' TheoryModel [DecRef]
rf
-- | Finds the domain of the 'ConceptChunk' contained in a 'TheoryModel'.
instance ConceptDomain      TheoryModel where cdom :: TheoryModel -> [UID]
cdom = ModelKind ModelExpr -> [UID]
forall c. ConceptDomain c => c -> [UID]
cdom (ModelKind ModelExpr -> [UID])
-> (TheoryModel -> ModelKind ModelExpr) -> TheoryModel -> [UID]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting (ModelKind ModelExpr) TheoryModel (ModelKind ModelExpr)
-> TheoryModel -> ModelKind ModelExpr
forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view Getting (ModelKind ModelExpr) TheoryModel (ModelKind ModelExpr)
Lens' TheoryModel (ModelKind ModelExpr)
mk
-- | Finds any additional notes for the 'TheoryModel'.
instance HasAdditionalNotes TheoryModel where getNotes :: Lens' TheoryModel [Sentence]
getNotes = ([Sentence] -> f [Sentence]) -> TheoryModel -> f TheoryModel
Lens' TheoryModel [Sentence]
notes

-- TODO: I think we should be gathering these from the ModelKinds of the TheoryModel.
--       If we need "more than 1 ModelKind" in the TheoryModel, we may need to create
--       a "stacked model" that allows for composing them.

-- | Finds the 'ShortName' of the 'TheoryModel'.
instance HasShortName       TheoryModel where shortname :: TheoryModel -> ShortName
shortname = TheoryModel -> ShortName
lb
-- | Finds the reference address of the 'TheoryModel'.
instance HasRefAddress      TheoryModel where getRefAdd :: TheoryModel -> LblType
getRefAdd TheoryModel
l = IRefProg -> String -> LblType
RP (String -> IRefProg
prepend (String -> IRefProg) -> String -> IRefProg
forall a b. (a -> b) -> a -> b
$ TheoryModel -> String
forall c. CommonIdea c => c -> String
abrv TheoryModel
l) (TheoryModel -> String
ra TheoryModel
l)
-- | Finds the idea of a 'TheoryModel' (abbreviation).
instance CommonIdea         TheoryModel where abrv :: TheoryModel -> String
abrv TheoryModel
_ = CI -> String
forall c. CommonIdea c => c -> String
abrv CI
thModel
instance Express            TheoryModel where mexpress :: TheoryModel -> NonEmpty ModelExpr
mexpress = ModelKind ModelExpr -> NonEmpty ModelExpr
forall c. Express c => c -> NonEmpty ModelExpr
mexpress (ModelKind ModelExpr -> NonEmpty ModelExpr)
-> (TheoryModel -> ModelKind ModelExpr)
-> TheoryModel
-> NonEmpty ModelExpr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TheoryModel
-> Getting (ModelKind ModelExpr) TheoryModel (ModelKind ModelExpr)
-> ModelKind ModelExpr
forall s a. s -> Getting a s a -> a
^. Getting (ModelKind ModelExpr) TheoryModel (ModelKind ModelExpr)
Lens' TheoryModel (ModelKind ModelExpr)
mk)
-- | Finds the reference address of a 'TheoryModel'.
instance Referable TheoryModel where
  refAdd :: TheoryModel -> String
refAdd      = TheoryModel -> String
ra
  renderRef :: TheoryModel -> LblType
renderRef TheoryModel
l = IRefProg -> String -> LblType
RP (String -> IRefProg
prepend (String -> IRefProg) -> String -> IRefProg
forall a b. (a -> b) -> a -> b
$ TheoryModel -> String
forall c. CommonIdea c => c -> String
abrv TheoryModel
l) (TheoryModel -> String
forall s. Referable s => s -> String
refAdd TheoryModel
l)

-- TODO: Theory Models should generally be using their own UID, instead of
--       having their UIDs derived by the model kind.

-- This "smart" constructor is really quite awful, it takes way too many arguments.
-- This should likely be re-arranged somehow. Especially since since of the arguments
-- have the same type!
-- | Constructor for theory models. Must have a source. Uses the shortname of the reference address.
tm :: ModelKind ModelExpr -> [DecRef] -> String -> [Sentence] -> TheoryModel
tm :: ModelKind ModelExpr
-> [DecRef] -> String -> [Sentence] -> TheoryModel
tm ModelKind ModelExpr
mkind [] String
_   = String -> [Sentence] -> TheoryModel
forall a. HasCallStack => String -> a
error (String -> [Sentence] -> TheoryModel)
-> String -> [Sentence] -> TheoryModel
forall a b. (a -> b) -> a -> b
$ String
"Source field of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ ModelKind ModelExpr -> String
forall a. HasUID a => a -> String
showUID ModelKind ModelExpr
mkind String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is empty"
tm ModelKind ModelExpr
mkind [DecRef]
r  String
lbe = ModelKind ModelExpr
-> [DecRef] -> ShortName -> String -> [Sentence] -> TheoryModel
TM ModelKind ModelExpr
mkind [DecRef]
r (Sentence -> ShortName
shortname' (Sentence -> ShortName) -> Sentence -> ShortName
forall a b. (a -> b) -> a -> b
$ String -> Sentence
S String
lbe) (CI -> String -> String
forall c. CommonIdea c => c -> String -> String
prependAbrv CI
thModel String
lbe)

-- | Constructor for theory models. Uses the shortname of the reference address.
tmNoRefs :: ModelKind ModelExpr -> String -> [Sentence] -> TheoryModel
tmNoRefs :: ModelKind ModelExpr -> String -> [Sentence] -> TheoryModel
tmNoRefs ModelKind ModelExpr
mkind String
lbe = ModelKind ModelExpr
-> [DecRef] -> ShortName -> String -> [Sentence] -> TheoryModel
TM ModelKind ModelExpr
mkind [] (Sentence -> ShortName
shortname' (Sentence -> ShortName) -> Sentence -> ShortName
forall a b. (a -> b) -> a -> b
$ String -> Sentence
S String
lbe) (CI -> String -> String
forall c. CommonIdea c => c -> String -> String
prependAbrv CI
thModel String
lbe)