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

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

import Language.Drasil
import Data.Drasil.TheoryConcepts (thModel)

import Theory.Drasil.ModelKinds

-- | Theories are the basis for building models with context,
-- spaces, quantities, operations, invariants, etc.
class Theory t where
  valid_context :: Lens' t [TheoryModel]
  spaces        :: Lens' t [SpaceDefn]
  quantities    :: Lens' t [QuantityDict]
  operations    :: Lens' t [ConceptChunk] -- FIXME: Should not be Concept
  defined_quant :: Lens' t [ModelQDef]
  invariants    :: Lens' t [ModelExpr]
  defined_fun   :: Lens' t [ModelQDef]

data SpaceDefn -- FIXME: This should be defined.

-- | A TheoryModel is a collection of:
--
--      * tUid - a UID,
--      * con - a ConceptChunk,
--      * vctx - definition context ('TheoryModel's),
--      * spc - type definitions ('SpaceDefn's),
--      * quan - quantities ('QuantityDict'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 -> [TheoryModel]
_vctx  :: [TheoryModel]
  , TheoryModel -> [SpaceDefn]
_spc   :: [SpaceDefn]
  , TheoryModel -> [QuantityDict]
_quan  :: [QuantityDict]
  , TheoryModel -> [ConceptChunk]
_ops   :: [ConceptChunk]
  , TheoryModel -> [ModelQDef]
_defq  :: [ModelQDef]
  , TheoryModel -> [ModelExpr]
_invs  :: [ModelExpr]
  , TheoryModel -> [ModelQDef]
_dfun  :: [ModelQDef]
  , TheoryModel -> [DecRef]
_rf    :: [DecRef]
  ,  TheoryModel -> ShortName
lb    :: ShortName
  ,  TheoryModel -> String
ra    :: String
  , TheoryModel -> [Sentence]
_notes :: [Sentence]
  }
makeLenses ''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 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 aspects of the 'Theory' behind the 'TheoryModel'.
instance Theory             TheoryModel where
  valid_context :: Lens' TheoryModel [TheoryModel]
valid_context = ([TheoryModel] -> f [TheoryModel]) -> TheoryModel -> f TheoryModel
Lens' TheoryModel [TheoryModel]
vctx
  spaces :: Lens' TheoryModel [SpaceDefn]
spaces        = ([SpaceDefn] -> f [SpaceDefn]) -> TheoryModel -> f TheoryModel
Lens' TheoryModel [SpaceDefn]
spc
  quantities :: Lens' TheoryModel [QuantityDict]
quantities    = ([QuantityDict] -> f [QuantityDict])
-> TheoryModel -> f TheoryModel
Lens' TheoryModel [QuantityDict]
quan
  operations :: Lens' TheoryModel [ConceptChunk]
operations    = ([ConceptChunk] -> f [ConceptChunk])
-> TheoryModel -> f TheoryModel
Lens' TheoryModel [ConceptChunk]
ops
  defined_quant :: Lens' TheoryModel [ModelQDef]
defined_quant = ([ModelQDef] -> f [ModelQDef]) -> TheoryModel -> f TheoryModel
Lens' TheoryModel [ModelQDef]
defq
  invariants :: Lens' TheoryModel [ModelExpr]
invariants    = ([ModelExpr] -> f [ModelExpr]) -> TheoryModel -> f TheoryModel
Lens' TheoryModel [ModelExpr]
invs
  defined_fun :: Lens' TheoryModel [ModelQDef]
defined_fun   = ([ModelQDef] -> f [ModelQDef]) -> TheoryModel -> f TheoryModel
Lens' TheoryModel [ModelQDef]
dfun
-- | 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
-- | 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 :: (Quantity q, MayHaveUnit q, Concept c) => ModelKind ModelExpr ->
    [q] -> [c] -> [ModelQDef] ->
    [ModelExpr] -> [ModelQDef] -> [DecRef] ->
    String -> [Sentence] -> TheoryModel
tm :: forall q c.
(Quantity q, MayHaveUnit q, Concept c) =>
ModelKind ModelExpr
-> [q]
-> [c]
-> [ModelQDef]
-> [ModelExpr]
-> [ModelQDef]
-> [DecRef]
-> String
-> [Sentence]
-> TheoryModel
tm ModelKind ModelExpr
mkind [q]
_ [c]
_ [ModelQDef]
_  [ModelExpr]
_   [ModelQDef]
_   [] 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 [q]
q [c]
c [ModelQDef]
dq [ModelExpr]
inv [ModelQDef]
dfn [DecRef]
r  String
lbe = 
  ModelKind ModelExpr
-> [TheoryModel]
-> [SpaceDefn]
-> [QuantityDict]
-> [ConceptChunk]
-> [ModelQDef]
-> [ModelExpr]
-> [ModelQDef]
-> [DecRef]
-> ShortName
-> String
-> [Sentence]
-> TheoryModel
TM ModelKind ModelExpr
mkind [] [] ((q -> QuantityDict) -> [q] -> [QuantityDict]
forall a b. (a -> b) -> [a] -> [b]
map q -> QuantityDict
forall q. (Quantity q, MayHaveUnit q) => q -> QuantityDict
qw [q]
q) ((c -> ConceptChunk) -> [c] -> [ConceptChunk]
forall a b. (a -> b) -> [a] -> [b]
map c -> ConceptChunk
forall c. Concept c => c -> ConceptChunk
cw [c]
c) [ModelQDef]
dq [ModelExpr]
inv [ModelQDef]
dfn [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 :: (Quantity q, MayHaveUnit q, Concept c) => ModelKind ModelExpr ->
    [q] -> [c] -> [ModelQDef] -> [ModelExpr] -> [ModelQDef] -> 
    String -> [Sentence] -> TheoryModel
tmNoRefs :: forall q c.
(Quantity q, MayHaveUnit q, Concept c) =>
ModelKind ModelExpr
-> [q]
-> [c]
-> [ModelQDef]
-> [ModelExpr]
-> [ModelQDef]
-> String
-> [Sentence]
-> TheoryModel
tmNoRefs ModelKind ModelExpr
mkind [q]
q [c]
c [ModelQDef]
dq [ModelExpr]
inv [ModelQDef]
dfn String
lbe = 
  ModelKind ModelExpr
-> [TheoryModel]
-> [SpaceDefn]
-> [QuantityDict]
-> [ConceptChunk]
-> [ModelQDef]
-> [ModelExpr]
-> [ModelQDef]
-> [DecRef]
-> ShortName
-> String
-> [Sentence]
-> TheoryModel
TM ModelKind ModelExpr
mkind [] [] ((q -> QuantityDict) -> [q] -> [QuantityDict]
forall a b. (a -> b) -> [a] -> [b]
map q -> QuantityDict
forall q. (Quantity q, MayHaveUnit q) => q -> QuantityDict
qw [q]
q) ((c -> ConceptChunk) -> [c] -> [ConceptChunk]
forall a b. (a -> b) -> [a] -> [b]
map c -> ConceptChunk
forall c. Concept c => c -> ConceptChunk
cw [c]
c) [ModelQDef]
dq [ModelExpr]
inv [ModelQDef]
dfn [] (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)