{-# 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, declareHasChunkRefs, Generically(..))
import Language.Drasil
import Language.Drasil.Document
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 -> [Char]
ra    :: String
  , TheoryModel -> [Sentence]
_notes :: [Sentence]
  }
makeLenses ''TheoryModel
declareHasChunkRefs ''TheoryModel

-- | 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 [Char]
getA = ModelKind ModelExpr -> Maybe [Char]
forall c. Idea c => c -> Maybe [Char]
getA (ModelKind ModelExpr -> Maybe [Char])
-> (TheoryModel -> ModelKind ModelExpr)
-> TheoryModel
-> Maybe [Char]
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 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 -> [Char] -> LblType
RP ([Char] -> IRefProg
prepend ([Char] -> IRefProg) -> [Char] -> IRefProg
forall a b. (a -> b) -> a -> b
$ TheoryModel -> [Char]
forall c. CommonIdea c => c -> [Char]
abrv TheoryModel
l) (TheoryModel -> [Char]
ra TheoryModel
l)
-- | Finds the idea of a 'TheoryModel' (abbreviation).
instance CommonIdea         TheoryModel where abrv :: TheoryModel -> [Char]
abrv TheoryModel
_ = CI -> [Char]
forall c. CommonIdea c => c -> [Char]
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 -> [Char]
refAdd      = TheoryModel -> [Char]
ra
  renderRef :: TheoryModel -> LblType
renderRef TheoryModel
l = IRefProg -> [Char] -> LblType
RP ([Char] -> IRefProg
prepend ([Char] -> IRefProg) -> [Char] -> IRefProg
forall a b. (a -> b) -> a -> b
$ TheoryModel -> [Char]
forall c. CommonIdea c => c -> [Char]
abrv TheoryModel
l) (TheoryModel -> [Char]
forall s. Referable s => s -> [Char]
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] -> [Char] -> [Sentence] -> TheoryModel
tm ModelKind ModelExpr
mkind [] [Char]
_   = [Char] -> [Sentence] -> TheoryModel
forall a. HasCallStack => [Char] -> a
error ([Char] -> [Sentence] -> TheoryModel)
-> [Char] -> [Sentence] -> TheoryModel
forall a b. (a -> b) -> a -> b
$ [Char]
"Source field of " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> ModelKind ModelExpr -> [Char]
forall a. HasUID a => a -> [Char]
showUID ModelKind ModelExpr
mkind [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> [Char]
" is empty"
tm ModelKind ModelExpr
mkind [DecRef]
r  [Char]
lbe = ModelKind ModelExpr
-> [DecRef] -> ShortName -> [Char] -> [Sentence] -> TheoryModel
TM ModelKind ModelExpr
mkind [DecRef]
r (Sentence -> ShortName
shortname' (Sentence -> ShortName) -> Sentence -> ShortName
forall a b. (a -> b) -> a -> b
$ [Char] -> Sentence
S [Char]
lbe) (CI -> [Char] -> [Char]
forall c. CommonIdea c => c -> [Char] -> [Char]
prependAbrv CI
thModel [Char]
lbe)

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