Loge: egglog smoke test

root = Path.expand("..", __DIR__)

Mix.install([
  {:loge, path: Path.join(root, "loge"), override: true},
  {:loge_egglog, path: Path.join(root, "loge_egglog")},
  {:kino_loge, path: Path.join(root, "kino_loge")}
])

Running

Expected: completed, the extracted term (Add (Num 2) (Num 3)) or (Add (Num 3) (Num 2)).

Loge.run!(
  Loge.Egglog.Engines.Egglog,
  "(datatype Math (Num i64) (Add Math Math) (Mul Math Math))\n(rewrite (Add a b) (Add b a))\n(rewrite (Mul a (Num 1)) a)\n\n(let e (Add (Mul (Num 2) (Num 1)) (Num 3)))\n(run 5)\n(check (= e (Add (Num 3) (Num 2))))\n(extract e)\n",
  graph: false
)

With Show the e-graph on, the Result tab also draws the e-graph: each e-class a box of its e-nodes.

Loge.run!(
  Loge.Egglog.Engines.Egglog,
  "(datatype Math (Num i64) (Add Math Math) (Mul Math Math))\n(rewrite (Add a b) (Add b a))\n(rewrite (Mul a (Num 1)) a)\n\n(let e (Add (Mul (Num 2) (Num 1)) (Num 3)))\n(run 5)\n",
  graph: true
)

A failed check: expected check failed, egglog's message in the Output tab.

Loge.run!(
  Loge.Egglog.Engines.Egglog,
  "(datatype Math (Num i64) (Add Math Math) (Mul Math Math))\n(rewrite (Add a b) (Add b a))\n(rewrite (Mul a (Num 1)) a)\n\n(let e (Add (Mul (Num 2) (Num 1)) (Num 3)))\n(run 5)\n(check (= e (Num 5)))\n",
  graph: false
)

This run grows without bound. Expected: it runs until stopped; stopping the evaluation ends it.

Loge.run!(
  Loge.Egglog.Engines.Egglog,
  "(datatype E (Num i64) (Add E E))\n(rule ((= x (Add a b)) (= y (Add c d))) ((Add x y)))\n(let e (Add (Num 1) (Num 2)))\n(run 10)\n",
  graph: false
)

Linting

Expected: under the editor, a parse error at the extra ) on line 2.

Loge.run!(Loge.Egglog.Engines.Egglog, "(datatype M (Num i64))\n(let x (Num 1)))\n", graph: false)