Asking about your code from the command line

WHAT.md asked its question in a notebook, in sentences. The same question can be asked from a shell, by you or by an agent, with the rofl command: one question in, one answer out, --json when a program is reading. The facts are the same, so the answer is the same. What changes is the language: the command line speaks Datalog, the notebook's sentences with the words taken out. rofl-nb vocab lists both forms side by side, the Datalog name in parentheses after each sentence:

$ rofl-nb vocab throw | head -4
controlflow: a call is an exit
  a function F always throws   (always_throws)
  a call C is a throwing call   (throwing_call)
  a function F throws at the top   (top_throw)

a function F may throw is may_throw(F). The shop of WHAT.md, guide/examples/first, serves here too.

A world file

The command line reads a world: a file of facts and rules. This one names the code to scan and defines the question:

-- The shop, for the command line. The scanner reads checkout.js and every file it imports.
scanner(js, "rofl scan .").
scan_request(js, "checkout.js").
scan_request(js, F) :- depends[code](_, F).

-- an exported function that may throw at its caller
risky(N) :- fn_name[code](F, N), exported_fn[code](F), may_throw[code](F).

It begins with where the facts come from. scanner names the command that turns a JavaScript file into facts, rofl scan, run in this directory. scan_request asks for checkout.js, and then for every file a scanned file depends on, so pay.js is scanned because checkout.js imports it, and a file nothing imports is never read. The last line is the rule from WHAT.md in Datalog: [code] after a name says which book the facts are in, the one the JavaScript model writes to.

Ask

$ rofl ask 'risky(N)' @rules/js.files shop.rofl
N = "charge"
N = "checkout"

One row a line, the variable and its value. @rules/js.files is the JavaScript model, the twenty-odd rule files that say what may_throw means; the rofl command finds them in its own package, so the line works from any directory. The world is the model plus shop.rofl, and shop.rofl fetches the code.

For a program, --json prints the same answer as one object a line:

$ rofl ask 'risky(N)' --json @rules/js.files shop.rofl
{"keys":["risky[main](\"checkout\")","risky[main](\"charge\")"],"ok":true,"partial":false,"rows":[["\"checkout\""],["\"charge\""]],"shrugs":[],"vars":["N"]}

partial is false: every row that follows from the facts is there. It is true, and the exit code 5, when the evaluation was cut short by a budget or a scan failed; then the rows may be short of an answer, and the output says so rather than passing a short list off as the whole one.

Why

$ rofl why 'risky("checkout")' @rules/js.files shop.rofl | head -23
risky[main]("checkout")  <= re667b5bf @tick 0
  fn_name[code](n017f49dbfbe9e0a8_fa4unkv52g4,"checkout")  <= r4664ba89 @tick 0
    ast_node[code](n017f49dbfbe9e0a8_fa4unkv52g4,function_declaration,"checkout.js") [axiom]
    ast_child[code](n017f49dbfbe9e0a8_fa4unkv52g4,id,0,n017f49dbfbe9e0a8_pi9h9ptud43) [axiom]
    ast_name[code](n017f49dbfbe9e0a8_pi9h9ptud43,"checkout")  <= r4a879967 @tick 0
      ast_attr[code](n017f49dbfbe9e0a8_pi9h9ptud43,name,"checkout") [axiom]
  exported_fn[code](n017f49dbfbe9e0a8_fa4unkv52g4)  <= r0df9c422 @tick 0
    fn_node[code](n017f49dbfbe9e0a8_fa4unkv52g4)  <= re519a619 @tick 0
      fn_kind[main](function_declaration) [axiom]
      ast_node[code](n017f49dbfbe9e0a8_fa4unkv52g4,function_declaration,"checkout.js") [axiom]
    not in_fn[code](n017f49dbfbe9e0a8_fa4unkv52g4) [finite failure]
      whynot in_fn[code](n017f49dbfbe9e0a8_fa4unkv52g4):
        rule r61bef758: in_fn[code](?N)@now :- nearest_v[flow](?_$0,?N)@now
          failed premise: nearest_v[flow](?_$0#0,n017f49dbfbe9e0a8_fa4unkv52g4)
    ast_within[code](n017f49dbfbe9e0a8_9l7lmkrrho2,n017f49dbfbe9e0a8_fa4unkv52g4)  <= rd361b6b6 @tick 0
      ast_in[code](n017f49dbfbe9e0a8_9l7lmkrrho2,n017f49dbfbe9e0a8_fa4unkv52g4)  <= r9e3f8aba @tick 0
        ast_child[code](n017f49dbfbe9e0a8_9l7lmkrrho2,declaration,0,n017f49dbfbe9e0a8_fa4unkv52g4) [axiom]
    ast_node[code](n017f49dbfbe9e0a8_9l7lmkrrho2,export_named_declaration,"checkout.js") [axiom]
    export_kind[main](export_named_declaration) [axiom]
  may_throw[code](n017f49dbfbe9e0a8_fa4unkv52g4)  <= rbef6bec0 @tick 0
    may_throw[code](na31b9c7ff583580b_v300rg8uh91)  <= r8e0a1ee0 @tick 0
      throws_outright[code](na31b9c7ff583580b_v300rg8uh91)  <= rd720c658 @tick 0
        ast_node[code](na31b9c7ff583580b_o5a7dfnm0m1,throw_statement,"pay.js") [axiom]

The same proof as the notebook's, in the engine's own form. Each line is a fact; <= re667b5bf @tick 0 names the rule that derived it; the lines indented under it are the facts that rule used; [axiom] is a fact that was given, by the scanner or by a rule file, and nothing is under an axiom. A node of the code is its id, not a name: n017f49dbfbe9e0a8_fa4unkv52g4 is the function checkout, and the fn_name line right under it is what ties the two together. The whole proof runs to some 150 lines. The notebook's sentence form, with [function checkout() at checkout.js:4] where the id is, is the one to read; the command line's is the one to parse.

Why not

$ rofl whynot 'risky("safeCheckout")' --depth 1 @rules/js.files shop.rofl
whynot risky[main]("safeCheckout"):
  rule re667b5bf: risky[main](?N)@now :- fn_name[code](?F,?N)@now, exported_fn[code](?F)@now, may_throw[code](?F)@now
    failed premise: may_throw[code](n017f49dbfbe9e0a8_gjdh70j2637)

The one rule that could conclude risky("safeCheckout"), and the premise that fails: may_throw of the node that is safeCheckout. --depth 2 goes one rule further and names, among the ways may_throw could have held, the one that was blocked: not caught_here(C) fails because caught_here(C) holds, the call to checkout being inside a try. Each level down multiplies the lines; --depth N and --nodes N bound the walk.

What it could not see

The notebook prints a note about ./log.js before anything else. On the command line the gap is a relation like any other, and you ask for it:

$ rofl ask 'unresolved_relative[code](F,L,S)' @rules/js.files shop.rofl
F = "checkout.js", L = 2, S = "./log.js"

A relative import that names no file of the code, with its file and line. An agent that asks a question about code should ask this one too: an answer over a world with an unresolved import holds only as far as the model sees.

The second question costs nothing

The first rofl ask over the shop scanned two files, evaluated the model and answered in about a second. It also kept the world it built, under ~/.cache/rofl/worlds, named by its files and the engine. The second question over the same files, this one or another, is answered from the kept world without evaluating: 0.03 s on the same machine. Change the <= in pay.js to < and ask again: the run scans that one file again, takes the change by delta instead of starting over, and says so on stderr:

the kept world took 1 file by delta: pay.js (scanned again) (1 facts out, 4 overdeleted or derived again; opened and taken in 285 ms, kept again in 0 ms, 220396 bytes written over the world it was kept from)

Nothing to turn on. The cache holds at most ROFL_CACHE_GB gigabytes (50 by default) and drops the least recently used world first. A world too large for it is answered and not kept, said on stderr; a world that grows past the cap while evaluating stops there, answers what it has as partial (exit 5), and goes on from where it stopped when asked under a larger cap.

Exit codes

A refusal wins over a partial answer: a run with a refused question exits 4 whatever else happened.

The rest

rofl excise F answers what changes without the given fact F: the rows that go and the rows that come. rofl load --ask L --why L --whynot L --excise F asks several questions in one evaluation, the answers in that order with a blank line after each. --kept F keeps the world at a path of your own, under a stricter rule: computed once, asked any number of times, refused rather than recomputed once a file it was built from changes. Every flag, the JSON shapes, rofl serve for a long-running process and rofl render for the sentence form are in docs/cli.md.

Next: QUICKSTART.md for the notebook, and CONCEPTS.md for the sentence form it speaks.