Commit 1cf4aa30 authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

Also recurse on the position in the Dedukti side.

Even for Assoc, which is a bit heavy but works well.

coerce is now a smart constructor.

Examples pass.
parent 64bcaa10
......@@ -7,16 +7,17 @@ Arrow := pts.Arrow.
Bool := dk_bool.Bool.
true : Bool := dk_bool.true.
false : Bool := dk_bool.false.
not : Bool -> Bool := dk_bool.not.
or : Bool -> Bool -> Bool
:= dk_bool.or.
Prop := dk_logic.Prop.
proof := dk_logic.eP.
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.
......@@ -30,29 +31,61 @@ if_label_eq := dk_string.if_eq.
Domain : Type.
nil : Domain.
cons : Label -> Domain -> Domain.
mem : Label -> Domain -> Bool.
[ l : Label ] mem l nil --> false.
[ l1 : Label,
l2 : Label,
D : Domain ]
mem l1 (cons l2 D)
(; Membership as predicate. ;)
position : Label -> Domain -> uT.
Position : Label -> Domain -> Type.
[ l : Label, D : Domain ] Position l D --> eT (position l D).
Position_head : l : Label -> d : Domain -> Position l (cons l d).
Position_tail : l : Label ->
l2 : Label ->
d : Domain ->
Position l d ->
Position l (cons l2 d).
Subset : Domain -> Domain -> Type.
[ A : Domain,
B : Domain ]
Subset A B
-->
or (label_eq l2 l1)
(mem l1 D).
l : Label ->
Position l A ->
Position l B.
(; Position and membership ;)
mem : l : Label -> d : Domain -> Bool.
[ l : Label ] mem l nil --> false
[ l1 : Label, l2 : Label, d : Domain ]
mem l1 (cons l2 d)
-->
or (label_eq l1 l2)
(mem l1 d).
mem_cons : l1 : Label ->
mem_diff : l1 : Label ->
l2 : Label ->
D : Domain ->
Istrue (mem l1 D) ->
Istrue (mem l1 (cons l2 D)).
Istrue (not (label_eq l1 l2)) ->
Istrue (mem l1 (cons l2 D)) ->
Istrue (mem l1 D).
[ l1 : Label,
l2 : Label,
D : Domain,
H : Istrue (mem l1 D) ]
mem_cons l1 l2 D H
H1 : Istrue (not (label_eq l1 l2)),
H12 : Istrue (mem l1 (cons l2 D)) ]
mem_diff l1 l2 D H1 H12
-->
dk_logic.bool_or_elim1 (label_eq l1 l2) (mem l1 D) H1 H12.
mem_pos : l : Label -> d : Domain -> Istrue (mem l d) -> Position l d.
[ l1 : Label, l2 : Label, d : Domain, H : Istrue (mem l1 (cons l2 d)) ]
mem_pos l1 (cons l2 d) H
-->
bool_or_intro2
(label_eq l2 l1)
(mem l1 D)
H.
dk_string.if_eq_diff
(l : Label => position l1 (cons l d))
l1
l2
(Position_head l1 d)
(Hdiff : Istrue (not (label_eq l2 l1)) =>
Position_tail l1 l2 d
(mem_pos l1 d (mem_diff l1 l2 d (dk_string.diff_sym l2 l1 Hdiff) H))).
......@@ -25,6 +25,14 @@ Istrue : Bool -> Type := b : Bool => eP (ebP b).
I : Istrue true.
False_elim : A : uT -> Istrue false -> eT A.
bool_and_intro : b1 : Bool ->
b2 : Bool ->
Istrue b1 ->
Istrue b2 ->
Istrue (dk_bool.and b1 b2).
[ H1 : Istrue true, H2 : Istrue true ]
bool_and_intro dk_bool.true dk_bool.true H1 H2 --> I.
bool_and_elim1 : b1 : Bool ->
b2 : Bool ->
Istrue (dk_bool.and b1 b2) ->
......@@ -60,6 +68,16 @@ bool_or_intro2 : b1 : Bool ->
[ b : Bool, H : Istrue b ]
bool_or_intro2 dk_bool.false b H --> H.
bool_or_elim1 : b1 : Bool ->
b2 : Bool ->
Istrue (dk_bool.not b1) ->
Istrue (dk_bool.or b1 b2) ->
Istrue b2.
[ b : Bool, H1 : Istrue false, H12 : Istrue true ]
bool_or_elim1 dk_bool.true b H1 H12 --> False_elim (istrue b) H1.
[ b : Bool, H1 : Istrue true, H12 : Istrue b ]
bool_or_elim1 dk_bool.false b H1 H12 --> H12.
not_or_elim : b1 : Bool ->
b2 : Bool ->
Istrue (dk_bool.not b1) ->
......
......@@ -30,24 +30,24 @@ 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.
domain_nil := dk_domain.nil.
domain_cons := dk_domain.cons.
domain_pos := dk_domain.Position.
domain_pos_hd := dk_domain.Position_head.
domain_pos_tl := dk_domain.Position_tail.
(; 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_domain_subtype := dk_type.domain_subtype.
Ot_assoc_subtype := dk_type.assoc_subtype.
(; Expressions, methods and objects ;)
......@@ -55,249 +55,295 @@ 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.
preObj : ObjType -> Domain -> uT.
PreObj : ObjType -> Domain -> Type.
[ A : ObjType,
f : Label -> ObjType,
D : Domain ] PreObj A f D --> eT (preObj A f D).
D : Domain ] PreObj A D --> eT (preObj A D).
Po_nil : A : ObjType ->
f : (Label -> ObjType) ->
PreObj A f dk_domain.nil.
PreObj A 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).
H : domain_pos l (Ot_domain A) ->
(Expr A -> Expr (Ot_assoc A l H)) ->
PreObj A D ->
PreObj A (dk_domain.cons l D).
mem_cons := A : ObjType =>
D : Domain =>
l : Label =>
H : Istrue (dk_domain.mem l (Ot_domain A)) =>
Po_cons A D l (dk_domain.mem_pos l (Ot_domain A) H).
preselect : A : ObjType ->
f : (Label -> ObjType) ->
D : Domain ->
o : PreObj A f D ->
o : PreObj A D ->
l : Label ->
H : dk_domain.Subset D (Ot_domain A) ->
Hd: domain_pos l D ->
Expr A ->
Expr (f l).
Expr (Ot_assoc A l (H l Hd)).
[ A : ObjType,
D : Domain,
l : Label,
Hsub : dk_domain.Subset (dk_domain.cons l D) (Ot_domain A),
m : Expr A -> Expr (Ot_assoc A l (Hsub l (dk_domain.Position_head l D))),
o : PreObj A D ]
preselect
A
(dk_domain.cons l D)
(Po_cons A D l {Hsub l (dk_domain.Position_head l D)} m o)
l
Hsub
(dk_domain.Position_head l D)
-->
m
[ A : ObjType,
f : Label -> ObjType,
D : Domain,
l1 : Label,
m : Expr A -> Expr (f l1),
o : PreObj A f D,
l2 : Label ]
preselect A f (dk_domain.cons l1 D) (Po_cons A f D l1 m o) l2
l : Label,
l2 : Label,
H : domain_pos l2 (Ot_domain A),
m : Expr A -> Expr (Ot_assoc A l2 H),
o : PreObj A D,
Hsub : dk_domain.Subset (dk_domain.cons l2 D) (Ot_domain A),
Htl : domain_pos l D ]
preselect
A
(dk_domain.cons l2 D)
(Po_cons A D l2 H m o)
l
Hsub
(dk_domain.Position_tail l l2 D Htl)
-->
if_label_eq
(l : Label => Arrow (expr A) (expr (f l)))
l1
l2
m
(preselect A f D o l2).
preselect A D o l
(l3 : Label =>
Hp : domain_pos l3 D =>
Hsub l3 (dk_domain.Position_tail l3 l2 D Hp))
Htl.
preupdate : A : ObjType ->
f : (Label -> ObjType) ->
D : Domain ->
o : PreObj A f D ->
o : PreObj A D ->
l : Label ->
(Expr A -> Expr (f l)) ->
PreObj A f D.
Hsub : dk_domain.Subset D (Ot_domain A) ->
Hp: domain_pos l D ->
(Expr A -> Expr (Ot_assoc A l (Hsub l Hp))) ->
PreObj A D.
[ A : ObjType,
D : Domain,
l : Label,
Hsub : dk_domain.Subset (dk_domain.cons l D) (Ot_domain A),
m1 : Expr A -> Expr (Ot_assoc A l (Hsub l (dk_domain.Position_head l D))),
o : PreObj A D,
m2 : Expr A -> Expr (Ot_assoc A l (Hsub l (dk_domain.Position_head l D))) ]
preupdate
A
(dk_domain.cons l D)
(Po_cons A D l {Hsub l (dk_domain.Position_head l D)} m1 o)
l
Hsub
(dk_domain.Position_head l D)
m2
-->
Po_cons A D l (Hsub l (dk_domain.Position_head l D)) m2 o
[ A : ObjType,
f : Label -> ObjType,
D : Domain,
l1 : Label,
m1 : Expr A -> Expr (f l1),
o : PreObj A f D,
l : Label,
l2 : Label,
m2 : Expr A -> Expr (f l2) ]
preupdate A f (dk_domain.cons l1 D) (Po_cons A f D l1 m1 o) l2 m2
H : domain_pos l D,
Hsub : dk_domain.Subset (dk_domain.cons l2 D) (Ot_domain A),
m2 : Expr A -> Expr (Ot_assoc A l (Hsub l (dk_domain.Position_tail l l2 D H))),
m1 : Expr A -> Expr (Ot_assoc A l2 (Hsub l2 (dk_domain.Position_head l2 D))),
o : PreObj A D ]
preupdate
A
(dk_domain.cons l2 D)
(Po_cons A D l2 {Hsub l2 (dk_domain.Position_head l2 D)} m1 o)
l
Hsub
(dk_domain.Position_tail l l2 D H)
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)).
Po_cons A D l2 (Hsub l2 (dk_domain.Position_head l2 D))
m1
(preupdate A D o l
(l3 : Label =>
Hp : domain_pos l3 D =>
Hsub l3 (dk_domain.Position_tail l3 l2 D Hp))
H
m2).
[ A : ObjType ] expr A --> preObj A (Ot_assoc A) (Ot_domain A).
[ A : ObjType ] expr A --> preObj A (Ot_domain A).
select : A : ObjType ->
eA : Expr A ->
l : Label ->
Expr (Ot_assoc A l).
obj_select : A : ObjType ->
eA : Expr A ->
l : Label ->
H : domain_pos l (Ot_domain A) ->
Expr (Ot_assoc A l H).
[ A : ObjType,
o : Expr A,
l : Label ]
select A o l
l : Label,
H : domain_pos l (Ot_domain A) ]
obj_select A o l H
-->
preselect
A
(Ot_assoc A)
(Ot_domain A)
o
l
(l : Label => Hpos : domain_pos l (Ot_domain A) => Hpos)
H
o.
update : A : ObjType ->
select : A : ObjType ->
eA : Expr A ->
l : Label ->
(Expr A -> Expr (Ot_assoc A l)) ->
Expr A.
H : domain_pos l (Ot_domain A) ->
Expr (Ot_assoc A l H).
[ l2 : Label,
A : ObjType,
B : ObjType,
Hpos : domain_pos l2 (domain_cons l2 (Ot_domain B)),
m : Expr (Ot_cons l2 A B) -> Expr (Ot_assoc (Ot_cons l2 A B) l2 Hpos),
po : PreObj (Ot_cons l2 A B) (Ot_domain B),
l : Label,
H : domain_pos l (domain_cons l2 (Ot_domain B)) ]
select (dk_type.cons l2 A B) (Po_cons {Ot_cons l2 A B} {Ot_domain B} l2 Hpos m po) l H
-->
obj_select (Ot_cons l2 A B) (Po_cons (Ot_cons l2 A B) (Ot_domain B) l2 Hpos m po) l H.
mem_select := A : ObjType =>
eA : Expr A =>
l : Label =>
H : Istrue (dk_domain.mem l (Ot_domain A)) =>
select A eA l (dk_domain.mem_pos l (Ot_domain A) H).
obj_update : A : ObjType ->
eA : Expr A ->
l : Label ->
H : domain_pos l (Ot_domain A) ->
(Expr A -> Expr (Ot_assoc A l H)) ->
Expr A.
[A : ObjType,
o : Expr A,
l : Label,
m : Expr A -> Expr (Ot_assoc A l)]
update A o l m
H : domain_pos l (Ot_domain A),
m : Expr A -> Expr (Ot_assoc A l H) ]
obj_update A o l H m
-->
preupdate
A
(Ot_assoc A)
(Ot_domain A)
o
l
(l : Label => Hpos : domain_pos l (Ot_domain A) => Hpos)
H
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,
update : A : ObjType ->
eA : Expr A ->
l : Label ->
H : domain_pos l (Ot_domain A) ->
(Expr A -> Expr (Ot_assoc A l H)) ->
Expr A.
[ l2 : Label,
A : ObjType,
B : ObjType,
m : Expr A -> Expr B,
H : Istrue true ] meth_eq A B B H 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,
H : (l : Label ->
Istrue (domain_mem l dk_domain.nil) ->
Istrue (Ot_eq (Ot_assoc B2 l) (Ot_assoc B1 l))) ]
Ot_eq_po A B1 B2 dk_domain.nil H (Po_nil A { Ot_assoc B1 })
-->
Po_nil A (Ot_assoc B2)
[ A : ObjType,
B1 : ObjType,
B2 : ObjType,
C : Domain,
Hpos : domain_pos l2 (domain_cons l2 (Ot_domain B)),
m : Expr (Ot_cons l2 A B) -> Expr (Ot_assoc (Ot_cons l2 A B) l2 Hpos),
po : PreObj (Ot_cons l2 A B) (Ot_domain B),
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 A { Ot_assoc B1 } C l m o)
H : domain_pos l (domain_cons l2 (Ot_domain B)),
m2 : Expr (Ot_cons l2 A B) -> Expr (Ot_assoc (Ot_cons l2 A B) l H) ]
update (dk_type.cons l2 A B) (Po_cons {Ot_cons l2 A B} {Ot_domain B} l2 Hpos m po) l H m2
-->
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).
obj_update (Ot_cons l2 A B) (Po_cons (Ot_cons l2 A B) (Ot_domain B) l2 Hpos m po) l H m2.
mem_update := A : ObjType =>
eA : Expr A =>
l : Label =>
H : Istrue (dk_domain.mem l (Ot_domain A)) =>
update A eA l (dk_domain.mem_pos l (Ot_domain A) H).
(; Subtyping ;)
preinit : A : ObjType ->
C : Domain ->
PreObj A (Ot_assoc A) C.
[ A : ObjType ]
preinit A dk_domain.nil
Hsub : dk_domain.Subset C (Ot_domain A) ->
PreObj A C.
[ A : ObjType,
Hsub : dk_domain.Subset dk_domain.nil (Ot_domain A) ]
preinit A dk_domain.nil Hsub
-->
Po_nil A (Ot_assoc A)
Po_nil A
[ A : ObjType,
l : Label,
C : Domain ]
preinit A (dk_domain.cons l C)
C : Domain,
Hsub : dk_domain.Subset (dk_domain.cons l C) (Ot_domain A) ]
preinit A (dk_domain.cons l C) Hsub
-->
Po_cons
A
(Ot_assoc A)
C
l
(self : Expr A => select A self l)
(preinit A C).
(Hsub l (domain_pos_hd l C))
(self : Expr A => select A self l (Hsub l (domain_pos_hd l C)))
(preinit A C
(l2 : Label => H : domain_pos l2 C => Hsub l2 (domain_pos_tl l2 l C H))).
init : A : ObjType -> Expr A
:= A : ObjType =>
preinit A (Ot_domain A).
preinit A (Ot_domain A) (l : Label => H : domain_pos l (Ot_domain A) => H).
eq_coerce : A : ObjType ->
B : ObjType ->
Istrue (Ot_eq A B) ->
Expr A ->
Expr B.
[ A : ObjType, H : Istrue true, a : Expr A ] eq_coerce A A H a --> a.
coerce : A : ObjType ->
B : ObjType ->
Istrue (Ot_st A B) ->
Ot_st A B ->
Expr A ->
Expr B
:=
A : ObjType =>
B : ObjType =>
H : Istrue (Ot_st A B) =>
o : Expr A =>
Ot_eq_po
B
A
B
(Ot_domain B)
(l : Label =>
Ot_assoc_subtype A B l H)
(ocast A B o).
Expr B.
[ A : ObjType,
B : ObjType,
st : Ot_st A B,
a : Expr A,
l : Label,
dp : domain_pos l (Ot_domain B) ]
select B (coerce A B st a) l dp
-->
eq_coerce
(Ot_assoc A l (Ot_domain_subtype A B st l dp))
(Ot_assoc B l dp)
(Ot_assoc_subtype A B l st dp)
(select A a l (Ot_domain_subtype A B st l dp)).
[ A : ObjType,
B : ObjType,
st : Ot_st A B,
a : Expr A,
l : Label,
dp : domain_pos l (Ot_domain B),
m : Expr B -> Expr (Ot_assoc B l dp) ]
update B (coerce A B st a) l dp m
-->
coerce A B st
(update A a l (Ot_domain_subtype A B st l dp)
(self : Expr A =>
eq_coerce
(Ot_assoc B l dp)
(Ot_assoc A l (Ot_domain_subtype A B st l dp))
(dk_type.assoc_subtype_sym A B l st dp)
(m (coerce A B st self)))).
[ A : ObjType, B : ObjType, C : ObjType,
stAB : Ot_st A B, stBC : Ot_st B C,
a : Expr A ]
coerce B C stBC (coerce A B stAB a)
-->
coerce A C (dk_type.st_trans A B C stAB stBC) a.
......@@ -55,25 +55,27 @@ BoolT : A : type -> Type
trueT : A : type -> BoolT A
:= A : type =>
dk_obj.update
dk_obj.mem_update
(boolT A)
(dk_obj.init (boolT A))
l_if
dk_logic.I
(self : BoolT A =>
dk_obj.select
dk_obj.mem_select
(boolT A)
self l_then).
self l_then dk_logic.I).
falseT : A : type -> BoolT A
:= A : type =>
dk_obj.update
dk_obj.mem_update
(boolT A)
(dk_obj.init (boolT A))