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

All obsolete #IMPORT and dot patterns removed

parent c928e27d
#NAME dk_builtins
(; This file defines basic types for the translation of FoCaLize
standard library into Dedukti ;)
#IMPORT cc
#IMPORT dk_tuple
#IMPORT dk_opt
#IMPORT dk_bool
Object : Type.
collection : cc.uT.
......@@ -15,27 +11,7 @@ unknown_type : cc.uT.
unknown_def : cc.eT unknown_type.
unknown_proof : cc.eT unknown_type.
(; String ;)
string : cc.uT.
string : cc.uT := dk_string.string.
some_string : cc.eT string.
(; Nat ;)
(; Nat is not a FoCaLize builtin type but it is usefull for the definition of Int ;)
#IMPORT dk_nat
(; Int ;)
#IMPORT dk_int
(; Binary naturals ;)
#IMPORT dk_binary_nat
(; Bounded binary naturals ;)
#IMPORT dk_machine_int
(; Prop ;)
#IMPORT dk_logic
prop : cc.uT := dk_logic.Prop.
#NAME dk_int
#IMPORT cc
#IMPORT dk_nat
N : Type := cc.eT dk_nat.Nat.
O : N := dk_nat.O.
S : N -> N := dk_nat.S.
#IMPORT dk_list
#IMPORT dk_bool
B : Type := cc.eT dk_bool.bool.
(; integers are defined by couples of naturals seen as their difference modulo the rule
......
......@@ -27,6 +27,14 @@ domain_cons := dk_list.cons label.
Typer := Label -> cc.uT.
record : f : Typer ->
D : Domain ->
cc.uT
:=
f : Typer =>
D : Domain =>
cc.Pi_TTT label f.
Record : f : Typer ->
D : Domain ->
Type
......
#NAME dk_monads
#IMPORT cc
#IMPORT dk_bool
istruetype : dk_bool.B -> cc.uT.
istrue : dk_bool.B -> Type := b : dk_bool.B => cc.eT (istruetype b).
I : istrue dk_bool.true.
......@@ -109,13 +106,13 @@ option_dep_case :
RET : cc.eT (option A) -> cc.uT,
None_case : cc.eT (RET (None A)),
Some_case : a : cc.eT A -> cc.eT (RET (Some A a))]
option_dep_case A RET None_case Some_case (None {A}) --> None_case
option_dep_case A RET None_case Some_case (None _) --> None_case
[A : cc.uT,
RET : cc.eT (option A) -> cc.uT,
None_case : cc.eT (RET (None A)),
Some_case : a : cc.eT A -> cc.eT (RET (Some A a)),
a : cc.eT A]
option_dep_case A RET None_case Some_case (Some {A} a) --> Some_case a.
option_dep_case A RET None_case Some_case (Some _ a) --> Some_case a.
option_case :
RET : cc.uT ->
......@@ -135,10 +132,10 @@ option_case :
[A : cc.uT,
B : cc.uT, f : cc.eT A -> cc.eT (option B)]
bind option A B (None {A}) f --> None B
bind option A B (None _) f --> None B
[A : cc.uT, a : cc.eT A,
B : cc.uT, f : cc.eT A -> cc.eT (option B)]
bind option A B (Some {A} a) f --> f a.
bind option A B (Some _ a) f --> f a.
(; Alternative definition of bind option leading to the same proofs :
......@@ -201,29 +198,28 @@ list_dep_case :
RET : cc.eT (list A) -> cc.uT,
Nil_case : cc.eT (RET (Nil A)),
Cons_case : a : cc.eT A -> l : cc.eT (list A) -> cc.eT (RET (Cons A a l))]
list_dep_case A RET Nil_case Cons_case (Nil {A}) --> Nil_case
list_dep_case A RET Nil_case Cons_case (Nil _) --> Nil_case
[A : cc.uT,
RET : cc.eT (list A) -> cc.uT,
Nil_case : cc.eT (RET (Nil A)),
Cons_case : a : cc.eT A -> l : cc.eT (list A) -> cc.eT (RET (Cons A a l)),
a : cc.eT A, l : cc.eT (list A)]
list_dep_case A RET Nil_case Cons_case (Cons {A} a l) --> Cons_case a l.
list_dep_case A RET Nil_case Cons_case (Cons _ a l) --> Cons_case a l.
append : A : cc.uT -> cc.eT (list A) -> cc.eT (list A) -> cc.eT (list A).
[A : cc.uT, l2 : cc.eT (list A)]
append A (Nil {A}) l2 --> l2
append A (Nil _) l2 --> l2
[A : cc.uT, a : cc.eT A, l1 : cc.eT (list A), l2 : cc.eT (list A)]
append A (Cons {A} a l1) l2 --> Cons A a (append A l1 l2)
append A (Cons _ a l1) l2 --> Cons A a (append A l1 l2)
(; Let's add a third rule to get append l Nil = l ;)
[A : cc.uT, l1 : cc.eT (list A)]
append A l1 (Nil {A}) --> l1.
append A l1 (Nil _) --> l1.
#IMPORT dk_tuple
[A : cc.uT,
a1 : cc.eT A, a2 : cc.eT A,
l1 : cc.eT (list A), l2 : cc.eT (list A)]
istruetype (equal (list A) (Cons {A} a1 l1) (Cons {A} a2 l2)) -->
istruetype (equal (list A) (Cons _ a1 l1) (Cons _ a2 l2)) -->
dk_tuple.Tuple
(istruetype (equal A a1 a2))
(istruetype (equal (list A) l1 l2)).
......@@ -234,10 +230,10 @@ append : A : cc.uT -> cc.eT (list A) -> cc.eT (list A) -> cc.eT (list A).
[A : cc.uT,
B : cc.uT, f : cc.eT A -> cc.eT (list B)]
bind list A B (Nil {A}) f --> Nil B
bind list A B (Nil _) f --> Nil B
[A : cc.uT, a : cc.eT A, l : cc.eT (list A),
B : cc.uT, f : cc.eT A -> cc.eT (list B)]
bind list A B (Cons {A} a l) f --> append B (f a) (bind list A B l f).
bind list A B (Cons _ a l) f --> append B (f a) (bind list A B l f).
[A : cc.uT, B : cc.uT, a : cc.eT A, f : cc.eT A -> cc.eT (list B)]
monad_neutral_left list A B a f --> refl (list B) (f a).
......
#NAME dk_opt
#IMPORT cc
(; options ;)
option : cc.uT -> cc.uT.
......@@ -26,11 +25,11 @@ simple_match_option : A : cc.uT ->
P : cc.eT (option A) -> cc.uT,
Hnone : cc.eT (P (None A)),
Hsome : a : cc.eT A -> cc.eT (P (Some A a))]
match_option {A} P Hnone Hsome (None A) --> Hnone
match_option A P Hnone Hsome (None _) --> Hnone
[A : cc.uT,
P : cc.eT (option A) -> cc.uT,
Hnone : cc.eT (P (None A)),
Hsome : a : cc.eT A -> cc.eT (P (Some A a)),
a : cc.eT A]
match_option {A} P Hnone Hsome (Some A a) --> Hsome a.
match_option A P Hnone Hsome (Some _ a) --> Hsome a.
#NAME dk_records
#IMPORT cc
(; Records as finite domain partial functions ;)
(; 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).
......@@ -23,16 +19,15 @@ axiom_label_eq_equal : l1 : Label ->
dk_logic.eP (dk_logic.equal label l1 l2).
(; Domains are lists of labels ;)
#IMPORT dk_list
domain := dk_list.list label.
Domain := cc.eT domain.
domain_nil := dk_list.nil label.
domain_cons := dk_list.cons label.
domain_mem : Label -> Domain -> Bool.
[ l : Label ] domain_mem l (dk_list.nil {label}) --> dk_bool.false
[ l : Label ] domain_mem l (dk_list.nil _) --> dk_bool.false
[ l1 : Label, l2 : Label, d : Domain ]
domain_mem l1 (dk_list.cons {label} l2 d)
domain_mem l1 (dk_list.cons _ l2 d)
-->
dk_bool.or (label_eq l2 l1) (domain_mem l1 d).
......@@ -51,7 +46,6 @@ domain_mem_cons : l2 : Label ->
(; partial functions ;)
(; partial functions from A to B can be seen as functions from A to option B ;)
#IMPORT dk_opt
option := dk_opt.option.
Option := A : cc.uT => cc.eT (option A).
......@@ -68,7 +62,7 @@ Partial := A : cc.uT =>
(; simple but a priori "unsafe" way to see a function from A to option B
as a function from A to B ;)
option_unsafe_get : A : cc.uT -> oA : Option A -> cc.eT A.
[ A : cc.uT, a : cc.eT A ] option_unsafe_get A (dk_opt.Some {A} a) --> a.
[ A : cc.uT, a : cc.eT A ] option_unsafe_get A (dk_opt.Some _ a) --> a.
unsafe_partial : A : cc.uT ->
B : (cc.eT A -> cc.uT) ->
f : Partial A B ->
......@@ -453,14 +447,14 @@ mk_record : f : Typer ->
c : Domain_match f D,
fun : Partial2 label f,
cert : dk_logic.eP (domain_mem_some2 f D fun c) ]
Record_fun {f} {D} {c} (mk_record f D c fun cert) --> fun.
Record_fun _ _ _ (mk_record f D c fun cert) --> fun.
[ f : Typer,
D : Domain,
c : Domain_match f D,
fun : Partial2 label f,
cert : dk_logic.eP (domain_mem_some2 f D fun c) ]
Record_cert {f} {D} {c} (mk_record f D c fun cert) --> cert.
Record_cert _ _ _ (mk_record f D c fun cert) --> cert.
Record_apply : f : Typer ->
D : Domain ->
......
#NAME dk_tuple
#IMPORT cc
Tuple : cc.uT -> cc.uT -> cc.uT.
cpl : A : cc.uT -> B : cc.uT -> cc.eT A -> cc.eT B -> cc.eT (Tuple A B).
fst : A : cc.uT -> B : cc.uT -> cc.eT (Tuple A B) -> cc.eT A.
snd : A : cc.uT -> B : cc.uT -> cc.eT (Tuple A B) -> cc.eT B.
[A : cc.uT, B : cc.uT, a : cc.eT A, b : cc.eT B] fst {A} {B} (cpl A B a b) --> a.
[A : cc.uT, B : cc.uT, a : cc.eT A, b : cc.eT B] snd {A} {B} (cpl A B a b) --> b.
[A : cc.uT, B : cc.uT, a : cc.eT A, b : cc.eT B] fst _ _ (cpl A B a b) --> a.
[A : cc.uT, B : cc.uT, a : cc.eT A, b : cc.eT B] snd _ _ (cpl A B a b) --> b.
dTuple : A : cc.uT -> (cc.eT A -> cc.uT) -> cc.uT.
dcpl : A : cc.uT -> B : (cc.eT A -> cc.uT) -> a : cc.eT A -> cc.eT (B a) -> cc.eT (dTuple A B).
dfst : A : cc.uT -> B : (cc.eT A -> cc.uT) -> cc.eT (dTuple A B) -> cc.eT A.
dsnd : A : cc.uT -> B : (cc.eT A -> cc.uT) -> t : cc.eT (dTuple A B) -> cc.eT (B (dfst A B t)).
[A : cc.uT, B : (cc.eT A -> cc.uT), a : cc.eT A, b : cc.eT (B a)] dfst {A} {B} (dcpl A B a b) --> a.
[A : cc.uT, B : (cc.eT A -> cc.uT), a : cc.eT A, b : cc.eT (B a)] dsnd {A} {B} (dcpl A B a b) --> b.
[A : cc.uT, B : (cc.eT A -> cc.uT), a : cc.eT A, b : cc.eT (B a)] dfst _ _ (dcpl A B a b) --> a.
[A : cc.uT, B : (cc.eT A -> cc.uT), a : cc.eT A, b : cc.eT (B a)] dsnd _ _ (dcpl A B a b) --> b.
......@@ -17,7 +17,7 @@ Method := Expr -> Expr.
object := cc.Arrow label method.
Object := Label -> Method.
empty_object : Label -> Method.
empty_object : Object.
update_object : Object -> Label -> Method -> Object
:= o : Object =>
l : Label =>
......@@ -337,9 +337,13 @@ classReCell :=
update empty contents (self : Expr => select classCell contents))
get (self : Expr => select classCell get))
set (self : Expr => lambda2 (s : Expr => lambda2 (n : Expr =>
apply2 (apply2 (select classCell set) (update s backup (self : Expr => select s contents))) n))))
apply2 (apply2
(select classCell set)
(update s backup (self : Expr => select s contents)))
n))))
backup (self : Expr => lambda2 (s : Expr => From_nat dk_nat.O)))
restore (self : Expr => lambda2 (s : Expr => update s contents (self : Expr => select s backup))))
restore (self : Expr => lambda2 (s : Expr =>
update s contents (self : Expr => select s backup))))
new (z : Expr =>
update (
update (
......
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