Commit 59d3e2f0 authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

Initial commit

parents
.bkp/
*.dko
.depend
tmp.dk
DKS = $(wildcard *.dk)
DKOS = $(DKS:.dk=.dko)
.PHONY: clean depend
.SUFFIXES: .dk .dko
.dk.dko:
dkcheck -e -nc -r $<
all: $(DKOS)
depend: .depend
.depend:
dkdep *.dk > .depend
clean:
rm -f *.dko .depend tmp.dk
-include .depend
#NAME dk_binary_nat
BNat : Type.
O : BNat.
S0 : BNat -> BNat.
S1 : BNat -> BNat.
(; twice zero is zero ;)
[] S0 O --> O.
#NAME dk_bool
uT := pts.uT.
eT := pts.eT.
(; Bool ;)
(; Declaration ;)
Bool : Type.
(; Constructors ;)
true : Bool.
false : Bool.
(; Pattern-matching ;)
match :
P : (Bool -> uT) ->
eT (P true) ->
eT (P false) ->
b : Bool ->
eT (P b).
[P : Bool -> uT,
Ht : eT (P true),
Hf : eT (P false) ]
match P Ht Hf true --> Ht
[P : Bool -> uT,
Ht : eT (P true),
Hf : eT (P false) ]
match P Ht Hf false --> Hf.
(; Operations ;)
(; polymorphic if .. then .. else .. ;)
ite :
A : uT ->
Bool ->
eT A ->
eT A ->
eT A.
[ A : uT,
x : eT A,
y : eT A,
b : Bool ]
ite A b x y
-->
match (b : Bool => A) x y b.
(; boolean if .. then .. else .. ;)
iteb : Bool -> Bool -> Bool -> Bool.
[ x : Bool, y : Bool ] iteb true x y --> x
[ x : Bool, y : Bool ] iteb false x y --> y.
(; negation ;)
not : Bool -> Bool.
[ b : Bool ] not b --> iteb b false true.
(; binary operators ;)
and : Bool -> Bool -> Bool.
[ x : Bool, y : Bool ] and x y --> iteb x y false.
or : Bool -> Bool -> Bool.
[ x : Bool, y : Bool ] or x y --> iteb x true y.
#NAME dk_char
(; 7bits (ascii) characters ;)
uT := pts.uT.
eT := pts.eT.
Char : Type := dk_machine_int.MInt dk_nat.7.
_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.
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)))))).
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))))))).
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))))))).
__ : Char := cast (S1 (S0 (S1 (S1 (S1 (S1 (S1 _O))))))).
equal : Char -> Char -> dk_bool.Bool
:= dk_machine_int.equal dk_nat.7.
#NAME dk_domain
uT := pts.uT.
eT := pts.eT.
Arrow := pts.Arrow.
Bool := dk_bool.Bool.
true : Bool := dk_bool.true.
false : Bool := dk_bool.false.
or : Bool -> Bool -> Bool
:= dk_bool.or.
Istrue := dk_logic.Istrue.
tt : Istrue true := dk_logic.I.
not : Bool -> Bool := dk_bool.not.
Char := dk_char.Char.
bool_or_intro2 := dk_logic.bool_or_intro2.
(; Labels ;)
Label := dk_string.String.
label_eq : Label -> Label -> Bool := dk_string.equal.
(; Correctness of label_eq ;)
label_eq_rect := dk_string.eq_rect.
(; Dependant if with equality ;)
if_label_eq := dk_string.if_eq.
Domain : Type.
nil : Domain.
cons : Label -> Domain -> Domain.
mem : Label -> Domain -> Bool.
[] mem _ nil --> false.
[ l1 : Label,
l2 : Label,
D : Domain ]
mem l1 (cons l2 D)
-->
or (label_eq l2 l1)
(mem l1 D).
mem_cons : l1 : Label ->
l2 : Label ->
D : Domain ->
Istrue (mem l1 D) ->
Istrue (mem l1 (cons l2 D)).
[ l1 : Label,
l2 : Label,
D : Domain,
H : Istrue (mem l1 D) ]
mem_cons l1 l2 D H
-->
bool_or_intro2
(label_eq l2 l1)
(mem l1 D)
H.
#NAME dk_logic
uT := pts.uT.
eT := pts.eT.
Pi := pts.Pi.
Arrow := pts.Arrow.
Bool := dk_bool.Bool.
true := dk_bool.true.
false := dk_bool.false.
(; Impredicative prop ;)
prop : uT.
Prop : Type := eT prop.
ebP : dk_bool.Bool -> Prop.
eeP : Prop -> uT.
eP : Prop -> Type
:= f : Prop => eT (eeP f).
istrue : Bool -> uT := b : Bool => eeP (ebP b).
Istrue : Bool -> Type := b : Bool => eP (ebP b).
I : Istrue true.
False_elim : A : uT -> Istrue false -> eT A.
bool_and_elim1 : b1 : Bool ->
b2 : Bool ->
Istrue (dk_bool.and b1 b2) ->
Istrue b1.
[ b : Bool, H : Istrue b ]
bool_and_elim1 dk_bool.true b H
-->
I
[ b : Bool, H : Istrue false ]
bool_and_elim1 dk_bool.false b H
-->
H.
bool_and_elim2 : b1 : Bool ->
b2 : Bool ->
Istrue (dk_bool.and b1 b2) ->
Istrue b2.
[ b : Bool, H : Istrue b ]
bool_and_elim2 dk_bool.true b H
-->
H
[ b : Bool, H : Istrue false]
bool_and_elim2 dk_bool.false b H
-->
False_elim (istrue b) H.
bool_or_intro2 : b1 : Bool ->
b2 : Bool ->
Istrue b2 ->
Istrue (dk_bool.or b1 b2).
[ b : Bool, H : Istrue b ]
bool_or_intro2 dk_bool.true b H --> I
[ b : Bool, H : Istrue b ]
bool_or_intro2 dk_bool.false b H --> H.
not_or_elim : b1 : Bool ->
b2 : Bool ->
Istrue (dk_bool.not b1) ->
Istrue (dk_bool.or b1 b2) ->
Istrue b2.
[ b : Bool,
Hb : Istrue b ]
not_or_elim dk_bool.false b _ Hb --> Hb.
#NAME dk_machine_int
uT := pts.uT.
eT := pts.eT.
Bool : Type := dk_bool.Bool.
UNat : Type := dk_nat.Nat.
UO : UNat := dk_nat.O.
US : UNat -> UNat := dk_nat.S.
MInt : UNat -> Type.
O : MInt UO.
S0 : N : UNat -> MInt N -> MInt (US N).
S1 : N : UNat -> MInt N -> MInt (US N).
zero : N : UNat -> MInt N.
[] zero dk_nat.O --> O
[ N : UNat ] zero (dk_nat.S N) --> S0 N (zero N).
(; equality ;)
equal : N : UNat -> MInt N -> MInt N -> Bool.
[ N : UNat, n : MInt N ] equal N n n --> dk_bool.true
[ N : UNat, n : MInt N, m : MInt N ]
equal _ (S0 _ n) (S0 N m) --> equal N n m
[ N : UNat, n : MInt N, m : MInt N ]
equal _ (S1 _ n) (S1 N m) --> equal N n m
[ N : UNat, n : MInt N, m : MInt N ]
equal _ (S0 _ n) (S1 N m) --> dk_bool.false
[ N : UNat, n : MInt N, m : MInt N ]
equal _ (S1 _ n) (S0 N m) --> dk_bool.false.
(; Casting binary natural numbers ;)
cast_bnat : N : UNat -> bn : dk_binary_nat.BNat -> MInt N.
[ N : UNat ] cast_bnat N dk_binary_nat.O --> zero N
[ bn : dk_binary_nat.BNat ] cast_bnat dk_nat.O bn --> O.
[ N : UNat, bn : dk_binary_nat.BNat ]
cast_bnat (dk_nat.S N) (dk_binary_nat.S0 bn)
-->
S0 N (cast_bnat N bn)
[ N : UNat, bn : dk_binary_nat.BNat ]
cast_bnat (dk_nat.S N) (dk_binary_nat.S1 bn)
-->
S1 N (cast_bnat N bn).
#NAME dk_nat
Bool : Type := dk_bool.Bool.
Nat : Type.
O : Nat.
S : Nat -> Nat.
(; Operations ;)
(; Addition ;)
(; This definition of plus is compatible with dependant list concatenation ;)
plus : Nat -> Nat -> Nat.
[ m : Nat ] plus O m --> m
[ n : Nat, m : Nat ] plus (S n) m --> S (plus n m).
(; Product ;)
mult : Nat -> Nat -> Nat.
[ m : Nat ] mult O m --> O
[ n : Nat, m : Nat ] mult (S n) m --> plus (mult n m) m.
1 := S O.
2 := S 1.
3 := S 2.
4 := S 3.
5 := S 4.
6 := S 5.
7 := S 6.
#NAME dk_obj
uT := pts.uT.
eT := pts.eT.
Arrow := pts.Arrow.
(; TODO: eliminate dependency on cc ;)
(; Have a version of bool independant of cc ;)
(; Booleans ;)
Bool := dk_bool.Bool.
true : Bool := dk_bool.true.
false : Bool := dk_bool.false.
not : Bool -> Bool := dk_bool.not.
and : Bool -> Bool -> Bool
:= dk_bool.and.
or : Bool -> Bool -> Bool
:= dk_bool.or.
(; Characters ;)
Char := dk_char.Char.
(; Logic ;)
Istrue := dk_logic.Istrue.
tt : Istrue true := dk_logic.I.
(; Labels ;)
Label := dk_string.String.
label_eq := dk_string.equal.
if_label_eq := dk_string.if_eq.
if_label_eq_diff := dk_string.if_eq_diff.
(; Domains ;)
Domain := dk_domain.Domain.
domain_mem := dk_domain.mem.
domain_mem_cons := dk_domain.mem_cons.
(; Object types ;)
ObjType := dk_type.type. (; ObjType := list (Label * ObjType) ;)
Ot_nil := dk_type.nil.
Ot_cons := dk_type.cons.
Ot_if := dk_type.if.
Ot_assoc := dk_type.assoc.
Ot_domain := dk_type.domain.
Ot_eq := dk_type.eq.
Ot_has_key := dk_type.has_key.
Ot_st := dk_type.st.
Ot_assoc_subtype := dk_type.assoc_subtype.
(; Expressions, methods and objects ;)
expr : ObjType -> uT.
Expr : ObjType -> Type.
[ A : ObjType ] Expr A --> eT (expr A).
preObj : ObjType -> (Label -> ObjType) -> Domain -> uT.
PreObj : ObjType -> (Label -> ObjType) -> Domain -> Type.
[ A : ObjType,
f : Label -> ObjType,
D : Domain ] PreObj A f D --> eT (preObj A f D).
Po_nil : A : ObjType ->
f : (Label -> ObjType) ->
PreObj A f dk_domain.nil.
Po_cons : A : ObjType ->
f : (Label -> ObjType) ->
D : Domain ->
l : Label ->
(Expr A -> Expr (f l)) ->
PreObj A f D ->
PreObj A f (dk_domain.cons l D).
preselect : A : ObjType ->
f : (Label -> ObjType) ->
D : Domain ->
o : PreObj A f D ->
l : Label ->
Expr A ->
Expr (f l).
[ A : ObjType,
f : Label -> ObjType,
D : Domain,
l1 : Label,
m : Expr A -> Expr (f l1),
o : PreObj A f D,
l2 : Label ]
preselect _ _ _ (Po_cons A f D l1 m o) l2
-->
if_label_eq
(l : Label => Arrow (expr A) (expr (f l)))
l1
l2
m
(preselect A f D o l2).
preupdate : A : ObjType ->
f : (Label -> ObjType) ->
D : Domain ->
o : PreObj A f D ->
l : Label ->
(Expr A -> Expr (f l)) ->
PreObj A f D.
[ A : ObjType,
f : Label -> ObjType,
D : Domain,
l1 : Label,
m1 : Expr A -> Expr (f l1),
o : PreObj A f D,
l2 : Label,
m2 : Expr A -> Expr (f l2) ]
preupdate _ _ _ (Po_cons A f D l1 m1 o) l2 m2
-->
if_label_eq
(l : Label => preObj A f (dk_domain.cons l D))
l2
l1
(Po_cons A f D l2 m2 o)
(Po_cons A f D l1 m1 (preupdate A f D o l2 m2)).
Obj : ObjType -> Type.
[ A : ObjType ]
Obj A
-->
PreObj A (Ot_assoc A) (Ot_domain A).
make : A : ObjType -> Obj A -> Expr A.
select : A : ObjType ->
eA : Expr A ->
l : Label ->
Expr (Ot_assoc A l).
[ A : ObjType,
o : Obj A,
l : Label ]
select A (make _ o) l
-->
preselect
A
(Ot_assoc A)
(Ot_domain A)
o
l
(make A o).
update : A : ObjType ->
eA : Expr A ->
l : Label ->
(Expr A -> Expr (Ot_assoc A l)) ->
Expr A.
[A : ObjType,
o : Obj A,
l : Label,
m : Expr A -> Expr (Ot_assoc A l)]
update A (make _ o) l m
-->
make
A
(preupdate
A
(Ot_assoc A)
(Ot_domain A)
o
l
m).
(; Subtyping ;)
precast : A : ObjType ->
B : ObjType ->
Expr A ->
C : Domain ->
PreObj B (Ot_assoc A) C.
[ A : ObjType,
B : ObjType,
o : Expr A ]
precast A B o dk_domain.nil
-->
Po_nil B (Ot_assoc A)
[ A : ObjType,
B : ObjType,
o : Expr A,
l2 : Label,
C : Domain ]
precast A B o (dk_domain.cons l2 C)
-->
Po_cons B (Ot_assoc A) C l2
(self : Expr B => select A o l2)
(precast A B o C).
ocast : A : ObjType ->
B : ObjType ->
Expr A ->
PreObj B (Ot_assoc A) (Ot_domain B)
:=
A : ObjType =>
B : ObjType =>
o : Expr A =>
precast A B o (Ot_domain B).
meth_eq : A : ObjType ->
B1 : ObjType ->
B2 : ObjType ->
Istrue (Ot_eq B2 B1) ->
(Expr A -> Expr B1) ->
Expr A ->
Expr B2.
[ A : ObjType,
B : ObjType,
m : Expr A -> Expr B ] meth_eq A B B _ m --> m.
Ot_eq_po : A : ObjType ->
B1 : ObjType ->
B2 : ObjType ->
C : Domain ->
(l : Label ->
Istrue (domain_mem l C) ->
Istrue (Ot_eq (Ot_assoc B2 l) (Ot_assoc B1 l))) ->
PreObj A (Ot_assoc B1) C ->
PreObj A (Ot_assoc B2) C.
[ A : ObjType,
B1 : ObjType,
B2 : ObjType,
o : PreObj A (Ot_assoc B1) dk_domain.nil ]
Ot_eq_po A B1 B2 _ _ (Po_nil _ _)
-->
Po_nil A (Ot_assoc B2)
[ A : ObjType,
B1 : ObjType,
B2 : ObjType,
C : Domain,
l : Label,
m : Expr A -> Expr (Ot_assoc B1 l),
H : l2 : Label ->
Istrue (domain_mem l2 (dk_domain.cons l C)) ->
Istrue (Ot_eq (Ot_assoc B2 l2) (Ot_assoc B1 l2)),
o : PreObj A (Ot_assoc B1) C]
Ot_eq_po A B1 B2 (dk_domain.cons l C) H (Po_cons _ _ _ _ m o)
-->
Po_cons
A
(Ot_assoc B2)
C
l
(meth_eq A (Ot_assoc B1 l) (Ot_assoc B2 l) (H l tt) m)
(Ot_eq_po A B1 B2 C
(l2 : Label =>
if_label_eq_diff
(l3 : Label =>
Arrow
(dk_logic.eeP (dk_logic.ebP (domain_mem l3 C)))
(dk_logic.eeP (dk_logic.ebP (Ot_eq (Ot_assoc B2 l3) (Ot_assoc B1 l3)))))
l
l2
(t : Istrue (domain_mem l C) => H l tt)
(Hdiff : Istrue (not (label_eq l2 l)) =>
t : Istrue (domain_mem l2 C) =>
H
l2
(domain_mem_cons l2 l C t))
)
o).
preinit : A : ObjType ->
C : Domain ->
PreObj A (Ot_assoc A) C.
[ A : ObjType ]
preinit A dk_domain.nil
-->
Po_nil A (Ot_assoc A)
[ A : ObjType,
l : Label,
C : Domain ]
preinit A (dk_domain.cons l C)
-->
Po_cons