|
| 1 | +This project is divided into three categories: The frontend (`app/`), |
| 2 | +the machinery behind it (`lib/`) and some tests (`test/`). |
| 3 | + |
| 4 | +# app |
| 5 | + |
| 6 | +# lib |
| 7 | + |
| 8 | +The library is responsible for multiple aspects of our program. For one, |
| 9 | +we have two languages (interaction calculus (IC) and lambda calculus |
| 10 | +(LC)) that have to be parsed, checked, compiled and reduced. The final |
| 11 | +product is always the `Net` structure, which abstracts aways over |
| 12 | +irrelevant things like named variables. |
| 13 | + |
| 14 | +We also have a lot of code responsible for the rendering of this `Net` |
| 15 | +structure. For that we use separate types (triangle, arrow) that only |
| 16 | +have properties actually required for rendering them. |
| 17 | + |
| 18 | +The library also defines the abstract implementations of the frontend |
| 19 | +model/view infrastructure. |
| 20 | + |
| 21 | +------------------------------------------------------------------------ |
| 22 | + |
| 23 | +The concrete different net representations: |
| 24 | + |
| 25 | + /// lambda calculus term |
| 26 | + /// (lib/language/lc/term) |
| 27 | + type Term { Sym(...); Abs(...); App(...) } |
| 28 | + |
| 29 | + /// IC constructor with named ports+polarities |
| 30 | + /// this is the intermediate representation as you would parse it from IC |
| 31 | + /// (lib/language/ic/term) |
| 32 | + type Constructor(...) |
| 33 | + |
| 34 | + /// IC constructor with unique, numeric ports, annotated with position vectors |
| 35 | + /// this is the intermediate representation used for force-directed layouting |
| 36 | + /// (lib/net/net) |
| 37 | + type Agent(...) |
| 38 | + |
| 39 | + /// as the Agents have unique ports, we have a separate Wire structure that connects them together |
| 40 | + /// (lib/net/net) |
| 41 | + type Wire(...) |
| 42 | + |
| 43 | + /// the final representation used for rendering the net to a canvas |
| 44 | + /// contains color, size, position, etc. |
| 45 | + type Triangle(...) |
| 46 | + type Arrow(...) |
| 47 | + |
| 48 | +As we generally stream all the constructs via effects between stages, we |
| 49 | +use type aliases for `WireStream = emit[Wire]`, |
| 50 | +`AgentStream = emit[Agent]`, `NetStream = { WireStream, AgentStream }`, |
| 51 | +as well as `Draw = { emit[Arrow], emit[Triangle] }`. We do not use |
| 52 | +interfaces for such streams, as we also have to reify them between |
| 53 | +stages because of the stateless UI model. Also, streams can otherwise |
| 54 | +not be replayed if they use side effects (like parsing). |
| 55 | + |
| 56 | +Roughly, a full pipeline from LC could look like this (slightly modified |
| 57 | +signatures for simplicity): |
| 58 | + |
| 59 | + language/lc/parser::parse!() / { read[Char], emit[Term] } // parse to term |
| 60 | + --> |
| 61 | + language/lc/netter::net! / { read[Term], emit[Constructor] } // translate to IC constructors |
| 62 | + --> |
| 63 | + language/ic/ruler::redexes { / emit[Constructor] } / emit[Redex] // find redexes between IC constructors |
| 64 | + --> |
| 65 | + language/ic/ruler::step { / emit[Constructor], emit[Redex] } / { emit[Constructor], emit[Redex] } // apply one rule to some redex |
| 66 | + --> |
| 67 | + ... // as many reduction steps as wanted |
| 68 | + --> |
| 69 | + net/net::net! / { read[Constructor], NetStream } // convert constructors to positioned nodes with explicit edges |
| 70 | + --> |
| 71 | + net/net::layout { / NetStream } / NetStream // single-step force-directed layout |
| 72 | + --> |
| 73 | + ... // as many layout steps as wanted |
| 74 | + --> |
| 75 | + [frontend] { / NetStream } / Draw // convert to canvas elements with color, frontend-specified sizes etc. |
| 76 | + --> |
| 77 | + ui/canvas::draw { / Draw }: Canvas // apply geometries to internal canvas structure |
| 78 | + --> |
| 79 | + ui/canvas::applyTo(canvas, node) // apply canvas to HTML node |
| 80 | + --> |
| 81 | + ... // repeat from reduction/layout step |
| 82 | + |
| 83 | +# test |
0 commit comments