minimips assembler/disassembler running in the browser!

[David Kahn]

minimips (https://github.com/orchid-hybrid/minimips) the relational MIPS assembler and disassembler written in miniKanren now works in the browser on top of veneer!

Try it here:

http://tca.github.io/veneer/examples/editor.html

The main change that was needed was delayed goals which I implemented using a co-routine that walks a structure, pausing any time it hits an un-ground variable. 

https://github.com/tca/veneer/blob/master/mk.js#L148

On a side note, with a small tweak it can also do the two watched literal scheme SAT solvers use for unit propagation. Could this be applied somewhere in miniKanren?

[William Byrd]

Hi David!

This is really awesome! :)

I'm curious: what do the _.n reified logic variables mean in the
output? Are these unknown label names, or other identifiers?

q: ((addi 29 29 65528) (sw 16 4 (29)) (sw 31 0 (29)) (bne 4 0 _.0)
(addi 2 5 1) (j _.1) (bne 5 0 _.2) (addi 4 4 65535) (addi 5 0 1) (jal
_.3) (j _.4) (add 16 4 0) (addi 5 5 65535) (jal _.5) (addi 4 16 65535)
(add 5 2 0) (jal _.6) (j _.7) (lw 16 4 (29)) (lw 31 0 (29)) (addi 29
29 8) (jr 31))

> --
> You received this message because you are subscribed to the Google Groups
> "minikanren" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to minikanren+...@googlegroups.com.
> To post to this group, send email to minik...@googlegroups.com.
> Visit this group at https://groups.google.com/group/minikanren.
> For more options, visit https://groups.google.com/d/optout.

[William Byrd]

> The main change that was needed was delayed goals which I implemented using
> a co-routine that walks a structure, pausing any time it hits an un-ground
> variable.
> https://github.com/tca/veneer/blob/master/mk.js#L148

Delayed goals are useful in general. For example, for adding
arithmetic over floating point numbers (with the understanding that
the program errors out if the numbers never become sufficiently ground
to perform the arithmetic operations). Is there an interface to the
delayed goals I could use to add (for example) delayed addition and
multiplication over the floating point numbers?

> On a side note, with a small tweak it can also do the two watched literal
> scheme SAT solvers use for unit propagation. Could this be applied somewhere
> in miniKanren?

Good question!

I've wanted to explore calling to a SAT solver (or other solvers) from
within miniKanren for a while. Do you think a simple SAT solver slong
the lines of MiniSAT could be implemented with this approach?

Are there any decent SAT solvers in JavaScript, BTW? Or finite domain
or SMT solvers in JavaScript? I wonder if calling out to an external
solver may be relatively simple in Veneer.

[David Kahn]

>Are these unknown label names, or other identifiers?

Yes that's what they are, could probably be more done about that.

[David Kahn]

> I've wanted to explore calling to a SAT solver (or other solvers) from 
> within miniKanren for a while.  Do you think a simple SAT solver slong 
> the lines of MiniSAT could be implemented with this approach? 

It's close to the original one that was made for minimips here: https://github.com/orchid-hybrid/microKanren-sagittarius/blob/master/miruKanren/eqeq-watch.scm

for example:

(fresh (x y)
  (watch x (lambda (x1) (watch y (lambda (y1) (== q (* x1 y1))))))
  (== x 5)
  (== y 5))

> I've wanted to explore calling to a SAT solver (or other solvers) from 
> within miniKanren for a while.  Do you think a simple SAT solver slong 
> the lines of MiniSAT could be implemented with this approach? 

I think it's to inefficient to do anything as involved as that, but may still be useful in triggering finite domain constraints or something.