Skip to content

P
PleinDeDk
Source
Select Git revision
...
Target
Select Git revision
 
Commits (2)
Hide whitespace changes
Inline Side-by-side
Showing with 118 additions and 88 deletions
Miscellaneous/Makefile
View file @ 7b2cafe8
#put the path of your dkcheck binary
DKCHECK = dkcheck
DKCHECK ?= dkcheck
#put the path of your dkdep binary
DKDEP = dkdep
DKDEP ?= dkdep
DKOPTIONS = -nl -errors-in-snf
DKS=$(wildcard *.dk)
DKS = $(wildcard *.dk)
DKOS = $(DKS:.dk=.dko)
# DKOS need not have the same name that the corresponding Dedukti
# files (modulogic.dk becomes zen.dko) but for each file f.dk, dkdep
# f.dk outputs the name of the produced dko file before the ':'
# character.
DKOS=$(shell cut -d ':' -f 1 .depend)
.PHONY: all clean
all: $(DKOS)
%.dko:
$(DKCHECK) -e $(DKOPTIONS) $<
%.dko: %.dk .depend
@echo "FILE: $<"
#time --format "TIME: %U" --output /dev/stdout $(DKCHECK) $(DKOPTIONS) -e $<
$(DKCHECK) $(DKOPTIONS) -e $<
clean:
rm -f *.dko .depend
# standard .depend file generation
.depend: $(DKS)
@echo "Producing .depend"
@$(DKDEP) $^ -o $@
depend: .depend
.depend:
$(DKDEP) *.dk > ./.depend
clean:
@rm -f *.dko .depend tmp.dk
ifneq ($(MAKECMDGOALS), clean)
-include .depend
endif
Miscellaneous/NonConfluenceIsDangerous.dk
View file @ 7b2cafe8
......@@ -17,8 +17,8 @@ def f : Nat -> Nat -> Nat.
[x,y] f x (S y) --> S 0.
[x,y] f (S (S x)) (S y) --> S (S (S 0)).
#SNF (f (double 0) 0).
#SNF (f (S (S 0)) (S (S 0))).
#EVAL (f (double 0) 0).
#EVAL (f (S (S 0)) (S (S 0))).
def eq : Nat -> Nat -> Nat.
[x] eq x x --> S 0.
......
Miscellaneous/intBinaire.dk
View file @ 7b2cafe8
Int : Type.
def Nat := Nat.Nat.
def Bool := Nat.Bool.
def Nat := natBinaire.Nat.
def Bool := natBinaire.Bool.
def T := Nat.T.
def F := Nat.F.
def T := natBinaire.T.
def F := natBinaire.F.
0 : Int.
Pos : Nat -> Int.
Neg : Nat -> Int.
def ifThenElse : Bool -> Int -> Int -> Int.
[x] ifThenElse Nat.T x _ --> x.
[y] ifThenElse Nat.F _ y --> y.
[x] ifThenElse natBinaire.T x _ --> x.
[y] ifThenElse natBinaire.F _ y --> y.
def plus : Int -> Int -> Int.
[x] plus x 0 --> x.
[y] plus 0 y --> y.
[x,y] plus (Pos x) (Pos y) --> Pos (Nat.plus x y).
[x,y] plus (Pos x) (Neg y) --> ifThenElse (Nat.greater x y) (Pos (Nat.moins x y)) (ifThenElse (Nat.eq x y) 0 (Neg (Nat.moins y x))).
[x,y] plus (Neg x) (Pos y) --> ifThenElse (Nat.greater x y) (Neg (Nat.moins x y)) (ifThenElse (Nat.eq x y) 0 (Pos (Nat.moins y x))).
[x,y] plus (Neg x) (Neg y) --> Neg (Nat.plus x y).
[x,y] plus (Pos x) (Pos y) --> Pos (natBinaire.plus x y).
[x,y] plus (Pos x) (Neg y) --> ifThenElse (natBinaire.greater x y) (Pos (natBinaire.moins x y)) (ifThenElse (natBinaire.eq x y) 0 (Neg (natBinaire.moins y x))).
[x,y] plus (Neg x) (Pos y) --> ifThenElse (natBinaire.greater x y) (Neg (natBinaire.moins x y)) (ifThenElse (natBinaire.eq x y) 0 (Pos (natBinaire.moins y x))).
[x,y] plus (Neg x) (Neg y) --> Neg (natBinaire.plus x y).
def moins : Int -> Int -> Int.
[x] moins x 0 --> x.
......@@ -30,21 +30,21 @@ def moins : Int -> Int -> Int.
def mult : Int -> Int -> Int.
[] mult 0 _ --> 0.
[] mult _ 0 --> 0.
[x,y] mult (Pos x) (Pos y) --> Pos (Nat.mult x y).
[x,y] mult (Pos x) (Neg y) --> Neg (Nat.mult x y).
[x,y] mult (Neg x) (Pos y) --> Neg (Nat.mult x y).
[x,y] mult (Neg x) (Neg y) --> Pos (Nat.mult x y).
[x,y] mult (Pos x) (Pos y) --> Pos (natBinaire.mult x y).
[x,y] mult (Pos x) (Neg y) --> Neg (natBinaire.mult x y).
[x,y] mult (Neg x) (Pos y) --> Neg (natBinaire.mult x y).
[x,y] mult (Neg x) (Neg y) --> Pos (natBinaire.mult x y).
def geq : Int -> Int -> Bool.
[] geq 0 0 --> T.
[y] geq 0 (Pos y) --> F.
[y] geq 0 (Neg y) --> T.
[x] geq (Pos x) 0 --> T.
[x,y] geq (Pos x) (Pos y) --> Nat.geq x y.
[x,y] geq (Pos x) (Pos y) --> natBinaire.geq x y.
[x,y] geq (Pos x) (Neg y) --> T.
[x] geq (Neg x) 0 --> F.
[x,y] geq (Neg x) (Pos y) --> F.
[x,y] geq (Neg x) (Neg y) --> Nat.geq y x.
[x,y] geq (Neg x) (Neg y) --> natBinaire.geq y x.
#EVAL[WHNF] mult (Pos (Nat.x2 (Nat.x2plus1 Nat.1))) (Pos (Nat.x2 Nat.1)).
#EVAL[WHNF] mult (Pos (natBinaire.x2 (natBinaire.x2plus1 natBinaire.1))) (Pos (natBinaire.x2 natBinaire.1)).
Miscellaneous/miller.dk
View file @ 7b2cafe8
......@@ -49,7 +49,7 @@ def f : R -> R -> R := plus (x : R => y : R => ch x) (x : R => y : R => sh y).
#EVAL flip (grad f).
(;
#EVAL #20 flip (grad f).
#EVAL[20] flip (grad f).
;)
#EVAL grad (trans f).
......
Miscellaneous/nat_prop.dk
View file @ 7b2cafe8
......@@ -2,7 +2,7 @@
(; Nat as first order terms ;)
(;-------------------------------------------;)
def N := FO.Term.
def N := firstOrder.Term.
0 : N.
S : N -> N.
......@@ -57,9 +57,9 @@ def 1000 := exp 10 3.
(; Shortnames for logic operators ;)
(;-------------------------------------------;)
def prf := FO.prf.
def Prop := FO.Prop.
def eq := FO.equals.
def prf := firstOrder.prf.
def Prop := firstOrder.Prop.
def eq := firstOrder.equals.
(;-------------------------------------------;)
......@@ -79,13 +79,13 @@ def N_ind_prop :
(; A couple of theorems ;)
(;-------------------------------------------;)
def is_pos : N -> Prop := (n:N => FO.exists (m : N => eq (S m) n)).
def succ_is_pos_thm : Prop := FO.forall (n : N => is_pos (S n)).
def is_pos : N -> Prop := (n:N => firstOrder.exists (m : N => eq (S m) n)).
def succ_is_pos_thm : Prop := firstOrder.forall (n : N => is_pos (S n)).
def sum_pos_is_pos_thm : Prop :=
FO.forall (n : N => FO.imp (is_pos n)
(FO.forall (m : N => is_pos (plus n m)))).
def fact_is_pos_thm : Prop := FO.forall (n : N => (is_pos (fact n))).
def ack_is_pos_thm : Prop := FO.forall (n : N => FO.forall (m : N => (is_pos (ack n m)))).
firstOrder.forall (n : N => firstOrder.imp (is_pos n)
(firstOrder.forall (m : N => is_pos (plus n m)))).
def fact_is_pos_thm : Prop := firstOrder.forall (n : N => (is_pos (fact n))).
def ack_is_pos_thm : Prop := firstOrder.forall (n : N => firstOrder.forall (m : N => (is_pos (ack n m)))).
(;-------------------------------------------;)
......@@ -128,11 +128,11 @@ def f100_is_pos2 : prf (is_pos (fact 100)) := fact_is_pos 100.
def ack_is_pos : prf ack_is_pos_thm :=
N_ind_prop
(n : N => FO.forall (m : N => is_pos (ack n m)))
(n : N => firstOrder.forall (m : N => is_pos (ack n m)))
(m : N => (succ_is_pos m))
(
n : N =>
p : prf (FO.forall (m : N => (is_pos (ack n m)))) =>
p : prf (firstOrder.forall (m : N => (is_pos (ack n m)))) =>
N_ind_prop
(m : N => is_pos (ack (S n) m))
(p 1)
......
Miscellaneous/numberBases.dk
View file @ 7b2cafe8
......@@ -20,55 +20,55 @@ Number : Type.
Zero : Number.
Cons : Number -> Figure -> Number.
def decimal : Tuto.Nat -> Number.
def decimal_aux : Tuto.Nat -> Number -> Number.
def decimal : tuto.Nat -> Number.
def decimal_aux : tuto.Nat -> Number -> Number.
[n] decimal n --> decimal_aux n Zero.
[N] decimal_aux Tuto.0 N --> N.
[n] decimal_aux (Tuto.S n) Zero --> decimal_aux n (Cons Zero 1).
[n,N] decimal_aux (Tuto.S n) (Cons N 0) --> decimal_aux n (Cons N 1).
[n,N] decimal_aux (Tuto.S n) (Cons N 1) --> decimal_aux n (Cons N 2).
[n,N] decimal_aux (Tuto.S n) (Cons N 2) --> decimal_aux n (Cons N 3).
[n,N] decimal_aux (Tuto.S n) (Cons N 3) --> decimal_aux n (Cons N 4).
[n,N] decimal_aux (Tuto.S n) (Cons N 4) --> decimal_aux n (Cons N 5).
[n,N] decimal_aux (Tuto.S n) (Cons N 5) --> decimal_aux n (Cons N 6).
[n,N] decimal_aux (Tuto.S n) (Cons N 6) --> decimal_aux n (Cons N 7).
[n,N] decimal_aux (Tuto.S n) (Cons N 7) --> decimal_aux n (Cons N 8).
[n,N] decimal_aux (Tuto.S n) (Cons N 8) --> decimal_aux n (Cons N 9).
[n,N] decimal_aux (Tuto.S n) (Cons N 9) --> decimal_aux n (Cons (decimal_aux (Tuto.S Tuto.0) N) 0).
[N] decimal_aux tuto.0 N --> N.
[n] decimal_aux (tuto.S n) Zero --> decimal_aux n (Cons Zero 1).
[n,N] decimal_aux (tuto.S n) (Cons N 0) --> decimal_aux n (Cons N 1).
[n,N] decimal_aux (tuto.S n) (Cons N 1) --> decimal_aux n (Cons N 2).
[n,N] decimal_aux (tuto.S n) (Cons N 2) --> decimal_aux n (Cons N 3).
[n,N] decimal_aux (tuto.S n) (Cons N 3) --> decimal_aux n (Cons N 4).
[n,N] decimal_aux (tuto.S n) (Cons N 4) --> decimal_aux n (Cons N 5).
[n,N] decimal_aux (tuto.S n) (Cons N 5) --> decimal_aux n (Cons N 6).
[n,N] decimal_aux (tuto.S n) (Cons N 6) --> decimal_aux n (Cons N 7).
[n,N] decimal_aux (tuto.S n) (Cons N 7) --> decimal_aux n (Cons N 8).
[n,N] decimal_aux (tuto.S n) (Cons N 8) --> decimal_aux n (Cons N 9).
[n,N] decimal_aux (tuto.S n) (Cons N 9) --> decimal_aux n (Cons (decimal_aux (tuto.S tuto.0) N) 0).
def binary : Tuto.Nat -> Number.
def binary_aux : Tuto.Nat -> Number -> Number.
def binary : tuto.Nat -> Number.
def binary_aux : tuto.Nat -> Number -> Number.
[n] binary n --> binary_aux n Zero.
[N] binary_aux Tuto.0 N --> N.
[n] binary_aux (Tuto.S n) Zero --> binary_aux n (Cons Zero 1).
[n,N] binary_aux (Tuto.S n) (Cons N 0) --> binary_aux n (Cons N 1).
[n,N] binary_aux (Tuto.S n) (Cons N 1) --> binary_aux n (Cons (decimal_aux (Tuto.S Tuto.0) N) 0).
[N] binary_aux tuto.0 N --> N.
[n] binary_aux (tuto.S n) Zero --> binary_aux n (Cons Zero 1).
[n,N] binary_aux (tuto.S n) (Cons N 0) --> binary_aux n (Cons N 1).
[n,N] binary_aux (tuto.S n) (Cons N 1) --> binary_aux n (Cons (decimal_aux (tuto.S tuto.0) N) 0).
def hexadecimal : Tuto.Nat -> Number.
def hexadecimal_aux : Tuto.Nat -> Number -> Number.
def hexadecimal : tuto.Nat -> Number.
def hexadecimal_aux : tuto.Nat -> Number -> Number.
[n] hexadecimal n --> hexadecimal_aux n Zero.
[N] hexadecimal_aux Tuto.0 N --> N.
[n] hexadecimal_aux (Tuto.S n) Zero --> hexadecimal_aux n (Cons Zero 1).
[n,N] hexadecimal_aux (Tuto.S n) (Cons N 0) --> hexadecimal_aux n (Cons N 1).
[n,N] hexadecimal_aux (Tuto.S n) (Cons N 1) --> hexadecimal_aux n (Cons N 2).
[n,N] hexadecimal_aux (Tuto.S n) (Cons N 2) --> hexadecimal_aux n (Cons N 3).
[n,N] hexadecimal_aux (Tuto.S n) (Cons N 3) --> hexadecimal_aux n (Cons N 4).
[n,N] hexadecimal_aux (Tuto.S n) (Cons N 4) --> hexadecimal_aux n (Cons N 5).
[n,N] hexadecimal_aux (Tuto.S n) (Cons N 5) --> hexadecimal_aux n (Cons N 6).
[n,N] hexadecimal_aux (Tuto.S n) (Cons N 6) --> hexadecimal_aux n (Cons N 7).
[n,N] hexadecimal_aux (Tuto.S n) (Cons N 7) --> hexadecimal_aux n (Cons N 8).
[n,N] hexadecimal_aux (Tuto.S n) (Cons N 8) --> hexadecimal_aux n (Cons N 9).
[n,N] hexadecimal_aux (Tuto.S n) (Cons N 9) --> hexadecimal_aux n (Cons N A).
[n,N] hexadecimal_aux (Tuto.S n) (Cons N A) --> hexadecimal_aux n (Cons N B).
[n,N] hexadecimal_aux (Tuto.S n) (Cons N B) --> hexadecimal_aux n (Cons N C).
[n,N] hexadecimal_aux (Tuto.S n) (Cons N C) --> hexadecimal_aux n (Cons N D).
[n,N] hexadecimal_aux (Tuto.S n) (Cons N D) --> hexadecimal_aux n (Cons N E).
[n,N] hexadecimal_aux (Tuto.S n) (Cons N E) --> hexadecimal_aux n (Cons N F).
[n,N] hexadecimal_aux (Tuto.S n) (Cons N F) --> hexadecimal_aux n (Cons (hexadecimal_aux (Tuto.S Tuto.0) N) 0).
[N] hexadecimal_aux tuto.0 N --> N.
[n] hexadecimal_aux (tuto.S n) Zero --> hexadecimal_aux n (Cons Zero 1).
[n,N] hexadecimal_aux (tuto.S n) (Cons N 0) --> hexadecimal_aux n (Cons N 1).
[n,N] hexadecimal_aux (tuto.S n) (Cons N 1) --> hexadecimal_aux n (Cons N 2).
[n,N] hexadecimal_aux (tuto.S n) (Cons N 2) --> hexadecimal_aux n (Cons N 3).
[n,N] hexadecimal_aux (tuto.S n) (Cons N 3) --> hexadecimal_aux n (Cons N 4).
[n,N] hexadecimal_aux (tuto.S n) (Cons N 4) --> hexadecimal_aux n (Cons N 5).
[n,N] hexadecimal_aux (tuto.S n) (Cons N 5) --> hexadecimal_aux n (Cons N 6).
[n,N] hexadecimal_aux (tuto.S n) (Cons N 6) --> hexadecimal_aux n (Cons N 7).
[n,N] hexadecimal_aux (tuto.S n) (Cons N 7) --> hexadecimal_aux n (Cons N 8).
[n,N] hexadecimal_aux (tuto.S n) (Cons N 8) --> hexadecimal_aux n (Cons N 9).
[n,N] hexadecimal_aux (tuto.S n) (Cons N 9) --> hexadecimal_aux n (Cons N A).
[n,N] hexadecimal_aux (tuto.S n) (Cons N A) --> hexadecimal_aux n (Cons N B).
[n,N] hexadecimal_aux (tuto.S n) (Cons N B) --> hexadecimal_aux n (Cons N C).
[n,N] hexadecimal_aux (tuto.S n) (Cons N C) --> hexadecimal_aux n (Cons N D).
[n,N] hexadecimal_aux (tuto.S n) (Cons N D) --> hexadecimal_aux n (Cons N E).
[n,N] hexadecimal_aux (tuto.S n) (Cons N E) --> hexadecimal_aux n (Cons N F).
[n,N] hexadecimal_aux (tuto.S n) (Cons N F) --> hexadecimal_aux n (Cons (hexadecimal_aux (tuto.S tuto.0) N) 0).
Paradoxes/Makefile 0 → 100644
View file @ 7b2cafe8
#put the path of your dkcheck binary
DKCHECK ?= dkcheck
#put the path of your dkdep binary
DKDEP ?= dkdep
DKOPTIONS = -nl -errors-in-snf
DKS = $(wildcard *.dk)
DKOS = $(DKS:.dk=.dko)
.PHONY: all clean
all: $(DKOS)
%.dko: %.dk .depend
@echo "FILE: $<"
#time --format "TIME: %U" --output /dev/stdout $(DKCHECK) $(DKOPTIONS) -e $<
$(DKCHECK) $(DKOPTIONS) -e $<
# standard .depend file generation
.depend: $(DKS)
@echo "Producing .depend"
@$(DKDEP) $^ -o $@
clean:
@rm -f *.dko .depend tmp.dk
ifneq ($(MAKECMDGOALS), clean)
-include .depend
endif