drasil-lang: clean up UID-related stuff and move it away from the other modules

[balacij]

Contributes to #2885

Once #2873 is merged, UID will move there, so I'm at least moving the module to a different namespace now, locally in drasil-lang.

[JacquesCarette]

I don't quite understand: #2873 is not a PR but an issue? Is there a PR that this is waiting on?

[JacquesCarette]

in this case, theory:v_x1 and v_x1:theory both make little sense... curious where it comes from. The reasoning above is sound, so it's super weird that the theory now comes at the end!

[balacij]

That UID is for:

Drasil/code/drasil-example/dblpend/lib/Drasil/DblPend/GenDefs.hs

Lines 33 to 34 in 1330bc4

	velXGD_1 :: GenDefn
	velXGD_1 = gdNoRefs (equationalModel' velXQD_1) (getUnit velocity) (Just velXDeriv_1) "velocityX1" [{-Notes-}]

Relevant 'backend' code:

Drasil/code/drasil-theory/lib/Theory/Drasil/ModelKinds.hs

Lines 89 to 91 in 1330bc4

	-- | Smart constructor for 'EquationalModel's, deriving UID+Term from the 'QDefinition'
	equationalModel' :: QDefinition e -> ModelKind e
	equationalModel' qd = MK (EquationalModel qd) (modelNs $ qd ^. uid) (qd ^. term)

Drasil/code/drasil-theory/lib/Theory/Drasil/ModelKinds.hs

Lines 58 to 59 in 1330bc4

	modelNs :: UID -> UID
	modelNs = nsUid "theory"

[balacij]

i.e., theory is a namespace

[JacquesCarette]

So you want namespaces to appear on the right?

[balacij]

If we have nest C $ nest B $ nest A X, the UID before this PR ends up as: C:B:A:X.

I read the relationships between C, B, and A as $C \subset B \subset A$. The code would then be read as "nest $X$ in $A$, then create a new namespace for $X$ within $A$, etc.". In which case, the update would make more sense because it shows $X$ near the smallest namespace, C (e.g., X:C:B:A).

Thinking about it again... maybe I was confused? The documentation is unclear about the relationship between the nested namespaces. I'm not sure, and I'm impartial because I'm fairly convinced we're going to have to completely rework the UID system once we get to the real work on editing the chunk graph, theory refinements, etc.

[balacij]

Or did you mean that you agreed with my view and just wanted the larger namespaces to appear leftmost rather than rightmost? e.g., A:B:C:X.

[JacquesCarette]

I want our name-spacing conventions to be the same as Haskell's and Agda's, so Data.List.Membership for example. I don't see this as having anything to do with subsets, but rather is all about hierarchical classification.

[balacij]

Yeah, that does make more sense. I just updated that now in 361b507 and e2f687c .

[balacij]

Sorry, I mean "once the prototype code written for #2873 is merged, UID will live in drasil-database much closer to the upgraded ChunkDB".