deducteam / dedukti Goto Github PK

Dedukti fails when two rewrite rules associated with the same definable symbol are of different arity. Is this restriction legit?

The function solve in module matching introduces domain free lambdas and invalid identifiers. This function is called when the module Reduction has to solve a Miller's pattern.

I have a complicated example (that comes from the arithmetic library) where the inference of a term fails because Dedukti cannot guess the type of a domain free lambda. However, there is no such lambda in the original file: This lambda has been introduced by the matching function.

This is also problematic since it might happen that this terms, once printed using the module Pp cannot be parsed again since this function introduces invalid identifiers.

While I think the second problem can be fixed easily, for example by changing the identifier, the first problem might be more complicated to fix since no type information is carried during the reduction. However, for the moment, I don't have a nice and simple example that reveal that behavior.

Line 23 of the parser we can find

let ident   = ['a'-'z' 'A'-'Z' '0'-'9' '_']['a'-'z' 'A'-'Z' '0'-'9' '_' '!' '?' '\'' ]*

so _ is a valid identifier according this regexp. However, because of line 44 that defines tokens :

  | "_"         { UNDERSCORE ( get_loc lexbuf ) }

``_` is never parsed as an identifier.

By the way, what is the reason that an identifier cannot start with a ?, ! ?

Frédéric a créé un jour un fichier TODO qui contenait :

Il faudrait que dkcheck inclut de lui-même <opam_root>//lib/dedukti
par exemple en utilisant un ./configure

Comme ce n'est pas directement le projet, j'ouvre une issue avec cette proposition et je supprime le fichier en question.

Brackets are replaced with fresh unapplied "a la Miller" variables together with the promise of a systematic conversion check before the rule is fired.

For instance the rule
[s1, s2, a, b] Term {rule s1 s2} (prod s1 s2 a b) --> x : Term s1 a -> Term s2 (b x).
is interpreted as
[?_1, s1, s2, a, b] Term ?_1 (prod s1 s2 a b) --> x : Term s1 a -> Term s2 (b x).
together with the promise that the rule is only applied when ?_1 is convertible with rule s1 s2.

A couple of sanity checks are performed when type checking the rule:

• The bracketed term should not use the locally bounded variables since it corresponds to unapplied variable from the context.
• Same for its type.
• The type inferred for the fresh variable in place of the bracket cannot depend on context variable occurring after the bracket. It seems reasonable to expect the bracketed term to have a type respecting this property as well.

(Potential) issues:

• For now the checks seem too restrictive. The term in brackets cannot depend on context variable declared after it in the rule context. Is there a reason for that ?
• Are the checks necessary ? Do we fail later on anyway if they are omitted ?
• Error messages could be more explicit. Make the distinction between all three reasons to fail.
• Should we fail or simply warn the user ? It could be that the user somehow "knows better" and indeed expects a term depending variables it's not supposed to.

It is currently not possible to just type "make install" in a user session because binaries are always installed system-wide. We should install them in the $(dir $(shell which ocamlc)) (in makefile language) or somewhere similar.

On the example below, we observe a strange behavior:

A : Type.

a : A.

aa : A -> A.

def f : (A -> A) -> A -> A.

def g : (A -> A) -> A -> A.

def h : (A -> A) -> (A -> A) -> A -> A.

def bb : A -> A := aa.

(; WHNF not well-defined on non confluent system ;)
[] f (x => bb x) --> (x : A => aa x).

#EVAL[WHNF] f (x => bb x).

Dedukti gives us that the WHNF of f (x => bb x) is itself while it is obviously a redex. The reason is that bb being defined, Dedukti tries first to reduce the argument (x => bb x) (not using a WHNF strategy), that reduces to (x => aa x), and then tries to match the pattern.

I think the manual should clearly state that the WHNF strategy is not well-defined for non-confluent systems. Notice that this behavior applies also to the HNF strategy.

I just got an issue with a tool that uses Dedukti with the master version: we change the intern representation of tree without changing the version number, hence the serialization with the Marshal module can do a segmentation fault. We should bump something in version number when we make such modifications.

The website of Dedukti is still in the master branch. One should move the website to the Deducteam.github.io repository maybe?

At FSCD 2016, Tomer Libal and Dale Miller propose an extension for patterns.

This extension allows to write this rewrite rule for example (if my understanding of their criterion is correct):

[F] foo (x => F (S x)) --> 0.

that is currently rejected by Dedukti.

As far as I know, I don't know any need to extend patterns with this criterion. However, I am curious, and I was wondering how hard it would be to extend the matching algorithm with this new criterion.

Do you have any remarks @rafoo @Gaspi @GuillaumeGen @rlepigre ?

Dedukti returns SUCCESS when type checking the following file.

A : Type.
B : Type.
#ASSERT (x : A => x) == (x : B => x).

Is this the expected behavior ?
Is it unsafe to have convertibility checks ignore type annotations or can we afford it because of the properties we assume on the system ?

In the following example, only the first rewrite is well-typed by Dedukti (and lambdapi) but not the second.

A : Type.

a : A.

def T : A -> Type.

[] T a --> A -> A.

True : Type.

def eq : A -> A -> Type.
[x] eq x x --> True.
true : True.
def f : x : A -> y : A -> eq x y -> T x ->  A.

(; OK ;)
[] f a _ true (x => x) --> a.

(; Not OK ;)
[] f _ a true (x => x) --> a.

However, the typing forces that the joker is convertible to a, hence the rewrite rule should be well-typed. In that simple example, writing the first or the second rule does not matter. But is it possible to have an example where it does? Also, is this behavior the one expected?

On the client side (dkcheck, dkindent, ...) opaque definitions and definitions are handled the same way. To avoid code duplication, it might be interesting to have only one method such as mk_definition that takes one more parameter to know if the definition is opaque or not.

The following system successfully typechecks in Dedukti:

def A : Type.
def eA : A -> Type.
a : A.
[] A --> eA a.

B : Type.
def eB : B -> Type.

[] eB a --> eA a.

even though eB has type B -> Type and a has type eA a with eA a and B are not convertible.

Dedukti should only successfully typecheck rules when the following two conditions are met:

1. All substitution yielding a well typed term from the left hand side pattern also yield a well typed term when applied to the right hand side term.
2. There exists such a substitution (yielding a well typed term from the left hand side pattern)

The following example:

A : Type.

def g : A -> A.
def f : A -> A -> A.

def a : A.
def b : A.

[] g a --> f a b.
[] a --> b.
[x] f x x --> g x.

#EVAL[WHNF] (f a b).

returns g a.
What happens, is that Dedukti detects that g uses its first argument, calculates the WHNF of a, it is b and since g bdoes not match any head rewrite rule, Dedukti throws the reduct of the argument away and prints that g a is a WHNF.
It is really frustrating, since there is a rule which can be applied on the head of such a term.
But, there is a way to perform reductions from g a to a normal form with no step at the head, that's the reason why Dedukti calls it Weak Head Normal Form.

When defining a rewrite rule, Dedukti's parsing uses the given "context" only to tell apart defined constant identifier from variables in the pre-pattern (since it can't access the signature).
Pattern is then built from reading the term and adding variable to the context as we encounter them.

Issues:

• the (facultatively) given types are completely ignored when type checking the rule (they can even be incorrect types). We could:
  • remove the possibility to write [v1 : T1, v2 : T2] .... Warning: this will raise some retro-compatibility issues.
  • consider these types as constraints on the types inferred for the corresponding variables (just like brackets) and check them during rule type checking.
• the list of identifiers in the given context is to be simply considered as a set of names (potentially) corresponding to variables. Their order is not the order of variables in the actual context, it doesn't really matter whether variable names are used or not, fresh (unapplied) extra variables are silently added to replace wildcards (jokers).
  • This behavior should be made clear in the documentation / tutorial. It is for instance misleading to refer to this list as "the context" of the rewrite rule.
  • We should probably simply ignore unused variables instead of warning about them.
  • Ideally, we should be able to drop the declaration of variable names at parsing and infer in the kernel which symbol is from the signature and which is a context variable.

The installation is quite hard to understand, and not at all documented (by reading the .travis.ml, we get some information, but reading the Readme is the normal choice):

• "oasis setup" raises "W: No exported module defined for library dedukti", but we are suppose to guess that it works
• "./configure --enable-tests" Would be great to be able to set in which folder the program will be installed (I know that I must set prefix in setup.data, but that's not a common knowledge)
• "make build" works as expected
• "make test" does a build again (I don't like this, but this was the previous behaviour on develop, not the behaviour on master).

Furthermore, there is no Makefile anymore, meaning that doing a checkouts between master and develop destroy the Makefile, meaning, that we must redo our changes in setup.data each time, that's a bit boring.

I have the impression with the new abstract type Dtree.t, it is not possible to know if a symbol is definable or not using the module Env.

In the following file, Dedukti fails to ensure that the right-hand-side uses the variable f with arity at least one. The rule is accepted but not always used as shown by the assertion.

#NAME bug.

type : Type.
def term : type -> Type.

arr : type -> type -> type.
[A,B] term (arr A B) --> term A -> term B.

E : A : type -> term A -> type.
r : A : type -> a : term A -> term (E A a).

A : type.
B : type.

def e : f : (term A -> term B) ->
        (x : term A -> term (E B (f x))) ->
        term (E (arr A B) f).
[f] e f (x => r B (f x)) --> r (arr A B) f.

#ASSERT (f : term (arr A B) => e f (x : term A => r B (f x))) ==
        (f : term (arr A B) => r (arr A B) f).

Error message: Fatal error: exception Failure("Assertion failed.")

The rewrite engine is a little bit dependent on the signature. For example, if you ask the rewrite engine to reduce the definition of test in the following example:

[] one --> S 0.

def test := x : nat => one.

it fails because nat doesn't have a Decision Tree in the signature (it is not the case if you remove the variable x). I think however that this is a silly reason for failing. Since we are not using typing information during the reduction. I have the impression that if no decision tree is associated with a symbol, the rewrite engine could go on.

This problem arises only when you use the rewrite engine without the type checker. The only way to do that right now is to use Dedukti as a library.

The master branch does not seem to have an opam file, thus the travis CI script fails when pinning the local dedukti repo.

In the following (non confluent) example, the two rules for f are forbidden because the locally bound variable x is used at the same position with different arities.

The reason for this constraint is unclear.

A : Type.
a : A.
b : A.

def T : A -> Type.
[] T a --> A -> A.
[] T _ --> (A -> A) -> A.

def f : x : A -> T x -> A.
[] f a (x => x  ) --> a.
[] f _ (x => x a) --> a.

I open this issue to discuss conditional rewriting as a possible
feature request because I just heard of the following benchmark that
might be of interest to compare the efficiency of Dedukti with
programming languages: http://rec.gforge.inria.fr/.

1. Is conditional rewriting desirable in Dedukti?

Apart from the mentioned benchmark, here are a few motivations for adding conditional rewriting.

• Encoding syntactic side-conditions

In the following example, we translate recursive ML programs using a
fixpoint combinator. In order to preserve termination, we need to
reduce the fixpoint only when it is applied to a value.

type : Type.
term : type -> Type.

Bool : type.
def bool := term Bool.
true : bool.
def and : bool -> bool -> bool.
[] and true true --> true.

Nat : type.
def nat := term Nat.
0 : nat.
S : nat -> nat.

Tree : Type.
def tree := term Tree.
leaf : nat -> tree.
node : tree -> tree -> tree.

def is_val : A : type -> term A -> bool.
[] is_val Nat 0 --> true
[n] is_val Nat (S n) --> is_val Nat n
[n] is_val Tree (leaf n) --> is_val Nat n
[l,r] is_val Tree (node l r) --> and (is_val Tree l) (is_val Tree r).

def fix : A : Type -> B : Type ->
          ((term A -> term B) -> term A -> term B) ->
          term A -> term B.
[A, B, f, v] fix A B f v ? is_val A v == true --> f (fix A B f) v.

• Poor-man's modulo AC

Thanks to conditional rewriting, we can implement sorted lists:

bool : Type.
true : bool.

nat : Type.
0 : nat.
S : nat -> nat.

def lt : nat -> nat -> bool.
[] lt 0 (S _) --> true
[m,n] lt (S m) (S n) --> lt m n.

slist : Type.
nil : slist.
def cons : nat -> slist -> slist.
[a,b,l] cons a (cons b l) ? lt b a == true --> cons b (cons a l).

#ASSERT (cons 0 (cons (S 0) nil)) == (cons (S 0) (cons 0 nil)).

Note that cons a (cons b l) and cons b (cons a l) are not
convertible in general but we can prove by induction the theorem a : nat -> b : nat -> l : slist -> eq list (cons a (cons b l)) (cons b (cons a l)).

2. Is it easy to encode?

Usually, when I want to use a rule of the form

[y1, ..., ym] f p1 ... pn ? t == t' --> a

(yi are variables, f is a definable, pi are patterns, t, t', and are terms).

what I do instead is that I declare a new definable f' and write the
following rules (note that the second is not linear):

[y1,...,ym] f p1 ... pn --> f' p1 ... pn t t'
[y1,...,ym,x] f' p1 ... pn x x --> a

I do not know what the limits of this trick are.

3. Is it already there?

It seems that Dedukti already uses conditional rewriting internally
but simply does not yet offer syntax for accessing this feature. Would
it be hard to add this feature?

4. Meta-theory with conditional higher-order rewriting?

Does conditional rewriting make harder proving good properties of the
rewrite system? Harder than non-linearity alone?

Now that we have an entry type, probably we should add a function print_entry in the module Pp. This probably makes dkindent a bit useless because it will just call this function. Maybe it would be interesting that dkindent becomes an option for dkcheck?

This would be very similar to the option --beautify of Coq.

On the following example, Dedukti fails for the last rule with the following error message:

ERROR line:98 column:41 Error while typing 'b[5]' in context:
[?_1, ?_2, ?_3, a, s1, s2, a', $, $, $, $, $, $].
The type is not allowed to refer to bound variables.
Infered type:$:(cic.Term s1[8] (a'[6] x[0])) -> cic.Univ s2[8].

Should we fail in this case? If so, what is the reason? Lanbdapi accepts the rule though.

#NAME cic.

Nat : Type.

z : Nat.
s : Nat -> Nat.

def m : Nat -> Nat -> Nat.
[i] m i z --> i.
[j] m z j --> j.
[i, j] m (s i) (s j) --> s (m i j).

(; Sorts ;)

Sort : Type.

prop : Sort.
type : Nat -> Sort.

(; Universe successors ;)
def succ : Sort -> Sort.
[] succ prop --> type z.
[i] succ (type i) --> type (s i).

(; Universe cumulativity ;)
def next : Sort -> Sort.
[] next prop --> type z.
[i] next (type i) --> type (s i).

(; Universe product rules ;)
def rule : Sort -> Sort -> Sort.
[s1] rule s1 prop --> prop.
[s2] rule prop s2 --> s2.
[i, j] rule (type i) (type j) --> type (m i j).

def max : Sort -> Sort -> Sort.
[s1] max s1 prop --> s1.
[s2] max prop s2 --> s2.
[i, j] max (type i) (type j) --> type (m i j).

(; Types and terms ;)

Univ : s : Sort -> Type.
def Term : s : Sort -> a : Univ s -> Type.

univ : s : Sort -> Univ (succ s).
def lift : s1 : Sort -> s2 : Sort -> a : Univ s1 -> Univ (max s1 s2).

def prod : s1 : Sort -> s2 : Sort -> a : Univ s1 -> b : (Term s1 a -> Univ s2) -> Univ (rule s1 s2).

def join : s1 : Sort -> s2 : Sort -> Univ s1 -> Univ s2 -> Univ (max s1 s2).

[s1,s2] succ (max s1 s2) --> max (succ s1) (succ s2).

[s1,s2] join _ _ (univ s1) (univ s2) --> univ (max s1 s2).

[s] Term _ (univ s) --> Univ s.
[s1, s2, a] Term _ (lift s1 s2 a) --> Term s1 a.
[s1, s2, a, b]
  Term _ (prod s1 s2 a b) --> x : Term s1 a -> Term s2 (b x).

(; Canonicity rules ;)

[s] max s s --> s.
[s1, s2, s3] max (max s1 s2) s3 --> max s1 (max s2 s3).
[s1, s2, s3] rule (max s1 s3) s2 --> max (rule s1 s2) (rule s3 s2).
[s1, s2, s3] rule s1 (max s2 s3) --> max (rule s1 s2) (rule s1 s3).

[s1,s2,s3,a,b,c]
    join _ _ (prod s1 s2 a b) (prod _ s3 a c)
--> prod s1 (max s2 s3) a (x : Term s1 a => join s2 s3 (b x) (c x)).


def cast : s1 : Sort -> s2 : Sort -> s3 : Sort ->
           a : Univ s1 -> b : (Term s1 a -> Univ s2) -> b' : (Term s1 a -> Univ s3) ->
           Term (rule s1 s2) (prod s1 s2 a b) ->
           Term (max (rule s1 s2) (rule s1 s3)) (join (rule s1 s2) (rule s1 s3) (prod s1 s2 a b) (prod s1 s3 a b')).


(; type checks ;)
[s1,s2,s3,a,a',b,b',m,x]
    cast _ _ _ a (x => prod s1 s2 (a' x) (b x)) (x => prod s1 s3 (a' x) (b' x)) m x
--> cast s1 s2 s3 (a' x) (b x) (b' x) (m x).

(; type checks ;)
[s1,s2,s3,a,a',b,b',m,x]
    cast _ _ _ a (x => prod s1 s2 a' b) (x => prod s1 s3 a' b') m x
--> cast s1 s2 s3 a' b b' (m x).

(; type checks ;)
[s1,s2,s3,a,a',b,b',m,x]
    cast _ _ _ a (x => prod s1 s2 a' (b x)) (x => prod s1 s3 a' b') m x
--> cast s1 s2 s3 a' (b x) b' (m x).

(; fails ;)
[s1,s2,s3,a,a',b,b',m,x]
    cast _ _ _ a (x => prod s1 s2 (a' x) b) (x => prod s1 s3 (a' x) b') m x
--> cast s1 s2 s3 (a' x) b b' (m x).

The whole project contains three representations of rules and patterns in Dedukti. Probably some representations are not needed and are cumbersome. Moreover, the translation chain between these representations makes things complicated for the type checker. It should be interesting to clean up a little bit these things.

1. The rules where the LHS is not a Miller's pattern should be rejected at the scoping level.

2. Non-linear rules where the LHS does not check the arity criterion (see #60) should be also rejected at the scoping level.

3. The types wf_pattern and pattern should be merged. Maybe we should keep the type wf_pattern representation.

4. The type 'a rule should be removed and only the type rule_infos should be used.

The last version of master answers success on the following term and it should not since ?26, ?28, ?29 and ?30 are free variables. Actually, you can replace these variables by any term and it still works. On has to use the cic encoding to type check this term.

On Rodolphe implementation, this term is ill-typed.

eq :
  cic.Term (cic.type cic.z)
    (cic.prod (cic.type cic.z) (cic.type cic.z) (cic.univ cic.prop)
       (A:(cic.Univ cic.prop) =>
        cic.prod cic.prop (cic.type cic.z) A
          (_x:(cic.Term cic.prop A) =>
           cic.prod cic.prop (cic.type cic.z) A (__:(cic.Term cic.prop A) => cic.univ cic.prop)))).

refl :
  cic.Term cic.prop
    (cic.prod (cic.type cic.z) cic.prop (cic.univ cic.prop)
       (A:(cic.Univ cic.prop) =>
        cic.prod cic.prop cic.prop A (x:(cic.Term cic.prop A) => eq A x x))).

def match_eq_Prop :
  cic.Term cic.prop
    (cic.prod (cic.type cic.z) cic.prop (cic.univ cic.prop)
       (A:(cic.Univ cic.prop) =>
        cic.prod cic.prop cic.prop A
          (_x:(cic.Term cic.prop A) =>
           cic.prod (cic.type cic.z) cic.prop
             (cic.prod cic.prop (cic.type cic.z) A
                (__:(cic.Term cic.prop A) =>
                 cic.prod cic.prop (cic.type cic.z) (eq A _x __)
                   (z:(cic.Term cic.prop (eq A _x __)) => cic.univ cic.prop)))
             (return_type:
              (cic.Term ?26
                 (cic.prod cic.prop ?28 A
                    (__:(cic.Term ?30 A) =>
                     cic.prod cic.prop ?29 (eq A _x __)
                       (z:(cic.Term cic.prop (eq A _x __)) =>
                        cic.univ cic.prop)))) =>
              cic.prod cic.prop cic.prop (return_type _x (refl A _x))
                (case_refl:
                 (cic.Term cic.prop (return_type _x (refl A _x))) =>
                 cic.prod cic.prop cic.prop A
                   (__:(cic.Term cic.prop A) =>
                    cic.prod cic.prop cic.prop (eq A _x __)
                      (z:(cic.Term cic.prop (eq A _x __)) => return_type __ z))))))).

The file

a : Type.
b : Type.
u : Type.
def inl : a->u.
def inr : b->u.
def casea : u->(a->a)->(b->a)->a.
[Ha,Z] casea Z (x => Ha (inl x)) (y => Ha (inr y))-->Ha Z.

is refused by Dedukti with the error message:

ERROR line:7 column:21 Error while typing 'Ha[1] (test.inl x[0])' in context:
Z: test.u.
$: $[0].
$: test.a.
The type could not be infered.

Does anyone know why ?

PS: I labeled it as a bug, but it might just be the expected behaviour for a reason I was not aware.

It would be interesting that the Reduction module proposed a way to know what are the rules that have been used. A way to do that, for example, would be to have an accumulator that the user can reset at any time.

A :Type.

a : A.
g : A -> A.

def ff : A -> (A -> A) -> A.
[x] ff x (y => {g x}) --> a.

def pr1 : A -> A -> A.
[x,y] pr1 x y --> x.

#WHNF (ff a (y => (pr1 a y))).

A fatal error occurred with the message
Fatal error: exception Failure("Error while reducing a term: a guard was not satisfied.")
The error should be catched.

Work on this issue should be done on the brackets-fatal-error branch:
develop...brackets-fatal-error

The website contains a link to "the manual for the current version (v2.5) of Dedukti" pointing to https://github.com/Deducteam/Dedukti/blob/master/README.md. However, this is not the manual for the v2.5 version anymore but the development version. In particular, it contains instructions for opam pinning which are relevant to developers but not necesseraly to regular users and it does not contain instructions to install Dedukti from Deducteam's opam repository.

Moreover, the current stable version is v2.5.1, not v2.5. I think the manual has not yet been updated with the new syntactic construct (named rewrite-rule).

The manual for v2.5 is here: https://github.com/Deducteam/Dedukti/blob/a2618ac914c74b815c1a45519bda3a4b1cf743eb/README.md but it should probably contain instructions to get the v2.5 version instead of the master branch.

In my opinion, even the Readme of the devel version of Dedukti should target regular users, if we have things to tell to developers, we can put them in another file say Readme_for_devs.md.

The makefiles of our libraries do not raise error, hence if an error occurs during the type-checking of a library, Travis will not consider this build as failed.

Dkcheck has an option -r that allows ignoring a declaration of a symbol that was declared before :

nat : Type.

A : Type.

A : nat -> Type.

#INFER A.
(; prints Type ;)

Is this option useful? I never used it before.

For example, to print a term, there is a function pp_term inside the module Term and a function print_term inside the module Pp. Probably one function is enough. What is the best choice to make here?

Most of the time, functions in Pp are just copy-paste code. Probably Pp should exist for the library, but probably it needs a little cleanup.

I don't understand the behaviour of #CHECK.
If a is of type A then #CHECK a, A print YES but if a is not of type A then #CHECK a, A raise an error:

Error while typing a.
Expected: A
Inferred: ...

I would prefer #CHECK to simply answer NO rather than raising an exception.

Although a .travis.yml file has been added to the repo, the build have not been activated on the travis interface (cf https://travis-ci.org/profile/Deducteam ), but it has been activated for the deducteam.github.io repo, maybe an error ?

In the following ill-typed exemple, Dedukti's error message refers to the free variable a that does not appear in the context of the error message.

#NAME bug.

type : Type.
def term : type -> Type.

pi : A : type -> (term A -> type) -> type.
[A,B] term (pi A B) --> a : term A -> term (B a).

def i (A : type) (B : term A -> type) : term (pi A B) := z : term A => z.

Error message:

ERROR line:9 column:71 Error while typing 'z[0]' in context:
A: bug.type.
B: ?:(bug.term A[0]) -> bug.type.
z: bug.term A[1].
Expected: bug.term (B[1] a[0])
Inferred: bug.term A[2].

Dedukti has changed a bit since the last few months and the manual has not been updated yet.

Everything is in the title

#NAME test.

foo

Now that we remove the #NAME command so that module name and filename should be the same, it might be interesting to have a look at the autodep option. For the moment, this option makes two hypothesis:

• module name and filename are the same (now it should be true)
• There is no circular dependencies

Maybe we could get rid of the second hypothesis. Also, this option is probably incompatible with the option --stdin.

Error given by OCamlbuild on my project:

Error: Files /home/fthire/.opam/4.04.2/lib/dedukti/parser.cmxa
       and /home/fthire/.opam/4.04.2/lib/dedukti/kernel.cmxa
       both define a module named Basic

This error probably extends to all the modules defined by the kernel.

The type rule_infos has a record ctx that is typed_context. Actually, the information that the context is typed is never used since the rewriting engine does not rely on types. It might be better to generalize the type rule_infos so that untyped_context are allowed. This implies that ill-typed rewrite rules can be added in the signature, but this was already the case anyway since the types are exposed.

This allows also to increase the separation between the rewriting engine and the type checking engine of Dedukti.

Currently the reduction commands

#SNF[n] t.
#WHNF[n] t.
#HNF[n] t.

implementation differs from the kernel's implementation. For instance

• #SNF[i] performs all possible reductions (call-by-value) while #SNF first compute the term's WHNF and then recursively dives into the subterms.
• A more delicate issue is that #WHNF[i] can't/shouldn't limit the reductions it's allowed to perform during pattern matching as it may change the reduction strategy as shown in the example below

Bool : Type.    T : Bool.    F : Bool.
def a := T.
def b := a.
def P : Bool -> Bool.
[]  P T --> T.
[x] P x --> F.
#WHNF P b.  (; T ;)
#WHNF[1] P b.
(; Should this be P a ?
b --> a in one step
   Should this be F ?
P b --> F in one step when b isn't allowed to reduce
   Should this be T ?
P b --> P a --> P T --> T with only one step performed "at the head"
the other steps are performed below and simply "recycled" when reducing at the head.
;)

TODO:

• Precisely define the expected behavior for the NSTEPS reduction commands
• Implement it

For the file

nat : Type.
def pair : (nat->nat)->nat->nat.
def split : nat->nat.
[F,Y] split (F Y)-->pair F Y.

which should obviously be refused by Dedukti since F is a free variable applied in the left-hand side of a rule, the error message is:

ERROR line:4 column:15 The variable 'Y[0]' was not found in context:

which is not informative at all.

Hello,

I am trying to use the dedukti.kernel sublib to build a v2.6.0 version of Sukerujo.

Currently, the dedukti library as well as its two sublibs dedukti.kernel and dedukti.parser are all installed in the same directory (typically ~/.opam/<switch>/lib/dedukti). As a result, it is not possible to add one of the sublibs to OCaml's path without also adding the other one.

As a result, when compiling Sukerujo, I get the following warning from ocamlfind:

findlib: [WARNING] Interface parser.cmi occurs in several directories: parser, /home/cauderlier/.opam/4.05.0+flambda/lib/dedukti.

On IRC (channel #deducteam on irc.freenode.net), @c-cube has suggested a solution based on jbuilder. His nunchaku project (https://github.com/nunchaku-inria/nunchaku) uses this solution.

Now that the type entry exists, why the function mk_entry of dkcheck is not in the module Env?

The benefit of this would be to avoid duplicating the code of dkcheck everytime you want to check terms via the kernel API.

We need to write a README file.

Aside from being standard for every binary installed, manpages can contain some complete and helpful documentation, particularly considering the rather concise documentation provided currently by the --help option.