{-# LANGUAGE PostfixOperators, Rank2Types, ScopedTypeVariables, TemplateHaskell,
             FlexibleInstances, MultiParamTypeClasses, TupleSections #-}

-- | Defines types and functions for creating mult-definitions.
module Theory.Drasil.MultiDefn(
  -- * Types
  MultiDefn, DefiningExpr,
  -- * Constructors
  mkMultiDefn, mkMultiDefnForQuant, mkDefiningExpr,
  -- * Functions
  multiDefnGenQD, multiDefnGenQDByUID,
) where

import Control.Lens (makeLenses, view, (^.))
import Data.List (union)
import qualified Data.List.NonEmpty as NE
import Language.Drasil hiding (DefiningExpr)
import Language.Drasil.Development (showUID)

-- | 'DefiningExpr' are the data that make up a (quantity) definition, namely
--   the description, the defining (rhs) expression and the context domain(s).
--   These are meant to be 'alternate' but equivalent definitions for a single
--   concept.
data DefiningExpr e = DefiningExpr
  { -- | UID
    forall e. DefiningExpr e -> UID
_deUid :: UID,
    -- | Concept domain
    forall e. DefiningExpr e -> [UID]
_cd :: [UID],
    -- | Defining description/statement
    forall e. DefiningExpr e -> Sentence
_rvDesc :: Sentence,
    -- | Defining expression
    forall e. DefiningExpr e -> e
_expr :: e
  }

makeLenses ''DefiningExpr

instance Eq (DefiningExpr e) where DefiningExpr e
a == :: DefiningExpr e -> DefiningExpr e -> Bool
== DefiningExpr e
b = DefiningExpr e
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
== DefiningExpr e
b forall s a. s -> Getting a s a -> a
^. forall c. HasUID c => Lens' c UID
uid

instance HasUID (DefiningExpr e) where uid :: Lens' (DefiningExpr e) UID
uid = forall e. Lens' (DefiningExpr e) UID
deUid

instance ConceptDomain (DefiningExpr e) where cdom :: DefiningExpr e -> [UID]
cdom = (forall s a. s -> Getting a s a -> a
^. forall e. Lens' (DefiningExpr e) [UID]
cd)

instance Definition (DefiningExpr e) where defn :: Lens' (DefiningExpr e) Sentence
defn = forall e. Lens' (DefiningExpr e) Sentence
rvDesc

-- | 'MultiDefn's are QDefinition factories, used for showing one or more ways
--   we can define a QDefinition.
data MultiDefn e = MultiDefn{
  -- | UID
  forall e. MultiDefn e -> UID
_rUid :: UID,
  -- | Underlying quantity it defines.
  forall e. MultiDefn e -> QuantityDict
_qd :: QuantityDict,
  -- | Explanation of the different ways we can define a quantity.
  forall e. MultiDefn e -> Sentence
_rDesc :: Sentence,
  -- | All possible ways we can define the related quantity.
  forall e. MultiDefn e -> NonEmpty (DefiningExpr e)
_rvs :: NE.NonEmpty (DefiningExpr e)
}

makeLenses ''MultiDefn

instance HasUID           (MultiDefn e) where uid :: Lens' (MultiDefn e) UID
uid     = forall e. Lens' (MultiDefn e) UID
rUid
instance HasSymbol        (MultiDefn e) where symbol :: MultiDefn e -> Stage -> Symbol
symbol  = forall c. HasSymbol c => c -> Stage -> Symbol
symbol forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall s a. s -> Getting a s a -> a
^. forall e. Lens' (MultiDefn e) QuantityDict
qd)
instance NamedIdea        (MultiDefn e) where term :: Lens' (MultiDefn e) NP
term    = forall e. Lens' (MultiDefn e) QuantityDict
qd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c. NamedIdea c => Lens' c NP
term
instance Idea             (MultiDefn e) where getA :: MultiDefn e -> Maybe String
getA    = forall c. Idea c => c -> Maybe String
getA forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall s a. s -> Getting a s a -> a
^. forall e. Lens' (MultiDefn e) QuantityDict
qd)
instance HasSpace         (MultiDefn e) where typ :: Getter (MultiDefn e) Space
typ     = forall e. Lens' (MultiDefn e) QuantityDict
qd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c. HasSpace c => Getter c Space
typ
instance Definition       (MultiDefn e) where defn :: Lens' (MultiDefn e) Sentence
defn    = forall e. Lens' (MultiDefn e) Sentence
rDesc
instance Quantity         (MultiDefn e)
instance MayHaveUnit      (MultiDefn e) where getUnit :: MultiDefn e -> Maybe UnitDefn
getUnit = forall u. MayHaveUnit u => u -> Maybe UnitDefn
getUnit forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s (m :: * -> *) a. MonadReader s m => Getting a s a -> m a
view forall e. Lens' (MultiDefn e) QuantityDict
qd
-- | The concept domain of a MultiDefn is the union of the concept domains of
-- the underlying variants.
instance ConceptDomain    (MultiDefn e) where
  cdom :: MultiDefn e -> [UID]
cdom = forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 forall a. Eq a => [a] -> [a] -> [a]
union forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. NonEmpty a -> [a]
NE.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
NE.map (forall s a. s -> Getting a s a -> a
^. forall e. Lens' (DefiningExpr e) [UID]
cd) forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall s a. s -> Getting a s a -> a
^. forall e e.
Lens
  (MultiDefn e)
  (MultiDefn e)
  (NonEmpty (DefiningExpr e))
  (NonEmpty (DefiningExpr e))
rvs)
instance RequiresChecking (MultiDefn Expr) Expr Space where
  requiredChecks :: MultiDefn Expr -> [(Expr, Space)]
requiredChecks MultiDefn Expr
md = forall a b. (a -> b) -> [a] -> [b]
map (\DefiningExpr Expr
x -> (DefiningExpr Expr
x forall s a. s -> Getting a s a -> a
^. forall e e. Lens (DefiningExpr e) (DefiningExpr e) e e
expr, MultiDefn Expr
md forall s a. s -> Getting a s a -> a
^. forall c. HasSpace c => Getter c Space
typ)) forall a b. (a -> b) -> a -> b
$ forall a. NonEmpty a -> [a]
NE.toList forall a b. (a -> b) -> a -> b
$ MultiDefn Expr
md forall s a. s -> Getting a s a -> a
^. forall e e.
Lens
  (MultiDefn e)
  (MultiDefn e)
  (NonEmpty (DefiningExpr e))
  (NonEmpty (DefiningExpr e))
rvs

-- | The complete Relation of a MultiDefn is defined as the quantity and the
--   related expressions being equal (e.g., `q $= a $= b $= ... $= z`)
instance Express e => Express (MultiDefn e) where
  express :: MultiDefn e -> ModelExpr
express MultiDefn e
q = forall r. ModelExprC r => [r] -> r
equiv forall a b. (a -> b) -> a -> b
$ forall r c. (ExprC r, HasUID c, HasSymbol c) => c -> r
sy MultiDefn e
q forall a. a -> [a] -> [a]
: forall a. NonEmpty a -> [a]
NE.toList (forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
NE.map (forall c. Express c => c -> ModelExpr
express forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall s a. s -> Getting a s a -> a
^. forall e e. Lens (DefiningExpr e) (DefiningExpr e) e e
expr)) (MultiDefn e
q forall s a. s -> Getting a s a -> a
^. forall e e.
Lens
  (MultiDefn e)
  (MultiDefn e)
  (NonEmpty (DefiningExpr e))
  (NonEmpty (DefiningExpr e))
rvs))

-- | Smart constructor for MultiDefns, does nothing special at the moment. First
-- argument is the 'String' to become a 'UID'.
mkMultiDefn :: String -> QuantityDict -> Sentence -> NE.NonEmpty (DefiningExpr e) -> MultiDefn e
mkMultiDefn :: forall e.
String
-> QuantityDict
-> Sentence
-> NonEmpty (DefiningExpr e)
-> MultiDefn e
mkMultiDefn String
u QuantityDict
q Sentence
s NonEmpty (DefiningExpr e)
des
  | forall (t :: * -> *) a. Foldable t => t a -> Int
length NonEmpty (DefiningExpr e)
des forall a. Eq a => a -> a -> Bool
== Int
dupsRemovedLen = forall e.
UID
-> QuantityDict
-> Sentence
-> NonEmpty (DefiningExpr e)
-> MultiDefn e
MultiDefn (String -> UID
mkUid String
u) QuantityDict
q Sentence
s NonEmpty (DefiningExpr e)
des
  | Bool
otherwise                    = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$
      String
"MultiDefn `" forall a. [a] -> [a] -> [a]
++ String
u forall a. [a] -> [a] -> [a]
++ String
"` created with non-unique list of expressions"
  where
    dupsRemovedLen :: Int
dupsRemovedLen = forall (t :: * -> *) a. Foldable t => t a -> Int
length forall a b. (a -> b) -> a -> b
$ forall a. Eq a => NonEmpty a -> NonEmpty a
NE.nub NonEmpty (DefiningExpr e)
des

-- Should showUID be used here?

-- | Smart constructor for 'MultiDefn's defining 'UID's using that of the 'QuantityDict'.
mkMultiDefnForQuant :: QuantityDict -> Sentence -> NE.NonEmpty (DefiningExpr e) -> MultiDefn e
mkMultiDefnForQuant :: forall e.
QuantityDict
-> Sentence -> NonEmpty (DefiningExpr e) -> MultiDefn e
mkMultiDefnForQuant QuantityDict
q = forall e.
String
-> QuantityDict
-> Sentence
-> NonEmpty (DefiningExpr e)
-> MultiDefn e
mkMultiDefn (forall a. HasUID a => a -> String
showUID QuantityDict
q) QuantityDict
q

-- | Smart constructor for 'DefiningExpr's.
mkDefiningExpr :: String -> [UID] -> Sentence -> e -> DefiningExpr e
mkDefiningExpr :: forall e. String -> [UID] -> Sentence -> e -> DefiningExpr e
mkDefiningExpr String
u = forall e. UID -> [UID] -> Sentence -> e -> DefiningExpr e
DefiningExpr (String -> UID
mkUid String
u)

-- | Convert 'MultiDefn's into 'QDefinition's via a specific 'DefiningExpr'.
multiDefnGenQD :: MultiDefn e -> DefiningExpr e -> QDefinition e
multiDefnGenQD :: forall e. MultiDefn e -> DefiningExpr e -> QDefinition e
multiDefnGenQD MultiDefn e
md DefiningExpr e
de =
  forall e.
UID
-> NP
-> Sentence
-> (Stage -> Symbol)
-> Space
-> Maybe UnitDefn
-> e
-> QDefinition e
mkQDefSt
    (MultiDefn e
md forall s a. s -> Getting a s a -> a
^. forall e. Lens' (MultiDefn e) QuantityDict
qd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c. HasUID c => Lens' c UID
uid)
    (MultiDefn e
md forall s a. s -> Getting a s a -> a
^. forall c. NamedIdea c => Lens' c NP
term)
    (MultiDefn e
md forall s a. s -> Getting a s a -> a
^. forall c. Definition c => Lens' c Sentence
defn)
    (forall c. HasSymbol c => c -> Stage -> Symbol
symbol MultiDefn e
md)
    (MultiDefn e
md forall s a. s -> Getting a s a -> a
^. forall c. HasSpace c => Getter c Space
typ)
    (forall u. MayHaveUnit u => u -> Maybe UnitDefn
getUnit MultiDefn e
md)
    (DefiningExpr e
de forall s a. s -> Getting a s a -> a
^. forall e e. Lens (DefiningExpr e) (DefiningExpr e) e e
expr)

-- | Convert 'MultiDefn's into 'QDefinition's via a specific 'DefiningExpr' (by 'UID').
multiDefnGenQDByUID :: MultiDefn e -> UID -> QDefinition e
multiDefnGenQDByUID :: forall e. MultiDefn e -> UID -> QDefinition e
multiDefnGenQDByUID MultiDefn e
md UID
u
  | forall (t :: * -> *) a. Foldable t => t a -> Int
length [DefiningExpr e]
matches forall a. Eq a => a -> a -> Bool
== Int
1 = forall e. MultiDefn e -> DefiningExpr e -> QDefinition e
multiDefnGenQD MultiDefn e
md DefiningExpr e
matched
  | Bool
otherwise           = forall a. HasCallStack => String -> a
error forall a b. (a -> b) -> a -> b
$
    String
"Invalid defining expression `" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show UID
u forall a. [a] -> [a] -> [a]
++ String
"` for QDef creation in MultiDefn `" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show UID
u forall a. [a] -> [a] -> [a]
++ String
"`"
  where
    matches :: [DefiningExpr e]
matches = forall a. (a -> Bool) -> NonEmpty a -> [a]
NE.filter (\DefiningExpr e
x -> DefiningExpr e
x forall s a. s -> Getting a s a -> a
^. forall c. HasUID c => Lens' c UID
uid forall a. Eq a => a -> a -> Bool
== UID
u) (MultiDefn e
md forall s a. s -> Getting a s a -> a
^. forall e e.
Lens
  (MultiDefn e)
  (MultiDefn e)
  (NonEmpty (DefiningExpr e))
  (NonEmpty (DefiningExpr e))
rvs)
    matched :: DefiningExpr e
matched = forall a. [a] -> a
head [DefiningExpr e]
matches