G. Allais

> I also wondered about clustering/reducing the dependency graph, but didn't really get started on that (there is a python script for that). We have been doing something like that...

I think it may be caused in part by https://github.com/idris-lang/Idris2/blob/05c9029b35c64873ab3ea13822039f004acd1101/src/TTImp/Elab/Case.idr#L243-L245 we throw out the nested names that were carried until we hit the `case`. It's strange though because we don't...

Probably Section 1 of: http://strictlypositive.org/Ripley.pdf We should be extremely careful about unfolding definitions when unifying under an `Inf` (as in: it's probably never OK to do so).

I'm too tired to check whether the report returned by syrup after this patch is sensible.

Ha! Because the problem is symmetric but our function was biased in one direction, I tried to run `experiment two = one` instead of the flipped version which makes Syrup...

I was thinking of just collecting the constraints and generating a file in DOT format. E.g. the following for mux: ```dot digraph mux { rankdir=TB; splines=ortho; ordering=out; subgraph cluster_inputs {...

Still thinking about the structure and writing graphs by hand I got the ripple carry adder working (still some side arrows though): ```dot digraph rca3 { rankdir=TB; splines=ortho; /***************************************************/ //...

Reusing this idea of ports for both inputs & outputs and putting all of these things into clusters, I managed to get arrows only coming and going out of the...

I have pushed a wee something on a branch: https://github.com/pigworker/Syrup/blob/diagram/SRC/Dot.hs The "blackbox" corresponds to a box with input & output ports. The next step is to define the "whitebox" view...

@laMudri I think you are right that A normal forms would make things a lot easier. I have started an implementation here: https://github.com/pigworker/Syrup/blob/diagram/SRC/Anf.hs