Skip to content

GitLab

Commit 2ba0577f authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

Adapt all files to new Dedukti syntax

parent 68ef4834
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 1111 additions and 1037 deletions
.gitignore
View file @ 2ba0577f
.bkp/
*.dko
.depend
*.depend
tmp.dk
Makefile
View file @ 2ba0577f
DKS = $(wildcard *.dk)
DKOS = $(DKS:.dk=.dko)
DKDEPENDS = $(DKS:.dk=.dk.depend)
DKDEP = dkdep
DKCHECK = dkcheck
......@@ -8,16 +9,24 @@ DKCHECK_OPTIONS =
.PHONY: clean depend
all: $(DKOS)
%.dko:
$(DKCHECK) -e $(DKCHECK_OPTIONS) $<
all: $(DKOS)
dk_monads.dko:
$(DKCHECK) -e $(DKCHECK_OPTIONS) -nl $<
dk_monads_coc.dko:
$(DKCHECK) -e $(DKCHECK_OPTIONS) -nl -coc $<
%.dk.depend: %.dk
$(DKDEP) $< > $@
depend: .depend
.depend:
$(DKDEP) *.dk > .depend
depend: $(DKDEPENDS)
clean:
rm -f *.dko .depend tmp.dk
rm -f *.dko *.depend tmp.dk
-include .depend
include $(DKDEPENDS)
cc.dk
View file @ 2ba0577f
......@@ -9,3 +9,43 @@ Pi : X : uT -> ((eT X) -> uT) -> uT.
def Arrow : uT -> uT -> uT.
[t1,t2] Arrow t1 t2 --> Pi t1 (x : eT t1 => t2).
(; Declaration of some types which need to add rules on eT. ;)
(; See dk_type ;)
(; Cartesian product ;)
Prod : uT -> uT -> Type.
prod : uT -> uT -> uT.
[X,Y] eT (prod X Y) --> Prod X Y.
(; Dependant sum ;)
Sigma : A : uT -> (eT A -> uT) -> Type.
sigma : A : uT -> (eT A -> uT) -> uT.
[X,Y] eT (sigma X Y) --> Sigma X Y.
(; Binary sum ;)
Sum : uT -> uT -> Type.
sum : uT -> uT -> uT.
[X,Y] eT (sum X Y) --> Sum X Y.
(; See dk_list ;)
(; Lists ;)
List : uT -> Type.
list : uT -> uT.
[A] eT (list A) --> List A.
(; See dk_nat ;)
Nat : Type.
nat : uT.
[] eT nat --> Nat.
(; See dk_machine_int ;)
MInt : Nat -> Type.
Mint : Nat -> uT.
[N] eT (Mint N) --> MInt N.
(; See dk_opt ;)
Option : uT -> Type.
option : uT -> uT.
[A] eT (option A) --> Option A.
dk_binary_nat.dk
View file @ 2ba0577f
#NAME dk_binary_nat.
UNat : Type := dk_nat.Nat.
Bool : Type := dk_bool.Bool.
def UNat : Type := dk_nat.Nat.
def Bool : Type := dk_bool.Bool.
bNat : cc.uT.
BNat : Type := cc.eT bNat.
def BNat : Type := cc.eT bNat.
O : BNat.
S0 : BNat -> BNat.
def S0 : BNat -> BNat.
S1 : BNat -> BNat.
(; twice zero is zero ;)
[] S0 O --> O.
nat_of_bnat : BNat -> UNat.
def nat_of_bnat : BNat -> UNat.
[] nat_of_bnat O --> dk_nat.O
[ bn : BNat ]
[bn]
nat_of_bnat (S0 bn)
-->
dk_nat.mult dk_nat.2 (nat_of_bnat bn)
[ bn : BNat ]
[bn]
nat_of_bnat (S1 bn)
-->
dk_nat.S (dk_nat.mult dk_nat.2 (nat_of_bnat bn)).
succ : BNat -> BNat.
def succ : BNat -> BNat.
(; 0 + 1 = 2 * 0 + 1 ;)
[] succ O --> S1 O.
(; 2n + 1 = 2n + 1 ;)
[ n : BNat ] succ (S0 n) --> S1 n
[n] succ (S0 n) --> S1 n
(; 2n + 1 + 1 = 2 (n+1) ;)
[ n : BNat ] succ (S1 n) --> S0 (succ n).
[n] succ (S1 n) --> S0 (succ n).
bnat_of_nat : UNat -> BNat.
def bnat_of_nat : UNat -> BNat.
[] bnat_of_nat dk_nat.O --> O
[ n : UNat ] bnat_of_nat (dk_nat.S n) --> succ (bnat_of_nat n).
[n] bnat_of_nat (dk_nat.S n) --> succ (bnat_of_nat n).
(; Order ;)
lt : BNat -> BNat -> Bool.
gt : BNat -> BNat -> Bool.
leq : BNat -> BNat -> Bool.
geq : BNat -> BNat -> Bool.
def lt : BNat -> BNat -> Bool.
def gt : BNat -> BNat -> Bool.
def leq : BNat -> BNat -> Bool.
def geq : BNat -> BNat -> Bool.
[ n : BNat ] lt n O --> dk_bool.false
[ m : BNat ] lt O m --> dk_bool.true
[ n : BNat, m : BNat ] lt (S0 n) (S0 m) --> lt n m
[ n : BNat, m : BNat ] lt (S0 n) (S1 m) --> leq n m
[ n : BNat, m : BNat ] lt (S1 n) (S0 m) --> lt n m
[ n : BNat, m : BNat ] lt (S1 n) (S1 m) --> lt n m.
[] lt _ O --> dk_bool.false
[] lt O _ --> dk_bool.true
[n,m] lt (S0 n) (S0 m) --> lt n m
[n,m] lt (S0 n) (S1 m) --> leq n m
[n,m] lt (S1 n) (S0 m) --> lt n m
[n,m] lt (S1 n) (S1 m) --> lt n m.
[ n : BNat, m : BNat ] gt n m --> lt m n.
[n,m] gt n m --> lt m n.
[ m : BNat ] leq O m --> dk_bool.true
[ n : BNat ] leq n O --> dk_bool.false
[ n : BNat, m : BNat ] leq (S0 n) (S0 m) --> leq n m
[ n : BNat, m : BNat ] leq (S0 n) (S1 m) --> leq n m
[ n : BNat, m : BNat ] leq (S1 n) (S0 m) --> lt n m
[ n : BNat, m : BNat ] leq (S1 n) (S1 m) --> leq n m.
[] leq O _ --> dk_bool.true
[] leq _ O --> dk_bool.false
[n,m] leq (S0 n) (S0 m) --> leq n m
[n,m] leq (S0 n) (S1 m) --> leq n m
[n,m] leq (S1 n) (S0 m) --> lt n m
[n,m] leq (S1 n) (S1 m) --> leq n m.
[ n : BNat, m : BNat ] geq n m --> leq m n.
[n,m] geq n m --> leq m n.
(; Equality ;)
eq : BNat -> BNat -> Bool.
[ n : BNat, m : BNat ] eq n m
def eq : BNat -> BNat -> Bool.
[n,m] eq n m
--> dk_bool.and (leq n m) (geq n m).
(; Operations ;)
(; Addition ;)
plus : BNat -> BNat -> BNat.
[ m : BNat ] plus O m --> m
[ n : BNat ] plus n O --> n
[ n : BNat, m : BNat ] plus (S0 n) (S0 m) --> S0 (plus n m)
[ n : BNat, m : BNat ] plus (S0 n) (S1 m) --> S1 (plus n m)
[ n : BNat, m : BNat ] plus (S1 n) (S0 m) --> S1 (plus n m)
[ n : BNat, m : BNat ] plus (S1 n) (S1 m) --> S0 (succ (plus n m)).
def plus : BNat -> BNat -> BNat.
[m] plus O m --> m
[n] plus n O --> n
[n,m] plus (S0 n) (S0 m) --> S0 (plus n m)
[n,m] plus (S0 n) (S1 m) --> S1 (plus n m)
[n,m] plus (S1 n) (S0 m) --> S1 (plus n m)
[n,m] plus (S1 n) (S1 m) --> S0 (succ (plus n m)).
(; Product ;)
mult : BNat -> BNat -> BNat.
[ m : BNat ] mult O m --> O
[ n : BNat ] mult n O --> O
[ n : BNat, m : BNat ] mult (S0 n) (S0 m) --> S0 (S0 (mult n m))
[ n : BNat, m : BNat ] mult (S0 n) (S1 m) --> S0 (plus m (S0 (mult n m)))
[ n : BNat, m : BNat ] mult (S1 n) (S0 m) --> S0 (plus n (S0 (mult n m)))
[ n : BNat, m : BNat ] mult (S1 n) (S1 m) --> S1 (plus (S0 (mult m n)) (plus n m)).
def mult : BNat -> BNat -> BNat.
[] mult O _ --> O
[] mult _ O --> O
[n,m] mult (S0 n) (S0 m) --> S0 (S0 (mult n m))
[n,m] mult (S0 n) (S1 m) --> S0 (plus m (S0 (mult n m)))
[n,m] mult (S1 n) (S0 m) --> S0 (plus n (S0 (mult n m)))
[n,m] mult (S1 n) (S1 m) --> S1 (plus (S0 (mult m n)) (plus n m)).
(; Min and Max ;)
max : BNat -> BNat -> BNat.
[ m : BNat, n : BNat ]
max m n --> dk_bool.ite bNat (leq m n) n m.
def max : BNat -> BNat -> BNat.
[m,n] max m n --> dk_bool.ite bNat (leq m n) n m.
min : BNat -> BNat -> BNat.
[ m : BNat, n : BNat ]
min m n --> dk_bool.ite bNat (leq m n) m n.
def min : BNat -> BNat -> BNat.
[m,n] min m n --> dk_bool.ite bNat (leq m n) m n.
(; Euclidian division ;)
(; by a power of 2 ;)
div2 : BNat -> BNat.
def div2 : BNat -> BNat.
[] div2 O --> O
[ n : BNat ] div2 (S0 n) --> n
[ n : BNat ] div2 (S1 n) --> n.
[n] div2 (S0 n) --> n
[n] div2 (S1 n) --> n.
length : BNat -> UNat.
def length : BNat -> UNat.
[] length O --> dk_nat.O
[ n : BNat ] length (S0 n) --> dk_nat.S (length n)
[ n : BNat ] length (S1 n) --> dk_nat.S (length n).
[n] length (S0 n) --> dk_nat.S (length n)
[n] length (S1 n) --> dk_nat.S (length n).
(; quo2 n k = n / 2^k ;)
quo2 : BNat -> UNat -> BNat.
[ n : BNat ] quo2 n dk_nat.O --> n
[ k : UNat ] quo2 O k --> O
[ n : BNat, k : UNat ]
quo2 (S0 n) (dk_nat.S k) --> quo2 n k
[ n : BNat, k : UNat ]
quo2 (S1 n) (dk_nat.S k) --> quo2 n k.
def quo2 : BNat -> UNat -> BNat.
[n] quo2 n dk_nat.O --> n
[] quo2 O _ --> O
[n,k] quo2 (S0 n) (dk_nat.S k) --> quo2 n k
[n,k] quo2 (S1 n) (dk_nat.S k) --> quo2 n k.
(; mod2 n k = n % 2^k ;)
mod2 : BNat -> UNat -> BNat.
[ n : BNat ] mod2 n dk_nat.O --> O
[ k : UNat ] mod2 O k --> O
[ n : BNat, k : UNat ]
mod2 (S0 n) (dk_nat.S k) --> S0 (mod2 n k)
[ n : BNat, k : UNat ]
mod2 (S1 n) (dk_nat.S k) --> S1 (mod2 n k).
def mod2 : BNat -> UNat -> BNat.
[] mod2 _ dk_nat.O --> O
[] mod2 O _ --> O
[n,k] mod2 (S0 n) (dk_nat.S k) --> S0 (mod2 n k)
[n,k] mod2 (S1 n) (dk_nat.S k) --> S1 (mod2 n k).
dk_builtins.dk
View file @ 2ba0577f
......@@ -4,7 +4,7 @@ standard library into Dedukti ;)
Object : Type.
collection : cc.uT.
Collection : Type := cc.eT collection.
def Collection : Type := cc.eT collection.
collmeth__rep : Collection -> cc.uT.
unknown_type : cc.uT.
......@@ -12,6 +12,6 @@ unknown_def : cc.eT unknown_type.
unknown_proof : cc.eT unknown_type.
(; String ;)
string : cc.uT := dk_string.string.
some_string : cc.eT string.
prop : cc.uT := dk_logic.prop.
def string : cc.uT := dk_string.string.
def some_string : cc.eT string.
def prop : cc.uT := dk_logic.prop.
dk_char.dk
View file @ 2ba0577f
#NAME dk_char.
(; 7bits (ascii) characters ;)
char : cc.uT := dk_machine_int.Mint dk_nat.7.
Char := cc.eT char.
_O : dk_binary_nat.BNat := dk_binary_nat.O.
S0 : dk_binary_nat.BNat -> dk_binary_nat.BNat := dk_binary_nat.S0.
S1 : dk_binary_nat.BNat -> dk_binary_nat.BNat := dk_binary_nat.S1.
cast : dk_binary_nat.BNat -> Char := dk_machine_int.cast_bnat dk_nat.7.
def char : cc.uT := dk_machine_int.Mint dk_nat.7.
def Char := cc.eT char.
def _O : dk_binary_nat.BNat := dk_binary_nat.O.
def S0 : dk_binary_nat.BNat -> dk_binary_nat.BNat := dk_binary_nat.S0.
def S1 : dk_binary_nat.BNat -> dk_binary_nat.BNat := dk_binary_nat.S1.
def cast : dk_binary_nat.BNat -> Char := dk_machine_int.cast_bnat dk_nat.7.
0 : Char := cast (S0 (S0 (S0 (S0 (S1 (S1 _O)))))).
1 : Char := cast (S1 (S0 (S0 (S0 (S1 (S1 _O)))))).
2 : Char := cast (S0 (S1 (S0 (S0 (S1 (S1 _O)))))).
3 : Char := cast (S1 (S1 (S0 (S0 (S1 (S1 _O)))))).
4 : Char := cast (S0 (S0 (S1 (S0 (S1 (S1 _O)))))).
5 : Char := cast (S1 (S0 (S1 (S0 (S1 (S1 _O)))))).
6 : Char := cast (S0 (S1 (S1 (S0 (S1 (S1 _O)))))).
7 : Char := cast (S1 (S1 (S1 (S0 (S1 (S1 _O)))))).
8 : Char := cast (S0 (S0 (S0 (S1 (S1 (S1 _O)))))).
9 : Char := cast (S1 (S0 (S0 (S1 (S1 (S1 _O)))))).
def 0 : Char := cast (S0 (S0 (S0 (S0 (S1 (S1 _O)))))).
def 1 : Char := cast (S1 (S0 (S0 (S0 (S1 (S1 _O)))))).
def 2 : Char := cast (S0 (S1 (S0 (S0 (S1 (S1 _O)))))).
def 3 : Char := cast (S1 (S1 (S0 (S0 (S1 (S1 _O)))))).
def 4 : Char := cast (S0 (S0 (S1 (S0 (S1 (S1 _O)))))).
def 5 : Char := cast (S1 (S0 (S1 (S0 (S1 (S1 _O)))))).
def 6 : Char := cast (S0 (S1 (S1 (S0 (S1 (S1 _O)))))).
def 7 : Char := cast (S1 (S1 (S1 (S0 (S1 (S1 _O)))))).
def 8 : Char := cast (S0 (S0 (S0 (S1 (S1 (S1 _O)))))).
def 9 : Char := cast (S1 (S0 (S0 (S1 (S1 (S1 _O)))))).
A : Char := cast (S1 (S0 (S0 (S0 (S0 (S0 (S1 _O))))))).
B : Char := cast (S0 (S1 (S0 (S0 (S0 (S0 (S1 _O))))))).
C : Char := cast (S1 (S1 (S0 (S0 (S0 (S0 (S1 _O))))))).
D : Char := cast (S0 (S0 (S1 (S0 (S0 (S0 (S1 _O))))))).
E : Char := cast (S1 (S0 (S1 (S0 (S0 (S0 (S1 _O))))))).
F : Char := cast (S0 (S1 (S1 (S0 (S0 (S0 (S1 _O))))))).
G : Char := cast (S1 (S1 (S1 (S0 (S0 (S0 (S1 _O))))))).
H : Char := cast (S0 (S0 (S0 (S1 (S0 (S0 (S1 _O))))))).
I : Char := cast (S1 (S0 (S0 (S1 (S0 (S0 (S1 _O))))))).
J : Char := cast (S0 (S1 (S0 (S1 (S0 (S0 (S1 _O))))))).
K : Char := cast (S1 (S1 (S0 (S1 (S0 (S0 (S1 _O))))))).
L : Char := cast (S0 (S0 (S1 (S1 (S0 (S0 (S1 _O))))))).
M : Char := cast (S1 (S0 (S1 (S1 (S0 (S0 (S1 _O))))))).
N : Char := cast (S0 (S1 (S1 (S1 (S0 (S0 (S1 _O))))))).
O : Char := cast (S1 (S1 (S1 (S1 (S0 (S0 (S1 _O))))))).
P : Char := cast (S0 (S0 (S0 (S0 (S1 (S0 (S1 _O))))))).
Q : Char := cast (S1 (S0 (S0 (S0 (S1 (S0 (S1 _O))))))).
R : Char := cast (S0 (S1 (S0 (S0 (S1 (S0 (S1 _O))))))).
S : Char := cast (S1 (S1 (S0 (S0 (S1 (S0 (S1 _O))))))).
T : Char := cast (S0 (S0 (S1 (S0 (S1 (S0 (S1 _O))))))).
U : Char := cast (S1 (S0 (S1 (S0 (S1 (S0 (S1 _O))))))).
V : Char := cast (S0 (S1 (S1 (S0 (S1 (S0 (S1 _O))))))).
W : Char := cast (S1 (S1 (S1 (S0 (S1 (S0 (S1 _O))))))).
X : Char := cast (S0 (S0 (S0 (S1 (S1 (S0 (S1 _O))))))).
Y : Char := cast (S1 (S0 (S0 (S1 (S1 (S0 (S1 _O))))))).
Z : Char := cast (S0 (S1 (S0 (S1 (S1 (S0 (S1 _O))))))).
def A : Char := cast (S1 (S0 (S0 (S0 (S0 (S0 (S1 _O))))))).
def B : Char := cast (S0 (S1 (S0 (S0 (S0 (S0 (S1 _O))))))).
def C : Char := cast (S1 (S1 (S0 (S0 (S0 (S0 (S1 _O))))))).
def D : Char := cast (S0 (S0 (S1 (S0 (S0 (S0 (S1 _O))))))).
def E : Char := cast (S1 (S0 (S1 (S0 (S0 (S0 (S1 _O))))))).
def F : Char := cast (S0 (S1 (S1 (S0 (S0 (S0 (S1 _O))))))).
def G : Char := cast (S1 (S1 (S1 (S0 (S0 (S0 (S1 _O))))))).
def H : Char := cast (S0 (S0 (S0 (S1 (S0 (S0 (S1 _O))))))).
def I : Char := cast (S1 (S0 (S0 (S1 (S0 (S0 (S1 _O))))))).
def J : Char := cast (S0 (S1 (S0 (S1 (S0 (S0 (S1 _O))))))).
def K : Char := cast (S1 (S1 (S0 (S1 (S0 (S0 (S1 _O))))))).
def L : Char := cast (S0 (S0 (S1 (S1 (S0 (S0 (S1 _O))))))).
def M : Char := cast (S1 (S0 (S1 (S1 (S0 (S0 (S1 _O))))))).
def N : Char := cast (S0 (S1 (S1 (S1 (S0 (S0 (S1 _O))))))).
def O : Char := cast (S1 (S1 (S1 (S1 (S0 (S0 (S1 _O))))))).
def P : Char := cast (S0 (S0 (S0 (S0 (S1 (S0 (S1 _O))))))).
def Q : Char := cast (S1 (S0 (S0 (S0 (S1 (S0 (S1 _O))))))).
def R : Char := cast (S0 (S1 (S0 (S0 (S1 (S0 (S1 _O))))))).
def S : Char := cast (S1 (S1 (S0 (S0 (S1 (S0 (S1 _O))))))).
def T : Char := cast (S0 (S0 (S1 (S0 (S1 (S0 (S1 _O))))))).
def U : Char := cast (S1 (S0 (S1 (S0 (S1 (S0 (S1 _O))))))).
def V : Char := cast (S0 (S1 (S1 (S0 (S1 (S0 (S1 _O))))))).
def W : Char := cast (S1 (S1 (S1 (S0 (S1 (S0 (S1 _O))))))).
def X : Char := cast (S0 (S0 (S0 (S1 (S1 (S0 (S1 _O))))))).
def Y : Char := cast (S1 (S0 (S0 (S1 (S1 (S0 (S1 _O))))))).
def Z : Char := cast (S0 (S1 (S0 (S1 (S1 (S0 (S1 _O))))))).
a : Char := cast (S1 (S0 (S0 (S0 (S0 (S1 (S1 _O))))))).
b : Char := cast (S0 (S1 (S0 (S0 (S0 (S1 (S1 _O))))))).
c : Char := cast (S1 (S1 (S0 (S0 (S0 (S1 (S1 _O))))))).
d : Char := cast (S0 (S0 (S1 (S0 (S0 (S1 (S1 _O))))))).
e : Char := cast (S1 (S0 (S1 (S0 (S0 (S1 (S1 _O))))))).
f : Char := cast (S0 (S1 (S1 (S0 (S0 (S1 (S1 _O))))))).
g : Char := cast (S1 (S1 (S1 (S0 (S0 (S1 (S1 _O))))))).
h : Char := cast (S0 (S0 (S0 (S1 (S0 (S1 (S1 _O))))))).
i : Char := cast (S1 (S0 (S0 (S1 (S0 (S1 (S1 _O))))))).
j : Char := cast (S0 (S1 (S0 (S1 (S0 (S1 (S1 _O))))))).
k : Char := cast (S1 (S1 (S0 (S1 (S0 (S1 (S1 _O))))))).
l : Char := cast (S0 (S0 (S1 (S1 (S0 (S1 (S1 _O))))))).
m : Char := cast (S1 (S0 (S1 (S1 (S0 (S1 (S1 _O))))))).
n : Char := cast (S0 (S1 (S1 (S1 (S0 (S1 (S1 _O))))))).
o : Char := cast (S1 (S1 (S1 (S1 (S0 (S1 (S1 _O))))))).
p : Char := cast (S0 (S0 (S0 (S0 (S1 (S1 (S1 _O))))))).
q : Char := cast (S1 (S0 (S0 (S0 (S1 (S1 (S1 _O))))))).
r : Char := cast (S0 (S1 (S0 (S0 (S1 (S1 (S1 _O))))))).
s : Char := cast (S1 (S1 (S0 (S0 (S1 (S1 (S1 _O))))))).
t : Char := cast (S0 (S0 (S1 (S0 (S1 (S1 (S1 _O))))))).
u : Char := cast (S1 (S0 (S1 (S0 (S1 (S1 (S1 _O))))))).
v : Char := cast (S0 (S1 (S1 (S0 (S1 (S1 (S1 _O))))))).
w : Char := cast (S1 (S1 (S1 (S0 (S1 (S1 (S1 _O))))))).
x : Char := cast (S0 (S0 (S0 (S1 (S1 (S1 (S1 _O))))))).
y : Char := cast (S1 (S0 (S0 (S1 (S1 (S1 (S1 _O))))))).
z : Char := cast (S0 (S1 (S0 (S1 (S1 (S1 (S1 _O))))))).
def a : Char := cast (S1 (S0 (S0 (S0 (S0 (S1 (S1 _O))))))).
def b : Char := cast (S0 (S1 (S0 (S0 (S0 (S1 (S1 _O))))))).
def c : Char := cast (S1 (S1 (S0 (S0 (S0 (S1 (S1 _O))))))).
def d : Char := cast (S0 (S0 (S1 (S0 (S0 (S1 (S1 _O))))))).
def e : Char := cast (S1 (S0 (S1 (S0 (S0 (S1 (S1 _O))))))).
def f : Char := cast (S0 (S1 (S1 (S0 (S0 (S1 (S1 _O))))))).
def g : Char := cast (S1 (S1 (S1 (S0 (S0 (S1 (S1 _O))))))).
def h : Char := cast (S0 (S0 (S0 (S1 (S0 (S1 (S1 _O))))))).
def i : Char := cast (S1 (S0 (S0 (S1 (S0 (S1 (S1 _O))))))).
def j : Char := cast (S0 (S1 (S0 (S1 (S0 (S1 (S1 _O))))))).
def k : Char := cast (S1 (S1 (S0 (S1 (S0 (S1 (S1 _O))))))).
def l : Char := cast (S0 (S0 (S1 (S1 (S0 (S1 (S1 _O))))))).
def m : Char := cast (S1 (S0 (S1 (S1 (S0 (S1 (S1 _O))))))).
def n : Char := cast (S0 (S1 (S1 (S1 (S0 (S1 (S1 _O))))))).
def o : Char := cast (S1 (S1 (S1 (S1 (S0 (S1 (S1 _O))))))).
def p : Char := cast (S0 (S0 (S0 (S0 (S1 (S1 (S1 _O))))))).
def q : Char := cast (S1 (S0 (S0 (S0 (S1 (S1 (S1 _O))))))).
def r : Char := cast (S0 (S1 (S0 (S0 (S1 (S1 (S1 _O))))))).
def s : Char := cast (S1 (S1 (S0 (S0 (S1 (S1 (S1 _O))))))).
def t : Char := cast (S0 (S0 (S1 (S0 (S1 (S1 (S1 _O))))))).
def u : Char := cast (S1 (S0 (S1 (S0 (S1 (S1 (S1 _O))))))).
def v : Char := cast (S0 (S1 (S1 (S0 (S1 (S1 (S1 _O))))))).
def w : Char := cast (S1 (S1 (S1 (S0 (S1 (S1 (S1 _O))))))).
def x : Char := cast (S0 (S0 (S0 (S1 (S1 (S1 (S1 _O))))))).
def y : Char := cast (S1 (S0 (S0 (S1 (S1 (S1 (S1 _O))))))).
def z : Char := cast (S0 (S1 (S0 (S1 (S1 (S1 (S1 _O))))))).
__ : Char := cast (S1 (S0 (S1 (S1 (S1 (S1 (S1 _O))))))).
def __ : Char := cast (S1 (S0 (S1 (S1 (S1 (S1 (S1 _O))))))).
equal : Char -> Char -> cc.eT dk_bool.bool
:= dk_machine_int.equal dk_nat.7.
def equal : Char -> Char -> cc.eT dk_bool.bool
:= dk_machine_int.equal dk_nat.7.
dk_int.dk
View file @ 2ba0577f
#NAME dk_int.
Nat : Type := dk_nat.Nat.
O : Nat := dk_nat.O.
S : Nat -> Nat := dk_nat.S.
def Nat : Type := dk_nat.Nat.
def O : Nat := dk_nat.O.
def S : Nat -> Nat := dk_nat.S.
B : Type := cc.eT dk_bool.bool.
def B : Type := cc.eT dk_bool.bool.
(; integers are defined by couples of naturals seen as their difference modulo the rule
S n - S m --> n - m
;)
int : cc.uT.
I : Type := cc.eT int.
def I : Type := cc.eT int.
(; the only constructor of Int, make n m builds the integer n - m ;)
make : Nat -> Nat -> I.
def make : Nat -> Nat -> I.
(;
thanks to this rule, intergers reduce to one of the three following normal form :
make O O which is 0
......@@ -20,86 +20,79 @@ or
or
make O (S n) which is -n-1
;)
[n : Nat, m : Nat] make (dk_nat.S n) (dk_nat.S m) --> make n m.
[n,m] make (dk_nat.S n) (dk_nat.S m) --> make n m.
nat_abs : I -> Nat.
[n : Nat] nat_abs (make n dk_nat.O) --> n
[m : Nat] nat_abs (make dk_nat.O m) --> m.
def nat_abs : I -> Nat.
[n] nat_abs (make n dk_nat.O) --> n
[m] nat_abs (make dk_nat.O m) --> m.
(; n - m <= p - q iff n + q <= m + p ;)
leq : I -> I -> B.
[n : Nat, m : Nat, p : Nat, q : Nat]
def leq : I -> I -> B.
[n,m,p,q]
leq (make n m) (make p q)
--> dk_nat.leq (dk_nat.plus n q) (dk_nat.plus m p).
(; n - m < p - q iff n + q < m + p ;)
lt : I -> I -> B.
[n : Nat, m : Nat, p : Nat, q : Nat]
def lt : I -> I -> B.
[n,m,p,q]
lt (make n m) (make p q)
--> dk_nat.lt (dk_nat.plus n q) (dk_nat.plus m p).
geq : I -> I -> B.
[ i : I, j : I ] geq i j --> leq j i.
def geq : I -> I -> B.
[i,j] geq i j --> leq j i.
gt : I -> I -> B.
[ i : I, j : I ] gt i j --> lt j i.
def gt : I -> I -> B.
[i,j] gt i j --> lt j i.
eq : I -> I -> B.
[ i : I, j : I ] eq i j --> dk_bool.and (leq i j) (geq i j).
def eq : I -> I -> B.
[i,j] eq i j --> dk_bool.and (leq i j) (geq i j).
(; (n - m) + (p - q) = (n + p) - (m + q) ;)
plus : I -> I -> I.
[n : Nat,
m : Nat,
p : Nat,
q : Nat]
def plus : I -> I -> I.
[n,m,p,q]
plus (make n m) (make p q)
--> make (dk_nat.plus n p) (dk_nat.plus m q).
opp : I -> I.
[n : Nat, m : Nat]
opp (make n m) --> make m n.
def opp : I -> I.
[n,m] opp (make n m) --> make m n.
sub : I -> I -> I.
[i : I, j : I]
sub i j --> plus i (opp j).
def sub : I -> I -> I.
[i,j] sub i j --> plus i (opp j).
mult : I -> I -> I.
[n : Nat, m : Nat, p : Nat, q : Nat]
def mult : I -> I -> I.
[n,m,p,q]
mult (make n m) (make p q)
--> make
(dk_nat.plus (dk_nat.mult n p) (dk_nat.mult m q))
(dk_nat.plus (dk_nat.mult n q) (dk_nat.mult m p)).
max : I -> I -> I.
[ m : I, n : I ]
max m n --> dk_bool.ite int (leq m n) n m.
def max : I -> I -> I.
[m,n] max m n --> dk_bool.ite int (leq m n) n m.
min : I -> I -> I.
[ m : I, n : I ]
min m n --> dk_bool.ite int (leq m n) m n.
def min : I -> I -> I.
[m,n] min m n --> dk_bool.ite int (leq m n) m n.
abs : I -> I.
[ i : I ] abs i --> make (nat_abs i) O.
def abs : I -> I.
[i] abs i --> make (nat_abs i) O.
mod : I -> I -> I.
[n : Nat, m : Nat, p : Nat]
def mod : I -> I -> I.
[n,m,p]
mod (make m n) (make p dk_nat.O)
--> make (dk_nat.mod m p) (dk_nat.mod n p)
[n : Nat, m : Nat, p : Nat]
[n,m,p]
mod (make m n) (make dk_nat.O p)
--> make (dk_nat.mod m p) (dk_nat.mod n p).
quo : I -> I -> I.
[m : Nat, p : Nat]
def quo : I -> I -> I.
[m,p]
quo (make m dk_nat.O) (make p dk_nat.O)
--> make (dk_nat.quo m p) O
[m : Nat, p : Nat]
[m,p]
quo (make dk_nat.O m) (make dk_nat.O p)
--> make (dk_nat.quo m p) O
[m : Nat, p : Nat]
[m,p]
quo (make dk_nat.O m) (make p dk_nat.O)
--> make O (dk_nat.quo m p)
[m : Nat, p : Nat]
[m,p]
quo (make m dk_nat.O) (make dk_nat.O p)
--> make O (dk_nat.quo m p).
dk_list.dk
View file @ 2ba0577f
#NAME dk_list.
(; Polymorphic lists ;)
list : cc.uT -> cc.uT.
List := A : cc.uT => cc.eT (list A).
def list : cc.uT -> cc.uT := cc.list.
def List : cc.uT -> Type := cc.List.
(; Constructors ;)
nil : A : cc.uT -> List A.
cons : A : cc.uT -> cc.eT A -> List A -> List A.
(; Case distinction ;)
match : A : cc.uT ->
P : (List A -> cc.uT) ->
cc.eT (P (nil A)) ->
(a : cc.eT A -> l : List A -> cc.eT (P (cons A a l))) ->
l : List A ->
cc.eT (P l).
def match : A : cc.uT ->
P : (List A -> cc.uT) ->
cc.eT (P (nil A)) ->
(a : cc.eT A -> l : List A -> cc.eT (P (cons A a l))) ->
l : List A ->
cc.eT (P l).
[A : cc.uT,
P : List A -> cc.uT,
Hnil : cc.eT (P (nil A)),
Hcons : a : cc.eT A -> l : List A -> cc.eT (P (cons A a l))]
match A P Hnil Hcons (nil A) --> Hnil
[A : cc.uT,
P : List A -> cc.uT,
Hnil : cc.eT (P (nil A)),
Hcons : a : cc.eT A -> l : List A -> cc.eT (P (cons A a l)),
a : cc.eT A,
l : List A]
match A P Hnil Hcons (cons A a l) --> Hcons a l.
[Hnil] match _ _ Hnil _ (nil _) --> Hnil
[Hcons,a,l] match _ _ _ Hcons (cons _ a l) --> Hcons a l.
(; Non dependant case distinction ;)
simple_match : A : cc.uT ->
def simple_match : A : cc.uT ->
return : cc.uT ->
cc.eT return ->
(cc.eT A -> List A -> cc.eT return) ->
......@@ -43,55 +32,37 @@ simple_match : A : cc.uT ->
match A (_x : List A => return).