lpcic / elpi Goto Github PK

From the API, but also internally if possible

As for elpi-checker and elpi2html one could rewrite the latex exported in elpi and process reified syntax rather than the AST.
As a result the elpi_API could be cleaned up.

What's the status of CIC kernel? It seems broken w.r.t. a test written for an older version which was forked shortly after Dalefest in December.

For instance, I see pts_cic accumulated in the alt_0/CIC kernel, but there is no such file in the repo. Minor thing since there are other CiC files in that folder.

But also, I get an error:

Fatal error: Variable can only be introspected (eg ?? X L) in the guard

...when running my test after accumulating:

loading pervasives-syntax.elpi
loading pervasives.elpi
loading kernel_v2.elpi
loading logic.mod
loading list.mod
loading elpi/bench/sources/cic/alt_0/pts_cic_floating.mod
loading elpi/bench/sources/cic/alt_0/refiner_pts.mod
loading elpi/bench/sources/cic/alt_0/kernel_pts.mod
loading elpi/bench/sources/cic/alt_0/kernel_case.mod
loading elpi/bench/sources/cic/alt_0/kernel_inductives.mod
loading elpi/bench/sources/cic/alt_0/kernel_global.mod
loading testttt.mod

Trying to debug but right now it's a guessing game. Thanks in advance.

The test in

B.txt

does not pass. Expected behaviour: it should pass and it should pass by expanding the O = t and OUT = t as well. I suspect a bug in unification.

Context

When working at the ppx to synthesize the glue code, it felt natural to link a "context" data type to the one of a data type with binders. Eg

type ctx = Decl of string * ty
type t = Lam of string * ty * (t [@binder (fun s ty -> Decl(s,ty))])

In this way the APIs can read back not only a term but also the context of binders under which it occurs. This requires the user to
systematically add a decl clause when moving under a binder, that is p (lam S TY F) :- pi x\ decl x S TY => ..F x...

Wish

This piece of info (the link between Lam's arguments and Decl) would also be useful in the implementation of spilling, which turns out to be very useful in Coq-Elpi and Hierarchy Builder.
For example:

some-pred T R :- typecheck T TY, some-more TY R.
main :- T = lam "x" bool x\ {some-pred x}.

The code after spilling should look like

main :- (pi x\ decl x "x" bool => some-pred x (Spill1 x)), T = lam "x" bool x\ (Spill1 x).

so that some-pred can call typecheck correctly (which requires the context entry decl x ... to be present).

Mock up

The proposal (up to syntax) would be to equip a type declaration with the piece of info that is attached to the ML code above, eg

type lam string -> ty -> (term --(s\t\x\ decl x s t)--> term) -> term.

Alternative & discussion

A "cheap" but also not 100% satisfactory alternative proposed by Dale was to have one special term constructor called binder.
In this way the ADT for terms would be

type decl string -> ty -> t -> prop.

type app t -> t -> t.
type binder (t -> prop) -> (t -> t) -> t.

then lam "x" bool x\ .. would be represented as binder (decl "x" bool) x\ ... and the idiom to cross it would be
p (binder B F) :- pi x\ B x => .. F x. In this setting the spilling problem is solved, since when one spills across binder he can just collect its first argument in order to build the context for the spilled computation.

I'm not in love with this because there is a little encoding step that is visible. Eg. in Coq we have 4+ binders (fun, prod, let and fix) and all but let create the same context entry so one would need to pass to binder some extra info, like "lam", and then you really start to see the encoding. Still this proposal clarifies very well what I'd like, it's just that I'd like the encoding to be performed behind the scenes. Also, then .. --(..)--> .. function space constructor can be used by a linter/checker to tell the user "hey, you forgot to use => after pi (if F has type .. --(C)--> .. then F x needs x to be used in a context where C x => is there.

CC @CohenCyril

Duplicate of #81

since js_of_ocaml does not know it

apparently f (uvar X) => ... does not match uvar.

Elpi 1.11.0 builds on windows using Coq's scripts:
https://github.com/coq/coq/tree/master/dev/build/windows
coq/coq#12032

It would be nice to build the standalone elpi.exe in CI and make it a release asset.

If one writes term list instead of list term the type checker should immediately bail out and complain. As of today it gives, later, errors like "..got term list but expected list term.." that to the eyes of an OCaml programmer just make no sense (since type application in OCaml is the other way around).

X = [2|_] should result in X = [2|Y]

While binding ML (efficient) data structures such as Set and Map I imposed the limitation that keys/elements had to be closed terms (no unif variables and no eigenvariables bound in the program).
In this way the data is easy to move around.
In coq-elpi all tactics are run in the proof context, and proof variables are represented as bound variables (immediately introduced via a pi), hence these ML data structure are not easily usable.

If cdata (eg ML sets/maps) could be annotated (internally) with the depth at which their creation takes place, we could allow to store in there terms with upto-depth program-bound variables and be sound when the cdata is assigned to a unification variable (eg we could fail, today cdata is moreally of depth 0). In a sense {x y z} |> ocaml.map.empty X should assign to X something like (cdata,[x,y,z]) so that we know that to hold that cdata you have to see x, y and z. This would let the user take advantage of ML data structures while writing tactics (eg the 101 example, reification, could use a ML Map rather than a Prolog List to represent the reification environment, and be nlog(n) (with little constants) rather than nn (with the overhead of interpreting the membership test)).

I think we should write the parser using standard technology, say menhir.
Then define and document a handful of infix operators, taken from the examples we found online.
Eventually support families of infixes, eg &&, &!&, &^&, &...& with the same precedence of &&.

Remove infix and co.

We installed version 1.4.0 using Opam 2.0.4 (with Ocaml 4.07.0).
Next, we tried #require "elpi" in order to experiment with how it works.
But this fails with "Error: Reference to undefined global `Grammar'"
Any help in getting this going would be appreciated!

In addition -- are there any simple examples as how this can be used as a prolog interpreter?

The operator mod is defined in Elpi, but its type declaration is missing:

type mod int -> int -> int.

Arguably, this can occur to other operators, too.

It would be convenient to provide a --version command-line flag that says which version of Elpi is running. I couldn't find it.

Allow the user to specify on which argument(s) do the indexing of a clause.

Readings:
https://www.researchgate.net/publication/220987061_A_Simple_Scheme_for_Implementing_Tabled_Logic_Programming_Systems_Based_on_Dynamic_Reordering_of_Alternatives/references
https://www.researchgate.net/publication/2862749_Implementation_of_a_Linear_Tabling_Mechanism
https://www.researchgate.net/publication/338569511_Tabled_Typeclass_Resolution
https://www.researchgate.net/publication/50520354_Beyond_depth-first_strategies_improving_tabled_logic_programs_through_alternative_scheduling
https://www.cs.mcgill.ca/~bpientka/papers/eftab-long.pdf

Like in ProbLog

See their GitHub repository

0.3::stress(X) :- person(X).
0.2::influences(X,Y) :- person(X), person(Y).

smokes(X) :- stress(X).
smokes(X) :- friend(X,Y), influences(Y,X), smokes(Y).

0.4::asthma(X) :- smokes(X).

person(angelika).
person(joris).
person(jonas).
person(dimitar).

friend(joris,jonas).
friend(joris,angelika).
friend(joris,dimitar).
friend(angelika,jonas).

It is so common to write

foo X :- !, bla.

or even

foo X :- !.

especially in hypothetical clauses that a dedicated syntax is desirable.

Getting this report after running make:

`Makefile:128: .depends: No such file or directory
Makefile:128: .depends.parser: No such file or directory
OCAMLDEP .depends.parser
OCAMLDEP .depends
OCAMLOPT elpi_util.cmi -c
OCAMLOPT elpi_util.cmx -c
OCAMLOPT elpi_ast.cmi -c
OCAMLOPT elpi_ast.cmx -c
OCAMLOPT elpi_trace.cmi -c
OCAMLOPT elpi_trace.cmx -c
OCAMLOPT elpi_parser.cmi -c
OCAMLOPT elpi_parser.cmx -c -pp camlp5o
OCAMLOPT elpi_ptmap.cmi -c
OCAMLOPT elpi_ptmap.cmx -c
OCAMLOPT elpi_data.cmx -c
OCAMLOPT elpi_compiler.cmi -c
OCAMLOPT elpi_runtime.cmi -c
OCAMLOPT elpi_runtime_trace_on.cmx -c -ppx 'trace_ppx -on' -for-pack
Failure("Ast_mapper: OCaml version mismatch or malformed input")
File "elpi_runtime.ml", line 1:
Error: Error while running external preprocessor
Command line: ./trace_ppx -on '/var/folders/df/kqdm_fnn70lbsz3jhptnq25h0000gn/T/camlppx3e9239' '/var/folders/df/kqdm_fnn70lbsz3jhptnq25h0000gn/T/camlppxa42828'

make: *** [elpi_runtime_trace_on.cmx] Error 2`

Double checked Ocaml version, and have reinstalled ppx packages. On OSX Darwin.

It would be nice to have a user manual built/published by CI.
Possibly it should contain code snippets and the output of elpi running them.

At some point, I guess when lists became primitive, nil became not equal to [].
The parser could take care of this, at least for compatibility with teyjus

I get this exception when an Elpi_ast.Lam term is at the head of an application. Why is this disallowed? In the test file llam.elpi there seems to be plenty of examples of lambda expression as head. What is the magic there?

Right now they are user space predicates.
Apart from performances, the user can change their semantics... that is not very sensible.

It is of general interest, now it is in coq-lib.elpi

goal> (pi F \ simpl (x \ F x) F) => simpl (x \ a x) a.
goal> a = x \ a x.

both fail, but

1. they should succeed when a has function type
2. fail otherwise

The implementation of ELPI is untyped, thus ELPI does not work up to eta.
This should be documented and compared to the behaviour of Teyjus, if they differ.

Context

When working at the ppx to synthesize the glue code, it felt natural to link a "context" data type to the one of a data type with binders. Eg

type ctx = Decl of string * ty
type t = Lam of string * ty * (t [@binder (fun s ty -> Decl(s,ty))])

In this way the APIs can read back not only a term but also the context of binders under which it occurs. This requires the user to
systematically add a decl clause when moving under a binder, that is p (lam S TY F) :- pi x\ decl x S TY => ..F x...

Wish

This piece of info (the link between Lam's arguments and Decl) would also be useful in the implementation of spilling, which turns out to be very useful in Coq-Elpi and Hierarchy Builder.
For example:

some-pred T R :- typecheck T TY, some-more TY R.
main :- T = lam "x" bool x\ {some-pred x}.

The code after spilling should look like

main :- (pi x\ decl x "x" bool => some-pred x (Spill1 x)), T = lam "x" bool x\ (Spill1 x).

so that some-pred can call typecheck correctly (which requires the context entry decl x ... to be present).

Mock up

The proposal (up to syntax) would be to equip a type declaration with the piece of info that is attached to the ML code above, eg

type lam string -> ty -> (term --(s\t\x\ decl x s t)--> term) -> term.

Alternative & discussion

A "cheap" but also not 100% satisfactory alternative proposed by Dale was to have one special term constructor called binder.
In this way the ADT for terms would be

type decl string -> ty -> t -> prop.

type app t -> t -> t.
type binder (t -> prop) -> (t -> t) -> t.

then lam "x" bool x\ .. would be represented as binder (decl "x" bool) x\ ... and the idiom to cross it would be
p (binder B F) :- pi x\ B x => .. F x. In this setting the spilling problem is solved, since when one spills across binder he can just collect its first argument in order to build the context for the spilled computation.

I'm not in love with this because there is a little encoding step that is visible. Eg. in Coq we have 4+ binders (fun, prod, let and fix) and all but let create the same context entry so one would need to pass to binder some extra info, like "lam", and then you really start to see the encoding. Still this proposal clarifies very well what I'd like, it's just that I'd like the encoding to be performed behind the scenes. Also, then .. --(..)--> .. function space constructor can be used by a linter/checker to tell the user "hey, you forgot to use => after pi (if F has type .. --(C)--> .. then F x needs x to be used in a context where C x => is there.

CC @CohenCyril

This would avoid all other conversions to deal with the context directly. Unclear of it is feasible.

The Elpi_API gives an option to print which files are loaded by Elpi when initializing it :

Elpi_API.Setup.init ~silent:false [] ""

But the resulting output is done on stderr when in my opinion it should be on stdout because these are infos, not errors.

That may be a matter of taste, but in case you agree with it I reference my first contribution to this great project: a massive pull request shortening the Elpi codebase by 1 character. #16

Dear elpi developers,

the use of low-level filesystems features makes ELPI not very portable for instance in jsCoq. I am attaching the patch used to make elpi work in jsCoq, but more changes to the code are needed (I'd suggest simplifying the whole file search logic)

diff --git a/elpi_parser.ml b/elpi_parser.ml
index a23dcce..35668b7 100644
--- a/elpi_parser.ml
+++ b/elpi_parser.ml
@@ -13,7 +13,7 @@ let set_precedence,precedence_of =
  (fun c -> ConstMap.find c !precs)
 ;;
 
-let cur_dirname = ref (Unix.getcwd ())
+let cur_dirname = ref "./"
 let last_loc : Ploc.t ref = ref (Ploc.make_loc "dummy" 1 0 (0, 0) "")
 let set_fname ?(line=1) fname = last_loc := (Ploc.make_loc fname line 0 (0, 0) "")
 
@@ -24,7 +24,7 @@ let rec readsymlinks f =
     else readsymlinks Filename.(concat (dirname f) link)
   with Unix.Unix_error _ -> f
 
-let symlink_dirname f = Filename.dirname (readsymlinks f)
+let symlink_dirname f = f (* Filename.dirname (readsymlinks f) *)
 
 let make_absolute filename =
   if not (Filename.is_relative filename) then filename
@@ -33,14 +33,15 @@ let make_absolute filename =
 let cur_tjpath = ref []
 
 let set_tjpath paths =
- let tjpath = try Sys.getenv "TJPATH" with Not_found -> "" in
- let tjpath = Str.split (Str.regexp ":") tjpath in
- let execname =
-   try Unix.readlink "/proc/self/exe" (* no such a thing on osx *)
-   with Unix.Unix_error _ -> "./elpi" in
- let tjpath = paths @ tjpath @ [ Filename.dirname execname ] in
- let tjpath = List.map (fun f -> make_absolute (readsymlinks f)) tjpath in
- cur_tjpath := tjpath
+ (* let tjpath = try Sys.getenv "TJPATH" with Not_found -> "" in *)
+ (* let tjpath = Str.split (Str.regexp ":") tjpath in *)
+ (* let execname = *)
+ (*   try Unix.readlink "/proc/self/exe" (\* no such a thing on osx *\) *)
+ (*   with Unix.Unix_error _ -> "./elpi" in *)
+ (* let tjpath = paths @ tjpath @ [ Filename.dirname execname ] in *)
+ (* let tjpath = List.map (fun f -> make_absolute (readsymlinks f)) tjpath in *)
+ (* cur_tjpath := tjpath *)
+ cur_tjpath := ["./"; "./elpi/"; "../elpi/"]
 
 module PointerFunc = struct
  type latex_export =
@@ -89,10 +90,10 @@ let rec parse_one e parsed (origfilename as filename) =
   in
    iter_tjpath (!cur_dirname :: !cur_tjpath)
  in
- let inode = (Unix.stat filename).Unix.st_ino in
- if List.mem_assoc inode !parsed then begin
+ (* let inode = (Unix.stat filename).Unix.st_ino in *)
+ if List.mem_assoc filename !parsed then begin
   if not !parse_silent then Printf.eprintf "already loaded %s\n%!" origfilename;
-  match !(List.assoc inode !parsed) with
+  match !(List.assoc filename !parsed) with
   | None -> []
   | Some l -> l
  end else begin
@@ -106,7 +107,7 @@ let rec parse_one e parsed (origfilename as filename) =
     else [] in
   if not !parse_silent then Printf.eprintf "loading %s\n%!" origfilename;
   let ast = ref None in
-  parsed := (inode,ast) ::!parsed ;
+  parsed := (filename,ast) ::!parsed ;
   let ch = open_in filename in
   let saved_cur_dirname = !cur_dirname in
   cur_dirname := symlink_dirname filename;

It would be nice to have a user manual built/published by CI.
Possibly it should contain code snippets and the output of elpi running them.

this is blocking for 1.11

This is quite verbose

mode (foo i o).
type foo ty -> toe -> prop.
foo X Y :- ...

One could imagine a single declaration for both the type and the mode. The following one is
not so compact but enable a kind of optimization the current mode syntax does not allow

def foo (X : ty/i) (Y : toe/o) :- orig X Y.
def bar (X : toe/i) (Y : ty/o) :- orig Y X.

Today we have this. Note that the code generated for bar has the input in the second argument,
so indexing is inefficient, while the syntax above could suggest how the code of orig can be turned into
an efficient implementation of bar.

mode (orig i o) xas foo, (orig o i) xas bar.

What I don't like of the proposal is that the types are repeated.

Does not use the right symbol map, so it prints SYMBOL-XX rather than the real name of the symbol

Right now trailing garbage is not detected

currently constraint preds { ... } forces all declarations of rules to share the same "clique" of predicates, which is not compositional.

tentative design

% declaration of a constraint foo in a context of foo bar
% if not present the context is [ foo], [] means empty, * means all
constraint [ foo, bar ] ?- foo.

% declare a set of rules, the "clique" is inferred looking at the heads
constraint { rules }. 

Since 1.11.0 the trace can be output in json format.
It would be nice to have a GUI to browse it

I've been trying to experiment with constraint handling rules with ELPI, and as far as I can tell the CHR behaviour does not match that of SWI. Specifically the SWI CHR manual (https://www.swi-prolog.org/pldoc/man?section=SyntaxAndSemantics) states:

The other way it may interact again with the rules is when a variable appearing in the constraint becomes bound to either a non-variable or another variable involved in one or more constraints. In that case the constraint is triggered, i.e. it becomes an active constraint and all the rules are tried.

Example

To demonstrate the behaviour I have written a small application in SWI and ELPI.

Correct Behaviour (SWI)

Program:

:- module(simple, [tr/2]).
:- use_module(library(chr)).
:- chr_constraint tr/2.

tr1 @ tr(X,0) <=> X = 0.

Running swipl simple.pl <<< "tr(X, Y), tr(Y, 0).":
Output:

X = Y, Y = 0.

Execution: SWI starts with tr(X,Y) and tries to match it with any rule. As this doesn't happen, tr(X,Y) is suspended and SWI considers the next rule tr(Y,0) as active. This second rule matches the tr1 rule, and updates Y=0. As the variable Y is used by tr(X,Y), this rule becomes active again and tries to match tr(X,0) which matches tr1, setting X=0.

Incorrect Behaviour (ELPI)

Program:

mode (tr i i).
tr X Y :- declare_constraint (tr X Y) [].
constraint tr {
  rule \ (tr X 0) <=> (X = 0).
}

Running elpi simple.elpi <<< "tr X Y, tr Y 0.":
Output:

Success:
  X = X0
  Y = 0

Constraints:
 tr X0 0  /* suspended on  */

Execution: ELPI similarly starts with the rule tr X Y, which does not match any rules, suspending it. It next tries the rule tr Y 0, which matches the equivalent of tr1, setting Y=0. The tr X0 0 rule is left suspended, even though it could be matched with tr1, eliminating it and setting X=0.

Comment

I'm not sure if I've misunderstood Elpi in some form or another. I have also noticed there is a small bug in the GCD example, where the line

gcd A (uvar as Group) :- declare_constraint (gcd A Group) Group.

should be:

gcd A (uvar as Group) :- declare_constraint (gcd A Group) [Group].

With (cache enabled) in my ~/.config/dune/config I got

#=== ERROR while compiling elpi.1.11.0 ========================================#
# context     2.0.5 | linux/x86_64 | ocaml-base-compiler.4.07.1 | https://opam.ocaml.org#bc6d04e5
# path        ~/.opam/4.07.1/.opam-switch/build/elpi.1.11.0
# command     ~/.opam/opam-init/hooks/sandbox.sh build make fix-elpi.install
# exit-code   2
# env-file    ~/.opam/log/elpi-109268-97bbf8.env
# output-file ~/.opam/log/elpi-109268-97bbf8.out
### output ###
# dune exec ./fix_elpi_install.exe -- elpi.install
# Error: Error: utimes: /home/gaetan/.cache/dune/db/v2/beacon: Read-only file
# system
# make: *** [Makefile:36: fix-elpi.install] Error 1

Disabling the cache allowed opam install elpi to succeed.

Should be much more clear from the user perspective, since the lvl is an optimization of the runtime but has no actual meaning

elpi should detect statically that

constrinat a c d {

  rule (b X).

}

is wrong since the head of the rule b is not in the constraint clique { a, c, d } hence the rule is never applied.

Consider a file file1.elpi that defines a macro:

macro @a :- tt.
pred test1 o:bool.
test1 @a.

The scope of the macro do not extend beyond file1.elpi as it can be seen in this example file2.elpi:

accumulate file1.
pred test2 o:bool.
test2 @a.

goal> test2 A.
Fatal error: file2.elpi, characters 38-47, line 4, column 4: Undeclared macro @a

However, if one try to redefine the macro in another file, Elpi report it as a duplicate declaration. E.g., file3.elpi:

accumulate file1.
macro @a :- tt.
pred test3 o:bool.
test3 @a.

goal> test3 A.
Fatal error: file1.elpi, characters 0-15, line 1, column 10: Macro @a declared twice:
first declaration: file3.elpi, characters 19-34, line 3, column 10
second declaration: file1.elpi, characters 0-15, line 1, column 10

After e039ca6 elpi accumulates files twice, if requested.
It should behave as before, don't do it. But instead of being done in the parser it should be done later by the compiler when namespaces are taken into account, since accumulating the same files twice, but in different namespaces is OK.

plece -> place
in in -> in
Some other -> Some others
are are -> are

@CohenCyril