Skip to content

Commit

Permalink
Proto-Realms?
Browse files Browse the repository at this point in the history
  • Loading branch information
balacij committed Jun 4, 2021
1 parent 8dc9d18 commit e45bc85
Show file tree
Hide file tree
Showing 7 changed files with 96 additions and 52 deletions.
8 changes: 4 additions & 4 deletions code/drasil-example/Drasil/GamePhysics/TMods.hs
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ module Drasil.GamePhysics.TMods (tMods, newtonSL, newtonSLR, newtonTL, newtonLUG
import qualified Data.List.NonEmpty as NE

import Language.Drasil
import Theory.Drasil (tmNoRefs, tmNoRefs', ModelKinds(..), RealmVariant(..), TheoryModel)
import Theory.Drasil
import Utils.Drasil
import qualified Utils.Drasil.Sentence as S

Expand Down Expand Up @@ -48,9 +48,9 @@ newtonTLNote = foldlSent [(S "Every action has an equal and opposite reaction" !

-- FIXME: Missing ConceptDomain!
newtonLUGModel :: ModelKinds
newtonLUGModel = EquationalRealm newtonForceQuant $ NE.fromList [
RV [] EmptyS (sy gravitationalConst `mulRe` (sy mass_1 `mulRe` sy mass_2 $/ square (sy dispNorm)) `mulRe` sy dVect),
RV [] EmptyS (sy gravitationalConst `mulRe` (sy mass_1 `mulRe` sy mass_2 $/ square (sy dispNorm)) `mulRe` (sy distMass $/ sy dispNorm))
newtonLUGModel = EquationalRealm $ mkRealmForQuant newtonForceQuant EmptyS $ NE.fromList [
mkRealmVariant [] EmptyS (sy gravitationalConst `mulRe` (sy mass_1 `mulRe` sy mass_2 $/ square (sy dispNorm)) `mulRe` sy dVect),
mkRealmVariant [] EmptyS (sy gravitationalConst `mulRe` (sy mass_1 `mulRe` sy mass_2 $/ square (sy dispNorm)) `mulRe` (sy distMass $/ sy dispNorm))
]

newtonLUG :: TheoryModel
Expand Down
5 changes: 4 additions & 1 deletion code/drasil-theory/Theory/Drasil.hs
Original file line number Diff line number Diff line change
Expand Up @@ -8,9 +8,11 @@ module Theory.Drasil (
, GenDefn
, gd, gdNoRefs, gd', gdNoRefs'
, getEqModQdsFromGd
-- Realms
, Realm, RealmVariant
, mkRealm, mkRealmForQuant, mkRealmVariant
-- ModelKinds
, ModelKinds(..), getEqModQds
, RealmVariant(..)
-- InstanceModel
, InstanceModel
, im, imNoDeriv, imNoRefs, imNoDerivNoRefs
Expand All @@ -24,4 +26,5 @@ import Theory.Drasil.DataDefinition (DataDefinition, dd, ddNoRefs, qdFromDD)
import Theory.Drasil.GenDefn
import Theory.Drasil.ModelKinds
import Theory.Drasil.InstanceModel
import Theory.Drasil.Realms
import Theory.Drasil.Theory
7 changes: 4 additions & 3 deletions code/drasil-theory/Theory/Drasil/GenDefn.hs
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ module Theory.Drasil.GenDefn (GenDefn,
import Language.Drasil
import Data.Drasil.TheoryConcepts (genDefn)
import Theory.Drasil.ModelKinds (ModelKinds(..), elimMk, setMk, getEqModQds)
import Theory.Drasil.Realms

import Control.Lens (makeLenses, view, lens, (^.), set, Lens')

Expand All @@ -22,7 +23,7 @@ data GenDefn = GD { _gUid :: UID
makeLenses ''GenDefn

-- | Make 'Lens' for a 'GenDefn' based on its 'ModelKinds'.
lensMk :: forall a. Lens' QDefinition a -> Lens' QuantityDict a -> Lens' RelationConcept a -> Lens' GenDefn a
lensMk :: forall a. Lens' QDefinition a -> Lens' Realm a -> Lens' RelationConcept a -> Lens' GenDefn a
lensMk lq lqd lr = lens g s
where g :: GenDefn -> a
g gd_ = elimMk lq lqd lr (gd_ ^. mk)
Expand All @@ -36,13 +37,13 @@ instance NamedIdea GenDefn where term = lensMk term term term
-- | Finds the idea contained in the 'GenDefn'.
instance Idea GenDefn where getA = getA . (^. mk)
-- | Finds the definition of the 'GenDefn'.
instance Definition GenDefn where defn = lensMk defn undefined defn
instance Definition GenDefn where defn = lensMk defn defn defn
-- | Finds the domain of the 'GenDefn'.
instance ConceptDomain GenDefn where cdom = cdom . (^. mk)
-- | Finds the relation expression for a 'GenDefn'.
instance ExprRelat GenDefn where relat = relat . (^. mk)
-- | Finds the defining expression for a 'GenDefn'.
instance DefiningExpr GenDefn where defnExpr = lensMk defnExpr undefined defnExpr
instance DefiningExpr GenDefn where defnExpr = lensMk defnExpr undefined defnExpr -- TODO: Defining expression of an EquationalRealm?
-- | Finds the derivation of the 'GenDefn'. May contain Nothing.
instance HasDerivation GenDefn where derivations = deri
-- | Finds 'Reference's contained in the 'GenDefn'.
Expand Down
5 changes: 3 additions & 2 deletions code/drasil-theory/Theory/Drasil/InstanceModel.hs
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ import Data.Drasil.TheoryConcepts (inModel)

import Control.Lens (set, (^.), lens, view, makeLenses, Lens', _1, _2)
import Theory.Drasil.ModelKinds (ModelKinds(..), elimMk, setMk, getEqModQds)
import Theory.Drasil.Realms

type Input = (QuantityDict, Maybe (RealInterval Expr Expr))
type Inputs = [Input]
Expand All @@ -31,7 +32,7 @@ data InstanceModel = IM { _mk :: ModelKinds
makeLenses ''InstanceModel

-- | Make 'Lens' for an 'InstanceModel' based on its 'ModelKinds'.
lensMk :: forall a. Lens' QDefinition a -> Lens' QuantityDict a -> Lens' RelationConcept a -> Lens' InstanceModel a
lensMk :: forall a. Lens' QDefinition a -> Lens' Realm a -> Lens' RelationConcept a -> Lens' InstanceModel a
lensMk lq lqd lr = lens g s
where g :: InstanceModel -> a
g im_ = elimMk lq lqd lr (im_ ^. mk)
Expand All @@ -45,7 +46,7 @@ instance NamedIdea InstanceModel where term = lensMk term term term
-- | Finds the idea contained in the 'InstanceModel'.
instance Idea InstanceModel where getA = getA . (^. mk)
-- | Finds the definition of the 'InstanceModel'.
instance Definition InstanceModel where defn = lensMk defn undefined defn
instance Definition InstanceModel where defn = lensMk defn defn defn
-- | Finds the domain of the 'InstanceModel'.
instance ConceptDomain InstanceModel where cdom = cdom . (^. mk)
-- | Finds the relation expression for an 'InstanceModel'.
Expand Down
61 changes: 20 additions & 41 deletions code/drasil-theory/Theory/Drasil/ModelKinds.hs
Original file line number Diff line number Diff line change
@@ -1,36 +1,21 @@
{-# LANGUAGE TemplateHaskell, Rank2Types, ScopedTypeVariables, PostfixOperators #-}
module Theory.Drasil.ModelKinds (ModelKinds(..), RealmVariant(..),
module Theory.Drasil.ModelKinds (ModelKinds(..),
setMk, elimMk, lensMk, getEqModQds) where

import Control.Lens ((^.), to, lens, set, makeLenses, makeLensesFor,
Getter, Lens', Setter')
import Control.Lens
import Data.Maybe (mapMaybe)
import Data.List (union)
import qualified Data.List.NonEmpty as NE

import Language.Drasil (($=), sy, Expr, RelationConcept,
NamedIdea(..), HasUID(..), ExprRelat(..), ConceptDomain(..), Definition(..),
Idea(..), DefiningExpr(..), UID, Sentence, QDefinition, QuantityDict)

-- | 'RealmVariant's are partial components of QDefinitions, containing only
-- the defining expressions and descriptions.
-- Any 'RealmVariant' paired with a 'QuantityDict' will form a "whole" 'QDefinition'.
data RealmVariant = RV {
_cd :: [UID],
_desc :: Sentence,
_expr :: Expr
}

makeLensesFor [("_expr", "expr")] ''RealmVariant
import Language.Drasil
import Theory.Drasil.Realms

-- | Models can be of different kinds:
--
-- * 'EquationalModel's represent quantities that are calculated via a single definition/'QDefinition'.
-- * 'EquationalRealm's represent quantities that may be calculated using any one of many 'RealmVariant's (e.g., 'x = A = ... = Z')
-- * 'EquationalRealm's represent Realms; quantities that may be calculated using any one of many 'RealmVariant's (e.g., 'x = A = ... = Z')
-- * 'DEModel's represent differential equations as 'RelationConcept's
-- * 'OthModel's are placeholders for models. No new 'OthModel's should be created, they should be using one of the other kinds.
data ModelKinds = EquationalModel QDefinition
| EquationalRealm QuantityDict (NE.NonEmpty RealmVariant)
| EquationalRealm Realm
| DEModel RelationConcept
| OthModel RelationConcept

Expand All @@ -43,38 +28,32 @@ instance NamedIdea ModelKinds where term = lensMk term term term
-- | Finds the idea of the 'ModelKinds'.
instance Idea ModelKinds where getA = elimMk (to getA) (to getA) (to getA)
-- | Finds the definition of the 'ModelKinds'.
instance Definition ModelKinds where defn = lensMk defn (error "ambiguous definition (defn) in EquationalRealm") defn
instance Definition ModelKinds where defn = lensMk defn defn defn
-- | Finds the domain of the 'ModelKinds'.
instance ConceptDomain ModelKinds where
cdom (EquationalRealm _ rvs) = foldr1 union $ NE.toList (NE.map _cd rvs)
cdom m = elimMk (to cdom) undefined (to cdom) m
instance ConceptDomain ModelKinds where cdom = elimMk (to cdom) (to cdom) (to cdom)
-- | Finds the defining expression of the 'ModelKinds'.
instance DefiningExpr ModelKinds where defnExpr = lensMk defnExpr (error "ambiguous defining expression (defnExpr) for EquationalRealm") defnExpr
-- | Finds the relation expression of the 'ModelKinds'.
instance ExprRelat ModelKinds where
relat (EquationalRealm q rs) = sy q $= foldr1 ($=) (NE.map (^. expr) rs)
relat (EquationalModel q) = relat q
relat (DEModel q) = relat q
relat (OthModel q) = relat q
instance ExprRelat ModelKinds where relat = elimMk (to relat) (to relat) (to relat)

-- TODO: implement MayHaveUnit for ModelKinds once we've sufficiently removed OthModels & RelationConcepts (else we'd be breaking too much of `stable`)

-- | Retrieve internal data from ModelKinds
elimMk :: Getter QDefinition a -> Getter QuantityDict a -> Getter RelationConcept a -> ModelKinds -> a
elimMk l _ _ (EquationalModel q) = q ^. l
elimMk _ l _ (EquationalRealm q _) = q ^. l
elimMk _ _ l (DEModel q) = q ^. l
elimMk _ _ l (OthModel q) = q ^. l
elimMk :: Getter QDefinition a -> Getter Realm a -> Getter RelationConcept a -> ModelKinds -> a
elimMk l _ _ (EquationalModel q) = q ^. l
elimMk _ l _ (EquationalRealm q) = q ^. l
elimMk _ _ l (DEModel q) = q ^. l
elimMk _ _ l (OthModel q) = q ^. l

-- | Map into internal representations of ModelKinds
setMk :: ModelKinds -> Setter' QDefinition a -> Setter' QuantityDict a -> Setter' RelationConcept a -> a -> ModelKinds
setMk (EquationalModel q) f _ _ x = EquationalModel $ set f x q
setMk (EquationalRealm q vs) _ f _ x = EquationalRealm (set f x q) vs
setMk (DEModel q) _ _ g x = DEModel $ set g x q
setMk (OthModel q) _ _ g x = OthModel $ set g x q
setMk :: ModelKinds -> Setter' QDefinition a -> Setter' Realm a -> Setter' RelationConcept a -> a -> ModelKinds
setMk (EquationalModel q) f _ _ x = EquationalModel $ set f x q
setMk (EquationalRealm q) _ f _ x = EquationalRealm $ set f x q
setMk (DEModel q) _ _ g x = DEModel $ set g x q
setMk (OthModel q) _ _ g x = OthModel $ set g x q

-- | Make a 'Lens' for 'ModelKinds'.
lensMk :: forall a. Lens' QDefinition a -> Lens' QuantityDict a -> Lens' RelationConcept a -> Lens' ModelKinds a
lensMk :: forall a. Lens' QDefinition a -> Lens' Realm a -> Lens' RelationConcept a -> Lens' ModelKinds a
lensMk lq lqd lr = lens g s
where g :: ModelKinds -> a
g mk = elimMk lq lqd lr mk
Expand Down
59 changes: 59 additions & 0 deletions code/drasil-theory/Theory/Drasil/Realms.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,59 @@
{-# LANGUAGE TemplateHaskell, Rank2Types, ScopedTypeVariables, PostfixOperators #-}

module Theory.Drasil.Realms (Realm, RealmVariant,
mkRealm, mkRealmForQuant, mkRealmVariant) where

import Control.Lens ((^.), view, makeLenses, makeLensesFor)
import Data.List (union)
import qualified Data.List.NonEmpty as NE

import Language.Drasil

-- TODO: Need a system for instantiating Realms into QDefs via "selecting" variants

-- | 'RealmVariant's are partial components of QDefinitions, containing only
-- the defining expressions and descriptions.
-- Any 'RealmVariant' paired with a 'QuantityDict' will form a "whole" 'QDefinition'.
data RealmVariant = RV {
_cd :: [UID], -- ^ Concept domain
_rvDesc :: Sentence, -- ^ Defining description/statement
_expr :: Expr -- ^ Defining expression
}
makeLensesFor [("_expr", "expr")] ''RealmVariant

-- | 'Realm's are QDefinition factories, used for showing one or more ways we
-- can define a QDefinition
data Realm = Realm {
_rUid :: UID, -- ^ UID
_qd :: QuantityDict, -- ^ Underlying quantity it defines
_rDesc :: Sentence, -- ^ Defining description/statement
_rvs :: NE.NonEmpty RealmVariant -- ^ All possible/omitted ways we can define the related quantity
}
makeLenses ''Realm


instance HasUID Realm where uid = rUid
instance HasSymbol Realm where symbol = symbol . (^. qd)
instance NamedIdea Realm where term = qd . term
instance Idea Realm where getA = getA . (^. qd)
instance HasSpace Realm where typ = qd . typ
instance Quantity Realm where
instance MayHaveUnit Realm where getUnit = getUnit . view qd
-- | The concept domain of a Realm is the union of the concept domains of the underlying variants.
instance ConceptDomain Realm where cdom = foldr1 union . NE.toList . NE.map _cd . (^. rvs)
instance Definition Realm where defn = rDesc
-- | The related Relation of a Realm is defined as the quantity and the related expressions being equal
-- e.g., `q $= a $= b $= ... $= z`
instance ExprRelat Realm where relat q = sy q $= foldr1 ($=) (NE.map (^. expr) (q ^. rvs))

-- | Smart constructor for Realms, does nothing special at the moment
mkRealm :: UID -> QuantityDict -> Sentence -> NE.NonEmpty RealmVariant -> Realm
mkRealm = Realm

-- | Smart constructor for Realms defining UIDs using that of the QuantityDict
mkRealmForQuant :: QuantityDict -> Sentence -> NE.NonEmpty RealmVariant -> Realm
mkRealmForQuant q = mkRealm (q ^. uid) q

-- | Smart constructor for RealmVariants
mkRealmVariant :: [UID] -> Sentence -> Expr -> RealmVariant
mkRealmVariant = RV
3 changes: 2 additions & 1 deletion code/drasil-theory/drasil-theory.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ cabal-version: 1.12
--
-- see: https://github.com/sol/hpack
--
-- hash: 7ac680e321d549078594c3d6ca4b19d095f5a7b72aae80dcefb44949eb511bed
-- hash: 766032e13eb65e0e109f78005d03f085276dd77f03e988d04ba815482d7145ce

name: drasil-theory
version: 0.1.0.0
Expand All @@ -30,6 +30,7 @@ library
Theory.Drasil.GenDefn
Theory.Drasil.InstanceModel
Theory.Drasil.ModelKinds
Theory.Drasil.Realms
Theory.Drasil.Theory
hs-source-dirs:
./
Expand Down

5 comments on commit e45bc85

@JacquesCarette
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hmm, what is in Theory.Drasil.Realms is super-useful - but incorrectly named. I like the "QDefinition factory" description.

The Realm paper and idea is that it is a collection of theories that end up being equivalent, so give different interfaces to the same underlying abstract component. So a Realm, in that sense, ought to fit 'above' theory, not inside.

What is true is that, indeed, the very same idea is present here, internally to a theory. One could externalize it, make a part of a "QDefinition factory" into its own theory and then use a 'Realm' to put them together -- but that would be wasteful and imprecise.

In other words, I think what's really needed is different vocabulary, with the implementation staying essentially as is. Brainstorming:

  • "Internal Realm" not wrong, but I don't like it.
  • "Multiple Definition" (shorten to MultiDefn ?) is better, as closer
  • "Definition Set". Meh. Too easy to misconstrue or misunderstand.
  • ??? (I'm tapped out).

@balacij
Copy link
Collaborator Author

@balacij balacij commented on e45bc85 Jun 6, 2021

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I agree, I definitely don't like leaving it named as a Realm.

Influenced by ADTs/"enumeration types"/disjoint unions, perhaps we could have "Quantity Definition Enumeration" (QDefEnum/QDefnEnum)? The name signals that there are many ways we can define this quantity, but that an instance of the quantity should be defined using a single constructor (in this case, a "constructor" would be the actual expression definitions).

What do you think?

@JacquesCarette
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hmm, that's still too implementation-oriented. I think I've warmed to "Multi-definition", with MultiDefn as a decent short form.

@balacij
Copy link
Collaborator Author

@balacij balacij commented on e45bc85 Jun 7, 2021

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I see. That sounds good. Would we want "DefnVar" for "Multi-Definition Variants"?

@JacquesCarette
Copy link
Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I would tend to try to be more descriptive and go with DefiningExpr. It's a tiny bit misleading (it's not just an Expr), but the Defining part should help with that, as a qualifier.

Please sign in to comment.