More pedagogical documentation

[gabrielhdt]

In the wake of the new documentation provided by #241, it can be further improved by

• explaining what the load path is,
• what happens when --stdin is used and a file is given as positional argument
• document exit status

[fblanqui]

Some commands are not explained in README:

• #REQUIRE: is it mandatory?
• #NAME: is it still accepted?
• defac
• defacu: what does that mean to declare a symbol ACU?
• #GDT

[francoisthire]

Indeed, contribution are welcome but in short:

• #REQUIRE is not mandatory but in some cases it is necessary (a rule in a file which depends on another rule, declared in another file to type check for example)
• '#NAME' should not be accepted anymore
• defac is for an ac symbol
• defacu is for an acu symbol
• #GDT is to print the decision tree of a symmbol

I welcome contributions with pleasure, but I don't have time to tackle all of this seriously for the moment, unfortunately.

[fblanqui]

But what ACU implies? Does that mean that matching is modulo ACU?

[francoisthire]

I suspect that if the top symbol of a rule (the symbol rewritten) is declared as ac or acu then we have matching (or filtering?) which is done ac or acu. I am not certain since I do not know that part of the code. Some description can be found here: https://github.com/Deducteam/Dedukti/pull/203

[GuillaumeGen]

But what ACU implies? Does that mean that matching is modulo ACU?

More or less. I don't know what the exact definition of matching modulo ACU is, but the results of a small experiment tells us that one can match on the presence of the symbol, but not on the length of the list of its arguments (once flatenned), since matching modulo ACU allows to "invent" new application of the neutral element.

N : Type.

0 : N.
s : N -> N.

defacu plus [N, 0].

def f : N -> N.
[] f (plus _ _) --> 0.

#EVAL (f (s (s 0))).  (; This line prints `f (s (s 0))` ;)

def g : N -> N.
[] g (plus _ (plus _ _)) --> 0.

#EVAL (g (plus (s (s 0)) (s 0))). (; This line prints 0` ;)

If one wants to see the "invented 0", modifying the last lines of the example gives us:

def g : N -> N.
h : N -> N -> N -> N.
[x,y,z] g (plus x (plus y z)) --> h x y z.

#EVAL (g (plus (s (s 0)) (s 0))). (; This line prints `h (s (s 0)) (s 0) 0` ;)