Handmade Network»leddoo

Recent Activity

got a basic "info panel" working. it shows the local assumptions and the current goal (at the cursor).
as in my previous demo, the first example shows using the rw tactic to use theorems to rewrite the goal into the form x = x, which is trivally true.
the second example shows unfolding definitions (negation is defined as P -> False) and introducing assumptions.
sadly, i only had two days to work on the project this week (so i didn't really get to the "interactivity" i had hoped for). still it was a lot of fun and i learned a couple of things 👌 &kibi-pa

got some basic proof tactics with manual proof goal inspection working. &kibi-pa

some experimental source code / bytecode mapping visualizations.
the idea is to show which source level values are stored in which registers at each point in the program.
i wish it wasn't as confusing 😄
it could help to highlight one source value as the primary one. and maybe make showing aliases optional.

i made a "little" video about switching to an ssa based compiler.
(though most of the vid is not actually about ssa form)
thanks again @ratchetfreak and @NeGate for all your help!
https://youtu.be/kESmRMDHZZk
oh, btw, useful resources for implementing ssa form in the description!

wip text layout abstraction on top of DirectWrite

leddoo

making some educational videos about vector graphics. hoping to eventually cover how my renderer works. https://youtu.be/33KqDTwdR08

[vector renderer] implemented basic stroking (butt caps and bevel joins). performance dropped quite a bit, because the renderer is currently memory bound. (frame buffer doesn't fit into the cache. i'll implement tiling next to fix that.)

working on a vector renderer once again. performance is pretty good 🙂 rendered on one cpu core without any caching. but haven't implemented stroking yet.

here are some more examples in a hypothetical functional language:

  • the last bit is arguably unreadable. you could try to "refactor" that, but i think different code representations are necessary to make this kind of computation understandable. the simplest of which is to visualize the computation in a parallel view for a given example.
  • here, each is actually a function (map). the language pretty much only has functions and let bindings.
  • uniform abstract syntax is nice for language extension and other kinds of meta programming.
  • the key idea here is to have a surface syntax on top of the AST to make things prettier.

recently discovered an interesting lispy, operator, whitespace syntax:

  • it is designed as syntactic sugar on top of a simple, meta programming friendly ast.
  • precedence isn't 100% worked out. (mistake in separator example: should of course parse as ... [make-random-list 5] ...)

messing with custom layout to avoid CSS

New forum thread: note app - "submission"
leddoo
Forum reply: note app
leddoo
Forum reply: note app
leddoo
Forum reply: note app
leddoo
Forum reply: note app
leddoo
Forum reply: note app
leddoo
Forum reply: note app
leddoo
Forum reply: note app
leddoo
Forum reply: note app
leddoo
Forum reply: note app
leddoo
Forum reply: note app
leddoo
New forum thread: note app
leddoo
Forum reply: [jam] Math thingy
leddoo

The dependency system now supports nested content sized elements, which is pretty noice 👌

I have also been working on an imgui library. It's still super early days and many things will change (like passing a string to a label), but the basic idea is there!