Redesign ExprRelat (Theoretical Models and Instance Models)

[palmerst]

The underlying infrastructure of ExprRelat needs revision with respect to the needs of code generation. Currently relations are just unrestricted Exprs which requires pattern matching hacks which may fail in order to get the information needed to generate code.

[JacquesCarette]

I think the basic issue is that Expr has :=, which is abused. We need to make a difference between 'definitions' and general relations. When you do code generation, you need to know that all your instance models are solved/oriented.

[szymczdm]

This needs to be looked at again, however, the instances of ExprRelat will very shortly ( once #104 and its related issues are done) be solely in the codegen domain (ie. none of the documentation generation will care about it once I fix a few issues and change a combinator or two).

I'll update once that's complete.

[palmerst]

@JacquesCarette should this be assigned to you? It feels like this is something that will be fixed with the Expr refactor you're working on?

[JacquesCarette]

Yep. Done.

[JacquesCarette]

@szymczdm it looks like it makes sense for me to tackle this one. But I'm a little fuzzy as to what needs done. I'm not even quite sure what ExprRelat is for at all. Could it be better documented? Its name is awful, it doesn't help me know what it is.

I get this idea that the codegen really wants to get QDefinitions only, and never really a Relation.

[szymczdm]

I believe ExprRelat was created for something like that, essentially any time we needed an expr from a chunk where we were guaranteed it would have one, but it wasn't known whether it would be a QDefn (ie. Symbol = Expr) or a relation (self-contained Expr).

[JacquesCarette]

I think we need to revisit that. I think this might pre-date some of the refactors to theories, and that's really where we should be pulling from. This may require us to deal with #473 (Teach Drasil about ODEs) first though.

[JacquesCarette]

Half of this has now been done - instance models now have a wider range of 'models' which are tagged. Code generation only looks at the 'equational' models and ignores the rest. ExprRelat itself is still used, but only for printing (where it's fine) and not for code generation, which is where the real problem was.

[balacij]

I think the basic issue is that Expr has :=, which is abused. We need to make a difference between 'definitions' and general relations. When you do code generation, you need to know that all your instance models are solved/oriented.

This looks like it's still an issue, and I think it should be addressed alongside the division of the expression language. relat right now is strictly used for creating new Exprs of the form sy x $= ... $= ... $= ... for display. If we create the discussed/proposed DisplayExpr, then I think we might want to use a := symbol (something other than = to say that we're defining something for extra differentiation between equality checking and definitions), and replace ExprRelat with something along the lines of Display that is intended to take some chunk and convert it into the display language. For example, if we had a QDefinition, it would generate the same sy x := y expressions but using the display language (so the $= would change into a :=).

[JacquesCarette]

Agreed. The only uses of relat right now should all be for display purposes.

So it would be interesting to start a new Display language that contains only two things: Expr and a new thing for :=. Then relat could be changed to output Display instead of Expr -- and we could see what breaks. Possibly not too much.