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

Dot patterns and imports are obsolete

parent 64ae7bdd
......@@ -22,4 +22,4 @@ Pi_TAA : A : uT -> X : uT -> ((eT X) -> (eT A))
-> (eT A).
[A : uT, X : uT, Y : (eT X) -> (eT A)]
ee A (Pi_TAA {A} X Y) --> Pi_TTT X (x : eT X => ee A (Y x)).
ee A (Pi_TAA _ X Y) --> Pi_TTT X (x : eT X => ee A (Y x)).
#NAME dk_binary_nat
#IMPORT cc
#IMPORT dk_nat
UNat : Type := cc.eT dk_nat.Nat.
#IMPORT dk_bool
B : Type := cc.eT dk_bool.bool.
BNat : cc.uT.
......
#NAME dk_bool
#IMPORT cc
(; B ;)
(; Declaration ;)
......
#NAME dk_char
(; 7bits (ascii) characters ;)
#IMPORT cc
#IMPORT dk_nat
#IMPORT dk_binary_nat
#IMPORT dk_machine_int
char : cc.uT := dk_machine_int.Mint dk_nat.__7.
Char := cc.eT char.
_O : dk_binary_nat.N := dk_binary_nat.O.
......@@ -80,5 +75,4 @@ z : Char := cast (S0 (S1 (S0 (S1 (S1 (S1 (S1 _O))))))).
__ : Char := cast (S1 (S0 (S1 (S1 (S1 (S1 (S1 _O))))))).
#IMPORT dk_bool
equal : Char -> Char -> cc.eT dk_bool.bool := dk_machine_int.equal dk_nat.__7.
#NAME dk_list
#IMPORT cc
#IMPORT dk_logic
(; Polymorphic lists ;)
list : cc.uT -> cc.uT.
......@@ -22,7 +20,7 @@ match : A : cc.uT ->
P : List A -> cc.uT,
Hnil : cc.eT (P (nil A)),
Hcons : a : cc.eT A -> l : List A -> cc.eT (P (cons A a l))]
match {A} P Hnil Hcons (nil A) --> Hnil
match _ P Hnil Hcons (nil A) --> Hnil
[A : cc.uT,
P : List A -> cc.uT,
......@@ -30,7 +28,7 @@ match : A : cc.uT ->
Hcons : a : cc.eT A -> l : List A -> cc.eT (P (cons A a l)),
a : cc.eT A,
l : List A]
match {A} P Hnil Hcons (cons A a l) --> Hcons a l.
match _ P Hnil Hcons (cons A a l) --> Hcons a l.
(; Non dependant case distinction ;)
simple_match : A : cc.uT ->
......@@ -47,11 +45,11 @@ simple_match : A : cc.uT ->
(; Append ;)
append : A : cc.uT -> List A -> List A -> List A.
[ A : cc.uT, l2 : List A ]
append A (nil A) l2 --> l2
append A (nil _) l2 --> l2
[ A : cc.uT, a1 : cc.eT A, l1 : List A, l2 : List A ]
append A (cons A a1 l1) l2 --> cons A a1 (append A l1 l2)
append A (cons _ a1 l1) l2 --> cons A a1 (append A l1 l2)
[ A : cc.uT, l1 : List A, l2 : List A, l3 : List A]
append A l1 (append A l2 l3) --> append A (append A l1 l2) l3.
append A l1 (append _ l2 l3) --> append A (append A l1 l2) l3.
(; Map ;)
map : A : cc.uT ->
......@@ -59,18 +57,18 @@ map : A : cc.uT ->
(cc.eT A -> cc.eT B) -> List A -> List B.
[A : cc.uT,
B : cc.uT,
f : cc.eT A -> cc.eT B] map A B f (nil {A}) --> nil B
f : cc.eT A -> cc.eT B] map A B f (nil _) --> nil B
[A : cc.uT,
B : cc.uT,
f : cc.eT A -> cc.eT B,
a : cc.eT A,
l : cc.eT (list A)] map A B f (cons {A} a l) --> cons B (f a) (map A B f l)
l : cc.eT (list A)] map A B f (cons _ a l) --> cons B (f a) (map A B f l)
[A : cc.uT,
B : cc.uT,
C : cc.uT,
f : cc.eT A -> cc.eT B,
g : cc.eT B -> cc.eT C,
l : cc.eT (list A)] map {B} C g (map A B f l) --> map A C (x : cc.eT A => g (f x)) l.
l : cc.eT (list A)] map _ C g (map A B f l) --> map A C (x : cc.eT A => g (f x)) l.
mem : A : cc.uT ->
(cc.eT A -> cc.eT A -> cc.eT dk_bool.bool) ->
......@@ -78,9 +76,9 @@ mem : A : cc.uT ->
List A ->
cc.eT dk_bool.bool.
[ A : cc.uT, eq : cc.eT A -> cc.eT A -> cc.eT dk_bool.bool, a : cc.eT A ]
mem A eq a (nil {A}) --> dk_bool.false
mem A eq a (nil _) --> dk_bool.false
[ A : cc.uT, eq : cc.eT A -> cc.eT A -> cc.eT dk_bool.bool, a1 : cc.eT A, a2 : cc.eT A, l : cc.eT (list A) ]
mem A eq a1 (cons {A} a2 l) --> dk_bool.or (eq a1 a2) (mem A eq a1 l).
mem A eq a1 (cons _ a2 l) --> dk_bool.or (eq a1 a2) (mem A eq a1 l).
......@@ -89,11 +87,11 @@ map_id :
l : cc.eT (list B) ->
dk_logic.eP (dk_logic.equal (list B) (map B B (x : cc.eT B => x) l) l).
[B : cc.uT]
map_id {B} (nil B) --> dk_logic.refl (list B) (nil B)
map_id _ (nil B) --> dk_logic.refl (list B) (nil B)
[A : cc.uT,
a : cc.eT A,
l : cc.eT (list A)]
map_id {A} (cons A a l) --> dk_logic.equal_congr (list A) (list A) (cons A a) (map A A (x : cc.eT A => x) l) l (map_id A l).
map_id _ (cons A a l) --> dk_logic.equal_congr (list A) (list A) (cons A a) (map A A (x : cc.eT A => x) l) l (map_id A l).
dlist : A : cc.uT -> cc.eT A -> cc.uT.
......
#NAME dk_logic
#IMPORT cc
#IMPORT dk_bool
Prop : cc.uT.
P : Type := cc.eT Prop.
......@@ -41,10 +39,10 @@ and_elim2 : f1 : P ->
(; cut elimination ;)
[f1 : P, f2 : P,
H1 : eP f1, H2 : eP f2]
and_elim1 {f1} {f2} (and_intro f1 f2 H1 H2) --> H1.
and_elim1 _ _ (and_intro f1 f2 H1 H2) --> H1.
[f1 : P, f2 : P,
H1 : eP f1, H2 : eP f2]
and_elim2 {f1} {f2} (and_intro f1 f2 H1 H2) --> H2.
and_elim2 _ _ (and_intro f1 f2 H1 H2) --> H2.
eqv_intro := f1 : P =>
f2 : P =>
......
......@@ -6,12 +6,10 @@
A -> option B. ;)
(; Labels are strings ;)
#IMPORT dk_string
label : cc.uT := dk_string.string.
Label := cc.eT label.
#IMPORT dk_logic
#IMPORT dk_bool
bool := dk_bool.bool.
Bool := cc.eT bool.
istrue := b : Bool => dk_logic.eeP (dk_logic.ebP b).
......@@ -20,7 +18,6 @@ Istrue := b : Bool => cc.eT (istrue b).
label_eq : Label -> Label -> Bool := dk_string.equal.
(; Domains are lists of labels ;)
#IMPORT dk_list
domain := dk_list.list label.
Domain := cc.eT domain.
domain_nil := dk_list.nil label.
......@@ -77,7 +74,7 @@ Assoc_list_domain : Assoc_list -> Domain := dk_list.map triple label fst.
assoc_type : Assoc_list -> Label -> cc.uT.
[ l1 : Label, A : cc.uT, a : cc.eT A,
L : Assoc_list, l2 : Label ]
assoc_type (dk_list.cons {triple} (mk_triple l1 A a) L) l2 -->
assoc_type (dk_list.cons _ (mk_triple l1 A a) L) l2 -->
dk_bool.ite cc.uuT
(label_eq l1 l2)
A
......@@ -86,7 +83,7 @@ assoc_type : Assoc_list -> Label -> cc.uT.
assoc_val : L : Assoc_list -> l : Label -> cc.eT (assoc_type L l).
[ l1 : Label, A : cc.uT, a : cc.eT A,
L : Assoc_list, l2 : Label ]
assoc_val (dk_list.cons {triple} (mk_triple l1 A a) L) l2 -->
assoc_val (dk_list.cons _ (mk_triple l1 A a) L) l2 -->
dk_bool.match
(b : Bool => dk_bool.ite cc.uuT b A (assoc_type L l2))
a
......
#NAME dk_machine_int
#IMPORT cc
#IMPORT dk_bool
B : Type := cc.eT dk_bool.bool.
#IMPORT dk_nat
UNat : Type := cc.eT dk_nat.Nat.
UO : UNat := dk_nat.O.
US : UNat -> UNat := dk_nat.S.
......@@ -25,34 +22,34 @@ bound : N : UNat -> MInt N.
(; cast ;)
downcast : N : UNat -> MInt (US N) -> MInt N.
[n : MInt (US UO)] downcast {UO} n --> O
[N : UNat, n : MInt (US N)] downcast {US N} (S0 (dk_nat.S N) n) --> S0 N (downcast N n)
[N : UNat, n : MInt (US N)] downcast {US N} (S1 (dk_nat.S N) n) --> S1 N (downcast N n).
[n : MInt (US UO)] downcast _ n --> O
[N : UNat, n : MInt (US N)] downcast _ (S0 (dk_nat.S N) n) --> S0 N (downcast N n)
[N : UNat, n : MInt (US N)] downcast _ (S1 (dk_nat.S N) n) --> S1 N (downcast N n).
double : N : UNat -> MInt N -> MInt N
:= N : UNat => n : MInt N => downcast N (S0 N n).
succ : N : UNat -> MInt N -> MInt N.
[] succ {UO} O --> O
[ N : UNat, n : MInt N ] succ {US N} (S0 N n) --> S1 N n
[ N : UNat, n : MInt N ] succ {US N} (S1 N n) --> S0 N (succ N n).
[] succ _ O --> O
[ N : UNat, n : MInt N ] succ _ (S0 N n) --> S1 N n
[ N : UNat, n : MInt N ] succ _ (S1 N n) --> S0 N (succ N n).
pred : N : UNat -> MInt N -> MInt N.
[] pred {UO} O --> O
[ N : UNat, n : MInt N ] pred {US N} (S1 N n) --> S0 N n
[ N : UNat, n : MInt N ] pred {US N} (S0 N n) --> S1 N (pred N n).
[] pred _ O --> O
[ N : UNat, n : MInt N ] pred _ (S1 N n) --> S0 N n
[ N : UNat, n : MInt N ] pred _ (S0 N n) --> S1 N (pred N n).
plus : N : UNat -> MInt N -> MInt N -> MInt N.
[ ] plus {UO} O O --> O
[ N : UNat, n : MInt N, m : MInt N ] plus {US N} (S0 {N} n) (S0 N m) --> S0 N (plus N n m)
[ N : UNat, n : MInt N, m : MInt N ] plus {US N} (S0 {N} n) (S1 N m) --> S1 N (plus N n m)
[ N : UNat, n : MInt N, m : MInt N ] plus {US N} (S1 {N} n) (S0 N m) --> S1 N (plus N n m)
[ N : UNat, n : MInt N, m : MInt N ] plus {US N} (S1 {N} n) (S1 N m) --> S0 N (succ N (plus N n m)).
[ ] plus _ O O --> O
[ N : UNat, n : MInt N, m : MInt N ] plus _ (S0 _ n) (S0 N m) --> S0 N (plus N n m)
[ N : UNat, n : MInt N, m : MInt N ] plus _ (S0 _ n) (S1 N m) --> S1 N (plus N n m)
[ N : UNat, n : MInt N, m : MInt N ] plus _ (S1 _ n) (S0 N m) --> S1 N (plus N n m)
[ N : UNat, n : MInt N, m : MInt N ] plus _ (S1 _ n) (S1 N m) --> S0 N (succ N (plus N n m)).
complement : N : UNat -> MInt N -> MInt N.
[] complement {UO} O --> O
[ N : UNat, n : MInt N ] complement {US N} (S0 N n) --> S1 N (complement N n)
[ N : UNat, n : MInt N ] complement {US N} (S1 N n) --> S0 N (complement N n).
[] complement _ O --> O
[ N : UNat, n : MInt N ] complement _ (S0 N n) --> S1 N (complement N n)
[ N : UNat, n : MInt N ] complement _ (S1 N n) --> S0 N (complement N n).
opp : N : UNat -> MInt N -> MInt N.
[ N : UNat, n : MInt N ] opp N n --> succ N (complement N n).
......@@ -62,42 +59,42 @@ sub : N : UNat -> MInt N -> MInt N -> MInt N.
(; Product ;)
mult : N : UNat -> MInt N -> MInt N -> MInt N.
[] mult {UO} O O --> O
[ N : UNat, n : MInt N, m : MInt N ] mult {US N} (S0 {N} n) (S0 N m) --> double (US N) (S0 N (mult N n m))
[ N : UNat, n : MInt N, m : MInt N ] mult {US N} (S0 {N} n) (S1 N m) --> S0 N (plus N m (double N (mult N n m)))
[ N : UNat, n : MInt N, m : MInt N ] mult {US N} (S1 {N} n) (S0 N m) --> S0 N (plus N n (double N (mult N n m)))
[ N : UNat, n : MInt N, m : MInt N ] mult {US N} (S1 {N} n) (S1 N m) --> S1 N (plus N (double N (mult N m n)) (plus N n m)).
[] mult _ O O --> O
[ N : UNat, n : MInt N, m : MInt N ] mult _ (S0 _ n) (S0 N m) --> double (US N) (S0 N (mult N n m))
[ N : UNat, n : MInt N, m : MInt N ] mult _ (S0 _ n) (S1 N m) --> S0 N (plus N m (double N (mult N n m)))
[ N : UNat, n : MInt N, m : MInt N ] mult _ (S1 _ n) (S0 N m) --> S0 N (plus N n (double N (mult N n m)))
[ N : UNat, n : MInt N, m : MInt N ] mult _ (S1 _ n) (S1 N m) --> S1 N (plus N (double N (mult N m n)) (plus N n m)).
(; equality ;)
equal : N : UNat -> MInt N -> MInt N -> B.
[] equal dk_nat.O O O --> dk_bool.true
[ N : UNat, n : MInt N, m : MInt N ] equal {US N} (S0 {N} n) (S0 N m) --> equal N n m
[ N : UNat, n : MInt N, m : MInt N ] equal {US N} (S1 {N} n) (S1 N m) --> equal N n m
[ N : UNat, n : MInt N, m : MInt N ] equal {US N} (S0 {N} n) (S1 N m) --> dk_bool.false
[ N : UNat, n : MInt N, m : MInt N ] equal {US N} (S1 {N} n) (S0 N m) --> dk_bool.false.
[ 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.
(; unsigned comparison ;)
unsigned_lt : N : UNat -> MInt N -> MInt N -> B.
unsigned_leq : N : UNat -> MInt N -> MInt N -> B.
[] unsigned_lt {UO} O O --> dk_bool.false
[ N : UNat, n : MInt N, m : MInt N ] unsigned_lt {US N} (S0 {N} n) (S0 N m) -->
[] unsigned_lt _ O O --> dk_bool.false
[ N : UNat, n : MInt N, m : MInt N ] unsigned_lt _ (S0 _ n) (S0 N m) -->
unsigned_lt N n m
[ N : UNat, n : MInt N, m : MInt N ] unsigned_lt {US N} (S1 {N} n) (S1 N m) -->
[ N : UNat, n : MInt N, m : MInt N ] unsigned_lt _ (S1 _ n) (S1 N m) -->
unsigned_lt N n m
[ N : UNat, n : MInt N, m : MInt N ] unsigned_lt {US N} (S0 {N} n) (S1 N m) -->
[ N : UNat, n : MInt N, m : MInt N ] unsigned_lt _ (S0 _ n) (S1 N m) -->
unsigned_leq N n m
[ N : UNat, n : MInt N, m : MInt N ] unsigned_lt {US N} (S1 {N} n) (S0 N m) -->
[ N : UNat, n : MInt N, m : MInt N ] unsigned_lt _ (S1 _ n) (S0 N m) -->
unsigned_lt N n m.
[] unsigned_leq {UO} O O --> dk_bool.true
[ N : UNat, n : MInt N, m : MInt N ] unsigned_leq {US N} (S0 {N} n) (S0 N m) -->
[] unsigned_leq _ O O --> dk_bool.true
[ N : UNat, n : MInt N, m : MInt N ] unsigned_leq _ (S0 _ n) (S0 N m) -->
unsigned_leq N n m
[ N : UNat, n : MInt N, m : MInt N ] unsigned_leq {US N} (S1 {N} n) (S1 N m) -->
[ N : UNat, n : MInt N, m : MInt N ] unsigned_leq _ (S1 _ n) (S1 N m) -->
unsigned_leq N n m
[ N : UNat, n : MInt N, m : MInt N ] unsigned_leq {US N} (S0 {N} n) (S1 N m) -->
[ N : UNat, n : MInt N, m : MInt N ] unsigned_leq _ (S0 _ n) (S1 N m) -->
unsigned_leq N n m
[ N : UNat, n : MInt N, m : MInt N ] unsigned_leq {US N} (S1 {N} n) (S0 N m) -->
[ N : UNat, n : MInt N, m : MInt N ] unsigned_leq _ (S1 _ n) (S0 N m) -->
unsigned_lt N n m.
unsigned_gt : N : UNat -> MInt N -> MInt N -> B
......@@ -108,11 +105,11 @@ unsigned_geq : N : UNat -> MInt N -> MInt N -> B
(; signed comparison ;)
positive : N : UNat -> MInt N -> B.
[] positive {UO} O --> dk_bool.true
[] positive {US UO} (S0 {UO} O) --> dk_bool.true
[] positive {US UO} (S1 {UO} O) --> dk_bool.false
[ N : UNat, n : MInt N ] positive {US N} (S0 N n) --> positive N n
[ N : UNat, n : MInt N ] positive {US N} (S1 N n) --> positive N n.
[] positive _ O --> dk_bool.true
[] positive _ (S0 _ O) --> dk_bool.true
[] positive _ (S1 _ O) --> dk_bool.false
[ N : UNat, n : MInt N ] positive _ (S0 N n) --> positive N n
[ N : UNat, n : MInt N ] positive _ (S1 N n) --> positive N n.
signed_leq : N : UNat -> n : MInt N -> m : MInt N -> B
:= N : UNat => n : MInt N => m : MInt N =>
......@@ -137,7 +134,7 @@ cast_peano : N : UNat -> n : UNat -> MInt N.
[ N : UNat, n : UNat ] cast_peano N (dk_nat.S n) --> succ N (cast_peano N n).
(; Casting binary natural numbers ;)
#IMPORT dk_binary_nat
cast_bnat : N : UNat -> bn : dk_binary_nat.N -> MInt N.
[ N : UNat ] cast_bnat N dk_binary_nat.O --> zero N
[ bn : dk_binary_nat.N ] cast_bnat dk_nat.O bn --> O.
......
......@@ -284,5 +284,5 @@ append : A : cc.uT -> cc.eT (list A) -> cc.eT (list A) -> cc.eT (list A).
(refl (list C) (Nil C))
(a : cc.eT A =>
l : cc.eT (list A) =>
refl (list C) (bind list B C (f a) g))
refl (list C) (bind list B C (append B (f a) (bind list A B l f)) g))
m.
#NAME dk_nat
#IMPORT cc
#IMPORT dk_list
#IMPORT dk_bool
B : Type := cc.eT dk_bool.bool.
Nat : cc.uT.
......
#NAME dk_string
(; lists of ascii characters ;)
#IMPORT cc
#IMPORT dk_list
#IMPORT dk_char
string : cc.uT := dk_list.list dk_char.char.
#IMPORT dk_bool
equal : cc.eT string -> cc.eT string -> cc.eT dk_bool.bool.
[]
equal (dk_list.nil {dk_char.char}) (dk_list.nil {dk_char.char})
--> dk_bool.true
[] equal (dk_list.nil _) (dk_list.nil _) --> dk_bool.true
[ c : cc.eT dk_char.char, s : cc.eT string ]
equal (dk_list.nil {dk_char.char}) (dk_list.cons {dk_char.char} c s)
--> dk_bool.false
equal (dk_list.nil _) (dk_list.cons _ c s) --> dk_bool.false
[ c : cc.eT dk_char.char, s : cc.eT string ]
equal (dk_list.cons {dk_char.char} c s) (dk_list.nil {dk_char.char})
--> dk_bool.false
equal (dk_list.cons _ c s) (dk_list.nil _) --> dk_bool.false
[ c1 : cc.eT dk_char.char, s1 : cc.eT string, c2 : cc.eT dk_char.char, s2 : cc.eT string]
equal (dk_list.cons {dk_char.char} c1 s1) (dk_list.cons {dk_char.char} c2 s2)
equal (dk_list.cons _ c1 s1) (dk_list.cons _ c2 s2)
--> dk_bool.and (dk_char.equal c1 c2) (equal s1 s2).
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