Commit a5ec0150 authored by Gaspard Ferey's avatar Gaspard Ferey

Moved files requiring new_features into sub folder. Added Makefile. Made files compatible with 2.7

parent 3c6f10f5
#put the path of your dkcheck binary
# The path to your dkcheck binary
DKCHECK ?= dkcheck DKCHECK ?= dkcheck
#put the path of your dkdep binary
DKDEP ?= dkdep # The path to your dkdep binary
DKOPTIONS = -nl -errors-in-snf DKDEP ?= dkdep
# dkcheck flags
DKFLAGS ?= -errors-in-snf -e
DKS = $(wildcard *.dk) DKS = $(wildcard *.dk)
DKOS = $(DKS:.dk=.dko) DKOS = $(DKS:.dk=.dko)
...@@ -13,8 +17,7 @@ all: $(DKOS) ...@@ -13,8 +17,7 @@ all: $(DKOS)
%.dko: %.dk .depend %.dko: %.dk .depend
@echo "FILE: $<" @echo "FILE: $<"
#time --format "TIME: %U" --output /dev/stdout $(DKCHECK) $(DKOPTIONS) -e $< $(DKCHECK) $(DKFLAGS) $<
$(DKCHECK) $(DKOPTIONS) -e $<
# standard .depend file generation # standard .depend file generation
.depend: $(DKS) .depend: $(DKS)
...@@ -22,7 +25,7 @@ all: $(DKOS) ...@@ -22,7 +25,7 @@ all: $(DKOS)
@$(DKDEP) $^ -o $@ @$(DKDEP) $^ -o $@
clean: clean:
@rm -f *.dko .depend tmp.dk @rm -f *.dko .depend
ifneq ($(MAKECMDGOALS), clean) ifneq ($(MAKECMDGOALS), clean)
-include .depend -include .depend
......
...@@ -15,34 +15,47 @@ def and : Bool -> Bool -> Bool. ...@@ -15,34 +15,47 @@ def and : Bool -> Bool -> Bool.
[] and False _ --> False. [] and False _ --> False.
[x] and True x --> x. [x] and True x --> x.
(; Une façon de définir and d'arité variable qui est rejetée avec un message d'erreur clair :
All the rewrite rules for the symbol 'and_' should have the same arity ;)
(; (;
def and_ : n : Nat -> Bool_ n. Une première façon de définir "and" par des règles d'arité variable.
[] and_ 0 --> True. Cette methode était rejetée avec un message d'erreur clair :
[x] and_ (S 0) x --> x. All the rewrite rules for the symbol 'and_' should have the same arity
[x,y,n] and_ (S (S n)) x y --> and_ (S n) (and x y). Depuis la version v2.7 elle est acceptée.
(; ;) ;)
(; Ici un and acceptant un nombre variable d'arguments qui type-check bien ;) def and_1 : n : Nat -> Bool_ n.
[] and_1 0 --> True.
[x] and_1 (S 0) x --> x.
[x,y,n] and_1 (S (S n)) x y --> and_1 (S n) (and x y).
(;
Ici une définition bien typée de "and" acceptant un nombre variable d'arguments
mais par des règles de réécriture de même arité.
;)
def and_ : n : Nat -> Bool_ n. def and_ : n : Nat -> Bool_ n.
[] and_ 0 --> True. [] and_ 0 --> True.
[] and_ (S 0) --> (x => x). [] and_ (S 0) --> (x => x).
[n] and_ (S (S n)) --> (x : Bool => y : Bool => (and_ (S n) (and x y))). [n] and_ (S (S n)) --> (x : Bool => y : Bool => (and_ (S n) (and x y))).
(; ;)
(; Quand les patterns d'arités différentes sont imbriqués dans un sous-pattern, on obtient :
Assertion failed lors de la construction de l'arbre de décision
(; This is an "evaluation" function. ;)
def e : n : Nat -> Bool_ n -> Bool_ n. def e : n : Nat -> Bool_ n -> Bool_ n.
def andb : n : Nat -> Bool_ n. (;
[] e 0 (andb 0 ) --> True. This defines the expression "and" over n boolean.
[x] e 0 (andb (S 0) x ) --> x. It does not compute but it should "evaluate" to True (using "e")
[x,y,n] e n (andb _ x y) --> andb (S n) (and x y). iif all n boolean arguments are True.
(; ;) i.e.: e n (andb n ...) -->* and_ n ...
;)
andb : n : Nat -> Bool_ n.
(;
Quand les patterns d'arités différentes sont imbriqués dans un sous-pattern,
on obtenait :
Assertion failed lors de la construction de l'arbre de décision
Depuis la v2.7 elle est acceptée.
;)
[] e 0 (andb 0 ) --> True.
[x] e 0 (andb (S 0) x ) --> x.
[x,y,n] e n (andb {S (S n)} x y) --> andb (S n) (and x y).
def g : n: Nat -> Bool_ n -> Bool. def g : n: Nat -> Bool_ n -> Bool.
[X] g (S (S (S 0))) X --> X True False True. [X] g (S (S (S 0))) X --> X True False True.
...@@ -5,19 +5,19 @@ S : nat -> nat. ...@@ -5,19 +5,19 @@ S : nat -> nat.
def plus: nat -> nat -> nat. def plus: nat -> nat -> nat.
[y] plus 0 y --> y. [y] plus 0 y --> y.
[x,y] plus (S x) y --> S (plus x y). [x,y] plus (S x) y --> S (plus x y).
(; The associativity of plus is needed to type the associativity of concat ;) (; The associativity of plus is needed to type the associativity of concat ;)
[x,y,z] plus (plus x y) z --> plus x (plus y z). [x,y,z] plus (plus x y) z --> plus x (plus y z).
(; ;)
Vect : nat -> Type. Vect : nat -> Type.
(; The non-linear version (;
(; The non-linear version ;)
def concat : n : nat -> Vect n -> m : nat -> Vect m -> Vect (plus n m). def concat : n : nat -> Vect n -> m : nat -> Vect m -> Vect (plus n m).
[n1,n2,n3,l1,l2,l3] concat (plus n1 n2) (concat n1 l1 n2 l2) n3 l3 --> concat n1 l1 (plus n2 n3) (concat n2 l2 n3 l3). [n1,n2,n3,l1,l2,l3] concat (plus n1 n2) (concat n1 l1 n2 l2) n3 l3 --> concat n1 l1 (plus n2 n3) (concat n2 l2 n3 l3).
(; ;) ;)
(; The linear version ;) (; The linear version ;)
def concat : n : nat -> Vect n -> m : nat -> Vect m -> Vect (plus n m). def concat : n : nat -> Vect n -> m : nat -> Vect m -> Vect (plus n m).
[n1,n2,n3,l1,l2,l3] concat _ (concat n1 l1 n2 l2) n3 l3 --> concat n1 l1 (plus n2 n3) (concat n2 l2 n3 l3). [n1,n2,n3,l1,l2,l3] concat _ (concat n1 l1 n2 l2) n3 l3 --> concat n1 l1 (plus n2 n3) (concat n2 l2 n3 l3).
(; ;)
...@@ -132,15 +132,16 @@ def inf : Nat -> Nat -> Bool. ...@@ -132,15 +132,16 @@ def inf : Nat -> Nat -> Bool.
def eqType : n : Nat -> Type. def eqType : n : Nat -> Type.
[] eqType 0 --> A : type -> eval A -> eval A. [] eqType 0 --> A : type -> eval A -> eval A.
[n] eqType (s n) --> A : type -> eval A -> eval A -> eqType n. [n] eqType (s n) --> A : type -> eval A -> eval A -> eqType n.
(; ;) ;)
(; Not allowed due to arity mismatching (; Not allowed due to arity mismatching
def eq : n : Nat -> eqType n. def eq : n : Nat -> eqType n.
[A, x] eq 0 A x --> x [A, x] eq 0 A x --> x
[A, x, n, tl] eq (s n) A x x --> eq n. [A, x, n, tl] eq (s n) A x x --> eq n.
(; ;) ;)
(; Hence, we define eq1 in a non-dependant type (in fact, a bit dependant, encoding polymorphism) ;) (; Hence, we define eq1 in a non-dependant type.
In fact, a bit dependant, encoding polymorphism ;)
def eq1 : A : type -> eval A -> eval A -> B : type -> eval B -> eval B. def eq1 : A : type -> eval A -> eval A -> B : type -> eval B -> eval B.
[A, x, B, y] eq1 A x x B y --> y. [A, x, B, y] eq1 A x x B y --> y.
......
...@@ -19,7 +19,7 @@ def taut : A -> Bool. ...@@ -19,7 +19,7 @@ def taut : A -> Bool.
def ifthensucc : Bool -> Nat -> Nat. def ifthensucc : Bool -> Nat -> Nat.
[n] ifthensucc True n --> S n. [n] ifthensucc True n --> S n.
[n] ifthensucc False n --> n. [n] ifthensucc False n --> n.
(; ;) ;)
def compute_length : (A -> Bool) -> (n: Nat) -> List n -> Nat. def compute_length : (A -> Bool) -> (n: Nat) -> List n -> Nat.
def aux_length : Bool -> (A -> Bool) -> (n: Nat) -> List n -> Nat. def aux_length : Bool -> (A -> Bool) -> (n: Nat) -> List n -> Nat.
......
...@@ -19,7 +19,7 @@ def taut : A -> Bool. ...@@ -19,7 +19,7 @@ def taut : A -> Bool.
def ifthensucc : Bool -> Nat -> Nat. def ifthensucc : Bool -> Nat -> Nat.
[n] ifthensucc True n --> S n. [n] ifthensucc True n --> S n.
[n] ifthensucc False n --> n. [n] ifthensucc False n --> n.
(; ;) ;)
def compute_length : (A -> Bool) -> (n: Nat) -> List -> Nat. def compute_length : (A -> Bool) -> (n: Nat) -> List -> Nat.
def aux_length : Bool -> (A -> Bool) -> (n: Nat) -> List -> Nat. def aux_length : Bool -> (A -> Bool) -> (n: Nat) -> List -> Nat.
......
...@@ -17,5 +17,5 @@ def id : n : nat -> lnt n -> lnt n. ...@@ -17,5 +17,5 @@ def id : n : nat -> lnt n -> lnt n.
(; Ici on obtient un Assertion Failed pour des problèmes d'arité (; Ici on obtient un Assertion Failed pour des problèmes d'arité
#EVAL[SNF] id O (g O). #EVAL[SNF] id O (g O).
(; ;) ;)
...@@ -151,4 +151,4 @@ def ack_is_pos : prf ack_is_pos_thm := ...@@ -151,4 +151,4 @@ def ack_is_pos : prf ack_is_pos_thm :=
(; (;
#EVAL[WHNF] fact_is_pos (exp 10 2). #EVAL[WHNF] fact_is_pos (exp 10 2).
#EVAL[WHNF] ack_is_pos 3 4. #EVAL[WHNF] ack_is_pos 3 4.
(;;) ;)
...@@ -27,7 +27,7 @@ def mult : NatBin -> NatBin -> NatBin. ...@@ -27,7 +27,7 @@ def mult : NatBin -> NatBin -> NatBin.
(; (;
#SNF mult (x2plus1 (x2plus1 1)) (x2plus1 (x2 1)). #SNF mult (x2plus1 (x2plus1 1)) (x2plus1 (x2 1)).
(; ;) ;)
def Syracuse : NatBin -> NatBin. def Syracuse : NatBin -> NatBin.
[] Syracuse 1 --> 1. [] Syracuse 1 --> 1.
...@@ -36,5 +36,5 @@ def Syracuse : NatBin -> NatBin. ...@@ -36,5 +36,5 @@ def Syracuse : NatBin -> NatBin.
(; (;
#EVAL[SNF] Syracuse (x2plus1 (x2plus1 (x2plus1 (x2plus1 (x2plus1 (x2plus1 (x2plus1 (x2 (x2 (x2plus1 (x2 (x2 (x2 (x2 (x2plus1 (x2 (x2plus1 1))))))))))))))))). #EVAL[SNF] Syracuse (x2plus1 (x2plus1 (x2plus1 (x2plus1 (x2plus1 (x2plus1 (x2plus1 (x2 (x2 (x2plus1 (x2 (x2 (x2 (x2 (x2plus1 (x2 (x2plus1 1))))))))))))))))).
(; ;) ;)
...@@ -21,12 +21,14 @@ Cons_bis : n : Nat -> elt -> Vect n -> Vect (S_bis n). ...@@ -21,12 +21,14 @@ Cons_bis : n : Nat -> elt -> Vect n -> Vect (S_bis n).
def Tail_bis : n : Nat -> Vect (S_bis n) -> Vect n. def Tail_bis : n : Nat -> Vect (S_bis n) -> Vect n.
(; La règle non-linéaire, qui est acceptée pour le typage ;) (; La règle non-linéaire, qui est acceptée pour le typage ;)
[n, x, l] Tail_bis n (Cons_bis n x l) --> l. [n, x, l] Tail_bis n (Cons_bis n x l) --> l.
(; ;)
(; La règle linéaire, qui pose un problème de préservation du typage (;
(; La règle linéaire, qui pose un problème de préservation du typage ;)
[n, x, l] Tail_bis n (Cons_bis _ x l) --> l. [n, x, l] Tail_bis n (Cons_bis _ x l) --> l.
(; ;) ;)
e : elt. e : elt.
def 1 := S 0. def 1 := S 0.
...@@ -39,9 +41,15 @@ def suite := Cons 2 e (Cons 1 e (Cons 0 e Nil)). ...@@ -39,9 +41,15 @@ def suite := Cons 2 e (Cons 1 e (Cons 0 e Nil)).
(; Un double YES pour les CHECK, donc on ne veut pas pouvoir convertir l'un en l'autre ;) (; Un double YES pour les CHECK, donc on ne veut pas pouvoir convertir l'un en l'autre ;)
def id_bis : n : Nat -> Vect (S_bis n) -> Vect (S_bis n). def id_bis : n : Nat -> Vect (S_bis n) -> Vect (S_bis n).
(; Une règle qui devrait bien typée, mais qui nécessite de trouver (S_bis n) = (S_bis _), sous la contrainte (S_bis n) = (S_bis _), contrainte qui est jetée, car comme S_bis n'est pas injective, on ne peut rien en déduire en termes de substitution
(;
(; Une règle qui devrait bien typée, mais qui nécessite
de trouver (S_bis n) = (S_bis _),
sous la contrainte (S_bis n) = (S_bis _),
contrainte qui est jetée, car comme S_bis n'est pas injective,
on ne peut rien en déduire en termes de substitution ;)
[n, x, l] id_bis n (Cons_bis _ x l) --> (Cons_bis n x l). [n, x, l] id_bis n (Cons_bis _ x l) --> (Cons_bis n x l).
(; ;) ;)
(; Sa version non-linéaire qui type-checke bien ;) (; Sa version non-linéaire qui type-checke bien ;)
[n, x, l] id_bis n (Cons_bis n x l) --> (Cons_bis n x l). [n, x, l] id_bis n (Cons_bis n x l) --> (Cons_bis n x l).
(; ;)
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment