Data bases

Shows how Elpi programs can store data and reuse it across multiple runs. Data bases are accumulated by name, hence can be shared among multiple commands or across successive executions of the same command.

Let's start with a db containing international phone prefixes:

From elpi Require Import elpi.
[Loading ML file ppx_deriving.runtime (implicit dependency) ... done]
[Loading ML file re (implicit dependency) ... done]
[Loading ML file re.str (implicit dependency) ... done]
[Loading ML file elpi.util (implicit dependency) ... done]
[Loading ML file elpi.lexer_config (implicit dependency) ... done]
[Loading ML file menhirLib (implicit dependency) ... done]
[Loading ML file stdlib-shims (implicit dependency) ... done]
[Loading ML file elpi.parser (implicit dependency) ... done]
[Loading ML file camlp-streams (implicit dependency) ... done]
[Loading ML file easy-format (implicit dependency) ... done]
[Loading ML file biniou (implicit dependency) ... done]
[Loading ML file yojson (implicit dependency) ... done]
[Loading ML file atdgen-runtime (implicit dependency) ... done]
[Loading ML file elpi.trace.atd (implicit dependency) ... done]
[Loading ML file elpi.trace.runtime (implicit dependency) ... done]
[Loading ML file elpi.runtime (implicit dependency) ... done]
[Loading ML file elpi.compiler (implicit dependency) ... done]
[Loading ML file elpi (implicit dependency) ... done]
[Loading ML file rocq-elpi.elpi ... done]



Elpi Db phonebook.db lp:{{
  pred phone_prefix -> string, int.
  phone_prefix "USA" 1.
}}.
Elpi Command print_db.
Elpi Accumulate Db phonebook.db.
Elpi Accumulate lp:{{
  main [] :- std.findall (phone_prefix S_ N_) L, !, coq.say "The Db contains" L.
  main [str S] :- coq.say "Phone prefix for" S "is" {phone_prefix S}, !.
  main [str S] :- coq.error "No prefix for" S.
}}.
Elpi print_db.
The Db contains [phone_prefix USA 1]

Elpi print_db USA.
Phone prefix for USA is 1

Fail Elpi print_db Italy.
The command has indeed failed with message:
No prefix for Italy

Elpi Command add_db.
Elpi Accumulate Db phonebook.db.
Elpi Accumulate lp:{{
  main [str S, int N] :-
    coq.elpi.accumulate _ "phonebook.db" (clause _ _ (phone_prefix S N)).
}}.
Elpi add_db France 33.
Elpi add_db Italy 39.
Elpi print_db.
The Db contains 
[phone_prefix USA 1, phone_prefix France 33, phone_prefix Italy 39]

Elpi print_db France.
Phone prefix for France is 33

Data bases don't need to be that simple, they can contain arbitrary clauses, in particular conditional ones:

Elpi Db food.db lp:{{

  pred sweet -> string.
  sweet "apricot".

  pred tasty -> string.
  tasty "salmon".

}}.
Elpi Command add_recipy.
Elpi Accumulate Db food.db.
Elpi Accumulate lp:{{
  pred test-sweetness argument -> (pred).
  test-sweetness (str X) (sweet X).

  pred test-tastiness argument -> (pred).
  test-tastiness (str X) (tasty X).

  main [str Name|Ingredients] :-
    std.map Ingredients test-sweetness SweetConditions,
    % trick: ":-" accepts a list of propositions on the RHS
    coq.elpi.accumulate _ "food.db" (clause _ _ (sweet Name :- SweetConditions)),

    std.map Ingredients test-tastiness TastyConditions,
    std.forall TastyConditions (i\
      coq.elpi.accumulate _ "food.db" (clause _ _ (tasty Name :- i))).
}}.
Elpi Command is_sweet.
Elpi Accumulate Db food.db.
Elpi Accumulate lp:{{
  main [str Name] :- if (sweet Name) (coq.say "sweet!") (coq.say "brr").
}}.
Elpi Command is_tasty.
Elpi Accumulate Db food.db.
Elpi Accumulate lp:{{
  main [str Name] :- if (tasty Name) (coq.say "yummy!") (coq.say "bohf").
}}.
Elpi add_recipy "pie"   "potato" "salmon".
Elpi add_recipy "jam"   "apricot".
Elpi add_recipy "tart"  "jam".
Elpi is_sweet "tart".
sweet!

Elpi is_sweet "pie".
brr

Elpi is_tasty "pie".
yummy!