Commit 639a0ea7 authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

Move dk_obj to its own repo.

parent 1a940969
#NAME dk_obj
(; 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.
(; Logic ;)
Istrue := b : Bool => dk_logic.eP (dk_logic.ebP b).
tt : Istrue true := dk_logic.I.
not_or_elim : b1 : Bool ->
b2 : Bool ->
Istrue (not b1) ->
Istrue (or b1 b2) ->
Istrue b2.
[ b : Bool,
Hb : Istrue b ]
not_or_elim dk_bool.false b _ Hb --> Hb.
and_elim1 := dk_logic.bool_and_elim1.
and_elim2 := dk_logic.bool_and_elim2.
(; Labels ;)
Label := dk_string.String.
label_eq : Label -> Label -> Bool := dk_string.equal.
(; Correctness of label_eq ;)
label_eq_rect : l1 : Label ->
l2 : Label ->
P : (Label -> cc.uT) ->
Istrue (label_eq l2 l1) ->
cc.eT (P l1) ->
cc.eT (P l2).
[ l : Label,
P : Label -> cc.uT,
x : cc.eT (P l) ]
label_eq_rect l l P _ x --> x.
(; Dependant if with equality ;)
if_label_eq : P : (Label -> cc.uT) ->
l1 : Label ->
l2 : Label ->
cc.eT (P l1) ->
cc.eT (P l2) ->
cc.eT (P l2).
[ P : Label -> cc.uT,
l1 : Label,
l2 : Label,
Heq : cc.eT (P l1),
Hdiff : cc.eT (P l2) ]
if_label_eq P l1 l2 Heq Hdiff
-->
dk_bool.match
(b : Bool =>
cc.Arrow (cc.Arrow (dk_logic.eeP (dk_logic.ebP b))
(P l2))
(cc.Arrow (P l2) (P l2)))
(H1 : (dk_logic.TrueT -> cc.eT (P l2)) =>
H2 : cc.eT (P l2) => H1 dk_logic.I)
(H1 : (dk_logic.FalseT -> cc.eT (P l2)) =>
H2 : cc.eT (P l2) => H2)
(label_eq l2 l1)
(H : Istrue (label_eq l2 l1) =>
label_eq_rect l1 l2 P H Heq)
Hdiff.
Domain := dk_list.List dk_string.string.
domain_nil := dk_list.nil dk_string.string.
domain_cons := dk_list.cons dk_string.string.
domain_mem : Label -> Domain -> Bool.
[] domain_mem _ (dk_list.nil _) --> false.
[ l1 : Label,
l2 : Label,
D : Domain ]
domain_mem l1 (dk_list.cons _ l2 D)
-->
or (label_eq l2 l1)
(domain_mem l1 D).
if_uT : b : Bool ->
cc.uT ->
cc.uT ->
cc.uT.
[ A : cc.uT, B : cc.uT ] if_uT dk_bool.true A B --> A
[ A : cc.uT, B : cc.uT ] if_uT dk_bool.false A B --> B.
if_dep : A : cc.uT ->
B : cc.uT ->
b : Bool ->
cc.eT A ->
cc.eT B ->
cc.eT (if_uT b A B).
[ A : cc.uT,
B : cc.uT,
a : cc.eT A ]
if_dep A B true a _ --> a
[ A : cc.uT,
B : cc.uT,
b : cc.eT B ]
if_dep A B false _ b --> b.
label_eq_sym : l1 : Label ->
l2 : Label ->
Istrue (label_eq l1 l2) ->
Istrue (label_eq l2 l1).
[ l : Label ] label_eq_sym l l _ --> tt.
label_diff_sym : l1 : Label ->
l2 : Label ->
Istrue (not (label_eq l1 l2)) ->
Istrue (not (label_eq l2 l1)).
[ c : dk_char.Char, l : Label ]
label_diff_sym (dk_list.cons _ c l) (dk_list.nil _) _
-->
tt
[ c : dk_char.Char, l : Label ]
label_diff_sym (dk_list.nil _) (dk_list.cons _ c l) _
-->
tt
[ c : dk_char.Char,
l1 : Label,
l2 : Label,
H : Istrue (not (label_eq l1 l2)) ]
label_diff_sym (dk_list.cons _ c l1) (dk_list.cons _ c l2) H
-->
label_diff_sym l1 l2 H.
if_label_eq_diff : P : (Label -> cc.uT) ->
l1 : Label ->
l2 : Label ->
cc.eT (P l1) ->
(Istrue (not (label_eq l2 l1)) -> cc.eT (P l2)) ->
cc.eT (P l2).
[ P : (Label -> cc.uT),
l1 : Label,
l2 : Label,
Heq : cc.eT (P l1),
Hdiff : (Istrue (not (label_eq l2 l1)) -> cc.eT (P l2)) ]
if_label_eq_diff P l1 l2 Heq Hdiff
-->
dk_bool.match
(b : Bool =>
cc.Arrow (cc.Arrow (dk_logic.eeP (dk_logic.ebP b)) (P l2))
(cc.Arrow (cc.Arrow (dk_logic.eeP (dk_logic.ebP (not b)))
(P l2)) (P l2)))
(H1 : (dk_logic.TrueT -> cc.eT (P l2)) =>
H2 : (dk_logic.FalseT -> cc.eT (P l2)) =>
H1 dk_logic.I)
(H1 : (dk_logic.FalseT -> cc.eT (P l2)) =>
H2 : (dk_logic.TrueT -> cc.eT (P l2)) =>
H2 dk_logic.I)
(label_eq l2 l1)
(H : Istrue (label_eq l2 l1) =>
label_eq_rect l1 l2 P H Heq)
Hdiff.
domain_mem_cons : l1 : Label ->
l2 : Label ->
D : Domain ->
Istrue (domain_mem l1 D) ->
Istrue (domain_mem l1 (domain_cons l2 D)).
[ l1 : Label,
l2 : Label,
D : Domain,
H : Istrue (domain_mem l1 D) ]
domain_mem_cons l1 l2 D H
-->
dk_logic.bool_or_intro2
(label_eq l2 l1)
(domain_mem l1 D)
H.
(; Object types ;)
ObjType : Type. (; ObjType := list (Label * ObjType) ;)
Ot_nil : ObjType.
Ot_cons : Label -> ObjType -> ObjType -> ObjType.
Ot_if : Bool -> ObjType -> ObjType -> ObjType.
[ A : ObjType, B : ObjType ] Ot_if dk_bool.true A B --> A
[ A : ObjType, B : ObjType ] Ot_if dk_bool.false A B --> B.
Ot_assoc : ObjType -> Label -> ObjType.
[ l1 : Label,
l2 : Label,
A : ObjType,
B : ObjType]
Ot_assoc (Ot_cons l2 A B) l1
-->
Ot_if
(label_eq l1 l2)
A
(Ot_assoc B l1).
Ot_domain : ObjType -> Domain.
[] Ot_domain Ot_nil --> domain_nil
[ l : Label,
A : ObjType ]
Ot_domain (Ot_cons l _ A)
-->
domain_cons l (Ot_domain A).
Ot_eq : ObjType -> ObjType -> Bool.
[ A : ObjType ] Ot_eq A A --> true
[ l1 : Label,
A1 : ObjType,
B1 : ObjType,
l2 : Label,
A2 : ObjType,
B2 : ObjType ]
Ot_eq (Ot_cons l1 A1 B1)
(Ot_cons l2 A2 B2)
-->
and
(label_eq l1 l2)
(and
(Ot_eq A1 A2)
(Ot_eq B1 B2))
[] Ot_eq Ot_nil (Ot_cons _ _ _) --> false
[] Ot_eq (Ot_cons _ _ _) Ot_nil --> false.
Ot_has_key : ObjType -> Label -> Bool
:=
A : ObjType =>
l : Label =>
domain_mem l (Ot_domain A).
(; Ot_st A B := A <: B ;)
Ot_st : ObjType -> ObjType -> Bool.
[ A : ObjType ] Ot_st A A --> true
[] Ot_st _ Ot_nil --> true
[ B1 : ObjType,
l2 : Label,
A2 : ObjType,
B2 : ObjType ]
Ot_st B1 (Ot_cons l2 A2 B2)
-->
and
(Ot_eq A2 (Ot_assoc B1 l2))
(Ot_st B1 B2).
(; Expressions, methods and objects ;)
expr : ObjType -> cc.uT.
Expr : ObjType -> Type.
[ A : ObjType ] Expr A --> cc.eT (expr A).
preObj : ObjType -> (Label -> ObjType) -> Domain -> cc.uT.
PreObj : ObjType -> (Label -> ObjType) -> Domain -> Type.
[ A : ObjType,
f : Label -> ObjType,
D : Domain ] PreObj A f D --> cc.eT (preObj A f D).
Po_nil : A : ObjType ->
f : (Label -> ObjType) ->
PreObj A f 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 (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 => cc.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 (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_list.nil _)
-->
Po_nil B (Ot_assoc A)
[ A : ObjType,
B : ObjType,
o : Expr A,
l2 : Label,
C : Domain ]
precast A B o (dk_list.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).
Ot_if_diff : b : Bool ->
Istrue (not b) ->
A : ObjType ->
B : ObjType ->
Istrue (Ot_eq (Ot_if b A B) B).
[ A : ObjType, B : ObjType ] Ot_if_diff false _ A B --> tt.
Ot_eq_trans : A : ObjType ->
B : ObjType ->
C : ObjType ->
Istrue (Ot_eq A B) ->
Istrue (Ot_eq B C) ->
Istrue (Ot_eq A C).
[ A : ObjType ] Ot_eq_trans A A A _ _ --> tt.
assoc_subtype : A : ObjType ->
B : ObjType ->
l : Label ->
Istrue (Ot_st A B) ->
Istrue (Ot_has_key B l) ->
Istrue (Ot_eq (Ot_assoc B l)
(Ot_assoc A l)).
[ A : ObjType,
l : Label,
refl : Istrue true ]
assoc_subtype A A l refl _ --> tt
[ l2 : Label,
A2 : ObjType,
B2 : ObjType,
l1 : Label,
B1 : ObjType,
st : Istrue (and (Ot_eq A2 (Ot_assoc B1 l2)) (Ot_st B1 B2)),
hk : Istrue (or (label_eq l2 l1) (Ot_has_key B2 l1))]
assoc_subtype B1 (Ot_cons l2 A2 B2) l1 st hk
-->
if_label_eq_diff
(l : Label => dk_logic.eeP (dk_logic.ebP
(Ot_eq (Ot_assoc (Ot_cons l2 A2 B2) l)
(Ot_assoc B1 l))))
l2 l1
(and_elim1
(Ot_eq A2 (Ot_assoc B1 l2))
(Ot_st B1 B2)
st)
(Hdiff : Istrue (not (label_eq l1 l2)) =>
Ot_eq_trans
(Ot_assoc (Ot_cons l2 A2 B2) l1)
(Ot_assoc B2 l1)
(Ot_assoc B1 l1)
(Ot_if_diff
(label_eq l1 l2)
Hdiff
A2
(Ot_assoc B2 l1))
(assoc_subtype
B1
B2
l1
(and_elim2
(Ot_eq A2 (Ot_assoc B1 l2))
(Ot_st B1 B2)
st)
(not_or_elim
(label_eq l2 l1)
(Ot_has_key B2 l1)
(label_diff_sym l1 l2 Hdiff)
hk))).
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) 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 (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_list.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 =>
cc.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_list.nil _)
-->
Po_nil A (Ot_assoc A)
[ A : ObjType,
l : Label,
C : Domain ]
preinit A (dk_list.cons _ l C)
-->
Po_cons
A
(Ot_assoc A)
C
l
(self : Expr A => select A self l)
(preinit A C).
init : A : ObjType -> Expr A
:= A : ObjType =>
make A (preinit A (Ot_domain A)).
coerce : A : ObjType ->
B : ObjType ->
Istrue (Ot_st A B) ->
Expr A ->
Expr B
:=
A : ObjType =>
B : ObjType =>
H : Istrue (Ot_st A B) =>
o : Expr A =>
make B
(Ot_eq_po
B
A
B
(Ot_domain B)
(l : Label =>
assoc_subtype A B l H)
(ocast A B o)).
#NAME dk_obj_examples
Label := dk_obj.Label.
type := dk_obj.ObjType.
type_cons := dk_obj.Ot_cons.
type_nil := dk_obj.Ot_nil.
Expr := dk_obj.Expr.
(; Booleans ;)
l_if : Label
:=
dk_string.cons dk_char.i (
dk_string.cons dk_char.f (
dk_string.nil)).
l_then : Label
:=
dk_string.cons dk_char.t (
dk_string.cons dk_char.h (
dk_string.cons dk_char.e (
dk_string.cons dk_char.n (
dk_string.nil)))).
l_else : Label
:=
dk_string.cons dk_char.e (
dk_string.cons dk_char.l (
dk_string.cons dk_char.s (
dk_string.cons dk_char.e (
dk_string.nil)))).
boolT : A : type -> type
:=
A : type =>
type_cons
l_if
A
(type_cons
l_then
A
(type_cons
l_else
A
type_nil)).
BoolT : A : type -> Type
:= A : type => Expr (boolT A).
trueT : A : type -> BoolT A
:= A : type =>
dk_obj.update
(boolT A)
(dk_obj.init (boolT A))
l_if
(self : BoolT A =>
dk_obj.select
(boolT A)
self l_then).
falseT : A : type -> BoolT A
:= A : type =>
dk_obj.update
(boolT A)
(dk_obj.init (boolT A))
l_if
(self : BoolT A =>
dk_obj.select
(boolT A)
self l_else).
ifT : A : type ->
BoolT A ->
Expr A ->
Expr A ->
Expr A
:=
A : type =>
b : BoolT A =>
then : Expr A =>
else : Expr A =>
dk_obj.select
(boolT A)
(dk_obj.update
(boolT A)
(dk_obj.update
(boolT A)
b
l_then