From 718811d873d1c6f2ff6fd40da19ce810899e1c9c Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Fri, 31 Jan 2020 08:08:22 +0100
Subject: [PATCH] restructuration
---
{prelude => adlib/core}/nat.lp | 2 +-
{prelude => adlib/core}/nat_ops.lp | 3 ++-
encodings/{cf.lp => cert_f.lp} | 14 +++++++-------
prelude/{cf => cert_f}/booleans.lp | 2 +-
prelude/{cf => cert_f}/equalities.lp | 0
prelude/{cf => cert_f}/int.lp | 0
prelude/{cf => cert_f}/naturalnumbers.lp | 0
prelude/{cf => cert_f}/notequal.lp | 0
prelude/{ => core}/boolean_props.lp | 3 ++-
prelude/{ => core}/booleans.lp | 2 +-
prelude/core/equalities.lp | 3 +++
prelude/core/if_def.lp | 4 ++++
prelude/core/notequal.lp | 3 +++
prelude/{ => core}/prelude.lp | 0
prelude/{ => core}/pvs_core.lp | 0
prelude/{ => core}/quantifier_props.lp | 2 +-
prelude/core/xor_def.lp | 3 +++
prelude/equalities.lp | 3 ---
prelude/if_def.lp | 3 ---
prelude/notequal.lp | 3 ---
prelude/xor_def.lp | 3 ---
prelude/rat_exp.lp => sandbox/core/rat.lp | 0
prelude/rat.lp => sandbox/core/rat_explicit.lp | 6 +++---
23 files changed, 31 insertions(+), 28 deletions(-)
rename {prelude => adlib/core}/nat.lp (77%)
rename {prelude => adlib/core}/nat_ops.lp (76%)
rename encodings/{cf.lp => cert_f.lp} (83%)
rename prelude/{cf => cert_f}/booleans.lp (69%)
rename prelude/{cf => cert_f}/equalities.lp (100%)
rename prelude/{cf => cert_f}/int.lp (100%)
rename prelude/{cf => cert_f}/naturalnumbers.lp (100%)
rename prelude/{cf => cert_f}/notequal.lp (100%)
rename prelude/{ => core}/boolean_props.lp (72%)
rename prelude/{ => core}/booleans.lp (94%)
create mode 100644 prelude/core/equalities.lp
create mode 100644 prelude/core/if_def.lp
create mode 100644 prelude/core/notequal.lp
rename prelude/{ => core}/prelude.lp (100%)
rename prelude/{ => core}/pvs_core.lp (100%)
rename prelude/{ => core}/quantifier_props.lp (83%)
create mode 100644 prelude/core/xor_def.lp
delete mode 100644 prelude/equalities.lp
delete mode 100644 prelude/if_def.lp
delete mode 100644 prelude/notequal.lp
delete mode 100644 prelude/xor_def.lp
rename prelude/rat_exp.lp => sandbox/core/rat.lp (100%)
rename prelude/rat.lp => sandbox/core/rat_explicit.lp (83%)
diff --git a/prelude/nat.lp b/adlib/core/nat.lp
similarity index 77%
rename from prelude/nat.lp
rename to adlib/core/nat.lp
index 0306c9d..11b1f7e 100644
--- a/prelude/nat.lp
+++ b/adlib/core/nat.lp
@@ -1,4 +1,4 @@
-require open pvs_core prelude.notequal
+require open encodings.pvs_core prelude.core.notequal
// Not part of prelude as integers are built in pvs
constant symbol int : Type
diff --git a/prelude/nat_ops.lp b/adlib/core/nat_ops.lp
similarity index 76%
rename from prelude/nat_ops.lp
rename to adlib/core/nat_ops.lp
index bdbaa55..b06f599 100644
--- a/prelude/nat_ops.lp
+++ b/adlib/core/nat_ops.lp
@@ -1,4 +1,5 @@
-require open pvs_core prelude.notequal prelude.nat prelude.equalities
+require open encodings.pvs_core prelude.core.notequal adlib.core.nat
+prelude.core.equalities
symbol times : eta int ⇒ eta int ⇒ eta int
rule times &n 1 → &n
diff --git a/encodings/cf.lp b/encodings/cert_f.lp
similarity index 83%
rename from encodings/cf.lp
rename to encodings/cert_f.lp
index 1770eea..bde178a 100644
--- a/encodings/cf.lp
+++ b/encodings/cert_f.lp
@@ -31,7 +31,7 @@ rule Term uProp → Univ Prop
symbol prod {s1 s2 : Sort} (A : Univ s1) :
(Term A ⇒ Univ s2) ⇒ Univ (Rule s1 s2)
-rule Term (prod &s1 &s2 &A &B) → ∀ x : Term &A, Term (&B x)
+rule Term (prod &A &B) → ∀ x : Term &A, Term (&B x)
// Predicate subtyping
// can be seen as a dependant pair type with
@@ -42,21 +42,21 @@ symbol psub (A : Univ Type) : (Term A ⇒ Univ Prop) ⇒ Univ Type
// Γ ⊢ M : { v : T | U }
// —————————————————————PROJl
// Γ ⊢ fst(M) : T
-symbol fst {T : Univ Type} {U : Term T ⇒ Univ Prop}: Term (psub T U) ⇒ Term T
+symbol fst {T : Univ Type} (U : Term T ⇒ Univ Prop): Term (psub T U) ⇒ Term T
// Γ ⊢ M : { v : T | U }
// ——————————————————————————PROJr
// Γ ⊢ snd(M) : U[v ≔ fst(M)]
-symbol snd (T: Univ Type) (U: Term T ⇒ Univ Prop) (M: Term (psub T U)):
- Term (U (@fst T U M))
+symbol snd {T: Univ Type} (U: Term T ⇒ Univ Prop) (M: Term (psub T U)):
+ Term (U (fst U M))
// An inhabitant of a predicate subtype, that is, a pair of
// an element and the proof that it satisfies the predicate
// Γ ⊢ M : T Γ ⊢ N : U[v ≔ M] Γ ⊢ { v : T | U }
// ——————————————————————————————————————————————————PAIR
// Γ ⊢ ⟨M, N⟩ : {v : T | U}
-symbol pair {T: Univ Type} (U: @Term Type T ⇒ Univ Prop) (M: @Term Type T):
+symbol pair {T: Univ Type} (U: Term T ⇒ Univ Prop) (M: Term T):
Term (U M) ⇒ Term (psub T U)
-rule @fst &T &U (@pair &T &U &M _) → &M
-rule @snd &T &U (@pair &T &U _ &P) → &P
+rule fst &U (pair &U &M _) → &M
+rule snd &U (pair &U _ &P) → &P
diff --git a/prelude/cf/booleans.lp b/prelude/cert_f/booleans.lp
similarity index 69%
rename from prelude/cf/booleans.lp
rename to prelude/cert_f/booleans.lp
index e0e80b6..68f2df9 100644
--- a/prelude/cf/booleans.lp
+++ b/prelude/cert_f/booleans.lp
@@ -1,7 +1,7 @@
require open encodings.cf
definition bool ≔ Prop
-definition false ≔ @prod Type Prop uProp (λ x : @Term Type uProp, x)
+definition false ≔ @prod Type Prop uProp (λ x : Term uProp, x)
definition true ≔ Term false ⇒ Term false
definition bnot (P: Term uProp) ≔ @prod Prop Prop P (λ x, false)
diff --git a/prelude/cf/equalities.lp b/prelude/cert_f/equalities.lp
similarity index 100%
rename from prelude/cf/equalities.lp
rename to prelude/cert_f/equalities.lp
diff --git a/prelude/cf/int.lp b/prelude/cert_f/int.lp
similarity index 100%
rename from prelude/cf/int.lp
rename to prelude/cert_f/int.lp
diff --git a/prelude/cf/naturalnumbers.lp b/prelude/cert_f/naturalnumbers.lp
similarity index 100%
rename from prelude/cf/naturalnumbers.lp
rename to prelude/cert_f/naturalnumbers.lp
diff --git a/prelude/cf/notequal.lp b/prelude/cert_f/notequal.lp
similarity index 100%
rename from prelude/cf/notequal.lp
rename to prelude/cert_f/notequal.lp
diff --git a/prelude/boolean_props.lp b/prelude/core/boolean_props.lp
similarity index 72%
rename from prelude/boolean_props.lp
rename to prelude/core/boolean_props.lp
index 120c143..aca40ad 100644
--- a/prelude/boolean_props.lp
+++ b/prelude/core/boolean_props.lp
@@ -1,4 +1,5 @@
-require open pvs_core prelude.booleans prelude.equalities prelude.if_def
+require open encodings.pvs_core
+prelude.core.booleans prelude.core.equalities prelude.core.if_def
// true /= false
symbol bool_inclusive : eps (bnot (eq bool false true))
diff --git a/prelude/booleans.lp b/prelude/core/booleans.lp
similarity index 94%
rename from prelude/booleans.lp
rename to prelude/core/booleans.lp
index 3fee8c9..e0ef4aa 100644
--- a/prelude/booleans.lp
+++ b/prelude/core/booleans.lp
@@ -1,4 +1,4 @@
-require open pvs_core
+require open encodings.pvs_core
set builtin "T" ≔ eta
set builtin "P" ≔ eps
diff --git a/prelude/core/equalities.lp b/prelude/core/equalities.lp
new file mode 100644
index 0000000..863cc7d
--- /dev/null
+++ b/prelude/core/equalities.lp
@@ -0,0 +1,3 @@
+require open encodings.pvs_core prelude.core.booleans
+
+symbol eq {T : Type} : eta T ⇒ eta T ⇒ eta bool
diff --git a/prelude/core/if_def.lp b/prelude/core/if_def.lp
new file mode 100644
index 0000000..ede0300
--- /dev/null
+++ b/prelude/core/if_def.lp
@@ -0,0 +1,4 @@
+require open encodings.pvs_core prelude.core.booleans prelude.core.equalities
+prelude.core.notequal
+
+symbol if (T:Type): eta bool ⇒ eta T ⇒ eta T ⇒ eta T
diff --git a/prelude/core/notequal.lp b/prelude/core/notequal.lp
new file mode 100644
index 0000000..1248661
--- /dev/null
+++ b/prelude/core/notequal.lp
@@ -0,0 +1,3 @@
+require open encodings.pvs_core prelude.core.booleans prelude.core.equalities
+
+definition neq {T: Type} (x: eta T) (y: eta T) ≔ bnot (eq x y)
diff --git a/prelude/prelude.lp b/prelude/core/prelude.lp
similarity index 100%
rename from prelude/prelude.lp
rename to prelude/core/prelude.lp
diff --git a/prelude/pvs_core.lp b/prelude/core/pvs_core.lp
similarity index 100%
rename from prelude/pvs_core.lp
rename to prelude/core/pvs_core.lp
diff --git a/prelude/quantifier_props.lp b/prelude/core/quantifier_props.lp
similarity index 83%
rename from prelude/quantifier_props.lp
rename to prelude/core/quantifier_props.lp
index 5cf168a..85c51a9 100644
--- a/prelude/quantifier_props.lp
+++ b/prelude/core/quantifier_props.lp
@@ -1,4 +1,4 @@
-require open pvs_core prelude.booleans prelude.equalities
+require open encodings.pvs_core prelude.core.booleans prelude.core.equalities
definition exists (T: Type) (p : eta T ⇒ eta bool) ≔
(bnot (all T (λ x, (bnot (p x)))))
diff --git a/prelude/core/xor_def.lp b/prelude/core/xor_def.lp
new file mode 100644
index 0000000..0ef5318
--- /dev/null
+++ b/prelude/core/xor_def.lp
@@ -0,0 +1,3 @@
+require open encodings.pvs_core prelude.core.booleans prelude.core.notequal
+
+definition xor (A : eta bool) (B : eta bool) ≔ neq bool A B
diff --git a/prelude/equalities.lp b/prelude/equalities.lp
deleted file mode 100644
index 9ad3b3f..0000000
--- a/prelude/equalities.lp
+++ /dev/null
@@ -1,3 +0,0 @@
-require open pvs_core prelude.booleans
-
-symbol eq {T : Type} : eta T ⇒ eta T ⇒ eta bool
diff --git a/prelude/if_def.lp b/prelude/if_def.lp
deleted file mode 100644
index 9e6b18b..0000000
--- a/prelude/if_def.lp
+++ /dev/null
@@ -1,3 +0,0 @@
-require open pvs_core prelude.booleans prelude.equalities prelude.notequal
-
-symbol if (T:Type): eta bool ⇒ eta T ⇒ eta T ⇒ eta T
diff --git a/prelude/notequal.lp b/prelude/notequal.lp
deleted file mode 100644
index abf4f86..0000000
--- a/prelude/notequal.lp
+++ /dev/null
@@ -1,3 +0,0 @@
-require open pvs_core prelude.booleans prelude.equalities
-
-definition neq {T: Type} (x: eta T) (y: eta T) ≔ bnot (eq x y)
diff --git a/prelude/xor_def.lp b/prelude/xor_def.lp
deleted file mode 100644
index 449e701..0000000
--- a/prelude/xor_def.lp
+++ /dev/null
@@ -1,3 +0,0 @@
-require open pvs_core prelude.booleans prelude.notequal
-
-definition xor (A : eta bool) (B : eta bool) ≔ neq bool A B
diff --git a/prelude/rat_exp.lp b/sandbox/core/rat.lp
similarity index 100%
rename from prelude/rat_exp.lp
rename to sandbox/core/rat.lp
diff --git a/prelude/rat.lp b/sandbox/core/rat_explicit.lp
similarity index 83%
rename from prelude/rat.lp
rename to sandbox/core/rat_explicit.lp
index 5afd078..4a03b1d 100644
--- a/prelude/rat.lp
+++ b/sandbox/core/rat_explicit.lp
@@ -1,6 +1,6 @@
-require open pvs_core prelude.booleans prelude.equalities prelude.notequal
-prelude.nat
-require prelude.nat_ops as N
+require open encodings.pvs_core prelude.core.booleans prelude.core.equalities
+prelude.core.notequal adlib.core.nat
+require adlib.core.nat_ops as N
constant symbol rat : Type
constant symbol zero : η rat
--
GitLab