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

Merge branch 'master' of zamok:www/git/dkobj

parents abd86754 817423db
......@@ -31,7 +31,7 @@ Domain : Type.
nil : Domain.
cons : Label -> Domain -> Domain.
mem : Label -> Domain -> Bool.
[] mem _ nil --> false.
[ l : Label ] mem l nil --> false.
[ l1 : Label,
l2 : Label,
D : Domain ]
......
......@@ -66,5 +66,6 @@ not_or_elim : b1 : Bool ->
Istrue (dk_bool.or b1 b2) ->
Istrue b2.
[ b : Bool,
H : Istrue true,
Hb : Istrue b ]
not_or_elim dk_bool.false b _ Hb --> Hb.
not_or_elim dk_bool.false b H Hb --> Hb.
......@@ -22,13 +22,13 @@ zero : N : UNat -> MInt N.
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
equal (dk_nat.S N) (S0 N 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
equal (dk_nat.S N) (S1 N 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
equal (dk_nat.S N) (S0 N n) (S1 N m) --> dk_bool.false
[ N : UNat, n : MInt N, m : MInt N ]
equal _ (S1 _ n) (S0 N m) --> dk_bool.false.
equal (dk_nat.S N) (S1 N n) (S0 N m) --> dk_bool.false.
(; Casting binary natural numbers ;)
......
......@@ -85,7 +85,7 @@ preselect : A : ObjType ->
m : Expr A -> Expr (f l1),
o : PreObj A f D,
l2 : Label ]
preselect _ _ _ (Po_cons A f D l1 m o) l2
preselect A f (dk_domain.cons l1 D) (Po_cons A f D l1 m o) l2
-->
if_label_eq
(l : Label => Arrow (expr A) (expr (f l)))
......@@ -109,7 +109,7 @@ preupdate : A : ObjType ->
o : PreObj A f D,
l2 : Label,
m2 : Expr A -> Expr (f l2) ]
preupdate _ _ _ (Po_cons A f D l1 m1 o) l2 m2
preupdate A f (dk_domain.cons l1 D) (Po_cons A f D l1 m1 o) l2 m2
-->
if_label_eq
(l : Label => preObj A f (dk_domain.cons l D))
......@@ -201,7 +201,8 @@ meth_eq : A : ObjType ->
Expr B2.
[ A : ObjType,
B : ObjType,
m : Expr A -> Expr B ] meth_eq A B B _ m --> m.
m : Expr A -> Expr B,
H : Istrue true ] meth_eq A B B H m --> m.
Ot_eq_po : A : ObjType ->
B1 : ObjType ->
......@@ -215,8 +216,11 @@ Ot_eq_po : A : ObjType ->
[ A : ObjType,
B1 : ObjType,
B2 : ObjType,
o : PreObj A (Ot_assoc B1) dk_domain.nil ]
Ot_eq_po A B1 B2 _ _ (Po_nil _ _)
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,
......@@ -229,7 +233,7 @@ Ot_eq_po : A : ObjType ->
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)
Ot_eq_po A B1 B2 (dk_domain.cons l C) H (Po_cons A (Ot_assoc B1) C l m o)
-->
Po_cons
A
......
......@@ -378,7 +378,9 @@ filtermaptype : (Label -> dk_bool.Bool) ->
(type -> type) ->
type ->
type.
[] filtermaptype _ _ dk_type.nil --> dk_type.nil
[ P : Label -> dk_bool.Bool,
f : type -> type ]
filtermaptype P f dk_type.nil --> dk_type.nil
[ P : Label -> dk_bool.Bool,
f : type -> type,
l : Label,
......
......@@ -19,8 +19,8 @@ cons : Char -> String -> String.
equal : String -> String -> Bool.
[ s : String ] equal s s --> true
[ ] equal nil (cons _ _) --> false
[ ] equal (cons _ _) nil --> false
[ c : Char, s : String ] equal nil (cons c s) --> false
[ c : Char, s : String ] equal (cons c s) nil --> false
[ c1 : Char, s1 : String,
c2 : Char, s2 : String ]
equal (cons c1 s1) (cons c2 s2)
......@@ -35,8 +35,9 @@ eq_rect : s1 : String ->
eT (P s2).
[ s : String,
P : String -> uT,
x : eT (P s) ]
eq_rect s s P _ x --> x.
x : eT (P s),
H : Istrue true ]
eq_rect s s P H x --> x.
if_eq : P : (String -> uT) ->
s1 : String ->
......@@ -69,18 +70,18 @@ equal_sym : l1 : String ->
l2 : String ->
Istrue (equal l1 l2) ->
Istrue (equal l2 l1).
[ l : String ] equal_sym l l _ --> dk_logic.I.
[ l : String, H : Istrue true ] equal_sym l l H --> dk_logic.I.
diff_sym : l1 : String ->
l2 : String ->
Istrue (not (equal l1 l2)) ->
Istrue (not (equal l2 l1)).
[ c : Char, l : String ]
diff_sym (dk_string.cons c l) dk_string.nil _
l2 : String ->
Istrue (not (equal l1 l2)) ->
Istrue (not (equal l2 l1)).
[ c : Char, l : String, H : Istrue true ]
diff_sym (dk_string.cons c l) dk_string.nil H
-->
dk_logic.I
[ c : Char, l : String ]
diff_sym dk_string.nil (dk_string.cons c l) _
[ c : Char, l : String, H : Istrue true ]
diff_sym dk_string.nil (dk_string.cons c l) H
-->
dk_logic.I
[ c : Char,
......
......@@ -47,8 +47,9 @@ assoc : type -> Label -> type.
domain : type -> Domain.
[] domain nil --> domain_nil
[ l : Label,
A : type ]
domain (cons l _ A)
A : type,
B : type ]
domain (cons l B A)
-->
domain_cons l (domain A).
......@@ -68,8 +69,8 @@ eq : type -> type -> Bool.
(and
(eq A1 A2)
(eq B1 B2))
[] eq nil (cons _ _ _) --> false
[] eq (cons _ _ _) nil --> false.
[ l : Label, A : type, B : type ] eq nil (cons l A B) --> false
[ l : Label, A : type, B : type ] eq (cons l A B) nil --> false.
has_key : type -> Label -> Bool
:=
......@@ -79,8 +80,8 @@ has_key : type -> Label -> Bool
(; st A B := A <: B ;)
st : type -> type -> Bool.
[ A : type ] st A A --> true
[] st _ nil --> true
(; [ A : type ] st A A --> true ;)
[ A : type ] st A nil --> true
[ B1 : type,
l2 : Label,
A2 : type,
......@@ -96,7 +97,7 @@ if_diff : b : Bool ->
A : type ->
B : type ->
Istrue (eq (if b A B) B).
[ A : type, B : type ] if_diff false _ A B --> tt.
[ A : type, B : type, H : Istrue true ] if_diff false H A B --> tt.
eq_trans : A : type ->
B : type ->
......@@ -104,7 +105,7 @@ eq_trans : A : type ->
Istrue (eq A B) ->
Istrue (eq B C) ->
Istrue (eq A C).
[ A : type ] eq_trans A A A _ _ --> tt.
[ A : type, H1 : Istrue true, H2 : Istrue true ] eq_trans A A A H1 H2 --> tt.
assoc_subtype : A : type ->
B : type ->
......@@ -115,8 +116,10 @@ assoc_subtype : A : type ->
(assoc A l)).
[ A : type,
l : Label,
refl : Istrue true ]
assoc_subtype A A l refl _ --> tt
refl : Istrue (st A A),
H : Istrue (has_key A l)
]
assoc_subtype A A l refl H --> tt
[ l2 : Label,
A2 : type,
B2 : type,
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment