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

[Dk] From dom/assoc to a ternary position relation

Decidability is replacedby a non-confluent non-linear rewrite-system
parent 13e46332
...@@ -74,7 +74,7 @@ depend: .depend ...@@ -74,7 +74,7 @@ depend: .depend
$(SKDEP) $(DKDEPOPTIONS) $(SKS) > .depend $(SKDEP) $(DKDEPOPTIONS) $(SKS) > .depend
clean: clean:
rm -rf *.dko pts.dk dk_*.dk *.vo *.glob .depend tmp.* \ rm -rf *.dko dk_*.dk *.vo *.glob .depend tmp.* \
test.sk test.v \ test.sk test.v \
sigmaid sigmaid.native sigmaid.byte _build sigmaid sigmaid.native sigmaid.byte _build
......
#NAME dk_bool.
(;
Copyright Raphaël Cauderlier (2014)
<raphael.cauderlier@inria.fr>
This software is a computer program whose purpose is to translate object-oriented program written in the simply-typed ς-calculus from Abadi and Cardelli to Dedukti and Coq.
This software is governed by the CeCILL-B license under French law and
abiding by the rules of distribution of free software. You can use,
modify and/ or redistribute the software under the terms of the CeCILL-B
license as circulated by CEA, CNRS and INRIA at the following URL
"http://www.cecill.info".
As a counterpart to the access to the source code and rights to copy,
modify and redistribute granted by the license, users are provided
only with a limited warranty and the software's author, the holder of
the economic rights, and the successive licensors have only limited
liability.
In this respect, the user's attention is drawn to the risks associated
with loading, using, modifying and/or developing or reproducing the
software by the user in light of its specific status of free software,
that may mean that it is complicated to manipulate, and that also
therefore means that it is reserved for developers and experienced
professionals having in-depth computer knowledge. Users are therefore
encouraged to load and test the software's suitability as regards
their requirements in conditions enabling the security of their
systems and/or data to be ensured and, more generally, to use and
operate it in the same conditions as regards security.
The fact that you are presently reading this means that you have had
knowledge of the CeCILL-B license and that you accept its terms.
;)
(; Bool ;)
(; Declaration ;)
bool : Type.
(; Constructors ;)
true : bool.
false : bool.
(; Pattern-matching ;)
def match :
P : (bool -> pts.uT) ->
pts.eT (P true) ->
pts.eT (P false) ->
b : bool ->
pts.eT (P b).
[H] match _ H _ true --> H
[H] match _ _ H false --> H.
(; boolean if .. then .. else .. ;)
def iteb : bool -> bool -> bool -> bool.
[b] iteb true b _ --> b
[b] iteb false _ b --> b.
(; negation ;)
def not : bool -> bool.
[b] not b --> iteb b false true.
(; binary operators ;)
def and : bool -> bool -> bool.
[x,y] and x y --> iteb x y false.
def or : bool -> bool -> bool.
[x,y] or x y --> iteb x true y.
#NAME dk_char.
(;
Copyright Raphaël Cauderlier (2014)
<raphael.cauderlier@inria.fr>
This software is a computer program whose purpose is to translate object-oriented program written in the simply-typed ς-calculus from Abadi and Cardelli to Dedukti and Coq.
This software is governed by the CeCILL-B license under French law and
abiding by the rules of distribution of free software. You can use,
modify and/ or redistribute the software under the terms of the CeCILL-B
license as circulated by CEA, CNRS and INRIA at the following URL
"http://www.cecill.info".
As a counterpart to the access to the source code and rights to copy,
modify and redistribute granted by the license, users are provided
only with a limited warranty and the software's author, the holder of
the economic rights, and the successive licensors have only limited
liability.
In this respect, the user's attention is drawn to the risks associated
with loading, using, modifying and/or developing or reproducing the
software by the user in light of its specific status of free software,
that may mean that it is complicated to manipulate, and that also
therefore means that it is reserved for developers and experienced
professionals having in-depth computer knowledge. Users are therefore
encouraged to load and test the software's suitability as regards
their requirements in conditions enabling the security of their
systems and/or data to be ensured and, more generally, to use and
operate it in the same conditions as regards security.
The fact that you are presently reading this means that you have had
knowledge of the CeCILL-B license and that you accept its terms.
;)
(; 7bits (ascii) characters ;)
def equal : char -> char -> dk_bool.bool.
[m,n] equal (char_of_nat m) (char_of_nat n) --> dk_nat.equal m n.
def equal_refl : c : char -> dk_logic.Istrue (equal c c).
[n] equal_refl (char_of_nat n) --> dk_nat.equal_refl n.
def eq_rect : c1 : char ->
c2 : char ->
P : (char -> pts.uT) ->
dk_logic.Istrue (equal c1 c2) ->
pts.eT (P c1) ->
pts.eT (P c2).
[n,m,P,H,x]
eq_rect (char_of_nat n) (char_of_nat m) P H x
-->
dk_nat.eq_rect n m (k : nat => P (char_of_nat k)) H x.
#NAME dk_domain.
(;
Copyright Raphaël Cauderlier (2014)
<raphael.cauderlier@inria.fr>
This software is a computer program whose purpose is to translate object-oriented program written in the simply-typed ς-calculus from Abadi and Cardelli to Dedukti and Coq.
This software is governed by the CeCILL-B license under French law and
abiding by the rules of distribution of free software. You can use,
modify and/ or redistribute the software under the terms of the CeCILL-B
license as circulated by CEA, CNRS and INRIA at the following URL
"http://www.cecill.info".
As a counterpart to the access to the source code and rights to copy,
modify and redistribute granted by the license, users are provided
only with a limited warranty and the software's author, the holder of
the economic rights, and the successive licensors have only limited
liability.
In this respect, the user's attention is drawn to the risks associated
with loading, using, modifying and/or developing or reproducing the
software by the user in light of its specific status of free software,
that may mean that it is complicated to manipulate, and that also
therefore means that it is reserved for developers and experienced
professionals having in-depth computer knowledge. Users are therefore
encouraged to load and test the software's suitability as regards
their requirements in conditions enabling the security of their
systems and/or data to be ensured and, more generally, to use and
operate it in the same conditions as regards security.
The fact that you are presently reading this means that you have had
knowledge of the CeCILL-B license and that you accept its terms.
;)
def uT := pts.uT.
def eT := pts.eT.
def Arrow := pts.Arrow.
def bool := dk_bool.bool.
def true : bool := dk_bool.true.
def false : bool := dk_bool.false.
def not : bool -> bool := dk_bool.not.
def or : bool -> bool -> bool
:= dk_bool.or.
def Prop := dk_logic.Prop.
def proof := dk_logic.eP.
def Istrue := dk_logic.Istrue.
def tt : Istrue true := dk_logic.I.
def bool_or_intro2 := dk_logic.bool_or_intro2.
(; Labels ;)
def Label := string.
def label_eq : Label -> Label -> bool := dk_string.equal.
Domain : Type.
dnil : Domain.
dcons : Label -> Domain -> Domain.
(; Membership as predicate. ;)
position : Label -> Domain -> uT.
Position : Label -> Domain -> Type.
[l,D] pts.eT (position l D) --> Position l D.
Position_head : l : Label -> d : Domain -> Position l (dcons l d).
Position_tail : l : Label ->
l2 : Label ->
d : Domain ->
Position l d ->
Position l (dcons l2 d).
def Subset : Domain -> Domain -> Type.
[A,B]
Subset A B
-->
(l : Label ->
Position l A ->
Position l B).
(; Position and membership ;)
def mem : l : Label -> d : Domain -> bool.
[ ] mem _ dnil --> false
[l1,l2,d]
mem l1 (dcons l2 d)
-->
or (label_eq l1 l2)
(mem l1 d).
def mem_diff : l1 : Label ->
l2 : Label ->
D : Domain ->
Istrue (not (label_eq l1 l2)) ->
Istrue (mem l1 (dcons l2 D)) ->
Istrue (mem l1 D).
[l1,l2,D,H1,H12]
mem_diff l1 l2 D H1 H12
-->
dk_logic.bool_or_elim1 (label_eq l1 l2) (mem l1 D) H1 H12.
def mem_pos : l : Label -> d : Domain -> Istrue (mem l d) -> Position l d.
[l1,l2,d,H]
mem_pos l1 (dcons l2 d) H
-->
dk_string.if_eq_diff
(l : Label => position l1 (dcons l d))
l1
l2
(Position_head l1 d)
(Hdiff : Istrue (not (label_eq l1 l2)) =>
Position_tail l1 l2 d
(mem_pos l1 d (mem_diff l1 l2 d Hdiff H))).
#NAME dk_logic.
(;
Copyright Raphaël Cauderlier (2014)
<raphael.cauderlier@inria.fr>
This software is a computer program whose purpose is to translate object-oriented program written in the simply-typed ς-calculus from Abadi and Cardelli to Dedukti and Coq.
This software is governed by the CeCILL-B license under French law and
abiding by the rules of distribution of free software. You can use,
modify and/ or redistribute the software under the terms of the CeCILL-B
license as circulated by CEA, CNRS and INRIA at the following URL
"http://www.cecill.info".
As a counterpart to the access to the source code and rights to copy,
modify and redistribute granted by the license, users are provided
only with a limited warranty and the software's author, the holder of
the economic rights, and the successive licensors have only limited
liability.
In this respect, the user's attention is drawn to the risks associated
with loading, using, modifying and/or developing or reproducing the
software by the user in light of its specific status of free software,
that may mean that it is complicated to manipulate, and that also
therefore means that it is reserved for developers and experienced
professionals having in-depth computer knowledge. Users are therefore
encouraged to load and test the software's suitability as regards
their requirements in conditions enabling the security of their
systems and/or data to be ensured and, more generally, to use and
operate it in the same conditions as regards security.
The fact that you are presently reading this means that you have had
knowledge of the CeCILL-B license and that you accept its terms.
;)
def uT := pts.uT.
def eT := pts.eT.
def Pi := pts.Pi.
def Arrow := pts.Arrow.
def bool := dk_bool.bool.
def true := dk_bool.true.
def false := dk_bool.false.
(; Impredicative prop ;)
prop : uT.
def Prop : Type := eT prop.
ebP : dk_bool.bool -> Prop.
eeP : Prop -> uT.
def eP : Prop -> Type
:= f : Prop => eT (eeP f).
def istrue : bool -> uT := b : bool => eeP (ebP b).
def Istrue : bool -> Type := b : bool => eP (ebP b).
I : Istrue true.
False_elim : A : uT -> Istrue false -> eT A.
def bool_and_intro : b1 : bool ->
b2 : bool ->
Istrue b1 ->
Istrue b2 ->
Istrue (dk_bool.and b1 b2).
[ ]
bool_and_intro dk_bool.true dk_bool.true _ _ --> I.
def bool_and_elim1 : b1 : bool ->
b2 : bool ->
Istrue (dk_bool.and b1 b2) ->
Istrue b1.
[ ]
bool_and_elim1 dk_bool.true _ _
-->
I
[H]
bool_and_elim1 dk_bool.false _ H
-->
H.
def bool_and_elim2 : b1 : bool ->
b2 : bool ->
Istrue (dk_bool.and b1 b2) ->
Istrue b2.
[H]
bool_and_elim2 dk_bool.true _ H
-->
H
[b,H]
bool_and_elim2 dk_bool.false b H
-->
False_elim (istrue b) H.
def bool_or_intro2 : b1 : bool ->
b2 : bool ->
Istrue b2 ->
Istrue (dk_bool.or b1 b2).
[ ]
bool_or_intro2 dk_bool.true _ _ --> I
[H]
bool_or_intro2 dk_bool.false _ H --> H.
def bool_or_elim1 : b1 : bool ->
b2 : bool ->
Istrue (dk_bool.not b1) ->
Istrue (dk_bool.or b1 b2) ->
Istrue b2.
[b,H1]
bool_or_elim1 dk_bool.true b H1 _ --> False_elim (istrue b) H1.
[H12]
bool_or_elim1 dk_bool.false _ _ H12 --> H12.
def not_or_elim : b1 : bool ->
b2 : bool ->
Istrue (dk_bool.not b1) ->
Istrue (dk_bool.or b1 b2) ->
Istrue b2.
[Hb]
not_or_elim dk_bool.false _ _ Hb --> Hb.
#NAME dk_nat.
(;
Copyright Raphaël Cauderlier (2014)
<raphael.cauderlier@inria.fr>
This software is a computer program whose purpose is to translate object-oriented program written in the simply-typed ς-calculus from Abadi and Cardelli to Dedukti and Coq.
This software is governed by the CeCILL-B license under French law and
abiding by the rules of distribution of free software. You can use,
modify and/ or redistribute the software under the terms of the CeCILL-B
license as circulated by CEA, CNRS and INRIA at the following URL
"http://www.cecill.info".
As a counterpart to the access to the source code and rights to copy,
modify and redistribute granted by the license, users are provided
only with a limited warranty and the software's author, the holder of
the economic rights, and the successive licensors have only limited
liability.
In this respect, the user's attention is drawn to the risks associated
with loading, using, modifying and/or developing or reproducing the
software by the user in light of its specific status of free software,
that may mean that it is complicated to manipulate, and that also
therefore means that it is reserved for developers and experienced
professionals having in-depth computer knowledge. Users are therefore
encouraged to load and test the software's suitability as regards
their requirements in conditions enabling the security of their
systems and/or data to be ensured and, more generally, to use and
operate it in the same conditions as regards security.
The fact that you are presently reading this means that you have had
knowledge of the CeCILL-B license and that you accept its terms.
;)
(; Operations ;)
def equal : nat -> nat -> dk_bool.bool.
[] equal 0 0 --> dk_bool.true
[] equal 0 (S _) --> dk_bool.false
[] equal (S _) 0 --> dk_bool.false
[n,m] equal (S n) (S m) --> equal n m.
def equal_refl : n : nat -> dk_logic.Istrue (equal n n).
[] equal_refl 0 --> dk_logic.I
[n] equal_refl (S n) --> equal_refl n.
def eq_rect : n : nat ->
m : nat ->
P : (nat -> pts.uT) ->
dk_logic.Istrue (equal n m) ->
pts.eT (P n) ->
pts.eT (P m).
[x] eq_rect 0 0 _ _ x --> x
[n,m,P,H,x] eq_rect (S n) (S m) P H x --> eq_rect n m (k : nat => P (S k)) H x.
...@@ -36,92 +36,43 @@ knowledge of the CeCILL-B license and that you accept its terms. ...@@ -36,92 +36,43 @@ knowledge of the CeCILL-B license and that you accept its terms.
;) ;)
def uT := pts.uT.
def eT := pts.eT.
def Arrow := pts.Arrow.
(; TODO: eliminate dependency on cc ;)
(; Have a version of bool independant of cc ;)
(; booleans ;)
def bool := dk_bool.bool.
def true : bool := dk_bool.true.
def false : bool := dk_bool.false.
def not : bool -> bool := dk_bool.not.
def and : bool -> bool -> bool
:= dk_bool.and.
def or : bool -> bool -> bool
:= dk_bool.or.
(; Logic ;)
def Istrue := dk_logic.Istrue.
def tt : Istrue true := dk_logic.I.
(; Labels ;) (; Labels ;)
def Label := string. def label := string.
def label_eq := dk_string.equal.
(; Domains ;)
def Domain := dk_domain.Domain.
def domain_pos := dk_domain.Position.
def domain_pos_hd := dk_domain.Position_head.
def domain_pos_tl := dk_domain.Position_tail.
(; Object types ;) (; Object types ;)
def ObjType := dk_type.type. (; ObjType := list (Label * ObjType) ;) def type := dk_type.type. (; type := list (label * type) ;)
def Ot_nil := dk_type.tnil. def Ot_nil := dk_type.tnil.
def Ot_cons := dk_type.tcons. def Ot_cons := dk_type.tcons.
def Ot_assoc := dk_type.assoc.
def Ot_domain := dk_type.domain.
def Ot_eq := dk_type.eq.
def Ot_st := dk_type.st. def Ot_st := dk_type.st.
def Ot_domain_subtype := dk_type.domain_subtype. def Ot_domain_subtype := dk_type.domain_subtype.
def Ot_assoc_subtype := dk_type.assoc_subtype.
(; Expressions, methods and objects ;) def pos := dk_type.pos.
def expr : ObjType -> uT.
def Expr : ObjType -> Type.
[A] Expr A --> eT (expr A).
preObj : ObjType -> Domain -> uT. (; Expressions, methods and objects ;)
PreObj : ObjType -> Domain -> Type. PreObj : type -> type -> Type.
[A,D] pts.eT (preObj A D) --> PreObj A D. def Expr : type -> Type.
[A] Expr A --> PreObj A A.
[A] expr A --> preObj A (Ot_domain A).
Po_nil : A : type ->
PreObj A Ot_nil.
Po_nil : A : ObjType -> Po_cons : A : type ->
PreObj A dk_domain.dnil. D : type ->
Po_cons : A : ObjType -> l : label ->
D : Domain -> B : type ->
l : Label -> (Expr A -> Expr B) ->
H : domain_pos l (Ot_domain A) ->
(Expr A -> Expr (Ot_assoc A l H)) ->
PreObj A D -> PreObj A D ->
PreObj A (dk_domain.dcons l D). PreObj A (Ot_cons l B D).
def mem_cons := A : ObjType => def preselect : A : type ->
D : Domain => D : type ->
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).
def preselect : A : ObjType ->
D : Domain ->
o : PreObj A D -> o : PreObj A D ->
l : Label -> l : label ->
H : domain_pos l (Ot_domain A) -> B : type ->
Hd: domain_pos l D -> pos l B D ->
Expr A -> Expr A ->
Expr (Ot_assoc A l H). Expr B.
[m,H] [m] preselect _ _ (Po_cons _ _ _ _ m _) _ _ (dk_type.at_head _ _ _) --> m.
preselect _ _ (Po_cons _ _ _ H m _) _ H (dk_domain.Position_head _ _)
-->
m
[A,D,l,l2,o,H,Htl] [A,D,l,l2,o,H,Htl]
preselect preselect
...@@ -130,174 +81,140 @@ def preselect : A : ObjType -> ...@@ -130,174 +81,140 @@ def preselect : A : ObjType ->
(Po_cons A D _ _ _ o) (Po_cons A D _ _ _ o)
l l
H H
(dk_domain.Position_tail _ _ _ Htl) (dk_type.in_tail _ _ _ _ _ Htl)
--> -->
preselect A D o l H Htl. preselect A D o l H Htl.
def preupdate : A : ObjType -> def preupdate : A : type ->
D : Domain -> D : type ->
o : PreObj A D -> o : PreObj A D ->
l : Label -> l : label ->
H : domain_pos l (Ot_domain A) -> B : type ->
Hp: domain_pos l D -> H : pos l B D ->
(Expr A -> Expr (Ot_assoc A l H)) -> (Expr A -> Expr B) ->
PreObj A D. PreObj A D.
[A,D,l,p,o,m2] [A,D,l,B,o,m2]
preupdate preupdate
_ _
_ _
(Po_cons A D l p _ o) (Po_cons A D l B _ o)
_
_ _
p (dk_type.at_head _ _ _)
(dk_domain.Position_head _ _)
m2 m2
--> -->
Po_cons A D l p m2 o Po_cons A D l B m2 o
[A,D,l,l2,H,Hsub,m1,m2,o,Hpos,p] [A,D,l,l2,B,m1,m2,o,p,C]
preupdate preupdate
A _
(dk_domain.dcons l2 D) _
(Po_cons _ _ _ Hpos m1 o) (Po_cons A D l2 B m1 o)
l l
p C
(dk_domain.Position_tail _ _ _ H) (dk_type.in_tail _ _ _ _ _ p)
m2 m2
--> -->
Po_cons A D l2 Hpos m1 (preupdate A D o l p H m2). Po_cons A D l2 B m1 (preupdate A D o l C p m2).
def obj_select : A : ObjType -> def obj_select : A : type ->
eA : Expr A -> eA : Expr A ->
l : Label -> l : label ->
H : domain_pos l (Ot_domain A) -> B : type ->
Expr (Ot_assoc A l H). pos l B A ->
[A,o,l,H] Expr B.
obj_select A o l H [A,o,l,B,p]
obj_select A o l B p
--> -->
preselect preselect
A A